Registry · Proposition IV.P39 tau-effective formalized

IV.P39 — Explicit Form of F_mu_nu

F_mu_nu = partial_mu A_nu - partial_nu A_mu, computed from the commutator of covariant derivatives with abelian cancellations.

Book IV Part 4 Ch. 27

Dependency Graph

Depends on (1)

IV.D92

Lean Formalization

Module: TauLib.BookIV.Electroweak.GaugeInvariance

Symbol: Tau.BookIV.Electroweak.ExplicitFormOfFmunu