mathlib4 icon indicating copy to clipboard operation
mathlib4 copied to clipboard

Published 20 hours ago • verified publisher icon leanprover-community

feat(AlgebraicGeometry/EllipticCurve/DivisionPolynomial): compute degrees of division polynomials

Open Multramate opened this issue 1 year ago • 2 comments

  • [x] depends on: #10814
  • [ ] depends on: #10843

Open in Gitpod

Multramate avatar Feb 23 '24 10:02 Multramate

Sorry, wrong PR. ~~I merged master in this branch; please merge if it looks good.~~

alreadydone avatar May 19 '24 00:05 alreadydone

PR summary fe88cbcb3f

Import changes

No significant changes to the import graph

Declarations diff

+ coeff_preΨ + coeff_preΨ' + coeff_preΨ₄ + coeff_Φ + coeff_ΨSq + coeff_Ψ₂Sq + coeff_Ψ₃ + natDegree_preΨ + natDegree_preΨ' + natDegree_preΨ₄ + natDegree_Φ + natDegree_ΨSq + natDegree_Ψ₂Sq + natDegree_Ψ₃ + not_even_two_mul_add_one

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 22:06 github-actions[bot]

This PR/issue depends on:

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

leanprover-community-mathlib4-bot avatar Jun 09 '24 22:06 leanprover-community-mathlib4-bot

Starting working on the new approach again ...

alreadydone avatar Jun 12 '24 15:06 alreadydone

This condenses the eight natDegree/coeff_even/odd_preΨ'_even/odd lemmas into one, but I think we still can't avoid the natDegree/coeff_preΨ'_add_* lemmas in the proof of natDegree_coeff_preΨ'? Maybe I'm missing something...

Multramate avatar Jun 12 '24 15:06 Multramate

See my latest commit for more details.

alreadydone avatar Jun 12 '24 16:06 alreadydone

Pushed another commit and I think you can handle the rest! Getting back to my own PRs ...

alreadydone avatar Jun 12 '24 16:06 alreadydone

@Multramate Have you tried to clean up the rest of my branch? If not, I'll try to see if I can golf the subsequent computations today.

alreadydone avatar Jun 14 '24 17:06 alreadydone

@Multramate Have you tried to clean up the rest of my branch? If not, I'll try to see if I can golf the subsequent computations today.

Thanks for waiting! This is now ready to be reviewed again.

Multramate avatar Jun 15 '24 19:06 Multramate

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

github-actions[bot] avatar Jun 16 '24 05:06 github-actions[bot]

Thanks!

bors merge

riccardobrasca avatar Jun 17 '24 15:06 riccardobrasca

Pull request successfully merged into master.

Build succeeded:

mathlib-bors[bot] avatar Jun 17 '24 16:06 mathlib-bors[bot]