English
For each integer d, the Pell solution set forms a commutative group under the standard Pell multiplication, identifying with the unit group of the ring Z[√d].
Русский
Для каждого целого числа d множество решений Пелля образует коммутативную группу под стандартным умножением Пелля, что соответствует единичной группе кольца Z[√d].
LaTeX
$$$$ S_d = \{(x,y) \in \mathbb{Z}^2 : x^2 - d y^2 = 1\}, \quad (x_1,y_1) \star (x_2,y_2) = (x_1 x_2 + d\,y_1 y_2, \; x_1 y_2 + x_2 y_1). $$
$$ (S_d, \star) \text{ is a commutative group with identity } (1,0) \text{ and } (x,y)^{-1}=(x,-y). $$$$
Lean4
instance instCommGroup : CommGroup (Solution₁ d) :=
inferInstanceAs (CommGroup (unitary (ℤ√d)))
