Commit 2022-11-13 01:44 ad3dfaca
View on Github →perf(analysis/complex/circle): fix a slow @[simps] (#17504)
This @[simps] is really slow on master and caused me a timeout in #17164, and moreover it generated a bad simp lemma (it used ↥(metric.sphere 0 1) instead of ↥circle), so I just wrote the lemma by hand.