initial commit

leanprover-community · Jun 13, 2021 · eac161c · eac161c
1 parent 6d2a051
commit eac161c
Showing 1 changed file with 6 additions and 0 deletions.
diff --git a/src/data/rat/denumerable.lean b/src/data/rat/denumerable.lean
@@ -6,6 +6,12 @@ Authors: Chris Hughes
 import data.rat
 import set_theory.cardinal
 
+/-!
+# Denumerability of ℚ
+
+This file proves that ℚ is infinite, denumerable, and deduces that it has cardinality `omega`.
+-/
+
 namespace rat
 open denumerable