mul_self_sub_mul_self_eq — Mathlib

English

If a and b commute in a ring, then a^2 - b^2 = (a + b)(a - b).

Русский

Если элементы a и b коммутируют в кольце, то a^2 - b^2 = (a + b)(a - b).

LaTeX

$$$\\text{Commute } a b \\Rightarrow a \\cdot a - b \\cdot b = (a + b) \\cdot (a - b)$$$

Lean4

/-- Representation of a difference of two squares of commuting elements as a product. -/
theorem mul_self_sub_mul_self_eq [NonUnitalNonAssocRing R] {a b : R} (h : Commute a b) :
    a * a - b * b = (a + b) * (a - b) := by rw [add_mul, mul_sub, mul_sub, h.eq, sub_add_sub_cancel]

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