module module

`IndisputableMonolith.Foundation.ArithmeticOf`

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

used by (1)

From the project-wide theorem graph. These declarations reference this one in their body.

IndisputableMonolith.Foundation.UniversalForcing module_import

depends on (2)

Lean names referenced from this declaration's body.

IndisputableMonolith.Foundation.ArithmeticFromLogic module_import
IndisputableMonolith.Foundation.LogicRealization module_import

declarations in this module (22)

structure PeanoObject L23
structure Hom L31
def id L42
def comp L48
structure IsInitial L58
structure ArithmeticOf L65
structure PeanoSurface L72
def logicNatPeano L84
def logicNatFold L90
def logicNatLift L95
theorem logicNatLift_unique_fun L102
def logicNat_initial L116
def realizationPeano L123
def realizationFold L130
def realizationLift L134
theorem realizationLift_unique_fun L150
def realization_initial L189
def extracted L197
theorem extracted_peanoSurface L202
def equivOfInitial L209
def canonical L237
theorem canonical_peanoSurface L242