instAdd — Mathlib

English

Let d ∈ ℤ. An element of ℤ√d is represented by a pair (x, y) with x, y ∈ ℤ, corresponding to x + y√d. Addition is defined componentwise: (x, y) + (x', y') = (x + x', y + y').

Русский

Пусть d ∈ ℤ. Элемент ℤ√d задаётся парой целых чисел (x, y), соответствующей x + y√d. Операция сложения задаётся покомпонентно: (x, y) + (x', y') = (x + x', y + y').

LaTeX

$$$\\forall x,y,x',y'\\in\\mathbb{Z},\\;(x,y)+(x',y')=(x+x',\,y+y').$$$

Lean4

/-- Addition of elements of `ℤ√d` -/
instance : Add (ℤ√d) :=
  ⟨fun z w => ⟨z.1 + w.1, z.2 + w.2⟩⟩

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