mathlib
2b23d2eb - chore(topology/algebra): remove dead code (#9467)

Commit
4 years ago
chore(topology/algebra): remove dead code (#9467) This code wasn't used and its historically intended use will soon be redone much better. The second file is only a dead import and a misleading comment (referring to the dead code of the *other* file).
Author
Parents
Loading