Documentation Verification Report

Lemmas

📁 Source: Mathlib/Algebra/BigOperators/Group/Finset/Lemmas.lean

Statistics

Metric	Count
Definitions	0
Theorems `coe_finset_sum`, `finset_sum_apply`, `even_sum`, `isSquare_prod`, `mulSupport_prod`, `support_sum`, `coe_finset_prod`, `finset_prod_apply`	8
Total	8

AddMonoidHom

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`coe_finset_sum` 📖	mathematical	—	`DFunLike.coe` `AddMonoidHom` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `instFunLike` `Finset.sum` `instAddCommMonoid` `Pi.addCommMonoid`	—	`map_sum` `instAddMonoidHomClass`
`finset_sum_apply` 📖	mathematical	—	`DFunLike.coe` `AddMonoidHom` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `instFunLike` `Finset.sum` `instAddCommMonoid`	—	`map_sum` `instAddMonoidHomClass`

Finset

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`even_sum` 📖	mathematical	`Even` `AddZero.toAdd` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid`	`sum`	—	`even_iff_exists_two_nsmul` `two_nsmul` `sum_add_distrib` `sum_coe_sort`
`isSquare_prod` 📖	mathematical	`IsSquare` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `CommMonoid.toMonoid`	`prod`	—	`isSquare_iff_exists_sq` `sq` `prod_mul_distrib` `prod_coe_sort`
`mulSupport_prod` 📖	mathematical	—	`Set` `Set.instHasSubset` `Function.mulSupport` `MulOne.toOne` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `CommMonoid.toMonoid` `prod` `Set.iUnion` `Finset` `instMembership`	—	`prod_eq_one`
`support_sum` 📖	mathematical	—	`Set` `Set.instHasSubset` `Function.support` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `sum` `Set.iUnion` `Finset` `instMembership`	—	`Function.support_subset_iff'` `Set.mem_iUnion` `Function.notMem_support` `sum_eq_zero`

MonoidHom

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`coe_finset_prod` 📖	mathematical	—	`DFunLike.coe` `MonoidHom` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `CommMonoid.toMonoid` `instFunLike` `Finset.prod` `instCommMonoid` `Pi.commMonoid`	—	`map_prod` `instMonoidHomClass`
`finset_prod_apply` 📖	mathematical	—	`DFunLike.coe` `MonoidHom` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `CommMonoid.toMonoid` `instFunLike` `Finset.prod` `instCommMonoid`	—	`map_prod` `instMonoidHomClass`

---

← Back to Index