BigOperators

📁 Source: Mathlib/Data/NNRat/BigOperators.lean

Statistics

Metric	Count
Definitions	0
Theorems cast_listProd, cast_listSum, cast_multisetProd, cast_multisetSum, cast_prod, cast_sum, toNNRat_prod_of_nonneg, toNNRat_sum_of_nonneg	8
Total	8

NNRat

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
cast_listProd 📖	mathematical	—	cast DivisionSemiring.toNNRatCast NNRat Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring DivisionSemiring.toSemiring Semifield.toDivisionSemiring instSemifield AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne	—	map_list_prod MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass
cast_listSum 📖	mathematical	—	cast DivisionSemiring.toNNRatCast NNRat Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring DivisionSemiring.toSemiring Semifield.toDivisionSemiring instSemifield MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass	—	map_list_sum RingHomClass.toAddMonoidHomClass RingHom.instRingHomClass
cast_multisetProd 📖	mathematical	—	cast DivisionSemiring.toNNRatCast Semifield.toDivisionSemiring Multiset.prod NNRat CommSemiring.toCommMonoid instCommSemiringNNRat Semifield.toCommSemiring Multiset.map	—	map_multiset_prod MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass
cast_multisetSum 📖	mathematical	—	cast DivisionSemiring.toNNRatCast Multiset.sum NNRat NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring DivisionSemiring.toSemiring Semifield.toDivisionSemiring instSemifield Multiset.map	—	map_multiset_sum RingHomClass.toAddMonoidHomClass RingHom.instRingHomClass
cast_prod 📖	mathematical	—	cast DivisionSemiring.toNNRatCast Semifield.toDivisionSemiring Finset.prod NNRat CommSemiring.toCommMonoid instCommSemiringNNRat Semifield.toCommSemiring	—	map_prod MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass
cast_sum 📖	mathematical	—	cast DivisionSemiring.toNNRatCast Finset.sum NNRat NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring DivisionSemiring.toSemiring Semifield.toDivisionSemiring instSemifield	—	map_sum RingHomClass.toAddMonoidHomClass RingHom.instRingHomClass
toNNRat_prod_of_nonneg 📖	mathematical	—	Rat.toNNRat Finset.prod Rat.commMonoid NNRat CommSemiring.toCommMonoid instCommSemiringNNRat	—	cast_prod Rat.instCharZero Rat.coe_toNNRat Finset.prod_nonneg Rat.instZeroLEOneClass Rat.instPosMulMono Finset.prod_congr
toNNRat_sum_of_nonneg 📖	mathematical	—	Rat.toNNRat Finset.sum Rat.addCommMonoid NNRat NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring DivisionSemiring.toSemiring Semifield.toDivisionSemiring instSemifield	—	cast_sum Rat.instCharZero Rat.coe_toNNRat Finset.sum_nonneg Rat.instAddLeftMono Finset.sum_congr

---

← Back to Index