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

tick4_is_neg1

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)

  64theorem tick4_is_neg1 : eightTickPhase 4 = -1 := by

proof body

Tactic-mode proof.

  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). -/

depends on (6)

Lean names referenced from this declaration's body.