English
If every x in s satisfies f(x) = m for some m in β, then the noncommutative product over s equals m raised to the cardinality of s.
Русский
Если для каждого x ∈ s выполняется f(x) = m, то некоммопрод по s равен m^{|s|}.
LaTeX
$$$ (s : \mathrm{Finset} \; \alpha) \; (f : \alpha \to \beta) \; (comm : s.\text{toSet}.Pairwise (\mathrm{Commute} \; on \; f)) (m : \beta) (h : \forall x \in s, f x = m) : s.noncommProd f comm = m^{s.card}$$$
Lean4
@[to_additive noncommSum_eq_card_nsmul]
theorem noncommProd_eq_pow_card (s : Finset α) (f : α → β) (comm) (m : β) (h : ∀ x ∈ s, f x = m) :
s.noncommProd f comm = m ^ s.card :=
by
rw [noncommProd, Multiset.noncommProd_eq_pow_card _ _ m]
· simp only [Finset.card_def, Multiset.card_map]
· simpa using h
