Registry · Definition
IV.D86
tau-effective
formalized
IV.D86 — Local Trivialization
A local trivialization of P_EM over an open set U in tau^1 is a fiber-preserving diffeomorphism to U x S^1_gamma.
Dependency Graph
Depends on (1)
Depended on by (1)
Lean Formalization
Module: TauLib.BookIV.Electroweak.GaugeInvariance
Symbol: Tau.BookIV.Electroweak.LocalTrivialization