English
There is a multiplicative equivalence between S.leftInv and S, given by a ↦ S.fromLeftInv a, with inverse provided by (hS).leftInvEquiv. This isomorphism under the hypothesis that S ≤ IsUnit.submonoid M.
Русский
Существуют перемножимые эквиваленты между S.leftInv и S: а ↦ S.fromLeftInv a, с обратной картой, задаваемой S.leftInvEquiv, существующей при условии S ≤ IsUnit.submonoid M.
LaTeX
$$$ S.leftInv \\simeq* S $$$
Lean4
/-- The submonoid of pointwise inverse of `S` is `MulEquiv` to `S`. -/
@[to_additive (attr := simps apply) /-- The additive submonoid of pointwise additive inverse of `S`
is `AddEquiv` to `S`. -/
]
noncomputable def leftInvEquiv : S.leftInv ≃* S :=
{ S.fromCommLeftInv with
invFun := fun x ↦ ⟨↑(hS x.2).unit⁻¹, x, by simp⟩
left_inv := by
intro x
ext
simp [← Units.mul_eq_one_iff_inv_eq]
right_inv := by
rintro ⟨x, hx⟩
ext
simp [fromLeftInv_eq_iff] }
