mathlib
43afc5ad - refactor(topology/algebra/ring): rename subring.subring_topological_closure to subring.le_topological_closure (#17649)

Commit
3 years ago
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](https://github.com/leanprover-community/mathlib/pull/17212#discussion_r1018230281) that the original names do not conform to the general naming policy in mathlib.
Author
Parents
Loading