coeff_mul_mem_ideal_of_coeff_left_mem_ideal

English

Let I be a two-sided ideal of a semiring A, and f,g ∈ A[[X]]. If for every i ≤ n the coefficient coeff_i f lies in I, then for every i ≤ n the coefficient coeff_i(f·g) lies in I.

Русский

Пусть I — двусторонний идеал полугруппы A, f,g ∈ A[[X]]. Если для каждого i ≤ n коэффициент coeff_i f принадлежит I, то для каждого i ≤ n коэффициент coeff_i(f·g) принадлежит I.

LaTeX

$$$ (\\forall i \\le n, \\operatorname{coeff}_i f \\in I) \\Rightarrow (\\forall i \\le n, \\operatorname{coeff}_i(f g) \\in I)$$$

Lean4

theorem coeff_mul_mem_ideal_of_coeff_left_mem_ideal (hf : ∀ i ≤ n, coeff i f ∈ I) : ∀ i ≤ n, coeff i (f * g) ∈ I := by
  simpa only [Ideal.IsTwoSided.mul_one] using
    coeff_mul_mem_ideal_mul_ideal_of_coeff_mem_ideal (J := 1) (g := g) n hf (by simp)

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