Theorems · Theorem · group theory

finprod_cond_eq_prod_of_cond_iff

∀ {α : Type u_1} {M : Type u_5} [inst : CommMonoid M] (f : α → M) {p : α → Prop} {t : Finset α},
  (∀ {x : α}, f x ≠ 1 → (p x ↔ x ∈ t)) → ∏ᶠ (i : α) (_ : p i), f i = ∏ i ∈ t, f i

Defined in

Mathlib.Algebra.BigOperators.Finprod

Cited by

6 results in Mathlib

Foundations

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

Assumes

CommMonoid