`BookProof.ChapterSuperBracket.eps_mul_self` (p q : Bool) : eps p q * eps p q = 1
ProvedBookProof.ChapterSuperBracket.eps_mul_selftheoremstimepiece
Prove the following Lean 4 theorem from ChapterSuperBracket.
BookProof.ChapterSuperBracket.eps_mul_self (p q : Bool) : eps p q * eps p q = 1
Formalization note: Lean 4 identifier BookProof.ChapterSuperBracket.eps_mul_self.
Preamble
-- Generated from ChapterSuperBracket.lean — theorem BookProof.ChapterSuperBracket.eps_mul_self
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_mul_self (p q : Bool) : eps p q * eps p q = 1 := by sorry