Theorems · Theorem · linear algebra

Module.End.isNilpotent_isSemisimple_unique

∀ {K : Type u_1} {V : Type u_2} [inst : Field K] [inst_1 : AddCommGroup V] [inst_2 : Module K V] [FiniteDimensional K V]
  [PerfectField K] {n₁ s₁ n₂ s₂ : Module.End K V},
  IsNilpotent n₁ →
    s₁.IsSemisimple →
      IsNilpotent n₂ → s₂.IsSemisimple → Commute n₁ s₁ → Commute n₂ s₂ → n₁ + s₁ = n₂ + s₂ → n₁ = n₂ ∧ s₁ = s₂

Uniqueness of Jordan-Chevalley-Dunford decomposition: if n₁ + s₁ = n₂ + s₂ with nᵢ nilpotent, sᵢ semisimple, and nᵢ, sᵢ commuting, then n₁ = n₂ and s₁ = s₂.

Defined in

Mathlib.LinearAlgebra.JordanChevalley

Cited by

1 results in Mathlib

Foundations

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

Assumes

FieldAddCommGroupModuleFiniteDimensionalPerfectField