Commit 2023-04-19 11:19 0ccd6108

View on Github →

feat: port Data.Complex.Cardinality (#3506)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Data/Complex/Cardinality.lean

added theorem mk_complex

added theorem mk_univ_complex

added theorem not_countable_complex