Theorem Equiv.swap_mul_involutive

Modification history