module module

`IndisputableMonolith.Relativity.Geometry.MetricUnification`

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

used by (2)

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

IndisputableMonolith.Relativity.Geometry module_import
IndisputableMonolith.Relativity.Geometry.DiscreteBridge module_import

depends on (3)

Lean names referenced from this declaration's body.

IndisputableMonolith.Relativity.Geometry.Curvature module_import
IndisputableMonolith.Relativity.Geometry.Metric module_import
IndisputableMonolith.Relativity.Geometry.Tensor module_import

declarations in this module (18)

def rs_eta L45
theorem rs_eta_eq_im_eta L51
def rs_minkowski L63
theorem rs_minkowski_eq L66
theorem rs_eta_00 L70
theorem rs_eta_11 L71
theorem rs_eta_22 L72
theorem rs_eta_33 L73
theorem rs_eta_offdiag L75
theorem rs_eta_symm L78
theorem minkowski_real_christoffel_zero L94
theorem scaffold_agrees_on_minkowski L99
structure RealGeodesic L110
structure TimelikeGeodesic L121
structure RealNullGeodesic L130
structure SpacelikeGeodesic L139
theorem geodesic_uses_real_christoffel L149
theorem minkowski_straight_line_geodesic L160