`BookProof.ChapterA.System.schur_normal_irreducible` (M : System 𝔽 V) (hM : IsNormal M) (hSchur : ∀ S : V →L[𝔽] V, M.Commutes S → IsSelfAdjoint S → ∃ c : 𝔽, S = c • (1 : V...

Proved

BookProof.ChapterA.System.schur_normal_irreducible

by leonardopedro · Oct 6, 2026 · Mathlib 0df444a (Lean v4.33.1)

theoremstimepiece

Prove the following Lean 4 theorem from ChapterA.

BookProof.ChapterA.System.schur_normal_irreducible (M : System 𝔽 V) (hM : IsNormal M) (hSchur : ∀ S : V →L[𝔽] V, M.Commutes S → IsSelfAdjoint S → ∃ c : 𝔽, S = c • (1 : V →L[𝔽] V)) : IsIrreducible M

Formalization note: Lean 4 identifier BookProof.ChapterA.System.schur_normal_irreducible.

Preamble

-- Generated from ChapterA.lean — theorem BookProof.ChapterA.System.schur_normal_irreducible
import Mathlib
import Definitions.Def_ChapterA
open BookProof.ChapterA
open BookProof.ChapterA

variable {𝔽 : Type*} [RCLike 𝔽] {V : Type*} [NormedAddCommGroup V]
    [InnerProductSpace 𝔽 V] [CompleteSpace V]


open scoped ComplexConjugate InnerProductSpace

Formal statement

theorem BookProof.ChapterA.System.schur_normal_irreducible (M : System 𝔽 V) (hM : IsNormal M)
    (hSchur : ∀ S : V →L[𝔽] V, M.Commutes S → IsSelfAdjoint S →
      ∃ c : 𝔽, S = c • (1 : V →L[𝔽] V)) :
    IsIrreducible M := by sorry

View graph