def definition def or abbrev

`sqrt_minus_g`

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

formal statement (Lean)

  31noncomputable def sqrt_minus_g (_g : MetricTensor) (_x : Fin 4 → ℝ) : ℝ := 1

Definition body.

  32
  33/-- Integrate a scalar function over spacetime volume (discrete approximation). -/

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

integrate_scalar in IndisputableMonolith.Relativity.Fields.Integration decl_use
integrate_smul in IndisputableMonolith.Relativity.Fields.Integration decl_use
kinetic_nonneg in IndisputableMonolith.Relativity.Fields.Integration decl_use

Lean names referenced from this declaration's body.