smuld_val

Mathlib.NumberTheory.Zsqrtd.Basic

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

English

For n ∈ ℤ and x,y ∈ ℤ, sqrt(d) * (n : ℤ√d) * ⟨x,y⟩ = ⟨d n y, n x⟩.

Русский

Для n ∈ ℤ и x,y ∈ ℤ, √d · (n) · ⟨x,y⟩ = ⟨d n y, n x⟩.

LaTeX

$$$$ \sqrt{d} \cdot (n: \mathbb{Z}[\sqrt{d}]) \cdot \langle x,y\rangle = \langle d n y, n x\rangle, \quad n,x,y \in \mathbb{Z}. $$$$

Lean4

@[simp]
theorem smuld_val (n x y : ℤ) : sqrtd * (n : ℤ√d) * ⟨x, y⟩ = ⟨d * n * y, n * x⟩ := by ext <;> simp

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

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

Разделы

Аффилиация

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