# mathlibdocumentation

data.complex.cardinality

# The cardinality of the complex numbers #

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

@[simp]
theorem mk_complex  :

The cardinality of the complex numbers, as a type.

@[simp]

The cardinality of the complex numbers, as a set.

The complex numbers are not countable.