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

Created analysis/complex.lean

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 def complex.conjugate

added theorem complex.eq_iff_re_eq_and_im_eq

added theorem complex.eq_of_re_eq_and_im_eq

added theorem complex.eta

added theorem complex.im_eq_zero_of_complex_nat

added theorem complex.mul_im

added theorem complex.mul_re

added theorem complex.neg_im

added theorem complex.neg_re

added def complex.norm_squared

added theorem complex.norm_squared_pos_of_nonzero

added def complex.of_real

added theorem complex.of_real_abs_squared

added theorem complex.of_real_add

added theorem complex.of_real_eq_coe

added theorem complex.of_real_injective

added theorem complex.of_real_int_eq_complex_int

added theorem complex.of_real_inv

added theorem complex.of_real_mul

added theorem complex.of_real_nat_eq_complex_nat

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