`BookProof.ChapterSE2.se2_coef_11` : mgamma5Z * mgammaZ 1 * (mgammaZ 0 + mgammaZ 3) * (mgamma5Z * mgammaZ 1 * (mgammaZ 0 + mgammaZ 3)) = 0
ProvedBookProof.ChapterSE2.se2_coef_11theoremstimepiece
Prove the following Lean 4 theorem from ChapterSE2.
BookProof.ChapterSE2.se2_coef_11 : mgamma5Z * mgammaZ 1 * (mgammaZ 0 + mgammaZ 3) * (mgamma5Z * mgammaZ 1 * (mgammaZ 0 + mgammaZ 3)) = 0
Formalization note: Lean 4 identifier BookProof.ChapterSE2.se2_coef_11.
Preamble
-- Generated from ChapterSE2.lean — theorem BookProof.ChapterSE2.se2_coef_11 import Mathlib import Definitions.Def_ChapterSE2 import Definitions.Def_ChapterA3 open BookProof.ChapterA3 open BookProof.ChapterSE2 open Matrix open BookProof.ChapterA3
Formal statement
theorem BookProof.ChapterSE2.se2_coef_11 :
mgamma5Z * mgammaZ 1 * (mgammaZ 0 + mgammaZ 3) *
(mgamma5Z * mgammaZ 1 * (mgammaZ 0 + mgammaZ 3)) = 0 := by sorry