mathlib

093ac77a - feat(analysis/calculus/specific_functions): smoothness of exp(-1/x) (#2087)

feat(analysis/calculus/specific_functions): smoothness of exp(-1/x) (#2087) * feat(analysis/calculus/specific_functions): smoothness of exp(-1/x) * use namespace; shorter names * fix field_simp Co-authored-by: mergify[bot] <37929162+mergify[bot]@users.noreply.github.com>