Documentation

Mathlib.Algebra.Ring.SumsOfSquares

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 #

Auxiliary declarations #

Theorems #

theorem isSumSq_iff {R : Type u_1} [Mul R] [Add R] [Zero R] :
∀ (a : R), IsSumSq a a = 0 ∃ (a_1 : R) (S : R), IsSumSq S a = a_1 * a_1 + S
inductive IsSumSq {R : Type u_1} [Mul R] [Add R] [Zero R] :
RProp

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
    @[deprecated IsSumSq]
    def isSumSq {R : Type u_1} [Mul R] [Add R] [Zero R] :
    RProp

    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.

    Equations
    Instances For
      theorem IsSumSq.add {R : Type u_1} [Mul R] [AddMonoid R] {S1 : R} {S2 : R} (p1 : IsSumSq S1) (p2 : IsSumSq S2) :
      IsSumSq (S1 + S2)

      If S1 and S2 are sums of squares in a semiring R, then S1 + S2 is a sum of squares in R.

      @[deprecated IsSumSq.add]
      theorem isSumSq.add {R : Type u_1} [Mul R] [AddMonoid R] {S1 : R} {S2 : R} (p1 : IsSumSq S1) (p2 : IsSumSq S2) :
      IsSumSq (S1 + S2)

      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.

      theorem isSumSq_sum_mul_self {R : Type u_1} [Mul R] {ι : Type u_2} [AddCommMonoid R] (s : Finset ι) (f : ιR) :
      IsSumSq (∑ is, f i * f i)

      A finite sum of squares is a sum of squares.

      def sumSqIn (R : Type u_1) [Mul R] [AddMonoid R] :

      In an additive monoid with multiplication R, the type sumSqIn R is the submonoid of sums of squares in R.

      Equations
      • sumSqIn R = { carrier := {S : R | IsSumSq S}, add_mem' := , zero_mem' := }
      Instances For
        @[deprecated sumSqIn]
        def SumSqIn (R : Type u_1) [Mul R] [AddMonoid R] :

        Alias of sumSqIn.


        In an additive monoid with multiplication R, the type sumSqIn R is the submonoid of sums of squares in R.

        Equations
        Instances For
          theorem mem_sumSqIn_of_isSquare {R : Type u_1} [Mul R] [AddMonoid R] {x : R} (px : IsSquare x) :

          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).

          @[deprecated mem_sumSqIn_of_isSquare]
          theorem SquaresInSumSq {R : Type u_1} [Mul R] [AddMonoid R] {x : R} (px : IsSquare x) :

          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.

          @[deprecated AddSubmonoid.closure_isSquare]
          theorem SquaresAddClosure {R : Type u_1} [Mul R] [AddMonoid R] :

          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.

          theorem IsSumSq.nonneg {R : Type u_2} [LinearOrderedSemiring R] [ExistsAddOfLE R] {S : R} (pS : IsSumSq S) :
          0 S

          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.

          @[deprecated IsSumSq.nonneg]
          theorem isSumSq.nonneg {R : Type u_2} [LinearOrderedSemiring R] [ExistsAddOfLE R] {S : R} (pS : IsSumSq S) :
          0 S

          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.