Def Condensed.abForget

Modification history

2024-05-01 09:30
Mathlib/Condensed/Adjunctions.lean
refactor(Condensed): redefine condensed abelian groups as condensed `ℤ`-modules (#12510)
Deleted Condensed.abForgetView on Github →
2023-11-16 20:59
Mathlib/Condensed/Adjunctions.lean
feat(Condensed): adjunctions between categories of condensed objects (#8210) …
Added Condensed.abForgetView on Github →