natDegree_minpolyDiv_lt — Mathlib

English

Let x be integral over R in a nontrivial S-algebra; then the degree of the divisor-minpoly of x over R is strictly smaller than the degree of the minimal polynomial of x over R.

Русский

Пусть x элемент, целочисленный над R в негодной S-алгебре; тогда deg(minpolyDiv R x) строго меньше deg(minpoly R x).

LaTeX

$$$\operatorname{natDegree}(\minpoly\_D R\ x) < \operatorname{natDegree}(\minpoly\ R\ x)$$$

Lean4

theorem natDegree_minpolyDiv_lt [Nontrivial S] : natDegree (minpolyDiv R x) < natDegree (minpoly R x) :=
  by
  rw [← natDegree_minpolyDiv_succ hx]
  exact Nat.lt_succ_self _

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