List

📁 Source: Mathlib/Algebra/BigOperators/Ring/List.lean

Statistics

Metric	Count
Definitions	0
Theorems list_sum_left, list_sum_right, dvd_sum, prod_eq_zero, prod_eq_zero_iff, prod_map_neg, prod_ne_zero, sum_map_mul_left, sum_map_mul_right, sum_zipWith_distrib_left	10
Total	10

Commute

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
list_sum_left 📖	mathematical	Commute Distrib.toMul NonUnitalNonAssocSemiring.toDistrib	Distrib.toAdd MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass	—	symm list_sum_right
list_sum_right 📖	mathematical	Commute Distrib.toMul NonUnitalNonAssocSemiring.toDistrib	Distrib.toAdd MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass	—	zero_right add_right

List

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
dvd_sum 📖	mathematical	semigroupDvd SemigroupWithZero.toSemigroup NonUnitalSemiring.toSemigroupWithZero	Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonUnitalSemiring.toNonUnitalNonAssocSemiring MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass	—	dvd_zero dvd_add Distrib.leftDistribClass
prod_eq_zero 📖	mathematical	MulZeroClass.toZero MulZeroOneClass.toMulZeroClass MonoidWithZero.toMulZeroOneClass	MulZeroClass.toMul MulOne.toOne MulOneClass.toMulOne MulZeroOneClass.toMulOneClass	—	mul_eq_zero_of_left mul_eq_zero_of_right
prod_eq_zero_iff 📖	mathematical	—	MulZeroClass.toMul MulZeroOneClass.toMulZeroClass MonoidWithZero.toMulZeroOneClass MulOne.toOne MulOneClass.toMulOne MulZeroOneClass.toMulOneClass MulZeroClass.toZero	—	NeZero.one mul_eq_zero
prod_map_neg 📖	mathematical	—	MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass MulOne.toOne InvolutiveNeg.toNeg HasDistribNeg.toInvolutiveNeg Monoid.toNatPow	—	pow_zero mul_one neg_mul pow_succ mul_neg Commute.left_comm Commute.pow_left Commute.neg_one_left
prod_ne_zero 📖	—	MulZeroClass.toZero MulZeroOneClass.toMulZeroClass MonoidWithZero.toMulZeroOneClass	—	—	prod_eq_zero_iff
sum_map_mul_left 📖	mathematical	—	Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass Distrib.toMul	—	sum_map_hom AddMonoidHom.instAddMonoidHomClass
sum_map_mul_right 📖	mathematical	—	Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass Distrib.toMul	—	sum_map_hom AddMonoidHom.instAddMonoidHomClass
sum_zipWith_distrib_left 📖	mathematical	—	Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass Distrib.toMul	—	MulZeroClass.mul_zero mul_add Distrib.leftDistribClass

---

← Back to Index