Theorem Function.injective_of_partial_inv_right

Modification history