Welcome to the mathlib review page. Everybody's help with reviewing is appreciated. Reviewing contributions is important, and everybody is welcome to review pull requests! If you're not sure how, the pull request review guide is there to help you.
This page contains tables of
| Number |
Author |
Title |
Description |
Labels |
+/- |
Modified files (first 100) |
📝 |
💬 |
All users who commented or reviewed |
Assignee(s) |
Updated |
Last status change |
total time in review |
| 31259 |
YaelDillies author:YaelDillies |
refactor(Dynamics): use `SetRel` notions of separation and cover |
... instead of the handmade ones.
---
[](https://gitpod.io/from-referrer/)
|
t-dynamics |
173/203 |
Mathlib/Data/Rel/Cover.lean,Mathlib/Dynamics/TopologicalEntropy/CoverEntropy.lean,Mathlib/Dynamics/TopologicalEntropy/DynamicalEntourage.lean,Mathlib/Dynamics/TopologicalEntropy/NetEntropy.lean,Mathlib/Dynamics/TopologicalEntropy/Semiconj.lean,Mathlib/Dynamics/TopologicalEntropy/Subset.lean,Mathlib/Topology/UniformSpace/Defs.lean |
7 |
7 |
['D-Thomine', 'YaelDillies', 'github-actions', 'mathlib4-merge-conflict-bot'] |
urkud assignee:urkud |
18-131 18 days ago |
21-11702 21 days ago |
34-13629 34 days |
| 30981 |
jsm28 author:jsm28 |
feat(Geometry/Euclidean/Angle/Bisector): oriented angle bisection mod π |
Add lemmas relating equal distance to two lines to bisecting the angle between them mod π (expressed as usual as equality of twice angles), building on the previous lemmas (#30477) dealing with bisection mod 2π.
---
- [ ] depends on: #30474
- [ ] depends on: #30477
- [ ] depends on: #30600
- [ ] depends on: #30703
[](https://gitpod.io/from-referrer/)
|
t-euclidean-geometry |
146/4 |
Mathlib/Geometry/Euclidean/Angle/Bisector.lean |
1 |
4 |
['github-actions', 'jsm28', 'mathlib4-dependent-issues-bot', 'mathlib4-merge-conflict-bot'] |
JovanGerb assignee:JovanGerb |
17-55475 17 days ago |
21-16221 21 days ago |
25-59451 25 days |
| 30886 |
urkud author:urkud |
feat(DifferentialForm): exterior derivative applied to vector fields |
---
- [ ] depends on: #30331
[](https://gitpod.io/from-referrer/)
|
t-analysis |
217/0 |
Mathlib.lean,Mathlib/Analysis/Calculus/DifferentialForm/VectorField.lean,Mathlib/Analysis/Calculus/FDeriv/ContinuousAlternatingMap.lean,Mathlib/Topology/Algebra/Module/Alternating/Basic.lean |
4 |
4 |
['github-actions', 'mathlib4-dependent-issues-bot', 'mathlib4-merge-conflict-bot'] |
kex-y assignee:kex-y |
13-51657 13 days ago |
14-64624 14 days ago |
23-33087 23 days |
| 30344 |
Deep0Thinking author:Deep0Thinking |
feat(MeasureTheory/Integral): add versions of `exists_eq_interval_average` and first mean value theorem for integrals |
Add the First mean value theorem for (unordered) interval integrals on ℝ.
- `exists_eq_const_mul_interval_integral_of_continuous_on_of_ae_nonneg`
- `exists_eq_const_mul_interval_integral_of_continuous_on_of_nonneg`
---
[](https://gitpod.io/from-referrer/)
|
t-measure-probability
new-contributor
|
294/41 |
Mathlib.lean,Mathlib/MeasureTheory/Integral/IntervalAverage.lean,Mathlib/MeasureTheory/Integral/IntervalIntegral/MeanValue.lean |
3 |
10 |
['Deep0Thinking', 'github-actions', 'mathlib4-merge-conflict-bot', 'plp127'] |
kex-y assignee:kex-y |
12-51674 12 days ago |
15-66860 15 days ago |
57-23795 57 days |
| 32042 |
chrisflav author:chrisflav |
feat(AlgebraicGeometry): quasi compact covers |
This will be used to define the fpqc topology on `Scheme`.
From Proetale.
---
[](https://gitpod.io/from-referrer/)
|
t-algebraic-geometry |
311/1 |
Mathlib.lean,Mathlib/AlgebraicGeometry/Cover/QuasiCompact.lean,Mathlib/AlgebraicGeometry/Morphisms/Affine.lean,Mathlib/AlgebraicGeometry/Morphisms/QuasiCompact.lean,Mathlib/AlgebraicGeometry/Morphisms/UnderlyingMap.lean,Mathlib/AlgebraicGeometry/Sites/MorphismProperty.lean,Mathlib/Topology/Sets/CompactOpenCovered.lean,Mathlib/Topology/Spectral/Prespectral.lean |
8 |
9 |
['chrisflav', 'erdOne', 'github-actions'] |
joneugster assignee:joneugster |
12-51659 12 days ago |
16-18948 16 days ago |
16-18924 16 days |
| 31059 |
gasparattila author:gasparattila |
feat(Topology/Sets): define the Vietoris topology on `(Nonempty)Compacts` |
This PR defines the Vietoris topology on `Compacts` and `NonemptyCompacts`, and proves that it is induced by the Hausdorff uniformity.
---
- [x] depends on: #31031
- [x] depends on: #31058
[](https://gitpod.io/from-referrer/)
|
t-topology |
227/29 |
Mathlib.lean,Mathlib/Data/Rel.lean,Mathlib/Topology/MetricSpace/Closeds.lean,Mathlib/Topology/Sets/Compacts.lean,Mathlib/Topology/Sets/VietorisTopology.lean,Mathlib/Topology/UniformSpace/Closeds.lean |
6 |
6 |
['github-actions', 'mathlib4-dependent-issues-bot', 'mathlib4-merge-conflict-bot', 'robin-carlier'] |
ADedecker assignee:ADedecker |
12-23596 12 days ago |
12-23743 12 days ago |
19-43477 19 days |
| 28944 |
linesthatinterlace author:linesthatinterlace |
refactor(Order/Hom/Basic): reorder definitions |
Reorder and disentangle definitions for OrderHom, OrderEmbedding and OrderIso.
---
This is a preamble to making all of these `def` and consistently defined - the aim is to first disentangle the definitions as it will make it more straightforward to perform these later PRs.
[](https://gitpod.io/from-referrer/)
|
t-order |
215/180 |
Mathlib/Order/Hom/Basic.lean |
1 |
17 |
['YaelDillies', 'github-actions', 'linesthatinterlace', 'mathlib4-merge-conflict-bot'] |
b-mehta and linesthatinterlace assignee:b-mehta assignee:linesthatinterlace |
12-23200 12 days ago |
15-81588 15 days ago |
42-1290 42 days |
| 31987 |
saodimao20 author:saodimao20 |
feat: add monotonicity and relation lemmas for mgf and cgf |
Add two lemmas about moment-generating and cumulant-generating functions:
- `mgf_mono_in_t_of_nonneg`: For nonnegative random variables, the mgf is monotone in the parameter `t`
- `cgf_zero_of_mgf_one`: The cgf equals zero iff the mgf equals one
These lemmas are useful for studying properties of mgf and cgf in probability theory.
Contributed by sequential-intelligence-lab(SIL), University of Virginia
---
[](https://gitpod.io/from-referrer/)
|
t-measure-probability
new-contributor
|
21/0 |
Mathlib/Probability/Moments/Basic.lean |
1 |
5 |
['DavidLedvinka', 'github-actions'] |
RemyDegenne assignee:RemyDegenne |
11-58246 11 days ago |
17-31117 17 days ago |
17-31155 17 days |
| 32019 |
jsm28 author:jsm28 |
feat(Geometry/Euclidean/Projection): `map` and subtype lemmas |
Add lemmas about mapping `orthogonalProjection`, `reflection` and `orthogonalProjectionSpan` under an affine isometry, and in particular mapping from a subspace to the full space.
---
- [x] depends on: #32016
[](https://gitpod.io/from-referrer/)
|
t-euclidean-geometry |
55/0 |
Mathlib/Geometry/Euclidean/Projection.lean |
1 |
2 |
['github-actions', 'mathlib4-dependent-issues-bot'] |
JovanGerb assignee:JovanGerb |
11-51669 11 days ago |
15-81189 15 days ago |
15-82002 15 days |
| 31733 |
jsm28 author:jsm28 |
feat(Geometry/Euclidean/Incenter): `orthRadius` lemmas |
Add lemmas, in the case where the dimensions are such that the simplex spans the whole space, exspheres are not merely tangent to the faces but the faces are the full tangent spaces (`orthRadius`).
---
- [x] depends on: #31727
- [x] depends on: #31728
- [x] depends on: #31731
[](https://gitpod.io/from-referrer/)
|
t-euclidean-geometry |
29/0 |
Mathlib/Geometry/Euclidean/Incenter.lean |
1 |
3 |
['github-actions', 'mathlib4-dependent-issues-bot', 'mathlib4-merge-conflict-bot'] |
JovanGerb assignee:JovanGerb |
11-1264 11 days ago |
20-5629 20 days ago |
20-6466 20 days |
| 31921 |
DavidLedvinka author:DavidLedvinka |
feat: FiniteExhaustion |
Creates a structure that contains the data of a non-decreasing sequence of finite sets whose union equals some countable set. This is used in the brownian motion project to transfer a theorem that holds over finite sets to a countable set (with monotone convergence).
The design is modelled on CompactExhaustion (of course it can be seen as precisely a special case but I think taking that approach would be much more convoluted).
I didn't want to give this its own file, but I couldn't put it in `Mathlib.Data.Set.Countable` without creating a `large-import` because I needed the fact that product of finite sets is finite, and couldn't find anywhere else sensible to put it that wouldn't create a `large-import`. Would be happy if someone has a better suggestion. |
t-data
brownian
|
105/0 |
Mathlib.lean,Mathlib/Data/Set/FiniteExhaustion.lean,Mathlib/Data/Set/Lattice.lean |
3 |
13 |
['ADedecker', 'DavidLedvinka', 'YaelDillies', 'github-actions'] |
pechersky assignee:pechersky |
10-82760 10 days ago |
14-68023 14 days ago |
17-54739 17 days |
| 28786 |
mitchell-horner author:mitchell-horner |
feat(Combinatorics/SimpleGraph): restate Turán's theorem in terms of `extremalNumber` |
Restates the existing proof of Turán's theorem in terms of the extremal numbers of `⊤`:
The `turanGraph` is, up to isomorphism, the unique extremal graph forbidding `⊤`.
---
- [x] depends on: #28719
- [x] depends on: #28785
[](https://gitpod.io/from-referrer/)
|
t-combinatorics |
30/0 |
Mathlib/Combinatorics/SimpleGraph/Extremal/Turan.lean |
1 |
7 |
['github-actions', 'mathlib4-dependent-issues-bot', 'mathlib4-merge-conflict-bot'] |
b-mehta assignee:b-mehta |
10-51641 10 days ago |
14-11806 14 days ago |
17-9475 17 days |
| 30921 |
EtienneC30 author:EtienneC30 |
feat: characterizing Gaussian measures through the shape of the characteristic function |
Prove that Gaussian measures over a Banach space `E` are exactly those measures `μ` such that there exist `m : E` and `f : StrongDual ℝ E →L[ℝ] StrongDual ℝ E →L[ℝ] ℝ` satisfying `f.toBilinForm.IsPosSemidef` and `charFunDual μ L = exp (L m * I - f L L / 2)`.
Prove that such `m` and `f` are unique and equal to `∫ x, x ∂μ` and `covarianceBilinDual μ`.
Specialize these statements in the case of Hilbert spaces, with `f : E →L[ℝ] E →L[ℝ] ℝ`, `charFun μ t = exp (⟪t, m⟫ * I - f t t / 2)` and `f = covarianceBilin μ`.
---
- [x] depends on: #30371
- [x] depends on: #31564
- [x] depends on: #31566
- [x] depends on: #31567
from BrownianMotion
[](https://gitpod.io/from-referrer/)
|
t-measure-probability
brownian
|
206/0 |
Mathlib.lean,Mathlib/Probability/Distributions/Gaussian/CharFun.lean,Mathlib/Probability/Moments/CovarianceBilinDual.lean |
3 |
4 |
['RemyDegenne', 'github-actions', 'mathlib4-dependent-issues-bot', 'mathlib4-merge-conflict-bot'] |
kex-y assignee:kex-y |
10-51639 10 days ago |
14-12852 14 days ago |
14-37346 14 days |
| 31988 |
winstonyin author:winstonyin |
feat: Uniqueness of implicit function |
As part of the implicit function theorem, the implicit function is locally unique.
I add some lemmas to facilitate the shuffling of factors of Cartesian products in Filter.Eventually statements.
- [ ] depends on: #30595
---
[](https://gitpod.io/from-referrer/)
|
t-analysis |
61/2 |
Mathlib/Analysis/Calculus/Implicit.lean,Mathlib/Analysis/Calculus/ImplicitContDiff.lean,Mathlib/Order/Filter/Prod.lean |
3 |
3 |
['github-actions', 'mathlib4-dependent-issues-bot', 'mathlib4-merge-conflict-bot'] |
ADedecker assignee:ADedecker |
9-51632 9 days ago |
12-73200 12 days ago |
12-73185 12 days |
| 32300 |
bjornsolheim author:bjornsolheim |
feat(Geometry/Convex/Cone): define and characterize generating convex cone |
Define the notion of a generating convex cone.
Prove some initial simple lemmas about generating cones.
---
[](https://gitpod.io/from-referrer/)
|
new-contributor
t-convex-geometry
|
18/0 |
Mathlib/Geometry/Convex/Cone/Basic.lean |
1 |
1 |
['github-actions'] |
nobody |
9-18267 9 days ago |
9-18338 9 days ago |
9-18377 9 days |
| 31891 |
jsm28 author:jsm28 |
feat(Geometry/Euclidean/Sphere/OrthRadius): lemmas for setting up and using polars |
Add further lemmas about `orthRadius` that are of use in setting up and using poles and polars. In particular,
`ncard_inter_orthRadius_eq_two_of_dist_lt_radius` is the key part of showing that, in two dimensions, there are exactly two tangents to a circle from a point outside that circle (where the points of tangency lie on the polar of the point from which the two tangents are drawn).
---
Feel free to golf the proof of `ncard_inter_orthRadius_eq_two_of_dist_lt_radius`, it could probably be rather shorter.
---
- [ ] depends on: #32296
[](https://gitpod.io/from-referrer/)
|
t-euclidean-geometry |
88/1 |
Mathlib/Geometry/Euclidean/Sphere/OrthRadius.lean |
1 |
2 |
['github-actions', 'mathlib4-dependent-issues-bot'] |
JovanGerb assignee:JovanGerb |
9-10273 9 days ago |
9-11796 9 days ago |
18-56547 18 days |
| 32146 |
foderm author:foderm |
feat(ModelTheory): add characterizations of complete theories |
Add `isComplete_eq_complete_theory` and `isComplete_iff_models_elementarily_equivalent` to connect syntactic completeness with semantic properties.
---
[](https://gitpod.io/from-referrer/)
|
t-logic
new-contributor
|
47/0 |
Mathlib/ModelTheory/Satisfiability.lean |
1 |
9 |
['awainverse', 'foderm', 'github-actions'] |
awainverse assignee:awainverse |
8-73646 8 days ago |
13-72371 13 days ago |
13-72413 13 days |
| 27100 |
staroperator author:staroperator |
feat(ModelTheory): Presburger definability and semilinear sets |
This PR formalizes the classical result that Presburger definable sets are the same as semilinear sets. As an application of this result, we show that the graph of multiplication is not Presburger definable.
---
- [x] depends on: #26896
- [x] depends on: #27081
- [x] depends on: #27087
- [x] depends on: #27414
- [x] depends on: #32123
---
[](https://gitpod.io/from-referrer/)
|
t-logic |
298/0 |
Mathlib.lean,Mathlib/ModelTheory/Arithmetic/Presburger/Definability.lean,Mathlib/ModelTheory/Arithmetic/Presburger/Semilinear/Defs.lean,docs/references.bib |
4 |
6 |
['github-actions', 'leanprover-community-bot-assistant', 'mathlib4-dependent-issues-bot', 'mathlib4-merge-conflict-bot'] |
fpvandoorn assignee:fpvandoorn |
8-51664 8 days ago |
12-888 12 days ago |
14-1314 14 days |
| 31057 |
jsm28 author:jsm28 |
feat(Geometry/Euclidean/Incenter): `reindex` lemmas |
Add lemmas about all the incenter/excenter-related definitions applied to a reindexed simplex.
---
- [x] depends on: #31054
- [x] depends on: #31055
- [x] depends on: #31056
[](https://gitpod.io/from-referrer/)
|
t-euclidean-geometry |
65/1 |
Mathlib/Geometry/Euclidean/Incenter.lean |
1 |
2 |
['github-actions', 'mathlib4-dependent-issues-bot'] |
JovanGerb assignee:JovanGerb |
8-51660 8 days ago |
12-21501 12 days ago |
12-22092 12 days |
| 32043 |
thomaskwaring author:thomaskwaring |
feat(Combinatorics/SimpleGraph/Acyclic): characterise maximal acyclic subgraphs |
We characterise subgraphs `H ≤ G` which are maximal among acyclic subgraphs of `G` as those for which `H.Reachable = G.Reachable`. We also prove that if `G` is acyclic and `x` and `y` are not reachable in `G`, then `G ⊔ fromEdgeSet {s(x,y)}` is acyclic.
---
|
t-combinatorics
new-contributor
|
91/0 |
Mathlib/Combinatorics/SimpleGraph/Acyclic.lean |
1 |
1 |
['github-actions'] |
b-mehta assignee:b-mehta |
8-51656 8 days ago |
16-18111 16 days ago |
16-18148 16 days |
| 32124 |
SnirBroshi author:SnirBroshi |
feat(SimpleGraph/Walks/Operations): expand basic drop/take/reverse API |
---
[](https://gitpod.io/from-referrer/)
|
t-combinatorics |
44/0 |
Mathlib/Combinatorics/SimpleGraph/Walks/Operations.lean |
1 |
1 |
['github-actions'] |
awainverse assignee:awainverse |
8-51654 8 days ago |
14-43964 14 days ago |
14-44007 14 days |
| 32355 |
bjornsolheim author:bjornsolheim |
feat(Geometry/Convex/Cone): define and characterize finitely generated and simplicial pointed cones |
Added file Simplicial.lean in which we:
* Define finitely generated and simplicial pointed cones.
* Prove lemmas simplicial_bot and Simplicial.fg.
---
[](https://gitpod.io/from-referrer/)
|
new-contributor
t-convex-geometry
|
80/0 |
Mathlib.lean,Mathlib/Geometry/Convex/Cone/Simplicial.lean |
2 |
1 |
['github-actions'] |
nobody |
8-1774 8 days ago |
8-1781 8 days ago |
8-1819 8 days |
| 29942 |
smmercuri author:smmercuri |
feat(InfinitePlace/Completion): embeddings of `w.Completion` factor through embeddings of `v.Completion` when `w` extends `v` |
If `w : v.Extension L` is an extension of `v : InfinitePlace K` to `L`, then `extensionEmbedding w : L →+* ℂ` factors through `extensionEmbedding v : K →+* ℂ`.
---
- [x] depends on: #27978
- [x] depends on: #29969
- [x] depends on: #29944
[](https://gitpod.io/from-referrer/)
|
FLT |
89/14 |
Mathlib/Analysis/Normed/Field/WithAbs.lean,Mathlib/NumberTheory/NumberField/InfinitePlace/Completion.lean,Mathlib/NumberTheory/NumberField/InfinitePlace/Embeddings.lean,Mathlib/NumberTheory/NumberField/InfinitePlace/Ramification.lean,Mathlib/Topology/MetricSpace/Completion.lean |
5 |
5 |
['github-actions', 'mathlib4-dependent-issues-bot', 'mathlib4-merge-conflict-bot'] |
joelriou assignee:joelriou |
7-75447 7 days ago |
11-75417 11 days ago |
11-76512 11 days |
| 32188 |
euprunin author:euprunin |
feat: add `grind` annotation for `ENNReal.inv_eq_zero` |
---
Note that the lemma being annotated is
1. already actively used with `grind` via explicit `grind [lemma]` invocations in Mathlib, and
2. already tagged with `@[simp]`.
---
[](https://gitpod.io/from-referrer/)
|
t-data |
4/5 |
Mathlib/Data/ENNReal/Inv.lean |
1 |
5 |
['euprunin', 'github-actions', 'leanprover-bot', 'leanprover-radar', 'metakunt'] |
TwoFX assignee:TwoFX |
7-66561 7 days ago |
12-68017 12 days ago |
12-68050 12 days |
| 30391 |
rudynicolop author:rudynicolop |
feat(Data/List): list splitting definitions and lemmas |
This PR continues the work from #24395.
Original PR: https://github.com/leanprover-community/mathlib4/pull/24395 |
new-contributor
t-data
|
108/2 |
Mathlib/Data/List/Perm/Lattice.lean,Mathlib/Data/List/TakeDrop.lean |
2 |
36 |
['BoltonBailey', 'github-actions', 'kckennylau', 'mathlib4-merge-conflict-bot', 'rudynicolop'] |
TwoFX assignee:TwoFX |
7-57135 7 days ago |
8-54300 8 days ago |
56-54384 56 days |
| 29393 |
staroperator author:staroperator |
feat(SetTheory/ZFC): `card (V_ o) = preBeth o` |
---
- [x] depends on: #26544
- [x] depends on: #29351
- [x] depends on: #29365
[](https://gitpod.io/from-referrer/)
|
t-set-theory
large-import
|
37/4 |
Mathlib/SetTheory/ZFC/Ordinal.lean,Mathlib/SetTheory/ZFC/VonNeumann.lean |
2 |
5 |
['github-actions', 'mathlib4-dependent-issues-bot', 'mathlib4-merge-conflict-bot', 'staroperator', 'vihdzp'] |
alreadydone assignee:alreadydone |
7-51650 7 days ago |
11-41729 11 days ago |
11-44353 11 days |
| 31967 |
bwangpj author:bwangpj |
feat: IrreducibleSpace.of_openCover |
Irreducibility can be checked on an open cover with pairwise non-empty intersections.
This contribution was created as part of the Heidelberg Lean workshop "Formalising algebraic geometry" in November 2025.
Co-authored-by: Christian Merten @chrisflav
---
[](https://gitpod.io/from-referrer/)
|
t-topology |
60/0 |
Mathlib/Topology/Irreducible.lean,Mathlib/Topology/Sets/OpenCover.lean,Mathlib/Topology/Sets/Opens.lean |
3 |
12 |
['bwangpj', 'chrisflav', 'erdOne', 'github-actions'] |
alreadydone assignee:alreadydone |
7-51645 7 days ago |
10-85672 10 days ago |
13-1738 13 days |
| 32238 |
YaelDillies author:YaelDillies |
feat(Combinatorics/SimpleGraph): distributivity of box product over sum |
From ProofBench
---
[](https://gitpod.io/from-referrer/)
|
t-combinatorics
large-import
|
21/2 |
Mathlib/Combinatorics/SimpleGraph/Prod.lean |
1 |
1 |
['github-actions'] |
kmill assignee:kmill |
7-51640 7 days ago |
11-2587 11 days ago |
11-2621 11 days |
| 31551 |
RemyDegenne author:RemyDegenne |
feat: `gaussianReal_const_sub` |
- Add lemmas stating that if `X` is a real Gaussian random variable with mean `μ` and variance `v`, then `-X`, `X - y` and `y - X` are Gaussian with variance `v` and respective means `-μ`, `μ - y` and `y - μ`.
- Generalize this section of the file from `MeasureSpace` to `MeasurableSpace`+`Measure`
---
[](https://gitpod.io/from-referrer/)
|
t-measure-probability |
31/23 |
Mathlib/Probability/Distributions/Gaussian/Real.lean |
1 |
4 |
['EtienneC30', 'github-actions'] |
EtienneC30 assignee:EtienneC30 |
7-20072 7 days ago |
7-20121 7 days ago |
7-48308 7 days |
| 32131 |
Vierkantor author:Vierkantor |
feat(scripts): count the number of tactics without a docstring |
We want to make sure every tactic is well documented. Right now, I count 33 tactics in Mathlib without any docstring at all. Add this number to the weekly technical debt metrics bot so we can track it and fix any regressions.
---
[](https://gitpod.io/from-referrer/)
|
t-meta
CI
large-import
|
68/1 |
Mathlib.lean,Mathlib/Init.lean,Mathlib/Tactic.lean,Mathlib/Tactic/Linter/TacticDocumentation.lean,scripts/nolints.json,scripts/technical-debt-metrics.sh |
6 |
18 |
['Vierkantor', 'adomani', 'bryangingechen', 'github-actions'] |
joneugster assignee:joneugster |
6-80696 6 days ago |
6-80828 6 days ago |
12-12123 12 days |
| 31425 |
robertmaxton42 author:robertmaxton42 |
feat(Topology) : implement delaborators for non-standard topology notation |
Add delaborators for unary and binary notation related to non-standard topologies in the TopologicalSpace namespace.
---
[](https://gitpod.io/from-referrer/)
|
t-topology |
104/0 |
Mathlib.lean,Mathlib/Topology/Defs/Basic.lean,Mathlib/Util/DelabNonCanonical.lean,MathlibTest/Delab/TopologicalSpace.lean |
4 |
30 |
['eric-wieser', 'github-actions', 'kckennylau', 'robertmaxton42'] |
PatrickMassot assignee:PatrickMassot |
6-51659 6 days ago |
16-30201 16 days ago |
16-61092 16 days |
| 32163 |
zhuyizheng author:zhuyizheng |
feat(MeasureTheory): interval integral is absolutely continuous |
The interval integral c..x is absolutely continuous wrt x.
Part of originally planned #29508
---
[](https://gitpod.io/from-referrer/)
|
t-measure-probability
new-contributor
|
98/3 |
Mathlib/MeasureTheory/Function/AbsolutelyContinuous.lean,Mathlib/MeasureTheory/Integral/IntervalIntegral/Basic.lean |
2 |
1 |
['github-actions'] |
urkud assignee:urkud |
6-51658 6 days ago |
13-48291 13 days ago |
13-48326 13 days |
| 32190 |
vihdzp author:vihdzp |
chore(Algebra/Order/Ring/Archimedean): generalize theorems to `OrderHomClass` + `RingHomClass` |
---
[](https://gitpod.io/from-referrer/)
|
t-algebra label:t-algebra$ |
16/12 |
Mathlib/Algebra/Order/Hom/Ring.lean,Mathlib/Algebra/Order/Ring/Archimedean.lean |
2 |
1 |
['github-actions'] |
alreadydone assignee:alreadydone |
6-51657 6 days ago |
12-65578 12 days ago |
12-65611 12 days |
| 31862 |
erdOne author:erdOne |
chore: unify `LocalizedModule` and `OreLocalization` |
We redefine `LocalizedModule` to be an abbrev of `OreLocalization S M` so that localization of a ring and localization of a module is now defeq. This is very useful to unify downstream constructions, in particular `ModuleCat.tilde` and `Spec.structureSheaf`.
Some of the declarations are switched to reducible to avoid diamonds.
This causes a significant performance regression, most notabaly in `Mathlib/AlgebraicGeometry/AffineSpace.lean`.
We shall investigate if there are ways to improve performances. For example by introducing
typeclasses to unify the two constructions on this and `LocalizedModule`, or by marking some
downstream constructions (e.g. `Spec.structureSheaf`) as irreducible.
---
[](https://gitpod.io/from-referrer/)
|
t-algebra label:t-algebra$ |
234/210 |
Mathlib/Algebra/Module/LocalizedModule/Basic.lean,Mathlib/AlgebraicGeometry/Modules/Tilde.lean,Mathlib/AlgebraicGeometry/Restrict.lean,Mathlib/GroupTheory/DivisibleHull.lean,Mathlib/GroupTheory/OreLocalization/Basic.lean,Mathlib/GroupTheory/OreLocalization/OreSet.lean,Mathlib/RingTheory/Localization/BaseChange.lean,Mathlib/RingTheory/OreLocalization/Ring.lean,Mathlib/RingTheory/TensorProduct/Nontrivial.lean,MathlibTest/Algebra/Module/LocalizedModule.lean |
10 |
73 |
['alreadydone', 'chrisflav', 'erdOne', 'github-actions', 'jcommelin', 'leanprover-bot', 'leanprover-radar', 'mattrobball', 'riccardobrasca', 'wwylele'] |
mariainesdff assignee:mariainesdff |
6-4560 6 days ago |
6-4560 6 days ago |
19-59055 19 days |
| 31886 |
CoolRmal author:CoolRmal |
feat: the family of limits in probability of sequences of uniformly integrable random variables is uniformly integrable |
---
[](https://gitpod.io/from-referrer/)
|
t-measure-probability
brownian
|
73/9 |
Mathlib/MeasureTheory/Function/ConvergenceInMeasure.lean,Mathlib/MeasureTheory/Function/UniformIntegrable.lean |
2 |
2 |
['github-actions', 'mathlib4-merge-conflict-bot'] |
EtienneC30 assignee:EtienneC30 |
5-53071 5 days ago |
6-11777 6 days ago |
6-13373 6 days |
| 32144 |
EtienneC30 author:EtienneC30 |
feat: add a predicate HasGaussianLaw |
Define a predicate `HasGaussianLaw X P`, which states that under the measure `P`, the random variable `X` has a Gaussian distribution, i.e. `IsGaussian (P.map X)`.
---
- [x] depends on: #32280
[](https://gitpod.io/from-referrer/)
|
t-measure-probability
brownian
|
267/0 |
Mathlib.lean,Mathlib/Probability/Distributions/Gaussian/HasGaussianLaw/Basic.lean,Mathlib/Probability/Distributions/Gaussian/HasGaussianLaw/Def.lean |
3 |
4 |
['EtienneC30', 'github-actions', 'mathlib4-dependent-issues-bot'] |
kex-y assignee:kex-y |
5-51638 5 days ago |
9-19093 9 days ago |
13-18551 13 days |
| 32303 |
joelriou author:joelriou |
feat(CategoryTheory): commutation of bifunctors to shifts in two variables |
This will be used when formalising triangulated bifunctors.
---
[](https://gitpod.io/from-referrer/)
|
t-category-theory |
148/1 |
Mathlib.lean,Mathlib/CategoryTheory/Center/NegOnePow.lean,Mathlib/CategoryTheory/Shift/CommShiftTwo.lean,Mathlib/CategoryTheory/Shift/Twist.lean |
4 |
1 |
['github-actions'] |
kim-em assignee:kim-em |
5-51634 5 days ago |
8-85876 8 days ago |
9-10490 9 days |
| 32306 |
plp127 author:plp127 |
fix(depRewrite): make `rw!` cleanup casts correctly |
The tactic `rw!` runs a round of `dsimp` with a minimal configuration, intended to cleanup casts. This minimal configuration is not always enough to fully reduce the casts, and may have other side effects. This PR reimplements the cast cleanup in a way not involving `dsimp` that will fully reduce casts introduced by depRewrite and will not touch other parts of the expression.
---
[](https://gitpod.io/from-referrer/)
|
t-meta |
140/51 |
Mathlib/Tactic/DepRewrite.lean,MathlibTest/depRewrite.lean |
2 |
1 |
['github-actions'] |
adamtopaz assignee:adamtopaz |
5-51633 5 days ago |
9-7171 9 days ago |
9-7157 9 days |
| 32194 |
alreadydone author:alreadydone |
feat(LinearAlgebra): more on StrongRankCondition |
Strong rank condition fails for R iff there is a copy of $R^{(\mathbb{N})}$ in some $R^n$, iff some $R^n$ has infinity rank, iff some $R^{n+1}$ has zero `finrank`. As consequences, if all $R^n$ are Noetherian or Artinian, then $R$ satisfies the strong rank condition.
To prove the first equivalence, I redeveloped a version of the ["tunnels and tailings"](https://github.com/leanprover-community/mathlib3/commit/86766851#diff-7829719aad6a9e3e617da2a7cf29dba4d55516b27e18f240eca352f4983d67b7R472-R491) construction @jcommelin and @kim-em contributed to mathlib ~4 years ago and made it work for Semiring/AddCommMonoid. The original construction was deprecated in [#12076](https://github.com/leanprover-community/mathlib4/commit/5948566497f56e1432c52d65623f1bb3c3937159) by @acmepjz and later removed, though some docstrings still remain, and I think it's now time to remove it.
Also add an instance that finite semirings satisfy the Orzech property (and therefore strong rank condition and invariant basis number).
---
- [x] depends on: #32123
[](https://gitpod.io/from-referrer/)
|
t-algebra label:t-algebra$ |
201/106 |
Mathlib/Data/Finsupp/Basic.lean,Mathlib/Data/Fintype/Card.lean,Mathlib/Data/Fintype/EquivFin.lean,Mathlib/LinearAlgebra/Dimension/StrongRankCondition.lean,Mathlib/LinearAlgebra/Finsupp/Pi.lean,Mathlib/LinearAlgebra/InvariantBasisNumber.lean,Mathlib/LinearAlgebra/LinearIndependent/Lemmas.lean,Mathlib/LinearAlgebra/Prod.lean,Mathlib/RingTheory/Artinian/Instances.lean,Mathlib/RingTheory/Artinian/Module.lean,Mathlib/RingTheory/Noetherian/Basic.lean,Mathlib/RingTheory/OrzechProperty.lean |
12 |
4 |
['alreadydone', 'eric-wieser', 'github-actions', 'mathlib4-dependent-issues-bot'] |
eric-wieser assignee:eric-wieser |
5-21304 5 days ago |
5-21304 5 days ago |
8-78862 8 days |
| 30333 |
paulorauber author:paulorauber |
feat(Probability): definition of trajMeasure |
A definition of `trajMeasure` and some basic lemmas.
In the context of the Ionescu-Tulcea theorem, `trajMeasure μ₀ κ` corresponds to the distribution of the trajectory obtained by starting with the distribution `μ₀` and then iterating the kernels `κ`.
Lemmas `partialTraj_compProd_kernel_eq_traj_map` and `traj_map_eq_kernel` are attributable to @EtienneC30 and some definitions borrow code from @RemyDegenne , who also improved the code considerably. Please let me know if you would like to be co-authors in this pull request.
From the LeanBandits project.
---
[](https://gitpod.io/from-referrer/)
|
t-measure-probability
new-contributor
maintainer-merge
|
80/2 |
Mathlib/Order/Interval/Finset/Basic.lean,Mathlib/Order/Interval/Finset/Nat.lean,Mathlib/Probability/Kernel/IonescuTulcea/PartialTraj.lean,Mathlib/Probability/Kernel/IonescuTulcea/Traj.lean |
4 |
28 |
['EtienneC30', 'RemyDegenne', 'github-actions', 'mathlib4-merge-conflict-bot', 'paulorauber'] |
EtienneC30 assignee:EtienneC30 |
5-17266 5 days ago |
5-17266 5 days ago |
12-82953 12 days |
| 32471 |
bjornsolheim author:bjornsolheim |
feat(Geometry/Convex/Cone): linear span of conic span of set equals linear span of set |
* Prove that the linear span of the conic span of a subset equals the linear span of the subset.
* This is a specialization of `Submodule.span_span_of_tower` to pointed cones.
---
[](https://gitpod.io/from-referrer/)
|
new-contributor
t-convex-geometry
|
8/0 |
Mathlib/Geometry/Convex/Cone/Pointed.lean |
1 |
1 |
['github-actions'] |
nobody |
5-7576 5 days ago |
5-7583 5 days ago |
5-7620 5 days |
| 30736 |
alreadydone author:alreadydone |
feat(RingTheory): Picard group of a domain is isomorphic to ClassGroup |
---
- [x] depends on: #30657
[](https://gitpod.io/from-referrer/)
|
t-algebra
large-import
label:t-algebra$ |
389/88 |
Mathlib/Algebra/Algebra/Bilinear.lean,Mathlib/Algebra/Algebra/Operations.lean,Mathlib/Data/Set/Semiring.lean,Mathlib/LinearAlgebra/Span/Defs.lean,Mathlib/RingTheory/ClassGroup.lean,Mathlib/RingTheory/FractionalIdeal/Basic.lean,Mathlib/RingTheory/FractionalIdeal/Operations.lean,Mathlib/RingTheory/Localization/Defs.lean,Mathlib/RingTheory/PicardGroup.lean,docs/references.bib |
10 |
17 |
['alreadydone', 'erdOne', 'github-actions', 'jcommelin', 'mathlib4-dependent-issues-bot', 'mathlib4-merge-conflict-bot'] |
mariainesdff assignee:mariainesdff |
4-85589 4 days ago |
4-85623 4 days ago |
19-78228 19 days |
| 31960 |
urkud author:urkud |
feat: a lower bound for the volume of a cone on the unit sphere |
---
- [x] depends on: #31956
- [x] depends on: #31957
[](https://gitpod.io/from-referrer/)
|
t-measure-probability |
95/0 |
Mathlib/MeasureTheory/Constructions/HaarToSphere.lean |
1 |
3 |
['github-actions', 'mathlib4-dependent-issues-bot', 'mathlib4-merge-conflict-bot'] |
hrmacbeth assignee:hrmacbeth |
4-84013 4 days ago |
14-64668 14 days ago |
14-67214 14 days |
| 30484 |
vihdzp author:vihdzp |
refactor: override `≤` and `<` in `Function.Injective.semilatticeSup`, etc. |
These constructors now take `LE` and `LT` instance arguments, and proofs that the "induced" relations are equal. This matches the behavior for all other data fields of the same constructors, which avoids diamonds which could otherwise arise.
To recover the old behavior, you can instantiate `LE` and `LT` instances through `PartialOrder.lift` (if they don't exist already), and set the `le` and `lt` fields to `Iff.rfl`.
---
I seem to have (somehow?) changed a syntactic equality on fractional ideals - given that this golfs various proofs and even removes a porting note, I think this change is desirable.
[](https://gitpod.io/from-referrer/)
|
t-order |
394/378 |
Mathlib/Algebra/Lie/Submodule.lean,Mathlib/Algebra/Module/Injective.lean,Mathlib/Algebra/Order/Group/Ideal.lean,Mathlib/Algebra/Order/Kleene.lean,Mathlib/Analysis/Convex/Cone/Dual.lean,Mathlib/Analysis/Normed/Group/Seminorm.lean,Mathlib/Analysis/Seminorm.lean,Mathlib/CategoryTheory/Sites/Precoverage.lean,Mathlib/Combinatorics/Digraph/Basic.lean,Mathlib/Combinatorics/SimpleGraph/Basic.lean,Mathlib/Combinatorics/SimpleGraph/Finsubgraph.lean,Mathlib/Combinatorics/SimpleGraph/Subgraph.lean,Mathlib/Combinatorics/Young/YoungDiagram.lean,Mathlib/FieldTheory/Galois/GaloisClosure.lean,Mathlib/GroupTheory/GroupAction/SubMulAction.lean,Mathlib/MeasureTheory/MeasurableSpace/MeasurablyGenerated.lean,Mathlib/ModelTheory/Definability.lean,Mathlib/NumberTheory/NumberField/FractionalIdeal.lean,Mathlib/Order/BooleanAlgebra/Basic.lean,Mathlib/Order/BooleanSubalgebra.lean,Mathlib/Order/CompleteBooleanAlgebra.lean,Mathlib/Order/CompleteLattice/Basic.lean,Mathlib/Order/CompleteLattice/Lemmas.lean,Mathlib/Order/CompleteSublattice.lean,Mathlib/Order/Concept.lean,Mathlib/Order/Disjoint.lean,Mathlib/Order/Heyting/Basic.lean,Mathlib/Order/Heyting/Regular.lean,Mathlib/Order/Hom/Bounded.lean,Mathlib/Order/Hom/BoundedLattice.lean,Mathlib/Order/Hom/Lattice.lean,Mathlib/Order/Interval/Basic.lean,Mathlib/Order/Lattice.lean,Mathlib/Order/Nucleus.lean,Mathlib/Order/Sublattice.lean,Mathlib/Order/UpperLower/CompleteLattice.lean,Mathlib/RingTheory/DedekindDomain/Different.lean,Mathlib/RingTheory/DedekindDomain/Factorization.lean,Mathlib/RingTheory/DedekindDomain/Ideal/Basic.lean,Mathlib/RingTheory/DividedPowers/SubDPIdeal.lean,Mathlib/RingTheory/Filtration.lean,Mathlib/RingTheory/FractionalIdeal/Basic.lean,Mathlib/RingTheory/FractionalIdeal/Extended.lean,Mathlib/RingTheory/FractionalIdeal/Inverse.lean,Mathlib/RingTheory/FractionalIdeal/Operations.lean,Mathlib/RingTheory/GradedAlgebra/Homogeneous/Ideal.lean,Mathlib/Topology/Algebra/Group/ClosedSubgroup.lean,Mathlib/Topology/Algebra/Group/GroupTopology.lean,Mathlib/Topology/Algebra/Module/ClosedSubmodule.lean,Mathlib/Topology/Algebra/OpenSubgroup.lean,Mathlib/Topology/ContinuousMap/Bounded/Normed.lean,Mathlib/Topology/ContinuousMap/CompactlySupported.lean,Mathlib/Topology/ContinuousMap/Ordered.lean,Mathlib/Topology/DiscreteQuotient.lean,Mathlib/Topology/Sets/Closeds.lean,Mathlib/Topology/Sets/Compacts.lean,Mathlib/Topology/Sets/Opens.lean,Mathlib/Topology/Sets/Order.lean |
58 |
40 |
['Vierkantor', 'YaelDillies', 'github-actions', 'jcommelin', 'leanprover-bot', 'leanprover-radar', 'mathlib4-merge-conflict-bot', 'plp127', 'vihdzp'] |
bryangingechen assignee:bryangingechen |
4-75219 4 days ago |
13-74071 13 days ago |
19-58755 19 days |
| 13740 |
YaelDillies author:YaelDillies |
feat: more robust ae notation |
Make sure that, when `μ : FiniteMeasure Ω`, `f =ᵐ[μ] g` elaborates to `f =ᵐ[↑μ] g` instead of complaining about `OuterMeasureClass (FiniteMeasure Ω) (Set Ω) ℝ≥0∞` not existing.
[Zulip](https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/ae.20of.20a.20finite.20measure)
---
[](https://gitpod.io/from-referrer/)
|
t-meta
t-measure-probability
|
67/8 |
Mathlib/MeasureTheory/Integral/Bochner/L1.lean,Mathlib/MeasureTheory/Measure/Decomposition/IntegralRNDeriv.lean,Mathlib/MeasureTheory/Measure/MeasureSpaceDef.lean,Mathlib/MeasureTheory/OuterMeasure/AE.lean,Mathlib/MeasureTheory/OuterMeasure/BorelCantelli.lean,Mathlib/Probability/Notation.lean |
6 |
40 |
['YaelDillies', 'eric-wieser', 'github-actions', 'leanprover-community-bot-assistant', 'thorimur', 'urkud'] |
RemyDegenne and thorimur assignee:RemyDegenne assignee:thorimur |
4-68182 4 days ago |
34-85158 1 month ago |
34-85115 34 days |
| 32127 |
CoolRmal author:CoolRmal |
feat: use IndexedPartition.piecewise to create simple/measurable/strongly measurable functions |
The lemmas proved in this PR are needed in https://github.com/RemyDegenne/brownian-motion/pull/304.
---
[](https://gitpod.io/from-referrer/)
|
t-measure-probability
large-import
brownian
|
122/4 |
Mathlib/Data/Setoid/Partition.lean,Mathlib/MeasureTheory/Function/SimpleFunc.lean,Mathlib/MeasureTheory/Function/StronglyMeasurable/Basic.lean,Mathlib/MeasureTheory/MeasurableSpace/Basic.lean |
4 |
17 |
['CoolRmal', 'EtienneC30', 'github-actions', 'hanwenzhu', 'mathlib4-merge-conflict-bot'] |
EtienneC30 assignee:EtienneC30 |
4-67342 4 days ago |
4-71953 4 days ago |
12-81311 12 days |
| 31805 |
joelriou author:joelriou |
feat(AlgebraicTopology): horns in Δ[n] as multicoequalizers |
Some API is also introduced for the particular case of inner horns in `Δ[3]`.
Co-authored-by: Nick Ward gio256@protonmail.com
From https://github.com/joelriou/topcat-model-category
---
- [x] depends on: #31802
- [x] depends on: #31797
[](https://gitpod.io/from-referrer/)
|
t-algebraic-topology |
179/1 |
Mathlib/AlgebraicTopology/SimplicialSet/HornColimits.lean,Mathlib/AlgebraicTopology/SimplicialSet/StdSimplex.lean |
2 |
3 |
['github-actions', 'mathlib4-dependent-issues-bot', 'mathlib4-merge-conflict-bot'] |
robin-carlier assignee:robin-carlier |
4-51666 4 days ago |
4-73600 4 days ago |
4-73592 4 days |
| 32267 |
vlad902 author:vlad902 |
feat(SimpleGraph): add `SimpleGraph.HomClass` |
Inspired by [this PR review feedback.](https://github.com/leanprover-community/mathlib4/pull/30129#discussion_r2530032044)
---
[](https://gitpod.io/from-referrer/)
|
t-combinatorics |
4/0 |
Mathlib/Combinatorics/SimpleGraph/Maps.lean |
1 |
1 |
['YaelDillies', 'github-actions'] |
b-mehta assignee:b-mehta |
4-51662 4 days ago |
10-16708 10 days ago |
10-16742 10 days |
| 32323 |
LLaurance author:LLaurance |
feat(Combinatorics/SimpleGraph/Connectivity): exists vertex adjacent to any vertex of a nontrivial connected graph |
---
[](https://gitpod.io/from-referrer/)
|
t-combinatorics |
15/0 |
Mathlib/Combinatorics/SimpleGraph/Connectivity/Connected.lean,Mathlib/Combinatorics/SimpleGraph/Connectivity/Subgraph.lean |
2 |
1 |
['github-actions'] |
kmill assignee:kmill |
4-51661 4 days ago |
8-76022 8 days ago |
8-78749 8 days |
| 32134 |
mitchell-horner author:mitchell-horner |
feat(Topology/Real): theorems linking `IsGLB` with `BddBelow`, `Antitone`, `Tendsto _ atTop` |
Implement theorems linking `IsGLB` (`IsLUB`) with `BddBelow` (`BddAbove`), `Antitone` (`Monotone`), `Tendsto _ atTop`
---
[](https://gitpod.io/from-referrer/)
|
t-topology
large-import
|
117/63 |
Mathlib/Algebra/Order/Monoid/Canonical/Basic.lean,Mathlib/Analysis/Normed/Unbundled/SeminormFromConst.lean,Mathlib/Analysis/Normed/Unbundled/SpectralNorm.lean,Mathlib/Topology/Instances/NNReal/Lemmas.lean |
4 |
18 |
['YaelDillies', 'github-actions', 'mitchell-horner'] |
YaelDillies assignee:YaelDillies |
4-14705 4 days ago |
4-17723 4 days ago |
4-59110 4 days |
| 31161 |
AntoineChambert-Loir author:AntoineChambert-Loir |
feat(RingTheory/MvPolynomial/IrrQuadratic): irreducibility of sum X_i Y_i |
The quadratic polynomial $$\sum_i c_i X_i Y_i$$ is irreducible, provided the following three conditions holds:
* the ground ring is a domain
* there are at least 2 nonzero $$c_i$$
* only units of $$R$$ divide all $$c_i$$.
This was used in the initial proof that the transvections have determinant 1. Now,
a more general result is proved there and this PR is no more needed.
I believe that it remains of independent interest (irreducibility of quadrics in algebraic geometry) but the maintainers might want that the general one.
---
- [x] depends on: #32226
[](https://gitpod.io/from-referrer/)
|
t-ring-theory |
346/3 |
Mathlib.lean,Mathlib/Algebra/Polynomial/RingDivision.lean,Mathlib/RingTheory/MvPolynomial/IrrQuadratic.lean,Mathlib/RingTheory/MvPolynomial/MonomialOrder/DegLex.lean |
4 |
38 |
['AntoineChambert-Loir', 'github-actions', 'jcommelin', 'joelriou', 'mathlib4-dependent-issues-bot', 'mathlib4-merge-conflict-bot', 'ocfnash'] |
joelriou assignee:joelriou |
4-1594 4 days ago |
4-1594 4 days ago |
31-20093 31 days |
| 32412 |
Brian-Nugent author:Brian-Nugent |
feat: add Artinian schemes |
Added the definition of Artinian Schemes and proved basic facts about them.
---
[](https://gitpod.io/from-referrer/)
|
t-algebraic-geometry
new-contributor
|
215/0 |
.vscode/keybindings.json,.vscode/settings.json,Mathlib.lean,Mathlib/AlgebraicGeometry/Artinian.lean,Mathlib/Topology/KrullDimension.lean |
5 |
51 |
['Brian-Nugent', 'alreadydone', 'erdOne', 'github-actions'] |
erdOne assignee:erdOne |
3-54174 3 days ago |
3-58008 3 days ago |
3-63350 3 days |
| 32527 |
PrParadoxy author:PrParadoxy |
chore(LinearAlgebra/PiTensorProduct): remove use of `erw` in `nonempty_lifts` and `liftAux_tprod` |
---
[](https://gitpod.io/from-referrer/)
|
t-algebra
new-contributor
label:t-algebra$ |
2/2 |
Mathlib/LinearAlgebra/PiTensorProduct.lean |
1 |
1 |
['github-actions'] |
nobody |
3-52247 3 days ago |
3-52251 3 days ago |
3-52291 3 days |
| 32492 |
bjornsolheim author:bjornsolheim |
feat(LinearAlgebra/TensorProduct): explicit tensor product decomposition in a finite basis |
* Given a finite basis `ℬ` for `M`, any tensor `x ∈ M ⊗ N` decomposes as `∑ᵢ ℬᵢ ⊗ₜ nᵢ`
where the `N`-component `nᵢ` is obtained by applying `ℬ.coord i ⊗ id` to `x` and then
identifying `R ⊗ N ≃ N` via `lid`.
* Similarly for the right hand tensor product component version.
---
[](https://gitpod.io/from-referrer/)
|
t-algebra
new-contributor
label:t-algebra$ |
22/0 |
Mathlib/LinearAlgebra/TensorProduct/Basis.lean |
1 |
6 |
['bjornsolheim', 'erdOne', 'github-actions', 'themathqueen'] |
nobody |
3-51831 3 days ago |
3-51831 3 days ago |
4-37599 4 days |
| 32532 |
SnirBroshi author:SnirBroshi |
feat(Combinatorics/SimpleGraph/Connectivity): connected components are maximally connected subsets/subgraphs |
---
[](https://gitpod.io/from-referrer/)
|
t-combinatorics |
32/0 |
Mathlib/Combinatorics/SimpleGraph/Connectivity/Connected.lean,Mathlib/Combinatorics/SimpleGraph/Connectivity/Subgraph.lean |
2 |
1 |
['github-actions'] |
nobody |
3-34962 3 days ago |
3-35374 3 days ago |
3-35418 3 days |
| 32482 |
sgouezel author:sgouezel |
feat: extend Stieltjes measures to more general index types |
Stieltjes measures are currently only defined on the real line. We extend the definition to more general index sets, to allow for instance the nonnegative reals or compact intervals. Some proofs become more cumbersome because we have to deal with the possibility of a bottom or a top element, but the end results are exactly the same as on the real line.
---
- [x] depends on: #32516
[](https://gitpod.io/from-referrer/)
|
t-measure-probability |
374/173 |
Mathlib/Analysis/Calculus/Monotone.lean,Mathlib/MeasureTheory/Measure/Stieltjes.lean,Mathlib/Probability/CDF.lean,Mathlib/Probability/Distributions/Exponential.lean,Mathlib/Probability/Distributions/Gamma.lean,Mathlib/Probability/Kernel/Disintegration/CDFToKernel.lean,Mathlib/Probability/Kernel/Disintegration/CondCDF.lean,Mathlib/Probability/Kernel/Disintegration/MeasurableStieltjes.lean,Mathlib/Probability/Kernel/Disintegration/StandardBorel.lean |
9 |
2 |
['github-actions', 'mathlib4-dependent-issues-bot'] |
nobody |
3-12073 3 days ago |
3-13327 3 days ago |
3-18920 3 days |
| 32537 |
erdOne author:erdOne |
feat(RingTheory): strongly transcendental elements |
---
[](https://gitpod.io/from-referrer/)
|
t-ring-theory |
152/0 |
Mathlib.lean,Mathlib/Algebra/Group/Action/Faithful.lean,Mathlib/RingTheory/Algebraic/StronglyTranscendental.lean |
3 |
1 |
['github-actions'] |
nobody |
3-8314 3 days ago |
3-8314 3 days ago |
3-8853 3 days |
| 32529 |
erdOne author:erdOne |
feat(RingTheory): the etale locus of an algebra |
---
[](https://gitpod.io/from-referrer/)
|
t-ring-theory |
109/1 |
Mathlib.lean,Mathlib/RingTheory/Etale/Locus.lean,Mathlib/RingTheory/Unramified/Locus.lean |
3 |
1 |
['github-actions'] |
nobody |
3-8277 3 days ago |
3-47794 3 days ago |
3-47829 3 days |
| 32432 |
YaelDillies author:YaelDillies |
feat: `MulDistribMulAction M Nˣ` instance |
From ClassFieldTheory
[Zulip](https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/MulDistribMulAction.20instances)
---
[](https://gitpod.io/from-referrer/)
|
t-algebra
CFT
label:t-algebra$ |
30/0 |
Mathlib/Algebra/Group/Action/Units.lean |
1 |
2 |
['erdOne', 'github-actions'] |
nobody |
3-8085 3 days ago |
3-8152 3 days ago |
5-13408 5 days |
| 32528 |
erdOne author:erdOne |
feat(RingTheory): going-down for integrally closed domains |
---
[](https://gitpod.io/from-referrer/)
|
t-ring-theory |
215/2 |
Mathlib.lean,Mathlib/FieldTheory/Minpoly/IsIntegrallyClosed.lean,Mathlib/RingTheory/Ideal/GoingDown.lean,Mathlib/RingTheory/IntegralClosure/Algebra/Ideal.lean,Mathlib/RingTheory/IntegralClosure/GoingDown.lean |
5 |
1 |
['github-actions'] |
nobody |
3-6710 3 days ago |
3-6710 3 days ago |
3-48214 3 days |
| 32540 |
erdOne author:erdOne |
feat(RingTheory): properties on `Algebra.TensorProduct.map` |
---
[](https://gitpod.io/from-referrer/)
|
t-ring-theory |
72/1 |
Mathlib/RingTheory/Finiteness/Basic.lean,Mathlib/RingTheory/SurjectiveOnStalks.lean,Mathlib/RingTheory/TensorProduct/Finite.lean |
3 |
1 |
['github-actions'] |
nobody |
3-6683 3 days ago |
3-6700 3 days ago |
3-6724 3 days |
| 32435 |
YaelDillies author:YaelDillies |
chore(Algebra/Module): make select `Module` assumptions |
This solves a thorny issue that we have when working with homological algebra: an element `X : ModuleCat ℤ` by construction contain the data of two (propeq) `Module ℤ X` instances. Instead of fighting typeclasses at the point of use, it is enough to make the `Module ℤ X` assumptions that can be inferred from other arguments actually be inferred by unification, rather than filled in with typeclass search. This PR does precisely that for the handful of definitions that are particularly problematic for the purpose of CFT.
This is not unlike the status of `MeasurableSpace` in the measure theory library, and in fact there already existed a library note explaining this design decision, but it didn't cover that use case, so I expanded it.
From ClassFieldTheory
---
[](https://gitpod.io/from-referrer/)
|
t-algebra
CFT
label:t-algebra$ |
37/18 |
Mathlib/Algebra/HierarchyDesign.lean,Mathlib/Algebra/Module/Equiv/Basic.lean,Mathlib/Algebra/Module/Equiv/Defs.lean,Mathlib/Algebra/Module/LinearMap/Defs.lean |
4 |
2 |
['erdOne', 'github-actions'] |
nobody |
3-5965 3 days ago |
3-6035 3 days ago |
5-2601 5 days |
| 26719 |
AntoineChambert-Loir author:AntoineChambert-Loir |
feat(RingTheory/PolynomialLaw/Basic): extends polynomial laws to arbitrary universes |
The definition of polynomial laws restricts its operations to a fixed universe.
This PR constructs the extension to any universe.
This is part of the project of studying divided powers on rings, in particular, for studying
the universal divided power algebra of a module.
Co-authored-by: María-Inés de Frutos Fernández @mariainesdff
---
- [x] depends on: #26717
- [ ] depends on: #26277
[](https://gitpod.io/from-referrer/)
|
blocked-by-other-PR
large-import
t-ring-theory
|
969/7 |
Mathlib.lean,Mathlib/Algebra/Ring/Subsemiring/Basic.lean,Mathlib/Algebra/RingQuot.lean,Mathlib/LinearAlgebra/TensorProduct/Tower.lean,Mathlib/RingTheory/Congruence/Basic.lean,Mathlib/RingTheory/Congruence/Defs.lean,Mathlib/RingTheory/Congruence/Hom.lean,Mathlib/RingTheory/PolynomialLaw/Basic.lean |
8 |
4 |
['acmepjz', 'github-actions', 'leanprover-community-bot-assistant', 'mathlib4-dependent-issues-bot'] |
nobody |
112-17177 3 months ago |
127-20827 4 months ago |
0-1757 29 minutes |
| 27599 |
mitchell-horner author:mitchell-horner |
feat(Combinatorics/SimpleGraph): define `CompleteEquipartiteSubgraph` |
Define the complete equipartite subgraphs in `r` parts each of size `t` in `G` as the `r` subsets of vertices each of size `t` such that vertices in distinct subsets are adjacent.
In this case `Nonempty (G.CompleteEquipartiteSubgraph r t)` is equivalent to `completeEquipartiteGraph r t ⊑ G`, that is, finding `r` subsets of vertices each of size `t` in `G` such that vertices in distinct subsets are adjacent is equivalent to finding an injective homomorphism from `completeEquipartiteGraph r t` to `G`.
---
- [x] depends on: #27597
- [x] depends on: #30287
[](https://gitpod.io/from-referrer/)
|
t-combinatorics |
117/7 |
Mathlib/Combinatorics/SimpleGraph/CompleteMultipartite.lean |
1 |
27 |
['YaelDillies', 'b-mehta', 'github-actions', 'mathlib4-dependent-issues-bot', 'mathlib4-merge-conflict-bot', 'mitchell-horner'] |
YaelDillies assignee:YaelDillies |
3-3224 3 days ago |
4-53740 4 days ago |
61-38773 61 days |
| 30436 |
wwylele author:wwylele |
feat(Topology/InfiniteSum): tprod_one_{add/sub}_ordered |
This extends the existing `Finset.prod_one_sub_ordered` to infinite sum/product, and also adds the more natural `add` version.
Together with some previous PRs about infinite sum/prod and powerseries, this is part of my effort of upstreaming useful stuff from https://github.com/wwylele/PentagonalNumberTheorem. It starts getting into niche lemma, so suggestions such that not wanting this in mathlib, or it should be stated in a different form, are all welcomed.
---
[](https://gitpod.io/from-referrer/)
|
t-topology |
42/0 |
Mathlib/Algebra/BigOperators/Ring/Finset.lean,Mathlib/Topology/Algebra/InfiniteSum/Ring.lean |
2 |
6 |
['github-actions', 'kckennylau', 'wwylele'] |
grunweg assignee:grunweg |
2-81701 2 days ago |
2-81701 2 days ago |
44-26319 44 days |
| 32541 |
YaelDillies author:YaelDillies |
chore: import Tactic.Attr.Register privately |
This is mostly to start a discussion: Should basic tactic files like this one be re-exported by all files out of them being basic, or whether they should be explicitly imported by the few files that actually need it.
Eg in #32245 Andrew and I are adding a new simp attribute, and it's a bit silly that we have to rebuild all of mathlib because that file is re-exported everywhere.
---
[](https://gitpod.io/from-referrer/)
|
large-import |
43/9 |
Mathlib/Algebra/Free.lean,Mathlib/CategoryTheory/Monoidal/Mon_.lean,Mathlib/Control/Applicative.lean,Mathlib/Control/Basic.lean,Mathlib/Control/Functor.lean,Mathlib/Control/Monad/Basic.lean,Mathlib/Control/Traversable/Basic.lean,Mathlib/Control/Traversable/Equiv.lean,Mathlib/Control/Traversable/Lemmas.lean,Mathlib/Data/Prod/Basic.lean,Mathlib/Data/Set/Operations.lean,Mathlib/Logic/Basic.lean,Mathlib/Logic/Equiv/Defs.lean,Mathlib/Logic/Function/Basic.lean,Mathlib/Logic/Function/Defs.lean,Mathlib/Logic/Nontrivial/Basic.lean,Mathlib/Tactic/Attr/Core.lean,Mathlib/Tactic/HigherOrder.lean,Mathlib/Tactic/Zify.lean |
19 |
1 |
['github-actions'] |
nobody |
2-79222 2 days ago |
2-80230 2 days ago |
3-4122 3 days |
| 26483 |
metakunt author:metakunt |
feat(RingTheory/RootsOfUnity/PrimitiveRoots): add equivPrimitiveRootsOfCoprimePow |
Adds equivalence of r-th primitive roots by a coprime e. |
new-contributor
t-ring-theory
|
55/0 |
Mathlib/RingTheory/RootsOfUnity/PrimitiveRoots.lean |
1 |
17 |
['Citronhat', 'Ruben-VandeVelde', 'github-actions', 'metakunt'] |
nobody |
2-77560 2 days ago |
2-77560 2 days ago |
31-72961 31 days |
| 32533 |
metakunt author:metakunt |
feat(Algebra/Polynomial/Roots): Add ofMultiset_injective |
This shows that the product of roots (as a multiset) is injective. |
t-algebra
new-contributor
label:t-algebra$ |
11/0 |
Mathlib/Algebra/Polynomial/Roots.lean |
1 |
3 |
['SnirBroshi', 'github-actions', 'metakunt'] |
nobody |
2-77223 2 days ago |
3-18548 3 days ago |
3-18585 3 days |
| 32367 |
BoltonBailey author:BoltonBailey |
feat(Computability): add finEncodings for List Bool and pairs of types |
This PR contains `finEncoding`s relevant to developing complexity theory in downstream libraries. It is adapted from [this](https://leanprover.zulipchat.com/#narrow/channel/116395-maths/topic/Formalise.20the.20proposition.20P.20.E2.89.A0NP/near/451765788)[#maths > Formalise the proposition P ≠NP @ 💬](https://leanprover.zulipchat.com/#narrow/channel/116395-maths/topic/Formalise.20the.20proposition.20P.20.E2.89.A0NP/near/451765788) comment.
Co-authored-by: Daniel Weber
---
[](https://gitpod.io/from-referrer/)
|
t-computability |
58/3 |
Mathlib/Computability/Encoding.lean,Mathlib/Data/List/Basic.lean,Mathlib/Data/Sum/Basic.lean |
3 |
2 |
['MichaelStollBayreuth', 'github-actions'] |
nobody |
2-75815 2 days ago |
2-75934 2 days ago |
7-70366 7 days |
| 32479 |
WenrongZou author:WenrongZou |
feat(RingTheory/PowerSeries/Substitution): add `le_order_subst` |
I add a theorem saying multiplication of order less than the order of substitution. I tried to put at the file `PowerSeries.Order`, but it seems like in this file we already import `PowerSeries.Substitution`.
---
[](https://gitpod.io/from-referrer/)
|
new-contributor
t-ring-theory
|
71/0 |
Mathlib/RingTheory/MvPowerSeries/Substitution.lean,Mathlib/RingTheory/PowerSeries/Order.lean,Mathlib/RingTheory/PowerSeries/Substitution.lean |
3 |
19 |
['AntoineChambert-Loir', 'WenrongZou', 'erdOne', 'github-actions'] |
nobody |
2-70771 2 days ago |
2-70771 2 days ago |
3-63186 3 days |
| 32559 |
WenrongZou author:WenrongZou |
feat(RingTheory/PowerSeries): toSubring and ofSubring for MvPowerSeries |
define MvPowerSeries.toSubring and MvPowerSeries.ofSubring, and prove their order and weighted order are equal. (same for PowerSeries.)
---
[](https://gitpod.io/from-referrer/)
|
new-contributor
t-ring-theory
|
104/0 |
Mathlib/RingTheory/MvPowerSeries/Basic.lean,Mathlib/RingTheory/MvPowerSeries/Order.lean,Mathlib/RingTheory/PowerSeries/Basic.lean,Mathlib/RingTheory/PowerSeries/Order.lean |
4 |
1 |
['github-actions'] |
nobody |
2-64293 2 days ago |
2-64548 2 days ago |
2-64587 2 days |
| 32546 |
anishrajeev author:anishrajeev |
feat(ModelTheory): Define and characterize the type space |
Define the space of types and prove various topological properties of it (zero dimensional, totally separated, compact, baire).
The goal is to formalize the proof of the Omitting Types Theorem |
t-logic
new-contributor
large-import
|
123/3 |
Mathlib/ModelTheory/Types.lean,Mathlib/Tactic/Linter/DirectoryDependency.lean |
2 |
1 |
['github-actions'] |
nobody |
2-64138 2 days ago |
2-80946 2 days ago |
2-80985 2 days |
| 31610 |
rudynicolop author:rudynicolop |
feat(Computability/NFA): Kleene star closure for Regular Languages via NFA |
This PR constructs a Kleene star closure for non-epsilon NFAs, and proves that regular languages are closed under Kleene star. The NFA construction is `NFA.kstar`. The main theorems are:
- `NFA.accepts_kstar`: demonstrates that `M.kstar` accepts the Kleene star closure of the language of `M`.
- `IsRegular.kstar`: demonstrates that regular languages are closed under Kleene star.
There is an onging zulip discussion about regular languages in Mathlib: https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/Regular.20languages.3A.20the.20review.20queue/with/553759136
This discussion is also tracked at #24205.
Furthermore, the construction and proofs in this PR are heavily inspired by @TpmKranz from his #15651. #15651 supersedes this PR, so if it is accepted then this PR is not needed.
---
- [x] depends on: #31038
[](https://gitpod.io/from-referrer/)
|
new-contributor
t-computability
|
405/7 |
Mathlib/Computability/NFA.lean |
1 |
5 |
['ctchou', 'github-actions', 'mathlib4-dependent-issues-bot', 'mathlib4-merge-conflict-bot'] |
nobody |
2-59873 2 days ago |
8-63075 8 days ago |
8-66029 8 days |
| 32560 |
AntoineChambert-Loir author:AntoineChambert-Loir |
feat(LinearAlgebra/Dimension/Constructions): construct a basis from one of submodule and quotient |
Let `V` be an `R`-module. Let `W` be a submodule of `V` with a basis `b` and `c` be a basis of the quotient module `V ⧸ W`.
`basisSum b c` is a basis of `V` indexed by the sum type of the index types of `b` and `c` that extends `b`and lifts `c`.
We apply this construction to a determinant equality: `LinearMap.det_eq_det_mul_det` shows that if a linear map `f : V →ₗ[R] V` stabilizes the submodule `W`,
then the determinant of `f` is the product of the determinants of the linear endomorphisms of `W` and `V ⧸ W` induced by `f`.
---
[](https://gitpod.io/from-referrer/)
|
t-algebra label:t-algebra$ |
151/0 |
Mathlib/LinearAlgebra/Determinant.lean,Mathlib/LinearAlgebra/Dimension/Constructions.lean |
2 |
1 |
['github-actions'] |
nobody |
2-53487 2 days ago |
2-58817 2 days ago |
2-58829 2 days |
| 31478 |
BGuillemet author:BGuillemet |
feat(CategoryTheory/Sites): `uliftYoneda` for sheaves over a subcanonical topology |
Add that `GrothendieckTopology.uliftYoneda` is fully faithful.
Add the (functorial) Yoneda lemma for sheaves, for both `yoneda` and `uliftYoneda`.
---
- [x] depends on: #27821
- [x] depends on: #31538
[](https://gitpod.io/from-referrer/)
|
t-category-theory |
88/1 |
Mathlib/CategoryTheory/Sites/Canonical.lean,Mathlib/CategoryTheory/Sites/Subcanonical.lean,Mathlib/CategoryTheory/Sites/Whiskering.lean |
3 |
13 |
['BGuillemet', 'dagurtomas', 'github-actions', 'joelriou', 'mathlib4-dependent-issues-bot', 'mathlib4-merge-conflict-bot'] |
dagurtomas assignee:dagurtomas |
2-51659 2 days ago |
6-5402 6 days ago |
7-27892 7 days |
| 31717 |
thorimur author:thorimur |
chore: refactor `Type*` and `Sort*` to use `mkFreshLevelParam` |
Uses the API for creating new level parameters introduced in #30797.
---
- [ ] depends on: #30797
[](https://gitpod.io/from-referrer/)
|
t-meta
large-import
|
4/7 |
Mathlib/Tactic/TypeStar.lean |
1 |
3 |
['github-actions', 'mathlib4-dependent-issues-bot', 'mathlib4-merge-conflict-bot'] |
dwrensha assignee:dwrensha |
2-51658 2 days ago |
5-78074 5 days ago |
8-32775 8 days |
| 32374 |
adamtopaz author:adamtopaz |
feat(Tactic/WildcardUniverse): Foo.{*, _, v*, max u v} |
This PR creates an elaborator for syntax of the form `Foo.{*, _, v*, max u v}`. A `*` indicates that a new universe parameter should be created, `_` and `max u v` elaborate using the existing level elaboration (so `_` elaborates to a level mvar). The syntax `v*` creates a level parameter of the form `v_n` for some value of `n`.
The newly created level parameters are ordered in a particular way to match the order in which they appear in the syntax. For example, in `Foo.{*, _, v*, max u v}`, the level parameter associated with `*` will come before the other universes, including the parameter created by `v*`, and the parameters `u` and `v`. Similarly the parameter associated with `v*` will come *after* the one for `*`, and before both `u` and `v`.
Note: Unlike `Category* C`, where we understand exactly how the universes involved in `C` (both in the term and its type) relate to the level parameter of the morphisms, we can't expect such precise control in general. For example, when `C.{u} : Type 0`, `Category* C` places the morphism level `v_1` before `u`, but `Category.{*} C` places it after `u`. In other words, `Foo.{...}` only reorders the level parameters based on the parameters that appear in the (elaborated) `...`, without any regard to the universes that appear in the *arguments* to `Foo.{...}`.
Co-authored-by: Claude
---
[](https://gitpod.io/from-referrer/)
|
t-meta |
703/0 |
Mathlib.lean,Mathlib/Tactic.lean,Mathlib/Tactic/WildcardLevel.lean,MathlibTest/WildcardLevel.lean |
4 |
25 |
['JovanGerb', 'adamtopaz', 'github-actions'] |
dwrensha assignee:dwrensha |
2-51656 2 days ago |
5-57987 5 days ago |
6-62587 6 days |
| 32427 |
YaelDillies author:YaelDillies |
refactor(Algebra/Algebra): genericise algebra instances for subsemirings |
From ClassFieldTheory
---
[](https://gitpod.io/from-referrer/)
|
t-algebra
CFT
label:t-algebra$ |
51/67 |
Mathlib/Algebra/Algebra/Basic.lean,Mathlib/Algebra/Algebra/Subalgebra/Basic.lean,Mathlib/Algebra/Algebra/Subalgebra/Tower.lean,Mathlib/Algebra/DirectSum/Internal.lean,Mathlib/Analysis/Normed/Unbundled/SpectralNorm.lean,Mathlib/NumberTheory/Cyclotomic/Basic.lean,Mathlib/NumberTheory/NumberField/CMField.lean,Mathlib/NumberTheory/Padics/PadicIntegers.lean,Mathlib/RingTheory/Algebraic/Integral.lean,Mathlib/RingTheory/Algebraic/MvPolynomial.lean,Mathlib/RingTheory/Extension/Presentation/Core.lean,Mathlib/RingTheory/IntegralClosure/IntegralRestrict.lean,Mathlib/RingTheory/LocalRing/LocalSubring.lean,Mathlib/RingTheory/Polynomial/Basic.lean,Mathlib/RingTheory/Valuation/AlgebraInstances.lean,Mathlib/RingTheory/Valuation/Integers.lean |
16 |
1 |
['github-actions'] |
joelriou assignee:joelriou |
2-51652 2 days ago |
6-11155 6 days ago |
6-11132 6 days |
| 32429 |
erdOne author:erdOne |
feat(RingTheory): `IsIntegrallyClosed R[X]` |
---
[](https://gitpod.io/from-referrer/)
|
t-ring-theory |
279/3 |
Mathlib.lean,Mathlib/RingTheory/IntegralClosure/IntegrallyClosed.lean,Mathlib/RingTheory/IntegralClosure/IsIntegral/AlmostIntegral.lean,Mathlib/RingTheory/Polynomial/IsIntegral.lean |
4 |
1 |
['github-actions'] |
alreadydone and mattrobball assignee:alreadydone assignee:mattrobball |
2-51651 2 days ago |
5-85853 5 days ago |
5-86009 5 days |
| 32428 |
sven-manthe author:sven-manthe |
feat(Algebra): add Subsemigroup.op |
the file Subsemigroup.MulOpposite is analogous to Submonoid.MulOpposite. Also add trivial lemmas on relation with monoids and groups in the corresponding file
---
[](https://gitpod.io/from-referrer/)
|
t-algebra label:t-algebra$ |
199/4 |
Mathlib.lean,Mathlib/Algebra/Group/Subgroup/MulOpposite.lean,Mathlib/Algebra/Group/Submonoid/MulOpposite.lean,Mathlib/Algebra/Group/Subsemigroup/MulOpposite.lean |
4 |
1 |
['github-actions'] |
dagurtomas assignee:dagurtomas |
2-51651 2 days ago |
6-4627 6 days ago |
6-4661 6 days |
| 32433 |
YaelDillies author:YaelDillies |
feat: an irreducible element of a submonoid isn't zero |
From ClassFieldTheory
---
[](https://gitpod.io/from-referrer/)
|
t-algebra
CFT
label:t-algebra$ |
4/0 |
Mathlib/Algebra/GroupWithZero/NonZeroDivisors.lean |
1 |
1 |
['github-actions'] |
mattrobball assignee:mattrobball |
2-51650 2 days ago |
5-79584 5 days ago |
5-79561 5 days |
| 32442 |
joelriou author:joelriou |
feat(CategoryTheory/Localization): inverse in `SmallShiftedHom` |
The post/precomposition on the types `SmallShiftedHom W` with a morphism which satisfies `W` is a bijection.
---
[](https://gitpod.io/from-referrer/)
|
t-category-theory |
109/0 |
Mathlib/CategoryTheory/Localization/SmallShiftedHom.lean |
1 |
1 |
['github-actions'] |
thorimur assignee:thorimur |
2-51649 2 days ago |
5-62011 5 days ago |
5-61987 5 days |
| 32443 |
vihdzp author:vihdzp |
feat: `SuccOrder` and `PredOrder` instances for `SignType` |
Used in the CGT repo.
---
A future to-do might be to pull out `SuccOrder` and `PredOrder` into a `Defs` file, so that this can be defined within the `Defs` file as well.
[](https://gitpod.io/from-referrer/)
|
t-data |
49/0 |
Mathlib.lean,Mathlib/Data/Sign/SuccPred.lean |
2 |
1 |
['github-actions'] |
pechersky assignee:pechersky |
2-51648 2 days ago |
5-61403 5 days ago |
5-61439 5 days |
| 32568 |
SnirBroshi author:SnirBroshi |
feat(Combinatorics/SimpleGraph/Acyclic): `IsAcyclic` -> `IsBipartite` |
This generalizes the existing `IsTree` -> `IsBipartite` result.
---
[](https://gitpod.io/from-referrer/)
|
t-combinatorics |
48/13 |
Mathlib/Combinatorics/SimpleGraph/Acyclic.lean,Mathlib/Combinatorics/SimpleGraph/Metric.lean |
2 |
2 |
['SnirBroshi', 'github-actions'] |
nobody |
2-46139 2 days ago |
2-48353 2 days ago |
2-48393 2 days |
| 32567 |
vihdzp author:vihdzp |
feat: `CompleteLinearOrder (Πₗ i, α i)` |
Used in the CGT repo.
---
[](https://gitpod.io/from-referrer/)
|
t-order |
195/9 |
Mathlib.lean,Mathlib/Order/CompleteLattice/PiLex.lean,Mathlib/Order/PiLex.lean |
3 |
8 |
['github-actions', 'plp127', 'vihdzp'] |
nobody |
2-44671 2 days ago |
2-48821 2 days ago |
2-48855 2 days |
| 32558 |
BoltonBailey author:BoltonBailey |
chore(RingTheory/MvPolynomial): weaken IsCancelMulZero to NoZeroDivisors |
... in assumptions of MonomialOrder and DegLex. Per [this](https://leanprover.zulipchat.com/#narrow/channel/116395-maths/topic/IsCancelMulZero.20and.20NoZeroDivisors.20for.20semirings/near/562327698) discussion, `NoZeroDivisors` is a strictly weaker assumption than `IsCancelMulZero`, so this should be a strict strengthening of these theorems.
---
[](https://gitpod.io/from-referrer/)
|
t-ring-theory |
19/14 |
Mathlib/RingTheory/MvPolynomial/MonomialOrder.lean,Mathlib/RingTheory/MvPolynomial/MonomialOrder/DegLex.lean |
2 |
1 |
['github-actions'] |
nobody |
2-37084 2 days ago |
2-65696 2 days ago |
2-65738 2 days |
| 32555 |
ksenono author:ksenono |
feat(Combinatorics/SimpleGraph/Matching): maximum and maximal matchings for Konig's theorem |
---
[](https://gitpod.io/from-referrer/)
|
t-combinatorics
new-contributor
|
40/0 |
Mathlib/Combinatorics/SimpleGraph/Matching.lean |
1 |
8 |
['SnirBroshi', 'github-actions', 'ksenono'] |
nobody |
2-34527 2 days ago |
2-67349 2 days ago |
2-67381 2 days |
| 32572 |
mcdoll author:mcdoll |
feat(Analysis/Calculus): norm bound for iterated derivatives of composition with CLM |
---
This is borderline trivial, but since `apply?` didn't give anything remotely useful, I think it is nice to have.
[](https://gitpod.io/from-referrer/)
|
|
16/5 |
Mathlib/Analysis/Calculus/ContDiff/Bounds.lean |
1 |
1 |
['github-actions'] |
nobody |
2-32709 2 days ago |
2-32865 2 days ago |
2-32840 2 days |
| 32464 |
YaelDillies author:YaelDillies |
feat: strengthen `pow_gcd_eq_one` |
From ClassFieldTheory
---
[](https://gitpod.io/from-referrer/)
|
t-algebra
CFT
label:t-algebra$ |
55/34 |
Mathlib/Data/Int/GCD.lean,Mathlib/Data/Int/Init.lean,Mathlib/GroupTheory/OrderOfElement.lean,Mathlib/GroupTheory/SpecificGroups/Cyclic.lean,Mathlib/RingTheory/RootsOfUnity/PrimitiveRoots.lean |
5 |
4 |
['YaelDillies', 'erdOne', 'github-actions', 'mathlib4-merge-conflict-bot'] |
nobody |
2-26596 2 days ago |
2-26606 2 days ago |
4-81472 4 days |
| 32045 |
xroblot author:xroblot |
chore(Trace/Quotient): move isomorphism to `Localization.AtPrime.Basic` |
This PR move isomorphisms previously defined in `Trace.Quotient` into `Localization.AtPrime.Basic`. The change is purely organizational: `Localization.AtPrime.Basic` is the canonical place for lemmas and constructions about localization at a prime. The isomorphisms are also renamed to match their new namespace:
- `equivQuotMaximalIdealOfIsLocalization` -> `IsLocalization.AtPrime.equivQuotMaximalIdeal`
- `quotMapEquivQuotMapMaximalIdealOfIsLocalization` -> `IsLocalization.AtPrime.equivQuotMapMaximalIdeal`
---
[](https://gitpod.io/from-referrer/)
|
t-ring-theory |
142/108 |
Mathlib/RingTheory/Localization/AtPrime/Basic.lean,Mathlib/RingTheory/Trace/Quotient.lean |
2 |
5 |
['erdOne', 'github-actions', 'xroblot'] |
mariainesdff assignee:mariainesdff |
2-22440 2 days ago |
2-22546 2 days ago |
6-33014 6 days |
| 30872 |
rudynicolop author:rudynicolop |
feat(Computability/NFA): NFA closure under concatenation |
This PR proves that regular languages are closed under concatenation via a direct construction on `NFA`s without `εNFA` nor ε-transitions. The main new definitions and results include:
- `M1.concat M2`, the concatenation of `NFA`s `M1` and `M2`, a direct construction without ε-transitions.
- Theorem `accepts_concat : (M1.concat M2).accepts = M1.accepts * M2.accepts`, showing the correctness of the construction.
- Theorem `IsRegular.mul`, showing that regular languages are closed under concatenation.
---
- [x] depends on: #31038
[](https://gitpod.io/from-referrer/)
|
new-contributor
t-computability
maintainer-merge
|
104/7 |
Mathlib/Computability/NFA.lean |
1 |
57 |
['YaelDillies', 'ctchou', 'github-actions', 'lambda-fairy', 'mathlib4-dependent-issues-bot', 'rudynicolop'] |
YaelDillies assignee:YaelDillies |
2-17966 2 days ago |
2-17967 2 days ago |
12-13281 12 days |
| 32273 |
jsm28 author:jsm28 |
feat(Analysis/Convex/Side): affine combinations on same / opposite side of face of a simplex as a vertex |
Build on #31205 by providing lemmas about when an affine combination of the vertices of a simplex is on the same / opposite side of a face (opposite a vertex) of the simplex as that vertex (a specific case of the lemmas from #31205 which involve two arbitrary affine combinations).
---
- [ ] depends on: #31205
[](https://gitpod.io/from-referrer/)
|
t-analysis
t-convex-geometry
|
62/0 |
Mathlib/Analysis/Convex/Side.lean |
1 |
3 |
['github-actions', 'mathlib4-dependent-issues-bot', 'mathlib4-merge-conflict-bot'] |
nobody |
2-13803 2 days ago |
2-13832 2 days ago |
2-21411 2 days |
| 31908 |
YaelDillies author:YaelDillies |
feat: Bernoulli random variables |
Define the product distribution of `p`-Bernoulli random variables a measure on `Set ι`.
It is important in applications to be able to restrict the product to a subset `u` of `ι`, eg in #31364 I define the `G(V, p)` distribution of binomial random graphs by setting `ι := Sym2 V` and `u := {e |¬ e.IsDiag}`.
---
- [x] depends on: #31909
- [x] depends on: #31911
- [x] depends on: #32096
- [x] depends on: #32287
[](https://gitpod.io/from-referrer/)
|
t-measure-probability |
149/7 |
Mathlib.lean,Mathlib/Probability/Distributions/Bernoulli.lean,Mathlib/Probability/HasLaw.lean |
3 |
5 |
['DavidLedvinka', 'github-actions', 'mathlib4-dependent-issues-bot', 'mathlib4-merge-conflict-bot', 'sgouezel'] |
sgouezel assignee:sgouezel |
2-7870 2 days ago |
7-46092 7 days ago |
12-75928 12 days |
| 30089 |
loefflerd author:loefflerd |
feat(NumberTheory/ModularForms): Bounds on modular forms and q-expansion coeffs |
Show that the q-expansion coefficients of a weight k modular form grow like `n ^ k`, and like `n ^ (k / 2)` for cusp forms.
---
This is a "blockbuster" PR from which many smaller chunks will be carved off for review and submission. The first in the series are the following:
- [x] depends on: #29743
- [x] depends on: #30475
- [x] depends on: #30461
- [ ] depends on: #30471
- [ ] depends on: #30512
- [ ] depends on: #30648
[](https://gitpod.io/from-referrer/)
|
WIP
blocked-by-other-PR
t-number-theory
large-import
|
943/94 |
Mathlib.lean,Mathlib/Analysis/Complex/CauchyIntegral.lean,Mathlib/NumberTheory/ModularForms/Basic.lean,Mathlib/NumberTheory/ModularForms/Bounds.lean,Mathlib/NumberTheory/ModularForms/Cusps.lean,Mathlib/NumberTheory/ModularForms/Identities.lean,Mathlib/NumberTheory/ModularForms/LevelOne.lean,Mathlib/NumberTheory/ModularForms/Petersson.lean,Mathlib/NumberTheory/ModularForms/QExpansion.lean,Mathlib/Topology/Algebra/Order/ArchimedeanDiscrete.lean |
10 |
n/a |
['github-actions', 'mathlib4-dependent-issues-bot', 'mathlib4-merge-conflict-bot'] |
nobody |
49-82086 1 month ago |
unknown |
unknown |
| 31092 |
FlAmmmmING author:FlAmmmmING |
feat(Algebra/Group/ForwardDiff.lean): Add theorem `sum_shift_eq_fwdDiff_iter`. |
---
[](https://gitpod.io/from-referrer/)
|
t-algebra
new-contributor
label:t-algebra$ |
21/1 |
Mathlib/Algebra/Group/ForwardDiff.lean |
1 |
13 |
['FlAmmmmING', 'Ruben-VandeVelde', 'dagurtomas', 'github-actions', 'mathlib4-merge-conflict-bot'] |
dagurtomas assignee:dagurtomas |
2-4526 2 days ago |
3-85743 3 days ago |
19-12024 19 days |
| 31579 |
xroblot author:xroblot |
feat(Data/Nat/Digits): prove the bijection induced by `Nat.ofDigits` and use it to compute the sum of the sum of digits |
We prove that `Nat.ofDigits` induces a bijection between the set of list of natural integers of length `l`
with coefficients `< b` and the set of natural integers `< b ^ l` and develop some API.
As a application, we prove that
```lean
theorem Nat.sum_digits_sum_eq {b : ℕ} (hb : 1 < b) (l : ℕ) :
∑ x ∈ Finset.range (b ^ l), (b.digits x).sum = l * b ^ (l - 1) * b.choose 2
```
---
|
t-data |
212/0 |
Mathlib/Data/Nat/Digits/Lemmas.lean |
1 |
12 |
['TwoFX', 'eric-wieser', 'github-actions', 'mathlib4-merge-conflict-bot', 'xroblot'] |
TwoFX assignee:TwoFX |
1-86228 1 day ago |
13-10107 13 days ago |
27-6605 27 days |
| 30678 |
YaelDillies author:YaelDillies |
refactor(Algebra/Quaternion): intermediate `Module` instance |
This `Module` instance allows me to not ungeneralise the `NoZeroSMulDivisors R ℍ[R,c₁,c₂,c₃]` in #30563.
---
[](https://gitpod.io/from-referrer/)
|
t-algebra label:t-algebra$ |
45/28 |
Mathlib/Algebra/Quaternion.lean |
1 |
25 |
['YaelDillies', 'eric-wieser', 'github-actions', 'jcommelin', 'kckennylau', 'leanprover-bot', 'leanprover-radar'] |
joneugster assignee:joneugster |
1-85300 1 day ago |
51-22604 1 month ago |
51-47341 51 days |
| 32403 |
FLDutchmann author:FLDutchmann |
fix(FieldSimp): `declaration has free variables` kernel errors |
Fix a bug in `field_simp` that produces a `(kernel) declaration has free variables '_example'` error which was caused by a misconfigured `simp` call.
---
The first new test produces this error on the current version of mathlib. What I believe is happening is that the discharger is using the `x != 0` hypothesis in the `then` branch, at which point that result is cached by `simp` and used in the `else` branch.
```
import Mathlib
/- (kernel) declaration has free variables '_example' -/
example {x y : ℚ}: (if x ≠ 0 then x / x else x / x) = 1 := by
field_simp
/- ⊢ (if x ≠ 0 then 1 else 1) = 1 -/
sorry
```
Edit: As @__JovanGerb__ pointed out, the correct solution was to set the `wellBehavedDischarge` flag to false, so that `simp` clears the cache more agressively. We might also want to turn on `contextual` in the future, but this would change the behaviour of `field_simp` by adding additional lemmas to the simp context. For now I propose a fix with a minimal change in behaviour.
Marking the simp context that calls the discharger as contextual appears to fix the issue, presumably by more aggressively pruning the cache. What I don't understand at this point, is why the discharger ever even had access to that hypothesis, given that contextual was set to false.
cc @JovanGerb : You understand the simp cache much better than I. Is there another bug here that I'm missing?
[](https://gitpod.io/from-referrer/)
|
t-meta |
52/14 |
Mathlib/Tactic/Abel.lean,Mathlib/Tactic/FieldSimp.lean,Mathlib/Tactic/Ring/RingNF.lean,Mathlib/Util/AtomM/Recurse.lean,MathlibTest/FieldSimp.lean |
5 |
7 |
['FLDutchmann', 'JovanGerb', 'github-actions', 'leanprover-radar'] |
kim-em assignee:kim-em |
1-84499 1 day ago |
6-2165 6 days ago |
6-82669 6 days |
| 27542 |
chrisflav author:chrisflav |
feat(RingTheory/KrullDimension): dimension of polynomial ring |
We show that for a Noetherian ring `R`, `dim R[X] = dim R + 1`.
Co-authored by: Sihan Su
Co-authored by: Yi Song
---
- [x] depends on: #27520
- [x] depends on: #27538
- [x] depends on: #27510
- [x] depends on: #32472
[](https://gitpod.io/from-referrer/)
|
large-import
t-ring-theory
|
123/0 |
Mathlib/Order/KrullDimension.lean,Mathlib/RingTheory/Ideal/Height.lean,Mathlib/RingTheory/KrullDimension/Polynomial.lean,Mathlib/RingTheory/Localization/AtPrime/Basic.lean |
4 |
n/a |
['github-actions', 'mathlib4-dependent-issues-bot', 'mathlib4-merge-conflict-bot'] |
nobody |
1-84477 1 day ago |
unknown |
unknown |
| 32202 |
joelriou author:joelriou |
feat(AlgebraicTopology): finite simplicial sets |
A simplicial set `X` is finite (`Simplicial.Finite`) if it has finitely many nondegenerate simplices. Equivalently, `X` is finite dimensional and the type of `n`-simplices of `X` is finite for any `n`.
---
- [x] depends on: #32201
[](https://gitpod.io/from-referrer/)
|
t-algebraic-topology |
150/1 |
Mathlib.lean,Mathlib/AlgebraicTopology/SimplicialSet/Finite.lean,Mathlib/AlgebraicTopology/SimplicialSet/StdSimplex.lean |
3 |
3 |
['github-actions', 'mathlib4-dependent-issues-bot', 'mathlib4-merge-conflict-bot'] |
nobody |
1-83704 1 day ago |
1-83704 1 day ago |
2-259 2 days |
| 32535 |
joelriou author:joelriou |
feat(CategoryTheory): the opposite of a triangulated category is triangulated |
---
[](https://gitpod.io/from-referrer/)
|
t-category-theory |
210/3 |
Mathlib.lean,Mathlib/CategoryTheory/Shift/Basic.lean,Mathlib/CategoryTheory/Triangulated/Opposite/Basic.lean,Mathlib/CategoryTheory/Triangulated/Opposite/Pretriangulated.lean,Mathlib/CategoryTheory/Triangulated/Opposite/Triangulated.lean,Mathlib/CategoryTheory/Triangulated/Pretriangulated.lean |
6 |
1 |
['github-actions'] |
nobody |
1-81254 1 day ago |
3-9956 3 days ago |
3-9933 3 days |
| 32590 |
sgouezel author:sgouezel |
feat: use `IsCompletelyPseudometrizable` class in measure regularity statements |
The new statements are slightly stronger than the old ones because they don't require the uniform structure to be given.
---
[](https://gitpod.io/from-referrer/)
|
|
37/59 |
Mathlib/MeasureTheory/Measure/RegularityCompacts.lean,Mathlib/Topology/Metrizable/Basic.lean |
2 |
1 |
['github-actions'] |
nobody |
1-79806 1 day ago |
1-82196 1 day ago |
1-82171 1 day |
| 32593 |
fpvandoorn author:fpvandoorn |
doc: refer between AEMeasurable and NullMeasurable |
---
[](https://gitpod.io/from-referrer/)
|
t-measure-probability |
8/2 |
Mathlib/MeasureTheory/Measure/MeasureSpaceDef.lean,Mathlib/MeasureTheory/Measure/NullMeasurable.lean |
2 |
1 |
['github-actions'] |
nobody |
1-77505 1 day ago |
1-77510 1 day ago |
1-77547 1 day |
| 32596 |
erdOne author:erdOne |
feat(RingTheory): localization commutes with integral closure |
---
[](https://gitpod.io/from-referrer/)
|
t-ring-theory |
126/1 |
Mathlib/Algebra/Polynomial/Reverse.lean,Mathlib/RingTheory/Localization/Integral.lean |
2 |
1 |
['github-actions'] |
nobody |
1-67895 1 day ago |
1-67895 1 day ago |
1-75636 1 day |
| 32562 |
YaelDillies author:YaelDillies |
chore(Data/Finsupp): rename the `toFun` projection to `apply` in `simps` |
This is the standard name for fun-like types.
---
[](https://gitpod.io/from-referrer/)
|
t-data |
20/37 |
Counterexamples/CliffordAlgebraNotInjective.lean,Mathlib/Algebra/Group/Finsupp.lean,Mathlib/Algebra/Polynomial/Derivative.lean,Mathlib/Data/Finsupp/Basic.lean,Mathlib/Data/Finsupp/Defs.lean,Mathlib/Data/Finsupp/Interval.lean,Mathlib/Data/Finsupp/Weight.lean,Mathlib/LinearAlgebra/Dual/Basis.lean,Mathlib/RingTheory/AlgebraTower.lean,Mathlib/RingTheory/Flat/EquationalCriterion.lean,Mathlib/RingTheory/HahnSeries/HEval.lean |
11 |
2 |
['github-actions', 'mathlib4-merge-conflict-bot'] |
nobody |
1-67270 1 day ago |
1-67270 1 day ago |
2-50009 2 days |
| 32160 |
SnirBroshi author:SnirBroshi |
feat(Combinatorics/SimpleGraph/Walks): helper theorems about `darts` and `support` |
---
[](https://gitpod.io/from-referrer/)
|
t-combinatorics |
39/1 |
Mathlib/Combinatorics/SimpleGraph/Walks/Basic.lean,Mathlib/Combinatorics/SimpleGraph/Walks/Traversal.lean |
2 |
1 |
['github-actions'] |
kmill assignee:kmill |
1-57250 1 day ago |
13-49277 13 days ago |
13-49310 13 days |
| 32611 |
tb65536 author:tb65536 |
feat(FieldTheory/Galois/IsGaloisGroup): add `IsGaloisGroup.finite` |
This PR adds `IsGaloisGroup.finite`, a companion lemma to `IsGaloisGroup.finiteDimensional` just above.
---
[](https://gitpod.io/from-referrer/)
|
t-algebra label:t-algebra$ |
3/0 |
Mathlib/FieldTheory/Galois/IsGaloisGroup.lean |
1 |
1 |
['github-actions'] |
nobody |
1-54675 1 day ago |
1-54675 1 day ago |
1-54651 1 day |
| 30112 |
gaetanserre author:gaetanserre |
feat(Probability.Kernel): add representation of kernel as a map of a uniform measure |
Add results about isolation of kernels randomness. In particular, it shows that one
can write a Markov kernel as the map by a deterministic of a uniform measure on `[0, 1]`.
It corresponds to Lemma 4.22 in "[Foundations of Modern Probability](https://link.springer.com/book/10.1007/978-3-030-61871-1)" by Olav Kallenberg, 2021.
---
[](https://gitpod.io/from-referrer/)
|
t-measure-probability |
149/0 |
Mathlib.lean,Mathlib/Probability/Kernel/Representation.lean |
2 |
4 |
['RemyDegenne', 'gaetanserre', 'github-actions', 'mathlib4-merge-conflict-bot'] |
sgouezel assignee:sgouezel |
1-51664 1 day ago |
2-12652 2 days ago |
2-12943 2 days |
| 31013 |
vihdzp author:vihdzp |
chore: deprecate `AsLinearOrder` |
This goes back to Lean 3 (https://github.com/leanprover-community/mathlib3/pull/4037). It was used to prove two results about "linearly ordered lattices" [`le_sup_iff`](https://leanprover-community.github.io/mathlib4_docs/Mathlib/Order/Lattice.html#le_sup_iff) and [`inf_le_iff`](https://leanprover-community.github.io/mathlib4_docs/Mathlib/Order/Lattice.html#inf_le_iff) which have long since been turned into theorems on linear orders. The proper way to deal with a totally ordered partial order is to just write a `LinearOrder` instance, so there is no need for this.
---
See some brief [Zulip](https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/AsLinearOrder/near/547525036) discussion.
[](https://gitpod.io/from-referrer/)
|
t-order |
7/5 |
Mathlib/Order/Basic.lean |
1 |
2 |
['github-actions', 'j-loreaux', 'urkud'] |
bryangingechen assignee:bryangingechen |
1-51662 1 day ago |
5-25592 5 days ago |
5-28865 5 days |
| 31873 |
wwylele author:wwylele |
refactor: re-prove Euler's partition theorem from Glaisher's theorem |
Less code to maintain is good. I hope the authors of the original proof are fine with this...
---
- [ ] depends on: #30618
[](https://gitpod.io/from-referrer/)
|
file-removed |
24/390 |
Archive.lean,Archive/Wiedijk100Theorems/Partition.lean,Mathlib/Combinatorics/Enumerative/Partition/Basic.lean,Mathlib/Combinatorics/Enumerative/Partition/Glaisher.lean,docs/100.yaml,docs/1000.yaml |
6 |
3 |
['github-actions', 'mathlib4-dependent-issues-bot', 'mathlib4-merge-conflict-bot'] |
dagurtomas assignee:dagurtomas |
1-51660 1 day ago |
4-61844 4 days ago |
4-62429 4 days |
| 31984 |
kim-em author:kim-em |
feat: definition of `ConvexSpace` |
Trying to get the ball rolling the notion of a space with convex combinations, I suggest:
```
class ConvexSpace (R : Type u) (M : Type v)
[PartialOrder R] [Semiring R] [IsStrictOrderedRing R] where
/-- Take a convex combination of a family of points with the given probability distribution. -/
convexCombination {ι : Type v} (f : FiniteProbability R ι) (xs : ι → M) : M
/-- Associativity of convex combination. -/
assoc
{κ : Type v} (f₀ : FiniteProbability R κ)
{ι : κ → Type v} (f₁ : (k : κ) → FiniteProbability R (ι k))
(xs : (k : κ) → (ι k) → M) :
convexCombination f₀ (fun m => convexCombination (f₁ m) (xs m)) =
convexCombination (f₀.comp f₁) (fun ⟨k, i⟩ => xs k i)
/-- A convex combination of a single point is that point. -/
single {ι : Type v} (i : ι) (x : M) : convexCombination (.single i) (fun _ => x) = x
/-- Convex combinations are determined by the points with non-zero weights. -/
-- Perhaps this follows from `assoc`, but I don't see how.
ext {ι : Type v} (f : FiniteProbability R ι) (xs xs' : ι → M)
(h : ∀ i, i ∈ f.support → xs i = xs' i) : convexCombination f xs = convexCombination f xs'
```
where
```
structure FiniteProbability (R : Type u) [LE R] [AddCommMonoid R] [One R] (ι : Type v)
extends weights : ι →₀ R where
/-- All weights are non-negative. -/
nonneg : ∀ m, 0 ≤ weights m
/-- The weights sum to 1. -/
total : weights.sum (fun _ r => r) = 1
```
The file also contains some TODOs for next steps. |
t-algebra label:t-algebra$ |
142/0 |
Mathlib.lean,Mathlib/LinearAlgebra/ConvexSpace.lean |
2 |
22 |
['ADedecker', 'github-actions', 'kim-em', 'plp127'] |
pechersky assignee:pechersky |
1-51659 1 day ago |
17-42587 17 days ago |
17-42625 17 days |
| 32444 |
vihdzp author:vihdzp |
feat: `SignType` is a complete linear order |
---
[](https://gitpod.io/from-referrer/)
|
t-order
t-data
|
38/17 |
Mathlib.lean,Mathlib/Analysis/Convex/Between.lean,Mathlib/Data/Sign/Basic.lean,Mathlib/Data/Sign/Order.lean |
4 |
5 |
['github-actions', 'ocfnash', 'vihdzp'] |
pechersky assignee:pechersky |
1-51656 1 day ago |
4-65853 4 days ago |
5-34388 5 days |
| 32455 |
vihdzp author:vihdzp |
feat: order topologies of successor orders |
---
Co-authored by @j-loreaux
[](https://gitpod.io/from-referrer/)
|
t-topology
t-order
|
124/43 |
Mathlib.lean,Mathlib/Order/Cover.lean,Mathlib/SetTheory/Ordinal/Topology.lean,Mathlib/Topology/Order/SuccPred.lean |
4 |
1 |
['github-actions'] |
pechersky assignee:pechersky |
1-51655 1 day ago |
5-38970 5 days ago |
5-38960 5 days |
| 32469 |
joelriou author:joelriou |
feat(CategoryTheory): right Bousfield localization |
This PR dualises definitions and basic results about `ObjectProperty.isLocal` and `MorphismProperty.isLocal`. The dual definitions are named `ObjectProperty.isColocal` and `MorphismProperty.isColocal`.
---
[](https://gitpod.io/from-referrer/)
|
t-category-theory |
221/12 |
Mathlib/CategoryTheory/Localization/Adjunction.lean,Mathlib/CategoryTheory/Localization/Bousfield.lean,Mathlib/CategoryTheory/Localization/Opposite.lean,Mathlib/CategoryTheory/MorphismProperty/Basic.lean,Mathlib/CategoryTheory/ObjectProperty/Local.lean,Mathlib/CategoryTheory/Triangulated/Orthogonal.lean |
6 |
1 |
['github-actions'] |
riccardobrasca assignee:riccardobrasca |
1-51654 1 day ago |
5-9474 5 days ago |
5-9498 5 days |
| 31449 |
kim-em author:kim-em |
feat(SemilocallySimplyConnected): definition and alternative formulation |
Note: Proofs in this PR were developed with assistance from Claude. |
|
114/0 |
Mathlib.lean,Mathlib/AlgebraicTopology/FundamentalGroupoid/SemilocallySimplyConnected.lean,Mathlib/Topology/Path.lean |
3 |
4 |
['ADedecker', 'github-actions', 'kim-em', 'mathlib4-merge-conflict-bot'] |
ADedecker assignee:ADedecker |
1-49444 1 day ago |
1-49444 1 day ago |
22-45512 22 days |
| 31141 |
peabrainiac author:peabrainiac |
feat(Analysis/Calculus): parametric integrals over smooth functions are smooth |
Show that for any smooth function `f : H × ℝ → E`, the parametric integral `fun x ↦ ∫ t in a..b, f (x, t) ∂μ` is smooth too.
The argument proceeds inductively, using the fact that derivatives of parametric integrals can themselves be computed as parametric integrals. The necessary lemmas on derivatives of parametric integrals already existed, but took some work to apply due to their generality; we state some convenient special cases.
---
- [x] depends on: #31077
[](https://gitpod.io/from-referrer/)
|
t-analysis |
202/5 |
Mathlib/Analysis/Calculus/ParametricIntegral.lean,Mathlib/Analysis/Calculus/ParametricIntervalIntegral.lean,Mathlib/MeasureTheory/Integral/DominatedConvergence.lean,Mathlib/MeasureTheory/Integral/IntegrableOn.lean |
4 |
11 |
['github-actions', 'mathlib4-dependent-issues-bot', 'mathlib4-merge-conflict-bot', 'peabrainiac', 'sgouezel'] |
sgouezel assignee:sgouezel |
1-46581 1 day ago |
1-46581 1 day ago |
13-30361 13 days |
| 28604 |
alreadydone author:alreadydone |
chore(Algebra/Ring/Defs): add two classes (minimally invasive version) |
Add the missing `NonAssocComm(Semi)ring` classes and add some missing instances between existing classes. Contrary to #28532, the approach here doesn't add any new `extends`.
---
[](https://gitpod.io/from-referrer/)
|
t-algebra label:t-algebra$ |
57/17 |
Mathlib/Algebra/Colimit/DirectLimit.lean,Mathlib/Algebra/Ring/Defs.lean |
2 |
30 |
['alreadydone', 'github-actions', 'j-loreaux', 'kckennylau', 'leanprover-bot', 'leanprover-community-mathlib4-bot', 'leanprover-radar', 'riccardobrasca'] |
riccardobrasca assignee:riccardobrasca |
1-38692 1 day ago |
1-38692 1 day ago |
62-31882 62 days |
| 30116 |
FormulaRabbit81 author:FormulaRabbit81 |
feat(MeasureTheory): a relatively compact set of measures is tight |
---
[](https://gitpod.io/from-referrer/)
|
t-measure-probability
large-import
|
181/6 |
Mathlib/MeasureTheory/Measure/Tight.lean |
1 |
20 |
['EtienneC30', 'FormulaRabbit81', 'github-actions', 'mathlib4-merge-conflict-bot'] |
RemyDegenne assignee:RemyDegenne |
1-38652 1 day ago |
1-59532 1 day ago |
61-38262 61 days |
| 32617 |
erdOne author:erdOne |
feat(RingTheory): field extension over perfect fields are smooth |
---
[](https://gitpod.io/from-referrer/)
|
t-ring-theory |
149/18 |
Mathlib.lean,Mathlib/FieldTheory/IntermediateField/Adjoin/Algebra.lean,Mathlib/FieldTheory/IntermediateField/Adjoin/Defs.lean,Mathlib/FieldTheory/SeparableClosure.lean,Mathlib/FieldTheory/SeparablyGenerated.lean,Mathlib/RingTheory/EssentialFiniteness.lean,Mathlib/RingTheory/Smooth/Field.lean |
7 |
1 |
['github-actions'] |
nobody |
1-38141 1 day ago |
1-38141 1 day ago |
1-40761 1 day |
| 32440 |
thorimur author:thorimur |
feat: make the `unusedDecidableInType` linter fire when `Decidable*` instances are used only inside of proofs in the type |
This PR adjusts the `unusedDecidableInType` to prevent false negatives on declarations that only use `Decidable*` hypotheses in proofs that appear in the type. That is, the linter now fires when the `Decidable*` linter is unused outside of proofs.
This PR also changes the warning message to be more direct, and indicates when the instance appears only in a proof (vs. not appearing at all).
We exempt some deprecated lemmas in `Mathlib.Analysis.Order.Matrix` which the linter now fires on. (Presumably, most prior violations had been cleaned up by #10235, which also detected such lemmas.)
Note that this took some tinkering to achieve sufficient performance. We use the following novel(?) "dolorous telescope" strategy (so named due to introducing `sorry`s) to avoid traversing the whole type:
- when encountering an instance binder of concern, telescope to create an fvar.
- when encountering any other binder, instantiate it with `sorry`.
- as we proceed, collect the free variables from these expressions which do not appear in proofs. Since the instances of concern are the only free variables, free variable collection avoids traversing many subexpressions by checking for `hasFVar`, which is a computed field accessible in constant time.
Perhaps surprisingly, this is (on net) more performant than using `eraseProofs` and then detecting dependence via bvars.
We also implement an `Expr`-level early exit for most types by checking if they bind any instance of concern first. (This adds a very small overhead to types which *do* have an instance of concern, but the check is very fast.)
This also adds a profiler category to this linter.
Note: we still have yet to optimize (pre)-infotree traversal performance, and have yet to avoid proofs that appear in the value of definitions. However, this PR sets us up to do so.
---
## Notes on performance
You might be wondering if this *is* actually a faster strategy, seeing as the bench is quite noisy. To determine this, I made a copy of the linter which I could vary without rebuilding mathlib, and profiled the relevant component locally on all imported declarations in Mathlib by linting the `eoi` token:
```lean
module
public meta import Lean
public import Mathlib.Tactic.Linter.UnusedInstancesInTypeCopy
import all Mathlib.Tactic.Linter.UnusedInstancesInTypeCopy
open Lean Meta Elab Term Command Mathlib.Linter.UnusedInstancesInType
meta section
local instance : Insert Name NameSet where
insert := fun n s => s.insert n
def runCopy : Linter where run stx := do
if stx.isOfKind ``Parser.Command.eoi then
let opts := (← getOptions).setBool `profiler true
let consts := (← getEnv).constants.map₁
-- The following expose private decls in their types, so break `MetaM` methods:
let badRecs : NameSet := {`IO.Promise.casesOn, `IO.Promise.recOn, `IO.Promise.rec}
profileitM Exception "control" opts do
for (n,_) in consts do
liftTermElabM do unless n.isInternalDetail || badRecs.contains n do pure ()
profileitM Exception "bench" opts do
for (n,cinfo) in consts do
unless n.isInternalDetail || badRecs.contains n do
cinfo.toConstantVal.onUnusedInstancesInTypeWhere isDecidableVariant
fun _ _ => pure ()
initialize addLinter runCopy
```
(This could have been done in a `run_cmd`, but I wanted to replicate the circumstances of linting as closely as possible, just in case it introduced mysterious async effects.)
Then, in a separate file, I imported `Mathlib` and the above linter, and cycled through reading out the result and editing the underlying component then rebuilding. The control was reliably ~1.07-1.12s. The different strategies came out as follows (the following values are not averaged, but are representative):
| | without early exit | with early exit |
| ---: | :---: | :---: |
| `eraseProofs` | 97.4s | 6.82s |
| dolorous telescope | 20.3s | 3.99s |
As you can see, the early exit cuts the absolute value (and therefore the absolute difference) down dramatically. But seeing as this lays the groundwork for linting defs and will be used for more linters (with wider scopes, and less early exit opportunities), I think we should opt for the more performant version even though there's some extra complexity. :)
[](https://gitpod.io/from-referrer/)
|
t-linter |
199/51 |
Mathlib/Analysis/Matrix/Order.lean,Mathlib/Lean/Expr/Basic.lean,Mathlib/Tactic/Linter/UnusedInstancesInType.lean,MathlibTest/UnusedInstancesInType.lean |
4 |
28 |
['github-actions', 'leanprover-radar', 'thorimur'] |
nobody |
1-38086 1 day ago |
1-38086 1 day ago |
4-69368 4 days |
| 26212 |
Thmoas-Guan author:Thmoas-Guan |
feat(Algebra): the Rees theorem for depth |
In this PR we proved the Rees theorem for depth.
Co-authored-by: Hu Yongle
---
- [x] depends on: #27416
[](https://gitpod.io/from-referrer/)
|
t-algebra
large-import
label:t-algebra$ |
233/15 |
Mathlib/RingTheory/Regular/Category.lean,Mathlib/RingTheory/Regular/Depth.lean |
2 |
n/a |
['Thmoas-Guan', 'erdOne', 'github-actions', 'mathlib4-dependent-issues-bot', 'mathlib4-merge-conflict-bot'] |
nobody |
1-31772 1 day ago |
unknown |
unknown |
| 32604 |
YaelDillies author:YaelDillies |
chore(Algebra/MonoidAlgebra): reduce dependence on defeq abuse, golf |
This is crucial for #25273.
---
[](https://gitpod.io/from-referrer/)
|
t-algebra label:t-algebra$ |
72/133 |
Mathlib/Algebra/MonoidAlgebra/Basic.lean,Mathlib/Algebra/MonoidAlgebra/Defs.lean,Mathlib/Algebra/MonoidAlgebra/Degree.lean,Mathlib/Algebra/MonoidAlgebra/Ideal.lean,Mathlib/Algebra/MonoidAlgebra/Support.lean,Mathlib/Algebra/MonoidAlgebra/ToDirectSum.lean,Mathlib/Algebra/Polynomial/Basic.lean,Mathlib/Algebra/Polynomial/Degree/CardPowDegree.lean,Mathlib/Algebra/Polynomial/Degree/Definitions.lean,Mathlib/Algebra/Polynomial/Laurent.lean |
10 |
5 |
['YaelDillies', 'erdOne', 'github-actions', 'grunweg', 'leanprover-radar'] |
nobody |
1-30148 1 day ago |
1-67945 1 day ago |
1-67922 1 day |
| 29687 |
vihdzp author:vihdzp |
feat: standard part in non-Archimedean field |
We define `ArchimedeanClass.standardPart x` as the unique real number with an infinitesimal difference from `x`. This generalizes `Hyperreal.st` for a general (non-)archimedean field.
---
- [x] depends on: #29611
- [x] depends on: #29685
- [x] depends on: #29735
- [x] depends on: #30486
- [x] depends on: #32212
[](https://gitpod.io/from-referrer/)
|
t-algebra label:t-algebra$ |
324/2 |
Mathlib.lean,Mathlib/Algebra/Order/CompleteField.lean,Mathlib/Algebra/Order/Ring/Archimedean.lean,Mathlib/Data/Real/StandardPart.lean,Mathlib/Order/Quotient.lean |
5 |
23 |
['github-actions', 'mathlib4-dependent-issues-bot', 'mathlib4-merge-conflict-bot', 'plp127', 'vihdzp', 'wwylele'] |
joneugster assignee:joneugster |
1-28148 1 day ago |
5-41808 5 days ago |
7-80239 7 days |
| 32461 |
joelriou author:joelriou |
feat(Algebra/Homology): more API for the HomComplex from a single cochain complex |
---
[](https://gitpod.io/from-referrer/)
|
t-category-theory
t-algebra
large-import
label:t-algebra$ |
98/3 |
Mathlib/Algebra/Homology/HomotopyCategory/HomComplex.lean,Mathlib/Algebra/Homology/HomotopyCategory/HomComplexCohomology.lean,Mathlib/Algebra/Homology/HomotopyCategory/HomComplexSingle.lean |
3 |
1 |
['github-actions'] |
joneugster assignee:joneugster |
1-15132 1 day ago |
5-27527 5 days ago |
5-27572 5 days |
| 32591 |
YaelDillies author:YaelDillies |
chore(Algebra/MonoidAlgebra): scope `Algebra R[M] A[M]` instance |
It is currently local, but then the Prop-valued instances about it are not and therefore bring the (non-)instance back from the dead.
---
[](https://gitpod.io/from-referrer/)
|
t-algebra label:t-algebra$ |
11/5 |
Mathlib/Algebra/MonoidAlgebra/Basic.lean,Mathlib/RingTheory/TensorProduct/MonoidAlgebra.lean |
2 |
1 |
['github-actions'] |
nobody |
1-12064 1 day ago |
1-12064 1 day ago |
1-81210 1 day |
| 32645 |
vihdzp author:vihdzp |
feat(SetTheory/Cardinal): formulas for `sum (fun n : ℕ ↦ x ^ n)` |
---
[](https://gitpod.io/from-referrer/)
|
t-set-theory |
23/5 |
Mathlib/SetTheory/Cardinal/Arithmetic.lean,Mathlib/SetTheory/Cardinal/Basic.lean,Mathlib/SetTheory/Cardinal/Defs.lean |
3 |
1 |
['github-actions'] |
nobody |
1-11118 1 day ago |
1-13530 1 day ago |
1-13575 1 day |
| 31595 |
astrainfinita author:astrainfinita |
chore: redefine `Ideal.IsPrime` |
Redefine `Ideal.IsPrime` to make it correct for non-commutative cases
---
[](https://gitpod.io/from-referrer/)
|
t-algebra label:t-algebra$ |
225/91 |
Mathlib/Algebra/Order/Ring/Ordering/Defs.lean,Mathlib/AlgebraicGeometry/StructureSheaf.lean,Mathlib/RingTheory/DedekindDomain/Ideal/Lemmas.lean,Mathlib/RingTheory/GradedAlgebra/Radical.lean,Mathlib/RingTheory/Ideal/AssociatedPrime/Basic.lean,Mathlib/RingTheory/Ideal/IsPrimary.lean,Mathlib/RingTheory/Ideal/Maps.lean,Mathlib/RingTheory/Ideal/Maximal.lean,Mathlib/RingTheory/Ideal/Oka.lean,Mathlib/RingTheory/Ideal/Operations.lean,Mathlib/RingTheory/Ideal/Over.lean,Mathlib/RingTheory/Ideal/Pointwise.lean,Mathlib/RingTheory/Ideal/Prime.lean,Mathlib/RingTheory/Ideal/Prod.lean,Mathlib/RingTheory/Ideal/Quotient/Basic.lean,Mathlib/RingTheory/Ideal/Quotient/Operations.lean,Mathlib/RingTheory/Localization/AtPrime/Basic.lean,Mathlib/RingTheory/Localization/Ideal.lean,Mathlib/RingTheory/Polynomial/Basic.lean,Mathlib/RingTheory/PrincipalIdealDomain.lean,Mathlib/RingTheory/Spectrum/Prime/Topology.lean,Mathlib/RingTheory/Valuation/Basic.lean |
22 |
18 |
['alreadydone', 'astrainfinita', 'github-actions', 'leanprover-bot', 'leanprover-community-mathlib4-bot', 'mathlib4-merge-conflict-bot'] |
alreadydone assignee:alreadydone |
1-9574 1 day ago |
1-19621 1 day ago |
8-19084 8 days |
| 32437 |
WenrongZou author:WenrongZou |
feat(Algebra/Category/ModuleCat/Sheaf/Quasicoherent): construction of `Presentation` |
We construct presentation of sheaf of module by sequence and add `Presentation.map`.
This contribution was created as part of the Heidelberg Lean workshop "Formalising algebraic geometry" in November 2025.
Co-authored-by: William Coram @WilliamCoram
Co-authored-by: Andrew Yang @erdOne
---
[](https://gitpod.io/from-referrer/)
|
t-algebra
new-contributor
label:t-algebra$ |
87/0 |
Mathlib/Algebra/Category/ModuleCat/Sheaf/Quasicoherent.lean |
1 |
12 |
['WenrongZou', 'github-actions', 'robin-carlier'] |
nobody |
1-3825 1 day ago |
1-4791 1 day ago |
1-72230 1 day |
| 32116 |
LessnessRandomness author:LessnessRandomness |
feat(Geometry/Euclidean/Angle/Unoriented/TriangleInequality): Add criterion for equality case |
The PR fills `proof_wanted` in the file `TriangleInequality.lean` (criterion for equality in the triangle inequality for angles).
---
- [ ] depends on: #32100
[](https://gitpod.io/from-referrer/)
|
t-euclidean-geometry |
137/33 |
Mathlib/Geometry/Euclidean/Angle/Unoriented/TriangleInequality.lean |
1 |
25 |
['JovanGerb', 'LessnessRandomness', 'github-actions', 'mathlib4-dependent-issues-bot', 'mathlib4-merge-conflict-bot', 'themathqueen'] |
jsm28 assignee:jsm28 |
1-785 1 day ago |
12-12363 12 days ago |
12-17372 12 days |
| 32651 |
harahu author:harahu |
doc(Probability/Martingale): fix typos |
This PR fixes presumed typos. Changes are as follows:
- Clarify the martingale_condExp result statement to match its actual signature (μ[f | ℱ i]).
- Rephrase the upcrossings lemma to state “finite number of upcrossings,” aligning wording with the assumption ≠ ∞.
- Fix the L¹ inequality in the proof sketch by removing a spurious norm bar.
- Correct the Markov bound and tail estimate to use 𝔼|h|, consistent with the definition f_n := 𝔼[h | ℱ_n].
- Close a missing bracket in 𝔼[· | ℱ_n] for readability in the conditional expectation identity.
---
Potential typos found and fixed by Codex. Although these fixes all seem correct to me, they are non-trivial enough that I feel like asking for careful review here.
[](https://gitpod.io/from-referrer/)
|
t-measure-probability |
6/6 |
Mathlib/Probability/Martingale/Basic.lean,Mathlib/Probability/Martingale/Convergence.lean |
2 |
1 |
['github-actions'] |
nobody |
0-84526 23 hours ago |
1-1960 1 day ago |
1-1996 1 day |
| 32618 |
dagurtomas author:dagurtomas |
feat(CategoryTheory): combine pullback cones in the functor category |
---
[](https://gitpod.io/from-referrer/)
|
t-category-theory |
71/5 |
Mathlib/CategoryTheory/Limits/FunctorCategory/Shapes/Pullbacks.lean,Mathlib/CategoryTheory/Limits/Shapes/Pullback/Cospan.lean |
2 |
4 |
['github-actions', 'joelriou', 'leanprover-radar'] |
nobody |
0-81706 22 hours ago |
0-81819 22 hours ago |
1-32440 1 day |
| 31757 |
mcdoll author:mcdoll |
feat(Analysis/Distribution): definition of tempered distributions |
Define the space of tempered distributions as an abbreviation. We also prove the abstract convergence results
for `PointwiseConvergenceCLM` and define the Fourier transform on tempered distributions.
There is a bit of disagreement in the literature about which is the correct topology on tempered distributions. For practical reasons, we will use the pointwise topology, but we might switch later to the bounded topology, if the abstract functional analysis is developed enough to prove the same statements.
---
- [x] depends on: #31756
- [x] depends on: #31577
- [x] depends on: #31760
[](https://gitpod.io/from-referrer/)
|
t-analysis |
225/9 |
Mathlib.lean,Mathlib/Analysis/Distribution/TemperedDistribution.lean,Mathlib/Analysis/LocallyConvex/PointwiseConvergence.lean,Mathlib/Topology/Algebra/Module/PointwiseConvergence.lean,docs/overview.yaml,docs/undergrad.yaml |
6 |
6 |
['ADedecker', 'github-actions', 'mathlib4-dependent-issues-bot', 'mathlib4-merge-conflict-bot', 'mcdoll'] |
nobody |
6-62352 6 days ago |
8-53741 8 days ago |
8-53724 8 days |
| 32654 |
YaelDillies author:YaelDillies |
feat(Combinatorics): a clique has size at most the chromatic number |
There already exists a version of this lemma for cliques given by a set, but it's impractical to provide an explicit clique on an explicit graph as a set, rather than an indexed family, especially because computing the size of the set would then involve proving that it is the range of an injective function, even though being a clique already implies being injective!
Application: google-deepmind/formal-conjectures#1369
From FormalConjectures
---
[](https://gitpod.io/from-referrer/)
|
t-combinatorics |
42/30 |
Mathlib/Combinatorics/SimpleGraph/Basic.lean,Mathlib/Combinatorics/SimpleGraph/Coloring.lean |
2 |
1 |
['github-actions'] |
nobody |
0-77696 21 hours ago |
0-78724 21 hours ago |
0-78758 21 hours |
| 31954 |
wwylele author:wwylele |
feat(Counterexamples): Weierstrass function is continuous and nowhere differentiable |
---
- [x] depends on: #31970
- [x] depends on: #31971
- [x] depends on: #31973
- [x] depends on: #31977
- [x] depends on: #31982
- [x] depends on: #32082
- [x] depends on: #32079
[](https://gitpod.io/from-referrer/)
|
t-analysis |
311/0 |
Counterexamples.lean,Counterexamples/Weierstrass.lean,docs/references.bib |
3 |
3 |
['SnirBroshi', 'github-actions', 'mathlib4-dependent-issues-bot', 'wwylele'] |
nobody |
0-74581 20 hours ago |
2-71261 2 days ago |
3-38514 3 days |
| 32657 |
mattrobball author:mattrobball |
chore: clean up imports from #31746 |
#31746 added `Data.Int.Cast.Lemmas` as a new import to `LinearAlgebra.Matrix.Diagonal` to access `Int.cast_ite` but did not remove `Data.Int.Cast.Basic` and did not do a public import. Following `Nat.cast_ite`, we move `Data.Int.Cast.Basic` and remove the added import.
---
[](https://gitpod.io/from-referrer/)
|
t-data |
8/8 |
Mathlib/Data/Int/Cast/Basic.lean,Mathlib/Data/Int/Cast/Lemmas.lean,Mathlib/Data/Matrix/Diagonal.lean |
3 |
1 |
['github-actions'] |
nobody |
0-73692 20 hours ago |
0-73869 20 hours ago |
0-73913 20 hours |
| 30576 |
smmercuri author:smmercuri |
feat: `adicCompletion` for `Rat` is uniform isomorphic to `Padic` |
---
- [x] depends on: #30133
- [x] depends on: #30574
- [x] depends on: #30363
- [x] depends on: #30171
- [ ] depends on: #31845
[](https://gitpod.io/from-referrer/)
|
|
306/6 |
Mathlib.lean,Mathlib/NumberTheory/Padics/HeightOneSpectrum.lean,Mathlib/RingTheory/DedekindDomain/Ideal/Lemmas.lean,Mathlib/Topology/Algebra/Algebra/Equiv.lean,Mathlib/Topology/Algebra/UniformRing.lean,Mathlib/Topology/Algebra/Valued/WithVal.lean |
6 |
5 |
['github-actions', 'mathlib4-dependent-issues-bot', 'mathlib4-merge-conflict-bot'] |
nobody |
0-71318 19 hours ago |
0-71321 19 hours ago |
0-71306 19 hours |
| 31133 |
thorimur author:thorimur |
feat(Linter): combinators for linter option boilerplate |
Provides simple combinators `whenLinterOption` and `whenNotLinterOption` to parallel `whenPPOption` and `whenNotPPOption`, and bundles `withSetOptionIn` and `whenLinterOption` into `whenLinterActivated`.
Currently, a typical linter action uses
```lean
run := withSetOptionIn fun stx => do
unless getLinterValue linter.foo (← getLinterOptions) do
return
...
```
This allows us to simply write
```lean
run := whenLinterActivated linter.foo fun stx => do
...
```
Using these combinators in Mathlib's linters is left to a subsequent PR (#31134).
Since this is a utility used in basic linters, including the header linter, we exclude it from `lint-style`.
---
I'm not sure I'm doing the right thing here re: Mathlib.Init. What exactly should happen?
[](https://gitpod.io/from-referrer/)
|
t-meta
t-linter
|
73/1 |
Mathlib.lean,Mathlib/Lean/Linter.lean,scripts/lint-style.lean |
3 |
12 |
['Vierkantor', 'adomani', 'github-actions', 'mathlib4-merge-conflict-bot', 'thorimur'] |
adomani assignee:adomani |
0-70966 19 hours ago |
0-70987 19 hours ago |
31-21727 31 days |
| 32584 |
CBirkbeck author:CBirkbeck |
feat(NumberTheory/EisensteinSeries/E2): Define the Eisenstein series E2 |
We define the Eisenstein series E2 and prove some basic results which will be needed in #32585 to prove how it transforms under the slash action of SL2.
---
[](https://gitpod.io/from-referrer/)
|
t-number-theory |
262/0 |
Mathlib.lean,Mathlib/NumberTheory/ModularForms/EisensteinSeries/E2/Defs.lean,Mathlib/NumberTheory/ModularForms/EisensteinSeries/E2/Summable.lean |
3 |
2 |
['github-actions', 'loefflerd'] |
nobody |
0-70511 19 hours ago |
1-66751 1 day ago |
1-72446 1 day |
| 26923 |
oliver-butterley author:oliver-butterley |
feat(Dynamics/BirkhoffSum): add the pointwise ergodic theorem (Birkhoff's) |
The Pointwise Ergodic Theorem, also known as Birkhoff's Ergodic Theorem.
Co-authored-by: Lua Viana Reis
- [x] depends on: #26074
- [x] depends on: #26807
- [x] depends on: #26810
- [x] depends on: #26840
- [x] depends on: #26842
- [x] depends on: #26848
- [x] depends on: #26851
- [x] depends on: #26852
- [x] depends on: #26853
- [x] depends on: #27008
- [x] depends on: #28901
Zulip: [PR thread](https://leanprover.zulipchat.com/#narrow/channel/144837-PR-reviews/topic/.2326923.20The.20pointwise.20ergodic.20theorem.20.28Birkhoff's.29/with/527835158)
---
[](https://gitpod.io/from-referrer/)
|
merge-conflict
t-dynamics
new-contributor
|
401/0 |
Mathlib.lean,Mathlib/Dynamics/BirkhoffSum/Pointwise.lean |
2 |
14 |
['D-Thomine', 'github-actions', 'leanprover-community-bot-assistant', 'lua-vr', 'mathlib4-dependent-issues-bot', 'mathlib4-merge-conflict-bot'] |
urkud assignee:urkud |
21-26996 21 days ago |
21-26997 21 days ago |
91-66923 91 days |
| 32259 |
jsm28 author:jsm28 |
feat(Analysis/SpecialFunctions/Trigonometric/Angle): `toReal` addition lemmas |
Add two lemmas
```lean
lemma toReal_add_eq_toReal_add_toReal {θ ψ : Angle} (hθ : θ ≠ π) (hψ : ψ ≠ π)
(hs : θ.sign ≠ ψ.sign ∨ θ.sign = (θ + ψ).sign) : (θ + ψ).toReal = θ.toReal + ψ.toReal := by
```
```lean
lemma abs_toReal_add_eq_two_pi_sub_abs_toReal_add_abs_toReal {θ ψ : Angle} (hs : θ.sign = ψ.sign)
(hsa : θ.sign ≠ (θ + ψ).sign) : |(θ + ψ).toReal| = 2 * π - (|θ.toReal| + |ψ.toReal|) := by
```
about `(θ + ψ).toReal`. Also add a lemma `abs_toReal_neg` used in proving them, and lemmas `sign_two_nsmul_eq_neg_sign_iff` and `sign_two_zsmul_eq_neg_sign_iff` (analogous to existing `sign_two_nsmul_eq_sign_iff` and `sign_two_zsmul_eq_sign_iff`) that are of use together with the `toReal` lemmas in relating oriented and unoriented angle bisection results.
---
Feel free to golf.
---
[](https://gitpod.io/from-referrer/)
|
t-analysis |
111/0 |
Mathlib/Analysis/SpecialFunctions/Trigonometric/Angle.lean |
1 |
4 |
['github-actions', 'j-loreaux', 'jsm28'] |
j-loreaux assignee:j-loreaux |
0-67433 18 hours ago |
0-67434 18 hours ago |
10-39921 10 days |
| 32360 |
YuvalFilmus author:YuvalFilmus |
feat(Chebyshev): degree, leadingCoeff, eval_neg |
Calculated the degree and leading coefficients of Chebyshev T and U, as well as formulas for T(-x) and U(-x).
---
[](https://gitpod.io/from-referrer/)
|
new-contributor
t-ring-theory
|
153/2 |
Mathlib/RingTheory/Polynomial/Chebyshev.lean |
1 |
7 |
['LLaurance', 'YuvalFilmus', 'github-actions'] |
kbuzzard assignee:kbuzzard |
0-67066 18 hours ago |
1-68959 1 day ago |
5-63945 5 days |
| 32281 |
ajirving author:ajirving |
feat(NumberTheory.Chebyshev): prove connection between prime counting and theta |
Uses Abel summation to express the prime counting function in terms of the Chebyshev theta function. This upstreams some results from PrimeNumberTheoremAnd.
---
- [x] depends on: #32247
[](https://gitpod.io/from-referrer/)
|
t-number-theory
new-contributor
large-import
|
225/0 |
Mathlib/NumberTheory/Chebyshev.lean |
1 |
5 |
['ajirving', 'github-actions', 'mathlib4-dependent-issues-bot', 'mathlib4-merge-conflict-bot'] |
nobody |
0-66509 18 hours ago |
0-78019 21 hours ago |
0-79799 22 hours |
| 30640 |
SnirBroshi author:SnirBroshi |
feat(Combinatorics/SimpleGraph/Acyclic): define `reachabilitySet` + a maximally acyclic graph is a tree |
Define `reachabilitySet` as the set of all pairs that have a walk between them.
`reachabilitySet` is to `Reachable` what `edgeSet` is to `Adj` (both related by `Sym2.fromRel`).
Prove that a graph is maximally acyclic iff it is a tree.
---
The motivation for the set is making it easier to work with definitions that require `Sym2 V`, such as `IsBridge` and `deleteEdges` (see `isBridge_iff_mem_edgeSet_and_notMem_reachabilitySet_deleteEdges` and `mem_edgeSet_and_mem_reachabilitySet_deleteEdges_iff_exists_isCycle_and_mem_edges` at the bottom).
- [x] depends on: #30542
- [x] depends on: #30570
[](https://gitpod.io/from-referrer/)
|
|
101/0 |
Mathlib/Combinatorics/SimpleGraph/Acyclic.lean,Mathlib/Combinatorics/SimpleGraph/Connectivity/Connected.lean |
2 |
3 |
['github-actions', 'mathlib4-dependent-issues-bot', 'mathlib4-merge-conflict-bot'] |
nobody |
0-66180 18 hours ago |
1-30291 1 day ago |
1-30892 1 day |
| 32600 |
PrParadoxy author:PrParadoxy |
feat(LinearAlgebra/Multilinear): composition of multilinear maps |
The composition of a multilinear map with a family of multilinear maps
is a multilinear map indexed by a dependent sum.
The result reduces to a lemma about the interaction of function
application, `Sigma.curry`, and `Function.update`. This variant of
`Function.apply_update` is included as `Sigma.apply_curry_update`.
---
Note to reviewers: If `apply_curry_update` is deemed too specialized for
the `Sigma` namespace, it could be included as a private lemma. An
optimized signature would obviate the need to work around a `DecidableEq`
diamond, and would reduce `map_update_add', map_update_mul'` to a single
`simp` call each.
[](https://gitpod.io/from-referrer/)
|
new-contributor |
40/0 |
Mathlib/Data/Sigma/Basic.lean,Mathlib/LinearAlgebra/Multilinear/Basic.lean |
2 |
3 |
['github-actions', 'kbuzzard'] |
nobody |
0-63686 17 hours ago |
0-75523 20 hours ago |
0-75787 21 hours |
| 32660 |
dagurtomas author:dagurtomas |
feat(Topology): sandwich lemmas for profinite sets |
We add two lemmas:
- `exists_clopen_of_closed_subset_open`: in a totally disconnected compact Hausdorff space `X`, if `Z ⊆ U` are subsets with `Z` closed and `U` open, there exists a clopen `C` with `Z ⊆ C ⊆ U`.
- `exists_clopen_partition_of_clopen_cover`: Let `X` be a totally disconnected compact Hausdorff space, `D i ⊆ X` a finite family of clopens, and `Z i ⊆ D i` closed. Assume that the `Z i` are pairwise disjoint. Then there exist clopens `Z i ⊆ C i ⊆ D i` with the `C i` disjoint, and such that `∪ D i ⊆ ∪ C i`.
These are required to prove injectivity of light profinite sets, see #31754
---
[](https://gitpod.io/from-referrer/)
|
t-topology |
94/0 |
Mathlib/Topology/Separation/Profinite.lean |
1 |
1 |
['github-actions'] |
nobody |
0-62995 17 hours ago |
0-63251 17 hours ago |
0-63288 17 hours |
| 32297 |
mcdoll author:mcdoll |
feat(Analysis/Distribution): composition of temperate growth functions |
Proves that the composition of temperate growth functions is again of temperate growth. We have to use the explicit bounds, because we want to have the case that the outer function `g` is only temperate on the image of the inner function `f`, to be able to apply this result for `f x = 1 + |x|^2` and `g x = x ^ r` for any real `r`.
---
[](https://gitpod.io/from-referrer/)
|
t-analysis |
91/1 |
Mathlib/Analysis/Distribution/SchwartzSpace.lean,Mathlib/Analysis/Distribution/TemperateGrowth.lean |
2 |
1 |
['github-actions'] |
nobody |
9-4783 9 days ago |
9-5015 9 days ago |
9-11762 9 days |
| 26831 |
AntoineChambert-Loir author:AntoineChambert-Loir |
feat(GroupTheory/SpecificGroups/Alternating/MaximalSubgroups): maximal subgroups of the alternating group |
This proves the first case (intransitive) of the O'Nan-Scott classification of maximal subgroups of the alternating group.
---
- [x] depends on: #26457
- [x] depends on: #26282
- [x] depends on: #26281
- [x] depends on: #26280
- [x] depends on: #26279
[](https://gitpod.io/from-referrer/)
|
t-group-theory |
522/20 |
Mathlib.lean,Mathlib/GroupTheory/GroupAction/MultiplePrimitivity.lean,Mathlib/GroupTheory/GroupAction/MultipleTransitivity.lean,Mathlib/GroupTheory/Perm/MaximalSubgroups.lean,Mathlib/GroupTheory/SpecificGroups/Alternating.lean,Mathlib/GroupTheory/SpecificGroups/Alternating/MaximalSubgroups.lean |
6 |
n/a |
['AntoineChambert-Loir', 'adomani', 'github-actions', 'leanprover-community-bot-assistant', 'mathlib4-dependent-issues-bot', 'mathlib4-merge-conflict-bot', 'tb65536'] |
tb65536 assignee:tb65536 |
0-58054 16 hours ago |
unknown |
unknown |
| 32665 |
erdOne author:erdOne |
feat(RingTheory): quasi-finite algebras |
---
[](https://gitpod.io/from-referrer/)
|
t-ring-theory |
341/2 |
Mathlib.lean,Mathlib/RingTheory/LocalRing/ResidueField/Ideal.lean,Mathlib/RingTheory/QuasiFinite/Basic.lean |
3 |
1 |
['github-actions'] |
nobody |
0-57008 15 hours ago |
0-57088 15 hours ago |
0-57111 15 hours |
| 30988 |
erdOne author:erdOne |
feat(AlgebraicGeometry): descending affine cover of an inverse limit |
---
[](https://gitpod.io/from-referrer/)
|
t-algebraic-geometry
large-import
|
350/35 |
Mathlib/Algebra/Category/Ring/Constructions.lean,Mathlib/AlgebraicGeometry/AffineTransitionLimit.lean,Mathlib/AlgebraicGeometry/Gluing.lean,Mathlib/AlgebraicGeometry/Morphisms/IsIso.lean,Mathlib/AlgebraicGeometry/Pullbacks.lean,Mathlib/AlgebraicGeometry/QuasiAffine.lean,Mathlib/AlgebraicGeometry/Sites/MorphismProperty.lean,Mathlib/Topology/LocalAtTarget.lean |
8 |
32 |
['chrisflav', 'erdOne', 'github-actions', 'mathlib4-merge-conflict-bot'] |
chrisflav assignee:chrisflav |
0-54286 15 hours ago |
0-54294 15 hours ago |
42-7214 42 days |
| 29948 |
mcdoll author:mcdoll |
feat(Analysis/Fourier): the Fourier transform on `L^2` |
We define the Fourier transform on L^2 as a linear isometry by extension of Schwartz functions.
The file is called `LpSpace` since we will extend the Fourier transform to L^p later on.
---
- [x] depends on: #29888
- [x] depends on: #29860
- [x] depends on: #31074
- [x] depends on: #31076
- [x] depends on: #31079
- [x] depends on: #32566
- [x] depends on: #32565
[](https://gitpod.io/from-referrer/)
|
t-analysis |
94/1 |
Mathlib.lean,Mathlib/Analysis/Distribution/SchwartzSpace.lean,Mathlib/Analysis/Fourier/LpSpace.lean,docs/undergrad.yaml |
4 |
4 |
['github-actions', 'mathlib4-dependent-issues-bot', 'mathlib4-merge-conflict-bot'] |
grunweg assignee:grunweg |
0-52839 14 hours ago |
0-52949 14 hours ago |
6-6661 6 days |
| 27378 |
peakpoint author:peakpoint |
refactor(Geometry/Euclidean/Projection): redefine projection and reflection for affine subspaces |
This PR continues the work from #25578.
Original PR: https://github.com/leanprover-community/mathlib4/pull/25578
- [x] depends on: #31395 |
t-euclidean-geometry
new-contributor
|
265/320 |
Mathlib/Geometry/Euclidean/Circumcenter.lean,Mathlib/Geometry/Euclidean/Projection.lean |
2 |
11 |
['github-actions', 'jsm28', 'leanprover-community-bot-assistant', 'mathlib4-dependent-issues-bot', 'mathlib4-merge-conflict-bot', 'peakpoint'] |
jsm28 assignee:jsm28 |
0-51659 14 hours ago |
0-61628 17 hours ago |
16-6427 16 days |
| 31138 |
AntoineChambert-Loir author:AntoineChambert-Loir |
feat(LinearAlgebra/Transvection): the determinant of transvection in a module is equal to 1 |
Proof that the determinant of a transvection is equal to 1.
The proof goes by showing that the determinant of `LinearMap.transvection f v` is `1 + f v` (even if `f v` is nonzero).
I first treat the case of a field, distinguishing whether `f v = 0` (so that we get
a transvection) or not (so that we have a dilation).
Then, by base change to the field of fractions, I can handle the case of a domain. Finally, the general case is treated by base change from the “universal case” where the base ring is the ring of polynomials in $$2n$$ indeterminates corresponding to the coefficients of $$f$$ and $$v$$.
---
- [ ] depends on: #31164
- [ ] depends on: #31165
- [ ] depends on: #30987
- [ ] depends on: #31078
- [ ] depends on: #31162
[](https://gitpod.io/from-referrer/)
|
blocked-by-other-PR
t-algebra
large-import
label:t-algebra$ |
595/26 |
Mathlib/Algebra/Polynomial/RingDivision.lean,Mathlib/LinearAlgebra/Determinant.lean,Mathlib/LinearAlgebra/DirectSum/Finsupp.lean,Mathlib/LinearAlgebra/Finsupp/LinearCombination.lean,Mathlib/LinearAlgebra/SpecialLinearGroup.lean,Mathlib/LinearAlgebra/Transvection.lean,Mathlib/RingTheory/TensorProduct/IsBaseChangeFree.lean,Mathlib/RingTheory/TensorProduct/IsBaseChangeHom.lean |
8 |
9 |
['github-actions', 'mathlib4-dependent-issues-bot', 'mathlib4-merge-conflict-bot', 'ocfnash'] |
nobody |
7-78511 7 days ago |
8-23718 8 days ago |
0-26 26 seconds |
| 31495 |
jsm28 author:jsm28 |
feat(Geometry/Euclidean/Sphere/SecondInter): `secondInter` and sides of faces of a simplex |
Add lemmas that, if you take a simplex with one vertex on a sphere and the others on or inside it (typically, a triangle and its circumcircle), and take a line through the given vertex and a point in the interior of the simplex or the interior of the opposite face, the second intersection of that line with the sphere lies on the opposite side (from the vertex) of the face opposite that vertex.
---
- [ ] depends on: #31451
- [ ] depends on: #31452
[](https://gitpod.io/from-referrer/)
|
t-euclidean-geometry |
52/0 |
Mathlib/Geometry/Euclidean/Sphere/SecondInter.lean |
1 |
3 |
['github-actions', 'mathlib4-dependent-issues-bot', 'mathlib4-merge-conflict-bot'] |
JovanGerb assignee:JovanGerb |
0-51656 14 hours ago |
4-51150 4 days ago |
4-51461 4 days |
| 31560 |
AntoineChambert-Loir author:AntoineChambert-Loir |
feat(Topology/Sion): the minimax theorem of von Neumann - Sion |
Prove `Sion.exists_isSaddlePointOn` :
Let X and Y be convex subsets of topological vector spaces E and F,
X being moreover compact,
and let f : X × Y → ℝ be a function such that
- for all x, f(x, ⬝) is upper semicontinuous and quasiconcave
- for all y, f(⬝, y) is lower semicontinuous and quasiconvex
Then inf_x sup_y f(x,y) = sup_y inf_x f(x,y).
The classical case of the theorem assumes that f is continuous,
f(x, ⬝) is concave, f(⬝, y) is convex.
As a particular case, one get the von Neumann theorem where
f is bilinear and E, F are finite dimensional.
We follow the proof of Komiya (1988).
## Remark on implementation
* The essential part of the proof holds for a function
`f : X → Y → β`, where `β` is a complete dense linear order.
* We have written part of it for just a dense linear order,
* On the other hand, if the theorem holds for such `β`,
it must hold for any linear order, for the reason that
any linear order embeds into a complete dense linear order.
However, this result does not seem to be known to Mathlib.
* When `β` is `ℝ`, one can use `Real.toEReal` and one gets a proof for `ℝ`.
## TODO
Give particular important cases (eg, bilinear maps in finite dimension).
Co-authored with @ADedecker
---
- [ ] depends on: #31548
- [ ] depends on: #31547
- [ ] depends on: #31558
[](https://gitpod.io/from-referrer/)
|
blocked-by-other-PR |
847/1 |
Mathlib.lean,Mathlib/Data/EReal/Basic.lean,Mathlib/Topology/Compactness/Compact.lean,Mathlib/Topology/Semicontinuous.lean,Mathlib/Topology/Sion.lean,Mathlib/Topology/Sublevel.lean,docs/references.bib |
7 |
4 |
['github-actions', 'mathlib4-dependent-issues-bot', 'mathlib4-merge-conflict-bot'] |
nobody |
10-85852 10 days ago |
11-871 11 days ago |
0-536 8 minutes |
| 31711 |
joelriou author:joelriou |
feat(CategoryTheory/Sites): the category structure on the points of a site |
---
- [x] depends on: #31708
- [x] depends on: #31710
- [x] depends on: #31859
[](https://gitpod.io/from-referrer/)
|
t-category-theory |
157/3 |
Mathlib.lean,Mathlib/CategoryTheory/Sites/Point/Basic.lean,Mathlib/CategoryTheory/Sites/Point/Category.lean,docs/references.bib |
4 |
5 |
['github-actions', 'joelriou', 'mathlib4-dependent-issues-bot', 'mathlib4-merge-conflict-bot', 'robin-carlier'] |
nobody |
4-20270 4 days ago |
4-20297 4 days ago |
6-12214 6 days |
| 32242 |
vihdzp author:vihdzp |
feat: missing instances for `OrderDual`/`Lex`/`Colex` |
---
The `Nonempty` and `Inhabited` instances for `OrderDual` exist in `Order.Basic` already.
[](https://gitpod.io/from-referrer/)
|
t-order |
12/14 |
Mathlib/Order/Synonym.lean |
1 |
2 |
['github-actions', 'mathlib4-merge-conflict-bot'] |
pechersky assignee:pechersky |
0-51652 14 hours ago |
3-63629 3 days ago |
6-33171 6 days |
| 32345 |
joelriou author:joelriou |
feat(AlgebraicTopology): relative morphisms of simplicial sets |
Given two simplicial sets `X` and `Y`, and subcomplexes `A` of `X`, and `B` of `Y`, we introduce a type `RelativeMorphism A B φ` of morphisms `X ⟶ Y` which induce a given morphism of simplicial sets `A ⟶ B`. We define homotopies between these relative morphisms and introduce the quotient type of homotopy classes.
(Homotopy groups of Kan complexes will be defined as a particular case of this construction.)
From https://github.com/joelriou/topcat-model-category
---
[](https://gitpod.io/from-referrer/)
|
t-algebraic-topology |
230/1 |
Mathlib.lean,Mathlib/AlgebraicTopology/SimplicialSet/Monoidal.lean,Mathlib/AlgebraicTopology/SimplicialSet/RelativeMorphism.lean,Mathlib/AlgebraicTopology/SimplicialSet/Subcomplex.lean |
4 |
4 |
['github-actions', 'joelriou', 'robin-carlier'] |
robin-carlier assignee:robin-carlier |
0-51649 14 hours ago |
4-20689 4 days ago |
7-49021 7 days |
| 32373 |
erdOne author:erdOne |
feat(Analysis): `HasFPowerSeriesOnBall (fun x ↦ 1 / (1 - x))` and friends |
---
[](https://gitpod.io/from-referrer/)
|
t-analysis |
160/4 |
Mathlib/Analysis/Analytic/Binomial.lean,Mathlib/Analysis/Analytic/OfScalars.lean |
2 |
10 |
['erdOne', 'github-actions', 'ocfnash'] |
j-loreaux assignee:j-loreaux |
0-51649 14 hours ago |
0-60013 16 hours ago |
3-36604 3 days |
| 32423 |
joelriou author:joelriou |
feat(CategoryTheory): more preservation properties of functors |
We consider the preservation of a limit or a colimit as an `ObjectProperty` in the category of functors.
---
[](https://gitpod.io/from-referrer/)
|
t-category-theory |
80/1 |
Mathlib/CategoryTheory/ObjectProperty/FunctorCategory/PreservesLimits.lean |
1 |
3 |
['github-actions', 'joelriou', 'robin-carlier'] |
nobody |
4-21541 4 days ago |
4-21602 4 days ago |
5-47901 5 days |
| 32424 |
joelriou author:joelriou |
feat(CategoryTheory): the Yoneda embedding for a locally small category |
Let `C` be a locally `w`-small category. We define the Yoneda embedding `shrinkYoneda : C ⥤ Cᵒᵖ ⥤ Type w`.
---
[](https://gitpod.io/from-referrer/)
|
t-category-theory |
143/4 |
Mathlib.lean,Mathlib/CategoryTheory/ShrinkYoneda.lean,Mathlib/CategoryTheory/Yoneda.lean |
3 |
7 |
['github-actions', 'joelriou', 'robin-carlier'] |
thorimur assignee:thorimur |
0-51647 14 hours ago |
4-20941 4 days ago |
5-45975 5 days |
| 32493 |
euprunin author:euprunin |
feat(Algebra/Group/Action): add `grind` annotation for `smul_eq_mul` |
---
Note that the lemma being annotated is
1. already actively used with `grind` via explicit `grind [lemma]` invocations in Mathlib, and
2. already tagged with `@[simp]`.
---
[](https://gitpod.io/from-referrer/)
|
|
4/4 |
Mathlib/Algebra/Group/Action/Defs.lean,Mathlib/Analysis/Calculus/LogDeriv.lean,Mathlib/NumberTheory/ModularForms/EisensteinSeries/QExpansion.lean,Mathlib/NumberTheory/ModularForms/QExpansion.lean |
4 |
3 |
['euprunin', 'github-actions', 'leanprover-radar'] |
alexjbest assignee:alexjbest |
0-51646 14 hours ago |
4-59777 4 days ago |
4-59752 4 days |
| 32513 |
euprunin author:euprunin |
feat(Algebra/Polynomial): add `grind` annotations for `C_mul_monomial` and `monomial_mul_C` |
---
Note that the lemma being annotated is
1. already actively used with `grind` via explicit `grind [lemma]` invocations in Mathlib, and
2. already tagged with `@[simp]`.
---
[](https://gitpod.io/from-referrer/)
|
t-algebra label:t-algebra$ |
4/4 |
Mathlib/Algebra/Polynomial/Basic.lean,Mathlib/Algebra/Polynomial/RuleOfSigns.lean |
2 |
3 |
['euprunin', 'github-actions', 'leanprover-radar'] |
nobody |
3-77311 3 days ago |
3-79618 3 days ago |
3-79659 3 days |
| 32515 |
joelriou author:joelriou |
feat(CategoryTheory): monomorphisms in Type are stable under coproducts |
We develop the API regarding colimit cofans in the category of types, and we apply it in order to show that monomorphisms are stable under coproducts in the category of types.
From https://github.com/joelriou/topcat-model-category
---
[](https://gitpod.io/from-referrer/)
|
t-category-theory |
196/3 |
Mathlib/CategoryTheory/Limits/Shapes/Products.lean,Mathlib/CategoryTheory/Limits/Types/ColimitType.lean,Mathlib/CategoryTheory/Limits/Types/Coproducts.lean,Mathlib/CategoryTheory/Types/Monomorphisms.lean |
4 |
2 |
['github-actions', 'joelriou'] |
dagurtomas assignee:dagurtomas |
0-51644 14 hours ago |
3-71317 3 days ago |
3-71293 3 days |
| 32526 |
PrParadoxy author:PrParadoxy |
chore(LinearAlgebra/Multilinear/Basic.lean): remove `erw`s in `restr` |
---
[](https://gitpod.io/from-referrer/)
|
t-algebra
new-contributor
label:t-algebra$ |
6/9 |
Mathlib/LinearAlgebra/Multilinear/Basic.lean |
1 |
1 |
['github-actions'] |
joelriou assignee:joelriou |
0-51643 14 hours ago |
3-53213 3 days ago |
3-53250 3 days |
| 32118 |
alreadydone author:alreadydone |
feat(Algebra): prerequisites for #31919 |
+ Extract a lemma `exists_aeval_invOf_eq_zero_of_ideal_map_adjoin_add_span_eq_top` that was used in the proof of [stacks#00IB](https://stacks.math.columbia.edu/tag/00IB) and are used to prove both parts of [stacks#090P](https://stacks.math.columbia.edu/tag/090P)
+ Add lemmas on units in a submonoid of a DivisionMonoid/Group(WithZero)
+ Add instances for `integralClosure` and API for integrally closed subrings
+ Add a lemma on `trailingCoeff` of polynomials
+ Fix a statement in `local_hom_TFAE` and rename to `isLocalHom_tfae`
+ Unify the instances `Algebra.ofSubsemiring` and `Algebra.ofSubring`
+ Move `NonUnitalSub(semi)ringClass` instance on `Ideal` to from Ideal/Operations to Defs
+ Upgrade `ValuationSubring.nonunits` from `Subsemigroup` to `NonUnitalSubring`
---
[](https://gitpod.io/from-referrer/)
|
t-algebra
t-ring-theory
label:t-algebra$ |
161/39 |
Mathlib/Algebra/Algebra/Basic.lean,Mathlib/Algebra/Polynomial/Degree/TrailingDegree.lean,Mathlib/NumberTheory/Padics/PadicIntegers.lean,Mathlib/RingTheory/Ideal/Nonunits.lean,Mathlib/RingTheory/IntegralClosure/IntegrallyClosed.lean,Mathlib/RingTheory/LocalRing/LocalSubring.lean,Mathlib/RingTheory/LocalRing/RingHom/Basic.lean,Mathlib/RingTheory/Polynomial/Basic.lean,Mathlib/RingTheory/Polynomial/Ideal.lean,Mathlib/RingTheory/Valuation/AlgebraInstances.lean,Mathlib/RingTheory/Valuation/Integers.lean,Mathlib/RingTheory/Valuation/ValuationSubring.lean |
12 |
37 |
['alreadydone', 'erdOne', 'github-actions', 'jcommelin', 'leanprover-bot', 'leanprover-community-mathlib4-bot', 'leanprover-radar'] |
nobody |
0-51586 14 hours ago |
1-62004 1 day ago |
6-61227 6 days |
| 32597 |
thorimur author:thorimur |
chore: ignore autoparam declarations in private module linter |
Autogenerated declarations for the syntax of autoparams never start with `_private`, and thus are in some sense always public. We manually exclude them from the class of public declarations here.
Note that something like `isInternalDetail` is too strong; that would also exclude public declarations generated by `initialize`, which ought to be considered bona-fide public declarations.
We add `@[expose] public section` to `Mathlib.Analysis.Normed.Lp.SmoothApprox`.
---
[](https://gitpod.io/from-referrer/)
|
t-linter |
31/3 |
Mathlib/Analysis/Normed/Lp/SmoothApprox.lean,Mathlib/Tactic/Linter/PrivateModule.lean,MathlibTest/PrivateModuleLinter/initialize.lean |
3 |
7 |
['github-actions', 'grunweg', 'thorimur'] |
nobody |
0-51031 14 hours ago |
1-38393 1 day ago |
1-39120 1 day |
| 32603 |
themathqueen author:themathqueen |
chore: add deprecated file and clean up imports in another |
Follow-up to #28100.
---
[](https://gitpod.io/from-referrer/)
|
t-algebra label:t-algebra$ |
10/5 |
Mathlib.lean,Mathlib/Algebra/Azumaya/Basic.lean,Mathlib/LinearAlgebra/GeneralLinearGroup.lean |
3 |
1 |
['github-actions'] |
nobody |
0-50742 14 hours ago |
1-69086 1 day ago |
1-69379 1 day |
| 32570 |
ksenono author:ksenono |
feat(Combinatorics/SimpleGraph): bipartite subgraphs and vertex-disjoint graphs for Konig's theorem |
---
[](https://gitpod.io/from-referrer/)
|
t-combinatorics
new-contributor
|
21/0 |
Mathlib/Combinatorics/SimpleGraph/Bipartite.lean,Mathlib/Combinatorics/SimpleGraph/Subgraph.lean |
2 |
10 |
['SnirBroshi', 'github-actions'] |
nobody |
0-50608 14 hours ago |
2-44148 2 days ago |
2-44191 2 days |
| 32552 |
ksenono author:ksenono |
feat(SetTheory/Cardinal): helpers for Konig's theorem |
---
[](https://gitpod.io/from-referrer/)
|
new-contributor
t-set-theory
|
64/0 |
Mathlib/SetTheory/Cardinal/Arithmetic.lean,Mathlib/SetTheory/Cardinal/Basic.lean |
2 |
24 |
['github-actions', 'ksenono', 'staroperator', 'vihdzp'] |
nobody |
0-46013 12 hours ago |
2-68627 2 days ago |
2-68669 2 days |
| 12695 |
chrisflav author:chrisflav |
feat(RingTheory/Smooth): smooth algebras are flat |
We show that smooth ring homomorphisms are flat. The strategy for a smooth `A`-algebra `B` is the following:
- first we find a model of `B` over a Noetherian base ring
- if `A` is Noetherian, we identify `B` as a retract of the adic completion of a polynomial ring over `A`, which is flat
This is the summary PR which will be split in several parts.
Co-authored-by: Judith Ludwig
---
- [x] depends on: #32064
- [x] depends on: #25143
[](https://gitpod.io/from-referrer/)
|
maintainer-merge
t-ring-theory
|
10/2 |
Mathlib/RingTheory/Smooth/Flat.lean |
1 |
3 |
['erdOne', 'github-actions', 'mathlib4-dependent-issues-bot'] |
nobody |
0-45848 12 hours ago |
0-45848 12 hours ago |
0-65656 18 hours |
| 32582 |
metakunt author:metakunt |
feat(Data/Finset): Add card_filter_add_card_filter_not |
Adds card_filter_add_card_filter_not and cleans up misuse of neg.
Filter.neg has a different meaning https://leanprover-community.github.io/mathlib4_docs/Mathlib/Order/Filter/Pointwise.html#Filter.instNeg |
new-contributor |
19/8 |
Mathlib/Algebra/BigOperators/Group/Finset/Basic.lean,Mathlib/Combinatorics/SetFamily/Compression/Down.lean,Mathlib/Combinatorics/SetFamily/Compression/UV.lean,Mathlib/Combinatorics/SetFamily/KruskalKatona.lean,Mathlib/Data/Finset/Basic.lean,Mathlib/Data/Finset/Card.lean,Mathlib/Data/Finset/Density.lean,Mathlib/Data/Finset/Prod.lean |
8 |
1 |
['github-actions'] |
nobody |
0-42085 11 hours ago |
2-15291 2 days ago |
2-15277 2 days |
| 32668 |
kim-em author:kim-em |
feat(TacticAnalysis): copy args when replacing linarith with grind |
This PR modifies `grindReplacementWith` to accept an `extractArgs` function that can extract term arguments from the original tactic syntax. When arguments are found, they are converted to `grindParam` syntax and included in the replacement `grind` call. Further, if an argument is a global identifier, we wrap it in `id` to ensure `grind` interprets it as a term (rather than trying to find a trigger pattern).
This makes the regression linter more useful - instead of just trying `grind`, it now tries `grind [X, Y]` when the original was `linarith [X, Y]`.
Example output before:
```
fail_if_success grind
linarith [Finset.mem_antidiagonal.mp hij, Real.pi_pos]
```
Example output after:
```
fail_if_success grind [Finset.mem_antidiagonal.mp hij, id Real.pi_pos]
linarith [Finset.mem_antidiagonal.mp hij, Real.pi_pos]
```
🤖 Prepared with Claude Code |
t-meta |
57/1 |
Mathlib/Tactic/TacticAnalysis/Declarations.lean |
1 |
1 |
['github-actions'] |
nobody |
0-39043 10 hours ago |
0-44179 12 hours ago |
0-44212 12 hours |
| 32252 |
ajirving author:ajirving |
feat(NumberTheory/Chebyshev): prove relationship between psi and theta |
Proves the relationship between the Chebyshev psi and theta functions; psi is a sum of theta evaluated at powers of x. This upstreams a result from the PrimeNumberTheoremAnd project.
---
- [x] depends on: #32247
[](https://gitpod.io/from-referrer/)
|
t-number-theory
new-contributor
large-import
|
155/2 |
Mathlib/NumberTheory/Chebyshev.lean |
1 |
10 |
['ajirving', 'erdOne', 'github-actions', 'mathlib4-dependent-issues-bot', 'mathlib4-merge-conflict-bot'] |
nobody |
0-36403 10 hours ago |
3-7108 3 days ago |
5-15964 5 days |
| 32357 |
YuvalFilmus author:YuvalFilmus |
feat(Polynomial/Roots): add a theorem for computing roots |
The theorem `roots_eq_of_degree` shows that S is the set of roots of a degree d polynomial P if #S = d and P(x) = 0 for every x in S.
---
[](https://gitpod.io/from-referrer/)
|
t-algebra
new-contributor
label:t-algebra$ |
7/0 |
Mathlib/Algebra/Polynomial/Roots.lean |
1 |
4 |
['LLaurance', 'erdOne', 'github-actions'] |
dagurtomas assignee:dagurtomas |
0-66960 18 hours ago |
1-68967 1 day ago |
5-75872 5 days |
| 32673 |
CoolRmal author:CoolRmal |
feat: an open subset of a Baire space is Baire |
This PR proves the following lemmas:
1. If `f : X → Y` is an open quotient map and `X` is a Baire space, then `Y` is Baire.
2. As a corollary of the first lemma, a homeomorphism maps a Baire space to a Baire space.
3. An open subset of a Baire space is Baire.
Formalized with help from Aristotle.
---
[](https://gitpod.io/from-referrer/)
|
t-topology
large-import
|
49/1 |
Mathlib/Topology/Baire/Lemmas.lean,Mathlib/Topology/Homeomorph/Lemmas.lean,Mathlib/Topology/Maps/OpenQuotient.lean |
3 |
2 |
['CoolRmal', 'github-actions'] |
nobody |
0-27736 7 hours ago |
0-30793 8 hours ago |
0-30835 8 hours |
| 29186 |
winstonyin author:winstonyin |
feat: IsIntegralCurve for solutions to ODEs |
I define `IsIntegralCurve` etc. for solutions to ODEs on vector spaces. The translation and scaling lemmas are also included. This parallels `IsMIntegralCurve` etc. for manifolds.
Moved from #26534.
- [x] depends on: #26563
---
[](https://gitpod.io/from-referrer/)
|
awaiting-author
t-differential-geometry
t-analysis
t-dynamics
|
312/100 |
Mathlib.lean,Mathlib/Analysis/ODE/Basic.lean,Mathlib/Analysis/ODE/Transform.lean,Mathlib/Geometry/Manifold/IntegralCurve/Basic.lean,Mathlib/Geometry/Manifold/IntegralCurve/Transform.lean |
5 |
8 |
['github-actions', 'grunweg', 'mathlib4-dependent-issues-bot', 'mathlib4-merge-conflict-bot', 'sgouezel'] |
sgouezel assignee:sgouezel |
1-15737 1 day ago |
5-84187 5 days ago |
86-36467 86 days |
| 32655 |
YaelDillies author:YaelDillies |
feat(Data/Set): a function surjective on univ is surjective |
---
[](https://gitpod.io/from-referrer/)
|
t-data |
3/0 |
Mathlib/Data/Set/Function.lean |
1 |
2 |
['github-actions', 'vihdzp'] |
nobody |
0-24950 6 hours ago |
0-78555 21 hours ago |
0-78591 21 hours |
| 32619 |
dagurtomas author:dagurtomas |
feat(CategoryTheory): the category of type-valued functors has images |
---
[](https://gitpod.io/from-referrer/)
|
t-category-theory |
87/24 |
Mathlib.lean,Mathlib/CategoryTheory/Limits/FunctorCategory/Shapes/Images.lean,Mathlib/CategoryTheory/Limits/Shapes/Images.lean,Mathlib/CategoryTheory/Subpresheaf/Basic.lean,Mathlib/CategoryTheory/Subpresheaf/Equalizer.lean,Mathlib/CategoryTheory/Subpresheaf/Image.lean,Mathlib/CategoryTheory/Subpresheaf/Subobject.lean |
7 |
10 |
['dagurtomas', 'github-actions', 'joelriou', 'leanprover-radar'] |
nobody |
0-24883 6 hours ago |
0-80620 22 hours ago |
1-16166 1 day |
| 32659 |
harahu author:harahu |
doc(Topology): fix typos |
Typos found and fixed by Codex.
---
I'd like feedback on whether this size of typo PR is fine to review, or whether it should be split up further.
[](https://gitpod.io/from-referrer/)
|
t-topology |
34/34 |
Mathlib/Topology/Algebra/InfiniteSum/UniformOn.lean,Mathlib/Topology/Bases.lean,Mathlib/Topology/EMetricSpace/PairReduction.lean,Mathlib/Topology/Homotopy/HSpaces.lean,Mathlib/Topology/MetricSpace/Bounded.lean,Mathlib/Topology/MetricSpace/Gluing.lean,Mathlib/Topology/MetricSpace/PiNat.lean,Mathlib/Topology/MetricSpace/ProperSpace.lean,Mathlib/Topology/MetricSpace/Pseudo/Defs.lean,Mathlib/Topology/Metrizable/Basic.lean,Mathlib/Topology/Metrizable/Uniformity.lean,Mathlib/Topology/OpenPartialHomeomorph/Constructions.lean,Mathlib/Topology/OpenPartialHomeomorph/IsImage.lean,Mathlib/Topology/UniformSpace/AbstractCompletion.lean |
14 |
7 |
['bryangingechen', 'github-actions', 'harahu', 'mathlib-bors', 'mathlib4-merge-conflict-bot'] |
nobody |
0-19464 5 hours ago |
0-25642 7 hours ago |
0-48302 13 hours |
| 31807 |
edegeltje author:edegeltje |
feat(CategoryTheory/Cat/Basic): Turning 1- and 2-morphisms in Cat into a 1-field structure |
This PR defines `Cat.Hom` and `Cat.Hom₂`, which are 1-field structures wrapping `Functor` and `NatTrans` respectively.
In addition, it changes the `Bicategory` instance for `Cat` to use these wrappers instead.
This PR adds such definitions as `NatTrans.toCatHom2`, `Cat.Hom.toFunctor`, `Cat.Hom₂.toNatTrans`, `Cat.Hom.isoMk` as well as simp lemmas for normalizing these to operations.
---
[](https://gitpod.io/from-referrer/)
|
t-category-theory |
793/587 |
Mathlib/Algebra/Category/ModuleCat/Pseudofunctor.lean,Mathlib/AlgebraicTopology/Quasicategory/StrictBicategory.lean,Mathlib/AlgebraicTopology/SimplicialSet/HomotopyCat.lean,Mathlib/AlgebraicTopology/SimplicialSet/Nerve.lean,Mathlib/AlgebraicTopology/SimplicialSet/NerveAdjunction.lean,Mathlib/CategoryTheory/Bicategory/CatEnriched.lean,Mathlib/CategoryTheory/Bicategory/Functor/Cat.lean,Mathlib/CategoryTheory/Bicategory/Grothendieck.lean,Mathlib/CategoryTheory/Category/Cat.lean,Mathlib/CategoryTheory/Category/Cat/Adjunction.lean,Mathlib/CategoryTheory/Category/Cat/AsSmall.lean,Mathlib/CategoryTheory/Category/Cat/CartesianClosed.lean,Mathlib/CategoryTheory/Category/Cat/Limit.lean,Mathlib/CategoryTheory/Category/Cat/Op.lean,Mathlib/CategoryTheory/Category/Cat/Terminal.lean,Mathlib/CategoryTheory/Category/Grpd.lean,Mathlib/CategoryTheory/Category/Quiv.lean,Mathlib/CategoryTheory/Category/ReflQuiv.lean,Mathlib/CategoryTheory/CodiscreteCategory.lean,Mathlib/CategoryTheory/Comma/Over/Basic.lean,Mathlib/CategoryTheory/Comma/StructuredArrow/Final.lean,Mathlib/CategoryTheory/Comma/StructuredArrow/Functor.lean,Mathlib/CategoryTheory/Elements.lean,Mathlib/CategoryTheory/FiberedCategory/Grothendieck.lean,Mathlib/CategoryTheory/Filtered/Grothendieck.lean,Mathlib/CategoryTheory/Functor/KanExtension/Adjunction.lean,Mathlib/CategoryTheory/Grothendieck.lean,Mathlib/CategoryTheory/Groupoid/FreeGroupoidOfCategory.lean,Mathlib/CategoryTheory/IsomorphismClasses.lean,Mathlib/CategoryTheory/Join/Pseudofunctor.lean,Mathlib/CategoryTheory/Limits/Final.lean,Mathlib/CategoryTheory/Limits/Shapes/Grothendieck.lean,Mathlib/CategoryTheory/Monoidal/Cartesian/Cat.lean,Mathlib/CategoryTheory/SingleObj.lean,Mathlib/CategoryTheory/Sites/Descent/DescentData.lean,Mathlib/CategoryTheory/Sites/Descent/IsPrestack.lean,Mathlib/CategoryTheory/Sites/PseudofunctorSheafOver.lean,Mathlib/CategoryTheory/WithTerminal/Basic.lean,Mathlib/Order/Category/Preord.lean,Mathlib/Tactic/CategoryTheory/ToApp.lean,MathlibTest/CategoryTheory/ToApp.lean |
41 |
29 |
['callesonne', 'edegeltje', 'github-actions', 'joelriou', 'mathlib4-merge-conflict-bot'] |
erdOne assignee:erdOne |
0-23020 6 hours ago |
3-64278 3 days ago |
13-55844 13 days |
| 32588 |
YaelDillies author:YaelDillies |
feat(Algebra/MonoidAlgebra): cardinality of monoid algebras |
Currently, all these lemmas are special cases of the `Finsupp` ones. After #25273 however, this will not be the case anymore.
---
[](https://gitpod.io/from-referrer/)
|
t-algebra label:t-algebra$ |
48/0 |
Mathlib.lean,Mathlib/Algebra/MonoidAlgebra/Cardinal.lean |
2 |
5 |
['YaelDillies', 'github-actions', 'vihdzp'] |
nobody |
0-22228 6 hours ago |
1-82898 1 day ago |
1-82931 1 day |
| 26608 |
vihdzp author:vihdzp |
feat(SetTheory/Cardinal/Aleph): `o.card ≤ ℵ_ o` and variants |
---
[](https://gitpod.io/from-referrer/)
|
merge-conflict
t-set-theory
|
24/0 |
Mathlib/SetTheory/Cardinal/Aleph.lean |
1 |
3 |
['github-actions', 'kckennylau', 'leanprover-community-bot-assistant'] |
nobody |
137-70729 4 months ago |
137-70730 4 months ago |
23-63406 23 days |
| 31019 |
vihdzp author:vihdzp |
feat: colex order on finsupps |
---
- [x] depends on: #30482
[](https://gitpod.io/from-referrer/)
|
maintainer-merge |
71/8 |
Mathlib/Data/Finsupp/Lex.lean,Mathlib/Order/Synonym.lean |
2 |
10 |
['YaelDillies', 'github-actions', 'mathlib4-dependent-issues-bot', 'mathlib4-merge-conflict-bot', 'vihdzp'] |
Vierkantor assignee:Vierkantor |
0-19415 5 hours ago |
0-19415 5 hours ago |
8-31610 8 days |
| 32640 |
vihdzp author:vihdzp |
feat: cardinality of Hahn series |
This is a very preliminary development; most of the PR is really just lemmas about `HahnSeries.support`. This will be needed in the CGT repo, to define surreal Hahn series as the subfield of real, small Hahn series over their own order dual.
---
[](https://gitpod.io/from-referrer/)
|
t-algebra
t-ring-theory
label:t-algebra$ |
149/35 |
Mathlib.lean,Mathlib/RingTheory/HahnSeries/Addition.lean,Mathlib/RingTheory/HahnSeries/Basic.lean,Mathlib/RingTheory/HahnSeries/Cardinal.lean,Mathlib/RingTheory/HahnSeries/Multiplication.lean,Mathlib/RingTheory/HahnSeries/Summable.lean |
6 |
5 |
['github-actions', 'mathlib4-merge-conflict-bot', 'vihdzp', 'wwylele'] |
nobody |
0-18731 5 hours ago |
0-18750 5 hours ago |
1-20426 1 day |
| 32610 |
alreadydone author:alreadydone |
feat(Algebra): Dedekind-finite monoids |
+ Prove equivalent characterizations of Dedekind-finite monoids.
+ Show commutative monoids, finite monoids, and Artinian semirings are Dedekind-finite, and finite monoids/rings are Dedekind-finite.
---
[](https://gitpod.io/from-referrer/)
|
t-algebra label:t-algebra$ |
201/29 |
Mathlib.lean,Mathlib/Algebra/Group/Basic.lean,Mathlib/Algebra/Group/Defs.lean,Mathlib/Algebra/Group/Equiv/Basic.lean,Mathlib/Algebra/Group/Hom/Defs.lean,Mathlib/Algebra/Group/Invertible/Defs.lean,Mathlib/Algebra/Group/Opposite.lean,Mathlib/Algebra/Group/Submonoid/Defs.lean,Mathlib/Algebra/Group/Units/Defs.lean,Mathlib/Algebra/Regular/Basic.lean,Mathlib/Algebra/Ring/Regular.lean,Mathlib/GroupTheory/DedekindFinite.lean,Mathlib/NumberTheory/NumberField/Norm.lean,Mathlib/RingTheory/Artinian/Module.lean,MathlibTest/LibraryRewrite.lean |
15 |
7 |
['alreadydone', 'github-actions', 'leanprover-radar', 'vihdzp'] |
nobody |
0-18261 5 hours ago |
1-60189 1 day ago |
1-61201 1 day |
| 30898 |
vihdzp author:vihdzp |
feat: characterization of `List.splitBy` |
---
- [x] depends on: #30892
Moved from #16837.
[](https://gitpod.io/from-referrer/)
|
t-data |
109/10 |
Mathlib/Data/List/Flatten.lean,Mathlib/Data/List/SplitBy.lean |
2 |
4 |
['github-actions', 'mathlib4-dependent-issues-bot', 'mathlib4-merge-conflict-bot', 'vihdzp'] |
nobody |
0-17991 4 hours ago |
0-20448 5 hours ago |
0-22939 6 hours |
| 32670 |
vihdzp author:vihdzp |
chore: notation `R⟦Γ⟧ = HahnSeries Γ R` |
As proposed on [Zulip](https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/Notation.20for.20Hahn.20series/with/562859530). This technically clashes with `R⟦X⟧` for power series, but a similar clash already exists between `R[G]` for `MonoidAlgebra` and `R[X]` for `Polynomial`, so it should be fine.
---
- [x] depends on: #32669
[](https://gitpod.io/from-referrer/)
|
t-algebra
t-ring-theory
label:t-algebra$ |
443/452 |
Mathlib/Algebra/Order/Module/HahnEmbedding.lean,Mathlib/Algebra/Order/Ring/Archimedean.lean,Mathlib/RingTheory/HahnSeries/Addition.lean,Mathlib/RingTheory/HahnSeries/Basic.lean,Mathlib/RingTheory/HahnSeries/Binomial.lean,Mathlib/RingTheory/HahnSeries/HEval.lean,Mathlib/RingTheory/HahnSeries/HahnEmbedding.lean,Mathlib/RingTheory/HahnSeries/Lex.lean,Mathlib/RingTheory/HahnSeries/Multiplication.lean,Mathlib/RingTheory/HahnSeries/PowerSeries.lean,Mathlib/RingTheory/HahnSeries/Summable.lean,Mathlib/RingTheory/HahnSeries/Valuation.lean,Mathlib/RingTheory/LaurentSeries.lean |
13 |
3 |
['github-actions', 'mathlib4-dependent-issues-bot', 'vihdzp'] |
nobody |
0-17728 4 hours ago |
0-28677 7 hours ago |
0-29596 8 hours |
| 32666 |
kim-em author:kim-em |
chore: replace `omega` with `lia` where possible |
As previously discussed, we'd like to move users off `omega` and on to `lia` (which is the linear integer arithmetic module from `grind`, plus a controlled set of instantiated lemmas).
This does not yet remove all uses of `omega` in Mathlib. |
|
766/765 |
Archive/Imo/Imo1960Q1.lean,Archive/Imo/Imo1962Q1.lean,Archive/Imo/Imo1985Q2.lean,Archive/Imo/Imo1988Q6.lean,Archive/Imo/Imo1994Q1.lean,Archive/Imo/Imo1997Q3.lean,Archive/Imo/Imo2001Q3.lean,Archive/Imo/Imo2001Q6.lean,Archive/Imo/Imo2008Q3.lean,Archive/Imo/Imo2015Q6.lean,Archive/Imo/Imo2021Q1.lean,Archive/Imo/Imo2024Q1.lean,Archive/Imo/Imo2024Q2.lean,Archive/Imo/Imo2024Q3.lean,Archive/Imo/Imo2024Q5.lean,Archive/Wiedijk100Theorems/FriendshipGraphs.lean,Counterexamples/AharoniKorman.lean,Counterexamples/DiscreteTopologyNonDiscreteUniformity.lean,Mathlib/Algebra/AffineMonoid/Irreducible.lean,Mathlib/Algebra/BigOperators/Fin.lean,Mathlib/Algebra/BigOperators/Group/Finset/Interval.lean,Mathlib/Algebra/BigOperators/Intervals.lean,Mathlib/Algebra/CharP/Lemmas.lean,Mathlib/Algebra/ContinuedFractions/Computation/Approximations.lean,Mathlib/Algebra/Group/Defs.lean,Mathlib/Algebra/Group/Fin/Basic.lean,Mathlib/Algebra/Homology/ComplexShapeSigns.lean,Mathlib/Algebra/Homology/DerivedCategory/Ext/Basic.lean,Mathlib/Algebra/Homology/DerivedCategory/TStructure.lean,Mathlib/Algebra/Homology/Embedding/AreComplementary.lean,Mathlib/Algebra/Homology/Embedding/Basic.lean,Mathlib/Algebra/Homology/ExactSequence.lean,Mathlib/Algebra/Homology/HomotopyCategory/DegreewiseSplit.lean,Mathlib/Algebra/Homology/HomotopyCategory/HomComplex.lean,Mathlib/Algebra/Homology/HomotopyCategory/HomComplexShift.lean,Mathlib/Algebra/Homology/HomotopyCategory/MappingCone.lean,Mathlib/Algebra/Homology/HomotopyCategory/Pretriangulated.lean,Mathlib/Algebra/Homology/HomotopyCategory/Shift.lean,Mathlib/Algebra/Homology/HomotopyCategory/SingleFunctors.lean,Mathlib/Algebra/Homology/LeftResolution/Basic.lean,Mathlib/Algebra/Homology/TotalComplexShift.lean,Mathlib/Algebra/Lie/Sl2.lean,Mathlib/Algebra/Lie/Weights/Chain.lean,Mathlib/Algebra/Lie/Weights/RootSystem.lean,Mathlib/Algebra/LinearRecurrence.lean,Mathlib/Algebra/Module/ZLattice/Summable.lean,Mathlib/Algebra/Order/Antidiag/Nat.lean,Mathlib/Algebra/Order/Group/Int/Sum.lean,Mathlib/Algebra/Order/Ring/Int.lean,Mathlib/Algebra/Polynomial/AlgebraMap.lean,Mathlib/Algebra/Polynomial/EraseLead.lean,Mathlib/Algebra/Polynomial/Laurent.lean,Mathlib/Algebra/Polynomial/RuleOfSigns.lean,Mathlib/Algebra/Ring/GeomSum.lean,Mathlib/Algebra/Squarefree/Basic.lean,Mathlib/AlgebraicTopology/DoldKan/Decomposition.lean,Mathlib/AlgebraicTopology/DoldKan/Degeneracies.lean,Mathlib/AlgebraicTopology/DoldKan/Faces.lean,Mathlib/AlgebraicTopology/DoldKan/FunctorGamma.lean,Mathlib/AlgebraicTopology/DoldKan/Projections.lean,Mathlib/AlgebraicTopology/SimplexCategory/Augmented/Monoidal.lean,Mathlib/AlgebraicTopology/SimplexCategory/Basic.lean,Mathlib/AlgebraicTopology/SimplexCategory/Defs.lean,Mathlib/AlgebraicTopology/SimplexCategory/Truncated.lean,Mathlib/AlgebraicTopology/SimplicialObject/Basic.lean,Mathlib/AlgebraicTopology/SimplicialSet/AnodyneExtensions/Rank.lean,Mathlib/AlgebraicTopology/SimplicialSet/Basic.lean,Mathlib/AlgebraicTopology/SimplicialSet/Coskeletal.lean,Mathlib/AlgebraicTopology/SimplicialSet/Nerve.lean,Mathlib/AlgebraicTopology/SimplicialSet/Path.lean,Mathlib/AlgebraicTopology/SimplicialSet/StrictSegal.lean,Mathlib/Analysis/Analytic/Composition.lean,Mathlib/Analysis/Analytic/Inverse.lean,Mathlib/Analysis/Analytic/IteratedFDeriv.lean,Mathlib/Analysis/Calculus/BumpFunction/FiniteDimension.lean,Mathlib/Analysis/Calculus/ContDiff/FaaDiBruno.lean,Mathlib/Analysis/Calculus/FDeriv/Measurable.lean,Mathlib/Analysis/Complex/Polynomial/Basic.lean,Mathlib/Analysis/Convex/Between.lean,Mathlib/Analysis/Distribution/FourierSchwartz.lean,Mathlib/Analysis/InnerProductSpace/Projection/FiniteDimensional.lean,Mathlib/Analysis/InnerProductSpace/TwoDim.lean,Mathlib/Analysis/Normed/Affine/Simplex.lean,Mathlib/Analysis/Normed/Unbundled/SeminormFromConst.lean,Mathlib/Analysis/SpecialFunctions/Gamma/BohrMollerup.lean,Mathlib/Analysis/SpecialFunctions/Integrals/Basic.lean,Mathlib/Analysis/SpecialFunctions/Trigonometric/Basic.lean,Mathlib/Analysis/SpecificLimits/Normed.lean,Mathlib/Analysis/SumIntegralComparisons.lean,Mathlib/CategoryTheory/ComposableArrows/Basic.lean,Mathlib/CategoryTheory/Functor/OfSequence.lean,Mathlib/CategoryTheory/Limits/Shapes/SequentialProduct.lean,Mathlib/Combinatorics/Additive/ApproximateSubgroup.lean,Mathlib/Combinatorics/Additive/Corner/Roth.lean,Mathlib/Combinatorics/Additive/ErdosGinzburgZiv.lean,Mathlib/Combinatorics/Derangements/Finite.lean,Mathlib/Combinatorics/Enumerative/Catalan.lean,Mathlib/Combinatorics/Enumerative/Composition.lean,Mathlib/Combinatorics/Enumerative/DyckWord.lean,Mathlib/Combinatorics/Quiver/Path.lean |
229 |
3 |
['github-actions', 'grunweg', 'leanprover-radar'] |
nobody |
0-16717 4 hours ago |
0-21610 5 hours ago |
0-44813 12 hours |
| 32480 |
ADedecker author:ADedecker |
feat: define `PolynormableSpace` |
A "polynormable space" is a TVS whose topology is induced by *some* family of seminorms. In the real or complex case this is just locally convex, but it makes sense (and will be used) for general nontrivially normed fields.
The name is inspired by Bourbaki's "espace polynormé", although they only allow ultrametric seminorms over an ultrametric field.
My motivation is the following:
- first, I want to be able to state [WithSeminorms.banach_steinhaus](https://leanprover-community.github.io/mathlib4_docs/Mathlib/Analysis/LocallyConvex/Barrelled.html#WithSeminorms.banach_steinhaus) without a choice of seminorm family. This is easy to do, and I have a PR on the way
- the notion of bornological TVS makes sense over an arbitrary nontrivially normed field, and we have that any sequentially continuous linear map from a bornological TVS to a polynormable space is continuous. I see no reason to restrict to the real or complex case here.
---
[](https://gitpod.io/from-referrer/)
|
t-analysis
maintainer-merge
|
51/0 |
Mathlib/Analysis/LocallyConvex/AbsConvexOpen.lean,Mathlib/Analysis/LocallyConvex/WithSeminorms.lean |
2 |
7 |
['ADedecker', 'github-actions', 'j-loreaux'] |
fpvandoorn assignee:fpvandoorn |
0-16550 4 hours ago |
0-16550 4 hours ago |
4-25645 4 days |
| 32664 |
harahu author:harahu |
doc: fix articles a/an |
Use the correct article “an” before certain single-letter code terms (`ℝ`, `N`, `R`, `S`, `n` and `r`).
---
[](https://gitpod.io/from-referrer/)
|
|
82/81 |
Mathlib/Algebra/Algebra/Operations.lean,Mathlib/Algebra/Category/ModuleCat/ChangeOfRings.lean,Mathlib/Algebra/Category/ModuleCat/LeftResolution.lean,Mathlib/Algebra/CharP/LinearMaps.lean,Mathlib/Algebra/Homology/DerivedCategory/Ext/Linear.lean,Mathlib/Algebra/Homology/ShortComplex/Linear.lean,Mathlib/Algebra/Module/FinitePresentation.lean,Mathlib/Algebra/Module/Presentation/Differentials.lean,Mathlib/Algebra/Module/Torsion/Basic.lean,Mathlib/Algebra/Module/Torsion/Free.lean,Mathlib/Algebra/MvPolynomial/Basic.lean,Mathlib/Algebra/Polynomial/Module/AEval.lean,Mathlib/AlgebraicGeometry/Over.lean,Mathlib/AlgebraicGeometry/RationalMap.lean,Mathlib/AlgebraicGeometry/SpreadingOut.lean,Mathlib/AlgebraicTopology/SimplicialSet/StrictSegal.lean,Mathlib/Analysis/Convex/Cone/Basic.lean,Mathlib/CategoryTheory/Center/Linear.lean,Mathlib/CategoryTheory/Localization/Linear.lean,Mathlib/CategoryTheory/Quotient/Linear.lean,Mathlib/Combinatorics/SimpleGraph/ConcreteColorings.lean,Mathlib/Data/Fin/Tuple/Take.lean,Mathlib/Data/Rel/Separated.lean,Mathlib/FieldTheory/KummerExtension.lean,Mathlib/FieldTheory/Minpoly/IsConjRoot.lean,Mathlib/Geometry/Convex/Cone/Basic.lean,Mathlib/MeasureTheory/Integral/RieszMarkovKakutani/NNReal.lean,Mathlib/NumberTheory/Cyclotomic/PrimitiveRoots.lean,Mathlib/NumberTheory/NumberField/CanonicalEmbedding/Basic.lean,Mathlib/NumberTheory/NumberField/Cyclotomic/Basic.lean,Mathlib/NumberTheory/NumberField/Cyclotomic/Embeddings.lean,Mathlib/RingTheory/Bialgebra/Basic.lean,Mathlib/RingTheory/Extension/Generators.lean,Mathlib/RingTheory/FilteredAlgebra/Basic.lean,Mathlib/RingTheory/Flat/Basic.lean,Mathlib/RingTheory/Kaehler/Basic.lean,Mathlib/RingTheory/KrullDimension/Module.lean,Mathlib/RingTheory/LaurentSeries.lean,Mathlib/RingTheory/Localization/NormTrace.lean,Mathlib/RingTheory/PicardGroup.lean,Mathlib/RingTheory/PolynomialLaw/Basic.lean,Mathlib/RingTheory/TensorProduct/Free.lean,Mathlib/RingTheory/Unramified/Finite.lean,Mathlib/Topology/ContinuousMap/CompactlySupported.lean,Mathlib/Topology/EMetricSpace/Defs.lean,Mathlib/Topology/MetricSpace/Defs.lean,Mathlib/Topology/MetricSpace/HausdorffDistance.lean,Mathlib/Topology/MetricSpace/Pseudo/Defs.lean |
48 |
3 |
['github-actions', 'harahu', 'vihdzp'] |
nobody |
0-16103 4 hours ago |
0-57809 16 hours ago |
0-58412 16 hours |
| 27702 |
FLDutchmann author:FLDutchmann |
feat(NumberTheory/SelbergSieve): define Lambda-squared sieves and prove important properties |
This PR continues the work from #22052.
Original PR: https://github.com/leanprover-community/mathlib4/pull/22052
- [x] depends on: #27820
|
t-number-theory
maintainer-merge
|
186/7 |
Mathlib/NumberTheory/SelbergSieve.lean |
1 |
41 |
['FLDutchmann', 'MichaelStollBayreuth', 'bryangingechen', 'github-actions', 'jcommelin', 'mathlib-bors', 'mathlib4-dependent-issues-bot', 'mathlib4-merge-conflict-bot'] |
MichaelStollBayreuth assignee:MichaelStollBayreuth |
0-15393 4 hours ago |
0-15621 4 hours ago |
15-24646 15 days |
| 32684 |
Parcly-Taxel author:Parcly-Taxel |
feat: a simple unit-distance embedding of the Heawood graph |
This PR is not meant to be merge-ready; it is just to record my work.
The embedding is depicted below, with vertex labels as in the formalisation. I originally found it in August 2025 – see https://github.com/Parcly-Taxel/Shibuya/commit/b5c86cbf1c8b2e1211b160f266480e7115a7e43a.
 |
t-combinatorics |
223/0 |
Mathlib.lean,Mathlib/Combinatorics/SimpleGraph/UnitDistance/Basic.lean,Mathlib/Combinatorics/SimpleGraph/UnitDistance/Heawood.lean |
3 |
1 |
['github-actions'] |
nobody |
0-14467 4 hours ago |
0-15322 4 hours ago |
0-15367 4 hours |
| 31416 |
SnirBroshi author:SnirBroshi |
feat(Combinatorics/SimpleGraph/Walk): lemmas about the first and last darts/edges |
---
[](https://gitpod.io/from-referrer/)
|
t-combinatorics |
96/8 |
Mathlib/Combinatorics/SimpleGraph/Acyclic.lean,Mathlib/Combinatorics/SimpleGraph/Paths.lean,Mathlib/Combinatorics/SimpleGraph/Walks/Basic.lean,Mathlib/Combinatorics/SimpleGraph/Walks/Traversal.lean |
4 |
18 |
['SnirBroshi', 'YaelDillies', 'github-actions', 'mathlib4-merge-conflict-bot'] |
YaelDillies assignee:YaelDillies |
0-24428 6 hours ago |
0-40103 11 hours ago |
21-10293 21 days |
| 32414 |
SnirBroshi author:SnirBroshi |
feat(NumberTheory/ArithmeticFunction/Carmichael): Carmichael totient function |
Define `ArithmeticFunction.Carmichael`, the Carmichael function `λ`, also known as the reduced totient function.
Prove the known formula for `λ n` in terms of the prime factorization of `n`, along with some useful properties:
- `a ^ λ n = 1`
- `λ n ∣ φ n`
- `a ∣ b → λ a ∣ λ b`
- `λ (lcm a b) = lcm (λ a) (λ b)`
---
I'm open to suggestions on where to place the `Finset.lcm` lemmas, I created a separate file to avoid adding imports to existing files.
I'm also wondering whether to change the `HasEnoughRootsOfUnity` here to use `Carmichael`: https://github.com/leanprover-community/mathlib4/blob/6a7385f3f6d2c0b674e3ecd96506e57737b77064/Mathlib/NumberTheory/DirichletCharacter/Orthogonality.lean#L31
[](https://gitpod.io/from-referrer/)
|
|
211/0 |
Mathlib.lean,Mathlib/Algebra/GCDMonoid/FinsetLemmas.lean,Mathlib/NumberTheory/ArithmeticFunction/Carmichael.lean |
3 |
1 |
['github-actions'] |
MichaelStollBayreuth assignee:MichaelStollBayreuth |
2-51653 2 days ago |
6-45515 6 days ago |
6-45490 6 days |
| 32691 |
alreadydone author:alreadydone |
feat(Topology/AddCircle): remove `0 < p` condition from `finite_torsion` |
---
[](https://gitpod.io/from-referrer/)
|
t-topology
t-algebra
t-order
maintainer-merge
label:t-algebra$ |
18/6 |
Mathlib/Topology/Instances/AddCircle/Defs.lean |
1 |
3 |
['github-actions', 'grunweg'] |
nobody |
0-2944 49 minutes ago |
0-2944 48 minutes ago |
0-5919 1 hour |
| 32598 |
PrParadoxy author:PrParadoxy |
feat(LinearAlgebra/PiTensorProduct): add version of `subsingletonEquiv` for dependent case |
Dependent `PiTensorProduct`s over singleton types occur naturally when
using `tmulEquivDep` to split off one index from a dependent
`PiTensorProduct`. This PR creates `subsingletonEquivDep` to deal with
this situation.
The non-dependent `subsingletonEquiv` is re-defined as a specialization
of the general case. This breaks `toDirectSum_ι` in
TensorAlgebra/ToTensorPower, which relies on the precise definition of
`subsingletonEquiv`. Its proof is therefore changed to use `simp` lemmas.
[](https://gitpod.io/from-referrer/)
|
t-algebra
new-contributor
label:t-algebra$ |
43/26 |
Mathlib/LinearAlgebra/PiTensorProduct.lean,Mathlib/LinearAlgebra/TensorAlgebra/ToTensorPower.lean |
2 |
2 |
['github-actions', 'kbuzzard'] |
ocfnash assignee:ocfnash |
0-2514 41 minutes ago |
1-73424 1 day ago |
1-73468 1 day |
| 31081 |
chrisflav author:chrisflav |
feat(RingTheory/StandardSmooth): presentation independent characterization |
We show that if `S` is of finite presentation over `R` such that `H¹(S/R) = 0` and `Ω[S⁄R]` is free on `{d sᵢ}ᵢ` for some `sᵢ : S`, then `S` is `R`-standard smooth. The converse of this is already in mathlib.
In the next PR, we will deduce from this that smooth is equivalent to locally standard smooth.
From Pi1.
---
- [x] depends on: #31034
- [x] depends on: #31082
- [x] depends on: #28769
[](https://gitpod.io/from-referrer/)
|
t-ring-theory |
151/0 |
Mathlib.lean,Mathlib/LinearAlgebra/Basis/Exact.lean,Mathlib/RingTheory/Extension/Cotangent/Free.lean,Mathlib/RingTheory/Smooth/StandardSmooth.lean,Mathlib/RingTheory/Smooth/StandardSmoothCotangent.lean,Mathlib/RingTheory/Smooth/StandardSmoothOfFree.lean |
6 |
5 |
['chrisflav', 'erdOne', 'github-actions', 'mathlib4-dependent-issues-bot', 'mathlib4-merge-conflict-bot'] |
mattrobball assignee:mattrobball |
0-45380 12 hours ago |
2-31 2 days ago |
2-714 2 days |