structure definition def or abbrev

`PeanoObject`

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

formal statement (Lean)

  23structure PeanoObject where
  24  carrier : Type u
  25  zero : carrier
  26  step : carrier → carrier
  27
  28namespace PeanoObject
  29
  30/-- Homomorphisms of Peano algebras. -/

used by (20)

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

ArithmeticOf in IndisputableMonolith.Foundation.ArithmeticOf decl_use
comp in IndisputableMonolith.Foundation.ArithmeticOf decl_use
equivOfInitial in IndisputableMonolith.Foundation.ArithmeticOf decl_use
Hom in IndisputableMonolith.Foundation.ArithmeticOf decl_use
id in IndisputableMonolith.Foundation.ArithmeticOf decl_use
IsInitial in IndisputableMonolith.Foundation.ArithmeticOf decl_use
logicNatFold in IndisputableMonolith.Foundation.ArithmeticOf decl_use
logicNat_initial in IndisputableMonolith.Foundation.ArithmeticOf decl_use
logicNatLift in IndisputableMonolith.Foundation.ArithmeticOf decl_use
logicNatLift_unique_fun in IndisputableMonolith.Foundation.ArithmeticOf decl_use
logicNatPeano in IndisputableMonolith.Foundation.ArithmeticOf decl_use
realizationFold in IndisputableMonolith.Foundation.ArithmeticOf decl_use
realization_initial in IndisputableMonolith.Foundation.ArithmeticOf decl_use
realizationLift in IndisputableMonolith.Foundation.ArithmeticOf decl_use
realizationLift_unique_fun in IndisputableMonolith.Foundation.ArithmeticOf decl_use
realizationPeano in IndisputableMonolith.Foundation.ArithmeticOf decl_use
categoryInterfaceOfLawvere in IndisputableMonolith.Foundation.CategoricalLogicRealization decl_use
LawvereNNO in IndisputableMonolith.Foundation.CategoricalLogicRealization decl_use
isInitial in IndisputableMonolith.Foundation.UniversalForcing.NaturalNumberObject decl_use
toPeano in IndisputableMonolith.Foundation.UniversalForcing.NaturalNumberObject decl_use

depends on (8)

Lean names referenced from this declaration's body.

of in IndisputableMonolith.Astrophysics.NucleosynthesisTiers decl_use
step in IndisputableMonolith.Complexity.CellularAutomata decl_use
carrier in IndisputableMonolith.Engineering.CorticalNeuromodulationDevice decl_use
carrier in IndisputableMonolith.Engineering.PhantomCoupledGWAntennaSensitivity decl_use
of in IndisputableMonolith.Foundation.DAlembert.LedgerFactorization decl_use
of in IndisputableMonolith.Foundation.PhiForcingDerived decl_use
of in IndisputableMonolith.Foundation.SpectralEmergence decl_use
of in IndisputableMonolith.Information.PhysicsComplexityStructure decl_use