fix(topology/algebra/basic): remove duplicate lemma (#12097)
fix(topology/algebra/basic): remove duplicate lemma (#12097)

This lemma duplicates the lemma of the same name in the root namespace, and should not be in this namespace in the first place.

The other half of #12072, now that the dependent PR is merged.





leanprover-community/mathlib,leanprover-community/mathlib