k : Type u
inst✝¹ : Field k
inst✝ : IsAlgClosed k
p : k[X]
h : roots p = 0
⊢ p = ↑C (coeff p 0)
k : Type u
inst✝¹ : Field k
inst✝ : IsAlgClosed k
p : k[X]
⊢ roots p = 0 ↔ p = ↑C (coeff p 0)
refine' ⟨fun h => _, fun hp => by rw [hp, roots_C]⟩
case inl
k : Type u
inst✝¹ : Field k
inst✝ : IsAlgClosed k
p : k[X]
h : roots p = 0
hd : degree p ≤ 0
⊢ p = ↑C (coeff p 0)

case inr
k : Type u
inst✝¹ : Field k
inst✝ : IsAlgClosed k
p : k[X]
h : roots p = 0
hd : 0 < degree p
⊢ p = ↑C (coeff p 0)
k : Type u
inst✝¹ : Field k
inst✝ : IsAlgClosed k
p : k[X]
h : roots p = 0
⊢ p = ↑C (coeff p 0)
cases' le_or_lt (degree p) 0 with hd hd
no goals
k : Type u
inst✝¹ : Field k
inst✝ : IsAlgClosed k
p : k[X]
hp : p = ↑C (coeff p 0)
⊢ roots p = 0
rw [hp, roots_C]
no goals
case inl
k : Type u
inst✝¹ : Field k
inst✝ : IsAlgClosed k
p : k[X]
h : roots p = 0
hd : degree p ≤ 0
⊢ p = ↑C (coeff p 0)
exact eq_C_of_degree_le_zero hd
case inr.intro
k : Type u
inst✝¹ : Field k
inst✝ : IsAlgClosed k
p : k[X]
h : roots p = 0
hd : 0 < degree p
z : k
hz : IsRoot p z
⊢ p = ↑C (coeff p 0)
case inr
k : Type u
inst✝¹ : Field k
inst✝ : IsAlgClosed k
p : k[X]
h : roots p = 0
hd : 0 < degree p
⊢ p = ↑C (coeff p 0)
obtain ⟨z, hz⟩ := IsAlgClosed.exists_root p hd.ne'
case inr.intro
k : Type u
inst✝¹ : Field k
inst✝ : IsAlgClosed k
p : k[X]
h : roots p = 0
hd : 0 < degree p
z : k
hz : z ∈ 0
⊢ p = ↑C (coeff p 0)
case inr.intro
k : Type u
inst✝¹ : Field k
inst✝ : IsAlgClosed k
p : k[X]
h : roots p = 0
hd : 0 < degree p
z : k
hz : IsRoot p z
⊢ p = ↑C (coeff p 0)
rw [← mem_roots (ne_zero_of_degree_gt hd), h] at hz
no goals
case inr.intro
k : Type u
inst✝¹ : Field k
inst✝ : IsAlgClosed k
p : k[X]
h : roots p = 0
hd : 0 < degree p
z : k
hz : z ∈ 0
⊢ p = ↑C (coeff p 0)
simp at hz