Real Projection Equals Cosine

StatusFully Proven
TypeTheorem
ModuleChebyshevCircles.Proofs.RootsOfUnity

Statement

Theorem Real Projection Equals Cosine
[blueprint]

For $k < N$, $\mathrm{Re}\bigl(e^{i(\theta + 2\pi k/N)}\bigr) = \cos(\theta + 2\pi k/N).$

theorem realProjection_eq_cos (N : ℕ) (θ : ℝ) (k : ℕ) (_hk : k < N) :
    (exp (I * (θ + 2 * π * k / N))).re = Real.cos (θ + 2 * π * k / N) := by
Proof ▼ 


  rw [mul_comm]
  convert exp_ofReal_mul_I_re (θ + 2 * π * k / N)
  norm_cast

Dependencies (uses)

None

Dependents (used by)

None

Neighborhood

Legend
Not Ready
Work in Progress
Sorry (theorems only)
Proven/Defined
Fully Proven (theorems only)
Axiom
Mathlib Ready
Theorems/Lemmas
Definitions
Axioms