noncommProd_mem — Mathlib

English

In a submonoid of a monoid, the finite noncommutative product over a finite set t with a commutation pattern is in the submonoid when each factor lies in the submonoid.

Русский

В подмономоде моноида конечное неканоническое произведение по конечному множеству t с заданной схемой взаимного приведения находится в подмономоде, если каждый фактор принадлежит подмономодy.

LaTeX

$$$$ t.noncommProd f comm \\in S $$$$

Lean4

@[to_additive]
theorem noncommProd_mem (S : Submonoid M) {ι : Type*} (t : Finset ι) (f : ι → M) (comm) (h : ∀ c ∈ t, f c ∈ S) :
    t.noncommProd f comm ∈ S := by
  apply multiset_noncommProd_mem
  intro y
  rw [Multiset.mem_map]
  rintro ⟨x, ⟨hx, rfl⟩⟩
  exact h x hx

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