Upstreaming dashboard
The eventual goal of the Toric project is to be fully upstreamed to Mathlib.
As such, it is crucial to continuously organise upstreaming from Toric to Mathlib.
The way we organise this is with the following two lists,
showing files with no Toric dependencies depending on whether they contain sorry or not.
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
18 open pull requests (0 with relevant labels)
Other
- chore: use `open scoped` #4960
- refactor: Use flat structures for morphisms #6791
- perf: do not search algebraic hierarchy when searching `FunLike` hierarchy #17675
- feat(RingTheory/Pure): pure submodules #22909
- chore(Algebra/*-{Category,Homology}): remove unnecessary universe variables #24285
- chore(RingTheory/Ideal): make `RingHom.ker` take a `RingHom` instead of `RingHomClass` #25138
- feat(RingTheory/GradedAlgebra): homogeneous relation #27307
- chore(Mathlib): replace `=>` by `↦` #28622
- refactor(Algebra/Algebra/Equiv): allow for non-unital `AlgEquiv` #29354
- refactor: rename `MulAction` to `MonoidAction` #32737
- chore: run docstrings through mdformat #35686
- chore: override `npow` in compositional monoids #36878
- refactor(Algebra): semialgebra maps #38376
- chore(Algebra): `coe_algHom` -> `coe_toAlgHom` #38950
- chore(Algebra): consolidate variables and sections for `AlgHom`/`AlgEquiv` #38964
- chore(Algebra): `coe_ringHom` -> `coe_toRingHom` #38966
- chore: shake --keep-implied --keep-prefix --fix #39386
- chore(Data/{FunLike/SetLike}): unprime `coe_injective'` #40215
10 open pull requests (1 with relevant labels)
Relevant
Other
- feat(EllipticCurve): ZSMul formula in terms of division polynomials #13782
- feat(EllipticCurve): the universal elliptic curve #13847
- feat(AlgebraicGeometry/EllipticCurve/Scheme): define the affine scheme associated to an elliptic curve #25983
- ignore this: Lean pr testing 9124 #26581
- trying #28803 using lean#10178 #29741
- Nagell lutz #35863
- feat(Algebra): add liftEquiv for groups, rings, algebras, and adjoin roots #36086
- perf: increase some instance priorities #39267
- feat: make the `dupNamespace` linter catch any duplicate namespace(s) #39793
12 open pull requests (0 with relevant labels)
Other
- chore: weaken commutativity assumptions for AdjoinRoot.lift and AdjoinRoot.liftHom #9564
- chore(FieldTheory/KummerExtension): move some lemmas earlier #9978
- feat: more linting of cdots #12411
- Clean up quotient APIs #16210
- chore(Data/Quot): deprecate `ind*'` APIs #16314
- chore(RingTheory/Ideal): make `RingHom.ker` take a `RingHom` instead of `RingHomClass` #25138
- feat(AlgebraicGeometry/EllipticCurve/Scheme): define the affine scheme associated to an elliptic curve #25983
- refactor(Algebra/Algebra/Equiv): allow for non-unital `AlgEquiv` #29354
- feat(RingTheory/AdjoinRoot): add IsFractionRing for AdjoinRoot #35157
- feat(Algebra): add liftEquiv for groups, rings, algebras, and adjoin roots #36086
- refactor(Algebra): semialgebra maps #38376
- chore(Algebra): `coe_ringHom` -> `coe_toRingHom` #38966
6 open pull requests (0 with relevant labels)
Other
- feat(RingTheory): category of finite étale algebras over a separably closed field #38054
- chore(Algebra): `coe_algHom` -> `coe_toAlgHom` #38950
- chore(Algebra): consolidate variables and sections for `AlgHom`/`AlgEquiv` #38964
- chore(Algebra): `coe_ringHom` -> `coe_toRingHom` #38966
- chore(Algebra/Module): rename multiplication lemmas and add `push/pull_end` attributes #39508
- feat: make the `dupNamespace` linter catch any duplicate namespace(s) #39793
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.