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 |
21-68803 21 days ago |
24-80374 24 days ago |
37-82298 37 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 |
17-33929 17 days ago |
18-46896 18 days ago |
27-15356 27 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 |
16-33931 16 days ago |
20-1220 20 days ago |
20-1193 20 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 |
16-5472 16 days ago |
19-63860 19 days ago |
45-69959 45 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 |
15-40518 15 days ago |
21-13389 21 days ago |
21-13424 21 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 |
14-33913 14 days ago |
17-80478 17 days ago |
20-78143 20 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 |
13-33904 13 days ago |
16-55472 16 days ago |
16-55454 16 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 |
12-78945 12 days ago |
12-80468 12 days ago |
22-38816 22 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 |
12-33936 12 days ago |
15-69560 15 days ago |
17-69983 17 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 |
12-33932 12 days ago |
16-3773 16 days ago |
16-4361 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 |
12-33926 12 days ago |
18-26236 18 days ago |
18-26276 18 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 |
11-57719 11 days ago |
15-57689 15 days ago |
15-58781 15 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 |
11-48833 11 days ago |
16-50289 16 days ago |
16-50319 16 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 |
11-39407 11 days ago |
12-36572 12 days ago |
60-36653 60 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 |
11-33922 11 days ago |
15-24001 15 days ago |
15-26622 15 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 |
11-33917 11 days ago |
14-67944 14 days ago |
16-70407 16 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 |
11-33912 11 days ago |
14-71259 14 days ago |
14-71290 14 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 |
11-2344 11 days ago |
11-2393 11 days ago |
11-30576 11 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 |
10-62968 10 days ago |
10-63100 10 days ago |
15-80792 15 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 |
10-33931 10 days ago |
20-12473 20 days ago |
20-43361 20 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 |
10-33930 10 days ago |
17-30563 17 days ago |
17-30595 17 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 |
9-73232 9 days ago |
9-73232 9 days ago |
23-41324 23 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 |
9-35343 9 days ago |
9-80449 9 days ago |
9-82042 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 |
9-3576 9 days ago |
9-3576 9 days ago |
12-61131 12 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 |
8-85938 8 days ago |
8-85938 8 days ago |
16-65222 16 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 |
8-67861 8 days ago |
8-67895 8 days ago |
23-60497 23 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 |
8-66285 8 days ago |
18-46940 18 days ago |
18-49483 18 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 |
8-57491 8 days ago |
17-56343 17 days ago |
23-41023 23 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 |
8-50454 8 days ago |
38-67430 1 month ago |
38-67382 38 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 |
8-49614 8 days ago |
8-54225 8 days ago |
16-63580 16 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 |
8-33934 8 days ago |
13-85380 13 days ago |
13-85411 13 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 |
8-33933 8 days ago |
12-58294 12 days ago |
12-61018 12 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 |
7-83377 7 days ago |
7-86395 7 days ago |
8-41379 8 days |
| 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 |
6-71896 6 days ago |
8-36012 8 days ago |
65-21041 65 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 |
6-63973 6 days ago |
6-63973 6 days ago |
48-8588 48 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 |
6-58087 6 days ago |
6-58206 6 days ago |
11-52635 11 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 |
6-42145 6 days ago |
12-45347 12 days ago |
12-48297 12 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 |
6-33928 6 days ago |
9-40259 9 days ago |
10-44856 10 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 |
6-33924 6 days ago |
9-79827 9 days ago |
9-79801 9 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 |
6-33922 6 days ago |
9-61856 9 days ago |
9-61830 9 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 |
5-82475 5 days ago |
5-82504 5 days ago |
6-3680 6 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 |
53-64358 1 month ago |
unknown |
unknown |
| 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 |
5-68500 5 days ago |
16-78779 16 days ago |
30-75273 30 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 |
5-39522 5 days ago |
17-31549 17 days ago |
17-31579 17 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 |
5-33931 5 days ago |
21-24859 21 days ago |
21-24894 21 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 |
5-33927 5 days ago |
9-21242 9 days ago |
9-21229 9 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 |
5-31716 5 days ago |
5-31716 5 days ago |
26-27781 26 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 |
5-20964 5 days ago |
5-20964 5 days ago |
66-14150 66 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 |
5-20924 5 days ago |
5-41804 5 days ago |
65-20531 65 days |
| 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 |
4-78246 4 days ago |
5-1893 5 days ago |
12-1352 12 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 |
4-59968 4 days ago |
4-60996 4 days ago |
4-61027 4 days |
| 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 |
4-53238 4 days ago |
4-53259 4 days ago |
35-3996 35 days |
| 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 |
4-36558 4 days ago |
4-36566 4 days ago |
45-75883 45 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 |
4-35111 4 days ago |
4-35221 4 days ago |
9-75330 9 days |
| 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 |
4-33928 4 days ago |
8-33422 8 days ago |
8-33729 8 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 |
4-33918 4 days ago |
8-42049 8 days ago |
8-42021 8 days |
| 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/)
|
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 |
4-7839 4 days ago |
4-7839 4 days ago |
90-44275 90 days |
| 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 |
3-85222 3 days ago |
3-85222 3 days ago |
8-7914 8 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 |
6 |
['github-actions', 'ocfnash', 'plp127', 'vihdzp'] |
pechersky assignee:pechersky |
3-67390 3 days ago |
8-48125 8 days ago |
9-16657 9 days |
| 32080 |
plp127 author:plp127 |
feat(Topology): Completely Regular Space iff Uniformizable |
This PR continues the work from #24096.
Original PR: https://github.com/leanprover-community/mathlib4/pull/24096
---------
- [x] depends on: #32140 |
t-topology |
122/0 |
Mathlib.lean,Mathlib/Data/Rel.lean,Mathlib/Topology/UniformSpace/Basic.lean,Mathlib/Topology/UniformSpace/Uniformizable.lean |
4 |
17 |
['alreadydone', 'github-actions', 'grunweg', 'j-loreaux', 'mathlib4-dependent-issues-bot', 'plp127'] |
urkud assignee:urkud |
3-47048 3 days ago |
3-47116 3 days ago |
16-85176 16 days |
| 32702 |
SnirBroshi author:SnirBroshi |
chore(Combinatorics/SimpleGraph/Connectivity): move `Finite ConnectedComponent` instance from `WalkCounting.lean` to `Connected.lean` |
---
This moves it near similar instances, and makes it available for more files.
[](https://gitpod.io/from-referrer/)
|
t-combinatorics |
1/2 |
Mathlib/Combinatorics/SimpleGraph/Connectivity/Connected.lean,Mathlib/Combinatorics/SimpleGraph/Connectivity/WalkCounting.lean |
2 |
1 |
['github-actions'] |
nobody |
3-46157 3 days ago |
3-46207 3 days ago |
3-46240 3 days |
| 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'] |
j-loreaux assignee:j-loreaux |
3-33927 3 days ago |
6-53533 6 days ago |
7-20783 7 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'] |
dagurtomas assignee:dagurtomas |
3-33923 3 days ago |
6-74707 6 days ago |
8-71270 8 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'] |
kex-y assignee:kex-y |
3-33920 3 days ago |
6-81999 6 days ago |
7-1189 7 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'] |
awainverse assignee:awainverse |
3-33915 3 days ago |
7-17646 7 days ago |
7-17687 7 days |
| 32710 |
erdOne author:erdOne |
feat(Topology/MetricSpace): proper iff `dist _` is proper map |
Also moved `ConditionallyCompleteLinearOrder.isCompact_Icc` and `ProperSpace ℝ` earlier to avoid large inputs.
---
[](https://gitpod.io/from-referrer/)
|
t-topology |
61/62 |
Mathlib/Topology/Algebra/ProperAction/ProperlyDiscontinuous.lean,Mathlib/Topology/Maps/Proper/CompactlyGenerated.lean,Mathlib/Topology/MetricSpace/ProperSpace.lean,Mathlib/Topology/MetricSpace/ProperSpace/Lemmas.lean,Mathlib/Topology/MetricSpace/ProperSpace/Real.lean,Mathlib/Topology/Order/Compact.lean,Mathlib/Topology/Order/IsLUB.lean |
7 |
2 |
['erdOne', 'github-actions'] |
nobody |
3-25714 3 days ago |
3-27043 3 days ago |
3-27082 3 days |
| 32307 |
mcdoll author:mcdoll |
feat(Analysis/Distribution): `(1 + |x|^2)^r` has temperate growth |
---
- [ ] depends on: #32297
[](https://gitpod.io/from-referrer/)
|
WIP
blocked-by-other-PR
t-analysis
|
166/2 |
Mathlib/Analysis/Distribution/SchwartzSpace.lean,Mathlib/Analysis/Distribution/TemperateGrowth.lean |
2 |
2 |
['github-actions', 'mathlib4-dependent-issues-bot'] |
nobody |
12-72255 12 days ago |
12-72256 12 days ago |
0-31 31 seconds |
| 32719 |
EtienneC30 author:EtienneC30 |
feat: another version of mapping Gaussian measures |
Mathlib has [ProbabilityTheory.isGaussian_map](https://leanprover-community.github.io/mathlib4_docs/Mathlib/Probability/Distributions/Gaussian/Basic.html#ProbabilityTheory.isGaussian_map) which states that mapping a Gaussian measure by a continuous linear map yields a Gaussian measure. However this requires the domain of the linear map to be Borel, which in turns requires some second countability assumption if said domain is a product space. This Borel assumption is only needed to ensure that the continuous linear map is measurable, but for instance `Prod.fst` and `Prod.snd` are measurable regardless of Borel considerations. We thus provide a new version which much less assumptions on the space and with the extra assumption that the map is measurable. This avoids some second countability assumptions in #32144.
---
[](https://gitpod.io/from-referrer/)
|
t-measure-probability
brownian
|
8/0 |
Mathlib/Probability/Distributions/Gaussian/Basic.lean |
1 |
1 |
['github-actions'] |
nobody |
3-3359 3 days ago |
3-3435 3 days ago |
3-3408 3 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 |
68/2 |
Mathlib/Geometry/Euclidean/Projection.lean |
1 |
3 |
['github-actions', 'mathlib4-dependent-issues-bot', 'mathlib4-merge-conflict-bot'] |
JovanGerb assignee:JovanGerb |
2-58232 2 days ago |
2-72049 2 days ago |
19-48108 19 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 |
2-57173 2 days ago |
24-84893 24 days ago |
29-41720 29 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
|
41/0 |
Mathlib/ModelTheory/Satisfiability.lean |
1 |
9 |
['awainverse', 'foderm', 'github-actions'] |
awainverse assignee:awainverse |
2-53824 2 days ago |
17-54643 17 days ago |
17-54682 17 days |
| 32755 |
alreadydone author:alreadydone |
chore(Topology/Compactness): golf |
---
[](https://gitpod.io/from-referrer/)
|
t-topology |
15/21 |
Mathlib/Topology/Compactness/Compact.lean |
1 |
1 |
['github-actions'] |
nobody |
2-53529 2 days ago |
2-53592 2 days ago |
2-53565 2 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 |
257/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,docs/references.bib |
7 |
6 |
['github-actions', 'mathlib4-dependent-issues-bot', 'mathlib4-merge-conflict-bot', 'robin-carlier'] |
ADedecker assignee:ADedecker |
2-51284 2 days ago |
2-65470 2 days ago |
23-25621 23 days |
| 32740 |
LTolDe author:LTolDe |
feat: add IsNowhereDense helpers |
add new lemmas to prove `IsNowhereDense s`
- IsNowhereDense.mono
- Topology.IsInducing.isNowhereDense_image
- IsNowhereDense.image_val
these lemmas will help to prove the **Effros Theorem**, see [zulip thread](https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/Effros.20Theorem/with/558712441)
---
[](https://gitpod.io/from-referrer/)
|
new-contributor
large-import
|
22/1 |
Mathlib/Topology/GDelta/Basic.lean |
1 |
1 |
['github-actions'] |
nobody |
2-47346 2 days ago |
2-66930 2 days ago |
2-66960 2 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/)
|
|
29/54 |
Mathlib/MeasureTheory/Measure/RegularityCompacts.lean |
1 |
2 |
['github-actions', 'mathlib4-merge-conflict-bot'] |
nobody |
2-47206 2 days ago |
2-68317 2 days ago |
5-50544 5 days |
| 30851 |
FormulaRabbit81 author:FormulaRabbit81 |
feat(Topology): prove there exists an embedding of separable metric spaces in the hilbert cube |
---
[](https://gitpod.io/from-referrer/)
- [x] depends on: #30849 |
t-topology |
78/8 |
Mathlib/Topology/Compactness/HilbertCubeEmbedding.lean,Mathlib/Topology/MetricSpace/HausdorffAlexandroff.lean,Mathlib/Topology/MetricSpace/PiNat.lean |
3 |
14 |
['FormulaRabbit81', 'erdOne', 'github-actions', 'j-loreaux', 'mathlib4-dependent-issues-bot', 'mathlib4-merge-conflict-bot'] |
ADedecker assignee:ADedecker |
2-39972 2 days ago |
2-40114 2 days ago |
31-47362 31 days |
| 32382 |
YaelDillies author:YaelDillies |
chore(Algebra/Order/AddGroupWithTop): golf |
---
[](https://gitpod.io/from-referrer/)
|
t-algebra label:t-algebra$ |
107/154 |
Mathlib/Algebra/Order/AddGroupWithTop.lean,Mathlib/Algebra/Order/GroupWithZero/Canonical.lean,Mathlib/Algebra/Order/Ring/Archimedean.lean |
3 |
1 |
['github-actions'] |
dagurtomas assignee:dagurtomas |
2-33922 2 days ago |
10-73754 10 days ago |
11-7020 11 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'] |
EtienneC30 assignee:EtienneC30 |
2-33920 2 days ago |
6-62502 6 days ago |
6-72791 6 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'] |
bryangingechen assignee:bryangingechen |
2-33916 2 days ago |
6-31093 6 days ago |
6-31124 6 days |
| 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'] |
kmill assignee:kmill |
2-33915 2 days ago |
6-26420 6 days ago |
6-26460 6 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'] |
joelriou assignee:joelriou |
2-33910 2 days ago |
5-36947 5 days ago |
5-36920 5 days |
| 32764 |
plp127 author:plp127 |
feat(Topology/Separation): completely normal iff hereditarily normal |
Prove a space is completely normal iff it is hereditarily normal iff all open subspaces are normal.
---
[](https://gitpod.io/from-referrer/)
|
t-topology |
71/0 |
Mathlib/Topology/Separation/Regular.lean |
1 |
1 |
['github-actions'] |
nobody |
2-32063 2 days ago |
2-32122 2 days ago |
2-32103 2 days |
| 32608 |
PrParadoxy author:PrParadoxy |
feat(LinearAlgebra/PiTensorProduct): API for PiTensorProducts indexed by sets |
This PR addresses a TODO item in LinearAlgebra/PiTensorProduct.lean:
* API for the various ways `ι` can be split into subsets; connect this
with the binary tensor product
-- specifically by describing tensors of type `⨂ (i : S), s i`, for `S : Set ι`.
Our primary motivation is to formalize the notion of "tensors with
infinite index set, which are equal to a distinguished element on all
but finitely many indices". This is a standard construction e.g. in the
theory of "infinite tensor products" of unital algebras.
Beyond that, the `Set` API is natural in contexts where the index type has
an independent interpretation. An example is quantum physics, where `ι`
ranges over distinguishable degrees of freedom, and where its is common
practice to annotate objects by the set of indices they are defined on.
This PR creates a directory LinearAlgebra/PiTensorProduct and starts the
file Set.lean.
---
- [x] depends on: #32598
[](https://gitpod.io/from-referrer/)
|
new-contributor |
301/0 |
Mathlib.lean,Mathlib/LinearAlgebra/PiTensorProduct/Set.lean |
2 |
6 |
['PrParadoxy', 'github-actions', 'leanprover-radar', 'mathlib4-dependent-issues-bot', 'mathlib4-merge-conflict-bot'] |
nobody |
2-31091 2 days ago |
2-37266 2 days ago |
2-42264 2 days |
| 27254 |
yuanyi-350 author:yuanyi-350 |
feat: 2025 imo problem3 |
- [x] depends on: #28788
- [x] depends on: #28790
- [x] depends on: #28829
---
[](https://gitpod.io/from-referrer/)
|
IMO |
222/0 |
Archive.lean,Archive/Imo/Imo2025Q3.lean |
2 |
29 |
['github-actions', 'jsm28', 'kbuzzard', 'leanprover-community-bot-assistant', 'madvorak', 'mathlib4-dependent-issues-bot', 'mathlib4-merge-conflict-bot', 'themathqueen', 'wwylele', 'yuanyi-350'] |
jsm28 assignee:jsm28 |
2-28127 2 days ago |
2-28130 2 days ago |
132-38296 132 days |
| 32766 |
mcdoll author:mcdoll |
feat(Analysis/TemperedDistribution): embedding of temperate growth functions |
Every temperate growth function defines a tempered distribution via integration.
---
[](https://gitpod.io/from-referrer/)
|
t-analysis |
19/1 |
Mathlib/Analysis/Distribution/TemperedDistribution.lean |
1 |
1 |
['github-actions'] |
nobody |
2-26431 2 days ago |
2-27600 2 days ago |
2-27631 2 days |
| 32767 |
mcdoll author:mcdoll |
feat(Analysis/TemperedDistribution): embedding of `Lp`-functions |
We prove that every `Lp` function defines a tempered distribution via integration. This embedding is a continuous linear map and it is injective.
We also record the embedding as a coercion from `Lp` to `TemperedDistribution`.
---
[](https://gitpod.io/from-referrer/)
|
t-analysis |
82/1 |
Mathlib/Analysis/Distribution/TemperedDistribution.lean |
1 |
1 |
['github-actions'] |
nobody |
2-26222 2 days ago |
2-27296 2 days ago |
2-27337 2 days |
| 32768 |
mcdoll author:mcdoll |
feat(Analysis/TemperedDistribution): embedding of Schwartz functions |
Every Schwartz function defines a tempered distribution and this embedding is continuous.
Moreover, we record the embedding as a coercion.
---
[](https://gitpod.io/from-referrer/)
|
t-analysis |
44/1 |
Mathlib/Analysis/Distribution/TemperedDistribution.lean |
1 |
1 |
['github-actions'] |
nobody |
2-26096 2 days ago |
2-26997 2 days ago |
2-27030 2 days |
| 32769 |
mcdoll author:mcdoll |
feat(Analysis/TemperedDistribution): multiplication with temperate growth functions |
The multiplication with a temperate growth function as a continuous linear map on tempered distributions.
---
[](https://gitpod.io/from-referrer/)
|
t-analysis |
80/2 |
Mathlib/Analysis/Distribution/SchwartzSpace.lean,Mathlib/Analysis/Distribution/TemperedDistribution.lean |
2 |
1 |
['github-actions'] |
nobody |
2-25359 2 days ago |
2-25373 2 days ago |
2-25403 2 days |
| 32771 |
tb65536 author:tb65536 |
feat(Algebra/Order/BigOperators/Group): criterion for `m.card ≤ m.toFinset.card + 1` |
This PR gives a criterion `m.card ≤ m.toFinset.card + 1` (note that we always have the inequality `m.toFinset.card ≤ m.card`).
---
[](https://gitpod.io/from-referrer/)
|
t-algebra
t-order
t-data
label:t-algebra$ |
21/0 |
Mathlib/Algebra/Order/BigOperators/Group/Finset.lean |
1 |
1 |
['github-actions'] |
nobody |
2-19011 2 days ago |
2-19275 2 days ago |
2-19248 2 days |
| 32772 |
tb65536 author:tb65536 |
feat(Data/Set/Card): criterion for `s.ncard ≤ (f '' s).ncard + 1` |
This PR gives a criterion `s.ncard ≤ (f '' s).ncard + 1` (note that we always have the inequality `(f '' s).ncard ≤ s.ncard`).
---
[](https://gitpod.io/from-referrer/)
|
t-data |
31/0 |
Mathlib/Data/Set/Card.lean |
1 |
1 |
['github-actions'] |
nobody |
2-16882 2 days ago |
2-16882 2 days ago |
2-16855 2 days |
| 32773 |
Hagb author:Hagb |
feat(Algebra/GroupWithZero/NonZeroDivisors): add some lemmas about multiplication |
Similar with `Is{Left,Right,}Regular.mul`.
---
`Is{Left,Right,}Regular.mul`: https://github.com/leanprover-community/mathlib4/blob/c671bc4215d64bd9cc8a84fdec9a12bd33fdcd26/Mathlib/Algebra/Regular/Basic.lean#L59-L76
[](https://gitpod.io/from-referrer/)
|
t-algebra label:t-algebra$ |
22/0 |
Mathlib/Algebra/GroupWithZero/NonZeroDivisors.lean |
1 |
1 |
['github-actions'] |
nobody |
2-15577 2 days ago |
2-15839 2 days ago |
2-15873 2 days |
| 32775 |
urkud author:urkud |
feat(VitaliFamily): prove `filterAt_enlarge` |
---
[](https://gitpod.io/from-referrer/)
|
t-measure-probability |
17/4 |
Mathlib/MeasureTheory/Covering/VitaliFamily.lean |
1 |
1 |
['github-actions'] |
nobody |
2-15008 2 days ago |
2-15016 2 days ago |
2-15048 2 days |
| 25042 |
alreadydone author:alreadydone |
feat(Topology): restriction/extension of Trivialization and composition with Homeomorph |
---
- [x] depends on: #25041
[](https://gitpod.io/from-referrer/)
|
merge-conflict
t-topology
|
148/2 |
Mathlib/Topology/FiberBundle/Trivialization.lean,Mathlib/Topology/Maps/Basic.lean |
2 |
4 |
['github-actions', 'leanprover-community-bot-assistant', 'mathlib4-dependent-issues-bot', 'mathlib4-merge-conflict-bot'] |
ADedecker assignee:ADedecker |
73-702 2 months ago |
73-703 2 months ago |
134-68375 134 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
---
- [x] depends on: #31548
- [x] depends on: #31547
- [x] depends on: #31558
[](https://gitpod.io/from-referrer/)
|
t-topology |
741/0 |
Mathlib.lean,Mathlib/Data/EReal/Basic.lean,Mathlib/Topology/Semicontinuous.lean,Mathlib/Topology/Sion.lean,docs/references.bib |
5 |
5 |
['github-actions', 'mathlib4-dependent-issues-bot', 'mathlib4-merge-conflict-bot'] |
dwrensha, kmill, thorimur assignee:kmill assignee:dwrensha assignee:thorimur |
2-8853 2 days ago |
2-8853 2 days ago |
4-53333 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 |
7 |
['euprunin', 'github-actions', 'leanprover-radar', 'mathlib4-merge-conflict-bot', 'riccardobrasca'] |
nobody |
2-8513 2 days ago |
2-69480 2 days ago |
7-61231 7 days |
| 32733 |
dleijnse author:dleijnse |
feat(FieldTheory): X^n - t separable iff n nonzero |
In a field `F`, for `t : F` and `n > 0`, we prove that the polynomial `X ^ n - t` is separable if and only if `n` is nonzero in `F`. This generalizes `X_pow_sub_one_separable_iff`, but the extra assumption that `n > 0` is needed (for `n = 0`, the polynomial `X ^ n - t` is separable iff `t` is not `1`).
---
[](https://gitpod.io/from-referrer/)
|
t-algebra
new-contributor
label:t-algebra$ |
13/0 |
Mathlib/FieldTheory/Separable.lean |
1 |
3 |
['dleijnse', 'github-actions', 'wwylele'] |
nobody |
2-6118 2 days ago |
2-73375 2 days ago |
2-73391 2 days |
| 32779 |
sgouezel author:sgouezel |
feat: more consequences of Riesz-Markov-Kakutani |
---
[](https://gitpod.io/from-referrer/)
|
t-measure-probability |
62/3 |
Mathlib/MeasureTheory/Integral/RieszMarkovKakutani/Real.lean |
1 |
1 |
['github-actions'] |
nobody |
2-5907 2 days ago |
2-5916 2 days ago |
2-5947 2 days |
| 32739 |
Rida-Hamadani author:Rida-Hamadani |
chore(SimpleGraph): golf and improve style of `Subwalks.lean` |
maintaining the sub-walks file after the walk split, golfing some proofs
---
[](https://gitpod.io/from-referrer/)
|
t-combinatorics |
11/18 |
Mathlib/Combinatorics/SimpleGraph/Walks/Subwalks.lean |
1 |
1 |
['github-actions'] |
nobody |
2-3702 2 days ago |
2-68334 2 days ago |
2-68411 2 days |
| 32782 |
xroblot author:xroblot |
feat(Cyclotomic): compute the torsion order of a cyclotomic field |
The order of the torsion group of the `n`-th cyclotomic field is `n` if `n` is even and `2n` if `n` is odd.
---
[](https://gitpod.io/from-referrer/)
|
|
113/1 |
Mathlib/Data/Nat/Totient.lean,Mathlib/NumberTheory/Cyclotomic/Basic.lean,Mathlib/NumberTheory/NumberField/Cyclotomic/Basic.lean |
3 |
1 |
['github-actions'] |
nobody |
2-3569 2 days ago |
2-3639 2 days ago |
2-3611 2 days |
| 32784 |
sgouezel author:sgouezel |
feat: more API for FiniteMeasure and ProbabilityMeasure |
---
[](https://gitpod.io/from-referrer/)
|
t-measure-probability |
169/3 |
Mathlib/MeasureTheory/Measure/FiniteMeasure.lean,Mathlib/MeasureTheory/Measure/ProbabilityMeasure.lean,Mathlib/MeasureTheory/Measure/Typeclasses/Probability.lean |
3 |
1 |
['github-actions'] |
nobody |
2-3175 2 days ago |
2-3175 2 days ago |
2-3212 2 days |
| 32786 |
sgouezel author:sgouezel |
feat: construct a bounded continuous map from a continuous compactly supported map |
---
[](https://gitpod.io/from-referrer/)
|
t-topology |
11/2 |
Mathlib/Topology/ContinuousMap/CompactlySupported.lean |
1 |
1 |
['github-actions'] |
nobody |
2-2885 2 days ago |
2-2927 2 days ago |
2-2961 2 days |
| 32724 |
grunweg author:grunweg |
feat: lint against unscoped uses of the linter.flexible option |
We extend the setOption linter to also lint on this option.
To facilitate this, we replace the remaining file-level exceptions by local annotations (and squeeze a few non-terminal simps where doing so seems easy enough).
---
[](https://gitpod.io/from-referrer/)
|
t-linter |
71/34 |
Mathlib/Computability/Halting.lean,Mathlib/Computability/Partrec.lean,Mathlib/Computability/PartrecCode.lean,Mathlib/Computability/Primrec.lean,Mathlib/Computability/TMToPartrec.lean,Mathlib/Data/Seq/Basic.lean,Mathlib/Data/WSeq/Basic.lean,Mathlib/SetTheory/Ordinal/Notation.lean,Mathlib/Tactic/Linter/Style.lean,MathlibTest/LintStyle.lean |
10 |
1 |
['github-actions'] |
nobody |
1-82215 1 day ago |
1-82215 1 day ago |
2-83044 2 days |
| 32793 |
harahu author:harahu |
doc(NumberTheory): fix typos |
Typos found and fixed by Codex.
---
[](https://gitpod.io/from-referrer/)
|
t-number-theory |
29/27 |
Mathlib/NumberTheory/ArithmeticFunction/Zeta.lean,Mathlib/NumberTheory/Cyclotomic/CyclotomicCharacter.lean,Mathlib/NumberTheory/Cyclotomic/PrimitiveRoots.lean,Mathlib/NumberTheory/EllipticDivisibilitySequence.lean,Mathlib/NumberTheory/EulerProduct/Basic.lean,Mathlib/NumberTheory/FLT/Three.lean,Mathlib/NumberTheory/FermatPsp.lean,Mathlib/NumberTheory/LSeries/AbstractFuncEq.lean,Mathlib/NumberTheory/LSeries/Dirichlet.lean,Mathlib/NumberTheory/LSeries/HurwitzZetaOdd.lean,Mathlib/NumberTheory/LSeries/PrimesInAP.lean,Mathlib/NumberTheory/LSeries/ZMod.lean,Mathlib/NumberTheory/LucasLehmer.lean,Mathlib/NumberTheory/MulChar/Basic.lean,Mathlib/NumberTheory/NumberField/CanonicalEmbedding/Basic.lean,Mathlib/NumberTheory/NumberField/CanonicalEmbedding/NormLeOne.lean,Mathlib/NumberTheory/NumberField/CanonicalEmbedding/PolarCoord.lean,Mathlib/NumberTheory/NumberField/Units/DirichletTheorem.lean,Mathlib/NumberTheory/Padics/PadicVal/Basic.lean,Mathlib/NumberTheory/Padics/PadicVal/Defs.lean,Mathlib/NumberTheory/Padics/WithVal.lean,Mathlib/NumberTheory/Pell.lean,Mathlib/NumberTheory/WellApproximable.lean |
23 |
1 |
['github-actions'] |
nobody |
1-79460 1 day ago |
1-79507 1 day ago |
1-81410 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 |
25-9268 25 days ago |
25-9269 25 days ago |
91-66923 91 days |
| 32698 |
farruhx author:farruhx |
feat(List): add aesop / simp annotations to selected lemmas for improved automation |
This PR adds `@[aesop safe]` and `@[simp]` annotations to a set
of List lemmas whose proofs are routine and benefit from standardized
automation. No statements or definitions are changed; only proof annotations
are added.
The lemmas updated in this PR are:
* `or_exists_of_exists_mem_cons`
* `append_subset_of_subset_of_subset`
* `map_subset_iff`
* `append_eq_has_append`
* `append_right_injective`
* `append_left_injective`
* `reverse_surjective`
* `reverse_bijective`
* `mem_getLast?_append_of_mem_getLast?`
* `mem_dropLast_of_mem_of_ne_getLast`
* `idxOf_eq_length_iff`
* `idxOf_append_of_mem`
* `length_eraseP_add_one`
The goal is to make these commonly used lemmas easier for `aesop`-based
automation to resolve, while avoiding any interference with simp-normal-form
lemmas or canonical rewrite rules.
There are no API changes and no new theorems—only improved automation behavior. |
new-contributor
t-data
|
18/1 |
Mathlib/Data/List/Basic.lean |
1 |
5 |
['euprunin', 'farruhx', 'github-actions'] |
nobody |
1-70696 1 day ago |
1-70761 1 day ago |
1-71160 1 day |
| 32330 |
ADedecker author:ADedecker |
feat: postcomposition by a CLM as a CLM on test functions |
---
- [x] depends on: #32368
- [x] depends on: #30239
[](https://gitpod.io/from-referrer/)
|
t-analysis |
38/0 |
Mathlib/Analysis/Distribution/TestFunction.lean |
1 |
n/a |
['github-actions', 'mathlib4-dependent-issues-bot'] |
nobody |
1-69938 1 day ago |
unknown |
unknown |
| 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$ |
143/0 |
Mathlib/Algebra/Category/ModuleCat/Sheaf/Free.lean,Mathlib/Algebra/Category/ModuleCat/Sheaf/Quasicoherent.lean |
2 |
41 |
['WenrongZou', 'dagurtomas', 'erdOne', 'github-actions', 'robin-carlier'] |
nobody |
1-67133 1 day ago |
1-70245 1 day ago |
5-36639 5 days |
| 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'] |
RemyDegenne assignee:RemyDegenne |
1-67119 1 day ago |
5-81324 5 days ago |
5-81612 5 days |
| 32265 |
joelriou author:joelriou |
feat(AlgebraicTopology): finite colimits of finite simplicial sets are finite |
From https://github.com/joelriou/topcat-model-category
---
- [x] depends on: #32201
- [x] depends on: #32202
[](https://gitpod.io/from-referrer/)
|
maintainer-merge
t-algebraic-topology
|
82/0 |
Mathlib.lean,Mathlib/AlgebraicTopology/SimplicialSet/Finite.lean,Mathlib/AlgebraicTopology/SimplicialSet/FiniteColimits.lean,Mathlib/CategoryTheory/FinCategory/Basic.lean |
4 |
5 |
['github-actions', 'mathlib4-dependent-issues-bot', 'mathlib4-merge-conflict-bot', 'robin-carlier'] |
nobody |
1-63276 1 day ago |
1-63276 1 day ago |
1-71498 1 day |
| 32803 |
erdOne author:erdOne |
feat(RIngTheory): more-linear version of `tensorKaehlerEquiv` |
---
[](https://gitpod.io/from-referrer/)
|
t-ring-theory |
74/0 |
Mathlib/RingTheory/Kaehler/TensorProduct.lean |
1 |
1 |
['github-actions'] |
nobody |
1-63168 1 day ago |
1-63207 1 day ago |
1-63207 1 day |
| 32805 |
gasparattila author:gasparattila |
feat(Topology/UniformSpace/Closeds): continuity of closure |
---
[](https://gitpod.io/from-referrer/)
|
t-topology |
51/0 |
Mathlib/Topology/UniformSpace/Closeds.lean,Mathlib/Topology/UniformSpace/Defs.lean |
2 |
1 |
['github-actions'] |
nobody |
1-62140 1 day ago |
1-62143 1 day ago |
1-62177 1 day |
| 32806 |
erdOne author:erdOne |
feat(RingTheory): base change of ideal with flat quotients |
---
[](https://gitpod.io/from-referrer/)
|
t-ring-theory |
108/0 |
Mathlib/RingTheory/Flat/Equalizer.lean |
1 |
1 |
['github-actions'] |
nobody |
1-61401 1 day ago |
1-61408 1 day ago |
1-61439 1 day |
| 32802 |
erdOne author:erdOne |
feat(RingTheory): more ergonomic version of jacobi criterion for smoothness |
---
[](https://gitpod.io/from-referrer/)
|
t-ring-theory |
125/2 |
Mathlib/RingTheory/Extension/Basic.lean,Mathlib/RingTheory/Extension/Cotangent/Basic.lean,Mathlib/RingTheory/Smooth/Local.lean |
3 |
1 |
['github-actions'] |
nobody |
1-61320 1 day ago |
1-63678 1 day ago |
1-63710 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/)
|
maintainer-merge
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 |
4 |
['JovanGerb', 'github-actions', 'mathlib4-merge-conflict-bot'] |
pechersky assignee:pechersky |
1-60746 1 day ago |
1-60746 1 day ago |
6-32278 6 days |
| 32808 |
gasparattila author:gasparattila |
feat(Topology/Maps): add `IsClosedEmbedding.of_comp` |
---
[](https://gitpod.io/from-referrer/)
|
t-topology |
7/0 |
Mathlib/Topology/Maps/Basic.lean |
1 |
1 |
['github-actions'] |
nobody |
1-59870 1 day ago |
1-59870 1 day ago |
1-59910 1 day |
| 32737 |
j-loreaux author:j-loreaux |
refactor: rename `MulAction` to `MonoidAction` |
Given that we now have [SemigroupAction](https://leanprover-community.github.io/mathlib4_docs/Mathlib/Algebra/Group/Action/Defs.html#SemigroupAction) we are in the unfortunate scenario that the name which seems to have less structure actually has *more* structure. This PR:
1. renames `MulAction` to `MonoidAction` to reflect this additional structure, as well as declarations referencing `MulAction` in their names.
2. does *not* rename modules with `MulAction` in the name
3. does *not* rename `DistribMulAction`, `SubMulAction`, `MulActionWithZero`, etc. If these need to happen, that can occur at a later time.
4. does *not* rename `SemigroupAction` to `MulAction`. Even if this rename is desired, because of the prevalence of `MulAction` in Mathlib, I think we should not conduct a move of this magnitude all at once. If we want to rename this to `MulAction`, we should wait for the 6 month embargo period during which time that name is deprecated, to give everyone downstream the opportunity to switch instead of silently breaking their builds.
Of course, another potential name is `MulOneAction`, but I don't think that's too helpful.
---
[](https://gitpod.io/from-referrer/)
|
|
1797/1745 |
Mathlib/Algebra/AddConstMap/Basic.lean,Mathlib/Algebra/AddTorsor/Basic.lean,Mathlib/Algebra/AddTorsor/Defs.lean,Mathlib/Algebra/Algebra/Equiv.lean,Mathlib/Algebra/Algebra/NonUnitalHom.lean,Mathlib/Algebra/Algebra/Subalgebra/Basic.lean,Mathlib/Algebra/Algebra/Subalgebra/Pointwise.lean,Mathlib/Algebra/Algebra/Tower.lean,Mathlib/Algebra/Algebra/Unitization.lean,Mathlib/Algebra/BigOperators/Group/Finset/Basic.lean,Mathlib/Algebra/BigOperators/Group/Finset/Defs.lean,Mathlib/Algebra/BigOperators/Group/Finset/Pi.lean,Mathlib/Algebra/BigOperators/Group/Finset/Preimage.lean,Mathlib/Algebra/BigOperators/GroupWithZero/Action.lean,Mathlib/Algebra/Category/ModuleCat/ChangeOfRings.lean,Mathlib/Algebra/Category/ModuleCat/FilteredColimits.lean,Mathlib/Algebra/Colimit/DirectLimit.lean,Mathlib/Algebra/Field/Subfield/Basic.lean,Mathlib/Algebra/FreeMonoid/Basic.lean,Mathlib/Algebra/GradedMonoid.lean,Mathlib/Algebra/GradedMulAction.lean,Mathlib/Algebra/Group/Action/Basic.lean,Mathlib/Algebra/Group/Action/Defs.lean,Mathlib/Algebra/Group/Action/End.lean,Mathlib/Algebra/Group/Action/Equidecomp.lean,Mathlib/Algebra/Group/Action/Faithful.lean,Mathlib/Algebra/Group/Action/Hom.lean,Mathlib/Algebra/Group/Action/Opposite.lean,Mathlib/Algebra/Group/Action/Option.lean,Mathlib/Algebra/Group/Action/Pi.lean,Mathlib/Algebra/Group/Action/Pointwise/Finset.lean,Mathlib/Algebra/Group/Action/Pointwise/Set/Basic.lean,Mathlib/Algebra/Group/Action/Pointwise/Set/Finite.lean,Mathlib/Algebra/Group/Action/Pretransitive.lean,Mathlib/Algebra/Group/Action/Prod.lean,Mathlib/Algebra/Group/Action/Sigma.lean,Mathlib/Algebra/Group/Action/Sum.lean,Mathlib/Algebra/Group/Action/TransferInstance.lean,Mathlib/Algebra/Group/Action/TypeTags.lean,Mathlib/Algebra/Group/Action/Units.lean,Mathlib/Algebra/Group/Conj.lean,Mathlib/Algebra/Group/End.lean,Mathlib/Algebra/Group/Equiv/Finite.lean,Mathlib/Algebra/Group/Nat/Range.lean,Mathlib/Algebra/Group/Pointwise/Finset/Basic.lean,Mathlib/Algebra/Group/Pointwise/Finset/Density.lean,Mathlib/Algebra/Group/Pointwise/Finset/Scalar.lean,Mathlib/Algebra/Group/Pointwise/Set/Basic.lean,Mathlib/Algebra/Group/Pointwise/Set/Card.lean,Mathlib/Algebra/Group/Pointwise/Set/Finite.lean,Mathlib/Algebra/Group/Pointwise/Set/Lattice.lean,Mathlib/Algebra/Group/Pointwise/Set/Scalar.lean,Mathlib/Algebra/Group/Shrink.lean,Mathlib/Algebra/Group/Subgroup/Actions.lean,Mathlib/Algebra/Group/Subgroup/Basic.lean,Mathlib/Algebra/Group/Subgroup/Pointwise.lean,Mathlib/Algebra/Group/Submonoid/Membership.lean,Mathlib/Algebra/Group/Submonoid/MulAction.lean,Mathlib/Algebra/Group/Submonoid/Pointwise.lean,Mathlib/Algebra/Group/TransferInstance.lean,Mathlib/Algebra/Group/TypeTags/Finite.lean,Mathlib/Algebra/GroupWithZero/Action/Basic.lean,Mathlib/Algebra/GroupWithZero/Action/ConjAct.lean,Mathlib/Algebra/GroupWithZero/Action/Defs.lean,Mathlib/Algebra/GroupWithZero/Action/End.lean,Mathlib/Algebra/GroupWithZero/Action/Faithful.lean,Mathlib/Algebra/GroupWithZero/Action/Opposite.lean,Mathlib/Algebra/GroupWithZero/Action/Pointwise/Finset.lean,Mathlib/Algebra/GroupWithZero/Action/Pointwise/Set.lean,Mathlib/Algebra/GroupWithZero/Action/Prod.lean,Mathlib/Algebra/GroupWithZero/Action/Units.lean,Mathlib/Algebra/GroupWithZero/NonZeroDivisors.lean,Mathlib/Algebra/GroupWithZero/Pointwise/Finset.lean,Mathlib/Algebra/GroupWithZero/Pointwise/Set/Basic.lean,Mathlib/Algebra/GroupWithZero/Pointwise/Set/Card.lean,Mathlib/Algebra/GroupWithZero/Subgroup.lean,Mathlib/Algebra/GroupWithZero/Submonoid/Pointwise.lean,Mathlib/Algebra/GroupWithZero/TransferInstance.lean,Mathlib/Algebra/GroupWithZero/Units/Lemmas.lean,Mathlib/Algebra/Module/Congruence/Defs.lean,Mathlib/Algebra/Module/Defs.lean,Mathlib/Algebra/Module/Equiv/Basic.lean,Mathlib/Algebra/Module/GradedModule.lean,Mathlib/Algebra/Module/LinearMap/Defs.lean,Mathlib/Algebra/Module/LinearMap/End.lean,Mathlib/Algebra/Module/PUnit.lean,Mathlib/Algebra/Module/PointwisePi.lean,Mathlib/Algebra/Module/Rat.lean,Mathlib/Algebra/Module/Submodule/Basic.lean,Mathlib/Algebra/Module/Submodule/Defs.lean,Mathlib/Algebra/Module/Submodule/Invariant.lean,Mathlib/Algebra/Module/Submodule/LinearMap.lean,Mathlib/Algebra/Module/Submodule/Pointwise.lean,Mathlib/Algebra/Module/ULift.lean,Mathlib/Algebra/Order/Group/Action.lean,Mathlib/Algebra/Order/Group/Action/End.lean,Mathlib/Algebra/Order/Group/Action/Flag.lean,Mathlib/Algebra/Order/Group/Action/Synonym.lean,Mathlib/Algebra/Order/Group/End.lean,Mathlib/Algebra/Order/Module/Defs.lean |
344 |
2 |
['github-actions', 'mathlib4-merge-conflict-bot'] |
nobody |
1-58190 1 day ago |
1-58572 1 day ago |
2-62357 2 days |
| 31138 |
AntoineChambert-Loir author:AntoineChambert-Loir |
feat(LinearAlgebra/Transvection): auxiliary lemmas to compute the determinant of transvection in a module |
Auxiliary results towards the proof that the determinant of a transvection is equal to 1.
---
- [x] depends on: #31164
- [x] depends on: #31165
- [x] depends on: #30987
- [x] depends on: #31078
- [x] depends on: #31162
[](https://gitpod.io/from-referrer/)
|
t-algebra
large-import
label:t-algebra$ |
243/33 |
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 |
7 |
26 |
['AntoineChambert-Loir', 'dagurtomas', 'github-actions', 'mathlib4-dependent-issues-bot', 'mathlib4-merge-conflict-bot', 'ocfnash'] |
dagurtomas assignee:dagurtomas |
1-53564 1 day ago |
1-53704 1 day ago |
3-69014 3 days |
| 32429 |
erdOne author:erdOne |
feat(RingTheory): `IsIntegrallyClosed R[X]` |
---
[](https://gitpod.io/from-referrer/)
|
t-ring-theory |
288/3 |
Mathlib.lean,Mathlib/RingTheory/IntegralClosure/IntegrallyClosed.lean,Mathlib/RingTheory/IntegralClosure/IsIntegral/AlmostIntegral.lean,Mathlib/RingTheory/Polynomial/IsIntegral.lean |
4 |
3 |
['github-actions', 'jcommelin'] |
alreadydone and mattrobball assignee:alreadydone assignee:mattrobball |
1-51832 1 day ago |
9-68125 9 days ago |
9-68278 9 days |
| 32747 |
j-loreaux author:j-loreaux |
feat: integer inequalities from multiples in a strict ordered ring |
These were useful during the review of #32259.
---
[](https://gitpod.io/from-referrer/)
|
t-algebra
maintainer-merge
label:t-algebra$ |
38/0 |
Mathlib.lean,Mathlib/Algebra/Order/Ring/Interval.lean |
2 |
3 |
['github-actions', 'jsm28'] |
nobody |
1-49595 1 day ago |
1-49595 1 day ago |
2-62783 2 days |
| 28411 |
zcyemi author:zcyemi |
feat(LinearAlgebra/AffineSpace/Simplex/Centroid): define centroid and medians |
---
This file proves several lemmas involving the centroids and medians of a simplex in affine space.
definitions:
- `centroid` is the centroid of a simplex, defined as abbreviation of the `Finset.univ.centroid`.
- `faceOppositeCentroid` is the centroid of the facet obtained as `(Simplex.faceOpposite i).centroid`
- `median` is the line connecting a vertex to the faceOppositeCentroid.
Main Results:
- Commandino's theorem
- The medians of a simplex are concurrent at the centroid
- [ ] depends on #29128 |
t-algebra
large-import
label:t-algebra$ |
440/7 |
Mathlib/Geometry/Euclidean/MongePoint.lean,Mathlib/Geometry/Euclidean/Simplex.lean,Mathlib/LinearAlgebra/AffineSpace/Simplex/Centroid.lean,docs/1000.yaml |
4 |
10 |
['github-actions', 'jsm28', 'mathlib4-merge-conflict-bot', 'zcyemi'] |
nobody |
1-49303 1 day ago |
2-12688 2 days ago |
28-6175 28 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 |
9 |
['FLDutchmann', 'JovanGerb', 'github-actions', 'leanprover-radar'] |
kim-em assignee:kim-em |
1-47876 1 day ago |
9-70837 9 days ago |
10-64938 10 days |
| 32813 |
erdOne author:erdOne |
feat(AlgebraicGeometry): relative normalization of schemes |
---
[](https://gitpod.io/from-referrer/)
|
t-algebraic-geometry |
356/0 |
Mathlib.lean,Mathlib/AlgebraicGeometry/IdealSheaf/Basic.lean,Mathlib/AlgebraicGeometry/Normalization.lean,Mathlib/AlgebraicGeometry/Properties.lean |
4 |
1 |
['github-actions'] |
nobody |
1-47286 1 day ago |
1-47286 1 day ago |
1-47323 1 day |
| 30131 |
fpvandoorn author:fpvandoorn |
feat: alias_in attribute |
* A small wrapper for adding an alias of a declaration in another namespace.
* application time `.afterCompilation` is necessary for `#eval` to work correctly
* Docstrings are copied, jump-to-definition works (no test in the test file, but tested locally)
* To be used for CW-complexes, where lemmas are frequently duplicated between `RelCWComplex` and `CWComplex`.
---
[](https://gitpod.io/from-referrer/)
cc @scholzhannah
|
t-meta |
113/0 |
Mathlib.lean,Mathlib/Util/AliasIn.lean,MathlibTest/Util/AliasIn.lean |
3 |
19 |
['JovanGerb', 'fpvandoorn', 'github-actions', 'mathlib4-merge-conflict-bot'] |
JovanGerb assignee:JovanGerb |
1-46825 1 day ago |
1-73627 1 day ago |
49-42987 49 days |
| 32809 |
erdOne author:erdOne |
feat(RingTheory): residue field of `I[X]` |
---
[](https://gitpod.io/from-referrer/)
|
t-ring-theory |
178/1 |
Mathlib.lean,Mathlib/FieldTheory/RatFunc/AsPolynomial.lean,Mathlib/FieldTheory/RatFunc/Basic.lean,Mathlib/RingTheory/Ideal/Quotient/Operations.lean,Mathlib/RingTheory/LocalRing/ResidueField/Polynomial.lean |
5 |
1 |
['github-actions'] |
nobody |
1-46802 1 day ago |
1-46802 1 day ago |
1-55551 1 day |
| 32237 |
joelriou author:joelriou |
feat(AlgebraicTopology): binary products of standard simplices |
We start the study of nondegenerate simplices in `Δ[p] ⊗ Δ[q]`. In particular, we show that it is of dimension `≤ p + q`.
From https://github.com/joelriou/topcat-model-category
---
- [x] depends on: #32201
- [x] depends on: #32202
[](https://gitpod.io/from-referrer/)
|
maintainer-merge
t-algebraic-topology
|
146/0 |
Mathlib.lean,Mathlib/AlgebraicTopology/SimplicialSet/Monoidal.lean,Mathlib/AlgebraicTopology/SimplicialSet/ProdStdSimplex.lean |
3 |
12 |
['github-actions', 'joelriou', 'mathlib4-dependent-issues-bot', 'mathlib4-merge-conflict-bot', 'robin-carlier'] |
nobody |
1-46213 1 day ago |
1-46213 1 day ago |
1-60890 1 day |
| 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
maintainer-merge
large-import
|
4/7 |
Mathlib/Tactic/TypeStar.lean |
1 |
5 |
['JovanGerb', 'github-actions', 'mathlib4-dependent-issues-bot', 'mathlib4-merge-conflict-bot'] |
dwrensha assignee:dwrensha |
1-46053 1 day ago |
1-46053 1 day ago |
12-15043 12 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 |
59 |
['YaelDillies', 'ctchou', 'github-actions', 'lambda-fairy', 'mathlib4-dependent-issues-bot', 'rudynicolop'] |
YaelDillies assignee:YaelDillies |
1-45382 1 day ago |
6-239 6 days ago |
15-81950 15 days |
| 32715 |
chiyunhsu author:chiyunhsu |
feat(Data/Nat/Factorization): add theorems about ordCompl |
Add theorems about ordCompl[p] n, the prime-to-p part of n, when n is a power of p. There are similar existing theorems in Data/Nat/Factorization/PrimePow.lean emphasizing isPrimePow. Motivation of PR is for a follow up PR on Combinatorial Proof of Euler's Partition Identity
---
[](https://gitpod.io/from-referrer/)
|
new-contributor
t-data
|
31/0 |
Mathlib/Data/Nat/BitIndices.lean,Mathlib/Data/Nat/Factorization/Basic.lean |
2 |
10 |
['chiyunhsu', 'github-actions', 'jcommelin'] |
nobody |
1-43762 1 day ago |
2-1914 2 days ago |
3-17304 3 days |
| 32820 |
gasparattila author:gasparattila |
feat(Topology/Sets): range of `(Nonempty)Compacts.map` |
---
[](https://gitpod.io/from-referrer/)
|
t-topology |
19/0 |
Mathlib/Topology/Sets/Compacts.lean |
1 |
1 |
['github-actions'] |
nobody |
1-41967 1 day ago |
1-41983 1 day ago |
1-42016 1 day |
| 32749 |
thorimur author:thorimur |
fix: respect visibility in `notation3` |
This PR makes sure that `notation3` respects visibility and does not introduce public declarations when preceded by `local`. In particular:
* we pass along the `attrKind` to `macro_rules`, thereby making them `local` when the `notation3` is (and therefore making sure their associated declaration under the hood is private)
* we use a `private aux_def` when the `attrKind` is `local` (and `public` otherwise, for `scoped` or none)
Note that, like `syntax` and `notation`, the declarations created by `notation3` will be `public` even when not in `public section`. Visibility for meta commands like these is controlled by `local`.
This was discovered because `local notation3` introduced public declarations which wrongly silenced the private module linter. We therefore include a test for the private module linter.
---
[](https://gitpod.io/from-referrer/)
|
t-meta |
42/3 |
Mathlib/Util/Notation3.lean,MathlibTest/PrivateModuleLinter/notation3.lean |
2 |
1 |
['github-actions'] |
nobody |
1-41577 1 day ago |
2-31713 2 days ago |
2-35895 2 days |
| 32818 |
tb65536 author:tb65536 |
refactor(Algebra/Polynomial/Splits): continue deprecation |
This PR continues the deprecation in Splits.lean as we move over to the new API in Factors.lean.
---
[](https://gitpod.io/from-referrer/)
|
t-algebra label:t-algebra$ |
52/39 |
Mathlib/Algebra/Polynomial/Factors.lean,Mathlib/Algebra/Polynomial/Splits.lean,Mathlib/FieldTheory/Galois/Basic.lean,Mathlib/FieldTheory/IsAlgClosed/Basic.lean,Mathlib/FieldTheory/Isaacs.lean,Mathlib/FieldTheory/Normal/Basic.lean,Mathlib/RingTheory/Polynomial/GaussLemma.lean |
7 |
1 |
['github-actions'] |
nobody |
1-36318 1 day ago |
1-36318 1 day ago |
1-38097 1 day |
| 30240 |
luigi-massacci author:luigi-massacci |
feat(Analysis/Distribution/ContDiffMapSupportedIn): Add a wrapper for fderiv on D_K^n |
Add a wrapper for `fderiv` as a map from `D_K^n` to `D_K^(n-1)`.
Co-Authored by: @ADedecker
---
- [ ] depends on: #30239
- [ ] depends on: #30236
- [ ] depends on: #30202
- [ ] depends on: #30201
- [ ] depends on: #30199
- [ ] depends on: #30198
- [ ] depends on: #30197
[](https://gitpod.io/from-referrer/)
|
blocked-by-other-PR
t-analysis
|
379/16 |
Mathlib/Analysis/Distribution/ContDiffMapSupportedIn.lean |
1 |
6 |
['ADedecker', 'github-actions', 'mathlib4-dependent-issues-bot', 'mathlib4-merge-conflict-bot'] |
nobody |
21-78929 21 days ago |
24-83029 24 days ago |
0-546 9 minutes |
| 32210 |
ADedecker author:ADedecker |
feat: iteratedFDeriv as a linear map on test functions |
Add `TestFunction.iteratedFDeriv[WithOrder]LM`, analogous to [ContDiffMapSupportedIn.iteratedFDerivWithOrderLM](https://leanprover-community.github.io/mathlib4_docs/Mathlib/Analysis/Distribution/ContDiffMapSupportedIn.html#ContDiffMapSupportedIn.iteratedFDerivWithOrderLM) and [ContDiffMapSupportedIn.iteratedFDerivLM](https://leanprover-community.github.io/mathlib4_docs/Mathlib/Analysis/Distribution/ContDiffMapSupportedIn.html#ContDiffMapSupportedIn.iteratedFDerivLM)
---
Co-authored-by: @luigi-massacci
[](https://gitpod.io/from-referrer/)
|
t-analysis |
109/2 |
Mathlib/Analysis/Distribution/TestFunction.lean |
1 |
2 |
['github-actions', 'mathlib4-merge-conflict-bot'] |
nobody |
12-76256 12 days ago |
12-83561 12 days ago |
15-71358 15 days |
| 32521 |
j-loreaux author:j-loreaux |
refactor: generalize semicontinuity |
---
I will split this if the general idea receives approval.
[](https://gitpod.io/from-referrer/)
|
t-topology
file-removed
|
946/342 |
Mathlib.lean,Mathlib/Analysis/LocallyConvex/Barrelled.lean,Mathlib/MeasureTheory/Constructions/BorelSpace/Order.lean,Mathlib/MeasureTheory/Integral/Bochner/VitaliCaratheodory.lean,Mathlib/Topology/EMetricSpace/BoundedVariation.lean,Mathlib/Topology/Instances/EReal/Lemmas.lean,Mathlib/Topology/Semicontinuity/Basic.lean,Mathlib/Topology/Semicontinuity/Defs.lean,Mathlib/Topology/Semicontinuity/Hemicontinuity.lean |
9 |
4 |
['alreadydone', 'github-actions', 'mathlib4-merge-conflict-bot', 'vihdzp'] |
PatrickMassot assignee:PatrickMassot |
1-33932 1 day ago |
1-61605 1 day ago |
4-59044 4 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 |
2 |
['JovanGerb', 'github-actions'] |
jcommelin assignee:jcommelin |
1-33931 1 day ago |
4-80736 4 days ago |
5-63479 5 days |
| 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 |
4 |
['github-actions', 'goliath-klein', 'kbuzzard'] |
dwrensha assignee:dwrensha |
1-33930 1 day ago |
4-57795 4 days ago |
4-58056 4 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'] |
chrisflav assignee:chrisflav |
1-33930 1 day ago |
5-20413 5 days ago |
5-23030 5 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'] |
TwoFX assignee:TwoFX |
1-33928 1 day ago |
4-56141 4 days ago |
4-56182 4 days |
| 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'] |
PatrickMassot assignee:PatrickMassot |
1-33927 1 day ago |
4-45523 4 days ago |
4-45557 4 days |
| 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'] |
kbuzzard assignee:kbuzzard |
1-33926 1 day ago |
4-39360 4 days ago |
4-39380 4 days |
| 32823 |
erdOne author:erdOne |
feat(RingTheory): construct etale neighborhood that isolates point in fiber |
---
[](https://gitpod.io/from-referrer/)
|
t-ring-theory |
280/1 |
Mathlib.lean,Mathlib/Algebra/Polynomial/Monic.lean,Mathlib/RingTheory/Etale/QuasiFinite.lean,Mathlib/RingTheory/Polynomial/UniversalFactorizationRing.lean,Mathlib/RingTheory/Spectrum/Prime/Noetherian.lean,Mathlib/RingTheory/Spectrum/Prime/RingHom.lean,Mathlib/RingTheory/Spectrum/Prime/Topology.lean |
7 |
1 |
['github-actions'] |
nobody |
1-33842 1 day ago |
1-33842 1 day ago |
1-34047 1 day |
| 32811 |
erdOne author:erdOne |
feat(RingTheory): predicate on satisfying Zariski's main theorem |
---
[](https://gitpod.io/from-referrer/)
|
t-ring-theory |
169/0 |
Mathlib.lean,Mathlib/Algebra/Algebra/Subalgebra/Lattice.lean,Mathlib/RingTheory/Localization/Away/Basic.lean,Mathlib/RingTheory/ZariskisMainTheorem.lean |
4 |
2 |
['github-actions'] |
nobody |
1-33790 1 day ago |
1-52451 1 day ago |
1-52934 1 day |
| 32826 |
felixpernegger author:felixpernegger |
feat(Data/Tuple/Sort): Sort of perm is its inverse |
One can use this to easily prove a permutation is monotone iff it is the identity. However I'm still unsure in what file to put that theorem. |
new-contributor
t-data
|
10/0 |
Mathlib/Data/Fin/Tuple/Sort.lean |
1 |
1 |
['github-actions'] |
nobody |
1-27053 1 day ago |
1-27053 1 day ago |
1-27057 1 day |
| 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/)
|
t-combinatorics |
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 |
1-19777 1 day ago |
1-19783 1 day ago |
5-13160 5 days |
| 32754 |
felixpernegger author:felixpernegger |
feat(Data/Set/Card): ncard of complement of set is Nat.card - ncard of set |
|
easy
new-contributor
maintainer-merge
t-data
|
4/0 |
Mathlib/Data/Set/Card.lean |
1 |
3 |
['felixpernegger', 'github-actions', 'tb65536'] |
nobody |
1-18569 1 day ago |
1-18569 1 day ago |
2-54472 2 days |
| 32828 |
Hagb author:Hagb |
feat(Algebra/Order/Group/Defs): add `IsOrderedAddMonoid.toIsOrderedCancelAddMonoid'` |
It is similar to `IsOrderedAddMonoid.toIsOrderedCancelAddMonoid`, while with different hypotheses.
The conclusion `IsOrderedCancelMonoid α` on
`IsOrderedAddMonoid.toIsOrderedCancelAddMonoid` still holds when the hypothesis `CommGroup α` is weakened to `CancelCommMonoid α` while `PartialOrder α` is strengthened to `LinearOrder α`.
---
[`IsOrderedAddMonoid.toIsOrderedCancelAddMonoid`](https://leanprover-community.github.io/mathlib4_docs/find/?pattern=IsOrderedAddMonoid.toIsOrderedCancelAddMonoid#doc) and `IsOrderedAddMonoid.toIsOrderedCancelAddMonoid'`:
https://github.com/leanprover-community/mathlib4/blob/97f78b1a4311fed1844b94f1c069219a48a098e1/Mathlib/Algebra/Order/Group/Defs.lean#L52-L62
[](https://gitpod.io/from-referrer/)
|
t-algebra label:t-algebra$ |
4/0 |
Mathlib/Algebra/Order/Group/Defs.lean |
1 |
1 |
['github-actions'] |
nobody |
1-10253 1 day ago |
1-23285 1 day ago |
1-23316 1 day |
| 32794 |
YuvalFilmus author:YuvalFilmus |
feat(Arcosh): continuity, differentiability, bijectivity |
We show that arcosh is continuous, differentiable, and continuously differentiable infinitely many times.
We also show that cosh and arcosh are bijective, injective, and surjective.
All of these, on the respective domains.
---
[](https://gitpod.io/from-referrer/)
|
t-analysis |
106/2 |
Mathlib/Analysis/SpecialFunctions/Arcosh.lean,Mathlib/Analysis/SpecialFunctions/Arsinh.lean |
2 |
8 |
['SnirBroshi', 'YuvalFilmus', 'github-actions', 'metakunt'] |
nobody |
1-7678 1 day ago |
1-75576 1 day ago |
1-75613 1 day |
| 32231 |
grunweg author:grunweg |
chore: use the to_fun attribute |
Reduce code duplication using the to_fun attribute.
This is not exhaustive, neither does it constitute an endorsement "we always want to generate the applied form of a lemma".
---
This may also want to wait until copying doc-strings is supported (to avoid regressions on that front),
and until the generated declaration is hoverable (for easier migration to the attribute).
- [x] depends on: #31872
[](https://gitpod.io/from-referrer/)
|
|
78/261 |
Mathlib/Analysis/Analytic/Constructions.lean,Mathlib/Analysis/Meromorphic/Basic.lean |
2 |
7 |
['JovanGerb', 'github-actions', 'grunweg', 'mathlib4-dependent-issues-bot', 'mathlib4-merge-conflict-bot'] |
joneugster assignee:joneugster |
1-4770 1 day ago |
3-40287 3 days ago |
12-5144 12 days |
| 32760 |
grunweg author:grunweg |
feat: inclusion of an open submanifold is an immersion |
---
[](https://gitpod.io/from-referrer/)
|
t-differential-geometry |
49/6 |
Mathlib/Geometry/Manifold/ChartedSpace.lean,Mathlib/Geometry/Manifold/Immersion.lean,Mathlib/Topology/OpenPartialHomeomorph/Constructions.lean |
3 |
3 |
['github-actions', 'grunweg'] |
nobody |
1-4021 1 day ago |
1-4026 1 day ago |
1-3999 1 day |
| 32837 |
erdOne author:erdOne |
feat(RingTheory): noetherian model for etale algebras |
---
[](https://gitpod.io/from-referrer/)
|
large-import
t-ring-theory
|
173/12 |
Mathlib/RingTheory/Extension/Presentation/Core.lean,Mathlib/RingTheory/Smooth/NoetherianDescent.lean |
2 |
1 |
['github-actions'] |
nobody |
1-345 1 day ago |
1-345 1 day ago |
1-383 1 day |
| 32684 |
Parcly-Taxel author:Parcly-Taxel |
feat: a simple unit-distance embedding of the Heawood graph |
Cf. [Zulip](https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/A.20simple.20unit-distance.20embedding.20of.20the.20Heawood.20graph/near/562930187). 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 |
330/0 |
Counterexamples.lean,Counterexamples/HeawoodUnitDistance.lean,Mathlib.lean,Mathlib/Combinatorics/SimpleGraph/UnitDistance/Basic.lean,docs/references.bib |
5 |
22 |
['Parcly-Taxel', 'SnirBroshi', 'alreadydone', 'b-mehta', 'github-actions'] |
nobody |
0-83032 23 hours ago |
3-83994 3 days ago |
3-84036 3 days |
| 32841 |
0xTerencePrime author:0xTerencePrime |
feat(Analysis/Normed/Group/Seminorm): define SupSet instances |
## Summary
This PR implements `SupSet` instances for `GroupSeminorm` and `NonarchAddGroupSeminorm`, enabling computation of suprema over sets of seminorms.
## Changes
- **`GroupSeminorm`**: Added `SupSet` instance. For bounded sets, returns pointwise supremum; for unbounded/empty sets, returns zero seminorm.
- **`NonarchAddGroupSeminorm`**: Added analogous `SupSet` instance.
- **`GroupNorm`**: Added explanatory comment explaining why `SupSet` is not implemented (no canonical bottom element for `sSup ∅`).
## Implementation Notes
The implementation handles:
- Bounded non-empty sets: `⨆ p : s, p.1 x`
- Empty sets: `Real.sSup_empty` gives 0
- Unbounded sets: Returns zero seminorm
For `GroupNorm`, the zero function is not a valid norm (fails definiteness `p(x) = 0 ↔ x = 1`), and while a discrete norm could work, its proofs are complex. This is left as future work.
## Related Issues
Addresses part of #7987
## Verification
- [x] `lake build Mathlib.Analysis.Normed.Group.Seminorm` passes
- [x] `lake exe runLinter Mathlib.Analysis.Normed.Group.Seminorm` passes
- [x] Full `lake build` passes |
t-analysis
new-contributor
|
90/5 |
Mathlib/Analysis/Normed/Group/Seminorm.lean |
1 |
1 |
['github-actions'] |
nobody |
0-82296 22 hours ago |
0-82296 22 hours ago |
0-82334 22 hours |
| 32838 |
YaelDillies author:YaelDillies |
feat(Algebra): localising a torsion-free module at regular elements |
---
[](https://gitpod.io/from-referrer/)
|
t-algebra label:t-algebra$ |
28/1 |
Mathlib/Algebra/Module/LocalizedModule/Basic.lean |
1 |
1 |
['github-actions'] |
nobody |
0-79500 22 hours ago |
1-215 1 day ago |
1-244 1 day |
| 32712 |
erdOne author:erdOne |
feat(Logic/Equiv): `Option α × β ≃ β ⊕ α × β` |
---
[](https://gitpod.io/from-referrer/)
|
t-logic |
40/6 |
Mathlib/Logic/Equiv/Prod.lean |
1 |
2 |
['github-actions', 'vihdzp'] |
nobody |
0-79340 22 hours ago |
3-25823 3 days ago |
3-25863 3 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
maintainer-merge
large-import
|
224/5 |
Mathlib.lean,Mathlib/NumberTheory/ModularForms/EisensteinSeries/E2/Defs.lean,Mathlib/NumberTheory/ModularForms/EisensteinSeries/E2/Summable.lean,Mathlib/Topology/Algebra/InfiniteSum/ConditionalInt.lean |
4 |
25 |
['CBirkbeck', 'github-actions', 'loefflerd'] |
nobody |
0-78939 21 hours ago |
0-83213 23 hours ago |
4-2934 4 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
maintainer-merge
t-convex-geometry
|
90/0 |
Mathlib/Geometry/Convex/Cone/Basic.lean |
1 |
17 |
['bjornsolheim', 'github-actions', 'ocfnash'] |
nobody |
0-78651 21 hours ago |
0-78651 21 hours ago |
11-77304 11 days |
| 32843 |
YaelDillies author:YaelDillies |
chore(GroupTheory/Torsion): delete deprecated declarations |
These are on my way for #30563.
---
[](https://gitpod.io/from-referrer/)
|
t-group-theory |
0/135 |
Mathlib/GroupTheory/Torsion.lean |
1 |
1 |
['github-actions'] |
nobody |
0-78632 21 hours ago |
0-78638 21 hours ago |
0-78674 21 hours |
| 32254 |
YaelDillies author:YaelDillies |
feat(Algebra/MonoidAlgebra): complete the map API |
Add congruence isomorphisms in both the ring and monoid arguments. Move `mapRangeRingHom` from `Algebra.MonoidAlgebra.Lift` to `Algebra.MonoidAlgebra.MapDomain` and make its proofs additivisable (by not using `lift`). Make `mapDomainRingHom` take a `MonoidHom` rather than `MonoidHomClass`.
---
- [x] depends on: #32486
[](https://gitpod.io/from-referrer/)
|
t-algebra label:t-algebra$ |
236/118 |
Mathlib/Algebra/MonoidAlgebra/Basic.lean,Mathlib/Algebra/MonoidAlgebra/Lift.lean,Mathlib/Algebra/MonoidAlgebra/MapDomain.lean,Mathlib/Algebra/Polynomial/Laurent.lean,Mathlib/RingTheory/Polynomial/Opposites.lean |
5 |
25 |
['YaelDillies', 'eric-wieser', 'github-actions', 'jcommelin', 'mathlib4-dependent-issues-bot', 'mathlib4-merge-conflict-bot'] |
nobody |
0-78164 21 hours ago |
0-79934 22 hours ago |
7-73367 7 days |
| 32846 |
jonasvanderschaaf author:jonasvanderschaaf |
feat(CategoryTheory): Prove thin categories with finite/countable objects are countable |
Prove thin categories with finite/countable objects are countable.
---
[](https://gitpod.io/from-referrer/)
|
t-category-theory
new-contributor
large-import
|
8/1 |
Mathlib/CategoryTheory/Countable.lean,Mathlib/CategoryTheory/FinCategory/Basic.lean |
2 |
1 |
['github-actions'] |
nobody |
0-74903 20 hours ago |
0-74911 20 hours ago |
0-74945 20 hours |
| 7596 |
alreadydone author:alreadydone |
feat: covering maps from properly discontinuous actions and discrete subgroups |
---
- [x] depends on: #23236
- [x] depends on: #32681
- [x] depends on: #32693
- [x] depends on: #32691
[](https://gitpod.io/from-referrer/)
|
t-topology |
448/18 |
Mathlib.lean,Mathlib/Algebra/Group/Action/Pointwise/Set/Basic.lean,Mathlib/Algebra/Group/Submonoid/MulAction.lean,Mathlib/Analysis/SpecialFunctions/Complex/Circle.lean,Mathlib/GroupTheory/GroupAction/SubMulAction.lean,Mathlib/Tactic/Translate/ToAdditive.lean,Mathlib/Topology/Algebra/ConstMulAction.lean,Mathlib/Topology/Algebra/Group/Pointwise.lean,Mathlib/Topology/Covering/AddCircle.lean,Mathlib/Topology/Covering/Basic.lean,Mathlib/Topology/Covering/Quotient.lean,Mathlib/Topology/Instances/AddCircle/Defs.lean |
12 |
44 |
['ADedecker', 'alreadydone', 'digama0', 'github-actions', 'grunweg', 'leanprover-community-bot-assistant', 'mathlib4-dependent-issues-bot', 'mathlib4-merge-conflict-bot', 'ocfnash', 'tb65536'] |
ocfnash assignee:ocfnash |
0-74833 20 hours ago |
2-9465 2 days ago |
76-45455 76 days |
| 32603 |
themathqueen author:themathqueen |
chore(Algebra/Azumaya/Basic): clean up imports |
Follow-up to #28100.
---
[](https://gitpod.io/from-referrer/)
|
t-algebra label:t-algebra$ |
4/5 |
Mathlib/Algebra/Azumaya/Basic.lean |
1 |
1 |
['github-actions'] |
dagurtomas assignee:dagurtomas |
0-72687 20 hours ago |
5-51358 5 days ago |
5-51648 5 days |
| 32847 |
gasparattila author:gasparattila |
feat: `SetRel.(pre)image` of `iUnion` and `sUnion` |
---
[](https://gitpod.io/from-referrer/)
|
easy
t-data
|
12/0 |
Mathlib/Data/Rel.lean |
1 |
2 |
['gasparattila', 'github-actions'] |
nobody |
0-71754 19 hours ago |
0-71756 19 hours ago |
0-71794 19 hours |
| 32804 |
vihdzp author:vihdzp |
feat: more lemmas on `LinearOrderedAddCommGroupWithTop` |
---
[](https://gitpod.io/from-referrer/)
|
t-algebra label:t-algebra$ |
29/17 |
Mathlib/Algebra/Order/AddGroupWithTop.lean |
1 |
1 |
['github-actions', 'wwylele'] |
nobody |
0-71132 19 hours ago |
1-62426 1 day ago |
1-62463 1 day |
| 32832 |
0xTerencePrime author:0xTerencePrime |
fix(Order/Interval): simplify Ioo lemmas under DenselyOrdered + LocallyFinite |
## Summary
This PR addresses part of #7987 by simplifying lemmas that have contradictory assumptions (`DenselyOrdered` + `LocallyFiniteOrder`).
## Changes
### `Mathlib/Order/Interval/Finset/Basic.lean`
- Added `Ioo_eq_empty_of_denselyOrdered_of_locallyFinite` lemma
- Simplified `nonempty_Ioo` to `(Ioo a b).Nonempty ↔ False`
- Simplified `Ioo_eq_empty_iff` to `Ioo a b = ∅ ↔ True`
- Removed TODO comments
### `Mathlib/Order/Interval/Multiset.lean`
- Updated `Ioo_eq_zero_iff` to match new Finset semantics
- Fixed implicit argument inference in `Ico_filter_lt_*` lemmas
## Mathematical Background
A type cannot be both `DenselyOrdered` and `LocallyFiniteOrder` with distinct elements. The existing `not_lt_of_denselyOrdered_of_locallyFinite` proves `¬ a < b`, which this PR uses to simplify related lemmas.
## Verification
- [x] `lake build` passes (7741 jobs)
- [x] `lake exe runLinter` passes |
t-order
new-contributor
|
28/16 |
Mathlib/Order/Interval/Finset/Basic.lean,Mathlib/Order/Interval/Multiset.lean |
2 |
1 |
['github-actions'] |
nobody |
0-68721 19 hours ago |
1-4909 1 day ago |
1-4943 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$ |
320/1 |
Mathlib.lean,Mathlib/Algebra/Order/Ring/Archimedean.lean,Mathlib/Algebra/Order/Ring/StandardPart.lean,Mathlib/Order/Quotient.lean |
4 |
52 |
['YaelDillies', 'github-actions', 'mathlib4-dependent-issues-bot', 'mathlib4-merge-conflict-bot', 'plp127', 'vihdzp', 'wwylele'] |
joneugster assignee:joneugster |
0-65443 18 hours ago |
0-75742 21 hours ago |
11-54847 11 days |
| 32792 |
plp127 author:plp127 |
feat(Topology): uniformity has linearly ordered basis implies completely normal |
Prove if the uniformity has linearly ordered basis then the space is completely normal. Golf a proof, and reduce imports.
---
[](https://gitpod.io/from-referrer/)
|
t-topology |
45/17 |
Mathlib/MeasureTheory/Measure/Regular.lean,Mathlib/Topology/GDelta/MetrizableSpace.lean,Mathlib/Topology/UniformSpace/Separation.lean |
3 |
1 |
['github-actions'] |
nobody |
0-62022 17 hours ago |
1-83459 1 day ago |
1-83439 1 day |
| 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 |
737/596 |
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 |
51 |
['callesonne', 'dagurtomas', 'edegeltje', 'github-actions', 'joelriou', 'mathlib4-merge-conflict-bot'] |
erdOne assignee:erdOne |
0-61514 17 hours ago |
0-61515 17 hours ago |
14-46490 14 days |
| 32849 |
plp127 author:plp127 |
feat: `UniformSpace.subset_countable_closure_of_almost_dense_set` |
Add the new theorem `UniformSpace.subset_countable_closure_of_almost_dense_set` and golf the `PseudoEMetricSpace` version with it. Move some stuff around:
- `IsSeparable.exists_countable_dense_subset` and `IsSeparable.separableSpace` are generalized to pseudometrizable spaces and moved to `Metrizable/Basic`.
- `TotallyBounded.isSeparable` is moved to `UniformSpace/Cauchy`
- `EMetric.subset_countable_closure_of_almost_dense_set` is moved to `EMetric/Basic`
---
[](https://gitpod.io/from-referrer/)
|
t-topology |
93/89 |
Mathlib/Topology/EMetricSpace/Basic.lean,Mathlib/Topology/EMetricSpace/Defs.lean,Mathlib/Topology/MetricSpace/Pseudo/Basic.lean,Mathlib/Topology/Metrizable/Basic.lean,Mathlib/Topology/Metrizable/Uniformity.lean,Mathlib/Topology/UniformSpace/Basic.lean,Mathlib/Topology/UniformSpace/Cauchy.lean |
7 |
1 |
['github-actions'] |
nobody |
0-60276 16 hours ago |
0-60276 16 hours ago |
0-61208 17 hours |
| 32814 |
joelriou author:joelriou |
feat(Algebra/Homology): equivOfIsKInjective |
We construct a bijection `CohomologyClass K L n ≃ SmallShiftedHom.{w} (HomologicalComplex.quasiIso C (.up ℤ)) K L n` when `K` and `L` are cochain complexes, and `L` is `K`-injective, or `K` is `K`-projective.
---
[](https://gitpod.io/from-referrer/)
|
t-category-theory
large-import
|
96/5 |
Mathlib/Algebra/Homology/DerivedCategory/KInjective.lean,Mathlib/Algebra/Homology/DerivedCategory/KProjective.lean,Mathlib/Algebra/Homology/Embedding/IsSupported.lean,Mathlib/CategoryTheory/Abelian/Injective/Extend.lean,Mathlib/CategoryTheory/Abelian/Projective/Extend.lean |
5 |
5 |
['github-actions', 'joelriou', 'mathlib4-merge-conflict-bot', 'metakunt'] |
nobody |
0-58169 16 hours ago |
0-58193 16 hours ago |
1-40649 1 day |
| 32835 |
vasnesterov author:vasnesterov |
fix(Tactic/Order): equal but not syntactically equal types |
When collecting atoms, `order` relies only on syntactic equality of types. This PR replaces this with defeq check and adds a test that failed before.
---
[](https://gitpod.io/from-referrer/)
|
bug
t-meta
|
18/1 |
Mathlib/Tactic/Order/CollectFacts.lean,MathlibTest/order.lean |
2 |
1 |
['artie2000', 'github-actions'] |
nobody |
0-56068 15 hours ago |
0-76083 21 hours ago |
0-76070 21 hours |
| 31505 |
dsfxcimk author:dsfxcimk |
feat: Add some oangle theorems |
Add several theorems relating oriented angles and affine independence / collinearity, together with auxiliary lemmas about the equality and sign of oriented angles.
Main additions
`oangle_ne_zero_and_ne_pi_iff_not_collinear`
– An oriented angle is neither `0` nor `π` if and only if the three points are not collinear.
`affineIndependent_iff_of_oangle_eq`
– If two oriented angles are equal, then the corresponding triples of points are affinely independent simultaneously.
`not_collinear_iff_of_angle_eq`
– If two oriented angles are equal, one triple is collinear if and only if the other is.
`oangle_eq_or_eq_neg_of_angle_eq`
– The oriented angles are equal or opposite if the unoriented angles are equal.
`angle_eq_neg_of_two_zsmul_angle_eq`
– If `2 • a = 2 • b` and the signs are opposite, then `a = b + π.`
`two_zsmul_eq_iff_eq`
– Characterizes equality of doubled angles when signs are equal.
`oangle_sub_oangle_ne_pi_of_not_collinear`
– If the signs of two oriented angles are equal and the points are not collinear, their difference is not `π`. |
t-euclidean-geometry
new-contributor
maintainer-merge
|
55/0 |
Mathlib/Analysis/SpecialFunctions/Trigonometric/Angle.lean,Mathlib/Geometry/Euclidean/Angle/Oriented/Affine.lean |
2 |
35 |
['dsfxcimk', 'github-actions', 'jsm28'] |
nobody |
0-55381 15 hours ago |
0-55381 15 hours ago |
3-65203 3 days |
| 32703 |
chrisflav author:chrisflav |
chore(RingTheory): rename `RingHom.specComap` to `PrimeSpectrum.comap` |
and remove the old `PrimeSpectrum.comap`, which was `RingHom.specComap` bundled as a continuous map.
Having both `RingHom.specComap` and `PrimeSpectrum.comap` leads to two ways of writing the same thing, with every lemma written before the topology-on-`PrimeSpectrum`-barrier stated in terms of `RingHom.specComap` and most lemmas after it stated in terms of `PrimeSpectrum.comap`. Since the bundled continuous map version is not useful, because the topology library rarely takes continuous maps as input, we remove the bundled version, but keep the name `PrimeSpectrum.comap` for the unbundled one.
---
[](https://gitpod.io/from-referrer/)
|
maintainer-merge
t-ring-theory
|
195/182 |
Mathlib/AlgebraicGeometry/GammaSpecAdjunction.lean,Mathlib/AlgebraicGeometry/IdealSheaf/Basic.lean,Mathlib/AlgebraicGeometry/Morphisms/OpenImmersion.lean,Mathlib/AlgebraicGeometry/Morphisms/UniversallyClosed.lean,Mathlib/AlgebraicGeometry/Scheme.lean,Mathlib/AlgebraicGeometry/Spec.lean,Mathlib/AlgebraicGeometry/StructureSheaf.lean,Mathlib/RingTheory/Flat/FaithfullyFlat/Algebra.lean,Mathlib/RingTheory/Ideal/GoingDown.lean,Mathlib/RingTheory/Ideal/KrullsHeightTheorem.lean,Mathlib/RingTheory/KrullDimension/Polynomial.lean,Mathlib/RingTheory/LocalRing/ResidueField/Fiber.lean,Mathlib/RingTheory/RingHom/FaithfullyFlat.lean,Mathlib/RingTheory/Spectrum/Maximal/Localization.lean,Mathlib/RingTheory/Spectrum/Prime/Chevalley.lean,Mathlib/RingTheory/Spectrum/Prime/ChevalleyComplexity.lean,Mathlib/RingTheory/Spectrum/Prime/ConstructibleSet.lean,Mathlib/RingTheory/Spectrum/Prime/FreeLocus.lean,Mathlib/RingTheory/Spectrum/Prime/Homeomorph.lean,Mathlib/RingTheory/Spectrum/Prime/Polynomial.lean,Mathlib/RingTheory/Spectrum/Prime/RingHom.lean,Mathlib/RingTheory/Spectrum/Prime/TensorProduct.lean,Mathlib/RingTheory/Spectrum/Prime/Topology.lean,docs/1000.yaml |
24 |
9 |
['chrisflav', 'erdOne', 'github-actions', 'leanprover-radar'] |
nobody |
0-54727 15 hours ago |
0-54727 15 hours ago |
3-43656 3 days |
| 32801 |
Hagb author:Hagb |
feat(RingTheory/MvPolynomial/Ideal): `sPolynomial` preserves ideal membership |
It will be used by Buchberger's Criterion (in #29203).
---
[](https://gitpod.io/from-referrer/)
|
maintainer-merge
t-ring-theory
|
10/0 |
Mathlib/RingTheory/MvPolynomial/Ideal.lean |
1 |
2 |
['erdOne', 'github-actions'] |
nobody |
0-54504 15 hours ago |
0-54504 15 hours ago |
1-64429 1 day |
| 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
maintainer-merge
t-ring-theory
|
71/0 |
Mathlib/RingTheory/MvPowerSeries/Substitution.lean,Mathlib/RingTheory/PowerSeries/Order.lean,Mathlib/RingTheory/PowerSeries/Substitution.lean |
3 |
22 |
['AntoineChambert-Loir', 'WenrongZou', 'erdOne', 'github-actions'] |
chrisflav assignee:chrisflav |
0-54044 15 hours ago |
0-54988 15 hours ago |
7-45455 7 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
|
71/0 |
Mathlib/RingTheory/MvPowerSeries/Basic.lean,Mathlib/RingTheory/MvPowerSeries/Order.lean,Mathlib/RingTheory/PowerSeries/Basic.lean,Mathlib/RingTheory/PowerSeries/Order.lean |
4 |
8 |
['WenrongZou', 'erdOne', 'github-actions'] |
mariainesdff assignee:mariainesdff |
0-53212 14 hours ago |
0-53225 14 hours ago |
6-45308 6 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 |
3 |
['artie2000', 'github-actions', 'j-loreaux', 'urkud'] |
bryangingechen assignee:bryangingechen |
0-51567 14 hours ago |
9-7864 9 days ago |
9-11134 9 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 |
['artie2000', 'github-actions', 'mathlib4-merge-conflict-bot'] |
pechersky assignee:pechersky |
0-50978 14 hours ago |
7-45901 7 days ago |
10-15440 10 days |
| 32852 |
artie2000 author:artie2000 |
refactor(Algebra): Generalise `support` from `Subsemiring` to `AddSubmonoid` |
* Generalise `support(Add)Subgroup`, `support` and `HasIdealSupport` from `Subsemiring` to `(Add)Submonoid`, moving the material to a new file
* Add documentation about supports
* Renamed declarations were not deprecated as the syntax for accessing them throughdot notation remains identical
This PR is one in a series for unbundling `RingCone` and `RingPreordering`
---
[](https://gitpod.io/from-referrer/)
|
t-algebra label:t-algebra$ |
147/66 |
Mathlib.lean,Mathlib/Algebra/Group/Submonoid/Support.lean,Mathlib/Algebra/Order/Ring/Ordering/Basic.lean,Mathlib/Algebra/Order/Ring/Ordering/Defs.lean |
4 |
1 |
['github-actions'] |
nobody |
0-49635 13 hours ago |
0-51838 14 hours ago |
0-51871 14 hours |
| 32789 |
harahu author:harahu |
doc(RingTheory): fix typos |
Typos found and fixed by Codex.
---
[](https://gitpod.io/from-referrer/)
|
maintainer-merge
t-ring-theory
|
29/30 |
Mathlib/RingTheory/AdicCompletion/AsTensorProduct.lean,Mathlib/RingTheory/AdicCompletion/Basic.lean,Mathlib/RingTheory/AdicCompletion/RingHom.lean,Mathlib/RingTheory/Conductor.lean,Mathlib/RingTheory/Congruence/Hom.lean,Mathlib/RingTheory/DedekindDomain/Factorization.lean,Mathlib/RingTheory/DividedPowers/Basic.lean,Mathlib/RingTheory/Etale/StandardEtale.lean,Mathlib/RingTheory/Extension/Generators.lean,Mathlib/RingTheory/Extension/Presentation/Basic.lean,Mathlib/RingTheory/FiniteType.lean,Mathlib/RingTheory/Flat/Basic.lean,Mathlib/RingTheory/Ideal/Over.lean,Mathlib/RingTheory/Ideal/Quotient/Operations.lean,Mathlib/RingTheory/Localization/LocalizationLocalization.lean,Mathlib/RingTheory/MvPolynomial/MonomialOrder.lean,Mathlib/RingTheory/MvPowerSeries/Trunc.lean,Mathlib/RingTheory/NonUnitalSubring/Basic.lean,Mathlib/RingTheory/NonUnitalSubsemiring/Basic.lean,Mathlib/RingTheory/Polynomial/Cyclotomic/Basic.lean,Mathlib/RingTheory/SimpleRing/Congr.lean,Mathlib/RingTheory/Valuation/Basic.lean,Mathlib/RingTheory/Valuation/ValuativeRel/Basic.lean |
23 |
4 |
['erdOne', 'github-actions', 'harahu'] |
nobody |
0-48823 13 hours ago |
0-48823 13 hours ago |
2-1000 2 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$ |
20/0 |
Mathlib/LinearAlgebra/TensorProduct/Basis.lean |
1 |
16 |
['bjornsolheim', 'erdOne', 'github-actions', 'robin-carlier', 'themathqueen'] |
erdOne assignee:erdOne |
0-56965 15 hours ago |
1-44715 1 day ago |
7-82632 7 days |
| 32671 |
themathqueen author:themathqueen |
chore(LinearAlgebra/GeneralLinearGroup/AlgEquiv): slightly generalize |
Also adds `trace (f x) = trace x` and `det (f x) = det x` for (star-)algebra equivalence `f`.
---
[](https://gitpod.io/from-referrer/)
|
t-algebra label:t-algebra$ |
61/17 |
Mathlib/LinearAlgebra/Determinant.lean,Mathlib/LinearAlgebra/GeneralLinearGroup/AlgEquiv.lean,Mathlib/LinearAlgebra/Trace.lean |
3 |
5 |
['erdOne', 'github-actions', 'themathqueen'] |
nobody |
0-47046 13 hours ago |
0-76163 21 hours ago |
4-17940 4 days |
| 32854 |
themathqueen author:themathqueen |
chore(LinearAlgebra/TensorProduct/Basic): some API for `lTensor` and `rTensor` |
---
This came up during review of #32492.
[](https://gitpod.io/from-referrer/)
|
t-algebra label:t-algebra$ |
18/0 |
Mathlib/LinearAlgebra/TensorProduct/Basic.lean |
1 |
1 |
['github-actions'] |
nobody |
0-46673 12 hours ago |
0-49201 13 hours ago |
0-49236 13 hours |
| 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 |
527/145 |
Mathlib.lean,Mathlib/Data/Set/Card.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 |
7 |
n/a |
['AntoineChambert-Loir', 'adomani', 'github-actions', 'leanprover-community-bot-assistant', 'mathlib4-dependent-issues-bot', 'mathlib4-merge-conflict-bot', 'tb65536'] |
tb65536 assignee:tb65536 |
0-46221 12 hours ago |
unknown |
unknown |
| 32787 |
Hagb author:Hagb |
feat(RingTheory/MvPolynomial/MonomialOrder): add several lemmas about `leadingTerm` and inequality on degree |
Some of them were abstracted from a proof of Buchberger's Criterion (#29203).
---
[](https://gitpod.io/from-referrer/)
|
maintainer-merge
t-ring-theory
|
34/0 |
Mathlib/RingTheory/MvPolynomial/MonomialOrder.lean |
1 |
3 |
['erdOne', 'github-actions'] |
nobody |
0-46093 12 hours ago |
0-46093 12 hours ago |
2-2847 2 days |
| 32857 |
gasparattila author:gasparattila |
feat: isometric equivalences of `WithLp` products |
This PR adds several equivalences of type `IsometryEquiv` and `LinearIsometryEquiv` for `WithLp p (_ × _)`, including commutativity, associativity and identity.
---
[](https://gitpod.io/from-referrer/)
|
|
167/2 |
Mathlib/Algebra/Group/Prod.lean,Mathlib/Analysis/Normed/Lp/ProdLp.lean,Mathlib/Topology/MetricSpace/Isometry.lean |
3 |
2 |
['gasparattila', 'github-actions'] |
nobody |
0-43102 11 hours ago |
0-43205 11 hours ago |
0-43178 11 hours |
| 32664 |
harahu author:harahu |
doc: fix articles a/an |
Use the correct article “an” before certain single-letter code terms that are pronounced with a vowel (`N`, `R`, `S`, `n` and `r`).
---
[](https://gitpod.io/from-referrer/)
|
|
73/72 |
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/NumberTheory/Cyclotomic/PrimitiveRoots.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 |
41 |
6 |
['github-actions', 'harahu', 'plp127', 'vihdzp'] |
JovanGerb assignee:JovanGerb |
1-33927 1 day ago |
4-40081 4 days ago |
4-40681 4 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
maintainer-merge
t-ring-theory
label:t-algebra$ |
148/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 |
8 |
['erdOne', 'github-actions', 'mathlib4-merge-conflict-bot', 'vihdzp', 'wwylele'] |
nobody |
0-39724 11 hours ago |
0-39724 11 hours ago |
4-67083 4 days |
| 32788 |
Hagb author:Hagb |
feat(RingTheory/MvPolynomial/MonomialOrder): add some variants of `sPolynomial_mul_monomial` |
This commit adds a variant `sPolynomial_mul_monomial'`, using `m.degree (monomial d c * p)` instead of `d + m.degree p`, which are different in the edge case that one of `c` and `p` is 0.
A pair of variants about `leadingTerm` instead of `monomial` are also added.
---
[](https://gitpod.io/from-referrer/)
|
maintainer-merge
t-ring-theory
|
30/0 |
Mathlib/RingTheory/MvPolynomial/MonomialOrder.lean |
1 |
3 |
['erdOne', 'github-actions'] |
nobody |
0-39629 11 hours ago |
0-39629 11 hours ago |
2-1958 2 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
maintainer-merge
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 |
39 |
['alreadydone', 'erdOne', 'github-actions', 'jcommelin', 'leanprover-bot', 'leanprover-community-mathlib4-bot', 'leanprover-radar'] |
mattrobball assignee:mattrobball |
0-39333 10 hours ago |
0-39333 10 hours ago |
10-43496 10 days |
| 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).
---
- [x] depends on: #32100
[](https://gitpod.io/from-referrer/)
|
awaiting-author
t-euclidean-geometry
|
137/33 |
Mathlib/Geometry/Euclidean/Angle/Unoriented/TriangleInequality.lean |
1 |
28 |
['JovanGerb', 'LessnessRandomness', 'Ruben-VandeVelde', 'github-actions', 'mathlib4-dependent-issues-bot', 'mathlib4-merge-conflict-bot', 'themathqueen'] |
jsm28 assignee:jsm28 |
1-69143 1 day ago |
2-47861 2 days ago |
13-38208 13 days |
| 32774 |
Hagb author:Hagb |
feat(Algebra/GroupWithZero/NonZeroDivisors): add a lemma about product |
Product of non-zero divisors is also a non-zero divisors.
It's similar with `IsRegular.prod`, while requiring non-zero divisors instead of regular elements.
---
`IsRegular.prod`:
https://github.com/leanprover-community/mathlib4/blob/c671bc4215d64bd9cc8a84fdec9a12bd33fdcd26/Mathlib/Algebra/Regular/Pow.lean#L36-L37
[](https://gitpod.io/from-referrer/)
|
t-algebra
large-import
label:t-algebra$ |
6/0 |
Mathlib/Algebra/GroupWithZero/NonZeroDivisors.lean |
1 |
1 |
['github-actions'] |
nobody |
0-38605 10 hours ago |
2-15292 2 days ago |
2-15344 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
|
63/0 |
Mathlib/Combinatorics/SimpleGraph/Matching.lean |
1 |
8 |
['SnirBroshi', 'github-actions', 'ksenono'] |
awainverse assignee:awainverse |
0-37739 10 hours ago |
6-49621 6 days ago |
6-49650 6 days |
| 32824 |
Vilin97 author:Vilin97 |
Prove that the diameter of a Euclidean ball is twice its radius. |
feat(Analysis/InnerProductSpace/EuclideanDist): prove that the diameter of an open Euclidean ball is twice its radius
Prove the same statement about the closed ball, and two related lemmas.
All lemmas and theorems: `image_closedBall_eq_metric_closedBall`, `diam_closed_ball_eq_two_mul_radius'`, `diam_closed_ball_eq_two_mul_radius`, `diam_ball_eq_two_mul_radius`
@Aristotle-Harmonic gave the initial version of the proofs.
Co-authored-by: Leo Mayer leomayer@uw.edu
---
[](https://gitpod.io/from-referrer/)
|
t-analysis
new-contributor
|
47/0 |
Mathlib/Analysis/InnerProductSpace/EuclideanDist.lean |
1 |
5 |
['github-actions', 'themathqueen'] |
nobody |
0-37251 10 hours ago |
1-33101 1 day ago |
1-33131 1 day |
| 28175 |
dsfxcimk author:dsfxcimk |
feat: exterior angle theorem |
Add Exterior angle theorem
---
The Exterior Angle Theorem states that the exterior angle of a triangle equals the sum of the two non-adjacent interior angles.
I plan to place this in Mathlib.Geometry.Euclidean.Triangle
[](https://gitpod.io/from-referrer/)
|
t-euclidean-geometry
new-contributor
|
9/0 |
Mathlib/Geometry/Euclidean/Triangle.lean,docs/1000.yaml |
2 |
24 |
['FrankieNC', 'JovanGerb', 'dsfxcimk', 'github-actions', 'grunweg', 'mathlib4-merge-conflict-bot', 'themathqueen'] |
jsm28 assignee:jsm28 |
0-33920 9 hours ago |
3-57071 3 days ago |
32-29220 32 days |
| 26608 |
vihdzp author:vihdzp |
feat(SetTheory/Cardinal/Aleph): `o.card ≤ ℵ_ o` and variants |
---
[](https://gitpod.io/from-referrer/)
|
t-set-theory |
24/0 |
Mathlib/SetTheory/Cardinal/Aleph.lean |
1 |
3 |
['github-actions', 'kckennylau', 'leanprover-community-bot-assistant'] |
alreadydone assignee:alreadydone |
0-33920 9 hours ago |
4-2967 4 days ago |
27-66339 27 days |
| 28972 |
themathqueen author:themathqueen |
feat(LinearAlgebra/Matrix): star-algebra automorphisms on matrices are unitarily inner |
Characterization of star-algebra automorphisms on matrices: for any star-algebra automorphism `f` on matrices, there exists a unitary matrix `U` such that `f x = U * x * star U`.
---
- [x] depends on: #28100
- [x] depends on: #28182
- [x] depends on: #28881
[](https://gitpod.io/from-referrer/)
|
t-algebra label:t-algebra$ |
118/0 |
Mathlib.lean,Mathlib/Analysis/Matrix/StarAlgEquiv.lean |
2 |
4 |
['github-actions', 'mathlib4-dependent-issues-bot', 'mathlib4-merge-conflict-bot', 'themathqueen'] |
dagurtomas assignee:dagurtomas |
0-33919 9 hours ago |
5-43307 5 days ago |
5-43688 5 days |
| 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'] |
TwoFX assignee:TwoFX |
0-33917 9 hours ago |
4-2720 4 days ago |
4-5208 4 days |
| 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 |
29 |
['github-actions', 'grunweg', 'leanprover-radar', 'thorimur'] |
joneugster assignee:joneugster |
0-33913 9 hours ago |
5-20358 5 days ago |
8-51637 8 days |
| 32589 |
grunweg author:grunweg |
feat: smooth embeddings |
Define smooth embeddings between smooth manifolds: a map is a smooth embedding iff it is both a smooth immersion and a topological embedding. We also prove basic properties (such as being stable under products); stronger results will be added in future PRs.
Note that unlike smooth immersions, we do not add definitions for
- being a smooth embedding on a set (as this doesn't exist in the topological category either),
- being an embedding at a point (being an embedding is a global notion; moreover, every immersion is locally an embedding anyway, so "being an immersion at x" is sufficient to state this)
- variants with respect to a fixed complement: the motivation for immersions (considering the equivalent local descriptions of smooth submanifolds) do not apply to this global notion.
-----
- [x] depends on: #28853
---
[](https://gitpod.io/from-referrer/)
|
t-differential-geometry |
94/3 |
Mathlib.lean,Mathlib/Geometry/Manifold/Immersion.lean,Mathlib/Geometry/Manifold/SmoothEmbedding.lean |
3 |
19 |
['chrisflav', 'github-actions', 'grunweg', 'mathlib4-dependent-issues-bot', 'peabrainiac'] |
PatrickMassot assignee:PatrickMassot |
0-33912 9 hours ago |
3-36082 3 days ago |
4-4323 4 days |
| 32639 |
euprunin author:euprunin |
chore: golf using `grind`. add `grind` annotations. |
---
Trace profiling results (shown if ≥10 ms before or after):
* `Finset.filter_product_card`: 39 ms before, 114 ms after
* `Finset.sym2_eq_image`: 13 ms before, 67 ms after
* `List.sublist_iff_exists_fin_orderEmbedding_get_eq`: 125 ms before, 148 ms after
* `Equiv.Perm.isThreeCycle_swap_mul_swap_same`: 51 ms before, 79 ms after
* `Polynomial.gaussNorm_monomial`: 12 ms before, 12 ms after 🎉
This golfing PR is batched under the following guidelines:
* Up to ~5 changed files per PR
* Up to ~25 changed declarations per PR
* Up to ~100 changed lines per PR
---
[](https://gitpod.io/from-referrer/)
|
|
23/57 |
Mathlib/Algebra/MvPolynomial/Basic.lean,Mathlib/Algebra/MvPolynomial/CommRing.lean,Mathlib/Algebra/Polynomial/Basic.lean,Mathlib/Combinatorics/SimpleGraph/Subgraph.lean,Mathlib/Data/Finset/Prod.lean,Mathlib/Data/Finset/Sym.lean,Mathlib/Data/Finsupp/Defs.lean,Mathlib/Data/List/NodupEquivFin.lean,Mathlib/Data/List/Sym.lean,Mathlib/Data/Sym/Sym2.lean,Mathlib/GroupTheory/Perm/Cycle/Type.lean,Mathlib/Order/Hom/Basic.lean,Mathlib/RingTheory/Polynomial/GaussNorm.lean |
13 |
9 |
['euprunin', 'github-actions', 'leanprover-radar', 'vihdzp'] |
nobody |
3-33418 3 days ago |
3-55156 3 days ago |
4-29418 4 days |
| 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 |
2 |
['artie2000', 'github-actions'] |
b-mehta assignee:b-mehta |
0-33911 9 hours ago |
4-82202 4 days ago |
4-82244 4 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'] |
dwrensha assignee:dwrensha |
0-33910 9 hours ago |
4-26451 4 days ago |
4-26481 4 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'] |
dagurtomas assignee:dagurtomas |
0-33909 9 hours ago |
4-13065 4 days ago |
4-13104 4 days |
| 32675 |
kebekus author:kebekus |
feat: meromorphic functions are measurable |
Show that meromorphic functions are measurable.
This material is used in [Project VD](https://github.com/kebekus/ProjectVD), which aims to formalize Value Distribution Theory for meromorphic functions on the complex plane.
---
[](https://gitpod.io/from-referrer/)
|
t-analysis
large-import
|
34/2 |
Mathlib/Analysis/Meromorphic/Basic.lean |
1 |
1 |
['github-actions'] |
j-loreaux assignee:j-loreaux |
0-33908 9 hours ago |
3-62151 3 days ago |
4-10839 4 days |
| 32678 |
harahu author:harahu |
doc(MeasureTheory): fix typos |
Fix a collection of simple typos in `Mathlib/MeasureTheory`.
---
Typos found and fixed by Codex.
[](https://gitpod.io/from-referrer/)
|
t-measure-probability |
22/22 |
Mathlib/MeasureTheory/Category/MeasCat.lean,Mathlib/MeasureTheory/Constructions/Cylinders.lean,Mathlib/MeasureTheory/Constructions/Pi.lean,Mathlib/MeasureTheory/Function/ConditionalExpectation/PullOut.lean,Mathlib/MeasureTheory/Function/UniformIntegrable.lean,Mathlib/MeasureTheory/Integral/Bochner/Basic.lean,Mathlib/MeasureTheory/Integral/IntervalIntegral/FundThmCalculus.lean,Mathlib/MeasureTheory/Integral/IntervalIntegral/Periodic.lean,Mathlib/MeasureTheory/Integral/RieszMarkovKakutani/NNReal.lean,Mathlib/MeasureTheory/Integral/RieszMarkovKakutani/Real.lean,Mathlib/MeasureTheory/Measure/Regular.lean,Mathlib/MeasureTheory/Measure/SeparableMeasure.lean |
12 |
1 |
['github-actions'] |
kex-y assignee:kex-y |
0-33907 9 hours ago |
4-2626 4 days ago |
4-2657 4 days |
| 32679 |
YaelDillies author:YaelDillies |
chore(Data/Sym2): improve defeq of `diagSet` |
#30559 introduced a regression on the defeqs in the `SimpleGraph` API. This PR fixes it.
From LeanCamCombi
---
I personally think this new `diagSet` definition is unnecessary: `{e | e.IsDiag}` is not much longer to write than `Sym2.diagSet` and more transparent, but whatever.
[](https://gitpod.io/from-referrer/)
|
t-data |
51/41 |
Mathlib/Combinatorics/SimpleGraph/Basic.lean,Mathlib/Combinatorics/SimpleGraph/DeleteEdges.lean,Mathlib/Combinatorics/SimpleGraph/Operations.lean,Mathlib/Data/Sym/Card.lean,Mathlib/Data/Sym/Sym2.lean |
5 |
6 |
['SnirBroshi', 'YaelDillies', 'github-actions', 'vihdzp'] |
pechersky assignee:pechersky |
0-33906 9 hours ago |
4-2046 4 days ago |
4-2234 4 days |
| 32696 |
YuvalFilmus author:YuvalFilmus |
feat(SpecialFunctions/Artanh): basic definition and partial equivalence |
Definition of `artanh`, and proof that it is an inverse of `tanh`.
---
[](https://gitpod.io/from-referrer/)
|
t-analysis
new-contributor
|
155/1 |
Mathlib.lean,Mathlib/Analysis/SpecialFunctions/Arcosh.lean,Mathlib/Analysis/SpecialFunctions/Artanh.lean,Mathlib/Data/Real/Sqrt.lean |
4 |
15 |
['SnirBroshi', 'YuvalFilmus', 'github-actions', 'j-loreaux', 'mathlib4-merge-conflict-bot'] |
j-loreaux assignee:j-loreaux |
0-33905 9 hours ago |
3-47005 3 days ago |
3-54990 3 days |
| 32704 |
euprunin author:euprunin |
chore: remove use of `erw` |
---
[](https://gitpod.io/from-referrer/)
|
|
20/26 |
Mathlib/Algebra/Category/ModuleCat/ChangeOfRings.lean,Mathlib/AlgebraicTopology/DoldKan/Homotopies.lean,Mathlib/CategoryTheory/Adjunction/PartialAdjoint.lean,Mathlib/CategoryTheory/Preadditive/AdditiveFunctor.lean,Mathlib/CategoryTheory/Triangulated/Opposite/Basic.lean,Mathlib/MeasureTheory/VectorMeasure/Decomposition/RadonNikodym.lean,Mathlib/Topology/Homotopy/Product.lean |
7 |
14 |
['bryangingechen', 'euprunin', 'github-actions', 'grunweg', 'leanprover-radar'] |
MichaelStollBayreuth assignee:MichaelStollBayreuth |
0-33904 9 hours ago |
3-42522 3 days ago |
3-42494 3 days |
| 32850 |
gasparattila author:gasparattila |
feat(Topology/UniformSpace): add `isRefl_of_mem_uniformity` |
This PR adds a lemma to directly obtain `U.IsRefl` for an entourage `U` of a uniform space.
---
[](https://gitpod.io/from-referrer/)
|
t-topology |
11/8 |
Mathlib/Dynamics/TopologicalEntropy/NetEntropy.lean,Mathlib/Topology/UniformSpace/Basic.lean,Mathlib/Topology/UniformSpace/Closeds.lean,Mathlib/Topology/UniformSpace/Defs.lean |
4 |
1 |
['github-actions'] |
nobody |
0-32183 8 hours ago |
0-32183 8 hours ago |
0-60694 16 hours |
| 32371 |
KaiErikNiermann author:KaiErikNiermann |
fix: minor error in comment of example for natural transformation |
---
[](https://gitpod.io/from-referrer/)
|
easy
new-contributor
|
2/2 |
Mathlib/CategoryTheory/NatTrans.lean |
1 |
2 |
['LLaurance', 'artie2000', 'github-actions'] |
nobody |
0-59406 16 hours ago |
11-10976 11 days ago |
11-45848 11 days |
| 32862 |
JovanGerb author:JovanGerb |
chore(Order/Iterate): avoid `to_dual existing` |
This PR adds a few uses of `to_dual`. Unfortunately many declarations cannot yet really be handled by `to_dual` because `Monotone` isn't supported yet.
---
[](https://gitpod.io/from-referrer/)
|
t-order |
3/9 |
Mathlib/Order/Iterate.lean |
1 |
1 |
['github-actions'] |
nobody |
0-30033 8 hours ago |
0-30041 8 hours ago |
0-30075 8 hours |
| 32851 |
tdwag123 author:tdwag123 |
feat(MeasureTheory/Measure/Hausdorff) add `exists_accPt_of_pos_hausdorffMeasure ` |
feat(MeasureTheory/Measure/Hausdorff): Added a theorem that states if a set has positive s-dimensional Hausdorff measure, then it has an accumulation point, along with necessary proofs.
Theorem added: `exists_accPt_of_pos_hausdorffMeasure`
**Harmonic's Aristotle gave the initial version of the proofs.**
`---`
[](https://gitpod.io/from-referrer/)
|
t-measure-probability
new-contributor
|
58/0 |
Mathlib/MeasureTheory/Measure/Hausdorff.lean |
1 |
2 |
['github-actions'] |
nobody |
0-28345 7 hours ago |
0-49799 13 hours ago |
0-51101 14 hours |
| 32860 |
johnrathgeber author:johnrathgeber |
feat: IMO 1998 Q3 |
---
[](https://gitpod.io/from-referrer/)
|
new-contributor
IMO
|
623/0 |
Archive.lean,Archive/Imo/Imo1998Q3.lean |
2 |
9 |
['SnirBroshi', 'github-actions', 'johnrathgeber'] |
nobody |
0-28366 7 hours ago |
0-32368 8 hours ago |
0-32405 9 hours |
| 32866 |
JovanGerb author:JovanGerb |
fix(to_fun): fix the `@[to_fun]` attribute when the proof is not by reflexivity |
This PR fixes the bug in `@[to_fun]` reported in https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/.60to_fun.60.20tactic/with/563623809
---
[](https://gitpod.io/from-referrer/)
|
t-meta |
21/2 |
Mathlib/Tactic/ToFun.lean,MathlibTest/ToFun.lean |
2 |
1 |
['github-actions'] |
nobody |
0-25615 7 hours ago |
0-25615 7 hours ago |
0-25654 7 hours |
| 32262 |
alreadydone author:alreadydone |
feat(Algebra): stably finite rings |
+ Show finite semirings are stably-finite.
+ Show stable finiteness is left-right symmetric.
+ Prove matrix characterizations of rank condition and invariant basis number; as consequences, show both properties are left-right symmetric.
+ Show stable finiteness implies the rank condition, generalizing [rankCondition_of_nontrivial_of_commSemiring](https://leanprover-community.github.io/mathlib4_docs/Mathlib/LinearAlgebra/Matrix/InvariantBasisNumber.html#rankCondition_of_nontrivial_of_commSemiring).
+ Reformulate a lemma as saying division rings are stably finite.
---
- [ ] depends on: #32610
[](https://gitpod.io/from-referrer/)
|
awaiting-author
t-algebra
t-ring-theory
label:t-algebra$ |
270/76 |
Mathlib/Data/Matrix/Basic.lean,Mathlib/Data/Matrix/Composition.lean,Mathlib/Data/Matrix/Mul.lean,Mathlib/LinearAlgebra/FiniteDimensional/Basic.lean,Mathlib/LinearAlgebra/InvariantBasisNumber.lean,Mathlib/LinearAlgebra/Matrix/BaseChange.lean,Mathlib/LinearAlgebra/Matrix/InvariantBasisNumber.lean,Mathlib/LinearAlgebra/Matrix/NonsingularInverse.lean,Mathlib/LinearAlgebra/Matrix/SchurComplement.lean,Mathlib/LinearAlgebra/Matrix/SemiringInverse.lean,Mathlib/LinearAlgebra/Matrix/ToLin.lean |
11 |
56 |
['Garmelon', 'alreadydone', 'artie2000', 'erdOne', 'github-actions', 'leanprover-bot', 'leanprover-community-mathlib4-bot', 'leanprover-radar', 'mathlib4-dependent-issues-bot'] |
erdOne assignee:erdOne |
0-56528 15 hours ago |
0-58080 16 hours ago |
7-14133 7 days |
| 32856 |
stepan2698-cpu author:stepan2698-cpu |
feat: definition of an irreducible representation |
Define irreducible monoid representations over a field and prove that a monoid representation is irreducible iff the corresponding module over the monoid algebra is simple. |
t-algebra
new-contributor
label:t-algebra$ |
165/4 |
Mathlib.lean,Mathlib/RepresentationTheory/Irreducible.lean,Mathlib/RepresentationTheory/Subrepresentation.lean |
3 |
8 |
['Whysoserioushah', 'github-actions'] |
nobody |
0-23333 6 hours ago |
0-45352 12 hours ago |
0-45386 12 hours |
| 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
|
183/0 |
Mathlib.lean,Mathlib/AlgebraicGeometry/Artinian.lean,Mathlib/Topology/KrullDimension.lean |
3 |
58 |
['Brian-Nugent', 'alreadydone', 'erdOne', 'github-actions'] |
erdOne assignee:erdOne |
0-23330 6 hours ago |
0-23330 6 hours ago |
6-73942 6 days |
| 32868 |
kim-em author:kim-em |
fix(scripts): make missing local tag a warning in verify_version_tags.py |
This PR fixes an issue where `verify_version_tags.py` fails when run from `release_checklist.py` because there's no local mathlib4 checkout with tags fetched.
The script was failing with "Tag not found locally" even though all real verification checks passed (GitHub tag exists, toolchain correct, cache works, build verification passes).
This change makes the missing local tag a warning instead of an error, since the GitHub API check already verifies the tag exists remotely.
🤖 Prepared with Claude Code |
CI |
8/1 |
scripts/verify_version_tags.py |
1 |
2 |
['github-actions', 'kim-em'] |
nobody |
0-19110 5 hours ago |
0-19124 5 hours ago |
0-19157 5 hours |
| 32552 |
ksenono author:ksenono |
feat(SetTheory/Cardinal): helpers for Konig's theorem |
---
[](https://gitpod.io/from-referrer/)
|
new-contributor
t-set-theory
|
70/0 |
Mathlib/SetTheory/Cardinal/Arithmetic.lean,Mathlib/SetTheory/Cardinal/Basic.lean |
2 |
32 |
['SnirBroshi', 'b-mehta', 'github-actions', 'ksenono', 'staroperator', 'vihdzp'] |
b-mehta assignee:b-mehta |
0-41405 11 hours ago |
6-50899 6 days ago |
6-50938 6 days |
| 32744 |
NoneMore author:NoneMore |
feat(ModelTheory/Definablity): add `DefinableFun` definition and lemmas |
This PR adds two basic shapes of definable sets and `DefinableFun` definition with relevant lemmas.
The main result is `definable_preimage_of_definableMap` asserting that the preimage of a definable set under a definable map is definable.
There are also some tool lemmas derived by the preimage lemma.
Not sure if it's necessary to create a new module `DefinableFun`.
---
[](https://gitpod.io/from-referrer/)
|
t-logic
new-contributor
|
134/0 |
Mathlib/ModelTheory/Definability.lean |
1 |
37 |
['NoneMore', 'github-actions', 'staroperator'] |
nobody |
0-8347 2 hours ago |
2-18584 2 days ago |
2-63886 2 days |
| 32853 |
euprunin author:euprunin |
chore: golf using `grind` and `simp` |
---
Trace profiling results (shown if ≥10 ms before or after):
* `Finset.filter_product_card`: 38 ms before, 107 ms after
* `List.Nat.antidiagonalTuple_pairwise_pi_lex`: 72 ms before, 162 ms after
* `RingHom.finitePresentation_isStableUnderBaseChange`: 207 ms before, 16 ms after 🎉
* `RingHom.finite_isStableUnderBaseChange`: 339 ms before, 36 ms after 🎉
* `ZSpan.fundamentalDomain_reindex`: 17 ms before, 11 ms after 🎉
This golfing PR is batched under the following guidelines:
* Up to ~5 changed files per PR
* Up to ~25 changed declarations per PR
* Up to ~100 changed lines per PR
---
[](https://gitpod.io/from-referrer/)
|
|
12/29 |
Mathlib/Algebra/Module/ZLattice/Basic.lean,Mathlib/Data/Fin/Tuple/NatAntidiagonal.lean,Mathlib/Data/Finset/Prod.lean,Mathlib/RingTheory/RingHom/Finite.lean,Mathlib/RingTheory/RingHom/FinitePresentation.lean |
5 |
7 |
['euprunin', 'github-actions', 'themathqueen'] |
nobody |
0-8265 2 hours ago |
0-50667 14 hours ago |
0-50640 14 hours |
| 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
|
111/0 |
Mathlib/Combinatorics/SimpleGraph/Acyclic.lean,Mathlib/Combinatorics/SimpleGraph/Connectivity/Connected.lean |
2 |
1 |
['github-actions'] |
b-mehta assignee:b-mehta |
0-5275 1 hour ago |
20-383 20 days ago |
20-417 20 days |
| 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
- [x] depends on: #31845
[](https://gitpod.io/from-referrer/)
|
|
282/1 |
Mathlib.lean,Mathlib/NumberTheory/Padics/HeightOneSpectrum.lean,Mathlib/RingTheory/DedekindDomain/Ideal/Lemmas.lean,Mathlib/Topology/Algebra/Algebra/Equiv.lean,Mathlib/Topology/Algebra/Valued/WithVal.lean |
5 |
5 |
['github-actions', 'mathlib4-dependent-issues-bot', 'mathlib4-merge-conflict-bot'] |
nobody |
0-3249 54 minutes ago |
4-53593 4 days ago |
4-53574 4 days |
| 32672 |
tb65536 author:tb65536 |
feat: haar measures on short exact sequences |
---
[](https://gitpod.io/from-referrer/)
|
t-measure-probability |
344/0 |
Mathlib.lean,Mathlib/MeasureTheory/Measure/Haar/Extension.lean |
2 |
2 |
['RemyDegenne', 'github-actions'] |
nobody |
0-2696 44 minutes ago |
3-9197 3 days ago |
3-17978 3 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
|
221/1 |
Mathlib/NumberTheory/Chebyshev.lean |
1 |
6 |
['ajirving', 'github-actions', 'mathlib4-dependent-issues-bot', 'mathlib4-merge-conflict-bot'] |
nobody |
1-1227 1 day ago |
1-1248 1 day ago |
4-15578 4 days |
| 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$ |
15/1 |
Mathlib/Algebra/Group/ForwardDiff.lean |
1 |
15 |
['FlAmmmmING', 'Ruben-VandeVelde', 'dagurtomas', 'github-actions', 'mathlib4-merge-conflict-bot'] |
dagurtomas assignee:dagurtomas |
3-30269 3 days ago |
3-30311 3 days ago |
22-44262 22 days |