`BookProof.SmDiracYukawa.diagOp_normSq` (d : Finset (Fin n) → ℝ) (ψ : FermiFock n) : ‖diagOp d ψ‖ ^ 2 = ∑ S : Finset (Fin n), (d S) ^ 2 * ‖ψ S‖ ^ 2

Initializing...

`BookProof.SmDiracYukawa.diagOp_normSq` (d : Finset (Fin n) → ℝ) (ψ : FermiFock n) : ‖diagOp d ψ‖ ^ 2 = ∑ S : Finset (Fin n), (d S) ^ 2 * ‖ψ S‖ ^ 2 · Prove2Me