Theorem Set.mul_subgroupClosure

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.mul_subgroupClosureView on Github →