`minkowski_christoffel_zero`

proved

show as: view math explainer →

module: IndisputableMonolith.Relativity.Geometry.Connection
domain: Relativity
line: 61 · github
papers citing: none yet

open explainer

Generate a durable explainer page for this declaration.

open lean source

IndisputableMonolith.Relativity.Geometry.Connection on GitHub at line 61.

browse module

All declarations in this module, on Recognition.

explainer page

Tracked in the explainer inventory; generation is lazy so crawlers do not trigger LLM jobs.

open explainer

depends on

formal source

  58  rfl
  59
  60
  61@[simp] theorem minkowski_christoffel_zero
  62    (x : Fin 4 → ℝ) (ρ μ ν : Fin 4) :
  63    (christoffel_from_metric minkowski_tensor).Γ x ρ μ ν = 0 := rfl
  64
  65end Geometry
  66end Relativity
  67end IndisputableMonolith

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.