totient_eq_card_filter
plain-language theorem explainer
Euler's totient counts the integers from 0 to n-1 that are coprime to n. Number theorists in the Recognition Science arithmetic layer cite this to equate the function definition with its explicit cardinality form for later coprimality arguments. The proof is a one-line term reduction that unfolds the local wrapper and invokes the standard library fact.
Claim. For any natural number $n$, $varphi(n) = |{a in {0,1,dots,n-1} : gcd(n,a)=1}|$.
background
The module supplies lightweight wrappers around Mathlib arithmetic functions, beginning with the Möbius function and including Euler's totient. The totient definition simply delegates to Nat.totient. The local setting focuses on providing footholds for Dirichlet algebra once basic interfaces stabilize, followed by additional coprimality facts for RS constants.
proof idea
The proof is a term-mode reduction: it simplifies using the totient definition and then applies the exact lemma Nat.totient_eq_card_coprime n from the standard library.
why it matters
This equivalence supports coprimality facts needed for RS constants in the NumberTheory layer. It connects to the broader arithmetic functions module that prepares Möbius inversion tools. No direct parent theorems appear in used_by, but the declaration sits immediately before the section on additional coprimality facts for RS constants.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.