case pos
K : Type u_2
L : Type u_1
L' : Type ?u.315453
inst✝⁴ : Field K
inst✝³ : Field L
inst✝² : Field L'
inst✝¹ : Algebra K L
inst✝ : Algebra K L'
S : IntermediateField K L
x : { x // x ∈ S }
hx : IsIntegral K x
⊢ minpoly K x = minpoly K ↑x

case neg
K : Type u_2
L : Type u_1
L' : Type ?u.315453
inst✝⁴ : Field K
inst✝³ : Field L
inst✝² : Field L'
inst✝¹ : Algebra K L
inst✝ : Algebra K L'
S : IntermediateField K L
x : { x // x ∈ S }
hx : ¬IsIntegral K x
⊢ minpoly K x = minpoly K ↑x
K : Type u_2
L : Type u_1
L' : Type ?u.315453
inst✝⁴ : Field K
inst✝³ : Field L
inst✝² : Field L'
inst✝¹ : Algebra K L
inst✝ : Algebra K L'
S : IntermediateField K L
x : { x // x ∈ S }
⊢ minpoly K x = minpoly K ↑x
by_cases hx : IsIntegral K x
no goals
case pos
K : Type u_2
L : Type u_1
L' : Type ?u.315453
inst✝⁴ : Field K
inst✝³ : Field L
inst✝² : Field L'
inst✝¹ : Algebra K L
inst✝ : Algebra K L'
S : IntermediateField K L
x : { x // x ∈ S }
hx : IsIntegral K x
⊢ minpoly K x = minpoly K ↑x
exact minpoly.eq_of_algebraMap_eq (algebraMap S L).injective hx rfl
no goals
case neg
K : Type u_2
L : Type u_1
L' : Type ?u.315453
inst✝⁴ : Field K
inst✝³ : Field L
inst✝² : Field L'
inst✝¹ : Algebra K L
inst✝ : Algebra K L'
S : IntermediateField K L
x : { x // x ∈ S }
hx : ¬IsIntegral K x
⊢ minpoly K x = minpoly K ↑x
exact (minpoly.eq_zero hx).trans (minpoly.eq_zero (mt isIntegral_iff.mpr hx)).symm