Theorem PEquiv.single_mul_single

Modification history