Commit 2024-01-22 20:12 2a7c4d65

View on Github →

feat(NumberTheory/EllipticDivisibilitySequence): define elliptic divisibility sequences (#9375) As a generalisation of the division polynomials in #6703 but also possibly for other number theoretic purposes. The recurrence relation is defined as isEllDivSequence, and a concrete sequence is defined as EllDivSequence. The fact that the two definitions are related requires a very long inductive proof, and will not be touched on in this PR.

Estimated changes

added def IsDivSequence
added theorem IsDivSequence_id
added theorem IsDivSequence_mul
added def IsEllDivSequence
added theorem IsEllDivSequence_id
added theorem IsEllDivSequence_mul
added def IsEllSequence
added theorem IsEllSequence_id
added theorem IsEllSequence_mul
added def normEDS'
added theorem normEDS'_even
added theorem normEDS'_four
added theorem normEDS'_odd
added theorem normEDS'_one
added theorem normEDS'_three
added theorem normEDS'_two
added theorem normEDS'_zero
added def normEDS
added theorem normEDS_even
added theorem normEDS_four
added theorem normEDS_neg
added theorem normEDS_odd
added theorem normEDS_one
added theorem normEDS_three
added theorem normEDS_two
added theorem normEDS_zero