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

metric_to_matrix

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)

  49noncomputable def metric_to_matrix (g : MetricTensor) (x : Fin 4 → ℝ) : Matrix (Fin 4) (Fin 4) ℝ :=

proof body

Definition body.

  50  fun i j => g.g x (fun _ => 0) (fun k => if (k : ℕ) = 0 then i else j)
  51
  52/-- The metric matrix is symmetric because the metric tensor is symmetric. -/

used by (5)

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

depends on (8)

Lean names referenced from this declaration's body.