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
21 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
- refactor(Algebra): semialgebra maps #38376
- chore(Mathlib): shake mathlib harder #38408
- test(Tactic/Algebra): try to replace `ring` with algebra in many places #38637
- refactor(Algebra): replace `AlgHomClass` coercions with structure-specific coercions #38715
3 open pull requests (0 with relevant labels)
No open pull requests.
No open pull requests.
No open pull requests.
5 open pull requests (0 with relevant labels)
Other
1 open pull request (0 with relevant labels)
13 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
- feat: check indentation of doc-strings #27897
- Lean pr testing 11156 #31587
- chore: fix markdown list indentation #35281
- feat(Data/Fin): add several lemmas about subtraction of `Fin.{castLT, castAdd, castSucc, castPred}` #35610
- chore(Data): avoid lazy continuation in md lists #36682
7 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
- chore(Algebra/Order/Monoid/Unbundled/Basic): golfing + formatting #38227
- refactor(Order/(Conditionally)CompletePartialOrder): extends `OrderSupSet` #38444
- chore(Data/Real): encapsulate real numbers #38702
9 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
- experiment: define a simproc for simplifying `a = b` from `b = a` #36534
- feat(Logic): declare optional simprocs for commuting equality and iff #37850
- feat(Data/Set): add Set.diag API #38380
5 open pull requests (0 with relevant labels)
Other
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
- Add an API for row echelon forms of matrices #38596
- feat: golf using `IsBotOneClass` and `IsBotZeroClass` #38663
4 open pull requests (0 with relevant labels)
Other
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.
1 open pull request (0 with relevant labels)
No open pull requests.
6 open pull requests (0 with relevant labels)
Other
- chore: make `finiteness` a default tactic #26090
- feat(Tactic/Push): add basic tags and tests #29000
- feat: use `LE.le` for subset relation in `Set`, `Finset`, `PSet`, `ZFSet` #32983
- doc(Algebra/Order): update mentions of `OrderedSemiring` and friends #37835
- feat: use `Is*Apply` classes for continuous linear maps #38561
- chore: tag (almost) all `mono` lemmas as `@[gcongr]` #38793
1 open pull request (1 with relevant labels)
1 open pull request (0 with relevant labels)
1 open pull request (0 with relevant labels)
3 open pull requests (0 with relevant labels)
Other
2 open pull requests (0 with relevant labels)
2 open pull requests (0 with relevant labels)
11 open pull requests (1 with relevant labels)
Relevant
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
- feat(Valued/ValuationTopology): creating instances of `IsValuativeTopology` #36769
- feat(Valuation/ValuativeRel): generalize `ValuativeRel` to non-commutative rings #36777
- fix(RingTheory/Valuation): change `ValueGroup` from taking HomClass to Hom #36911
- feat(DedekindDomain/AdicValuation): `intValuation` on uniformizers is `exp (-1)` #37501
- feat: elements of Dedekind domain approximate elements of valuation ring #37523
- feat: golf using `IsBotOneClass` and `IsBotZeroClass` #38663
6 open pull requests (0 with relevant labels)
Other
- chore: redefine `Ideal.IsPrime` #31595
- refactor(Algebra): weaken NormalizationMonoid #34179
- chore(Algebra/Order/GroupWithZero): flatten `Unbundled` folder #37832
- feat: overlapping instances linter #38126
- feat(RingTheory.DedekindDomain.Factorization): add API for factorization #38654
- feat(IsDedekindDomain.HeightOneSpectrum): simp lemma ofPrime_prime #38757
4 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
No open pull requests.
No open pull requests.
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(AlgebraicGeometry): rank of finite flat morphism #38090
- feat(RingTheory): local isomorphisms #38176
- chore(RingTheory/Localization): mirror tensor product compatibilities and golf #38177
- 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
1 open pull request (0 with relevant labels)
No open pull requests.
7 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
- feat(Algebra): add liftEquiv for groups, rings, algebras, and adjoin roots #36086
- feat: golf using `IsBotOneClass` and `IsBotZeroClass` #38663
- chore: tag (almost) all `mono` lemmas as `@[gcongr]` #38793
2 open pull requests (0 with relevant labels)
No open pull requests.
6 open pull requests (0 with relevant labels)
Other
- refactor: deprecate `SemilinearMapClass` #18805
- refactor: deprecate `ContinuousLinearMapClass` #33448
- refactor: deprecate `LinearIsometryClass` #33450
- refactor(Algebra): replace `SemilinearEquivClass.semilinearEquiv` by structure-specific coercions #37944
- feat: generalize Submodule.ClosedComplemented.of_quotient_finiteDimensional #38579
- feat: golf using `IsBotOneClass` and `IsBotZeroClass` #38663
No open pull requests.
3 open pull requests (0 with relevant labels)
Other
4 open pull requests (0 with relevant labels)
Other
No open pull requests.
8 open pull requests (0 with relevant labels)
Other
- fix(Topology/Algebra/Valued): repair definition of Valued #14752
- 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
- feat(Valued/ValuationTopology): creating instances of `IsValuativeTopology` #36769
- fix(RingTheory/Valuation): change `ValueGroup` from taking HomClass to Hom #36911
- feat: golf using `IsBotOneClass` and `IsBotZeroClass` #38663
6 open pull requests (0 with relevant labels)
Other
- style: replace preimage_val with ↓∩ notation #12418
- feat: restore some explicit binders from Lean 3 #24100
- chore: fix some explicitVarOfIff linter errors #32095
- feat: a measurable space structure on the type of continuous maps #36815
- feat(Topology/ClosedBases): `TopologicalSpace.IsClosedBasis` and `TopologicalSpace.IsClosedSubbasis s` #36954
- feat(Topology): some lemmas about topological bases #38538
No open pull requests.
3 open pull requests (0 with relevant labels)
Other
- chore: replace every usage of ⬝ᵥ (with old \cdot) by ·ᵥ (with \centerdot) #27399
- fix: replace probably erroneous usage of ⬝ (with old \cdot) by · (with \centerdot) #27403
- feat(LinearAlgebra/Matrix/Block, Analysis/Normed/Algebra/MatrixExponential): add BlockTriangular.pow and BlockTriangular.exp #37006
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.