coeff_mul_mem_ideal_mul_ideal_of_coeff_mem_ideal

English

If coefficients of f are in I up to n and coefficients of g are in J up to n, then each coefficient of f·g up to n lies in the product I·J.

Русский

Если коэффициенты f лежат в I до n, а коэффициенты g в J до n, то каждый коэффициент произведения f·g до n лежит в I·J.

LaTeX

$$$\\forall i \\le n, \\; \\mathrm{coeff}_i(fg) \\in I J$$$

Lean4

theorem coeff_mul_mem_ideal_mul_ideal_of_coeff_mem_ideal (hf : ∀ i ≤ n, coeff i f ∈ I) (hg : ∀ i ≤ n, coeff i g ∈ J) :
    ∀ i ≤ n, coeff i (f * g) ∈ I * J := fun i hi ↦ by
  rw [coeff_mul]
  exact
    Ideal.sum_mem _ fun p hp ↦
      Ideal.mul_mem_mul (hf _ ((Finset.antidiagonal.fst_le hp).trans hi))
        (hg _ ((Finset.antidiagonal.snd_le hp).trans hi))

Похожие утверждения