feat: port AlgebraicGeometry.EllipticCurve.Point (#5541)

Co-authored-by: David Kurniadi Angdinata <dka31@cantab.ac.uk> Co-authored-by: David Kurniadi Angdinata <dka31@cantab.ac.uk>
leanprover-community · Jul 3, 2023 · c7c8ac3 · c7c8ac3
1 parent f32c393
commit c7c8ac3
Show file tree

Hide file tree

Showing 3 changed files with 1,055 additions and 25 deletions.
diff --git a/Mathlib.lean b/Mathlib.lean
@@ -417,6 +417,7 @@ import Mathlib.Algebra.Tropical.Basic
 import Mathlib.Algebra.Tropical.BigOperators
 import Mathlib.Algebra.Tropical.Lattice
 import Mathlib.AlgebraicGeometry.AffineScheme
+import Mathlib.AlgebraicGeometry.EllipticCurve.Point
 import Mathlib.AlgebraicGeometry.EllipticCurve.Weierstrass
 import Mathlib.AlgebraicGeometry.FunctionField
 import Mathlib.AlgebraicGeometry.GammaSpecAdjunction