Left and right inverse of function

Stream: Is there code for X?

[Pedro Minicz]

Is there a definition like the following in mathlib?

variables {α : Type*} {β : Type*}

def inverse (g : β → α) (f : α → β) : Prop :=
  function.left_inverse g f ∧ function.right_inverse g f

I believe there should be one in logic.function.basic, but I can't it.

[Adam Topaz]

You can probably get what you need with docs#equiv