I_pow_three

Mathlib.Data.Complex.Basic

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

English

The imaginary unit cubed equals minus the imaginary unit: i^3 = -i.

Русский

Куб мнимой единицы равен минус мнимая единица: i^3 = -i.

LaTeX

$$$i^3 = -i$$$

Lean4

@[simp]
theorem I_pow_three : I ^ 3 = -I := by rw [pow_succ, I_sq, neg_one_mul]

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

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

Разделы

Аффилиация

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