module module

`IndisputableMonolith.Relativity.Geometry.Curvature`

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 (7)

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

IndisputableMonolith.Relativity.Geometry module_import
IndisputableMonolith.Relativity.Geometry.CovariantDerivative module_import
IndisputableMonolith.Relativity.Geometry.DiscreteBridge module_import
IndisputableMonolith.Relativity.Geometry.LeviCivitaTheorem module_import
IndisputableMonolith.Relativity.Geometry.MetricUnification module_import
IndisputableMonolith.Relativity.Geometry.ParallelTransport module_import
IndisputableMonolith.Relativity.Geometry.RiemannSymmetries module_import

depends on (3)

Lean names referenced from this declaration's body.

IndisputableMonolith.Relativity.Calculus.Derivatives module_import
IndisputableMonolith.Relativity.Geometry.Metric module_import
IndisputableMonolith.Relativity.Geometry.Tensor module_import

declarations in this module (13)

def christoffel L13
theorem christoffel_symmetric L23
def riemann_tensor L38
def ricci_tensor L51
theorem riemann_antisymmetric_last_two L63
def ricci_scalar L104
def einstein_tensor L110
lemma eta_deriv_zero L122
theorem minkowski_christoffel_zero_proper L128
theorem minkowski_riemann_zero L135
theorem minkowski_ricci_zero L145
theorem minkowski_ricci_scalar_zero L151
theorem minkowski_einstein_zero L156