multiSetProd_mem — Mathlib

English

Let I be a two-sided ideal in a commutative ring R, and let s be a multiset of indices with f: ι → R. If there exists x ∈ s with f(x) ∈ I, then the product of all f(x) (taken over s) lies in I.

Русский

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

LaTeX

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

Lean4

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

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