structure definition def or abbrev

`MetricTensor`

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

formal statement (Lean)

  18structure MetricTensor where
  19  g : (Fin 4 → ℝ) → (Fin 4 → ℝ) → (Fin 2 → Fin 4) → ℝ := fun _ _ _ => 0

proof body

Definition body.

  20
  21/-- Local non-sealed bilinear form interface. -/

used by (40)

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

energy_conservation in IndisputableMonolith.Foundation.Hamiltonian decl_use
HamiltonianDensity in IndisputableMonolith.Foundation.Hamiltonian decl_use
hamiltonian_equivalence in IndisputableMonolith.Foundation.Hamiltonian decl_use
H_EnergyConservation in IndisputableMonolith.Foundation.Hamiltonian decl_use
H_HamiltonianEquivalence in IndisputableMonolith.Foundation.Hamiltonian decl_use
inverse_metric in IndisputableMonolith.Foundation.Hamiltonian decl_use
IsTimeTranslationInvariant in IndisputableMonolith.Foundation.Hamiltonian decl_use
metric_det in IndisputableMonolith.Foundation.Hamiltonian decl_use
StressEnergyTensor in IndisputableMonolith.Foundation.Hamiltonian decl_use
TotalHamiltonian in IndisputableMonolith.Foundation.Hamiltonian decl_use
metric_compatibility in IndisputableMonolith.Gravity.Connection decl_use
MetricTensor in IndisputableMonolith.Gravity.Connection decl_use
minkowski in IndisputableMonolith.Gravity.Connection decl_use
hilbert_variation_holds in IndisputableMonolith.Gravity.EinsteinHilbertAction decl_use
jacobi_variation in IndisputableMonolith.Gravity.EinsteinHilbertAction decl_use
jacobi_variation_structural in IndisputableMonolith.Gravity.EinsteinHilbertAction decl_use
einstein_symmetric in IndisputableMonolith.Gravity.RicciTensor decl_use
einstein_tensor 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
perfect_fluid in IndisputableMonolith.Gravity.StressEnergyTensor decl_use
vacuum_is_special_case in IndisputableMonolith.Gravity.StressEnergyTensor decl_use
H_HomogenizationLimit in IndisputableMonolith.Meta.Homogenization decl_use
homogenization_limit in IndisputableMonolith.Meta.Homogenization decl_use
metric_det in IndisputableMonolith.Meta.Homogenization decl_use
MetricTensor in IndisputableMonolith.Meta.Homogenization decl_use
metric_FRW in IndisputableMonolith.Relativity.Cosmology.FRWMetric decl_use
einstein_hilbert_action in IndisputableMonolith.Relativity.Fields.Integration decl_use

… and 10 more

depends on (3)

Lean names referenced from this declaration's body.

MetricTensor in IndisputableMonolith.Gravity.Connection decl_use
MetricTensor in IndisputableMonolith.Meta.Homogenization decl_use
MetricTensor in IndisputableMonolith.Relativity.Geometry.Metric decl_use