English
Let R, K, T, U be rings with R ↪ K ↪ T and R ↪ U, K ↪ U forming scalar towers, and x ∈ T, y ∈ U with hy: aeval_y(minpoly_K(x)) = 0. Then aeval_y(minpoly_R(x)) = 0. In words, if y is a root of the minimal polynomial of x over K, then it is a root of the minimal polynomial of x over R.
Русский
Пусть R, K, T, U образуют скалярные башни R → K → T и R → U, а также x ∈ T, y ∈ U с условием hy: aeval_y(minpoly_K(x)) = 0. Тогда aeval_y(minpoly_R(x)) = 0. Иными словами, если y является корнем минимального многочлена x над K, то он является корнем минимального многочлена x над R.
LaTeX
$$$\\text{aeval}_y(\\minpoly R x) = 0$ при условии $\\text{aeval}_y(\\minpoly K x) = 0$$$
Lean4
/-- If `y` is a conjugate of `x` over a field `K`, then it is a conjugate over a subring `R`. -/
theorem aeval_of_isScalarTower (R : Type*) {K T U : Type*} [CommRing R] [Field K] [CommRing T] [Algebra R K]
[Algebra K T] [Algebra R T] [IsScalarTower R K T] [CommSemiring U] [Algebra K U] [Algebra R U] [IsScalarTower R K U]
(x : T) (y : U) (hy : Polynomial.aeval y (minpoly K x) = 0) : Polynomial.aeval y (minpoly R x) = 0 :=
aeval_map_algebraMap K y (minpoly R x) ▸
eval₂_eq_zero_of_dvd_of_eval₂_eq_zero (algebraMap K U) y (minpoly.dvd_map_of_isScalarTower R K x) hy
