minpoly_eq — Mathlib

English

For a ∈ L, minpoly K a = X^{p^{e}} − C(y) where e = elemExponent K a and y = elemReduct K a.

Русский

Для a ∈ L минимальный многочлен равен minpoly K a = X^{p^{e}} − C(y), где e = elemExponent K a и y = elemReduct K a.

LaTeX

$$minpoly K a = X^{ringExpChar K^{elemExponent K a}} - C (elemReduct K a)$$

Lean4

theorem minpoly_eq (a : L) : minpoly K a = X ^ ringExpChar K ^ elemExponent K a - C (elemReduct K a) :=
  Classical.choose_spec <| Nat.find_spec <| minpoly_eq_X_pow_sub_C K (ringExpChar K) a

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