`BookProof.Bosonic.star_ann` (h : BosonicCCR J a) (v : V) : star (ann a J v) = cre a J v

-- Generated from ChapterBosonicCCR.lean — theorem BookProof.Bosonic.star_ann
import Mathlib
import Definitions.Def_ChapterBosonicCCR
import Definitions.Def_ChapterStoneConverse
open BookProof.ChapterStoneMeasurable
open BookProof.ChapterStoneMeasurable.WeakMeasurableUnitaryGroup
open BookProof.Bosonic


open RealInnerProductSpace


variable {V : Type*} [NormedAddCommGroup V] [InnerProductSpace ℝ V]
variable {R : Type*} [Ring R] [StarRing R] [Algebra ℂ R] [Algebra ℝ R]
  [IsScalarTower ℝ ℂ R] [StarModule ℂ R]

variable {J : V →ₗ[ℝ] V} {a : V →ₗ[ℝ] R}

theorem BookProof.Bosonic.star_ann (h : BosonicCCR J a) (v : V) : star (ann a J v) = cre a J v := by sorry