Def StarRingEquiv.ofStarRingHom

Modification history