def
definition
covariant_deriv_bilinear
show as:
view math explainer →
open explainer
Read the cached plain-language explainer.
open lean source
IndisputableMonolith.Relativity.Geometry.Connection on GitHub at line 50.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
used by
formal source
47 (_ω : CovectorField) (_μ : Fin 4) : CovectorField := fun _ _ _ => 0
48
49/-- Covariant derivative of a bilinear form; collapses to zero. -/
50noncomputable def covariant_deriv_bilinear (_g : MetricTensor)
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