Theorems · Theorem · general algebraic systems
Finset.prod_insertNone
∀ {α : Type u_1} {M : Type u_2} [inst : CommMonoid M] (f : Option α → M) (s : Finset α),
∏ x ∈ Finset.insertNone s, f x = f none * ∏ x ∈ s, f (some x)- Defined in
- Mathlib.Algebra.BigOperators.Option
- Cited by
- 4 results in Mathlib
- Foundations
- Depth 62 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.
Cites11
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- DFunLike.coestatement · cited by 62,936
- Finsetstatement and proof · cited by 13,712
- Finset.prodstatement and proof · cited by 2,356
- CommMonoidstatement and proof · cited by 2,264
- Finset.prod_congrproof · cited by 646
- OrderEmbeddingstatement · cited by 619
- Finset.prod_mapproof · cited by 75
- Finset.prod_consproof · cited by 60
- Function.Embedding.someproof · cited by 43
- Finset.insertNonestatement · cited by 21
- Function.Embedding.some_applyproof · cited by 11
Cited by4
Results whose statement or proof uses this declaration.
- Fintype.prod_optionproof · cited by 2
- ENNReal.lintegral_mul_prod_norm_pow_leproof · cited by 1
- MeasureTheory.Measure.pi_map_piOptionEquivProdproof · cited by 0
- Finset.mul_prod_eq_prod_insertNoneproof · cited by 0