eightTickPhase

formal source

  48    Tick 6: e^{i·3π/2} = -i
  49    Tick 7: e^{i·7π/4} = (1-i)/√2
  50    Tick 8 = Tick 0: e^{i·2π} = 1 -/
  51noncomputable def eightTickPhase (n : Fin 8) : ℂ :=
  52  cexp (I * ((n : ℝ) * Real.pi / 4))
  53
  54/-- Tick 2 is i. -/
  55theorem tick2_is_i : eightTickPhase 2 = I := by
  56  unfold eightTickPhase
  57  simp only [Fin.val_two, Nat.cast_ofNat]
  58  have h : I * (2 * Real.pi / 4) = I * (Real.pi / 2) := by ring
  59  rw [h]
  60  rw [Complex.exp_mul_I, Complex.cos_pi_div_two, Complex.sin_pi_div_two]
  61  simp
  62
  63/-- Tick 4 is -1. -/
  64theorem tick4_is_neg1 : eightTickPhase 4 = -1 := by
  65  unfold eightTickPhase
  66  simp only [Fin.val_four, Nat.cast_ofNat]
  67  have h : I * (4 * Real.pi / 4) = I * Real.pi := by ring
  68  rw [h]
  69  rw [Complex.exp_mul_I, Complex.cos_pi, Complex.sin_pi]
  70  simp
  71
  72/-! ## Rotation and Multiplication -/
  73
  74/-- Multiplication by i is rotation by π/2 (2 ticks). -/
  75theorem i_is_rotation :
  76    ∀ z : ℂ, I * z = z * cexp (I * Real.pi / 2) := by
  77  intro z
  78  have h : cexp (I * Real.pi / 2) = I := by
  79    rw [Complex.exp_mul_I, Complex.cos_pi_div_two, Complex.sin_pi_div_two]
  80    simp
  81  rw [h, mul_comm]