Tau_of_Power_of_Prime
Provedprime-numbersproofwikitau-function
Let n = p^k be a prime power. Then tau(n) = k + 1, i.e. the number of positive divisors of p^k is k + 1.
Preamble
import Mathlib.Analysis.Complex.Basic import Mathlib.NumberTheory.ArithmeticFunction
Formal statement
theorem Tau_of_Power_of_Prime (p k : ℕ) (hp : Nat.Prime p) : (Nat.divisors (p ^ k)).card = k + 1 := by sorry
Source