mul_self_sub_mul_self_eq'

Mathlib.Algebra.Ring.Commute

URI: https://scilib.ai/kg/mathlib#Commute.mul_self_sub_mul_self_eq'

← MathLib Explorer

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

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 [mul_add, sub_mul, sub_mul, h.eq, sub_add_sub_cancel]

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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