natDegree_le — Mathlib

English

For x ∈ L, if L is finite dimensional over K, then the natural degree of minpoly K x is at most the finite dimension [K L].

Русский

Для x ∈ L, если L конечно над K, то natDegree(minpoly K x) ≤ [K L].

LaTeX

$$$\operatorname{natDegree}(\minpoly K x) \le \operatorname{finrank}_K L$$$

Lean4

theorem _root_.minpoly.natDegree_le (x : L) [FiniteDimensional K L] : (minpoly K x).natDegree ≤ finrank K L :=
  le_of_eq_of_le (IntermediateField.adjoin.finrank (.of_finite _ _)).symm K⟮x⟯.toSubmodule.finrank_le

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