Theorem Function.LeftInverse.right_inverse_of_surjective

Modification history