Clearing a common power of X from a family of polynomials

Given a family of polynomials that is not identically zero, the least exponent occurring with a nonzero coefficient across the family is the largest power of X dividing every member. Dividing by that power leaves at least one polynomial with nonzero constant term. The family may be infinite: the least exponent exists by well-ordering of the natural numbers.

This elementary polynomial result is used in three function-field linear-independence arguments: the valuation criterion of Stichtenoth, Lemma 1.1.7 (Place.OfValuationSubring), the place-degree bound of Proposition 1.1.15 (Place.Degree), and the bound on zeros counted with multiplicity and degree of Proposition 1.3.3 (Place.Zeros).

Main results

• TauCeti.Polynomial.exists_common_X_pow_factor: a family of polynomials, not all zero, is X ^ m times a family in which some member has nonzero constant term.

References

• H. Stichtenoth, Algebraic Function Fields and Codes, 2nd ed., GTM 254, Springer, 2009, Lemma 1.1.7 and Propositions 1.1.15 and 1.3.3.

theorem TauCeti.Polynomial.exists_common_X_pow_factor {k : Type u} [Semiring k] {ι : Type u_1} (s : Set ι) (p : ι → Polynomial k) (hne : ∃ i ∈ s, p i ≠ 0) : ∃ (m : ℕ) (q : ι → Polynomial k), (∀ i ∈ s, p i = Polynomial.X ^ m * q i) ∧ ∃ j ∈ s, (q j).coeff 0 ≠ 0

Dividing a family of polynomials, not all zero, by the largest common power of X leaves at least one quotient with nonzero constant term. The exponent is the least index carrying a nonzero coefficient across the family.