prod_eq_pow_single — Mathlib

English

Let a ∈ M and m a multiset with counts; if the only nontrivial element is a, then s.prod = a^{count a}.

Русский

Пусть a ∈ M и мультимножество имеет только счет a в роли отличного элемента; тогда prod сохраняется как a^{count a}.

LaTeX

$$$ s.\mathrm{prod} = a^{\mathrm{count}\ a\ s} $$$

Lean4

@[to_additive]
theorem prod_eq_pow_single [DecidableEq M] (a : M) (h : ∀ a' ≠ a, a' ∈ s → a' = 1) : s.prod = a ^ s.count a := by
  induction s using Quotient.inductionOn; simp [List.prod_eq_pow_single a h]

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