`BookProof.SmOneParticle.unitary_row_sum_normSq` (hV : IsMixing V) (i : Fin 3) : ∑ j : Fin 3, ‖V i j‖ ^ 2 = 1

Initializing...

`BookProof.SmOneParticle.unitary_row_sum_normSq` (hV : IsMixing V) (i : Fin 3) : ∑ j : Fin 3, ‖V i j‖ ^ 2 = 1 · Prove2Me