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 (rearranged).

Русский

В коммутативном полугосле α имеет же самое тождество, но с иным расположением членов: (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 + b ^ 2 + 2 * a * b := by
  rw [add_sq, add_assoc, add_comm _ (b ^ 2), add_assoc]

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

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

Разделы

Аффилиация

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