Shared Trigonometric Identities

Euler-formula expansion of exp(θ * I) and exact values at 2π/3, used by both WindingWeights/Common.lean and RectHomotopy/HomotopyDef.lean.

theorem exp_real_angle_I (θ : ℝ) : Complex.exp (↑θ * Complex.I) = ↑(Real.cos θ) + ↑(Real.sin θ) * Complex.I

theorem cos_two_pi_div_three : Real.cos (2 * Real.pi / 3) = -1 / 2

theorem sin_two_pi_div_three : Real.sin (2 * Real.pi / 3) = √3 / 2