Commit 2024-12-28 14:09 0c419e32

View on Github →

feat: add Submonoid.mem_closure_range_iff (#19495)

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Algebra/BigOperators/Finsupp.lean

added theorem Finsupp.prod_zpow

Created Mathlib/Algebra/Group/Subgroup/Finsupp.lean

added theorem Subgroup.exists_finsupp_of_mem_closure_range

added theorem Subgroup.exists_of_mem_closure_range

added theorem Subgroup.mem_closure_range_iff

added theorem Subgroup.mem_closure_range_iff_of_fintype

Created Mathlib/Algebra/Group/Submonoid/Finsupp.lean

added theorem Submonoid.exists_finsupp_of_mem_closure_range

added theorem Submonoid.exists_of_mem_closure_range

added theorem Submonoid.mem_closure_range_iff

added theorem Submonoid.mem_closure_range_iff_of_fintype

Modified Mathlib/Data/Finsupp/Multiset.lean