Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-10-01 01:14 2b23d2eb

View on Github →

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).

Estimated changes