Theorems · Theorem · group theory
Finset.prod_apply
∀ {ι : Type u_1} {α : Type u_7} {M : α → Type u_8} [inst : (a : α) → CommMonoid (M a)] (a : α) (s : Finset ι)
(g : ι → (a : α) → M a), (∏ c ∈ s, g c) a = ∏ c ∈ s, g c a- Defined in
- Mathlib.Algebra.BigOperators.Pi
- Cited by
- 70 results in Mathlib
- Foundations
- Depth 16 from the axioms · uses propext, 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
- map_prodproof · cited by 108
- Pi.evalMonoidHomproof · cited by 14
Cited by70
Results whose statement or proof uses this declaration.
- Finset.prod_fnproof · cited by 9
- ProbabilityTheory.Kernel.iIndepFun.indepFun_finsetProd_of_notMemproof · cited by 5
- prod_indicator_applyproof · cited by 4
- ProbabilityTheory.iIndepFun.charFunDual_map_finsetSum_eq_prodproof · cited by 4
- indicator_indepFun_pi_of_prod_bcfproof · cited by 4
- Measure.ext_of_integral_prod_mul_prod_boundedContinuousFunctionproof · cited by 4
- Summable.hasProdUniformlyOn_one_addproof · cited by 3
- ProbabilityTheory.iIndepFun.charFun_map_finsetSum_eq_prodproof · cited by 3
- indepFun_pi_of_prod_bcfproof · cited by 3
- meromorphicNFAt_prodproof · cited by 3
- ProbabilityTheory.Kernel.iIndepFun.indepFun_finsetProd_of_notMem₀proof · cited by 3
- MeromorphicOn.extract_zeros_poles_logproof · cited by 3