Registry · Definition IV.D102 tau-effective formalized

IV.D102 — Hodge Dual of F

The Hodge dual (*F)_mu_nu = (1/2)*epsilon_mu_nu_rho_sigma*F^rho_sigma implements electric-magnetic duality: E -> B, B -> -E.

Book IV Part 4 Ch. 28

Dependency Graph

Depends on (1)

IV.D111

Depended on by (2)

IV.D378 IV.D379

Lean Formalization

Module: TauLib.BookIV.Electroweak.TauMaxwell

Symbol: Tau.BookIV.Electroweak.HodgeDualOfF