Theorem Equiv.mul_swap_mul_self

Modification history