sumSq

Mathlib.Algebra.Ring.SumsOfSquares

URI: https://scilib.ai/kg/mathlib#AddSubmonoid.sumSq

Lean4

/-- In an additive monoid with multiplication `R`, `AddSubmonoid.sumSq R` is the submonoid of sums of
squares in `R`.
-/
@[simps]
def sumSq [AddMonoid T] : AddSubmonoid T where
  carrier := {s : T | IsSumSq s}
  zero_mem' := .zero
  add_mem' := .add

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

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

Разделы

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

Аффилиация

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