mathlib
842557b6 - chore(number_theory/pell): Move def. of solution type and API to beginning (#18639)

Commit
3 years ago
chore(number_theory/pell): Move def. of solution type and API to beginning (#18639) On the suggestion of @eric-wieser, this PR separates moving the definition of the type of solutions and the API lemmas to the beginning of the file, to help with the reviewing of #18626. Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
Parents
Loading