mathlib
04e93ae3 - perf(topology/continuous_function/stone_weierstrass): fix timeout (#16844)

Commit
3 years ago
perf(topology/continuous_function/stone_weierstrass): fix timeout (#16844) Squeeze simps and replace a slow `convert` by `eq.subst` with explicit motive (maybe `convert` was unfolding the instances?). From >20s to 4s on my machine. Co-authored-by: sgouezel <sebastien.gouezel@univ-rennes1.fr>
Author
Parents
Loading