frobenius_of_isSeparable — Mathlib

English

A separable extension keeps a basis after q-powering; preserves properties.

Русский

Разделяемое расширение сохраняет базис после q-возведения; сохраняются свойства.

LaTeX

$$$\text{Basis} \mapsto \text{Basis}$ under power$$

Lean4

/-- For an extension `E / F` of exponential characteristic `q` and a separable element `a : E`, the
minimal polynomial of `a ^ q` equals the minimal polynomial of `a` mapped via `(⬝ ^ q)`. -/
theorem frobenius_of_isSeparable [ExpChar E q] {a : E} (hsep : IsSeparable F a) :
    minpoly F (frobenius E q a) = (minpoly F a).map (frobenius F q) := by
  simpa using minpoly.iterateFrobenius_of_isSeparable q 1 hsep

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