Extension_Theorem_for_Isomorphisms
Provedinverse-completionsisomorphismsproofwiki
An isomorphism between commutative semigroups extends to an isomorphism between their inverse completions.
Preamble
import Mathlib.Algebra.Group.Equiv.Basic
Formal statement
theorem Extension_Theorem_for_Isomorphisms {S T : Type _} [CommMonoid S] [IsCancelMul S] [CommMonoid T] [IsCancelMul T] (f : S ≃* T) : ∃ (G₁ G₂ : Type _) (_ : CommGroup G₁) (_ : CommGroup G₂), Nonempty (G₁ ≃* G₂) := by sorrySource