sq_eq_sq_iff_eq_or_eq_neg — Mathlib

English

Let R be a ring with NoZeroDivisors and a,b ∈ R such that ab = ba. Then a^2 = b^2 if and only if a = b or a = -b.

Русский

Пусть R — кольцо без нулевых делителей, и элементы a, b ∈ R коммутируют. Тогда a^2 = b^2 тогда и только тогда, когда a = b или a = −b.

LaTeX

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

Lean4

protected theorem sq_eq_sq_iff_eq_or_eq_neg (h : Commute a b) : a ^ 2 = b ^ 2 ↔ a = b ∨ a = -b := by
  rw [← sub_eq_zero, h.sq_sub_sq, mul_eq_zero, add_eq_zero_iff_eq_neg, sub_eq_zero, or_comm]

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