Inverse_Completion_Theorem

⚠️ Retired — incorrect formalization

The Lean statement below does not express the result Inverse_Completion_Theorem is named for, so its Proved status carries no information about it. Do not import it or use it as a dependency.

Every commutative monoid with cancellation embeds into a commutative group (its inverse completion).

Why this node was retired

The posted statement is

theorem Inverse_Completion_Theorem {S : Type _} [CommMonoid S] [IsCancelMul S] : ∃ (G : Type _) (_ : CommGroup G), True := by sorry

The goal is ∃ (G : Type _) (_ : CommGroup G), True, asserting only that some commutative group exists, witnessed by PUnit. The monoid S does not appear in the conclusion.

What a faithful statement would require

The conclusion must produce a group G together with an injective monoid homomorphism S →* G whose image generates G, i.e. the actual inverse completion.

No corrected replacement node exists yet.