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)
41def N_c : ℕ := 3
proof body
Definition body.
42
43/-- Casimir of the fundamental: C_F = (N_c^2 - 1)/(2 N_c) = 4/3. -/
used by (9)
From the project-wide theorem graph. These declarations reference this one in their body.
-
three_colors_from_D3
in IndisputableMonolith.Foundation.QuarkColors
decl_use
-
beta0
in IndisputableMonolith.Physics.QCDRGE.AlphaRunning
decl_use
-
beta0_at_Z
in IndisputableMonolith.Physics.QCDRGE.AlphaRunning
decl_use
-
beta0_pos
in IndisputableMonolith.Physics.QCDRGE.AlphaRunning
decl_use
-
N_c
in IndisputableMonolith.Physics.QCDRGE.AlphaRunning
decl_use
-
c0
in IndisputableMonolith.Physics.QCDRGE.MassAnomalousDimension
decl_use
-
alpha_s_two_loop_b1_zero_eq_one_loop
in IndisputableMonolith.Physics.QCDRGE.TwoLoopAlphaS
decl_use
-
b0
in IndisputableMonolith.Physics.QCDRGE.TwoLoopAlphaS
decl_use
-
b0_at_Nf5_pos
in IndisputableMonolith.Physics.QCDRGE.TwoLoopAlphaS
decl_use
depends on (7)
Lean names referenced from this declaration's body.
-
of
in IndisputableMonolith.Astrophysics.NucleosynthesisTiers
decl_use
-
of
in IndisputableMonolith.Foundation.DAlembert.LedgerFactorization
decl_use
-
of
in IndisputableMonolith.Foundation.PhiForcingDerived
decl_use
-
of
in IndisputableMonolith.Foundation.SpectralEmergence
decl_use
-
of
in IndisputableMonolith.Information.PhysicsComplexityStructure
decl_use
-
N_c
in IndisputableMonolith.Physics.QCDRGE.AlphaRunning
decl_use
-
C_F
in IndisputableMonolith.Physics.QCDRGE.TwoLoopAlphaS
decl_use