Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2018-11-05 05:03 f00ed774

View on Github →

feat(data/complex/basic): I_ne_zero and cast_re, cast_im lemmas

Estimated changes

added theorem complex.I_ne_zero
added theorem complex.int_cast_im
added theorem complex.int_cast_re
added theorem complex.nat_cast_im
added theorem complex.nat_cast_re
added theorem complex.rat_cast_im
added theorem complex.rat_cast_re