Commit 2026-10-19 22:29 d4acc3be

View on Github →

chore: additivize the profinite completion (#44627) The plan is to use this to define ZHat as the profinite completion of ℤ.

Estimated changes

Modified Mathlib/Topology/Algebra/Category/ProfiniteGrp/Completion.lean

deleted def ProfiniteGrp.ProfiniteCompletion.adjunction

deleted def ProfiniteGrp.ProfiniteCompletion.homEquiv

deleted def ProfiniteGrp.ProfiniteCompletion.lift

Modified Mathlib/Topology/Algebra/Category/ProfiniteGrp/Limits.lean

deleted theorem ProfiniteGrp.denseRange_toLimit