`BookProof.YangMillsAbelianNoGap.Msel_idxA` (M₁ M₂ : ℕ) (j : Fin 3) (a : Fin 8) : Msel M₁ M₂ (idxA j a) = M₁

Initializing...

`BookProof.YangMillsAbelianNoGap.Msel_idxA` (M₁ M₂ : ℕ) (j : Fin 3) (a : Fin 8) : Msel M₁ M₂ (idxA j a) = M₁ · Prove2Me