English
If a finite family of polynomials f i with coefficients in I^{n i - k} for all k, then the k-th coefficient of the product ∏ f i lies in I^{(sum n) - k}.
Русский
Если конечная совокупность полиномов имеет коэффициенты в I^{n_i - k} для каждого k, то k-й коэффициент произведения лежит в I^{(sum n) - k}.
LaTeX
$$$ (\\forall i \\in s)(\\forall k)\\ (f_i).coeff(k) \\in I^{(n_i - k)} \\Rightarrow (\\prod_{i \\in s} f_i).coeff(k) \\in I^{(\\sum n_i) - k}$$$
Lean4
/-- If `I` is an ideal, and `pᵢ` is a finite family of polynomials each satisfying
`∀ k, (pᵢ)ₖ ∈ Iⁿⁱ⁻ᵏ` for some `nᵢ`, then `p = ∏ pᵢ` also satisfies `∀ k, pₖ ∈ Iⁿ⁻ᵏ` with `n = ∑ nᵢ`.
-/
theorem _root_.Polynomial.coeff_prod_mem_ideal_pow_tsub {ι : Type*} (s : Finset ι) (f : ι → R[X]) (I : Ideal R)
(n : ι → ℕ) (h : ∀ i ∈ s, ∀ (k), (f i).coeff k ∈ I ^ (n i - k)) (k : ℕ) : (s.prod f).coeff k ∈ I ^ (s.sum n - k) :=
by
classical
induction s using Finset.induction generalizing k with
| empty =>
rw [sum_empty, prod_empty, coeff_one, zero_tsub, pow_zero, Ideal.one_eq_top]
exact Submodule.mem_top
| insert a s ha hs =>
rw [sum_insert ha, prod_insert ha, coeff_mul]
apply sum_mem
rintro ⟨i, j⟩ e
obtain rfl : i + j = k := mem_antidiagonal.mp e
apply Ideal.pow_le_pow_right add_tsub_add_le_tsub_add_tsub
rw [pow_add]
exact Ideal.mul_mem_mul (by grind) (by grind)
