prod_pow — Mathlib

English

If α is finite and f: α → ℕ, then the product of g(a) raised to f(a) over a equals the product over all a of g(a)^{f(a)}.

Русский

Пусть α конечен и f: α → ℕ; тогда произведение g(a)^{f(a)} по всем a равно произведению по всем a:g(a)^{f(a)}.

LaTeX

$$$$ (f.prod (\\\\lambda a b, g(a)^{b})) = \\prod_{a} g(a)^{f(a)} $$$$

Lean4

@[to_additive (attr := simp)]
theorem prod_pow [Fintype α] (f : α →₀ ℕ) (g : α → N) : (f.prod fun a b => g a ^ b) = ∏ a, g a ^ f a :=
  f.prod_fintype _ fun _ ↦ pow_zero _

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