Theorems · Theorem · ring theory

Finsupp.prod_zpow

∀ {α : Type u_1} {N : Type u_16} [inst : DivisionCommMonoid N] [inst_1 : Fintype α] (f : α →₀ ℤ) (g : α → N),
  (f.prod fun a b => g a ^ b) = ∏ a, g a ^ f a

Defined in

Mathlib.Algebra.BigOperators.Finsupp.Basic

Cited by

2 results in Mathlib

Foundations

Depth 70 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

DivisionCommMonoidFintype