Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-06-12 11:43 f78693db

View on Github →

chore(data/complex/exponential): linting and pp_nodot (#3045)

Estimated changes

modified def complex.cos
modified def complex.cosh
modified def complex.exp'
modified def complex.exp
modified theorem complex.is_cau_exp
modified def complex.sin
modified def complex.sinh
modified def complex.tan
modified def complex.tanh
modified theorem is_cau_geo_series_const
modified theorem is_cau_series_of_abv_le_cau
modified def real.cos
modified theorem real.cos_bound
modified def real.cosh
modified def real.exp
modified def real.sin
modified theorem real.sin_bound
modified def real.sinh
modified def real.tan
modified def real.tanh