Theorem mk_complex

Modification history

2023-07-03 11:03

Mathlib/Data/Complex/Cardinality.lean

fix: precedence of `#` (#5623)

Modified mk_complex View on Github →

2023-04-19 11:19

Mathlib/Data/Complex/Cardinality.lean

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

Added mk_complex View on Github →