Inverse_Completion_of_Commutative_Semigroup_is_Inverse_Completion_of_Itself
Provedcommutative-semigroupsinverse-completionsproofwiki
The inverse completion of a commutative group is itself; every element already has an inverse.
Preamble
import Mathlib.Algebra.Group.Defs
Formal statement
theorem Inverse_Completion_of_Commutative_Semigroup_is_Inverse_Completion_of_Itself {G : Type _} [CommGroup G] (g : G) : ∃ h : G, g * h = 1 := by sorrySource