Finsupp

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

Statistics

Metric	Count
Definitions	0
Theorems exists_finsupp_of_mem_closure_range, exists_of_mem_closure_range, mem_closure_finset', mem_closure_iff_of_fintype, mem_closure_range_iff, mem_closure_range_iff_of_fintype, exists_finsupp_of_mem_closure_range, exists_of_mem_closure_range, mem_closure_finset', mem_closure_iff_of_fintype, mem_closure_range_iff, mem_closure_range_iff_of_fintype	12
Total	12

AddSubmonoid

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
exists_finsupp_of_mem_closure_range 📖	mathematical	AddSubmonoid AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid SetLike.instMembership instSetLike closure Set.range	Finsupp.sum MulZeroClass.toZero Nat.instMulZeroClass AddMonoid.toNatSMul	—	closure_induction Finsupp.sum_single_index zero_nsmul one_nsmul Finsupp.sum_add_index Finset.mem_union Finsupp.mem_support_iff add_nsmul
exists_of_mem_closure_range 📖	mathematical	AddSubmonoid AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid SetLike.instMembership instSetLike closure Set.range	Finset.sum Finset.univ AddMonoid.toNatSMul	—	exists_finsupp_of_mem_closure_range Finsupp.sum_nsmul
mem_closure_finset' 📖	mathematical	—	AddSubmonoid AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid SetLike.instMembership instSetLike closure SetLike.coe Finset Finset.instSetLike Finset.sum Finset.univ Finset.Subtype.fintype AddMonoid.toNatSMul	—	mem_closure_iff_of_fintype
mem_closure_iff_of_fintype 📖	mathematical	—	AddSubmonoid AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid SetLike.instMembership instSetLike closure Finset.sum Set.Elem Finset.univ AddMonoid.toNatSMul Set Set.instMembership	—	Subtype.range_coe mem_closure_range_iff_of_fintype
mem_closure_range_iff 📖	mathematical	—	AddSubmonoid AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid SetLike.instMembership instSetLike closure Set.range Finsupp.sum MulZeroClass.toZero Nat.instMulZeroClass AddMonoid.toNatSMul	—	exists_finsupp_of_mem_closure_range sum_mem nsmul_mem instAddSubmonoidClass subset_closure Set.mem_range_self
mem_closure_range_iff_of_fintype 📖	mathematical	—	AddSubmonoid AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid SetLike.instMembership instSetLike closure Set.range Finset.sum Finset.univ AddMonoid.toNatSMul	—	Finite.of_fintype Equiv.exists_congr_left mem_closure_range_iff Finsupp.sum_nsmul Finset.sum_congr

Submonoid

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
exists_finsupp_of_mem_closure_range 📖	mathematical	Submonoid Monoid.toMulOneClass CommMonoid.toMonoid SetLike.instMembership instSetLike closure Set.range	Finsupp.prod MulZeroClass.toZero Nat.instMulZeroClass Monoid.toNatPow	—	closure_induction Finsupp.prod_single_index pow_zero pow_one Finsupp.prod_add_index pow_add
exists_of_mem_closure_range 📖	mathematical	Submonoid Monoid.toMulOneClass CommMonoid.toMonoid SetLike.instMembership instSetLike closure Set.range	Finset.prod Finset.univ Monoid.toNatPow	—	exists_finsupp_of_mem_closure_range Finsupp.prod_pow
mem_closure_finset' 📖	mathematical	—	Submonoid Monoid.toMulOneClass CommMonoid.toMonoid SetLike.instMembership instSetLike closure SetLike.coe Finset Finset.instSetLike Finset.prod Finset.univ Finset.Subtype.fintype Monoid.toNatPow	—	mem_closure_iff_of_fintype
mem_closure_iff_of_fintype 📖	mathematical	—	Submonoid Monoid.toMulOneClass CommMonoid.toMonoid SetLike.instMembership instSetLike closure Finset.prod Set.Elem Finset.univ Monoid.toNatPow Set Set.instMembership	—	Subtype.range_coe mem_closure_range_iff_of_fintype
mem_closure_range_iff 📖	mathematical	—	Submonoid Monoid.toMulOneClass CommMonoid.toMonoid SetLike.instMembership instSetLike closure Set.range Finsupp.prod MulZeroClass.toZero Nat.instMulZeroClass Monoid.toNatPow	—	exists_finsupp_of_mem_closure_range prod_mem pow_mem instSubmonoidClass subset_closure Set.mem_range_self
mem_closure_range_iff_of_fintype 📖	mathematical	—	Submonoid Monoid.toMulOneClass CommMonoid.toMonoid SetLike.instMembership instSetLike closure Set.range Finset.prod Finset.univ Monoid.toNatPow	—	Finite.of_fintype Equiv.exists_congr_left mem_closure_range_iff Finsupp.prod_pow Finset.prod_congr

---

← Back to Index