sumSq — Mathlib

English

The Subsemiring associated to sums of squares is the subsemiring whose carrier consists of all sums of squares.

Русский

Подсемиринг, связанный с суммами квадратов, состоит из элементов, являющихся суммами квадратов.

LaTeX

$$$\text{sumSq } T \text{ is a Subsemiring of } T$$$

Lean4

/-- In a commutative semiring `R`, `Subsemiring.sumSq R` is the subsemiring of sums of squares in `R`.
-/
def sumSq : Subsemiring T where
  __ := NonUnitalSubsemiring.sumSq T
  one_mem' := by simp

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