k : Type u
inst✝ : Field k
H : ∀ (p : k[X]), Monic p → Irreducible p → ∃ x, eval x p = 0
p : k[X]
⊢ ∀ {g : k[X]}, Irreducible g → g ∣ map (RingHom.id k) p → degree g = 1
k : Type u
inst✝ : Field k
H : ∀ (p : k[X]), Monic p → Irreducible p → ∃ x, eval x p = 0
⊢ IsAlgClosed k
refine ⟨fun p ↦ Or.inr ?_⟩
k : Type u
inst✝ : Field k
H : ∀ (p : k[X]), Monic p → Irreducible p → ∃ x, eval x p = 0
p q : k[X]
hq : Irreducible q
a✝ : q ∣ map (RingHom.id k) p
⊢ degree q = 1
k : Type u
inst✝ : Field k
H : ∀ (p : k[X]), Monic p → Irreducible p → ∃ x, eval x p = 0
p : k[X]
⊢ ∀ {g : k[X]}, Irreducible g → g ∣ map (RingHom.id k) p → degree g = 1
intro q hq _
k : Type u
inst✝ : Field k
H : ∀ (p : k[X]), Monic p → Irreducible p → ∃ x, eval x p = 0
p q : k[X]
hq : Irreducible q
a✝ : q ∣ map (RingHom.id k) p
this : Irreducible (q * ↑C (leadingCoeff q)⁻¹)
⊢ degree q = 1
k : Type u
inst✝ : Field k
H : ∀ (p : k[X]), Monic p → Irreducible p → ∃ x, eval x p = 0
p q : k[X]
hq : Irreducible q
a✝ : q ∣ map (RingHom.id k) p
⊢ degree q = 1
have : Irreducible (q * C (leadingCoeff q)⁻¹) := by
  rw [← coe_normUnit_of_ne_zero hq.ne_zero]
  exact (associated_normalize _).irreducible hq
case intro
k : Type u
inst✝ : Field k
H : ∀ (p : k[X]), Monic p → Irreducible p → ∃ x, eval x p = 0
p q : k[X]
hq : Irreducible q
a✝ : q ∣ map (RingHom.id k) p
this : Irreducible (q * ↑C (leadingCoeff q)⁻¹)
x : k
hx : eval x (q * ↑C (leadingCoeff q)⁻¹) = 0
⊢ degree q = 1
k : Type u
inst✝ : Field k
H : ∀ (p : k[X]), Monic p → Irreducible p → ∃ x, eval x p = 0
p q : k[X]
hq : Irreducible q
a✝ : q ∣ map (RingHom.id k) p
this : Irreducible (q * ↑C (leadingCoeff q)⁻¹)
⊢ degree q = 1
obtain ⟨x, hx⟩ := H (q * C (leadingCoeff q)⁻¹) (monic_mul_leadingCoeff_inv hq.ne_zero) this
no goals
case intro
k : Type u
inst✝ : Field k
H : ∀ (p : k[X]), Monic p → Irreducible p → ∃ x, eval x p = 0
p q : k[X]
hq : Irreducible q
a✝ : q ∣ map (RingHom.id k) p
this : Irreducible (q * ↑C (leadingCoeff q)⁻¹)
x : k
hx : eval x (q * ↑C (leadingCoeff q)⁻¹) = 0
⊢ degree q = 1
exact degree_mul_leadingCoeff_inv q hq.ne_zero ▸ degree_eq_one_of_irreducible_of_root this hx
k : Type u
inst✝ : Field k
H : ∀ (p : k[X]), Monic p → Irreducible p → ∃ x, eval x p = 0
p q : k[X]
hq : Irreducible q
a✝ : q ∣ map (RingHom.id k) p
⊢ Irreducible (q * ↑(normUnit q))
k : Type u
inst✝ : Field k
H : ∀ (p : k[X]), Monic p → Irreducible p → ∃ x, eval x p = 0
p q : k[X]
hq : Irreducible q
a✝ : q ∣ map (RingHom.id k) p
⊢ Irreducible (q * ↑C (leadingCoeff q)⁻¹)
rw [← coe_normUnit_of_ne_zero hq.ne_zero]
no goals
k : Type u
inst✝ : Field k
H : ∀ (p : k[X]), Monic p → Irreducible p → ∃ x, eval x p = 0
p q : k[X]
hq : Irreducible q
a✝ : q ∣ map (RingHom.id k) p
⊢ Irreducible (q * ↑(normUnit q))
exact (associated_normalize _).irreducible hq