Submonoid of inverses #
Given a submonoid
N of a monoid
M, we define the submonoid
N.leftInv as the submonoid of
left inverses of
M is commutative, we may define
fromCommLeftInv : N.leftInv →* N
since the inverses are unique. When
N ≤ IsUnit.Submonoid M, this is precisely
the pointwise inverse of
N, and we may define
leftInvEquiv : S.leftInv ≃* S.
For the pointwise inverse of submonoids of groups, please refer to
Define the submonoid of right inverses and two-sided inverses. See the comments of #10679 for a possible implementation.