zero_im

Mathlib.Analysis.RCLike.Basic

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

English

Let K be an RCLike type. The imaginary part of 0 in K is 0.

Русский

Пусть K является RCLike. Мнимая часть нуля в K равна нулю.

LaTeX

$$$\operatorname{Im}(0) = 0$$$

Lean4

@[rclike_simps]
theorem zero_im : im (0 : K) = (0 : ℝ) :=
  map_zero im

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

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

Разделы

Аффилиация

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