Finsupp

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

Statistics

Metric	Count
Definitions	0
Theorems exists_finsupp_of_mem_closure_range, exists_of_mem_closure_range, 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_iff_of_fintype, mem_closure_range_iff, mem_closure_range_iff_of_fintype	10
Total	10

AddSubgroup

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
exists_finsupp_of_mem_closure_range 📖	mathematical	AddSubgroup AddCommGroup.toAddGroup SetLike.instMembership instSetLike closure Set.range	Finsupp.sum MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Int.instCommRing AddCommGroup.toAddCommMonoid SubNegMonoid.toZSMul AddGroup.toSubNegMonoid	—	closure_induction Finsupp.sum_single_index zero_zsmul one_zsmul Finsupp.sum_add_index Finset.mem_union Finsupp.mem_support_iff add_zsmul Finsupp.sum_neg_index neg_zsmul Finsupp.sum_neg
exists_of_mem_closure_range 📖	mathematical	AddSubgroup AddCommGroup.toAddGroup SetLike.instMembership instSetLike closure Set.range	Finset.sum AddCommGroup.toAddCommMonoid Finset.univ SubNegMonoid.toZSMul AddGroup.toSubNegMonoid	—	exists_finsupp_of_mem_closure_range Finsupp.sum_zsmul
mem_closure_iff_of_fintype 📖	mathematical	—	AddSubgroup AddCommGroup.toAddGroup SetLike.instMembership instSetLike closure Finset.sum Set.Elem AddCommGroup.toAddCommMonoid Finset.univ SubNegMonoid.toZSMul AddGroup.toSubNegMonoid Set Set.instMembership	—	Subtype.range_coe mem_closure_range_iff_of_fintype
mem_closure_range_iff 📖	mathematical	—	AddSubgroup AddCommGroup.toAddGroup SetLike.instMembership instSetLike closure Set.range Finsupp.sum MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Int.instCommRing AddCommGroup.toAddCommMonoid SubNegMonoid.toZSMul AddGroup.toSubNegMonoid	—	exists_finsupp_of_mem_closure_range AddSubmonoid.sum_mem zsmul_mem instAddSubgroupClass subset_closure Set.mem_range_self
mem_closure_range_iff_of_fintype 📖	mathematical	—	AddSubgroup AddCommGroup.toAddGroup SetLike.instMembership instSetLike closure Set.range Finset.sum AddCommGroup.toAddCommMonoid Finset.univ SubNegMonoid.toZSMul AddGroup.toSubNegMonoid	—	Finite.of_fintype Equiv.exists_congr_left mem_closure_range_iff Finsupp.sum_zsmul Finset.sum_congr

Subgroup

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
exists_finsupp_of_mem_closure_range 📖	mathematical	Subgroup CommGroup.toGroup SetLike.instMembership instSetLike closure Set.range	Finsupp.prod MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Int.instCommRing CommGroup.toCommMonoid DivInvMonoid.toZPow Group.toDivInvMonoid	—	closure_induction Finsupp.prod_single_index zpow_zero zpow_one Finsupp.prod_add_index zpow_add Finsupp.prod_neg_index zpow_neg Finsupp.prod_inv
exists_of_mem_closure_range 📖	mathematical	Subgroup CommGroup.toGroup SetLike.instMembership instSetLike closure Set.range	Finset.prod CommGroup.toCommMonoid Finset.univ DivInvMonoid.toZPow Group.toDivInvMonoid	—	exists_finsupp_of_mem_closure_range Finsupp.prod_zpow
mem_closure_iff_of_fintype 📖	mathematical	—	Subgroup CommGroup.toGroup SetLike.instMembership instSetLike closure Finset.prod Set.Elem CommGroup.toCommMonoid Finset.univ DivInvMonoid.toZPow Group.toDivInvMonoid Set Set.instMembership	—	Subtype.range_coe mem_closure_range_iff_of_fintype
mem_closure_range_iff 📖	mathematical	—	Subgroup CommGroup.toGroup SetLike.instMembership instSetLike closure Set.range Finsupp.prod MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Int.instCommRing CommGroup.toCommMonoid DivInvMonoid.toZPow Group.toDivInvMonoid	—	exists_finsupp_of_mem_closure_range Submonoid.prod_mem zpow_mem instSubgroupClass subset_closure Set.mem_range_self
mem_closure_range_iff_of_fintype 📖	mathematical	—	Subgroup CommGroup.toGroup SetLike.instMembership instSetLike closure Set.range Finset.prod CommGroup.toCommMonoid Finset.univ DivInvMonoid.toZPow Group.toDivInvMonoid	—	Finite.of_fintype Equiv.exists_congr_left mem_closure_range_iff Finsupp.prod_zpow Finset.prod_congr

---

← Back to Index