pith. machine review for the scientific record. sign in
theorem proved term proof

m_c_predicted_pos

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)

  80theorem m_c_predicted_pos (alpha_at_mc alpha_at_MZ : ℝ)
  81    (h_alpha_pos : 0 < alpha_at_mc) (h_alpha_0_pos : 0 < alpha_at_MZ) :
  82    0 < m_c_predicted alpha_at_mc alpha_at_MZ := by

proof body

Term-mode proof.

  83  unfold m_c_predicted
  84  exact m_running_pos m_c_at_MZ_GeV alpha_at_mc alpha_at_MZ 5
  85    m_c_at_MZ_pos h_alpha_pos h_alpha_0_pos
  86
  87/-! ## Master cert -/
  88

used by (1)

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

depends on (4)

Lean names referenced from this declaration's body.