Theorem Commute.mul_inv_eq_mul_inv_iff_of_isUnit

Modification history