Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-03-24 04:46 7967128a

View on Github →

feat(data/complex/basic): #ℂ = 𝔠 (#12871)

Estimated changes

added theorem mk_complex
added theorem mk_univ_complex
added theorem not_countable_complex