elemExponent — Mathlib

English

For any a ∈ L, the natDegree of the minimal polynomial minpoly K a equals ringExpChar K to the power elemExponent K a; i.e., natDegree(minpoly K a) = ringExpChar K ^ elemExponent K a.

Русский

Для любого a ∈ L степень натуральна минимального многочлена minpoly K a равна ringExpChar K в степени elemExponent K a; то есть natDegree(minpoly K a) = ringExpChar K ^ elemExponent K a.

LaTeX

$$(minpoly\;K\;a).natDegree = \operatorname{ringExpChar} K^{\operatorname{elemExponent} K a}$$

Lean4

/-- The exponent of an element `a ∈ L` of a purely inseparable field extension `L / K`
is the smallest natural number `e` such that `a ^ ringExpChar K ^ e ∈ K`. -/
noncomputable def elemExponent (a : L) : ℕ :=
  Nat.find <| minpoly_eq_X_pow_sub_C K (ringExpChar K) a

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