def definition def or abbrev

`inv_pole_factor`

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

formal statement (Lean)

  73def inv_pole_factor (alpha_s : ℝ) (N_l : ℕ) : ℝ :=

Definition body.

  74  1 - K_1 * (alpha_s / Real.pi) +
  75  (K_1 ^ 2 - K_2 N_l) * (alpha_s / Real.pi) ^ 2
  76

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

inv_pole_factor_at_zero in IndisputableMonolith.Physics.QCDRGE.PoleToMSbar decl_use
m_MS_from_pole in IndisputableMonolith.Physics.QCDRGE.PoleToMSbar decl_use

Lean names referenced from this declaration's body.