Commit 2022-04-05 11:05 c7626b7dView on Github →
feat(analysis/calculus/fderiv_analytic): an analytic function is smooth (#13127)
This basic fact was missing from the library, but all the nontrivial maths were already there, we are just adding the necessary glue.
ring in several proofs (to go down from 30s to 4s in one proof, for instance). I wonder if we should ban
ac_refl from mathlib currently.