Theorems · Theorem · group theory
Finset.prod_cons
∀ {ι : Type u_1} {M : Type u_4} {s : Finset ι} {a : ι} [inst : CommMonoid M] {f : ι → M} (h : a ∉ s),
∏ x ∈ Finset.cons a s h, f x = f a * ∏ x ∈ s, f x- Cited by
- 60 results in Mathlib
- Foundations
- Depth 58 from the axioms · uses propext, Classical.choice, Quot.sound
- Assumes
- CommMonoid
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites5
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Finsetstatement and proof · cited by 13,712
- Finset.prodstatement · cited by 2,356
- CommMonoidstatement and proof · cited by 2,264
- Finset.consstatement · cited by 221
- Finset.fold_consproof · cited by 6
Cited by60
Results whose statement or proof uses this declaration.
- Finset.prod_le_prodproof · cited by 40
- Finset.prod_pow_eq_pow_sumproof · cited by 18
- Fin.prod_univ_succAboveproof · cited by 9
- Nat.prod_factorial_dvd_factorial_sumproof · cited by 5
- Finset.prod_insertNoneproof · cited by 4
- logDeriv_prodproof · cited by 4
- Polynomial.cyclotomic_coeff_zeroproof · cited by 3
- ENNReal.prod_inv_distribproof · cited by 3
- Polynomial.int_coeff_of_cyclotomic'proof · cited by 3
- Finset.noncommProd_eq_prodproof · cited by 3
- Nat.multinomial_consproof · cited by 3
- MvPowerSeries.le_weightedOrder_prodproof · cited by 3