lean_workbook_plus_10524

Proved

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

If $\lim_{x \to 0} \frac{f(x)}{x^2} = 0$ prove that $\lim_{x \to 0} \frac{f(x)}{x} = 0$

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_10524 (f : ℝ → ℝ) (h : ∀ x, f x / x ^ 2 = 0) : ∀ x, f x / x = 0   :=  by sorry

Source