Registry · Definition IV.D90 tau-effective formalized

IV.D90 — Covariant Derivative

The covariant derivative D_mu psi = partial_mu psi - ieA_mu psi is the unique first-order operator that transforms homogeneously under gauge transformations.

Book IV Part 4 Ch. 27

Dependency Graph

Depends on (1)

Depended on by (2)

Lean Formalization

Module: TauLib.BookIV.Electroweak.GaugeInvariance

Symbol: Tau.BookIV.Electroweak.CovariantDerivative