Integer powers of i equal to ±i

Since i has multiplicative order four, i ^ m depends only on m % 4 (Complex.I_zpow_eq_zpow_mod). This file records when an integer power of i is i or -i.

Main results

• TauCeti.Complex.I_zpow_eq_I_iff: i ^ m = i exactly when m % 4 = 1.
• TauCeti.Complex.I_zpow_eq_neg_I_iff: i ^ m = -i exactly when m % 4 = 3.

theorem TauCeti.Complex.I_zpow_eq_I_iff (m : ℤ) : Complex.I ^ m = Complex.I ↔ m % 4 = 1

An integer power i ^ m equals i exactly when m ≡ 1 (mod 4).

theorem TauCeti.Complex.I_zpow_eq_neg_I_iff (m : ℤ) : Complex.I ^ m = -Complex.I ↔ m % 4 = 3

An integer power i ^ m equals -i exactly when m ≡ 3 (mod 4).