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.

@[irreducible]

theorem Polynomial.coeff_divModByMonicAux_mem_span_pow_mul_span {R : Type u_1} {S : Type u_2} [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_1} {S : Type u_2} [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 : ℕ) : (p %ₘ q).coeff i ∈ Mq ^ p.natDegree * Mp

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_1} {S : Type u_2} [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 : ℕ) : (p /ₘ q).coeff i ∈ Mq ^ p.natDegree * Mp

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.