Mathlib Map

Theorems · Theorem · real analysis

Real.hasDerivAt_log

∀ {x : ℝ}, x ≠ 0 → HasDerivAt Real.log x⁻¹ x
Defined in
Mathlib.Analysis.SpecialFunctions.Log.Deriv
Cited by
10 results in Mathlib
Foundations
Depth 203 from the axioms · uses propext, Classical.choice, Quot.sound
Mathlib docsSourceLoogleLeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

Real.differentiableAt_log · cited by 7Real.differentiableAt_logReal.deriv_log · cited by 4Real.deriv_logHasDerivWithinAt.log · cited by 2HasDerivWithinAt.logReal.not_continuousAt_inv_log_one · cited by 2Real.not_continuousAt_inv…Real.not_continuousAt_log_log_one · cited by 2Real.not_continuousAt_log…not_integrableOn_Ici_inv · cited by 2not_integrableOn_Ici_invHasFDerivAt.log · cited by 2HasFDerivAt.logHasFDerivWithinAt.log · cited by 2HasFDerivWithinAt.logderiv2_sqrt_mul_log · cited by 1deriv2_sqrt_mul_loghasDerivAt_sqrt_mul_log · cited by 1hasDerivAt_sqrt_mul_logReal · cited by 25697RealReal.log · cited by 939Real.logHasDerivAt · cited by 493HasDerivAtHasStrictDerivAt.hasDerivAt · cited by 52HasStrictDerivAt.hasDeriv…Real.hasStrictDerivAt_log · cited by 3Real.hasStrictDerivAt_logReal.hasDerivAt_logCITED BYCITES

Cites5

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

Cited by10

Results whose statement or proof uses this declaration.