prod_le_inf — Mathlib

English

For a finite index set s and a function f: s → Ideal R, the product over s is contained in the infimum over s: s.prod f ≤ s.inf f.

Русский

Для конечного множества индексов s и функции f: s → Ideal R произведение по s содержится в наибольшем общем делителе по s: s.prod f ≤ s.inf f.

LaTeX

$$$ s \prod f \le s \inf f. $$$

Lean4

theorem prod_le_inf {s : Finset ι} {f : ι → Ideal R} : s.prod f ≤ s.inf f :=
  multiset_prod_le_inf

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