Skip to content
This repository has been archived by the owner on Jul 24, 2024. It is now read-only.

[Merged by Bors] - feat(algebraic_geometry/EllipticCurve/weierstrass): define Weierstrass polynomials and prove basic facts #17631

Closed
wants to merge 78 commits into from
Closed
Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
78 commits
Select commit Hold shift + click to select a range
272044f
Define addition of K-rational points
Multramate Oct 26, 2022
206347e
Fix documentation
Multramate Oct 26, 2022
4cf811d
Remove simps
Multramate Oct 26, 2022
0fec7fb
Improve documentation
Multramate Oct 27, 2022
1895682
Fix documentation
Multramate Oct 27, 2022
c1ca848
Expand documentation for addition
Multramate Oct 28, 2022
6abbf02
Update documentation for K-rational points
Multramate Oct 28, 2022
66796ce
Add simps
Multramate Oct 29, 2022
abcec5f
Fix linter
Multramate Oct 29, 2022
c9de6ca
Refactor weierstrass into polynomial evaluation
Multramate Nov 15, 2022
609032b
Fix linter
Multramate Nov 15, 2022
215a0d3
Generalise fields to commutative rings
Multramate Nov 16, 2022
bb09155
Add add_eq_zero
Multramate Nov 19, 2022
7bcb93e
Add eq_zero and ne_zero lemmas
Multramate Nov 19, 2022
eb0b54f
Add nat.add_eq_iff lemmas
Multramate Nov 19, 2022
2de945c
Add nat.with_bot.add_eq_iff lemmas
Multramate Nov 19, 2022
4b17e90
Fix linter
Multramate Nov 19, 2022
ae2e640
Merge branch 'add_eq_iff' into weierstrass_polynomial
Multramate Nov 19, 2022
168c2c9
Merge branch 'cubic_discriminant' into weierstrass_polynomial
Multramate Nov 19, 2022
cb1ef4a
Prove that the weierstrass ring is a domain
Multramate Nov 19, 2022
4e76f04
Golf
Multramate Nov 19, 2022
e1396b0
feat(data/polynomial): generalize lemmas
alreadydone Nov 21, 2022
4129e49
golf erase_lead
alreadydone Nov 21, 2022
5cbf5f5
monic/quadratic irreducible lemmas
alreadydone Nov 21, 2022
5627fa4
premote to iff
alreadydone Nov 21, 2022
c2888e5
@[simps] constant_coeff
alreadydone Nov 21, 2022
8ac47c6
tinygolf, add monic namespace to a lemma
alreadydone Nov 22, 2022
beb21fe
Merge branch 'polynomial_is_unit_generalize' of https://github.com/le…
alreadydone Nov 22, 2022
65bbfd8
Add base changes
Multramate Nov 23, 2022
9cb6ce9
Merge branch 'base_change' into point
Multramate Nov 23, 2022
7221e16
Refactor base changes and make coordinates implicit
Multramate Nov 23, 2022
d29a653
Fix rcases
Multramate Nov 23, 2022
3b6d58a
Golf
Multramate Nov 23, 2022
9b45aed
incorporate #17696
alreadydone Nov 24, 2022
d13ca88
eval_ring_hom 0 = constant_coeff
alreadydone Nov 24, 2022
7af1044
add monic.is_unit_iff
alreadydone Nov 24, 2022
b5f71d1
Attempt to fix linter
Multramate Nov 24, 2022
c90bf68
Attempt to fix linter
Multramate Nov 24, 2022
2615618
Merge remote-tracking branch 'origin/master' into polynomial_is_unit_…
alreadydone Nov 24, 2022
f6ac06a
Refactor base change and variable change
Multramate Nov 24, 2022
4c339a5
Merge branch 'base_variable_change' into point
Multramate Nov 25, 2022
a79a80c
`g.nat_degree ∉ Ioc 0 (p.nat_degree / 2)` version
alreadydone Nov 27, 2022
53a2ec2
Merge remote-tracking branch 'origin/master' into polynomial_is_unit_…
alreadydone Nov 27, 2022
c0cc718
no need of interval_cases
alreadydone Nov 27, 2022
584845a
golf constant_coeff / is_unit_C
alreadydone Nov 30, 2022
dc54830
add X_add_C_ne_one / monic.eq_X_add_C
alreadydone Nov 30, 2022
557d496
Merge remote-tracking branch 'origin/master' into polynomial_is_unit_…
alreadydone Nov 30, 2022
9d283f5
golf by @tb65536
alreadydone Nov 30, 2022
3012f23
Merge remote-tracking branch 'origin/master' into point
Multramate Nov 30, 2022
b7e51ea
Merge remote-tracking branch 'origin/master' into weierstrass
Multramate Nov 30, 2022
b4eafc2
Merge remote-tracking branch 'origin/master' into weierstrass_polynomial
Multramate Nov 30, 2022
147edd4
Merge branch 'point' into weierstrass_polynomial
Multramate Nov 30, 2022
ba244bc
Merge remote-tracking branch 'origin/polynomial_is_unit_generalize' i…
Multramate Nov 30, 2022
c6dd43d
Attempt to merge
Multramate Nov 30, 2022
42bba70
Fix universe error
Multramate Nov 30, 2022
f461316
Add nat degree and monic lemmas
Multramate Dec 1, 2022
51fa702
Relocate leading coeff and monic lemmas
Multramate Dec 1, 2022
8185143
Remove nontriviality assumption
Multramate Dec 1, 2022
efabbbe
Fix linter
Multramate Dec 1, 2022
08464c8
Merge branch 'cubic.nat_degree_monic' into weierstrass_polynomial
Multramate Dec 1, 2022
c5dd6b6
Use monic.not_irreducible_iff_exists_add_mul_eq_coeff
Multramate Dec 1, 2022
4c15d32
Generalise elliptic curves into Weierstrass curves
Multramate Dec 4, 2022
1db863f
Fix linter
Multramate Dec 4, 2022
dcd7e24
Rename folder
Multramate Dec 4, 2022
a479e0b
Merge branch 'weierstrass' into weierstrass_polynomial
Multramate Dec 5, 2022
6159bf8
Relocate Weierstrass polynomials
Multramate Dec 5, 2022
126b66b
Merge remote-tracking branch 'origin/master' into weierstrass_polynomial
Multramate Dec 5, 2022
abaac2e
Define smoothness and update documentation
Multramate Dec 5, 2022
7bb7114
Golf smooth_of_Delta_ne_zero using variable changes
Multramate Dec 6, 2022
fb4106f
Fix linter
Multramate Dec 6, 2022
751fae2
Merge remote-tracking branch 'origin/master' into weierstrass_polynomial
Multramate Dec 6, 2022
ebe7022
Merge remote-tracking branch 'origin/master' into weierstrass_polynomial
Multramate Dec 6, 2022
e0c6c45
Change names
Multramate Dec 10, 2022
42b54a1
Add polynomial degree
Multramate Dec 17, 2022
632d645
Add function field
Multramate Dec 17, 2022
5effc12
Add elliptic_curve.nonsingular
Multramate Dec 17, 2022
01a0d3b
Add is_domain instance for fields
Multramate Dec 17, 2022
f401b1a
Update src/algebraic_geometry/elliptic_curve/weierstrass.lean
Multramate Dec 17, 2022
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
8 changes: 8 additions & 0 deletions docs/references.bib
Original file line number Diff line number Diff line change
Expand Up @@ -1859,6 +1859,14 @@ @Book{ serre1965
url = {https://doi.org/10.1007/978-1-4757-3910-7}
}

@Book{ silverman2009,
author = {Silverman, Joseph},
publisher = {Springer New York, NY},
series = {Graduate Texts in Mathematics},
title = {The Arithmetic of Elliptic Curves},
year = {2009}
}

@Book{ simon2011,
author = {Simon, Barry},
title = {Convexity: An Analytic Viewpoint},
Expand Down
Loading