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
๐Ÿ”ถ coverage
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
    ๐Ÿ”ธ coverage
    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
      ๐Ÿ“ coverage
      @[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
      ๐Ÿ“ coverage
      @[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
      ๐Ÿ“ coverage
      theorem Polynomial.Sequence.degree_strictMono {R : Type u_1} [Semiring R] (S : Sequence R) :
      StrictMono (degree โˆ˜ โ†‘S)

      S i has strictly monotone degree.

      source
      ๐Ÿ“ coverage
      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
      ๐Ÿ“ coverage
      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
      ๐Ÿ“ coverage
      theorem Polynomial.Sequence.linearIndependent {R : Type u_1} [Ring R] (S : Sequence R) [IsDomain R] :
      LinearIndependent R โ†‘S

      Polynomials in a polynomial sequence are linearly independent.

      source
      ๐Ÿ”ธ coverage
      noncomputable def Polynomial.Sequence.basis {R : Type u_1} [Ring R] (S : Sequence R) [IsDomain 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
          ๐Ÿ“ coverage
          @[simp]
          theorem Polynomial.Sequence.basis_eq_self {R : Type u_1} [Ring R] (S : Sequence R) [IsDomain 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
          ๐Ÿ“ coverage
          theorem Polynomial.Sequence.basis_degree_strictMono {R : Type u_1} [Ring R] (S : Sequence R) [IsDomain R] (hCoeff : โˆ€ (i : โ„•), IsUnit (โ†‘S i).leadingCoeff) :
          StrictMono (degree โˆ˜ โ‡‘(S.basis hCoeff))

          Basis elements have strictly monotone degree.

          source
          ๐Ÿ“ coverage
          theorem Polynomial.Sequence.basis_natDegree_strictMono {R : Type u_1} [Ring R] (S : Sequence R) [IsDomain R] (hCoeff : โˆ€ (i : โ„•), IsUnit (โ†‘S i).leadingCoeff) :
          StrictMono (natDegree โˆ˜ โ‡‘(S.basis hCoeff))

          Basis elements have strictly monotone natural degree.