I_mul_re

Mathlib.Data.Complex.Basic

URI: https://scilib.ai/kg/mathlib#Complex.I_mul_re

English

For all z ∈ ℂ, Re(i z) = -Im(z).

Русский

Пусть z ∈ ℂ. Тогда Re(i z) = -Im(z).

LaTeX

$$$\\operatorname{Re}(i z) = -\\operatorname{Im}(z)$$$

Lean4

theorem I_mul_re (z : ℂ) : (I * z).re = -z.im := by simp

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

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

Разделы

Аффилиация

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