Commit 2022-04-05 11:05 c7626b7d

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. Also, replace ac_refl by 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.