Commit 2024-12-28 10:33 d09b8698

View on Github →

chore: rename iteratedDeriv_const_{smul,mul} (#20136)

Estimated changes

Modified Mathlib/Analysis/Calculus/Deriv/Basic.lean

added theorem derivWithin_id'

Modified Mathlib/Analysis/Calculus/FDeriv/Basic.lean

added theorem differentiableWithinAt_id'

Modified Mathlib/Analysis/Calculus/IteratedDeriv/Lemmas.lean

added theorem iteratedDerivWithin_comp_const_smul

added theorem iteratedDeriv_comp_const_mul

added theorem iteratedDeriv_comp_const_smul

deleted theorem iteratedDeriv_const_mul

deleted theorem iteratedDeriv_const_smul

Modified Mathlib/Analysis/SpecialFunctions/ExpDeriv.lean