Commit 2022-02-17 12:16 eb8d58d6
View on Github →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.