`BookProof.FreeEMField.emFieldStrength_gauge_invariant` (δ : Fin 3 → R → R) (A : Fin 3 → R) (θ : R) (hadd : ∀ j x y, δ j (x + y) = δ j x + δ j y) (hcomm : ∀ j k x, δ j (δ k x) = δ

Proved

BookProof.FreeEMField.emFieldStrength_gauge_invariant

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

theoremstimepiece

Prove the following Lean 4 theorem from ChapterFreeEMField.

BookProof.FreeEMField.emFieldStrength_gauge_invariant (δ : Fin 3 → R → R) (A : Fin 3 → R) (θ : R) (hadd : ∀ j x y, δ j (x + y) = δ j x + δ j y) (hcomm : ∀ j k x, δ j (δ k x) = δ k (δ j x)) (j k : Fin 3) : emFieldStrength δ (fun i => A i + δ i θ) j k = emFieldStrength δ A j k

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

Preamble

-- Generated from ChapterFreeEMField.lean — theorem BookProof.FreeEMField.emFieldStrength_gauge_invariant
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_gauge_invariant
    (δ : Fin 3 → R → R) (A : Fin 3 → R) (θ : R)
    (hadd : ∀ j x y, δ j (x + y) = δ j x + δ j y)
    (hcomm : ∀ j k x, δ j (δ k x) = δ k (δ j x))
    (j k : Fin 3) :
    emFieldStrength δ (fun i => A i + δ i θ) j k = emFieldStrength δ A j k := by sorry

View graph