Skip to content

Commit

Permalink
chore(number_theory/pell*): rename files, update doc (#18503)
Browse files Browse the repository at this point in the history
Following a suggestion by @ocfnash in a comment to [#18484](#18484), this
* renames `number_theory.pell` to `number_theory.pell_matiyasevic`
* renames `number_theory.pell_general` to `number_theory.pell`
* updates documentation accordingly
* moves the "TODO" note from `pell_matiyasevic` to `pell` (and updates it)

See also [this Zulip thread](https://leanprover.zulipchat.com/#narrow/stream/217875-Is-there-code-for-X.3F/topic/Proving.20Pell's.20equation.20is.20solvable/near/322885832).
  • Loading branch information
MichaelStollBayreuth committed Feb 26, 2023
1 parent c6b5330 commit a66d07e
Show file tree
Hide file tree
Showing 4 changed files with 865 additions and 861 deletions.
2 changes: 1 addition & 1 deletion src/number_theory/dioph.lean
Expand Up @@ -6,7 +6,7 @@ Authors: Mario Carneiro
import data.fin.fin2
import data.pfun
import data.vector3
import number_theory.pell
import number_theory.pell_matiyasevic

/-!
# Diophantine functions and Matiyasevic's theorem
Expand Down

0 comments on commit a66d07e

Please sign in to comment.