Real Projection Membership

StatusFully Proven
TypeTheorem
ModuleChebyshevCircles.Proofs.RootsOfUnity

Statement

Theorem Real Projection Membership
[blueprint]

For $k < N$, $\cos(\theta + 2\pi k/N) \in \mathrm{realProjectionsList}(N, \theta).$

theorem realProjection_mem_list (N : ℕ) (θ : ℝ) (k : ℕ) (hk : k < N) :
    Real.cos (θ + 2 * π * k / N) ∈ realProjectionsList N θ := by
Proof ▼ 


  simp [realProjectionsList, List.mem_map, List.mem_range]
  exact ⟨k, hk, rfl⟩

Dependencies (uses)

Dependents (used by)

Neighborhood

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