`BookProof.SmCar.fermiEnergy_occ` (m : Fin n → ℝ) (S : Finset (Fin n)) : fermiEnergy m (occ S) = ((∑ i ∈ S, m i : ℝ) : ℂ) • occ S

Initializing...

`BookProof.SmCar.fermiEnergy_occ` (m : Fin n → ℝ) (S : Finset (Fin n)) : fermiEnergy m (occ S) = ((∑ i ∈ S, m i : ℝ) : ℂ) • occ S · Prove2Me