Theorems · Definition · group theory
finprod
{M : Type u_7} → {α : Sort u_8} → [CommMonoid M] → (α → M) → MProduct of f x as x ranges over the elements of the multiplicative support of f, if it's
finite. One otherwise.
- Defined in
- Mathlib.Algebra.BigOperators.Finprod
- Cited by
- 257 results in Mathlib
- Foundations
- Depth 70 from the axioms, rests on 1,018 definitions · uses propext, Classical.choice, Quot.sound
- Assumes
- CommMonoid
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites1
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- CommMonoidstatement · cited by 2,264
Cited by270
Results whose statement or proof uses this declaration.
- Multipliable.hasProdproof · cited by 88
- Height.mulHeightproof · cited by 64
- Height.mulHeight₁proof · cited by 35
- finprod_eq_prod_of_mulSupport_subsetstatement · cited by 21
- Height.mulHeight_zeroproof · cited by 17
- Height.mulHeight_eqstatement and proof · cited by 14
- finprod_of_infinite_mulSupportstatement · cited by 13
- tprod_oneproof · cited by 12
- finprod_onestatement · cited by 12
- MeromorphicOn.circleIntegrable_log_normproof · cited by 11
- tprod_defstatement and proof · cited by 11
- Height.mulHeightBoundproof · cited by 10
Showing the 200 most cited of 270.