Theorems · Theorem · linear algebra

Module.End.exists_isNilpotent_isSemisimple_of_separable_of_dvd_pow

∀ {K : Type u_1} {V : Type u_2} [inst : Field K] [inst_1 : AddCommGroup V] [inst_2 : Module K V] {f : Module.End K V}
  {P : Polynomial K} {k : ℕ},
  P.Separable → minpoly K f ∣ P ^ k → ∃ n ∈ K[f], ∃ s ∈ K[f], IsNilpotent n ∧ s.IsSemisimple ∧ f = n + s

Defined in

Mathlib.LinearAlgebra.JordanChevalley

Cited by

1 results in Mathlib

Foundations

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

Assumes

FieldAddCommGroupModule