Mathlib Changelog
Changelog
About
Github
Commit
2018-01-20 17:03
bcbf0d56
View on Github →
refactor(data/complex): clean up proofs
Estimated changes
Modified
data/complex.lean
modified
def
complex.I
modified
theorem
complex.I_im
modified
theorem
complex.I_re
modified
theorem
complex.add_im
modified
theorem
complex.add_re
deleted
theorem
complex.coe_im
deleted
theorem
complex.coe_re
added
def
complex.conj
modified
theorem
complex.conj_im
added
theorem
complex.conj_of_real
modified
theorem
complex.conj_re
deleted
def
complex.conjugate
deleted
theorem
complex.eq_iff_re_eq_and_im_eq
deleted
theorem
complex.eq_of_re_eq_and_im_eq
modified
theorem
complex.eta
added
theorem
complex.ext
added
theorem
complex.ext_iff
deleted
theorem
complex.im_eq_zero_of_complex_nat
added
theorem
complex.inv_def
added
theorem
complex.inv_im
added
theorem
complex.inv_re
added
theorem
complex.inv_zero
added
theorem
complex.mk_eq_add_mul_I
added
theorem
complex.mul_conj
modified
theorem
complex.mul_im
added
theorem
complex.mul_inv_cancel
modified
theorem
complex.mul_re
modified
theorem
complex.neg_im
modified
theorem
complex.neg_re
added
def
complex.norm_sq
added
theorem
complex.norm_sq_eq_zero
added
theorem
complex.norm_sq_nonneg
added
theorem
complex.norm_sq_of_real
added
theorem
complex.norm_sq_one
added
theorem
complex.norm_sq_pos
added
theorem
complex.norm_sq_zero
deleted
def
complex.norm_squared
deleted
theorem
complex.norm_squared_pos_of_nonzero
modified
def
complex.of_real
deleted
theorem
complex.of_real_abs_squared
modified
theorem
complex.of_real_add
modified
theorem
complex.of_real_eq_coe
added
theorem
complex.of_real_eq_zero
added
theorem
complex.of_real_im
added
theorem
complex.of_real_inj
deleted
theorem
complex.of_real_injective
added
theorem
complex.of_real_int_cast
deleted
theorem
complex.of_real_int_eq_complex_int
modified
theorem
complex.of_real_inv
modified
theorem
complex.of_real_mul
added
theorem
complex.of_real_nat_cast
deleted
theorem
complex.of_real_nat_eq_complex_nat
added
theorem
complex.of_real_ne_zero
modified
theorem
complex.of_real_neg
modified
theorem
complex.of_real_one
added
theorem
complex.of_real_rat_cast
added
theorem
complex.of_real_re
modified
theorem
complex.of_real_sub
modified
theorem
complex.of_real_zero
modified
theorem
complex.one_im
modified
theorem
complex.one_re
deleted
theorem
complex.proj_im
deleted
theorem
complex.proj_re
modified
theorem
complex.sub_im
modified
theorem
complex.sub_re
modified
theorem
complex.zero_im
modified
theorem
complex.zero_re
Modified
data/real.lean
Modified
tactic/interactive.lean
Modified
tactic/ring.lean