feat(group_theory/submonoid): add closure_singleton (#810)
feat(group_theory/submonoid): add closure_singleton (#810)

* feat(group_theory/submonoid): add closure_singleton

* adding some to_additive

leanprover-community/mathlib,leanprover-community/mathlib