case pos
n p : ℕ
pp : Prime p
⊢ 0 < p ^ ↑(factorization n) p

case neg
n p : ℕ
pp : ¬Prime p
⊢ 0 < p ^ ↑(factorization n) p
n p : ℕ
⊢ 0 < p ^ ↑(factorization n) p
by_cases pp : p.Prime
no goals
case pos
n p : ℕ
pp : Prime p
⊢ 0 < p ^ ↑(factorization n) p
simp [pow_pos pp.pos]
no goals
case neg
n p : ℕ
pp : ¬Prime p
⊢ 0 < p ^ ↑(factorization n) p
simp [pp]