abbrev definition def or abbrev

`VolumeElement`

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

formal statement (Lean)

  12abbrev VolumeElement := Fields.VolumeElement

proof body

Definition body.

  13
  14/-- Einstein–Hilbert action: S_EH = (M_P²/2) ∫ √(-g) R d^4x.
  15    Scaffold: returns symbolic R evaluation (integration machinery pending). -/

used by (11)

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

eh_action_minkowski in IndisputableMonolith.Relativity.Fields.Integration decl_use
einstein_hilbert_action in IndisputableMonolith.Relativity.Fields.Integration decl_use
integrate_add in IndisputableMonolith.Relativity.Fields.Integration decl_use
integrate_scalar in IndisputableMonolith.Relativity.Fields.Integration decl_use
integrate_smul in IndisputableMonolith.Relativity.Fields.Integration decl_use
kinetic_action in IndisputableMonolith.Relativity.Fields.Integration decl_use
kinetic_nonneg in IndisputableMonolith.Relativity.Fields.Integration decl_use
potential_action in IndisputableMonolith.Relativity.Fields.Integration decl_use
sample_grid in IndisputableMonolith.Relativity.Fields.Integration decl_use
VolumeElement in IndisputableMonolith.Relativity.Fields.Integration decl_use
default_volume in IndisputableMonolith.Relativity.ILG.Action decl_use

depends on (2)

Lean names referenced from this declaration's body.

VolumeElement in IndisputableMonolith.Relativity.Fields.Integration decl_use
S_EH in IndisputableMonolith.Relativity.ILG.Action decl_use