Registry · Theorem IV.T38 tau-effective formalized

IV.T38 — Gauge Invariance of F_mu_nu

The field strength tensor is gauge-invariant: under A_mu -> A_mu + (1/e)*partial_mu alpha, F_mu_nu -> F_mu_nu (mixed partials commute).

Book IV Part 4 Ch. 27

Dependency Graph

Depends on (1)

Depended on by (5)

Lean Formalization

Module: TauLib.BookIV.Electroweak.GaugeInvariance

Symbol: Tau.BookIV.Electroweak.GaugeInvarianceOfFmunu