Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2018-01-23 00:14 5fe8fbf1

View on Github →

feat(data/complex): properties of the complex absolute value function

Estimated changes

Modified algebra/field.lean

Created analysis/complex.lean

added theorem complex.dist_eq

Modified data/complex.lean

added theorem complex.abs_I

added theorem complex.abs_abs

added theorem complex.abs_add

added theorem complex.abs_conj

added theorem complex.abs_eq_zero

added theorem complex.abs_im_le_abs

added theorem complex.abs_mul

added theorem complex.abs_neg

added theorem complex.abs_nonneg

added theorem complex.abs_of_nonneg

added theorem complex.abs_of_real

added theorem complex.abs_one

added theorem complex.abs_pos

added theorem complex.abs_re_le_abs

added theorem complex.abs_sub

added theorem complex.abs_sub_le

added theorem complex.abs_zero

added theorem complex.conj_I

added theorem complex.conj_add

added theorem complex.conj_bijective

added theorem complex.conj_conj

added theorem complex.conj_div

added theorem complex.conj_eq_zero

added theorem complex.conj_inj

added theorem complex.conj_inv

added theorem complex.conj_mul

added theorem complex.conj_neg

added theorem complex.conj_one

added theorem complex.conj_zero

added theorem complex.im_le_abs

added theorem complex.im_sq_le_norm_sq

added theorem complex.mul_self_abs

added theorem complex.norm_sq_I

added theorem complex.norm_sq_add

added theorem complex.norm_sq_conj

added theorem complex.norm_sq_div

added theorem complex.norm_sq_inv

added theorem complex.norm_sq_mul

added theorem complex.norm_sq_neg

modified theorem complex.norm_sq_one

added theorem complex.norm_sq_sub

modified theorem complex.norm_sq_zero

added theorem complex.re_le_abs

added theorem complex.re_sq_le_norm_sq

Modified data/real.lean

added theorem real.sqrt_mul_self_eq_abs

added theorem real.sqrt_sqr_eq_abs