Commit 2026-10-28 01:55 ce8caa46

View on Github →

chore: rename ContDiffAt.hasStrict(F)DerivAt to hasStrict(F)DerivAt_(… (#44840) Currently, mathlib has both ContDiffAt.hasStrict(F)DerivAt and ContDiffAt.hasStrict(F)DerivAt': avoid the primed names by

renaming ContDiffAt.hasStrict(F)DerivAt to ContDiffAt.hasStrict(F)DerivAt_(f)deriv (which describes their statement more faithfully), and
renaming ContDiffAt.hasStrict(F)DerivAt' to ContDiffAt.hasStrict(F)DerivAt Because this is a cyclic rename, we can only generate deprecations for half of these.

Estimated changes

Modified Mathlib/Analysis/Calculus/ContDiff/RCLike.lean

deleted theorem ContDiffAt.hasStrictDerivAt'

modified theorem ContDiffAt.hasStrictDerivAt

added theorem ContDiffAt.hasStrictDerivAt_deriv

deleted theorem ContDiffAt.hasStrictFDerivAt'

modified theorem ContDiffAt.hasStrictFDerivAt

added theorem ContDiffAt.hasStrictFDerivAt_fderiv

Modified Mathlib/Analysis/Calculus/ImplicitContDiff.lean

Modified Mathlib/Analysis/Calculus/InverseFunctionTheorem/ContDiff.lean

Modified Mathlib/Analysis/SpecialFunctions/ExpDeriv.lean

Modified Mathlib/Analysis/SpecialFunctions/Pow/Deriv.lean