module module

`IndisputableMonolith.Constants.FermiConstantScoreCard`

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

used by (1)

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

IndisputableMonolith.Physics.DarkMatterWeakReferenceCrossSectionScoreCard module_import

depends on (2)

Lean names referenced from this declaration's body.

IndisputableMonolith.Constants.ElectroweakVEVStructure module_import
IndisputableMonolith.Numerics.Interval.W8Bounds module_import

declarations in this module (11)

def row_fermi_pred L50
def row_fermi_codata L54
theorem row_fermi_pred_eq L56
theorem sqrt2_pos L59
theorem fermi_den_pos L61
theorem row_fermi_pred_lower L65
theorem row_fermi_pred_upper L80
theorem row_fermi_pred_bracket L94
theorem row_fermi_codata_in_bracket L98
structure FermiConstantScoreCardCert L103
theorem fermiConstantScoreCardCert_holds L110