theorem other other

`toNat_zero`

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

formal statement (Lean)

 230@[simp] theorem toNat_zero : toNat zero = 0 := rfl

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

toNat_add in IndisputableMonolith.Foundation.ArithmeticFromLogic decl_use
toNat_mul in IndisputableMonolith.Foundation.ArithmeticFromLogic decl_use
toInt_fromInt in IndisputableMonolith.Foundation.IntegersFromLogic decl_use
toInt_one in IndisputableMonolith.Foundation.IntegersFromLogic decl_use
toInt_zero in IndisputableMonolith.Foundation.IntegersFromLogic decl_use
natOrderedRealization in IndisputableMonolith.Foundation.OrderedLogicRealization decl_use
prime_logic_is_positive_ledger_state in IndisputableMonolith.NumberTheory.LogicPrimeLedgerAtom decl_use

Lean names referenced from this declaration's body.