`mul_eq_zero`

proved

show as: view math explainer →

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

open explainer

Read the cached plain-language explainer.

open lean source

IndisputableMonolith.Foundation.IntegersFromLogic on GitHub at line 408.

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

 405
 406/-- `LogicInt` has no zero divisors: from `a * b = 0`, either `a = 0`
 407or `b = 0`. Forced by the ring isomorphism with `Int`. -/
 408theorem mul_eq_zero {a b : LogicInt} : a * b = 0 ↔ a = 0 ∨ b = 0 := by
 409  constructor
 410  · intro h
 411    have hint : toInt a * toInt b = 0 := by
 412      rw [← toInt_mul]
 413      have := congrArg toInt h
 414      rwa [toInt_zero] at this
 415    rcases Int.mul_eq_zero.mp hint with ha | hb
 416    · left
 417      rw [eq_iff_toInt_eq, toInt_zero]; exact ha
 418    · right
 419      rw [eq_iff_toInt_eq, toInt_zero]; exact hb
 420  · rintro (ha | hb)
 421    · rw [ha, eq_iff_toInt_eq, toInt_mul, toInt_zero]; ring
 422    · rw [hb, eq_iff_toInt_eq, toInt_mul, toInt_zero]; ring
 423
 424/-- Cancellation: if `c ≠ 0` and `a * c = b * c`, then `a = b`. -/
 425theorem mul_right_cancel {a b c : LogicInt} (hc : c ≠ 0) (h : a * c = b * c) : a = b := by
 426  have hc' : toInt c ≠ 0 := by
 427    intro habs
 428    apply hc
 429    rw [eq_iff_toInt_eq, toInt_zero]; exact habs
 430  rw [eq_iff_toInt_eq, toInt_mul, toInt_mul] at h
 431  rw [eq_iff_toInt_eq]
 432  exact Int.eq_of_mul_eq_mul_right hc' h
 433
 434end LogicInt
 435
 436/-! ## Summary
 437
 438  Foundation.LogicAsFunctionalEquation     (Law of Logic)

papers checked against this theorem

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