`BookProof.SmHamiltonian.wall_sq` (P : SmParams) (q : ℝ) : 1 / 2 * (Real.sqrt (P.lam / 2) * (q - P.vev ^ 2)) ^ 2 = P.lam / 4 * (q

Initializing...

`BookProof.SmHamiltonian.wall_sq` (P : SmParams) (q : ℝ) : 1 / 2 * (Real.sqrt (P.lam / 2) * (q - P.vev ^ 2)) ^ 2 = P.lam / 4 * (q - P.vev ^ 2) ^ 2 · Prove2Me