F : Type u
K : Type v
L : Type w
inst✝⁴ : Field K
inst✝³ : Field L
inst✝² : Field F
inst✝¹ : Algebra K L
f : K[X]
inst✝ : IsSplittingField K L f
y : L
hy : y ∈ ↑(Multiset.toFinset 0)
hf : f = 0
⊢ IsIntegral K y
F : Type u
K : Type v
L : Type w
inst✝⁴ : Field K
inst✝³ : Field L
inst✝² : Field F
inst✝¹ : Algebra K L
f : K[X]
inst✝ : IsSplittingField K L f
y : L
hy : y ∈ ↑(Multiset.toFinset (roots (Polynomial.map (algebraMap K L) f)))
hf : f = 0
⊢ IsIntegral K y
rw [hf, Polynomial.map_zero, roots_zero] at hy
no goals
F : Type u
K : Type v
L : Type w
inst✝⁴ : Field K
inst✝³ : Field L
inst✝² : Field F
inst✝¹ : Algebra K L
f : K[X]
inst✝ : IsSplittingField K L f
y : L
hy : y ∈ ↑(Multiset.toFinset 0)
hf : f = 0
⊢ IsIntegral K y
cases hy