Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2019-01-27 22:37 19c2f68c

View on Github →

feat(analysis/exponential): complex powers

Estimated changes

Modified src/analysis/exponential.lean

added theorem complex.exp_eq_exp_iff_exists_int

added theorem complex.exp_eq_exp_iff_exp_sub_eq_one

added theorem complex.exp_eq_one_iff

added theorem complex.pow_add

added theorem complex.pow_def

added theorem complex.pow_int_cast

added theorem complex.pow_mul

added theorem complex.pow_nat_cast

added theorem real.log_mul