totient_le
plain-language theorem explainer
φ(n) ≤ n holds for every natural number n. Researchers handling arithmetic functions within the Recognition Science number theory layer cite this inequality when bounding sums over divisors or sieving primes. The argument reduces to a direct call on the underlying Mathlib lemma after the local wrapper is unfolded.
Claim. For every natural number $n$, $ϕ(n) ≤ n$.
background
The module supplies lightweight wrappers around Mathlib's arithmetic functions, beginning with the Möbius function μ and including Euler's totient ϕ as a simple alias. The upstream definition states totient n := Nat.totient n. This places the bound among siblings such as mobius and bigOmega that prepare basic tools for Dirichlet inversion and prime counting.
proof idea
The term proof unfolds the local totient definition via simp only [totient] and then applies the Mathlib lemma Nat.totient_le directly.
why it matters
The inequality supplies a basic bound on the totient that supports estimates in prime number theory. No downstream theorems currently invoke it, yet it closes a necessary interface in the arithmetic-functions layer. The module documentation describes these wrappers as lightweight scaffolding for later Dirichlet-algebra work.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.