English
Let A, K be rings with A a commutative ring, K a field, and R a ring equipped with compatible A-algebra structures so that A → K → R forms a scalar tower. For any element x ∈ R, the minimal polynomial of x over K divides the polynomial obtained by mapping the minimal polynomial of x over A along the inclusion A → K. Symbolically, minpoly_K(x) ∣ (minpoly_A(x)).map(algebraMap A K).
Русский
Пусть A, K — кольца/поля, причём A — кольцо, K — поле; R — кольцо с соответствующими A-алгебрическими структурами так, что образуется скалярная башня A → K → R. Для любого x ∈ R минимальный многочлен x над K делится полином, полученным из минимального многочлена x над A путём отображения алгебраMap A K. Обозначим через map алгебраMap A K: minpoly_K(x) делится на (minpoly_A(x)).map(algebraMap A K).
LaTeX
$$$\\minpoly K x \\mid \\operatorname{map}(\\mathrm{algebraMap} A K)\\bigl(\\minpoly A x\\bigr)$$$
Lean4
theorem dvd_map_of_isScalarTower (A K : Type*) {R : Type*} [CommRing A] [Field K] [Ring R] [Algebra A K] [Algebra A R]
[Algebra K R] [IsScalarTower A K R] (x : R) : minpoly K x ∣ (minpoly A x).map (algebraMap A K) :=
by
refine minpoly.dvd K x ?_
rw [aeval_map_algebraMap, minpoly.aeval]
