cos_three_mul — Mathlib

English

For any 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

theorem cos_three_mul : cos (3 * x) = 4 * cos x ^ 3 - 3 * cos x :=
  by
  have h1 : x + 2 * x = 3 * x := by ring
  rw [← h1, cos_add x (2 * x)]
  simp only [cos_two_mul, sin_two_mul, mul_sub, mul_one, sq]
  have h2 : 4 * cos x ^ 3 = 2 * cos x * cos x * cos x + 2 * cos x * cos x ^ 2 := by ring
  rw [h2, cos_sq']
  ring

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