def definition def or abbrev

`mZ`

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

formal statement (Lean)

  59def mZ (g gp v : ℝ) : ℝ := Real.sqrt (mZ_sq g gp v)

Definition body.

  60
  61/-- `m_W² ≥ 0` always. -/

From the project-wide theorem graph. These declarations reference this one in their body.

mW_over_mZ_eq_cos_thetaW in IndisputableMonolith.StandardModel.ElectroweakMassBridge decl_use
higgsMassSq_simplifies in IndisputableMonolith.StandardModel.Q3Representations decl_use

Lean names referenced from this declaration's body.