`BookProof.SmCar.fermiEnergy_apply` (m : Fin n → ℝ) (ψ : FermiFock n) (S : Finset (Fin n)) : (fermiEnergy m ψ) S = ((∑ i ∈ S, m i : ℝ) : ℂ) * ψ S

Initializing...

`BookProof.SmCar.fermiEnergy_apply` (m : Fin n → ℝ) (ψ : FermiFock n) (S : Finset (Fin n)) : (fermiEnergy m ψ) S = ((∑ i ∈ S, m i : ℝ) : ℂ) * ψ S · Prove2Me