Registry · Proposition IV.P42 tau-effective formalized

IV.P42 — Non-Abelian Holonomy

For non-abelian gauge groups, holonomy around a closed loop is the path-ordered exponential P exp(ig oint A_mu^a T_a dx^mu).

Book IV Part 4 Ch. 27

Dependency Graph

Depends on (1)

IV.D97

Lean Formalization

Module: TauLib.BookIV.Electroweak.GaugeInvariance2

Symbol: Tau.BookIV.Electroweak.NonabelianHolonomy