coeff_mul_mem_ideal_of_coeff_right_mem_ideal'

English

Let I be an ideal of a semiring A, and f,g ∈ A[[X]]. If every coefficient of g lies in I, then every coefficient of the product f·g lies in I.

Русский

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

LaTeX

$$$ (\\forall i : \\mathbb{N}, \\operatorname{coeff}_i(g) \\in I) \\Rightarrow ( \\forall i : \\mathbb{N}, \\operatorname{coeff}_i(f \\cdot g) \\in I)$$$

Lean4

theorem coeff_mul_mem_ideal_of_coeff_right_mem_ideal' (hg : ∀ i, coeff i g ∈ I) : ∀ i, coeff i (f * g) ∈ I := by
  simpa using coeff_mul_mem_ideal_mul_ideal_of_coeff_mem_ideal' (I := ⊤) (f := f) (by simp) hg

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