def definition def or abbrev

`b0`

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

formal statement (Lean)

  47def b0 (N_f : ℕ) : ℝ := (11 * (N_c : ℝ) - 2 * (N_f : ℝ)) / (12 * Real.pi)

Definition body.

  48
  49/-- Two-loop beta coefficient in MS-bar (canonical SU(3) form). -/

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

exists_shift_ae_abs_sub_le_of_oscOn_Icc_exhaustion in IndisputableMonolith.NumberTheory.RiemannHypothesis.LocalToGlobalWedge decl_use
b0_pos_at5 in IndisputableMonolith.Physics.QCDRGE.MassAnomalousDimension decl_use
mass_ratio_leading in IndisputableMonolith.Physics.QCDRGE.MassAnomalousDimension decl_use
mass_ratio_two_loop in IndisputableMonolith.Physics.QCDRGE.MassAnomalousDimension decl_use
alpha_s_two_loop in IndisputableMonolith.Physics.QCDRGE.TwoLoopAlphaS decl_use
alpha_s_two_loop_b1_zero_eq_one_loop in IndisputableMonolith.Physics.QCDRGE.TwoLoopAlphaS decl_use
alpha_s_two_loop_pos_when_denom_pos in IndisputableMonolith.Physics.QCDRGE.TwoLoopAlphaS decl_use
b0_at_Nf5_pos in IndisputableMonolith.Physics.QCDRGE.TwoLoopAlphaS decl_use
TwoLoopAlphaSCert in IndisputableMonolith.Physics.QCDRGE.TwoLoopAlphaS decl_use

Lean names referenced from this declaration's body.