divisors_card_twelve
plain-language theorem explainer
Twelve possesses exactly six positive divisors. Number theorists working with arithmetic functions cite this when verifying small-case divisor counts in multiplicative settings. The proof reduces to a direct kernel evaluation via the native_decide tactic.
Claim. The cardinality of the set of positive divisors of the natural number 12 equals 6, that is, $|{d ∈ ℕ : d | 12}| = 6$.
background
The module supplies lightweight wrappers around Mathlib arithmetic functions, beginning with the Möbius function μ and its squarefree detection properties. This declaration records a basic divisor count for the integer 12 inside that setting. The module documentation states the intent to keep statements lightweight before layering deeper Dirichlet algebra and inversion.
proof idea
The proof is a one-line wrapper that applies the native_decide tactic, which evaluates the finite set of divisors of 12 and its cardinality directly inside the Lean kernel.
why it matters
The declaration supplies a verified arithmetic constant in the NumberTheory layer of the Recognition framework. It fills a basic proposition in the arithmetic functions module, consistent with the module's goal of stabilizing interfaces. No downstream theorems currently reference it, and it does not yet link to the phi-ladder or forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.