instStar

Mathlib.NumberTheory.Zsqrtd.Basic

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

English

Conjugation on Z[√d] sends a + b√d to a − b√d.

Русский

Сопряжение на Z[√d] переводит a + b√d в a − b√d.

LaTeX

$$$$ (a+b\sqrt{d})^{*} = a - b\sqrt{d}, \quad a,b \in \mathbb{Z}. $$$$

Lean4

/-- Conjugation in `ℤ√d`. The conjugate of `a + b √d` is `a - b √d`. -/
instance : Star (ℤ√d) where star z := ⟨z.1, -z.2⟩

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

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

Разделы

Аффилиация

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