Upstreaming dashboard

Files ready to upstream

The following files are sorry-free and do not depend on any other file, meaning they can be readily PRed to Mathlib.

PRs are grouped as 'relevant' if they contain the following label: toric

Toric.Mathlib.Algebra.Polynomial.Bivariate

4 open pull requests (1 with relevant labels)

Relevant

• refactor(Polynomial/Bivariate): swap `X` and `Y` for improved notation #27196
  WIP, t-algebra, toric

Other

• feat(EllipticCurve): ZSMul formula in terms of division polynomials #13782
  t-algebra, t-number-theory, blocked-by-other-PR, merge-conflict, t-algebraic-geometry
• feat(EllipticCurve): the universal elliptic curve #13847
  merge-conflict, awaiting-author, t-algebra, t-algebraic-geometry
• feat: Group scheme structure on Weierstrass curve #14167
  merge-conflict, WIP, t-algebraic-geometry, workshop-AIM-AG-2024

Files easy to unlock

The following files do not depend on any other file but still contain sorry, usually indicating that working on eliminating those sorries might unblock some part of the project.

Toric.Mathlib.ToricIdeal.ToricIdeal

3 sorries