mul_self_eq_mul_self_iff — Mathlib

English

For any a,b in a NoZeroDivisors nonunital commutative ring, a^2 = b^2 iff a = b or a = −b.

Русский

Для любых a,b в кольце без нулевых делителей, коммутативном без единицы, a^2 = b^2 тогда и только тогда, когда a = b или a = −b.

LaTeX

$$$ a^2 = b^2 \\iff a = b \\lor a = -b $$$

Lean4

theorem mul_self_eq_mul_self_iff [NonUnitalNonAssocCommRing R] [NoZeroDivisors R] {a b : R} :
    a * a = b * b ↔ a = b ∨ a = -b :=
  (Commute.all a b).mul_self_eq_mul_self_iff

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