k : Type u
inst✝¹ : Field k
inst✝ : IsAlgClosed k
x : k
n : ℕ
hn : 0 < n
this : degree (X ^ n - ↑C x) ≠ 0
⊢ ∃ z, z ^ n = x
k : Type u
inst✝¹ : Field k
inst✝ : IsAlgClosed k
x : k
n : ℕ
hn : 0 < n
⊢ ∃ z, z ^ n = x
have : degree (X ^ n - C x) ≠ 0 := by
  rw [degree_X_pow_sub_C hn x]
  exact ne_of_gt (WithBot.coe_lt_coe.2 hn)
case intro
k : Type u
inst✝¹ : Field k
inst✝ : IsAlgClosed k
x : k
n : ℕ
hn : 0 < n
this : degree (X ^ n - ↑C x) ≠ 0
z : k
hz : IsRoot (X ^ n - ↑C x) z
⊢ ∃ z, z ^ n = x
k : Type u
inst✝¹ : Field k
inst✝ : IsAlgClosed k
x : k
n : ℕ
hn : 0 < n
this : degree (X ^ n - ↑C x) ≠ 0
⊢ ∃ z, z ^ n = x
obtain ⟨z, hz⟩ := exists_root (X ^ n - C x) this
k : Type u
inst✝¹ : Field k
inst✝ : IsAlgClosed k
x : k
n : ℕ
hn : 0 < n
⊢ ↑n ≠ 0
k : Type u
inst✝¹ : Field k
inst✝ : IsAlgClosed k
x : k
n : ℕ
hn : 0 < n
⊢ degree (X ^ n - ↑C x) ≠ 0
rw [degree_X_pow_sub_C hn x]
no goals
k : Type u
inst✝¹ : Field k
inst✝ : IsAlgClosed k
x : k
n : ℕ
hn : 0 < n
⊢ ↑n ≠ 0
exact ne_of_gt (WithBot.coe_lt_coe.2 hn)
case intro
k : Type u
inst✝¹ : Field k
inst✝ : IsAlgClosed k
x : k
n : ℕ
hn : 0 < n
this : degree (X ^ n - ↑C x) ≠ 0
z : k
hz : IsRoot (X ^ n - ↑C x) z
⊢ z ^ n = x
case intro
k : Type u
inst✝¹ : Field k
inst✝ : IsAlgClosed k
x : k
n : ℕ
hn : 0 < n
this : degree (X ^ n - ↑C x) ≠ 0
z : k
hz : IsRoot (X ^ n - ↑C x) z
⊢ ∃ z, z ^ n = x
use z
case intro
k : Type u
inst✝¹ : Field k
inst✝ : IsAlgClosed k
x : k
n : ℕ
hn : 0 < n
this : degree (X ^ n - ↑C x) ≠ 0
z : k
hz : z ^ n - x = 0
⊢ z ^ n = x
case intro
k : Type u
inst✝¹ : Field k
inst✝ : IsAlgClosed k
x : k
n : ℕ
hn : 0 < n
this : degree (X ^ n - ↑C x) ≠ 0
z : k
hz : IsRoot (X ^ n - ↑C x) z
⊢ z ^ n = x
simp only [eval_C, eval_X, eval_pow, eval_sub, IsRoot.def] at hz
no goals
case intro
k : Type u
inst✝¹ : Field k
inst✝ : IsAlgClosed k
x : k
n : ℕ
hn : 0 < n
this : degree (X ^ n - ↑C x) ≠ 0
z : k
hz : z ^ n - x = 0
⊢ z ^ n = x
exact sub_eq_zero.1 hz