74theorem einstein_flat (mu nu : Idx) : 75 einstein_tensor minkowski minkowski_inverse 76 (fun _ _ _ => 0) (fun _ _ _ _ => 0) mu nu = 0 := by
proof body
Term-mode proof.
77 simp [einstein_tensor, ricci_flat, scalar_flat] 78 79/-- Einstein tensor is symmetric when the Ricci tensor is symmetric 80 (which holds when the connection is torsion-free). -/
used by (5)
From the project-wide theorem graph. These declarations reference this one in their body.