English
For polynomials p,q with q monic, each coefficient of p divModByMonicAux hq lies in the same span-based product as above, and this holds for both quotient and remainder.
Русский
Для многочленов p,q с q мононичным каждый коэффициент p деления по Q лежит в той же произведении пространств на основе разреженности, применимо и к частям частного и остатка.
LaTeX
$$$ (p.divModByMonicAux hq).coeff i ∈ span(q)^{deg(p)} * span(p) $$$
Lean4
/-- 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 coeff_modByMonic_mem_pow_natDegree_mul (p q : S[X]) (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 := by
delta modByMonic
split_ifs with H
· refine SetLike.le_def.mp ?_ (coeff_divModByMonicAux_mem_span_pow_mul_span (R := R) p q H i).2
gcongr <;> exact sup_le (by simpa) (by simpa [Submodule.span_le, Set.range_subset_iff])
· rw [← one_mul (p.coeff i), ← one_pow p.natDegree]
exact Submodule.mul_mem_mul (Submodule.pow_mem_pow Mq hq' _) (hp i)
