one

Mathlib.Algebra.Ring.SumsOfSquares

URI: https://scilib.ai/kg/mathlib#IsSumSq.one

English

The element 1 is a sum of squares in any semiring with addition and multiplication.

Русский

Единица 1 является суммой квадратов в любом полукольце с сложением и умножением.

LaTeX

$$IsSumSq(1)$$

Lean4

@[simp, aesop safe]
theorem one [AddZeroClass R] [MulOneClass R] : IsSumSq (1 : R) := by aesop

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

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

Разделы

Аффилиация

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