theorem proved term proof

`toInt_zero`

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

formal statement (Lean)

 313theorem toInt_zero : toInt (0 : LogicInt) = 0 := by

Term-mode proof.

 314  show toInt (mk LogicNat.zero LogicNat.zero) = 0
 315  rw [toInt_mk]
 316  simp [toNat_zero]
 317

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

add_left_neg' in IndisputableMonolith.Foundation.IntegersFromLogic decl_use
add_zero' in IndisputableMonolith.Foundation.IntegersFromLogic decl_use
mul_eq_zero in IndisputableMonolith.Foundation.IntegersFromLogic decl_use
mul_right_cancel in IndisputableMonolith.Foundation.IntegersFromLogic decl_use
zero_add' in IndisputableMonolith.Foundation.IntegersFromLogic decl_use
fromRat in IndisputableMonolith.Foundation.RationalsFromLogic decl_use
fromRat_toRat in IndisputableMonolith.Foundation.RationalsFromLogic decl_use
ofLogicInt in IndisputableMonolith.Foundation.RationalsFromLogic decl_use
one in IndisputableMonolith.Foundation.RationalsFromLogic decl_use
toRat_add in IndisputableMonolith.Foundation.RationalsFromLogic decl_use
toRatCore_respects in IndisputableMonolith.Foundation.RationalsFromLogic decl_use
toRat_mul in IndisputableMonolith.Foundation.RationalsFromLogic decl_use
toRat_neg in IndisputableMonolith.Foundation.RationalsFromLogic decl_use
toRat_zero in IndisputableMonolith.Foundation.RationalsFromLogic decl_use
zero in IndisputableMonolith.Foundation.RationalsFromLogic decl_use

Lean names referenced from this declaration's body.