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
    @[implicit_reducible]
    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.

    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_degreeLT {R : Type u_1} [Ring R] (S : Sequence R) {m : โ„•} (hCoeff : โˆ€ i < m, IsUnit (โ†‘S i).leadingCoeff) :
    Submodule.span R (โ†‘S '' Set.Iio m) = degreeLT R m

    The first m polynomials of a polynomial sequence span all polynomials of degree < m if their leading coefficients are units.

    source
    ๐Ÿ“ coverage
    theorem Polynomial.Sequence.span_degreeLE {R : Type u_1} [Ring R] (S : Sequence R) {m : โ„•} (hCoeff : โˆ€ i โ‰ค m, IsUnit (โ†‘S i).leadingCoeff) :
    Submodule.span R (โ†‘S '' Set.Iic m) = degreeLE R โ†‘m

    The first m + 1 polynomials of a polynomial sequence span all polynomials of degree โ‰ค m if their leading coefficients are units.

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

    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.