∀ {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