A single odd-multiplicity prime forces prime times a square
ProvedOddPerfectNumber.Kernel.odd_mult_single_gives_prime_mul_sqfactorizationnumber-theoryperfect-numbers
If a nonzero natural number a has exactly one prime t with odd multiplicity in its factorization, then a = t*x^2 for some x.
Preamble
import Mathlib
Formal statement
namespace OddPerfectNumber.Kernel
theorem odd_mult_single_gives_prime_mul_sq {a t : Nat} (ha0 : a != 0) (ht : t.Prime)
(ht0 : ! Even (a.factorization t))
(hall : forall z : Nat, z != t -> Even (a.factorization z)) :
exists y : Nat, a = t * y ^ 2 := by
sorry
end OddPerfectNumber.Kernel