def definition def or abbrev

`christoffel_from_metric`

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

formal statement (Lean)

  32noncomputable def christoffel_from_metric (_g : MetricTensor) : ChristoffelSymbols := {}

Definition body.

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

christoffel_from_metric in IndisputableMonolith.Gravity.Connection decl_use
christoffel_symmetric in IndisputableMonolith.Gravity.Connection decl_use
ConnectionCert in IndisputableMonolith.Gravity.Connection decl_use
flat_christoffel_vanish in IndisputableMonolith.Gravity.Connection decl_use
geodesic_unique in IndisputableMonolith.Relativity.Geodesics.NullGeodesic decl_use
NullGeodesic in IndisputableMonolith.Relativity.Geodesics.NullGeodesic decl_use
straight_null_geodesic in IndisputableMonolith.Relativity.Geodesics.NullGeodesic decl_use
christoffel_from_metric_symmetric in IndisputableMonolith.Relativity.Geometry.Connection decl_use
minkowski_christoffel_zero in IndisputableMonolith.Relativity.Geometry.Connection decl_use
rs_eta_symm in IndisputableMonolith.Relativity.Geometry.MetricUnification decl_use
SpacelikeGeodesic in IndisputableMonolith.Relativity.Geometry.MetricUnification decl_use

Lean names referenced from this declaration's body.

MetricTensor in IndisputableMonolith.Foundation.Hamiltonian decl_use
christoffel_from_metric in IndisputableMonolith.Gravity.Connection decl_use
MetricTensor in IndisputableMonolith.Gravity.Connection decl_use
MetricTensor in IndisputableMonolith.Meta.Homogenization decl_use
ChristoffelSymbols in IndisputableMonolith.Relativity.Geometry.Connection decl_use
MetricTensor in IndisputableMonolith.Relativity.Geometry.Metric decl_use