Mathlib v3 is deprecated. Go to Mathlib v4

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.

Estimated changes