module module

`IndisputableMonolith.Foundation.UniversalForcing.CanonicalSemiringIso`

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.CanonicalIso module_import

declarations in this module (15)

def foldHom L55
theorem foldHom_toFun L61
theorem fold_iso_compat L69
def forcedZero L84
def forcedOne L89
def forcedAdd L94
def forcedMul L99
def forcedLe L104
theorem iso_map_forcedZero L111
theorem iso_map_forcedOne L117
theorem iso_map_forcedAdd L124
theorem iso_map_forcedMul L134
theorem iso_map_forcedLe L144
structure ForcedOrderedSemiringIsoCert L160
def forcedOrderedSemiringIsoCert L179