Registry · Theorem IV.T42 tau-effective formalized

IV.T42 — Homogeneous Maxwell Equations

The Bianchi identity dF = 0 on the EM gauge bundle yields div B = 0 (no monopoles) and curl E + dB/dt = 0 (Faraday), automatic from d^2 = 0.

Book IV Part 4 Ch. 28

Dependency Graph

Depends on (2)

Depended on by (1)

Lean Formalization

Module: TauLib.BookIV.Electroweak.TauMaxwell

Symbol: Tau.BookIV.Electroweak.HomogeneousMaxwellEquations