We read every piece of feedback, and take your input very seriously.
To see all available qualifiers, see our documentation.
1 parent 660a83c commit 5f502f1Copy full SHA for 5f502f1
Mathlib.lean
@@ -3606,6 +3606,7 @@ public import Mathlib.Condensed.Light.InternallyProjective
3606
public import Mathlib.Condensed.Light.Limits
3607
public import Mathlib.Condensed.Light.Module
3608
public import Mathlib.Condensed.Light.Monoidal
3609
+public import Mathlib.Condensed.Light.Sequence
3610
public import Mathlib.Condensed.Light.Small
3611
public import Mathlib.Condensed.Light.TopCatAdjunction
3612
public import Mathlib.Condensed.Light.TopComparison
0 commit comments