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)

  64noncomputable def metric_det (g : MetricTensor) (x : Fin 4 → ℝ) : ℝ :=

Definition body.

  65  (metric_to_matrix g x).det
  66

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

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

Lean names referenced from this declaration's body.

metric_det in IndisputableMonolith.Foundation.Hamiltonian decl_use
MetricTensor in IndisputableMonolith.Foundation.Hamiltonian decl_use
MetricTensor in IndisputableMonolith.Gravity.Connection decl_use
metric_det in IndisputableMonolith.Meta.Homogenization decl_use
MetricTensor in IndisputableMonolith.Meta.Homogenization decl_use
MetricTensor in IndisputableMonolith.Relativity.Geometry.Metric decl_use
metric_to_matrix in IndisputableMonolith.Relativity.Geometry.Metric decl_use