Commit 2023-03-19 19:14 7ec29468
View on Github →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.