  51  (_B : BilinearForm) (_ρ : Fin 4) : BilinearForm := fun _ _ _ => 0
  52
  53/-- Metric compatibility: ∇_ρ g_μν = 0. -/
  54theorem metric_compatibility (g : MetricTensor) :
  55    ∀ ρ x up low, covariant_deriv_bilinear g g.g ρ x up low = 0 := by
  56  intro ρ x up low
  57  unfold covariant_deriv_bilinear
  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.