Upstreaming dashboard
The eventual goal of the MeanFourier project is to be fully upstreamed to Mathlib.
As such, it is crucial to continuously organise upstreaming from MeanFourier to Mathlib.
The way we organise this is with the following two lists,
showing files with no MeanFourier 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: mean-fourier
8 open pull requests (0 with relevant labels)
Other
- perf: do not search algebraic hierarchy when searching `FunLike` hierarchy #17675
- refactor: deprecate `SemilinearMapClass` #18805
- refactor: deprecate `ContinuousLinearMapClass` #33448
- refactor: deprecate `LinearIsometryClass` #33450
- feat: lemmas about `IsometryClass` #33454
- refactor(Analysis): golf 100 files #37968
- feat(Analysis): more `LinearIsometryEquiv` API #39144
- refactor(Analysis): golf `Mathlib/Analysis/Normed/Operator/LinearIsometry` #39187
2 open pull requests (0 with relevant labels)
8 open pull requests (0 with relevant labels)
Other
- fix: replace probably erroneous usage of ⬝ (with old \cdot) by · (with \centerdot) #27403
- refactor: deprecate `ContinuousLinearMapClass` #33448
- refactor: deprecate `LinearIsometryClass` #33450
- feat: add instances of `LawfulInv` #33810
- fix(fun_prop): do not unfold semireducible definitions in the presence of projections #35548
- feat: flip arguments for continuous linear maps under finite dimension assumptions #36775
- refactor(Algebra): replace `SemilinearEquivClass.semilinearEquiv` by structure-specific coercions #37944
- feat(Analysis): more `LinearIsometryEquiv` API #39144
10 open pull requests (0 with relevant labels)
Other
- refactor: deprecate `ContinuousLinearMapClass` #33448
- refactor: deprecate `LinearIsometryClass` #33450
- feat: analytification of schemes (affine case) #34626
- fix(fun_prop): do not unfold semireducible definitions in the presence of projections #35548
- chore: override `npow` in compositional monoids #36878
- chore: call `dsimp` in the default tactic of `ContinuousLinearMap` #37386
- feat: `NSMul`/`NPow` type class #38036
- refactor(Analysis): add `toSpanSingleton` isometry API #38272
- feat: use `Is*Apply` classes for continuous linear maps #38561
- feat(Analysis): more `LinearIsometryEquiv` API #39144
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.