instAddMonoid

Mathlib.NumberTheory.Zsqrtd.Basic

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

English

ℤ√d carries an additive monoid structure, i.e., it has an associative addition with an identity element.

Русский

ℤ√d имеет структуру аддитивного моноида: операция сложения ассоциативна с единицей.

LaTeX

$$$ (\\mathbb{Z}\\sqrt{d}, +, 0) \\text{ is an additive monoid.} $$$

Lean4

instance : AddMonoid (ℤ√d) := by infer_instance

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

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

Разделы

Аффилиация

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