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)
47def sigma_nu_weak_ref_cm2 : ℝ :=
proof body
Definition body.
48 row_fermi_pred ^ (2 : ℕ) * E_ref_GeV ^ (2 : ℕ) * gev2_to_cm2
49
50/-- Derived absolute dark-matter cross-section in cm^2 on this reference. -/
used by (4)
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.
-
row_fermi_pred
in IndisputableMonolith.Constants.FermiConstantScoreCard
decl_use
-
E_ref_GeV
in IndisputableMonolith.Physics.DarkMatterWeakReferenceCrossSectionScoreCard
decl_use
-
gev2_to_cm2
in IndisputableMonolith.Physics.DarkMatterWeakReferenceCrossSectionScoreCard
decl_use