A : Type ?u.57254
B : Type ?u.57257
inst✝¹³ : Field A
inst✝¹² : Ring B
inst✝¹¹ : Algebra A B
x : B
R : Type u_1
S : Type u_2
K : Type u_3
L : Type u_4
inst✝¹⁰ : CommRing R
inst✝⁹ : CommRing S
inst✝⁸ : Field K
inst✝⁷ : CommRing L
inst✝⁶ : Algebra R S
inst✝⁵ : Algebra R K
inst✝⁴ : Algebra S L
inst✝³ : Algebra K L
inst✝² : Algebra R L
inst✝¹ : IsScalarTower R K L
inst✝ : IsScalarTower R S L
s : S
⊢ ↑(Polynomial.aeval (↑(algebraMap S L) s)) (map (algebraMap R K) (minpoly R s)) = 0
A : Type ?u.57254
B : Type ?u.57257
inst✝¹³ : Field A
inst✝¹² : Ring B
inst✝¹¹ : Algebra A B
x : B
R : Type u_1
S : Type u_2
K : Type u_3
L : Type u_4
inst✝¹⁰ : CommRing R
inst✝⁹ : CommRing S
inst✝⁸ : Field K
inst✝⁷ : CommRing L
inst✝⁶ : Algebra R S
inst✝⁵ : Algebra R K
inst✝⁴ : Algebra S L
inst✝³ : Algebra K L
inst✝² : Algebra R L
inst✝¹ : IsScalarTower R K L
inst✝ : IsScalarTower R S L
s : S
⊢ minpoly K (↑(algebraMap S L) s) ∣ map (algebraMap R K) (minpoly R s)
apply minpoly.dvd K (algebraMap S L s)
case h
A : Type ?u.57254
B : Type ?u.57257
inst✝¹³ : Field A
inst✝¹² : Ring B
inst✝¹¹ : Algebra A B
x : B
R : Type u_1
S : Type u_2
K : Type u_3
L : Type u_4
inst✝¹⁰ : CommRing R
inst✝⁹ : CommRing S
inst✝⁸ : Field K
inst✝⁷ : CommRing L
inst✝⁶ : Algebra R S
inst✝⁵ : Algebra R K
inst✝⁴ : Algebra S L
inst✝³ : Algebra K L
inst✝² : Algebra R L
inst✝¹ : IsScalarTower R K L
inst✝ : IsScalarTower R S L
s : S
⊢ RingHom.comp (algebraMap K ((fun x => L) s)) (algebraMap R K) = RingHom.comp (algebraMap S L) (algebraMap R S)
A : Type ?u.57254
B : Type ?u.57257
inst✝¹³ : Field A
inst✝¹² : Ring B
inst✝¹¹ : Algebra A B
x : B
R : Type u_1
S : Type u_2
K : Type u_3
L : Type u_4
inst✝¹⁰ : CommRing R
inst✝⁹ : CommRing S
inst✝⁸ : Field K
inst✝⁷ : CommRing L
inst✝⁶ : Algebra R S
inst✝⁵ : Algebra R K
inst✝⁴ : Algebra S L
inst✝³ : Algebra K L
inst✝² : Algebra R L
inst✝¹ : IsScalarTower R K L
inst✝ : IsScalarTower R S L
s : S
⊢ ↑(Polynomial.aeval (↑(algebraMap S L) s)) (map (algebraMap R K) (minpoly R s)) = 0
rw [← map_aeval_eq_aeval_map, minpoly.aeval, map_zero]
no goals
case h
A : Type ?u.57254
B : Type ?u.57257
inst✝¹³ : Field A
inst✝¹² : Ring B
inst✝¹¹ : Algebra A B
x : B
R : Type u_1
S : Type u_2
K : Type u_3
L : Type u_4
inst✝¹⁰ : CommRing R
inst✝⁹ : CommRing S
inst✝⁸ : Field K
inst✝⁷ : CommRing L
inst✝⁶ : Algebra R S
inst✝⁵ : Algebra R K
inst✝⁴ : Algebra S L
inst✝³ : Algebra K L
inst✝² : Algebra R L
inst✝¹ : IsScalarTower R K L
inst✝ : IsScalarTower R S L
s : S
⊢ RingHom.comp (algebraMap K ((fun x => L) s)) (algebraMap R K) = RingHom.comp (algebraMap S L) (algebraMap R S)
rw [← IsScalarTower.algebraMap_eq, ← IsScalarTower.algebraMap_eq]