Quotient substitution and the final polynomial root bound #
Reducing source powers modulo E does not change their classes in AdjoinRoot E.
The base-h monomials then become distinct powers indexed by Fin K. A surviving
coefficient makes the resulting polynomial nonzero of degree below K.
theorem
Algebraic.Cutwidth.Extractor.Internal.substitutedSum_quotient_eval
{F : Type u_1}
[Field F]
{h K m : ℕ}
(E : Polynomial F)
(monic : E.Monic)
(bound : K ≤ h ^ m)
(p : Fin K → Polynomial F)
(f : Polynomial F)
:
Polynomial.eval ((AdjoinRoot.mk E) f) (∑ j : Fin K, (Polynomial.monomial ↑j) ((AdjoinRoot.mk E) (p j))) = (AdjoinRoot.mk E) (substitutedSum E h m p f)
theorem
Algebraic.Cutwidth.Extractor.Internal.card_lt_of_quotient_polynomial_roots
{F : Type u_1}
[Field F]
{K : ℕ}
(E : Polynomial F)
(monic : E.Monic)
(irreducible : Irreducible E)
(p : Fin K → Polynomial F)
(primitive : ∃ (j : Fin K), ¬E ∣ p j)
(P : Finset (Polynomial F))
(source : ∀ f ∈ P, f.degree < E.degree)
(roots :
∀ f ∈ P, Polynomial.eval ((AdjoinRoot.mk E) f) (∑ j : Fin K, (Polynomial.monomial ↑j) ((AdjoinRoot.mk E) (p j))) = 0)
: