list_prod_mem — Mathlib

English

If every element of a list l of M lies in a submonoid S, then the product of all elements of l lies in S.

Русский

Если каждый элемент списка l множества M принадлежит подмономоиду S, то произведение всех элементов списка принадлежит S.

LaTeX

$$$$ \\forall l:\\mathrm{List}(M), \\; (\\forall x \\in l, x \\in S) \\Rightarrow l.D\\,\\mathrm{prod} \\in S $$$$

Lean4

/-- Product of a list of elements in a submonoid is in the submonoid. -/
@[to_additive /-- Sum of a list of elements in an `AddSubmonoid` is in the `AddSubmonoid`. -/
    ]
theorem list_prod_mem {l : List M} (hl : ∀ x ∈ l, x ∈ s) : l.prod ∈ s :=
  _root_.list_prod_mem hl

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