`BookProof.SmHamiltonian.higgs_mexican_hat` (lam mu q : ℝ) (hlam : 0 < lam) : lam / 4 * (q - mu ^ 2 / lam) ^ 2 = -(mu ^ 2 / 2) * q + lam / 4 * q ^ 2 + mu ^ 4 / (4 * lam)

Initializing...

`BookProof.SmHamiltonian.higgs_mexican_hat` (lam mu q : ℝ) (hlam : 0 < lam) : lam / 4 * (q - mu ^ 2 / lam) ^ 2 = -(mu ^ 2 / 2) * q + lam / 4 * q ^ 2 + mu ^ 4 / (4 * lam) · Prove2Me