BookProof.ChapterWeylSl2.Sl2Rep.hf'

-- Generated from ChapterWeylSl2.lean — theorem BookProof.ChapterWeylSl2.Sl2Rep.hf'
import Mathlib
import Definitions.Def_ChapterWeylSl2
import Definitions.Def_ChapterDoubleSlit
open BookProof.ChapterDoubleSlit
open BookProof.ChapterWeylSl2
open BookProof.ChapterWeylSl2



universe u

variable {V : Type u} [AddCommGroup V] [Module ℂ V]

variable (R : Sl2Rep V)
variable {R}

theorem BookProof.ChapterWeylSl2.Sl2Rep.hf_prime : R.H * R.F = R.F * R.H - 2 • R.F := by sorry