Commit 2023-06-02 06:13 b89360a6

View on Github →

feat: port Analysis.Calculus.LHopital (#4556)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Analysis/Calculus/LHopital.lean

added theorem HasDerivAt.lhopital_zero_atBot

added theorem HasDerivAt.lhopital_zero_atBot_on_Iio

added theorem HasDerivAt.lhopital_zero_atTop

added theorem HasDerivAt.lhopital_zero_atTop_on_Ioi

added theorem HasDerivAt.lhopital_zero_left_on_Ioc

added theorem HasDerivAt.lhopital_zero_left_on_Ioo

added theorem HasDerivAt.lhopital_zero_nhds'

added theorem HasDerivAt.lhopital_zero_nhds

added theorem HasDerivAt.lhopital_zero_nhds_left

added theorem HasDerivAt.lhopital_zero_nhds_right

added theorem HasDerivAt.lhopital_zero_right_on_Ico

added theorem HasDerivAt.lhopital_zero_right_on_Ioo

added theorem deriv.lhopital_zero_atBot

added theorem deriv.lhopital_zero_atBot_on_Iio

added theorem deriv.lhopital_zero_atTop

added theorem deriv.lhopital_zero_atTop_on_Ioi

added theorem deriv.lhopital_zero_left_on_Ioo

added theorem deriv.lhopital_zero_nhds'

added theorem deriv.lhopital_zero_nhds

added theorem deriv.lhopital_zero_nhds_left

added theorem deriv.lhopital_zero_nhds_right

added theorem deriv.lhopital_zero_right_on_Ico

added theorem deriv.lhopital_zero_right_on_Ioo