Skip to content

Commit 6d2b39c

Browse files
kim-emadamtopaz
andcommitted
feat: port Topology.Category.Profinite.Basic (#3705)
Co-authored-by: Scott Morrison <scott.morrison@gmail.com> Co-authored-by: adamtopaz <github@adamtopaz.com>
1 parent c27be72 commit 6d2b39c

File tree

2 files changed

+429
-0
lines changed

2 files changed

+429
-0
lines changed

Mathlib.lean

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -1931,6 +1931,7 @@ import Mathlib.Topology.Bornology.Hom
19311931
import Mathlib.Topology.Category.Born
19321932
import Mathlib.Topology.Category.CompHaus.Basic
19331933
import Mathlib.Topology.Category.CompHaus.Projective
1934+
import Mathlib.Topology.Category.Profinite.Basic
19341935
import Mathlib.Topology.Category.Top.Adjunctions
19351936
import Mathlib.Topology.Category.Top.Basic
19361937
import Mathlib.Topology.Category.Top.EpiMono

0 commit comments

Comments
 (0)