Square if number of divisors is odd

Stream: mathlib4

[Haoran Luo]

Hi, everyone! Does anyone know how to prove the following theorem in Lean? Is it already a theorem in Mathlib? (I have some difficulty in that even if I proved the multiplicity of every prime divisor is even, how to conclude that n is a square... Is there a theorem for this?)
Thanks!

theorem odd_divisors_imp_square (n : ℕ) (h : Odd (Nat.divisors n).card) : IsSquare n

[Yury G. Kudryashov]

Hi, in what context do you need this theorem?

[Haoran Luo]

Yury G. Kudryashov said:

Hi, in what context do you need this theorem?

I am trying to prove this, for some math problem. The previous one is one step in it.
IsSquare (n ^ (Nat.divisors n).card)

[Yury G. Kudryashov]

• Do you have a pen&paper proof?
• Please read #backticks and #mwe
• Is it for a homework? AI contractor's job? Something else?