naming: _root_.closure

Stream: mathlib4

[Yury G. Kudryashov]

I'm formalizing a statement that involves docs#AddSubgroup, docs#Submodule, and docs#closure. I don't want to use docs#AddSubgroup.topologicalClosure and docs#Submodule.topologicalClosure to use simp normal forms. What should I use as a part of the name corresponding to closure?

[Yury G. Kudryashov]

Currently, I plan to use closure, because the name is long enough to disambiguate with AddSubgroup.closure.