Documentation Verification Report

BigOperators

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

Statistics

Metric	Count
Definitions	0
Theorems `cast_list_prod`, `cast_list_sum`, `cast_multiset_prod`, `cast_multiset_sum`, `cast_prod`, `cast_sum`	6
Total	6

Rat

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`cast_list_prod` 📖	mathematical	—	`DivisionRing.toRatCast` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `DivisionRing.toRing` `instDivisionRing` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing`	—	`map_list_prod` `MonoidWithZeroHomClass.toMonoidHomClass` `RingHomClass.toMonoidWithZeroHomClass` `RingHom.instRingHomClass`
`cast_list_sum` 📖	mathematical	—	`DivisionRing.toRatCast` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `commRing` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `DivisionRing.toRing`	—	`map_list_sum` `RingHomClass.toAddMonoidHomClass` `RingHom.instRingHomClass`
`cast_multiset_prod` 📖	mathematical	—	`DivisionRing.toRatCast` `Field.toDivisionRing` `Multiset.prod` `commMonoid` `CommRing.toCommMonoid` `Field.toCommRing` `Multiset.map`	—	`map_multiset_prod` `MonoidWithZeroHomClass.toMonoidHomClass` `RingHomClass.toMonoidWithZeroHomClass` `RingHom.instRingHomClass`
`cast_multiset_sum` 📖	mathematical	—	`DivisionRing.toRatCast` `Multiset.sum` `addCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `DivisionRing.toRing` `Multiset.map`	—	`map_multiset_sum` `RingHomClass.toAddMonoidHomClass` `RingHom.instRingHomClass`
`cast_prod` 📖	mathematical	—	`DivisionRing.toRatCast` `Field.toDivisionRing` `Finset.prod` `commMonoid` `CommRing.toCommMonoid` `Field.toCommRing`	—	`map_prod` `MonoidWithZeroHomClass.toMonoidHomClass` `RingHomClass.toMonoidWithZeroHomClass` `RingHom.instRingHomClass`
`cast_sum` 📖	mathematical	—	`DivisionRing.toRatCast` `Finset.sum` `addCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `DivisionRing.toRing`	—	`map_sum` `RingHomClass.toAddMonoidHomClass` `RingHom.instRingHomClass`

---

← Back to Index