Theorems · Theorem · linear algebra

Module.End.IsFinitelySemisimple.iSup_maxGenEigenspace_eq_top_iff

∀ {R : Type u_1} {M : Type u_2} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  {f : Module.End R M}, f.IsFinitelySemisimple → (⨆ μ, f.maxGenEigenspace μ = ⊤ ↔ ⨆ μ, f.eigenspace μ = ⊤)

A finitely-semisimple endomorphism is triangularizable if and only if it is diagonalizable.

Defined in: Mathlib.LinearAlgebra.Eigenspace.Semisimple
Cited by: 1 results in Mathlib
Foundations: Depth 137 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes: CommRing AddCommGroup Module

Mathlib docs Source Loogle LeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

Cites11

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

Modulestatement and proof · cited by 20,661
CommRingstatement and proof · cited by 17,173
AddCommGroupstatement and proof · cited by 12,871
Top.topstatement and proof · cited by 9,680
Submodulestatement · cited by 7,192
iSupstatement and proof · cited by 2,415
Module.Endstatement and proof · cited by 774
Module.End.eigenspacestatement and proof · cited by 56
Module.End.maxGenEigenspacestatement · cited by 41
Module.End.IsFinitelySemisimplestatement and proof · cited by 12
Module.End.IsFinitelySemisimple.maxGenEigenspace_eq_eigenspaceproof · cited by 4

Cited by1

Results whose statement or proof uses this declaration.

Module.End.IsSemisimple.iSup_maxGenEigenspace_eq_top_iffproof · cited by 0