def definition def or abbrev

`row_mH_codata`

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

formal statement (Lean)

  30noncomputable def row_mH_codata : ℝ := mH_obs

Definition body.

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

row_mH_codata_pos in IndisputableMonolith.Physics.HiggsMassScoreCard decl_use
row_mH_within_five_percent in IndisputableMonolith.Physics.HiggsMassScoreCard decl_use

Lean names referenced from this declaration's body.