q : ℚ
x y : ℝ
n : ℕ
h : Irrational (x ^ n)
⊢ Irrational x
q : ℚ
x y : ℝ
n : ℕ
h : Irrational (x ^ ↑n)
⊢ Irrational x
rw [zpow_ofNat] at h
no goals
q : ℚ
x y : ℝ
n : ℕ
h : Irrational (x ^ n)
⊢ Irrational x
exact h.of_pow _
q : ℚ
x y : ℝ
n : ℕ
h : Irrational (x ^ (n + 1))⁻¹
⊢ Irrational x
q : ℚ
x y : ℝ
n : ℕ
h : Irrational (x ^ -[n+1])
⊢ Irrational x
rw [zpow_negSucc] at h
no goals
q : ℚ
x y : ℝ
n : ℕ
h : Irrational (x ^ (n + 1))⁻¹
⊢ Irrational x
exact h.of_inv.of_pow _