Theorem Set.subgroupClosure_mul_pow

Modification history

2024-11-28 16:50
Mathlib/Algebra/Group/Subgroup/Pointwise.lean
feat: `S ^ n = S` where `S` is a submonoid (#19259) …
Added Set.subgroupClosure_mul_powView on Github →