Cardinality of Real Projections List

StatusFully Proven
TypeTheorem
ModuleChebyshevCircles.Proofs.RootsOfUnity

Statement

Theorem Cardinality of Real Projections List
[blueprint]

$\lvert\mathrm{realProjectionsList}(N, \theta)\rvert = N.$

theorem card_realProjectionsList (N : ℕ) (θ : ℝ) :
    (realProjectionsList N θ).length = N := by
Proof ▼ 


  simp [realProjectionsList]

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