module module

`IndisputableMonolith.Foundation.UniversalForcing.ForcedIntegers`

show as: view Lean formalization →

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

generate prose now

depends on (1)

Lean names referenced from this declaration's body.

IndisputableMonolith.Foundation.UniversalForcing.ForcedSemiring module_import

declarations in this module (13)

def toInt L46
theorem toInt_zero L48
theorem toInt_one L50
theorem toInt_add L55
theorem toInt_mul L61
theorem toInt_injective L67
theorem toInt_nonneg L74
theorem integers_surject L83
theorem forced_difference_zero_iff L93
theorem forced_difference_neg_swap L103
theorem forced_difference_fixed_iff L111
structure ForcedIntegersCert L127
def forcedIntegersCert_holds L139