mathlib3

0b20dffb - feat(number_theory/pell): add def and properties of fundamental solutions (#18901)

feat(number_theory/pell): add def and properties of fundamental solutions (#18901) This is the next step in developing the theory of Pell's equation. We define what a *fundamental solution* is, show that it exists and is unique and that it is characterized by the property that it (is positive and) generates the group of solutions up to sign. See [this Zulip thread](https://leanprover.zulipchat.com/#narrow/stream/217875-Is-there-code-for-X.3F/topic/Proving.20Pell's.20equation.20is.20solvable/near/343270338).