cos_add_sin_mul_I_pow — Mathlib

English

For n ∈ ℕ and z ∈ ℂ, (cos z + i sin z)^n = cos(nz) + i sin(nz).

Русский

Для любого n ∈ ℕ и z ∈ ℂ выполняется (cos z + i sin z)^n = cos(nz) + i sin(nz).

LaTeX

$$$\\forall n \\in \\mathbb{N}, \\forall z \\in \\mathbb{C},\\; (\\cos z + i \\sin z)^n = \\cos(nz) + i \\sin(nz)$$$

Lean4

/-- **De Moivre's formula** -/
theorem cos_add_sin_mul_I_pow (n : ℕ) (z : ℂ) : (cos z + sin z * I) ^ n = cos (↑n * z) + sin (↑n * z) * I := by
  rw [← exp_mul_I, ← exp_mul_I, ← exp_nat_mul, mul_assoc]

Похожие утверждения