re_add

Mathlib.NumberTheory.Zsqrtd.Basic

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

English

For z, w ∈ ℤ√d, the real part is additive: 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_add (z w : ℤ√d) : (z + w).re = z.re + w.re :=
  rfl

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

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

Разделы

Аффилиация

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