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 |
23-17063 23 days ago |
26-28634 26 days ago |
39-30561 39 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 |
17-68591 17 days ago |
21-35880 21 days ago |
21-35855 21 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 |
17-40132 17 days ago |
21-12120 21 days ago |
47-18221 47 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 |
15-68573 15 days ago |
19-28738 19 days ago |
22-26406 22 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 |
14-68564 14 days ago |
18-3732 18 days ago |
18-3716 18 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 |
14-27205 14 days ago |
14-28728 14 days ago |
23-73478 23 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 |
13-68596 13 days ago |
17-17820 17 days ago |
19-18246 19 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 |
13-68592 13 days ago |
17-38433 17 days ago |
17-39024 17 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 |
13-68586 13 days ago |
19-60896 19 days ago |
19-60939 19 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 |
13-5979 13 days ago |
17-5949 17 days ago |
17-7043 17 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 |
12-74067 12 days ago |
13-71232 13 days ago |
61-71316 61 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 |
12-68582 12 days ago |
16-58661 16 days ago |
16-61285 16 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 |
12-68577 12 days ago |
16-16204 16 days ago |
18-18669 18 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 |
12-68572 12 days ago |
16-19519 16 days ago |
16-19553 16 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 |
12-37004 12 days ago |
12-37053 12 days ago |
12-65239 12 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 |
12-11228 12 days ago |
12-11360 12 days ago |
17-29055 17 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 |
11-68591 11 days ago |
21-47133 21 days ago |
21-78024 21 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 |
11-68590 11 days ago |
18-65223 18 days ago |
18-65258 18 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 |
11-21492 11 days ago |
11-21492 11 days ago |
24-75986 24 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 |
10-70003 10 days ago |
11-28709 11 days ago |
11-30304 11 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 |
10-38236 10 days ago |
10-38236 10 days ago |
14-9394 14 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 |
10-16121 10 days ago |
10-16155 10 days ago |
25-8759 25 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 |
10-14545 10 days ago |
19-81600 19 days ago |
19-84145 19 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 |
10-5751 10 days ago |
19-4603 19 days ago |
24-75686 24 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 |
9-85114 9 days ago |
40-15690 1 month ago |
40-15645 40 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 |
9-84274 9 days ago |
10-2485 10 days ago |
18-11843 18 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 |
9-68593 9 days ago |
14-6554 14 days ago |
14-9281 14 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 |
9-31637 9 days ago |
9-34655 9 days ago |
9-76042 9 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 |
8-20156 8 days ago |
9-70672 9 days ago |
66-55704 66 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 |
8-12233 8 days ago |
8-12233 8 days ago |
49-43251 49 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 |
8-6347 8 days ago |
8-6466 8 days ago |
13-898 13 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 |
7-76805 7 days ago |
13-80007 13 days ago |
13-82960 13 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 |
7-68588 7 days ago |
10-74919 10 days ago |
11-79519 11 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 |
7-68582 7 days ago |
11-10116 11 days ago |
11-10093 11 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 |
7-30735 7 days ago |
7-30764 7 days ago |
7-38343 7 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 |
55-12618 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 |
7-16760 7 days ago |
18-27039 18 days ago |
32-23536 32 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 |
6-74182 6 days ago |
18-66209 18 days ago |
18-66242 18 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 |
6-68591 6 days ago |
22-59519 22 days ago |
22-59556 22 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 |
6-68587 6 days ago |
10-55902 10 days ago |
10-55892 10 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 |
6-66376 6 days ago |
6-66376 6 days ago |
27-62444 27 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 |
6-26506 6 days ago |
6-36553 6 days ago |
13-36015 13 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 |
6-1498 6 days ago |
6-1519 6 days ago |
36-38659 36 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 |
5-69771 5 days ago |
5-69881 5 days ago |
11-23592 11 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 |
5-68588 5 days ago |
9-68082 9 days ago |
9-68392 9 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 |
5-68578 5 days ago |
9-76709 9 days ago |
9-76684 9 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 |
5-42499 5 days ago |
5-42499 5 days ago |
91-78938 91 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 |
5-33482 5 days ago |
5-33482 5 days ago |
9-42577 9 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 |
5-15650 5 days ago |
9-82785 9 days ago |
10-51320 10 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 |
4-81708 4 days ago |
4-81776 4 days ago |
18-33439 18 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 |
4-68587 4 days ago |
8-1793 8 days ago |
8-55445 8 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 |
4-68583 4 days ago |
8-22967 8 days ago |
10-19533 10 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 |
4-68575 4 days ago |
8-52306 8 days ago |
8-52350 8 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 |
14-20515 14 days ago |
14-20516 14 days ago |
0-31 31 seconds |
| 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 |
4-6492 4 days ago |
4-20309 4 days ago |
20-82770 20 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 |
4-5433 4 days ago |
26-33153 26 days ago |
30-76383 30 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 |
4-2084 4 days ago |
19-2903 19 days ago |
19-2945 19 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 |
3-85944 3 days ago |
4-13730 4 days ago |
24-60284 24 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 |
3-74632 3 days ago |
3-74774 3 days ago |
32-82024 32 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 |
3-68580 3 days ago |
8-10762 8 days ago |
8-21054 8 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 |
3-68576 3 days ago |
7-65753 7 days ago |
7-65787 7 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 |
3-68570 3 days ago |
6-71607 6 days ago |
6-71583 6 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 |
3-66723 3 days ago |
3-66782 3 days ago |
3-66766 3 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 |
3-61091 3 days ago |
3-62260 3 days ago |
3-62294 3 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 |
3-60756 3 days ago |
3-61657 3 days ago |
3-61693 3 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 |
3-53671 3 days ago |
3-53935 3 days ago |
3-53911 3 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 |
3-51542 3 days ago |
3-51542 3 days ago |
3-51518 3 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 |
3-50237 3 days ago |
3-50499 3 days ago |
3-50536 3 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 |
3-49668 3 days ago |
3-49676 3 days ago |
3-49711 3 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 |
3-43513 3 days ago |
3-43513 3 days ago |
6-1596 6 days |
| 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 |
26-43928 26 days ago |
26-43929 26 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 |
3-18956 3 days ago |
3-19021 3 days ago |
3-19423 3 days |
| 32437 |
WenrongZou author:WenrongZou |
feat(Algebra/Category/ModuleCat/Sheaf/Quasicoherent): construction of `Presentation` |
We construct presentation of sheaf of module by sequence and add `Presentation.map`.
This contribution was created as part of the Heidelberg Lean workshop "Formalising algebraic geometry" in November 2025.
Co-authored-by: William Coram @WilliamCoram
Co-authored-by: Andrew Yang @erdOne
---
[](https://gitpod.io/from-referrer/)
|
t-algebra
new-contributor
label:t-algebra$ |
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 |
3-15393 3 days ago |
3-18505 3 days ago |
6-71302 6 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 |
3-15379 3 days ago |
7-29584 7 days ago |
7-29875 7 days |
| 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 |
3-11428 3 days ago |
3-11467 3 days ago |
3-11470 3 days |
| 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 |
3-10400 3 days ago |
3-10403 3 days ago |
3-10440 3 days |
| 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 |
3-9661 3 days ago |
3-9668 3 days ago |
3-9702 3 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 |
3-8130 3 days ago |
3-8130 3 days ago |
3-8173 3 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 |
3-1824 3 days ago |
3-1964 3 days ago |
5-17277 5 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 |
2-83963 2 days ago |
3-47348 3 days ago |
29-40838 29 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 |
2-82536 2 days ago |
11-19097 11 days ago |
12-13201 12 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 |
2-81946 2 days ago |
2-81946 2 days ago |
2-81986 2 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 |
2-80042 2 days ago |
7-34899 7 days ago |
17-30212 17 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 |
2-76627 2 days ago |
2-76643 2 days ago |
2-76679 2 days |
| 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 |
2-76237 2 days ago |
3-66373 3 days ago |
3-70558 3 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 |
2-68592 2 days ago |
3-9865 3 days ago |
6-7307 6 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 |
2-68590 2 days ago |
6-55073 6 days ago |
6-57693 6 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 |
2-68588 2 days ago |
6-4401 6 days ago |
6-4445 6 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 |
2-68587 2 days ago |
5-80183 5 days ago |
5-80220 5 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 |
2-68586 2 days ago |
5-74020 5 days ago |
5-74043 5 days |
| 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 |
2-54437 2 days ago |
2-54443 2 days ago |
6-47823 6 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 |
2-44913 2 days ago |
2-57945 2 days ago |
2-57979 2 days |
| 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 |
2-42338 2 days ago |
3-23836 3 days ago |
3-23876 3 days |
| 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 |
2-35005 2 days ago |
2-35005 2 days ago |
2-35045 2 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 |
2-30556 2 days ago |
2-30556 2 days ago |
2-30596 2 days |
| 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 |
2-27760 2 days ago |
2-34875 2 days ago |
2-34906 2 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 |
2-26892 2 days ago |
2-26898 2 days ago |
2-26936 2 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 |
2-20947 2 days ago |
6-86018 6 days ago |
6-86311 6 days |
| 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 |
2-19392 2 days ago |
3-10686 3 days ago |
3-10726 3 days |
| 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 |
2-16981 2 days ago |
2-39569 2 days ago |
2-39606 2 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 |
2-10282 2 days ago |
3-31719 3 days ago |
3-31702 3 days |
| 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 |
2-9774 2 days ago |
2-9775 2 days ago |
15-81152 15 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 |
2-8536 2 days ago |
2-8536 2 days ago |
2-9470 2 days |
| 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 |
2-6429 2 days ago |
2-6453 2 days ago |
2-75312 2 days |
| 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 |
2-4328 2 days ago |
2-24343 2 days ago |
2-24332 2 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 |
2-1472 2 days ago |
2-1485 2 days ago |
7-79971 7 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 |
1-86227 1 day ago |
10-42524 10 days ago |
10-45797 10 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 |
1-85638 1 day ago |
8-80561 8 days ago |
11-50103 11 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 |
1-81333 1 day ago |
1-83861 1 day ago |
1-83898 1 day |
| 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 |
1-77762 1 day ago |
1-77865 1 day ago |
1-77840 1 day |
| 32116 |
LessnessRandomness author:LessnessRandomness |
feat(Geometry/Euclidean/Angle/Unoriented/TriangleInequality): Add criterion for equality case |
The PR fills `proof_wanted` in the file `TriangleInequality.lean` (criterion for equality in the triangle inequality for angles).
---
- [x] depends on: #32100
[](https://gitpod.io/from-referrer/)
|
t-euclidean-geometry |
137/33 |
Mathlib/Geometry/Euclidean/Angle/Unoriented/TriangleInequality.lean |
1 |
29 |
['JovanGerb', 'LessnessRandomness', 'Ruben-VandeVelde', 'github-actions', 'mathlib4-dependent-issues-bot', 'mathlib4-merge-conflict-bot', 'themathqueen'] |
jsm28 assignee:jsm28 |
1-73585 1 day ago |
1-73585 1 day ago |
15-25368 15 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 |
1-72399 1 day ago |
7-84281 7 days ago |
7-84313 7 days |
| 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 |
1-68580 1 day ago |
5-5331 5 days ago |
33-63883 33 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 |
1-68580 1 day ago |
5-37627 5 days ago |
29-14602 29 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 |
1-68577 1 day ago |
5-37380 5 days ago |
5-39870 5 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 |
1-68573 1 day ago |
6-55018 6 days ago |
9-86300 9 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'] |
mattrobball assignee:mattrobball |
1-68572 1 day ago |
5-3416 5 days ago |
5-64081 5 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 |
1-68570 1 day ago |
5-61111 5 days ago |
5-61144 5 days |
| 32673 |
CoolRmal author:CoolRmal |
feat: an open subset of a Baire space is Baire |
This PR proves the following lemmas:
1. If `f : X → Y` is an open quotient map and `X` is a Baire space, then `Y` is Baire.
2. As a corollary of the first lemma, a homeomorphism maps a Baire space to a Baire space.
3. An open subset of a Baire space is Baire.
Formalized with help from Aristotle.
---
[](https://gitpod.io/from-referrer/)
|
t-topology
large-import
|
49/1 |
Mathlib/Topology/Baire/Lemmas.lean,Mathlib/Topology/Homeomorph/Lemmas.lean,Mathlib/Topology/Maps/OpenQuotient.lean |
3 |
2 |
['CoolRmal', 'github-actions'] |
dagurtomas assignee:dagurtomas |
1-68569 1 day ago |
5-47725 5 days ago |
5-47767 5 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 |
1-68568 1 day ago |
5-10411 5 days ago |
5-45502 5 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 |
1-68567 1 day ago |
5-37286 5 days ago |
5-37320 5 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 |
1-68566 1 day ago |
5-36706 5 days ago |
5-36897 5 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 |
1-68565 1 day ago |
4-81665 4 days ago |
5-3253 5 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 |
1-66843 1 day ago |
1-66843 1 day ago |
2-8956 2 days |
| 32863 |
JovanGerb author:JovanGerb |
feat(to_dual): don't translate the order on `Set` |
This PR adds the tag `attribute [to_dual_dont_translate] Set`, as discussed in https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/Order.20dual.20tactic/near/560952736
It is not obvious where this tag should go, since `Set` and `to_dual` don't import eachother. A natural place seems to be the place where the `sInf`/`sSup` notations are declared for `Set`, since this is where one could start trying to use `to_dual` for translating the order on `Set`.
---
[](https://gitpod.io/from-referrer/)
|
t-order |
2/0 |
Mathlib/Order/SetNotation.lean |
1 |
1 |
['github-actions'] |
nobody |
1-63918 1 day ago |
1-63923 1 day ago |
1-63957 1 day |
| 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 |
1-60275 1 day ago |
1-60275 1 day ago |
1-60316 1 day |
| 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.
---
- [x] depends on: #32610
[](https://gitpod.io/from-referrer/)
|
t-algebra
t-ring-theory
label:t-algebra$ |
281/80 |
Mathlib/Algebra/Group/Equiv/Basic.lean,Mathlib/Algebra/Group/Hom/Defs.lean,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 |
13 |
60 |
['Garmelon', 'alreadydone', 'artie2000', 'erdOne', 'github-actions', 'leanprover-bot', 'leanprover-community-mathlib4-bot', 'leanprover-radar', 'mathlib4-dependent-issues-bot'] |
erdOne assignee:erdOne |
1-36565 1 day ago |
1-61313 1 day ago |
8-85818 8 days |
| 32412 |
Brian-Nugent author:Brian-Nugent |
feat: add Artinian schemes |
Added the definition of Artinian Schemes and proved basic facts about them.
---
[](https://gitpod.io/from-referrer/)
|
t-algebraic-geometry
new-contributor
|
183/0 |
Mathlib.lean,Mathlib/AlgebraicGeometry/Artinian.lean,Mathlib/Topology/KrullDimension.lean |
3 |
58 |
['Brian-Nugent', 'alreadydone', 'erdOne', 'github-actions'] |
erdOne assignee:erdOne |
1-57990 1 day ago |
1-57990 1 day ago |
8-22205 8 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 |
1-53770 1 day ago |
1-53784 1 day ago |
1-53819 1 day |
| 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 |
33 |
['SnirBroshi', 'b-mehta', 'github-actions', 'ksenono', 'staroperator', 'vihdzp'] |
b-mehta assignee:b-mehta |
1-52716 1 day ago |
7-85559 7 days ago |
7-85601 7 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 |
1-42925 1 day ago |
1-85327 1 day ago |
1-85302 1 day |
| 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 |
1-39935 1 day ago |
21-35043 21 days ago |
21-35079 21 days |
| 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.
 |
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 |
1-30069 1 day ago |
5-32254 5 days ago |
5-32299 5 days |
| 32836 |
YaelDillies author:YaelDillies |
feat(Algebra): characterise when a submodule constructor is equal to `⊥` |
---
[](https://gitpod.io/from-referrer/)
|
t-algebra label:t-algebra$ |
36/3 |
Mathlib/Algebra/Algebra/NonUnitalSubalgebra.lean,Mathlib/Algebra/Group/Submonoid/Defs.lean,Mathlib/Algebra/Group/Subsemigroup/Defs.lean,Mathlib/Algebra/Module/Submodule/Lattice.lean |
4 |
7 |
['YaelDillies', 'erdOne', 'github-actions'] |
nobody |
1-29779 1 day ago |
1-29814 1 day ago |
1-61887 1 day |
| 26351 |
RemyDegenne author:RemyDegenne |
feat: covering and packing numbers of sets in a metric space |
We define covering numbers of sets in a pseudo-metric space, which are minimal cardinalities of
`ε`-covers of sets. We also define the packing number, which is the maximal cardinality of
an `ε`-separated set.
From the Brownian motion project.
---
- [x] depends on: #31537
[](https://gitpod.io/from-referrer/)
|
t-topology
brownian
|
212/0 |
Mathlib.lean,Mathlib/Topology/MetricSpace/CoveringNumbers.lean |
2 |
17 |
['ADedecker', 'RemyDegenne', 'YaelDillies', 'github-actions', 'j-loreaux', 'mathlib4-dependent-issues-bot', 'mathlib4-merge-conflict-bot'] |
j-loreaux assignee:j-loreaux |
1-20469 1 day ago |
1-21406 1 day ago |
46-59483 46 days |
| 32855 |
harahu author:harahu |
doc: fix file references |
This PR fixes some defective file references. I've verified that all the updated references are pointing to files that existed when this PR was created. I don't make any promises in terms of the files still containing what they are claimed to contain in the relevant context.
---
[](https://gitpod.io/from-referrer/)
|
|
60/55 |
Archive/Examples/MersennePrimes.lean,Mathlib/Algebra/Polynomial/Eval/Algebra.lean,Mathlib/AlgebraicGeometry/ProjectiveSpectrum/Basic.lean,Mathlib/AlgebraicGeometry/ProjectiveSpectrum/Scheme.lean,Mathlib/Analysis/Calculus/FDeriv/Add.lean,Mathlib/Analysis/Calculus/FDeriv/Comp.lean,Mathlib/Analysis/Calculus/FDeriv/Equiv.lean,Mathlib/Analysis/Calculus/FDeriv/Linear.lean,Mathlib/Analysis/Calculus/FDeriv/Prod.lean,Mathlib/Analysis/Calculus/FDeriv/RestrictScalars.lean,Mathlib/Analysis/Calculus/FDeriv/Star.lean,Mathlib/CategoryTheory/EffectiveEpi/Basic.lean,Mathlib/CategoryTheory/Limits/ConeCategory.lean,Mathlib/CategoryTheory/Limits/HasLimits.lean,Mathlib/CategoryTheory/Limits/Preserves/Finite.lean,Mathlib/CategoryTheory/Limits/Shapes/Equalizers.lean,Mathlib/CategoryTheory/Limits/Shapes/Kernels.lean,Mathlib/CategoryTheory/Sites/Coherent/SheafComparison.lean,Mathlib/Data/Finsupp/Option.lean,Mathlib/Data/Matrix/Invertible.lean,Mathlib/GroupTheory/GroupExtension/Defs.lean,Mathlib/LinearAlgebra/Dimension/RankNullity.lean,Mathlib/LinearAlgebra/Matrix/GeneralLinearGroup/Basic.lean,Mathlib/LinearAlgebra/Trace.lean,Mathlib/MeasureTheory/Measure/GiryMonad.lean,Mathlib/NumberTheory/LucasLehmer.lean,Mathlib/Probability/Independence/Conditional.lean,Mathlib/Probability/Kernel/CondDistrib.lean,Mathlib/RepresentationTheory/Homological/GroupCohomology/LowDegree.lean,Mathlib/RepresentationTheory/Homological/GroupCohomology/Shapiro.lean,Mathlib/RepresentationTheory/Homological/Resolution.lean,Mathlib/RingTheory/AlgebraTower.lean,Mathlib/RingTheory/Spectrum/Prime/TensorProduct.lean,Mathlib/SetTheory/Cardinal/Arithmetic.lean,Mathlib/Tactic/Linter/TextBased.lean,Mathlib/Tactic/SetLike.lean,Mathlib/Topology/Instances/Matrix.lean,Mathlib/Topology/Sheaves/SheafOfFunctions.lean,MathlibTest/FieldSimp.lean |
39 |
1 |
['github-actions'] |
nobody |
1-16344 1 day ago |
1-82359 1 day ago |
1-82334 1 day |
| 32671 |
themathqueen author:themathqueen |
chore(LinearAlgebra/GeneralLinearGroup/AlgEquiv): slightly generalize |
Also adds `trace (f x) = trace x` and `det (f x) = det x` for algebra equivalence `f`.
---
[](https://gitpod.io/from-referrer/)
|
t-algebra label:t-algebra$ |
64/17 |
Mathlib/LinearAlgebra/Determinant.lean,Mathlib/LinearAlgebra/GeneralLinearGroup/AlgEquiv.lean,Mathlib/LinearAlgebra/Trace.lean |
3 |
5 |
['erdOne', 'github-actions', 'themathqueen'] |
nobody |
1-15836 1 day ago |
2-24423 2 days ago |
5-52603 5 days |
| 32699 |
mirefek author:mirefek |
doc: update `use` doc-string to distinguish `exists` / `use` / `use!` |
Zulip discussion: [#general > use vs. exists @ 💬](https://leanprover.zulipchat.com/#narrow/channel/113488-general/topic/use.20vs.2E.20exists/near/562650656)
---
[](https://gitpod.io/from-referrer/)
|
t-meta
new-contributor
|
25/9 |
Mathlib/Tactic/Use.lean,MathlibTest/Use.lean |
2 |
3 |
['github-actions', 'mathlib4-merge-conflict-bot'] |
nobody |
1-15348 1 day ago |
1-15367 1 day ago |
5-5092 5 days |
| 31161 |
AntoineChambert-Loir author:AntoineChambert-Loir |
feat(RingTheory/MvPolynomial/IrrQuadratic): irreducibility of sum X_i Y_i |
The quadratic polynomial $$\sum_i c_i X_i Y_i$$ is irreducible, provided the following three conditions holds:
* the ground ring is a domain
* there are at least 2 nonzero $$c_i$$
* only units of $$R$$ divide all $$c_i$$.
This was used in the initial proof that the transvections have determinant 1. Now,
a more general result is proved there and this PR is no more needed.
I believe that it remains of independent interest (irreducibility of quadrics in algebraic geometry) but the maintainers might want that the general one.
---
- [x] depends on: #32226
[](https://gitpod.io/from-referrer/)
|
t-ring-theory |
320/3 |
Mathlib.lean,Mathlib/Algebra/MvPolynomial/Equiv.lean,Mathlib/Algebra/Polynomial/RingDivision.lean,Mathlib/Algebra/Prime/Lemmas.lean,Mathlib/Data/Finsupp/Defs.lean,Mathlib/Logic/Nontrivial/Defs.lean,Mathlib/RingTheory/MvPolynomial/IrreducibleQuadratic.lean,Mathlib/RingTheory/MvPolynomial/MonomialOrder/DegLex.lean,Mathlib/RingTheory/Polynomial/Nilpotent.lean |
9 |
63 |
['AntoineChambert-Loir', 'erdOne', 'github-actions', 'jcommelin', 'joelriou', 'mathlib4-dependent-issues-bot', 'mathlib4-merge-conflict-bot', 'ocfnash'] |
joelriou assignee:joelriou |
1-13217 1 day ago |
1-15440 1 day ago |
34-20126 34 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', 'vihdzp'] |
nobody |
1-12478 1 day ago |
1-64701 1 day ago |
1-64737 1 day |
| 32870 |
0xTerencePrime author:0xTerencePrime |
feat(Combinatorics/SimpleGraph): define edge-connectivity |
## Summary
This PR introduces k-edge-connectivity definitions for SimpleGraph, addressing #31691.
## Main Changes
- **New file:** `Mathlib/Combinatorics/SimpleGraph/Connectivity/EdgeConnectivity.lean`
### Definitions
- `IsEdgeReachable k u v`: vertices remain reachable after removing < k edges
- `IsEdgeConnected k`: graph is k-edge-connected
### Lemmas
- Basic properties: `rfl`, `symm`, `trans`, `mono`, `zero`
- `isEdgeReachable_one`: equivalence with standard `Reachable`
- `isEdgeConnected_one`: equivalence with `Preconnected`
- `isEdgeReachable_succ`: inductive characterization
- `isEdgeConnected_succ`: inductive characterization for graphs
- `isEdgeConnected_two`: equivalence with `Preconnected ∧ ¬∃ e, IsBridge e`
## Verification
- [x] `lake build` passes
- [x] `lake exe runLinter` passes
Closes #31691 |
t-combinatorics
new-contributor
|
154/0 |
Mathlib.lean,Mathlib/Combinatorics/SimpleGraph/Connectivity/EdgeConnectivity.lean |
2 |
1 |
['github-actions'] |
nobody |
1-12229 1 day ago |
1-32585 1 day ago |
1-32625 1 day |
| 32600 |
PrParadoxy author:PrParadoxy |
feat(LinearAlgebra/Multilinear): composition of multilinear maps |
The composition of a multilinear map with a family of multilinear maps
is a multilinear map indexed by a dependent sum.
The result reduces to a lemma about the interaction of function
application, `Sigma.curry`, and `Function.update`. This variant of
`Function.apply_update` is included as `Sigma.apply_curry_update`.
[](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-11187 1 day ago |
6-6055 6 days ago |
6-6319 6 days |
| 30293 |
vlad902 author:vlad902 |
feat(SimpleGraph): there exists a maximal path/trail in a graph with finite edges |
Inspired by [this Zulip thread](https://leanprover.zulipchat.com/#narrow/channel/252551-graph-theory/topic/Help.20me.20learn.20good.20style.3A.20IsTree/near/543395218)
---
[](https://gitpod.io/from-referrer/)
|
t-combinatorics |
29/0 |
Mathlib/Combinatorics/SimpleGraph/Paths.lean |
1 |
6 |
['SnirBroshi', 'github-actions', 'mathlib4-merge-conflict-bot', 'vlad902'] |
awainverse assignee:awainverse |
1-10706 1 day ago |
1-10706 1 day ago |
55-74893 55 days |
| 28546 |
Sfgangloff author:Sfgangloff |
feat(SymbolicDynamics): basic setup of Zd, full shift, cylinders, pat… |
This PR adds a **group-generic** foundation for symbolic dynamics over an arbitrary group `G`, together with convenient specializations for `ℤ` and `ℤ^d`.
Summary of additions:
- **Full shift and shift action**
- `abbrev FullShift (A G) := G → A` (inherits product topology from the Π-type).
- Right shift `shift g x` with convention `(shift g x) h = x (h * g)`.
- **Cylinders and topology**
- `cylinder U x : Set (G → A)` for finite `U : Finset G`.
- Cylinders are open under `[DiscreteTopology A]`; with a finite alphabet they are also closed.
- Equality with dependent products:
`cylinder U x = Set.pi (↑U) (fun i => ({x i} : Set A))`, enabling use of the `Set.pi` API.
- **Patterns, occurrences, and subshifts**
- `Pattern A G` with finite `support : Finset G` and `data : support → A`.
- `Pattern.occursIn p x g` (occurrence at translate `g`) and the expected shift law.
- `forbids F` and `Subshift A G` (closed, shift-invariant subsets).
- `FixedSupport A G U` with an equivalence to `(U → A)` to obtain finiteness.
- **Language on finite shapes and counting**
- `languageOn X U`, `languageCardOn X U`, and `patternCountOn Y U`.
- **Entropy along a shape sequence**
- `limsupAtTop` (as an `sInf` of eventual upper bounds).
- `entropyAlong X F hF := limsup (log (patternCountOn X (F n) + 1) / |F n|)`
for any nonempty finite shapes `F : ℕ → Finset G` (the `+ 1` avoids `log 0`).
- **Specializations**
- `IntShapes`: segments `[-n,n]` on `Multiplicative ℤ`, with `entropy_Z`.
- `ZdShapes`: boxes `[-n,n]^d` on `ℤ^d` (as functions `Fin d → ℤ`), with `entropy_Zd`.
Mathematical remarks:
- The API is **shape-parametric**: entropy is defined along user-provided finite shapes.
- On **amenable** groups, using a **Følner** sequence yields a canonical value (Ornstein–Weiss).
This PR does not assume amenability; the family of shapes is an explicit input.
Motivation:
Provide a clean, reusable base for symbolic dynamics on groups in mathlib.
Future work:
- Add a Følner predicate and prove shape-independence / limit existence on amenable groups.
- Expand the `ℤ`/`ℤ^d` toolkit (alternative shapes, mixing, factors).
- Develop 1D theory and, longer-term, multidimensional SFT results (e.g. along the lines of Hochman–Meyerovitch).
|
t-dynamics
new-contributor
|
759/1 |
Mathlib.lean,Mathlib/Dynamics/SymbolicDynamics/Basic.lean,Mathlib/Tactic/Translate/ToAdditive.lean |
3 |
154 |
['Sfgangloff', 'eric-wieser', 'github-actions', 'kckennylau', 'mathlib4-merge-conflict-bot', 'sgouezel'] |
sgouezel assignee:sgouezel |
1-10174 1 day ago |
1-10174 1 day ago |
77-28242 77 days |
| 32405 |
Shaddaaa author:Shaddaaa |
feat(CategoryTheory/Sites): (Co)continuity of `Over.iteratedSliceEquiv` |
Show that the `Over.iteratedSliceEquiv` functor is continuous and cocontinuous.
This contribution was created as part of the Heidelberg Lean workshop "Formalising algebraic geometry" in November 2025.
Co-authored-by: Ben Eltschig @peabrainiac
Co-authored-by: Andrew Yang @erdOne
---
[](https://gitpod.io/from-referrer/)
|
t-category-theory
new-contributor
maintainer-merge
large-import
|
44/4 |
Mathlib/CategoryTheory/Sites/Equivalence.lean,Mathlib/CategoryTheory/Sites/Over.lean |
2 |
29 |
['Shaddaaa', 'dagurtomas', 'erdOne', 'github-actions', 'jcommelin', 'joelriou'] |
nobody |
1-8097 1 day ago |
1-8097 1 day ago |
1-60552 1 day |
| 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 |
12 |
['SnirBroshi', 'Timeroot', 'github-actions', 'johnrathgeber'] |
nobody |
1-7768 1 day ago |
1-67028 1 day ago |
1-67067 1 day |
| 32672 |
tb65536 author:tb65536 |
feat: haar measures on short exact sequences |
This PR defines the notion of a short exact sequence of topological groups, and proves that if `1 → A → B → C → 1` is a short exact sequence of topological groups, then Haar measures on `A` and `C` induce a Haar measure on `B`.
The final result of the file is a consequence needed for FLT: If `B → C` is injective on an open set `U`, then `U` has bounded measure.
---
[](https://gitpod.io/from-referrer/)
|
t-topology
t-measure-probability
FLT
|
378/0 |
Mathlib.lean,Mathlib/MeasureTheory/Measure/Haar/Extension.lean,Mathlib/Topology/Algebra/Group/Extension.lean |
3 |
6 |
['RemyDegenne', 'github-actions', 'kbuzzard', 'tb65536'] |
nobody |
1-2730 1 day ago |
1-3136 1 day ago |
4-52641 4 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 |
2/2 |
Mathlib/Data/ENNReal/Inv.lean |
1 |
6 |
['euprunin', 'github-actions', 'leanprover-bot', 'leanprover-radar', 'mathlib4-merge-conflict-bot', 'metakunt'] |
TwoFX assignee:TwoFX |
1-807 1 day ago |
1-824 1 day ago |
17-69923 17 days |
| 32875 |
euprunin author:euprunin |
chore: golf using `grind` and `simp` |
---
Trace profiling results (shown if ≥10 ms before or after):
* `Finset.mem_map_equiv`: <10 ms before, 25 ms after
* `Rat.inv_intCast_den_of_pos`: <10 ms before, 17 ms after
* `MeasureTheory.Measure.pi_map_piCongrLeft`: 55 ms before, 48 ms after 🎉
* `MeasureTheory.tendsto_of_forall_isClosed_limsup_real_le'`: 268 ms before, <10 ms after 🎉
* `limsup_finset_sup'`: 64 ms before, 51 ms after 🎉
* `ProbabilityTheory.setLIntegral_condKernel_eq_measure_prod`: 69 ms before, 17 ms after 🎉
* `Metric.exists_lt_mem_ball_of_mem_ball`: 81 ms before, <10 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/)
|
|
16/53 |
Mathlib/Data/Finset/Image.lean,Mathlib/Data/Rat/Lemmas.lean,Mathlib/MeasureTheory/Constructions/Pi.lean,Mathlib/MeasureTheory/Measure/Portmanteau.lean,Mathlib/Order/LiminfLimsup.lean,Mathlib/Probability/Kernel/Disintegration/Integral.lean,Mathlib/Topology/MetricSpace/Pseudo/Defs.lean |
7 |
5 |
['euprunin', 'github-actions', 'vihdzp'] |
nobody |
1-272 1 day ago |
1-23706 1 day ago |
1-23681 1 day |
| 32882 |
DavidLedvinka author:DavidLedvinka |
feat(Probability): Rename `Adapted` to `StronglyAdapted` and add `Adapted ` |
Rename the currently named `Adapted` to `StronglyAdapted` (since it requires strong measurability) and add `Adapted`.
Also add theorems which state when one property implies the other and when they are equivalent. |
t-measure-probability |
197/128 |
Mathlib/Probability/Kernel/Disintegration/Density.lean,Mathlib/Probability/Martingale/Basic.lean,Mathlib/Probability/Martingale/BorelCantelli.lean,Mathlib/Probability/Martingale/Centering.lean,Mathlib/Probability/Martingale/Convergence.lean,Mathlib/Probability/Martingale/OptionalStopping.lean,Mathlib/Probability/Martingale/Upcrossing.lean,Mathlib/Probability/Moments/SubGaussian.lean,Mathlib/Probability/Process/Adapted.lean,Mathlib/Probability/Process/HittingTime.lean,Mathlib/Probability/Process/Predictable.lean,Mathlib/Probability/Process/Stopping.lean |
12 |
1 |
['github-actions'] |
nobody |
0-86394 23 hours ago |
1-971 1 day ago |
1-1005 1 day |
| 30860 |
FormulaRabbit81 author:FormulaRabbit81 |
feat(MeasureTheory): the space of probability measures on a compact space is compact |
---
- [x] depends on: #30845
- [x] depends on: #28061
- [x] depends on #31656
- [x] depends on #31964
[](https://gitpod.io/from-referrer/) |
|
165/24 |
Mathlib/Algebra/Order/Module/PositiveLinearMap.lean,Mathlib/MeasureTheory/Measure/LevyProkhorovMetric.lean,Mathlib/MeasureTheory/Measure/ProbabilityMeasure.lean,Mathlib/Topology/ContinuousMap/CompactlySupported.lean |
4 |
10 |
['FormulaRabbit81', 'YaelDillies', 'github-actions', 'mathlib4-dependent-issues-bot', 'mathlib4-merge-conflict-bot'] |
nobody |
0-83635 23 hours ago |
1-3328 1 day ago |
1-3775 1 day |
| 31908 |
YaelDillies author:YaelDillies |
feat: set-valued product of bernoulli random variables |
Define the product distribution of `p`-Bernoulli random variables a measure on `Set ι`.
It is important in applications to be able to restrict the product to a subset `u` of `ι`, eg in #31364 I define the `G(V, p)` distribution of binomial random graphs by setting `ι := Sym2 V` and `u := {e |¬ e.IsDiag}`.
---
- [x] depends on: #31909
- [x] depends on: #31911
- [x] depends on: #32096
- [x] depends on: #32287
[](https://gitpod.io/from-referrer/)
|
t-measure-probability |
147/7 |
Mathlib.lean,Mathlib/Probability/Distributions/SetBernoulli.lean,Mathlib/Probability/HasLaw.lean |
3 |
12 |
['DavidLedvinka', 'RemyDegenne', 'YaelDillies', 'github-actions', 'mathlib4-dependent-issues-bot', 'mathlib4-merge-conflict-bot', 'sgouezel'] |
sgouezel assignee:sgouezel |
0-81648 22 hours ago |
1-28129 1 day ago |
17-80281 17 days |
| 32382 |
YaelDillies author:YaelDillies |
chore(Algebra/Order/AddGroupWithTop): golf |
---
[](https://gitpod.io/from-referrer/)
|
t-algebra label:t-algebra$ |
108/153 |
Mathlib/Algebra/Order/AddGroupWithTop.lean,Mathlib/Algebra/Order/GroupWithZero/Canonical.lean,Mathlib/Algebra/Order/Ring/Archimedean.lean |
3 |
2 |
['github-actions', 'vihdzp'] |
dagurtomas assignee:dagurtomas |
0-81288 22 hours ago |
12-22014 12 days ago |
12-41683 12 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$ |
118/10 |
Mathlib.lean,Mathlib/RepresentationTheory/Irreducible.lean,Mathlib/RepresentationTheory/Subrepresentation.lean |
3 |
15 |
['Whysoserioushah', 'github-actions', 'stepan2698-cpu'] |
nobody |
0-79686 22 hours ago |
1-80012 1 day ago |
1-80048 1 day |
| 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 |
3-60019 3 days ago |
3-60033 3 days ago |
3-60066 3 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 |
3-60882 3 days ago |
3-61956 3 days ago |
3-62000 3 days |
| 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 |
23-27189 23 days ago |
26-31289 26 days ago |
0-546 9 minutes |
| 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'] |
jcommelin assignee:jcommelin |
0-68590 19 hours ago |
6-1853 6 days ago |
6-1837 6 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'] |
mariainesdff assignee:mariainesdff |
0-68588 19 hours ago |
4-17740 4 days ago |
9-9494 9 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'] |
j-loreaux assignee:j-loreaux |
0-68587 19 hours ago |
4-16577 4 days ago |
6-85207 6 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'] |
dagurtomas assignee:dagurtomas |
0-68586 19 hours ago |
3-71926 3 days ago |
3-76927 3 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'] |
b-mehta assignee:b-mehta |
0-68585 19 hours ago |
6-9256 6 days ago |
6-9290 6 days |
| 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'] |
j-loreaux assignee:j-loreaux |
0-68585 19 hours ago |
5-74741 5 days ago |
5-75344 5 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'] |
dagurtomas assignee:dagurtomas |
0-68582 19 hours ago |
4-21635 4 days ago |
4-21654 4 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'] |
dupuisf assignee:dupuisf |
0-68581 19 hours ago |
4-15190 4 days ago |
4-15223 4 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'] |
j-loreaux assignee:j-loreaux |
0-68580 19 hours ago |
4-1852 4 days ago |
4-1828 4 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-64576 17 hours ago |
2-67761 2 days ago |
2-67794 2 days |
| 32886 |
alreadydone author:alreadydone |
refactor(Algebra/Order): change `MulArchimedeanClass.subgroup` to `FiniteArchimedeanClass.subgroup` |
This gets rid of a junk value without much modification the main HahnEmbedding application.
---
[](https://gitpod.io/from-referrer/)
|
t-algebra
t-order
label:t-algebra$ |
297/156 |
Mathlib/Algebra/Order/Archimedean/Class.lean,Mathlib/Algebra/Order/Module/Archimedean.lean,Mathlib/Algebra/Order/Module/HahnEmbedding.lean |
3 |
3 |
['alreadydone', 'github-actions', 'wwylele'] |
nobody |
0-61175 16 hours ago |
0-61375 17 hours ago |
0-61352 17 hours |
| 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-58467 16 hours ago |
6-30462 6 days ago |
6-30507 6 days |
| 32888 |
staroperator author:staroperator |
feat(Tactic/FunProp): make `fun_prop` able to tag `→` and `∀` |
by representing forall as a function application internally. Also tag `Measurable.imp` and `Measurable.forall` which were rejected by `fun_prop`.
---
[](https://gitpod.io/from-referrer/)
|
t-meta
large-import
|
14/1 |
Mathlib/MeasureTheory/MeasurableSpace/Constructions.lean,Mathlib/Tactic/FunProp/Mor.lean |
2 |
1 |
['github-actions'] |
nobody |
0-52538 14 hours ago |
0-52538 14 hours ago |
0-56168 15 hours |
| 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 |
0-50930 14 hours ago |
4-64971 4 days ago |
23-78925 23 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
|
240/4 |
Mathlib/Analysis/SpecialFunctions/Log/Deriv.lean,Mathlib/Computability/AkraBazzi/SumTransform.lean,Mathlib/NumberTheory/AbelSummation.lean,Mathlib/NumberTheory/Chebyshev.lean |
4 |
17 |
['Ruben-VandeVelde', 'ajirving', 'github-actions', 'loefflerd', 'mathlib4-dependent-issues-bot', 'mathlib4-merge-conflict-bot'] |
nobody |
0-42133 11 hours ago |
2-35908 2 days ago |
5-50241 5 days |
| 32892 |
Parcly-Taxel author:Parcly-Taxel |
feat(Analysis/SpecialFunctions): arithmetic-geometric mean |
|
t-analysis |
243/0 |
Mathlib.lean,Mathlib/Analysis/SpecialFunctions/AGM.lean |
2 |
1 |
['github-actions'] |
nobody |
0-40650 11 hours ago |
0-40656 11 hours ago |
0-40696 11 hours |
| 32861 |
JovanGerb author:JovanGerb |
feat: avoid `private irreducible_def` using module system |
This PR removes the instances of `private irreducible_def`, replacing them with a module system based solution, using `@[no_expose]` to not expose the definition. This helps make proofs shorter, while still not exporting the value of the definition.
One case required `set_option backward.proofsInPublic false` to work. Note that this is turning off the backwards option that is globally set to `true`. The eventual aim is to have it globally `false`, so setting it to `false` locally is not a problem.
In order to do this refactor, I locally set
```
set_option backward.proofsInPublic false
set_option backward.privateInPublic false
```
so that the module system is happy with the new version.
---
[](https://gitpod.io/from-referrer/)
|
|
85/131 |
Mathlib/Algebra/Polynomial/Basic.lean,Mathlib/Algebra/RingQuot.lean,Mathlib/Algebra/SkewMonoidAlgebra/Basic.lean,Mathlib/Algebra/Star/RingQuot.lean,Mathlib/Data/Finsupp/Defs.lean |
5 |
4 |
['JovanGerb', 'github-actions', 'jcommelin', 'leanprover-radar', 'vihdzp'] |
nobody |
0-33441 9 hours ago |
1-17423 1 day ago |
1-65824 1 day |
| 32894 |
harahu author:harahu |
doc(Geometry): fix typos |
Typos found and fixed by Codex.
---
[](https://gitpod.io/from-referrer/)
|
|
34/33 |
Mathlib/Geometry/Euclidean/Angle/Oriented/Affine.lean,Mathlib/Geometry/Euclidean/Angle/Sphere.lean,Mathlib/Geometry/Euclidean/Congruence.lean,Mathlib/Geometry/Euclidean/Inversion/Basic.lean,Mathlib/Geometry/Euclidean/SignedDist.lean,Mathlib/Geometry/Manifold/Algebra/LeftInvariantDerivation.lean,Mathlib/Geometry/Manifold/Algebra/LieGroup.lean,Mathlib/Geometry/Manifold/ChartedSpace.lean,Mathlib/Geometry/Manifold/DerivationBundle.lean,Mathlib/Geometry/Manifold/Immersion.lean,Mathlib/Geometry/Manifold/Instances/Real.lean,Mathlib/Geometry/Manifold/IsManifold/ExtChartAt.lean,Mathlib/Geometry/Manifold/IsManifold/InteriorBoundary.lean,Mathlib/Geometry/Manifold/LocalSourceTargetProperty.lean,Mathlib/Geometry/Manifold/MFDeriv/Atlas.lean,Mathlib/Geometry/Manifold/MFDeriv/Tangent.lean,Mathlib/Geometry/Manifold/Riemannian/PathELength.lean,Mathlib/Geometry/Manifold/VectorBundle/Hom.lean,Mathlib/Geometry/Manifold/VectorBundle/Riemannian.lean |
19 |
1 |
['github-actions'] |
nobody |
0-28947 8 hours ago |
0-37518 10 hours ago |
0-37493 10 hours |
| 32701 |
sgouezel author:sgouezel |
feat: Prokhorov theorem |
We prove a version of Prokhorov theorem: given a sequence of compact sets `Kₙ` and a sequence `uₙ` tending to zero, the probability measures giving mass at most `uₙ` to the complement of `Kₙ` form a compact set. We only assume that the space is T2 and normal (no metrizability, no second-countability).
---
The PR is somewhat long, but to me it looks like a coherent unit, so it makes sense to keep it like that. If you think it's too long to review and you'd rather have smaller chunks, just tell me and I'll split it.
- [x] depends on: #32778
- [x] depends on: #32779
- [x] depends on: #32783
- [x] depends on: #32784
- [x] depends on: #32785
- [x] depends on: #32786
[](https://gitpod.io/from-referrer/)
|
t-measure-probability |
479/0 |
Mathlib.lean,Mathlib/MeasureTheory/Measure/FiniteMeasure.lean,Mathlib/MeasureTheory/Measure/ProbabilityMeasure.lean,Mathlib/MeasureTheory/Measure/Prokhorov.lean |
4 |
3 |
['github-actions', 'mathlib4-dependent-issues-bot', 'mathlib4-merge-conflict-bot'] |
nobody |
0-26343 7 hours ago |
0-26433 7 hours ago |
1-16958 1 day |
| 32898 |
riccardobrasca author:riccardobrasca |
feat(RepresentationTheory/Homological/GroupCohomology): cohomology of finite cyclic groups |
Let `k` be a commutative ring, `G` a group and `A` a `k`-linear `G`-representation. Given endomorphisms `φ, ψ : A ⟶ A` such that `φ ∘ ψ = ψ ∘ φ = 0`. Denote by `Chains(A, φ, ψ)` the periodic chain complex `... ⟶ A --φ--> A --ψ--> A --φ--> A --ψ--> A ⟶ 0` and by `Cochains(A, φ, ψ)` the periodic cochain complex `0 ⟶ A --ψ--> A --φ--> A --ψ--> A --φ--> A ⟶ ...`.
When `G` is finite and generated by `g : G`, then `P := Chains(k[G], N, ρ(g) - Id)` (with `ρ` the left regular representation) is a projective resolution of `k` as a trivial representation. In this PR we show that for `A : Rep k G`, `Hom(P, A)` is isomorphic to
`Cochains(A, N, ρ_A(g) - Id)` as a complex of `k`-modules, and hence the cohomology of this complex computes group cohomology.
Co-authored-by: [101damnations](https://github.com/101damnations)
---
This was originally #27364, and Amelia did all the work, I am just adopting the PR.
[](https://gitpod.io/from-referrer/)
|
t-algebra label:t-algebra$ |
145/3 |
Mathlib.lean,Mathlib/RepresentationTheory/Homological/FiniteCyclic.lean,Mathlib/RepresentationTheory/Homological/GroupCohomology/FiniteCyclic.lean |
3 |
4 |
['copilot-pull-request-reviewer', 'github-actions'] |
nobody |
0-22591 6 hours ago |
0-23796 6 hours ago |
0-23786 6 hours |
| 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 |
6-55624 6 days ago |
6-55624 6 days ago |
67-48813 67 days |
| 32901 |
felixpernegger author:felixpernegger |
refactor(Data/Nat/Choose): Merge Basic.lean and Mul.lean |
Previously, Mul.lean contained two very basic identities about polynomial coefficients and was its own file due to the use of ```ring```.
I replaced the usage of ```ring``` via some rewrites (not too bad), making it possible to merge Mul.lean into Basic.lean (which is appropriate content-wise).
Sidenote: The list of authors is now over 100 characters long. I did not find another file where this is the case, so I don''t know what is the standard format in this case. |
new-contributor |
34/43 |
Mathlib/Combinatorics/Enumerative/Bell.lean,Mathlib/Data/Nat/Choose/Basic.lean,Mathlib/Data/Nat/Choose/Mul.lean |
3 |
1 |
['github-actions'] |
nobody |
0-22166 6 hours ago |
0-22166 6 hours ago |
0-22569 6 hours |
| 32776 |
pirapira author:pirapira |
feat: grind and aesop annotations for ZMod |
This PR adds some `grind` and `aesop` annotations to `ZMod`.
This PR is not meant to annotate exhaustively. (That requires `guard` feature of `grind_pattern`, which is only available in nightly).
This work is produced as part of Italean 2025 project "improving automation". |
new-contributor |
10/5 |
Mathlib/Data/ZMod/Basic.lean,Mathlib/Data/ZMod/ValMinAbs.lean,Mathlib/NumberTheory/LegendreSymbol/ZModChar.lean,MathlibTest/aesop/zmod.lean |
4 |
7 |
['euprunin', 'github-actions', 'pirapira'] |
nobody |
0-17349 4 hours ago |
0-18833 5 hours ago |
1-11373 1 day |
| 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
maintainer-merge
|
94/3 |
Mathlib.lean,Mathlib/Geometry/Manifold/Immersion.lean,Mathlib/Geometry/Manifold/SmoothEmbedding.lean |
3 |
21 |
['chrisflav', 'github-actions', 'grunweg', 'mathlib4-dependent-issues-bot', 'peabrainiac'] |
PatrickMassot assignee:PatrickMassot |
0-33759 9 hours ago |
0-34934 9 hours ago |
5-38986 5 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 |
74-35362 2 months ago |
74-35363 2 months ago |
134-68375 134 days |
| 26831 |
AntoineChambert-Loir author:AntoineChambert-Loir |
feat(GroupTheory/SpecificGroups/Alternating/MaximalSubgroups): maximal subgroups of the alternating group |
This proves the first case (intransitive) of the O'Nan-Scott classification of maximal subgroups of the alternating group.
---
- [x] depends on: #26457
- [x] depends on: #26282
- [x] depends on: #26281
- [x] depends on: #26280
- [x] depends on: #26279
[](https://gitpod.io/from-referrer/)
|
t-group-theory |
520/174 |
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-14062 3 hours ago |
unknown |
unknown |
| 32887 |
artie2000 author:artie2000 |
chore(Algebra): consistently tag `mem_sInf`, `mem_iInf`, `coe_sInf`, `coe_iInf` |
* Consistently tag `mem_sInf`, `mem_iInf` as `simp` across all algebraic substructures
* Consistently tag `coe_sInf`, `coe_iInf` as `simp, norm_cast` across all algebraic substructures
---
[](https://gitpod.io/from-referrer/)
|
t-algebra
maintainer-merge
label:t-algebra$ |
25/7 |
Mathlib/Algebra/Algebra/NonUnitalSubalgebra.lean,Mathlib/Algebra/Algebra/Subalgebra/Lattice.lean,Mathlib/Algebra/Field/Subfield/Basic.lean,Mathlib/Algebra/Group/Subgroup/Lattice.lean,Mathlib/Algebra/Group/Submonoid/Basic.lean,Mathlib/Algebra/Group/Subsemigroup/Basic.lean,Mathlib/Algebra/Module/Submodule/Lattice.lean,Mathlib/Algebra/Ring/Subring/Basic.lean,Mathlib/Algebra/Ring/Subsemiring/Basic.lean,Mathlib/Algebra/Star/NonUnitalSubalgebra.lean,Mathlib/Algebra/Star/Subalgebra.lean,Mathlib/RingTheory/NonUnitalSubring/Basic.lean,Mathlib/RingTheory/NonUnitalSubsemiring/Basic.lean |
13 |
4 |
['YaelDillies', 'artie2000', 'github-actions', 'vihdzp'] |
nobody |
0-13393 3 hours ago |
0-13393 3 hours ago |
0-60070 16 hours |
| 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 |
2 |
['github-actions', 'jcommelin'] |
nobody |
0-12882 3 hours ago |
0-12899 3 hours ago |
2-53258 2 days |
| 27542 |
chrisflav author:chrisflav |
feat(RingTheory/KrullDimension): dimension of polynomial ring |
We show that for a Noetherian ring `R`, `dim R[X] = dim R + 1`.
Co-authored by: Sihan Su
Co-authored by: Yi Song
---
- [x] depends on: #27520
- [x] depends on: #27538
- [x] depends on: #27510
- [x] depends on: #32472
[](https://gitpod.io/from-referrer/)
|
awaiting-author
large-import
t-ring-theory
|
123/0 |
Mathlib/Order/KrullDimension.lean,Mathlib/RingTheory/Ideal/Height.lean,Mathlib/RingTheory/KrullDimension/Polynomial.lean,Mathlib/RingTheory/Localization/AtPrime/Basic.lean |
4 |
n/a |
['erdOne', 'github-actions', 'mathlib4-dependent-issues-bot', 'mathlib4-merge-conflict-bot'] |
nobody |
2-5211 2 days ago |
unknown |
unknown |
| 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 |
65/11 |
Mathlib/Combinatorics/SimpleGraph/Maps.lean,Mathlib/Order/RelIso/Basic.lean |
2 |
7 |
['YaelDillies', 'github-actions', 'vlad902'] |
YaelDillies assignee:YaelDillies |
0-77576 21 hours ago |
1-23091 1 day ago |
15-27069 15 days |
| 32251 |
joelriou author:joelriou |
feat(AlgebraicTopology): binary products of finite simplicial sets are finite |
If `X₁` and `X₂` are respectively of dimensions `≤ d₁` and `≤ d₂`, then `X₁ ⊗ X₂` has dimension `≤ d₁ + d₂`. We also show that if `X₁` and `X₂` are finite, then `X₁ ⊗ X₂` is also finite.
From https://github.com/joelriou/topcat-model-category
- [x] depends on: #32201
- [x] depends on: #32202
- [x] depends on: #32237
---
[](https://gitpod.io/from-referrer/)
|
t-algebraic-topology |
131/2 |
Mathlib.lean,Mathlib/AlgebraicTopology/SimplicialSet/FiniteProd.lean,Mathlib/AlgebraicTopology/SimplicialSet/Monoidal.lean,Mathlib/AlgebraicTopology/SimplicialSet/NonDegenerateSimplices.lean,Mathlib/AlgebraicTopology/SimplicialSet/StdSimplex.lean |
5 |
5 |
['github-actions', 'mathlib4-dependent-issues-bot', 'mathlib4-merge-conflict-bot'] |
nobody |
0-11066 3 hours ago |
0-17948 4 hours ago |
0-34948 9 hours |
| 31478 |
BGuillemet author:BGuillemet |
feat(CategoryTheory/Sites): `uliftYoneda` for sheaves over a subcanonical topology |
Add that `GrothendieckTopology.uliftYoneda` is fully faithful.
Add the (functorial) Yoneda lemma for sheaves, for both `yoneda` and `uliftYoneda`.
---
- [x] depends on: #27821
- [x] depends on: #31538
[](https://gitpod.io/from-referrer/)
|
awaiting-author
t-category-theory
|
88/1 |
Mathlib/CategoryTheory/Sites/Canonical.lean,Mathlib/CategoryTheory/Sites/Subcanonical.lean,Mathlib/CategoryTheory/Sites/Whiskering.lean |
3 |
16 |
['BGuillemet', 'dagurtomas', 'github-actions', 'joelriou', 'mathlib4-dependent-issues-bot', 'mathlib4-merge-conflict-bot'] |
dagurtomas assignee:dagurtomas |
5-14148 5 days ago |
5-14148 5 days ago |
7-30702 7 days |
| 32652 |
BGuillemet author:BGuillemet |
feat(CategoryTheory/Sites): add the Grothendieck topology generated by a precoverage |
Add the file `PrecoverageToGrothendieck.lean`, in which the Grothendieck topology generated by a precoverage is defined as `Precoverage.toGrothendieck`. This replace the previous `Precoverage.toGrothendieck`, which was defined only in the case of a precoverage having pullbacks and being stable under base change. The equivalence between the two constructions is `Precoverage.toGrothendieck_toCoverage`.
Prove `Precoverage.isSheaf_toGrothendieck_iff`: given a precoverage `J`, a type-valued presheaf is a sheaf for `J.toGrothendieck` if and only if it is a sheaf for all the pullback sieves of the presieves in `J`. The proof is based on the previous proof of `isSheaf_coverage`, which is now a consequence of `Precoverage.isSheaf_toGrothendieck_iff`.
---
[](https://gitpod.io/from-referrer/)
|
t-category-theory
maintainer-merge
|
237/106 |
Mathlib.lean,Mathlib/CategoryTheory/Sites/Coverage.lean,Mathlib/CategoryTheory/Sites/Over.lean,Mathlib/CategoryTheory/Sites/PrecoverageToGrothendieck.lean |
4 |
22 |
['BGuillemet', 'chrisflav', 'github-actions'] |
nobody |
0-9706 2 hours ago |
0-9706 2 hours ago |
1-49068 1 day |
| 32889 |
artie2000 author:artie2000 |
feat(Algebra): forgetful lemmas for `map` and `comap` on substructures |
* Standardise the form of forgetful lemmas for `map` and `comap` (ie, `(co)map_toSubfoo`)
* Add missing lemmas of this form
* Mark all such lemmas as `simp`
---
[](https://gitpod.io/from-referrer/)
|
t-algebra label:t-algebra$ |
73/17 |
Mathlib/Algebra/Algebra/NonUnitalSubalgebra.lean,Mathlib/Algebra/Algebra/Subalgebra/Basic.lean,Mathlib/Algebra/Group/Subgroup/Map.lean,Mathlib/Algebra/Module/Submodule/Map.lean,Mathlib/Algebra/Ring/Subsemiring/Basic.lean,Mathlib/Algebra/Star/Subalgebra.lean |
6 |
6 |
['YaelDillies', 'artie2000', 'github-actions', 'vihdzp'] |
nobody |
0-9550 2 hours ago |
0-54426 15 hours ago |
0-54467 15 hours |
| 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/)
|
awaiting-author
t-algebra
label:t-algebra$ |
339/1 |
Mathlib.lean,Mathlib/Algebra/Order/Ring/Archimedean.lean,Mathlib/Algebra/Order/Ring/StandardPart.lean,Mathlib/Order/Quotient.lean |
4 |
69 |
['YaelDillies', 'github-actions', 'mathlib4-dependent-issues-bot', 'mathlib4-merge-conflict-bot', 'plp127', 'vihdzp', 'wwylele'] |
joneugster assignee:joneugster |
0-60014 16 hours ago |
0-81531 22 hours ago |
12-8007 12 days |
| 32811 |
erdOne author:erdOne |
feat(RingTheory): predicate on satisfying Zariski's main theorem |
---
[](https://gitpod.io/from-referrer/)
|
t-ring-theory |
173/0 |
Mathlib.lean,Mathlib/Algebra/Algebra/Subalgebra/Lattice.lean,Mathlib/RingTheory/Localization/Away/Basic.lean,Mathlib/RingTheory/ZariskisMainTheorem.lean |
4 |
4 |
['erdOne', 'github-actions', 'joelriou'] |
nobody |
1-13701 1 day ago |
1-13701 1 day ago |
2-81161 2 days |
| 32401 |
ADedecker author:ADedecker |
feat: monotonicity of D^n(U) in n and in U as CLMs |
---
[](https://gitpod.io/from-referrer/)
|
merge-conflict
t-analysis
|
177/3 |
Mathlib/Analysis/Distribution/ContDiffMapSupportedIn.lean,Mathlib/Analysis/Distribution/TestFunction.lean |
2 |
n/a |
['ADedecker', 'faenuccio', 'github-actions', 'mathlib4-merge-conflict-bot'] |
nobody |
3-15224 3 days ago |
unknown |
unknown |
| 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 |
14-24516 14 days ago |
14-31821 14 days ago |
17-19621 17 days |
| 32780 |
Hagb author:Hagb |
feat(RingTheory/MvPolynomial/MonomialOrder): generalize some `IsRegular` hypotheses to `∈ nonZeroDivisors` |
Similar with #25925, some theorems hypothesizing regular element(s) are generalized to hypothesize non zero-divisors.
---
It is also for similar generalization in #29203.
- [ ] depends on: #32774
[](https://gitpod.io/from-referrer/)
|
blocked-by-other-PR
large-import
|
64/10 |
Mathlib/Algebra/GroupWithZero/NonZeroDivisors.lean,Mathlib/RingTheory/MvPolynomial/Groebner.lean,Mathlib/RingTheory/MvPolynomial/MonomialOrder.lean |
3 |
2 |
['github-actions', 'mathlib4-dependent-issues-bot'] |
nobody |
1-73216 1 day ago |
3-37615 3 days ago |
0-2671 44 minutes |
| 32910 |
felixpernegger author:felixpernegger |
feat(Data/Nat/Choose): two binomial coefficient sum identities |
This PR proves two well-known sum identities around binomial coefficients.
While there are probably hundreds of such identities, these two seem to be well known enough to be in mathlib (i.e. are mentioned in the Wikipedia [article](https://en.wikipedia.org/wiki/Binomial_coefficient#math_8) about binomial coefficients). |
new-contributor
t-data
|
31/0 |
Mathlib/Data/Nat/Choose/Sum.lean,Mathlib/Data/Nat/Choose/Vandermonde.lean |
2 |
1 |
['github-actions'] |
nobody |
0-3931 1 hour ago |
0-18145 5 hours ago |
0-18473 5 hours |
| 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 |
2-39430 2 days ago |
4-74947 4 days ago |
13-39807 13 days |
| 32427 |
YaelDillies author:YaelDillies |
refactor(Algebra/Algebra): genericise algebra instances for subsemirings |
From ClassFieldTheory
---
[](https://gitpod.io/from-referrer/)
|
merge-conflict
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 |
2 |
['github-actions', 'mathlib4-merge-conflict-bot'] |
joelriou assignee:joelriou |
0-19019 5 hours ago |
0-19020 5 hours ago |
11-9069 11 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 |
3-38362 3 days ago |
4-16594 4 days ago |
4-16674 4 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', 'vlad902'] |
nobody |
0-2590 43 minutes ago |
4-80867 4 days ago |
4-80903 4 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 |
3-68575 3 days ago |
7-61080 7 days ago |
7-61123 7 days |
| 32911 |
erdOne author:erdOne |
feat(Analysis): ℘ is analytic |
---
[](https://gitpod.io/from-referrer/)
|
t-analysis |
322/1 |
Mathlib/Analysis/SpecialFunctions/Elliptic/Weierstrass.lean,Mathlib/Topology/Order/IsLUB.lean |
2 |
1 |
['github-actions'] |
nobody |
0-1737 28 minutes ago |
0-1737 28 minutes ago |
0-13386 3 hours |
| 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 |
19 |
['bjornsolheim', 'github-actions', 'jcommelin', 'ocfnash'] |
nobody |
0-40282 11 hours ago |
2-26911 2 days ago |
13-25567 13 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
|
139/0 |
Mathlib/ModelTheory/Definability.lean |
1 |
58 |
['NoneMore', 'github-actions', 'staroperator'] |
nobody |
0-1392 23 minutes ago |
3-53244 3 days ago |
4-12149 4 days |
| 32920 |
ocfnash author:ocfnash |
feat: there exists a linear form not vanishing on any finite collection of vectors |
Provided this is not false for trivial reasons (finite coefficients or one of the vectors is zero).
---
Work toward https://github.com/leanprover-community/mathlib4/issues/28717
[](https://gitpod.io/from-referrer/)
|
easy
t-algebra
large-import
label:t-algebra$ |
8/1 |
Mathlib/Algebra/Module/Submodule/Union.lean |
1 |
2 |
['github-actions', 'ocfnash'] |
nobody |
0-1173 19 minutes ago |
0-3503 57 minutes ago |
0-3537 58 minutes |
| 32922 |
ocfnash author:ocfnash |
feat: miscellaneous lemmas about root systems |
These are useful when proving that a root system has a base.
---
Work toward https://github.com/leanprover-community/mathlib4/issues/28717
[](https://gitpod.io/from-referrer/)
|
t-algebra label:t-algebra$ |
63/11 |
Mathlib/LinearAlgebra/PerfectPairing/Restrict.lean,Mathlib/LinearAlgebra/RootSystem/BaseChange.lean,Mathlib/LinearAlgebra/RootSystem/Finite/Nondegenerate.lean,Mathlib/LinearAlgebra/RootSystem/IsValuedIn.lean |
4 |
1 |
['github-actions'] |
nobody |
0-1163 19 minutes ago |
0-3233 53 minutes ago |
0-3209 53 minutes |
| 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 |
11 |
['CoolRmal', 'github-actions', 'plp127'] |
nobody |
0-845 14 minutes ago |
1-84459 1 day ago |
1-85763 1 day |