Theorems · Theorem · field theory

minpoly.iterateFrobenius_of_isSeparable

∀ {F : Type u} {E : Type v} [inst : Field F] [inst_1 : Field E] [inst_2 : Algebra F E] (q : ℕ) [hF : ExpChar F q]
  [inst_3 : ExpChar E q] (n : ℕ) {a : E},
  IsSeparable F a → minpoly F ((iterateFrobenius E q n) a) = Polynomial.map (iterateFrobenius F q n) (minpoly F a)

For an extension E / F of exponential characteristic q and a separable element a : E, the minimal polynomial of a ^ q ^ n equals the minimal polynomial of a mapped via (⬝ ^ q ^ n).

Defined in

Mathlib.FieldTheory.PurelyInseparable.PerfectClosure

Cited by

1 results in Mathlib

Foundations

Depth 198 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

FieldFieldAlgebraExpCharExpChar