mul_self_sub_mul_self — Mathlib

English

For any a,b in a nonunital commutative ring, a^2 − b^2 = (a + b)(a − b).

Русский

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

LaTeX

$$$ a^2 - b^2 = (a + b)(a - b) $$$

Lean4

/-- Representation of a difference of two squares in a commutative ring as a product. -/
theorem mul_self_sub_mul_self [NonUnitalNonAssocCommRing R] (a b : R) : a * a - b * b = (a + b) * (a - b) :=
  (Commute.all a b).mul_self_sub_mul_self_eq

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