Linear independence of polynomial sequences

This file generalizes Mathlib's Polynomial.Sequence.linearIndependent from domains to additive cancellation semirings where the sequence elements have right-regular leading coefficients, and constructs a basis over rings when those coefficients are units.

Main statements

• Polynomial.Sequence.linearIndependent_of_isRightRegular_leadingCoeff: a polynomial sequence whose elements have right-regular leading coefficients is linearly independent over any additive cancellation semiring.
• Polynomial.Sequence.basisOfIsUnitLeadingCoeff: the corresponding basis of R[X].

theorem Polynomial.Sequence.linearIndependent_of_isRightRegular_leadingCoeff {R : Type u_1} [Semiring R] (S : Sequence R) [IsRightCancelAdd R] (hCoeff : ∀ (i : ℕ), IsRightRegular (↑S i).leadingCoeff) : LinearIndependent R ↑S

Polynomials in a polynomial sequence whose leading coefficients are right-regular are linearly independent.

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

Every polynomial sequence with unit leading coefficients is a basis of R[X].

Equations

• S.basisOfIsUnitLeadingCoeff hCoeff = Module.Basis.mk ⋯ ⋯

@[simp]

theorem Polynomial.Sequence.basisOfIsUnitLeadingCoeff_apply {R : Type u_2} [Ring R] (S : Sequence R) (hCoeff : ∀ (i : ℕ), IsUnit (↑S i).leadingCoeff) (i : ℕ) : (S.basisOfIsUnitLeadingCoeff hCoeff) i = ↑S i

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