prod_mem — Mathlib

English

Product of a subring of a commutative ring indexed by a finite set is in the subring.

Русский

Произведение элементов подп кольца внутри комм кольца по индексу Finset принадлежит подп кольцу.

LaTeX

$$$\\forall R\\, [\\text{CommRing }R]\\, (s: Subring R)\\, (t: Finset\\, ι)\\, (f: ι \\to R),\\ (\\forall c \\in t, f c \\in s) \\Rightarrow (\\prod i \\in t, f i) \\in s.$$$

Lean4

/-- Product of elements of a subring of a `CommRing` indexed by a `Finset` is in the
subring. -/
protected theorem prod_mem {R : Type*} [CommRing R] (s : Subring R) {ι : Type*} {t : Finset ι} {f : ι → R}
    (h : ∀ c ∈ t, f c ∈ s) : (∏ i ∈ t, f i) ∈ s :=
  prod_mem h

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