mathlib4 icon indicating copy to clipboard operation
mathlib4 copied to clipboard

Published 20 hours ago • verified publisher icon leanprover-community

feat(AlgebraicGeometry/EllipticCurve/DivisionPolynomial): define division polynomials

Open Multramate opened this issue 2 years ago • 2 comments

  • [x] depends on: #10814

Open in Gitpod

Multramate avatar Aug 21 '23 11:08 Multramate

This PR/issue depends on:

  • ~~leanprover-community/mathlib4#10814~~ By Dependent Issues (🤖). Happy coding!

leanprover-community-mathlib4-bot avatar May 16 '24 08:05 leanprover-community-mathlib4-bot

Since we need both univariate and bivariate division polynomials, here is my suggestion for the naming:

  • φ, ω, and ψ will be the bivariate versions defined in the usual sense using normEDS
  • Ψ₂Sq, Ψ', ΨSq, and Φ will be the univariate versions defined ad-hoc using preNormEDS
  • Ψ will be bivariate, but defined using the univariate Ψ', which will be congruent to ψ in the coordinate ring

I'll make their definitions as clear as possible in the module docstring.

Multramate avatar May 24 '24 22:05 Multramate

PR summary

Import changes

No significant changes to the import graph

Declarations diff

+ C_Ψ₂Sq_eq + as + in + preΨ + preΨ' + preΨ'_even + preΨ'_four + preΨ'_odd + preΨ'_one + preΨ'_three + preΨ'_two + preΨ'_zero + preΨ_even + preΨ_four + preΨ_neg + preΨ_odd + preΨ_ofNat + preΨ_one + preΨ_three + preΨ_two + preΨ_zero + preΨ₄ + Φ + Φ_four + Φ_neg + Φ_ofNat + Φ_one + Φ_three + Φ_two + Φ_zero + Ψ + ΨSq + ΨSq_even + ΨSq_four + ΨSq_neg + ΨSq_odd + ΨSq_ofNat + ΨSq_one + ΨSq_three + ΨSq_two + ΨSq_zero + Ψ_even + Ψ_four + Ψ_neg + Ψ_odd + Ψ_ofNat + Ψ_one + Ψ_three + Ψ_two + Ψ_zero + Ψ₂Sq + Ψ₂Sq_eq + Ψ₃ + φ + φ_four + φ_neg + φ_one + φ_three + φ_two + φ_zero + ψ + ψ_even + ψ_four + ψ_neg + ψ_odd + ψ_one + ψ_three + ψ_two + ψ_zero + ψ₂

You can run this locally as follows 
## summary with just the declaration names:
./scripts/no_lost_declarations.sh short <optional_commit>

## more verbose report:
./scripts/no_lost_declarations.sh <optional_commit>

github-actions[bot] avatar Jun 08 '24 17:06 github-actions[bot]

I only moved the files into a subdirectory in latest commit, while the changes reflecting the suggestions are in the previous commit. Note that there seems to be a weird bug with neg lemmas not recognising the negation in R[X][Y] in lines 429 and 430 without supplying the type.

Multramate avatar Jun 08 '24 17:06 Multramate

Don't we need the map lemmas for that? I think I started #13399 pretty much immediately after I realised this. I suggest keeping the PR as it is and continue there.

Multramate avatar Jun 08 '24 20:06 Multramate

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

github-actions[bot] avatar Jun 09 '24 14:06 github-actions[bot]

This is great, thanks!

bors merge

riccardobrasca avatar Jun 09 '24 22:06 riccardobrasca

Pull request successfully merged into master.

Build succeeded:

mathlib-bors[bot] avatar Jun 09 '24 22:06 mathlib-bors[bot]