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 |
| 35627 |
SnirBroshi author:SnirBroshi |
feat(Combinatorics/SimpleGraph/Finite): min/max degrees of top/bot |
And a couple of lemmas about `IsRegularOfDegree`, e.g. the empty graph is regular of any degree.
---
[](https://gitpod.io/from-referrer/)
|
t-combinatorics
maintainer-merge
|
30/1 |
Mathlib/Combinatorics/SimpleGraph/Finite.lean,Mathlib/Combinatorics/SimpleGraph/StronglyRegular.lean |
2 |
15 |
['SnirBroshi', 'YaelDillies', 'github-actions', 'vlad902'] |
kmill assignee:kmill |
14-40244 14 days ago |
15-60666 15 days ago |
41-8961 41 days |
| 35084 |
edegeltje author:edegeltje |
feat(Combinatorics/SimpleGraph): Cayley graph for structures with `Mul`/`Add` |
This pr:
- adds the definition `SimpleGraph.mulCayley`, where `x` is adjacent to a distinct `y` when there is `g` such that `x * g = y` or `x = y * g`,
- proves various lemmas about the above,
- adds/proves the additive versions of all of the above
some related zulip conversation: https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/Cayley.20and.20circulant.20graph/with/572839048
---
[](https://gitpod.io/from-referrer/)
|
t-combinatorics
maintainer-merge
|
141/0 |
Mathlib.lean,Mathlib/Combinatorics/SimpleGraph/Cayley.lean |
2 |
44 |
['SnirBroshi', 'YaelDillies', 'edegeltje', 'github-actions', 'vihdzp', 'vlad902'] |
kmill assignee:kmill |
13-17021 13 days ago |
16-9041 16 days ago |
52-81301 52 days |
| 36216 |
michaellee94 author:michaellee94 |
feat(CategoryTheory): characterize pullback squares via the `Over` category |
---
[](https://gitpod.io/from-referrer/)
|
t-category-theory
new-contributor
maintainer-merge
awaiting-author
|
47/0 |
Mathlib/CategoryTheory/Limits/Shapes/Pullback/IsPullback/Basic.lean |
1 |
18 |
['dagurtomas', 'github-actions', 'joelriou', 'michaellee94'] |
robin-carlier assignee:robin-carlier |
10-79141 10 days ago |
10-79141 10 days ago |
2-50782 2 days |
| 37053 |
artie2000 author:artie2000 |
refactor(Analysis/Convex/Cone): use `PointedCone` in Riesz extension theorem |
Change the statement of the Riesz extension theorem to take a `PointedCone` rather than a `ConvexCone`.
---
[](https://gitpod.io/from-referrer/)
|
t-convex-geometry
maintainer-merge
|
15/12 |
Mathlib/Analysis/Convex/Cone/Extension.lean,Mathlib/Geometry/Convex/Cone/Pointed.lean |
2 |
3 |
['YaelDillies', 'github-actions'] |
nobody |
9-66452 9 days ago |
11-57669 11 days ago |
12-31305 12 days |
| 35613 |
SnirBroshi author:SnirBroshi |
feat(Combinatorics/SimpleGraph/Clique): use `IsContained` instead of an explicit embedding from top |
This makes theorems require only a proof that a `Copy` exists rather than provide an explicit `Embedding`.
Also tag monotonicity lemmas with `@[gcongr]`, and add `Copy.isContained` / `Embedding.isIndContained` / `Embedding.isContained` / `Iso.isContained'`.
---
This isn't a generalization per-se since one could use choice plus `Copy.topEmbedding` to upgrade the `IsContained` to an embedding, but `IsContained` makes more sense in theorems.
[](https://gitpod.io/from-referrer/)
|
t-combinatorics
maintainer-merge
|
65/55 |
Mathlib/Combinatorics/SimpleGraph/Clique.lean,Mathlib/Combinatorics/SimpleGraph/CompleteMultipartite.lean,Mathlib/Combinatorics/SimpleGraph/Copy.lean,Mathlib/Combinatorics/SimpleGraph/Extremal/Turan.lean |
4 |
21 |
['SnirBroshi', 'YaelDillies', 'github-actions'] |
awainverse assignee:awainverse |
8-26898 8 days ago |
14-19277 14 days ago |
38-1562 38 days |
| 33935 |
mckoen author:mckoen |
feat(CategoryTheory/Monoidal/Arrow): define monoidal structure on arrow category |
defines a monoidal category structure on the arrow category of a cartesian closed category.
---
- [x] depends on: #33974
- [x] depends on: #34887
[](https://gitpod.io/from-referrer/)
|
t-category-theory
maintainer-merge
large-import
|
635/1 |
Mathlib.lean,Mathlib/CategoryTheory/Monoidal/Arrow.lean,Mathlib/CategoryTheory/Monoidal/Closed/Basic.lean,Mathlib/CategoryTheory/Monoidal/Limits/HasLimits.lean,Mathlib/CategoryTheory/Monoidal/Limits/Shapes/Pullback.lean,Mathlib/CategoryTheory/Monoidal/PushoutProduct.lean |
6 |
39 |
['dagurtomas', 'github-actions', 'joelriou', 'mathlib-dependent-issues', 'mckoen'] |
joelriou assignee:joelriou |
4-86194 4 days ago |
4-86194 4 days ago |
26-40759 26 days |
| 37420 |
artie2000 author:artie2000 |
refactor: change definitions to avoid `ConvexCone` |
Change the definitions of `PointedCone.positive` and `PointedCone.closure` to avoid mentioning `ConvexCone`.
This PR is part of a series deprecating `ConvexCone`: https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/Replacing.20.60ConvexCone.60.20with.20.60PointedCone.60/with/582738985
---
[](https://gitpod.io/from-referrer/)
|
t-convex-geometry
maintainer-merge
|
10/4 |
Mathlib/Analysis/Convex/Cone/Closure.lean,Mathlib/Geometry/Convex/Cone/Pointed.lean |
2 |
2 |
['YaelDillies', 'github-actions', 'ooovi', 'vihdzp'] |
nobody |
4-35558 4 days ago |
6-35177 6 days ago |
6-35306 6 days |
| 37592 |
erdOne author:erdOne |
feat: set up API for `ConvexSpace` |
We introduce `sConvexCombo` and the indexed version `iConvexCombo` as the main API for `ConvexSpace` and prove lemmas around the new definitions.
---
[](https://gitpod.io/from-referrer/)
|
t-algebra
large-import
maintainer-merge
label:t-algebra$ |
452/133 |
Mathlib/Analysis/Convex/MetricSpace.lean,Mathlib/LinearAlgebra/ConvexSpace.lean,Mathlib/LinearAlgebra/ConvexSpace/AffineSpace.lean |
3 |
15 |
['YaelDillies', 'erdOne', 'github-actions'] |
nobody |
3-2539 3 days ago |
3-18467 3 days ago |
3-19726 3 days |
| 35250 |
vlad902 author:vlad902 |
feat(SimpleGraph): redefine `cycleGraph` independent of `circulantGraph` |
Right now the `cycleGraph` definition relies on `circulantGraph` which requires importing Group definitions from the algebra hierarchy. This causes large-imports for me in later PRs where I try to make more widespread use of cycleGraphs, so here I redefine it to be its own independent object, and leave moving it from `Circulant.lean` to another PR (this is parallel to #35084.)
---
[](https://gitpod.io/from-referrer/)
|
t-combinatorics
maintainer-merge
|
10/10 |
Mathlib/Combinatorics/SimpleGraph/Circulant.lean |
1 |
5 |
['SnirBroshi', 'YaelDillies', 'b-mehta', 'github-actions', 'vihdzp', 'vlad902'] |
nobody |
2-80172 2 days ago |
52-20396 52 days ago |
52-20388 52 days |
| 33463 |
khwilson author:khwilson |
feat(Mathlib/Analysis/Polynomial/MahlerMeasure): Mahler Measure for other rings |
Define `mahlerMeasure'` which allows you specify a norm preserving map `v` from any `NormedRing A` (or more general) to `ℂ`. Also provide wrappers around the main `mahlerMeasure` lemmas that are used for estimation.
---
[](https://gitpod.io/from-referrer/)
|
new-contributor
t-analysis
maintainer-merge
|
98/5 |
Mathlib/Analysis/Polynomial/MahlerMeasure.lean,Mathlib/NumberTheory/MahlerMeasure.lean |
2 |
40 |
['github-actions', 'j-loreaux', 'khwilson', 'kim-em', 'plp127', 'vlad902'] |
nobody |
2-79072 2 days ago |
3-19154 3 days ago |
3-24208 3 days |
| 36399 |
chrisflav author:chrisflav |
feat(RingTheory/Flat): finite flat algebra is trivial if rank is equal to `1` |
From Pi1.
---
[](https://gitpod.io/from-referrer/)
|
t-ring-theory
maintainer-merge
|
168/3 |
Mathlib.lean,Mathlib/LinearAlgebra/Trace.lean,Mathlib/RingTheory/Flat/Rank.lean,Mathlib/RingTheory/Localization/BaseChange.lean,Mathlib/RingTheory/Spectrum/Prime/Topology.lean,Mathlib/RingTheory/TensorProduct/Maps.lean |
6 |
11 |
['chrisflav', 'github-actions', 'riccardobrasca', 'robin-carlier'] |
alreadydone assignee:alreadydone |
2-25112 2 days ago |
3-20868 3 days ago |
28-7437 28 days |
| 36638 |
CoolRmal author:CoolRmal |
feat: if `f` lies in a closed convex set `s` almost everywhere, then its conditional expectation also lies in `s` almost everywhere |
---
- [x] depends on: #27953
[](https://gitpod.io/from-referrer/)
|
t-measure-probability
maintainer-merge
|
64/14 |
Mathlib/MeasureTheory/Function/ConditionalExpectation/CondJensen.lean |
1 |
10 |
['CoolRmal', 'EtienneC30', 'github-actions', 'mathlib-dependent-issues', 'mathlib-merge-conflicts'] |
EtienneC30 assignee:EtienneC30 |
2-11653 2 days ago |
4-68308 4 days ago |
17-3961 17 days |
| 35906 |
scp020 author:scp020 |
feat(Combinatorics/SimpleGraph/Walk): chords of walks |
Define `Walk.IsChord` and `Walk.IsChordless` predicates in a new file `SimpleGraph/Walks/Chord.lean`.
See "chord" in https://en.wikipedia.org/wiki/Glossary_of_graph_theory
---
[Zulip](https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/Walk.2EIsChordless.20live.20in.20mathlib.3F/with/575277309)
[](https://gitpod.io/from-referrer/)
|
t-combinatorics
new-contributor
maintainer-merge
|
59/0 |
Mathlib.lean,Mathlib/Combinatorics/SimpleGraph/Walk/Chord.lean |
2 |
68 |
['SnirBroshi', 'YaelDillies', 'github-actions', 'mathlib-merge-conflicts', 'scp020'] |
YaelDillies assignee:YaelDillies |
1-45186 1 day ago |
1-62323 1 day ago |
26-52180 26 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 |
| 35627 |
SnirBroshi author:SnirBroshi |
feat(Combinatorics/SimpleGraph/Finite): min/max degrees of top/bot |
And a couple of lemmas about `IsRegularOfDegree`, e.g. the empty graph is regular of any degree.
---
[](https://gitpod.io/from-referrer/)
|
t-combinatorics
maintainer-merge
|
30/1 |
Mathlib/Combinatorics/SimpleGraph/Finite.lean,Mathlib/Combinatorics/SimpleGraph/StronglyRegular.lean |
2 |
15 |
['SnirBroshi', 'YaelDillies', 'github-actions', 'vlad902'] |
kmill assignee:kmill |
14-40244 14 days ago |
15-60666 15 days ago |
41-8961 41 days |
| 35084 |
edegeltje author:edegeltje |
feat(Combinatorics/SimpleGraph): Cayley graph for structures with `Mul`/`Add` |
This pr:
- adds the definition `SimpleGraph.mulCayley`, where `x` is adjacent to a distinct `y` when there is `g` such that `x * g = y` or `x = y * g`,
- proves various lemmas about the above,
- adds/proves the additive versions of all of the above
some related zulip conversation: https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/Cayley.20and.20circulant.20graph/with/572839048
---
[](https://gitpod.io/from-referrer/)
|
t-combinatorics
maintainer-merge
|
141/0 |
Mathlib.lean,Mathlib/Combinatorics/SimpleGraph/Cayley.lean |
2 |
44 |
['SnirBroshi', 'YaelDillies', 'edegeltje', 'github-actions', 'vihdzp', 'vlad902'] |
kmill assignee:kmill |
13-17021 13 days ago |
16-9041 16 days ago |
52-81301 52 days |
| 36216 |
michaellee94 author:michaellee94 |
feat(CategoryTheory): characterize pullback squares via the `Over` category |
---
[](https://gitpod.io/from-referrer/)
|
t-category-theory
new-contributor
maintainer-merge
awaiting-author
|
47/0 |
Mathlib/CategoryTheory/Limits/Shapes/Pullback/IsPullback/Basic.lean |
1 |
18 |
['dagurtomas', 'github-actions', 'joelriou', 'michaellee94'] |
robin-carlier assignee:robin-carlier |
10-79141 10 days ago |
10-79141 10 days ago |
2-50782 2 days |
| 37053 |
artie2000 author:artie2000 |
refactor(Analysis/Convex/Cone): use `PointedCone` in Riesz extension theorem |
Change the statement of the Riesz extension theorem to take a `PointedCone` rather than a `ConvexCone`.
---
[](https://gitpod.io/from-referrer/)
|
t-convex-geometry
maintainer-merge
|
15/12 |
Mathlib/Analysis/Convex/Cone/Extension.lean,Mathlib/Geometry/Convex/Cone/Pointed.lean |
2 |
3 |
['YaelDillies', 'github-actions'] |
nobody |
9-66452 9 days ago |
11-57669 11 days ago |
12-31305 12 days |
| 35613 |
SnirBroshi author:SnirBroshi |
feat(Combinatorics/SimpleGraph/Clique): use `IsContained` instead of an explicit embedding from top |
This makes theorems require only a proof that a `Copy` exists rather than provide an explicit `Embedding`.
Also tag monotonicity lemmas with `@[gcongr]`, and add `Copy.isContained` / `Embedding.isIndContained` / `Embedding.isContained` / `Iso.isContained'`.
---
This isn't a generalization per-se since one could use choice plus `Copy.topEmbedding` to upgrade the `IsContained` to an embedding, but `IsContained` makes more sense in theorems.
[](https://gitpod.io/from-referrer/)
|
t-combinatorics
maintainer-merge
|
65/55 |
Mathlib/Combinatorics/SimpleGraph/Clique.lean,Mathlib/Combinatorics/SimpleGraph/CompleteMultipartite.lean,Mathlib/Combinatorics/SimpleGraph/Copy.lean,Mathlib/Combinatorics/SimpleGraph/Extremal/Turan.lean |
4 |
21 |
['SnirBroshi', 'YaelDillies', 'github-actions'] |
awainverse assignee:awainverse |
8-26898 8 days ago |
14-19277 14 days ago |
38-1562 38 days |
| 33935 |
mckoen author:mckoen |
feat(CategoryTheory/Monoidal/Arrow): define monoidal structure on arrow category |
defines a monoidal category structure on the arrow category of a cartesian closed category.
---
- [x] depends on: #33974
- [x] depends on: #34887
[](https://gitpod.io/from-referrer/)
|
t-category-theory
maintainer-merge
large-import
|
635/1 |
Mathlib.lean,Mathlib/CategoryTheory/Monoidal/Arrow.lean,Mathlib/CategoryTheory/Monoidal/Closed/Basic.lean,Mathlib/CategoryTheory/Monoidal/Limits/HasLimits.lean,Mathlib/CategoryTheory/Monoidal/Limits/Shapes/Pullback.lean,Mathlib/CategoryTheory/Monoidal/PushoutProduct.lean |
6 |
39 |
['dagurtomas', 'github-actions', 'joelriou', 'mathlib-dependent-issues', 'mckoen'] |
joelriou assignee:joelriou |
4-86194 4 days ago |
4-86194 4 days ago |
26-40759 26 days |
| 37420 |
artie2000 author:artie2000 |
refactor: change definitions to avoid `ConvexCone` |
Change the definitions of `PointedCone.positive` and `PointedCone.closure` to avoid mentioning `ConvexCone`.
This PR is part of a series deprecating `ConvexCone`: https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/Replacing.20.60ConvexCone.60.20with.20.60PointedCone.60/with/582738985
---
[](https://gitpod.io/from-referrer/)
|
t-convex-geometry
maintainer-merge
|
10/4 |
Mathlib/Analysis/Convex/Cone/Closure.lean,Mathlib/Geometry/Convex/Cone/Pointed.lean |
2 |
2 |
['YaelDillies', 'github-actions', 'ooovi', 'vihdzp'] |
nobody |
4-35558 4 days ago |
6-35177 6 days ago |
6-35306 6 days |
| 37592 |
erdOne author:erdOne |
feat: set up API for `ConvexSpace` |
We introduce `sConvexCombo` and the indexed version `iConvexCombo` as the main API for `ConvexSpace` and prove lemmas around the new definitions.
---
[](https://gitpod.io/from-referrer/)
|
t-algebra
large-import
maintainer-merge
label:t-algebra$ |
452/133 |
Mathlib/Analysis/Convex/MetricSpace.lean,Mathlib/LinearAlgebra/ConvexSpace.lean,Mathlib/LinearAlgebra/ConvexSpace/AffineSpace.lean |
3 |
15 |
['YaelDillies', 'erdOne', 'github-actions'] |
nobody |
3-2539 3 days ago |
3-18467 3 days ago |
3-19726 3 days |
| 35250 |
vlad902 author:vlad902 |
feat(SimpleGraph): redefine `cycleGraph` independent of `circulantGraph` |
Right now the `cycleGraph` definition relies on `circulantGraph` which requires importing Group definitions from the algebra hierarchy. This causes large-imports for me in later PRs where I try to make more widespread use of cycleGraphs, so here I redefine it to be its own independent object, and leave moving it from `Circulant.lean` to another PR (this is parallel to #35084.)
---
[](https://gitpod.io/from-referrer/)
|
t-combinatorics
maintainer-merge
|
10/10 |
Mathlib/Combinatorics/SimpleGraph/Circulant.lean |
1 |
5 |
['SnirBroshi', 'YaelDillies', 'b-mehta', 'github-actions', 'vihdzp', 'vlad902'] |
nobody |
2-80172 2 days ago |
52-20396 52 days ago |
52-20388 52 days |
| 33463 |
khwilson author:khwilson |
feat(Mathlib/Analysis/Polynomial/MahlerMeasure): Mahler Measure for other rings |
Define `mahlerMeasure'` which allows you specify a norm preserving map `v` from any `NormedRing A` (or more general) to `ℂ`. Also provide wrappers around the main `mahlerMeasure` lemmas that are used for estimation.
---
[](https://gitpod.io/from-referrer/)
|
new-contributor
t-analysis
maintainer-merge
|
98/5 |
Mathlib/Analysis/Polynomial/MahlerMeasure.lean,Mathlib/NumberTheory/MahlerMeasure.lean |
2 |
40 |
['github-actions', 'j-loreaux', 'khwilson', 'kim-em', 'plp127', 'vlad902'] |
nobody |
2-79072 2 days ago |
3-19154 3 days ago |
3-24208 3 days |
| 36399 |
chrisflav author:chrisflav |
feat(RingTheory/Flat): finite flat algebra is trivial if rank is equal to `1` |
From Pi1.
---
[](https://gitpod.io/from-referrer/)
|
t-ring-theory
maintainer-merge
|
168/3 |
Mathlib.lean,Mathlib/LinearAlgebra/Trace.lean,Mathlib/RingTheory/Flat/Rank.lean,Mathlib/RingTheory/Localization/BaseChange.lean,Mathlib/RingTheory/Spectrum/Prime/Topology.lean,Mathlib/RingTheory/TensorProduct/Maps.lean |
6 |
11 |
['chrisflav', 'github-actions', 'riccardobrasca', 'robin-carlier'] |
alreadydone assignee:alreadydone |
2-25112 2 days ago |
3-20868 3 days ago |
28-7437 28 days |
| 36638 |
CoolRmal author:CoolRmal |
feat: if `f` lies in a closed convex set `s` almost everywhere, then its conditional expectation also lies in `s` almost everywhere |
---
- [x] depends on: #27953
[](https://gitpod.io/from-referrer/)
|
t-measure-probability
maintainer-merge
|
64/14 |
Mathlib/MeasureTheory/Function/ConditionalExpectation/CondJensen.lean |
1 |
10 |
['CoolRmal', 'EtienneC30', 'github-actions', 'mathlib-dependent-issues', 'mathlib-merge-conflicts'] |
EtienneC30 assignee:EtienneC30 |
2-11653 2 days ago |
4-68308 4 days ago |
17-3961 17 days |
| 35906 |
scp020 author:scp020 |
feat(Combinatorics/SimpleGraph/Walk): chords of walks |
Define `Walk.IsChord` and `Walk.IsChordless` predicates in a new file `SimpleGraph/Walks/Chord.lean`.
See "chord" in https://en.wikipedia.org/wiki/Glossary_of_graph_theory
---
[Zulip](https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/Walk.2EIsChordless.20live.20in.20mathlib.3F/with/575277309)
[](https://gitpod.io/from-referrer/)
|
t-combinatorics
new-contributor
maintainer-merge
|
59/0 |
Mathlib.lean,Mathlib/Combinatorics/SimpleGraph/Walk/Chord.lean |
2 |
68 |
['SnirBroshi', 'YaelDillies', 'github-actions', 'mathlib-merge-conflicts', 'scp020'] |
YaelDillies assignee:YaelDillies |
1-45186 1 day ago |
1-62323 1 day ago |
26-52180 26 days |
| 37506 |
wwylele author:wwylele |
feat(Analysis/InnerProductSpace): singleton basis for 1d space |
This was brought up in #36462. Similar to existing `FiniteDimensional.basisSingleton`, this provides a OrthonormalBasis version. Also adds simp lemma for `∀ (i j : ι), P i j` for subsingleton `ι`.
---
[](https://gitpod.io/from-referrer/)
|
t-analysis
maintainer-merge
|
49/4 |
Mathlib/Analysis/InnerProductSpace/Orthonormal.lean,Mathlib/Analysis/InnerProductSpace/PiL2.lean,Mathlib/Combinatorics/SimpleGraph/Connectivity/Connected.lean,Mathlib/Combinatorics/SimpleGraph/Diam.lean,Mathlib/Logic/Basic.lean |
5 |
35 |
['eric-wieser', 'github-actions', 'leanprover-radar', 'loefflerd', 'themathqueen', 'wwylele'] |
loefflerd assignee:loefflerd |
0-81831 22 hours ago |
1-19927 1 day ago |
4-66570 4 days |
| 31242 |
plp127 author:plp127 |
feat: express filter as supremum of principal filter and free filter |
Prove a filter is free iff it is smaller than the cofinite filter. Prove that every filter decomposes as the disjoint supremum of a principal filter and a free filter.
---
- [x] depends on: #31264
[](https://gitpod.io/from-referrer/)
|
t-order
maintainer-merge
|
78/4 |
Mathlib/Order/Filter/Basic.lean,Mathlib/Order/Filter/Cofinite.lean,Mathlib/Order/Heyting/Boundary.lean,Mathlib/Order/Lattice.lean |
4 |
10 |
['Komyyy', 'YaelDillies', 'github-actions', 'jcommelin', 'kckennylau', 'mathlib4-dependent-issues-bot', 'mathlib4-merge-conflict-bot', 'plp127'] |
nobody |
0-64044 17 hours ago |
9-9884 9 days ago |
33-32723 33 days |
| 37391 |
grunweg author:grunweg |
fix(create_deprecated_modules): fix the build again |
The code needed updating to the new String API; it failed to build before this PR.
This also removes uses of deprecated String API.
A future PR will add CI to ensure this script builds fine.
(Future future: can we test that we tested all .lean scripts? Or have a test which builds all .lean files in scripts?)
---
We need to annotate a type as `Char` now, perhaps because the default instances (from a `Char` to a `Slice.Pattern`) don't work out as well any more.
[](https://gitpod.io/from-referrer/)
|
tech debt
CI
maintainer-merge
|
22/20 |
scripts/create_deprecated_modules.lean |
1 |
24 |
['adomani', 'github-actions', 'grunweg'] |
adomani assignee:adomani |
0-46957 13 hours ago |
2-11414 2 days ago |
4-55760 4 days |
| 35879 |
Jun2M author:Jun2M |
feat(Combinatorics/Graph): graph deletion operations |
This PR adds definitions and basic lemmas for deleting edges and vertices from a graph in Mathlib/Combinatorics/Graph/Delete.lean.
It introduces the following operations:
- `G ↾ F` (edgeRestrict): The subgraph of G restricted to the edges in F (vertices are preserved).
- `G ＼ F` (edgeDelete): The subgraph of G with the edges in F deleted.
- `G[X]` (induce): The subgraph of G induced by the set of vertices X.
- `G - X` (vertexDelete): The graph obtained from G by deleting the set of vertices X.
These definitions are accompanied by simp lemmas describing their edge sets, incidence relations, and basic properties such as monotonicity.
Co-authored-by: Peter Nelson [apn.uni@gmail.com](mailto:apn.uni@gmail.com)
---
- [x] depends on: #26770
[](https://gitpod.io/from-referrer/)
|
t-combinatorics
maintainer-merge
|
208/0 |
Mathlib.lean,Mathlib/Combinatorics/Graph/Delete.lean |
2 |
8 |
['Jun2M', 'YaelDillies', 'github-actions', 'mathlib-dependent-issues', 'mathlib-merge-conflicts'] |
nobody |
0-40035 11 hours ago |
15-73266 15 days ago |
15-79443 15 days |
| 36720 |
YanYablonovskiy author:YanYablonovskiy |
feat(Order): `OrderType.lift` and more order type API |
Adding the universe lifting operation to `OrderType` , addresses a 'TODO' .
---
[](https://gitpod.io/from-referrer/)
|
t-order
new-contributor
maintainer-merge
|
41/2 |
Mathlib/Order/Types/Defs.lean |
1 |
25 |
['YaelDillies', 'YanYablonovskiy', 'github-actions', 'vihdzp'] |
bryangingechen assignee:bryangingechen |
0-39442 10 hours ago |
14-33973 14 days ago |
15-83921 15 days |
| 36979 |
Komyyy author:Komyyy |
feat: `↑(Nat.log m n) = Ordinal.log ↑m ↑n` |
---
[](https://gitpod.io/from-referrer/)
|
t-set-theory
maintainer-merge
|
12/3 |
Mathlib/SetTheory/Ordinal/Exponential.lean |
1 |
22 |
['Komyyy', 'YaelDillies', 'github-actions', 'mathlib-merge-conflicts', 'plp127', 'vihdzp'] |
YaelDillies assignee:YaelDillies |
0-38163 10 hours ago |
13-24822 13 days ago |
14-77476 14 days |
| 37115 |
tb65536 author:tb65536 |
feat(RingTheory/Flat/Basic): `Submodule.toBaseChange` as a `LinearEquiv` |
If the extensions of rings is flat, then `Submodule.toBaseChange` becomes a `LinearEquiv`.
---
[](https://gitpod.io/from-referrer/)
|
t-ring-theory
t-algebra
maintainer-merge
awaiting-CI
label:t-algebra$ |
21/0 |
Mathlib/RingTheory/Flat/Basic.lean |
1 |
10 |
['faenuccio', 'github-actions', 'robin-carlier', 'tb65536'] |
faenuccio assignee:faenuccio |
0-21757 6 hours ago |
0-23341 6 hours ago |
9-61055 9 days |
| 37000 |
Qulinecier author:Qulinecier |
feat: generalize rank_submatrix_le to arbitrary column maps |
This PR generalizes `rank_submatrix_le` to allow an arbitrary function on columns
instead of requiring an `Equiv`. The previous version required `e : m₀ ≃ m` and
`[Fintype m]`, while this version only requires `c : n₀ → n` and `[Fintype n₀]`.
The previous version can be recovered as a special case of the new one.
---
[](https://gitpod.io/from-referrer/)
|
t-algebra
new-contributor
maintainer-merge
label:t-algebra$ |
16/6 |
Mathlib/LinearAlgebra/Matrix/Rank.lean |
1 |
8 |
['Qulinecier', 'dagurtomas', 'github-actions', 'themathqueen'] |
dagurtomas assignee:dagurtomas |
0-13622 3 hours ago |
0-14242 3 hours ago |
10-46317 10 days |
| 37057 |
erdOne author:erdOne |
feat(AlgebraicTopology): `SimplexCategory.toTop_map_δ_apply` |
---
[](https://gitpod.io/from-referrer/)
|
t-algebraic-topology
maintainer-merge
awaiting-author
|
48/2 |
Mathlib/AlgebraicTopology/CechNerve.lean,Mathlib/AlgebraicTopology/SimplexCategory/Basic.lean,Mathlib/AlgebraicTopology/SimplexCategory/Defs.lean,Mathlib/AlgebraicTopology/TopologicalSimplex.lean,Mathlib/Data/Fin/SuccPred.lean |
5 |
15 |
['Raph-DG', 'dagurtomas', 'erdOne', 'github-actions', 'joelriou', 'mathlib-merge-conflicts', 'riccardobrasca'] |
robin-carlier assignee:robin-carlier |
0-7184 1 hour ago |
0-7184 1 hour ago |
4-49805 4 days |
| 37569 |
j-loreaux author:j-loreaux |
feat: the Fuglede–Putnam–Rosenblum theorem for C⋆-algebras |
Let `A` be a C⋆-algebra, and let `a b x : A`. The Fuglede–Putnam–Rosenblum theorem states that if `a` and `b` are normal and `x` intertwines `a` and `b` (i.e., `SemiconjBy x a b`). Then `x` also intertwines `star a` and `star b`. Fuglede's original result was for `a = b` (i.e., if `x` commutes with `a`, then `x` also commutes with `star a`), and Putnam extended it to intertwining elements. Rosenblum later gave the elementary proof formalized here using Liouville's theorem.
A version of the Fuglede–Putnam theorem also holds for unbounded operators, but it necessitates a different proof technique and holds in different generality than the one given here.
---
[](https://gitpod.io/from-referrer/)
|
t-analysis
maintainer-merge
|
323/13 |
Mathlib.lean,Mathlib/Algebra/Group/Action/Defs.lean,Mathlib/Algebra/GroupWithZero/Action/Units.lean,Mathlib/Analysis/CStarAlgebra/Fuglede.lean,Mathlib/Analysis/Normed/Algebra/Exponential.lean,Mathlib/Analysis/SpecialFunctions/Exponential.lean,Mathlib/Topology/Algebra/InfiniteSum/Ring.lean,docs/references.bib |
8 |
21 |
['github-actions', 'j-loreaux', 'loefflerd'] |
loefflerd assignee:loefflerd |
0-6609 1 hour ago |
0-6668 1 hour ago |
3-62409 3 days |
| 37693 |
Maldooor author:Maldooor |
chore(Analysis/InnerProductSpace/Reproducing): clarify TODO |
---
[](https://gitpod.io/from-referrer/)
|
maintainer-merge
t-analysis
|
3/3 |
Mathlib/Analysis/InnerProductSpace/Reproducing.lean |
1 |
2 |
['YaelDillies', 'github-actions'] |
nobody |
0-3303 55 minutes ago |
0-24419 6 hours ago |
0-24411 6 hours |
| 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 |
| 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 |
502-23876 1 year ago |
509-16435 509 days ago |
33-53295 33 days |
| 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 |
335-73553 11 months ago |
605-10338 605 days ago |
0-179 2 minutes |
| 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 |
275-53902 9 months ago |
547-1545 547 days ago |
0-66650 18 hours |
| 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 |
275-52740 9 months ago |
308-27857 308 days ago |
6-44784 6 days |
| 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 |
215-68385 7 months ago |
224-19539 224 days ago |
0-19882 5 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 |
172-45595 5 months ago |
223-77392 223 days ago |
0-1 1 second |
| 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 |
144-56469 4 months ago |
184-35135 184 days ago |
1-160 1 day |
| 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 |
139-73601 4 months ago |
559-14589 559 days ago |
45-84611 45 days |
| 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 |
139-3442 4 months ago |
484-53372 484 days ago |
23-54870 23 days |
| 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 |
138-40610 4 months ago |
335-73539 335 days ago |
75-77754 75 days |
| 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 |
138-12476 4 months ago |
613-32758 613 days ago |
123-25636 123 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 |
116-80722 3 months ago |
169-49575 169 days ago |
0-81 1 minute |
| 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 |
89-49035 2 months ago |
90-9368 90 days ago |
7-33574 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 |
74-11470 2 months ago |
74-11470 74 days ago |
40-42357 40 days |
| 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 |
67-16288 2 months ago |
67-16288 67 days ago |
42-22427 42 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 |
64-28698 2 months ago |
90-12830 90 days ago |
11-7507 11 days |
| 34720 |
Paul-Lez author:Paul-Lez |
feat(RingTheory/PowerSeries/Composition): define composition of power series |
This PR defines the composition of two power series, and adds various pieces of API lemmas (this is mostly fixing up and upstreaming code from [this repo](https://github.com/rmhi/formal_deriv)).
This is the first of a series of PRs upstreaming work that was done at the CFT workshop in Oxford last summer, working towards proving some results about the `exp` and `log` power series (and their composition!), and constructing the isomorphism $(\mathfrak{m}_K ^ n, +) \cong (1 + \mathfrak{m}_K ^ n, \times)$ for sufficiently large $n$, where $K$ is a characteristic zero local field.
Co-authored-by: Richard Hill
Co-authored-by: Calle Sönne
---
[](https://gitpod.io/from-referrer/)
|
t-ring-theory
awaiting-zulip
|
844/0 |
Mathlib.lean,Mathlib/RingTheory/PowerSeries/Composition.lean |
2 |
3 |
['Paul-Lez', 'github-actions', 'vihdzp'] |
nobody |
55-74707 1 month ago |
63-26627 63 days ago |
0-10 10 seconds |
| 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
merge-conflict
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 |
35 |
['dupuisf', 'eric-wieser', 'github-actions', 'j-loreaux', 'mathlib-merge-conflicts', 'mathlib4-merge-conflict-bot', 'plp127'] |
nobody |
47-47046 1 month ago |
75-80181 75 days ago |
7-54141 7 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
awaiting-author
|
55/7 |
Mathlib/Tactic/Linter/Whitespace.lean |
1 |
19 |
['adomani', 'eric-wieser', 'github-actions', 'grunweg', 'joneugster', 'kim-em', 'leanprover-bot', 'leanprover-radar', 'mathlib-bors', 'mathlib4-merge-conflict-bot'] |
grunweg assignee:grunweg |
47-39472 1 month ago |
220-35790 220 days ago |
66-73556 66 days |
| 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'] |
nobody |
39-33844 1 month ago |
385-11783 385 days ago |
48-67492 48 days |
| 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'] |
nobody |
39-33828 1 month ago |
336-15722 336 days ago |
39-61332 39 days |
| 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
awaiting-author
|
101/10 |
Mathlib/Computability/EpsilonNFA.lean,Mathlib/Computability/NFA.lean |
2 |
42 |
['YaelDillies', 'dagurtomas', 'github-actions', 'leanprover-community-bot-assistant', 'mathlib4-dependent-issues-bot', 'meithecatte'] |
nobody |
38-53857 1 month ago |
302-83156 302 days ago |
34-10092 34 days |
| 34649 |
peabrainiac author:peabrainiac |
feat(Analysis/Calculus/ContDiff): add notation `ℕ∞ω` for `WithTop ℕ∞` |
Add a `ContDiff`-scoped notation `ℕ∞ω` for `WithTop ℕ∞`, accompanying the existing notations `∞` and `ω` for `(⊤ : ℕ∞) : ℕ∞ω` and `⊤ : ℕ∞ω`.
---
[Zulip discussion](https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/RFC.3A.20notation.20for.20.60WithTop.20.E2.84.95.E2.88.9E.60/near/573917824)
I've also replaced `WithTop ℕ∞` with this new notation already in the files that mention it the most, but not in all files yet; many mention `WithTop ℕ∞` just a couple of times but don't open the `ContDiff` namespace. I'm not sure whether that should be taken as a sign to not make the notation scoped, or whether the solution is just to `open scoped ContDiff` in these files or not use the notation there.
[](https://gitpod.io/from-referrer/)
|
t-differential-geometry
t-analysis
awaiting-author
awaiting-zulip
merge-conflict
|
221/218 |
Mathlib/Analysis/Calculus/BumpFunction/FiniteDimension.lean,Mathlib/Analysis/Calculus/ContDiff/Basic.lean,Mathlib/Analysis/Calculus/ContDiff/Bounds.lean,Mathlib/Analysis/Calculus/ContDiff/CPolynomial.lean,Mathlib/Analysis/Calculus/ContDiff/Comp.lean,Mathlib/Analysis/Calculus/ContDiff/Defs.lean,Mathlib/Analysis/Calculus/ContDiff/Deriv.lean,Mathlib/Analysis/Calculus/ContDiff/FTaylorSeries.lean,Mathlib/Analysis/Calculus/ContDiff/Operations.lean,Mathlib/Analysis/Calculus/FDeriv/Symmetric.lean,Mathlib/Analysis/Calculus/ImplicitContDiff.lean,Mathlib/Analysis/Calculus/IteratedDeriv/Defs.lean,Mathlib/Analysis/Calculus/VectorField.lean,Mathlib/Analysis/Distribution/ContDiffMapSupportedIn.lean,Mathlib/Analysis/SpecialFunctions/Log/Deriv.lean,Mathlib/Analysis/SpecialFunctions/Trigonometric/InverseDeriv.lean,Mathlib/Geometry/Manifold/Algebra/LieGroup.lean,Mathlib/Geometry/Manifold/Algebra/Monoid.lean,Mathlib/Geometry/Manifold/Algebra/SmoothFunctions.lean,Mathlib/Geometry/Manifold/Algebra/Structures.lean,Mathlib/Geometry/Manifold/ContMDiff/Atlas.lean,Mathlib/Geometry/Manifold/ContMDiff/Basic.lean,Mathlib/Geometry/Manifold/ContMDiff/Defs.lean,Mathlib/Geometry/Manifold/Instances/Sphere.lean,Mathlib/Geometry/Manifold/Instances/UnitsOfNormedAlgebra.lean,Mathlib/Geometry/Manifold/IsManifold/Basic.lean,Mathlib/Geometry/Manifold/VectorBundle/Basic.lean,Mathlib/Geometry/Manifold/VectorBundle/FiberwiseLinear.lean |
28 |
5 |
['github-actions', 'j-loreaux', 'mathlib-merge-conflicts', 'peabrainiac'] |
sgouezel assignee:sgouezel |
35-85796 1 month ago |
54-74037 54 days ago |
8-6287 8 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
awaiting-zulip
|
82/4 |
Mathlib/Analysis/Real/Cardinality.lean,Mathlib/Data/Set/Countable.lean,Mathlib/SetTheory/Cardinal/Basic.lean |
3 |
17 |
['github-actions', 'joneugster', 'staroperator', 'vihdzp'] |
joneugster assignee:joneugster |
31-32071 1 month ago |
62-5318 62 days ago |
12-21154 12 days |
| 35524 |
grunweg author:grunweg |
feat: text-based linter against \t followed by tactic mode |
Wait for the zulip discussion to converge. **If** there is consensus in favour of this change, summarise the motivation here.
[zulip discuss](https://leanprover.zulipchat.com/#narrow/channel/345428-mathlib-reviewers/topic/proposal.3A.20no.20more.20use.20of.20.60.E2.96.B8.60.20in.20Mathlib.3F/with/574680826)
---
There are currently 80 remaining exceptions in mathlib: ideally, these would get fixed before merging this.
Works best when combined with #35523.
[](https://gitpod.io/from-referrer/)
|
t-linter
awaiting-zulip
merge-conflict
|
23/2 |
Mathlib/Tactic/Linter/TextBased.lean |
1 |
5 |
['github-actions', 'grunweg', 'joneugster', 'mathlib-merge-conflicts', 'vihdzp'] |
nobody |
19-71609 19 days ago |
46-32771 46 days ago |
0-187 3 minutes |
| 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'] |
nobody |
19-6604 19 days ago |
105-5795 105 days ago |
10-66980 10 days |
| 36890 |
vihdzp author:vihdzp |
chore(SetTheory): `le_mul_left` → `le_mul_of_pos_left` |
The new theorem names/statements match [`Nat.le_mul_of_pos_left`](https://leanprover-community.github.io/mathlib4_docs/Init/Data/Nat/Lemmas.html#Nat.le_mul_of_pos_left). The cardinal one has also been moved to an earlier file.
---
[](https://gitpod.io/from-referrer/)
|
t-set-theory
awaiting-zulip
merge-conflict
|
28/23 |
Mathlib/SetTheory/Cardinal/Arithmetic.lean,Mathlib/SetTheory/Cardinal/Basic.lean,Mathlib/SetTheory/Cardinal/Free.lean,Mathlib/SetTheory/Ordinal/Arithmetic.lean,Mathlib/SetTheory/Ordinal/Exponential.lean,Mathlib/SetTheory/Ordinal/Notation.lean |
6 |
2 |
['github-actions', 'mathlib-merge-conflicts'] |
nobody |
14-44013 14 days ago |
17-30753 17 days ago |
0-10825 3 hours |
| 34077 |
kbuzzard author:kbuzzard |
perf: increase priority of instSMulOfMul |
#31040 deprecated `Mul.toSMul` in place of the core instance `instSMulOfMul`, which is at a lowered priority of 910. This PR undeprecates it and makes it a higher priority instance (1100) which seems better for mathlib.
---
[](https://gitpod.io/from-referrer/)
This PR follows the philosophy seen in Mathlib's `Algebra.id : Algebra R R`, which also has raised priority. The idea is the same as `Algebra.id`: if you're looking for an instance of `Algebra R S` with R not equal to S then `Algebra.id` is extremely likely to fail quickly in practice, and if you're looking for an instance of `Algebra R R` then `Algebra.id` is unambiguously the right answer so should be tried ASAP. However the instance is defined so early in mathlib that in in practice it is tried last unless the priority is raised. The same philosophy holds here; if you're looking for an instance of `SMul X X` then you absolutely want to try `Mul.toSMul` first and if you're looking for an instance of `SMul X Y` with Y not X then `Mul.toSMul` will in practice be quick to fail.
This PR was inspired by #33908 (another "this should be quick to fail and if it fits then it's almost certainly what we want" prio change) which made an instance of `IsScalarTower R A A` high priority and gave a performance boost. This PR also gives a performance boost.
Note that the performance in #31040 looks very bad but the radar output is incorrect; there was a hardware change between the two runs. In fact #31040 produced no changes in profiling, as one might expect.
I don't know the correct way to change the priority of a core instance in mathlib, and I didn't know if just changing the priority naively would work repo-wide rather than just file-wide, which was why this PR introduces a second instance.
Zulip discussion at [#mathlib4 > priority hacks](https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/priority.20hacks/with/574353616)
|
t-algebra
awaiting-zulip
label:t-algebra$ |
3/9 |
Mathlib/Algebra/Group/Action/Defs.lean,Mathlib/Algebra/Group/Action/Units.lean |
2 |
26 |
['alreadydone', 'github-actions', 'kbuzzard', 'leanprover-radar', 'mathlib-merge-conflicts'] |
jcommelin assignee:jcommelin |
10-73702 10 days ago |
47-40797 47 days ago |
0-58585 16 hours |
| 35578 |
Shreyas4991 author:Shreyas4991 |
fix: writer monad should use an additive logging type |
The Writer monad's w type is supposed to be additive, not multiplicative. This is how it is conceptually used in Haskell (as a logging type). Haskell uses `Monoid` because it doesn't make a distinction between `AddMonoid` and `Monoid`.
[#mathlib4 > Writer should use an additive monoid @ 💬](https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/Writer.20should.20use.20an.20additive.20monoid/near/574990415)
---
[](https://gitpod.io/from-referrer/)
|
t-data
awaiting-zulip
merge-conflict
|
10/10 |
Mathlib/Control/Monad/Cont.lean,Mathlib/Control/Monad/Writer.lean |
2 |
5 |
['Shreyas4991', 'eric-wieser', 'github-actions', 'mathlib-merge-conflicts'] |
nobody |
10-54488 10 days ago |
44-75006 44 days ago |
0-18707 5 hours |
| 36401 |
JovanGerb author:JovanGerb |
feat(positivity): positivity extension for `a - b` |
This PR adds support in `positivity` for proving things about subtraction. For example, if the goal is `0 < a - b`, and there is a local hypothesis of type `b < a`, then we close the goal.
The motivation is that we want `positivity` to be a flexible tactic. So, when trying to prove `0 < a - b` using a local hypothesis, we should look for the simp normal form of this, which is `b < a`.
---
[Zulip discussion](https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/Can.20I.20make.20positivity.20work.20for.20this.3F/near/578277240)
[](https://gitpod.io/from-referrer/)
|
t-meta
awaiting-zulip
|
63/26 |
Mathlib/Analysis/Calculus/Taylor.lean,Mathlib/Analysis/Complex/AbelLimit.lean,Mathlib/Analysis/Complex/BorelCaratheodory.lean,Mathlib/Analysis/Complex/Hadamard.lean,Mathlib/Analysis/Convex/BetweenList.lean,Mathlib/Analysis/SpecialFunctions/Log/Deriv.lean,Mathlib/Analysis/SpecificLimits/FloorPow.lean,Mathlib/Geometry/Manifold/Riemannian/PathELength.lean,Mathlib/Tactic/Positivity/Basic.lean,MathlibTest/positivity.lean |
10 |
8 |
['JovanGerb', 'github-actions', 'hrmacbeth', 'j-loreaux', 'joneugster', 'leanprover-radar'] |
joneugster assignee:joneugster |
10-2498 10 days ago |
10-16306 10 days ago |
17-57303 17 days |
| 36087 |
matthewjasper author:matthewjasper |
chore: fix diamonds for Real/Complex Algebra instances |
Unfold or make `implicit_reducible` some definitions used to define `Algebra ℝ ℂ` . This should allow reducing use of `set_option backward.isDefEq.respectTransparency false`.
---
- [x] depends on: #36694
[](https://gitpod.io/from-referrer/)
|
awaiting-zulip |
24/19 |
Mathlib/Algebra/Algebra/Defs.lean,Mathlib/Algebra/Algebra/Pi.lean,Mathlib/Algebra/Algebra/Prod.lean,Mathlib/Analysis/Complex/Basic.lean,Mathlib/Data/Complex/Basic.lean,Mathlib/LinearAlgebra/Complex/Module.lean,MathlibTest/instance_diamonds.lean |
7 |
8 |
['eric-wieser', 'github-actions', 'mathlib-dependent-issues', 'mathlib-merge-conflicts', 'matthewjasper'] |
eric-wieser assignee:eric-wieser |
7-74808 7 days ago |
9-3764 9 days ago |
11-84307 11 days |
| 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`.
[](https://gitpod.io/from-referrer/)
|
t-data
awaiting-author
awaiting-zulip
|
162/0 |
Mathlib/Data/Quot.lean,Mathlib/Data/Set/Image.lean,Mathlib/Data/SetLike/Basic.lean,Mathlib/Data/Setoid/Basic.lean |
4 |
7 |
['SnirBroshi', 'TwoFX', 'eric-wieser', 'github-actions', 'linesthatinterlace', 'mathlib-merge-conflicts'] |
TwoFX assignee:TwoFX |
7-5527 7 days ago |
130-39398 130 days ago |
35-84279 35 days |