BigOperators

Statistics

Metric	Count
Definitions	0
Theorems `coe_prod`, `coe_sum`, `prod_inv_index`, `prod_neg_index`, `sum_inv_index`, `sum_neg_index`	6
Total	6

Name	Kind	Assumes	Proves	Validates	Depends On
`coe_prod` 📖	mathematical	—	`SetLike.coe` `Finset` `instSetLike` `prod` `commMonoid` `Set` `Set.commMonoid`	—	`map_prod` `MonoidHom.instMonoidHomClass`
`coe_sum` 📖	mathematical	—	`SetLike.coe` `Finset` `instSetLike` `sum` `addCommMonoid` `Set` `Set.addCommMonoid`	—	`map_sum` `AddMonoidHom.instAddMonoidHomClass`
`prod_inv_index` 📖	mathematical	—	`prod` `Finset` `inv` `InvolutiveInv.toInv`	—	`prod_image` `Function.Injective.injOn` `inv_injective`
`prod_neg_index` 📖	mathematical	—	`prod` `Finset` `neg` `InvolutiveNeg.toNeg`	—	`prod_image` `Function.Injective.injOn` `neg_injective`
`sum_inv_index` 📖	mathematical	—	`sum` `Finset` `inv` `InvolutiveInv.toInv`	—	`sum_image` `Function.Injective.injOn` `inv_injective`
`sum_neg_index` 📖	mathematical	—	`sum` `Finset` `neg` `InvolutiveNeg.toNeg`	—	`sum_image` `Function.Injective.injOn` `neg_injective`

---