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

Initializing...

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