mathlib3
eefa4257 - perf(analysis/convec/topology): remove topological_add_group.path_connected instance (#12675)

Commit
3 years ago
perf(analysis/convec/topology): remove topological_add_group.path_connected instance (#12675) The linter was right in #10011 and `topological_add_group.path_connected` should not be an instance, because it creates enormous TC subproblems (turn on `pp.all` to get an idea of what's going on). Apparently the instance isn't even used in mathlib.
Author
Parents
Loading