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
2 open pull requests (0 with relevant labels)
10 open pull requests (0 with relevant labels)
Other
- ignore this: Lean pr testing 9124 #26581
- chore: fix naming of `mono` and `monotone` #26911
- chore: dedent `to_additive` docstrings #28298
- feat(Tactic/Push): add basic tags and tests #29000
- refactor (Algebra.Group.Defs): add npow/zpow/nsmul/zsmul as fields of new parents classes #29482
- experiment(Algebra): unbundle npow/zpow from Monoid/InvDivMonoid #29605
- feat(push): `@[push]` attributes for `∈` in `Set`, `Finset` and `Multiset` #30042
- refactor: rename `MulAction` to `MonoidAction` #32737
- feat: use `LE.le` for subset relation in `Set`, `Finset`, `PSet`, `ZFSet` #32983
- feat(Analysis/Convex/Intrinsic): add `affineSpan_prod_eq` and `intrinsicInterior_prod_eq` #38551
10 open pull requests (0 with relevant labels)
Other
- refactor(*): migrate from `Matrix.toLin'` to `Matrix.mulVecLin` #25012
- feat(Algebra/Module/Equiv/Basic): Restriction of scalars from a semilinear equivalence to a linear equivalence #25034
- WIP: experiments with vertex algebras #25822
- fix: replace probably erroneous usage of ⬝ (with old \cdot) by · (with \centerdot) #27403
- refactor: rename `MulAction` to `MonoidAction` #32737
- refactor(Algebra): add type-classes for algebraic properties of `FunLike` #33477
- chore(misc): fix typos #35896
- feat: @[simps] warns when generating defeq abusing lemmas #37528
- feat(Tactic): convert now discharges side goals at reducible transparency #39039
- experiment: have `LinearMap` extend `DistribMulActionHom` #40001
1 open pull request (0 with relevant labels)
4 open pull requests (0 with relevant labels)
Other
8 open pull requests (0 with relevant labels)
Other
- chore: add typeclasses to unify various `add_top`, `add_eq_top`, etc. #14598
- refactor: Make ENNReal an abbrev #23509
- chore: make `finiteness` a default tactic #26090
- chore: fix naming of `mono` and `monotone` #26911
- feat: `GroupWithZero` versions of `le` lemmas #34120
- feat(Algebra/Order/Ring): replace ENNReal lemmas with WithTop versions #34674
- experiment: define a simproc for simplifying `a = b` from `b = a` #36534
- test(Tactic/Algebra): try to replace `ring` with algebra in many places #38637
15 open pull requests (0 with relevant labels)
Other
- chore: add typeclasses to unify various `add_top`, `add_eq_top`, etc. #14598
- feat: Add type class for ENat-valued floor functions #15773
- feat: Topology on `ENat` #15774
- feat(RingTheory/Valuation/PrimeMultiplicity): define `WithTop ℤ`-valued prime multiplicity on a fraction field #19596
- feat: Multiplicity and prime-adic valuation of derivations #19621
- feat(Topology/Instances/ENat): ENat and tsum #23503
- feat: replace `IsWellFounded` with `WellFounded` #35602
- feat(Valued/ValuationTopology): creating instances of `IsValuativeTopology` #36769
- fix(RingTheory/Valuation): change `ValueGroup` from taking HomClass to Hom #36911
- refactor(Order): make completeness typeclasses mixins #38537
- feat(NumberTheory/ModularForms): Sturm bound for finite-index subgroups #39000
- feat(Mathlib): preparations for finite-index Sturm bound #39083
- feat(NumberTheory/ModularForms): Galois product machinery #39086
- feat(NumberTheory/ModularForms): integer cusp width and T-power slash action #39087
- feat(NumberTheory/ModularForms): norm map decomposition for Sturm bound #39088
No open pull requests.
1 open pull request (0 with relevant labels)
11 open pull requests (0 with relevant labels)
Other
- feat: The finite product of semi-rings (in terms of measure theory) is a semi-ring. #25902
- feat(MeasureTheory): finite unions of sets in a semi-ring (in terms of measure theory) form a ring #25903
- chore: fix links #27709
- feat(Tactic/Push): add basic tags and tests #29000
- perf: remove some `aesop`s and `grind`s #35738
- feat (Topology/Compactness/CompactSystem): closed and compact square cylinders form a compact system #36160
- experiment: define a simproc for simplifying `a = b` from `b = a` #36534
- feat(Data/Set): add Set.diag API #38380
- chore(Data/Set): reduce defeq abuse of `Set α = α → Prop` #39110
- refactor: turn `Set` into a 1-field structure #39211
- feat: `Pi.map` rename to `Function.map` #39233
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
- feat(Mathlib.Topology.Algebra.Module.Equiv): add results on IsHomeomorph #39476
- chore: tag `(Continuous)LinearEquiv.prodCongr_symm` with `@[simp]` #39975
1 open pull request (0 with relevant labels)
1 open pull request (0 with relevant labels)
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.