diff --git a/src/data/rat/denumerable.lean b/src/data/rat/denumerable.lean
index e4a435c7d012b..ccc33d5296dd2 100644
--- 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