structure definition def or abbrev

`InverseMetric`

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

formal statement (Lean)

  44structure InverseMetric where
  45  ginv : Idx → Idx → ℝ
  46  symmetric : ∀ mu nu, ginv mu nu = ginv nu mu
  47
  48/-- The flat Minkowski metric eta = diag(-1, +1, +1, +1). -/

used by (13)

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
minkowski_inverse in IndisputableMonolith.Gravity.Connection decl_use
hilbert_variation_holds in IndisputableMonolith.Gravity.EinsteinHilbertAction decl_use
einstein_symmetric in IndisputableMonolith.Gravity.RicciTensor decl_use
einstein_tensor in IndisputableMonolith.Gravity.RicciTensor decl_use
scalar_curvature in IndisputableMonolith.Gravity.RicciTensor decl_use
sourced_efe_coord in IndisputableMonolith.Gravity.RicciTensor decl_use
vacuum_efe_coord in IndisputableMonolith.Gravity.RicciTensor decl_use
contracted_bianchi in IndisputableMonolith.Gravity.StressEnergyTensor decl_use
efe_with_source in IndisputableMonolith.Gravity.StressEnergyTensor decl_use
vacuum_is_special_case in IndisputableMonolith.Gravity.StressEnergyTensor decl_use

depends on (4)

Lean names referenced from this declaration's body.

eta in IndisputableMonolith.Cosmology.Nucleosynthesis decl_use
mu in IndisputableMonolith.Cost.Ndim.Projector decl_use
Idx in IndisputableMonolith.Gravity.Connection decl_use
eta in IndisputableMonolith.Relativity.Geometry.Metric decl_use