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:

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.

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

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

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

S i has strictly monotone degree.

S i has strictly monotone natural degree.

theorem Polynomial.Sequence.span {R : Type u_1} [Ring R] (S : Sequence R) (hCoeff : ∀ (i : ), IsUnit (S i).leadingCoeff) :

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

Polynomials in a polynomial sequence are linearly independent.

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

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

Equations
@[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.

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.

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.