minpoly_natDegree_eq' — Mathlib

English

Variant: natDegree(minpoly K a) = ringExpChar K ^ elemExponent K a.

Русский

Вариант: natDegree(minpoly K a) = ringExpChar K ^ elemExponent K a.

LaTeX

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

Lean4

/-- Version of `minpoly_natDegree_eq` using `ExpChar`. -/
theorem minpoly_natDegree_eq' (p : ℕ) [ExpChar K p] (a : L) : (minpoly K a).natDegree = p ^ elemExponent K a :=
  ringExpChar.eq K p ▸ minpoly_natDegree_eq K a

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