def definition def or abbrev

`row_fermi_pred`

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

formal statement (Lean)

  50noncomputable def row_fermi_pred : ℝ :=

Definition body.

  51  1 / (Real.sqrt 2 * vev_canonical ^ 2)
  52
  53/-- CODATA/PDG Fermi constant in GeV^-2. -/

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

FermiConstantScoreCardCert in IndisputableMonolith.Constants.FermiConstantScoreCard decl_use
row_fermi_pred_bracket in IndisputableMonolith.Constants.FermiConstantScoreCard decl_use
row_fermi_pred_eq in IndisputableMonolith.Constants.FermiConstantScoreCard decl_use
row_fermi_pred_lower in IndisputableMonolith.Constants.FermiConstantScoreCard decl_use
row_fermi_pred_upper in IndisputableMonolith.Constants.FermiConstantScoreCard decl_use
DarkMatterWeakReferenceCrossSectionScoreCardCert in IndisputableMonolith.Physics.DarkMatterWeakReferenceCrossSectionScoreCard decl_use
row_weak_ref_cross_section_band in IndisputableMonolith.Physics.DarkMatterWeakReferenceCrossSectionScoreCard decl_use
sigma_nu_weak_ref_cm2 in IndisputableMonolith.Physics.DarkMatterWeakReferenceCrossSectionScoreCard decl_use

Lean names referenced from this declaration's body.

vev_canonical in IndisputableMonolith.Constants.ElectroweakVEVStructure decl_use
constant in IndisputableMonolith.Relativity.Fields.Scalar decl_use