BigOperators

Statistics

Metric	Count
Definitions	0
Theorems `isSelfAdjoint_sum`, `star_finsuppProd`, `star_finsuppSum`, `star_prod`, `star_sum`	5
Total	5

Name	Kind	Assumes	Proves	Validates	Depends On
`isSelfAdjoint_sum` 📖	mathematical	`IsSelfAdjoint` `InvolutiveStar.toStar` `StarAddMonoid.toInvolutiveStar` `AddCommMonoid.toAddMonoid`	`Finset.sum`	—	`star_sum` `Finset.sum_congr`
`star_finsuppProd` 📖	mathematical	—	`Star.star` `InvolutiveStar.toStar` `StarMul.toInvolutiveStar` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `CommMonoid.toMonoid` `Finsupp.prod` `Pi.instStarForall`	—	`star_prod` `Finset.prod_congr`
`star_finsuppSum` 📖	mathematical	—	`Star.star` `InvolutiveStar.toStar` `StarAddMonoid.toInvolutiveStar` `AddCommMonoid.toAddMonoid` `Finsupp.sum` `Pi.instStarForall`	—	`star_sum` `Finset.sum_congr`
`star_prod` 📖	mathematical	—	`Star.star` `InvolutiveStar.toStar` `StarMul.toInvolutiveStar` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `CommMonoid.toMonoid` `Finset.prod`	—	`map_prod` `MulEquivClass.instMonoidHomClass` `MulEquiv.instMulEquivClass`
`star_sum` 📖	mathematical	—	`Star.star` `InvolutiveStar.toStar` `StarAddMonoid.toInvolutiveStar` `AddCommMonoid.toAddMonoid` `Finset.sum`	—	`map_sum` `AddEquivClass.instAddMonoidHomClass` `AddEquiv.instAddEquivClass`

---