Mathlib v3 is deprecated. Go to Mathlib v4

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