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.
PRs are grouped as 'relevant' if they contain the following label: FLT
23 open pull requests (0 with relevant labels)
Other
- chore: use `open scoped` #4960
- refactor: Use flat structures for morphisms #6791
- perf: reorder `extends` and change instance priority in algebra hierarchy #7873
- chore: weaken commutativity assumptions for AdjoinRoot.lift and AdjoinRoot.liftHom #9564
- perf: reorder `extends` and remove some instances in algebra hierarchy #16594
- perf: reorder `extends` of `(Add)Monoid` #16637
- perf: do not search algebraic hierarchy when searching `FunLike` hierarchy #17675
- refactor: deprecate `SemilinearMapClass` #18805
- chore(Algebra/*-{Category,Homology}): remove unnecessary universe variables #24285
- chore(RingTheory/Ideal): make `RingHom.ker` take a `RingHom` instead of `RingHomClass` #25138
- chore(FreeAbelianGroup): deprecate multiplication #27759
- chore(Mathlib): replace `=>` by `↦` #28622
- feat: some lemmas about AlgHom 1 and * #34238
- chore: add simp lemma to unfold Algebra.algHom #36346
- feat(NumberTheory/RamificationInertia/HilbertTheory): compositum of unramified extensions is unramified #36843
- chore: override `npow` in compositional monoids #36878
- feat(NumberTheory/NumberField): linear disjointness from coprime discriminants #37023
- feat(RingTheory/AugmentationIdeal): base change for augmentation ideals #37745
- refactor(Algebra): semialgebra maps #38376
- test(Tactic/Algebra): try to replace `ring` with algebra in many places #38637
- chore(Algebra): consolidate variables and sections for `AlgHom`/`AlgEquiv` #38964
- chore(Algebra): `coe_ringHom` -> `coe_toRingHom` #38966
- chore: shake --keep-implied --keep-prefix --fix #39386
9 open pull requests (0 with relevant labels)
Other
- chore: use `open scoped` #4960
- lint also `let` vs `have` #12181
- chore(Algebra/*-{Category,Homology}): remove unnecessary universe variables #24285
- chore(RingTheory/Ideal): make `RingHom.ker` take a `RingHom` instead of `RingHomClass` #25138
- chore(Mathlib): replace `=>` by `↦` #28622
- refactor(Algebra/Algebra/Equiv): allow for non-unital `AlgEquiv` #29354
- refactor: rename `MulAction` to `MonoidAction` #32737
- chore: run docstrings through mdformat #35686
- chore: shake --keep-implied --keep-prefix --fix #39386
5 open pull requests (0 with relevant labels)
Other
No open pull requests.
No open pull requests.
No open pull requests.
5 open pull requests (0 with relevant labels)
Other
No open pull requests.
4 open pull requests (0 with relevant labels)
Other
8 open pull requests (0 with relevant labels)
Other
- feat: add Qq wrappers for ToExpr #5952
- style: Change Subtype.val to (↑) #12465
- feat(MvPolynomial/Equiv): Add `MvPolynomial.finSuccEquivNth` #19467
- feat: `Clone` and some instances #20051
- feat: Definition of `Clone` #23460
- chore: fix recursors #23489
- Post's lattice #24744
- feat: a linter for duplicated `open` #25362
8 open pull requests (0 with relevant labels)
Other
- feat(Algebra/Order/Field/Basic): generalize lemmas #24378
- feat(Tactic/Push): add basic tags and tests #29000
- refactor: use `OrderSupInfSet` #35263
- refactor: use `OrderSupSet` in `ConditionallyCompleteLattice` #35674
- refactor(Order/(Conditionally)CompletePartialOrder): extends `OrderSupSet` #38444
- test(Tactic/Algebra): try to replace `ring` with algebra in many places #38637
- chore(Data/Real): encapsulate real numbers #38702
- chore: remove @[expose] from def-free public sections #39388
11 open pull requests (0 with relevant labels)
Other
- feat: The finite product of semi-rings (in terms of measure theory) is a semi-ring. #25902
- feat(MeasureTheory): finite unions of sets in a semi-ring (in terms of measure theory) form a ring #25903
- chore: fix links #27709
- feat(Tactic/Push): add basic tags and tests #29000
- perf: remove some `aesop`s and `grind`s #35738
- feat(Topology/Compactness/CompactSystem): closed and compact square cylinders form a compact system #36160
- feat(Data/Set): add `Set.diag` #38380
- chore(Data/Set): reduce defeq abuse of `Set α = α → Prop` #39110
- refactor: turn `Set` into a 1-field structure #39211
- feat: `Pi.map` rename to `Function.map` #39233
- feat(Logic/Function/Defs): add `Function.diag` #41082
1 open pull request (0 with relevant labels)
6 open pull requests (0 with relevant labels)
Other
- Clean up quotient APIs #16210
- chore(Data/Quot): deprecate `ind*'` APIs #16314
- feat(Algebra): additivize Dvd and Prime #27936
- feat(MonoidAlgebra): criteria for `single` to be a unit, irreducible or prime #27950
- feat(Translate): copy `alias` and `deprecated` attributes #40503
- refactor(GroupTheory/Commensurable): add and generalize API #41030
No open pull requests.
2 open pull requests (0 with relevant labels)
5 open pull requests (0 with relevant labels)
Other
- feat(Data/Matrix/Basic): add notation for `m×n`-Matrices #12178
- refactor(Algebra/Algebra/Equiv): allow for non-unital `AlgEquiv` #29354
- feat(Matrix/Transvection): Gauss pivot determinant identity and pivot preservation #29871
- chore: deprecate duplicate theorems about `IsBotZeroClass` #38663
- feat(LinearAlgebra/SymplecticGroup): symplectic matrices have determinant 1 #40352
6 open pull requests (0 with relevant labels)
Other
- feat: move `ContinuousSMul` to a finite extension with the module topology #31948
- chore: prefer `Pi.single i 1 j` over `fun j => if i = j then 1 else 0` #31949
- feat: `Pi.map` rename to `Function.map` #39233
- feat(Algebra): use `Is*Apply` for `LinearMap` #39638
- feat(LinearAlgebra/Contraction): bijectivity of `dualTensorHom` + generalize to `CommSemiring` #40297
- refactor(Algebra/Module/Equiv): update name and refactor API ofLinearEquiv #40865
No open pull requests.
No open pull requests.
No open pull requests.
No open pull requests.
No open pull requests.
No open pull requests.
No open pull requests.
3 open pull requests (0 with relevant labels)
No open pull requests.
4 open pull requests (0 with relevant labels)
Other
No open pull requests.
2 open pull requests (0 with relevant labels)
1 open pull request (0 with relevant labels)
3 open pull requests (0 with relevant labels)
Other
3 open pull requests (0 with relevant labels)
3 open pull requests (0 with relevant labels)
Other
7 open pull requests (0 with relevant labels)
Other
- feat(AlgebraicGeometry/EllipticCurve): generalise nonsingular condition #25991
- refactor: make `Valuation.Completion` a `def` and refactor more of `AdicValuation.lean` #27972
- feat : `v.adicCompletionIntegers K` is compact when `K` is a number field #30579
- feat: the adele ring of a number field is locally compact #36404
- chore(Topology): `UniformSpace.Completion` renames for morphisms #38039
- chore: deprecate duplicate theorems about `IsBotZeroClass` #38663
- chore(Data/ENat): replace `coe` with `natCast` in lemma names #41140
4 open pull requests (0 with relevant labels)
Other
5 open pull requests (0 with relevant labels)
Other
- chore(Data/Quot): deprecate `ind*'` APIs #16314
- feat: the ring of integers of a `ℤₘ₀`-valued field is compact whenever it is a DVR and the residue field is finite #27973
- chore: redefine `Ideal.IsPrime` #31595
- feat(Tactic/FastInstance): warn when a synthesized sub-instance has leaky binder types #36706
- refactor: make `IsAtom` not depend on `OrderBot` #40369
No open pull requests.
1 open pull request (0 with relevant labels)
7 open pull requests (0 with relevant labels)
Other
- refactor(Algebra/Module/LocalizedModule): Redefine `LocalizedModule` in terms of `OreLocalization`. #13156
- chore: get rid of `LocalizedModule.mk` #34248
- feat(RingTheory): algebra maps between finite étale algebras are locally finite split #38586
- chore(RingTheory): equality of linear map with values in finite module spreads out #38649
- feat(RingTheory/Flat): a finite flat `R`-module `M` is locally free if `rankAtStalk M` is constant #39412
- feat(RingTheory/LocalProperties): `Module.Invertible` is a local property #39420
- WIP: any regular local ring is a UFD #39510
1 open pull request (0 with relevant labels)
No open pull requests.
6 open pull requests (0 with relevant labels)
Other
- perf: reorder `extends` and change instance priority in algebra hierarchy #7873
- chore: remove `CovariantClass` and `ContravariantClass` #13124
- chore: deprecate `LinearOrderedComm{Monoid, Group}WithZero` #23621
- feat(AlgebraicGeometry/EllipticCurve/Scheme): define the affine scheme associated to an elliptic curve #25983
- chore: deprecate duplicate theorems about `IsBotZeroClass` #38663
- chore(Order): infer `toDecidable*` in `*LinearOrder`s when possible #39908
10 open pull requests (0 with relevant labels)
Other
- feat(Data/ZMod/Defs): Topological structure on `ZMod` #9146
- feat: rename `connectedComponentOfOne` to `identityComponent`, prove that it is normal and open #10024
- chore: fix some explicitVarOfIff linter errors #32095
- feat: add `IsMulCommutative` instances for topological closures of subobjects #36418
- feat: prove strict group homs are stable under Prod.map #39270
- feat(Dynamics): pointwise ergodic theorem (via maximal inequality) #40178
- refactor(Topology/Algebra): use `IsOpenUnits` more widely #40379
- feat(Analysis): the inclusion of the general linear group into linear maps is an open embedding for finite-dimensional TVS #40380
- chore(Topology): rename `IndiscreteTopology` to `HasIndiscreteTopology` #40994
- feat(Topology/Algebra/Group/Basic): add eq_of_tendsto_div_nhds_one #41230
No open pull requests.
No open pull requests.
5 open pull requests (0 with relevant labels)
Other
No open pull requests.
6 open pull requests (0 with relevant labels)
Other
- chore: fix some explicitVarOfIff linter errors #32095
- feat(Analysis/SpecialFunctions/ImproperIntegrals): Frullani integral #34815
- feat: add `IsMulCommutative` instances for topological closures of subobjects #36418
- feat(Dynamics): pointwise ergodic theorem (via maximal inequality) #40178
- feat: make topologicalClosure a ClosureOperator #40251
- chore(Topology): rename `IndiscreteTopology` to `HasIndiscreteTopology` #40994
5 open pull requests (0 with relevant labels)
Other
2 open pull requests (0 with relevant labels)
5 open pull requests (0 with relevant labels)
Other
- chore: refactor algebraic filter bases #18202
- chore: deprecate `LinearOrderedComm{Monoid, Group}WithZero` #23621
- feat(Topology/Algebra/Valued): `IsLinearTopology 𝒪[K] K` and `𝒪[K] 𝒪[K]` #24627
- feat(TopologyValued): `Valued` based on a range topology #27314
- chore: deprecate duplicate theorems about `IsBotZeroClass` #38663
4 open pull requests (0 with relevant labels)
Other
No open pull requests.
2 open pull requests (0 with relevant labels)
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.