No prose has been written for this declaration yet. The Lean source and graph data below render
without it.
generate prose now
formal statement (Lean)
62def toPeano (_h : IsNaturalNumberObject z s) : PeanoObject where
63 carrier := N
proof body
Definition body.
64 zero := z
65 step := s
66
67/-- Initiality of an NNO in the category of pointed endomap algebras. -/
used by (1)
From the project-wide theorem graph. These declarations reference this one in their body.
-
isInitial
in IndisputableMonolith.Foundation.UniversalForcing.NaturalNumberObject
decl_use
depends on (10)
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
-
PeanoObject
in IndisputableMonolith.Foundation.ArithmeticOf
decl_use
-
of
in IndisputableMonolith.Foundation.DAlembert.LedgerFactorization
decl_use
-
of
in IndisputableMonolith.Foundation.PhiForcingDerived
decl_use
-
of
in IndisputableMonolith.Foundation.SpectralEmergence
decl_use
-
IsNaturalNumberObject
in IndisputableMonolith.Foundation.UniversalForcing.NaturalNumberObject
decl_use
-
of
in IndisputableMonolith.Information.PhysicsComplexityStructure
decl_use