Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-03-06 01:31 093ac77a

View on Github →

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

Estimated changes

Modified src/algebra/field.lean

added theorem div_sub'

added theorem sub_div'

Created src/analysis/calculus/specific_functions.lean

added def exp_neg_inv_glue.f_aux

added theorem exp_neg_inv_glue.f_aux_deriv

added theorem exp_neg_inv_glue.f_aux_deriv_pos

added theorem exp_neg_inv_glue.f_aux_deriv_zero

added theorem exp_neg_inv_glue.f_aux_has_deriv_at

added theorem exp_neg_inv_glue.f_aux_iterated_deriv

added theorem exp_neg_inv_glue.f_aux_limit

added theorem exp_neg_inv_glue.f_aux_zero_eq

added theorem exp_neg_inv_glue.nonneg

added theorem exp_neg_inv_glue.pos_of_pos

added theorem exp_neg_inv_glue.smooth

added theorem exp_neg_inv_glue.zero_of_nonpos

added def exp_neg_inv_glue

Modified test/ring.lean