`BookProof.SmBrstGhost.smStruct_jacobi` {f3 : Fin 8 → Fin 8 → Fin 8 → ℝ} (h3 : ∀ a b c h : Fin 8, ∑ e, (f3 a b e * f3 e c h + f3 b c e * f3 e a h + f3 c a e * f3 e b h) = 0) (a b c

Proved

BookProof.SmBrstGhost.smStruct_jacobi

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

theoremstimepiece

Prove the following Lean 4 theorem from ChapterSmBrstGhost.

BookProof.SmBrstGhost.smStruct_jacobi {f3 : Fin 8 → Fin 8 → Fin 8 → ℝ} (h3 : ∀ a b c h : Fin 8, ∑ e, (f3 a b e * f3 e c h + f3 b c e * f3 e a h + f3 c a e * f3 e b h) = 0) (a b c h : Fin 12) : ∑ e, (smStruct f3 a b e * smStruct f3 e c h + smStruct f3 b c e * smStruct f3 e a h + smStruct f3 c a e * smStruct f3 e b h) = 0

Formalization note: Lean 4 identifier BookProof.SmBrstGhost.smStruct_jacobi.

Preamble

-- Generated from ChapterSmBrstGhost.lean — theorem BookProof.SmBrstGhost.smStruct_jacobi
import Definitions.Def_ChapterSmCarAlgebra
import Definitions.Def_ChapterBRSTNilpotent
import Definitions.Def_ChapterYangMillsSU3
import Mathlib
import Definitions.Def_ChapterSmBrstGhost
open BookProof.SmBrstGhost



open BookProof.SmCar BookProof.BRSTNilpotent BookProof.YangMillsSU3

noncomputable section

Formal statement

theorem BookProof.SmBrstGhost.smStruct_jacobi {f3 : Fin 8 → Fin 8 → Fin 8 → ℝ}
    (h3 : ∀ a b c h : Fin 8, ∑ e, (f3 a b e * f3 e c h + f3 b c e * f3 e a h
      + f3 c a e * f3 e b h) = 0) (a b c h : Fin 12) :
    ∑ e, (smStruct f3 a b e * smStruct f3 e c h + smStruct f3 b c e * smStruct f3 e a h
      + smStruct f3 c a e * smStruct f3 e b h) = 0 := by sorry

View graph