Upstreaming dashboard
The eventual goal of the LeanCamCombi project is to not contain any significant new formalisation, but instead to act as a shallow layer over Mathlib showing concretely how to turn paper-combinatorics into Lean-combinatorics.
As such, it is crucial to continuously upstream code from LeanCamCombi to Mathlib. The way we organise this is with the following two lists, showing files with no LeanCamCombi 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 LeanCamCombi, meaning they can be readily PRed to Mathlib.
LeanCamCombi.MultipartiteLeanCamCombi.MetricBetweenLeanCamCombi.UtilLeanCamCombi.GrowthInGroups.LinearLowerBoundLeanCamCombi.GrowthInGroups.ConstructibleSetDataLeanCamCombi.Kneser.MulStabLeanCamCombi.ConvexityRefactor.StdSimplexLeanCamCombi.GraphTheory.ExampleSheet2LeanCamCombi.PlainCombi.OrderShatterLeanCamCombi.Corners.CombiDegenLeanCamCombi.PhD.VCDim.AddVCDimLeanCamCombi.Mathlib.RingTheory.FinitePresentationLeanCamCombi.Mathlib.Order.BooleanSubalgebraLeanCamCombi.Mathlib.Analysis.RCLike.BasicLeanCamCombi.Mathlib.Topology.MetricSpace.MetricSeparatedLeanCamCombi.Mathlib.Probability.ProbabilityMassFunction.ConstructionsLeanCamCombi.Mathlib.Data.Prod.LexLeanCamCombi.Mathlib.Data.Set.Image- refactor(Finset): redefine Finset.diag, review API #11617
- style: replace preimage_val with ↓∩ notation #12418
- chore: remove global
Quotient.mk⟦·⟧notation #17127 - chore: tidy various files #20225
- feat: split a set in the prime spectrum of
R[X]into its localization away fromc : Rand quotient bycparts #20303 - feat: commutative semirings satisfy rank condition #20584
- feat(Function/Basic): iff lemmas for injectivity/surjectivity of composition #20646
LeanCamCombi.Mathlib.Data.Set.Pointwise.SMulLeanCamCombi.Mathlib.RingTheory.Spectrum.Prime.TopologyLeanCamCombi.Mathlib.Order.Partition.FinpartitionLeanCamCombi.Mathlib.Combinatorics.SimpleGraph.Basic- chore: deprime
induction, casesinCombinatorics#16250 - feat(Combinatorics/SimpleGraph): define turanDensity #20171
- feat(Combinatorics/SimpleGraph): define deleteIncidenceSet #20681
- chore: cleanup many porting notes in Combinatorics #20823
- refactor: create HasAdj class, define Digraph, and generalize some SimpleGraph API #4127
- chore: deprime
LeanCamCombi.Mathlib.Combinatorics.SimpleGraph.Finite- feat(Combinatorics/SimpleGraph): Some lemmas about walk, cycle and Hamiltonian cycle #15711
- feat(SimpleGraph): The Bondy-Chvátal theorem #15720
- chore: deprime
induction, casesinCombinatorics#16250 - feat(Combinatorics/SimpleGraph): define turanDensity #20171
- chore: use mixin ordered algebraic typeclasses (part 1) #20594
- feat(Combinatorics/SimpleGraph): define deleteIncidenceSet #20681
- chore: cleanup many porting notes in Combinatorics #20823
- feat(Combinatorics/SimpleGraph): prove finite results for induced subgraphs of
G.support#20825
LeanCamCombi.Mathlib.Combinatorics.SimpleGraph.Subgraph- feat(Combinatorics/SimpleGraph/Path): representatives of connected components #20024
- feat(Combinatorics/SimpleGraph): define turanDensity #20171
- feat(Combinatorics/SimpleGraph): add monotonicity of number of odd components #20398
- feat(Combinatorics/SimpleGraph): define deleteIncidenceSet #20681
- refactor: create HasAdj class, define Digraph, and generalize some SimpleGraph API #4127
LeanCamCombi.Mathlib.Combinatorics.SetFamily.ShatterLeanCamCombi.Mathlib.Algebra.MvPolynomial.Equiv- feat: add lemma about
degreeOf_eq_degree#12664 - chore(*): deprecate
Option.elim'#15448 - feat(Data/Finsupp/Fin): Add
Finsuppoperations onFintuple #19315 - chore: move results on
Σ i : Fin n, f iearlier #19415 - feat(MvPolynomial/Equiv): Add
MvPolynomial.finSuccEquivNth#19467 - feat(MvPolynomial): commuting the variables of mv-polynomials of mv-polynomials #20447
- feat: add lemma about
LeanCamCombi.Mathlib.Algebra.MvPolynomial.Basic- feat(Mathlib.RingTheory.TensorProduct.Polynomial) : tensor product of a (univariate) polynomial ring #12294
- chore: attribute [induction_eliminator] #12605
- feat: add
simplemmacoeff_eq_zero_of_not_mem_support#13026 - wip: run the pedantic linter on mathlib #15941
- chore(Algebra/{MonoidAlgebra,Polynomial}): algebra structure in
Basic.lean#19281 - feat(Data/Finsupp): generalise
Finsuppto any “zero” value #19337 - chore: make
SMulCommClass A A BandSMulCommClass A B Bhigher priority #7875
LeanCamCombi.Mathlib.Algebra.MvPolynomial.DegreesLeanCamCombi.Mathlib.Algebra.Ring.Hom.Defs- feat(Algebra/ModuleCat/Differentials/Presheaf): the presheaf of relative differentials #17469
- feat(Algebra/ModuleCat/Differentials/Sheaf): the sheaf of relative differentials #17471
- refactor(*): generalize typeclass assumptions in morphisms #17757
- refactor: make
LinearOrderedCommMonoidWithZeroextendOrderBot#19193 - chore: golf using
List.toArrayMap#20613
Files easy to unlock
The following files do not depend on any other LeanCamCombi file but still contain sorry, usually indicating that working on eliminating those sorries might unblock some part of the project.
LeanCamCombi.MinkowskiCaratheodory2 sorriesLeanCamCombi.DiscreteDeriv4 sorriesLeanCamCombi.PosDiffs2 sorriesLeanCamCombi.SliceRank2 sorriesLeanCamCombi.Impact5 sorriesLeanCamCombi.GroupMarking17 sorriesLeanCamCombi.StableCombi.Rel2 sorriesLeanCamCombi.SimplicialComplex.Simplex5 sorriesLeanCamCombi.GrowthInGroups.ApproximateSubgroup7 sorriesLeanCamCombi.GraphTheory.ExampleSheet116 sorriesLeanCamCombi.PlainCombi.VanDenBergKesten1 sorryLeanCamCombi.PlainCombi.LittlewoodOfford1 sorryLeanCamCombi.Mathlib.GroupTheory.OrderOfElement1 sorryLeanCamCombi.Mathlib.Combinatorics.Schnirelmann6 sorriesLeanCamCombi.Mathlib.Analysis.Convex.Independence1 sorryLeanCamCombi.Mathlib.Analysis.Convex.Extreme10 sorriesLeanCamCombi.Mathlib.Analysis.Convex.SimplicialComplex.Basic1 sorryLeanCamCombi.Mathlib.Data.List.DropRight6 sorriesLeanCamCombi.Mathlib.Order.RelIso.Group1 sorryLeanCamCombi.Mathlib.LinearAlgebra.AffineSpace.FiniteDimensional1 sorry