Theorems · Theorem · group theory

prod_finprod_comm

∀ {α : Type u_1} {β : Type u_2} {M : Type u_5} [inst : CommMonoid M] (s : Finset α) (f : α → β → M),
  (∀ a ∈ s, Function.HasFiniteMulSupport (f a)) → ∏ a ∈ s, ∏ᶠ (b : β), f a b = ∏ᶠ (b : β), ∏ a ∈ s, f a b

Defined in

Mathlib.Algebra.BigOperators.Finprod

Cited by

0 results in Mathlib

Foundations

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

Assumes

CommMonoid