English
If x ∈ B is integral over A and y ∈ A is a root of minpoly_A x, then algebraMap A B y = x.
Русский
Если x ∈ B интегрирован над A и y ∈ A является корнем minpoly_A x, тогда algebraMap A B y = x.
LaTeX
$$minpoly.root hx hy := algebraMap A B y = x$$
Lean4
/-- If `L/K` is a field extension and an element `y` of `K` is a root of the minimal polynomial
of an element `x ∈ L`, then `y` maps to `x` under the field embedding. -/
theorem root {x : B} (hx : IsIntegral A x) {y : A} (h : IsRoot (minpoly A x) y) : algebraMap A B y = x :=
by
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))
have := aeval A x
rwa [key, map_sub, aeval_X, aeval_C, sub_eq_zero, eq_comm] at this
