list_prod_mem — Mathlib

English

If every element of a list l lies in a subgroup K, then the list product lies in K.

Русский

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

LaTeX

$$$\\forall x \\in l, x \\in K \\Rightarrow l.prod \\in K$$$

Lean4

/-- Product of a list of elements in a subgroup is in the subgroup. -/
@[to_additive /-- Sum of a list of elements in an `AddSubgroup` is in the `AddSubgroup`. -/
    ]
protected theorem list_prod_mem {l : List G} : (∀ x ∈ l, x ∈ K) → l.prod ∈ K :=
  list_prod_mem

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