fix: erdos_828.variants.phi_dvd_self_iff_pow2_pow3 (google-deepmind#1155)

claim is true only for positive `a`

Author: smmercuri

FormalConjectures/ErdosProblems/828.lean

@@ -45,7 +45,8 @@ theorem erdos_828.variants.lehmer_conjecture : (∀ n > 1, φ n ∣ n - 1 ↔ Pr
 It is an easy exercise to show that, for $n > 1$, $\phi(n) | n$ if and only if $n = 2^a 3^b$.
 -/
 @[category undergraduate, AMS 11]
-theorem erdos_828.variants.phi_dvd_self_iff_pow2_pow3 : ∀ n > 1, φ n ∣ n ↔ ∃ a b, n = 2^a * 3^b := by
+theorem erdos_828.variants.phi_dvd_self_iff_pow2_pow3 {n : ℕ} (hn : 1 > n):
+    φ n ∣ n ↔ ∃ᵉ (a > 0) (b), n = 2^a * 3^b := by
   sorry
 
 end Erdos828