Merge pull request leanprover-community#128 from leanprover-community…

…/profinite_rename
maXXusXYZ · Oct 12, 2022 · ebb498c · ebb498c
2 parents 13777e1 + 9c6f277
commit ebb498c
Showing 1 changed file with 10 additions and 0 deletions.
diff --git a/src/examples/profinite.lean → src/examples/cond.lean b/src/examples/profinite.lean → src/examples/cond.lean
@@ -1,5 +1,15 @@
 import challenge
 
+/-!
+
+The main goal of this file is to discuss the definition of
+condensed abelian groups which is used in this project.
+
+As prerequisites, we also discuss continuous maps and the
+category of profinite sets.
+
+-/
+
 open category_theory category_theory.limits opposite
 open_locale liquid_tensor_experiment