I_re

Mathlib.Analysis.RCLike.Basic

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

English

The real part of the imaginary unit I is zero.

Русский

Действительная часть мнимой единицы I равна нулю.

LaTeX

$$$\operatorname{Re}(I) = 0$$$

Lean4

/-- The imaginary unit. -/
@[simp, rclike_simps]
theorem I_re : re (I : K) = 0 :=
  I_re_ax

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

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

Разделы

Аффилиация

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