divisors_card_sixty_gt
plain-language theorem explainer
The declaration proves that 60 has more positive divisors than any smaller positive integer. Number theorists checking small highly composite cases or bounding divisor functions would cite this bound. The proof exhausts the finite interval 1 to 59 by case splitting and direct computation of divisor cardinalities.
Claim. For every natural number $n$ with $0 < n < 60$, the cardinality of the divisor set of $n$ is strictly less than the cardinality of the divisor set of 60.
background
The module supplies lightweight wrappers around Mathlib arithmetic functions, beginning with the Möbius function and related divisor operations. The divisor cardinality is the standard Mathlib function that returns the size of the set of positive divisors of a natural number. The local setting is a collection of small, stable interfaces for Dirichlet arithmetic that can later support inversion formulas.
proof idea
The term proof introduces n together with the positivity and upper-bound hypotheses. It then invokes interval_cases to partition the range 1 to 59 into individual cases, each discharged by native_decide which evaluates the divisor cardinalities directly.
why it matters
The result records the concrete fact that 60 is highly composite in the sense stated in its declaration comment. It supplies a verified small-case bound inside the arithmetic-functions module of the primes development. No downstream uses are recorded, so the lemma functions as a self-contained reference point rather than a link in a longer chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.