conj_I

Mathlib.Analysis.RCLike.Basic

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

English

Conjugate of I is -I: conj(I) = -I.

Русский

Сопряжение мнимаой единицы равно -I.

LaTeX

$$$\operatorname{conj}(I) = -I$$$

Lean4

@[simp, rclike_simps]
theorem conj_I : conj (I : K) = -I :=
  RCLike.conj_I_ax

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

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

Разделы

Аффилиация

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