case inl

⊢ ↑Λ 1 ≠ 0 ↔ IsPrimePow 1

case inr
n : ℕ
hn : n ≠ 1
⊢ ↑Λ n ≠ 0 ↔ IsPrimePow n
n : ℕ
⊢ ↑Λ n ≠ 0 ↔ IsPrimePow n
rcases eq_or_ne n 1 with (rfl | hn)
no goals
case inr
n : ℕ
hn : n ≠ 1
⊢ ↑Λ n ≠ 0 ↔ IsPrimePow n
exact (Real.log_pos (one_lt_cast.2 (minFac_prime hn).one_lt)).ne'.ite_ne_right_iff
no goals
case inl

⊢ ↑Λ 1 ≠ 0 ↔ IsPrimePow 1
simp [not_isPrimePow_one]