Upstreaming dashboard
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.
4 open pull requests
15 open pull requests
- chore: deprecate `LinearOrderedComm{Monoid, Group}WithZero` #23621
- refactor: unbundle algebra from `{Seminormed, Normed}(Add)(Comm)Group` #23966
- refactor: unbundle algebra from `(NonUnital){Seminormed, Normed}(Comm)Ring` #24040
- refactor: unbundle algebra from `*NormedField` #24058
- refactor: unbundle algebra from `*CStarAlgebra` #24106
- feat(Algebra/Order/Field/Basic): generalize lemmas #24378
- feat(Algebra/Module/ZLattice): align `ZSpan.floor` to `Int.floor` API #33746
- feat: also check for norm_num in the flexible linter #37671
- feat(Algebra/Order/Floor): weaken assumptions on theorems about `FloorRing` #37964
- chore: remove redundant `unfold`s #39029
- feat(Tactic): convert now discharges side goals at reducible transparency #39039
- chore: replace `by calc` by `calc` whenever possible #40292
- chore: remove redudant `have`'s #41749
- feat(Algebra/Order/Floor): floor-of-sum dichotomy via fractional parts #41861
- feat(Algebra/Order/Floor): add fract-absorption lemmas for sums and d… #42080
3 open pull requests
5 open pull requests
- feat: maximum modulus principle for functions vanishing at infinity #9469
- refactor(Topology/UniformSpace/Completion): more descriptive names for `α → Completion α` #20527
- chore: rename `continuous{,On,At,Within}_const` to `ContinuousFoo.const` #31607
- test: insert `@[informal]` attributes from overview #38195
- chore(Order/Filter/Extr): rename various lemmas #41863
14 open pull requests
- refactor(Analysis/Normed/{Group/Field}/Basic): Let `extends` generate the repeated fields #9642
- feat(Data/Complex/Exponential): prove some useful results about the complex exponential. #20313
- chore: fix links #27709
- chore: rename `continuous{,On,At,Within}_const` to `ContinuousFoo.const` #31607
- chore: deprecate duplicate theorems about `IsBotZeroClass` #38663
- chore: replace `by calc` by `calc` whenever possible #40292
- chore: no `noncomputable` inside noncomputable section #41551
- chore: replace terminal `convert` with `exact` #41762
- chore: replace `simp_all` with `simp` whenever possible #41896
- chore: remove declarations deprecated between 2021-08-11 and 2026-02-11 #42655
- refactor: unify `Set.mem_ofPred_eq` into `Set.mem_ofPred` #42692
- chore(Data): move some files to Basic #43176
- chore: delete deprecated declarations from February 2026 #43178
- chore: deprecated aliases for #43176 #43222
4 open pull requests
1 open pull request
9 open pull requests
- feat(Analysis/Complex/CauchyIntegral): Cauchy–Goursat for Unbounded Rectangles #26479
- chore: rename `continuous{,On,At,Within}_const` to `ContinuousFoo.const` #31607
- refactor(Algebra): add type-classes for algebraic properties of `FunLike` #33477
- chore(EMetric/*): rename theorems #34096
- test: insert `@[informal]` attributes from overview #38195
- refactor: turn `Set` into a 1-field structure #39211
- refactor(Data): make `Set` a one-field structure #41506
- chore: remove `noncomputable section` when only theorems in file #41554
- feat(Analysis/Complex/CauchyIntegral): add Cauchy formula at interior points #43100
No open pull requests.
6 open pull requests
- chore: reduce `Topology` imports in `Data` #29012
- chore(Data/Real): encapsulate real numbers #38702
- feat(Analysis/Complex): the equality case of the triangle inequality #39915
- chore: no `noncomputable` inside noncomputable section #41551
- chore(Data): move some files to Basic #43176
- chore: deprecated aliases for #43176 #43222
11 open pull requests
- feat: `GroupWithZero` versions of `le` lemmas #34120
- chore: golf using .ne and friends #37553
- feat: linters for recommended field_simp style, rebased #38000
- test: insert `@[informal]` attributes from overview #38195
- feat(Analysis): van der Corput's lemma #39406
- feat(Analysis/Complex): add `conj_exp_ofReal_mul_I` #40464
- chore: remove redudant `nonrec`'s #41259
- chore: remove simple `nonrec` occurences #41276
- feat(Tactic): automatic positivity attribute #41895
- chore: add newline between public and private imports #42063
- experiment: make `neg_div'` a `@[simp]` lemma #42882
No open pull requests.
No open pull requests.
5 open pull requests
- chore: change some `nlinarith`s to `linear_combination`s #19352
- chore: golf using the field tactic #37461
- feat: linters for recommended field_simp style, rebased #38000
- fix(Tactic/FunProp): apply theorems at reducible transparency #42330
- chore: use simp instead of norm_num where simp suffices #43035
No open pull requests.
No open pull requests.
No open pull requests.
No open pull requests.
No open pull requests.
9 open pull requests
- chore: change some `linarith`s to `linear_combination`s #18841
- feat(Tactic/Push): add basic tags and tests #29000
- feat: new `isolate` tactic #29982
- chore: replace long terminal `rw […]`:s (≥4 lemmas) with bare `simp`:s #36774
- chore: golf using .ne and friends #37553
- test: insert `@[informal]` attributes from overview #38195
- refactor: turn `Set` into a 1-field structure #39211
- refactor(Data): make `Set` a one-field structure #41506
- chore: no `noncomputable` inside noncomputable section #41551
No open pull requests.
4 open pull requests
10 open pull requests
- chore: change some `linarith`s to `linear_combination`s #18841
- feat(Analysis/Calculus/FDeriv): Fderiv on torsors #24243
- chore: rename `continuous{,On,At,Within}_const` to `ContinuousFoo.const` #31607
- feat(Tactic/FunProp): set up fun_prop for HasDerivAt #37270
- feat(Tactic/FunProp): theorem priority #37365
- chore: replace `by calc` by `calc` whenever possible #40292
- chore: remove redudant `nonrec`'s #41259
- chore: remove simple `nonrec` occurences #41276
- chore: remove `noncomputable section` when only theorems in file #41554
- chore: replace terminal `convert` with `exact` #41762
10 open pull requests
- WIP: feat: Holder's inequality n-ary #12279
- feat: more linting of cdots #12411
- chore: change some `linarith`s to `linear_combination`s #18841
- feat: new `isolate` tactic #29982
- chore: golf using .ne and friends #37553
- feat(Analysis/SpecialFunctions/Gamma/Deriv,NumberTheory/Harmonic/GammaDeriv): formulae for the derivative of Gamma / eulerMascheroni #41120
- Rename Real rpow order lemmas #41396
- chore: no `noncomputable` inside noncomputable section #41551
- chore: make `norm_num` normalize negative rationals as `-a / b` #42498
- chore(Analysis/SpecialFunctions/Pow/Real): deprecate six misnamed duplicate log/rpow lemmas #42533
10 open pull requests
- feat: integrals and integrability with .re #17176
- feat(LocallyIntegrable): generalise more to enorms #24862
- chore: more enorm lemmas #27446
- refactor: unbundle algebra from `ENormed*` #28803
- feat(MeasureTheory): add `MemLp.Const` class and instances to unify `p = ∞` and `μ.IsFiniteMeasure` cases #30030
- perf: unbundle algebra from `ENormed*`, April 2026 version #38032
- feat: fun_prop for integrability #39323
- feat(FunProp): tag integrableOn #39325
- chore: rename Directed to Predirected #42290
- chore(MeasureTheory): generalize hypotheses to `NullMeasurableSet` #42924
8 open pull requests
- refactor: unbundle algebra from `ENormed*` #28803
- chore: rename `continuous{,On,At,Within}_const` to `ContinuousFoo.const` #31607
- feat(Topology/Compactness/CompactSystem): set system of countable intersections of sets in a compact system is again a compact system #36225
- perf: unbundle algebra from `ENormed*`, April 2026 version #38032
- refactor(Order): make completeness typeclasses mixins #38537
- feat(IntervalIntegrable): add `fun_prop` support #38822
- feat: define contour integrals #39254
- chore: remove redudant `nonrec`'s #41259
4 open pull requests
- feat(Tactic/Push): add basic tags and tests #29000
- chore(MeasureTheory/IntervalIntegral): generalize fundamental theorem of calculus to `HasDerivWithinAt` instead of `HasDerivAt` #31836
- chore: do not use `inf` `sup` in `LinearOrder` lemmas #35881
- chore: remove `noncomputable section` when only theorems in file #41554
7 open pull requests
- feat(Tactic/Linter): linter for comments that should become docstrings #36636
- feat(NumberTheory): Chebyshev's lower bound on primorial #37299
- feat: also check for norm_num in the flexible linter #37671
- feat: linters for recommended field_simp style, rebased #38000
- chore: replace `by calc` by `calc` whenever possible #40292
- feat(Tactic): automatic positivity attribute #41895
- chore: use simp instead of norm_num where simp suffices #43035
No 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.