theorem proved term proof

`row_fermi_codata_in_bracket`

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

formal statement (Lean)

  98theorem row_fermi_codata_in_bracket :
  99    (1.16e-5 : ℝ) < row_fermi_codata ∧ row_fermi_codata < (1.17e-5 : ℝ) := by

Term-mode proof.

 100  unfold row_fermi_codata
 101  constructor <;> norm_num
 102

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

fermiConstantScoreCardCert_holds in IndisputableMonolith.Constants.FermiConstantScoreCard decl_use

Lean names referenced from this declaration's body.

row_fermi_codata in IndisputableMonolith.Constants.FermiConstantScoreCard decl_use