Registry · Theorem IV.T41 tau-effective formalized

IV.T41 — Ambrose-Singer Reconstruction

The holonomy group of the connection is generated by parallel transports of the curvature; for U(1) the holonomy equals exp(i int F).

Book IV Part 4 Ch. 27

Dependency Graph

Depends on (2)

IV.D89 IV.D92

Lean Formalization

Module: TauLib.BookIV.Electroweak.GaugeInvariance2

Symbol: Tau.BookIV.Electroweak.AmbrosesingerReconstruction