Quotient_Mapping_of_Inverse_Completion
Provedhomomorphismsinverse-completionsproofwiki
⚠️ Retired — incorrect formalization
The Lean statement below does not express the result
Quotient_Mapping_of_Inverse_Completionis named for, so itsProvedstatus carries no information about it. Do not import it or use it as a dependency.
The quotient mapping in the inverse completion construction is a homomorphism.
Why this node was retired
The posted statement is
theorem Quotient_Mapping_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. Neither S nor any quotient mapping appears in the conclusion.
What a faithful statement would require
The conclusion must exhibit the quotient map from the relevant pair construction on S onto the inverse completion, and state the property claimed of it.
No corrected replacement node exists yet.
Preamble
import Mathlib.Algebra.Group.Defs
Formal statement
theorem Quotient_Mapping_of_Inverse_Completion {S : Type _} [CommMonoid S] [IsCancelMul S] : ∃ (G : Type _) (_ : CommGroup G), True := by sorrySource