`BookProof.ChapterWeylSl2.Sl2Rep.apply_H_E` (v : V) : R.H (R.E v) = R.E (R.H v) + 2 • R.E v

Initializing...

`BookProof.ChapterWeylSl2.Sl2Rep.apply_H_E` (v : V) : R.H (R.E v) = R.E (R.H v) + 2 • R.E v · Prove2Me