Theorems · Theorem · group theory

Finset.prod_attach_eq_prod_dite

∀ {ι : Type u_1} {M : Type u_3} [inst : CommMonoid M] [inst_1 : Fintype ι] (s : Finset ι) (f : ↥s → M)
  [inst_2 : DecidablePred fun x => x ∈ s], ∏ i ∈ s.attach, f i = ∏ i, if h : i ∈ s then f ⟨i, h⟩ else 1

Defined in

Mathlib.Algebra.BigOperators.Group.Finset.Piecewise

Cited by

1 results in Mathlib

Foundations

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

Assumes

CommMonoidFintypeDecidablePred