pith. machine review for the scientific record. sign in
def definition def or abbrev

einstein_tensor

show as:
view Lean formalization →

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

generate prose now

formal statement (Lean)

  65noncomputable def einstein_tensor
  66    (met : MetricTensor) (ginv : InverseMetric)
  67    (gamma : Idx → Idx → Idx → ℝ)
  68    (dgamma : Idx → Idx → Idx → Idx → ℝ)
  69    (mu nu : Idx) : ℝ :=

proof body

Definition body.

  70  ricci_tensor gamma dgamma mu nu -
  71  (1/2) * scalar_curvature ginv gamma dgamma * met.g mu nu
  72
  73/-- Einstein tensor vanishes for flat spacetime. -/

used by (10)

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

depends on (15)

Lean names referenced from this declaration's body.