`BookProof.ChapterWeylSl2.Sl2Rep.apply_H_F` (v : V) : R.H (R.F v) = R.F (R.H v) - 2 • R.F v
ProvedBookProof.ChapterWeylSl2.Sl2Rep.apply_H_Ftheoremstimepiece
Prove the following Lean 4 theorem from ChapterWeylSl2.
BookProof.ChapterWeylSl2.Sl2Rep.apply_H_F (v : V) : R.H (R.F v) = R.F (R.H v) - 2 • R.F v
Formalization note: Lean 4 identifier BookProof.ChapterWeylSl2.Sl2Rep.apply_H_F.
Preamble
-- Generated from ChapterWeylSl2.lean — theorem BookProof.ChapterWeylSl2.Sl2Rep.apply_H_F
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}
variable {R : Sl2Rep V}Formal statement
theorem BookProof.ChapterWeylSl2.Sl2Rep.apply_H_F (v : V) : R.H (R.F v) = R.F (R.H v) - 2 • R.F v := by sorry