Upstreaming dashboard
The eventual goal of the PFR project is to be fully upstreamed to Mathlib.
As such, it is crucial to continuously organise upstreaming from PFR to Mathlib.
The way we organise this is with the following two lists,
showing files with no PFR 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.
12 open pull requests
- chore: use `open scoped` #4960
- feat(Algebra/BigOperators/Fin): Add `finSigmaFinEquiv` #19013
- feat(Data/Finsupp/Fin): Add `Finsupp` operations on `Fin` tuple #19315
- feat(MvPolynomial/Equiv): Add `MvPolynomial.finSuccEquivNth` #19467
- feat(BigOperators/Fin): Sum/product over `Fin` intervals #19697
- ignore this: Lean pr testing 9124 #26581
- chore: dedent `to_additive` docstrings #28298
- chore(Mathlib): replace `=>` by `↦` #28622
- Lean pr testing 11156 #31587
- feat(Mathlib/Algebra/BigOperators/Fin): lemma about List.ofFn #37405
- chore: golf using .ne and friends #37553
- chore(Mathlib): shake mathlib harder #38408
4 open pull requests
No open pull requests.
13 open pull requests
- feat: add Qq wrappers for ToExpr #5952
- style: Change Subtype.val to (↑) #12465
- feat(MvPolynomial/Equiv): Add `MvPolynomial.finSuccEquivNth` #19467
- feat: `Clone` and some instances #20051
- feat: Definition of `Clone` #23460
- chore: fix recursors #23489
- Post's lattice #24744
- feat: a linter for duplicated `open` #25362
- feat: check indentation of doc-strings #27897
- Lean pr testing 11156 #31587
- chore: fix markdown list indentation #35281
- feat(Data/Fin): add several lemmas about subtraction of `Fin.{castLT, castAdd, castSucc, castPred}` #35610
- chore(Data): avoid lazy continuation in md lists #36682
7 open pull requests
- feat: grind tags for set operations #27683
- feat(Tactic/Push): add basic tags and tests #29000
- feat(push): `@[push]` attributes for `∈` in `Set`, `Finset` and `Multiset` #30042
- bench: lean4#10832 #30642
- bench: before lean4#10832 #30643
- (WIP) Separation axioms #32865
- feat: use `LE.le` for subset relation in `Set`, `Finset`, `PSet`, `ZFSet` #32983
5 open pull requests
No open pull requests.
No open pull requests.
1 open pull request
4 open pull requests
3 open pull requests
6 open pull requests
- style: replace preimage_val with ↓∩ notation #12418
- feat(Dynamics): Hopf decomposition #16150
- Clean up quotient APIs #16210
- feat(Topology/Baire/BaireMeasurable): add the Kuratowski-Ulam theorem #17368
- feat: blumenthal's zero-one law for Brownian motion #37259
- chore(MeasureTheory): replace remaining `@[measurability]` attributes by `@[fun_prop]` #38512
9 open pull requests
- chore(Co*variantClass): replace eta-expanded (· * ·), (· + ·), (· ≤ ·), (· < ·) #6777
- feat: more linting of cdots #12411
- chore: add typeclasses to unify various `add_top`, `add_eq_top`, etc. #14598
- Docstring enumerations #28067
- feat: extend the `whitespace` linter to proof bodies #30658
- feat: use `LE.le` for subset relation in `Set`, `Finset`, `PSet`, `ZFSet` #32983
- refactor: use `OrderSupInfSet` #35263
- feat(Topology/Algebra/InfiniteSum): Deprecate generalized ENNReal lemmas #38193
- [incomplete] rename Directed -> Predirected #38792
4 open pull requests
No open pull requests.
No open pull requests.
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.