Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2018-01-07 14:32 5ff51dc6

View on Github →

feat(analysis/complex): complex numbers as a field

Estimated changes

added def complex.I
added theorem complex.I_im
added theorem complex.I_re
added theorem complex.add_im
added theorem complex.add_re
added theorem complex.coe_im
added theorem complex.coe_re
added theorem complex.conj_im
added theorem complex.conj_re
added theorem complex.eta
added theorem complex.mul_im
added theorem complex.mul_re
added theorem complex.neg_im
added theorem complex.neg_re
added def complex.of_real
added theorem complex.of_real_add
added theorem complex.of_real_eq_coe
added theorem complex.of_real_inv
added theorem complex.of_real_mul
added theorem complex.of_real_neg
added theorem complex.of_real_one
added theorem complex.of_real_sub
added theorem complex.of_real_zero
added theorem complex.one_im
added theorem complex.one_re
added theorem complex.proj_im
added theorem complex.proj_re
added theorem complex.sub_im
added theorem complex.sub_re
added theorem complex.zero_im
added theorem complex.zero_re
added structure complex