divisors_card_onehundredtwenty
plain-language theorem explainer
120 has exactly 16 positive divisors. Researchers checking small cases in arithmetic functions or preparing Möbius inversion examples would cite this count. The proof is a one-line native_decide tactic that evaluates the divisor set and its cardinality directly.
Claim. $d(120) = 16$, where $d(n)$ is the number of positive divisors of the natural number $n$.
background
The module supplies lightweight wrappers around Mathlib's arithmetic function library, beginning with the Möbius function μ. The divisor counting function appears here as a basic companion fact. No upstream lemmas are invoked.
proof idea
The proof is a one-line wrapper that applies the native_decide tactic to decide the equality.
why it matters
This records a concrete numerical value inside the arithmetic functions module. It anchors small-case checks that later support Möbius-related statements, even though no immediate downstream theorems reference it yet.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.