theorem proved term proof

`i_squared_from_8tick`

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

formal statement (Lean)

  93theorem i_squared_from_8tick :
  94    I^2 = -1 := by

Term-mode proof.

  95  simp [sq, I_mul_I]
  96
  97/-- More generally: i^n corresponds to n×2 ticks. -/