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
20 open pull requests (0 with relevant labels)
Other
- chore: use `open scoped` #4960
- refactor: Use flat structures for morphisms #6791
- perf: do not search algebraic hierarchy when searching `FunLike` hierarchy #17675
- feat(RingTheory/Pure): pure submodules #22909
- chore(RingTheory/Ideal): make `RingHom.ker` take a `RingHom` instead of `RingHomClass` #25138
- feat(RingTheory/GradedAlgebra): homogeneous relation #27307
- chore(Mathlib): replace `=>` by `↦` #28622
- refactor(Algebra/Algebra/Equiv): allow for non-unital `AlgEquiv` #29354
- chore: run docstrings through mdformat #35686
- chore: override `npow` in compositional monoids #36878
- refactor(Algebra): semialgebra maps #38376
- chore(Algebra): consolidate variables and sections for `AlgHom`/`AlgEquiv` #38964
- chore: shake --keep-implied --keep-prefix --fix #39386
- feat(RingTheory): etale lifting property of henselian local rings #41086
- feat(FieldTheory/Minpoly): generalize theorem #42068
- refactor: rename `MulAction` to `MonoidAction` #43404
- perf: remove all abbrev #44074
- refactor(GroupTheory): make `AddAut` multiplicative again #44244
- refactor: replace bundled commutative classes by `IsMulCommutative` (experiment) #44466
- chore: remove declarations deprecated between 2021-10-15 and 2026-04-15 #44886
20 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
- 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(RingTheory/Ideal): make `RingHom.ker` take a `RingHom` instead of `RingHomClass` #25138
- chore(Mathlib): replace `=>` by `↦` #28622
- chore: override `npow` in compositional monoids #36878
- 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: shake --keep-implied --keep-prefix --fix #39386
- perf: reorder `extends` and change instance priority in algebra hierarchy #41846
- feat(FieldTheory/Minpoly): generalize theorem #42068
- chore(MonoidHom): make definitions take `MonoidHom` instead of `MonoidHomClass` #43611
- chore(Algebra/MonoidHom): moving coe from `.ofClass` to `.toMonoidHom` #43765
- refactor: replace bundled commutative classes by `IsMulCommutative` (experiment) #44466
10 open pull requests (0 with relevant labels)
Other
- chore: use `open scoped` #4960
- lint also `let` vs `have` #12181
- 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
- chore: run docstrings through mdformat #35686
- chore: shake --keep-implied --keep-prefix --fix #39386
- refactor: rename `MulAction` to `MonoidAction` #43404
- chore: weaken unused typeclass assumptions on section variables #43503
- refactor: replace bundled commutative classes by `IsMulCommutative` (experiment) #44466
4 open pull requests (0 with relevant labels)
No open pull requests.
6 open pull requests (0 with relevant labels)
Other
- fix: improve defeqs of comp actions #38968
- chore: specify doc-strings of auto-generated additive declarations di… #41565
- chore: add missing `to_additive` docstrings #41628
- chore: add missing `to_additive` docstrings in Algebra/Group actions and homs #41636
- refactor: rename `MulAction` to `MonoidAction` #43404
- perf: remove all abbrev #44074
6 open pull requests (0 with relevant labels)
Other
- feat/refactor: redefinition of homology + derived categories #25848
- test: insert `@[informal]` attributes from overview #38195
- feat(AlgebraicTopology/SimplicialSet/Homology): long exact sequence of a triple #41318
- WIP: inline noncomputable sections #41599
- perf: remove all abbrev #44074
- feat(Algebra/Homology/HomologicalComplex): use `to_dual` #44672
No open pull requests.
No open pull requests.
4 open pull requests (0 with relevant labels)
3 open pull requests (0 with relevant labels)
Other
1 open pull request (0 with relevant labels)
7 open pull requests (0 with relevant labels)
Other
- refactor(Algebra/Group): make `IsUnit` a typeclass #17458
- refactor(Algebra/Polynomial): make into an `abbrev` of `AddMonoidAlgebra` #41981
- feat: use `max`/`min` for `union`/`intersection` in `Set`, `Finset`, `ZFSet`, `Class` #42316
- chore(MonoidHom): make definitions take `MonoidHom` instead of `MonoidHomClass` #43611
- chore(Algebra/MonoidHom): moving coe from `.ofClass` to `.toMonoidHom` #43765
- feat(FieldTheory): Artin-Schreier extensions of fields #43947
- feat(FieldTheory): implement Artin-Schreier polynomials #44926
8 open pull requests (0 with relevant labels)
Other
- feat(AlgebraicGeometry/EllipticCurve): generalise nonsingular condition #25991
- feat(AlgebraicGeometry): add x, y, px, py for points on elliptic curves #26078
- Nagell lutz #35863
- feat(AlgebraicGeometry/EllipticCurve): add notation and pretty printer for points #36334
- chore: replace `:= by rfl` with `:= rfl` #40381
- feat(EllipticCurve): the universal elliptic curve #41300
- refactor: unify `Set.mem_ofPred_eq` into `Set.mem_ofPred` #42692
- chore: lake shake --add-public --keep-implied --keep-prefix --add-public-downstream Mathlib.Init --fix #43782
2 open pull requests (0 with relevant labels)
Other
5 open pull requests (0 with relevant labels)
Other
- feat(CategoryTheory): The Preliminaries for Locally Cartesian Closed Categories #30366
- feat: instance diamond linter #38781
- chore: lake shake --add-public --keep-implied --keep-prefix --add-public-downstream Mathlib.Init --fix #43782
- Instancediamonds merged #44367
- chore(Analysis/Normed/Ring/WithAbs): automated extraction from #44367 #45144
10 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
- chore: rename arguments of `Nat.strong_induction_on` #41540
- chore(Data/Nat/Init): rename recursor arguments #43848
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
- 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
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
- feat(Data/Set): add `Set.diag` #38380
- refactor: turn `Set` into a 1-field structure #39211
- feat: `Pi.map` rename to `Function.map` #39233
- chore(Data/Set): move lemmas from `Set.Disjoint` to `Disjoint` #41913
- refactor: rename the `diag` name token to `diagonal` #43494
6 open pull requests (0 with relevant labels)
Other
- refactor(Algebra/Group): make `IsUnit` a typeclass #17458
- refactor(Algebra/Algebra/Equiv): allow for non-unital `AlgEquiv` #29354
- chore: rename arguments of `Nat.strong_induction_on` #41540
- feat(FieldTheory): extension is separable if its degree is less than the positive char #43205
- feat: `wlog` dischargers (`grind` by default) #43315
- refactor(Logic/Pairwise): define more general pairwise based on mem, change old pairwise into pairwise' #43635
7 open pull requests (0 with relevant labels)
Other
- refactor(Algebra/Group): make `IsUnit` a typeclass #17458
- add subsingleton case to ExpChar #38154
- refactor(Algebra): semialgebra maps #38376
- chore(Algebra): consolidate variables and sections for `AlgHom`/`AlgEquiv` #38964
- chore: remove unused `haveI` and `letI` #41625
- chore: deprecate monad operations on `MvPolynomial` #43372
- chore: rename `nonzero` to `ne_zero` in theorem names #44824
1 open pull request (0 with relevant labels)
8 open pull requests (0 with relevant labels)
Other
- feat: more linting of cdots #12411
- test make `HasQuotient` out put a `setoid` #15586
- Clean up quotient APIs #16210
- chore(Data/Quot): deprecate `ind*'` APIs #16314
- chore: remove global `Quotient.mk` `⟦·⟧` notation #17127
- chore: dedent `to_additive` docstrings #28298
- chore: replace terminal `convert` with `exact` #41762
- chore: prefer `beta_reduce` over `(d)simp only` #41933
8 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
- chore(Algebra/MonoidHom): moving coe from `.ofClass` to `.toMonoidHom` #43765
- refactor(GroupTheory): make `AddAut` multiplicative again #44244
- doc: add lmfdb attributes #44293
- feat: finite index subgroups of ℤ biject with ℕ+ #44718
9 open pull requests (0 with relevant labels)
Other
- feat(MonoidAlgebra): criteria for `single` to be a unit, irreducible or prime #27950
- feat(CategoryTheory): The Preliminaries for Locally Cartesian Closed Categories #30366
- feat(GroupTheory/SpecificGroups/Cyclic): a quotient of a cyclic group is cyclic #34186
- chore: rename arguments of `Nat.strong_induction_on` #41540
- chore: add missing `to_additive` docstrings #41628
- chore(Data/SetLike): rename `IsConcreteLE` #42702
- refactor(GroupTheory): make `AddAut` multiplicative again #44244
- feat(CategoryTheory): stabilizer and outer endomorphisms #44565
- feat(Topology): mapping class group and outer automorphism of fundamental group #44611
No open pull requests.
No open pull requests.
8 open pull requests (0 with relevant labels)
Other
- feat(NumberTheory/Modular): stabilizers for action on upper halfplane #33461
- chore: replace `:= by rfl` with `:= rfl` #40381
- chore: remove unused `haveI` and `letI` #41625
- chore(Algebra/MonoidHom): moving coe from `.ofClass` to `.toMonoidHom` #43765
- feat(LinearAlgebra/Matrix/GeneralLinearGroup/Defs): add `MulEquiv` for `GL` #43945
- feat(LinearAlgebra/Matrix/GeneralLinearGroup/Card): add the cardinality of `GL n R` given `f : R →+* S` a local ring hom #44039
- feat(LinearAlgebra/Matrix/GeneralLinearGroup/Card): add the cardinal of `GL n ZMod N` #44043
- feat(LinearAlgebra/Matrix): add the `prodEquiv` for `Matrix`, `GL` and `SL` #44876
7 open pull requests (0 with relevant labels)
Other
- 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
- refactor(Logic/Pairwise): define more general pairwise based on mem, change old pairwise into pairwise' #43635
- refactor(LinearAlgebra/Matrix/Transvection): generalize the pivot elimination step to commutative rings #44139
- feat(LinearAlgebra/Matrix/Transvection): add the api for define the elementary subgroup #44228
- feat(LinearAlgebra/Matrix/ElementarySubgroup): add the definition of the elementary subgroup and prove that it is equal to `SL` for local rings #44314
9 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: relate `Hom.piMap` and `Subobject.pi` #41686
- feat: generalize `MonoidHom.isStrictMap_prodMap` to arbitrary products #41693
- chore: replace terminal `convert` with `exact` #41762
- chore(Data/SetLike): rename `IsConcreteLE` #42702
- refactor: rename the `diag` name token to `diagonal` #43494
No open pull requests.
1 open pull request (0 with relevant labels)
No open pull requests.
No open pull requests.
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
No open pull requests.
2 open pull requests (0 with relevant labels)
No open pull requests.
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
17 open pull requests (0 with relevant labels)
Other
- chore(FieldTheory/KummerExtension): move some lemmas earlier #9978
- feat: more linting of cdots #12411
- Clean up quotient APIs #16210
- chore(Data/Quot): deprecate `ind*'` APIs #16314
- chore(RingTheory/Ideal): make `RingHom.ker` take a `RingHom` instead of `RingHomClass` #25138
- feat(AlgebraicGeometry/EllipticCurve/Scheme): define the affine scheme associated to an elliptic curve #25983
- refactor(Algebra/Algebra/Equiv): allow for non-unital `AlgEquiv` #29354
- feat(Algebra): add liftEquiv for groups, rings, algebras, and adjoin roots #36086
- feat(Algebra/Category): the category of local extensions over a fixed field #37940
- refactor(Algebra): semialgebra maps #38376
- feat(RingTheory/LocalRing): `adjoinRoot` and local rings #41064
- feat(RingTheory/AdjoinRoot): add AdjoinRoot.isFractionRing #41443
- chore: rename arguments of `Nat.strong_induction_on` #41540
- refactor(Algebra/Polynomial): make into an `abbrev` of `AddMonoidAlgebra` #41981
- chore(Data/Nat/Init): rename recursor arguments #43848
- chore: weaken commutativity assumptions for AdjoinRoot.lift and AdjoinRoot.liftHom #43971
- chore(RingTheory/AdjoinRoot): remove simple set_options #44424
9 open pull requests (0 with relevant labels)
Other
- 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
- refactor: make adicCompletionIntegers a type #41490
- perf: speed up kernel typechecking of some of mathlib's slowest declarations #41705
- refactor(Algebra/GroupWithZero): SubgroupWithZero, and rebase the valuation value group on it #43000
- chore(Valuation/Integers): rename `Valuation.Integers` to `Valuation.IsIntegers` #43250
- chore(Algebra/MonoidHom): moving coe from `.ofClass` to `.toMonoidHom` #43765
6 open pull requests (0 with relevant labels)
Other
- chore: redefine `Ideal.IsPrime` #31595
- bench: review #39049
- feat(NumberTheory/NumberField): summability of the prime ideal zeta sum #42567
- chore(Data/SetLike): rename `IsConcreteLE` #42702
- chore: make a few lemmas using in `RingHomClass` definitions take in a concrete morphism #43585
- chore: golf using new `@[gcongr]` lemmas #44335
4 open pull requests (0 with relevant labels)
Other
No open pull requests.
1 open pull request (0 with relevant labels)
6 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
- chore: refactor Algebra.TensorProduct.rightAlgebra #39699
- chore(MonoidHom): make definitions take `MonoidHom` instead of `MonoidHomClass` #43611
No open pull requests.
2 open pull requests (0 with relevant labels)
2 open pull requests (0 with relevant labels)
1 open pull request (0 with relevant labels)
No open pull requests.
5 open pull requests (0 with relevant labels)
Other
- chore(Valuation/Integers): rename `Valuation.Integers` to `Valuation.IsIntegers` #43250
- feat(RingTheory/Valuation/Discrete/Equiv): equivalence of discrete valuations #44162
- feat(RingTheory/Valuation/Discrete/Normalized): normalization of discrete valuations #44179
- feat(RingTheory/Valuation/ValuativeRel/Discrete): characterize one rank discrete valuative relations #44187
- refactor: deprecate `le_zero_iff` and `zero_lt_iff` #44980
7 open pull requests (0 with relevant labels)
Other
- perf: reorder `extends` and change instance priority in algebra hierarchy #7873
- chore: deprecate `LinearOrderedComm{Monoid, Group}WithZero` #23621
- chore: deprecate duplicate theorems about `IsBotZeroClass` #38663
- chore: remove `CovariantClass` and `ContravariantClass` #42273
- chore(Valuation/Integers): rename `Valuation.Integers` to `Valuation.IsIntegers` #43250
- refactor: replace `SemilatticeSup.sup` with `max` #43472
- chore(Order/RelClasses): remove redundant instances #43608
12 open pull requests (0 with relevant labels)
Other
- feat(RingTheory): `ValuativeRel` on subrings #30135
- feat(RingTheory): valuative topology = adic topology for discrete rank 1 valuations #30192
- chore: redefine `Ideal.IsPrime` #31595
- chore: deprecate duplicate theorems about `IsBotZeroClass` #38663
- chore(Order): infer `toDecidable*` in `*LinearOrder`s when possible #39908
- chore: replace `simp_all` with `simp` whenever possible #41896
- refactor(Algebra/GroupWithZero): SubgroupWithZero, and rebase the valuation value group on it #43000
- feat(RingTheory/LinearTopology): instance `IsLinearTopology O R` #43603
- feat(RingTheory/Valuation/Discrete/Equiv): equivalence of discrete valuations #44162
- feat(RingTheory/Valuation/Discrete/Normalized): normalization of discrete valuations #44179
- feat(RingTheory/Valuation/ValuativeRel/Discrete): characterize one rank discrete valuative relations #44187
- refactor: deprecate `le_zero_iff` and `zero_lt_iff` #44980
No open pull requests.
9 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: prove strict group homs are stable under Prod.map #39270
- 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/Module): introduce the projective locally convex tensor product topology #42127
- feat: add a wrapper around `fun_prop` that calls `simp` on the function #42398
2 open pull requests (0 with relevant labels)
2 open pull requests (0 with relevant labels)
No open pull requests.
8 open pull requests (0 with relevant labels)
Other
- refactor: deprecate `SemilinearMapClass` #18805
- refactor: deprecate `ContinuousLinearMapClass` #33448
- refactor: deprecate `LinearIsometryClass` #33450
- chore: deprecate duplicate theorems about `IsBotZeroClass` #38663
- feat(Topology): use `FComp` in `ContinuousLinearMap` #41224
- feat(Topology/Algebra/IsUniformGroup): more versions of `isUniformGroup_of_commGroup` #44444
- chore: rename `nonzero` to `ne_zero` in theorem names #44824
- refactor: deprecate `le_zero_iff` and `zero_lt_iff` #44980
No open pull requests.
3 open pull requests (0 with relevant labels)
Other
5 open pull requests (0 with relevant labels)
Other
No open pull requests.
6 open pull requests (0 with relevant labels)
Other
- chore: deprecate duplicate theorems about `IsBotZeroClass` #38663
- feat(IsValuativeTopology/Normed): `Normed` to `IsValuativeTopology` #40309
- refactor(Algebra/GroupWithZero): SubgroupWithZero, and rebase the valuation value group on it #43000
- feat(ValuativeTopology): valuative topology of Z_p #43285
- feat(RingTheory/LinearTopology): instance `IsLinearTopology O R` #43603
- feat(Topology/Algebra/IsUniformGroup): more versions of `isUniformGroup_of_commGroup` #44444
7 open pull requests (0 with relevant labels)
Other
- chore: refactor algebraic filter bases #18202
- chore: deprecate `LinearOrderedComm{Monoid, Group}WithZero` #23621
- feat(TopologyValued): `Valued` based on a range topology #27314
- chore: deprecate duplicate theorems about `IsBotZeroClass` #38663
- chore: remove redudant haveI/letI in defs #41680
- refactor(Algebra/GroupWithZero): SubgroupWithZero, and rebase the valuation value group on it #43000
- feat(Topology/Algebra/IsUniformGroup): more versions of `isUniformGroup_of_commGroup` #44444
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(Topology): the small inductive dimension of the reals is 1 #43116
- chore: golf using new `@[gcongr]` lemmas #44335
- feat({Topology,MeasureTheory}): instances for `Additive`/`Multiplicative` #45174
3 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.