case intro
p : ℝ
⊢ (Summable fun n => ↑n ^ (-p)) ↔ -p < -1
p : ℝ
⊢ (Summable fun n => ↑n ^ p) ↔ p < -1
rcases neg_surjective p with ⟨p, rfl⟩
no goals
case intro
p : ℝ
⊢ (Summable fun n => ↑n ^ (-p)) ↔ -p < -1
simp [rpow_neg]