I_pow_four

Mathlib.Data.Complex.Basic

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

English

The imaginary unit to the fourth power equals one: i^4 = 1.

Русский

Четвёртая степень мнимой единицы равна единице: i^4 = 1.

LaTeX

$$$i^4 = 1$$$

Lean4

@[simp]
theorem I_pow_four : I ^ 4 = 1 := by rw [(by simp : 4 = 2 * 2), pow_mul, I_sq, neg_one_sq]

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

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

Разделы

Аффилиация

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