feat(number_theory/pell): group structure (#18568)
This continues the sequence of PRs related to the Pell equation.
We define a type for the solutions of `x^2 - d*y^2 = 1` and give it the structure of a commutative mutiplicative group with compatible negation.
See [this thread on Zulip](https://leanprover.zulipchat.com/#narrow/stream/217875-Is-there-code-for-X.3F/topic/Proving.20Pell's.20equation.20is.20solvable/near/338175458).
