BigOperators

📁 Source: Mathlib/Algebra/Group/Pointwise/Set/BigOperators.lean

Statistics

Metric	Count
Definitions	0
Theorems finset_prod_mem_finset_prod, finset_prod_singleton, finset_prod_subset_finset_prod, finset_sum_mem_finset_sum, finset_sum_singleton, finset_sum_subset_finset_sum, image_finset_prod, image_finset_prod_pi, image_finset_sum, image_finset_sum_pi, image_fintype_prod_pi, image_fintype_sum_pi, image_list_prod, image_list_sum, image_multiset_prod, image_multiset_sum, list_prod_mem_list_prod, list_prod_singleton, list_prod_subset_list_prod, list_sum_mem_list_sum, list_sum_singleton, list_sum_subset_list_sum, mem_finset_prod, mem_finset_sum, mem_fintype_prod, mem_fintype_sum, mem_nsmul_iff_sum, mem_pow_iff_prod, multiset_prod_mem_multiset_prod, multiset_prod_singleton, multiset_prod_subset_multiset_prod, multiset_sum_mem_multiset_sum, multiset_sum_singleton, multiset_sum_subset_multiset_sum	34
Total	34

Set

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
finset_prod_mem_finset_prod 📖	mathematical	Set instMembership	Finset.prod commMonoid	—	multiset_prod_mem_multiset_prod
finset_prod_singleton 📖	mathematical	—	Finset.prod Set commMonoid instSingletonSet	—	map_prod MonoidHom.instMonoidHomClass
finset_prod_subset_finset_prod 📖	mathematical	Set instHasSubset	Finset.prod commMonoid	—	multiset_prod_subset_multiset_prod
finset_sum_mem_finset_sum 📖	mathematical	Set instMembership	Finset.sum addCommMonoid	—	multiset_sum_mem_multiset_sum
finset_sum_singleton 📖	mathematical	—	Finset.sum Set addCommMonoid instSingletonSet	—	map_sum AddMonoidHom.instAddMonoidHomClass
finset_sum_subset_finset_sum 📖	mathematical	Set instHasSubset	Finset.sum addCommMonoid	—	multiset_sum_subset_multiset_sum
image_finset_prod 📖	mathematical	—	image DFunLike.coe Finset.prod Set commMonoid	—	image_multiset_prod Multiset.map_map
image_finset_prod_pi 📖	mathematical	—	image Finset.prod pi SetLike.coe Finset Finset.instSetLike Set commMonoid	—	ext
image_finset_sum 📖	mathematical	—	image DFunLike.coe Finset.sum Set addCommMonoid	—	image_multiset_sum Multiset.map_map
image_finset_sum_pi 📖	mathematical	—	image Finset.sum pi SetLike.coe Finset Finset.instSetLike Set addCommMonoid	—	ext mem_finset_sum mem_image mem_pi Finset.mem_coe
image_fintype_prod_pi 📖	mathematical	—	image Finset.prod Finset.univ pi univ Set commMonoid	—	Finset.coe_univ image_finset_prod_pi
image_fintype_sum_pi 📖	mathematical	—	image Finset.sum Finset.univ pi univ Set addCommMonoid	—	Finset.coe_univ image_finset_sum_pi
image_list_prod 📖	mathematical	—	image DFunLike.coe Set mul MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass one MulOne.toOne	—	image_one map_one MonoidHomClass.toOneHomClass image_mul MonoidHomClass.toMulHomClass
image_list_sum 📖	mathematical	—	image DFunLike.coe Set add AddZero.toAdd AddZeroClass.toAddZero AddMonoid.toAddZeroClass zero AddZero.toZero	—	image_zero map_zero AddMonoidHomClass.toZeroHomClass image_add AddMonoidHomClass.toAddHomClass
image_multiset_prod 📖	mathematical	—	image DFunLike.coe Multiset.prod Set commMonoid Multiset.map	—	image_list_prod
image_multiset_sum 📖	mathematical	—	image DFunLike.coe Multiset.sum Set addCommMonoid Multiset.map	—	image_list_sum
list_prod_mem_list_prod 📖	mathematical	Set instMembership	mul MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass CommMonoid.toMonoid one MulOne.toOne	—	mul_mem_mul
list_prod_singleton 📖	mathematical	—	Set mul MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass one MulOne.toOne instSingletonSet	—	map_list_prod MonoidHom.instMonoidHomClass
list_prod_subset_list_prod 📖	mathematical	Set instHasSubset	mul MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass CommMonoid.toMonoid one MulOne.toOne	—	subset_refl instReflSubset mul_subset_mul
list_sum_mem_list_sum 📖	mathematical	Set instMembership	add AddZero.toAdd AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid zero AddZero.toZero	—	mem_zero add_mem_add
list_sum_singleton 📖	mathematical	—	Set add AddZero.toAdd AddZeroClass.toAddZero AddMonoid.toAddZeroClass zero AddZero.toZero instSingletonSet	—	map_list_sum AddMonoidHom.instAddMonoidHomClass
list_sum_subset_list_sum 📖	mathematical	Set instHasSubset	add AddZero.toAdd AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid zero AddZero.toZero	—	subset_refl instReflSubset add_subset_add
mem_finset_prod 📖	mathematical	—	Set instMembership Finset.prod commMonoid	—	Finset.induction_on Finset.notMem_empty Finset.prod_insert mem_mul Finset.mem_insert Function.update_self Function.update_of_ne Finset.prod_update_of_notMem Finset.mem_insert_self Finset.mem_insert_of_mem
mem_finset_sum 📖	mathematical	—	Set instMembership Finset.sum addCommMonoid	—	Finset.induction_on mem_zero Finset.notMem_empty Finset.sum_insert mem_add Finset.mem_insert Function.update_self Function.update_of_ne Finset.sum_update_of_notMem Finset.mem_insert_self Finset.mem_insert_of_mem
mem_fintype_prod 📖	mathematical	—	Set instMembership Finset.prod commMonoid Finset.univ	—	mem_finset_prod
mem_fintype_sum 📖	mathematical	—	Set instMembership Finset.sum addCommMonoid Finset.univ	—	mem_finset_sum Finset.mem_univ
mem_nsmul_iff_sum 📖	mathematical	—	Set instMembership NSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid AddZero.toAdd Finset.sum Finset.univ Fin.fintype	—	Finset.sum_const Fintype.card_fin Finset.mem_univ mem_finset_sum
mem_pow_iff_prod 📖	mathematical	—	Set instMembership NPow MulOne.toOne MulOneClass.toMulOne Monoid.toMulOneClass CommMonoid.toMonoid MulOne.toMul Finset.prod Finset.univ Fin.fintype	—	Finset.prod_const Fintype.card_fin mem_finset_prod
multiset_prod_mem_multiset_prod 📖	mathematical	Set instMembership	Multiset.prod commMonoid Multiset.map	—	list_prod_mem_list_prod
multiset_prod_singleton 📖	mathematical	—	Multiset.prod Set commMonoid Multiset.map instSingletonSet	—	map_multiset_prod MonoidHom.instMonoidHomClass
multiset_prod_subset_multiset_prod 📖	mathematical	Set instHasSubset	Multiset.prod commMonoid Multiset.map	—	list_prod_subset_list_prod
multiset_sum_mem_multiset_sum 📖	mathematical	Set instMembership	Multiset.sum addCommMonoid Multiset.map	—	list_sum_mem_list_sum
multiset_sum_singleton 📖	mathematical	—	Multiset.sum Set addCommMonoid Multiset.map instSingletonSet	—	map_multiset_sum AddMonoidHom.instAddMonoidHomClass
multiset_sum_subset_multiset_sum 📖	mathematical	Set instHasSubset	Multiset.sum addCommMonoid Multiset.map	—	list_sum_subset_list_sum

---

← Back to Index