`toInt_one`

proved

show as: view math explainer →

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

open explainer

Read the cached plain-language explainer.

open lean source

IndisputableMonolith.Foundation.IntegersFromLogic on GitHub at line 318.

browse module

All declarations in this module, on Recognition.

explainer page

A cached Ask Recognition explainer exists for this declaration.

open explainer

depends on

used by

formal source

 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
 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 =>

papers checked against this theorem

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