pith. machine review for the scientific record. sign in
structure definition def or abbrev

TopQuarkMassScoreCardCert

show as:
view Lean formalization →

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

generate prose now

formal statement (Lean)

  47structure TopQuarkMassScoreCardCert where
  48  positive : 0 < top_quark_pred
  49  top_charm : top_quark_pred / charm_quark_pred = phi ^ (6 : ℕ)
  50  order_MeV : (10000 : ℝ) < top_quark_pred ∧ top_quark_pred < 1000000
  51  pdg_ref_pos : 0 < row_pdg_top_MeV
  52

used by (1)

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

depends on (3)

Lean names referenced from this declaration's body.