`BookProof.ChapterWeylSl2.Sl2Rep.exists_highestWeight` [FiniteDimensional ℂ V] [Nontrivial V] (R : Sl2Rep V) : ∃ (w : V) (lam : ℂ), w ≠ 0 ∧ R.E w = 0 ∧ R.H w = lam • w

Initializing...

`BookProof.ChapterWeylSl2.Sl2Rep.exists_highestWeight` [FiniteDimensional ℂ V] [Nontrivial V] (R : Sl2Rep V) : ∃ (w : V) (lam : ℂ), w ≠ 0 ∧ R.E w = 0 ∧ R.H w = lam • w · Prove2Me