Commit 2024-11-28 16:50 adcc9a19

View on Github →

feat: S ^ n = S where S is a submonoid (#19259) From GrowthInGroups

Estimated changes

Modified Mathlib/Algebra/Group/Subgroup/Pointwise.lean

added theorem Set.mul_subgroupClosure

added theorem Set.pow_mul_subgroupClosure

added theorem Set.subgroupClosure_mul

added theorem Set.subgroupClosure_mul_pow

deleted theorem coe_mul_coe

Modified Mathlib/Algebra/Group/Submonoid/Pointwise.lean

added theorem coe_mul_coe

added theorem coe_set_pow