BigOperators

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

Statistics

Metric	Count
Definitions	0
Theorems finsetProd_mem, finsetSum_mem, listProd_mem, listSum_mem, multiSetProd_mem, multisetSum_mem	6
Total	6

TwoSidedIdeal

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
finsetProd_mem 📖	mathematical	Finset Finset.instMembership TwoSidedIdeal NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing SetLike.instMembership setLike	Finset.prod CommRing.toCommMonoid	—	multiSetProd_mem
finsetSum_mem 📖	mathematical	TwoSidedIdeal SetLike.instMembership setLike	Finset.sum NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring	—	mem_iff Finset.sum_const_zero RingCon.finsetSum
listProd_mem 📖	mathematical	TwoSidedIdeal NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing SetLike.instMembership setLike	Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne	—	mul_mem_right mul_mem_left
listSum_mem 📖	mathematical	TwoSidedIdeal SetLike.instMembership setLike	Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass	—	mem_iff List.sum_map_zero RingCon.listSum
multiSetProd_mem 📖	mathematical	Multiset Multiset.instMembership TwoSidedIdeal NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing SetLike.instMembership setLike	Multiset.prod CommRing.toCommMonoid Multiset.map	—	listProd_mem
multisetSum_mem 📖	mathematical	TwoSidedIdeal SetLike.instMembership setLike	Multiset.sum NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring Multiset.map	—	mem_iff Multiset.sum_map_zero RingCon.multisetSum

---

← Back to Index