Documentation

Mathlib.Algebra.Polynomial.Sequence

Polynomial sequences #

We define polynomial sequences – sequences of polynomials a₀, a₁, ... such that the polynomial aᵢ has degree i.

Main definitions #

Main statements #

TODO #

Generalize linear independence to:

source
structure Polynomial.Sequence (R : Type u_1) [Semiring R] :
Type u_1

A sequence of polynomials such that the polynomial at index i has degree i.

  • elems' : ℕ → Polynomial R

    The i'th element in the sequence. Use S i instead, defined via CoeFun.

  • degree_eq' (i : ℕ) : (↑self i).degree = ↑i

    The i'th element in the sequence has degree i. Use S.degree_eq instead.

Instances For
    source
    instance Polynomial.Sequence.coeFun {R : Type u_1} [Semiring R] :
    CoeFun (Sequence R) fun (x : Sequence R) => ℕ → Polynomial R

    Make S i mean S.elems' i.

    Equations
      source
      @[simp]
      theorem Polynomial.Sequence.degree_eq {R : Type u_1} [Semiring R] (S : Sequence R) (i : ℕ) :
      (↑S i).degree = ↑i

      S i has degree i.

      source
      @[simp]
      theorem Polynomial.Sequence.natDegree_eq {R : Type u_1} [Semiring R] (S : Sequence R) (i : ℕ) :
      (↑S i).natDegree = i

      S i has natDegree i.

      source
      @[simp]
      theorem Polynomial.Sequence.ne_zero {R : Type u_1} [Semiring R] (S : Sequence R) (i : ℕ) :
      ↑S i ≠ 0

      No polynomial in the sequence is zero.

      source
      theorem Polynomial.Sequence.degree_strictMono {R : Type u_1} [Semiring R] (S : Sequence R) :
      StrictMono (degree ∘ ↑S)

      S i has strictly monotone degree.

      source
      theorem Polynomial.Sequence.natDegree_strictMono {R : Type u_1} [Semiring R] (S : Sequence R) :
      StrictMono (natDegree ∘ ↑S)

      S i has strictly monotone natural degree.

      source
      theorem Polynomial.Sequence.span {R : Type u_1} [Ring R] (S : Sequence R) (hCoeff : ∀ (i : ℕ), IsUnit (↑S i).leadingCoeff) :
      Submodule.span R (Set.range ↑S) = ⊤

      A polynomial sequence spans R[X] if all of its elements' leading coefficients are units.

      source
      theorem Polynomial.Sequence.linearIndependent {R : Type u_1} [Ring R] (S : Sequence R) [NoZeroDivisors R] :
      LinearIndependent R ↑S

      Polynomials in a polynomial sequence are linearly independent.

      source
      noncomputable def Polynomial.Sequence.basis {R : Type u_1} [Ring R] (S : Sequence R) [NoZeroDivisors R] (hCoeff : ∀ (i : ℕ), IsUnit (↑S i).leadingCoeff) :
      Module.Basis ℕ R (Polynomial R)

      Every polynomial sequence is a basis of R[X].

      Equations
        Instances For
          source
          @[simp]
          theorem Polynomial.Sequence.basis_eq_self {R : Type u_1} [Ring R] (S : Sequence R) [NoZeroDivisors R] (hCoeff : ∀ (i : ℕ), IsUnit (↑S i).leadingCoeff) (i : ℕ) :
          (S.basis hCoeff) i = ↑S i

          The i'th basis vector is the i'th polynomial in the sequence.

          source
          theorem Polynomial.Sequence.basis_degree_strictMono {R : Type u_1} [Ring R] (S : Sequence R) [NoZeroDivisors R] (hCoeff : ∀ (i : ℕ), IsUnit (↑S i).leadingCoeff) :
          StrictMono (degree ∘ ⇑(S.basis hCoeff))

          Basis elements have strictly monotone degree.

          source
          theorem Polynomial.Sequence.basis_natDegree_strictMono {R : Type u_1} [Ring R] (S : Sequence R) [NoZeroDivisors R] (hCoeff : ∀ (i : ℕ), IsUnit (↑S i).leadingCoeff) :
          StrictMono (natDegree ∘ ⇑(S.basis hCoeff))

          Basis elements have strictly monotone natural degree.