Theorem Equiv.Perm.mulLeft_mul

Modification history