lean_workbook_plus_77200

Proved

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

Let $n\in\mathbb{N}$ . Show that $d(n)\leq n$ where $d(n)$ denote the number of divisors of $n$ . When does the equality hold ?

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_77200 : ∀ n : ℕ, n.divisors.card ≤ n   :=  by sorry

Source