Commit 2026-04-11 08:45 e0793673

View on Github →

chore(Condensed): make Condensed an abbrev (#37823)

Estimated changes

Modified Mathlib/CategoryTheory/Limits/Shapes/Countable.lean

Modified Mathlib/CategoryTheory/Limits/Shapes/SequentialProduct.lean

Modified Mathlib/Condensed/Basic.lean

deleted def Condensed

Modified Mathlib/Condensed/CartesianClosed.lean

Modified Mathlib/Condensed/Discrete/Characterization.lean

Modified Mathlib/Condensed/Epi.lean

Modified Mathlib/Condensed/Light/Basic.lean

deleted def LightCondensed

Modified Mathlib/Condensed/Light/CartesianClosed.lean

Modified Mathlib/Condensed/Light/Epi.lean

Modified Mathlib/Condensed/Light/Functors.lean

Modified Mathlib/Condensed/Light/InternallyProjective.lean

Modified Mathlib/Condensed/Light/Limits.lean

Modified Mathlib/Condensed/Light/Monoidal.lean