Commit 2026-02-23 19:12 82ad9869
View on Github →chore(RingTheory/AdicCompletion): update the definition of AdicCompletion.map (#35595)
This PR extracts the change of the definition of AdicCompletion.map from #34936.
@Thmoas-Guan expressed interest in using this result, so I am splitting it out here to unblock it.