# Sums of squares #

We introduce sums of squares in a type `R`

endowed with an `[Add R]`

, `[Zero R]`

and `[Mul R]`

instances. Sums of squares in `R`

are defined by an inductive predicate `IsSumSq : R → Prop`

:
`0 : R`

is a sum of squares and if `S`

is a sum of squares, then for all `a : R`

, `a * a + S`

is a
sum of squares in `R`

.

## Main declaration #

- The predicate
`IsSumSq : R → Prop`

, defining the property of being a sum of squares in`R`

.

## Auxiliary declarations #

- The type
`sumSqIn R`

: in an additive monoid with multiplication`R`

, we introduce the type`sumSqIn R`

as the submonoid of`R`

whose carrier is the subset`{S : R | IsSumSq S}`

.

## Theorems #

`IsSumSq.add`

: if`S1`

and`S2`

are sums of squares in`R`

, then so is`S1 + S2`

.`IsSumSq.nonneg`

: in a linearly ordered semiring`R`

with an`[ExistsAddOfLE R]`

instance, sums of squares are non-negative.`mem_sumSqIn_of_isSquare`

: a square is a sum of squares.`AddSubmonoid.closure_isSquare`

: the submonoid of`R`

generated by the squares in`R`

is the set of sums of squares in`R`

.

In a type `R`

with an addition, a zero element and a multiplication, the property of being a sum of
squares is defined by an inductive predicate: `0 : R`

is a sum of squares and if `S`

is a sum of
squares, then for all `a : R`

, `a * a + S`

is a sum of squares in `R`

.

- zero: ∀ {R : Type u_1} [inst : Mul R] [inst_1 : Add R] [inst_2 : Zero R], IsSumSq 0
- sq_add: ∀ {R : Type u_1} [inst : Mul R] [inst_1 : Add R] [inst_2 : Zero R] (a S : R), IsSumSq S → IsSumSq (a * a + S)

## Instances For

**Alias** of `IsSumSq`

.

In a type `R`

with an addition, a zero element and a multiplication, the property of being a sum of
squares is defined by an inductive predicate: `0 : R`

is a sum of squares and if `S`

is a sum of
squares, then for all `a : R`

, `a * a + S`

is a sum of squares in `R`

.

## Instances For

**Alias** of `IsSumSq.add`

.

If `S1`

and `S2`

are sums of squares in a semiring `R`

, then `S1 + S2`

is a sum of squares in `R`

.

A finite sum of squares is a sum of squares.

In an additive monoid with multiplication, every square is a sum of squares. By definition, a square
in `R`

is a term `x : R`

such that `x = y * y`

for some `y : R`

and in Mathlib this is known as
`IsSquare R`

(see Mathlib.Algebra.Group.Even).

**Alias** of `mem_sumSqIn_of_isSquare`

.

In an additive monoid with multiplication, every square is a sum of squares. By definition, a square
in `R`

is a term `x : R`

such that `x = y * y`

for some `y : R`

and in Mathlib this is known as
`IsSquare R`

(see Mathlib.Algebra.Group.Even).

In an additive monoid with multiplication `R`

, the submonoid generated by the squares is the set of
sums of squares.

**Alias** of `AddSubmonoid.closure_isSquare`

.

In an additive monoid with multiplication `R`

, the submonoid generated by the squares is the set of
sums of squares.

Let `R`

be a linearly ordered semiring in which the property `a ≤ b → ∃ c, a + c = b`

holds
(e.g. `R = ℕ`

). If `S : R`

is a sum of squares in `R`

, then `0 ≤ S`

. This is used in
`Mathlib.Algebra.Ring.Semireal.Defs`

to show that linearly ordered fields are semireal.

**Alias** of `IsSumSq.nonneg`

.

Let `R`

be a linearly ordered semiring in which the property `a ≤ b → ∃ c, a + c = b`

holds
(e.g. `R = ℕ`

). If `S : R`

is a sum of squares in `R`

, then `0 ≤ S`

. This is used in
`Mathlib.Algebra.Ring.Semireal.Defs`

to show that linearly ordered fields are semireal.