IndisputableMonolith.Foundation.UniversalForcing.ForcedSemiring

declarations in this module (17)

• theorem map_preserves_add L40
• theorem map_preserves_mul L56
• theorem map_preserves_one L71
• def forcingFn L82
• theorem forcingFn_zero L86
• theorem forcingFn_succ L90
• theorem forcingFn_add L95
• theorem forcingFn_mul L101
• theorem forcingFn_one L107
• theorem forcingFn_bijective L113
• theorem forcingFn_unique L121
• structure ForcedSemiringCert L132
• def forcedSemiringCert_holds L145
• theorem forcingFn_eq_id L163
• theorem toNat_one L169
• structure ForcedArithmeticIsNat L177
• def forcedArithmeticIsNat L185