English
For any x in a ring B that is an algebra over A, minpoly A (−x) equals (−1)^(natDegree(minpoly A x)) times the composition (minpoly A x) ∘ (−X).
Русский
Для любого x в кольце B, являющемся алгеброй над A, minpoly_A(−x) равно (-1)^{natDegree(minpoly_A x)} умноженному на (minpoly_A x) ∘ (−X).
LaTeX
$$$\minpoly_A(-x) = (-1)^{\operatorname{natDegree}(\minpoly_A x)} \cdot (\minpoly_A x) \circ (-X)$$$
Lean4
/-- If `B/K` is a nontrivial algebra over a field, and `x` is an element of `K`,
then the minimal polynomial of `algebraMap K B x` is `X - C x`. -/
theorem eq_X_sub_C (a : A) : minpoly A (algebraMap A B a) = X - C a :=
eq_X_sub_C_of_algebraMap_inj a (algebraMap A B).injective
