tick2_is_i

formal source

  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]
  82
  83/-- Two rotations by π/2 equals rotation by π. -/
  84theorem two_rotations :
  85    cexp (I * Real.pi / 2) * cexp (I * Real.pi / 2) = cexp (I * Real.pi) := by