`toRat_zero`

proved

show as: view math explainer →

module: IndisputableMonolith.Foundation.RationalsFromLogic
domain: Foundation
line: 297 · github
papers citing: none yet

open explainer

Read the cached plain-language explainer.

open lean source

IndisputableMonolith.Foundation.RationalsFromLogic on GitHub at line 297.

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

 294    rw [fromRat_toRat, fromRat_toRat] at this
 295    exact this
 296
 297theorem toRat_zero : toRat (0 : LogicRat) = 0 := by
 298  show toRat (mk 0 1 _) = 0
 299  rw [toRat_mk, toInt_zero, toInt_one]
 300  norm_num
 301
 302theorem toRat_one : toRat (1 : LogicRat) = 1 := by
 303  show toRat (mk 1 1 _) = 1
 304  rw [toRat_mk, toInt_one]
 305  norm_num
 306
 307theorem toRat_neg (a : LogicRat) : toRat (-a) = -toRat a := by
 308  induction a using Quotient.inductionOn with
 309  | h p =>
 310    rcases p with ⟨a, b, hb⟩
 311    show toRat (mk (-a) b hb) = -toRat (mk a b hb)
 312    rw [toRat_mk, toRat_mk, toInt_neg]
 313    have hbq : (toInt b : ℚ) ≠ 0 := by
 314      intro h; apply hb; rw [eq_iff_toInt_eq, toInt_zero]; exact_mod_cast h
 315    field_simp [hbq]
 316    norm_num
 317
 318theorem toRat_add (a b : LogicRat) : toRat (a + b) = toRat a + toRat b := by
 319  induction a using Quotient.inductionOn with
 320  | h p =>
 321    induction b using Quotient.inductionOn with
 322    | h q =>
 323      rcases p with ⟨a, b, hb⟩
 324      rcases q with ⟨c, d, hd⟩
 325      show toRat (mk (a * d + c * b) (b * d) _) =
 326        toRat (mk a b hb) + toRat (mk c d hd)
 327      simp only [toRat_mk, toInt_add, toInt_mul]

papers checked against this theorem

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