natDegree_minpolyDiv — Mathlib

English

If x is integral over R, then natDegree(minpolyDiv R x) equals natDegree(minpoly R x) minus 1.

Русский

Если x интеграл над R, то deg(minpolyDiv R x) = deg(minpoly R x) − 1.

LaTeX

$$$\operatorname{natDegree}(\minpoly\,Div\,R\ x) = \operatorname{natDegree}(\minpoly\ R\ x) - 1$$$

Lean4

theorem natDegree_minpolyDiv : natDegree (minpolyDiv R x) = natDegree (minpoly R x) - 1 :=
  by
  nontriviality S
  by_cases hx : IsIntegral R x
  · rw [← natDegree_minpolyDiv_succ hx]; rfl
  · rw [minpolyDiv_eq_zero hx, minpoly.eq_zero hx]; rfl

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