Theorems · Theorem · field theory

minpoly_algEquiv_toLinearMap

∀ {K : Type u_1} {L : Type u_2} [inst : Field K] [inst_1 : CommRing L] [IsDomain L] [inst_3 : Algebra K L]
  (σ : L ≃ₐ[K] L), IsOfFinOrder σ → minpoly K σ.toLinearMap = Polynomial.X ^ orderOf σ - Polynomial.C 1

The minimal polynomial (over K) of σ : L ≃ₐ[K] L is X ^ (orderOf σ) - 1.

Defined in

Mathlib.FieldTheory.Minpoly.Field

Cited by

2 results in Mathlib

Foundations

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

Assumes

FieldCommRingIsDomainAlgebra