Tau_Function_Odd_Iff_Argument_is_Square
Provedproofwikisquare-numberstau-function
The number of divisors tau(n) is odd iff n is a perfect square.
Preamble
import Mathlib.Analysis.Complex.Basic import Mathlib.NumberTheory.ArithmeticFunction
Formal statement
theorem Tau_Function_Odd_Iff_Argument_is_Square (n : ℕ) (hn : 0 < n) : ¬ Even ((Nat.divisors n).card) ↔ IsSquare n := by sorry
Source