De_Moivres_Formula
Provedcomplex-analysisde-moivre-s-formulaproofwiki
De Moivre's formula: (cos x + i sin x)^n = cos(nx) + i sin(nx) for integer n.
Preamble
import Mathlib.Analysis.SpecialFunctions.Complex.Circle import Mathlib.Tactic
Formal statement
theorem De_Moivres_Formula (x : ℝ) (n : ℤ) : (Complex.ofReal (Real.cos x) + Complex.I * Complex.ofReal (Real.sin x)) ^ n = Complex.ofReal (Real.cos (n * x)) + Complex.I * Complex.ofReal (Real.sin (n * x)) := by sorry
Source