Bounding the coefficients of the quotient and remainder of polynomials #
This file proves that, for polynomials p q : R[X], the coefficients of p /ₘ q and p %ₘ q can
be written as sums of products of coefficients of p and q.
Precisely, we show that each summand needs at most one coefficient of p and deg p coefficients
of q.
theorem Polynomial.coeff_divModByMonicAux_mem_span_pow_mul_span {R : Type u_2} {S : Type u_3} [CommRing R] [Ring S] [Algebra R S] (p q : Polynomial S) (hq : q.Monic) (i : ℕ) :
(p.divModByMonicAux hq).1.coeff i ∈ (1 ⊔ Submodule.span R (Set.range ⇑q.coeff)) ^ p.natDegree * (1 ⊔ Submodule.span R (Set.range ⇑p.coeff)) ∧ (p.divModByMonicAux hq).2.coeff i ∈ (1 ⊔ Submodule.span R (Set.range ⇑q.coeff)) ^ p.natDegree * (1 ⊔ Submodule.span R (Set.range ⇑p.coeff))
theorem Polynomial.coeff_modByMonic_mem_pow_natDegree_mul {R : Type u_2} {S : Type u_3} [CommRing R] [Ring S] [Algebra R S] (p q : Polynomial S) (Mp : Submodule R S) (hp : ∀ (i : ℕ), p.coeff i ∈ Mp) (hp' : 1 ∈ Mp) (Mq : Submodule R S) (hq : ∀ (i : ℕ), q.coeff i ∈ Mq) (hq' : 1 ∈ Mq) (i : ℕ) :
For polynomials p q : R[X], the coefficients of p %ₘ q can be written as sums of products of
coefficients of p and q.
Precisely, each summand needs at most one coefficient of p and deg p coefficients of q.
theorem Polynomial.coeff_divByMonic_mem_pow_natDegree_mul {R : Type u_2} {S : Type u_3} [CommRing R] [Ring S] [Algebra R S] (p q : Polynomial S) (Mp : Submodule R S) (hp : ∀ (i : ℕ), p.coeff i ∈ Mp) (hp' : 1 ∈ Mp) (Mq : Submodule R S) (hq : ∀ (i : ℕ), q.coeff i ∈ Mq) (hq' : 1 ∈ Mq) (i : ℕ) :
For polynomials p q : R[X], the coefficients of p /ₘ q can be written as sums of products of
coefficients of p and q.
Precisely, each summand needs at most one coefficient of p and deg p coefficients of q.
theorem Polynomial.idealSpan_range_update_divByMonic {ι : Type u_1} {R : Type u_2} [CommRing R] [DecidableEq ι] {i j : ι} (hij : i ≠ j) (v : ι → Polynomial R) :