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

Commit
3 years ago
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.
Author
Parents
Loading