Mathlib Changelog
v3
Changelog
About
Github
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