add_sq

Mathlib.Algebra.Ring.Defs

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

English

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

Русский

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

LaTeX

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

Lean4

theorem add_sq (a b : α) : (a + b) ^ 2 = a ^ 2 + 2 * a * b + b ^ 2 := by simp only [sq, add_mul_self_eq]

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

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

Разделы

Аффилиация

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