def definition def or abbrev

`wZRatio`

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

formal statement (Lean)

  83noncomputable def wZRatio (theta_W : ℝ) : ℝ := Real.cos theta_W

Definition body.

  84
  85/-- Observed masses:
  86    m_W ≈ 80.4 GeV
  87    m_Z ≈ 91.2 GeV
  88    Ratio ≈ 0.882 -/

Lean names referenced from this declaration's body.