Theorem mul_inv_eq_mul_inv_iff_mul_eq_mul

Modification history