English
Let A be a nontrivial commutative ring, B an A-algebra, and x ∈ B integral over A. Then the minimal polynomial of x over A has positive degree, i.e., its natDegree is strictly greater than 0.
Русский
Пусть A — ненулевое коммутативное кольцо, B — A-алгебра, и x ∈ B интегрален над A. Тогда минимальный полином x над A имеет положительную степень, т.е. natDegree(minpoly A x) > 0.
LaTeX
$$$0 < \operatorname{natDegree}(\minpoly A x)$$$
Lean4
/-- The degree of a minimal polynomial, as a natural number, is positive. -/
theorem natDegree_pos [Nontrivial B] (hx : IsIntegral A x) : 0 < natDegree (minpoly A x) :=
by
rw [pos_iff_ne_zero]
intro ndeg_eq_zero
have eq_one : minpoly A x = 1 := by
rw [eq_C_of_natDegree_eq_zero ndeg_eq_zero]
convert C_1 (R := A)
simpa only [ndeg_eq_zero.symm] using (monic hx).leadingCoeff
simpa only [eq_one, map_one, one_ne_zero] using aeval A x
