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 |
20-80992 20 days ago |
24-6163 24 days ago |
37-8087 37 days |
| 30886 |
urkud author:urkud |
feat(DifferentialForm): exterior derivative applied to vector fields |
---
- [ ] depends on: #30331
[](https://gitpod.io/from-referrer/)
|
t-analysis |
217/0 |
Mathlib.lean,Mathlib/Analysis/Calculus/DifferentialForm/VectorField.lean,Mathlib/Analysis/Calculus/FDeriv/ContinuousAlternatingMap.lean,Mathlib/Topology/Algebra/Module/Alternating/Basic.lean |
4 |
4 |
['github-actions', 'mathlib4-dependent-issues-bot', 'mathlib4-merge-conflict-bot'] |
kex-y assignee:kex-y |
16-46118 16 days ago |
17-59085 17 days ago |
26-27545 26 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 |
15-46120 15 days ago |
19-13409 19 days ago |
19-13382 19 days |
| 28944 |
linesthatinterlace author:linesthatinterlace |
refactor(Order/Hom/Basic): reorder definitions |
Reorder and disentangle definitions for OrderHom, OrderEmbedding and OrderIso.
---
This is a preamble to making all of these `def` and consistently defined - the aim is to first disentangle the definitions as it will make it more straightforward to perform these later PRs.
[](https://gitpod.io/from-referrer/)
|
t-order |
215/180 |
Mathlib/Order/Hom/Basic.lean |
1 |
17 |
['YaelDillies', 'github-actions', 'linesthatinterlace', 'mathlib4-merge-conflict-bot'] |
b-mehta and linesthatinterlace assignee:b-mehta assignee:linesthatinterlace |
15-17661 15 days ago |
18-76049 18 days ago |
44-82148 44 days |
| 31987 |
saodimao20 author:saodimao20 |
feat: add monotonicity and relation lemmas for mgf and cgf |
Add two lemmas about moment-generating and cumulant-generating functions:
- `mgf_mono_in_t_of_nonneg`: For nonnegative random variables, the mgf is monotone in the parameter `t`
- `cgf_zero_of_mgf_one`: The cgf equals zero iff the mgf equals one
These lemmas are useful for studying properties of mgf and cgf in probability theory.
Contributed by sequential-intelligence-lab(SIL), University of Virginia
---
[](https://gitpod.io/from-referrer/)
|
t-measure-probability
new-contributor
|
21/0 |
Mathlib/Probability/Moments/Basic.lean |
1 |
5 |
['DavidLedvinka', 'github-actions'] |
RemyDegenne assignee:RemyDegenne |
14-52707 14 days ago |
20-25578 20 days ago |
20-25613 20 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 |
13-46102 13 days ago |
17-6267 17 days ago |
20-3933 20 days |
| 30921 |
EtienneC30 author:EtienneC30 |
feat: characterizing Gaussian measures through the shape of the characteristic function |
Prove that Gaussian measures over a Banach space `E` are exactly those measures `μ` such that there exist `m : E` and `f : StrongDual ℝ E →L[ℝ] StrongDual ℝ E →L[ℝ] ℝ` satisfying `f.toBilinForm.IsPosSemidef` and `charFunDual μ L = exp (L m * I - f L L / 2)`.
Prove that such `m` and `f` are unique and equal to `∫ x, x ∂μ` and `covarianceBilinDual μ`.
Specialize these statements in the case of Hilbert spaces, with `f : E →L[ℝ] E →L[ℝ] ℝ`, `charFun μ t = exp (⟪t, m⟫ * I - f t t / 2)` and `f = covarianceBilin μ`.
---
- [x] depends on: #30371
- [x] depends on: #31564
- [x] depends on: #31566
- [x] depends on: #31567
from BrownianMotion
[](https://gitpod.io/from-referrer/)
|
t-measure-probability
brownian
|
206/0 |
Mathlib.lean,Mathlib/Probability/Distributions/Gaussian/CharFun.lean,Mathlib/Probability/Moments/CovarianceBilinDual.lean |
3 |
4 |
['RemyDegenne', 'github-actions', 'mathlib4-dependent-issues-bot', 'mathlib4-merge-conflict-bot'] |
kex-y assignee:kex-y |
13-46100 13 days ago |
17-7313 17 days ago |
17-31804 17 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 |
12-46093 12 days ago |
15-67661 15 days ago |
15-67643 15 days |
| 31891 |
jsm28 author:jsm28 |
feat(Geometry/Euclidean/Sphere/OrthRadius): lemmas for setting up and using polars |
Add further lemmas about `orthRadius` that are of use in setting up and using poles and polars. In particular,
`ncard_inter_orthRadius_eq_two_of_dist_lt_radius` is the key part of showing that, in two dimensions, there are exactly two tangents to a circle from a point outside that circle (where the points of tangency lie on the polar of the point from which the two tangents are drawn).
---
Feel free to golf the proof of `ncard_inter_orthRadius_eq_two_of_dist_lt_radius`, it could probably be rather shorter.
---
- [ ] depends on: #32296
[](https://gitpod.io/from-referrer/)
|
t-euclidean-geometry |
88/1 |
Mathlib/Geometry/Euclidean/Sphere/OrthRadius.lean |
1 |
2 |
['github-actions', 'mathlib4-dependent-issues-bot'] |
JovanGerb assignee:JovanGerb |
12-4734 12 days ago |
12-6257 12 days ago |
21-51005 21 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 |
11-46125 11 days ago |
14-81749 14 days ago |
16-82172 16 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 |
11-46121 11 days ago |
15-15962 15 days ago |
15-16550 15 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 |
11-46115 11 days ago |
17-38425 17 days ago |
17-38465 17 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 |
10-69908 10 days ago |
14-69878 14 days ago |
14-70970 14 days |
| 32188 |
euprunin author:euprunin |
feat: add `grind` annotation for `ENNReal.inv_eq_zero` |
---
Note that the lemma being annotated is
1. already actively used with `grind` via explicit `grind [lemma]` invocations in Mathlib, and
2. already tagged with `@[simp]`.
---
[](https://gitpod.io/from-referrer/)
|
t-data |
4/5 |
Mathlib/Data/ENNReal/Inv.lean |
1 |
5 |
['euprunin', 'github-actions', 'leanprover-bot', 'leanprover-radar', 'metakunt'] |
TwoFX assignee:TwoFX |
10-61022 10 days ago |
15-62478 15 days ago |
15-62508 15 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 |
10-51596 10 days ago |
11-48761 11 days ago |
59-48843 59 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 |
10-46111 10 days ago |
14-36190 14 days ago |
14-38812 14 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 |
10-46106 10 days ago |
13-80133 13 days ago |
15-82596 15 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 |
10-46101 10 days ago |
13-83448 13 days ago |
13-83479 13 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 |
10-14533 10 days ago |
10-14582 10 days ago |
10-42766 10 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 |
9-75157 9 days ago |
9-75289 9 days ago |
15-6581 15 days |
| 31425 |
robertmaxton42 author:robertmaxton42 |
feat(Topology) : implement delaborators for non-standard topology notation |
Add delaborators for unary and binary notation related to non-standard topologies in the TopologicalSpace namespace.
---
[](https://gitpod.io/from-referrer/)
|
t-topology |
104/0 |
Mathlib.lean,Mathlib/Topology/Defs/Basic.lean,Mathlib/Util/DelabNonCanonical.lean,MathlibTest/Delab/TopologicalSpace.lean |
4 |
30 |
['eric-wieser', 'github-actions', 'kckennylau', 'robertmaxton42'] |
PatrickMassot assignee:PatrickMassot |
9-46120 9 days ago |
19-24662 19 days ago |
19-55551 19 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 |
9-46119 9 days ago |
16-42752 16 days ago |
16-42784 16 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 |
8-85421 8 days ago |
8-85421 8 days ago |
22-53513 22 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 |
8-47532 8 days ago |
9-6238 9 days ago |
9-7831 9 days |
| 32194 |
alreadydone author:alreadydone |
feat(LinearAlgebra): more on StrongRankCondition |
Strong rank condition fails for R iff there is a copy of $R^{(\mathbb{N})}$ in some $R^n$, iff some $R^n$ has infinity rank, iff some $R^{n+1}$ has zero `finrank`. As consequences, if all $R^n$ are Noetherian or Artinian, then $R$ satisfies the strong rank condition.
To prove the first equivalence, I redeveloped a version of the ["tunnels and tailings"](https://github.com/leanprover-community/mathlib3/commit/86766851#diff-7829719aad6a9e3e617da2a7cf29dba4d55516b27e18f240eca352f4983d67b7R472-R491) construction @jcommelin and @kim-em contributed to mathlib ~4 years ago and made it work for Semiring/AddCommMonoid. The original construction was deprecated in [#12076](https://github.com/leanprover-community/mathlib4/commit/5948566497f56e1432c52d65623f1bb3c3937159) by @acmepjz and later removed, though some docstrings still remain, and I think it's now time to remove it.
Also add an instance that finite semirings satisfy the Orzech property (and therefore strong rank condition and invariant basis number).
---
- [x] depends on: #32123
[](https://gitpod.io/from-referrer/)
|
t-algebra label:t-algebra$ |
201/106 |
Mathlib/Data/Finsupp/Basic.lean,Mathlib/Data/Fintype/Card.lean,Mathlib/Data/Fintype/EquivFin.lean,Mathlib/LinearAlgebra/Dimension/StrongRankCondition.lean,Mathlib/LinearAlgebra/Finsupp/Pi.lean,Mathlib/LinearAlgebra/InvariantBasisNumber.lean,Mathlib/LinearAlgebra/LinearIndependent/Lemmas.lean,Mathlib/LinearAlgebra/Prod.lean,Mathlib/RingTheory/Artinian/Instances.lean,Mathlib/RingTheory/Artinian/Module.lean,Mathlib/RingTheory/Noetherian/Basic.lean,Mathlib/RingTheory/OrzechProperty.lean |
12 |
4 |
['alreadydone', 'eric-wieser', 'github-actions', 'mathlib4-dependent-issues-bot'] |
eric-wieser assignee:eric-wieser |
8-15765 8 days ago |
8-15765 8 days ago |
11-73320 11 days |
| 30333 |
paulorauber author:paulorauber |
feat(Probability): definition of trajMeasure |
A definition of `trajMeasure` and some basic lemmas.
In the context of the Ionescu-Tulcea theorem, `trajMeasure μ₀ κ` corresponds to the distribution of the trajectory obtained by starting with the distribution `μ₀` and then iterating the kernels `κ`.
Lemmas `partialTraj_compProd_kernel_eq_traj_map` and `traj_map_eq_kernel` are attributable to @EtienneC30 and some definitions borrow code from @RemyDegenne , who also improved the code considerably. Please let me know if you would like to be co-authors in this pull request.
From the LeanBandits project.
---
[](https://gitpod.io/from-referrer/)
|
t-measure-probability
new-contributor
maintainer-merge
|
80/2 |
Mathlib/Order/Interval/Finset/Basic.lean,Mathlib/Order/Interval/Finset/Nat.lean,Mathlib/Probability/Kernel/IonescuTulcea/PartialTraj.lean,Mathlib/Probability/Kernel/IonescuTulcea/Traj.lean |
4 |
28 |
['EtienneC30', 'RemyDegenne', 'github-actions', 'mathlib4-merge-conflict-bot', 'paulorauber'] |
EtienneC30 assignee:EtienneC30 |
8-11727 8 days ago |
8-11727 8 days ago |
15-77412 15 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 |
7-80050 7 days ago |
7-80084 7 days ago |
22-72686 22 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 |
7-78474 7 days ago |
17-59129 17 days ago |
17-61672 17 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 |
7-69680 7 days ago |
16-68532 16 days ago |
22-53213 22 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 |
7-62643 7 days ago |
37-79619 1 month ago |
37-79572 37 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 |
7-61803 7 days ago |
7-66414 7 days ago |
15-75769 15 days |
| 32267 |
vlad902 author:vlad902 |
feat(SimpleGraph): add `SimpleGraph.HomClass` |
Inspired by [this PR review feedback.](https://github.com/leanprover-community/mathlib4/pull/30129#discussion_r2530032044)
---
[](https://gitpod.io/from-referrer/)
|
t-combinatorics |
4/0 |
Mathlib/Combinatorics/SimpleGraph/Maps.lean |
1 |
1 |
['YaelDillies', 'github-actions'] |
b-mehta assignee:b-mehta |
7-46123 7 days ago |
13-11169 13 days ago |
13-11200 13 days |
| 32323 |
LLaurance author:LLaurance |
feat(Combinatorics/SimpleGraph/Connectivity): exists vertex adjacent to any vertex of a nontrivial connected graph |
---
[](https://gitpod.io/from-referrer/)
|
t-combinatorics |
15/0 |
Mathlib/Combinatorics/SimpleGraph/Connectivity/Connected.lean,Mathlib/Combinatorics/SimpleGraph/Connectivity/Subgraph.lean |
2 |
1 |
['github-actions'] |
kmill assignee:kmill |
7-46122 7 days ago |
11-70483 11 days ago |
11-73207 11 days |
| 32134 |
mitchell-horner author:mitchell-horner |
feat(Topology/Real): theorems linking `IsGLB` with `BddBelow`, `Antitone`, `Tendsto _ atTop` |
Implement theorems linking `IsGLB` (`IsLUB`) with `BddBelow` (`BddAbove`), `Antitone` (`Monotone`), `Tendsto _ atTop`
---
[](https://gitpod.io/from-referrer/)
|
t-topology
large-import
|
117/63 |
Mathlib/Algebra/Order/Monoid/Canonical/Basic.lean,Mathlib/Analysis/Normed/Unbundled/SeminormFromConst.lean,Mathlib/Analysis/Normed/Unbundled/SpectralNorm.lean,Mathlib/Topology/Instances/NNReal/Lemmas.lean |
4 |
18 |
['YaelDillies', 'github-actions', 'mitchell-horner'] |
YaelDillies assignee:YaelDillies |
7-9166 7 days ago |
7-12184 7 days ago |
7-53568 7 days |
| 26719 |
AntoineChambert-Loir author:AntoineChambert-Loir |
feat(RingTheory/PolynomialLaw/Basic): extends polynomial laws to arbitrary universes |
The definition of polynomial laws restricts its operations to a fixed universe.
This PR constructs the extension to any universe.
This is part of the project of studying divided powers on rings, in particular, for studying
the universal divided power algebra of a module.
Co-authored-by: María-Inés de Frutos Fernández @mariainesdff
---
- [x] depends on: #26717
- [ ] depends on: #26277
[](https://gitpod.io/from-referrer/)
|
blocked-by-other-PR
large-import
t-ring-theory
|
969/7 |
Mathlib.lean,Mathlib/Algebra/Ring/Subsemiring/Basic.lean,Mathlib/Algebra/RingQuot.lean,Mathlib/LinearAlgebra/TensorProduct/Tower.lean,Mathlib/RingTheory/Congruence/Basic.lean,Mathlib/RingTheory/Congruence/Defs.lean,Mathlib/RingTheory/Congruence/Hom.lean,Mathlib/RingTheory/PolynomialLaw/Basic.lean |
8 |
4 |
['acmepjz', 'github-actions', 'leanprover-community-bot-assistant', 'mathlib4-dependent-issues-bot'] |
nobody |
115-11638 3 months ago |
130-15288 4 months ago |
0-1757 29 minutes |
| 27599 |
mitchell-horner author:mitchell-horner |
feat(Combinatorics/SimpleGraph): define `CompleteEquipartiteSubgraph` |
Define the complete equipartite subgraphs in `r` parts each of size `t` in `G` as the `r` subsets of vertices each of size `t` such that vertices in distinct subsets are adjacent.
In this case `Nonempty (G.CompleteEquipartiteSubgraph r t)` is equivalent to `completeEquipartiteGraph r t ⊑ G`, that is, finding `r` subsets of vertices each of size `t` in `G` such that vertices in distinct subsets are adjacent is equivalent to finding an injective homomorphism from `completeEquipartiteGraph r t` to `G`.
---
- [x] depends on: #27597
- [x] depends on: #30287
[](https://gitpod.io/from-referrer/)
|
t-combinatorics |
117/7 |
Mathlib/Combinatorics/SimpleGraph/CompleteMultipartite.lean |
1 |
27 |
['YaelDillies', 'b-mehta', 'github-actions', 'mathlib4-dependent-issues-bot', 'mathlib4-merge-conflict-bot', 'mitchell-horner'] |
YaelDillies assignee:YaelDillies |
5-84085 5 days ago |
7-48201 7 days ago |
64-33231 64 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 |
5-76162 5 days ago |
5-76162 5 days ago |
47-20778 47 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 |
5-70276 5 days ago |
5-70395 5 days ago |
10-64824 10 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 |
5-54334 5 days ago |
11-57536 11 days ago |
11-60487 11 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 |
5-46117 5 days ago |
8-52448 8 days ago |
9-57045 9 days |
| 32427 |
YaelDillies author:YaelDillies |
refactor(Algebra/Algebra): genericise algebra instances for subsemirings |
From ClassFieldTheory
---
[](https://gitpod.io/from-referrer/)
|
t-algebra
CFT
label:t-algebra$ |
51/67 |
Mathlib/Algebra/Algebra/Basic.lean,Mathlib/Algebra/Algebra/Subalgebra/Basic.lean,Mathlib/Algebra/Algebra/Subalgebra/Tower.lean,Mathlib/Algebra/DirectSum/Internal.lean,Mathlib/Analysis/Normed/Unbundled/SpectralNorm.lean,Mathlib/NumberTheory/Cyclotomic/Basic.lean,Mathlib/NumberTheory/NumberField/CMField.lean,Mathlib/NumberTheory/Padics/PadicIntegers.lean,Mathlib/RingTheory/Algebraic/Integral.lean,Mathlib/RingTheory/Algebraic/MvPolynomial.lean,Mathlib/RingTheory/Extension/Presentation/Core.lean,Mathlib/RingTheory/IntegralClosure/IntegralRestrict.lean,Mathlib/RingTheory/LocalRing/LocalSubring.lean,Mathlib/RingTheory/Polynomial/Basic.lean,Mathlib/RingTheory/Valuation/AlgebraInstances.lean,Mathlib/RingTheory/Valuation/Integers.lean |
16 |
1 |
['github-actions'] |
joelriou assignee:joelriou |
5-46113 5 days ago |
9-5616 9 days ago |
9-5590 9 days |
| 32433 |
YaelDillies author:YaelDillies |
feat: an irreducible element of a submonoid isn't zero |
From ClassFieldTheory
---
[](https://gitpod.io/from-referrer/)
|
t-algebra
CFT
label:t-algebra$ |
4/0 |
Mathlib/Algebra/GroupWithZero/NonZeroDivisors.lean |
1 |
1 |
['github-actions'] |
mattrobball assignee:mattrobball |
5-46111 5 days ago |
8-74045 8 days ago |
8-74019 8 days |
| 32045 |
xroblot author:xroblot |
chore(Trace/Quotient): move isomorphism to `Localization.AtPrime.Basic` |
This PR move isomorphisms previously defined in `Trace.Quotient` into `Localization.AtPrime.Basic`. The change is purely organizational: `Localization.AtPrime.Basic` is the canonical place for lemmas and constructions about localization at a prime. The isomorphisms are also renamed to match their new namespace:
- `equivQuotMaximalIdealOfIsLocalization` -> `IsLocalization.AtPrime.equivQuotMaximalIdeal`
- `quotMapEquivQuotMapMaximalIdealOfIsLocalization` -> `IsLocalization.AtPrime.equivQuotMapMaximalIdeal`
---
[](https://gitpod.io/from-referrer/)
|
t-ring-theory |
142/108 |
Mathlib/RingTheory/Localization/AtPrime/Basic.lean,Mathlib/RingTheory/Trace/Quotient.lean |
2 |
5 |
['erdOne', 'github-actions', 'xroblot'] |
mariainesdff assignee:mariainesdff |
5-16901 5 days ago |
5-17007 5 days ago |
9-27472 9 days |
| 32273 |
jsm28 author:jsm28 |
feat(Analysis/Convex/Side): affine combinations on same / opposite side of face of a simplex as a vertex |
Build on #31205 by providing lemmas about when an affine combination of the vertices of a simplex is on the same / opposite side of a face (opposite a vertex) of the simplex as that vertex (a specific case of the lemmas from #31205 which involve two arbitrary affine combinations).
---
- [ ] depends on: #31205
[](https://gitpod.io/from-referrer/)
|
t-analysis
t-convex-geometry
|
62/0 |
Mathlib/Analysis/Convex/Side.lean |
1 |
3 |
['github-actions', 'mathlib4-dependent-issues-bot', 'mathlib4-merge-conflict-bot'] |
nobody |
5-8264 5 days ago |
5-8293 5 days ago |
5-15869 5 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 |
52-76547 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 |
4-80689 4 days ago |
16-4568 16 days ago |
30-1063 30 days |
| 27542 |
chrisflav author:chrisflav |
feat(RingTheory/KrullDimension): dimension of polynomial ring |
We show that for a Noetherian ring `R`, `dim R[X] = dim R + 1`.
Co-authored by: Sihan Su
Co-authored by: Yi Song
---
- [x] depends on: #27520
- [x] depends on: #27538
- [x] depends on: #27510
- [x] depends on: #32472
[](https://gitpod.io/from-referrer/)
|
large-import
t-ring-theory
|
123/0 |
Mathlib/Order/KrullDimension.lean,Mathlib/RingTheory/Ideal/Height.lean,Mathlib/RingTheory/KrullDimension/Polynomial.lean,Mathlib/RingTheory/Localization/AtPrime/Basic.lean |
4 |
n/a |
['github-actions', 'mathlib4-dependent-issues-bot', 'mathlib4-merge-conflict-bot'] |
nobody |
4-78938 4 days ago |
unknown |
unknown |
| 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 |
4-51711 4 days ago |
16-43738 16 days ago |
16-43768 16 days |
| 31013 |
vihdzp author:vihdzp |
chore: deprecate `AsLinearOrder` |
This goes back to Lean 3 (https://github.com/leanprover-community/mathlib3/pull/4037). It was used to prove two results about "linearly ordered lattices" [`le_sup_iff`](https://leanprover-community.github.io/mathlib4_docs/Mathlib/Order/Lattice.html#le_sup_iff) and [`inf_le_iff`](https://leanprover-community.github.io/mathlib4_docs/Mathlib/Order/Lattice.html#inf_le_iff) which have long since been turned into theorems on linear orders. The proper way to deal with a totally ordered partial order is to just write a `LinearOrder` instance, so there is no need for this.
---
See some brief [Zulip](https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/AsLinearOrder/near/547525036) discussion.
[](https://gitpod.io/from-referrer/)
|
t-order |
7/5 |
Mathlib/Order/Basic.lean |
1 |
2 |
['github-actions', 'j-loreaux', 'urkud'] |
bryangingechen assignee:bryangingechen |
4-46123 4 days ago |
8-20053 8 days ago |
8-23323 8 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 |
4-46120 4 days ago |
20-37048 20 days ago |
20-37083 20 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 |
4-46116 4 days ago |
8-33431 8 days ago |
8-33418 8 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 |
4-43905 4 days ago |
4-43905 4 days ago |
25-39971 25 days |
| 28604 |
alreadydone author:alreadydone |
chore(Algebra/Ring/Defs): add two classes (minimally invasive version) |
Add the missing `NonAssocComm(Semi)ring` classes and add some missing instances between existing classes. Contrary to #28532, the approach here doesn't add any new `extends`.
---
[](https://gitpod.io/from-referrer/)
|
t-algebra label:t-algebra$ |
57/17 |
Mathlib/Algebra/Colimit/DirectLimit.lean,Mathlib/Algebra/Ring/Defs.lean |
2 |
30 |
['alreadydone', 'github-actions', 'j-loreaux', 'kckennylau', 'leanprover-bot', 'leanprover-community-mathlib4-bot', 'leanprover-radar', 'riccardobrasca'] |
riccardobrasca assignee:riccardobrasca |
4-33153 4 days ago |
4-33153 4 days ago |
65-26340 65 days |
| 30116 |
FormulaRabbit81 author:FormulaRabbit81 |
feat(MeasureTheory): a relatively compact set of measures is tight |
---
[](https://gitpod.io/from-referrer/)
|
t-measure-probability
large-import
|
181/6 |
Mathlib/MeasureTheory/Measure/Tight.lean |
1 |
20 |
['EtienneC30', 'FormulaRabbit81', 'github-actions', 'mathlib4-merge-conflict-bot'] |
RemyDegenne assignee:RemyDegenne |
4-33113 4 days ago |
4-53993 4 days ago |
64-32720 64 days |
| 32645 |
vihdzp author:vihdzp |
feat(SetTheory/Cardinal): formulas for `sum (fun n : ℕ ↦ x ^ n)` |
---
[](https://gitpod.io/from-referrer/)
|
t-set-theory |
23/5 |
Mathlib/SetTheory/Cardinal/Arithmetic.lean,Mathlib/SetTheory/Cardinal/Basic.lean,Mathlib/SetTheory/Cardinal/Defs.lean |
3 |
1 |
['github-actions'] |
nobody |
4-5579 4 days ago |
4-7991 4 days ago |
4-8034 4 days |
| 31595 |
astrainfinita author:astrainfinita |
chore: redefine `Ideal.IsPrime` |
Redefine `Ideal.IsPrime` to make it correct for non-commutative cases
---
[](https://gitpod.io/from-referrer/)
|
t-algebra label:t-algebra$ |
225/91 |
Mathlib/Algebra/Order/Ring/Ordering/Defs.lean,Mathlib/AlgebraicGeometry/StructureSheaf.lean,Mathlib/RingTheory/DedekindDomain/Ideal/Lemmas.lean,Mathlib/RingTheory/GradedAlgebra/Radical.lean,Mathlib/RingTheory/Ideal/AssociatedPrime/Basic.lean,Mathlib/RingTheory/Ideal/IsPrimary.lean,Mathlib/RingTheory/Ideal/Maps.lean,Mathlib/RingTheory/Ideal/Maximal.lean,Mathlib/RingTheory/Ideal/Oka.lean,Mathlib/RingTheory/Ideal/Operations.lean,Mathlib/RingTheory/Ideal/Over.lean,Mathlib/RingTheory/Ideal/Pointwise.lean,Mathlib/RingTheory/Ideal/Prime.lean,Mathlib/RingTheory/Ideal/Prod.lean,Mathlib/RingTheory/Ideal/Quotient/Basic.lean,Mathlib/RingTheory/Ideal/Quotient/Operations.lean,Mathlib/RingTheory/Localization/AtPrime/Basic.lean,Mathlib/RingTheory/Localization/Ideal.lean,Mathlib/RingTheory/Polynomial/Basic.lean,Mathlib/RingTheory/PrincipalIdealDomain.lean,Mathlib/RingTheory/Spectrum/Prime/Topology.lean,Mathlib/RingTheory/Valuation/Basic.lean |
22 |
18 |
['alreadydone', 'astrainfinita', 'github-actions', 'leanprover-bot', 'leanprover-community-mathlib4-bot', 'mathlib4-merge-conflict-bot'] |
alreadydone assignee:alreadydone |
4-4035 4 days ago |
4-14082 4 days ago |
11-13542 11 days |
| 32654 |
YaelDillies author:YaelDillies |
feat(Combinatorics): a clique has size at most the chromatic number |
There already exists a version of this lemma for cliques given by a set, but it's impractical to provide an explicit clique on an explicit graph as a set, rather than an indexed family, especially because computing the size of the set would then involve proving that it is the range of an injective function, even though being a clique already implies being injective!
Application: google-deepmind/formal-conjectures#1369
From FormalConjectures
---
[](https://gitpod.io/from-referrer/)
|
t-combinatorics |
42/30 |
Mathlib/Combinatorics/SimpleGraph/Basic.lean,Mathlib/Combinatorics/SimpleGraph/Coloring.lean |
2 |
1 |
['github-actions'] |
nobody |
3-72157 3 days ago |
3-73185 3 days ago |
3-73217 3 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 |
3-65427 3 days ago |
3-65448 3 days ago |
34-16185 34 days |
| 30988 |
erdOne author:erdOne |
feat(AlgebraicGeometry): descending affine cover of an inverse limit |
---
[](https://gitpod.io/from-referrer/)
|
t-algebraic-geometry
large-import
|
350/35 |
Mathlib/Algebra/Category/Ring/Constructions.lean,Mathlib/AlgebraicGeometry/AffineTransitionLimit.lean,Mathlib/AlgebraicGeometry/Gluing.lean,Mathlib/AlgebraicGeometry/Morphisms/IsIso.lean,Mathlib/AlgebraicGeometry/Pullbacks.lean,Mathlib/AlgebraicGeometry/QuasiAffine.lean,Mathlib/AlgebraicGeometry/Sites/MorphismProperty.lean,Mathlib/Topology/LocalAtTarget.lean |
8 |
32 |
['chrisflav', 'erdOne', 'github-actions', 'mathlib4-merge-conflict-bot'] |
chrisflav assignee:chrisflav |
3-48747 3 days ago |
3-48755 3 days ago |
45-1672 45 days |
| 29948 |
mcdoll author:mcdoll |
feat(Analysis/Fourier): the Fourier transform on `L^2` |
We define the Fourier transform on L^2 as a linear isometry by extension of Schwartz functions.
The file is called `LpSpace` since we will extend the Fourier transform to L^p later on.
---
- [x] depends on: #29888
- [x] depends on: #29860
- [x] depends on: #31074
- [x] depends on: #31076
- [x] depends on: #31079
- [x] depends on: #32566
- [x] depends on: #32565
[](https://gitpod.io/from-referrer/)
|
t-analysis |
94/1 |
Mathlib.lean,Mathlib/Analysis/Distribution/SchwartzSpace.lean,Mathlib/Analysis/Fourier/LpSpace.lean,docs/undergrad.yaml |
4 |
4 |
['github-actions', 'mathlib4-dependent-issues-bot', 'mathlib4-merge-conflict-bot'] |
grunweg assignee:grunweg |
3-47300 3 days ago |
3-47410 3 days ago |
9-1119 9 days |
| 31495 |
jsm28 author:jsm28 |
feat(Geometry/Euclidean/Sphere/SecondInter): `secondInter` and sides of faces of a simplex |
Add lemmas that, if you take a simplex with one vertex on a sphere and the others on or inside it (typically, a triangle and its circumcircle), and take a line through the given vertex and a point in the interior of the simplex or the interior of the opposite face, the second intersection of that line with the sphere lies on the opposite side (from the vertex) of the face opposite that vertex.
---
- [ ] depends on: #31451
- [ ] depends on: #31452
[](https://gitpod.io/from-referrer/)
|
t-euclidean-geometry |
52/0 |
Mathlib/Geometry/Euclidean/Sphere/SecondInter.lean |
1 |
3 |
['github-actions', 'mathlib4-dependent-issues-bot', 'mathlib4-merge-conflict-bot'] |
JovanGerb assignee:JovanGerb |
3-46117 3 days ago |
7-45611 7 days ago |
7-45919 7 days |
| 32242 |
vihdzp author:vihdzp |
feat: missing instances for `OrderDual`/`Lex`/`Colex` |
---
The `Nonempty` and `Inhabited` instances for `OrderDual` exist in `Order.Basic` already.
[](https://gitpod.io/from-referrer/)
|
t-order |
12/14 |
Mathlib/Order/Synonym.lean |
1 |
2 |
['github-actions', 'mathlib4-merge-conflict-bot'] |
pechersky assignee:pechersky |
3-46113 3 days ago |
6-58090 6 days ago |
9-27629 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 |
3-46107 3 days ago |
7-54238 7 days ago |
7-54210 7 days |
| 32668 |
kim-em author:kim-em |
feat(TacticAnalysis): copy args when replacing linarith with grind |
This PR modifies `grindReplacementWith` to accept an `extractArgs` function that can extract term arguments from the original tactic syntax. When arguments are found, they are converted to `grindParam` syntax and included in the replacement `grind` call. Further, if an argument is a global identifier, we wrap it in `id` to ensure `grind` interprets it as a term (rather than trying to find a trigger pattern).
This makes the regression linter more useful - instead of just trying `grind`, it now tries `grind [X, Y]` when the original was `linarith [X, Y]`.
Example output before:
```
fail_if_success grind
linarith [Finset.mem_antidiagonal.mp hij, Real.pi_pos]
```
Example output after:
```
fail_if_success grind [Finset.mem_antidiagonal.mp hij, id Real.pi_pos]
linarith [Finset.mem_antidiagonal.mp hij, Real.pi_pos]
```
🤖 Prepared with Claude Code |
t-meta |
57/1 |
Mathlib/Tactic/TacticAnalysis/Declarations.lean |
1 |
1 |
['github-actions'] |
nobody |
3-33504 3 days ago |
3-38640 3 days ago |
3-38671 3 days |
| 32673 |
CoolRmal author:CoolRmal |
feat: an open subset of a Baire space is Baire |
This PR proves the following lemmas:
1. If `f : X → Y` is an open quotient map and `X` is a Baire space, then `Y` is Baire.
2. As a corollary of the first lemma, a homeomorphism maps a Baire space to a Baire space.
3. An open subset of a Baire space is Baire.
Formalized with help from Aristotle.
---
[](https://gitpod.io/from-referrer/)
|
t-topology
large-import
|
49/1 |
Mathlib/Topology/Baire/Lemmas.lean,Mathlib/Topology/Homeomorph/Lemmas.lean,Mathlib/Topology/Maps/OpenQuotient.lean |
3 |
2 |
['CoolRmal', 'github-actions'] |
nobody |
3-22197 3 days ago |
3-25254 3 days ago |
3-25294 3 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 |
3-20028 3 days ago |
3-20028 3 days ago |
89-56464 89 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'] |
nobody |
3-15083 3 days ago |
3-15156 3 days ago |
26-78529 26 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'] |
nobody |
3-13740 3 days ago |
3-14815 3 days ago |
3-14847 3 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'] |
nobody |
3-12452 3 days ago |
3-14909 3 days ago |
3-17397 3 days |
| 32480 |
ADedecker author:ADedecker |
feat: define `PolynormableSpace` |
A "polynormable space" is a TVS whose topology is induced by *some* family of seminorms. In the real or complex case this is just locally convex, but it makes sense (and will be used) for general nontrivially normed fields.
The name is inspired by Bourbaki's "espace polynormé", although they only allow ultrametric seminorms over an ultrametric field.
My motivation is the following:
- first, I want to be able to state [WithSeminorms.banach_steinhaus](https://leanprover-community.github.io/mathlib4_docs/Mathlib/Analysis/LocallyConvex/Barrelled.html#WithSeminorms.banach_steinhaus) without a choice of seminorm family. This is easy to do, and I have a PR on the way
- the notion of bornological TVS makes sense over an arbitrary nontrivially normed field, and we have that any sequentially continuous linear map from a bornological TVS to a polynormable space is continuous. I see no reason to restrict to the real or complex case here.
---
[](https://gitpod.io/from-referrer/)
|
t-analysis
maintainer-merge
|
51/0 |
Mathlib/Analysis/LocallyConvex/AbsConvexOpen.lean,Mathlib/Analysis/LocallyConvex/WithSeminorms.lean |
2 |
7 |
['ADedecker', 'github-actions', 'j-loreaux'] |
fpvandoorn assignee:fpvandoorn |
3-11011 3 days ago |
3-11011 3 days ago |
7-20103 7 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 |
2-79579 2 days ago |
7-60314 7 days ago |
8-28846 8 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'] |
nobody |
2-74340 2 days ago |
2-74340 2 days ago |
3-23029 3 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'] |
nobody |
2-69260 2 days ago |
2-69260 2 days ago |
31-41409 31 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 |
2-59237 2 days ago |
2-59305 2 days ago |
16-10965 16 days |
| 32702 |
SnirBroshi author:SnirBroshi |
chore(Combinatorics/SimpleGraph/Connectivity): move `Finite ConnectedComponent` instance from `WalkCounting.lean` to `Connected.lean` |
---
This moves it near similar instances, and makes it available for more files.
[](https://gitpod.io/from-referrer/)
|
t-combinatorics |
1/2 |
Mathlib/Combinatorics/SimpleGraph/Connectivity/Connected.lean,Mathlib/Combinatorics/SimpleGraph/Connectivity/WalkCounting.lean |
2 |
1 |
['github-actions'] |
nobody |
2-58346 2 days ago |
2-58396 2 days ago |
2-58430 2 days |
| 26483 |
metakunt author:metakunt |
feat(RingTheory/RootsOfUnity/PrimitiveRoots): add equivPrimitiveRootsOfCoprimePow |
Adds equivalence of r-th primitive roots by a coprime e. |
new-contributor
t-ring-theory
|
55/0 |
Mathlib/RingTheory/RootsOfUnity/PrimitiveRoots.lean |
1 |
17 |
['Citronhat', 'Ruben-VandeVelde', 'github-actions', 'metakunt'] |
erdOne assignee:erdOne |
2-46120 2 days ago |
5-72021 5 days ago |
34-67419 34 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 |
2-46116 2 days ago |
5-65722 5 days ago |
6-32972 6 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 |
2-46112 2 days ago |
6-496 6 days ago |
7-83459 7 days |
| 32479 |
WenrongZou author:WenrongZou |
feat(RingTheory/PowerSeries/Substitution): add `le_order_subst` |
I add a theorem saying multiplication of order less than the order of substitution. I tried to put at the file `PowerSeries.Order`, but it seems like in this file we already import `PowerSeries.Substitution`.
---
[](https://gitpod.io/from-referrer/)
|
new-contributor
t-ring-theory
|
71/0 |
Mathlib/RingTheory/MvPowerSeries/Substitution.lean,Mathlib/RingTheory/PowerSeries/Order.lean,Mathlib/RingTheory/PowerSeries/Substitution.lean |
3 |
19 |
['AntoineChambert-Loir', 'WenrongZou', 'erdOne', 'github-actions'] |
chrisflav assignee:chrisflav |
2-46110 2 days ago |
5-65232 5 days ago |
6-57644 6 days |
| 32482 |
sgouezel author:sgouezel |
feat: extend Stieltjes measures to more general index types |
Stieltjes measures are currently only defined on the real line. We extend the definition to more general index sets, to allow for instance the nonnegative reals or compact intervals. Some proofs become more cumbersome because we have to deal with the possibility of a bottom or a top element, but the end results are exactly the same as on the real line.
---
- [x] depends on: #32516
[](https://gitpod.io/from-referrer/)
|
t-measure-probability |
374/173 |
Mathlib/Analysis/Calculus/Monotone.lean,Mathlib/MeasureTheory/Measure/Stieltjes.lean,Mathlib/Probability/CDF.lean,Mathlib/Probability/Distributions/Exponential.lean,Mathlib/Probability/Distributions/Gamma.lean,Mathlib/Probability/Kernel/Disintegration/CDFToKernel.lean,Mathlib/Probability/Kernel/Disintegration/CondCDF.lean,Mathlib/Probability/Kernel/Disintegration/MeasurableStieltjes.lean,Mathlib/Probability/Kernel/Disintegration/StandardBorel.lean |
9 |
2 |
['github-actions', 'mathlib4-dependent-issues-bot'] |
kex-y assignee:kex-y |
2-46109 2 days ago |
6-7788 6 days ago |
6-13378 6 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 |
2-46104 2 days ago |
6-29835 6 days ago |
6-29876 6 days |
| 32555 |
ksenono author:ksenono |
feat(Combinatorics/SimpleGraph/Matching): maximum and maximal matchings for Konig's theorem |
---
[](https://gitpod.io/from-referrer/)
|
t-combinatorics
new-contributor
|
40/0 |
Mathlib/Combinatorics/SimpleGraph/Matching.lean |
1 |
8 |
['SnirBroshi', 'github-actions', 'ksenono'] |
awainverse assignee:awainverse |
2-46098 2 days ago |
5-61810 5 days ago |
5-61840 5 days |
| 32559 |
WenrongZou author:WenrongZou |
feat(RingTheory/PowerSeries): toSubring and ofSubring for MvPowerSeries |
define MvPowerSeries.toSubring and MvPowerSeries.ofSubring, and prove their order and weighted order are equal. (same for PowerSeries.)
---
[](https://gitpod.io/from-referrer/)
|
new-contributor
t-ring-theory
|
104/0 |
Mathlib/RingTheory/MvPowerSeries/Basic.lean,Mathlib/RingTheory/MvPowerSeries/Order.lean,Mathlib/RingTheory/PowerSeries/Basic.lean,Mathlib/RingTheory/PowerSeries/Order.lean |
4 |
1 |
['github-actions'] |
mariainesdff assignee:mariainesdff |
2-46097 2 days ago |
5-59009 5 days ago |
5-59046 5 days |
| 32639 |
euprunin author:euprunin |
chore: golf using `grind`. add `grind` annotations. |
---
Trace profiling results (shown if ≥10 ms before or after):
* `Finset.filter_product_card`: 39 ms before, 114 ms after
* `Finset.sym2_eq_image`: 13 ms before, 67 ms after
* `List.sublist_iff_exists_fin_orderEmbedding_get_eq`: 125 ms before, 148 ms after
* `Equiv.Perm.isThreeCycle_swap_mul_swap_same`: 51 ms before, 79 ms after
* `Polynomial.gaussNorm_monomial`: 12 ms before, 12 ms after 🎉
This golfing PR is batched under the following guidelines:
* Up to ~5 changed files per PR
* Up to ~25 changed declarations per PR
* Up to ~100 changed lines per PR
---
[](https://gitpod.io/from-referrer/)
|
|
23/57 |
Mathlib/Algebra/MvPolynomial/Basic.lean,Mathlib/Algebra/MvPolynomial/CommRing.lean,Mathlib/Algebra/Polynomial/Basic.lean,Mathlib/Combinatorics/SimpleGraph/Subgraph.lean,Mathlib/Data/Finset/Prod.lean,Mathlib/Data/Finset/Sym.lean,Mathlib/Data/Finsupp/Defs.lean,Mathlib/Data/List/NodupEquivFin.lean,Mathlib/Data/List/Sym.lean,Mathlib/Data/Sym/Sym2.lean,Mathlib/GroupTheory/Perm/Cycle/Type.lean,Mathlib/Order/Hom/Basic.lean,Mathlib/RingTheory/Polynomial/GaussNorm.lean |
13 |
9 |
['euprunin', 'github-actions', 'leanprover-radar', 'vihdzp'] |
nobody |
2-45607 2 days ago |
2-67345 2 days ago |
3-41608 3 days |
| 31092 |
FlAmmmmING author:FlAmmmmING |
feat(Algebra/Group/ForwardDiff.lean): Add theorem `sum_shift_eq_fwdDiff_iter`. |
---
[](https://gitpod.io/from-referrer/)
|
t-algebra
new-contributor
label:t-algebra$ |
15/1 |
Mathlib/Algebra/Group/ForwardDiff.lean |
1 |
15 |
['FlAmmmmING', 'Ruben-VandeVelde', 'dagurtomas', 'github-actions', 'mathlib4-merge-conflict-bot'] |
dagurtomas assignee:dagurtomas |
2-42458 2 days ago |
2-42500 2 days ago |
21-56451 21 days |
| 32710 |
erdOne author:erdOne |
feat(Topology/MetricSpace): proper iff `dist _` is proper map |
Also moved `ConditionallyCompleteLinearOrder.isCompact_Icc` and `ProperSpace ℝ` earlier to avoid large inputs.
---
[](https://gitpod.io/from-referrer/)
|
t-topology |
61/62 |
Mathlib/Topology/Algebra/ProperAction/ProperlyDiscontinuous.lean,Mathlib/Topology/Maps/Proper/CompactlyGenerated.lean,Mathlib/Topology/MetricSpace/ProperSpace.lean,Mathlib/Topology/MetricSpace/ProperSpace/Lemmas.lean,Mathlib/Topology/MetricSpace/ProperSpace/Real.lean,Mathlib/Topology/Order/Compact.lean,Mathlib/Topology/Order/IsLUB.lean |
7 |
2 |
['erdOne', 'github-actions'] |
nobody |
2-37903 2 days ago |
2-39232 2 days ago |
2-39272 2 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 |
11-84444 11 days ago |
11-84445 11 days ago |
0-31 31 seconds |
| 32672 |
tb65536 author:tb65536 |
feat: haar measures on short exact sequences |
---
[](https://gitpod.io/from-referrer/)
|
t-measure-probability |
344/0 |
Mathlib.lean,Mathlib/MeasureTheory/Measure/Haar/Extension.lean |
2 |
1 |
['github-actions'] |
nobody |
2-21386 2 days ago |
2-21386 2 days ago |
2-30168 2 days |
| 32719 |
EtienneC30 author:EtienneC30 |
feat: another version of mapping Gaussian measures |
Mathlib has [ProbabilityTheory.isGaussian_map](https://leanprover-community.github.io/mathlib4_docs/Mathlib/Probability/Distributions/Gaussian/Basic.html#ProbabilityTheory.isGaussian_map) which states that mapping a Gaussian measure by a continuous linear map yields a Gaussian measure. However this requires the domain of the linear map to be Borel, which in turns requires some second countability assumption if said domain is a product space. This Borel assumption is only needed to ensure that the continuous linear map is measurable, but for instance `Prod.fst` and `Prod.snd` are measurable regardless of Borel considerations. We thus provide a new version which much less assumptions on the space and with the extra assumption that the map is measurable. This avoids some second countability assumptions in #32144.
---
[](https://gitpod.io/from-referrer/)
|
t-measure-probability
brownian
|
8/0 |
Mathlib/Probability/Distributions/Gaussian/Basic.lean |
1 |
1 |
['github-actions'] |
nobody |
2-15548 2 days ago |
2-15624 2 days ago |
2-15598 2 days |
| 32019 |
jsm28 author:jsm28 |
feat(Geometry/Euclidean/Projection): `map` and subtype lemmas |
Add lemmas about mapping `orthogonalProjection`, `reflection` and `orthogonalProjectionSpan` under an affine isometry, and in particular mapping from a subspace to the full space.
---
- [x] depends on: #32016
[](https://gitpod.io/from-referrer/)
|
t-euclidean-geometry |
68/2 |
Mathlib/Geometry/Euclidean/Projection.lean |
1 |
3 |
['github-actions', 'mathlib4-dependent-issues-bot', 'mathlib4-merge-conflict-bot'] |
JovanGerb assignee:JovanGerb |
1-70421 1 day ago |
1-84238 1 day ago |
18-60297 18 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 |
1-69362 1 day ago |
24-10682 24 days ago |
28-53909 28 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 |
1-66013 1 day ago |
16-66832 16 days ago |
16-66871 16 days |
| 32755 |
alreadydone author:alreadydone |
chore(Topology/Compactness): golf |
---
[](https://gitpod.io/from-referrer/)
|
t-topology |
15/21 |
Mathlib/Topology/Compactness/Compact.lean |
1 |
1 |
['github-actions'] |
nobody |
1-65718 1 day ago |
1-65781 1 day ago |
1-65755 1 day |
| 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 |
1-63473 1 day ago |
1-77659 1 day ago |
22-37810 22 days |
| 32740 |
LTolDe author:LTolDe |
feat: add IsNowhereDense helpers |
add new lemmas to prove `IsNowhereDense s`
- IsNowhereDense.mono
- Topology.IsInducing.isNowhereDense_image
- IsNowhereDense.image_val
these lemmas will help to prove the **Effros Theorem**, see [zulip thread](https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/Effros.20Theorem/with/558712441)
---
[](https://gitpod.io/from-referrer/)
|
new-contributor
large-import
|
22/1 |
Mathlib/Topology/GDelta/Basic.lean |
1 |
1 |
['github-actions'] |
nobody |
1-59535 1 day ago |
1-79119 1 day ago |
1-79150 1 day |
| 32590 |
sgouezel author:sgouezel |
feat: use `IsCompletelyPseudometrizable` class in measure regularity statements |
The new statements are slightly stronger than the old ones because they don't require the uniform structure to be given.
---
[](https://gitpod.io/from-referrer/)
|
|
29/54 |
Mathlib/MeasureTheory/Measure/RegularityCompacts.lean |
1 |
2 |
['github-actions', 'mathlib4-merge-conflict-bot'] |
nobody |
1-59395 1 day ago |
1-80506 1 day ago |
4-62734 4 days |
| 32703 |
chrisflav author:chrisflav |
chore(RingTheory): rename `RingHom.specComap` to `PrimeSpectrum.comap` |
and remove the old `PrimeSpectrum.comap`, which was `RingHom.specComap` bundled as a continuous map.
Having both `RingHom.specComap` and `PrimeSpectrum.comap` leads to two ways of writing the same thing, with every lemma written before the topology-on-`PrimeSpectrum`-barrier stated in terms of `RingHom.specComap` and most lemmas after it stated in terms of `PrimeSpectrum.comap`. Since the bundled continuous map version is not useful, because the topology library rarely takes continuous maps as input, we remove the bundled version, but keep the name `PrimeSpectrum.comap` for the unbundled one.
---
[](https://gitpod.io/from-referrer/)
|
t-ring-theory |
195/182 |
Mathlib/AlgebraicGeometry/GammaSpecAdjunction.lean,Mathlib/AlgebraicGeometry/IdealSheaf/Basic.lean,Mathlib/AlgebraicGeometry/Morphisms/OpenImmersion.lean,Mathlib/AlgebraicGeometry/Morphisms/UniversallyClosed.lean,Mathlib/AlgebraicGeometry/Scheme.lean,Mathlib/AlgebraicGeometry/Spec.lean,Mathlib/AlgebraicGeometry/StructureSheaf.lean,Mathlib/RingTheory/Flat/FaithfullyFlat/Algebra.lean,Mathlib/RingTheory/Ideal/GoingDown.lean,Mathlib/RingTheory/Ideal/KrullsHeightTheorem.lean,Mathlib/RingTheory/KrullDimension/Polynomial.lean,Mathlib/RingTheory/LocalRing/ResidueField/Fiber.lean,Mathlib/RingTheory/RingHom/FaithfullyFlat.lean,Mathlib/RingTheory/Spectrum/Maximal/Localization.lean,Mathlib/RingTheory/Spectrum/Prime/Chevalley.lean,Mathlib/RingTheory/Spectrum/Prime/ChevalleyComplexity.lean,Mathlib/RingTheory/Spectrum/Prime/ConstructibleSet.lean,Mathlib/RingTheory/Spectrum/Prime/FreeLocus.lean,Mathlib/RingTheory/Spectrum/Prime/Homeomorph.lean,Mathlib/RingTheory/Spectrum/Prime/Polynomial.lean,Mathlib/RingTheory/Spectrum/Prime/RingHom.lean,Mathlib/RingTheory/Spectrum/Prime/TensorProduct.lean,Mathlib/RingTheory/Spectrum/Prime/Topology.lean,docs/1000.yaml |
24 |
7 |
['chrisflav', 'erdOne', 'github-actions', 'leanprover-radar'] |
nobody |
1-55718 1 day ago |
2-55872 2 days ago |
2-55846 2 days |
| 32589 |
grunweg author:grunweg |
feat: smooth embeddings |
Define smooth embeddings between smooth manifolds: a map is a smooth embedding iff it is both a smooth immersion and a topological embedding. We also prove basic properties (such as being stable under products); stronger results will be added in future PRs.
Note that unlike smooth immersions, we do not add definitions for
- being a smooth embedding on a set (as this doesn't exist in the topological category either),
- being an embedding at a point (being an embedding is a global notion; moreover, every immersion is locally an embedding anyway, so "being an immersion at x" is sufficient to state this)
- variants with respect to a fixed complement: the motivation for immersions (considering the equivalent local descriptions of smooth submanifolds) do not apply to this global notion.
-----
- [x] depends on: #28853
---
[](https://gitpod.io/from-referrer/)
|
t-differential-geometry |
94/3 |
Mathlib.lean,Mathlib/Geometry/Manifold/Immersion.lean,Mathlib/Geometry/Manifold/SmoothEmbedding.lean |
3 |
19 |
['chrisflav', 'github-actions', 'grunweg', 'mathlib4-dependent-issues-bot', 'peabrainiac'] |
nobody |
1-55678 1 day ago |
2-48271 2 days ago |
3-16513 3 days |
| 32704 |
euprunin author:euprunin |
chore: remove use of `erw` |
---
[](https://gitpod.io/from-referrer/)
|
|
20/26 |
Mathlib/Algebra/Category/ModuleCat/ChangeOfRings.lean,Mathlib/AlgebraicTopology/DoldKan/Homotopies.lean,Mathlib/CategoryTheory/Adjunction/PartialAdjoint.lean,Mathlib/CategoryTheory/Preadditive/AdditiveFunctor.lean,Mathlib/CategoryTheory/Triangulated/Opposite/Basic.lean,Mathlib/MeasureTheory/VectorMeasure/Decomposition/RadonNikodym.lean,Mathlib/Topology/Homotopy/Product.lean |
7 |
14 |
['bryangingechen', 'euprunin', 'github-actions', 'grunweg', 'leanprover-radar'] |
nobody |
1-52628 1 day ago |
2-54711 2 days ago |
2-54684 2 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 |
1-52161 1 day ago |
1-52303 1 day ago |
30-59551 30 days |
| 32118 |
alreadydone author:alreadydone |
feat(Algebra): prerequisites for #31919 |
+ Extract a lemma `exists_aeval_invOf_eq_zero_of_ideal_map_adjoin_add_span_eq_top` that was used in the proof of [stacks#00IB](https://stacks.math.columbia.edu/tag/00IB) and are used to prove both parts of [stacks#090P](https://stacks.math.columbia.edu/tag/090P)
+ Add lemmas on units in a submonoid of a DivisionMonoid/Group(WithZero)
+ Add instances for `integralClosure` and API for integrally closed subrings
+ Add a lemma on `trailingCoeff` of polynomials
+ Fix a statement in `local_hom_TFAE` and rename to `isLocalHom_tfae`
+ Unify the instances `Algebra.ofSubsemiring` and `Algebra.ofSubring`
+ Move `NonUnitalSub(semi)ringClass` instance on `Ideal` to from Ideal/Operations to Defs
+ Upgrade `ValuationSubring.nonunits` from `Subsemigroup` to `NonUnitalSubring`
---
[](https://gitpod.io/from-referrer/)
|
t-algebra
t-ring-theory
label:t-algebra$ |
161/39 |
Mathlib/Algebra/Algebra/Basic.lean,Mathlib/Algebra/Polynomial/Degree/TrailingDegree.lean,Mathlib/NumberTheory/Padics/PadicIntegers.lean,Mathlib/RingTheory/Ideal/Nonunits.lean,Mathlib/RingTheory/IntegralClosure/IntegrallyClosed.lean,Mathlib/RingTheory/LocalRing/LocalSubring.lean,Mathlib/RingTheory/LocalRing/RingHom/Basic.lean,Mathlib/RingTheory/Polynomial/Basic.lean,Mathlib/RingTheory/Polynomial/Ideal.lean,Mathlib/RingTheory/Valuation/AlgebraInstances.lean,Mathlib/RingTheory/Valuation/Integers.lean,Mathlib/RingTheory/Valuation/ValuationSubring.lean |
12 |
37 |
['alreadydone', 'erdOne', 'github-actions', 'jcommelin', 'leanprover-bot', 'leanprover-community-mathlib4-bot', 'leanprover-radar'] |
mattrobball assignee:mattrobball |
1-46116 1 day ago |
4-56465 4 days ago |
9-55685 9 days |
| 32382 |
YaelDillies author:YaelDillies |
chore(Algebra/Order/AddGroupWithTop): golf |
---
[](https://gitpod.io/from-referrer/)
|
t-algebra label:t-algebra$ |
107/154 |
Mathlib/Algebra/Order/AddGroupWithTop.lean,Mathlib/Algebra/Order/GroupWithZero/Canonical.lean,Mathlib/Algebra/Order/Ring/Archimedean.lean |
3 |
1 |
['github-actions'] |
dagurtomas assignee:dagurtomas |
1-46111 1 day ago |
9-85943 9 days ago |
10-19209 10 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 |
1-46109 1 day ago |
5-74691 5 days ago |
5-84981 5 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 |
1-46105 1 day ago |
5-43282 5 days ago |
5-43314 5 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 |
1-46104 1 day ago |
5-38609 5 days ago |
5-38650 5 days |
| 32603 |
themathqueen author:themathqueen |
chore: add deprecated file and clean up imports in another |
Follow-up to #28100.
---
[](https://gitpod.io/from-referrer/)
|
t-algebra label:t-algebra$ |
10/5 |
Mathlib.lean,Mathlib/Algebra/Azumaya/Basic.lean,Mathlib/LinearAlgebra/GeneralLinearGroup.lean |
3 |
1 |
['github-actions'] |
dagurtomas assignee:dagurtomas |
1-46102 1 day ago |
4-63547 4 days ago |
4-63838 4 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 |
1-46099 1 day ago |
4-49136 4 days ago |
4-49110 4 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 |
1-44252 1 day ago |
1-44311 1 day ago |
1-44293 1 day |
| 32608 |
PrParadoxy author:PrParadoxy |
feat(LinearAlgebra/PiTensorProduct): API for PiTensorProducts indexed by sets |
This PR addresses a TODO item in LinearAlgebra/PiTensorProduct.lean:
* API for the various ways `ι` can be split into subsets; connect this
with the binary tensor product
-- specifically by describing tensors of type `⨂ (i : S), s i`, for `S : Set ι`.
Our primary motivation is to formalize the notion of "tensors with
infinite index set, which are equal to a distinguished element on all
but finitely many indices". This is a standard construction e.g. in the
theory of "infinite tensor products" of unital algebras.
Beyond that, the `Set` API is natural in contexts where the index type has
an independent interpretation. An example is quantum physics, where `ι`
ranges over distinguishable degrees of freedom, and where its is common
practice to annotate objects by the set of indices they are defined on.
This PR creates a directory LinearAlgebra/PiTensorProduct and starts the
file Set.lean.
---
- [x] depends on: #32598
[](https://gitpod.io/from-referrer/)
|
new-contributor |
301/0 |
Mathlib.lean,Mathlib/LinearAlgebra/PiTensorProduct/Set.lean |
2 |
6 |
['PrParadoxy', 'github-actions', 'leanprover-radar', 'mathlib4-dependent-issues-bot', 'mathlib4-merge-conflict-bot'] |
nobody |
1-43280 1 day ago |
1-49455 1 day ago |
1-54454 1 day |
| 27254 |
yuanyi-350 author:yuanyi-350 |
feat: 2025 imo problem3 |
- [x] depends on: #28788
- [x] depends on: #28790
- [x] depends on: #28829
---
[](https://gitpod.io/from-referrer/)
|
IMO |
222/0 |
Archive.lean,Archive/Imo/Imo2025Q3.lean |
2 |
29 |
['github-actions', 'jsm28', 'kbuzzard', 'leanprover-community-bot-assistant', 'madvorak', 'mathlib4-dependent-issues-bot', 'mathlib4-merge-conflict-bot', 'themathqueen', 'wwylele', 'yuanyi-350'] |
jsm28 assignee:jsm28 |
1-40316 1 day ago |
1-40319 1 day ago |
131-50485 131 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 |
1-38620 1 day ago |
1-39789 1 day ago |
1-39821 1 day |
| 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 |
1-38411 1 day ago |
1-39485 1 day ago |
1-39527 1 day |
| 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 |
1-38285 1 day ago |
1-39186 1 day ago |
1-39220 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 |
1-37548 1 day ago |
1-37562 1 day ago |
1-37593 1 day |
| 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 |
1-31200 1 day ago |
1-31464 1 day ago |
1-31438 1 day |
| 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 |
1-29071 1 day ago |
1-29071 1 day ago |
1-29045 1 day |
| 32640 |
vihdzp author:vihdzp |
feat: cardinality of Hahn series |
This is a very preliminary development; most of the PR is really just lemmas about `HahnSeries.support`. This will be needed in the CGT repo, to define surreal Hahn series as the subfield of real, small Hahn series over their own order dual.
---
[](https://gitpod.io/from-referrer/)
|
t-algebra
t-ring-theory
label:t-algebra$ |
148/35 |
Mathlib.lean,Mathlib/RingTheory/HahnSeries/Addition.lean,Mathlib/RingTheory/HahnSeries/Basic.lean,Mathlib/RingTheory/HahnSeries/Cardinal.lean,Mathlib/RingTheory/HahnSeries/Multiplication.lean,Mathlib/RingTheory/HahnSeries/Summable.lean |
6 |
6 |
['github-actions', 'mathlib4-merge-conflict-bot', 'vihdzp', 'wwylele'] |
nobody |
1-28744 1 day ago |
1-78132 1 day ago |
3-79273 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 |
1-27766 1 day ago |
1-28028 1 day ago |
1-28063 1 day |
| 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 |
1-27197 1 day ago |
1-27205 1 day ago |
1-27238 1 day |
| 32774 |
Hagb author:Hagb |
feat(Algebra/GroupWithZero/NonZeroDivisors): add a lemma about product |
Similar with `IsRegular.prod`.
---
`IsRegular.prod`:
https://github.com/leanprover-community/mathlib4/blob/c671bc4215d64bd9cc8a84fdec9a12bd33fdcd26/Mathlib/Algebra/Regular/Pow.lean#L36-L37
[](https://gitpod.io/from-referrer/)
|
t-algebra
large-import
label:t-algebra$ |
6/0 |
Mathlib/Algebra/GroupWithZero/NonZeroDivisors.lean |
1 |
1 |
['github-actions'] |
nobody |
1-27136 1 day ago |
1-27481 1 day ago |
1-27534 1 day |
| 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 |
72-12891 2 months ago |
72-12892 2 months ago |
134-68375 134 days |
| 31560 |
AntoineChambert-Loir author:AntoineChambert-Loir |
feat(Topology/Sion): the minimax theorem of von Neumann - Sion |
Prove `Sion.exists_isSaddlePointOn` :
Let X and Y be convex subsets of topological vector spaces E and F,
X being moreover compact,
and let f : X × Y → ℝ be a function such that
- for all x, f(x, ⬝) is upper semicontinuous and quasiconcave
- for all y, f(⬝, y) is lower semicontinuous and quasiconvex
Then inf_x sup_y f(x,y) = sup_y inf_x f(x,y).
The classical case of the theorem assumes that f is continuous,
f(x, ⬝) is concave, f(⬝, y) is convex.
As a particular case, one get the von Neumann theorem where
f is bilinear and E, F are finite dimensional.
We follow the proof of Komiya (1988).
## Remark on implementation
* The essential part of the proof holds for a function
`f : X → Y → β`, where `β` is a complete dense linear order.
* We have written part of it for just a dense linear order,
* On the other hand, if the theorem holds for such `β`,
it must hold for any linear order, for the reason that
any linear order embeds into a complete dense linear order.
However, this result does not seem to be known to Mathlib.
* When `β` is `ℝ`, one can use `Real.toEReal` and one gets a proof for `ℝ`.
## TODO
Give particular important cases (eg, bilinear maps in finite dimension).
Co-authored with @ADedecker
---
- [ ] depends on: #31548
- [ ] depends on: #31547
- [ ] depends on: #31558
[](https://gitpod.io/from-referrer/)
|
blocked-by-other-PR |
847/1 |
Mathlib.lean,Mathlib/Data/EReal/Basic.lean,Mathlib/Topology/Compactness/Compact.lean,Mathlib/Topology/Semicontinuous.lean,Mathlib/Topology/Sion.lean,Mathlib/Topology/Sublevel.lean,docs/references.bib |
7 |
4 |
['github-actions', 'mathlib4-dependent-issues-bot', 'mathlib4-merge-conflict-bot'] |
nobody |
13-80313 13 days ago |
13-81732 13 days ago |
0-536 8 minutes |
| 32513 |
euprunin author:euprunin |
feat(Algebra/Polynomial): add `grind` annotations for `C_mul_monomial` and `monomial_mul_C` |
---
Note that the lemma being annotated is
1. already actively used with `grind` via explicit `grind [lemma]` invocations in Mathlib, and
2. already tagged with `@[simp]`.
---
[](https://gitpod.io/from-referrer/)
|
t-algebra label:t-algebra$ |
4/4 |
Mathlib/Algebra/Polynomial/Basic.lean,Mathlib/Algebra/Polynomial/RuleOfSigns.lean |
2 |
7 |
['euprunin', 'github-actions', 'leanprover-radar', 'mathlib4-merge-conflict-bot', 'riccardobrasca'] |
nobody |
1-20702 1 day ago |
1-81669 1 day ago |
6-73420 6 days |
| 32043 |
thomaskwaring author:thomaskwaring |
feat(Combinatorics/SimpleGraph/Acyclic): characterise maximal acyclic subgraphs |
We characterise subgraphs `H ≤ G` which are maximal among acyclic subgraphs of `G` as those for which `H.Reachable = G.Reachable`. We also prove that if `G` is acyclic and `x` and `y` are not reachable in `G`, then `G ⊔ fromEdgeSet {s(x,y)}` is acyclic.
---
|
t-combinatorics
new-contributor
|
91/0 |
Mathlib/Combinatorics/SimpleGraph/Acyclic.lean |
1 |
1 |
['github-actions'] |
b-mehta assignee:b-mehta |
1-18795 1 day ago |
19-12572 19 days ago |
19-12606 19 days |
| 32733 |
dleijnse author:dleijnse |
feat(FieldTheory): X^n - t separable iff n nonzero |
In a field `F`, for `t : F` and `n > 0`, we prove that the polynomial `X ^ n - t` is separable if and only if `n` is nonzero in `F`. This generalizes `X_pow_sub_one_separable_iff`, but the extra assumption that `n > 0` is needed (for `n = 0`, the polynomial `X ^ n - t` is separable iff `t` is not `1`).
---
[](https://gitpod.io/from-referrer/)
|
t-algebra
new-contributor
label:t-algebra$ |
13/0 |
Mathlib/FieldTheory/Separable.lean |
1 |
3 |
['dleijnse', 'github-actions', 'wwylele'] |
nobody |
1-18307 1 day ago |
1-85564 1 day ago |
1-85581 1 day |
| 32779 |
sgouezel author:sgouezel |
feat: more consequences of Riesz-Markov-Kakutani |
---
[](https://gitpod.io/from-referrer/)
|
t-measure-probability |
62/3 |
Mathlib/MeasureTheory/Integral/RieszMarkovKakutani/Real.lean |
1 |
1 |
['github-actions'] |
nobody |
1-18096 1 day ago |
1-18105 1 day ago |
1-18137 1 day |
| 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 |
1-15891 1 day ago |
1-80523 1 day ago |
1-80601 1 day |
| 32782 |
xroblot author:xroblot |
feat(Cyclotomic): compute the torsion order of a cyclotomic field |
The order of the torsion group of the `n`-th cyclotomic field is `n` if `n` is even and `2n` if `n` is odd.
---
[](https://gitpod.io/from-referrer/)
|
|
113/1 |
Mathlib/Data/Nat/Totient.lean,Mathlib/NumberTheory/Cyclotomic/Basic.lean,Mathlib/NumberTheory/NumberField/Cyclotomic/Basic.lean |
3 |
1 |
['github-actions'] |
nobody |
1-15758 1 day ago |
1-15828 1 day ago |
1-15801 1 day |
| 32784 |
sgouezel author:sgouezel |
feat: more API for FiniteMeasure and ProbabilityMeasure |
---
[](https://gitpod.io/from-referrer/)
|
t-measure-probability |
169/3 |
Mathlib/MeasureTheory/Measure/FiniteMeasure.lean,Mathlib/MeasureTheory/Measure/ProbabilityMeasure.lean,Mathlib/MeasureTheory/Measure/Typeclasses/Probability.lean |
3 |
1 |
['github-actions'] |
nobody |
1-15364 1 day ago |
1-15364 1 day ago |
1-15402 1 day |
| 32786 |
sgouezel author:sgouezel |
feat: construct a bounded continuous map from a continuous compactly supported map |
---
[](https://gitpod.io/from-referrer/)
|
t-topology |
11/2 |
Mathlib/Topology/ContinuousMap/CompactlySupported.lean |
1 |
1 |
['github-actions'] |
nobody |
1-15074 1 day ago |
1-15116 1 day ago |
1-15151 1 day |
| 32787 |
Hagb author:Hagb |
feat(RingTheory/MvPolynomial/MonomialOrder): add several lemmas about `leadingTerm` and inequality on degree |
Some of them were abstracted from a proof of Buchberger's Criterion (#29203).
---
[](https://gitpod.io/from-referrer/)
|
t-ring-theory |
34/0 |
Mathlib/RingTheory/MvPolynomial/MonomialOrder.lean |
1 |
1 |
['github-actions'] |
nobody |
1-14684 1 day ago |
1-14998 1 day ago |
1-15037 1 day |
| 32788 |
Hagb author:Hagb |
feat(RingTheory/MvPolynomial/MonomialOrder): add some variants of `sPolynomial_mul_monomial` |
This commit adds a variant `sPolynomial_mul_monomial'`, using `m.degree (monomial d c * p)` instead of `d + m.degree p`, which are different in the edge case that one of `c` and `p` is 0.
A pair of variants about `leadingTerm` instead of `monomial` are also added.
---
[](https://gitpod.io/from-referrer/)
|
t-ring-theory |
30/0 |
Mathlib/RingTheory/MvPolynomial/MonomialOrder.lean |
1 |
1 |
['github-actions'] |
nobody |
1-14109 1 day ago |
1-14113 1 day ago |
1-14148 1 day |
| 32724 |
grunweg author:grunweg |
feat: lint against unscoped uses of the linter.flexible option |
We extend the setOption linter to also lint on this option.
To facilitate this, we replace the remaining file-level exceptions by local annotations (and squeeze a few non-terminal simps where doing so seems easy enough).
---
[](https://gitpod.io/from-referrer/)
|
t-linter |
71/34 |
Mathlib/Computability/Halting.lean,Mathlib/Computability/Partrec.lean,Mathlib/Computability/PartrecCode.lean,Mathlib/Computability/Primrec.lean,Mathlib/Computability/TMToPartrec.lean,Mathlib/Data/Seq/Basic.lean,Mathlib/Data/WSeq/Basic.lean,Mathlib/SetTheory/Ordinal/Notation.lean,Mathlib/Tactic/Linter/Style.lean,MathlibTest/LintStyle.lean |
10 |
1 |
['github-actions'] |
nobody |
1-8004 1 day ago |
1-8004 1 day ago |
2-8834 2 days |
| 32789 |
harahu author:harahu |
doc(RingTheory): fix typos |
Typos found and fixed by Codex.
---
[](https://gitpod.io/from-referrer/)
|
t-ring-theory |
29/30 |
Mathlib/RingTheory/AdicCompletion/AsTensorProduct.lean,Mathlib/RingTheory/AdicCompletion/Basic.lean,Mathlib/RingTheory/AdicCompletion/RingHom.lean,Mathlib/RingTheory/Conductor.lean,Mathlib/RingTheory/Congruence/Hom.lean,Mathlib/RingTheory/DedekindDomain/Factorization.lean,Mathlib/RingTheory/DividedPowers/Basic.lean,Mathlib/RingTheory/Etale/StandardEtale.lean,Mathlib/RingTheory/Extension/Generators.lean,Mathlib/RingTheory/Extension/Presentation/Basic.lean,Mathlib/RingTheory/FiniteType.lean,Mathlib/RingTheory/Flat/Basic.lean,Mathlib/RingTheory/Ideal/Over.lean,Mathlib/RingTheory/Ideal/Quotient/Operations.lean,Mathlib/RingTheory/Localization/LocalizationLocalization.lean,Mathlib/RingTheory/MvPolynomial/MonomialOrder.lean,Mathlib/RingTheory/MvPowerSeries/Trunc.lean,Mathlib/RingTheory/NonUnitalSubring/Basic.lean,Mathlib/RingTheory/NonUnitalSubsemiring/Basic.lean,Mathlib/RingTheory/Polynomial/Cyclotomic/Basic.lean,Mathlib/RingTheory/SimpleRing/Congr.lean,Mathlib/RingTheory/Valuation/Basic.lean,Mathlib/RingTheory/Valuation/ValuativeRel/Basic.lean |
23 |
1 |
['github-actions'] |
nobody |
1-7059 1 day ago |
1-13158 1 day ago |
1-13190 1 day |
| 32793 |
harahu author:harahu |
doc(NumberTheory): fix typos |
Typos found and fixed by Codex.
---
[](https://gitpod.io/from-referrer/)
|
t-number-theory |
29/27 |
Mathlib/NumberTheory/ArithmeticFunction/Zeta.lean,Mathlib/NumberTheory/Cyclotomic/CyclotomicCharacter.lean,Mathlib/NumberTheory/Cyclotomic/PrimitiveRoots.lean,Mathlib/NumberTheory/EllipticDivisibilitySequence.lean,Mathlib/NumberTheory/EulerProduct/Basic.lean,Mathlib/NumberTheory/FLT/Three.lean,Mathlib/NumberTheory/FermatPsp.lean,Mathlib/NumberTheory/LSeries/AbstractFuncEq.lean,Mathlib/NumberTheory/LSeries/Dirichlet.lean,Mathlib/NumberTheory/LSeries/HurwitzZetaOdd.lean,Mathlib/NumberTheory/LSeries/PrimesInAP.lean,Mathlib/NumberTheory/LSeries/ZMod.lean,Mathlib/NumberTheory/LucasLehmer.lean,Mathlib/NumberTheory/MulChar/Basic.lean,Mathlib/NumberTheory/NumberField/CanonicalEmbedding/Basic.lean,Mathlib/NumberTheory/NumberField/CanonicalEmbedding/NormLeOne.lean,Mathlib/NumberTheory/NumberField/CanonicalEmbedding/PolarCoord.lean,Mathlib/NumberTheory/NumberField/Units/DirichletTheorem.lean,Mathlib/NumberTheory/Padics/PadicVal/Basic.lean,Mathlib/NumberTheory/Padics/PadicVal/Defs.lean,Mathlib/NumberTheory/Padics/WithVal.lean,Mathlib/NumberTheory/Pell.lean,Mathlib/NumberTheory/WellApproximable.lean |
23 |
1 |
['github-actions'] |
nobody |
1-5249 1 day ago |
1-5296 1 day ago |
1-7200 1 day |
| 26923 |
oliver-butterley author:oliver-butterley |
feat(Dynamics/BirkhoffSum): add the pointwise ergodic theorem (Birkhoff's) |
The Pointwise Ergodic Theorem, also known as Birkhoff's Ergodic Theorem.
Co-authored-by: Lua Viana Reis
- [x] depends on: #26074
- [x] depends on: #26807
- [x] depends on: #26810
- [x] depends on: #26840
- [x] depends on: #26842
- [x] depends on: #26848
- [x] depends on: #26851
- [x] depends on: #26852
- [x] depends on: #26853
- [x] depends on: #27008
- [x] depends on: #28901
Zulip: [PR thread](https://leanprover.zulipchat.com/#narrow/channel/144837-PR-reviews/topic/.2326923.20The.20pointwise.20ergodic.20theorem.20.28Birkhoff's.29/with/527835158)
---
[](https://gitpod.io/from-referrer/)
|
merge-conflict
t-dynamics
new-contributor
|
401/0 |
Mathlib.lean,Mathlib/Dynamics/BirkhoffSum/Pointwise.lean |
2 |
14 |
['D-Thomine', 'github-actions', 'leanprover-community-bot-assistant', 'lua-vr', 'mathlib4-dependent-issues-bot', 'mathlib4-merge-conflict-bot'] |
urkud assignee:urkud |
24-21457 24 days ago |
24-21458 24 days ago |
91-66923 91 days |
| 32262 |
alreadydone author:alreadydone |
feat(Algebra): stably finite rings |
+ Show finite semirings are stably-finite.
+ Show stable finiteness is left-right symmetric.
+ Prove matrix characterizations of rank condition and invariant basis number; as consequences, show both properties are left-right symmetric.
+ Show stable finiteness implies the rank condition, generalizing [rankCondition_of_nontrivial_of_commSemiring](https://leanprover-community.github.io/mathlib4_docs/Mathlib/LinearAlgebra/Matrix/InvariantBasisNumber.html#rankCondition_of_nontrivial_of_commSemiring).
+ Reformulate a lemma as saying division rings are stably finite.
---
- [ ] depends on: #32610
[](https://gitpod.io/from-referrer/)
|
t-algebra
t-ring-theory
label:t-algebra$ |
270/76 |
Mathlib/Data/Matrix/Basic.lean,Mathlib/Data/Matrix/Composition.lean,Mathlib/Data/Matrix/Mul.lean,Mathlib/LinearAlgebra/FiniteDimensional/Basic.lean,Mathlib/LinearAlgebra/InvariantBasisNumber.lean,Mathlib/LinearAlgebra/Matrix/BaseChange.lean,Mathlib/LinearAlgebra/Matrix/InvariantBasisNumber.lean,Mathlib/LinearAlgebra/Matrix/NonsingularInverse.lean,Mathlib/LinearAlgebra/Matrix/SchurComplement.lean,Mathlib/LinearAlgebra/Matrix/SemiringInverse.lean,Mathlib/LinearAlgebra/Matrix/ToLin.lean |
11 |
50 |
['Garmelon', 'alreadydone', 'artie2000', 'erdOne', 'github-actions', 'leanprover-bot', 'leanprover-community-mathlib4-bot', 'leanprover-radar', 'mathlib4-dependent-issues-bot'] |
erdOne assignee:erdOne |
1-2349 1 day ago |
1-2652 1 day ago |
6-84374 6 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 |
0-82885 23 hours ago |
0-82950 23 hours ago |
0-83350 23 hours |
| 32330 |
ADedecker author:ADedecker |
feat: postcomposition by a CLM as a CLM on test functions |
---
- [x] depends on: #32368
- [x] depends on: #30239
[](https://gitpod.io/from-referrer/)
|
t-analysis |
38/0 |
Mathlib/Analysis/Distribution/TestFunction.lean |
1 |
n/a |
['github-actions', 'mathlib4-dependent-issues-bot'] |
nobody |
0-82127 22 hours ago |
unknown |
unknown |
| 32360 |
YuvalFilmus author:YuvalFilmus |
feat(Chebyshev): degree, leadingCoeff, eval_neg |
Calculated the degree and leading coefficients of Chebyshev T and U, as well as formulas for T(-x) and U(-x).
---
[](https://gitpod.io/from-referrer/)
|
new-contributor
t-ring-theory
|
152/2 |
Mathlib/RingTheory/Polynomial/Chebyshev.lean |
1 |
7 |
['LLaurance', 'YuvalFilmus', 'github-actions'] |
kbuzzard assignee:kbuzzard |
0-81679 22 hours ago |
4-63420 4 days ago |
8-58403 8 days |
| 32437 |
WenrongZou author:WenrongZou |
feat(Algebra/Category/ModuleCat/Sheaf/Quasicoherent): construction of `Presentation` |
We construct presentation of sheaf of module by sequence and add `Presentation.map`.
This contribution was created as part of the Heidelberg Lean workshop "Formalising algebraic geometry" in November 2025.
Co-authored-by: William Coram @WilliamCoram
Co-authored-by: Andrew Yang @erdOne
---
[](https://gitpod.io/from-referrer/)
|
t-algebra
new-contributor
label:t-algebra$ |
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 |
0-79322 22 hours ago |
0-82434 22 hours ago |
4-48828 4 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 |
0-79308 22 hours ago |
5-7113 5 days ago |
5-7401 5 days |
| 32552 |
ksenono author:ksenono |
feat(SetTheory/Cardinal): helpers for Konig's theorem |
---
[](https://gitpod.io/from-referrer/)
|
new-contributor
t-set-theory
|
64/0 |
Mathlib/SetTheory/Cardinal/Arithmetic.lean,Mathlib/SetTheory/Cardinal/Basic.lean |
2 |
32 |
['SnirBroshi', 'b-mehta', 'github-actions', 'ksenono', 'staroperator', 'vihdzp'] |
b-mehta assignee:b-mehta |
0-79028 21 hours ago |
5-63088 5 days ago |
5-63128 5 days |
| 32801 |
Hagb author:Hagb |
feat(RingTheory/MvPolynomial/Ideal): `sPolynomial` preserves ideal membership |
It will be used by Buchberger's Criterion (in #29203).
---
[](https://gitpod.io/from-referrer/)
|
t-ring-theory |
10/0 |
Mathlib/RingTheory/MvPolynomial/Ideal.lean |
1 |
1 |
['github-actions'] |
nobody |
0-76578 21 hours ago |
0-76582 21 hours ago |
0-76619 21 hours |
| 32265 |
joelriou author:joelriou |
feat(AlgebraicTopology): finite colimits of finite simplicial sets are finite |
From https://github.com/joelriou/topcat-model-category
---
- [x] depends on: #32201
- [x] depends on: #32202
[](https://gitpod.io/from-referrer/)
|
maintainer-merge
t-algebraic-topology
|
82/0 |
Mathlib.lean,Mathlib/AlgebraicTopology/SimplicialSet/Finite.lean,Mathlib/AlgebraicTopology/SimplicialSet/FiniteColimits.lean,Mathlib/CategoryTheory/FinCategory/Basic.lean |
4 |
5 |
['github-actions', 'mathlib4-dependent-issues-bot', 'mathlib4-merge-conflict-bot', 'robin-carlier'] |
nobody |
0-75465 20 hours ago |
0-75465 20 hours ago |
0-83687 23 hours |
| 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 |
0-75357 20 hours ago |
0-75396 20 hours ago |
0-75397 20 hours |
| 32692 |
WilliamCoram author:WilliamCoram |
feat: define multivariate restricted power series |
We define multivariate restricted power series over a normed ring R, and show the properties that they form a ring when R has the ultrametric property.
This work generalises my previous work in #26089 which will need to be refactored.
---
[](https://gitpod.io/from-referrer/)
|
t-number-theory
new-contributor
t-ring-theory
|
208/0 |
Mathlib.lean,Mathlib/RingTheory/MvPowerSeries/Restricted.lean |
2 |
2 |
['WilliamCoram', 'github-actions'] |
nobody |
0-74778 20 hours ago |
2-85954 2 days ago |
2-86013 2 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 |
0-74329 20 hours ago |
0-74332 20 hours ago |
0-74367 20 hours |
| 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 |
0-73590 20 hours ago |
0-73597 20 hours ago |
0-73629 20 hours |
| 32802 |
erdOne author:erdOne |
feat(RingTheory): more ergonomic version of jacobi criterion for smoothness |
---
[](https://gitpod.io/from-referrer/)
|
t-ring-theory |
125/2 |
Mathlib/RingTheory/Extension/Basic.lean,Mathlib/RingTheory/Extension/Cotangent/Basic.lean,Mathlib/RingTheory/Smooth/Local.lean |
3 |
1 |
['github-actions'] |
nobody |
0-73509 20 hours ago |
0-75867 21 hours ago |
0-75900 21 hours |
| 32562 |
YaelDillies author:YaelDillies |
chore(Data/Finsupp): rename the `toFun` projection to `apply` in `simps` |
This is the standard name for fun-like types.
---
[](https://gitpod.io/from-referrer/)
|
maintainer-merge
t-data
|
20/37 |
Counterexamples/CliffordAlgebraNotInjective.lean,Mathlib/Algebra/Group/Finsupp.lean,Mathlib/Algebra/Polynomial/Derivative.lean,Mathlib/Data/Finsupp/Basic.lean,Mathlib/Data/Finsupp/Defs.lean,Mathlib/Data/Finsupp/Interval.lean,Mathlib/Data/Finsupp/Weight.lean,Mathlib/LinearAlgebra/Dual/Basis.lean,Mathlib/RingTheory/AlgebraTower.lean,Mathlib/RingTheory/Flat/EquationalCriterion.lean,Mathlib/RingTheory/HahnSeries/HEval.lean |
11 |
4 |
['JovanGerb', 'github-actions', 'mathlib4-merge-conflict-bot'] |
pechersky assignee:pechersky |
0-72935 20 hours ago |
0-72935 20 hours ago |
5-44468 5 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 |
0-72059 20 hours ago |
0-72059 20 hours ago |
0-72100 20 hours |
| 32737 |
j-loreaux author:j-loreaux |
refactor: rename `MulAction` to `MonoidAction` |
Given that we now have [SemigroupAction](https://leanprover-community.github.io/mathlib4_docs/Mathlib/Algebra/Group/Action/Defs.html#SemigroupAction) we are in the unfortunate scenario that the name which seems to have less structure actually has *more* structure. This PR:
1. renames `MulAction` to `MonoidAction` to reflect this additional structure, as well as declarations referencing `MulAction` in their names.
2. does *not* rename modules with `MulAction` in the name
3. does *not* rename `DistribMulAction`, `SubMulAction`, `MulActionWithZero`, etc. If these need to happen, that can occur at a later time.
4. does *not* rename `SemigroupAction` to `MulAction`. Even if this rename is desired, because of the prevalence of `MulAction` in Mathlib, I think we should not conduct a move of this magnitude all at once. If we want to rename this to `MulAction`, we should wait for the 6 month embargo period during which time that name is deprecated, to give everyone downstream the opportunity to switch instead of silently breaking their builds.
Of course, another potential name is `MulOneAction`, but I don't think that's too helpful.
---
[](https://gitpod.io/from-referrer/)
|
|
1797/1745 |
Mathlib/Algebra/AddConstMap/Basic.lean,Mathlib/Algebra/AddTorsor/Basic.lean,Mathlib/Algebra/AddTorsor/Defs.lean,Mathlib/Algebra/Algebra/Equiv.lean,Mathlib/Algebra/Algebra/NonUnitalHom.lean,Mathlib/Algebra/Algebra/Subalgebra/Basic.lean,Mathlib/Algebra/Algebra/Subalgebra/Pointwise.lean,Mathlib/Algebra/Algebra/Tower.lean,Mathlib/Algebra/Algebra/Unitization.lean,Mathlib/Algebra/BigOperators/Group/Finset/Basic.lean,Mathlib/Algebra/BigOperators/Group/Finset/Defs.lean,Mathlib/Algebra/BigOperators/Group/Finset/Pi.lean,Mathlib/Algebra/BigOperators/Group/Finset/Preimage.lean,Mathlib/Algebra/BigOperators/GroupWithZero/Action.lean,Mathlib/Algebra/Category/ModuleCat/ChangeOfRings.lean,Mathlib/Algebra/Category/ModuleCat/FilteredColimits.lean,Mathlib/Algebra/Colimit/DirectLimit.lean,Mathlib/Algebra/Field/Subfield/Basic.lean,Mathlib/Algebra/FreeMonoid/Basic.lean,Mathlib/Algebra/GradedMonoid.lean,Mathlib/Algebra/GradedMulAction.lean,Mathlib/Algebra/Group/Action/Basic.lean,Mathlib/Algebra/Group/Action/Defs.lean,Mathlib/Algebra/Group/Action/End.lean,Mathlib/Algebra/Group/Action/Equidecomp.lean,Mathlib/Algebra/Group/Action/Faithful.lean,Mathlib/Algebra/Group/Action/Hom.lean,Mathlib/Algebra/Group/Action/Opposite.lean,Mathlib/Algebra/Group/Action/Option.lean,Mathlib/Algebra/Group/Action/Pi.lean,Mathlib/Algebra/Group/Action/Pointwise/Finset.lean,Mathlib/Algebra/Group/Action/Pointwise/Set/Basic.lean,Mathlib/Algebra/Group/Action/Pointwise/Set/Finite.lean,Mathlib/Algebra/Group/Action/Pretransitive.lean,Mathlib/Algebra/Group/Action/Prod.lean,Mathlib/Algebra/Group/Action/Sigma.lean,Mathlib/Algebra/Group/Action/Sum.lean,Mathlib/Algebra/Group/Action/TransferInstance.lean,Mathlib/Algebra/Group/Action/TypeTags.lean,Mathlib/Algebra/Group/Action/Units.lean,Mathlib/Algebra/Group/Conj.lean,Mathlib/Algebra/Group/End.lean,Mathlib/Algebra/Group/Equiv/Finite.lean,Mathlib/Algebra/Group/Nat/Range.lean,Mathlib/Algebra/Group/Pointwise/Finset/Basic.lean,Mathlib/Algebra/Group/Pointwise/Finset/Density.lean,Mathlib/Algebra/Group/Pointwise/Finset/Scalar.lean,Mathlib/Algebra/Group/Pointwise/Set/Basic.lean,Mathlib/Algebra/Group/Pointwise/Set/Card.lean,Mathlib/Algebra/Group/Pointwise/Set/Finite.lean,Mathlib/Algebra/Group/Pointwise/Set/Lattice.lean,Mathlib/Algebra/Group/Pointwise/Set/Scalar.lean,Mathlib/Algebra/Group/Shrink.lean,Mathlib/Algebra/Group/Subgroup/Actions.lean,Mathlib/Algebra/Group/Subgroup/Basic.lean,Mathlib/Algebra/Group/Subgroup/Pointwise.lean,Mathlib/Algebra/Group/Submonoid/Membership.lean,Mathlib/Algebra/Group/Submonoid/MulAction.lean,Mathlib/Algebra/Group/Submonoid/Pointwise.lean,Mathlib/Algebra/Group/TransferInstance.lean,Mathlib/Algebra/Group/TypeTags/Finite.lean,Mathlib/Algebra/GroupWithZero/Action/Basic.lean,Mathlib/Algebra/GroupWithZero/Action/ConjAct.lean,Mathlib/Algebra/GroupWithZero/Action/Defs.lean,Mathlib/Algebra/GroupWithZero/Action/End.lean,Mathlib/Algebra/GroupWithZero/Action/Faithful.lean,Mathlib/Algebra/GroupWithZero/Action/Opposite.lean,Mathlib/Algebra/GroupWithZero/Action/Pointwise/Finset.lean,Mathlib/Algebra/GroupWithZero/Action/Pointwise/Set.lean,Mathlib/Algebra/GroupWithZero/Action/Prod.lean,Mathlib/Algebra/GroupWithZero/Action/Units.lean,Mathlib/Algebra/GroupWithZero/NonZeroDivisors.lean,Mathlib/Algebra/GroupWithZero/Pointwise/Finset.lean,Mathlib/Algebra/GroupWithZero/Pointwise/Set/Basic.lean,Mathlib/Algebra/GroupWithZero/Pointwise/Set/Card.lean,Mathlib/Algebra/GroupWithZero/Subgroup.lean,Mathlib/Algebra/GroupWithZero/Submonoid/Pointwise.lean,Mathlib/Algebra/GroupWithZero/TransferInstance.lean,Mathlib/Algebra/GroupWithZero/Units/Lemmas.lean,Mathlib/Algebra/Module/Congruence/Defs.lean,Mathlib/Algebra/Module/Defs.lean,Mathlib/Algebra/Module/Equiv/Basic.lean,Mathlib/Algebra/Module/GradedModule.lean,Mathlib/Algebra/Module/LinearMap/Defs.lean,Mathlib/Algebra/Module/LinearMap/End.lean,Mathlib/Algebra/Module/PUnit.lean,Mathlib/Algebra/Module/PointwisePi.lean,Mathlib/Algebra/Module/Rat.lean,Mathlib/Algebra/Module/Submodule/Basic.lean,Mathlib/Algebra/Module/Submodule/Defs.lean,Mathlib/Algebra/Module/Submodule/Invariant.lean,Mathlib/Algebra/Module/Submodule/LinearMap.lean,Mathlib/Algebra/Module/Submodule/Pointwise.lean,Mathlib/Algebra/Module/ULift.lean,Mathlib/Algebra/Order/Group/Action.lean,Mathlib/Algebra/Order/Group/Action/End.lean,Mathlib/Algebra/Order/Group/Action/Flag.lean,Mathlib/Algebra/Order/Group/Action/Synonym.lean,Mathlib/Algebra/Order/Group/End.lean,Mathlib/Algebra/Order/Module/Defs.lean |
344 |
2 |
['github-actions', 'mathlib4-merge-conflict-bot'] |
nobody |
0-70379 19 hours ago |
0-70761 19 hours ago |
1-74547 1 day |
| 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 |
0-65753 18 hours ago |
0-65893 18 hours ago |
2-81203 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 |
44/17 |
Mathlib/MeasureTheory/Measure/Regular.lean,Mathlib/Topology/GDelta/MetrizableSpace.lean,Mathlib/Topology/UniformSpace/Separation.lean |
3 |
1 |
['github-actions'] |
nobody |
0-64032 17 hours ago |
1-9248 1 day ago |
1-9229 1 day |
| 32429 |
erdOne author:erdOne |
feat(RingTheory): `IsIntegrallyClosed R[X]` |
---
[](https://gitpod.io/from-referrer/)
|
t-ring-theory |
288/3 |
Mathlib.lean,Mathlib/RingTheory/IntegralClosure/IntegrallyClosed.lean,Mathlib/RingTheory/IntegralClosure/IsIntegral/AlmostIntegral.lean,Mathlib/RingTheory/Polynomial/IsIntegral.lean |
4 |
3 |
['github-actions', 'jcommelin'] |
alreadydone and mattrobball assignee:alreadydone assignee:mattrobball |
0-64021 17 hours ago |
8-80314 8 days ago |
8-80467 8 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 |
315/3 |
Mathlib.lean,Mathlib/Algebra/MvPolynomial/Equiv.lean,Mathlib/Algebra/Polynomial/RingDivision.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 |
8 |
51 |
['AntoineChambert-Loir', 'github-actions', 'jcommelin', 'joelriou', 'mathlib4-dependent-issues-bot', 'mathlib4-merge-conflict-bot', 'ocfnash'] |
joelriou assignee:joelriou |
0-63372 17 hours ago |
0-65928 18 hours ago |
32-64139 32 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'] |
nobody |
0-62830 17 hours ago |
2-59194 2 days ago |
2-67180 2 days |
| 32747 |
j-loreaux author:j-loreaux |
feat: integer inequalities from multiples in a strict ordered ring |
These were useful during the review of #32259.
---
[](https://gitpod.io/from-referrer/)
|
t-algebra
maintainer-merge
label:t-algebra$ |
38/0 |
Mathlib.lean,Mathlib/Algebra/Order/Ring/Interval.lean |
2 |
3 |
['github-actions', 'jsm28'] |
nobody |
0-61784 17 hours ago |
0-61784 17 hours ago |
1-74973 1 day |
| 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 |
0-61492 17 hours ago |
1-24877 1 day ago |
27-18365 27 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 |
0-60065 16 hours ago |
8-83026 8 days ago |
9-77127 9 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 |
0-59475 16 hours ago |
0-59475 16 hours ago |
0-59513 16 hours |
| 30131 |
fpvandoorn author:fpvandoorn |
feat: alias_in attribute |
* A small wrapper for adding an alias of a declaration in another namespace.
* application time `.afterCompilation` is necessary for `#eval` to work correctly
* Docstrings are copied, jump-to-definition works (no test in the test file, but tested locally)
* To be used for CW-complexes, where lemmas are frequently duplicated between `RelCWComplex` and `CWComplex`.
---
[](https://gitpod.io/from-referrer/)
cc @scholzhannah
|
t-meta |
113/0 |
Mathlib.lean,Mathlib/Util/AliasIn.lean,MathlibTest/Util/AliasIn.lean |
3 |
19 |
['JovanGerb', 'fpvandoorn', 'github-actions', 'mathlib4-merge-conflict-bot'] |
JovanGerb assignee:JovanGerb |
0-59014 16 hours ago |
0-85816 23 hours ago |
48-55176 48 days |
| 32809 |
erdOne author:erdOne |
feat(RingTheory): residue field of `I[X]` |
---
[](https://gitpod.io/from-referrer/)
|
t-ring-theory |
178/1 |
Mathlib.lean,Mathlib/FieldTheory/RatFunc/AsPolynomial.lean,Mathlib/FieldTheory/RatFunc/Basic.lean,Mathlib/RingTheory/Ideal/Quotient/Operations.lean,Mathlib/RingTheory/LocalRing/ResidueField/Polynomial.lean |
5 |
1 |
['github-actions'] |
nobody |
0-58991 16 hours ago |
0-58991 16 hours ago |
0-67741 18 hours |
| 32237 |
joelriou author:joelriou |
feat(AlgebraicTopology): binary products of standard simplices |
We start the study of nondegenerate simplices in `Δ[p] ⊗ Δ[q]`. In particular, we show that it is of dimension `≤ p + q`.
From https://github.com/joelriou/topcat-model-category
---
- [x] depends on: #32201
- [x] depends on: #32202
[](https://gitpod.io/from-referrer/)
|
maintainer-merge
t-algebraic-topology
|
146/0 |
Mathlib.lean,Mathlib/AlgebraicTopology/SimplicialSet/Monoidal.lean,Mathlib/AlgebraicTopology/SimplicialSet/ProdStdSimplex.lean |
3 |
12 |
['github-actions', 'joelriou', 'mathlib4-dependent-issues-bot', 'mathlib4-merge-conflict-bot', 'robin-carlier'] |
nobody |
0-58402 16 hours ago |
0-58402 16 hours ago |
0-73079 20 hours |
| 31717 |
thorimur author:thorimur |
chore: refactor `Type*` and `Sort*` to use `mkFreshLevelParam` |
Uses the API for creating new level parameters introduced in #30797.
---
- [ ] depends on: #30797
[](https://gitpod.io/from-referrer/)
|
t-meta
large-import
|
4/7 |
Mathlib/Tactic/TypeStar.lean |
1 |
3 |
['github-actions', 'mathlib4-dependent-issues-bot', 'mathlib4-merge-conflict-bot'] |
dwrensha assignee:dwrensha |
5-46119 5 days ago |
8-72535 8 days ago |
11-27233 11 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 |
0-57571 15 hours ago |
5-12428 5 days ago |
15-7739 15 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 |
3 |
['github-actions', 'joelriou', 'metakunt'] |
nobody |
0-57388 15 hours ago |
0-58989 16 hours ago |
0-59019 16 hours |
| 32492 |
bjornsolheim author:bjornsolheim |
feat(LinearAlgebra/TensorProduct): explicit tensor product decomposition in a finite basis |
* Given a finite basis `ℬ` for `M`, any tensor `x ∈ M ⊗ N` decomposes as `∑ᵢ ℬᵢ ⊗ₜ nᵢ`
where the `N`-component `nᵢ` is obtained by applying `ℬ.coord i ⊗ id` to `x` and then
identifying `R ⊗ N ≃ N` via `lid`.
* Similarly for the right hand tensor product component version.
---
[](https://gitpod.io/from-referrer/)
|
t-algebra
new-contributor
label:t-algebra$ |
20/0 |
Mathlib/LinearAlgebra/TensorProduct/Basis.lean |
1 |
8 |
['bjornsolheim', 'erdOne', 'github-actions', 'robin-carlier', 'themathqueen'] |
erdOne assignee:erdOne |
0-56904 15 hours ago |
0-56904 15 hours ago |
7-8421 7 days |
| 32715 |
chiyunhsu author:chiyunhsu |
feat(Data/Nat/Factorization): add theorems about ordCompl |
Add theorems about ordCompl[p] n, the prime-to-p part of n, when n is a power of p. There are similar existing theorems in Data/Nat/Factorization/PrimePow.lean emphasizing isPrimePow. Motivation of PR is for a follow up PR on Combinatorial Proof of Euler's Partition Identity
---
[](https://gitpod.io/from-referrer/)
|
new-contributor
t-data
|
31/0 |
Mathlib/Data/Nat/BitIndices.lean,Mathlib/Data/Nat/Factorization/Basic.lean |
2 |
10 |
['chiyunhsu', 'github-actions', 'jcommelin'] |
nobody |
0-55951 15 hours ago |
1-14103 1 day ago |
2-29494 2 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 |
0-54156 15 hours ago |
0-54172 15 hours ago |
0-54206 15 hours |
| 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 |
0-53766 14 hours ago |
1-43902 1 day ago |
1-48085 1 day |
| 32371 |
KaiErikNiermann author:KaiErikNiermann |
fix: minor error in comment of example for natural transformation |
---
[](https://gitpod.io/from-referrer/)
|
easy
new-contributor
|
2/2 |
Mathlib/CategoryTheory/NatTrans.lean |
1 |
2 |
['LLaurance', 'github-actions'] |
nobody |
0-52334 14 hours ago |
10-23165 10 days ago |
10-58037 10 days |
| 32818 |
tb65536 author:tb65536 |
refactor(Algebra/Polynomial/Splits): continue deprecation |
This PR continues the deprecation in Splits.lean as we move over to the new API in Factors.lean.
---
[](https://gitpod.io/from-referrer/)
|
t-algebra label:t-algebra$ |
52/39 |
Mathlib/Algebra/Polynomial/Factors.lean,Mathlib/Algebra/Polynomial/Splits.lean,Mathlib/FieldTheory/Galois/Basic.lean,Mathlib/FieldTheory/IsAlgClosed/Basic.lean,Mathlib/FieldTheory/Isaacs.lean,Mathlib/FieldTheory/Normal/Basic.lean,Mathlib/RingTheory/Polynomial/GaussLemma.lean |
7 |
1 |
['github-actions'] |
nobody |
0-48507 13 hours ago |
0-48507 13 hours ago |
0-50287 13 hours |
| 30240 |
luigi-massacci author:luigi-massacci |
feat(Analysis/Distribution/ContDiffMapSupportedIn): Add a wrapper for fderiv on D_K^n |
Add a wrapper for `fderiv` as a map from `D_K^n` to `D_K^(n-1)`.
Co-Authored by: @ADedecker
---
- [ ] depends on: #30239
- [ ] depends on: #30236
- [ ] depends on: #30202
- [ ] depends on: #30201
- [ ] depends on: #30199
- [ ] depends on: #30198
- [ ] depends on: #30197
[](https://gitpod.io/from-referrer/)
|
blocked-by-other-PR
t-analysis
|
379/16 |
Mathlib/Analysis/Distribution/ContDiffMapSupportedIn.lean |
1 |
6 |
['ADedecker', 'github-actions', 'mathlib4-dependent-issues-bot', 'mathlib4-merge-conflict-bot'] |
nobody |
21-4718 21 days ago |
24-8818 24 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'] |
RemyDegenne assignee:RemyDegenne |
0-46131 12 hours ago |
3-65782 3 days ago |
3-65764 3 days |
| 32210 |
ADedecker author:ADedecker |
feat: iteratedFDeriv as a linear map on test functions |
Add `TestFunction.iteratedFDeriv[WithOrder]LM`, analogous to [ContDiffMapSupportedIn.iteratedFDerivWithOrderLM](https://leanprover-community.github.io/mathlib4_docs/Mathlib/Analysis/Distribution/ContDiffMapSupportedIn.html#ContDiffMapSupportedIn.iteratedFDerivWithOrderLM) and [ContDiffMapSupportedIn.iteratedFDerivLM](https://leanprover-community.github.io/mathlib4_docs/Mathlib/Analysis/Distribution/ContDiffMapSupportedIn.html#ContDiffMapSupportedIn.iteratedFDerivLM)
---
Co-authored-by: @luigi-massacci
[](https://gitpod.io/from-referrer/)
|
t-analysis |
109/2 |
Mathlib/Analysis/Distribution/TestFunction.lean |
1 |
2 |
['github-actions', 'mathlib4-merge-conflict-bot'] |
nobody |
12-2045 12 days ago |
12-9350 12 days ago |
14-83547 14 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 |
0-46121 12 hours ago |
0-73794 20 hours ago |
3-71233 3 days |
| 32591 |
YaelDillies author:YaelDillies |
chore(Algebra/MonoidAlgebra): scope `Algebra R[M] A[M]` instance |
It is currently local, but then the Prop-valued instances about it are not and therefore bring the (non-)instance back from the dead.
---
[](https://gitpod.io/from-referrer/)
|
t-algebra label:t-algebra$ |
11/5 |
Mathlib/Algebra/MonoidAlgebra/Basic.lean,Mathlib/RingTheory/TensorProduct/MonoidAlgebra.lean |
2 |
2 |
['JovanGerb', 'github-actions'] |
jcommelin assignee:jcommelin |
0-46120 12 hours ago |
4-6525 4 days ago |
4-75669 4 days |
| 32600 |
PrParadoxy author:PrParadoxy |
feat(LinearAlgebra/Multilinear): composition of multilinear maps |
The composition of a multilinear map with a family of multilinear maps
is a multilinear map indexed by a dependent sum.
The result reduces to a lemma about the interaction of function
application, `Sigma.curry`, and `Function.update`. This variant of
`Function.apply_update` is included as `Sigma.apply_curry_update`.
---
Note to reviewers: If `apply_curry_update` is deemed too specialized for
the `Sigma` namespace, it could be included as a private lemma. An
optimized signature would obviate the need to work around a `DecidableEq`
diamond, and would reduce `map_update_add', map_update_mul'` to a single
`simp` call each.
[](https://gitpod.io/from-referrer/)
|
new-contributor |
40/0 |
Mathlib/Data/Sigma/Basic.lean,Mathlib/LinearAlgebra/Multilinear/Basic.lean |
2 |
4 |
['github-actions', 'goliath-klein', 'kbuzzard'] |
dwrensha assignee:dwrensha |
0-46119 12 hours ago |
3-69984 3 days ago |
3-70246 3 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 |
0-46119 12 hours ago |
4-32602 4 days ago |
4-35220 4 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 |
0-46117 12 hours ago |
3-68330 3 days ago |
3-68372 3 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 |
0-46116 12 hours ago |
3-57712 3 days ago |
3-57747 3 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'] |
JovanGerb assignee:JovanGerb |
0-46116 12 hours ago |
3-52270 3 days ago |
3-52871 3 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 |
0-46115 12 hours ago |
3-51549 3 days ago |
3-51570 3 days |
| 32823 |
erdOne author:erdOne |
feat(RingTheory): construct etale neighborhood that isolates point in fiber |
---
[](https://gitpod.io/from-referrer/)
|
t-ring-theory |
280/1 |
Mathlib.lean,Mathlib/Algebra/Polynomial/Monic.lean,Mathlib/RingTheory/Etale/QuasiFinite.lean,Mathlib/RingTheory/Polynomial/UniversalFactorizationRing.lean,Mathlib/RingTheory/Spectrum/Prime/Noetherian.lean,Mathlib/RingTheory/Spectrum/Prime/RingHom.lean,Mathlib/RingTheory/Spectrum/Prime/Topology.lean |
7 |
1 |
['github-actions'] |
nobody |
0-46031 12 hours ago |
0-46031 12 hours ago |
0-46237 12 hours |
| 32811 |
erdOne author:erdOne |
feat(RingTheory): predicate on satisfying Zariski's main theorem |
---
[](https://gitpod.io/from-referrer/)
|
t-ring-theory |
169/0 |
Mathlib.lean,Mathlib/Algebra/Algebra/Subalgebra/Lattice.lean,Mathlib/RingTheory/Localization/Away/Basic.lean,Mathlib/RingTheory/ZariskisMainTheorem.lean |
4 |
2 |
['github-actions'] |
nobody |
0-45979 12 hours ago |
0-64640 17 hours ago |
0-65124 18 hours |
| 32412 |
Brian-Nugent author:Brian-Nugent |
feat: add Artinian schemes |
Added the definition of Artinian Schemes and proved basic facts about them.
---
[](https://gitpod.io/from-referrer/)
|
awaiting-author
t-algebraic-geometry
new-contributor
|
187/0 |
Mathlib.lean,Mathlib/AlgebraicGeometry/Artinian.lean,Mathlib/Topology/KrullDimension.lean |
3 |
55 |
['Brian-Nugent', 'alreadydone', 'erdOne', 'github-actions'] |
erdOne assignee:erdOne |
0-49893 13 hours ago |
0-57823 16 hours ago |
6-13 6 days |
| 32744 |
NoneMore author:NoneMore |
feat(ModelTheory/Definablity): add `DefinableFun` definition and lemmas |
This PR adds two basic shapes of definable sets and `DefinableFun` definition with relevant lemmas.
The main result is `definable_preimage_of_definableMap` asserting that the preimage of a definable set under a definable map is definable.
There are also some tool lemmas derived by the preimage lemma.
Not sure if it's necessary to create a new module `DefinableFun`.
---
[](https://gitpod.io/from-referrer/)
|
t-logic
new-contributor
|
139/0 |
Mathlib/ModelTheory/Definability.lean |
1 |
12 |
['github-actions', 'staroperator'] |
nobody |
0-39795 11 hours ago |
1-30773 1 day ago |
1-76076 1 day |
| 32826 |
felixpernegger author:felixpernegger |
feat(Data/Tuple/Sort): Sort of perm is its inverse |
One can use this to easily prove a permutation is monotone iff it is the identity. However I'm still unsure in what file to put that theorem. |
new-contributor
t-data
|
10/0 |
Mathlib/Data/Fin/Tuple/Sort.lean |
1 |
1 |
['github-actions'] |
nobody |
0-39242 10 hours ago |
0-39242 10 hours ago |
0-39247 10 hours |
| 31505 |
dsfxcimk author:dsfxcimk |
feat: Add some oangle theorems |
Add several theorems relating oriented angles and affine independence / collinearity, together with auxiliary lemmas about the equality and sign of oriented angles.
Main additions
`oangle_ne_zero_and_ne_pi_iff_not_collinear`
– An oriented angle is neither `0` nor `π` if and only if the three points are not collinear.
`affineIndependent_iff_of_oangle_eq`
– If two oriented angles are equal, then the corresponding triples of points are affinely independent simultaneously.
`not_collinear_iff_of_angle_eq`
– If two oriented angles are equal, one triple is collinear if and only if the other is.
`oangle_eq_or_eq_neg_of_angle_eq`
– The oriented angles are equal or opposite if the unoriented angles are equal.
`angle_eq_neg_of_two_zsmul_angle_eq`
– If `2 • a = 2 • b` and the signs are opposite, then `a = b + π.`
`two_zsmul_eq_iff_eq`
– Characterizes equality of doubled angles when signs are equal.
`oangle_sub_oangle_ne_pi_of_not_collinear`
– If the signs of two oriented angles are equal and the points are not collinear, their difference is not `π`. |
t-euclidean-geometry
new-contributor
|
55/0 |
Mathlib/Analysis/SpecialFunctions/Trigonometric/Angle.lean,Mathlib/Geometry/Euclidean/Angle/Oriented/Affine.lean |
2 |
31 |
['dsfxcimk', 'github-actions', 'jsm28'] |
nobody |
0-36229 10 hours ago |
2-77371 2 days ago |
2-77393 2 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 |
0-31966 8 hours ago |
0-31972 8 hours ago |
4-25350 4 days |
| 32754 |
felixpernegger author:felixpernegger |
feat(Data/Set/Card): ncard of complement of set is Nat.card - ncard of set |
|
easy
new-contributor
maintainer-merge
t-data
|
4/0 |
Mathlib/Data/Set/Card.lean |
1 |
3 |
['felixpernegger', 'github-actions', 'tb65536'] |
nobody |
0-30758 8 hours ago |
0-30758 8 hours ago |
1-66662 1 day |
| 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 |
0-22442 6 hours ago |
0-35474 9 hours ago |
0-35506 9 hours |
| 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 |
0-19867 5 hours ago |
1-1365 1 day ago |
1-1403 1 day |
| 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`
Harmonic's Aristotle gave the initial version of the proofs.
Co-authored-by: Leo Mayer leomayer@uw.edu
---
[](https://gitpod.io/from-referrer/)
|
t-analysis
new-contributor
|
52/0 |
Mathlib/Analysis/InnerProductSpace/EuclideanDist.lean |
1 |
5 |
['github-actions', 'themathqueen'] |
nobody |
0-17813 4 hours ago |
0-45290 12 hours ago |
0-45321 12 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 |
0-16959 4 hours ago |
2-52476 2 days ago |
11-17333 11 days |
| 32760 |
grunweg author:grunweg |
feat: inclusion of an open submanifold is an immersion |
---
[](https://gitpod.io/from-referrer/)
|
t-differential-geometry |
49/6 |
Mathlib/Geometry/Manifold/ChartedSpace.lean,Mathlib/Geometry/Manifold/Immersion.lean,Mathlib/Topology/OpenPartialHomeomorph/Constructions.lean |
3 |
3 |
['github-actions', 'grunweg'] |
nobody |
0-16210 4 hours ago |
0-16215 4 hours ago |
0-16189 4 hours |
| 32822 |
artie2000 author:artie2000 |
chore(Algebra/Ring/Subsemiring/Order): relate `Subsemiring.nonneg` with `AddSubmonoid.nonneg` |
* Redefine `Subsemiring.nonneg` to extend `AddSubmonoid.nonneg`
* Add a `simp` lemma for the forgetful map
---
[](https://gitpod.io/from-referrer/)
|
t-algebra label:t-algebra$ |
6/3 |
Mathlib/Algebra/Ring/Subsemiring/Order.lean |
1 |
2 |
['github-actions', 'vihdzp'] |
nobody |
0-16181 4 hours ago |
0-47782 13 hours ago |
0-47817 13 hours |
| 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'] |
nobody |
0-13583 3 hours ago |
4-32547 4 days ago |
7-63826 7 days |
| 32281 |
ajirving author:ajirving |
feat(NumberTheory.Chebyshev): prove connection between prime counting and theta |
Uses Abel summation to express the prime counting function in terms of the Chebyshev theta function. This upstreams some results from PrimeNumberTheoremAnd.
---
- [x] depends on: #32247
[](https://gitpod.io/from-referrer/)
|
t-number-theory
new-contributor
large-import
|
221/1 |
Mathlib/NumberTheory/Chebyshev.lean |
1 |
6 |
['ajirving', 'github-actions', 'mathlib4-dependent-issues-bot', 'mathlib4-merge-conflict-bot'] |
nobody |
0-13416 3 hours ago |
0-13437 3 hours ago |
3-27767 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 |
0-12534 3 hours ago |
0-12534 3 hours ago |
0-12572 3 hours |
| 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'] |
nobody |
0-9745 2 hours ago |
3-14235 3 days ago |
3-14424 3 days |
| 31908 |
YaelDillies author:YaelDillies |
feat: Bernoulli random variables |
Define the product distribution of `p`-Bernoulli random variables a measure on `Set ι`.
It is important in applications to be able to restrict the product to a subset `u` of `ι`, eg in #31364 I define the `G(V, p)` distribution of binomial random graphs by setting `ι := Sym2 V` and `u := {e |¬ e.IsDiag}`.
---
- [x] depends on: #31909
- [x] depends on: #31911
- [x] depends on: #32096
- [x] depends on: #32287
[](https://gitpod.io/from-referrer/)
|
t-measure-probability |
149/7 |
Mathlib.lean,Mathlib/Probability/Distributions/Bernoulli.lean,Mathlib/Probability/HasLaw.lean |
3 |
8 |
['DavidLedvinka', 'YaelDillies', 'github-actions', 'mathlib4-dependent-issues-bot', 'mathlib4-merge-conflict-bot', 'sgouezel'] |
sgouezel assignee:sgouezel |
0-77204 21 hours ago |
10-40553 10 days ago |
15-70386 15 days |
| 32839 |
YaelDillies author:YaelDillies |
chore(RingTheory/HahnSeries): fix delaborator |
This is copy-pasta from `MonoidAlgebra`.
---
[](https://gitpod.io/from-referrer/)
|
easy
t-ring-theory
|
1/1 |
Mathlib/RingTheory/HahnSeries/Basic.lean |
1 |
1 |
['github-actions', 'vihdzp'] |
nobody |
0-9149 2 hours ago |
0-9516 2 hours ago |
0-10041 2 hours |
| 32804 |
vihdzp author:vihdzp |
feat: more lemmas on `LinearOrderedAddCommGroupWithTop` |
---
[](https://gitpod.io/from-referrer/)
|
t-algebra label:t-algebra$ |
29/17 |
Mathlib/Algebra/Order/AddGroupWithTop.lean |
1 |
1 |
['github-actions'] |
nobody |
0-8480 2 hours ago |
0-74615 20 hours ago |
0-74653 20 hours |
| 32306 |
plp127 author:plp127 |
fix(depRewrite): make `rw!` cleanup casts correctly |
The tactic `rw!` runs a round of `dsimp` with a minimal configuration, intended to cleanup casts. This minimal configuration is not always enough to fully reduce the casts, and may have other side effects. This PR reimplements the cast cleanup in a way not involving `dsimp` that will fully reduce casts introduced by depRewrite and will not touch other parts of the expression.
---
[](https://gitpod.io/from-referrer/)
|
t-meta |
140/51 |
Mathlib/Tactic/DepRewrite.lean,MathlibTest/depRewrite.lean |
2 |
3 |
['adamtopaz', 'github-actions'] |
adamtopaz assignee:adamtopaz |
0-60156 16 hours ago |
12-1632 12 days ago |
12-1615 12 days |
| 32815 |
tb65536 author:tb65536 |
refactor: rename `Splits.splits_of_dvd` to `Splits.of_dvd` |
This PR renames `Splits.splits_of_dvd` to `Splits.of_dvd`, per this poll: https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/.60Splits.2Eof_dvd.60.20vs.20.60Splits.2Esplits_of_dvd.60/near/560925458
---
[](https://gitpod.io/from-referrer/)
|
t-algebra label:t-algebra$ |
33/33 |
Mathlib/Algebra/Polynomial/Factors.lean,Mathlib/Algebra/Polynomial/Splits.lean,Mathlib/FieldTheory/AbelRuffini.lean,Mathlib/FieldTheory/Finite/GaloisField.lean,Mathlib/FieldTheory/Galois/Basic.lean,Mathlib/FieldTheory/IsAlgClosed/Basic.lean,Mathlib/FieldTheory/Isaacs.lean,Mathlib/FieldTheory/Normal/Closure.lean,Mathlib/FieldTheory/Normal/Defs.lean,Mathlib/FieldTheory/PolynomialGaloisGroup.lean,Mathlib/FieldTheory/PrimitiveElement.lean,Mathlib/FieldTheory/Separable.lean,Mathlib/FieldTheory/SplittingField/IsSplittingField.lean,Mathlib/NumberTheory/Cyclotomic/Basic.lean,Mathlib/RingTheory/Adjoin/Field.lean,Mathlib/RingTheory/Invariant/Basic.lean,Mathlib/RingTheory/Polynomial/IsIntegral.lean |
17 |
1 |
['github-actions'] |
nobody |
0-53947 14 hours ago |
0-53947 14 hours ago |
0-53921 14 hours |
| 32712 |
erdOne author:erdOne |
feat(Logic/Equiv): `Option α × β ≃ β ⊕ α × β` |
---
[](https://gitpod.io/from-referrer/)
|
t-logic |
40/6 |
Mathlib/Logic/Equiv/Prod.lean |
1 |
1 |
['github-actions'] |
nobody |
2-38003 2 days ago |
2-38012 2 days ago |
2-38053 2 days |
| 32584 |
CBirkbeck author:CBirkbeck |
feat(NumberTheory/EisensteinSeries/E2): Define the Eisenstein series E2 |
We define the Eisenstein series E2 and prove some basic results which will be needed in #32585 to prove how it transforms under the slash action of SL2.
---
[](https://gitpod.io/from-referrer/)
|
awaiting-author
t-number-theory
maintainer-merge
large-import
|
222/4 |
Mathlib.lean,Mathlib/NumberTheory/ModularForms/EisensteinSeries/E2/Defs.lean,Mathlib/NumberTheory/ModularForms/EisensteinSeries/E2/Summable.lean,Mathlib/Topology/Algebra/InfiniteSum/ConditionalInt.lean |
4 |
24 |
['CBirkbeck', 'github-actions', 'loefflerd'] |
nobody |
0-74974 20 hours ago |
0-74974 20 hours ago |
3-6149 3 days |
| 32300 |
bjornsolheim author:bjornsolheim |
feat(Geometry/Convex/Cone): define and characterize generating convex cone |
Define the notion of a generating convex cone.
Prove some initial simple lemmas about generating cones.
---
[](https://gitpod.io/from-referrer/)
|
new-contributor
maintainer-merge
t-convex-geometry
|
90/0 |
Mathlib/Geometry/Convex/Cone/Basic.lean |
1 |
17 |
['bjornsolheim', 'github-actions', 'ocfnash'] |
nobody |
0-4440 1 hour ago |
0-4440 1 hour ago |
11-3093 11 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$ |
17/1 |
Mathlib/Algebra/Group/Submonoid/Defs.lean,Mathlib/Algebra/Module/Submodule/Lattice.lean |
2 |
3 |
['YaelDillies', 'erdOne', 'github-actions'] |
nobody |
0-4250 1 hour ago |
0-12808 3 hours ago |
0-12839 3 hours |
| 32254 |
YaelDillies author:YaelDillies |
feat(Algebra/MonoidAlgebra): complete the map API |
Add congruence isomorphisms in both the ring and monoid arguments. Move `mapRangeRingHom` from `Algebra.MonoidAlgebra.Lift` to `Algebra.MonoidAlgebra.MapDomain` and make its proofs additivisable (by not using `lift`). Make `mapDomainRingHom` take a `MonoidHom` rather than `MonoidHomClass`.
---
- [x] depends on: #32486
[](https://gitpod.io/from-referrer/)
|
t-algebra label:t-algebra$ |
193/103 |
Mathlib/Algebra/MonoidAlgebra/Lift.lean,Mathlib/Algebra/MonoidAlgebra/MapDomain.lean,Mathlib/Algebra/Polynomial/Laurent.lean,Mathlib/RingTheory/Polynomial/Opposites.lean |
4 |
25 |
['YaelDillies', 'eric-wieser', 'github-actions', 'jcommelin', 'mathlib4-dependent-issues-bot', 'mathlib4-merge-conflict-bot'] |
nobody |
0-46114 12 hours ago |
0-77958 21 hours ago |
6-85593 6 days |
| 32671 |
themathqueen author:themathqueen |
chore(LinearAlgebra/GeneralLinearGroup/AlgEquiv): slightly generalize |
---
[](https://gitpod.io/from-referrer/)
|
t-algebra label:t-algebra$ |
15/12 |
Mathlib/LinearAlgebra/GeneralLinearGroup/AlgEquiv.lean |
1 |
1 |
['github-actions'] |
nobody |
1-65727 1 day ago |
3-30057 3 days ago |
3-30130 3 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 |
470/20 |
Mathlib.lean,Mathlib/GroupTheory/GroupAction/MultiplePrimitivity.lean,Mathlib/GroupTheory/GroupAction/MultipleTransitivity.lean,Mathlib/GroupTheory/Perm/MaximalSubgroups.lean,Mathlib/GroupTheory/SpecificGroups/Alternating.lean,Mathlib/GroupTheory/SpecificGroups/Alternating/MaximalSubgroups.lean |
6 |
n/a |
['AntoineChambert-Loir', 'adomani', 'github-actions', 'leanprover-community-bot-assistant', 'mathlib4-dependent-issues-bot', 'mathlib4-merge-conflict-bot', 'tb65536'] |
tb65536 assignee:tb65536 |
0-7353 2 hours ago |
unknown |
unknown |
| 29687 |
vihdzp author:vihdzp |
feat: standard part in non-Archimedean field |
We define `ArchimedeanClass.standardPart x` as the unique real number with an infinitesimal difference from `x`. This generalizes `Hyperreal.st` for a general (non-)archimedean field.
---
- [x] depends on: #29611
- [x] depends on: #29685
- [x] depends on: #29735
- [x] depends on: #30486
- [x] depends on: #32212
[](https://gitpod.io/from-referrer/)
|
t-algebra label:t-algebra$ |
324/2 |
Mathlib.lean,Mathlib/Algebra/Order/CompleteField.lean,Mathlib/Algebra/Order/Ring/Archimedean.lean,Mathlib/Algebra/Order/Ring/StandardPart.lean,Mathlib/Order/Quotient.lean |
5 |
25 |
['YaelDillies', 'github-actions', 'mathlib4-dependent-issues-bot', 'mathlib4-merge-conflict-bot', 'plp127', 'vihdzp', 'wwylele'] |
joneugster assignee:joneugster |
0-60853 16 hours ago |
8-36269 8 days ago |
10-74697 10 days |
| 32842 |
robin-carlier author:robin-carlier |
chore: use `Category*` everywhere |
Use the new `Category*` syntax that landed in #30797.
- Import the syntax in the `CategoryTheory/Functor/Basic.lean` file: this is the first file in the hierarchy after `CategoryTheory/Category/Basic.lean`. This makes it available in basically every file which uses category theory.
- All occurences of `[Category …]` have been replaced by `[Category* …]`. Cases of `[Category.{…} …]` remain untouched.
This change did uncover a few "bad uses" of `[Category …]`
- The most notable one is the `(J: Type*) [Category J] [FinCategory J]` pattern: in that pattern, `[FinCategory J]` actually requires a `SmallCategory`, so it was silently setting the universe metavariable in `[Category J]` to make it equal to the level of `J`. This pattern have been replaced by `(J: Type*) [SmallCategory J] [FinCategory J]`.
- Some similar uses of `[Category …]` (where later declarations would silently "set" the universe levels" have been found in `CategoryTheory/Category/Cat.lean` and `CategoryTheory/Category/ReflQuiv.lean`: here, the levels have been clarified.
The only notable "breakage" is that the way Category* sets levels in order did change the universes order for `PresheafedSpace`, which was sometimes called with explicit levels, so `PresheafedSpace.{u, v, w}` becomes `PresheafedSpace.{v, u, w}` (as expected, universe levels for morphisms come first). Happy to revert if this is deemed too inconvenient (in practice, `PresheafedSpace` is often written `PresheafedSpace.{_, _, v}`, so this did not break a lot.)
Finally, minor adjustement in a few files had to be made as adding the `*` character broke through the 100char width limit.
---
All the "large" import stems from importing `Tactic/CategoryTheory/CategoryStar` in `CategoryTheory/Functor/Basic`. I think this is acceptable: at some point we need to put it in the loop if we want to use it.
To help reviewers, here is the list of files where the changes are more that running a search-replace `s/\[Category /\[Category* /`
- `Mathlib/CategoryTheory/Category/Cat.lean`: some decl were abusing the metavariable: universes got specified
- `Mathlib/CategoryTheory/Category/ReflQuiv.lean`: same
- `Mathlib/CategoryTheory/Countable.lean`: Had the `(J: Type*) [Category J] [FinCategory J]` pattern, changed to `(J: Type*) [SmallCategory J] [FinCategory J]`, and an unspecified universe in a declaration with Ulifts that got precised
- `Mathlib/Algebra/Category/FGModuleCat/Limits`: Had the `(J: Type*) [Category J] [FinCategory J]` pattern, changed to `(J: Type*) [SmallCategory J] [FinCategory J]`.
- `Mathlib/Algebra/Category/FGModuleCat/Colimits`: same
- `Mathlib/CategoryTheory/Limits/FintypeCat.lean`: same
- `Mathlib/Topology/Sheaves/Presheaf.lean`: an instance couldn’t be correctly infered. Put explicit universes.
- `Mathlib.Geometry.RingedSpace.PresheafedSpace.HasColimits`: had to adapt to the change of univ order in `PresheafedSpace`
- `Mathlib/Geometry/RingedSpace/PresheafedSpace/Gluing.lean`: same
- `Mathlib.CategoryTheory.Opposites`: long line, added line break
- `Mathlib.CategoryTheory.MorphismProperty.Basic`: long line, added line break
- `Mathlib.CategoryTheory.Action.Limits`: long line, added line break
- `Mathlib.CategoryTheory.Functor.KanExtension.Basic`: long line, added line break
- `Mathlib.CategoryTheory.Limits.Preserves.FunctorCategory`: long line, added line break
- `Mathlib.CategoryTheory.Abelian.GrothendieckAxioms.Basic`: long line, added line break
- `Mathlib.CategoryTheory.Monoidal.FunctorCategory`: long line, added line break
[](https://gitpod.io/from-referrer/)
|
t-category-theory
large-import
|
905/896 |
Mathlib/Algebra/Category/FGModuleCat/Colimits.lean,Mathlib/Algebra/Category/FGModuleCat/Limits.lean,Mathlib/Algebra/Category/Grp/AB.lean,Mathlib/Algebra/Category/ModuleCat/Adjunctions.lean,Mathlib/Algebra/Category/ModuleCat/ChangeOfRings.lean,Mathlib/Algebra/Category/ModuleCat/Presheaf/Monoidal.lean,Mathlib/Algebra/Category/ModuleCat/Topology/Basic.lean,Mathlib/Algebra/Homology/Additive.lean,Mathlib/Algebra/Homology/AlternatingConst.lean,Mathlib/Algebra/Homology/Bifunctor.lean,Mathlib/Algebra/Homology/BifunctorAssociator.lean,Mathlib/Algebra/Homology/BifunctorFlip.lean,Mathlib/Algebra/Homology/BifunctorHomotopy.lean,Mathlib/Algebra/Homology/BifunctorShift.lean,Mathlib/Algebra/Homology/CochainComplexOpposite.lean,Mathlib/Algebra/Homology/CommSq.lean,Mathlib/Algebra/Homology/DerivedCategory/Basic.lean,Mathlib/Algebra/Homology/DifferentialObject.lean,Mathlib/Algebra/Homology/Double.lean,Mathlib/Algebra/Homology/Embedding/AreComplementary.lean,Mathlib/Algebra/Homology/Embedding/CochainComplex.lean,Mathlib/Algebra/Homology/Embedding/Extend.lean,Mathlib/Algebra/Homology/Embedding/ExtendHomology.lean,Mathlib/Algebra/Homology/Embedding/ExtendHomotopy.lean,Mathlib/Algebra/Homology/Embedding/HomEquiv.lean,Mathlib/Algebra/Homology/Embedding/IsSupported.lean,Mathlib/Algebra/Homology/Embedding/Restriction.lean,Mathlib/Algebra/Homology/Embedding/RestrictionHomology.lean,Mathlib/Algebra/Homology/Embedding/StupidTrunc.lean,Mathlib/Algebra/Homology/Embedding/TruncGE.lean,Mathlib/Algebra/Homology/Embedding/TruncGEHomology.lean,Mathlib/Algebra/Homology/Embedding/TruncLE.lean,Mathlib/Algebra/Homology/Embedding/TruncLEHomology.lean,Mathlib/Algebra/Homology/ExactSequence.lean,Mathlib/Algebra/Homology/Factorizations/Basic.lean,Mathlib/Algebra/Homology/Factorizations/CM5b.lean,Mathlib/Algebra/Homology/Functor.lean,Mathlib/Algebra/Homology/HomologicalBicomplex.lean,Mathlib/Algebra/Homology/HomologicalComplexAbelian.lean,Mathlib/Algebra/Homology/HomologicalComplexBiprod.lean,Mathlib/Algebra/Homology/HomologicalComplexLimits.lean,Mathlib/Algebra/Homology/HomologySequence.lean,Mathlib/Algebra/Homology/HomologySequenceLemmas.lean,Mathlib/Algebra/Homology/Homotopy.lean,Mathlib/Algebra/Homology/HomotopyCategory.lean,Mathlib/Algebra/Homology/HomotopyCategory/HomComplex.lean,Mathlib/Algebra/Homology/HomotopyCategory/HomologicalFunctor.lean,Mathlib/Algebra/Homology/HomotopyCategory/KInjective.lean,Mathlib/Algebra/Homology/HomotopyCategory/KProjective.lean,Mathlib/Algebra/Homology/HomotopyCategory/Pretriangulated.lean,Mathlib/Algebra/Homology/HomotopyCategory/ShiftSequence.lean,Mathlib/Algebra/Homology/HomotopyCategory/ShortExact.lean,Mathlib/Algebra/Homology/HomotopyCofiber.lean,Mathlib/Algebra/Homology/LeftResolution/Basic.lean,Mathlib/Algebra/Homology/LeftResolution/Reduced.lean,Mathlib/Algebra/Homology/LeftResolution/Transport.lean,Mathlib/Algebra/Homology/Linear.lean,Mathlib/Algebra/Homology/Localization.lean,Mathlib/Algebra/Homology/Monoidal.lean,Mathlib/Algebra/Homology/Opposite.lean,Mathlib/Algebra/Homology/QuasiIso.lean,Mathlib/Algebra/Homology/Refinements.lean,Mathlib/Algebra/Homology/ShortComplex/Basic.lean,Mathlib/Algebra/Homology/ShortComplex/Exact.lean,Mathlib/Algebra/Homology/ShortComplex/ExactFunctor.lean,Mathlib/Algebra/Homology/ShortComplex/FunctorEquivalence.lean,Mathlib/Algebra/Homology/ShortComplex/HomologicalComplex.lean,Mathlib/Algebra/Homology/ShortComplex/LeftHomology.lean,Mathlib/Algebra/Homology/ShortComplex/Limits.lean,Mathlib/Algebra/Homology/ShortComplex/Linear.lean,Mathlib/Algebra/Homology/ShortComplex/Preadditive.lean,Mathlib/Algebra/Homology/ShortComplex/PreservesHomology.lean,Mathlib/Algebra/Homology/ShortComplex/QuasiIso.lean,Mathlib/Algebra/Homology/ShortComplex/Retract.lean,Mathlib/Algebra/Homology/ShortComplex/RightHomology.lean,Mathlib/Algebra/Homology/ShortComplex/ShortExact.lean,Mathlib/Algebra/Homology/ShortComplex/SnakeLemma.lean,Mathlib/Algebra/Homology/Square.lean,Mathlib/Algebra/Homology/TotalComplex.lean,Mathlib/Algebra/Homology/TotalComplexShift.lean,Mathlib/Algebra/Homology/TotalComplexSymmetry.lean,Mathlib/AlgebraicGeometry/Cover/Directed.lean,Mathlib/AlgebraicGeometry/Limits.lean,Mathlib/AlgebraicGeometry/LimitsOver.lean,Mathlib/AlgebraicGeometry/Sites/SmallAffineZariski.lean,Mathlib/AlgebraicTopology/AlternatingFaceMapComplex.lean,Mathlib/AlgebraicTopology/DoldKan/Compatibility.lean,Mathlib/AlgebraicTopology/DoldKan/Decomposition.lean,Mathlib/AlgebraicTopology/DoldKan/Degeneracies.lean,Mathlib/AlgebraicTopology/DoldKan/Equivalence.lean,Mathlib/AlgebraicTopology/DoldKan/EquivalenceAdditive.lean,Mathlib/AlgebraicTopology/DoldKan/EquivalencePseudoabelian.lean,Mathlib/AlgebraicTopology/DoldKan/Faces.lean,Mathlib/AlgebraicTopology/DoldKan/FunctorGamma.lean,Mathlib/AlgebraicTopology/DoldKan/FunctorN.lean,Mathlib/AlgebraicTopology/DoldKan/GammaCompN.lean,Mathlib/AlgebraicTopology/DoldKan/Homotopies.lean,Mathlib/AlgebraicTopology/DoldKan/HomotopyEquivalence.lean,Mathlib/AlgebraicTopology/DoldKan/NCompGamma.lean,Mathlib/AlgebraicTopology/DoldKan/NReflectsIso.lean |
447 |
3 |
['github-actions', 'leanprover-radar', 'robin-carlier'] |
nobody |
0-185 3 minutes ago |
0-2568 42 minutes ago |
0-2926 48 minutes |