Def MulHom.toMulEquiv

Modification history