Def HasStrictDerivAt.localInverse

Modification history

2024-05-07 01:05

Mathlib/Analysis/Calculus/InverseFunctionTheorem/Deriv.lean

refactor: replace `@[reducible]` with `abbrev` (#12614) …

Deleted HasStrictDerivAt.localInverse View on Github →

2023-12-09 02:01

Mathlib/Analysis/Calculus/InverseFunctionTheorem/ApproximatesLinearOn.lean

chore(Calculus/Inverse): split (#8603)

Modified HasStrictDerivAt.localInverse View on Github →

2023-06-04 17:52

Mathlib/Analysis/Calculus/Inverse.lean

feat: port Analysis.Calculus.Inverse (#4644)

Added HasStrictDerivAt.localInverse View on Github →