`BookProof.ChapterMajoranaFourier.nslash_sq` (n : Fin 3 → ℝ) (hn : ∑ i, (n i) ^ 2 = 1) : nslash n * nslash n = -1

Initializing...

`BookProof.ChapterMajoranaFourier.nslash_sq` (n : Fin 3 → ℝ) (hn : ∑ i, (n i) ^ 2 = 1) : nslash n * nslash n = -1 · Prove2Me