Theorems · Definition · ring theory
Finsupp.prod
{α : Type u_1} → {M : Type u_8} → {N : Type u_10} → [inst : Zero M] → [CommMonoid N] → (α →₀ M) → (α → M → N) → Nprod f g is the product of g a (f a) over the support of f.
- Cited by
- 231 results in Mathlib
- Foundations
- Depth 59 from the axioms, rests on 849 definitions · uses propext, Classical.choice, Quot.sound
- Assumes
- ZeroCommMonoid
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.
- DFunLike.coeproof · cited by 62,936
- Finsuppstatement and proof · cited by 5,255
- Finset.prodproof · cited by 2,356
- CommMonoidstatement and proof · cited by 2,264
- Finsupp.supportproof · cited by 828
Cited by246
Results whose statement or proof uses this declaration.
- MvPolynomial.eval₂proof · cited by 103
- Finsupp.prod_single_indexstatement · cited by 26
- MvPolynomial.eval₂_addproof · cited by 23
- Nat.prod_factorization_pow_eq_selfstatement and proof · cited by 22
- MvPolynomial.monomial_eqstatement and proof · cited by 20
- Nat.factorization_le_iff_dvdproof · cited by 18
- Nat.factorizationLCMLeftproof · cited by 15
- Nat.factorizationLCMRightproof · cited by 15
- MvPowerSeries.coeff_subststatement and proof · cited by 15
- MvPowerSeries.rescaleproof · cited by 14
- MvPolynomial.eval₂_monomialstatement and proof · cited by 13
- Finsupp.prod_of_support_subsetstatement · cited by 13
Showing the 200 most cited of 246.