`BookProof.FreeEMField.Fbook_eq_emFieldStrength_of_commute` (δ : Fin 3 → R → R) (g : ℝ) (A : Fin 3 → R) (hcommute : ∀ j k, A j * A k = A k * A j) (j k : Fin 3) : Fbook δ g A j k =

Proved

BookProof.FreeEMField.Fbook_eq_emFieldStrength_of_commute

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

theoremstimepiece

Prove the following Lean 4 theorem from ChapterFreeEMField.

BookProof.FreeEMField.Fbook_eq_emFieldStrength_of_commute (δ : Fin 3 → R → R) (g : ℝ) (A : Fin 3 → R) (hcommute : ∀ j k, A j * A k = A k * A j) (j k : Fin 3) : Fbook δ g A j k = emFieldStrength δ A j k

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

Preamble

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



open BookProof.YangMillsFieldStrength


variable {R : Type*} [Ring R]

variable {R : Type*} [Ring R] [Algebra ℂ R]

Formal statement

theorem BookProof.FreeEMField.Fbook_eq_emFieldStrength_of_commute
    (δ : Fin 3 → R → R) (g : ℝ) (A : Fin 3 → R)
    (hcommute : ∀ j k, A j * A k = A k * A j) (j k : Fin 3) :
    Fbook δ g A j k = emFieldStrength δ A j k := by sorry

View graph