x✝ y z x : ℝ
hx : 0 ≤ x
n : ℕ
hn : n ≠ 0
hn0 : ↑n ≠ 0
⊢ (x ^ (↑n)⁻¹) ^ n = x
x✝ y z x : ℝ
hx : 0 ≤ x
n : ℕ
hn : n ≠ 0
⊢ (x ^ (↑n)⁻¹) ^ n = x
have hn0 : (n : ℝ) ≠ 0 := Nat.cast_ne_zero.2 hn
no goals
x✝ y z x : ℝ
hx : 0 ≤ x
n : ℕ
hn : n ≠ 0
hn0 : ↑n ≠ 0
⊢ (x ^ (↑n)⁻¹) ^ n = x
rw [← rpow_nat_cast, ← rpow_mul hx, inv_mul_cancel hn0, rpow_one]