Theorem AlgEquiv.arrowCongr_trans

Modification history