prod_mem — Mathlib

English

Let I be an ideal of a commutative semiring α, and s a finite set with i ∈ s and f(i) ∈ I. Then ∏ i∈s f(i) ∈ I.

Русский

Пусть I — идеал коммутативного полускольца α, а s — конечный набор; если существует i ∈ s такой, что f(i) ∈ I, то произведение ∏_{i∈s} f(i) принадлежит I.

LaTeX

$$$\\exists I\\in\\text{Ideal}(\\alpha),\\ i\\in s:\\, f(i)\\in I \\Rightarrow \\prod_{i\\in s} f(i) \\in I$$$

Lean4

theorem prod_mem {ι : Type*} {f : ι → α} {s : Finset ι} (I : Ideal α) {i : ι} (hi : i ∈ s) (hfi : f i ∈ I) :
    ∏ i ∈ s, f i ∈ I := by
  classical
  rw [Finset.prod_eq_prod_diff_singleton_mul hi]
  exact Ideal.mul_mem_left _ _ hfi

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