Commit 2024-11-29 11:09 90f062fe

View on Github →

feat(NumberTheory/EllipticDivisibilitySequence): extend even-odd recursion to integers (#13786) Provide a quick proof that normalised EDSs satisfy an even-odd recursion over all integers rather than just natural numbers, without relying on heavier machinery i.e. the full EDS recurrence in #13155, and make Int.negInduction slightly stronger.

Estimated changes

modified theorem normEDS_even
added theorem normEDS_even_ofNat
modified theorem normEDS_odd
added theorem normEDS_odd_ofNat
modified theorem preNormEDS_even
added theorem preNormEDS_even_ofNat
modified theorem preNormEDS_odd
added theorem preNormEDS_odd_ofNat