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.

LeanOA.Mathlib.Algebra.LinearAlgebra.Span.Defs

No open pull requests.

LeanOA.Mathlib.Algebra.Order.Module.PositiveLinearMap

No open pull requests.

LeanOA.Mathlib.Algebra.Order.Star.Basic

3 open pull requests

• feat: modify `cfc_tac` to use `grind` #27829
  merge-conflict, WIP
• doc(Algebra/Order): update mentions of `OrderedSemiring` and friends #37835
  t-algebra, t-order
• feat(Tactic): convert now discharges side goals at reducible transparency #39039
  t-meta, awaiting-author, merge-conflict, WIP

LeanOA.Mathlib.Algebra.Star.StarAlgHom

4 open pull requests

• refactor(Algebra/Algebra/Equiv): allow for non-unital `AlgEquiv` #29354
  t-algebra, awaiting-author, merge-conflict
• chore: override `npow` in compositional monoids #36878
• feat: add `Function.{prod,diag,fstComp,sndComp,prodMap}` #37631
  t-logic, WIP
• refactor(Algebra): semialgebra maps #38376
  WIP, blocked-by-other-PR

LeanOA.Mathlib.Algebra.Star.Unitary

1 open pull request

• feat(LinearAlgebra/Matrix): add Hadamard matrices #38582
  t-algebra, new-contributor

LeanOA.Mathlib.Analysis.CStarAlgebra.ApproximateUnit

1 open pull request

• feat(Analysis/CStarAlgebra/Extreme): a C⋆-algebra is unital iff there exists an extreme point in the closed unit ball #36327
  t-analysis, awaiting-author, merge-conflict, blocked-by-other-PR

LeanOA.Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Basic

1 open pull request

• feat: transfer instances of `ContinuousFunctionalCalculus` to type synonyms with weaker topologies #35605
  merge-conflict, t-analysis

LeanOA.Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Order

4 open pull requests

• test: refactor in CI #15679
  merge-conflict, WIP
• perf: reorder `extends` and remove some instances in algebra hierarchy #16594
  merge-conflict, slow-typeclass-synthesis, t-algebra
• feat: preliminary `grind` tags for `IsUnit` #28132
  merge-conflict, t-algebra
• feat: `GroupWithZero` versions of `le` lemmas #34120
  WIP, large-import, merge-conflict

LeanOA.Mathlib.Analysis.CStarAlgebra.Module.Defs

No open pull requests.

LeanOA.Mathlib.Analysis.CStarAlgebra.MulNonneg

No open pull requests.

LeanOA.Mathlib.Analysis.Complex.Basic

5 open pull requests

• refactor(Analysis/Normed/{Group/Field}/Basic): Let `extends` generate the repeated fields #9642
  WIP, merge-conflict, awaiting-author, help-wanted, t-analysis
• feat(Data/Complex/Exponential): prove some useful results about the complex exponential. #20313
  merge-conflict, t-analysis, new-contributor
• chore: fix links #27709
  merge-conflict, WIP
• chore: add a computable shortcut for `AddCommMonoid ℂ` #29615
  t-analysis, easy
• chore: rename `continuous{,On,At,Within}_const` to `ContinuousFoo.const` #31607
  delegated, merge-conflict, awaiting-CI

LeanOA.Mathlib.Analysis.LocallyConvex.Bounded

1 open pull request

• chore: fix some explicitVarOfIff linter errors #32095
  please-adopt, WIP, merge-conflict

LeanOA.Mathlib.Analysis.LocallyConvex.WithSeminorms

7 open pull requests

• feat(Analysis.Distribution.ContDiffMapSupportedIn): space of smooth maps with support in a fixed compact #5912
  merge-conflict, WIP, t-analysis
• chore: migrate to `tfae` block tactic #11003
  merge-conflict, WIP, blocked-by-other-PR, t-meta
• feat(Tactic/Push): add basic tags and tests #29000
  merge-conflict, blocked-by-other-PR, t-meta
• chore: reduce `Topology` imports in `Data` #29012
  merge-conflict, file-removed
• chore: golf using .ne and friends #37553
  merge-conflict
• feat: Analytic Hahn Banach theorem for locally convex spaces #38739
  t-analysis, delegated, large-import
• chore: remove `Dynamics` dependency from `Data` #39983
  WIP, tech debt, file-removed, blocked-by-other-PR, merge-conflict

LeanOA.Mathlib.Analysis.Normed.Group.Uniform

3 open pull requests

• refactor: deprecate `LinearIsometryClass` #33450
  t-algebra, t-analysis, blocked-by-other-PR, t-topology, merge-conflict
• feat: lemmas about `IsometryClass` #33454
  t-topology, t-analysis, awaiting-author, merge-conflict
• feat(RCLike): add `Continuous.re` and similar #34419
  t-analysis, new-contributor, awaiting-author, merge-conflict

LeanOA.Mathlib.Analysis.RCLike.Extend

No open pull requests.

LeanOA.Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Basic

4 open pull requests

• feat: modify `cfc_tac` to use `grind` #27829
  merge-conflict, WIP
• feat: preliminary `grind` tags for `IsUnit` #28132
  merge-conflict, t-algebra
• feat(UniformOnFun): lemma for proving uniform convergence from uncurried form #38789
  WIP, t-topology
• chore: remove redundant `unfold`s #39029

LeanOA.Mathlib.Data.Real.Archimedean

4 open pull requests

• feat(Tactic/Push): add basic tags and tests #29000
  merge-conflict, blocked-by-other-PR, t-meta
• refactor(Order/(Conditionally)CompletePartialOrder): extends `OrderSupSet` #38444
  blocked-by-other-PR, merge-conflict
• chore(Data/Real): encapsulate real numbers #38702
  delegated, merge-conflict
• chore: remove @[expose] from def-free public sections #39388
  merge-conflict

LeanOA.Mathlib.Misc

1 open pull request

• Development branch (1) #30122
  WIP, large-import, merge-conflict

LeanOA.Mathlib.Order.Hom.Basic

8 open pull requests

• refactor(CategoryTheory/MorphismProperty): some clean-ups #10349
  merge-conflict, t-category-theory
• feat(Order/FunLike): define `PointwiseLE` #10721
  merge-conflict, t-order, t-logic
• feat: replace `IsWellFounded` with `WellFounded` #35602
  t-data, awaiting-author, merge-conflict
• feat(Topology): Relating irreducible components of a space to codimension one points in non dense subsets #38002
  large-import, t-topology
• feat(AlgebraicGeometry): The Weil divisor associated to an element of the function field on a locally Noetherian integral scheme #38472
  large-import, blocked-by-other-PR
• feat(Order/Hom/Basic): `Relation.Map`/`Function.onFun` form an order isomorphism between `α`-relations and `β`-relations #38499
  t-order, blocked-by-other-PR
• feat(Order/Hom/Basic): equivalences of `Order{Hom/Embedding/Iso}` #38667
  t-order
• feat(AlgebraicGeometry): The sheaf of modules associated to a Weil divisor #38953
  WIP, large-import, blocked-by-other-PR, merge-conflict

LeanOA.Mathlib.Topology.Algebra.Module.LinearMap

7 open pull requests

• refactor: deprecate `ContinuousLinearMapClass` #33448
  t-topology, t-algebra, awaiting-author, merge-conflict
• refactor: deprecate `LinearIsometryClass` #33450
  t-algebra, t-analysis, blocked-by-other-PR, t-topology, merge-conflict
• feat: analytification of schemes (affine case) #34626
  merge-conflict, WIP, t-differential-geometry, blocked-by-other-PR, please-merge-master
• feat: `NSMul`/`NPow` type class #38036
  merge-conflict
• feat: define contour integrals #39254
  t-measure-probability, merge-conflict
• chore(Algebra/Module): rename multiplication lemmas and add `push/pull_end` attributes #39508
  t-algebra, awaiting-CI, merge-conflict
• chore(Topology): add `push/pull_end` tags for CLMs #39509
  t-topology, merge-conflict

LeanOA.Mathlib.Topology.Algebra.Module.Spaces.UniformConvergenceCLM

2 open pull requests

• feat: flip arguments for continuous linear maps under finite dimension assumptions #36775
  t-topology, blocked-by-other-PR, merge-conflict
• fix: use notation3 more #39383
  delegated

LeanOA.Mathlib.Topology.Algebra.Module.WeakBilin

No open pull requests.

LeanOA.Mathlib.Topology.Algebra.UniformConvergence

No open pull requests.

LeanOA.Mathlib.Topology.Bornology.Basic

1 open pull request

• feat: define `UnboundedSpace` #7903
  merge-conflict, help-wanted, t-topology

LeanOA.Mathlib.Topology.Order.LeftRightNhds

1 open pull request

• chore: migrate to `tfae` block tactic #11003
  merge-conflict, WIP, blocked-by-other-PR, t-meta

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.