111 fun x up low => 112 ricci_tensor g x up low - (1/2 : ℝ) * g.g x up low * ricci_scalar g x 113 114/-! The previous `ricci_tensor_symmetric'` wrapper depended on the deleted 115`ricci_tensor_symmetric` axiom. Use `RiemannSymmetries.ricci_tensor_symmetric_proof` 116(which takes the trace-vanishing hypothesis explicitly) or 117`RiemannSymmetries.curvature_axioms_hold` (bundled). -/ 118 119/-! ## Minkowski Space Theorems -/ 120 121/-- The Minkowski metric η doesn't depend on x, so its derivatives vanish. -/
used by (10)
From the project-wide theorem graph. These declarations reference this one in their body.