A : Type u_1
B : Type u_2
inst✝³ : Field A
inst✝² : Ring B
inst✝¹ : IsDomain B
inst✝ : Algebra A B
x✝ x : B
hx : IsIntegral A x
y : A
h : IsRoot (minpoly A x) y
key : minpoly A x = X - ↑C y
⊢ ↑(algebraMap A B) y = x
A : Type u_1
B : Type u_2
inst✝³ : Field A
inst✝² : Ring B
inst✝¹ : IsDomain B
inst✝ : Algebra A B
x✝ x : B
hx : IsIntegral A x
y : A
h : IsRoot (minpoly A x) y
⊢ ↑(algebraMap A B) y = x
have key : minpoly A x = X - C y := eq_of_monic_of_associated (monic hx) (monic_X_sub_C y)
  (associated_of_dvd_dvd ((irreducible_X_sub_C y).dvd_symm (irreducible hx) (dvd_iff_isRoot.2 h))
    (dvd_iff_isRoot.2 h))
A : Type u_1
B : Type u_2
inst✝³ : Field A
inst✝² : Ring B
inst✝¹ : IsDomain B
inst✝ : Algebra A B
x✝ x : B
hx : IsIntegral A x
y : A
h : IsRoot (minpoly A x) y
key : minpoly A x = X - ↑C y
this : ↑(Polynomial.aeval x) (minpoly A x) = 0
⊢ ↑(algebraMap A B) y = x
A : Type u_1
B : Type u_2
inst✝³ : Field A
inst✝² : Ring B
inst✝¹ : IsDomain B
inst✝ : Algebra A B
x✝ x : B
hx : IsIntegral A x
y : A
h : IsRoot (minpoly A x) y
key : minpoly A x = X - ↑C y
⊢ ↑(algebraMap A B) y = x
have := aeval A x
no goals
A : Type u_1
B : Type u_2
inst✝³ : Field A
inst✝² : Ring B
inst✝¹ : IsDomain B
inst✝ : Algebra A B
x✝ x : B
hx : IsIntegral A x
y : A
h : IsRoot (minpoly A x) y
key : minpoly A x = X - ↑C y
this : ↑(Polynomial.aeval x) (minpoly A x) = 0
⊢ ↑(algebraMap A B) y = x
rwa [key, AlgHom.map_sub, aeval_X, aeval_C, sub_eq_zero, eq_comm] at this