conj_I

Mathlib.Data.Complex.Basic

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

English

Conjugation sends the imaginary unit to its negation: conj(I) = -I.

Русский

Сопряжение переводит мнимую единицу в противоположную: conj(I) = -I.

LaTeX

$$$\overline{I} = -I$$$

Lean4

@[simp]
theorem conj_I : conj I = -I :=
  Complex.ext_iff.2 <| by simp

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

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

Разделы

Аффилиация

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