mathlib3
b401f074 - feat(src/group_theory/subgroup): add closure.submonoid.closure (#7328)

Commit
5 years ago
feat(src/group_theory/subgroup): add closure.submonoid.closure (#7328) `subgroup.closure S` equals `submonoid.closure (S ∪ S⁻¹)`.
Parents
Loading