Theorem isUnit_map_of_leftInverse

Modification history