def JordanForm.IsNilpotentOperator {R : Type u_1} {M : Type u_2} [Ring R] [AddCommGroup M] [Module R M] (T : Module.End R M) : Prop

def JordanForm.jordanBlock {F : Type u_1} [Field F] (a : ℕ) (μ : F) : Matrix (Fin a) (Fin a) F

def JordanForm.jordanNormalForm {F : Type u_1} [Field F] {r : ℕ} [DecidableEq (Fin r)] (blockSize : Fin r → ℕ) (μ : Fin r → F) : Matrix ((i : Fin r) × Fin (blockSize i)) ((i : Fin r) × Fin (blockSize i)) F

noncomputable def JordanForm.jordanMatrix {F : Type u_1} [Field F] {r : ℕ} [DecidableEq (Fin r)] (blockSize : Fin r → ℕ) (μ : Fin r → F) {n : ℕ} (hsum : ∑ i : Fin r, blockSize i = n) : Matrix (Fin n) (Fin n) F

theorem JordanForm.jordan_decomposition_matrix {F : Type u_1} [Field F] [IsAlgClosed F] [DecidableEq F] {n : ℕ} (M : Matrix (Fin n) (Fin n) F) : ∃ (r : ℕ) (blockSize : Fin r → ℕ) (hsum : ∑ i : Fin r, blockSize i = n) (μ : Fin r → F) (P : Matrix (Fin n) (Fin n) F), IsUnit P ∧ P⁻¹ * M * P = jordanMatrix blockSize μ hsum