im_eq_zero

Mathlib.Analysis.RCLike.Basic

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

English

If the imaginary unit I is zero in K, then the imaginary part is identically zero for all z.

Русский

Если единица мнимого числа I равна нулю в K, тогда мнимая часть всех z равна нулю.

LaTeX

$$$$ \\text{im\_eq\_zero}(h : I = (0 : K)) (z : K) : \\operatorname{im}(z) = 0. $$$$

Lean4

theorem im_eq_zero (h : I = (0 : K)) (z : K) : im z = 0 :=
  by
  rw [← re_add_im z, h]
  simp

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

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

Разделы

Аффилиация

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