Assumptions:
TeX:
{i}^{n} = \begin{cases} 1, & n \equiv 0 \pmod {4}\\i, & n \equiv 1 \pmod {4}\\-1, & n \equiv 2 \pmod {4}\\-i, & n \equiv 3 \pmod {4}\\ \end{cases}
n \in \mathbb{Z}Definitions:
| Fungrim symbol | Notation | Short description |
|---|---|---|
| Pow | Power | |
| ConstI | Imaginary unit | |
| ZZ | Integers |
Source code for this entry:
Entry(ID("c12a41"),
Formula(Equal(Pow(ConstI, n), Cases(Tuple(1, CongruentMod(n, 0, 4)), Tuple(ConstI, CongruentMod(n, 1, 4)), Tuple(-1, CongruentMod(n, 2, 4)), Tuple(Neg(ConstI), CongruentMod(n, 3, 4))))),
Variables(n),
Assumptions(Element(n, ZZ)))