add_sq

Mathlib.Algebra.Ring.Commute

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

← MathLib Explorer

English

If a and b commute in a semiring, then (a + b)^2 = a^2 + 2ab + b^2.

Русский

Если a и b коммутируют в полуприводящем кольце, то (a + b)^2 = a^2 + 2ab + b^2.

LaTeX

$$$\\text{Commute } a b \\Rightarrow (a + b)^2 = a^2 + 2ab + b^2$$$

Lean4

protected theorem add_sq {a b : R} (h : Commute a b) : (a + b) ^ 2 = a ^ 2 + 2 * a * b + b ^ 2 := by
  simp [sq, add_mul, mul_add, two_mul, h.eq, add_assoc]

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

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

Разделы

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

Аффилиация

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