Commit 2022-12-11 08:23 43afc5ad
View on Github →refactor(topology/algebra/ring): rename subring.subring_topological_closure to subring.le_topological_closure (#17649)
Change the name of the different versions of the result
s ≤ s.closure
for various substructures s, eg. subring, subalgebra, etc., from substructure.substructure_topological_closure to substructure.le_topological_structure.
Indeed, it was noted in this discussion that the original names do not conform to the general naming policy in mathlib.