pow_count — Mathlib

English

Count of a in a multiset relates to the product of a's: a^{s.count a} equals the product of elements equal to a in s.

Русский

Число вхождений a в мультсет определяет произведение элементов равных a: a^{s.count a} = prod( (s.filter (Eq a)) ).

LaTeX

$$$a^{s.count a} = (s.filter (Eq a)).prod$$$

Lean4

@[to_additive]
theorem pow_count [DecidableEq M] (a : M) : a ^ s.count a = (s.filter (Eq a)).prod := by rw [filter_eq, prod_replicate]

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