totient
plain-language theorem explainer
Euler's totient function φ(n) counts positive integers up to n that are coprime to n. Number theorists working inside the Recognition Science project cite this wrapper to obtain standard arithmetic properties without repeated Mathlib references. The definition is a one-line alias to Nat.totient.
Claim. Euler's totient function is defined by $φ(n) := |{k ∈ ℕ | 1 ≤ k ≤ n, gcd(k,n)=1}|$. The declaration sets totient n := φ(n) for each natural number n.
background
The module supplies lightweight wrappers around Mathlib's arithmetic function library, beginning with the Möbius function μ. The local theoretical setting keeps statements lightweight before Dirichlet algebra and inversion are added. The totient wrapper supplies the standard Euler function φ(n) directly from Nat.totient, enabling later results on divisor sums and concrete evaluations.
proof idea
One-line wrapper that applies Nat.totient.
why it matters
This definition feeds parent results such as the divisor-sum identity ∑_{d|n} φ(d) = n and concrete evaluations like φ(8)=4. It supplies the arithmetic-functions layer required for prime-related theorems in NumberTheory.Primes, providing the Möbius footholds that precede deeper Recognition Science constructions. No open questions are closed by this declaration.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.