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)
105def zero : LogicInt := mk LogicNat.zero LogicNat.zero
proof body
Definition body.
106
107/-- One in `LogicInt`. -/
depends on (5)
Lean names referenced from this declaration's body.
-
LogicNat
in IndisputableMonolith.Foundation.ArithmeticFromLogic
decl_use
-
LogicInt
in IndisputableMonolith.Foundation.IntegersFromLogic
decl_use
-
mk
in IndisputableMonolith.Foundation.IntegersFromLogic
decl_use
-
mk
in IndisputableMonolith.Foundation.RationalsFromLogic
decl_use
-
LogicInt
in IndisputableMonolith.NumberTheory.LogicLedgerInterop
decl_use