# Commit 2022-04-05 11:05 c7626b7d

View 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.
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.