abs_sub_sq — Mathlib

English

The square of the difference equals the sum and product terms: |a - b|^2 = a^2 + b^2 - 2ab.

Русский

Квадрат разницы равен сумме квадратов минус удвоенное произведение: (a - b)^2 = a^2 + b^2 - 2ab.

LaTeX

$$|a - b|^2 = a^2 + b^2 - 2ab$$

Lean4

theorem abs_sub_sq (a b : α) : |a - b| * |a - b| = a * a + b * b - (1 + 1) * a * b :=
  by
  rw [abs_mul_abs_self]
  simp only [mul_add, add_comm, add_left_comm, mul_comm, sub_eq_add_neg, mul_one, mul_neg, neg_add_rev, neg_neg,
    add_assoc]

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