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
14 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
- perf(Algebra/Ring): faster Ring.toAddGroupWithOne instance #38017
- 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: delete deprecated declarations to the end of 2025 #41178
3 open pull requests
4 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
8 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
- feat(Topology/UniformSpace): tag `UniformContinuous` with `@[fun_prop]` #41019
- chore: delete deprecated declarations to the end of 2025 #41178
8 open pull requests
- feat(Analysis/Complex/CauchyIntegral): Cauchy–Goursat for Unbounded Rectangles #26479
- chore: rename `continuous{,On,At,Within}_const` to `ContinuousFoo.const` #31607
- feat: lemmas for the analytic part of the proof of the Gelfond–Schneider theorem #33050
- refactor(Algebra): add type-classes for algebraic properties of `FunLike` #33477
- chore(EMetric/*): rename theorems #34096
- refactor(Analysis): golf 100 files #37968
- test: insert `@[informal]` attributes from overview #38195
- refactor: turn `Set` into a 1-field structure #39211
No open pull requests.
10 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
- chore: lake shake --add-public --keep-implied --keep-prefix --fix #40343
- feat(Analysis/Complex): add `conj_exp_ofReal_mul_I` #40464
- feat(Analysis): strengthen bounds for sin #41094
- chore: remove redudant `nonrec`'s #41259
- chore: remove simple `nonrec` occurences #41276
4 open pull requests
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
- refactor(Analysis): golf 100 files #37968
- feat: linters for recommended field_simp style, rebased #38000
- feat(NumberTheory/EulerProduct/DirichletLSeries): establish Dirichlet series for log of L-functions or Riemann-zeta #41097
4 open pull requests
- chore: golf using fun_prop [foo] syntax #34000
- feat(Analysis/SpecialFunctions): images of Ioi/Ici/Icc/Ico/Ioc/Ioo/uIcc under exp and log #41118
- feat(MeasureTheory/Integral/IntegralEqImproper): {integral,integrableOn}_comp_{exp,log}_Ioi #41119
- feat(Analysis/SpecialFunctions/Gamma/Deriv,NumberTheory/Harmonic/GammaDeriv): formulae for the derivative of Gamma / eulerMascheroni #41120
No open pull requests.
No open pull requests.
No open pull requests.
No open pull requests.
No open pull requests.
10 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
- feat(Analysis/SpecialFunctions): images of Ioi/Ici/Icc/Ico/Ioc/Ioo/uIcc under exp and log #41118
- feat(MeasureTheory/Integral/IntegralEqImproper): {integral,integrableOn}_comp_{exp,log}_Ioi #41119
- feat(Analysis/SpecialFunctions/Gamma/Deriv,NumberTheory/Harmonic/GammaDeriv): formulae for the derivative of Gamma / eulerMascheroni #41120
No open pull requests.
4 open pull requests
9 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
- refactor: use `Function.prod` instead of anonymous version #41147
- chore: remove redudant `nonrec`'s #41259
- chore: remove simple `nonrec` occurences #41276
5 open pull requests
8 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
9 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
- feat(MeasureTheory): weaken hypotheses on the continuity-multiplication and xˢ·exp(-xᵖ) integrability lemmas #40587
- chore: remove redudant `nonrec`'s #41259
3 open pull requests
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(NumberTheory): mertens first and second theorems #40656
- feat(Analysis/SpecialFunctions/Log/InvLog): add more API for inv_log and log_log #40847
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.