`BookProof.ChapterSuperBracket.eps_comm` (p q : Bool) : eps p q = eps q p
ProvedBookProof.ChapterSuperBracket.eps_commtheoremstimepiece
Prove the following Lean 4 theorem from ChapterSuperBracket.
BookProof.ChapterSuperBracket.eps_comm (p q : Bool) : eps p q = eps q p
Formalization note: Lean 4 identifier BookProof.ChapterSuperBracket.eps_comm.
Preamble
-- Generated from ChapterSuperBracket.lean — theorem BookProof.ChapterSuperBracket.eps_comm
import Mathlib
import Definitions.Def_ChapterSuperBracket
import Definitions.Def_ChapterElectroweakFieldStrength
open BookProof.ChapterElectroweakFieldStrength
open BookProof.ChapterSuperBracket
variable {R : Type*} [Ring R]Formal statement
theorem BookProof.ChapterSuperBracket.eps_comm (p q : Bool) : eps p q = eps q p := by sorry