Theorem inv_mul_eq_iff_eq_mul

Modification history