def definition def or abbrev

`minkowski`

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

formal statement (Lean)

  49def minkowski : MetricTensor where
  50  g := fun mu nu => if mu = nu then (if mu = 0 then -1 else 1) else 0

Definition body.

  51  symmetric := by intro mu nu; split_ifs <;> simp_all [eq_comm]
  52
  53/-- The Minkowski inverse equals the Minkowski metric itself. -/

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

HilbertVariationCert in IndisputableMonolith.Gravity.EinsteinHilbertAction decl_use
hilbert_variation_flat in IndisputableMonolith.Gravity.EinsteinHilbertAction decl_use
einstein_flat in IndisputableMonolith.Gravity.RicciTensor decl_use
minkowski_is_vacuum_solution in IndisputableMonolith.Gravity.RicciTensor decl_use
RicciCert in IndisputableMonolith.Gravity.RicciTensor decl_use

Lean names referenced from this declaration's body.