I_im

Mathlib.Analysis.RCLike.Basic

URI: https://scilib.ai/kg/mathlib#RCLike.I_im

English

The imaginary part of the imaginary unit I is 1.

Русский

Мнимая часть числа I равна единице.

LaTeX

$$$\operatorname{Im}(I) = 1$$$

Lean4

@[simp, rclike_simps]
theorem I_im (z : K) : im z * im (I : K) = im z :=
  mul_im_I_ax z

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

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

Разделы

Аффилиация

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