Squares_with_All_Odd_Digits
Provednumber-theoryproofwikisquare-numbers
The only perfect squares whose base-10 digits are all odd are 1 and 9.
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem Squares_with_All_Odd_Digits (n : ℕ) (hn : n * n % 10 % 2 = 1) (hn2 : n * n / 10 = 0 ∨ n * n / 10 % 10 % 2 = 1) : n * n = 1 ∨ n * n = 9 := by sorry
Source