`BookProof.SmHiggsVacuum.higgsV_eq_min_iff` {lam mu2 : ℝ} (hlam : 0 < lam) (phi : E) : higgsV lam mu2 phi = -(mu2 ^ 2 / (4 * lam)) ↔ ‖phi‖ ^ 2 = mu2 / lam

Initializing...

`BookProof.SmHiggsVacuum.higgsV_eq_min_iff` {lam mu2 : ℝ} (hlam : 0 < lam) (phi : E) : higgsV lam mu2 phi = -(mu2 ^ 2 / (4 * lam)) ↔ ‖phi‖ ^ 2 = mu2 / lam · Prove2Me