sq_sub_sq

Mathlib.Algebra.Ring.Commute

URI: https://scilib.ai/kg/mathlib#Commute.sq_sub_sq

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^2 - b^2 = (a + b)(a - b)$$$

Lean4

protected theorem sq_sub_sq (h : Commute a b) : a ^ 2 - b ^ 2 = (a + b) * (a - b) := by
  rw [sq, sq, h.mul_self_sub_mul_self_eq]

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru