`BookProof.SmBrstGhost.u1Struct_jacobi` (a b c h : Fin 1) : ∑ e, (u1Struct a b e * u1Struct e c h + u1Struct b c e * u1Struct e a h + u1Struct c a e * u1Struct e b h) = 0

Initializing...

`BookProof.SmBrstGhost.u1Struct_jacobi` (a b c h : Fin 1) : ∑ e, (u1Struct a b e * u1Struct e c h + u1Struct b c e * u1Struct e a h + u1Struct c a e * u1Struct e b h) = 0 · Prove2Me