Theorem AlgEquiv.piCongrLeft_apply

Modification history