`BookProof.SmHiggsVacuum.higgs_radial` {lam mu2 : ℝ} {u : E} (hu : lam * ‖u‖ ^ 2 = mu2) (t : ℝ) : higgsV lam mu2 ((1 + t) • u) = higgsV lam mu2 u + mu2 * ‖u‖ ^ 2 * t ^ 2 * (1 + t +

Initializing...

`BookProof.SmHiggsVacuum.higgs_radial` {lam mu2 : ℝ} {u : E} (hu : lam * ‖u‖ ^ 2 = mu2) (t : ℝ) : higgsV lam mu2 ((1 + t) • u) = higgsV lam mu2 u + mu2 * ‖u‖ ^ 2 * t ^ 2 * (1 + t + · Prove2Me