Mathlib Changelog
v4
Changelog
About
Github
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