totient_six
plain-language theorem explainer
Euler's totient function evaluates to 2 at the integer 6. Researchers checking small composite cases while building arithmetic function libraries or Möbius inversion setups would cite this verification. The proof is a one-line native_decide that directly evaluates the totient wrapper definition.
Claim. Euler's totient function satisfies $φ(6) = 2$.
background
The module supplies lightweight wrappers around Mathlib arithmetic functions, beginning with the Möbius function μ and including Euler's totient. The totient definition is a direct wrapper: def totient (n : ℕ) : ℕ := Nat.totient n, which counts integers up to n coprime to n. This theorem sits inside the NumberTheory.Primes.ArithmeticFunctions module, which keeps statements lightweight pending deeper Dirichlet algebra and inversion layers.
proof idea
The proof is a one-line wrapper that applies the native_decide tactic to evaluate the totient definition at 6 by direct computation.
why it matters
This supplies a concrete verified value for the totient function inside the arithmetic functions module. It supports potential later use in prime factorization or squarefree checks, though no downstream theorems currently depend on it. The module focuses on Möbius footholds as preparation for inversion formulas.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.