isUnit_add_isUnit_eq_isUnit_add_isUnit

English

For integers a,b,c,d with ha,hb,hc,hd units, a+b = c+d iff (a=c ∧ b=d) ∨ (a=d ∧ b=c).

Русский

Для целых чисел a,b,c,d с ha,hb,hc,hd единицами, a+b = c+d тогда и только тогда, когда (a=c ∧ b=d) или (a=d ∧ b=c).

LaTeX

$$∀ {a b c d : ℤ}, IsUnit a → IsUnit b → IsUnit c → IsUnit d → (a + b = c + d ↔ (a = c ∧ b = d) ∨ (a = d ∧ b = c))$$

Lean4

theorem isUnit_add_isUnit_eq_isUnit_add_isUnit {a b c d : ℤ} (ha : IsUnit a) (hb : IsUnit b) (hc : IsUnit c)
    (hd : IsUnit d) : a + b = c + d ↔ a = c ∧ b = d ∨ a = d ∧ b = c :=
  by
  rw [isUnit_iff] at ha hb hc hd
  cutsat

Похожие утверждения