pith. machine review for the scientific record. sign in
structure definition def or abbrev

ClosedLoop

show as:
view Lean formalization →

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

generate prose now

formal statement (Lean)

 177structure ClosedLoop extends SpacetimeCurve where
 178  closed : path 0 = path 1
 179
 180/-- The holonomy defect: the difference between a vector and its parallel
 181    transport around a closed loop.
 182
 183    For an infinitesimal loop enclosing area δA^{μν}, the defect is:
 184    δV^ρ = R^ρ_{σμν} V^σ δA^{μν}
 185
 186    This is the geometric meaning of the Riemann tensor. -/

used by (2)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (18)

Lean names referenced from this declaration's body.