Documentation

Mathlib.Algebra.Ring.SumsOfSquares

Sums of squares #

We introduce a predicate for sums of squares in a ring.

Main declarations #

inductive IsSumSq {R : Type u_1} [Mul R] [Add R] [Zero R] :
RProp

The property of being a sum of squares is defined inductively by: 0 : R is a sum of squares and if s : R is a sum of squares, then for all a : R, a * a + s is a sum of squares in R.

Instances For
    theorem isSumSq_iff {R : Type u_1} [Mul R] [Add R] [Zero R] (a✝ : R) :
    IsSumSq a✝ a✝ = 0 ∃ (a : R) (s : R), IsSumSq s a✝ = a * a + s
    theorem IsSumSq.rec' {R : Type u_1} [Mul R] [Add R] [Zero R] {motive : (s : R) → IsSumSq sProp} (zero : motive 0 ) (sq_add : ∀ {x s : R} (hx : IsSquare x) (hs : IsSumSq s), motive s hsmotive (x + s) ) {s : R} (h : IsSumSq s) :
    motive s h

    Alternative induction scheme for IsSumSq which uses IsSquare.

    theorem IsSumSq.add {R : Type u_1} [AddMonoid R] [Mul R] {s₁ s₂ : R} (h₁ : IsSumSq s₁) (h₂ : IsSumSq s₂) :
    IsSumSq (s₁ + s₂)

    In an additive monoid with multiplication, if s₁ and s₂ are sums of squares, then s₁ + s₂ is a sum of squares.

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

    Equations
    Instances For
      @[simp]
      theorem AddSubmonoid.coe_sumSq (T : Type u_2) [Mul T] [AddMonoid T] :
      (sumSq T) = {s : T | IsSumSq s}
      @[simp]
      theorem AddSubmonoid.mem_sumSq {T : Type u_2} [AddMonoid T] [Mul T] {s : T} :
      @[simp]
      theorem IsSumSq.mul_self {R : Type u_1} [AddZeroClass R] [Mul R] (a : R) :
      IsSumSq (a * a)

      In an additive unital magma with multiplication, x * x is a sum of squares for all x.

      theorem IsSquare.isSumSq {R : Type u_1} [AddZeroClass R] [Mul R] {x : R} (hx : IsSquare x) :

      In an additive unital magma with multiplication, squares are sums of squares (see Mathlib.Algebra.Group.Even).

      @[simp]

      In an additive monoid with multiplication R, the submonoid generated by the squares is the set of sums of squares in R.

      theorem IsSumSq.sum {R : Type u_1} [AddCommMonoid R] [Mul R] {ι : Type u_2} {I : Finset ι} {s : ιR} (hs : iI, IsSumSq (s i)) :
      IsSumSq (∑ iI, s i)

      In an additive commutative monoid with multiplication, a finite sum of sums of squares is a sum of squares.

      theorem IsSumSq.sum_isSquare {R : Type u_1} [AddCommMonoid R] [Mul R] {ι : Type u_2} (I : Finset ι) {x : ιR} (hx : iI, IsSquare (x i)) :
      IsSumSq (∑ iI, x i)

      In an additive commutative monoid with multiplication, ∑ i ∈ I, x i, where each x i is a square, is a sum of squares.

      @[simp]
      theorem IsSumSq.sum_mul_self {R : Type u_1} [AddCommMonoid R] [Mul R] {ι : Type u_2} (I : Finset ι) (a : ιR) :
      IsSumSq (∑ iI, a i * a i)

      In an additive commutative monoid with multiplication, ∑ i ∈ I, a i * a i is a sum of squares.

      @[deprecated IsSumSq.sum_mul_self (since := "2024-12-27")]
      theorem isSumSq_sum_mul_self {R : Type u_1} [AddCommMonoid R] [Mul R] {ι : Type u_2} (I : Finset ι) (a : ιR) :
      IsSumSq (∑ iI, a i * a i)

      Alias of IsSumSq.sum_mul_self.


      In an additive commutative monoid with multiplication, ∑ i ∈ I, a i * a i is a sum of squares.

      In a commutative (possibly non-unital) semiring R, NonUnitalSubsemiring.sumSq R is the (possibly non-unital) subsemiring of sums of squares in R.

      Equations
      Instances For
        theorem IsSumSq.mul {R : Type u_1} [NonUnitalCommSemiring R] {s₁ s₂ : R} (h₁ : IsSumSq s₁) (h₂ : IsSumSq s₂) :
        IsSumSq (s₁ * s₂)

        In a commutative (possibly non-unital) semiring, if s₁ and s₂ are sums of squares, then s₁ * s₂ is a sum of squares.

        In a commutative semiring R, Subsemiring.sumSq R is the subsemiring of sums of squares in R.

        Equations
        Instances For
          @[simp]
          theorem Subsemiring.mem_sumSq {T : Type u_2} [CommSemiring T] {s : T} :
          @[simp]
          theorem Subsemiring.coe_sumSq {T : Type u_2} [CommSemiring T] :
          (sumSq T) = {s : T | IsSumSq s}
          theorem IsSumSq.prod {R : Type u_1} [CommSemiring R] {ι : Type u_2} {I : Finset ι} {x : ιR} (hx : iI, IsSumSq (x i)) :
          IsSumSq (∏ iI, x i)

          In a commutative semiring, a finite product of sums of squares is a sum of squares.

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

          In a linearly ordered semiring with the property a ≤ b → ∃ c, a + c = b (e.g. ), sums of squares are non-negative.