list_prod_mem — Mathlib

English

If every element of a list l lies in a Subsemiring s, then the product of the elements of l lies in s.

Русский

Если каждый элемент списка l принадлежит Subsemiring s, то произведение элементов l принадлежит s.

LaTeX

$${l : List R} → (∀ x ∈ l, x ∈ s) → l.prod ∈ s$$

Lean4

/-- Product of a list of elements in a `Subsemiring` is in the `Subsemiring`. -/
nonrec theorem list_prod_mem {R : Type*} [Semiring R] (s : Subsemiring R) {l : List R} :
    (∀ x ∈ l, x ∈ s) → l.prod ∈ s :=
  list_prod_mem

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