Sigma

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

Statistics

Metric	Count
Definitions	0
Theorems `card_sigma`, `prod_comm`, `prod_comm'`, `prod_comm_cycle`, `prod_finset_product`, `prod_finset_product'`, `prod_finset_product_right`, `prod_finset_product_right'`, `prod_product`, `prod_product'`, `prod_product_right`, `prod_product_right'`, `prod_sigma`, `prod_sigma'`, `sum_comm`, `sum_comm'`, `sum_comm_cycle`, `sum_finset_product`, `sum_finset_product'`, `sum_finset_product_right`, `sum_finset_product_right'`, `sum_product`, `sum_product'`, `sum_product_right`, `sum_product_right'`, `sum_sigma`, `sum_sigma'`	27
Total	27

Finset

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`card_sigma` 📖	mathematical	—	`card` `sigma` `sum` `Nat.instAddCommMonoid`	—	`Multiset.card_sigma`
`prod_comm` 📖	mathematical	—	`prod`	—	`prod_comm'`
`prod_comm'` 📖	mathematical	`Finset` `instMembership`	`prod`	—	`prod_finset_product'` `prod_finset_product_right'`
`prod_comm_cycle` 📖	mathematical	—	`prod`	—	`prod_congr` `prod_comm`
`prod_finset_product` 📖	mathematical	`Finset` `instMembership`	`prod`	—	`prod_equiv` `prod_sigma`
`prod_finset_product'` 📖	mathematical	`Finset` `instMembership`	`prod`	—	`prod_finset_product`
`prod_finset_product_right` 📖	mathematical	`Finset` `instMembership`	`prod`	—	`prod_equiv` `prod_sigma`
`prod_finset_product_right'` 📖	mathematical	`Finset` `instMembership`	`prod`	—	`prod_finset_product_right`
`prod_product` 📖	mathematical	—	`prod` `SProd.sprod` `Finset` `instSProd`	—	`prod_finset_product` `mem_product`
`prod_product'` 📖	mathematical	—	`prod` `SProd.sprod` `Finset` `instSProd`	—	`prod_product`
`prod_product_right` 📖	mathematical	—	`prod` `SProd.sprod` `Finset` `instSProd`	—	`prod_finset_product_right` `mem_product`
`prod_product_right'` 📖	mathematical	—	`prod` `SProd.sprod` `Finset` `instSProd`	—	`prod_product_right`
`prod_sigma` 📖	mathematical	—	`prod` `sigma`	—	`pairwiseDisjoint_map_sigmaMk` `prod_disjiUnion` `prod_congr` `prod_map`
`prod_sigma'` 📖	mathematical	—	`prod` `sigma`	—	`prod_sigma`
`sum_comm` 📖	mathematical	—	`sum`	—	`sum_comm'`
`sum_comm'` 📖	mathematical	`Finset` `instMembership`	`sum`	—	`mem_biUnion` `mem_map` `sum_finset_product'` `sum_finset_product_right'`
`sum_comm_cycle` 📖	mathematical	—	`sum`	—	`sum_congr` `sum_comm`
`sum_finset_product` 📖	mathematical	`Finset` `instMembership`	`sum`	—	`sum_equiv` `mem_sigma` `sum_sigma`
`sum_finset_product'` 📖	mathematical	`Finset` `instMembership`	`sum`	—	`sum_finset_product`
`sum_finset_product_right` 📖	mathematical	`Finset` `instMembership`	`sum`	—	`sum_equiv` `mem_sigma` `sum_sigma`
`sum_finset_product_right'` 📖	mathematical	`Finset` `instMembership`	`sum`	—	`sum_finset_product_right`
`sum_product` 📖	mathematical	—	`sum` `SProd.sprod` `Finset` `instSProd`	—	`sum_finset_product` `mem_product`
`sum_product'` 📖	mathematical	—	`sum` `SProd.sprod` `Finset` `instSProd`	—	`sum_product`
`sum_product_right` 📖	mathematical	—	`sum` `SProd.sprod` `Finset` `instSProd`	—	`sum_finset_product_right` `mem_product`
`sum_product_right'` 📖	mathematical	—	`sum` `SProd.sprod` `Finset` `instSProd`	—	`sum_product_right`
`sum_sigma` 📖	mathematical	—	`sum` `sigma`	—	`pairwiseDisjoint_map_sigmaMk` `sum_disjiUnion` `sum_congr` `sum_map`
`sum_sigma'` 📖	mathematical	—	`sum` `sigma`	—	`sum_sigma`

---

← Back to Index