add_def — Mathlib

English

Let z = (x, y) and w = (x', y') be elements of ℤ√d. Then the addition is explicitly (⟨x, y⟩ + ⟨x', y'⟩) = ⟨x + x', y + y'⟩.

Русский

Пусть z = (x, y) и w = (x', y') — элементы ℤ√d. Тогда сложение даётся явно: (⟨x, y⟩ + ⟨x', y'⟩) = ⟨x + x', y + y'⟩.

LaTeX

$$$ (x,y)+(x',y')=(x+x',\,y+y').$$$

Lean4

@[simp]
theorem add_def (x y x' y' : ℤ) : (⟨x, y⟩ + ⟨x', y'⟩ : ℤ√d) = ⟨x + x', y + y'⟩ :=
  rfl

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