pith. machine review for the scientific record. sign in
theorem proved tactic proof

tick_phases_roots_of_unity

show as:
view Lean formalization →

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

generate prose now

formal statement (Lean)

  54theorem tick_phases_roots_of_unity (k : Fin 8) :
  55    (tickPhase k)^8 = 1 := by

proof body

Tactic-mode proof.

  56  unfold tickPhase
  57  -- exp(I × π × k / 4)^8 = exp(8 × I × π × k / 4) = exp(2πIk) = 1
  58  rw [← Complex.exp_nat_mul]
  59  have h : (8 : ℕ) * (I * ↑π * ↑(k : ℕ) / 4) = ↑(k : ℕ) * (2 * ↑π * I) := by
  60    push_cast
  61    ring
  62  rw [h]
  63  exact Complex.exp_nat_mul_two_pi_mul_I k
  64
  65/-- The phases are equally spaced around the unit circle.
  66    Consecutive phases differ by π/4 (45°). -/

depends on (1)

Lean names referenced from this declaration's body.