Commit 2024-05-01 09:30 154a87cd

View on Github →

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

Estimated changes

Modified Mathlib.lean

Deleted Mathlib/Condensed/Abelian.lean

Deleted Mathlib/Condensed/Adjunctions.lean

deleted def Condensed.abForget

deleted def Condensed.freeAb

deleted def Condensed.setAbAdjunction

Modified Mathlib/Condensed/Explicit.lean

Modified Mathlib/Condensed/Limits.lean

Modified Mathlib/Condensed/Module.lean

added def Condensed.forget

added def Condensed.free

added def Condensed.freeForgetAdjunction

Modified Mathlib/Condensed/Solid.lean

modified def Condensed.profiniteSolid

modified def Condensed.profiniteSolidification