minpoly_eq' — Mathlib

English

A variant of the minpoly formula: minpoly K a = X^{p^{elemExponent K a}} − C (elemReduct K a).

Русский

Вариант формулы для минполино: minpoly K a = X^{p^{elemExponent K a}} − C (elemReduct K a).

LaTeX

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

Lean4

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

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