def definition def or abbrev

`metric_det`

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

formal statement (Lean)

  28noncomputable def metric_det (_g : MetricTensor) (_x : Fin 4 → ℝ) : ℝ := 1

Definition body.

  29
  30/-- Placeholder inverse metric component accessor. -/

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

TotalHamiltonian in IndisputableMonolith.Foundation.Hamiltonian 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
metric_det in IndisputableMonolith.Relativity.Geometry.Metric decl_use
spacetime_emergence_cert in IndisputableMonolith.Unification.SpacetimeEmergence decl_use
SpacetimeEmergenceCert in IndisputableMonolith.Unification.SpacetimeEmergence decl_use

Lean names referenced from this declaration's body.