no goals
K : Type ?u.261453
L : Type ?u.261456
R : Type u_1
S : Type u_2
A : Type u_3
inst✝¹² : Field K
inst✝¹¹ : Field L
inst✝¹⁰ : CommRing R
inst✝⁹ : CommRing S
inst✝⁸ : CommRing A
inst✝⁷ : Algebra K L
inst✝⁶ : Algebra L A
inst✝⁵ : Algebra K A
inst✝⁴ : IsScalarTower K L A
inst✝³ : Algebra R S
inst✝² : Algebra S A
inst✝¹ : Algebra R A
inst✝ : IsScalarTower R S A
hinj : Function.Injective ↑(algebraMap R S)
x : A
A_alg : _root_.IsAlgebraic R x
p : R[X]
hp₁ : p ≠ 0
hp₂ : ↑(aeval x) p = 0
⊢ map (algebraMap R S) p ≠ 0
rwa [Ne.def, ← degree_eq_bot, degree_map_eq_of_injective hinj, degree_eq_bot]
no goals
K : Type ?u.261453
L : Type ?u.261456
R : Type u_1
S : Type u_2
A : Type u_3
inst✝¹² : Field K
inst✝¹¹ : Field L
inst✝¹⁰ : CommRing R
inst✝⁹ : CommRing S
inst✝⁸ : CommRing A
inst✝⁷ : Algebra K L
inst✝⁶ : Algebra L A
inst✝⁵ : Algebra K A
inst✝⁴ : IsScalarTower K L A
inst✝³ : Algebra R S
inst✝² : Algebra S A
inst✝¹ : Algebra R A
inst✝ : IsScalarTower R S A
hinj : Function.Injective ↑(algebraMap R S)
x : A
A_alg : _root_.IsAlgebraic R x
p : R[X]
hp₁ : p ≠ 0
hp₂ : ↑(aeval x) p = 0
⊢ ↑(aeval x) (map (algebraMap R S) p) = 0
simpa