re_smul

Mathlib.NumberTheory.Zsqrtd.Basic

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

English

For a ∈ ℤ and b ∈ ℤ√d, Re(a·b) = a·Re(b).

Русский

Для a ∈ ℤ и b ∈ ℤ√d, Re(a·b) = a·Re(b).

LaTeX

$$$$ \operatorname{Re}(a\cdot b) = a\cdot \operatorname{Re}(b), \quad a \in \mathbb{Z}, \ b \in \mathbb{Z}[\sqrt{d}]. $$$$

Lean4

theorem re_smul (a : ℤ) (b : ℤ√d) : (↑a * b).re = a * b.re := by simp

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

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

Разделы

Аффилиация

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