[Merged by Bors] - feat(NumberTheory/EllipticDivisibilitySequence): extend even-odd recursion to integers

[Multramate]

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.

---

• depends on: [Merged by Bors] - feat(AlgebraicGeometry/EllipticCurve/DivisionPolynomial/Basic): add maps for division polynomials #13399

[kim-em]

@Multramate please remember to mark old conversations as resolved. If they are left unresolved it is hard for a new reviewer coming in to understand the status of the PR.

[Multramate]

They're resolved in the sense that I still intend to move forward with this PR (despite #13057), but they're not resolved in the sense that @alreadydone hasn't explicitly agreed to this. Note that #13057 will take a while to get merged, while this is essentially standalone, and I think it's fine to have this easy proof early on without relying on that.

[faenuccio]

@alreadydone I have been assigned this PR and am having a look. Can you perform another round of revision? Thanks.

[faenuccio]

Can you please update your doc by using unicode characters for all latex codes? Although MathJax will probably render them nicely in a browser, they're still pretty unreadable in VSCode, and if you use unicode things are much more readable. Thanks!

[faenuccio]

Why is erw needed? Is there perhaps a bit of API missing, making rw work smoothly?

[Multramate]

Some of these are just for the sake of my sanity, e.g. converting 4 - 1 to 3 by rw [show (4 - 1 : ℤ) = 3 by rfl] etc.

I can add these to the bottom of this file though, what do you think?

[Multramate]

Wait, I have to find a different home for those lemmas, since I don't think file imports AddGroup...

[Multramate]

@faenuccio just to be clear, would we prefer something like this instead?

Let `W` be a Weierstrass curve over a commutative ring `R`. The sequence of `n`-division polynomials
`ψₙ ∈ R[X, Y]` of `W` is the normalised EDS with initial values
 * `ψ₀ := 0`,
 * `ψ₁ := 1`,
 * `ψ₂ := 2Y + a₁X + a₃`,
 * `ψ₃ := 3X⁴ + b₂X³ + 3b₄X² + 3b₆X + b₈`, and
 * `ψ₄ := ψ₂⬝(2X⁶ + b₂X⁵ + 5b₄X⁴ + 10b₆X³ + 10b₈X² + (b₂b₈ - b₄b₆)X + (b₄b₈ - b₆²))`.

[faenuccio]

@faenuccio just to be clear, would we prefer something like this instead?

Let `W` be a Weierstrass curve over a commutative ring `R`. The sequence of `n`-division polynomials
`ψₙ ∈ R[X, Y]` of `W` is the normalised EDS with initial values
 * `ψ₀ := 0`,
 * `ψ₁ := 1`,
 * `ψ₂ := 2Y + a₁X + a₃`,
 * `ψ₃ := 3X⁴ + b₂X³ + 3b₄X² + 3b₆X + b₈`, and
 * `ψ₄ := ψ₂⬝(2X⁶ + b₂X⁵ + 5b₄X⁴ + 10b₆X³ + 10b₈X² + (b₂b₈ - b₄b₆)X + (b₄b₈ - b₆²))`.

If you're asking with regard to the unicode business, then yes: I find this much more readable.

[faenuccio]

maintainer merge

[github-actions]

🚀 Pull request has been placed on the maintainer queue by faenuccio.

[riccardobrasca]

Thanks!

bors merge

[mathlib-bors]

Pull request successfully merged into master.

Build succeeded:

• Build
• Lint style