im_sub

Mathlib.NumberTheory.Zsqrtd.Basic

URI: https://scilib.ai/kg/mathlib#Zsqrtd.im_sub

English

For z, w ∈ ℤ√d, Im(z − w) = Im(z) − Im(w).

Русский

Для z, w ∈ ℤ√d, Im(z − w) = Im(z) − Im(w).

LaTeX

$$$\\Im(z-w) = \\Im(z) - \\Im(w).$$$

Lean4

@[simp]
theorem im_sub (z w : ℤ√d) : (z - w).im = z.im - w.im :=
  rfl

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

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

Разделы

Аффилиация

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