Project
This project will typically want to contribute some files into Mathlib itself. These files, which we can call “upstreaming candidates”, exist in this repository while they are being developed. This dashboard shows upstreaming candidates that look ready to ingest into Mathlib, and also files in the project that look “easy to unlock” for upstreaming.
For the dashboard to be correct, the repository must follow the same directory and filename structure as Mathlib for their upstreaming candidates. Namely, the upstream candidate A/B/C.lean should exist in Mathlib/A/B/C.lean.
The dashboard highlights any open PRs to the Mathlib repository containing the corresponding files.
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.
7 open pull requests (1 with relevant labels)
- feat(EllipticCurve): ZSMul formula in terms of division polynomials #13782
- feat(EllipticCurve): the universal elliptic curve #13847
- feat: Group scheme structure on Weierstrass curve #14167
- feat(AlgebraicGeometry/EllipticCurve/Scheme): define the affine scheme associated to an elliptic curve #25983
- feat(Algebra): add liftEquiv for groups, rings, algebras, and adjoin roots #36086
- chore: camel-case `finset_sum` in lemma names #37793
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.