sub_sq

Mathlib.Algebra.Ring.Commute

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

← MathLib Explorer

English

Let R be a ring and a,b ∈ R commute. Then (a - b)^2 = a^2 - 2ab + b^2.

Русский

Пусть R — кольцо и элементы a, b ∈ R коммутируют. Тогда (a − b)^2 = a^2 − 2ab + b^2.

LaTeX

$$$ ab = ba \\Rightarrow (a - b)^2 = a^2 - 2ab + b^2 $$$

Lean4

protected theorem sub_sq {a b : R} (h : Commute a b) : (a - b) ^ 2 = a ^ 2 - 2 * a * b + b ^ 2 := by
  simp [sq, add_mul, sub_mul, mul_sub, two_mul, h.eq, ← sub_add, ← sub_sub]

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

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

Разделы

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

Аффилиация

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