Documentation Verification Report

BigOperators

📁 Source: Mathlib/Algebra/Group/Submonoid/BigOperators.lean

Statistics

Metric	Count
Definitions	0
Theorems `coe_finset_sum`, `coe_list_sum`, `coe_multiset_sum`, `list_sum_mem`, `mem_closure_finset`, `mem_closure_iff_exists_finset_subset`, `multiset_noncommSum_mem`, `multiset_sum_mem`, `noncommSum_mem`, `sum_mem`, `coe_finset_sum`, `coe_list_sum`, `coe_multiset_sum`, `coe_finset_prod`, `coe_list_prod`, `coe_multiset_prod`, `list_prod_mem`, `mem_closure_finset`, `mem_closure_iff_exists_finset_subset`, `multiset_noncommProd_mem`, `multiset_prod_mem`, `noncommProd_mem`, `prod_mem`, `coe_finset_prod`, `coe_list_prod`, `coe_multiset_prod`, `list_prod_mem`, `list_sum_mem`, `multiset_prod_mem`, `multiset_sum_mem`, `prod_mem`, `sum_mem`	32
Total	32

AddSubmonoid

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`coe_finset_sum` 📖	mathematical	—	`AddSubmonoid` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `SetLike.instMembership` `instSetLike` `Finset.sum` `toAddCommMonoid`	—	`map_sum` `AddMonoidHom.instAddMonoidHomClass`
`coe_list_sum` 📖	mathematical	—	`AddSubmonoid` `AddMonoid.toAddZeroClass` `SetLike.instMembership` `instSetLike` `add` `zero` `AddZero.toAdd` `AddZeroClass.toAddZero` `AddZero.toZero`	—	`map_list_sum` `AddMonoidHom.instAddMonoidHomClass`
`coe_multiset_sum` 📖	mathematical	—	`AddSubmonoid` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `SetLike.instMembership` `instSetLike` `Multiset.sum` `toAddCommMonoid` `Multiset.map`	—	`AddMonoidHom.map_multiset_sum`
`list_sum_mem` 📖	mathematical	`AddSubmonoid` `AddMonoid.toAddZeroClass` `SetLike.instMembership` `instSetLike`	`AddZero.toAdd` `AddZeroClass.toAddZero` `AddZero.toZero`	—	`list_sum_mem` `instAddSubmonoidClass`
`mem_closure_finset` 📖	mathematical	—	`AddSubmonoid` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `SetLike.instMembership` `instSetLike` `closure` `SetLike.coe` `Finset` `Finset.instSetLike` `Set` `Set.instHasSubset` `Function.support` `AddZero.toZero` `AddZeroClass.toAddZero` `Nat.instAddMonoid` `Finset.sum` `AddMonoid.toNatSMul`	—	`mem_closure_iff_exists_finset_subset` `HasSubset.Subset.trans` `Set.instIsTransSubset` `Finset.sum_subset` `Function.support_subset_iff'` `SetLike.mem_coe` `zero_nsmul` `sum_mem` `nsmul_mem` `instAddSubmonoidClass` `subset_closure`
`mem_closure_iff_exists_finset_subset` 📖	mathematical	—	`AddSubmonoid` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `SetLike.instMembership` `instSetLike` `closure` `Set` `Set.instHasSubset` `SetLike.coe` `Finset` `Finset.instSetLike` `Function.support` `AddZero.toZero` `AddZeroClass.toAddZero` `Nat.instAddMonoid` `Finset.sum` `AddMonoid.toNatSMul`	—	`closure_induction` `Finset.coe_singleton` `Set.singleton_subset_iff` `Pi.support_single_of_ne` `one_ne_zero` `subset_refl` `Set.instReflSubset` `Finset.sum_congr` `Pi.single_apply` `ite_smul` `one_nsmul` `zero_nsmul` `Finset.sum_singleton` `Finset.coe_empty` `Set.empty_subset` `Function.support_zero` `Finset.sum_const_zero` `Finset.coe_union` `Set.union_subset` `HasSubset.Subset.trans` `Set.instIsTransSubset` `Function.support_add` `Set.union_subset_union` `add_nsmul` `Finset.sum_add_distrib` `Finset.sum_subset` `Finset.subset_union_left` `Finset.mem_union` `Function.support_subset_iff'` `SetLike.mem_coe` `Finset.subset_union_right` `sum_mem` `nsmul_mem` `instAddSubmonoidClass` `subset_closure`
`multiset_noncommSum_mem` 📖	mathematical	`Set.Pairwise` `setOf` `Multiset` `Multiset.instMembership` `AddCommute` `AddZero.toAdd` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddSubmonoid` `SetLike.instMembership` `instSetLike`	`Multiset.noncommSum`	—	`Multiset.noncommSum_coe` `list_sum_mem`
`multiset_sum_mem` 📖	mathematical	`AddSubmonoid` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `SetLike.instMembership` `instSetLike`	`Multiset.sum`	—	`multiset_sum_mem` `instAddSubmonoidClass`
`noncommSum_mem` 📖	mathematical	`Set.Pairwise` `SetLike.coe` `Finset` `Finset.instSetLike` `Function.onFun` `AddCommute` `AddZero.toAdd` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddSubmonoid` `SetLike.instMembership` `instSetLike`	`Finset.noncommSum`	—	`multiset_noncommSum_mem` `Finset.noncommSum_lemma` `Multiset.mem_map`
`sum_mem` 📖	mathematical	`AddSubmonoid` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `SetLike.instMembership` `instSetLike`	`Finset.sum`	—	`multiset_sum_mem` `Multiset.mem_map`

AddSubmonoidClass

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`coe_finset_sum` 📖	mathematical	—	`SetLike.instMembership` `Finset.sum` `toAddCommMonoid`	—	`map_sum` `AddMonoidHom.instAddMonoidHomClass`
`coe_list_sum` 📖	mathematical	—	`SetLike.instMembership` `AddZero.toAdd` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `toAddMonoid` `ZeroMemClass.zero` `AddZero.toZero` `toZeroMemClass`	—	`map_list_sum` `AddMonoidHom.instAddMonoidHomClass`
`coe_multiset_sum` 📖	mathematical	—	`SetLike.instMembership` `Multiset.sum` `toAddCommMonoid` `Multiset.map`	—	`AddMonoidHom.map_multiset_sum`

Submonoid

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`coe_finset_prod` 📖	mathematical	—	`Submonoid` `Monoid.toMulOneClass` `CommMonoid.toMonoid` `SetLike.instMembership` `instSetLike` `Finset.prod` `toCommMonoid`	—	`map_prod` `MonoidHom.instMonoidHomClass`
`coe_list_prod` 📖	mathematical	—	`Submonoid` `Monoid.toMulOneClass` `SetLike.instMembership` `instSetLike` `mul` `one` `MulOne.toMul` `MulOneClass.toMulOne` `MulOne.toOne`	—	`map_list_prod` `MonoidHom.instMonoidHomClass`
`coe_multiset_prod` 📖	mathematical	—	`Submonoid` `Monoid.toMulOneClass` `CommMonoid.toMonoid` `SetLike.instMembership` `instSetLike` `Multiset.prod` `toCommMonoid` `Multiset.map`	—	`MonoidHom.map_multiset_prod`
`list_prod_mem` 📖	mathematical	`Submonoid` `Monoid.toMulOneClass` `SetLike.instMembership` `instSetLike`	`MulOne.toMul` `MulOneClass.toMulOne` `MulOne.toOne`	—	`list_prod_mem` `instSubmonoidClass`
`mem_closure_finset` 📖	mathematical	—	`Submonoid` `Monoid.toMulOneClass` `CommMonoid.toMonoid` `SetLike.instMembership` `instSetLike` `closure` `SetLike.coe` `Finset` `Finset.instSetLike` `Set` `Set.instHasSubset` `Function.support` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `Nat.instAddMonoid` `Finset.prod` `Monoid.toNatPow`	—	`mem_closure_iff_exists_finset_subset` `HasSubset.Subset.trans` `Set.instIsTransSubset` `Finset.prod_subset` `Function.support_subset_iff'` `pow_zero` `prod_mem` `pow_mem` `instSubmonoidClass` `subset_closure`
`mem_closure_iff_exists_finset_subset` 📖	mathematical	—	`Submonoid` `Monoid.toMulOneClass` `CommMonoid.toMonoid` `SetLike.instMembership` `instSetLike` `closure` `Set` `Set.instHasSubset` `SetLike.coe` `Finset` `Finset.instSetLike` `Function.support` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `Nat.instAddMonoid` `Finset.prod` `Monoid.toNatPow`	—	`closure_induction` `Finset.coe_singleton` `Pi.support_single_of_ne` `Set.instReflSubset` `Finset.prod_congr` `Pi.single_apply` `pow_ite` `pow_one` `pow_zero` `Finset.prod_singleton` `Finset.coe_empty` `Function.support_zero` `Finset.prod_const_one` `Set.union_subset` `HasSubset.Subset.trans` `Set.instIsTransSubset` `Function.support_add` `Set.union_subset_union` `pow_add` `Finset.prod_mul_distrib` `Finset.prod_subset` `Finset.subset_union_left` `Function.support_subset_iff'` `Finset.subset_union_right` `prod_mem` `pow_mem` `instSubmonoidClass` `subset_closure`
`multiset_noncommProd_mem` 📖	mathematical	`Set.Pairwise` `setOf` `Multiset` `Multiset.instMembership` `Commute` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `Submonoid` `SetLike.instMembership` `instSetLike`	`Multiset.noncommProd`	—	`Multiset.noncommProd_coe` `list_prod_mem`
`multiset_prod_mem` 📖	mathematical	`Submonoid` `Monoid.toMulOneClass` `CommMonoid.toMonoid` `SetLike.instMembership` `instSetLike`	`Multiset.prod`	—	`multiset_prod_mem` `instSubmonoidClass`
`noncommProd_mem` 📖	mathematical	`Set.Pairwise` `SetLike.coe` `Finset` `Finset.instSetLike` `Function.onFun` `Commute` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `Submonoid` `SetLike.instMembership` `instSetLike`	`Finset.noncommProd`	—	`multiset_noncommProd_mem` `Finset.noncommProd_lemma` `Multiset.mem_map`
`prod_mem` 📖	mathematical	`Submonoid` `Monoid.toMulOneClass` `CommMonoid.toMonoid` `SetLike.instMembership` `instSetLike`	`Finset.prod`	—	`multiset_prod_mem` `Multiset.mem_map`

SubmonoidClass

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`coe_finset_prod` 📖	mathematical	—	`SetLike.instMembership` `Finset.prod` `toCommMonoid`	—	`map_prod` `MonoidHom.instMonoidHomClass`
`coe_list_prod` 📖	mathematical	—	`SetLike.instMembership` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `toMonoid` `OneMemClass.one` `MulOne.toOne` `toOneMemClass`	—	`map_list_prod` `MonoidHom.instMonoidHomClass`
`coe_multiset_prod` 📖	mathematical	—	`SetLike.instMembership` `Multiset.prod` `toCommMonoid` `Multiset.map`	—	`MonoidHom.map_multiset_prod`

(root)

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`list_prod_mem` 📖	mathematical	`SetLike.instMembership`	`MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `MulOne.toOne`	—	`CanLift.prf` `List.canLift` `Subtype.canLift` `SubmonoidClass.toOneMemClass` `SubmonoidClass.coe_list_prod` `Subtype.coe_prop`
`list_sum_mem` 📖	mathematical	`SetLike.instMembership`	`AddZero.toAdd` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddZero.toZero`	—	`CanLift.prf` `List.canLift` `Subtype.canLift` `AddSubmonoidClass.toZeroMemClass` `AddSubmonoidClass.coe_list_sum` `Subtype.coe_prop`
`multiset_prod_mem` 📖	mathematical	`SetLike.instMembership`	`Multiset.prod`	—	`CanLift.prf` `Multiset.canLift` `Subtype.canLift` `SubmonoidClass.coe_multiset_prod` `Subtype.coe_prop`
`multiset_sum_mem` 📖	mathematical	`SetLike.instMembership`	`Multiset.sum`	—	`CanLift.prf` `Multiset.canLift` `Subtype.canLift` `AddSubmonoidClass.coe_multiset_sum` `Subtype.coe_prop`
`prod_mem` 📖	mathematical	`SetLike.instMembership`	`Finset.prod`	—	`multiset_prod_mem` `Multiset.mem_map`
`sum_mem` 📖	mathematical	`SetLike.instMembership`	`Finset.sum`	—	`multiset_sum_mem` `Multiset.mem_map`

---

← Back to Index