module module

`IndisputableMonolith.Relativity.Geodesics.NullGeodesic`

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

depends on (2)

Lean names referenced from this declaration's body.

IndisputableMonolith.Relativity.Calculus module_import
IndisputableMonolith.Relativity.Geometry module_import

declarations in this module (8)

structure NullGeodesic L20
structure InitialConditions L37
def straight_line L42
def straight_null_geodesic L46
theorem null_geodesic_exists_minkowski L68
theorem affine_reparametrization L76
theorem minkowski_straight_line_is_geodesic L93
theorem geodesic_unique L113