def definition def or abbrev

`fromNat`

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

formal statement (Lean)

 226def fromNat : Nat → LogicNat
 227  | 0          => .identity
 228  | Nat.succ n => .step (fromNat n)
 229

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

add_left_cancel in IndisputableMonolith.Foundation.ArithmeticFromLogic decl_use
embed_injective in IndisputableMonolith.Foundation.ArithmeticFromLogic decl_use
eq_iff_toNat_eq in IndisputableMonolith.Foundation.ArithmeticFromLogic decl_use
equivNat in IndisputableMonolith.Foundation.ArithmeticFromLogic decl_use
fromNat_succ in IndisputableMonolith.Foundation.ArithmeticFromLogic decl_use
fromNat_toNat in IndisputableMonolith.Foundation.ArithmeticFromLogic decl_use
fromNat_zero in IndisputableMonolith.Foundation.ArithmeticFromLogic decl_use
le_antisymm in IndisputableMonolith.Foundation.ArithmeticFromLogic decl_use
toNat_fromNat in IndisputableMonolith.Foundation.ArithmeticFromLogic decl_use
toNat_le in IndisputableMonolith.Foundation.ArithmeticFromLogic decl_use
fromInt in IndisputableMonolith.Foundation.IntegersFromLogic decl_use
fromInt_toInt in IndisputableMonolith.Foundation.IntegersFromLogic decl_use
toInt_fromInt in IndisputableMonolith.Foundation.IntegersFromLogic decl_use
modular_interpret_periodic in IndisputableMonolith.Foundation.ModularLogicRealization decl_use
fromNat in IndisputableMonolith.LedgerUnits decl_use
kOf_fromNat in IndisputableMonolith.LedgerUnits decl_use
kOf_step_succ in IndisputableMonolith.LedgerUnits decl_use
one_not_primeLedgerAtomLogic in IndisputableMonolith.NumberTheory.LogicPrimeLedgerAtom decl_use
PrimeLedgerLogicCert in IndisputableMonolith.NumberTheory.LogicPrimeLedgerAtom decl_use

Lean names referenced from this declaration's body.