Commit 2026-10-17 17:39 d2687755

feat(NumberTheory/EllipticDivisibilitySequence): prove that a normalised elliptic divisibility sequence is an elliptic sequence (#42453) This is the updated version of #13155 and contains the proof that a sequence satisfying the even and odd elliptic relations (with mild additional conditions) is an elliptic net and hence an elliptic sequence. This is the main argument in Section 2 of Junyan's paper. Previously it was broken down into hundreds of lines of multiple lemmas but I was able to condense it into a single lemma with multiple wlogs that are hopefully self-explanatory.