Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

[Merged by Bors] - feat(AlgebraicGeometry/EllipticCurve/DivisionPolynomial/Degree): add further degree lemmas #14063

Closed
wants to merge 1 commit into from
Closed

[Merged by Bors] - feat(AlgebraicGeometry/EllipticCurve/DivisionPolynomial/Degree): add further degree lemmas #14063

wants to merge 1 commit into from

Conversation

Multramate
Copy link
Collaborator

Open in Gitpod

@Multramate Multramate added awaiting-review awaiting-CI t-number-theory Number theory (also use t-algebra or t-analysis to specialize) t-algebraic-geometry Algebraic geometry labels Jun 23, 2024
@github-actions GitHub Actions
Copy link

PR summary 55c7026620

Import changes

No significant changes to the import graph

Declarations diff

+ coeff_preΨ'_ne_zero
+ coeff_preΨ_ne_zero
+ coeff_preΨ₄_ne_zero
+ coeff_Φ_ne_zero
+ coeff_ΨSq_ne_zero
+ coeff_Ψ₂Sq_ne_zero
+ coeff_Ψ₃_ne_zero
+ leadingCoeff_preΨ
+ leadingCoeff_preΨ'
+ leadingCoeff_preΨ₄
+ leadingCoeff_Φ
+ leadingCoeff_ΨSq
+ leadingCoeff_Ψ₂Sq
+ leadingCoeff_Ψ₃
+ natDegree_preΨ'_le
+ natDegree_preΨ'_pos
+ natDegree_preΨ_le
+ natDegree_preΨ_pos
+ natDegree_preΨ₄_le
+ natDegree_preΨ₄_pos
+ natDegree_Φ_le
+ natDegree_Φ_pos
+ natDegree_ΨSq_le
+ natDegree_ΨSq_pos
+ natDegree_Ψ₂Sq_le
+ natDegree_Ψ₂Sq_pos
+ natDegree_Ψ₃_le
+ natDegree_Ψ₃_pos
+ preΨ'_ne_zero
+ preΨ_ne_zero
+ preΨ₄_ne_zero
+ Φ_ne_zero
+ ΨSq_ne_zero
+ Ψ₂Sq_ne_zero
+ Ψ₃_ne_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>

Ruben-VandeVelde
Ruben-VandeVelde approved these changes Jun 24, 2024
View reviewed changes
Copy link
Collaborator

@Ruben-VandeVelde Ruben-VandeVelde left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

maintainer merge

@github-actions GitHub Actions
Copy link

🚀 Pull request has been placed on the maintainer queue by Ruben-VandeVelde.

@riccardobrasca
Copy link
Member

Thanks!

bors merge

@github-actions github-actions bot added ready-to-merge This PR has been sent to bors. and removed awaiting-review labels Jun 24, 2024
mathlib-bors bot pushed a commit that referenced this pull request Jun 24, 2024
@Multramate
feat(AlgebraicGeometry/EllipticCurve/DivisionPolynomial/Degree): add …
39d2a24 
…further degree lemmas (#14063)
@mathlib-bors
Copy link
Contributor

mathlib-bors bot commented Jun 24, 2024

Build failed (retrying...):

mathlib-bors bot pushed a commit that referenced this pull request Jun 24, 2024
@Multramate
feat(AlgebraicGeometry/EllipticCurve/DivisionPolynomial/Degree): add …
ea59701 
…further degree lemmas (#14063)
@mathlib-bors
Copy link
Contributor

mathlib-bors bot commented Jun 24, 2024

This PR was included in a batch that was canceled, it will be automatically retried

mathlib-bors bot pushed a commit that referenced this pull request Jun 24, 2024
@Multramate
feat(AlgebraicGeometry/EllipticCurve/DivisionPolynomial/Degree): add …
dc3d440 
…further degree lemmas (#14063)
@mathlib-bors
Copy link
Contributor

mathlib-bors bot commented Jun 24, 2024

Pull request successfully merged into master.

Build succeeded:

@mathlib-bors mathlib-bors bot changed the title feat(AlgebraicGeometry/EllipticCurve/DivisionPolynomial/Degree): add further degree lemmas [Merged by Bors] - feat(AlgebraicGeometry/EllipticCurve/DivisionPolynomial/Degree): add further degree lemmas Jun 24, 2024
@mathlib-bors mathlib-bors bot closed this Jun 24, 2024
@mathlib-bors mathlib-bors bot deleted the DivisionPolynomial.Degree branch June 24, 2024 12:36
alreadydone
alreadydone reviewed Jun 24, 2024
View reviewed changes
Mathlib/AlgebraicGeometry/EllipticCurve/DivisionPolynomial/Degree.lean
* $\tilde{\Psi}_n = \tfrac{n}{2}X^{\tfrac{n^2 - 4}{2}} + \dots$ if $n$ is even,
* $\tilde{\Psi}_n = nX^{\tfrac{n^2 - 1}{2}} + \dots$ if $n$ is odd,
* $\Psi_n^{[2]} = n^2X^{n^2 - 1} + \dots$, and
* $\Phi_n = X^{n^2} + \dots$.

In particular, when $R$ is an integral domain of characteristic different from $n$, the univariate
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

this should say "not dividing n" right?

Copy link
Collaborator Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Yes... this got merged a bit too quickly, but I'll make the change in a different PR.

kbuzzard pushed a commit that referenced this pull request Jun 26, 2024
@Multramate @kbuzzard
feat(AlgebraicGeometry/EllipticCurve/DivisionPolynomial/Degree): add …
50ae0e6 
…further degree lemmas (#14063)
dagurtomas pushed a commit that referenced this pull request Jul 2, 2024
@Multramate @dagurtomas
feat(AlgebraicGeometry/EllipticCurve/DivisionPolynomial/Degree): add …
365cc58 
…further degree lemmas (#14063)
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@alreadydone alreadydone alreadydone left review comments

@Ruben-VandeVelde Ruben-VandeVelde Ruben-VandeVelde approved these changes

Assignees
No one assigned
Labels
maintainer-merge ready-to-merge This PR has been sent to bors. t-algebraic-geometry Algebraic geometry t-number-theory Number theory (also use t-algebra or t-analysis to specialize)
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.
4 participants
@Multramate @riccardobrasca @alreadydone @Ruben-VandeVelde