theorem
proved
tactic proof
phases_require_complex_k2
show as:
view Lean formalization →
formal statement (Lean)
117theorem phases_require_complex_k2 : (tickPhase ⟨2, by omega⟩).im ≠ 0 := by
proof body
Tactic-mode proof.
118 unfold tickPhase
119 have h : I * ↑π * ↑(2 : ℕ) / 4 = ↑(π / 2 : ℝ) * I := by push_cast; ring
120 simp only [show (⟨2, by omega⟩ : Fin 8).val = 2 from rfl] at *
121 rw [h, Complex.exp_mul_I]
122 rw [← Complex.ofReal_cos, ← Complex.ofReal_sin]
123 simp only [Complex.add_im, Complex.mul_I_im, Complex.ofReal_im, Complex.ofReal_re, zero_add]
124 rw [Real.sin_pi_div_two]
125 norm_num
126
127/-- General statement: for k ∈ {1,2,3,5,6,7}, the tick phase has nonzero imaginary part. -/