add_mul_self_eq

Mathlib.Algebra.Ring.Defs

URI: https://scilib.ai/kg/mathlib#add_mul_self_eq

← MathLib Explorer

English

In a commutative semiring α, (a + b)^2 = a^2 + 2ab + b^2.

Русский

В коммутативном полугослиляющем полугруппе α выполнено (a + b)^2 = a^2 + 2ab + b^2.

LaTeX

$$$ (a + b)^2 = a^2 + 2 \cdot a \cdot b + b^2 $$$

Lean4

theorem add_mul_self_eq (a b : α) : (a + b) * (a + b) = a * a + 2 * a * b + b * b := by
  simp only [two_mul, add_mul, mul_add, add_assoc, mul_comm b]

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

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

Разделы

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

Аффилиация

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