`BookProof.Bosonic.field_commute_self_scalar` (hJ : ∀ v w : V, ⟪J v, w⟫ = -⟪v, J w⟫) (v : V) : algebraMap ℂ R (Complex.I * (⟪v, J v⟫ : ℂ)) = 0

Initializing...

`BookProof.Bosonic.field_commute_self_scalar` (hJ : ∀ v w : V, ⟪J v, w⟫ = -⟪v, J w⟫) (v : V) : algebraMap ℂ R (Complex.I * (⟪v, J v⟫ : ℂ)) = 0 · Prove2Me