`toInt_zero`

proved

show as: view math explainer →

module: IndisputableMonolith.Foundation.IntegersFromLogic
domain: Foundation
line: 313 · github
papers citing: none yet

open explainer

Generate a durable explainer page for this declaration.

open lean source

IndisputableMonolith.Foundation.IntegersFromLogic on GitHub at line 313.

browse module

All declarations in this module, on Recognition.

explainer page

Tracked in the explainer inventory; generation is lazy so crawlers do not trigger LLM jobs.

open explainer

depends on

used by

formal source

 310operations and use them, plus a transfer principle, to derive the
 311full ring structure on `LogicInt`. -/
 312
 313theorem toInt_zero : toInt (0 : LogicInt) = 0 := by
 314  show toInt (mk LogicNat.zero LogicNat.zero) = 0
 315  rw [toInt_mk]
 316  simp [toNat_zero]
 317
 318theorem toInt_one : toInt (1 : LogicInt) = 1 := by
 319  show toInt (mk (LogicNat.succ LogicNat.zero) LogicNat.zero) = 1
 320  rw [toInt_mk, toNat_succ, toNat_zero]
 321  norm_num
 322
 323theorem toInt_add (a b : LogicInt) : toInt (a + b) = toInt a + toInt b := by
 324  induction a using Quotient.inductionOn with
 325  | h p =>
 326    induction b using Quotient.inductionOn with
 327    | h q =>
 328      rcases p with ⟨a, b⟩
 329      rcases q with ⟨c, d⟩
 330      show toInt (mk (a + c) (b + d)) = toInt (mk a b) + toInt (mk c d)
 331      rw [toInt_mk, toInt_mk, toInt_mk]
 332      rw [toNat_add, toNat_add]
 333      push_cast
 334      ring
 335
 336theorem toInt_neg (a : LogicInt) : toInt (-a) = -toInt a := by
 337  induction a using Quotient.inductionOn with
 338  | h p =>
 339    rcases p with ⟨a, b⟩
 340    show toInt (mk b a) = -toInt (mk a b)
 341    rw [toInt_mk, toInt_mk]
 342    ring
 343

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.