Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-10-18 19:21 93b7e635

View on Github →

feat(analysis/special_functions/trigonometric): range_{exp,cos,sin} (#4595)

Estimated changes

Modified src/algebra/ordered_ring.lean

Modified src/algebra/quadratic_discriminant.lean

Modified src/analysis/special_functions/exp_log.lean

added theorem real.log_surjective

added theorem real.range_exp

added theorem real.range_log

Modified src/analysis/special_functions/trigonometric.lean

added theorem complex.cos_surjective

added theorem complex.exists_eq_mul_self

added theorem complex.exists_pow_nat_eq

added theorem complex.range_cos

added theorem complex.range_exp

added theorem complex.range_sin

added theorem complex.sin_surjective

added theorem real.range_cos_infinite

added theorem real.range_sin_infinite

Modified src/data/set/finite.lean

added theorem set.infinite_of_infinite_image