`toInt_neg`

proved

show as: view math explainer →

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

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

 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]
 354      push_cast
 355      ring
 356
 357/-- Transfer principle: an equation in `LogicInt` holds iff it holds
 358under `toInt`. The workhorse for proving ring identities on
 359`LogicInt` by reduction to `Int`. -/
 360theorem eq_iff_toInt_eq {a b : LogicInt} : a = b ↔ toInt a = toInt b := by
 361  constructor
 362  · exact congrArg toInt
 363  · intro h
 364    have := congrArg fromInt h
 365    rw [fromInt_toInt, fromInt_toInt] at this
 366    exact this

papers checked against this theorem

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