x : ℂ
n : ℕ
⊢ ↑abs (x ^ (↑n)⁻¹) = ↑abs (x ^ ↑(↑n)⁻¹)
x : ℂ
n : ℕ
⊢ ↑abs (x ^ (↑n)⁻¹) = ↑abs x ^ (↑n)⁻¹
rw [← abs_cpow_real]
no goals
x : ℂ
n : ℕ
⊢ ↑abs (x ^ (↑n)⁻¹) = ↑abs (x ^ ↑(↑n)⁻¹)
simp [-abs_cpow_real]