Registry · Theorem IV.T121 tau-effective formalized

IV.T121 — Gauge covariance of D_mu

Under a change of local trivialization g_{UV}(x) = e^{i alpha(x)}, the gauge potential transforms as A_mu^(V) = A_mu^(U) + (1/e) partial_mu alpha, and D_mu psi transforms covariantly; the field strength F_{mu nu} is gauge-invariant because mixed partial derivatives commute.

Book IV Part 4 Ch. 27

Dependency Graph

Depends on (1)

Lean Formalization

Module: TauLib.BookIV.Electroweak.GaugeInvariance2

Symbol: Tau.BookIV.Electroweak.GaugeCovarianceOfDmu