Tau_Function_of_Square_Free_Integer_is_Power_of_2
Provedproofwikisquare-free-integerstau-function
Let n be a square-free integer. Then tau(n) = 2^r for some r >= 1.
Preamble
import Mathlib.Analysis.Complex.Basic import Mathlib.NumberTheory.ArithmeticFunction
Formal statement
theorem Tau_Function_of_Square_Free_Integer_is_Power_of_2 (n : ℕ) (hn : 0 < n) (hsf : Squarefree n) : ∃ r : ℕ, (Nat.divisors n).card = 2 ^ r := by sorry
Source