Identity_of_Inverse_Completion_of_Commutative_Monoid

⚠️ Retired — incorrect formalization

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

The identity of the monoid maps to the identity of its inverse completion.

Why this node was retired

The posted statement is

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

The goal is ∃ (G : Type _) (_ : CommGroup G), True, asserting only that a commutative group exists — PUnit witnesses it. The monoid M never appears in the conclusion, so nothing is said about its inverse completion or the identity thereof.

What a faithful statement would require

The conclusion must relate G to M — a monoid homomorphism M →* G that is universal among maps from M into groups — and then state the property being claimed of its identity.

No corrected replacement node exists yet.