Theorems · Theorem · real analysis
HasStrictDerivAt.hasStrictFDerivAt_equiv
∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {f : 𝕜 → 𝕜} {f' x : 𝕜},
HasStrictDerivAt f f' x →
∀ (hf' : f' ≠ 0), HasStrictFDerivAt f (↑((ContinuousLinearEquiv.unitsEquivAut 𝕜) (Units.mk0 f' hf'))) x- Defined in
- Mathlib.Analysis.Calculus.Deriv.Inverse
- Cited by
- 10 results in Mathlib
- Foundations
- Depth 166 from the axioms · uses propext, Classical.choice, Quot.sound
- Assumes
- NontriviallyNormedField
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites11
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- DFunLike.coestatement · cited by 62,936
- RingHom.idstatement · cited by 18,349
- NontriviallyNormedFieldstatement and proof · cited by 8,742
- Equivstatement · cited by 8,337
- Unitsstatement · cited by 2,804
- ContinuousLinearEquivstatement · cited by 743
- ContinuousLinearEquiv.toContinuousLinearMapstatement · cited by 448
- HasStrictFDerivAtstatement · cited by 261
- Units.mk0statement · cited by 181
- HasStrictDerivAtstatement and proof · cited by 163
- ContinuousLinearEquiv.unitsEquivAutstatement · cited by 7
Cited by11
Results whose statement or proof uses this declaration.
- HasStrictDerivAt.localInverseproof · cited by 7
- HasStrictDerivAt.eventually_right_inverseproof · cited by 2
- Function.Periodic.differentiableAt_cuspFunctionproof · cited by 2
- analyticAt_comp_iff_of_deriv_ne_zeroproof · cited by 2
- meromorphicAt_comp_iff_of_deriv_ne_zeroproof · cited by 2
- HasStrictDerivAt.of_local_left_inverseproof · cited by 2
- HasStrictDerivAt.to_localInverseproof · cited by 1
- Polynomial.isCoveringMapOn_evalproof · cited by 1
- HasStrictDerivAt.map_nhds_eqproof · cited by 1
- HasStrictDerivAt.eventually_left_inverseproof · cited by 0
- HasStrictDerivAt.to_local_left_inverseproof · cited by 0