totient_mul_of_coprime
plain-language theorem explainer
Euler's totient function satisfies φ(mn) = φ(m)φ(n) for coprime natural numbers m and n. Number theorists building multiplicative arithmetic functions would cite this when proving properties of φ ahead of Dirichlet inversion. The proof is a one-line wrapper that unfolds the local totient definition and invokes the matching Mathlib lemma.
Claim. If $m$ and $n$ are coprime natural numbers, then $φ(mn) = φ(m)φ(n)$, where $φ$ denotes Euler's totient function.
background
The module supplies lightweight wrappers around Mathlib arithmetic functions, starting with the Möbius function μ and including Euler's totient. The local definition is totient (n : ℕ) : ℕ := Nat.totient n. The setting prepares basic interfaces for later Dirichlet algebra and inversion once the wrappers stabilize.
proof idea
The proof is a one-line wrapper that applies Nat.totient_mul after unfolding the local totient definition via simp.
why it matters
This declaration feeds directly into totient_isMultiplicative, which restates the same property with universal quantifiers. It supplies the core multiplicativity step required by the module's roadmap toward divisor sums and prime-power cases. In the Recognition Science setting the result anchors discrete counting tools that appear in phi-ladder mass formulas and forcing-chain constructions.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.