degree_pos — Mathlib

English

Let A be a commutative ring, B a nontrivial A-algebra, and x ∈ B integral over A. Then the degree of minpoly A x is positive.

Русский

Пусть A — коммутативное кольцо, B — ненуливая A-алгебра, и x ∈ B интегрирован над A. Тогда deg(minpoly A x) > 0.

LaTeX

$$$0 < \operatorname{degree}(\minpoly A x)$$$

Lean4

/-- The degree of a minimal polynomial is positive. -/
theorem degree_pos [Nontrivial B] (hx : IsIntegral A x) : 0 < degree (minpoly A x) :=
  natDegree_pos_iff_degree_pos.mp (natDegree_pos hx)

Похожие утверждения