I_pow_eq_pow_mod

Mathlib.Data.Complex.Basic

URI: https://scilib.ai/kg/mathlib#Complex.I_pow_eq_pow_mod

English

Powers of i are periodic with period 4: i^n = i^(n mod 4).

Русский

Степени i периодичны с периодом 4: i^n = i^(n mod 4).

LaTeX

$$$i^n = i^{(n \\\\% 4)}$$$

Lean4

theorem I_pow_eq_pow_mod (n : ℕ) : I ^ n = I ^ (n % 4) :=
  by
  conv_lhs => rw [← Nat.div_add_mod n 4]
  simp [pow_add, pow_mul, I_pow_four]

Похожие утверждения

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru