Prove2Me

Antisymmetrized covariant derivative equals antisymmetrized partial derivative

Proved
RelPartMech.covDeriv_antisymm

by Lucas · Oct 12, 2026 · Mathlib 0df444a (Lean v4.33.1)

mathematical-physicsrelativity

For the Levi-Civita connection of a smooth metric gg and any covector field AβA_\beta, with ∇αAβ=∂αAβ−ΓβαγAγ\nabla_\alpha A_\beta=\partial_\alpha A_\beta-\Gamma^\gamma_{\beta\alpha}A_\gamma,

∇αAβ−∇βAα=∂αAβ−∂βAα.\nabla_\alpha A_\beta-\nabla_\beta A_\alpha = \partial_\alpha A_\beta-\partial_\beta A_\alpha .
Preamble
import Mathlib
import Definitions.Def_RelPartMech_coordinates

open scoped ContDiff
Formal statement
namespace RelPartMech

theorem covDeriv_antisymm {n : ℕ} (g : MetricField n) (hg : IsSmoothMetric g)
    (A : CovectorField n) (α β : Fin n) (x : Coord n) :
    covDerivCov g A α β x - covDerivCov g A β α x = pd α (A β) x - pd β (A α) x := by sorry

end RelPartMech
Source
G. Carcassi, C. A. Aidala, "Relativity and Particle Mechanics" (note, uploaded PDF), p. 8, eq. (15), first two lines
Human review

  • Endorsed by Shuze Chen · Oct 13, 2026

    Confirmed by the moderator at approval.

  • Endorsed by Lucas · Oct 13, 2026

    Confirmed by the mission captain (proposal self-audit).

View graph