multiset_prod_mem — Mathlib

English

If every element of a multiset g lies in K, then the product g.prod lies in K (in a commutative group).

Русский

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

LaTeX

$$$\\forall a \\in g, a \\in K \\Rightarrow g.prod \\in K$$$

Lean4

/-- Product of a multiset of elements in a subgroup of a `CommGroup` is in the subgroup. -/
@[to_additive /-- Sum of a multiset of elements in an `AddSubgroup` of an `AddCommGroup` is in
    the `AddSubgroup`. -/
    ]
protected theorem multiset_prod_mem {G} [CommGroup G] (K : Subgroup G) (g : Multiset G) :
    (∀ a ∈ g, a ∈ K) → g.prod ∈ K :=
  multiset_prod_mem g

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