Mathlib.Data.Rat.Denumerable
source
This file proves that ℚ is infinite, denumerable, and deduces that it has cardinality omega.
omega
Denumerability of the Rational Numbers