English
For polynomials p,q over a ring with Mp,Mq submodules and hp,hq membership, the coefficient of p /ₘ q lies in Mq^{deg p} * Mp.
Русский
Для многочленов p,q над кольцом с подмодулями Mp,Mq и условиями принадлежности коэффициентов, коэффициент p /ₘ q принадлежит Mq^{deg p} * Mp.
LaTeX
$$$ (p /ₘ q).coeff i ∈ Mq ^ p.natDegree * Mp $$$
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_divByMonic_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 divByMonic
split_ifs with H
· refine SetLike.le_def.mp ?_ (coeff_divModByMonicAux_mem_span_pow_mul_span (R := R) p q H i).1
gcongr <;> exact sup_le (by simpa) (by simpa [Submodule.span_le, Set.range_subset_iff])
· simp
