# The cardinality of the complex numbers #

This file shows that the complex numbers have cardinality continuum, i.e. `#ℂ = 𝔠`.

source
@[simp]
theorem Cardinal.mk_complex :
mk ℂ = continuum

The cardinality of the complex numbers, as a type.

source
theorem Cardinal.mk_univ_complex :
mk ↑Set.univ = continuum

The cardinality of the complex numbers, as a set.

source
theorem not_countable_complex :
¬Set.univ.Countable

The complex numbers are not countable.