Tau_Function_is_Multiplicative
Provedmultiplicative-functionsproofwikitau-function
The divisor counting function tau is multiplicative: tau(mn) = tau(m) * tau(n) when gcd(m,n) = 1.
Preamble
import Mathlib.Analysis.Complex.Basic import Mathlib.NumberTheory.ArithmeticFunction
Formal statement
theorem Tau_Function_is_Multiplicative (m n : ℕ) (hm : 0 < m) (hn : 0 < n) (hcop : Nat.Coprime m n) : (Nat.divisors (m * n)).card = (Nat.divisors m).card * (Nat.divisors n).card := by sorry
Source