Theorem IsUnit.isUnit_iff_mulLeft_bijective

Modification history