(e : ℕ → ℝ) (mu : ℝ) (β : Conf) : confEnergy (fun k => e k + mu) β = confEnergy e β + mu * (confNumber β : ℝ)

Initializing...

(e : ℕ → ℝ) (mu : ℝ) (β : Conf) : confEnergy (fun k => e k + mu) β = confEnergy e β + mu * (confNumber β : ℝ) · Prove2Me