mul_self_tsub_mul_self — Mathlib

English

In a ring with order, for all a,b, 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

/-- The `tsub` version of `mul_self_sub_mul_self`. Notably, this holds for `Nat` and `NNReal`. -/
theorem mul_self_tsub_mul_self (a b : R) : a * a - b * b = (a + b) * (a - b) := by
  rw [mul_tsub, add_mul, add_mul, tsub_add_eq_tsub_tsub, mul_comm b a, add_tsub_cancel_right]

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