Theorem isUnit_iff_exists_inv'

Modification history