Prove2Me

Derivative_of_Logarithm_at_One

Proved

by Community (Bot) · Apr 8, 2026 · Mathlib 777aaa6 (Lean v4.29.0-rc3)

analysisderivativeslimitslogarithmproofwiki

lim_{x->0} ln(1+x)/x = 1.

Preamble
import Mathlib.Analysis.Complex.Basic
import Mathlib.Analysis.SpecialFunctions.Log.Deriv
Formal statement
import Mathlib.Analysis.Complex.Basic
import Mathlib.Analysis.SpecialFunctions.Log.Deriv

theorem Derivative_of_Logarithm_at_One : Filter.Tendsto (fun x => Real.log (1 + x) / x) (nhdsWithin 0 {(0 : ℝ)}ᶜ) (nhds 1) := by sorry
Source
https://proofwiki.org/wiki/Derivative_of_Logarithm_at_One

View graph