Theorems · Theorem · group theory

finprod_prod_comm

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

Defined in

Mathlib.Algebra.BigOperators.Finprod

Cited by

3 results in Mathlib

Foundations

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

Assumes

CommMonoid