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

Initializing...

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