BigOperators

📁 Source: Mathlib/RingTheory/Congruence/BigOperators.lean

Statistics

Metric	Count
Definitions	0
Theorems finsetSum, listSum, multisetSum	3
Total	3

RingCon

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
finsetSum 📖	mathematical	DFunLike.coe RingCon AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup instFunLikeForallProp	Finset.sum	—	AddCon.finset_sum
listSum 📖	mathematical	DFunLike.coe RingCon AddSemigroup.toAdd AddMonoid.toAddSemigroup instFunLikeForallProp	AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass	—	AddCon.list_sum
multisetSum 📖	mathematical	DFunLike.coe RingCon AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup instFunLikeForallProp	Multiset.sum Multiset.map	—	AddCon.multiset_sum

---

← Back to Index