`BookProof.ChapterA3.mgamma_irreducible` (W : Submodule ℂ MajoranaSpace) (hW : ∀ μ, ∀ x ∈ W, mgammaLin μ x ∈ W) : W = ⊥ ∨ W = ⊤

Initializing...

`BookProof.ChapterA3.mgamma_irreducible` (W : Submodule ℂ MajoranaSpace) (hW : ∀ μ, ∀ x ∈ W, mgammaLin μ x ∈ W) : W = ⊥ ∨ W = ⊤ · Prove2Me