A✝ : Type ?u.54450
B : Type ?u.54453
inst✝⁹ : Field A✝
inst✝⁸ : Ring B
inst✝⁷ : Algebra A✝ B
x✝ : B
A : Type u_1
K : Type u_2
R : Type u_3
inst✝⁶ : CommRing A
inst✝⁵ : Field K
inst✝⁴ : CommRing R
inst✝³ : Algebra A K
inst✝² : Algebra A R
inst✝¹ : Algebra K R
inst✝ : IsScalarTower A K R
x : R
⊢ ↑(Polynomial.aeval x) (map (algebraMap A K) (minpoly A x)) = 0
A✝ : Type ?u.54450
B : Type ?u.54453
inst✝⁹ : Field A✝
inst✝⁸ : Ring B
inst✝⁷ : Algebra A✝ B
x✝ : B
A : Type u_1
K : Type u_2
R : Type u_3
inst✝⁶ : CommRing A
inst✝⁵ : Field K
inst✝⁴ : CommRing R
inst✝³ : Algebra A K
inst✝² : Algebra A R
inst✝¹ : Algebra K R
inst✝ : IsScalarTower A K R
x : R
⊢ minpoly K x ∣ map (algebraMap A K) (minpoly A x)
refine' minpoly.dvd K x _
no goals
A✝ : Type ?u.54450
B : Type ?u.54453
inst✝⁹ : Field A✝
inst✝⁸ : Ring B
inst✝⁷ : Algebra A✝ B
x✝ : B
A : Type u_1
K : Type u_2
R : Type u_3
inst✝⁶ : CommRing A
inst✝⁵ : Field K
inst✝⁴ : CommRing R
inst✝³ : Algebra A K
inst✝² : Algebra A R
inst✝¹ : Algebra K R
inst✝ : IsScalarTower A K R
x : R
⊢ ↑(Polynomial.aeval x) (map (algebraMap A K) (minpoly A x)) = 0
rw [aeval_map_algebraMap, minpoly.aeval]