lemma proved term proof

`basisVec_ne`

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

formal statement (Lean)

  16@[simp] lemma basisVec_ne {μ ν : Fin 4} (h : ν ≠ μ) : basisVec μ ν = 0 := by

Term-mode proof.

  17  simp [basisVec, h]
  18
  19/-- Coordinate ray `x + t e_μ`. -/

From the project-wide theorem graph. These declarations reference this one in their body.

deriv_coordRay_j in IndisputableMonolith.Relativity.Calculus.Derivatives decl_use
partialDeriv_v2_x_sq in IndisputableMonolith.Relativity.Calculus.Derivatives decl_use

Lean names referenced from this declaration's body.