def definition def or abbrev

`K_2`

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

formal statement (Lean)

  34def K_2 (N_l : ℕ) : ℝ := 11.1 - 1.04 * (N_l : ℝ)

Definition body.

  35
  36/-- The two-loop pole-to-MS-bar conversion factor.
  37
  38    `pole_factor alpha_s N_l = 1 + (4/3)(a/π) + K_2 (a/π)^2`
  39-/

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

inv_pole_factor in IndisputableMonolith.Physics.QCDRGE.PoleToMSbar decl_use
K_2_at5_pos in IndisputableMonolith.Physics.QCDRGE.PoleToMSbar decl_use
pole_factor in IndisputableMonolith.Physics.QCDRGE.PoleToMSbar decl_use
pole_factor_pos_top in IndisputableMonolith.Physics.QCDRGE.PoleToMSbar decl_use
PoleToMSbarCert in IndisputableMonolith.Physics.QCDRGE.PoleToMSbar decl_use

Lean names referenced from this declaration's body.