`BookProof.ChapterWignerLittleGroup.hermOfMom_trace` (p : Fin 4 → ℝ) : (hermOfMom p).trace = ((2 * p 0 : ℝ) : ℂ)

Initializing...

`BookProof.ChapterWignerLittleGroup.hermOfMom_trace` (p : Fin 4 → ℝ) : (hermOfMom p).trace = ((2 * p 0 : ℝ) : ℂ) · Prove2Me