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.
5 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
- 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: `wlog` dischargers (`grind` by default) #43315
- feat: weaken even more assumptions on theorems about `FloorRing` #44741
- WIP: Feat/positivity lemma #44923
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: golf using new `@[gcongr]` lemmas #44335
11 open pull requests
- refactor(Analysis/Normed/{Group/Field}/Basic): Let `extends` generate the repeated fields #9642
- 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
- refactor: unify `Set.mem_ofPred_eq` into `Set.mem_ofPred` #42692
- chore: rename `Isometry` to `Isometric` #43654
- chore: remove declarations deprecated between 2021-10-15 and 2026-04-15 #44886
4 open pull requests
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
- chore(EMetric/*): rename theorems #34096
- test: insert `@[informal]` attributes from overview #38195
- refactor: turn `Set` into a 1-field structure #39211
- feat(Analysis/Complex/CauchyIntegral): add Cauchy formula at interior points #43100
- perf: remove `simp` from `sup_of_le_left` and friends #43436
- chore: lake shake --add-public --keep-implied --keep-prefix --add-public-downstream Mathlib.Init --fix #43782
No open pull requests.
14 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
- experiment: make `neg_div'` a `@[simp]` lemma #42882
- feat(Trigonometric): define coth and prove basic properties #43902
- feat: simplify computations in complex analysis by extracting frequently-used lemmas #43958
- chore: replace `exact_mod_cast` with `exact mod_cast` #44348
- WIP: Feat/positivity lemma #44923
3 open pull requests
No open pull requests.
No open pull requests.
4 open pull requests
4 open pull requests
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
- chore: no `noncomputable` inside noncomputable section #41551
- WIP: Feat/positivity lemma #44923
- chore(Analysis): golf proofs with `grind` #45023
No open pull requests.
4 open pull requests
13 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: replace terminal `convert` with `exact` #41762
- chore(Calculus/FDeriv/Comp): reorganize the file #44207
- chore: rename ContDiffAt.hasStrict(F)DerivAt to hasStrict(F)DerivAt_(… #44840
- feat: `ContDiffAt.hasStrictFDerivAt_fderiv_of_minSmoothness_le` #44841
- feat(Analysis/LocallyConvex): asymptotics for LCTVS and normed spaces #44850
11 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
- 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
- chore: replace `exact_mod_cast` with `exact mod_cast` #44348
- WIP: Feat/positivity lemma #44923
9 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
- feat(Analysis/TemperedDistribution): polynomially bounded locally integrable functions define tempered distributions #36595
- feat: fun_prop for integrability #39323
- chore: rename Directed to Predirected #42290
- chore: tag definitions with `fun_prop` #44064
12 open pull requests
- refactor: unbundle algebra from `ENormed*` #28803
- chore: rename `continuous{,On,At,Within}_const` to `ContinuousFoo.const` #31607
- refactor(Order): make completeness typeclasses mixins #38537
- feat(IntervalIntegrable): add `fun_prop` support #38822
- feat: define contour integrals #39254
- chore: replace `by exact` occurences #40223
- chore: remove redudant `nonrec`'s #41259
- perf: remove `simp` from `sup_of_le_left` and friends #43436
- chore: tag definitions with `fun_prop` #44064
- perf(Linter/Multigoal): use `InfoTree.foldInfo` #44247
- chore: remove declarations deprecated between 2021-10-15 and 2026-04-15 #44886
- chore: rename `notation3` to `notation +delab` #45028
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: replace `exact_mod_cast` with `exact mod_cast` #44348
9 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
- feat: `2 ^ n ≤ lcmUpto n` for `7 ≤ n` #43373
- chore: replace `exact_mod_cast` with `exact mod_cast` #44348
- WIP: Feat/positivity lemma #44923
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.