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.

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

[Merged by Bors] - feat(AlgebraicGeometry/EllipticCurve/DivisionPolynomial/Basic): define division polynomials #6703

Closed
wants to merge 43 commits into from
Closed
Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
43 commits
Select commit Hold shift + click to select a range
4ee67ce
Add Ring.divide
Multramate Jul 15, 2023
eab1469
Add IsUnit.divide_eq_mul_inverse
Multramate Jul 18, 2023
50f07f5
Remove redundant assumption
Multramate Jul 18, 2023
7cd0323
Replace NeZero with Nontrivial
Multramate Aug 8, 2023
4dc082e
Merge branch 'master' into Ring.divide
Multramate Aug 21, 2023
bd2f111
Define division polynomials
Multramate Aug 21, 2023
3d63eed
Merge branch 'master' into division_polynomial
Multramate Nov 27, 2023
24f6d6e
Remove divisibility changes
Multramate Nov 27, 2023
dec8062
Merge branch 'master' into division_polynomial
Multramate Dec 29, 2023
04200b4
Define elliptic divisibility sequences
Multramate Jan 1, 2024
09adefb
Merge branch 'EllipticDivisibilitySequence' into division_polynomial
Multramate Jan 1, 2024
ba72afb
Use elliptic divisibility sequences
Multramate Jan 1, 2024
bb1bf7e
Implement Jacobian coordinates
Multramate Jan 2, 2024
906e858
Implement equations and nonsingularity for Jacobian coordinates
Multramate Jan 4, 2024
b9e60a1
Implement group operation polynomials for Jacobian coordinates
Multramate Jan 4, 2024
d42c841
Implement group operations on point representatives for Jacobian coor…
Multramate Jan 4, 2024
59a7cf4
Implement group operations on nonsingular rational points for Jacobia…
Multramate Jan 4, 2024
4449702
Merge branch 'EllipticCurve.Jacobian.Point' into EllipticCurve.Jacobian
Multramate Jan 4, 2024
18e2fd4
Remove extraneous factor in addition
Multramate Jan 5, 2024
04c8b01
Merge branch 'EllipticCurve.Jacobian.Polynomial' into EllipticCurve.J…
Multramate Jan 5, 2024
44f37d6
Fix merge error
Multramate Jan 5, 2024
2fdd995
Merge branch 'EllipticCurve.Jacobian.Representative' into EllipticCur…
Multramate Jan 5, 2024
8b3cc83
Fix merge error
Multramate Jan 5, 2024
640f3a4
Merge branch 'EllipticCurve.Jacobian.Point' into EllipticCurve.Jacobian
Multramate Jan 5, 2024
aebed9b
Merge branch 'EllipticCurve.Jacobian' into DivisionPolynomial
Multramate Jan 6, 2024
595eee8
Merge remote-tracking branch 'origin/master' into division_polynomial
Multramate Feb 3, 2024
d67fb6a
Expose the auxiliary sequence
Multramate Feb 21, 2024
9abf5de
Define recursion principle for normalised EDS
Multramate Feb 22, 2024
21fd348
Merge branch 'EllipticDivisibilitySequence' into division_polynomial
Multramate Feb 22, 2024
59b7909
Redefine division polynomials
Multramate Feb 22, 2024
9f4fb43
Fix dependencies
Multramate Feb 22, 2024
750cb47
Merge branch 'EDSRec' into DivisionPolynomial
Multramate Feb 22, 2024
2e23f41
Compute degrees of division polynomials
Multramate Feb 23, 2024
e774105
Merge remote-tracking branch 'origin/master' into DivisionPolynomial
Multramate May 22, 2024
863e697
Fix merge
Multramate May 22, 2024
6a76f32
Fix upstream
Multramate May 23, 2024
343fc96
Rename division polynomials and add further documentation
Multramate May 27, 2024
0eeb05e
Golf odd/even lemmas
Multramate May 31, 2024
3176ddb
Merge remote-tracking branch 'origin/master' into division_polynomial
Multramate Jun 8, 2024
fa64986
Fix merge
Multramate Jun 8, 2024
7190e5e
Move DivisionPolynomial to DivisionPolynomial.Basic
Multramate Jun 8, 2024
d97a437
Fix names
Multramate Jun 8, 2024
83ca5ba
Remove protection
Multramate Jun 9, 2024
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
1 change: 1 addition & 0 deletions Mathlib.lean
Original file line number Diff line number Diff line change
Expand Up @@ -700,6 +700,7 @@ import Mathlib.Algebra.Tropical.Lattice
import Mathlib.Algebra.Vertex.HVertexOperator
import Mathlib.AlgebraicGeometry.AffineScheme
import Mathlib.AlgebraicGeometry.EllipticCurve.Affine
import Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Basic
import Mathlib.AlgebraicGeometry.EllipticCurve.Group
import Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian
import Mathlib.AlgebraicGeometry.EllipticCurve.Projective
Expand Down
Loading
Loading