`BookProof.SmBrstGhost.su2Struct_jacobi` (a b c h : Fin 3) : ∑ e, (su2Struct a b e * su2Struct e c h + su2Struct b c e * su2Struct e a h + su2Struct c a e * su2Struct e b h) = 0

Initializing...

`BookProof.SmBrstGhost.su2Struct_jacobi` (a b c h : Fin 3) : ∑ e, (su2Struct a b e * su2Struct e c h + su2Struct b c e * su2Struct e a h + su2Struct c a e * su2Struct e b h) = 0 · Prove2Me