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.