feat(analysis/special_functions/pow): exp_mul (#4409)

Add the lemma that `exp (x * y) = (exp x) ^ y`, for real `x` and `y`.

src/analysis/special_functions/pow.lean

@@ -141,6 +141,9 @@ by simp only [rpow_def, complex.cpow_def];
 lemma rpow_def_of_pos {x : ℝ} (hx : 0 < x) (y : ℝ) : x ^ y = exp (log x * y) :=
 by rw [rpow_def_of_nonneg (le_of_lt hx), if_neg (ne_of_gt hx)]
 
+lemma exp_mul (x y : ℝ) : exp (x * y) = (exp x) ^ y :=
+by rw [rpow_def_of_pos (exp_pos _), log_exp]
+
 lemma rpow_eq_zero_iff_of_nonneg {x y : ℝ} (hx : 0 ≤ x) : x ^ y = 0 ↔ x = 0 ∧ y ≠ 0 :=
 by { simp only [rpow_def_of_nonneg hx], split_ifs; simp [*, exp_ne_zero] }