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 the keyword sorry or not.

Files ready to upstream

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

• Toric.MvLaurentPolynomial
• Toric.Mathlib.Algebra.MonoidAlgebra.Basic
  • chore(Algebra/MonoidAlgebra): split Defs.lean further #19091
  • chore(Algebra.Polynomial): split Polynomial/Basic.lean into smaller files #19097
  • chore(Algebra/{MonoidAlgebra,Polynomial}): algebra structure in Basic.lean #19281
  • chore(Algebra/*-{Category,Homology}): remove unnecessary universe variables #24285
  • refactor: make the algebra hierarchy use flat structures #3171
  • chore: use open scoped #4960
  • fix: deduplicate variables #6079
  • feat: Lindemann-Weierstrass Theorem #6718
  • chore: make SMulCommClass A A B and SMulCommClass A B B higher priority #7875
  • refactor: allow non-unital AlgEquiv #8686
• Toric.Mathlib.Algebra.NoZeroSMulDivisors.Defs
  • Mr librarynote def 2b #23786
  • chore: replace Monoid.IsTorsionFree with IsMulTorsionFree #24311
  • feat: more lemmas about torsion-free monoids #24312
• Toric.Mathlib.Algebra.Category.Grp.Basic
  • refactor(CategoryTheory/Limits): colimits in Type #23364
  • feat: multicoequalizers in the category of types #23872
• Toric.Mathlib.Algebra.Category.MonCat.Basic
  • refactor(CategoryTheory/Limits): colimits in Type #23364
  • feat: multicoequalizers in the category of types #23872
  • refactor: Use flat structures for morphisms #6791
• Toric.Mathlib.Algebra.Category.CommAlg.Basic
  • feat(CommAlg): the category of commutative algebras #23601
• Toric.Mathlib.Algebra.Module.Equiv.Defs
  • refactor: deprecate MulEquivClass #18806
  • Mr librarynote def 2b #23786
  • chore: semilinearize LinearAlgebra.TensorProduct.Basic #24208
  • chore: merge repeated Type* binders #24322
• Toric.Mathlib.LinearAlgebra.TensorProduct.Basic
  • chore: attribute [induction_eliminator] #12605
  • chore: semilinearize LinearAlgebra.TensorProduct.Basic #24208
• Toric.Mathlib.LinearAlgebra.TensorProduct.Associator
  • chore: semilinearize LinearAlgebra.TensorProduct.Basic #24208
• Toric.Mathlib.LinearAlgebra.Finsupp.LinearCombination
  • feat(Data/Finsupp/Basic): Finsupp.optionElim' #13861
• Toric.Mathlib.LinearAlgebra.FreeModule.Finite.Basic
• Toric.Mathlib.Analysis.Convex.Polytope
  • feat: polytopes #23940
• Toric.Mathlib.Analysis.Convex.Cone.Pointed
  • refactor(Convex/Cone): reorder, streamline #24149
• Toric.Mathlib.GroupTheory.MonoidLocalization.Basic
  • chore(Data/Quot): deprecate ind*' APIs #16314
  • chore: get rid of generic hom coercions #21031
  • refactor: make use of FunLike for Submonoid.LocalizationMap #22655
• Toric.Mathlib.GroupTheory.MonoidLocalization.DivPairs
  • feat: submonoid of pairs with quotient in a submonoid #22635
• Toric.Mathlib.Data.Finset.Powerset
  • feat: extensible push_neg tactic #21769
  • feat: a finitely generated submonoid has a minimal generating set #23904
• Toric.Mathlib.CategoryTheory.Monoidal.Mod_
  • feat(CategoryTheory/Monoidal/Mod_): add a class version of modules over monoid objects #23972
• Toric.Mathlib.CategoryTheory.Monoidal.Mon_
  • feat(CategoryTheory/Monoidal): premonoidal categories #21488
  • chore: rename AlgebraCat to Alg #23721
  • feat: an equivalence of categories lifts to an equivalence of their group objects #23912
• Toric.Mathlib.CategoryTheory.WithTerminal.Cones

Files easy to unlock

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

• Toric.Hopf.GroupLike 1 sorry
• Toric.Mathlib.RingTheory.HopfAlgebra.Basic 1 sorry
• Toric.Mathlib.RingTheory.Bialgebra.Hom 4 sorries