Theorem PEquiv.single_mul_single_of_ne

Modification history