`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) = δ

Initializing...

`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) = δ · Prove2Me