Removing common modulus factors from an interpolating family #
If every coefficient polynomial is divisible by the modulus, divide each by it. The family stays nonzero, its degree budget decreases, and its weighted evaluation constraints persist wherever the modulus evaluates nonzero.
theorem
Algebraic.Cutwidth.Extractor.Internal.exists_primitive_polynomialFamily
{F : Type u_1}
{X : Type u_2}
[Field F]
{A K : ℕ}
(E : Polynomial F)
(monic : E.Monic)
(positive : 0 < E.natDegree)
(T : Finset X)
(seed : X → F)
(weight : X → Fin K → F)
(nonvanishing : ∀ x ∈ T, Polynomial.eval (seed x) E ≠ 0)
(p : Fin K → Polynomial F)
(nonzero : p ≠ 0)
(degree : ∀ (j : Fin K), (p j).degree < ↑A)
(vanish : ∀ x ∈ T, ∑ j : Fin K, Polynomial.eval (seed x) (p j) * weight x j = 0)
: