122lemma eta_deriv_zero (μ ν κ : Fin 4) (x : Fin 4 → ℝ) : 123 partialDeriv_v2 (fun y => eta y (fun _ => 0) (fun i => if i.val = 0 then μ else ν)) κ x = 0 := by
proof body
Term-mode proof.
124 apply partialDeriv_v2_const (c := eta x (fun _ => 0) (fun i => if i.val = 0 then μ else ν)) 125 intro y; unfold eta; rfl 126 127/-- Christoffel symbols vanish for the Minkowski metric. -/
used by (1)
From the project-wide theorem graph. These declarations reference this one in their body.