re_sub

Mathlib.NumberTheory.Zsqrtd.Basic

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

English

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

Русский

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

LaTeX

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

Lean4

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

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

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

Разделы

Аффилиация

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