Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2018-01-23 03:30 acb9093f

View on Github →

feat(analysis/complex): complex numbers are a top ring

Estimated changes

Modified analysis/complex.lean

added theorem complex.continuous_abs

added theorem complex.continuous_inv'

added theorem complex.continuous_inv

added theorem complex.continuous_mul

modified theorem complex.dist_eq

added theorem complex.tendsto_inv

added theorem complex.uniform_continuous_abs

added theorem complex.uniform_continuous_add

added theorem complex.uniform_continuous_inv

added theorem complex.uniform_continuous_mul

added theorem complex.uniform_continuous_mul_const

added theorem complex.uniform_continuous_neg

Modified data/complex.lean

added theorem complex.abs_abs_sub_le_abs_sub

Modified data/real/cau_seq.lean

added theorem is_absolute_value.abs_abv_sub_le_abv_sub

added theorem is_absolute_value.sub_abv_le_abv_sub