conj_neg_I

Mathlib.Analysis.RCLike.Basic

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

English

Conjugation of negative imaginary unit: conj(-I) = I.

Русский

Сопряжение отрицательной мнимой единицы: conj(-I) = I.

LaTeX

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

Lean4

@[rclike_simps, simp]
theorem conj_neg_I : conj (-I) = (I : K) := by rw [map_neg, conj_I, neg_neg]

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

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

Разделы

Аффилиация

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