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

riemann_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)

  38noncomputable def riemann_tensor (g : MetricTensor) : Tensor 1 3 :=

proof body

Definition body.

  39  fun x up low =>
  40    let rho := up 0
  41    let sigma := low 0
  42    let mu := low 1
  43    let nu := low 2
  44    let Γ := christoffel g
  45    (partialDeriv_v2 (fun y => Γ y rho nu sigma) mu x) -
  46    (partialDeriv_v2 (fun y => Γ y rho mu sigma) nu x) +
  47    Finset.univ.sum (fun (lambda : Fin 4) => Γ x rho mu lambda * Γ x lambda nu sigma) -
  48    Finset.univ.sum (fun (lambda : Fin 4) => Γ x rho nu lambda * Γ x lambda mu sigma)
  49
  50/-- **Ricci Tensor** $R_{\mu\nu} = R^{\rho}_{\mu\rho\nu}$. -/

used by (17)

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

depends on (14)

Lean names referenced from this declaration's body.