English
Let A be a field, B an A-algebra, x ∈ B and a ∈ A. Then the minimal polynomial of x − algebraMap_A_B(a) over A equals (minpoly_A x) composed with the polynomial X + C a; i.e., minpoly_A(x − algebraMap_A_B(a)) = (minpoly_A x).comp (X + C a).
Русский
Пусть A — поле, B — A-алгебра, x ∈ B и a ∈ A. Тогда минимальный многочлен x − algebraMap_A_B(a) по отношению к A равен композиции minpoly_A(x) и полинома X + C a; то есть minpoly_A(x − algebraMap_A_B(a)) = (minpoly_A x).comp (X + C a).
LaTeX
$$$\minpoly_A(x - \mathrm{algebraMap}_A^B(a)) = (\minpoly_A x) \circ (X + C a)$$$
Lean4
theorem sub_algebraMap {B : Type*} [CommRing B] [Algebra A B] (x : B) (a : A) :
minpoly A (x - algebraMap A B a) = (minpoly A x).comp (X + C a) := by
simpa [sub_eq_add_neg] using add_algebraMap x (-a)
