Theorems · Theorem · group theory

Finset.prod_fn

∀ {α : Type u_7} {M : α → Type u_8} {ι : Type u_9} [inst : (a : α) → CommMonoid (M a)] (s : Finset ι)
  (g : ι → (a : α) → M a), ∏ c ∈ s, g c = fun a => ∏ c ∈ s, g c a

An 'unapplied' analogue of Finset.prod_apply.

Defined in

Mathlib.Algebra.BigOperators.Pi

Cited by

9 results in Mathlib

Foundations

Depth 17 from the axioms · uses propext, Quot.sound

Assumes

CommMonoid