Theorem MulEquiv.prodProdProdComm_toEquiv

Modification history