`BookProof.ChapterSchurIrreducible.isIrreducible_iff_schur` (M : System ℂ V) (hM : M.IsNormal) : M.IsIrreducible ↔ ∀ S : V →L[ℂ] V, M.Commutes S → IsSelfAdjoint S → ∃ c : ℂ, S = c

Initializing...

`BookProof.ChapterSchurIrreducible.isIrreducible_iff_schur` (M : System ℂ V) (hM : M.IsNormal) : M.IsIrreducible ↔ ∀ S : V →L[ℂ] V, M.Commutes S → IsSelfAdjoint S → ∃ c : ℂ, S = c · Prove2Me