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)
318theorem toInt_one : toInt (1 : LogicInt) = 1 := by
proof body
Term-mode proof.
319 show toInt (mk (LogicNat.succ LogicNat.zero) LogicNat.zero) = 1
320 rw [toInt_mk, toNat_succ, toNat_zero]
321 norm_num
322
used by (7)
From the project-wide theorem graph. These declarations reference this one in their body.
-
mul_one'
in IndisputableMonolith.Foundation.IntegersFromLogic
decl_use
-
one_mul'
in IndisputableMonolith.Foundation.IntegersFromLogic
decl_use
-
ofLogicInt
in IndisputableMonolith.Foundation.RationalsFromLogic
decl_use
-
one
in IndisputableMonolith.Foundation.RationalsFromLogic
decl_use
-
toRat_one
in IndisputableMonolith.Foundation.RationalsFromLogic
decl_use
-
toRat_zero
in IndisputableMonolith.Foundation.RationalsFromLogic
decl_use
-
zero
in IndisputableMonolith.Foundation.RationalsFromLogic
decl_use
depends on (11)
Lean names referenced from this declaration's body.
-
LogicNat
in IndisputableMonolith.Foundation.ArithmeticFromLogic
decl_use
-
succ
in IndisputableMonolith.Foundation.ArithmeticFromLogic
decl_use
-
toNat_succ
in IndisputableMonolith.Foundation.ArithmeticFromLogic
decl_use
-
toNat_zero
in IndisputableMonolith.Foundation.ArithmeticFromLogic
decl_use
-
LogicInt
in IndisputableMonolith.Foundation.IntegersFromLogic
decl_use
-
mk
in IndisputableMonolith.Foundation.IntegersFromLogic
decl_use
-
toInt
in IndisputableMonolith.Foundation.IntegersFromLogic
decl_use
-
toInt_mk
in IndisputableMonolith.Foundation.IntegersFromLogic
decl_use
-
mk
in IndisputableMonolith.Foundation.RationalsFromLogic
decl_use
-
LogicInt
in IndisputableMonolith.NumberTheory.LogicLedgerInterop
decl_use
-
succ
in IndisputableMonolith.RRF.Core.Vantage
decl_use