divisors_card_eighthundredforty
plain-language theorem explainer
840 has exactly 32 positive divisors. Number theorists checking small arithmetic computations or divisor counts would cite this result when validating basic facts in prime-related modules. The proof is a one-line term that invokes native_decide to evaluate the divisor cardinality directly.
Claim. The number of positive divisors of 840 is 32, that is, $d(840) = 32$.
background
The module supplies lightweight wrappers around Mathlib's arithmetic function library, beginning with the Möbius function μ. This theorem records a concrete small-case computation that fits the module's pattern of stabilizing basic interfaces before layering on Dirichlet algebra. No upstream results are invoked.
proof idea
The proof is a one-line term proof that applies native_decide to compute the equality directly from the definition of the divisor set.
why it matters
It supplies a verified divisor count inside the arithmetic functions module that supports the broader construction of Möbius footholds. No downstream theorems or open questions are linked to it.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.