add_sq

Mathlib.Algebra.CharP.Two

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

English

In a commutative semiring R with ringChar(R) = 2, we have (x + y)^2 = x^2 + y^2 for all x, y in R.

Русский

В коммутативной полуправой R с характеристикой кольца 2 выполняется (x + y)^2 = x^2 + y^2 для всех x, y ∈ R.

LaTeX

$$$(\\\\operatorname{ringChar}(R) = 2) \\\\Rightarrow (x+y)^2 = x^2 + y^2$$$

Lean4

theorem add_sq (x y : R) : (x + y) ^ 2 = x ^ 2 + y ^ 2 :=
  add_pow_char _ _ _

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

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

Разделы

Аффилиация

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