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.
No open pull requests.
1 open pull request
No open pull requests.
6 open pull requests
- feat: preliminary `grind` tags for `IsUnit` #28132
- chore: prefer `beta_reduce` over `(d)simp only` #41933
- refactor: unify `Set.mem_ofPred_eq` into `Set.mem_ofPred` #42692
- chore: rename `Isometry` to `Isometric` #43654
- chore(Algebra/Order): make `Nonneg` a structure #45709
- chore: rename lemmas about Subtype.val using subtypeVal #45865
No open pull requests.
3 open pull requests
8 open pull requests
- chore: rename `continuous{,On,At,Within}_const` to `ContinuousFoo.const` #31607
- chore: replace `by calc` by `calc` whenever possible #40292
- 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(Algebra/Order): make `Nonneg` a structure #45709
- chore: rename `nndist` to `nnDist` #45788
6 open pull requests
- chore: rename `Set.mem_singleton` #42551
- chore(Analysis/LocallyConvex): make `Bounded.lean` independent of `NormedSpace` #43329
- chore: rename `Isometry` to `Isometric` #43654
- feat(Topology/Algebra/IsUniformGroup): more versions of `isUniformGroup_of_commGroup` #44444
- chore: rename `nndist` to `nnDist` #45788
- feat: characterize von Neumann boundedness when the topology is induced by a family of linear maps #45925
9 open pull requests
- feat(Tactic/Push): add basic tags and tests #29000
- chore: reduce `Topology` imports in `Data` #29012
- chore: golf using .ne and friends #37553
- chore: remove all terminal `refine`'s with `exact` #40166
- chore: rename `Set.mem_singleton` #42551
- chore(Analysis/LocallyConvex): make `Bounded.lean` independent of `NormedSpace` #43329
- chore: lake shake --add-public --keep-implied --keep-prefix --add-public-downstream Mathlib.Init --fix #43782
- feat(Topology/Algebra/IsUniformGroup): more versions of `isUniformGroup_of_commGroup` #44444
- feat(Analysis/LocallyConvex/WithSeminorms): bases of closed seminorm balls #45964
6 open pull requests
- chore: remove redudant `nonrec`'s #41259
- chore: remove simple `nonrec` occurences #41276
- chore: rename `Isometry` to `Isometric` #43654
- refactor(Topology): unclass `IsClosed` #45643
- feat: precomposing with the quotient map preserves the operator norm #45959
- refactor(Analysis/Normed/Group/Quotient): state `norm_normedMk` in terms of the quotient topology #45960
6 open pull requests
4 open pull requests
- chore: use `private` proof elaborator to remove `set_option backward.privateInPublic` #42755
- refactor: change definition of operator norm to depend only on modules over semirings #42865
- chore: remove backward.privateInPublic by wrapping proofs with private_decl% #44032
- feat: precomposing with the quotient map preserves the operator norm #45959
No open pull requests.
No open pull requests.
7 open pull requests
- chore(Geometry/Convex/Cone/Pointed): clean up variables #37191
- chore(Geometry/Convex/Cone): rework `PointedCone.dual` to take a cone as input in place of a set #37951
- chore: replace terminal `convert` with `exact` #41762
- chore(Data/SetLike): rename `IsConcreteLE` #42702
- feat(Geometry/Convex/Cone/Caratheodory): conic Carathéodory theorem #44900
- chore: rename `notation3` to `notation +delab` #45028
- chore(Algebra/Order): make `Nonneg` a structure #45709
No open pull requests.
No open pull requests.
No open pull requests.
3 open pull requests
4 open pull requests
3 open pull requests
- feat: flip arguments for continuous linear maps under finite dimension assumptions #36775
- feat(Topology/Algebra/IsUniformGroup): group is left/right uniform group iff it's equal to left/right uniformity #44443
- feat(Topology/Algebra/IsUniformGroup): more versions of `isUniformGroup_of_commGroup` #44444
No open pull requests.
No open pull requests.
4 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.