`BookProof.SmCar.normSq_eq_sum` (x : FermiFock n) : ‖x‖ ^ 2 = ∑ S : Finset (Fin n), ‖x S‖ ^ 2

Initializing...

`BookProof.SmCar.normSq_eq_sum` (x : FermiFock n) : ‖x‖ ^ 2 = ∑ S : Finset (Fin n), ‖x S‖ ^ 2 · Prove2Me