case pos
F : Type u
K : Type v
L : Type w
inst✝² : CommRing K
inst✝¹ : Field L
inst✝ : Field F
i✝ : K →+* L
p : K[X]
i : K →+* L
hsplit : Splits i p
hp : map i p = 0
⊢ natDegree (map i p) = ↑Multiset.card (roots (map i p))

case neg
F : Type u
K : Type v
L : Type w
inst✝² : CommRing K
inst✝¹ : Field L
inst✝ : Field F
i✝ : K →+* L
p : K[X]
i : K →+* L
hsplit : Splits i p
hp : ¬map i p = 0
⊢ natDegree (map i p) = ↑Multiset.card (roots (map i p))
F : Type u
K : Type v
L : Type w
inst✝² : CommRing K
inst✝¹ : Field L
inst✝ : Field F
i✝ : K →+* L
p : K[X]
i : K →+* L
hsplit : Splits i p
⊢ natDegree (map i p) = ↑Multiset.card (roots (map i p))
by_cases hp : p.map i = 0
case neg.intro.intro.intro
F : Type u
K : Type v
L : Type w
inst✝² : CommRing K
inst✝¹ : Field L
inst✝ : Field F
i✝ : K →+* L
p : K[X]
i : K →+* L
hsplit : Splits i p
hp : ¬map i p = 0
q : L[X]
he : Multiset.prod (Multiset.map (fun a => X - ↑C a) (roots (map i p))) * q = map i p
hd : ↑Multiset.card (roots (map i p)) + natDegree q = natDegree (map i p)
hr : roots q = 0
⊢ natDegree (map i p) = ↑Multiset.card (roots (map i p))
case neg
F : Type u
K : Type v
L : Type w
inst✝² : CommRing K
inst✝¹ : Field L
inst✝ : Field F
i✝ : K →+* L
p : K[X]
i : K →+* L
hsplit : Splits i p
hp : ¬map i p = 0
⊢ natDegree (map i p) = ↑Multiset.card (roots (map i p))
obtain ⟨q, he, hd, hr⟩ := exists_prod_multiset_X_sub_C_mul (p.map i)
case neg.intro.intro.intro
F : Type u
K : Type v
L : Type w
inst✝² : CommRing K
inst✝¹ : Field L
inst✝ : Field F
i✝ : K →+* L
p : K[X]
i : K →+* L
hp : ¬map i p = 0
q : L[X]
hsplit : Splits (RingHom.id L) (Multiset.prod (Multiset.map (fun a => X - ↑C a) (roots (map i p))) * q)
he : Multiset.prod (Multiset.map (fun a => X - ↑C a) (roots (map i p))) * q = map i p
hd : ↑Multiset.card (roots (map i p)) + natDegree q = natDegree (map i p)
hr : roots q = 0
⊢ natDegree (map i p) = ↑Multiset.card (roots (map i p))
case neg.intro.intro.intro
F : Type u
K : Type v
L : Type w
inst✝² : CommRing K
inst✝¹ : Field L
inst✝ : Field F
i✝ : K →+* L
p : K[X]
i : K →+* L
hsplit : Splits i p
hp : ¬map i p = 0
q : L[X]
he : Multiset.prod (Multiset.map (fun a => X - ↑C a) (roots (map i p))) * q = map i p
hd : ↑Multiset.card (roots (map i p)) + natDegree q = natDegree (map i p)
hr : roots q = 0
⊢ natDegree (map i p) = ↑Multiset.card (roots (map i p))
rw [← splits_id_iff_splits, ← he] at hsplit
case neg.intro.intro.intro
F : Type u
K : Type v
L : Type w
inst✝² : CommRing K
inst✝¹ : Field L
inst✝ : Field F
i✝ : K →+* L
p : K[X]
i : K →+* L
q : L[X]
hp : ¬Multiset.prod (Multiset.map (fun a => X - ↑C a) (roots (map i p))) * q = 0
hsplit : Splits (RingHom.id L) (Multiset.prod (Multiset.map (fun a => X - ↑C a) (roots (map i p))) * q)
he : Multiset.prod (Multiset.map (fun a => X - ↑C a) (roots (map i p))) * q = map i p
hd : ↑Multiset.card (roots (map i p)) + natDegree q = natDegree (map i p)
hr : roots q = 0
⊢ natDegree (map i p) = ↑Multiset.card (roots (map i p))
case neg.intro.intro.intro
F : Type u
K : Type v
L : Type w
inst✝² : CommRing K
inst✝¹ : Field L
inst✝ : Field F
i✝ : K →+* L
p : K[X]
i : K →+* L
hp : ¬map i p = 0
q : L[X]
hsplit : Splits (RingHom.id L) (Multiset.prod (Multiset.map (fun a => X - ↑C a) (roots (map i p))) * q)
he : Multiset.prod (Multiset.map (fun a => X - ↑C a) (roots (map i p))) * q = map i p
hd : ↑Multiset.card (roots (map i p)) + natDegree q = natDegree (map i p)
hr : roots q = 0
⊢ natDegree (map i p) = ↑Multiset.card (roots (map i p))
rw [← he] at hp
case neg.intro.intro.intro
F : Type u
K : Type v
L : Type w
inst✝² : CommRing K
inst✝¹ : Field L
inst✝ : Field F
i✝ : K →+* L
p : K[X]
i : K →+* L
q : L[X]
hp : ¬Multiset.prod (Multiset.map (fun a => X - ↑C a) (roots (map i p))) * q = 0
hsplit : Splits (RingHom.id L) (Multiset.prod (Multiset.map (fun a => X - ↑C a) (roots (map i p))) * q)
he : Multiset.prod (Multiset.map (fun a => X - ↑C a) (roots (map i p))) * q = map i p
hd : ↑Multiset.card (roots (map i p)) + natDegree q = natDegree (map i p)
hr : roots q = 0
hq : q ≠ 0
⊢ natDegree (map i p) = ↑Multiset.card (roots (map i p))
case neg.intro.intro.intro
F : Type u
K : Type v
L : Type w
inst✝² : CommRing K
inst✝¹ : Field L
inst✝ : Field F
i✝ : K →+* L
p : K[X]
i : K →+* L
q : L[X]
hp : ¬Multiset.prod (Multiset.map (fun a => X - ↑C a) (roots (map i p))) * q = 0
hsplit : Splits (RingHom.id L) (Multiset.prod (Multiset.map (fun a => X - ↑C a) (roots (map i p))) * q)
he : Multiset.prod (Multiset.map (fun a => X - ↑C a) (roots (map i p))) * q = map i p
hd : ↑Multiset.card (roots (map i p)) + natDegree q = natDegree (map i p)
hr : roots q = 0
⊢ natDegree (map i p) = ↑Multiset.card (roots (map i p))
have hq : q ≠ 0 := fun h => hp (by rw [h, MulZeroClass.mul_zero])
case neg.intro.intro.intro
F : Type u
K : Type v
L : Type w
inst✝² : CommRing K
inst✝¹ : Field L
inst✝ : Field F
i✝ : K →+* L
p : K[X]
i : K →+* L
q : L[X]
hp : ¬Multiset.prod (Multiset.map (fun a => X - ↑C a) (roots (map i p))) * q = 0
hsplit : Splits (RingHom.id L) (Multiset.prod (Multiset.map (fun a => X - ↑C a) (roots (map i p))) * q)
he : Multiset.prod (Multiset.map (fun a => X - ↑C a) (roots (map i p))) * q = map i p
hd : ↑Multiset.card (roots (map i p)) + natDegree q = natDegree (map i p)
hr : roots q = 0
hq : q ≠ 0
⊢ natDegree q = 0
case neg.intro.intro.intro
F : Type u
K : Type v
L : Type w
inst✝² : CommRing K
inst✝¹ : Field L
inst✝ : Field F
i✝ : K →+* L
p : K[X]
i : K →+* L
q : L[X]
hp : ¬Multiset.prod (Multiset.map (fun a => X - ↑C a) (roots (map i p))) * q = 0
hsplit : Splits (RingHom.id L) (Multiset.prod (Multiset.map (fun a => X - ↑C a) (roots (map i p))) * q)
he : Multiset.prod (Multiset.map (fun a => X - ↑C a) (roots (map i p))) * q = map i p
hd : ↑Multiset.card (roots (map i p)) + natDegree q = natDegree (map i p)
hr : roots q = 0
hq : q ≠ 0
⊢ natDegree (map i p) = ↑Multiset.card (roots (map i p))
rw [← hd, add_right_eq_self]
case neg.intro.intro.intro
F : Type u
K : Type v
L : Type w
inst✝² : CommRing K
inst✝¹ : Field L
inst✝ : Field F
i✝ : K →+* L
p : K[X]
i : K →+* L
q : L[X]
hp : ¬Multiset.prod (Multiset.map (fun a => X - ↑C a) (roots (map i p))) * q = 0
hsplit : Splits (RingHom.id L) (Multiset.prod (Multiset.map (fun a => X - ↑C a) (roots (map i p))) * q)
he : Multiset.prod (Multiset.map (fun a => X - ↑C a) (roots (map i p))) * q = map i p
hd : ↑Multiset.card (roots (map i p)) + natDegree q = natDegree (map i p)
hr : roots q = 0
hq : q ≠ 0
h : ¬natDegree q = 0
⊢ False
case neg.intro.intro.intro
F : Type u
K : Type v
L : Type w
inst✝² : CommRing K
inst✝¹ : Field L
inst✝ : Field F
i✝ : K →+* L
p : K[X]
i : K →+* L
q : L[X]
hp : ¬Multiset.prod (Multiset.map (fun a => X - ↑C a) (roots (map i p))) * q = 0
hsplit : Splits (RingHom.id L) (Multiset.prod (Multiset.map (fun a => X - ↑C a) (roots (map i p))) * q)
he : Multiset.prod (Multiset.map (fun a => X - ↑C a) (roots (map i p))) * q = map i p
hd : ↑Multiset.card (roots (map i p)) + natDegree q = natDegree (map i p)
hr : roots q = 0
hq : q ≠ 0
⊢ natDegree q = 0
by_contra h
case neg.intro.intro.intro
F : Type u
K : Type v
L : Type w
inst✝² : CommRing K
inst✝¹ : Field L
inst✝ : Field F
i✝ : K →+* L
p : K[X]
i : K →+* L
q : L[X]
hp : ¬Multiset.prod (Multiset.map (fun a => X - ↑C a) (roots (map i p))) * q = 0
hsplit : Splits (RingHom.id L) (Multiset.prod (Multiset.map (fun a => X - ↑C a) (roots (map i p))) * q)
he : Multiset.prod (Multiset.map (fun a => X - ↑C a) (roots (map i p))) * q = map i p
hd : ↑Multiset.card (roots (map i p)) + natDegree q = natDegree (map i p)
hr : roots q = 0
hq : q ≠ 0
h : ¬natDegree q = 0
h' : natDegree (map (RingHom.id L) q) ≠ 0
⊢ False
case neg.intro.intro.intro
F : Type u
K : Type v
L : Type w
inst✝² : CommRing K
inst✝¹ : Field L
inst✝ : Field F
i✝ : K →+* L
p : K[X]
i : K →+* L
q : L[X]
hp : ¬Multiset.prod (Multiset.map (fun a => X - ↑C a) (roots (map i p))) * q = 0
hsplit : Splits (RingHom.id L) (Multiset.prod (Multiset.map (fun a => X - ↑C a) (roots (map i p))) * q)
he : Multiset.prod (Multiset.map (fun a => X - ↑C a) (roots (map i p))) * q = map i p
hd : ↑Multiset.card (roots (map i p)) + natDegree q = natDegree (map i p)
hr : roots q = 0
hq : q ≠ 0
h : ¬natDegree q = 0
⊢ False
have h' : (map (RingHom.id L) q).natDegree ≠ 0 := by simp [h]
case neg.intro.intro.intro.refine_2
F : Type u
K : Type v
L : Type w
inst✝² : CommRing K
inst✝¹ : Field L
inst✝ : Field F
i✝ : K →+* L
p : K[X]
i : K →+* L
q : L[X]
hp : ¬Multiset.prod (Multiset.map (fun a => X - ↑C a) (roots (map i p))) * q = 0
hsplit : Splits (RingHom.id L) (Multiset.prod (Multiset.map (fun a => X - ↑C a) (roots (map i p))) * q)
he : Multiset.prod (Multiset.map (fun a => X - ↑C a) (roots (map i p))) * q = map i p
hd : ↑Multiset.card (roots (map i p)) + natDegree q = natDegree (map i p)
hr : roots q = 0
hq : q ≠ 0
h : ¬natDegree q = 0
h' : natDegree (map (RingHom.id L) q) ≠ 0
this : roots (map (RingHom.id L) q) ≠ 0
⊢ False

case neg.intro.intro.intro.refine_1
F : Type u
K : Type v
L : Type w
inst✝² : CommRing K
inst✝¹ : Field L
inst✝ : Field F
i✝ : K →+* L
p : K[X]
i : K →+* L
q : L[X]
hp : ¬Multiset.prod (Multiset.map (fun a => X - ↑C a) (roots (map i p))) * q = 0
hsplit : Splits (RingHom.id L) (Multiset.prod (Multiset.map (fun a => X - ↑C a) (roots (map i p))) * q)
he : Multiset.prod (Multiset.map (fun a => X - ↑C a) (roots (map i p))) * q = map i p
hd : ↑Multiset.card (roots (map i p)) + natDegree q = natDegree (map i p)
hr : roots q = 0
hq : q ≠ 0
h : ¬natDegree q = 0
h' : natDegree (map (RingHom.id L) q) ≠ 0
⊢ map (RingHom.id L) (Multiset.prod (Multiset.map (fun a => X - ↑C a) (roots (map i p))) * q) ≠ 0
case neg.intro.intro.intro
F : Type u
K : Type v
L : Type w
inst✝² : CommRing K
inst✝¹ : Field L
inst✝ : Field F
i✝ : K →+* L
p : K[X]
i : K →+* L
q : L[X]
hp : ¬Multiset.prod (Multiset.map (fun a => X - ↑C a) (roots (map i p))) * q = 0
hsplit : Splits (RingHom.id L) (Multiset.prod (Multiset.map (fun a => X - ↑C a) (roots (map i p))) * q)
he : Multiset.prod (Multiset.map (fun a => X - ↑C a) (roots (map i p))) * q = map i p
hd : ↑Multiset.card (roots (map i p)) + natDegree q = natDegree (map i p)
hr : roots q = 0
hq : q ≠ 0
h : ¬natDegree q = 0
h' : natDegree (map (RingHom.id L) q) ≠ 0
⊢ False
have := roots_ne_zero_of_splits' (RingHom.id L) (splits_of_splits_mul' _ ?_ hsplit).2 h'
no goals
case pos
F : Type u
K : Type v
L : Type w
inst✝² : CommRing K
inst✝¹ : Field L
inst✝ : Field F
i✝ : K →+* L
p : K[X]
i : K →+* L
hsplit : Splits i p
hp : map i p = 0
⊢ natDegree (map i p) = ↑Multiset.card (roots (map i p))
rw [hp, natDegree_zero, roots_zero, Multiset.card_zero]
no goals
F : Type u
K : Type v
L : Type w
inst✝² : CommRing K
inst✝¹ : Field L
inst✝ : Field F
i✝ : K →+* L
p : K[X]
i : K →+* L
q : L[X]
hp : ¬Multiset.prod (Multiset.map (fun a => X - ↑C a) (roots (map i p))) * q = 0
hsplit : Splits (RingHom.id L) (Multiset.prod (Multiset.map (fun a => X - ↑C a) (roots (map i p))) * q)
he : Multiset.prod (Multiset.map (fun a => X - ↑C a) (roots (map i p))) * q = map i p
hd : ↑Multiset.card (roots (map i p)) + natDegree q = natDegree (map i p)
hr : roots q = 0
h : q = 0
⊢ Multiset.prod (Multiset.map (fun a => X - ↑C a) (roots (map i p))) * q = 0
rw [h, MulZeroClass.mul_zero]
no goals
F : Type u
K : Type v
L : Type w
inst✝² : CommRing K
inst✝¹ : Field L
inst✝ : Field F
i✝ : K →+* L
p : K[X]
i : K →+* L
q : L[X]
hp : ¬Multiset.prod (Multiset.map (fun a => X - ↑C a) (roots (map i p))) * q = 0
hsplit : Splits (RingHom.id L) (Multiset.prod (Multiset.map (fun a => X - ↑C a) (roots (map i p))) * q)
he : Multiset.prod (Multiset.map (fun a => X - ↑C a) (roots (map i p))) * q = map i p
hd : ↑Multiset.card (roots (map i p)) + natDegree q = natDegree (map i p)
hr : roots q = 0
hq : q ≠ 0
h : ¬natDegree q = 0
⊢ natDegree (map (RingHom.id L) q) ≠ 0
simp [h]
case neg.intro.intro.intro.refine_2
F : Type u
K : Type v
L : Type w
inst✝² : CommRing K
inst✝¹ : Field L
inst✝ : Field F
i✝ : K →+* L
p : K[X]
i : K →+* L
q : L[X]
hp : ¬Multiset.prod (Multiset.map (fun a => X - ↑C a) (roots (map i p))) * q = 0
hsplit : Splits (RingHom.id L) (Multiset.prod (Multiset.map (fun a => X - ↑C a) (roots (map i p))) * q)
he : Multiset.prod (Multiset.map (fun a => X - ↑C a) (roots (map i p))) * q = map i p
hd : ↑Multiset.card (roots (map i p)) + natDegree q = natDegree (map i p)
hr : roots q = 0
hq : q ≠ 0
h : ¬natDegree q = 0
h' : natDegree (map (RingHom.id L) q) ≠ 0
this : roots q ≠ 0
⊢ False
case neg.intro.intro.intro.refine_2
F : Type u
K : Type v
L : Type w
inst✝² : CommRing K
inst✝¹ : Field L
inst✝ : Field F
i✝ : K →+* L
p : K[X]
i : K →+* L
q : L[X]
hp : ¬Multiset.prod (Multiset.map (fun a => X - ↑C a) (roots (map i p))) * q = 0
hsplit : Splits (RingHom.id L) (Multiset.prod (Multiset.map (fun a => X - ↑C a) (roots (map i p))) * q)
he : Multiset.prod (Multiset.map (fun a => X - ↑C a) (roots (map i p))) * q = map i p
hd : ↑Multiset.card (roots (map i p)) + natDegree q = natDegree (map i p)
hr : roots q = 0
hq : q ≠ 0
h : ¬natDegree q = 0
h' : natDegree (map (RingHom.id L) q) ≠ 0
this : roots (map (RingHom.id L) q) ≠ 0
⊢ False
rw [map_id] at this
no goals
case neg.intro.intro.intro.refine_2
F : Type u
K : Type v
L : Type w
inst✝² : CommRing K
inst✝¹ : Field L
inst✝ : Field F
i✝ : K →+* L
p : K[X]
i : K →+* L
q : L[X]
hp : ¬Multiset.prod (Multiset.map (fun a => X - ↑C a) (roots (map i p))) * q = 0
hsplit : Splits (RingHom.id L) (Multiset.prod (Multiset.map (fun a => X - ↑C a) (roots (map i p))) * q)
he : Multiset.prod (Multiset.map (fun a => X - ↑C a) (roots (map i p))) * q = map i p
hd : ↑Multiset.card (roots (map i p)) + natDegree q = natDegree (map i p)
hr : roots q = 0
hq : q ≠ 0
h : ¬natDegree q = 0
h' : natDegree (map (RingHom.id L) q) ≠ 0
this : roots q ≠ 0
⊢ False
exact this hr
case neg.intro.intro.intro.refine_1
F : Type u
K : Type v
L : Type w
inst✝² : CommRing K
inst✝¹ : Field L
inst✝ : Field F
i✝ : K →+* L
p : K[X]
i : K →+* L
q : L[X]
hp : ¬Multiset.prod (Multiset.map (fun a => X - ↑C a) (roots (map i p))) * q = 0
hsplit : Splits (RingHom.id L) (Multiset.prod (Multiset.map (fun a => X - ↑C a) (roots (map i p))) * q)
he : Multiset.prod (Multiset.map (fun a => X - ↑C a) (roots (map i p))) * q = map i p
hd : ↑Multiset.card (roots (map i p)) + natDegree q = natDegree (map i p)
hr : roots q = 0
hq : q ≠ 0
h : ¬natDegree q = 0
h' : natDegree (map (RingHom.id L) q) ≠ 0
⊢ Multiset.prod (Multiset.map (fun a => X - ↑C a) (roots (map i p))) * q ≠ 0
case neg.intro.intro.intro.refine_1
F : Type u
K : Type v
L : Type w
inst✝² : CommRing K
inst✝¹ : Field L
inst✝ : Field F
i✝ : K →+* L
p : K[X]
i : K →+* L
q : L[X]
hp : ¬Multiset.prod (Multiset.map (fun a => X - ↑C a) (roots (map i p))) * q = 0
hsplit : Splits (RingHom.id L) (Multiset.prod (Multiset.map (fun a => X - ↑C a) (roots (map i p))) * q)
he : Multiset.prod (Multiset.map (fun a => X - ↑C a) (roots (map i p))) * q = map i p
hd : ↑Multiset.card (roots (map i p)) + natDegree q = natDegree (map i p)
hr : roots q = 0
hq : q ≠ 0
h : ¬natDegree q = 0
h' : natDegree (map (RingHom.id L) q) ≠ 0
⊢ map (RingHom.id L) (Multiset.prod (Multiset.map (fun a => X - ↑C a) (roots (map i p))) * q) ≠ 0
rw [map_id]
no goals
case neg.intro.intro.intro.refine_1
F : Type u
K : Type v
L : Type w
inst✝² : CommRing K
inst✝¹ : Field L
inst✝ : Field F
i✝ : K →+* L
p : K[X]
i : K →+* L
q : L[X]
hp : ¬Multiset.prod (Multiset.map (fun a => X - ↑C a) (roots (map i p))) * q = 0
hsplit : Splits (RingHom.id L) (Multiset.prod (Multiset.map (fun a => X - ↑C a) (roots (map i p))) * q)
he : Multiset.prod (Multiset.map (fun a => X - ↑C a) (roots (map i p))) * q = map i p
hd : ↑Multiset.card (roots (map i p)) + natDegree q = natDegree (map i p)
hr : roots q = 0
hq : q ≠ 0
h : ¬natDegree q = 0
h' : natDegree (map (RingHom.id L) q) ≠ 0
⊢ Multiset.prod (Multiset.map (fun a => X - ↑C a) (roots (map i p))) * q ≠ 0
exact mul_ne_zero monic_prod_multiset_X_sub_C.ne_zero hq