mathlib4 icon indicating copy to clipboard operation
mathlib4 copied to clipboard

Published 20 hours ago • verified publisher icon leanprover-community

feat(NumberTheory): characterize elliptic divisibility sequences

Open alreadydone opened this issue 1 year ago • 1 comments

Main results:

  • Every normEDS is an elliptic divisibility sequence (EDS). The key proof is rel₄_of_anti_oddRec_evenRec, based on my original argument first published on MathSE

  • Conversely, every EDS is equal to some normEDS (assuming that the first two terms are not zero divisors)

Some more results are to be added be for I mark this awaiting-review.

  • [ ] depends on: #10843

Open in Gitpod

alreadydone avatar May 20 '24 09:05 alreadydone

This PR/issue depends on:

  • leanprover-community/mathlib4#13155
  • ~~leanprover-community/mathlib4#13153~~
  • ~~leanprover-community/mathlib4#10843~~ By Dependent Issues (🤖). Happy coding!

leanprover-community-mathlib4-bot avatar May 22 '24 17:05 leanprover-community-mathlib4-bot

I think this is a massive PR, especially because it's a long argument. Can you try to split it to smaller self-contained chunks, so it's easier to review?

Multramate avatar May 23 '24 16:05 Multramate