mathlib3

e2e7f2ac - feat(algebraic_geometry/elliptic_curve/point): the group law on the nonsingular rational points of a Weierstrass curve (#18000)

feat(algebraic_geometry/elliptic_curve/point): the group law on the nonsingular rational points of a Weierstrass curve (#18000) Define a group structure on the nonsingular rational points of a Weierstrass curve by constructing an explicit injective group homomorphism into the class group of its coordinate ring and therefore proving associativity of the addition law. Co-authored-by: Junyan Xu <junyanxumath@gmail.com> - [x] depends on: #17999 - [x] depends on: #17194 - [x] depends on: #18038 - [x] depends on: #18101 - [x] depends on: #19121 Co-authored-by: Junyan Xu <junyanxumath@gmail.com>