`toInt_add`

proved

show as: view math explainer →

module: IndisputableMonolith.Foundation.IntegersFromLogic
domain: Foundation
line: 323 · 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 323.

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

 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
 344theorem toInt_mul (a b : LogicInt) : toInt (a * b) = toInt a * toInt b := by
 345  induction a using Quotient.inductionOn with
 346  | h p =>
 347    induction b using Quotient.inductionOn with
 348    | h q =>
 349      rcases p with ⟨a, b⟩
 350      rcases q with ⟨c, d⟩
 351      show toInt (mk (a * c + b * d) (a * d + b * c)) = toInt (mk a b) * toInt (mk c d)
 352      rw [toInt_mk, toInt_mk, toInt_mk]
 353      rw [toNat_add, toNat_add, toNat_mul, toNat_mul, toNat_mul, toNat_mul]

papers checked against this theorem

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