Mathlib v3 is deprecated. Go to Mathlib v4

Theorem complex.I_ne_zero

Modification history

2018-11-05 05:03
data/complex/basic.lean
feat(data/complex/basic): I_ne_zero and cast_re, cast_im lemmas
Added complex.I_ne_zeroView on Github →