Documentation
Mathlib
.
SetTheory
.
Cardinal
.
Rat
Search
return to top
source
Imports
Init
Mathlib.Algebra.CharZero.Infinite
Mathlib.Algebra.Ring.Rat
Mathlib.Data.Rat.Encodable
Mathlib.SetTheory.Cardinal.Basic
Imported by
Cardinal
.
mkRat
Cardinality of ℚ
#
This file proves that the Cardinality of ℚ is ℵ₀
source
theorem
Cardinal
.
mkRat
:
mk
ℚ
=
aleph0