Skip to content
This repository was archived by the owner on Jul 24, 2024. It is now read-only.

Commit a66d07e

Browse files
MichaelStollBayreuthMichaelStollBayreuth
committed
chore(number_theory/pell*): rename files, update doc (#18503)
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).
1 parent c6b5330 commit a66d07e

4 files changed

Lines changed: 865 additions & 861 deletions

File tree

‎src/number_theory/dioph.lean‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -6,7 +6,7 @@ Authors: Mario Carneiro
66
import data.fin.fin2
77
import data.pfun
88
import data.vector3
9-
import number_theory.pell
9+
import number_theory.pell_matiyasevic
1010

1111
/-!
1212
# Diophantine functions and Matiyasevic's theorem

0 commit comments

Comments
 (0)