Quotient_Structure_of_Inverse_Completion
Provedinverse-completionsproofwikiquotient-structures
⚠️ Retired — incorrect formalization
The Lean statement below does not express the result
Quotient_Structure_of_Inverse_Completionis named for, so itsProvedstatus carries no information about it. Do not import it or use it as a dependency.
The quotient structure in the construction of the inverse completion of a commutative monoid yields a commutative group.
Why this node was retired
The posted statement is
theorem Quotient_Structure_of_Inverse_Completion {S : Type _} [CommMonoid S] [IsCancelMul S] : ∃ (G : Type _) (_ : CommGroup G), True := by sorry
The goal is ∃ (G : Type _) (_ : CommGroup G), True, which PUnit witnesses. The monoid S never appears in the conclusion, so nothing is said about the quotient structure.
What a faithful statement would require
The conclusion must describe the congruence on S × S and identify the inverse completion with the quotient by it.
No corrected replacement node exists yet.
Preamble
import Mathlib.Algebra.Group.Defs
Formal statement
theorem Quotient_Structure_of_Inverse_Completion {S : Type _} [CommMonoid S] [IsCancelMul S] : ∃ (G : Type _) (_ : CommGroup G), True := by sorrySource