div_I

Mathlib.Data.Complex.Basic

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

English

Dividing by the imaginary unit I is equivalent to multiplying by −I: z / I = −(z I).

Русский

Деление на мнимая единица I эквивалентно умножению на −I: z / I = −(z I).

LaTeX

$$$$z / I = -\,(z \cdot I).$$$$

Lean4

@[simp]
theorem div_I (z : ℂ) : z / I = -(z * I) :=
  (div_eq_iff_mul_eq I_ne_zero).2 <| by simp [mul_assoc]

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

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

Разделы

Аффилиация

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