feat: port AlgebraicGeometry.EllipticCurve.Weierstrass (#5294)

Co-authored-by: Xavier-François Roblot <46200072+xroblot@users.noreply.github.com> Co-authored-by: Riccardo Brasca <riccardo.brasca@gmail.com> Co-authored-by: Chris Hughes <chrishughes24@gmail.com> Co-authored-by: Moritz Firsching <firsching@google.com>
leanprover-community · Jul 6, 2023 · d4126d4 · d4126d4
1 parent 3c21b20
commit d4126d4
Show file tree

Hide file tree

Showing 3 changed files with 1,002 additions and 0 deletions.
diff --git a/Mathlib.lean b/Mathlib.lean
@@ -411,6 +411,7 @@ import Mathlib.Algebra.TrivSqZeroExt
 import Mathlib.Algebra.Tropical.Basic
 import Mathlib.Algebra.Tropical.BigOperators
 import Mathlib.Algebra.Tropical.Lattice
+import Mathlib.AlgebraicGeometry.EllipticCurve.Weierstrass
 import Mathlib.AlgebraicGeometry.GammaSpecAdjunction
 import Mathlib.AlgebraicGeometry.LocallyRingedSpace
 import Mathlib.AlgebraicGeometry.LocallyRingedSpace.HasColimits