mul_self_eq_mul_self_iff — Mathlib

English

If a and b commute in a ring with NoZeroDivisors, a^2 = b^2 implies a = b or a = -b.

Русский

Если a и b коммутируют в кольце без нулевых делителей, то a^2 = b^2 приводит к a = b или a = -b.

LaTeX

$$$\\text{Commute } a b \\Rightarrow a \\cdot a = b \\cdot b \\Longrightarrow a = b \\lor a = -b$$$

Lean4

theorem mul_self_eq_mul_self_iff [NonUnitalNonAssocRing R] [NoZeroDivisors R] {a b : R} (h : Commute a b) :
    a * a = b * b ↔ a = b ∨ a = -b := by
  rw [← sub_eq_zero, h.mul_self_sub_mul_self_eq, mul_eq_zero, or_comm, sub_eq_zero, add_eq_zero_iff_eq_neg]

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