English
The complex exponential respects addition: exp(x+y) = exp(x) exp(y).
Русский
Комплексная экспонента сохраняет сложение: exp(x+y) = exp(x) exp(y).
LaTeX
$$$\\forall x,y\\in\\mathbb{C},\\; \\exp(x+y) = \\exp(x)\\exp(y)$$$
Lean4
theorem exp_add : exp (x + y) = exp x * exp y :=
by
have hj :
∀ j : ℕ,
(∑ m ∈ range j, (x + y) ^ m / m.factorial) =
∑ i ∈ range j, ∑ k ∈ range (i + 1), x ^ k / k.factorial * (y ^ (i - k) / (i - k).factorial) :=
by
intro j
refine Finset.sum_congr rfl fun m _ => ?_
rw [add_pow, div_eq_mul_inv, sum_mul]
refine Finset.sum_congr rfl fun I hi => ?_
have h₁ : (m.choose I : ℂ) ≠ 0 :=
Nat.cast_ne_zero.2 (pos_iff_ne_zero.1 (Nat.choose_pos (Nat.le_of_lt_succ (mem_range.1 hi))))
have h₂ := Nat.choose_mul_factorial_mul_factorial (Nat.le_of_lt_succ <| Finset.mem_range.1 hi)
rw [← h₂, Nat.cast_mul, Nat.cast_mul, mul_inv, mul_inv]
simp only [mul_left_comm (m.choose I : ℂ), mul_assoc, mul_left_comm (m.choose I : ℂ)⁻¹, mul_comm (m.choose I : ℂ)]
rw [inv_mul_cancel₀ h₁]
simp [div_eq_mul_inv, mul_assoc, mul_left_comm]
simp_rw [exp, exp', lim_mul_lim]
apply (lim_eq_lim_of_equiv _).symm
simp only [hj]
exact cauchy_product (isCauSeq_norm_exp x) (isCauSeq_exp y)
