Def Condensed.forget

Modification history

2024-05-01 09:30

Mathlib/Condensed/Module.lean

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

Added Condensed.forget View on Github →