Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-11-05 17:51 cc59673b

View on Github →

chore(complex): add a few simp lemmas (#10187)

Estimated changes

Modified src/analysis/special_functions/trigonometric/basic.lean

added theorem complex.exp_add_pi_mul_I

modified theorem complex.exp_int_mul_two_pi_mul_I

modified theorem complex.exp_nat_mul_two_pi_mul_I

modified theorem complex.exp_pi_mul_I

added theorem complex.exp_sub_pi_mul_I

modified theorem complex.exp_two_pi_mul_I

Modified src/data/complex/basic.lean

added theorem complex.norm_sq_mk

Modified src/data/complex/exponential.lean

added theorem complex.exp_of_real_mul_I_im

added theorem complex.exp_of_real_mul_I_re