Are you a maintainer with just a short amount of time? The following kinds of pull requests could be relevant for you.
| 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 |
| 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/)
|
maintainer-merge
t-computability
|
77/21 |
Mathlib/Computability/Encoding.lean,Mathlib/Data/List/Basic.lean,Mathlib/Data/Sum/Basic.lean |
3 |
12 |
['BoltonBailey', 'MichaelStollBayreuth', 'YaelDillies', 'github-actions'] |
YaelDillies assignee:YaelDillies |
19-10256 19 days ago |
19-42181 19 days ago |
62-46284 62 days |
| 32825 |
erdOne author:erdOne |
perf(RingTheory): `attribute [irreducible] KaehlerDifferential` |
---
[](https://gitpod.io/from-referrer/)
|
maintainer-merge
awaiting-author
t-ring-theory
|
5/1 |
Mathlib/Algebra/Category/ModuleCat/Differentials/Basic.lean,Mathlib/AlgebraicGeometry/Morphisms/FormallyUnramified.lean,Mathlib/RingTheory/Kaehler/Basic.lean |
3 |
7 |
['erdOne', 'github-actions', 'jcommelin', 'leanprover-radar', 'robin-carlier'] |
nobody |
18-75954 18 days ago |
18-75954 18 days ago |
1-44258 1 day |
| 33291 |
BoltonBailey author:BoltonBailey |
refactor(Computability): file for state transition systems |
This PR makes a new file to contain content having to do with state transition systems defined by a function `σ → Option σ`. This content was previously split over `PostTuringMachine.lean` and `TMComputable.lean`, but since these definitions don't only apply to Turing machines in particular, it seems sensible to refactor them and remove them from the `Turing` namespace and put them in a new `StateTransition` namespace.
---
[](https://gitpod.io/from-referrer/)
|
maintainer-merge
t-computability
|
313/234 |
Mathlib.lean,Mathlib/Computability/PostTuringMachine.lean,Mathlib/Computability/StateTransition.lean,Mathlib/Computability/TMConfig.lean,Mathlib/Computability/TMToPartrec.lean,Mathlib/Computability/TuringMachine.lean |
6 |
10 |
['BoltonBailey', 'YaelDillies', 'github-actions'] |
YaelDillies assignee:YaelDillies |
14-29687 14 days ago |
14-30253 14 days ago |
35-33822 35 days |
| 34006 |
martinwintermath author:martinwintermath |
feat(RingTheory/Finiteness/Cofinite): co-finitely generated submodules |
Add new file `Cofinite.lean` that defines *co-finitely generated* (CoFG) submodules. The main definition is
* `Submodule.CoFG`: A submodule is CoFG if the quotient of the module by this submodule is finitely generated (FG).
Prove
* lattice operations for CoFG submodules.
* complements of FG submodules are CoFG and vice versa.
* the kernel of a linear map is CoFG if and only if the range is FG.
---
[](https://gitpod.io/from-referrer/)
|
t-ring-theory
new-contributor
maintainer-merge
|
108/0 |
Mathlib.lean,Mathlib/RingTheory/Finiteness/Cofinite.lean |
2 |
26 |
['erdOne', 'github-actions', 'jcommelin', 'martinwintermath', 'plp127', 'vihdzp'] |
erdOne assignee:erdOne |
9-32151 9 days ago |
13-6148 13 days ago |
16-6006 16 days |
| 33280 |
michelsol author:michelsol |
feat(MeasureTheory/Integral/IntervalIntegral): add variant `integral_deriv_eq_sub_uIoo` of 2nd theorem of calculus. |
Add a continuous on uIcc, differentiable on uIoo, deriv version of the 2nd fundamental theorem of calculus.
This corresponds to what is written [here](https://en.wikipedia.org/wiki/Fundamental_theorem_of_calculus#Second_part).
For example it makes it easier to compute the integral :
```lean4
∫ x : ℝ in 0..1, (√(1 - x ^ 2))⁻¹ = ∫ x : ℝ in 0..1, deriv arcsin x = arcsin 1 - arcsin 0
```
It is not possible to use [`interval_deriv_eq_sub`](https://leanprover-community.github.io/mathlib4_docs/Mathlib/MeasureTheory/Integral/IntervalIntegral/FundThmCalculus.html#intervalIntegral.integral_deriv_eq_sub) which requires differentiability on all of [0,1], as `arcsin` isn't differentiable at 1.
---
[](https://gitpod.io/from-referrer/)
|
t-measure-probability
new-contributor
maintainer-merge
|
14/0 |
Mathlib/MeasureTheory/Integral/IntervalIntegral/FundThmCalculus.lean |
1 |
4 |
['EtienneC30', 'github-actions'] |
EtienneC30 assignee:EtienneC30 |
8-59656 8 days ago |
40-56800 40 days ago |
40-56362 40 days |
| 33644 |
vihdzp author:vihdzp |
feat(Analysis/Real/Hyperreal): more lemmas on `Tendsto` |
I've taken care to neither state or prove these using the various specialized predicates for `Hyperreal`, such as `Infinitesimal`, `Infinite`, `IsSt`. These will be deprecated in a followup PR in favor of reasoning with `ArchimedeanClass.mk` and `ArchimedeanClass.stdPart`.
---
- [x] depends on: #33649
[](https://gitpod.io/from-referrer/)
|
t-analysis
maintainer-merge
|
83/0 |
Mathlib/Analysis/Real/Hyperreal.lean |
1 |
4 |
['github-actions', 'j-loreaux', 'mathlib4-dependent-issues-bot', 'mathlib4-merge-conflict-bot'] |
j-loreaux assignee:j-loreaux |
7-32170 7 days ago |
11-79143 11 days ago |
11-84284 11 days |
| 31706 |
Thmoas-Guan author:Thmoas-Guan |
feat(Algebra/ModuleCat): `ModuleCat.uliftFunctor` |
Add `ModuleCat.uliftFunctor`
---
[](https://gitpod.io/from-referrer/)
|
t-algebra
maintainer-merge
label:t-algebra$ |
101/0 |
Mathlib.lean,Mathlib/Algebra/Category/ModuleCat/Ulift.lean |
2 |
20 |
['Thmoas-Guan', 'dagurtomas', 'erdOne', 'github-actions', 'mathlib4-merge-conflict-bot', 'robin-carlier'] |
mattrobball assignee:mattrobball |
6-74735 6 days ago |
6-73881 6 days ago |
21-66815 21 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/)
|
t-computability
new-contributor
maintainer-merge
|
104/7 |
Mathlib/Computability/NFA.lean |
1 |
67 |
['YaelDillies', 'ctchou', 'eric-wieser', 'github-actions', 'lambda-fairy', 'mathlib4-dependent-issues-bot', 'mathlib4-merge-conflict-bot', 'rudynicolop'] |
YaelDillies assignee:YaelDillies |
5-36668 5 days ago |
5-51270 5 days ago |
59-48116 59 days |
| 34539 |
grunweg author:grunweg |
feat(Cache): continue trying to download if the first repository had some errors |
For me, it happens occasionally when working on a mathlib PR that downloading from mathlib, just one file fails.
(This is more likely when e.g. modifying a syntax linter, so all of mathlib has to be rebuilt, and the mathlib cache has no hits.)
Right now, lake exe cache get then skips downloading files from my fork.
This is not helpful; these cache files are the ones I would have liked to download.
In such situations, I have to manually retry the command. Depending on my network, this can happen several times.
This PR changes the cache to keep downloading from the second (or third, fourth, ...) repository.
To prevent lots of wasted work, we only do so if the number of failed downloads is small (at most 10).
---
The second commit is optional: I'm happy to remove it, if you feel strongly about this.
[](https://gitpod.io/from-referrer/)
|
CI
maintainer-merge
|
38/31 |
Cache/Requests.lean |
1 |
8 |
['bryangingechen', 'github-actions', 'grunweg'] |
kim-em assignee:kim-em |
5-10148 5 days ago |
6-212 5 days ago |
6-29556 6 days |
| 33975 |
pfaffelh author:pfaffelh |
feat(Data/Set/Dissipate): Introduce dissipate s x := ⋂ y ≤ x, s y |
Introduce Dissipate s x := ⋂ y ≤ x, s y (Data/Set/Dissipate), which is parallel to Data/Set/Accumulate and provide some API for it.
This will be used for compact systems in another PR.
Co-authored-by: Rémy Degenne [remydegenne@gmail.com](mailto:remydegenne@gmail.com)
This PR continues the work from https://github.com/leanprover-community/mathlib4/pull/25899.
---
[](https://gitpod.io/from-referrer/)
|
t-data
new-contributor
maintainer-merge
|
90/4 |
Mathlib.lean,Mathlib/Data/Set/Accumulate.lean,Mathlib/Data/Set/Dissipate.lean |
3 |
27 |
['github-actions', 'joneugster', 'pfaffelh', 'vihdzp'] |
joneugster assignee:joneugster |
5-1078 5 days ago |
8-42779 8 days ago |
12-78944 12 days |
| 33147 |
SnirBroshi author:SnirBroshi |
feat(Combinatorics/SimpleGraph/Coloring): add a few missing instances (`IsEmpty`/`Nontrivial`/`Infinite`) |
---
[](https://gitpod.io/from-referrer/)
|
maintainer-merge
t-combinatorics
|
22/0 |
Mathlib/Combinatorics/SimpleGraph/Coloring.lean,Mathlib/Combinatorics/SimpleGraph/Maps.lean |
2 |
7 |
['Ruben-VandeVelde', 'SnirBroshi', 'github-actions', 'jcommelin', 'mathlib4-merge-conflict-bot'] |
b-mehta assignee:b-mehta |
4-61272 4 days ago |
4-60418 4 days ago |
45-17713 45 days |
| 30898 |
vihdzp author:vihdzp |
feat: characterization of `List.splitBy` |
---
- [x] depends on: #30892
Moved from #16837.
[](https://gitpod.io/from-referrer/)
|
t-data
maintainer-merge
|
117/10 |
Mathlib/Data/List/Flatten.lean,Mathlib/Data/List/SplitBy.lean |
2 |
12 |
['Ruben-VandeVelde', 'github-actions', 'mathlib4-dependent-issues-bot', 'mathlib4-merge-conflict-bot', 'vihdzp'] |
TwoFX assignee:TwoFX |
4-1293 4 days ago |
45-26208 45 days ago |
54-66730 54 days |
| 34668 |
SnirBroshi author:SnirBroshi |
feat(Order/Monotone/Basic): `MonotoneOn` + `InjOn` implies `StrictMonoOn` |
This matches the API for the variants without "on":
- (already exists) `StrictMonoOn → InjOn` for `[LinearOrder α] [Preorder β]`
- `MonotoneOn → InjOn → StrictMonoOn` for `[Preorder α] [PartialOrder β]`
- `MonotoneOn → (StrictMonoOn ↔ InjOn)` for `[LinearOrder α] [PartialOrder β]`
---
[](https://gitpod.io/from-referrer/)
|
t-order
maintainer-merge
|
21/1 |
Mathlib/Order/Monotone/Basic.lean |
1 |
3 |
['Ruben-VandeVelde', 'github-actions'] |
nobody |
1-2601 1 day ago |
1-21557 1 day ago |
3-10819 3 days |
| 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 |
| 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/)
|
maintainer-merge
t-computability
|
77/21 |
Mathlib/Computability/Encoding.lean,Mathlib/Data/List/Basic.lean,Mathlib/Data/Sum/Basic.lean |
3 |
12 |
['BoltonBailey', 'MichaelStollBayreuth', 'YaelDillies', 'github-actions'] |
YaelDillies assignee:YaelDillies |
19-10256 19 days ago |
19-42181 19 days ago |
62-46284 62 days |
| 32825 |
erdOne author:erdOne |
perf(RingTheory): `attribute [irreducible] KaehlerDifferential` |
---
[](https://gitpod.io/from-referrer/)
|
maintainer-merge
awaiting-author
t-ring-theory
|
5/1 |
Mathlib/Algebra/Category/ModuleCat/Differentials/Basic.lean,Mathlib/AlgebraicGeometry/Morphisms/FormallyUnramified.lean,Mathlib/RingTheory/Kaehler/Basic.lean |
3 |
7 |
['erdOne', 'github-actions', 'jcommelin', 'leanprover-radar', 'robin-carlier'] |
nobody |
18-75954 18 days ago |
18-75954 18 days ago |
1-44258 1 day |
| 33291 |
BoltonBailey author:BoltonBailey |
refactor(Computability): file for state transition systems |
This PR makes a new file to contain content having to do with state transition systems defined by a function `σ → Option σ`. This content was previously split over `PostTuringMachine.lean` and `TMComputable.lean`, but since these definitions don't only apply to Turing machines in particular, it seems sensible to refactor them and remove them from the `Turing` namespace and put them in a new `StateTransition` namespace.
---
[](https://gitpod.io/from-referrer/)
|
maintainer-merge
t-computability
|
313/234 |
Mathlib.lean,Mathlib/Computability/PostTuringMachine.lean,Mathlib/Computability/StateTransition.lean,Mathlib/Computability/TMConfig.lean,Mathlib/Computability/TMToPartrec.lean,Mathlib/Computability/TuringMachine.lean |
6 |
10 |
['BoltonBailey', 'YaelDillies', 'github-actions'] |
YaelDillies assignee:YaelDillies |
14-29687 14 days ago |
14-30253 14 days ago |
35-33822 35 days |
| 34006 |
martinwintermath author:martinwintermath |
feat(RingTheory/Finiteness/Cofinite): co-finitely generated submodules |
Add new file `Cofinite.lean` that defines *co-finitely generated* (CoFG) submodules. The main definition is
* `Submodule.CoFG`: A submodule is CoFG if the quotient of the module by this submodule is finitely generated (FG).
Prove
* lattice operations for CoFG submodules.
* complements of FG submodules are CoFG and vice versa.
* the kernel of a linear map is CoFG if and only if the range is FG.
---
[](https://gitpod.io/from-referrer/)
|
t-ring-theory
new-contributor
maintainer-merge
|
108/0 |
Mathlib.lean,Mathlib/RingTheory/Finiteness/Cofinite.lean |
2 |
26 |
['erdOne', 'github-actions', 'jcommelin', 'martinwintermath', 'plp127', 'vihdzp'] |
erdOne assignee:erdOne |
9-32151 9 days ago |
13-6148 13 days ago |
16-6006 16 days |
| 33280 |
michelsol author:michelsol |
feat(MeasureTheory/Integral/IntervalIntegral): add variant `integral_deriv_eq_sub_uIoo` of 2nd theorem of calculus. |
Add a continuous on uIcc, differentiable on uIoo, deriv version of the 2nd fundamental theorem of calculus.
This corresponds to what is written [here](https://en.wikipedia.org/wiki/Fundamental_theorem_of_calculus#Second_part).
For example it makes it easier to compute the integral :
```lean4
∫ x : ℝ in 0..1, (√(1 - x ^ 2))⁻¹ = ∫ x : ℝ in 0..1, deriv arcsin x = arcsin 1 - arcsin 0
```
It is not possible to use [`interval_deriv_eq_sub`](https://leanprover-community.github.io/mathlib4_docs/Mathlib/MeasureTheory/Integral/IntervalIntegral/FundThmCalculus.html#intervalIntegral.integral_deriv_eq_sub) which requires differentiability on all of [0,1], as `arcsin` isn't differentiable at 1.
---
[](https://gitpod.io/from-referrer/)
|
t-measure-probability
new-contributor
maintainer-merge
|
14/0 |
Mathlib/MeasureTheory/Integral/IntervalIntegral/FundThmCalculus.lean |
1 |
4 |
['EtienneC30', 'github-actions'] |
EtienneC30 assignee:EtienneC30 |
8-59656 8 days ago |
40-56800 40 days ago |
40-56362 40 days |
| 33644 |
vihdzp author:vihdzp |
feat(Analysis/Real/Hyperreal): more lemmas on `Tendsto` |
I've taken care to neither state or prove these using the various specialized predicates for `Hyperreal`, such as `Infinitesimal`, `Infinite`, `IsSt`. These will be deprecated in a followup PR in favor of reasoning with `ArchimedeanClass.mk` and `ArchimedeanClass.stdPart`.
---
- [x] depends on: #33649
[](https://gitpod.io/from-referrer/)
|
t-analysis
maintainer-merge
|
83/0 |
Mathlib/Analysis/Real/Hyperreal.lean |
1 |
4 |
['github-actions', 'j-loreaux', 'mathlib4-dependent-issues-bot', 'mathlib4-merge-conflict-bot'] |
j-loreaux assignee:j-loreaux |
7-32170 7 days ago |
11-79143 11 days ago |
11-84284 11 days |
| 31706 |
Thmoas-Guan author:Thmoas-Guan |
feat(Algebra/ModuleCat): `ModuleCat.uliftFunctor` |
Add `ModuleCat.uliftFunctor`
---
[](https://gitpod.io/from-referrer/)
|
t-algebra
maintainer-merge
label:t-algebra$ |
101/0 |
Mathlib.lean,Mathlib/Algebra/Category/ModuleCat/Ulift.lean |
2 |
20 |
['Thmoas-Guan', 'dagurtomas', 'erdOne', 'github-actions', 'mathlib4-merge-conflict-bot', 'robin-carlier'] |
mattrobball assignee:mattrobball |
6-74735 6 days ago |
6-73881 6 days ago |
21-66815 21 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/)
|
t-computability
new-contributor
maintainer-merge
|
104/7 |
Mathlib/Computability/NFA.lean |
1 |
67 |
['YaelDillies', 'ctchou', 'eric-wieser', 'github-actions', 'lambda-fairy', 'mathlib4-dependent-issues-bot', 'mathlib4-merge-conflict-bot', 'rudynicolop'] |
YaelDillies assignee:YaelDillies |
5-36668 5 days ago |
5-51270 5 days ago |
59-48116 59 days |
| 34539 |
grunweg author:grunweg |
feat(Cache): continue trying to download if the first repository had some errors |
For me, it happens occasionally when working on a mathlib PR that downloading from mathlib, just one file fails.
(This is more likely when e.g. modifying a syntax linter, so all of mathlib has to be rebuilt, and the mathlib cache has no hits.)
Right now, lake exe cache get then skips downloading files from my fork.
This is not helpful; these cache files are the ones I would have liked to download.
In such situations, I have to manually retry the command. Depending on my network, this can happen several times.
This PR changes the cache to keep downloading from the second (or third, fourth, ...) repository.
To prevent lots of wasted work, we only do so if the number of failed downloads is small (at most 10).
---
The second commit is optional: I'm happy to remove it, if you feel strongly about this.
[](https://gitpod.io/from-referrer/)
|
CI
maintainer-merge
|
38/31 |
Cache/Requests.lean |
1 |
8 |
['bryangingechen', 'github-actions', 'grunweg'] |
kim-em assignee:kim-em |
5-10148 5 days ago |
6-212 5 days ago |
6-29556 6 days |
| 33975 |
pfaffelh author:pfaffelh |
feat(Data/Set/Dissipate): Introduce dissipate s x := ⋂ y ≤ x, s y |
Introduce Dissipate s x := ⋂ y ≤ x, s y (Data/Set/Dissipate), which is parallel to Data/Set/Accumulate and provide some API for it.
This will be used for compact systems in another PR.
Co-authored-by: Rémy Degenne [remydegenne@gmail.com](mailto:remydegenne@gmail.com)
This PR continues the work from https://github.com/leanprover-community/mathlib4/pull/25899.
---
[](https://gitpod.io/from-referrer/)
|
t-data
new-contributor
maintainer-merge
|
90/4 |
Mathlib.lean,Mathlib/Data/Set/Accumulate.lean,Mathlib/Data/Set/Dissipate.lean |
3 |
27 |
['github-actions', 'joneugster', 'pfaffelh', 'vihdzp'] |
joneugster assignee:joneugster |
5-1078 5 days ago |
8-42779 8 days ago |
12-78944 12 days |
| 33147 |
SnirBroshi author:SnirBroshi |
feat(Combinatorics/SimpleGraph/Coloring): add a few missing instances (`IsEmpty`/`Nontrivial`/`Infinite`) |
---
[](https://gitpod.io/from-referrer/)
|
maintainer-merge
t-combinatorics
|
22/0 |
Mathlib/Combinatorics/SimpleGraph/Coloring.lean,Mathlib/Combinatorics/SimpleGraph/Maps.lean |
2 |
7 |
['Ruben-VandeVelde', 'SnirBroshi', 'github-actions', 'jcommelin', 'mathlib4-merge-conflict-bot'] |
b-mehta assignee:b-mehta |
4-61272 4 days ago |
4-60418 4 days ago |
45-17713 45 days |
| 30898 |
vihdzp author:vihdzp |
feat: characterization of `List.splitBy` |
---
- [x] depends on: #30892
Moved from #16837.
[](https://gitpod.io/from-referrer/)
|
t-data
maintainer-merge
|
117/10 |
Mathlib/Data/List/Flatten.lean,Mathlib/Data/List/SplitBy.lean |
2 |
12 |
['Ruben-VandeVelde', 'github-actions', 'mathlib4-dependent-issues-bot', 'mathlib4-merge-conflict-bot', 'vihdzp'] |
TwoFX assignee:TwoFX |
4-1293 4 days ago |
45-26208 45 days ago |
54-66730 54 days |
| 34668 |
SnirBroshi author:SnirBroshi |
feat(Order/Monotone/Basic): `MonotoneOn` + `InjOn` implies `StrictMonoOn` |
This matches the API for the variants without "on":
- (already exists) `StrictMonoOn → InjOn` for `[LinearOrder α] [Preorder β]`
- `MonotoneOn → InjOn → StrictMonoOn` for `[Preorder α] [PartialOrder β]`
- `MonotoneOn → (StrictMonoOn ↔ InjOn)` for `[LinearOrder α] [PartialOrder β]`
---
[](https://gitpod.io/from-referrer/)
|
t-order
maintainer-merge
|
21/1 |
Mathlib/Order/Monotone/Basic.lean |
1 |
3 |
['Ruben-VandeVelde', 'github-actions'] |
nobody |
1-2601 1 day ago |
1-21557 1 day ago |
3-10819 3 days |
| 34538 |
Vierkantor author:Vierkantor |
chore(Tactic/CasesM): improve `casesm`, `cases_type` and `constructorm` tactic docstrings |
This PR (re)writes the docstrings for the `casesm`, `cases_type` and `constructorm` tactics to consistently match the official style guide, to make sure they are complete while not getting too long.
---
[](https://gitpod.io/from-referrer/)
|
documentation
t-meta
maintainer-merge
|
43/23 |
Mathlib/Tactic/CasesM.lean |
1 |
6 |
['Vierkantor', 'github-actions', 'joneugster'] |
joneugster assignee:joneugster |
0-80917 22 hours ago |
6-58006 6 days ago |
6-57568 6 days |
| 33697 |
artie2000 author:artie2000 |
feat(FieldTheory): real closed field |
* Define real closed fields
* Prove some very basic properties
---
[](https://gitpod.io/from-referrer/)
|
t-algebra
maintainer-merge
label:t-algebra$ |
128/0 |
Mathlib.lean,Mathlib/FieldTheory/IsRealClosed/Basic.lean |
2 |
61 |
['artie2000', 'github-actions', 'riccardobrasca', 'urkud', 'vihdzp'] |
vihdzp assignee:vihdzp |
0-67770 18 hours ago |
1-38490 1 day ago |
21-84835 21 days |
| 34598 |
A-M-Berns author:A-M-Berns |
feat(Geometry/Polygon): nondegeneracy conditions and interconversion with Affine.Triangle |
This PR implements suggestions provided in [this comment](https://github.com/leanprover-community/mathlib4/pull/34393#issuecomment-3810047384) by @jsm28: interconversion between `Polygon P 3` and `Affine.Triangle` as well as the nondegeneracy conditions `NondegenerateVertices` and `NondegenerateEdges`. I tried to keep typeclass restrictions as minimal as possible.
---
|
new-contributor
t-euclidean-geometry
maintainer-merge
|
114/5 |
Mathlib/Geometry/Polygon/Basic.lean |
1 |
15 |
['A-M-Berns', 'github-actions', 'jcommelin', 'jsm28'] |
nobody |
0-62993 17 hours ago |
0-62997 17 hours ago |
3-70977 3 days |
| 34245 |
staroperator author:staroperator |
feat(Data/Set): add `Set.Uncountable` |
There are `Set` specialized shortcuts `Set.Finite`, `Set.Infinite` and `Set.Countable`, but lacking `Set.Uncountable`. I find this useful in #34246.
---
[](https://gitpod.io/from-referrer/)
|
t-data
maintainer-merge
awaiting-zulip
|
82/4 |
Mathlib/Analysis/Real/Cardinality.lean,Mathlib/Data/Set/Countable.lean,Mathlib/SetTheory/Cardinal/Basic.lean |
3 |
16 |
['github-actions', 'joneugster', 'staroperator', 'vihdzp'] |
joneugster assignee:joneugster |
0-59480 16 hours ago |
0-59480 16 hours ago |
12-11217 12 days |
| 34783 |
Jun2M author:Jun2M |
feat(Combinatorics/Graph): add Compatible definition and API |
Preliminary PR for #26770 (subgraph). Adds the `Compatible` predicate and basic API to `Mathlib.Combinatorics.Graph.Basic`.
- **Compatible**: two graphs are compatible if they agree on incidence for every edge in the intersection of their edge sets.
- Includes `Compatible.isLink_iff`, reflexivity/symmetry instances, `IsLink.of_compatible`, `Compatible.of_disjoint_edgeSet`, and the `Inc`/`IsLoopAt`/`IsNonloopAt` variants.
- **copy** API for copying a graph with new vertex/edge sets and `IsLink`.
---
[](https://gitpod.io/from-referrer/)
|
t-combinatorics
maintainer-merge
|
101/1 |
Mathlib/Combinatorics/Graph/Basic.lean |
1 |
8 |
['YaelDillies', 'github-actions'] |
nobody |
0-46621 12 hours ago |
0-48998 13 hours ago |
0-52622 14 hours |
| 34597 |
urkud author:urkud |
chore(UpperHalfPlane): redefine as a structure |
Make `UpperHalfPlane` into a two-field structure rather than a type alias for a subtype, to reduce defeq abuse.
---
[](https://gitpod.io/from-referrer/)
|
maintainer-merge |
179/141 |
Mathlib/Analysis/Complex/IntegerCompl.lean,Mathlib/Analysis/Complex/Periodic.lean,Mathlib/Analysis/Complex/UpperHalfPlane/Basic.lean,Mathlib/Analysis/Complex/UpperHalfPlane/FunctionsBoundedAtInfty.lean,Mathlib/Analysis/Complex/UpperHalfPlane/Manifold.lean,Mathlib/Analysis/Complex/UpperHalfPlane/Metric.lean,Mathlib/Analysis/Complex/UpperHalfPlane/MoebiusAction.lean,Mathlib/Analysis/Complex/UpperHalfPlane/Topology.lean,Mathlib/Analysis/SpecialFunctions/Trigonometric/Cotangent.lean,Mathlib/MeasureTheory/Function/Jacobian.lean,Mathlib/NumberTheory/Modular.lean,Mathlib/NumberTheory/ModularForms/Basic.lean,Mathlib/NumberTheory/ModularForms/Bounds.lean,Mathlib/NumberTheory/ModularForms/EisensteinSeries/E2/Summable.lean,Mathlib/NumberTheory/ModularForms/EisensteinSeries/IsBoundedAtImInfty.lean,Mathlib/NumberTheory/ModularForms/EisensteinSeries/QExpansion.lean,Mathlib/NumberTheory/ModularForms/EisensteinSeries/Summable.lean,Mathlib/NumberTheory/ModularForms/EisensteinSeries/UniformConvergence.lean,Mathlib/NumberTheory/ModularForms/JacobiTheta/OneVariable.lean,Mathlib/NumberTheory/ModularForms/LevelOne.lean,Mathlib/NumberTheory/ModularForms/QExpansion.lean |
21 |
40 |
['CBirkbeck', 'github-actions', 'loefflerd', 'urkud'] |
nobody |
0-36025 10 hours ago |
0-37853 10 hours ago |
4-75453 4 days |
| 34222 |
erdOne author:erdOne |
feat(RingTheory): flat + smooth fibers => smooth |
---
[](https://gitpod.io/from-referrer/)
|
t-ring-theory
maintainer-merge
|
322/13 |
Mathlib.lean,Mathlib/RingTheory/Artinian/Instances.lean,Mathlib/RingTheory/Artinian/Module.lean,Mathlib/RingTheory/Artinian/Ring.lean,Mathlib/RingTheory/Etale/Field.lean,Mathlib/RingTheory/Flat/Localization.lean,Mathlib/RingTheory/Jacobson/Artinian.lean,Mathlib/RingTheory/LocalRing/ResidueField/Fiber.lean,Mathlib/RingTheory/Smooth/Fiber.lean,Mathlib/RingTheory/Unramified/Locus.lean |
10 |
18 |
['chrisflav', 'erdOne', 'github-actions'] |
chrisflav assignee:chrisflav |
0-3829 1 hour ago |
0-39083 10 hours ago |
8-36756 8 days |
| 34695 |
SnirBroshi author:SnirBroshi |
feat(SetTheory/Cardinal/Arithmetic): `Cardinal.mk` is strictly monotone on finite sets |
---
[](https://gitpod.io/from-referrer/)
|
t-set-theory
awaiting-author
maintainer-merge
|
19/0 |
Mathlib/SetTheory/Cardinal/Arithmetic.lean,Mathlib/SetTheory/Cardinal/Basic.lean |
2 |
7 |
['SnirBroshi', 'YaelDillies', 'github-actions'] |
nobody |
0-784 13 minutes ago |
0-7706 2 hours ago |
2-37440 2 days |
| 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 |
| 17518 |
grunweg author:grunweg |
feat: lint on declarations mentioning `Invertible` or `Unique` |
Using the same infrastructure as for #10235. Depends on that PR to land first, and also (for the first lint) a zulip discussion if that change is desired/about the best way to enact it.
---
- [ ] depends on: #10235 |
merge-conflict
t-linter
blocked-by-other-PR
awaiting-zulip
|
149/7 |
Mathlib.lean,Mathlib/Algebra/MvPolynomial/PDeriv.lean,Mathlib/Computability/Halting.lean,Mathlib/Computability/TuringMachine.lean,Mathlib/Data/Fintype/Card.lean,Mathlib/GroupTheory/Perm/DomMulAct.lean,Mathlib/Logic/Basic.lean,Mathlib/Logic/Encodable/Basic.lean,Mathlib/NumberTheory/JacobiSum/Basic.lean,Mathlib/Order/Heyting/Regular.lean,Mathlib/RingTheory/MvPolynomial/Symmetric/FundamentalTheorem.lean,Mathlib/Tactic.lean,Mathlib/Tactic/Linter/UnusedAssumptionInType.lean |
13 |
3 |
['github-actions', 'mathlib4-dependent-issues-bot', 'mergify'] |
nobody |
458-58507 1 year ago |
unknown |
unknown |
| 17623 |
astrainfinita author:astrainfinita |
feat(Algebra/Order/GroupWithZero/Unbundled): add some lemmas |
Some lemmas in `Algebra.Order.GroupWithZero.Unbundled` have incorrect or unsatisfactory names, or assumptions that can be omitted using `ZeroLEOneClass`. The lemmas added in this PR are versions of existing lemmas that use the correct or better name or `ZeroLEOneClass` to omit an assumption. The original lemmas will be deprecated in #17593.
| New name | Old name |
|-------------------------|-------------------------|
| `mul_le_one_left₀` | `Left.mul_le_one_of_le_of_le` |
| `mul_lt_one_of_le_of_lt_left₀` (`0 ≤ ·` version) / `mul_lt_one_of_le_of_lt_of_pos_left` | `Left.mul_lt_of_le_of_lt_one_of_pos` |
| `mul_lt_one_of_lt_of_le_left₀` | `Left.mul_lt_of_lt_of_le_one_of_nonneg` |
| `mul_le_one_right₀` | `Right.mul_le_one_of_le_of_le` |
| `mul_lt_one_of_lt_of_le_right₀` (`0 ≤ ·` version) / `mul_lt_one_of_lt_of_le_of_pos_right` | `Right.mul_lt_one_of_lt_of_le_of_pos` |
| `mul_lt_one_of_le_of_lt_right₀` | `Right.mul_lt_one_of_le_of_lt_of_nonneg` |
The following lemmas use `ZeroLEOneClass`.
| New name | Old name |
|-------------------------|-------------------------|
| `(Left.)one_le_mul₀` | `Left.one_le_mul_of_le_of_le` |
| `Left.one_lt_mul_of_le_of_lt₀` | `Left.one_lt_mul_of_le_of_lt_of_pos` |
| `Left.one_lt_mul_of_lt_of_le₀` | `Left.lt_mul_of_lt_of_one_le_of_nonneg` / `one_lt_mul_of_lt_of_le` (still there) |
| `(Left.)one_lt_mul₀` | |
| `Right.one_le_mul₀` | `Right.one_le_mul_of_le_of_le` |
| `Right.one_lt_mul_of_lt_of_le₀` | `Right.one_lt_mul_of_lt_of_le_of_pos` |
| `Right.one_lt_mul_of_le_of_lt₀` | `Right.one_lt_mul_of_le_of_lt_of_nonneg` / `one_lt_mul_of_le_of_lt` (still there) / `one_lt_mul` (still there) |
| `Right.one_lt_mul₀` | `Right.one_lt_mul_of_lt_of_lt` |
---
Split from #17593.
[](https://gitpod.io/from-referrer/)
|
merge-conflict
t-algebra
awaiting-zulip
t-order
label:t-algebra$ |
146/44 |
Mathlib/Algebra/Order/GroupWithZero/Canonical.lean,Mathlib/Algebra/Order/GroupWithZero/Unbundled.lean |
2 |
11 |
['YaelDillies', 'astrainfinita', 'github-actions', 'j-loreaux'] |
nobody |
440-78038 1 year ago |
unknown |
unknown |
| 8370 |
eric-wieser author:eric-wieser |
refactor(Analysis/NormedSpace/Exponential): remove the `𝕂` argument from `exp` |
This argument is still needed for almost all the lemmas, which means it can longer be found by unification.
We keep around `expSeries 𝕂 A`, as it's needed for talking about the radius of convergence over different base fields.
This is a prerequisite for #8372, as we can't merge the functions until they have the same interface.\
Zulip thread: [#mathlib4 > Real.exp @ 💬](https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/Real.2Eexp/near/401602245)
---
[](https://gitpod.io/from-referrer/)
This is started from the mathport output on https://github.com/leanprover-community/mathlib/pull/19244 |
merge-conflict
t-analysis
awaiting-zulip
|
432/387 |
Mathlib/Analysis/CStarAlgebra/Exponential.lean,Mathlib/Analysis/CStarAlgebra/Spectrum.lean,Mathlib/Analysis/Normed/Algebra/Exponential.lean,Mathlib/Analysis/Normed/Algebra/MatrixExponential.lean,Mathlib/Analysis/Normed/Algebra/QuaternionExponential.lean,Mathlib/Analysis/Normed/Algebra/Spectrum.lean,Mathlib/Analysis/Normed/Algebra/TrivSqZeroExt.lean,Mathlib/Analysis/NormedSpace/DualNumber.lean,Mathlib/Analysis/SpecialFunctions/ContinuousFunctionalCalculus/ExpLog.lean,Mathlib/Analysis/SpecialFunctions/Exponential.lean,Mathlib/Analysis/SpecialFunctions/Trigonometric/Series.lean |
11 |
29 |
['YaelDillies', 'eric-wieser', 'girving', 'github-actions', 'j-loreaux', 'kbuzzard', 'leanprover-community-bot-assistant', 'urkud'] |
nobody |
285-33415 9 months ago |
unknown |
unknown |
| 15654 |
TpmKranz author:TpmKranz |
feat(Computability): language-preserving maps between NFA and RE |
Map REs to NFAs via Thompson's construction and NFAs to REs using GNFAs
Last chunk of #12648
---
- [ ] depends on: #15651
- [ ] depends on: #15649
[](https://gitpod.io/from-referrer/)
|
blocked-by-other-PR
new-contributor
t-computability
merge-conflict
awaiting-zulip
|
985/2 |
Mathlib.lean,Mathlib/Computability/GNFA.lean,Mathlib/Computability/Language.lean,Mathlib/Computability/NFA.lean,Mathlib/Computability/RegularExpressions.lean,Mathlib/Data/FinEnum/Option.lean,docs/references.bib |
7 |
3 |
['github-actions', 'leanprover-community-mathlib4-bot', 'meithecatte'] |
nobody |
274-41315 8 months ago |
unknown |
unknown |
| 23929 |
meithecatte author:meithecatte |
feat(Computability/NFA): improve bound on pumping lemma |
---
- [x] depends on: #25321
[](https://gitpod.io/from-referrer/)
|
t-computability
awaiting-zulip
new-contributor
|
101/10 |
Mathlib/Computability/EpsilonNFA.lean,Mathlib/Computability/NFA.lean |
2 |
41 |
['YaelDillies', 'github-actions', 'leanprover-community-bot-assistant', 'mathlib4-dependent-issues-bot', 'meithecatte'] |
nobody |
241-50917 7 months ago |
241-50918 241 days ago |
0-37135 10 hours |
| 17458 |
urkud author:urkud |
refactor(Algebra/Group): make `IsUnit` a typeclass |
Also change some lemmas to assume `[IsUnit _]` instead of `[Invertible _]`.
Motivated by potential non-defeq diamonds in #14986, see also [Zulip](https://leanprover.zulipchat.com/#narrow/stream/116395-maths/topic/Invertible.20and.20data)
I no longer plan to merge this PR, but I'm going to cherry-pick some changes to a new PR before closing this one.
---
[](https://gitpod.io/from-referrer/)
|
merge-conflict
t-algebra
awaiting-zulip
label:t-algebra$ |
82/72 |
Mathlib/Algebra/CharP/Invertible.lean,Mathlib/Algebra/Group/Invertible/Basic.lean,Mathlib/Algebra/Group/Units/Defs.lean,Mathlib/Algebra/GroupWithZero/Invertible.lean,Mathlib/Algebra/GroupWithZero/Units/Basic.lean,Mathlib/Algebra/Polynomial/Degree/Units.lean,Mathlib/Algebra/Polynomial/Splits.lean,Mathlib/Analysis/Convex/Segment.lean,Mathlib/Analysis/Normed/Affine/Isometry.lean,Mathlib/Analysis/Normed/Ring/Units.lean,Mathlib/CategoryTheory/Linear/Basic.lean,Mathlib/FieldTheory/Finite/Basic.lean,Mathlib/FieldTheory/Separable.lean,Mathlib/FieldTheory/SeparableDegree.lean,Mathlib/GroupTheory/Submonoid/Inverses.lean,Mathlib/LinearAlgebra/AffineSpace/AffineEquiv.lean,Mathlib/LinearAlgebra/AffineSpace/Combination.lean,Mathlib/LinearAlgebra/CliffordAlgebra/Contraction.lean,Mathlib/LinearAlgebra/CliffordAlgebra/Inversion.lean,Mathlib/LinearAlgebra/CliffordAlgebra/SpinGroup.lean,Mathlib/LinearAlgebra/Eigenspace/Minpoly.lean,Mathlib/NumberTheory/MulChar/Basic.lean,Mathlib/RingTheory/Localization/NumDen.lean,Mathlib/RingTheory/Polynomial/Content.lean,Mathlib/RingTheory/Polynomial/GaussLemma.lean,Mathlib/RingTheory/Valuation/Basic.lean |
26 |
12 |
['MichaelStollBayreuth', 'acmepjz', 'eric-wieser', 'github-actions', 'leanprover-bot', 'leanprover-community-bot-assistant', 'urkud'] |
nobody |
214-21664 6 months ago |
unknown |
unknown |
| 25218 |
kckennylau author:kckennylau |
feat(AlgebraicGeometry): Tate normal form of elliptic curves |
---
[](https://gitpod.io/from-referrer/)
|
merge-conflict
t-algebraic-geometry
awaiting-zulip
new-contributor
|
291/26 |
Mathlib.lean,Mathlib/AlgebraicGeometry/EllipticCurve/IsomOfJ.lean,Mathlib/AlgebraicGeometry/EllipticCurve/Modular/TateNormalForm.lean,Mathlib/AlgebraicGeometry/EllipticCurve/NormalForms.lean,Mathlib/AlgebraicGeometry/EllipticCurve/VariableChange.lean |
5 |
31 |
['MichaelStollBayreuth', 'Multramate', 'acmepjz', 'github-actions', 'grunweg', 'kckennylau', 'leanprover-community-bot-assistant'] |
nobody |
214-20502 6 months ago |
unknown |
unknown |
| 28803 |
astrainfinita author:astrainfinita |
refactor: unbundle algebra from `ENormed*` |
Further speed up the search in the algebraic typeclass hierarchy by avoiding searching for `TopologicalSpace`.
This PR continues the work from #23961.
- Change `ESeminormed(Add)Monoid` and `ENormed(Add)Monoid` so they no longer carry algebraic data.
- Deprecate `ESeminormed(Add)CommMonoid` and `ENormed(Add)CommMonoid` in favor of `ESeminormed(Add)Monoid` and `ENormed(Add)Monoid` with a commutative algebraic typeclass.
|Old|New|
|---|---|
| `[ESeminormed(Add)(Comm)Monoid E]` | `[(Add)(Comm)Monoid E] [ESeminormed(Add)Monoid E]` |
| `[ENormed(Add)(Comm)Monoid]` | `[(Add)(Comm)Monoid E] [ENormed(Add)Monoid]` |
See [Zulip discussion](https://leanprover.zulipchat.com/#narrow/channel/144837-PR-reviews/topic/.2328803.20refactor.3A.20unbundle.20algebra.20from.20.60ENormed*.60/with/536024350)
------------
- [x] depends on: #28813 |
t-algebra
merge-conflict
slow-typeclass-synthesis
awaiting-zulip
t-analysis
label:t-algebra$ |
80/63 |
Mathlib/Analysis/CStarAlgebra/CStarMatrix.lean,Mathlib/Analysis/Normed/Group/Basic.lean,Mathlib/Analysis/Normed/Group/Continuity.lean,Mathlib/Analysis/Normed/Group/InfiniteSum.lean,Mathlib/Analysis/NormedSpace/IndicatorFunction.lean,Mathlib/MeasureTheory/Function/L1Space/AEEqFun.lean,Mathlib/MeasureTheory/Function/L1Space/HasFiniteIntegral.lean,Mathlib/MeasureTheory/Function/L1Space/Integrable.lean,Mathlib/MeasureTheory/Function/LocallyIntegrable.lean,Mathlib/MeasureTheory/Function/LpSeminorm/Basic.lean,Mathlib/MeasureTheory/Function/LpSeminorm/CompareExp.lean,Mathlib/MeasureTheory/Function/LpSeminorm/TriangleInequality.lean,Mathlib/MeasureTheory/Integral/IntegrableOn.lean,Mathlib/MeasureTheory/Integral/IntervalIntegral/Basic.lean |
14 |
28 |
['astrainfinita', 'bryangingechen', 'github-actions', 'grunweg', 'kbuzzard', 'leanprover-bot', 'leanprover-community-mathlib4-bot', 'mathlib-bors', 'mathlib4-dependent-issues-bot', 'mathlib4-merge-conflict-bot', 'sgouezel'] |
grunweg assignee:grunweg |
154-36147 5 months ago |
162-73701 162 days ago |
0-16864 4 hours |
| 28925 |
grunweg author:grunweg |
chore: remove `linear_combination'` tactic |
When `linear_combination` was refactored in #15899, the old code was kept as the `linear_combination'` tactic, for easier migration. The consensus of the zulip discussion ([#mathlib4 > Narrowing the scope of `linear_combination` @ 💬](https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/Narrowing.20the.20scope.20of.20.60linear_combination.60/near/470237816)) was to wait, and "revisit this once people have experienced the various tactics in practice".
One year later, the old tactic has almost no uses: it is unused in mathlib; [searching on github](https://github.com/search?q=linear_combination%27%20path%3A*.lean&type=code) yields 37 hits --- all of which are in various forks of mathlib. Thus, removing this tactic seems appropriate.
---
Do not merge before the zulip discussion has concluded!
[](https://gitpod.io/from-referrer/)
|
merge-conflict
file-removed
awaiting-zulip
|
0/564 |
Mathlib.lean,Mathlib/Tactic.lean,Mathlib/Tactic/LinearCombination'.lean,Mathlib/Tactic/Linter/UnusedTactic.lean,MathlibTest/linear_combination'.lean |
5 |
4 |
['euprunin', 'github-actions', 'grunweg', 'mathlib4-merge-conflict-bot'] |
nobody |
111-13357 3 months ago |
unknown |
unknown |
| 22361 |
rudynicolop author:rudynicolop |
feat(Computability/NFA): nfa closure properties |
Add the closure properties union, intersection and reversal for NFA.
---
[](https://gitpod.io/from-referrer/)
|
new-contributor
t-computability
merge-conflict
awaiting-author
awaiting-zulip
|
218/2 |
Mathlib/Computability/Language.lean,Mathlib/Computability/NFA.lean |
2 |
91 |
['EtienneC30', 'b-mehta', 'ctchou', 'github-actions', 'leanprover-community-bot-assistant', 'meithecatte', 'rudynicolop'] |
EtienneC30 assignee:EtienneC30 |
92-23047 3 months ago |
unknown |
unknown |
| 30150 |
imbrem author:imbrem |
feat(CategoryTheory/Monoidal): to_additive for MonoidalCategory |
Add `AddMonoidalCategory`, the additive version of `MonoidalCategory`.
To get this to work, I needed to _remove_ the `to_additive` attributes in `Discrete.lean`, since existing code relies on the `AddMonoid M → MonoidalCategory M` instance. For now, we simply implement the additive variants by hand instead.
---
As discussed in #28718; I added an `AddMonoidalCategory` struct and tagged `MonoidalCategory` with `to_additive`, along with the lemmas in `Category.lean`.
I think this is the right approach, since under this framework the "correct" additive version of `Discrete.lean` would be mapping an `AddMonoid` to an `AddMonoidalCategory`.
Next steps would be to:
- Make `monoidal_coherence` and `coherence` support `AddMonoidalCategory`
- Add `CocartesianMonoidalCategory` extending `AddMonoidalCategory`
[](https://gitpod.io/from-referrer/)
|
t-category-theory
large-import
new-contributor
merge-conflict
awaiting-zulip
t-meta
|
444/125 |
Mathlib/CategoryTheory/Monoidal/Category.lean,Mathlib/CategoryTheory/Monoidal/Discrete.lean,Mathlib/Tactic/ToAdditive/GuessName.lean |
3 |
22 |
['JovanGerb', 'YaelDillies', 'github-actions', 'imbrem', 'mathlib4-merge-conflict-bot'] |
nobody |
83-24231 2 months ago |
123-2897 123 days ago |
0-29227 8 hours |
| 15651 |
TpmKranz author:TpmKranz |
feat(Computability/NFA): operations for Thompson's construction |
Lays the groundwork for a proof of equivalence of RE and NFA, w.r.t. described language. Actual connection to REs comes later, after the groundwork for the opposite direction has been laid.
Third chunk of #12648
---
[](https://gitpod.io/from-referrer/)
|
new-contributor
t-computability
merge-conflict
awaiting-author
awaiting-zulip
|
307/5 |
Mathlib/Computability/NFA.lean |
1 |
27 |
['TpmKranz', 'YaelDillies', 'dupuisf', 'github-actions', 'leanprover-community-bot-assistant', 'meithecatte', 'rudynicolop'] |
nobody |
78-41363 2 months ago |
unknown |
unknown |
| 15649 |
TpmKranz author:TpmKranz |
feat(Computability): introduce Generalised NFA as bridge to Regular Expression |
Lays the groundwork for a proof of equivalence of NFA and RE, w.r.t. described language. Actual connection to NFA comes later, after the groundwork for the opposite direction has been laid.
Second chunk of #12648
---
- [x] depends on: #15647 [Data.FinEnum.Option unchanged since then]
[](https://gitpod.io/from-referrer/)
|
new-contributor
t-computability
merge-conflict
awaiting-author
awaiting-zulip
|
298/0 |
Mathlib.lean,Mathlib/Computability/GNFA.lean,Mathlib/Computability/Language.lean,Mathlib/Computability/RegularExpressions.lean,docs/references.bib |
5 |
7 |
['github-actions', 'mathlib4-dependent-issues-bot', 'mathlib4-merge-conflict-bot', 'meithecatte', 'trivial1711'] |
nobody |
77-57604 2 months ago |
unknown |
unknown |
| 20238 |
maemre author:maemre |
feat(Computability/DFA): Closure of regular languages under some set operations |
This shows that regular languages are closed under complement and intersection by constructing DFAs for them.
---
Closure under all other operations will be proved when someone adds the proof for DFA<->regular expression equivalence, so they are not part of this PR.
[](https://gitpod.io/from-referrer/)
|
new-contributor
t-computability
merge-conflict
awaiting-author
awaiting-zulip
|
159/0 |
Mathlib/Computability/DFA.lean,Mathlib/Computability/Language.lean |
2 |
60 |
['EtienneC30', 'YaelDillies', 'github-actions', 'maemre', 'mathlib4-merge-conflict-bot', 'meithecatte', 'urkud'] |
EtienneC30 assignee:EtienneC30 |
77-56694 2 months ago |
unknown |
unknown |
| 20648 |
anthonyde author:anthonyde |
feat: formalize regular expression -> εNFA |
The file `Computability/RegularExpressionsToEpsilonNFA.lean` contains a formal definition of Thompson's method for constructing an `εNFA` from a `RegularExpression` and a proof of its correctness.
---
- [x] depends on: #20644
- [x] depends on: #20645
[](https://gitpod.io/from-referrer/)
|
merge-conflict
t-computability
awaiting-zulip
new-contributor
|
490/0 |
Mathlib.lean,Mathlib/Computability/RegularExpressionsToEpsilonNFA.lean,docs/references.bib |
3 |
7 |
['anthonyde', 'github-actions', 'mathlib4-dependent-issues-bot', 'mathlib4-merge-conflict-bot', 'meithecatte', 'qawbecrdtey'] |
nobody |
77-8372 2 months ago |
unknown |
unknown |
| 11800 |
JADekker author:JADekker |
feat: KappaLindelöf spaces |
Define KappaLindelöf spaces by following the first one-third of the API for Lindelöf spaces. The remainder will be added in a future PR.
---
[](https://gitpod.io/from-referrer/)
|
please-adopt
merge-conflict
t-topology
awaiting-zulip
|
301/2 |
Mathlib.lean,Mathlib/Topology/Compactness/KappaLindelof.lean,Mathlib/Topology/Compactness/Lindelof.lean |
3 |
38 |
['ADedecker', 'JADekker', 'PatrickMassot', 'StevenClontz', 'adomani', 'github-actions', 'grunweg', 'kim-em', 'urkud'] |
nobody |
76-66638 2 months ago |
unknown |
unknown |
| 30750 |
SnirBroshi author:SnirBroshi |
feat(Data/Quot): `toSet` and `equivClassOf` |
Define `toSet` which gets the set corresponding to an element of a quotient, and `equivClassOf` which gets the equivalence class of an element under a quotient.
---
I found these definitions helpful when working with quotients, specifically `ConnectedComponents` of a `TopologicalSpace`.
Additionally, I need `equivSigmaToSet` (in `Data/Setoid/Basic`) to prove things about `SimpleGraph.ConnectedComponent`.
[](https://gitpod.io/from-referrer/)
|
t-data
awaiting-author
awaiting-zulip
|
179/0 |
Mathlib/Data/Quot.lean,Mathlib/Data/Set/Image.lean,Mathlib/Data/SetLike/Basic.lean,Mathlib/Data/Setoid/Basic.lean |
4 |
3 |
['TwoFX', 'eric-wieser', 'github-actions'] |
TwoFX assignee:TwoFX |
69-7160 2 months ago |
69-7160 69 days ago |
35-75966 35 days |
| 30668 |
astrainfinita author:astrainfinita |
feat: `QuotType` |
This typeclass is primarily for use by type synonyms of `Quot` and `Quotient`. Using `QuotType` API for type synonyms of `Quot` and `Quotient` will avoid defeq abuse caused by directly using `Quot` and `Quotient` APIs.
This PR also adds some typeclasses to support different ways to find the quotient map that should be used. See the documentation comments of these typeclasses for examples of usage.
---
It's not a typical design to use these auxiliary typeclasses and term elaborators, but I haven't found a better way to support these notations.
Some of the naming may need to be discussed. For example:
- `⟦·⟧` is currently called `mkQ` in names. This distinguishes it from other `.mk`s and makes it possible to write the quotient map as `mkQ` `mkQ'` ~~`mkQ_ h`~~. But this will also require changing the old lemma names.
- It would be helpful if the names of new type classes explained their functionality better.
[Zulip](https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/migrate.20to.20.60QuotLike.60.20API)
This PR continues the work from #16421.
Original PR: https://github.com/leanprover-community/mathlib4/pull/16421 |
RFC
t-data
awaiting-zulip
|
629/0 |
Mathlib.lean,Mathlib/Data/QuotType.lean,MathlibTest/QuotType.lean |
3 |
20 |
['YaelDillies', 'astrainfinita', 'github-actions', 'mathlib4-merge-conflict-bot', 'plp127', 'vihdzp'] |
nobody |
55-48484 1 month ago |
unknown |
unknown |
| 33368 |
urkud author:urkud |
feat: define `Complex.UnitDisc.shift` |
Also review the existing API
UPD: I'm going to define a `PSL(2, Real)` action instead.
---
[](https://gitpod.io/from-referrer/) |
t-analysis
awaiting-zulip
merge-conflict
|
273/39 |
Mathlib.lean,Mathlib/Analysis/Complex/UnitDisc/Basic.lean,Mathlib/Analysis/Complex/UnitDisc/Shift.lean |
3 |
7 |
['github-actions', 'j-loreaux', 'mathlib4-merge-conflict-bot', 'sgouezel', 'urkud'] |
j-loreaux assignee:j-loreaux |
28-16797 28 days ago |
28-63530 28 days ago |
5-70690 5 days |
| 33441 |
dupuisf author:dupuisf |
feat: add `LawfulInv` class for types with an inverse that behaves like `Ring.inverse` |
This PR introduces a new typeclass `LawfulInv` for types which have an `Inv` instance that is equal to zero on non-invertible elements. This is meant to replace `Ring.inverse`. The current plan is to do this refactor in several steps:
1. This PR, which only introduces the class and adds instances for matrices and continuous linear maps.
2. Add instances for all C*-algebras, and make `CStarAlgebra` extend this.
3. Deprecate `Ring.inverse`.
---
[](https://gitpod.io/from-referrer/)
|
awaiting-zulip
t-algebra
label:t-algebra$ |
185/27 |
Mathlib/Algebra/GroupWithZero/Defs.lean,Mathlib/Algebra/GroupWithZero/Invertible.lean,Mathlib/Algebra/GroupWithZero/Units/Basic.lean,Mathlib/LinearAlgebra/Matrix/NonsingularInverse.lean,Mathlib/LinearAlgebra/Matrix/PosDef.lean,Mathlib/RingTheory/DividedPowers/Padic.lean,Mathlib/Topology/Algebra/Module/Equiv.lean |
7 |
34 |
['dupuisf', 'eric-wieser', 'github-actions', 'j-loreaux', 'mathlib4-merge-conflict-bot', 'plp127'] |
nobody |
14-46876 14 days ago |
14-47943 14 days ago |
7-54144 7 days |
| 32828 |
Hagb author:Hagb |
feat(Algebra/Order/Group/Defs): add `IsOrderedAddMonoid.toIsOrderedCancelAddMonoid'` |
It is similar to `IsOrderedAddMonoid.toIsOrderedCancelAddMonoid`, while with different hypotheses.
The conclusion `IsOrderedCancelMonoid α` on
`IsOrderedAddMonoid.toIsOrderedCancelAddMonoid` still holds when the hypothesis `CommGroup α` is weakened to `CancelCommMonoid α` while `PartialOrder α` is strengthened to `LinearOrder α`.
---
[`IsOrderedAddMonoid.toIsOrderedCancelAddMonoid`](https://leanprover-community.github.io/mathlib4_docs/find/?pattern=IsOrderedAddMonoid.toIsOrderedCancelAddMonoid#doc) and `IsOrderedAddMonoid.toIsOrderedCancelAddMonoid'`:
https://github.com/leanprover-community/mathlib4/blob/97f78b1a4311fed1844b94f1c069219a48a098e1/Mathlib/Algebra/Order/Group/Defs.lean#L52-L62
[](https://gitpod.io/from-referrer/)
|
awaiting-zulip
t-algebra
label:t-algebra$ |
4/0 |
Mathlib/Algebra/Order/Group/Defs.lean |
1 |
8 |
['Garmelon', 'Vierkantor', 'artie2000', 'github-actions', 'leanprover-radar'] |
eric-wieser assignee:eric-wieser |
12-65632 12 days ago |
12-65632 12 days ago |
40-36049 40 days |
| 34396 |
dupuisf author:dupuisf |
feat: notation for `Ring.inverse` |
This PR adds the global notation `x⁻¹ʳ` for `Ring.inverse x`, and a few extra API lemmas about it.
---
[](https://gitpod.io/from-referrer/)
|
t-algebra
awaiting-zulip
label:t-algebra$ |
58/19 |
Mathlib/Algebra/GroupWithZero/Units/Basic.lean |
1 |
1 |
['github-actions'] |
nobody |
10-18663 10 days ago |
unknown |
unknown |
| 33031 |
chiyunhsu author:chiyunhsu |
feat(Combinatorics/Enumerative/Partition): add combinatorial proof of Euler's partition theorem |
The new file EulerComb.lean contains the combinatorial proof of Euler's partition theorem. The analytic proof of the theorem and its generalization of Glaisher's Theorem has already been formalized in [Glaisher.lean](https://github.com/leanprover-community/mathlib4/blob/master/Mathlib/Combinatorics/Enumerative/Partition/Glaisher.lean). The generalization of the combinatorial proof from this file to Glaisher's Theorem is within reach.
---
Zulip discussion: [#mathlib4 > Glaisher’s Bijection on integer partitions](https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/Glaisher.E2.80.99s.20Bijection.20on.20integer.20partitions/with/570808111)
[](https://gitpod.io/from-referrer/)
|
t-combinatorics
new-contributor
awaiting-zulip
|
531/0 |
Mathlib.lean,Mathlib/Combinatorics/Enumerative/Partition/EulerComb.lean |
2 |
5 |
['chiyunhsu', 'github-actions', 'tb65536', 'vihdzp'] |
b-mehta assignee:b-mehta |
5-70450 5 days ago |
5-70450 5 days ago |
42-19879 42 days |
| 26299 |
adomani author:adomani |
perf: the `whitespace` linter only acts on modified files |
Introduces an `IO.Ref` to allow the `commandStart` linter to only run on files that git considers modified with respect to `master`.
The linter is also active on files that have had some error, as these are likely being modified!
The PR should also mitigate the speed-up that the linter introduced:
[#mathlib4 > A whitespace linter @ 💬](https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/A.20whitespace.20linter/near/525091877)
Assuming that this goes well, a similar mechanism could be applied to several linters that do not need to run on all code, just on the modified code.
Implementation detail: the linter is currently either on or off in "whole" files. It may be also a future development to make this more granular and only run the linter on "modifed commands in modified files", but this is not currently the plan for this modification!
---
[](https://gitpod.io/from-referrer/)
|
t-linter
awaiting-zulip
|
55/7 |
Mathlib/Tactic/Linter/Whitespace.lean |
1 |
18 |
['adomani', 'eric-wieser', 'github-actions', 'grunweg', 'kim-em', 'leanprover-bot', 'leanprover-radar', 'mathlib-bors', 'mathlib4-merge-conflict-bot'] |
grunweg assignee:grunweg |
5-30160 5 days ago |
159-3552 159 days ago |
66-67660 66 days |
| 34656 |
vihdzp author:vihdzp |
refactor: review `exists_irreducible_of_degree_pos` theorems |
This PR does the following:
- Rename `exists_irreducible_of_degree_pos` to `exists_irreducible_dvd_of_degree_pos`. The previous name reads as if this were proving that an irreducible polynomial of any positive degree exists.
- Deprecate variants which differ only in the spelling of `0 < f.degree`. We already have quite a lot of API for converting between `natDegree` and `degree`, and we should just use that instead.
---
[](https://gitpod.io/from-referrer/)
|
t-ring-theory
t-algebra
awaiting-zulip
label:t-algebra$ |
9/4 |
Mathlib/RingTheory/Polynomial/UniqueFactorization.lean |
1 |
4 |
['github-actions', 'tb65536', 'vihdzp'] |
nobody |
3-6116 3 days ago |
3-6116 3 days ago |
0-48545 13 hours |
| 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), M i, for S : Set ι.
Our primary motivation is to formalise the notion of "restricted tensor
products". This will be the content of a follow-up PR.
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.
---
Stub file with preliminary definition of the restricted tensor product as a direct limit of tensors indexed by finite subsets of an index type:
https://github.com/PrParadoxy/mathlib4/blob/restricted-stub/Mathlib/LinearAlgebra/PiTensorProduct/Restricted.lean
---
- [x] depends on: #32598
[](https://gitpod.io/from-referrer/)
|
new-contributor
awaiting-zulip
t-algebra
label:t-algebra$ |
300/2 |
Mathlib.lean,Mathlib/LinearAlgebra/PiTensorProduct.lean,Mathlib/LinearAlgebra/PiTensorProduct/Set.lean |
3 |
28 |
['PrParadoxy', 'dagurtomas', 'eric-wieser', 'github-actions', 'goliath-klein', 'leanprover-radar', 'mathlib4-dependent-issues-bot', 'mathlib4-merge-conflict-bot'] |
dagurtomas assignee:dagurtomas |
2-83055 2 days ago |
43-59957 43 days ago |
10-64694 10 days |
| 32742 |
LTolDe author:LTolDe |
feat(MeasureTheory/Constructions/Polish/Basic): add class SuslinSpace |
add new class `SuslinSpace` for a topological space that is an analytic set in itself
This will be useful 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
awaiting-zulip
t-measure-probability
|
4/0 |
Mathlib/MeasureTheory/Constructions/Polish/Basic.lean |
1 |
9 |
['ADedecker', 'LTolDe', 'dupuisf', 'github-actions', 'jcommelin'] |
PatrickMassot assignee:PatrickMassot |
2-82860 2 days ago |
28-66992 28 days ago |
11-6345 11 days |
| 34111 |
themathqueen author:themathqueen |
feat(Algebra/Star/LinearMap): the convolutive intrinsic star ring on linear maps |
There is a star ring on linear maps from coalgebras to star-algebras, where the ring structure is given by [convNonUnitalNonAssocRing](https://leanprover-community.github.io/mathlib4_docs/Mathlib/RingTheory/Coalgebra/Convolution.html#LinearMap.convNonUnitalNonAssocRing) and the star structure is given by [intrinsicStarAddMonoid](https://leanprover-community.github.io/mathlib4_docs/Mathlib/Algebra/Star/LinearMap.html#LinearMap.intrinsicStarAddMonoid), given that `star comul = comm ∘ₗ comul`. This is true, for example, in finite-dimensional C*-algebras under the GNS construction [PositiveLinearMap.GNS](https://leanprover-community.github.io/mathlib4_docs/Mathlib/Analysis/CStarAlgebra/GelfandNaimarkSegal.html#PositiveLinearMap.GNS) and the adjoint coalgebra [InnerProductSpace.coalgebraOfAlgebra](https://leanprover-community.github.io/mathlib4_docs/Mathlib/Analysis/InnerProductSpace/Coalgebra.html#InnerProductSpace.coalgebraOfAlgebra).
Another separate example is linear maps from `n -> R` to `m -> R`.
---
[](https://gitpod.io/from-referrer/)
|
t-algebra
awaiting-author
awaiting-zulip
label:t-algebra$ |
66/0 |
Mathlib/Algebra/Star/LinearMap.lean,Mathlib/LinearAlgebra/TensorProduct/Basic.lean |
2 |
10 |
['github-actions', 'j-loreaux', 'themathqueen'] |
j-loreaux assignee:j-loreaux |
0-60228 16 hours ago |
0-60295 16 hours ago |
15-33481 15 days |
| 34245 |
staroperator author:staroperator |
feat(Data/Set): add `Set.Uncountable` |
There are `Set` specialized shortcuts `Set.Finite`, `Set.Infinite` and `Set.Countable`, but lacking `Set.Uncountable`. I find this useful in #34246.
---
[](https://gitpod.io/from-referrer/)
|
t-data
maintainer-merge
awaiting-zulip
|
82/4 |
Mathlib/Analysis/Real/Cardinality.lean,Mathlib/Data/Set/Countable.lean,Mathlib/SetTheory/Cardinal/Basic.lean |
3 |
16 |
['github-actions', 'joneugster', 'staroperator', 'vihdzp'] |
joneugster assignee:joneugster |
0-59480 16 hours ago |
0-59480 16 hours ago |
12-11217 12 days |