exponential function to a natural power

Stream: Is there code for X?

[Mark Andrew Gerads]

This should definitely be in mathlib (I need it), but library_search! is not finding it.

lemma expPowEqExpMul (z:ℂ) (n : ℕ) : exp (z) ^ n = exp (z * n) :=
begin
  induction n with n ih,
  simp only [pow_zero, nat.cast_zero, mul_zero, complex.exp_zero],
  rw [pow_succ],
  rw (show (n.succ:ℂ) = n + 1, by {simp} ),
  rw (show (z * (n + 1)) = z + z * n, by {ring} ),
  rw complex.exp_add z _,
  congr,
  exact ih,
end

[Moritz Doll]

docs#complex.exp_nat_mul

[Moritz Doll]

modulo symmetry and commuting factors

[Eric Wieser]

Or docs#exp_nsmul