case a
k✝ : Type u
inst✝³ : Field k✝
k : Type u_1
K : Type u_2
inst✝² : Field k
inst✝¹ : IsAlgClosed k
inst✝ : Field K
f : K →+* k
p : K[X]
⊢ Splits f p ↔ Splits (RingHom.id k) (map f p)
k✝ : Type u
inst✝³ : Field k✝
k : Type u_1
K : Type u_2
inst✝² : Field k
inst✝¹ : IsAlgClosed k
inst✝ : Field K
f : K →+* k
p : K[X]
⊢ Splits f p
convert IsAlgClosed.splits (p.map f)
no goals
case a
k✝ : Type u
inst✝³ : Field k✝
k : Type u_1
K : Type u_2
inst✝² : Field k
inst✝¹ : IsAlgClosed k
inst✝ : Field K
f : K →+* k
p : K[X]
⊢ Splits f p ↔ Splits (RingHom.id k) (map f p)
simp [splits_map_iff]