prod_eq_pow_single — Mathlib

English

Let l be a list over α, a ∈ α, and f: α → M. If every a' ≠ a in l satisfies f(a') = 1, then (l.map f).prod = f(a)^{l.count(a)}.

Русский

Пусть l — список над α, а ∈ α, и f: α → M. Если для всех a' ≠ a из l выполняется f(a') = 1, то произведение отображённых значений равно f(a) в степени количества вхождений a в l.

LaTeX

$$$ (l.map f).prod = f(a)^{\ l.count a \} $$$

Lean4

@[to_additive]
theorem prod_eq_pow_single [DecidableEq M] (a : M) (h : ∀ a', a' ≠ a → a' ∈ l → a' = 1) : l.prod = a ^ l.count a :=
  _root_.trans (by rw [map_id]) (prod_map_eq_pow_single a id h)

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