English
If deg(minpoly_A(x)) = 1, then x lies in the range of algebraMap A B.
Русский
Если deg(minpoly_A(x)) = 1, то x принадлежит образу algebraMap A B.
LaTeX
$$$\\deg(\\minpoly_A(x)) = 1 \\Rightarrow x \\in \\mathrm{range}(\\text{algebraMap}_{A \\to B}).$$$
Lean4
/-- The defining property of the minimal polynomial of an element `x`:
it is the monic polynomial with smallest degree that has `x` as its root. -/
theorem min {p : A[X]} (pmonic : p.Monic) (hp : Polynomial.aeval x p = 0) : degree (minpoly A x) ≤ degree p :=
by
delta minpoly; split_ifs with hx
· exact le_of_not_gt (degree_lt_wf.not_lt_min _ hx ⟨pmonic, hp⟩)
· simp only [degree_zero, bot_le]
