finsetProd_mem — Mathlib

English

Let I be a two-sided ideal of a commutative ring R, and s a finite set (Finset) of indices with f: ι → R. If there exists x ∈ s with f x ∈ I, then the finite product ∏_{x∈s} f x lies in I.

Русский

Пусть I — двусторонний идеал кольца R, а s — конечное множество индексов, с функцией f: ι → R. Если найдётся x ∈ s такое, что f(x) ∈ I, то произведение всех f(x) по x ∈ s принадлежит I.

LaTeX

$$$\\left(\\exists x \\in s,\\ f(x) \\in I\\right) \\rightarrow s.prod f \\in I$$$

Lean4

theorem finsetProd_mem {ι : Type*} (s : Finset ι) (f : ι → R) (hs : ∃ x ∈ s, f x ∈ I) : s.prod f ∈ I :=
  by
  rcases s
  simpa using multiSetProd_mem (hs := hs)

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