Registry · Definition II.D79 tau-effective formalized

II.D79 — Parallel Transport

Parallel transport along a path γ in Z/M_k Z: sequential composition of the connection transport operator along each edge. For the flat connection, this reduces to addition mod M_k.

Book II Part 10 Ch. 55

Dependency Graph

Depends on (1)

Depended on by (2)

Lean Formalization

Module: TauLib.BookII.Closure.Connection

Symbol: parallel_transport