80structure FlatChain : Prop where 81 minkowski_christoffel : ∀ x ρ μ ν, 82 christoffel minkowski_tensor x ρ μ ν = 0 83 minkowski_riemann : ∀ x up low, 84 riemann_tensor minkowski_tensor x up low = 0 85 minkowski_ricci : ∀ x up low, 86 ricci_tensor minkowski_tensor x up low = 0 87 minkowski_scalar : ∀ x, 88 ricci_scalar minkowski_tensor x = 0 89 minkowski_einstein : ∀ x up low, 90 einstein_tensor minkowski_tensor x up low = 0 91 92/-- The flat chain holds. All fields proved in `Curvature.lean`. -/
used by (2)
From the project-wide theorem graph. These declarations reference this one in their body.