I_to_real

Mathlib.Analysis.RCLike.Basic

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

English

In the RCLike setting, the imaginary unit I_R equals zero in the real subfield.

Русский

В контексте RCLike мнимая единица I_R равна нулю в вещественном подполе.

LaTeX

$$$I_R = 0$$$

Lean4

@[simp, rclike_simps]
theorem I_to_real : IR = 0 :=
  rfl

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

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

Разделы

Аффилиация

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