Documentation Verification Report

BigOperators

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

Statistics

Metric	Count
Definitions	0
Theorems `finset_sum`, `list_sum`, `multiset_sum`, `finset_prod`, `list_prod`, `multiset_prod`	6
Total	6

AddCon

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`finset_sum` 📖	mathematical	`DFunLike.coe` `AddCon` `AddZero.toAdd` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `instFunLikeForallProp`	`Finset.sum`	—	`multiset_sum`
`list_sum` 📖	mathematical	`DFunLike.coe` `AddCon` `AddZero.toAdd` `AddZeroClass.toAddZero` `instFunLikeForallProp`	`AddZero.toZero`	—	`refl` `add`
`multiset_sum` 📖	mathematical	`DFunLike.coe` `AddCon` `AddZero.toAdd` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `instFunLikeForallProp`	`Multiset.sum` `Multiset.map`	—	`list_sum`

Con

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`finset_prod` 📖	mathematical	`DFunLike.coe` `Con` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `CommMonoid.toMonoid` `instFunLikeForallProp`	`Finset.prod`	—	`multiset_prod`
`list_prod` 📖	mathematical	`DFunLike.coe` `Con` `MulOne.toMul` `MulOneClass.toMulOne` `instFunLikeForallProp`	`MulOne.toOne`	—	`refl` `mul`
`multiset_prod` 📖	mathematical	`DFunLike.coe` `Con` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `CommMonoid.toMonoid` `instFunLikeForallProp`	`Multiset.prod` `Multiset.map`	—	`list_prod`

---

← Back to Index