`BookProof.Bosonic.ann_add_cre` (v : V) : ann a J v + cre a J v = a v + a v
ProvedBookProof.Bosonic.ann_add_cretheoremstimepiece
Prove the following Lean 4 theorem from ChapterBosonicCCR.
BookProof.Bosonic.ann_add_cre (v : V) : ann a J v + cre a J v = a v + a v
Formalization note: Lean 4 identifier BookProof.Bosonic.ann_add_cre.
Preamble
-- Generated from ChapterBosonicCCR.lean — theorem BookProof.Bosonic.ann_add_cre
import Mathlib
import Definitions.Def_ChapterBosonicCCR
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}Formal statement
theorem BookProof.Bosonic.ann_add_cre (v : V) : ann a J v + cre a J v = a v + a v := by sorry