noncommProd_eq_pow_card — Mathlib

English

If α is a commutative monoid, then the noncommProd over any s equals the ordinary product: s.noncommProd comm = prod s.

Русский

Если α — коммутативный моноид, то некоммутативное произведение по любому s равно обычному произведению: s.noncommProd comm = prod s.

LaTeX

$$$\\forall s:\\mathrm{Multiset}\\,\\alpha\\;[CommMonoid\\;\\alpha]\\; (s.noncommProd comm) = s.prod$$$

Lean4

@[to_additive noncommSum_eq_card_nsmul]
theorem noncommProd_eq_pow_card (s : Multiset α) (comm) (m : α) (h : ∀ x ∈ s, x = m) :
    s.noncommProd comm = m ^ Multiset.card s :=
  by
  induction s using Quotient.inductionOn
  simp only [quot_mk_to_coe, noncommProd_coe, coe_card, mem_coe] at *
  exact List.prod_eq_pow_card _ m h

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