def
definition
def or abbrev
predicted_median
show as:
view Lean formalization →
formal statement (Lean)
100def predicted_median : ℝ := 2.75
proof body
Definition body.
101
102/-- The RS prediction: median chi2/dof ≈ 2.75 (within 1.0). -/