F : Type u
K : Type v
L : Type w
inst✝⁴ : Field K
inst✝³ : Field L
inst✝² : Field F
i : K →+* L
R : Type u_1
inst✝¹ : CommRing R
inst✝ : Algebra R K
f : K[X]
hs : Splits (RingHom.id K) f
hm : Monic f
hr : ∀ (a : K), a ∈ roots f → a ∈ RingHom.range (algebraMap R K)
⊢ Multiset.prod (Multiset.map (fun a => X - ↑C a) (roots f)) ∈ liftsRing (algebraMap R K)
F : Type u
K : Type v
L : Type w
inst✝⁴ : Field K
inst✝³ : Field L
inst✝² : Field F
i : K →+* L
R : Type u_1
inst✝¹ : CommRing R
inst✝ : Algebra R K
f : K[X]
hs : Splits (RingHom.id K) f
hm : Monic f
hr : ∀ (a : K), a ∈ roots f → a ∈ RingHom.range (algebraMap R K)
⊢ f ∈ lifts (algebraMap R K)
rw [eq_prod_roots_of_monic_of_splits_id hm hs, lifts_iff_liftsRing]
F : Type u
K : Type v
L : Type w
inst✝⁴ : Field K
inst✝³ : Field L
inst✝² : Field F
i : K →+* L
R : Type u_1
inst✝¹ : CommRing R
inst✝ : Algebra R K
f : K[X]
hs : Splits (RingHom.id K) f
hm : Monic f
hr : ∀ (a : K), a ∈ roots f → a ∈ RingHom.range (algebraMap R K)
P : K[X]
hP : P ∈ Multiset.map (fun a => X - ↑C a) (roots f)
⊢ P ∈ liftsRing (algebraMap R K)
F : Type u
K : Type v
L : Type w
inst✝⁴ : Field K
inst✝³ : Field L
inst✝² : Field F
i : K →+* L
R : Type u_1
inst✝¹ : CommRing R
inst✝ : Algebra R K
f : K[X]
hs : Splits (RingHom.id K) f
hm : Monic f
hr : ∀ (a : K), a ∈ roots f → a ∈ RingHom.range (algebraMap R K)
⊢ Multiset.prod (Multiset.map (fun a => X - ↑C a) (roots f)) ∈ liftsRing (algebraMap R K)
refine' Subring.multiset_prod_mem _ _ fun P hP => _
case intro.intro
F : Type u
K : Type v
L : Type w
inst✝⁴ : Field K
inst✝³ : Field L
inst✝² : Field F
i : K →+* L
R : Type u_1
inst✝¹ : CommRing R
inst✝ : Algebra R K
f : K[X]
hs : Splits (RingHom.id K) f
hm : Monic f
hr : ∀ (a : K), a ∈ roots f → a ∈ RingHom.range (algebraMap R K)
b : K
hb : b ∈ roots f
hP : X - ↑C b ∈ Multiset.map (fun a => X - ↑C a) (roots f)
⊢ X - ↑C b ∈ liftsRing (algebraMap R K)
F : Type u
K : Type v
L : Type w
inst✝⁴ : Field K
inst✝³ : Field L
inst✝² : Field F
i : K →+* L
R : Type u_1
inst✝¹ : CommRing R
inst✝ : Algebra R K
f : K[X]
hs : Splits (RingHom.id K) f
hm : Monic f
hr : ∀ (a : K), a ∈ roots f → a ∈ RingHom.range (algebraMap R K)
P : K[X]
hP : P ∈ Multiset.map (fun a => X - ↑C a) (roots f)
⊢ P ∈ liftsRing (algebraMap R K)
obtain ⟨b, hb, rfl⟩ := Multiset.mem_map.1 hP
no goals
case intro.intro
F : Type u
K : Type v
L : Type w
inst✝⁴ : Field K
inst✝³ : Field L
inst✝² : Field F
i : K →+* L
R : Type u_1
inst✝¹ : CommRing R
inst✝ : Algebra R K
f : K[X]
hs : Splits (RingHom.id K) f
hm : Monic f
hr : ∀ (a : K), a ∈ roots f → a ∈ RingHom.range (algebraMap R K)
b : K
hb : b ∈ roots f
hP : X - ↑C b ∈ Multiset.map (fun a => X - ↑C a) (roots f)
⊢ X - ↑C b ∈ liftsRing (algebraMap R K)
exact Subring.sub_mem _ (X_mem_lifts _) (C'_mem_lifts (hr _ hb))