Def AdicCompletion.map

Modification history

2026-02-24 10:38

Mathlib/RingTheory/AdicCompletion/Functoriality.lean

chore: bump toolchain to v4.29.0-rc2 (#35708)

Modified AdicCompletion.map View on Github →

2026-02-23 19:12

Mathlib/RingTheory/AdicCompletion/Functoriality.lean

chore(RingTheory/AdicCompletion): update the definition of `AdicCompletion.map` (#35595) …

Modified AdicCompletion.map View on Github →

2024-06-11 14:59

Mathlib/RingTheory/AdicCompletion/Functoriality.lean

feat(RingTheory/AdicCompletion): functoriality (#12543) …

Added AdicCompletion.map View on Github →