`BookProof.YangMillsAbelianNoGap.vsel_idxD` (v₁ v₂ : ℝ) (j k : Fin 3) (a : Fin 8) : vsel v₁ v₂ (idxD j k a) = v₂

Initializing...

`BookProof.YangMillsAbelianNoGap.vsel_idxD` (v₁ v₂ : ℝ) (j k : Fin 3) (a : Fin 8) : vsel v₁ v₂ (idxD j k a) = v₂ · Prove2Me