Mathlib Changelog
v4
Changelog
About
Github
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