Upstreaming dashboard
The eventual goal of the APAP project is to be fully upstreamed to Mathlib.
As such, it is crucial to continuously organise upstreaming from APAP to Mathlib.
The way we organise this is with the following two lists,
showing files with no APAP 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.
11 open pull requests
- chore: use `open scoped` #4960
- chore: dedent `to_additive` docstrings #28298
- chore(Mathlib): replace `=>` by `↦` #28622
- experiment(Algebra): unbundle npow/zpow from Monoid/InvDivMonoid #29605
- chore: prefer `Pi.single i 1 j` over `fun j => if i = j then 1 else 0` #31949
- refactor(Algebra): add type-classes for algebraic properties of `FunLike` #33477
- chore: shake --keep-implied --keep-prefix --fix #39386
- chore: remove many redundant imports #41222
- refactor(Data/FunLike): make the arguments of `Is*Apply` implicit #42704
- chore(Basic): move `FunLike` from Data #43253
- chore(Algebra/MonoidHom): moving coe from `.ofClass` to `.toMonoidHom` #43765
6 open pull requests
- feat(Tactic/Push): add basic tags and tests #29000
- feat(Combinatorics/Schnirelmann): prove Mann's theorem #38077
- chore: remove trailing semicolons #41695
- feat(Algebra/Group/Action/Pointwise/Set/Basic): `mul_mem_smul_set` #42646
- refactor: rename `MulAction` to `MonoidAction` #43404
- refactor(Logic/Pairwise): define more general pairwise based on mem, change old pairwise into pairwise' #43635
7 open pull requests
- 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` #43404
No open pull requests.
No open pull requests.
No open pull requests.
14 open pull requests
- feat: define the additive submonoid of positive elements in a star ordered ring #4871
- chore: fix links #27709
- feat: modify `cfc_tac` to use `grind` #27829
- feat(Tactic/Linter): linter for comments that should become docstrings #36636
- test: insert `@[informal]` attributes from overview #38195
- feat: ℕ+ powers in semigroups #40785
- refactor: rename Function.swap #42282
- feat: `membership` tactic #42342
- chore: weaken unused typeclass assumptions on section variables #43503
- Jireh ppow perf lower reverse bridge #44166
- Jireh ppow perf lower default priority #44167
- Jireh ppow perf no reverse bridge #44168
- Jireh ppow perf reorder pow parent #44169
- Jireh ppow perf demote pow simp #44170
4 open pull requests
6 open pull requests
- lint also `let` vs `have` #12181
- chore: rename `continuous{,On,At,Within}_const` to `ContinuousFoo.const` #31607
- feat: add convolution_comp_add_right #32169
- chore: golf using .ne and friends #37553
- feat: try using grind as gcongr discharger #37688
- test: insert `@[informal]` attributes from overview #38195
10 open pull requests
- feat(Analysis/Normed/Ring/Basic): Add NonUnitalNonAssocSeminormedRing and NonUnitalNonAssocNormedRing #29856
- feat: `GroupWithZero` versions of `le` lemmas #34120
- feat: instance diamond linter #38781
- test #40172
- feat(GroupTheory): `AddSubgroupClass` implies `SMulMemClass` over `ℤ` #41866
- refactor(Algebra/Module/ZLattice): generalise from ℤ-submodules to `AddSubgroupClass` #41867
- chore: rename Directed to Predirected #42290
- refactor: update `spectralRadius` material to assume `HasSummableGeomSeries` instead of `CompleteSpace` #42782
- chore: rename `Isometry` to `Isometric` #43654
- chore: correct instances for normed rings on subrings #44082
14 open pull requests
- refactor(Analysis/Normed*): use `RingHomIsometric` for `*.norm_cast` #6931
- chore: migrate to `tfae` block tactic #11003
- feat: more linting of cdots #12411
- feat: a norm_num extension for complex numbers #26975
- chore: reduce `Topology` imports in `Data` #29012
- refactor(Algebra/Algebra/Equiv): allow for non-unital `AlgEquiv` #29354
- chore: rename `continuous{,On,At,Within}_const` to `ContinuousFoo.const` #31607
- feat(RCLike): add `Continuous.re` and similar #34419
- feat(Tactic/Linter): linter for comments that should become docstrings #36636
- fix(Tactic/Continuity): mark Continuous.comp' as unsafe #36806
- chore(Data/Real): encapsulate real numbers #38702
- feat(MeasureTheory/Integral/Bochner/ContinuousLinearMap): add conj_div_mul_eq_norm, enorm_integral_mul_conj_comm #42262
- chore: remove `CovariantClass` and `ContravariantClass` #42273
- feat(Analysis): radial functions #44305
7 open pull requests
- feat: ℕ+ powers in semigroups #40785
- refactor(Algebra/Group/*): redefine `IsAddTorsionFree` and `IsMulTorsionFree` #42407
- Jireh ppow perf lower reverse bridge #44166
- Jireh ppow perf lower default priority #44167
- Jireh ppow perf no reverse bridge #44168
- Jireh ppow perf reorder pow parent #44169
- Jireh ppow perf demote pow simp #44170
10 open pull requests
- feat(IsValuativeTopology/Normed): `Normed` to `IsValuativeTopology` #40309
- feat: ℕ+ powers in semigroups #40785
- chore: remove redudant `nonrec`'s #41259
- perf: remove `simp` from `sup_of_le_left` and friends #43436
- chore: lake shake --add-public --keep-implied --keep-prefix --fix #43782
- Jireh ppow perf lower reverse bridge #44166
- Jireh ppow perf lower default priority #44167
- Jireh ppow perf no reverse bridge #44168
- Jireh ppow perf reorder pow parent #44169
- Jireh ppow perf demote pow simp #44170
7 open pull requests
- chore: remove redundant `unfold`s #39029
- feat(Data/ZMod/Basic): isUnit characterisation in prime power moduli #40005
- feat(Data/ZMod/Basic): idempotents in ZMod (p^d) are exactly {0, 1} #40006
- feat(ModularForm): add eisensteinSeries G_k^v #41613
- chore: replace `simp_all` with `simp` whenever possible #41896
- chore(Data/SetLike): rename `IsConcreteLE` #42702
- feat: char two API (WIP) #43575
No open pull requests.
9 open pull requests
- feat(MeasureTheory/Function): Add ContinuousLinearMap.bilinearCompLp(L) #20372
- WIP: generalise lemmas to ENorm #21375
- chore: change more lemmas to be about enorm instead of nnnorm #21433
- chore: make `finiteness` a default tactic #26090
- chore: more enorm lemmas #27446
- refactor: unbundle algebra from `ENormed*` #28803
- refactor: redefine `eLpNorm` at `p = 0` #39311
- chore: replace `by calc` by `calc` whenever possible #40292
- chore: extend L^p lemmas from normed spaces to enormed setting #43834
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.