totient_pos_iff
plain-language theorem explainer
Euler's totient function is positive precisely when its argument is a positive natural number. Researchers working with arithmetic functions and Möbius inversion cite the equivalence to drop zero cases from sums and products. The proof is a one-line wrapper that unfolds the local definition and invokes the corresponding Mathlib fact.
Claim. For every natural number $n$, $0 < ϕ(n)$ if and only if $0 < n$, where $ϕ$ denotes Euler's totient function.
background
The module supplies lightweight wrappers around Mathlib arithmetic functions, beginning with the Möbius function and including Euler's totient as a companion. The totient wrapper is defined by direct delegation: totient n := Nat.totient n. An upstream one-sided result establishes that positivity holds whenever the argument is positive.
proof idea
The proof is a one-line wrapper. Simplification unfolds the totient definition, after which the Mathlib theorem Nat.totient_pos is applied directly.
why it matters
This equivalence completes the basic positivity statement for totient inside the arithmetic functions module. It supports later Möbius inversion and Dirichlet series constructions that rest on these footholds. No downstream uses are recorded yet.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.