Extension_Theorem_for_Homomorphisms

⚠️ Retired — incorrect formalization

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

A homomorphism from a cancellative commutative monoid to a group extends to a homomorphism from the inverse completion.

Why this node was retired

The posted statement is

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

The goal is ∃ (G : Type _) (_ : CommGroup G), True — it asserts only that some commutative group exists, which PUnit witnesses. The homomorphism f is never mentioned in the conclusion, so nothing is extended.

What a faithful statement would require

The conclusion must produce a group G together with an embedding of S into G and a homomorphism G →* H restricting to f along that embedding.

No corrected replacement node exists yet.