Def Condensed.freeForgetAdjunction

Modification history

2024-05-01 09:30

Mathlib/Condensed/Module.lean

refactor(Condensed): redefine condensed abelian groups as condensed `ℤ`-modules (#12510)

Added Condensed.freeForgetAdjunction View on Github →