`BookProof.FreeEMField.emFieldStrength_antisymm` (δ : Fin 3 → R → R) (A : Fin 3 → R) (j k : Fin 3) : emFieldStrength δ A j k = - emFieldStrength δ A k j

Proved

BookProof.FreeEMField.emFieldStrength_antisymm

by leonardopedro · Oct 8, 2026 · Mathlib 0df444a (Lean v4.33.1)

theoremstimepiece

Prove the following Lean 4 theorem from ChapterFreeEMField.

BookProof.FreeEMField.emFieldStrength_antisymm (δ : Fin 3 → R → R) (A : Fin 3 → R) (j k : Fin 3) : emFieldStrength δ A j k = - emFieldStrength δ A k j

Formalization note: Lean 4 identifier BookProof.FreeEMField.emFieldStrength_antisymm.

Preamble

-- Generated from ChapterFreeEMField.lean — theorem BookProof.FreeEMField.emFieldStrength_antisymm
import Definitions.Def_ChapterYangMillsFieldStrength
import Mathlib
import Definitions.Def_ChapterFreeEMField
open BookProof.FreeEMField



open BookProof.YangMillsFieldStrength


variable {R : Type*} [Ring R]

Formal statement

theorem BookProof.FreeEMField.emFieldStrength_antisymm (δ : Fin 3 → R → R) (A : Fin 3 → R) (j k : Fin 3) :
    emFieldStrength δ A j k = - emFieldStrength δ A k j := by sorry

View graph