noncommProd_eq_prod — Mathlib

English

If every element of s equals m, then the noncommProd over s equals m raised to the power of the cardinality of s: s.noncommProd comm = m^{|s|}.

Русский

Если все элементы s равны m, то некоммутативное произведение по s равно m в степени |s|.

LaTeX

$$$\\forall s:\\mathrm{Multiset}\\,\\alpha\\; (\\forall x\\in s, x=m) \\Rightarrow s.noncommProd comm = m^{\\lvert s\\rvert}$$$

Lean4

@[to_additive]
theorem noncommProd_eq_prod {α : Type*} [CommMonoid α] (s : Multiset α) :
    (noncommProd s fun _ _ _ _ _ => Commute.all _ _) = prod s :=
  by
  induction s using Quotient.inductionOn
  simp

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