`minkowski_ricci_zero`

proved

show as: view math explainer →

module: IndisputableMonolith.Relativity.Geometry.Curvature
domain: Relativity
line: 145 · github
papers citing: none yet

open explainer

Read the cached plain-language explainer.

open lean source

IndisputableMonolith.Relativity.Geometry.Curvature on GitHub at line 145.

browse module

All declarations in this module, on Recognition.

explainer page

A cached Ask Recognition explainer exists for this declaration.

open explainer

depends on

used by

formal source

 142  simp [hΓ, h_deriv, Finset.sum_const_zero]
 143
 144/-- Ricci tensor vanishes for Minkowski space. -/
 145theorem minkowski_ricci_zero (x : Fin 4 → ℝ) (up : Fin 0 → Fin 4) (low : Fin 2 → Fin 4) :
 146    ricci_tensor minkowski_tensor x up low = 0 := by
 147  unfold ricci_tensor
 148  simp [minkowski_riemann_zero, Finset.sum_const_zero]
 149
 150/-- Ricci scalar vanishes for Minkowski space. -/
 151theorem minkowski_ricci_scalar_zero (x : Fin 4 → ℝ) : ricci_scalar minkowski_tensor x = 0 := by
 152  unfold ricci_scalar
 153  simp [minkowski_ricci_zero, Finset.sum_const_zero]
 154
 155/-- Einstein tensor vanishes for Minkowski space. -/
 156theorem minkowski_einstein_zero (x : Fin 4 → ℝ) (up : Fin 0 → Fin 4) (low : Fin 2 → Fin 4) :
 157    einstein_tensor minkowski_tensor x up low = 0 := by
 158  unfold einstein_tensor
 159  simp only [minkowski_ricci_zero, minkowski_ricci_scalar_zero, mul_zero, sub_zero]
 160
 161end Geometry
 162end Relativity
 163end IndisputableMonolith

papers checked against this theorem

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