Tau_Function_from_Prime_Decomposition
Provedproofwikitau-function
If n = p1^k1 * ... * pr^kr, then τ(n) = (k1+1)(k2+1)...(kr+1).
Preamble
import Mathlib.Data.Nat.Factorization.Basic import Mathlib.NumberTheory.Divisors
Formal statement
theorem Tau_Function_from_Prime_Decomposition (n : ℕ) (hn : 0 < n) : (Nat.divisors n).card = n.factorization.prod (fun _ k => k + 1) := by sorry
Source