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 |
| 24816 |
ciskiko author:ciskiko |
feat(GroupTheory): add Regular Wreath Product |
feat: add regular wreath product and some results; add iterated wreath product; add the isomorphism of iterated wreath product of Z_p to sylow p subgroup of S_{p^n}.
Needs some work simplifying final result.
---
[](https://gitpod.io/from-referrer/)
|
maintainer-merge
new-contributor
t-algebra
label:t-algebra$ |
285/1 |
Mathlib.lean,Mathlib/Algebra/Group/End.lean,Mathlib/Combinatorics/Additive/AP/Three/Behrend.lean,Mathlib/Data/Nat/Multiplicity.lean,Mathlib/GroupTheory/RegularWreathProduct.lean,Mathlib/Logic/Equiv/Fin/Basic.lean,Mathlib/SetTheory/Cardinal/Finite.lean |
7 |
102 |
['ciskiko', 'github-actions', 'tb65536'] |
tb65536 assignee:tb65536 |
18-54249 18 days ago |
18-54250 18 days ago |
27-58846 27 days |
| 25236 |
adomani author:adomani |
feat: the empty line in commands linter |
This linter flags empty lines within a command.
It allows empty lines within doc-strings, module-docs and a couple of other "sensible" places.
It also skips files that are likely to contain meta-code, since there the use of empty lines in definition is more widespread.
---
[](https://gitpod.io/from-referrer/)
|
large-import
t-linter
maintainer-merge
|
373/11 |
Archive/Wiedijk100Theorems/BuffonsNeedle.lean,Mathlib.lean,Mathlib/CategoryTheory/Limits/Shapes/NormalMono/Equalizers.lean,Mathlib/Init.lean,Mathlib/Tactic.lean,Mathlib/Tactic/Linter/EmptyLine.lean,MathlibTest/EmptyLine.lean |
7 |
23 |
['adomani', 'bryangingechen', 'github-actions', 'grunweg', 'leanprover-community-bot-assistant'] |
nobody |
8-59861 8 days ago |
9-44441 9 days ago |
16-41648 16 days |
| 24465 |
adomani author:adomani |
feat: a linter to enforce formatting |
This linter enforces that the hypotheses of every declaration are correctly formatted.
This already required multiple PRs to make mathlib compliant. Ideally, little by little the linter can be extended to format more of mathlib.
---
The default linter option is `false`, but the lakefile enforces it to be `true`.
This means that the linter does not run on `MathlibTest`. However, the tests should still be compliant, since the default option was `true` in development and the tests were fixed.
[](https://gitpod.io/from-referrer/)
|
large-import
t-linter
maintainer-merge
|
876/4 |
Mathlib.lean,Mathlib/Algebra/Group/Int/Defs.lean,Mathlib/Algebra/Group/Nat/Defs.lean,Mathlib/Algebra/Ring/Int/Defs.lean,Mathlib/Data/FunLike/Basic.lean,Mathlib/Data/SetLike/Basic.lean,Mathlib/Init.lean,Mathlib/Tactic.lean,Mathlib/Tactic/Linter/CommandStart.lean,Mathlib/Tactic/Simps/NotationClass.lean,MathlibTest/CommandStart.lean,MathlibTest/EuclideanSpace.lean,MathlibTest/Simps.lean,MathlibTest/Traversable.lean,MathlibTest/antidiagonal.lean,MathlibTest/delabLinearIndependent.lean,MathlibTest/matrix.lean,MathlibTest/norm_num.lean,MathlibTest/set_like.lean,MathlibTest/vec_notation.lean |
20 |
89 |
['Parcly-Taxel', 'adomani', 'eric-wieser', 'github-actions', 'grunweg', 'leanprover-community-bot-assistant'] |
grunweg assignee:grunweg |
7-51508 7 days ago |
30-63201 30 days ago* |
43-67922 43 days* |
| 25265 |
FMLJohn author:FMLJohn |
feat(Order/SupClosed): `compl_image_latticeClosure` and `compl_image_latticeClosure_eq_of_compl_image_eq_self` |
The main results in this pull request are:
1. `compl_image_latticeClosure`: given any Boolean algebra `α` and `s : Set α`, `compl '' latticeClosure s` is the same as `latticeClosure (compl '' s)`;
2. `compl_image_latticeClosure_eq_of_compl_image_eq_self`: given any Boolean algebra `α` and `s : Set α` such that `compl '' s = s`, we have `compl '' latticeClosure s = latticeClosure s`.
---
[](https://gitpod.io/from-referrer/) |
maintainer-merge
t-order
|
59/1 |
Mathlib/Order/SupClosed.lean |
1 |
8 |
['FMLJohn', 'YaelDillies', 'github-actions'] |
bryangingechen assignee:bryangingechen |
7-42968 7 days ago |
10-22940 10 days ago |
14-32559 14 days |
| 25172 |
eric-wieser author:eric-wieser |
feat: restricting `Affine.Simplex` to an affine subspace that contains it |
Also removes a redundant `Nonempty` argument.
---
[](https://gitpod.io/from-referrer/)
|
maintainer-merge
t-euclidean-geometry
|
68/5 |
Mathlib/LinearAlgebra/AffineSpace/AffineSubspace/Basic.lean,Mathlib/LinearAlgebra/AffineSpace/Independent.lean |
2 |
10 |
['eric-wieser', 'github-actions', 'jsm28', 'ocfnash'] |
nobody |
7-37011 7 days ago |
18-46990 18 days ago |
19-1463 19 days |
| 25059 |
s235282 author:s235282 |
feat(Combinatorics/SimpleGraph/Bipartite): a graph is 2-colorable iff it's bipartite |
Define a predicate for a simple graph to be bipartite (`def IsBipartite (G : SimpleGraph V) : Prop := G.Colorable 2`) and prove ` G.IsBipartite ↔ ∃ s t : Set V, G.IsBipartiteWith s t`.
---
This is my first attempt at contributing to mathlib and therefore I have a couple of points of uncertainty related to:
- Naming conventions for theorems - Seeing a lot of isBipartite vs IsBipartite in the original work. What do we want to go with when?
- Definition placement - Where should I put the IsBipartite definition.
- Structure of biimplication theorems - Should I combine the different lemmas into 1 bgi theorem?
Feedback is greatly appreciated :)
[](https://gitpod.io/from-referrer/)
|
large-import
maintainer-merge
new-contributor
t-combinatorics
|
36/3 |
Mathlib/Combinatorics/SimpleGraph/Bipartite.lean |
1 |
30 |
['YaelDillies', 'github-actions', 'mitchell-horner', 's235282'] |
nobody |
5-57274 5 days ago |
5-57821 5 days ago |
12-18851 12 days |
| 25089 |
Bergschaf author:Bergschaf |
feat(Order/Sublocale): definition of sublocales |
There are several possible definition of sublocales. I used one from [nlab](https://ncatlab.org/nlab/show/sublocale) which states that a sublocale is a subset of a locale which is closed under all meets and for any ∈ S and x ∈ X, we have x ⇨ s ∈ S.
This PR also includes an order isomorphism between (Nucleus)ᵒᵈ and Sublocale.
---
I am open to better name suggestions for the order isomorphism.
- [x] depends on: #24941
[](https://gitpod.io/from-referrer/)
|
maintainer-merge
t-order
|
265/8 |
Mathlib.lean,Mathlib/Order/Hom/Lattice.lean,Mathlib/Order/Nucleus.lean,Mathlib/Order/Sublocale.lean,Mathlib/Order/Synonym.lean,docs/references.bib |
6 |
71 |
['Bergschaf', 'YaelDillies', 'github-actions', 'leanprover-community-bot-assistant', 'mathlib4-dependent-issues-bot', 'xhalo32'] |
nobody |
5-21774 5 days ago |
5-21774 5 days ago |
19-1197 19 days |
| 25563 |
Komyyy author:Komyyy |
chore: move `Topology.StoneCech` into `Topology.Compactification` (1/2) |
At present, the `Topology.Compactification` directory includes results on one-point compactifications, but results on Stone-Čech compactifications are currently located elsewhere.
The removed file `Topology.Compactification` is deprecated in another PR (#25583) to leave a good git diff history.
---
[](https://gitpod.io/from-referrer/)
|
file-removed
maintainer-merge
t-topology
|
9/9 |
Mathlib.lean,Mathlib/Combinatorics/Hindman.lean,Mathlib/Topology/Category/CompHaus/Basic.lean,Mathlib/Topology/Category/CompHaus/Projective.lean,Mathlib/Topology/Category/Profinite/Projective.lean,Mathlib/Topology/Category/Stonean/Adjunctions.lean,Mathlib/Topology/Compactification/StoneCech.lean,Mathlib/Topology/ExtremallyDisconnected.lean,Mathlib/Topology/Maps/Proper/UniversallyClosed.lean,Mathlib/Topology/Separation/CompletelyRegular.lean |
10 |
4 |
['Komyyy', 'github-actions', 'grunweg'] |
nobody |
4-62930 4 days ago |
4-62930 4 days ago |
5-38463 5 days |
| 24382 |
joelriou author:joelriou |
feat(CategoryTheory): pseudofunctors from strict bicategories |
This PR provides an API for pseudofunctors `F` from a strict bicategory `B`. In particular, this shall apply to pseudofunctors from locally discrete bicategories.
We first introduce more flexible variants of `mapId` and `mapComp`: for example, if `f` and `g` are composable morphisms and `fg` is such that `h : fg = f ≫ f`, we provide an isomorphism `F.mapComp' f g fg h : F.map fg ≅ F.map f ≫ F.map g`. We study the compatibilities of these isomorphisms with respect to composition with identities and associativity.
Secondly, given a commutative square `t ≫ r = l ≫ b` in `B`, we construct an isomorphism `F.map t ≫ F.map r ≅ F.map l ≫ F.map b`.
Co-authored-by: Christian Merten
---
[](https://gitpod.io/from-referrer/)
|
maintainer-merge
t-category-theory
|
168/0 |
Mathlib.lean,Mathlib/CategoryTheory/Bicategory/Functor/Pseudofunctor.lean,Mathlib/CategoryTheory/Bicategory/Functor/Strict.lean |
3 |
17 |
['callesonne', 'erdOne', 'github-actions', 'joelriou'] |
nobody |
4-33376 4 days ago |
5-12760 5 days ago |
47-26730 47 days |
| 25600 |
Komyyy author:Komyyy |
refactor: lemma expressing `ContinuousAt` using a punctured neighbourhood |
---
This lemma is used to prove that the Riemann zeta function is meromorphic in #25597.
[](https://gitpod.io/from-referrer/)
|
maintainer-merge
t-topology
|
4/0 |
Mathlib/Topology/ContinuousOn.lean |
1 |
5 |
['Komyyy', 'github-actions', 'grunweg'] |
nobody |
4-13647 4 days ago |
4-13647 4 days ago |
4-25535 4 days |
| 24669 |
qawbecrdtey author:qawbecrdtey |
feat(Analysis/Normed/Operator/LinearIsometry): added definition `LinearIsometryEquiv.prodComm` |
---
[](https://gitpod.io/from-referrer/)
This commit defines a `LinearIsometryEquiv`, and states some trivial theorems about it.
```lean
def prodComm [Module R E₂] : E × E₂ ≃ₗᵢ[R] E₂ × E
```
|
maintainer-merge
t-analysis
awaiting-author
|
8/1 |
Mathlib/Analysis/Normed/Operator/LinearIsometry.lean |
1 |
10 |
['Ruben-VandeVelde', 'eric-wieser', 'faenuccio', 'github-actions', 'j-loreaux', 'jcommelin', 'qawbecrdtey'] |
faenuccio assignee:faenuccio |
2-75432 2 days ago |
2-75432 2 days ago |
32-83569 32 days |
| 23849 |
chrisflav author:chrisflav |
feat(Data/Set): add `Set.encard_iUnion` |
---
[](https://gitpod.io/from-referrer/)
|
large-import
t-data
maintainer-merge
|
69/0 |
Mathlib/Algebra/BigOperators/Finprod.lean,Mathlib/Data/Set/Card/Arithmetic.lean,Mathlib/Data/Set/Finite/Lattice.lean |
3 |
25 |
['YaelDillies', 'chrisflav', 'github-actions'] |
YaelDillies assignee:YaelDillies |
2-51495 2 days ago |
2-51495 2 days ago |
64-65286 64 days |
| 21751 |
vihdzp author:vihdzp |
refactor(SetTheory/Ordinal/Arithmetic): rework `Ordinal.pred` API |
This PR does the following:
- give a simpler definition of `Ordinal.pred`
- replace `¬ ∃ a, o = succ a` and `∀ a, o ≠ succ a` by `IsSuccPrelimit o` throughout
- improve theorem names
---
There's a legitimate question of whether we even want `Ordinal.pred` (see [Zulip](https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/Ordinal.2Epred)) but this should be a good change in the meanwhile regardless.
[](https://gitpod.io/from-referrer/)
|
t-set-theory
maintainer-merge
merge-conflict
|
102/67 |
Mathlib/SetTheory/Ordinal/Arithmetic.lean,Mathlib/SetTheory/Ordinal/Exponential.lean |
2 |
13 |
['YaelDillies', 'github-actions', 'grunweg', 'vihdzp'] |
nobody |
37-14217 1 month ago |
83-79244 2 months ago |
36-50134 36 days |
| 24965 |
erdOne author:erdOne |
refactor: Make `IsLocalHom` take unbundled map |
---
[](https://gitpod.io/from-referrer/)
|
maintainer-merge
t-algebra
merge-conflict
awaiting-author
label:t-algebra$ |
16/7 |
Mathlib/Algebra/Group/Units/Hom.lean,Mathlib/AlgebraicGeometry/Scheme.lean,Mathlib/Geometry/RingedSpace/LocallyRingedSpace.lean,Mathlib/Geometry/RingedSpace/LocallyRingedSpace/HasColimits.lean,Mathlib/Geometry/RingedSpace/OpenImmersion.lean |
5 |
6 |
['alreadydone', 'erdOne', 'eric-wieser', 'github-actions', 'leanprover-community-bot-assistant'] |
nobody |
9-83585 9 days ago |
9-83586 9 days ago |
10-26015 10 days |
| 23961 |
FR-vdash-bot author:FR-vdash-bot |
refactor: unbundle algebra from `ENormed*` |
Further speed up the search in the algebraic typeclass hierarchy by avoiding searching for `TopologicalSpace`.
---
[](https://gitpod.io/from-referrer/)
|
slow-typeclass-synthesis
maintainer-merge
t-algebra
t-analysis
merge-conflict
awaiting-author
label:t-algebra$ |
32/25 |
Mathlib/Analysis/CStarAlgebra/CStarMatrix.lean,Mathlib/Analysis/Normed/Group/Basic.lean,Mathlib/Analysis/Normed/Group/Continuity.lean,Mathlib/Analysis/NormedSpace/IndicatorFunction.lean,Mathlib/MeasureTheory/Function/LpSeminorm/Basic.lean |
5 |
12 |
['FR-vdash-bot', 'github-actions', 'grunweg', 'jcommelin', 'leanprover-bot', 'leanprover-community-bot-assistant'] |
nobody |
5-67803 5 days ago |
5-67803 5 days ago |
17-72244 17 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 |
| 24816 |
ciskiko author:ciskiko |
feat(GroupTheory): add Regular Wreath Product |
feat: add regular wreath product and some results; add iterated wreath product; add the isomorphism of iterated wreath product of Z_p to sylow p subgroup of S_{p^n}.
Needs some work simplifying final result.
---
[](https://gitpod.io/from-referrer/)
|
maintainer-merge
new-contributor
t-algebra
label:t-algebra$ |
285/1 |
Mathlib.lean,Mathlib/Algebra/Group/End.lean,Mathlib/Combinatorics/Additive/AP/Three/Behrend.lean,Mathlib/Data/Nat/Multiplicity.lean,Mathlib/GroupTheory/RegularWreathProduct.lean,Mathlib/Logic/Equiv/Fin/Basic.lean,Mathlib/SetTheory/Cardinal/Finite.lean |
7 |
102 |
['ciskiko', 'github-actions', 'tb65536'] |
tb65536 assignee:tb65536 |
18-54249 18 days ago |
18-54250 18 days ago |
27-58846 27 days |
| 25236 |
adomani author:adomani |
feat: the empty line in commands linter |
This linter flags empty lines within a command.
It allows empty lines within doc-strings, module-docs and a couple of other "sensible" places.
It also skips files that are likely to contain meta-code, since there the use of empty lines in definition is more widespread.
---
[](https://gitpod.io/from-referrer/)
|
large-import
t-linter
maintainer-merge
|
373/11 |
Archive/Wiedijk100Theorems/BuffonsNeedle.lean,Mathlib.lean,Mathlib/CategoryTheory/Limits/Shapes/NormalMono/Equalizers.lean,Mathlib/Init.lean,Mathlib/Tactic.lean,Mathlib/Tactic/Linter/EmptyLine.lean,MathlibTest/EmptyLine.lean |
7 |
23 |
['adomani', 'bryangingechen', 'github-actions', 'grunweg', 'leanprover-community-bot-assistant'] |
nobody |
8-59861 8 days ago |
9-44441 9 days ago |
16-41648 16 days |
| 24465 |
adomani author:adomani |
feat: a linter to enforce formatting |
This linter enforces that the hypotheses of every declaration are correctly formatted.
This already required multiple PRs to make mathlib compliant. Ideally, little by little the linter can be extended to format more of mathlib.
---
The default linter option is `false`, but the lakefile enforces it to be `true`.
This means that the linter does not run on `MathlibTest`. However, the tests should still be compliant, since the default option was `true` in development and the tests were fixed.
[](https://gitpod.io/from-referrer/)
|
large-import
t-linter
maintainer-merge
|
876/4 |
Mathlib.lean,Mathlib/Algebra/Group/Int/Defs.lean,Mathlib/Algebra/Group/Nat/Defs.lean,Mathlib/Algebra/Ring/Int/Defs.lean,Mathlib/Data/FunLike/Basic.lean,Mathlib/Data/SetLike/Basic.lean,Mathlib/Init.lean,Mathlib/Tactic.lean,Mathlib/Tactic/Linter/CommandStart.lean,Mathlib/Tactic/Simps/NotationClass.lean,MathlibTest/CommandStart.lean,MathlibTest/EuclideanSpace.lean,MathlibTest/Simps.lean,MathlibTest/Traversable.lean,MathlibTest/antidiagonal.lean,MathlibTest/delabLinearIndependent.lean,MathlibTest/matrix.lean,MathlibTest/norm_num.lean,MathlibTest/set_like.lean,MathlibTest/vec_notation.lean |
20 |
89 |
['Parcly-Taxel', 'adomani', 'eric-wieser', 'github-actions', 'grunweg', 'leanprover-community-bot-assistant'] |
grunweg assignee:grunweg |
7-51508 7 days ago |
30-63201 30 days ago* |
43-67922 43 days* |
| 25265 |
FMLJohn author:FMLJohn |
feat(Order/SupClosed): `compl_image_latticeClosure` and `compl_image_latticeClosure_eq_of_compl_image_eq_self` |
The main results in this pull request are:
1. `compl_image_latticeClosure`: given any Boolean algebra `α` and `s : Set α`, `compl '' latticeClosure s` is the same as `latticeClosure (compl '' s)`;
2. `compl_image_latticeClosure_eq_of_compl_image_eq_self`: given any Boolean algebra `α` and `s : Set α` such that `compl '' s = s`, we have `compl '' latticeClosure s = latticeClosure s`.
---
[](https://gitpod.io/from-referrer/) |
maintainer-merge
t-order
|
59/1 |
Mathlib/Order/SupClosed.lean |
1 |
8 |
['FMLJohn', 'YaelDillies', 'github-actions'] |
bryangingechen assignee:bryangingechen |
7-42968 7 days ago |
10-22940 10 days ago |
14-32559 14 days |
| 25172 |
eric-wieser author:eric-wieser |
feat: restricting `Affine.Simplex` to an affine subspace that contains it |
Also removes a redundant `Nonempty` argument.
---
[](https://gitpod.io/from-referrer/)
|
maintainer-merge
t-euclidean-geometry
|
68/5 |
Mathlib/LinearAlgebra/AffineSpace/AffineSubspace/Basic.lean,Mathlib/LinearAlgebra/AffineSpace/Independent.lean |
2 |
10 |
['eric-wieser', 'github-actions', 'jsm28', 'ocfnash'] |
nobody |
7-37011 7 days ago |
18-46990 18 days ago |
19-1463 19 days |
| 25059 |
s235282 author:s235282 |
feat(Combinatorics/SimpleGraph/Bipartite): a graph is 2-colorable iff it's bipartite |
Define a predicate for a simple graph to be bipartite (`def IsBipartite (G : SimpleGraph V) : Prop := G.Colorable 2`) and prove ` G.IsBipartite ↔ ∃ s t : Set V, G.IsBipartiteWith s t`.
---
This is my first attempt at contributing to mathlib and therefore I have a couple of points of uncertainty related to:
- Naming conventions for theorems - Seeing a lot of isBipartite vs IsBipartite in the original work. What do we want to go with when?
- Definition placement - Where should I put the IsBipartite definition.
- Structure of biimplication theorems - Should I combine the different lemmas into 1 bgi theorem?
Feedback is greatly appreciated :)
[](https://gitpod.io/from-referrer/)
|
large-import
maintainer-merge
new-contributor
t-combinatorics
|
36/3 |
Mathlib/Combinatorics/SimpleGraph/Bipartite.lean |
1 |
30 |
['YaelDillies', 'github-actions', 'mitchell-horner', 's235282'] |
nobody |
5-57274 5 days ago |
5-57821 5 days ago |
12-18851 12 days |
| 25089 |
Bergschaf author:Bergschaf |
feat(Order/Sublocale): definition of sublocales |
There are several possible definition of sublocales. I used one from [nlab](https://ncatlab.org/nlab/show/sublocale) which states that a sublocale is a subset of a locale which is closed under all meets and for any ∈ S and x ∈ X, we have x ⇨ s ∈ S.
This PR also includes an order isomorphism between (Nucleus)ᵒᵈ and Sublocale.
---
I am open to better name suggestions for the order isomorphism.
- [x] depends on: #24941
[](https://gitpod.io/from-referrer/)
|
maintainer-merge
t-order
|
265/8 |
Mathlib.lean,Mathlib/Order/Hom/Lattice.lean,Mathlib/Order/Nucleus.lean,Mathlib/Order/Sublocale.lean,Mathlib/Order/Synonym.lean,docs/references.bib |
6 |
71 |
['Bergschaf', 'YaelDillies', 'github-actions', 'leanprover-community-bot-assistant', 'mathlib4-dependent-issues-bot', 'xhalo32'] |
nobody |
5-21774 5 days ago |
5-21774 5 days ago |
19-1197 19 days |
| 25563 |
Komyyy author:Komyyy |
chore: move `Topology.StoneCech` into `Topology.Compactification` (1/2) |
At present, the `Topology.Compactification` directory includes results on one-point compactifications, but results on Stone-Čech compactifications are currently located elsewhere.
The removed file `Topology.Compactification` is deprecated in another PR (#25583) to leave a good git diff history.
---
[](https://gitpod.io/from-referrer/)
|
file-removed
maintainer-merge
t-topology
|
9/9 |
Mathlib.lean,Mathlib/Combinatorics/Hindman.lean,Mathlib/Topology/Category/CompHaus/Basic.lean,Mathlib/Topology/Category/CompHaus/Projective.lean,Mathlib/Topology/Category/Profinite/Projective.lean,Mathlib/Topology/Category/Stonean/Adjunctions.lean,Mathlib/Topology/Compactification/StoneCech.lean,Mathlib/Topology/ExtremallyDisconnected.lean,Mathlib/Topology/Maps/Proper/UniversallyClosed.lean,Mathlib/Topology/Separation/CompletelyRegular.lean |
10 |
4 |
['Komyyy', 'github-actions', 'grunweg'] |
nobody |
4-62930 4 days ago |
4-62930 4 days ago |
5-38463 5 days |
| 24382 |
joelriou author:joelriou |
feat(CategoryTheory): pseudofunctors from strict bicategories |
This PR provides an API for pseudofunctors `F` from a strict bicategory `B`. In particular, this shall apply to pseudofunctors from locally discrete bicategories.
We first introduce more flexible variants of `mapId` and `mapComp`: for example, if `f` and `g` are composable morphisms and `fg` is such that `h : fg = f ≫ f`, we provide an isomorphism `F.mapComp' f g fg h : F.map fg ≅ F.map f ≫ F.map g`. We study the compatibilities of these isomorphisms with respect to composition with identities and associativity.
Secondly, given a commutative square `t ≫ r = l ≫ b` in `B`, we construct an isomorphism `F.map t ≫ F.map r ≅ F.map l ≫ F.map b`.
Co-authored-by: Christian Merten
---
[](https://gitpod.io/from-referrer/)
|
maintainer-merge
t-category-theory
|
168/0 |
Mathlib.lean,Mathlib/CategoryTheory/Bicategory/Functor/Pseudofunctor.lean,Mathlib/CategoryTheory/Bicategory/Functor/Strict.lean |
3 |
17 |
['callesonne', 'erdOne', 'github-actions', 'joelriou'] |
nobody |
4-33376 4 days ago |
5-12760 5 days ago |
47-26730 47 days |
| 25600 |
Komyyy author:Komyyy |
refactor: lemma expressing `ContinuousAt` using a punctured neighbourhood |
---
This lemma is used to prove that the Riemann zeta function is meromorphic in #25597.
[](https://gitpod.io/from-referrer/)
|
maintainer-merge
t-topology
|
4/0 |
Mathlib/Topology/ContinuousOn.lean |
1 |
5 |
['Komyyy', 'github-actions', 'grunweg'] |
nobody |
4-13647 4 days ago |
4-13647 4 days ago |
4-25535 4 days |
| 24669 |
qawbecrdtey author:qawbecrdtey |
feat(Analysis/Normed/Operator/LinearIsometry): added definition `LinearIsometryEquiv.prodComm` |
---
[](https://gitpod.io/from-referrer/)
This commit defines a `LinearIsometryEquiv`, and states some trivial theorems about it.
```lean
def prodComm [Module R E₂] : E × E₂ ≃ₗᵢ[R] E₂ × E
```
|
maintainer-merge
t-analysis
awaiting-author
|
8/1 |
Mathlib/Analysis/Normed/Operator/LinearIsometry.lean |
1 |
10 |
['Ruben-VandeVelde', 'eric-wieser', 'faenuccio', 'github-actions', 'j-loreaux', 'jcommelin', 'qawbecrdtey'] |
faenuccio assignee:faenuccio |
2-75432 2 days ago |
2-75432 2 days ago |
32-83569 32 days |
| 23849 |
chrisflav author:chrisflav |
feat(Data/Set): add `Set.encard_iUnion` |
---
[](https://gitpod.io/from-referrer/)
|
large-import
t-data
maintainer-merge
|
69/0 |
Mathlib/Algebra/BigOperators/Finprod.lean,Mathlib/Data/Set/Card/Arithmetic.lean,Mathlib/Data/Set/Finite/Lattice.lean |
3 |
25 |
['YaelDillies', 'chrisflav', 'github-actions'] |
YaelDillies assignee:YaelDillies |
2-51495 2 days ago |
2-51495 2 days ago |
64-65286 64 days |
| 25716 |
JovanGerb author:JovanGerb |
feat(gcongr): fix pattern elaborator and @[gcongr] for lemmas introducing binders |
This PR adds @[gcongr] tags so that
- `gcongr` can move inside Eventually and Frequently,
- moving inside of `∀ ε > 0,` or `∃ ε > 0,` adds the hypothesis/condition to the local context.
---
[](https://gitpod.io/from-referrer/)
|
large-import
maintainer-merge
|
57/6 |
Mathlib/Order/Filter/Basic.lean,Mathlib/Tactic/GCongr/Core.lean,Mathlib/Tactic/GCongr/CoreAttrs.lean,MathlibTest/GCongr/inequalities.lean,MathlibTest/peel.lean |
5 |
6 |
['JovanGerb', 'github-actions', 'grunweg'] |
nobody |
0-62419 17 hours ago |
0-69032 19 hours ago |
1-10601 1 day |
| 25144 |
wwylele author:wwylele |
feat(Algebra/Order): add Archimedean class |
This is the first of PRs for Hahn embedding theorem #25140
---
[](https://gitpod.io/from-referrer/)
|
maintainer-merge
t-order
t-algebra
label:t-algebra$ |
424/0 |
Mathlib.lean,Mathlib/Algebra/Order/Archimedean/Class.lean,Mathlib/Algebra/Order/Group/Unbundled/Abs.lean |
3 |
85 |
['YaelDillies', 'eric-wieser', 'github-actions', 'wwylele'] |
nobody |
0-46320 12 hours ago |
0-59573 16 hours ago |
19-22404 19 days |
| 25785 |
Parcly-Taxel author:Parcly-Taxel |
feat: IMO 2001 Q3 |
|
IMO
maintainer-merge
|
111/0 |
Archive.lean,Archive/Imo/Imo2001Q3.lean |
2 |
3 |
['dwrensha', 'github-actions'] |
nobody |
0-23415 6 hours ago |
0-23415 6 hours ago |
0-0 0 seconds |
| 25062 |
erdOne author:erdOne |
feat(Algebra/MvPolynomial): nilpotents and units |
---
[](https://gitpod.io/from-referrer/)
|
maintainer-merge
t-algebra
label:t-algebra$ |
113/0 |
Mathlib.lean,Mathlib/Algebra/MvPolynomial/Nilpotent.lean,Mathlib/Data/Finsupp/Basic.lean |
3 |
9 |
['alreadydone', 'erdOne', 'eric-wieser', 'github-actions'] |
nobody |
0-22234 6 hours ago |
0-22234 6 hours ago |
23-4527 23 days |
| 25255 |
Raph-DG author:Raph-DG |
feat(RingTheory): Order of vanishing in a ring |
In this PR we define the order of vanishing of a ring and its extension to elements of the function field (as in stacks project 02MD) as well as some basic API.
---
Note that I'm slightly unsure that some of the lemmas used to prove this are at the right level of generality, and further I'm not quite sure where some of these lemmas belong (as indicated by the comments in the main OrderOfVanishing.lean file). Any comments about this would be very much appreciated.
[](https://gitpod.io/from-referrer/)
|
maintainer-merge
new-contributor
t-algebra
RFC
label:t-algebra$ |
247/0 |
Mathlib.lean,Mathlib/Algebra/Order/Monoid/Unbundled/WithTop.lean,Mathlib/RingTheory/Artinian/Module.lean,Mathlib/RingTheory/Ideal/Operations.lean,Mathlib/RingTheory/Ideal/Quotient/Operations.lean,Mathlib/RingTheory/OrderOfVanishing.lean |
6 |
84 |
['Raph-DG', 'chrisflav', 'erdOne', 'github-actions', 'jcommelin', 'riccardobrasca'] |
nobody |
0-12257 3 hours ago |
7-16428 7 days ago |
13-82211 13 days |
| 25820 |
euprunin author:euprunin |
chore: rename test of `Mathlib.Tactic.ClearExclamation` (from `Clear!.lean` to `ClearExclamation.lean`) |
Some context:
* filename Clear!.lean contains illegal character "!" (#1212)
* chore(Mathlib/Tactic/Clear!): rename `Clear!.lean` to `ClearExclamation.lean` to avoid the illegal character `!` (#12757)
This PR renames `MathlibTest/Clear!.lean` to `MathlibTest/ClearExclamation.lean` to avoid shell quoting issues caused by the `!` character in file names.
For example:
```
% ls -l MathlibTest/Clear!.lean
zsh: event not found: .lean
% ls -l "MathlibTest/Clear!.lean"
zsh: event not found: .lean
```
See issue #1212 for some additional context.
---
[](https://gitpod.io/from-referrer/)
|
file-removed
maintainer-merge
|
0/0 |
MathlibTest/ClearExclamation.lean |
1 |
3 |
['github-actions', 'grunweg'] |
nobody |
0-12054 3 hours ago |
0-12054 3 hours ago |
0-0 0 seconds |
| 25817 |
Vierkantor author:Vierkantor |
cache: change working directory when running the post-update hook |
`lake exe cache` expects to run in the root package directory that includes the lakefile and `.lake` folder. The Lake update hook isn't always run from that position (for example if it is run as part of a more complicated Lake command), so change directories when calling into the executable.
The assumption that the command is run from the working directory is so pervasive that we'd need to touch a lot of Cache in order to get rid of it. I think it's better to accept this as a design decision.
---
[](https://gitpod.io/from-referrer/)
|
maintainer-merge |
8/1 |
lakefile.lean |
1 |
3 |
['github-actions', 'grunweg'] |
nobody |
0-11987 3 hours ago |
0-11987 3 hours ago |
0-0 0 seconds |
| 25811 |
plp127 author:plp127 |
fix(Tactic/DeprecateTo): get date from Lean |
Fixes an issue I encountered on windows where `IO.Process.run { cmd := "date", args := #["-I"] }` exits with an error `no such file or directory (error code: 2)`, making this tactic unusable.
---
[](https://gitpod.io/from-referrer/)
|
large-import
maintainer-merge
t-meta
|
7/3 |
Mathlib/Tactic/DeprecateTo.lean |
1 |
3 |
['github-actions', 'grunweg'] |
nobody |
0-11892 3 hours ago |
0-11892 3 hours ago |
0-0 0 seconds |
| 21751 |
vihdzp author:vihdzp |
refactor(SetTheory/Ordinal/Arithmetic): rework `Ordinal.pred` API |
This PR does the following:
- give a simpler definition of `Ordinal.pred`
- replace `¬ ∃ a, o = succ a` and `∀ a, o ≠ succ a` by `IsSuccPrelimit o` throughout
- improve theorem names
---
There's a legitimate question of whether we even want `Ordinal.pred` (see [Zulip](https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/Ordinal.2Epred)) but this should be a good change in the meanwhile regardless.
[](https://gitpod.io/from-referrer/)
|
t-set-theory
maintainer-merge
merge-conflict
|
102/67 |
Mathlib/SetTheory/Ordinal/Arithmetic.lean,Mathlib/SetTheory/Ordinal/Exponential.lean |
2 |
13 |
['YaelDillies', 'github-actions', 'grunweg', 'vihdzp'] |
nobody |
37-14217 1 month ago |
83-79244 2 months ago |
36-50134 36 days |
| 24965 |
erdOne author:erdOne |
refactor: Make `IsLocalHom` take unbundled map |
---
[](https://gitpod.io/from-referrer/)
|
maintainer-merge
t-algebra
merge-conflict
awaiting-author
label:t-algebra$ |
16/7 |
Mathlib/Algebra/Group/Units/Hom.lean,Mathlib/AlgebraicGeometry/Scheme.lean,Mathlib/Geometry/RingedSpace/LocallyRingedSpace.lean,Mathlib/Geometry/RingedSpace/LocallyRingedSpace/HasColimits.lean,Mathlib/Geometry/RingedSpace/OpenImmersion.lean |
5 |
6 |
['alreadydone', 'erdOne', 'eric-wieser', 'github-actions', 'leanprover-community-bot-assistant'] |
nobody |
9-83585 9 days ago |
9-83586 9 days ago |
10-26015 10 days |
| 23961 |
FR-vdash-bot author:FR-vdash-bot |
refactor: unbundle algebra from `ENormed*` |
Further speed up the search in the algebraic typeclass hierarchy by avoiding searching for `TopologicalSpace`.
---
[](https://gitpod.io/from-referrer/)
|
slow-typeclass-synthesis
maintainer-merge
t-algebra
t-analysis
merge-conflict
awaiting-author
label:t-algebra$ |
32/25 |
Mathlib/Analysis/CStarAlgebra/CStarMatrix.lean,Mathlib/Analysis/Normed/Group/Basic.lean,Mathlib/Analysis/Normed/Group/Continuity.lean,Mathlib/Analysis/NormedSpace/IndicatorFunction.lean,Mathlib/MeasureTheory/Function/LpSeminorm/Basic.lean |
5 |
12 |
['FR-vdash-bot', 'github-actions', 'grunweg', 'jcommelin', 'leanprover-bot', 'leanprover-community-bot-assistant'] |
nobody |
5-67803 5 days ago |
5-67803 5 days ago |
17-72244 17 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 |
| 23772 |
SEU-Prime author:SEU-Prime |
Create Amice.lean |
i built amice equiv
[](https://gitpod.io/from-referrer/)
|
t-number-theory
WIP
|
283/0 |
Mathlib/NumberTheory/Padics/Amice.lean |
1 |
2 |
['grunweg'] |
nobody |
66-42413 2 months ago |
66-42413 2 months ago |
0-0 0 seconds |
| 23986 |
ShouxinZhang author:ShouxinZhang |
feat(FieldTheory/RatFunc): add RatFunc.toFractionRingAlgEquiv |
---
[](https://gitpod.io/from-referrer/)
|
will-close-soon
t-algebra
label:t-algebra$ |
17/0 |
Mathlib/FieldTheory/RatFunc/Basic.lean |
1 |
1 |
['joneugster'] |
nobody |
56-15195 1 month ago |
56-15195 1 month ago |
0-0 0 seconds |
| 25680 |
kim-em author:kim-em |
chore: remove some `Nat` shortcut instances |
This PR continues the work from #24928.
Original PR: https://github.com/leanprover-community/mathlib4/pull/24928 |
|
0/9 |
Mathlib/Algebra/Ring/Divisibility/Basic.lean,Mathlib/Data/List/TakeDrop.lean,Mathlib/Data/Nat/Basic.lean |
3 |
5 |
['b-mehta', 'github-actions', 'leanprover-bot', 'mattrobball'] |
nobody |
1-31629 1 day ago |
2-7523 2 days ago |
0-0 0 seconds |
| 25726 |
tb65536 author:tb65536 |
(WIP) Galois group of `x ^ n - x - 1` |
---
[](https://gitpod.io/from-referrer/)
|
large-import
t-algebra
WIP
label:t-algebra$ |
250/145 |
Archive/Wiedijk100Theorems/AbelRuffini.lean,Mathlib/RingTheory/Polynomial/Selmer.lean |
2 |
1 |
['github-actions'] |
nobody |
0-77741 21 hours ago |
0-77748 21 hours ago |
0-0 0 seconds |
| 25730 |
xroblot author:xroblot |
feat(ZLattice/Covolume): add `covolume_div_covolume_eq_relindex` |
Add the following result:
Let `L₁` be a sub-`ℤ`-lattice of `L₂`. Then the index of `L₁` inside `L₂` is equal to `covolume L₁ / covolume L₂`.
---
- [x] depends on: #22940
- [x] depends on: #23759
[](https://gitpod.io/from-referrer/)
---
*This PR continues the work from #22961.*
*Original PR: https://github.com/leanprover-community/mathlib4/pull/22961* |
t-algebra label:t-algebra$ |
66/3 |
Mathlib/Algebra/Module/ZLattice/Basic.lean,Mathlib/Algebra/Module/ZLattice/Covolume.lean,Mathlib/GroupTheory/Index.lean,Mathlib/LinearAlgebra/Determinant.lean |
4 |
2 |
['github-actions', 'mathlib4-dependent-issues-bot'] |
nobody |
0-70239 19 hours ago |
0-71330 19 hours ago |
0-0 0 seconds |
| 25731 |
robin-carlier author:robin-carlier |
feat(CategoryTheory/Monoidal): external product of diagrams in monoidal categories |
Given functors `K₁ : J₁ ⥤ C` and `K₂ : J₂ ⥤ C` with values in a monoidal category, define a construction `externalProduct K₁ K₂` (denoted `K₁ ⊠ K₂`) as the bifunctor `(j₁, j₂) ↦ K₁ j₁ ⊗ K₂ j₂`.
We show that composition of this construction with the diagonal functor to the product recovers the pointwise tensor product of functors, and we show that this construction satisfies a symmetry whenever `C` is braided.
---
[](https://gitpod.io/from-referrer/)
---
*This PR continues the work from #24703.*
*Original PR: https://github.com/leanprover-community/mathlib4/pull/24703* |
t-category-theory |
99/0 |
Mathlib.lean,Mathlib/CategoryTheory/Monoidal/ExternalProduct.lean |
2 |
1 |
['github-actions'] |
nobody |
0-66973 18 hours ago |
0-67047 18 hours ago |
0-0 0 seconds |
| 25732 |
robin-carlier author:robin-carlier |
feat(CategoryTheory/Monoidal/Limits): miscellany about preservation of (co)limits by tensor products |
Register some instances regarding preservations of (co)limits for the tensor product of a monoidal category. More precisely, we register the fact that if the category is braided and `tensorLeft c` preserves colimits (this can be inferred e.g via `MonoidalClosed C`), then so does `tensorRight c` for every `c`.
We also rephrase preservation of (co)limits for `curriedTensor C` in terms of preservations of (co)limits for `tensorRight c`.
The PR introduces also introduces a directory `CategoryTheory.Monoidal.Limits` and moves the existing file `CategoryTheory.Monoidal.Limits.lean` to `CategoryTheory.Monoidal.Limits.Basic`.
---
The instances registered here are tailored so that for a braided monoidal closed category, `PreservesColimit₂` instances from #24685 can be inferred with the results of #24686 for the external product of diagrams defined in #24703
[](https://gitpod.io/from-referrer/)
---
*This PR continues the work from #24711.*
*Original PR: https://github.com/leanprover-community/mathlib4/pull/24711* |
file-removed
t-category-theory
|
72/2 |
Mathlib.lean,Mathlib/CategoryTheory/Monoidal/Internal/Limits.lean,Mathlib/CategoryTheory/Monoidal/Limits/Basic.lean,Mathlib/CategoryTheory/Monoidal/Limits/Preserves.lean |
4 |
1 |
['github-actions'] |
nobody |
0-66796 18 hours ago |
0-66925 18 hours ago |
0-0 0 seconds |
| 25733 |
robin-carlier author:robin-carlier |
feat(CategoryTheory/Limits/Preserves): Preservations of (co)limits by bifunctors |
Introduce a typeclass `PreservesColimit₂` that bundles the assumption that a bifunctor preserves a pair of colimit diagrams in each of its variables. This is stated in terms of a construction `Functor.mapCocone₂` that applies a bifunctor `G` to a pair of cocones to get a cocone over the uncurryfication of `whiskeringLeft₂ _|>.obj _|>.obj _|>.obj G`. The cocone points of this construction is definitionally the evaluation of `G` at the cocone points of the two cocones given as parameters.
We give helper functions to extract isomorphisms with abstract colimits out of this typeclass, and we characterize these isomorphisms with respect to the canonical maps to the colimits.
The dual typeclass for limits is also introduced.
---
The definition of `Functor.mapCocone₂` and of `PreservesColimit₂` is due to @joelriou and was suggested during review of #17781.
This PR only contains basic definitions, but does not give any interesting ways of inferring a `PreservesColimit₂` instance.
This will be the content of a follow-up PR.
This PR continues the work from #24685.
Original PR: https://github.com/leanprover-community/mathlib4/pull/24685 |
t-category-theory |
272/0 |
Mathlib.lean,Mathlib/CategoryTheory/Limits/Preserves/Bifunctor.lean |
2 |
1 |
['github-actions'] |
nobody |
0-65701 18 hours ago |
0-66783 18 hours ago |
0-0 0 seconds |
| 25742 |
robin-carlier author:robin-carlier |
feat(AlgebraicTopology/SimplexCategory): the augmented simplex category |
This PR defines `AugmentedSimplexCategory` as `WithInitial SimplexCategory`. Using the API in `CategoryTheory.WithTerminal`, we check that functors out of this category (resp. out of its opposite) corresponds to cosimplicial (resp. simplicial) objects, and we link various construction about simplicial objects in terms of this category.
---
- [x] depends on : #22658
[](https://gitpod.io/from-referrer/)
---
*This PR continues the work from #22767.*
*Original PR: https://github.com/leanprover-community/mathlib4/pull/22767* |
t-topology
t-category-theory
|
118/0 |
Mathlib.lean,Mathlib/AlgebraicTopology/SimplexCategory/Augmented.lean |
2 |
1 |
['github-actions'] |
nobody |
0-65100 18 hours ago |
0-65100 18 hours ago |
0-0 0 seconds |
| 25738 |
JovanGerb author:JovanGerb |
feat(gcongr): tag lemmas for `Subtype.mk` |
---
[](https://gitpod.io/from-referrer/)
|
|
5/1 |
Mathlib/MeasureTheory/Integral/Lebesgue/Basic.lean,Mathlib/Order/Basic.lean |
2 |
1 |
['github-actions', 'grunweg'] |
nobody |
0-65073 18 hours ago |
0-65681 18 hours ago |
0-0 0 seconds |
| 25745 |
robin-carlier author:robin-carlier |
chore(Category/Theory/Whiskering): tag `[reassoc]` some lemmas about isoWhisker |
Using the extension of `reassoc` to equality of isomorphisms, tags some lemmas in `CategoryTheory.Whiskering` with this new version of the attribute.
---
- [x] depends on: #24303
[](https://gitpod.io/from-referrer/)
---
*This PR continues the work from #24320.*
*Original PR: https://github.com/leanprover-community/mathlib4/pull/24320* |
t-category-theory
easy
|
9/4 |
Mathlib/CategoryTheory/Whiskering.lean |
1 |
2 |
['github-actions', 'mathlib4-dependent-issues-bot'] |
nobody |
0-64196 17 hours ago |
0-64723 17 hours ago |
0-0 0 seconds |
| 25743 |
robin-carlier author:robin-carlier |
feat(AlgebraicTopology/SimplexCategory/Augmented): monoidal structure on `AugmentedSimplexCategory` |
We construct a monoidal category structure on `AugmentedSimplexCategory`. The tensor products corresponds to ordinal sum. We characterize morphisms out of a tensor product of object in terms of their precomposition with canonical maps `x ⟶ x ⊗ y` and `y ⟶ x ⊗ y` coming from the fact that the unit is an initial object.
Finally, we show that `⦋0⦌` admits a canonical internal monoid object structure.
---
- [ ] depends on: #25742
I hope to be able to clear the TODO in `AlgebreaicTopology.SimplexCategory.Augmented.Mon_` in future work, as this should be the "right" statement for the monoidal bar construction, but there is still a long way to go.
[](https://gitpod.io/from-referrer/)
---
*This PR continues the work from #22768.*
*Original PR: https://github.com/leanprover-community/mathlib4/pull/22768* |
t-topology
t-category-theory
blocked-by-other-PR
|
560/0 |
Mathlib.lean,Mathlib/AlgebraicTopology/SimplexCategory/Augmented/Basic.lean,Mathlib/AlgebraicTopology/SimplexCategory/Augmented/Mon_.lean,Mathlib/AlgebraicTopology/SimplexCategory/Augmented/Monoidal.lean,Mathlib/AlgebraicTopology/SimplexCategory/Basic.lean |
5 |
2 |
['github-actions', 'mathlib4-dependent-issues-bot'] |
nobody |
0-64194 17 hours ago |
0-65053 18 hours ago |
0-0 0 seconds |
| 25744 |
robin-carlier author:robin-carlier |
feat(CategoryTheory/Join): Pseudofunctoriality of joins of categories |
Promote the constructions `C ↦ C ⋆ D` and `D ↦ C ⋆ D` to pseudofunctors from `Cat` to `Cat`. The construction is carried in a new file `CategoryTheory/Join/Pseudofunctor.lean` to reduce imports.
---
- [x] depends on: #23412
The pseudofunctoriality statements here are not the most general. The "right" statements would be
1) "pseudobifunctoriality".
2) pseudofunctoriality with values in slice bicategories.
Unfortunately, the two-categorical machinery in mathlib is not advanced enough yet to even make sense of the statements (first would require at least product bicategories, or 2-categories of pseudofunctors for a curried version, second would require slice bicategories.).
The content of this file should be upgraded once said constructions in bicategories are available, but for now I want at least to have statements that recover what we already have for `WithInitial` and `WithTerminal` rather than conditioning everything on a (probably rather long) bicategorical sidequest.
[](https://gitpod.io/from-referrer/)
---
*This PR continues the work from #23413.*
*Original PR: https://github.com/leanprover-community/mathlib4/pull/23413* |
t-category-theory |
169/0 |
Mathlib.lean,Mathlib/CategoryTheory/Join/Basic.lean,Mathlib/CategoryTheory/Join/Pseudofunctor.lean |
3 |
2 |
['github-actions', 'mathlib4-dependent-issues-bot'] |
nobody |
0-64194 17 hours ago |
0-64894 18 hours ago |
0-0 0 seconds |
| 25741 |
robin-carlier author:robin-carlier |
feat(AlgebraicTopology/SimplexCategory/SimplicialObject): definitions of simplicial objects by generators and relation |
We leverage the equivalence between `SimplexCategory` and `SimplexCategoryGenRel` to give new constructors for (co)simplicial objects, as well as constructors for natural transformations (resp. isomorphism) between those.
Final PR in the series of PR formalising the equivalence between `SimplexCategory` and `SimplexCategoryGenRel`.
---
- [ ] depends on: #21747
[](https://gitpod.io/from-referrer/)
---
*This PR continues the work from #21748.*
*Original PR: https://github.com/leanprover-community/mathlib4/pull/21748* |
large-import
t-topology
t-category-theory
|
1363/9 |
Mathlib.lean,Mathlib/AlgebraicTopology/SimplexCategory/GeneratorsRelations/Equivalence.lean,Mathlib/AlgebraicTopology/SimplexCategory/GeneratorsRelations/NormalForms.lean,Mathlib/AlgebraicTopology/SimplicialObject/GeneratorsRelations.lean |
4 |
2 |
['github-actions', 'mathlib4-dependent-issues-bot'] |
nobody |
0-64192 17 hours ago |
0-64193 17 hours ago |
0-0 0 seconds |
| 25740 |
robin-carlier author:robin-carlier |
feat(AlgebraicTopology/SimplexCategory/GeneratorsRelations): `SimplexCategoryGenRel.toSimplexCategory` is an equivalence |
We use the normal forms for morphisms in `SimplexCategoryGenRel` to prove that `SimplexCategoryGenRel.toSimplexCategory` is an equivalence. We prove in order that there exists unique lifts in `SimplexCategoryGenRel` of mono (resp. epis) in `SimplexCategory`, and use this to deduce fully faithfulness of `SimplexCategoryGenRel.toSimplexCategory` thanks to the existing epi-mono factorisation in `SimplexCategory`.
Part of a series of PR formalising that `SimplexCategoryGenRel` is equivalent to `SimplexCategory`.
---
- [ ] depends on: #25737
[](https://gitpod.io/from-referrer/)
---
*This PR continues the work from #21747.*
*Original PR: https://github.com/leanprover-community/mathlib4/pull/21747* |
large-import
t-topology
t-category-theory
blocked-by-other-PR
|
942/9 |
Mathlib.lean,Mathlib/AlgebraicTopology/SimplexCategory/GeneratorsRelations/Equivalence.lean,Mathlib/AlgebraicTopology/SimplexCategory/GeneratorsRelations/NormalForms.lean |
3 |
2 |
['github-actions', 'mathlib4-dependent-issues-bot'] |
nobody |
0-64191 17 hours ago |
0-65440 18 hours ago |
0-0 0 seconds |
| 25737 |
robin-carlier author:robin-carlier |
feat(AlgebraicTopology/SimplexCategory/GeneratorsRelations/NormalForms): Normal forms for `P_δ`s |
We prove that admissible lists indeed provide a normal form for morphisms of satisfying `P_δ`.
To this end, we introduce `standardδ`, a construction that takes a list and turn it into a composition of `δ i`s in `SimplexCategoryGenRel`. We then prove that, thanks to the first simplicial identity, composition on the left corresponds to simplicial insertion in the list. This gives existence of a normal form for every morphism satisfying `P_δ`.
For unicity, we introduce an auxiliary function `simplicialEvalδ : (List ℕ) → ℕ → ℕ` and show that for admissible lists, it lifts to `ℕ` the `orderHom` attached to `toSimplexCategory.map standardδ`, and that we can recover elements of the list only by looking at values of this function.
Part of a series of PR formalising that `SimplexCategoryGenRel` is equivalent to `SimplexCategory`.
---
- [ ] depends on: #25736
[](https://gitpod.io/from-referrer/)
---
*This PR continues the work from #21746.*
*Original PR: https://github.com/leanprover-community/mathlib4/pull/21746* |
large-import
t-topology
t-category-theory
blocked-by-other-PR
|
568/9 |
Mathlib/AlgebraicTopology/SimplexCategory/GeneratorsRelations/NormalForms.lean |
1 |
2 |
['github-actions', 'mathlib4-dependent-issues-bot'] |
nobody |
0-64190 17 hours ago |
0-66056 18 hours ago |
0-0 0 seconds |
| 25735 |
robin-carlier author:robin-carlier |
feat(CategoryTheory/Limits/Sifted): characterization of sifted categories |
Characterize small sifted as those for which the `Type`-valued colimit functor preserves finite product. Deduce that filtered categories, and that categories admitting a final functor from a sifted categories are also sifted.
---
Second part of what used to be #17554. The core of the proof relies on a few private lemmas/defs (`colimBoxIsoColimTensColim` and `factorization_prod_comparison_colim` being the most important ones) and I don’t know if that can be avoided.
I am still unsure wether or not the part relating sifted categories to filtered categories should be split off in a different file to avoid importing `CategoryTheory/Limits/FilteredColimitCommutesFiniteLimit.lean` every time `CategoryTheory/Limits/Sifted.lean` is imported.
The fact that filtered categories are sifted can also be proved without the characterization in this PR (it reduces essentially to `IsFiltered.bowtie`), and so it could also stay in this file with less imports, but I find it nicer to do it using the characterization.
- [x] depends on: #17766
- [x] depends on: #17779
- [ ] depends on: #25732
- [ ] depends on: #25734
- [ ] depends on: #25731
- [x] depends on: #24735
[](https://gitpod.io/from-referrer/)
---
*This PR continues the work from #17781.*
*Original PR: https://github.com/leanprover-community/mathlib4/pull/17781* |
file-removed
large-import
t-category-theory
blocked-by-other-PR
|
689/5 |
Mathlib.lean,Mathlib/CategoryTheory/Limits/Indization/FilteredColimits.lean,Mathlib/CategoryTheory/Limits/Preserves/Bifunctor.lean,Mathlib/CategoryTheory/Limits/Sifted.lean,Mathlib/CategoryTheory/Monoidal/ExternalProduct.lean,Mathlib/CategoryTheory/Monoidal/Internal/Limits.lean,Mathlib/CategoryTheory/Monoidal/Limits/Basic.lean,Mathlib/CategoryTheory/Monoidal/Limits/Preserves.lean |
8 |
2 |
['github-actions', 'mathlib4-dependent-issues-bot'] |
nobody |
0-64188 17 hours ago |
0-66591 18 hours ago |
0-0 0 seconds |
| 25734 |
robin-carlier author:robin-carlier |
feat(CategoryTheory/Limits/Preserves/Bifunctor): construction of `PreservesColimit₂` instances |
Given a bifunctor `G : C₁ ⥤ C₂ ⥤ C` and two diagrams `K₁ : J₁ ⥤ C₁` and `K₂ : J₂ ⥤ C₂`, we show that if `C` has limits of shape `J₁`, `G` preserves the colimit of `K₁`, and `G` objectwise preserves colimits of `K₂`, then there is a `PreservesColimit₂ K₁ K₂ G` instance.
We also show that if there is a `PreservesColimit₂ K₁ K₂ G` instance, then there is a `PreservesColimit₂ K₂ K₁ G.flip` instance as well.
All results are dualised for limits.
---
- [ ] depends on: #25733
[](https://gitpod.io/from-referrer/)
---
*This PR continues the work from #24686.*
*Original PR: https://github.com/leanprover-community/mathlib4/pull/24686* |
t-category-theory
blocked-by-other-PR
|
376/0 |
Mathlib.lean,Mathlib/CategoryTheory/Limits/Preserves/Bifunctor.lean |
2 |
2 |
['github-actions', 'mathlib4-dependent-issues-bot'] |
nobody |
0-63056 17 hours ago |
0-63057 17 hours ago |
0-0 0 seconds |
| 25753 |
robin-carlier author:robin-carlier |
feat(CategoryTheory/Functor/KanExtension): preservations of Kan extensions |
Introduce a typeclass `G.PreservesLeftKanExtension F L` that asserts that a functor `G` preserves the left Kan extension of `F` along a functor `L`. Introduce a pointwise variant, and relate it to the non-pointwise version when pointwise extensions exist.
Show that a functor that preserves the relevant colimits preserve pointwise left Kan extensions. Construct isomorphisms `L.leftKanExtension F ⋙ G ≅ L.leftKanExtension (F ⋙ G)` when `G.PreservesLeftKanExtension F L` holds. Also construct a functorial version, as an isomorphism `L.lan ⋙ (whiskeringRight _ _ _).obj G ≅ (whiskeringRight _ _ _).obj G ⋙ L.lan`.
All results are dualised to right Kan extensions.
---
[](https://gitpod.io/from-referrer/)
---
*This PR continues the work from #24809.*
*Original PR: https://github.com/leanprover-community/mathlib4/pull/24809* |
t-category-theory |
551/0 |
Mathlib.lean,Mathlib/CategoryTheory/Functor/KanExtension/Basic.lean,Mathlib/CategoryTheory/Functor/KanExtension/Preserves.lean |
3 |
1 |
['github-actions'] |
nobody |
0-62411 17 hours ago |
0-62480 17 hours ago |
0-0 0 seconds |
| 25754 |
robin-carlier author:robin-carlier |
feat(CategoryTheory/Monoidal/ExternalProduct): external product of left Kan extended functors |
Given a functor `H' : D' ⥤ V` to a monoidal category that is pointwise left Kan extended along `L : D ⥤ D'`, we show that for a functor `K : E ⥤ V` and under suitable preservations of colimits by the tensor product of `V`, the functor `H' ⊠ K : D' × E ⥤ V` is pointwise left Kan extended along `L.prod (𝟭 E)`. We show a similar statement for the functor `K ⊠ H'`.
This property is crucial for proving properties of Day convolutions of functors from a monoidal category to `V`.
---
- [ ] depends on: #25731
[](https://gitpod.io/from-referrer/)
---
*This PR continues the work from #24989.*
*Original PR: https://github.com/leanprover-community/mathlib4/pull/24989* |
t-category-theory
blocked-by-other-PR
|
244/0 |
Mathlib.lean,Mathlib/CategoryTheory/Monoidal/ExternalProduct/Basic.lean,Mathlib/CategoryTheory/Monoidal/ExternalProduct/KanExtension.lean |
3 |
2 |
['github-actions', 'mathlib4-dependent-issues-bot'] |
nobody |
0-61348 17 hours ago |
0-62083 17 hours ago |
0-0 0 seconds |
| 25760 |
robin-carlier author:robin-carlier |
feat(CategoryTheory/Bicategory): (2,1)-categories and `Pith` |
This PR introduces a class `IsLocallyGroupoid` on bicategories, asserting that every hom-category has an `IsGroupoid` instance.
With this definition, `IsLocallyGroupoid (LocallyDiscrete C)` is correctly inferred.
Given a bicategory `B`, we introduce a type alias `Pith B` for `B` (realized as a one-field structure), and we equip it with a `Bicategory` instance where the hom-categories are the cores of the hom-categories of `B`. We show that this bicategory is a (2,1)-category, construct an inclusion pseudo-functor from `Pith B` to `B`, and show that every pseudofunctor from a (2,1)-category to `B` factors through this inclusion.
---
We can’t fully state the fact that `(pseudofunctorToPith F).comp (inclusion F)` "is" `F` because #18254 is still not merged.
[](https://gitpod.io/from-referrer/)
---
*This PR continues the work from #25150.*
*Original PR: https://github.com/leanprover-community/mathlib4/pull/25150* |
t-category-theory |
191/0 |
Mathlib.lean,Mathlib/CategoryTheory/Bicategory/LocallyGroupoid.lean |
2 |
1 |
['github-actions'] |
nobody |
0-61265 17 hours ago |
0-61338 17 hours ago |
0-0 0 seconds |
| 25761 |
robin-carlier author:robin-carlier |
feat(CategoryTheory/Monoidal): left action of monoidal categories |
Define (left) actions of a monoidal category on a category: a `MonoidalLeftAction` of a monoidal category `C` on a category `D` consists of an action bifunctor `- ⊙ - : C ⥤ D ⥤ D`, equipped with structural natural isomorphisms `(- ⊗ -) ⊙ - ≅ - ⊙ - ⊙ -` and `𝟙_ C ⊙ - ≅ -`, subject to coherence conditions.
The code in this PR is parallel to the existing code for monoidal category.
We provide a battery of basic `simp` lemmas to ease working with this type class, and show that every monoidal category acts on itself via its tensor product.
The code is put in a new subdirectory `CategoryTheory/Monoidal/Action`.
Future wok on the subject includes
- Providing a constructor for `MonoidalLeftAction` taking a monoidal functor from `C` to `D ⥤ D`, where the latter has the "composition" monoidal structure.
- Constructing the action of `C ⥤ C` on `C`.
- Extending the notion of module objects internal to a monoidal category to allow the `Mon_ ` object to be in `C`, and the module to be in `D` where `D` has a monoidal left action of `C`.
- Using the two previous points, show that given a monad `M`, there is an equivalence of categories between `Algebra M` and modules in `C` over the monoid `M.toMon : Mon_ (C ⥤ C)̀`.
---
[](https://gitpod.io/from-referrer/)
---
*This PR continues the work from #25499.*
*Original PR: https://github.com/leanprover-community/mathlib4/pull/25499* |
t-category-theory |
348/0 |
Mathlib.lean,Mathlib/CategoryTheory/Monoidal/Action/Basic.lean,docs/references.bib |
3 |
1 |
['github-actions'] |
nobody |
0-61194 16 hours ago |
0-61262 17 hours ago |
0-0 0 seconds |
| 25763 |
robin-carlier author:robin-carlier |
chore(CategoryTheory/Limits/Shape/End): define coends |
The content of `CategoryTheory/Limits/Shapes/End` was not dualized, so only ends where defined, but not coends.
This PR dualizes the content of the file: we introduce `Cowedge`s as special kinds of `Multicofork`s, and define the `coend_ F` as the colimit of a canonical cowedge we can build from `F : Jᵒᵖ ⥤ J ⥤ C`.
Also, we rename `CategoryTheory.Limits.hom_ext` to `CategoryTheory.Limits.end_.hom_ext`.
---
[](https://gitpod.io/from-referrer/)
---
*This PR continues the work from #25548.*
*Original PR: https://github.com/leanprover-community/mathlib4/pull/25548* |
t-category-theory |
137/7 |
Mathlib/CategoryTheory/Limits/Shapes/End.lean,Mathlib/CategoryTheory/Limits/Shapes/Multiequalizer.lean |
2 |
1 |
['github-actions'] |
nobody |
0-61020 16 hours ago |
0-61087 16 hours ago |
0-0 0 seconds |
| 25765 |
JovanGerb author:JovanGerb |
feat(gcongr): lemma for rewriting inside divisibility |
TODO: add test to show that we can rewrite using `a ≡ b [ZMOD n]` inside `n ∣ 2 * a + 1`.
---
[](https://gitpod.io/from-referrer/)
|
t-data |
5/0 |
Mathlib/Data/Int/ModEq.lean |
1 |
1 |
['github-actions'] |
nobody |
0-60630 16 hours ago |
0-60633 16 hours ago |
0-0 0 seconds |
| 25766 |
robin-carlier author:robin-carlier |
chore/refactor(CategoryTheory/Monoidal/Functor): deprime LaxMonoidal and OplaxMonoidal fields |
Discussed in #25628. We use the new language feature that allows to change expliciteness of binders in the definition of classes. Hence, the "primed" versions of `Functor.LaxMonoidal.μ`, `Functor.LaxMonoidal.ε`, `Functor.OplaxMonoidal.δ` and `Functor.OplaxMonoidal.η` are not needed anymore, as well as the primed version of attached lemmas.
This refactor introduces a bunch of deprecations, as `simps` now become a viable attribute for `LaxMonoidal` and `OplaxMonoidal` classes. These attribute are not systematically applied though, as in some cases the name of the lemmas might be bad.
---
[](https://gitpod.io/from-referrer/)
---
*This PR continues the work from #25664.*
*Original PR: https://github.com/leanprover-community/mathlib4/pull/25664* |
t-category-theory
awaiting-CI
WIP
|
235/331 |
Mathlib/CategoryTheory/Action/Monoidal.lean,Mathlib/CategoryTheory/Monoidal/Braided/Basic.lean,Mathlib/CategoryTheory/Monoidal/Cartesian/Basic.lean,Mathlib/CategoryTheory/Monoidal/CommMon_.lean,Mathlib/CategoryTheory/Monoidal/Functor.lean,Mathlib/CategoryTheory/Monoidal/Limits.lean,Mathlib/CategoryTheory/Monoidal/Mon_.lean,Mathlib/CategoryTheory/Monoidal/OfHasFiniteProducts.lean,Mathlib/CategoryTheory/Monoidal/Opposite.lean,Mathlib/CategoryTheory/Monoidal/Types/Coyoneda.lean |
10 |
1 |
['github-actions'] |
nobody |
0-60524 16 hours ago |
0-60600 16 hours ago |
0-0 0 seconds |
| 25768 |
sgouezel author:sgouezel |
feat: derivative of continuous affine maps |
---
[](https://gitpod.io/from-referrer/)
|
t-analysis |
33/2 |
Mathlib/Analysis/Calculus/AddTorsor/AffineMap.lean,Mathlib/Analysis/Normed/Operator/LinearIsometry.lean,Mathlib/Topology/Algebra/ContinuousAffineMap.lean |
3 |
1 |
['github-actions'] |
nobody |
0-60160 16 hours ago |
0-60226 16 hours ago |
0-0 0 seconds |
| 25771 |
sgouezel author:sgouezel |
feat: drop an assumption in congruence lemma for manifold derivatives |
---
[](https://gitpod.io/from-referrer/)
|
t-differential-geometry |
32/12 |
Mathlib/Geometry/Manifold/ContMDiff/Basic.lean,Mathlib/Geometry/Manifold/MFDeriv/Atlas.lean,Mathlib/Geometry/Manifold/MFDeriv/Basic.lean |
3 |
1 |
['github-actions'] |
nobody |
0-60020 16 hours ago |
0-60093 16 hours ago |
0-0 0 seconds |
| 25767 |
robin-carlier author:robin-carlier |
feat(CategoryTheory/Monoidal/Opposite): the equivalence `Cᴹᵒᵖᴹᵒᵖ ≌ C` is monoidal |
It was left as a TODO in #10415 that the equivalence `Cᴹᵒᵖᴹᵒᵖ ≌ C` is monoidal. We clear this todo.
---
- [ ] depends on: #25766
This used to be a very low-hanging fruit.
[](https://gitpod.io/from-referrer/)
---
*This PR continues the work from #25628.*
*Original PR: https://github.com/leanprover-community/mathlib4/pull/25628* |
t-category-theory
blocked-by-other-PR
|
263/332 |
Mathlib/CategoryTheory/Action/Monoidal.lean,Mathlib/CategoryTheory/Monoidal/Braided/Basic.lean,Mathlib/CategoryTheory/Monoidal/Cartesian/Basic.lean,Mathlib/CategoryTheory/Monoidal/CommMon_.lean,Mathlib/CategoryTheory/Monoidal/Functor.lean,Mathlib/CategoryTheory/Monoidal/Limits.lean,Mathlib/CategoryTheory/Monoidal/Mon_.lean,Mathlib/CategoryTheory/Monoidal/OfHasFiniteProducts.lean,Mathlib/CategoryTheory/Monoidal/Opposite.lean,Mathlib/CategoryTheory/Monoidal/Types/Coyoneda.lean |
10 |
2 |
['github-actions', 'mathlib4-dependent-issues-bot'] |
nobody |
0-59504 16 hours ago |
0-60536 16 hours ago |
0-0 0 seconds |
| 25762 |
robin-carlier author:robin-carlier |
refactor(CategoryTheory/Monoidal/Mod_): refactor `Mod_` using `MonoidalLeftAction` |
Generalize the definition of `CategoryTheory.Monoidal.Mod_Class` and `CategoryTheory.Monoidal.Mod_` to modules in `D` over a monoid object in `C`, where `C` acts monoidally on `D`.
At the same time, we refactor `Mod_` in a way similar to the one `Mon_` has been refactored in #24646. i.e we favor `Mod_Class` in the definition and `Mod_`, and introduce a Prop-class `IsMod_Hom` to define morphisms of modules.
---
- [ ] depends on: #25761
[](https://gitpod.io/from-referrer/)
---
*This PR continues the work from #25545.*
*Original PR: https://github.com/leanprover-community/mathlib4/pull/25545* |
t-category-theory
blocked-by-other-PR
|
551/112 |
Mathlib.lean,Mathlib/CategoryTheory/Monoidal/Action/Basic.lean,Mathlib/CategoryTheory/Monoidal/Cartesian/Mod_.lean,Mathlib/CategoryTheory/Monoidal/Mod_.lean,docs/references.bib |
5 |
2 |
['github-actions', 'mathlib4-dependent-issues-bot'] |
nobody |
0-59502 16 hours ago |
0-61154 16 hours ago |
0-0 0 seconds |
| 25757 |
robin-carlier author:robin-carlier |
feat(CategoryTheory/Monoidal/DayConvolution): left and right unitors for Day convolution |
Given a `DayConvolutionUnit U` a functor `F : C ⥤ V` and a Day convolution of `U` and `F`, we construct the left unitor isomorphism. `U ⊛ F ≅ F`. Similarly, given a Day convolution of `F` and `U`, we construct the right unitor.
We characterize the isomorphisms, show their naturality, and show that the triangle identity is satisfied.
---
- [ ] depends on: #25756
[](https://gitpod.io/from-referrer/)
---
*This PR continues the work from #24993.*
*Original PR: https://github.com/leanprover-community/mathlib4/pull/24993* |
t-category-theory
blocked-by-other-PR
|
954/0 |
Mathlib.lean,Mathlib/CategoryTheory/Functor/KanExtension/Basic.lean,Mathlib/CategoryTheory/Monoidal/DayConvolution.lean,Mathlib/CategoryTheory/Monoidal/ExternalProduct/Basic.lean,Mathlib/CategoryTheory/Monoidal/ExternalProduct/KanExtension.lean |
5 |
2 |
['github-actions', 'mathlib4-dependent-issues-bot'] |
nobody |
0-59501 16 hours ago |
0-61559 17 hours ago |
0-0 0 seconds |
| 25756 |
robin-carlier author:robin-carlier |
feat(CategoryTheory/Monoidal/DayConvolution): Associators and pentagon for Day Convolution |
Under some assumptions on the tensor product of a monoidal category `V`, we show that if three functors `F, G, H` are such that the relevant Day convolutions exist, then there is an associator isomorphism for day convolution. We characterize this isomorphism, and show it is natural.
When all relevant Day convolutions exist, we show that the pentagon identity holds for these associators.
---
- [ ] depends on: #25755
- [ ] depends on: #25754
[](https://gitpod.io/from-referrer/)
---
*This PR continues the work from #24992.*
*Original PR: https://github.com/leanprover-community/mathlib4/pull/24992* |
t-category-theory
blocked-by-other-PR
|
686/0 |
Mathlib.lean,Mathlib/CategoryTheory/Functor/KanExtension/Basic.lean,Mathlib/CategoryTheory/Monoidal/DayConvolution.lean,Mathlib/CategoryTheory/Monoidal/ExternalProduct/Basic.lean,Mathlib/CategoryTheory/Monoidal/ExternalProduct/KanExtension.lean |
5 |
2 |
['github-actions', 'mathlib4-dependent-issues-bot'] |
nobody |
0-59500 16 hours ago |
0-61640 17 hours ago |
0-0 0 seconds |
| 25755 |
robin-carlier author:robin-carlier |
feat(CategoryTheory/Monoidal): Day convolution of functors |
Given monoidal categories `C`,`V` and functors `F G : C ⥤ V`, we introduce a typeclass `[DayConvolution F G]` that bundles the data of a functor `F ⊛ G`, as well as the data required to exhibit `F ⊛ G` as a pointwise left Kan extension of `F ⊠ G` (the external product of `F` and `G`) along the tensor product of `C`.
We give basic API around this class.
We also define a class `DayConvolutionUnit U` which contains the data that `U` is pointwise left Kan extended from `fromPUnit (𝟙_ V)` along `fromPUnit (𝟙_ C)`. Again, we give basic API around this class.
Properties like construction of associators and unitors isomorphisms (and the pentagon/triangle identities) will be the subject of subsequent PRs.
---
- [ ] depends on: #25731
I opted to make `DayConvolution` a class to make assumptions on `C` and `V` minimal.
Also, I realized that `C ⥤ V` already has a monoidal structure (given by pointwise tensor product), so trying to turn it into a monoidal category through Day convolution is probably pointless.
What I intend to do instead is to define a typeclass `DayConvolutionMonoidalCategory A` that will extend `MonoidalCategory A`. This class will contain the data of a fully faithful functor `A ⥤ (C ⥤ V)`, and the data required to make it a "monoidal full subcategory" of `C ⥤ V`. This should allow us to register instances on type aliases for `C ⥤ V`, of course, there should be a constructor for this class that takes as input the embedding and existence of suitable pointwise extensions, and then turn it into a `DayConvolutionMonoidalCategory`. This is upcoming work
[](https://gitpod.io/from-referrer/)
---
*This PR continues the work from #24991.*
*Original PR: https://github.com/leanprover-community/mathlib4/pull/24991* |
t-category-theory
blocked-by-other-PR
|
309/0 |
Mathlib.lean,Mathlib/CategoryTheory/Functor/KanExtension/Basic.lean,Mathlib/CategoryTheory/Monoidal/DayConvolution.lean,Mathlib/CategoryTheory/Monoidal/ExternalProduct.lean |
4 |
2 |
['github-actions', 'mathlib4-dependent-issues-bot'] |
nobody |
0-59499 16 hours ago |
0-59500 16 hours ago |
0-0 0 seconds |
| 25775 |
emilyriehl author:emilyriehl |
feat(AlgebraicTopology/SimplicialSet/NerveAdjunction): to Strict Segal 2 |
Under a suitable hypothesis, a map of 2-truncated simplicial sets can be generated from a refl prefunctor between the underlying reflexive quivers --- provided the codomain is `StrictSegal`. This abstracts a previously formalized result that requires the codomain to be the 2-truncated nerve of a category.
Co-authored-by: Aaron Liu
---
The current draft displays the old code for comparison with new versions labeled ALT. After initial review this will be cut.
[](https://gitpod.io/from-referrer/)
---
*This PR continues the work from #23848.*
*Original PR: https://github.com/leanprover-community/mathlib4/pull/23848* |
infinity-cosmos
t-topology
t-category-theory
|
490/202 |
Mathlib/AlgebraicTopology/SimplexCategory/Basic.lean,Mathlib/AlgebraicTopology/SimplicialSet/HomotopyCat.lean,Mathlib/AlgebraicTopology/SimplicialSet/NerveAdjunction.lean,Mathlib/AlgebraicTopology/SimplicialSet/StrictSegal.lean,Mathlib/CategoryTheory/ComposableArrows.lean,Mathlib/CategoryTheory/EqToHom.lean |
6 |
1 |
['github-actions'] |
nobody |
0-57848 16 hours ago |
0-57910 16 hours ago |
0-0 0 seconds |
| 25779 |
robin-carlier author:robin-carlier |
feat(CategoryTheory/Bicategory/NaturalTransformations): strong and lax natural transformations of lax functors |
Given two lax functors `F G` between bicategories, we define lax natural transformations as families of 1-morphisms `∀ a : B, F.obj a ⟶ G.obj a` equipped with a naturality 2-cell `∀ {a b : B} (f : a ⟶ b), app a ≫ G.map f ⟶ F.map f ≫ app b` that are required to satisfy conditions such as naturality, and compatibility with the `mapId` and `mapComp` fields of the source and target functors.
This notion dualizes the existing notion of oplax natural transformations between, and tries to narrow the current gap between lax and oplax functors in the library, where the latter has much more formalized API. For maintainability, The code tries to stay as aligned as possible with the code in `CategoryTheory.Bicategory.Naturaltransformations.Oplax`.
---
I followed the book by Johnson and Yau for the definition.
I made @yuma-mizuno and @callesonne authors of the files, as they are the authors of the original code for Oplax functors, which I basically copy-pasted and modified to make it work with lax functors. They should feel free to modify this if they want.
Next thing on the list is to tackle modifications between lax/strong natural transforms of lax transforms, as well as the category instance on lax functors.
[](https://gitpod.io/from-referrer/)
---
*This PR continues the work from #25565.*
*Original PR: https://github.com/leanprover-community/mathlib4/pull/25565* |
t-category-theory |
286/0 |
Mathlib.lean,Mathlib/CategoryTheory/Bicategory/NaturalTransformation/Lax.lean,scripts/noshake.json |
3 |
1 |
['github-actions'] |
nobody |
0-57574 15 hours ago |
0-57639 16 hours ago |
0-0 0 seconds |
| 25780 |
emilyriehl author:emilyriehl |
the homotopy category functor preserves products |
This is work in progress with several sorries.
Co-authored-by: Dominic Verity and Thomas Murrills
---
[](https://gitpod.io/from-referrer/)
---
*This PR continues the work from #25010.*
*Original PR: https://github.com/leanprover-community/mathlib4/pull/25010* |
infinity-cosmos
large-import
t-category-theory
WIP
|
352/4 |
Mathlib/AlgebraicTopology/SimplexCategory/Basic.lean,Mathlib/AlgebraicTopology/SimplicialSet/HoFunctorPreservesBinaryProducts.lean,Mathlib/AlgebraicTopology/SimplicialSet/Monoidal.lean,Mathlib/CategoryTheory/ComposableArrows.lean,Mathlib/CategoryTheory/PUnit.lean |
5 |
1 |
['github-actions'] |
nobody |
0-57506 15 hours ago |
0-57564 15 hours ago |
0-0 0 seconds |
| 25776 |
Parcly-Taxel author:Parcly-Taxel |
chore: deprime `induction` in `Analysis` |
I think this is very marginally dependent on #25770. |
tech debt
t-analysis
|
256/208 |
Mathlib/Analysis/Analytic/Composition.lean,Mathlib/Analysis/Analytic/Constructions.lean,Mathlib/Analysis/Analytic/Inverse.lean,Mathlib/Analysis/BoxIntegral/Basic.lean,Mathlib/Analysis/BoxIntegral/Box/SubboxInduction.lean,Mathlib/Analysis/BoxIntegral/Partition/Additive.lean,Mathlib/Analysis/BoxIntegral/Partition/Split.lean,Mathlib/Analysis/CStarAlgebra/Basic.lean,Mathlib/Analysis/CStarAlgebra/Multiplier.lean,Mathlib/Analysis/Calculus/ContDiff/Basic.lean,Mathlib/Analysis/Calculus/ContDiff/Bounds.lean,Mathlib/Analysis/Calculus/ContDiff/FTaylorSeries.lean,Mathlib/Analysis/Calculus/ContDiff/Operations.lean,Mathlib/Analysis/Calculus/Deriv/ZPow.lean,Mathlib/Analysis/Calculus/InverseFunctionTheorem/ApproximatesLinearOn.lean,Mathlib/Analysis/Calculus/IteratedDeriv/Lemmas.lean,Mathlib/Analysis/Calculus/SmoothSeries.lean,Mathlib/Analysis/Convex/Combination.lean,Mathlib/Analysis/Convex/Radon.lean,Mathlib/Analysis/InnerProductSpace/Projection.lean,Mathlib/Analysis/Normed/Algebra/Exponential.lean,Mathlib/Analysis/NormedSpace/Multilinear/Basic.lean,Mathlib/Analysis/Seminorm.lean,Mathlib/Analysis/SpecialFunctions/Complex/Arg.lean,Mathlib/Analysis/SpecialFunctions/Complex/Circle.lean,Mathlib/Analysis/SpecialFunctions/Gamma/Basic.lean,Mathlib/Analysis/SpecialFunctions/Gamma/Beta.lean,Mathlib/Analysis/SpecialFunctions/Gamma/BohrMollerup.lean,Mathlib/Analysis/SpecialFunctions/Gamma/Deriv.lean,Mathlib/Analysis/SpecialFunctions/Integrals.lean,Mathlib/Analysis/SpecialFunctions/Log/Basic.lean,Mathlib/Analysis/SpecialFunctions/Pow/Deriv.lean,Mathlib/Analysis/SpecialFunctions/Pow/NNReal.lean,Mathlib/Analysis/SpecialFunctions/Pow/Real.lean,Mathlib/Analysis/SpecialFunctions/Trigonometric/EulerSineProd.lean |
35 |
2 |
['Parcly-Taxel', 'github-actions'] |
nobody |
0-57418 15 hours ago |
0-57851 16 hours ago |
0-0 0 seconds |
| 25769 |
sgouezel author:sgouezel |
feat: easier to use FTC-2 versions for `C^1` functions |
---
[](https://gitpod.io/from-referrer/)
|
t-measure-probability
t-analysis
|
116/0 |
Mathlib.lean,Mathlib/Analysis/Normed/Operator/LinearIsometry.lean,Mathlib/MeasureTheory/Integral/IntervalIntegral/ContDiff.lean |
3 |
1 |
['github-actions'] |
nobody |
0-57328 15 hours ago |
0-60087 16 hours ago |
0-0 0 seconds |
| 25784 |
emilyriehl author:emilyriehl |
feat(Bicategory/CatEnriched): 2-cat from Cat-enriched cat |
A construction of the canonical strict bicategory structure given a `EnrichedCategory Cat C`.
From the ∞-cosmos project.
Co-Authored-By: Emily Riehl
---
[](https://gitpod.io/from-referrer/)
---
*This PR continues the work from #25287.*
*Original PR: https://github.com/leanprover-community/mathlib4/pull/25287* |
infinity-cosmos
t-category-theory
awaiting-author
|
129/0 |
Mathlib.lean,Mathlib/CategoryTheory/Bicategory/CatEnriched.lean |
2 |
1 |
['github-actions'] |
nobody |
0-57072 15 hours ago |
0-57136 15 hours ago |
0-0 0 seconds |
| 25736 |
robin-carlier author:robin-carlier |
feat(AlgebraicTopology/SimplexCategory/GeneratorsRelations/NormalForms): Normal forms for `P_σ`s |
We prove that admissible lists indeed provide a normal form for morphisms of satisfying `P_σ`.
To this end, we introduce `standardσ`, a construction that takes a list and turn it into a composition of `σ i`s in `SimplexCategoryGenRel`. We then prove that, thangs to the fifth simplicial identity, composition on the right corresponds to simplicial insertion in the list. This gives existence of a normal form for every morphism satisfying `P_σ`.
For unicity, we introduce an auxiliary function `simplicialEvalσ : (List ℕ) → ℕ → ℕ` and show that for admissible lists, it lifts to `ℕ` the `orderHom` attached to `toSimplexCategory.map standardσ`, and that we can recover elements of the list only by looking at values of this function.
Part of a series of PR formalising that `SimplexCategoryGenRel` is equivalent to `SimplexCategory`.
---
- [x] depends on: #21744
[](https://gitpod.io/from-referrer/)
---
*This PR continues the work from #21745.*
*Original PR: https://github.com/leanprover-community/mathlib4/pull/21745* |
large-import
t-topology
t-category-theory
|
253/7 |
Mathlib/AlgebraicTopology/SimplexCategory/GeneratorsRelations/NormalForms.lean |
1 |
2 |
['github-actions', 'mathlib4-dependent-issues-bot'] |
nobody |
0-56838 15 hours ago |
0-66528 18 hours ago |
0-0 0 seconds |
| 25786 |
Parcly-Taxel author:Parcly-Taxel |
feat: IMO 2001 Q4 |
|
IMO |
131/4 |
Archive.lean,Archive/Imo/Imo2001Q4.lean,Mathlib/Logic/Equiv/Fin/Rotate.lean |
3 |
1 |
['github-actions'] |
nobody |
0-56837 15 hours ago |
0-56905 15 hours ago |
0-0 0 seconds |
| 25790 |
Parcly-Taxel author:Parcly-Taxel |
chore: remove >6 month old material in `Deprecated` |
|
file-removed
tech debt
|
0/250 |
Mathlib.lean,Mathlib/Deprecated/Cardinal/Continuum.lean,Mathlib/Deprecated/Cardinal/Finite.lean,Mathlib/Deprecated/Cardinal/PartENat.lean,Mathlib/Deprecated/Order.lean |
5 |
1 |
['github-actions'] |
nobody |
0-56094 15 hours ago |
0-56193 15 hours ago |
0-0 0 seconds |
| 25794 |
dagurtomas author:dagurtomas |
feat(CategoryTheory): localization preserves braided structure |
---
[](https://gitpod.io/from-referrer/)
---
*This PR continues the work from #24485.*
*Original PR: https://github.com/leanprover-community/mathlib4/pull/24485* |
t-category-theory |
733/427 |
Mathlib.lean,Mathlib/CategoryTheory/Localization/Monoidal.lean,Mathlib/CategoryTheory/Localization/Monoidal/Basic.lean,Mathlib/CategoryTheory/Localization/Monoidal/Braided.lean,Mathlib/CategoryTheory/Monoidal/Braided/Basic.lean,Mathlib/CategoryTheory/Sites/Monoidal.lean |
6 |
1 |
['github-actions'] |
nobody |
0-54881 15 hours ago |
0-54953 15 hours ago |
0-0 0 seconds |
| 25795 |
dagurtomas author:dagurtomas |
chore(Condensed): introduce an abbrev for the equivalence of light condensed sets with a category of sheaves on a small site |
---
[](https://gitpod.io/from-referrer/)
---
*This PR continues the work from #24522.*
*Original PR: https://github.com/leanprover-community/mathlib4/pull/24522* |
t-condensed |
39/0 |
Mathlib.lean,Mathlib/Condensed/Light/Small.lean |
2 |
1 |
['github-actions'] |
nobody |
0-54723 15 hours ago |
0-54788 15 hours ago |
0-0 0 seconds |
| 25799 |
dagurtomas author:dagurtomas |
feat(CategoryTheory): the universal property of localized monoidal categories |
This PR provides a monoidal structure on any functor out of a localized monoidal category whose precomposition with the localization functor is monoidal
---
[](https://gitpod.io/from-referrer/)
---
*This PR continues the work from #24727.*
*Original PR: https://github.com/leanprover-community/mathlib4/pull/24727* |
t-category-theory
WIP
|
457/0 |
Mathlib.lean,Mathlib/CategoryTheory/Localization/Bifunctor.lean,Mathlib/CategoryTheory/Localization/MonoidalFunctor.lean |
3 |
1 |
['github-actions'] |
nobody |
0-54320 15 hours ago |
0-54386 15 hours ago |
0-0 0 seconds |
| 25789 |
kim-em author:kim-em |
fix: handle remote conflicts in migrate_to_fork.py |
This PR fixes a bug in the fork migration script where it would try to remove the 'origin' remote twice in certain scenarios. When a user's main repository remote was named 'origin' (pointing to leanprover-community/mathlib4), the script would: (1) Rename 'origin' to 'upstream' (removing the old 'origin'), (2) Later try to remove 'origin' again when setting up the fork remote, (3) Fail with error: 'No such remote: origin'. The solution adds proper logic to handle the case where user declines to rename their upstream remote, checks if 'origin' remote exists before trying to add/remove it, offers fallback to use 'fork' remote name if user wants to keep existing 'origin', and ensures the script returns the correct remote name for the fork in all scenarios. This resolves the 'No such remote: origin' error.
(AI generated.) |
|
14/14 |
scripts/migrate_to_fork.py |
1 |
2 |
['CBirkbeck', 'github-actions'] |
nobody |
0-54272 15 hours ago |
0-56726 15 hours ago |
0-0 0 seconds |
| 25797 |
dagurtomas author:dagurtomas |
feat(Condensed): closed symmetric monoidal structure on light condensed modules |
---
- [ ] depends on: #24485
- [x] depends on: #24490
- [x] depends on: #24522
[](https://gitpod.io/from-referrer/)
---
*This PR continues the work from #24523.*
*Original PR: https://github.com/leanprover-community/mathlib4/pull/24523* |
t-condensed
WIP
|
906/427 |
Mathlib.lean,Mathlib/CategoryTheory/Localization/Monoidal.lean,Mathlib/CategoryTheory/Localization/Monoidal/Basic.lean,Mathlib/CategoryTheory/Localization/Monoidal/Braided.lean,Mathlib/CategoryTheory/Monoidal/Braided/Basic.lean,Mathlib/CategoryTheory/Monoidal/Braided/Transport.lean,Mathlib/CategoryTheory/Sites/Monoidal.lean,Mathlib/Condensed/Light/Monoidal.lean,Mathlib/Condensed/Light/Small.lean |
9 |
2 |
['github-actions', 'mathlib4-dependent-issues-bot'] |
nobody |
0-54259 15 hours ago |
0-54260 15 hours ago |
0-0 0 seconds |
| 25802 |
dagurtomas author:dagurtomas |
feat(AlgebraicTopology): anodyne morphisms of simplicial sets |
---
[](https://gitpod.io/from-referrer/)
---
*This PR continues the work from #20201.*
*Original PR: https://github.com/leanprover-community/mathlib4/pull/20201* |
t-topology
WIP
|
148/0 |
Mathlib.lean,Mathlib/AlgebraicTopology/Anodyne.lean,Mathlib/AlgebraicTopology/KanFibration.lean,Mathlib/CategoryTheory/MorphismProperty/WeakSaturation.lean |
4 |
1 |
['github-actions'] |
nobody |
0-53253 14 hours ago |
0-53270 14 hours ago |
0-0 0 seconds |
| 25796 |
dagurtomas author:dagurtomas |
feat(CategoryTheory): transport symmetric monoidal structure along equivalence |
---
[](https://gitpod.io/from-referrer/)
---
*This PR continues the work from #24490.*
*Original PR: https://github.com/leanprover-community/mathlib4/pull/24490* |
t-category-theory |
97/0 |
Mathlib.lean,Mathlib/CategoryTheory/Monoidal/Braided/Basic.lean,Mathlib/CategoryTheory/Monoidal/Braided/Transport.lean |
3 |
1 |
['github-actions'] |
nobody |
0-52423 14 hours ago |
0-54733 15 hours ago |
0-0 0 seconds |
| 25783 |
Parcly-Taxel author:Parcly-Taxel |
feat: IMO 1985 Q2 |
|
IMO |
100/0 |
Archive.lean,Archive/Imo/Imo1985Q2.lean |
2 |
1 |
['github-actions'] |
nobody |
0-51711 14 hours ago |
0-57222 15 hours ago |
0-0 0 seconds |
| 25806 |
jcommelin author:jcommelin |
fix: make create-adaptation-pr.sh robust against remote naming conventions |
This PR fixes the create-adaptation-pr.sh script to work with different remote naming conventions by dynamically discovering the correct upstream remote instead of assuming 'origin' points to leanprover-community/mathlib4. |
|
25/8 |
scripts/create-adaptation-pr.sh |
1 |
1 |
['github-actions'] |
nobody |
0-50733 14 hours ago |
0-50805 14 hours ago |
0-0 0 seconds |
| 25773 |
JovanGerb author:JovanGerb |
chore(grewrite): import `grewrite` where we import `gcongr` |
TODO: investigate importing it into Mathlib.Tactic.Common
This PR imports `grewrite` where `gcongr` is being imported. I think the extra import size is acceptable.
---
[](https://gitpod.io/from-referrer/)
|
large-import |
66/81 |
Mathlib/Algebra/Order/Module/OrderedSMul.lean,Mathlib/Analysis/Normed/Group/Seminorm.lean,Mathlib/Data/Nat/Basic.lean,Mathlib/Data/Nat/Factorial/Basic.lean,Mathlib/Order/Defs/PartialOrder.lean,Mathlib/Order/Lattice.lean,Mathlib/Order/RelClasses.lean,Mathlib/Tactic/Common.lean,Mathlib/Tactic/GCongr.lean,Mathlib/Tactic/GCongr/Core.lean,scripts/noshake.json |
11 |
1 |
['github-actions'] |
nobody |
0-46388 12 hours ago |
0-46395 12 hours ago |
0-0 0 seconds |
| 25778 |
thefundamentaltheor3m author:thefundamentaltheor3m |
feat: Monotonicity of `setIntegral` for nonnegative functions |
This PR makes it easier to prove monotonicity of the Bochner integral on sets for nonnegative functions by removing the stronger assumption required by the general monotonicity lemma that both of the functions being compared must be integrable.
---
[](https://gitpod.io/from-referrer/)
|
new-contributor
t-measure-probability
awaiting-author
|
16/0 |
Mathlib/MeasureTheory/Integral/Bochner/Set.lean |
1 |
1 |
['github-actions'] |
nobody |
0-45767 12 hours ago |
0-45767 12 hours ago |
0-0 0 seconds |
| 25804 |
erdOne author:erdOne |
feat: `∑ z ∈ L, ‖z - x‖⁻ʳ` converges for lattices `L` |
---
[](https://gitpod.io/from-referrer/)
---
*This PR continues the work from #21673.*
*Original PR: https://github.com/leanprover-community/mathlib4/pull/21673* |
t-analysis |
319/0 |
Mathlib.lean,Mathlib/Algebra/BigOperators/Group/Finset/Disjoint.lean,Mathlib/Algebra/Module/ZLattice/Summable.lean,Mathlib/Order/Disjointed.lean |
4 |
1 |
['github-actions'] |
nobody |
0-45299 12 hours ago |
0-51998 14 hours ago |
0-0 0 seconds |
| 25774 |
Parcly-Taxel author:Parcly-Taxel |
chore: deprime `induction` in `AlgebraicTopology/CategoryTheory` |
Most replacements that are also in #23676 have been copied over, but some have been optimised further. |
tech debt |
133/124 |
Mathlib/AlgebraicTopology/DoldKan/Decomposition.lean,Mathlib/AlgebraicTopology/DoldKan/Degeneracies.lean,Mathlib/AlgebraicTopology/DoldKan/NCompGamma.lean,Mathlib/AlgebraicTopology/DoldKan/Projections.lean,Mathlib/AlgebraicTopology/SimplexCategory/MorphismProperty.lean,Mathlib/AlgebraicTopology/SimplicialObject/Split.lean,Mathlib/AlgebraicTopology/SimplicialSet/Degenerate.lean,Mathlib/AlgebraicTopology/SimplicialSet/NerveAdjunction.lean,Mathlib/AlgebraicTopology/SimplicialSet/StdSimplex.lean,Mathlib/CategoryTheory/Abelian/GrothendieckCategory/EnoughInjectives.lean,Mathlib/CategoryTheory/Abelian/GrothendieckCategory/Subobject.lean,Mathlib/CategoryTheory/Action/Concrete.lean,Mathlib/CategoryTheory/Action/Monoidal.lean,Mathlib/CategoryTheory/ComposableArrows.lean,Mathlib/CategoryTheory/Extensive.lean,Mathlib/CategoryTheory/Filtered/Basic.lean,Mathlib/CategoryTheory/Galois/Decomposition.lean,Mathlib/CategoryTheory/Galois/EssSurj.lean,Mathlib/CategoryTheory/Limits/Shapes/Equalizers.lean,Mathlib/CategoryTheory/Limits/Shapes/SequentialProduct.lean,Mathlib/CategoryTheory/Limits/Types/Colimits.lean,Mathlib/CategoryTheory/Limits/VanKampen.lean,Mathlib/CategoryTheory/Quotient.lean,Mathlib/CategoryTheory/Sites/Sheaf.lean,Mathlib/CategoryTheory/Subobject/Basic.lean,Mathlib/CategoryTheory/Subobject/FactorThru.lean,Mathlib/CategoryTheory/Subobject/Lattice.lean,Mathlib/CategoryTheory/Triangulated/TStructure/Basic.lean |
28 |
3 |
['Parcly-Taxel', 'eric-wieser', 'github-actions'] |
nobody |
0-44063 12 hours ago |
0-58300 16 hours ago |
0-0 0 seconds |
| 25788 |
Parcly-Taxel author:Parcly-Taxel |
feat: number of edges in the Turán graph |
We provide two theorems, the first `card_edgeFinset_turanGraph` providing the exact number of edges and the other `card_edgeFinset_turanGraph_le` providing a (slightly) looser bound whose main advantage is its lack of integer division/modulus operations.
The bound in `card_edgeFinset_turanGraph_le` is also the bound provided in [Motzkin and Straus (1965)](https://doi.org/10.4153%2FCJM-1965-053-6). |
large-import
t-combinatorics
|
132/0 |
Mathlib/Combinatorics/SimpleGraph/Turan.lean,Mathlib/Data/Nat/ModEq.lean |
2 |
2 |
['YaelDillies', 'github-actions'] |
nobody |
0-43801 12 hours ago |
0-56754 15 hours ago |
0-0 0 seconds |
| 25781 |
emilyriehl author:emilyriehl |
Feat(CategoryTheory): terminal categories with an application to hoFunctor |
Some preliminary API around terminal categories is developed with an application for the infinity-cosmos project: proving that the homotopy category functor preserves terminal objects. We also include proofs that `[0]` is terminal in the simplex category and `Δ[0]` is the terminal simplicial set.
Co-authored by [Robin Carlier](robin.carlier@ens-lyon.fr), [Adam Topaz](topaz@ualberta.ca), and [Zeyi Zhao](zzhao95@jh.edu).
---
[](https://gitpod.io/from-referrer/)
---
*This PR continues the work from #25459.*
*Original PR: https://github.com/leanprover-community/mathlib4/pull/25459* |
infinity-cosmos
large-import
t-category-theory
|
176/3 |
Mathlib.lean,Mathlib/AlgebraicTopology/SimplexCategory/Basic.lean,Mathlib/AlgebraicTopology/SimplicialSet/HomotopyCat.lean,Mathlib/AlgebraicTopology/SimplicialSet/Monoidal.lean,Mathlib/CategoryTheory/Category/Cat/Terminal.lean,Mathlib/CategoryTheory/Category/ReflQuiv.lean,Mathlib/CategoryTheory/Quotient.lean |
7 |
1 |
['github-actions'] |
nobody |
0-43192 11 hours ago |
0-57411 15 hours ago |
0-0 0 seconds |
| 25787 |
riccardobrasca author:riccardobrasca |
RB-cyclo |
---
[](https://gitpod.io/from-referrer/)
|
WIP |
1221/1 |
Mathlib.lean,Mathlib/Data/ZMod/QuotientRing.lean,Mathlib/LinearAlgebra/Dimension/Finrank.lean,Mathlib/NumberTheory/NumberField/Ideal/KummerDedekind.lean,Mathlib/NumberTheory/RamificationInertia/Basic.lean,Mathlib/Order/Atoms.lean,Mathlib/RingTheory/AdjoinRoot.lean,Mathlib/RingTheory/DedekindDomain/Ideal.lean,Mathlib/RingTheory/Ideal/Over.lean,Mathlib/RingTheory/Ideal/Span.lean,Mathlib/Stuff/Cyclotomic.lean,Mathlib/Stuff/Eleven.lean,Mathlib/Stuff/Factorization.lean,Mathlib/Stuff/Inertia.lean,Mathlib/Stuff/Minkowski.lean,Mathlib/Stuff/OrderOf.lean,Mathlib/Stuff/Seven.lean,Mathlib/Stuff/Thirteen.lean |
18 |
1 |
['github-actions'] |
nobody |
0-42711 11 hours ago |
0-56758 15 hours ago |
0-0 0 seconds |
| 25812 |
vlad902 author:vlad902 |
feat(data): List.Chain' helper lemmas |
Add two helpers lemmas to go from a List.Chain' hypothesis to a concrete
predicate about two consecutive elements, one in the positive and one in
the negative. |
t-data |
23/0 |
Mathlib/Data/List/Chain.lean |
1 |
1 |
['github-actions'] |
nobody |
0-42534 11 hours ago |
0-42535 11 hours ago |
0-0 0 seconds |
| 25724 |
bryangingechen author:bryangingechen |
chore: disable scheduled runs of stale issues workflow |
There's no point in having this run on schedule while it's still in limbo.
---
This also seems to have been [completely broken](https://github.com/leanprover-community/mathlib4/actions/workflows/stale.yml) since #21681, since the search string is too long. Maybe we should just delete this. |
CI |
1/2 |
.github/workflows/stale.yml |
1 |
1 |
['github-actions'] |
nobody |
0-42096 11 hours ago |
0-78965 21 hours ago |
0-0 0 seconds |
| 25814 |
vlad902 author:vlad902 |
feat(SimpleGraph): Weaker condition for paths in acyclic graphs |
`IsAcyclic.isPath_iff_chain'` defines a weaker condition for proving that a walk is a path, in particular it shows that rather than proving that all vertices in the support of a walk are distinct, one must only show that consecutive edges are distinct (e.g. every other vertex must be distinct.) This leads to a simple corollary that trails are also paths in acyclic graphs.
---
*This PR continues the work from #25630.*
*Original PR: https://github.com/leanprover-community/mathlib4/pull/25630* |
t-combinatorics |
48/0 |
Mathlib/Combinatorics/SimpleGraph/Acyclic.lean,Mathlib/Combinatorics/SimpleGraph/Path.lean |
2 |
1 |
['github-actions'] |
nobody |
0-41206 11 hours ago |
0-41750 11 hours ago |
0-0 0 seconds |
| 25816 |
sgouezel author:sgouezel |
chore: kill coercion from EquivLike to Equiv |
---
[](https://gitpod.io/from-referrer/)
|
t-logic
WIP
|
35/37 |
Mathlib/Logic/Equiv/Defs.lean |
1 |
1 |
['github-actions'] |
nobody |
0-39343 10 hours ago |
0-39346 10 hours ago |
0-0 0 seconds |
| 25739 |
literandltx author:literandltx |
feat(number_theory/legendre_symbol): Add sqrt‐of‐residue theorems for p=4k+3 and p=8k+5 |
Add a new file `QuadraticResidueRoots.lean` under `Mathlib/NumberTheory/LegendreSymbol/` that proves two explicit “square-root of quadratic residue” theorems for primes of the specific form.
- **`exists_sqrt_of_residue_mod4_eq3`** for primes `p = 4*k + 3`
- **`exists_sqrt_of_residue_mod8_eq5`** for primes `p = 8*k + 5`
It also introduces the helper lemmas `euler_criterion_traditional` and `legendreSym.at_two_mod8_eq_5`. Import lines in `Mathlib.lean` and `Mathlib/NumberTheory/LegendreSymbol/Basic.lean` have been updated accordingly.
|
new-contributor
t-number-theory
|
217/0 |
Mathlib.lean,Mathlib/NumberTheory/LegendreSymbol/Basic.lean,Mathlib/NumberTheory/LegendreSymbol/QuadraticReciprocity.lean,Mathlib/NumberTheory/LegendreSymbol/QuadraticResidueRoots.lean |
4 |
1 |
['github-actions'] |
literandltx assignee:literandltx |
0-38938 10 hours ago |
0-65522 18 hours ago |
0-0 0 seconds |
| 25759 |
FrankieNC author:FrankieNC |
feat(MeasureTheory/Measure): bound Hausdorff measure under orthogonal projection |
Formalisation that Hausdorff measure is non-increasing under orthogonal projection onto a finite-dimensional Euclidean subspace.
This includes:
* a bound on the norm of orthogonal projections;
* a proof that orthogonal projection is 1-Lipschitz;
* the main result: the s-dimensional Hausdorff measure of the projection of a set is less than or equal to that of the original set.
This formalises Lemma 3.5 from Julian Fox’s REU paper:
*Besicovitch Sets, Kakeya Sets, and Their Properties*, UChicago REU, 2021.
---
[](https://gitpod.io/from-referrer/)
---
*This PR continues the work from #25543.*
*Original PR: https://github.com/leanprover-community/mathlib4/pull/25543* |
new-contributor
t-measure-probability
|
87/8 |
Mathlib/Analysis/InnerProductSpace/Projection.lean,Mathlib/Analysis/NormedSpace/OperatorNorm/Basic.lean,Mathlib/MeasureTheory/Measure/Hausdorff.lean,Mathlib/Topology/MetricSpace/HausdorffDimension.lean,scripts/migrate_to_fork.py |
5 |
1 |
['github-actions'] |
nobody |
0-37565 10 hours ago |
0-37565 10 hours ago |
0-0 0 seconds |
| 25807 |
Vierkantor author:Vierkantor |
ci: Empty commit to test the bench-after-CI workflow. |
---
[](https://gitpod.io/from-referrer/)
|
test-ci
CI
|
0/0 |
|
0 |
3 |
['github-actions', 'leanprover-bot', 'leanprover-community-mathlib4-bot'] |
nobody |
0-34243 9 hours ago |
0-34243 9 hours ago |
0-0 0 seconds |
| 25818 |
xroblot author:xroblot |
feat(NumberField/CMField): All CM-extensions come from the real maximal subfield |
Main result: if `K/F` is a CM-extension then `F` is isomorphic to the maximal real subfield of `K`
---
- [x] depends on: #23760
[](https://gitpod.io/from-referrer/)
---
*This PR continues the work from #23858.*
*Original PR: https://github.com/leanprover-community/mathlib4/pull/23858* |
t-number-theory |
113/6 |
Mathlib/Algebra/Field/Subfield/Basic.lean,Mathlib/FieldTheory/IntermediateField/Adjoin/Basic.lean,Mathlib/FieldTheory/IntermediateField/Basic.lean,Mathlib/LinearAlgebra/Dimension/Finrank.lean,Mathlib/NumberTheory/NumberField/CMField.lean |
5 |
2 |
['github-actions', 'mathlib4-dependent-issues-bot'] |
nobody |
0-33291 9 hours ago |
0-33595 9 hours ago |
0-0 0 seconds |
| 25803 |
erdOne author:erdOne |
feat: taylor expansion of `1 / z ^ r` |
---
This might exist somewhere else but I couldn't find them.
[](https://gitpod.io/from-referrer/)
---
*This PR continues the work from #21693.*
*Original PR: https://github.com/leanprover-community/mathlib4/pull/21693* |
t-analysis |
95/0 |
Mathlib.lean,Mathlib/Analysis/SpecificLimits/InvPow.lean |
2 |
3 |
['erdOne', 'github-actions', 'j-loreaux'] |
nobody |
0-30729 8 hours ago |
0-30729 8 hours ago |
0-0 0 seconds |
| 25782 |
emilyriehl author:emilyriehl |
feat(CategoryTheory/Category/Cat): cartesian closed instance on small categories |
The category of small categories is cartesian closed, with exponentials defined by functor categories. Adjoint transposition is defined by currying and uncurrying.
[](https://gitpod.io/from-referrer/)
---
*This PR continues the work from #25646.*
*Original PR: https://github.com/leanprover-community/mathlib4/pull/25646* |
infinity-cosmos
t-category-theory
awaiting-author
|
167/1 |
Mathlib.lean,Mathlib/CategoryTheory/Category/Cat.lean,Mathlib/CategoryTheory/Category/Cat/CartesianClosed.lean,Mathlib/CategoryTheory/Functor/Currying.lean |
4 |
2 |
['callesonne', 'github-actions', 'joelriou'] |
nobody |
0-28001 7 hours ago |
0-28002 7 hours ago |
0-0 0 seconds |
| 25822 |
ScottCarnahan author:ScottCarnahan |
WIP: experiments with vertex algebras |
This is a testbed for various attempts at things. Please don't bother reviewing.
---
[](https://gitpod.io/from-referrer/)
---
*This PR continues the work from #25821.*
*Original PR: https://github.com/leanprover-community/mathlib4/pull/25821* |
large-import
WIP
|
7445/616 |
Mathlib.lean,Mathlib/Algebra/Lie/ChevalleyEilenberg.lean,Mathlib/Algebra/Lie/Cocycle.lean,Mathlib/Algebra/Lie/Extension.lean,Mathlib/Algebra/Lie/Extension/Basic.lean,Mathlib/Algebra/Lie/Extension/CentralExtension.lean,Mathlib/Algebra/Lie/Loop.lean,Mathlib/Algebra/Module/Equiv/Basic.lean,Mathlib/Algebra/Module/Equiv/Defs.lean,Mathlib/Algebra/Order/AddTorsor.lean,Mathlib/Algebra/Order/Hom/Monoid.lean,Mathlib/Algebra/Order/Hom/MonoidWithZero.lean,Mathlib/Algebra/Order/Hom/Ring.lean,Mathlib/Algebra/Order/Monoid/Prod.lean,Mathlib/Algebra/Polynomial/Laurent.lean,Mathlib/Algebra/Polynomial/Nusmeval.lean,Mathlib/Algebra/Polynomial/Smeval.lean,Mathlib/Algebra/Vertex/Affine.lean,Mathlib/Algebra/Vertex/Basic.lean,Mathlib/Algebra/Vertex/Defs.lean,Mathlib/Algebra/Vertex/HVertexOperator.lean,Mathlib/Algebra/Vertex/VertexOperator.lean,Mathlib/Data/Finset/SMulAntidiagonal.lean,Mathlib/Data/FunLike/Equiv.lean,Mathlib/Data/Prod/RevLex.lean,Mathlib/GroupTheory/ArchimedeanDensely.lean,Mathlib/GroupTheory/GroupAction/Equiv.lean,Mathlib/GroupTheory/GroupAction/Hom.lean,Mathlib/RingTheory/Binomial.lean,Mathlib/RingTheory/DividedPowers/Cauchy.lean,Mathlib/RingTheory/FormalSeries.lean,Mathlib/RingTheory/HahnSeries/Addition.lean,Mathlib/RingTheory/HahnSeries/Basic.lean,Mathlib/RingTheory/HahnSeries/Binomial.lean,Mathlib/RingTheory/HahnSeries/HEval.lean,Mathlib/RingTheory/HahnSeries/Multiplication.lean,Mathlib/RingTheory/HahnSeries/PowerSeries.lean,Mathlib/RingTheory/HahnSeries/Summable.lean,Mathlib/RingTheory/PowerSeries/Binomial.lean,Mathlib/RingTheory/PowerSeries/Eval.lean |
40 |
1 |
['github-actions'] |
nobody |
0-27743 7 hours ago |
0-27828 7 hours ago |
0-0 0 seconds |
| 25823 |
joelriou author:joelriou |
refactor(CategoryTheory/Limits): colimits in Type |
Colimits in `Type` are refactored so as to relate them with the non categorical constructions introduced in #23339.
---
- [x] depends on: #23346
- [x] depends on: #23339
[](https://gitpod.io/from-referrer/)
---
*This PR continues the work from #23364.*
*Original PR: https://github.com/leanprover-community/mathlib4/pull/23364* |
t-category-theory |
444/363 |
Mathlib/Algebra/Category/Grp/Basic.lean,Mathlib/Algebra/Category/Grp/FilteredColimits.lean,Mathlib/Algebra/Category/ModuleCat/FilteredColimits.lean,Mathlib/Algebra/Category/MonCat/Basic.lean,Mathlib/Algebra/Category/MonCat/FilteredColimits.lean,Mathlib/Algebra/Category/Ring/Basic.lean,Mathlib/Algebra/Category/Ring/FilteredColimits.lean,Mathlib/CategoryTheory/Limits/Final.lean,Mathlib/CategoryTheory/Limits/FintypeCat.lean,Mathlib/CategoryTheory/Limits/IsConnected.lean,Mathlib/CategoryTheory/Limits/Preserves/Ulift.lean,Mathlib/CategoryTheory/Limits/Shapes/SingleObj.lean,Mathlib/CategoryTheory/Limits/Types/ColimitType.lean,Mathlib/CategoryTheory/Limits/Types/Colimits.lean,Mathlib/CategoryTheory/Limits/Types/Filtered.lean,Mathlib/CategoryTheory/Types.lean,Mathlib/Topology/Category/TopCat/Limits/Basic.lean |
17 |
5 |
['erdOne', 'github-actions', 'mathlib4-dependent-issues-bot'] |
nobody |
0-24268 6 hours ago |
0-26672 7 hours ago |
0-0 0 seconds |
| 25785 |
Parcly-Taxel author:Parcly-Taxel |
feat: IMO 2001 Q3 |
|
IMO
maintainer-merge
|
111/0 |
Archive.lean,Archive/Imo/Imo2001Q3.lean |
2 |
3 |
['dwrensha', 'github-actions'] |
nobody |
0-23415 6 hours ago |
0-23415 6 hours ago |
0-0 0 seconds |
| 25827 |
j-loreaux author:j-loreaux |
feat: define a metric structure on `α →ᵤ β` |
When `β` is a (pseudo, extended) metric space, the space of function `α →ᵤ β` equipped with the topology of uniform convergence is naturally a (pseudo, extended) metric space with distance given by `edist f g := ⨆ x, edist (f x) (g x)` (and this induces the pre-existing uniformity on `α →ᵤ β`).
Likewise for `α →ᵤ[𝔖] β` with `𝔖` finite, `⨆ x ∈ ⋃₀ 𝔖, edist (f x) (g x)` is a natural metric which induces the existing uniformity. In certain situations, `α →ᵤ[𝔖] β` is metrizable even if `𝔖` is not finite, but in these cases, the above is not a suitable distance function. As an example, if `β` is a σ-compact metric space, then [UniformOnFun.isCountablyGenerated_uniformity](https://leanprover-community.github.io/mathlib4_docs/Mathlib/Topology/UniformSpace/UniformConvergenceTopology.html#UniformOnFun.isCountablyGenerated_uniformity) guarantees that `α →ᵤ[{K | IsCompact K}] β` is metrizable, but since the union of the compact sets is the entire space, the metric above would generate the topology of uniform convergence (everywhere, not just on compact sets).
In this PR, we provide these instances, and derive several consequences. For example, we derive the natural sufficient condition for uniform equicontinuity in terms of the individual functions being Lipschitz with the same constant:
```lean
lemma LipschitzWith.uniformEquicontinuous (f : α → γ → β) (K : ℝ≥0)
(h : ∀ c, LipschitzWith K (f c)) : UniformEquicontinuous f :=
sorry
```
In addition, we prove that the natural maps from `BoundedContinuousFunction` and `ContinuousMap` (when the domain is compact) are isometries.
This is all motivated by the desire to state joint continuity results for the continuous functional calculus (`cfc`) in terms of bare functions. See #25635.
---
- [x] depends on: #25633
- [ ] depends on: #25695
[](https://gitpod.io/from-referrer/)
---
*This PR continues the work from #25632.*
*Original PR: https://github.com/leanprover-community/mathlib4/pull/25632* |
t-topology |
299/0 |
Mathlib.lean,Mathlib/Topology/MetricSpace/UniformConvergence.lean,Mathlib/Topology/UniformSpace/UniformConvergenceTopology.lean |
3 |
2 |
['github-actions', 'mathlib4-dependent-issues-bot'] |
nobody |
0-21053 5 hours ago |
0-21231 5 hours ago |
0-0 0 seconds |
| 25825 |
yuma-mizuno author:yuma-mizuno |
feat(CategoryTheory/Bicategory): define lax transformations between oplax functors |
and also define oplax transformations between lax functors.
- [x] depends on: #25779
---
[](https://gitpod.io/from-referrer/)
---
*This PR continues the work from #25672.*
*Original PR: https://github.com/leanprover-community/mathlib4/pull/25672* |
large-import
t-category-theory
blocked-by-other-PR
WIP
|
433/4 |
Mathlib.lean,Mathlib/CategoryTheory/Bicategory/NaturalTransformation/Lax.lean,Mathlib/CategoryTheory/Bicategory/NaturalTransformation/Oplax.lean,scripts/noshake.json |
4 |
2 |
['github-actions', 'mathlib4-dependent-issues-bot'] |
nobody |
0-21052 5 hours ago |
0-21052 5 hours ago |
0-0 0 seconds |
| 25826 |
yuma-mizuno author:yuma-mizuno |
refactor(CategoryTheory/Monoidal): define `Mon_.Hom` using type class `IsMon_Hom` |
This PR changes
```lean
structure Mon_.Hom (M N : Mon_ C) where
hom : M.X ⟶ N.X
one_hom : η ≫ hom = η := by aesop_cat
mul_hom : μ ≫ hom = (hom ⊗ hom) ≫ μ := by aesop_cat
```
to
```lean
structure Mon_.Hom (M N : Mon_ C) where
hom : M.X ⟶ N.X
[is_mon_hom : IsMon_Hom hom]
```
and similarly for `Comon_.Hom`.
The discussion on Zulip: [#mathlib4 > Refactoring Mod_? @ 💬](https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/Refactoring.20Mod_.3F/near/522782252)
---
[](https://gitpod.io/from-referrer/)
---
*This PR continues the work from #25549.*
*Original PR: https://github.com/leanprover-community/mathlib4/pull/25549* |
t-category-theory |
208/172 |
Mathlib/Algebra/Category/CoalgCat/ComonEquivalence.lean,Mathlib/CategoryTheory/Monad/EquivMon.lean,Mathlib/CategoryTheory/Monoidal/Bimon_.lean,Mathlib/CategoryTheory/Monoidal/Cartesian/Comon_.lean,Mathlib/CategoryTheory/Monoidal/Cartesian/Mon_.lean,Mathlib/CategoryTheory/Monoidal/CommGrp_.lean,Mathlib/CategoryTheory/Monoidal/CommMon_.lean,Mathlib/CategoryTheory/Monoidal/Comon_.lean,Mathlib/CategoryTheory/Monoidal/Grp_.lean,Mathlib/CategoryTheory/Monoidal/Internal/FunctorCategory.lean,Mathlib/CategoryTheory/Monoidal/Internal/Limits.lean,Mathlib/CategoryTheory/Monoidal/Internal/Module.lean,Mathlib/CategoryTheory/Monoidal/Internal/Types/Basic.lean,Mathlib/CategoryTheory/Monoidal/Mod_.lean,Mathlib/CategoryTheory/Monoidal/Mon_.lean,Mathlib/CategoryTheory/Preadditive/CommGrp_.lean |
16 |
1 |
['github-actions'] |
nobody |
0-20104 5 hours ago |
0-21539 5 hours ago |
0-0 0 seconds |
| 25715 |
kbuzzard author:kbuzzard |
feat: more RestrictedProduct API |
A constructor, more algebra boilerplate (e.g. `SMul ℕ` on a restricted product of `AddMonoid`s, restricted product of `CommMonoid`s is a `CommMonoid`, restricted product of `R`-modules wrt `R`-submodules is an `R`-module, variant of `map` when the index set doesn't change.
From the FLT project.
---
[](https://gitpod.io/from-referrer/)
|
FLT
t-topology
|
66/4 |
Mathlib/Topology/Algebra/RestrictedProduct/Basic.lean |
1 |
2 |
['github-actions', 'matthewjasper'] |
nobody |
0-18462 5 hours ago |
1-8990 1 day ago |
0-0 0 seconds |
| 25728 |
acmepjz author:acmepjz |
feat(RingTheory/KrullDimension/PID): remove domain condition in `IsPrincipalIdealRing.krullDimLE_one` |
---
[](https://gitpod.io/from-referrer/)
Migrated from #25702 |
t-algebra
awaiting-CI
label:t-algebra$ |
15/5 |
Mathlib/RingTheory/KrullDimension/PID.lean |
1 |
2 |
['github-actions', 'kckennylau'] |
nobody |
0-17277 4 hours ago |
0-74271 20 hours ago |
0-0 0 seconds |
| 25828 |
euprunin author:euprunin |
feat: register more tactics for `hint` |
The following example shows test cases that `hint` now supports, which were unsupported prior to this PR:
```
import Mathlib
-- The tactics registered in this PR
register_hint compute_degree
register_hint field_simp
register_hint finiteness
-- "hint" now correctly suggests "compute_degree" which closes the goal (no closing tactic suggested prior to this PR)
open Polynomial in
example : natDegree ((X + 1) : Nat[X]) ≤ 1 := by hint
-- "hint" now correctly suggests "field_simp" which closes the goal (no closing tactic suggested prior to this PR)
example (R : Type) (a b : R) [CommRing R] (u₁ : Rˣ) : a /ₚ u₁ + b /ₚ u₁ = (a + b) /ₚ u₁ := by hint
-- "hint" now correctly suggests "finiteness" which closes the goal (no closing tactic suggested prior to this PR)
example (a : ℝ) : (ENNReal.ofReal (1 + a ^ 2))⁻¹ < ⊤ := by hint
``` |
t-meta |
15/0 |
Mathlib/Tactic/ComputeDegree.lean,Mathlib/Tactic/FieldSimp.lean,Mathlib/Tactic/Finiteness.lean |
3 |
1 |
['github-actions'] |
nobody |
0-14419 4 hours ago |
0-14435 4 hours ago |
0-0 0 seconds |
| 25792 |
erdOne author:erdOne |
feat(NumberTheory): discriminant is norm of different |
---
[](https://gitpod.io/from-referrer/)
---
|
|
289/0 |
Mathlib.lean,Mathlib/LinearAlgebra/Span/Basic.lean,Mathlib/NumberTheory/NumberField/Discriminant/Different.lean,Mathlib/RingTheory/DedekindDomain/Factorization.lean,Mathlib/RingTheory/DedekindDomain/Ideal.lean,Mathlib/RingTheory/FractionalIdeal/Basic.lean |
6 |
1 |
['github-actions'] |
riccardobrasca assignee:riccardobrasca |
0-12467 3 hours ago |
0-56129 15 hours ago |
0-0 0 seconds |
| 25820 |
euprunin author:euprunin |
chore: rename test of `Mathlib.Tactic.ClearExclamation` (from `Clear!.lean` to `ClearExclamation.lean`) |
Some context:
* filename Clear!.lean contains illegal character "!" (#1212)
* chore(Mathlib/Tactic/Clear!): rename `Clear!.lean` to `ClearExclamation.lean` to avoid the illegal character `!` (#12757)
This PR renames `MathlibTest/Clear!.lean` to `MathlibTest/ClearExclamation.lean` to avoid shell quoting issues caused by the `!` character in file names.
For example:
```
% ls -l MathlibTest/Clear!.lean
zsh: event not found: .lean
% ls -l "MathlibTest/Clear!.lean"
zsh: event not found: .lean
```
See issue #1212 for some additional context.
---
[](https://gitpod.io/from-referrer/)
|
file-removed
maintainer-merge
|
0/0 |
MathlibTest/ClearExclamation.lean |
1 |
3 |
['github-actions', 'grunweg'] |
nobody |
0-12054 3 hours ago |
0-12054 3 hours ago |
0-0 0 seconds |
| 25817 |
Vierkantor author:Vierkantor |
cache: change working directory when running the post-update hook |
`lake exe cache` expects to run in the root package directory that includes the lakefile and `.lake` folder. The Lake update hook isn't always run from that position (for example if it is run as part of a more complicated Lake command), so change directories when calling into the executable.
The assumption that the command is run from the working directory is so pervasive that we'd need to touch a lot of Cache in order to get rid of it. I think it's better to accept this as a design decision.
---
[](https://gitpod.io/from-referrer/)
|
maintainer-merge |
8/1 |
lakefile.lean |
1 |
3 |
['github-actions', 'grunweg'] |
nobody |
0-11987 3 hours ago |
0-11987 3 hours ago |
0-0 0 seconds |
| 25811 |
plp127 author:plp127 |
fix(Tactic/DeprecateTo): get date from Lean |
Fixes an issue I encountered on windows where `IO.Process.run { cmd := "date", args := #["-I"] }` exits with an error `no such file or directory (error code: 2)`, making this tactic unusable.
---
[](https://gitpod.io/from-referrer/)
|
large-import
maintainer-merge
t-meta
|
7/3 |
Mathlib/Tactic/DeprecateTo.lean |
1 |
3 |
['github-actions', 'grunweg'] |
nobody |
0-11892 3 hours ago |
0-11892 3 hours ago |
0-0 0 seconds |
| 25829 |
kbuzzard author:kbuzzard |
feat: add mulEquivHaarChar |
API for the positive real factor by which an continuous multiplicative equivalence scales a regular Haar measure on a locally compact topological group.
From FLT.
---
[](https://gitpod.io/from-referrer/)
|
t-measure-probability |
158/0 |
Mathlib.lean,Mathlib/MeasureTheory/Group/Measure.lean,Mathlib/MeasureTheory/Measure/Haar/MulEquivHaarChar.lean,Mathlib/MeasureTheory/Measure/Haar/Unique.lean |
4 |
1 |
['github-actions'] |
nobody |
0-8506 2 hours ago |
0-9470 2 hours ago |
0-0 0 seconds |
| 25770 |
Parcly-Taxel author:Parcly-Taxel |
chore: fix more induction/recursor branch names |
These were found using the regex `\| h. =>` and `def.*rec.*\(h. :`. |
tech debt |
131/112 |
Mathlib/Analysis/Convolution.lean,Mathlib/Data/ENat/Basic.lean,Mathlib/Data/Fin/Tuple/Basic.lean,Mathlib/Data/Fin/Tuple/NatAntidiagonal.lean,Mathlib/Data/Nat/Factorization/Induction.lean,Mathlib/Data/Seq/Computation.lean,Mathlib/Data/Set/Card.lean,Mathlib/Data/WSeq/Basic.lean,Mathlib/FieldTheory/KummerExtension.lean,Mathlib/Logic/Function/Iterate.lean,Mathlib/NumberTheory/ArithmeticFunction.lean,Mathlib/NumberTheory/SumFourSquares.lean,Mathlib/NumberTheory/SumTwoSquares.lean,Mathlib/Order/Synonym.lean |
14 |
5 |
['Parcly-Taxel', 'eric-wieser', 'github-actions'] |
nobody |
0-5322 1 hour ago |
0-60125 16 hours ago |
0-0 0 seconds |
| 3610 |
TimothyGu author:TimothyGu |
feat: derive Infinite automatically for inductive types |
Deals with recursive types, but not mutually recursive types or types with indices right now. See docstring for details.
---
[](https://gitpod.io/from-referrer/)
|
t-meta
merge-conflict
awaiting-author
|
517/0 |
Mathlib.lean,Mathlib/Tactic/DeriveInfinite.lean,test/DeriveInfinite.lean |
3 |
11 |
['TimothyGu', 'digama0', 'eric-wieser', 'grunweg', 'kim-em', 'kmill'] |
kmill assignee:kmill |
158-77225 5 months ago |
158-77225 5 months ago |
0-0 0 seconds |
| 25749 |
Rob23oba author:Rob23oba |
chore: lint `show` (adaptation for leanprover/lean4#7395) |
Adds `show` as an exception to the unused tactic linter and adds a separate linter for `show`s that should be replaced by `change`.
Context: https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/unused.20tactic.20linter.20for.20.60show.60/with/523701633 |
new-contributor
merge-conflict
|
696/600 |
Counterexamples/DiscreteTopologyNonDiscreteUniformity.lean,Mathlib/Algebra/Algebra/NonUnitalSubalgebra.lean,Mathlib/Algebra/Algebra/Operations.lean,Mathlib/Algebra/Algebra/Subalgebra/Operations.lean,Mathlib/Algebra/Algebra/Subalgebra/Pointwise.lean,Mathlib/Algebra/Algebra/Unitization.lean,Mathlib/Algebra/Algebra/ZMod.lean,Mathlib/Algebra/BigOperators/Fin.lean,Mathlib/Algebra/Category/ModuleCat/Topology/Basic.lean,Mathlib/Algebra/Category/ModuleCat/Topology/Homology.lean,Mathlib/Algebra/Category/Ring/Epi.lean,Mathlib/Algebra/Colimit/Module.lean,Mathlib/Algebra/DirectSum/Algebra.lean,Mathlib/Algebra/DirectSum/Ring.lean,Mathlib/Algebra/DualNumber.lean,Mathlib/Algebra/Equiv/TransferInstance.lean,Mathlib/Algebra/Group/Action/Basic.lean,Mathlib/Algebra/Group/End.lean,Mathlib/Algebra/Group/Subgroup/Basic.lean,Mathlib/Algebra/GroupWithZero/Action/Defs.lean,Mathlib/Algebra/GroupWithZero/NonZeroDivisors.lean,Mathlib/Algebra/Lie/CartanExists.lean,Mathlib/Algebra/Lie/LieTheorem.lean,Mathlib/Algebra/Lie/Weights/RootSystem.lean,Mathlib/Algebra/Module/FinitePresentation.lean,Mathlib/Algebra/MonoidAlgebra/Defs.lean,Mathlib/Algebra/MonoidAlgebra/ToDirectSum.lean,Mathlib/Algebra/MvPolynomial/Basic.lean,Mathlib/Algebra/MvPolynomial/Equiv.lean,Mathlib/Algebra/MvPolynomial/Eval.lean,Mathlib/Algebra/MvPolynomial/Variables.lean,Mathlib/Algebra/Order/CauSeq/Completion.lean,Mathlib/Algebra/Order/Ring/Unbundled/Rat.lean,Mathlib/Algebra/Polynomial/Degree/CardPowDegree.lean,Mathlib/Algebra/Polynomial/HasseDeriv.lean,Mathlib/Algebra/Ring/CentroidHom.lean,Mathlib/Algebra/Ring/GrindInstances.lean,Mathlib/Algebra/RingQuot.lean,Mathlib/Algebra/Star/NonUnitalSubalgebra.lean,Mathlib/Algebra/Star/NonUnitalSubsemiring.lean,Mathlib/AlgebraicGeometry/AffineScheme.lean,Mathlib/AlgebraicGeometry/AffineSpace.lean,Mathlib/AlgebraicGeometry/GammaSpecAdjunction.lean,Mathlib/AlgebraicGeometry/IdealSheaf/Basic.lean,Mathlib/AlgebraicGeometry/IdealSheaf/Subscheme.lean,Mathlib/AlgebraicGeometry/Limits.lean,Mathlib/AlgebraicGeometry/Modules/Tilde.lean,Mathlib/AlgebraicGeometry/Morphisms/Affine.lean,Mathlib/AlgebraicGeometry/Morphisms/AffineAnd.lean,Mathlib/AlgebraicGeometry/Morphisms/Basic.lean,Mathlib/AlgebraicGeometry/Morphisms/ClosedImmersion.lean,Mathlib/AlgebraicGeometry/Morphisms/Constructors.lean,Mathlib/AlgebraicGeometry/Morphisms/Finite.lean,Mathlib/AlgebraicGeometry/Morphisms/FinitePresentation.lean,Mathlib/AlgebraicGeometry/Morphisms/Immersion.lean,Mathlib/AlgebraicGeometry/Morphisms/Integral.lean,Mathlib/AlgebraicGeometry/Morphisms/QuasiCompact.lean,Mathlib/AlgebraicGeometry/Morphisms/QuasiSeparated.lean,Mathlib/AlgebraicGeometry/Morphisms/RingHomProperties.lean,Mathlib/AlgebraicGeometry/Morphisms/Separated.lean,Mathlib/AlgebraicGeometry/Morphisms/UniversallyOpen.lean,Mathlib/AlgebraicGeometry/ProjectiveSpectrum/Basic.lean,Mathlib/AlgebraicGeometry/ProjectiveSpectrum/Proper.lean,Mathlib/AlgebraicGeometry/ProjectiveSpectrum/Scheme.lean,Mathlib/AlgebraicGeometry/ProjectiveSpectrum/StructureSheaf.lean,Mathlib/AlgebraicGeometry/Properties.lean,Mathlib/AlgebraicGeometry/Pullbacks.lean,Mathlib/AlgebraicGeometry/RationalMap.lean,Mathlib/AlgebraicGeometry/Restrict.lean,Mathlib/AlgebraicGeometry/Scheme.lean,Mathlib/AlgebraicGeometry/Spec.lean,Mathlib/AlgebraicGeometry/SpreadingOut.lean,Mathlib/AlgebraicGeometry/ValuativeCriterion.lean,Mathlib/AlgebraicTopology/SimplexCategory/Basic.lean,Mathlib/AlgebraicTopology/SimplicialSet/Basic.lean,Mathlib/AlgebraicTopology/SimplicialSet/HomotopyCat.lean,Mathlib/AlgebraicTopology/SimplicialSet/NerveAdjunction.lean,Mathlib/Analysis/Analytic/Composition.lean,Mathlib/Analysis/BoxIntegral/Integrability.lean,Mathlib/Analysis/CStarAlgebra/ApproximateUnit.lean,Mathlib/Analysis/CStarAlgebra/ContinuousFunctionalCalculus/Basic.lean,Mathlib/Analysis/CStarAlgebra/ContinuousFunctionalCalculus/Continuity.lean,Mathlib/Analysis/CStarAlgebra/ContinuousFunctionalCalculus/Isometric.lean,Mathlib/Analysis/Calculus/FDeriv/Equiv.lean,Mathlib/Analysis/Calculus/TangentCone.lean,Mathlib/Analysis/Complex/Tietze.lean,Mathlib/Analysis/Complex/UpperHalfPlane/MoebiusAction.lean,Mathlib/Analysis/Fourier/AddCircle.lean,Mathlib/Analysis/Fourier/AddCircleMulti.lean,Mathlib/Analysis/InnerProductSpace/Projection.lean,Mathlib/Analysis/MellinInversion.lean,Mathlib/Analysis/MellinTransform.lean,Mathlib/Analysis/Normed/Lp/lpSpace.lean,Mathlib/Analysis/NormedSpace/MStructure.lean,Mathlib/Analysis/SpecialFunctions/Exponential.lean,Mathlib/Analysis/SpecialFunctions/Gamma/Beta.lean,Mathlib/Analysis/SpecialFunctions/Gamma/BohrMollerup.lean,Mathlib/Analysis/SpecificLimits/Normed.lean,Mathlib/CategoryTheory/Action/Concrete.lean,Mathlib/CategoryTheory/Action/Continuous.lean |
327 |
0 |
[] |
nobody |
0-35470 9 hours ago |
0-63401 17 hours ago |
0-0 0 seconds |
| 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 |
| 23866 |
kim-em author:kim-em |
chore: remove `[AtLeastTwo n]` hypothesis from the `NatCast` to `OfNat` instance |
This PR observes that we can change
```
instance (priority := 100) instOfNatAtLeastTwo {n : ℕ} [NatCast R] [Nat.AtLeastTwo n] : OfNat R n
```
to
```
instance (priority := 100) instOfNatAtLeastTwo {n : ℕ} [NatCast R] : OfNat R n
```
with minimal fall-out.
A follow-up PR #23867 then observes that we can remove nearly all the `[Nat.AtLeastTwo n]` hypotheses in Mathlib.
This is slightly dangerous -- it does make it more likely that we'll generate non-defeq instances, but it appears to happen very rarely.
However, it will make life slightly easier for something Leo and I are trying to do with `grind` and Grobner bases (we'd like to be able to assume types we consume have `[∀ n, OfNat α n]`, which is possible with this change, but not without...).
Zulip thread: [#PR reviews > #23866 and #23867, removing most `[Nat.AtLeastTwo n]` @ 💬](https://leanprover.zulipchat.com/#narrow/channel/144837-PR-reviews/topic/.2323866.20and.20.2323867.2C.20removing.20most.20.60.5BNat.2EAtLeastTwo.20n.5D.60/near/511157297) |
awaiting-zulip |
21/26 |
Mathlib/AlgebraicTopology/FundamentalGroupoid/Basic.lean,Mathlib/Data/Nat/Cast/Defs.lean,Mathlib/Data/Nat/Cast/Order/Basic.lean |
3 |
3 |
['eric-wieser', 'github-actions', 'urkud'] |
nobody |
64-24847 2 months ago |
64-24936 2 months ago |
0-23929 6 hours |
| 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/)
|
awaiting-zulip
t-computability
new-contributor
awaiting-author
|
298/0 |
Mathlib.lean,Mathlib/Computability/GNFA.lean,Mathlib/Computability/Language.lean,Mathlib/Computability/RegularExpressions.lean,docs/references.bib |
5 |
6 |
['github-actions', 'mathlib4-dependent-issues-bot', 'meithecatte', 'trivial1711'] |
nobody |
38-12324 1 month ago |
38-12333 1 month 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/)
|
awaiting-zulip
t-computability
new-contributor
|
490/0 |
Mathlib.lean,Mathlib/Computability/RegularExpressionsToEpsilonNFA.lean,docs/references.bib |
3 |
5 |
['github-actions', 'mathlib4-dependent-issues-bot', 'meithecatte', 'qawbecrdtey'] |
nobody |
38-11635 1 month ago |
38-12270 1 month ago |
75-77754 75 days |
| 23048 |
scholzhannah author:scholzhannah |
feat: PartialEquiv on closed sets restricts to closed map |
This PR shows that a PartialEquiv that is continuous on both source and target restricts to a homeomorphism. It then uses that to show that a PartialEquiv with closed source and target and which is continuous on both the source and target restricts to a closed map.
---
See [this Zulip discussion](https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/Generalizing.20.60PartialHomeomorph.60.3F) that will probably mean that I close this PR.
I need the latter statement to prove that one can transport a CW complex along a PartialEquiv. I had trouble finding a good spot for these statements; I hope this solution works.
[](https://gitpod.io/from-referrer/)
|
awaiting-zulip
t-topology
|
53/0 |
Mathlib.lean,Mathlib/Topology/PartialEquiv.lean |
2 |
3 |
['ADedecker', 'github-actions', 'scholzhannah'] |
ADedecker assignee:ADedecker |
30-36219 30 days ago |
34-42995 1 month ago |
51-86236 51 days |
| 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/)
|
awaiting-zulip
t-algebra
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 |
11 |
['MichaelStollBayreuth', 'acmepjz', 'eric-wieser', 'github-actions', 'leanprover-bot', 'urkud'] |
nobody |
24-84685 24 days ago |
25-18712 25 days ago |
0-66650 18 hours |
| 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/)
|
awaiting-zulip
t-computability
new-contributor
awaiting-author
|
159/0 |
Mathlib/Computability/DFA.lean,Mathlib/Computability/Language.lean |
2 |
59 |
['EtienneC30', 'YaelDillies', 'github-actions', 'maemre', 'meithecatte', 'urkud'] |
EtienneC30 assignee:EtienneC30 |
8-64495 8 days ago |
38-12234 1 month ago |
48-67492 48 days |
| 25218 |
kckennylau author:kckennylau |
feat(AlgebraicGeometry): Tate normal form of elliptic curves |
---
[](https://gitpod.io/from-referrer/)
|
awaiting-zulip
new-contributor
t-algebraic-geometry
|
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 |
29 |
['MichaelStollBayreuth', 'Multramate', 'acmepjz', 'github-actions', 'grunweg', 'kckennylau'] |
nobody |
7-14176 7 days ago |
10-52988 10 days ago |
6-51040 6 days |
| 23929 |
meithecatte author:meithecatte |
feat(Computability/NFA): improve bound on pumping lemma |
---
- [x] depends on: #25321
[](https://gitpod.io/from-referrer/)
|
awaiting-zulip
t-computability
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 |
5-21886 5 days ago |
5-21887 5 days ago |
34-10595 34 days |
| 23658 |
grunweg author:grunweg |
feat: require that real or complex models with corners have convex interior |
Follow-up to #18403.
---
- [x] depends on: #23657
- [x] depends on: #25808
- [x] depends on: #25809
[](https://gitpod.io/from-referrer/)
|
awaiting-zulip
t-differential-geometry
WIP
|
116/18 |
Mathlib/Geometry/Manifold/Instances/Real.lean,Mathlib/Geometry/Manifold/IsManifold/Basic.lean |
2 |
9 |
['github-actions', 'grunweg', 'mathlib4-dependent-issues-bot', 'sgouezel'] |
nobody |
0-25240 7 hours ago |
0-38942 10 hours ago |
0-9 9 seconds |
| 25824 |
sgouezel author:sgouezel |
feat: require that the range of a real or complex model with corners is convex |
This is important to ensure that the distance coming from a Riemannian metric generates the same topology as the original one.
See Zulip discussion at [#mathlib4 > Fixing the definition of models with corners @ 💬](https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/Fixing.20the.20definition.20of.20models.20with.20corners/near/522572964)
---
[](https://gitpod.io/from-referrer/)
|
large-import
awaiting-zulip
t-differential-geometry
|
164/63 |
Mathlib/Geometry/Manifold/Diffeomorph.lean,Mathlib/Geometry/Manifold/Instances/Real.lean,Mathlib/Geometry/Manifold/IsManifold/Basic.lean |
3 |
2 |
['github-actions', 'grunweg'] |
nobody |
0-12142 3 hours ago |
0-12142 3 hours ago |
0-13134 3 hours |
| 11800 |
JADekker author:JADekker |
feat : Define 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/)
|
awaiting-zulip
t-topology
merge-conflict
please-adopt
|
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 |
269-75757 8 months ago |
270-11332 8 months ago |
119-10687 119 days |
| 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 |
awaiting-zulip
t-linter
merge-conflict
blocked-by-other-PR
|
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 |
222-29476 7 months ago |
248-17998 8 months ago* |
0-0 0 seconds* |
| 17623 |
FR-vdash-bot author:FR-vdash-bot |
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/)
|
awaiting-zulip
t-order
t-algebra
merge-conflict
label:t-algebra$ |
146/44 |
Mathlib/Algebra/Order/GroupWithZero/Canonical.lean,Mathlib/Algebra/Order/GroupWithZero/Unbundled.lean |
2 |
11 |
['FR-vdash-bot', 'YaelDillies', 'github-actions', 'j-loreaux'] |
nobody |
204-49007 6 months ago |
204-49007 6 months ago |
33-64877 33 days |
| 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 |
awaiting-zulip
t-analysis
merge-conflict
|
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 |
49-4384 1 month ago |
60-33014 1 month ago |
29-60989 29 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/)
|
awaiting-zulip
t-computability
new-contributor
merge-conflict
blocked-by-other-PR
|
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 |
38-12284 1 month ago |
38-12289 1 month ago |
0-179 2 minutes |
| 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/)
|
awaiting-zulip
t-computability
new-contributor
merge-conflict
awaiting-author
|
307/5 |
Mathlib/Computability/NFA.lean |
1 |
15 |
['TpmKranz', 'YaelDillies', 'dupuisf', 'github-actions', 'leanprover-community-bot-assistant', 'meithecatte'] |
nobody |
24-34890 24 days ago |
24-34891 24 days ago |
45-84611 45 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/)
|
awaiting-zulip
t-computability
new-contributor
merge-conflict
awaiting-author
|
218/2 |
Mathlib/Computability/Language.lean,Mathlib/Computability/NFA.lean |
2 |
90 |
['EtienneC30', 'b-mehta', 'github-actions', 'leanprover-community-bot-assistant', 'meithecatte', 'rudynicolop'] |
EtienneC30 assignee:EtienneC30 |
24-33964 24 days ago |
24-33966 24 days ago |
39-67601 39 days |
| 24409 |
urkud author:urkud |
chore(*): fix `nmem` vs `not_mem` names |
---
There are some missing/buggy deprecations, I'm going to fix them later today or tomorrow.
[](https://gitpod.io/from-referrer/)
|
awaiting-zulip
tech debt
merge-conflict
delegated
awaiting-author
|
317/176 |
Mathlib/Algebra/BigOperators/Finprod.lean,Mathlib/Algebra/BigOperators/Group/Finset/Lemmas.lean,Mathlib/Algebra/Group/Indicator.lean,Mathlib/Algebra/Group/Support.lean,Mathlib/Algebra/GroupWithZero/NonZeroDivisors.lean,Mathlib/Algebra/Order/Group/Indicator.lean,Mathlib/Algebra/Polynomial/AlgebraMap.lean,Mathlib/Algebra/Polynomial/Degree/Operations.lean,Mathlib/Analysis/Calculus/BumpFunction/Basic.lean,Mathlib/Analysis/Calculus/DSlope.lean,Mathlib/Analysis/Calculus/Deriv/Basic.lean,Mathlib/Analysis/Calculus/Deriv/Support.lean,Mathlib/Analysis/Calculus/FDeriv/Basic.lean,Mathlib/Analysis/Calculus/Rademacher.lean,Mathlib/Analysis/Complex/RemovableSingularity.lean,Mathlib/Analysis/Convex/Cone/InnerDual.lean,Mathlib/Analysis/Convex/Cone/Proper.lean,Mathlib/Analysis/Convolution.lean,Mathlib/Analysis/Distribution/AEEqOfIntegralContDiff.lean,Mathlib/Data/LocallyFinsupp.lean,Mathlib/Data/Set/Basic.lean,Mathlib/Data/Set/Insert.lean,Mathlib/Dynamics/Ergodic/Conservative.lean,Mathlib/Dynamics/Ergodic/Ergodic.lean,Mathlib/Dynamics/Ergodic/Function.lean,Mathlib/Dynamics/PeriodicPts/Defs.lean,Mathlib/Geometry/Manifold/ContMDiff/Basic.lean,Mathlib/Geometry/Manifold/PartitionOfUnity.lean,Mathlib/GroupTheory/CosetCover.lean,Mathlib/LinearAlgebra/Dual/Lemmas.lean,Mathlib/LinearAlgebra/FreeModule/PID.lean,Mathlib/LinearAlgebra/PID.lean,Mathlib/LinearAlgebra/RootSystem/Base.lean,Mathlib/LinearAlgebra/RootSystem/Finite/Lemmas.lean,Mathlib/MeasureTheory/Function/ContinuousMapDense.lean,Mathlib/MeasureTheory/Function/ConvergenceInMeasure.lean,Mathlib/MeasureTheory/Function/L2Space.lean,Mathlib/MeasureTheory/Function/LocallyIntegrable.lean,Mathlib/MeasureTheory/Function/LpSpace/Indicator.lean,Mathlib/MeasureTheory/Integral/Average.lean,Mathlib/MeasureTheory/Integral/Bochner/Set.lean,Mathlib/MeasureTheory/Integral/Layercake.lean,Mathlib/MeasureTheory/Integral/Lebesgue/Add.lean,Mathlib/MeasureTheory/Integral/Lebesgue/Basic.lean,Mathlib/MeasureTheory/Integral/RieszMarkovKakutani/Basic.lean,Mathlib/MeasureTheory/Integral/RieszMarkovKakutani/Real.lean,Mathlib/MeasureTheory/Measure/AbsolutelyContinuous.lean,Mathlib/MeasureTheory/Measure/AddContent.lean,Mathlib/MeasureTheory/Measure/DiracProba.lean,Mathlib/MeasureTheory/Measure/Haar/Unique.lean,Mathlib/MeasureTheory/Measure/Restrict.lean,Mathlib/MeasureTheory/Measure/WithDensity.lean,Mathlib/MeasureTheory/OuterMeasure/AE.lean,Mathlib/MeasureTheory/SetSemiring.lean,Mathlib/Order/Filter/AtTopBot/CountablyGenerated.lean,Mathlib/Order/Filter/Cocardinal.lean,Mathlib/Order/Filter/Cofinite.lean,Mathlib/Order/Filter/Tendsto.lean,Mathlib/Order/Filter/Ultrafilter/Basic.lean,Mathlib/Probability/Distributions/Uniform.lean,Mathlib/Probability/Kernel/Basic.lean,Mathlib/Probability/Kernel/Composition/MeasureCompProd.lean,Mathlib/RingTheory/AdicCompletion/LocalRing.lean,Mathlib/RingTheory/Ideal/Maximal.lean,Mathlib/RingTheory/LaurentSeries.lean,Mathlib/RingTheory/MvPolynomial/Symmetric/NewtonIdentities.lean,Mathlib/RingTheory/MvPowerSeries/NoZeroDivisors.lean,Mathlib/RingTheory/Spectrum/Maximal/Localization.lean,Mathlib/RingTheory/Spectrum/Prime/RingHom.lean,Mathlib/RingTheory/Spectrum/Prime/Topology.lean,Mathlib/Topology/Algebra/InfiniteSum/Group.lean,Mathlib/Topology/Algebra/Module/Cardinality.lean,Mathlib/Topology/Algebra/Support.lean,Mathlib/Topology/Bases.lean,Mathlib/Topology/ContinuousMap/BoundedCompactlySupported.lean,Mathlib/Topology/Order/Basic.lean,Mathlib/Topology/UrysohnsLemma.lean |
77 |
4 |
['b-mehta', 'github-actions', 'jcommelin', 'leanprover-community-bot-assistant', 'mathlib-bors'] |
nobody |
10-69862 10 days ago |
10-69862 10 days ago |
0-55045 15 hours |
| 24396 |
JovanGerb author:JovanGerb |
feat(Order/Defs): refactor in preparation of `to_dual` attribute |
When the `to_dual` attribute lands in Mathlib, we will tag many lemmas about order with this tag, which will automatically give us the dual statements. This PR prepares for this by
- moving dual declarations closer together
- replacing occurrences of `>` and `≥` with `<` and `≤`
- consistently applying a new naming convention that helps us to name dual lemmas: we use the keywords `ge` and `gt` in place of `le` and `lt` to indicate that the same pair `a, b` in `a < b` is in the opposite order to the order in which it appeared the first time.
- when we have to disambiguate the order of the argument to `<` or `≤`, we sometimes use `gt` or `ge` instead of `lt` or `le`. We also use this to get rid of many primed lemma names.
This is a copy of #24376, but it doesn't remove the old lemma names, so doesn't require making changes in >500 files. deprecating these lemmas will be left to a future PR.
[#mathlib4 > naming convention for ≤ and <](https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/naming.20convention.20for.20.E2.89.A4.20and.20.3C)
---
[](https://gitpod.io/from-referrer/)
|
awaiting-zulip
t-order
merge-conflict
|
248/230 |
Mathlib/Algebra/Order/CauSeq/Basic.lean,Mathlib/Algebra/Order/Ring/Unbundled/Rat.lean,Mathlib/Algebra/Polynomial/Degree/Domain.lean,Mathlib/Algebra/Tropical/Basic.lean,Mathlib/Analysis/SpecialFunctions/Pow/Continuity.lean,Mathlib/Analysis/SpecialFunctions/Trigonometric/Arctan.lean,Mathlib/Computability/TuringMachine.lean,Mathlib/Data/Bool/Basic.lean,Mathlib/Data/Char.lean,Mathlib/Data/Complex/Order.lean,Mathlib/Data/ENat/Basic.lean,Mathlib/Data/Int/Order/Basic.lean,Mathlib/Data/Nat/Basic.lean,Mathlib/Data/Nat/Factorization/Defs.lean,Mathlib/Data/Nat/Find.lean,Mathlib/Data/Nat/PartENat.lean,Mathlib/Data/Num/Lemmas.lean,Mathlib/Data/Num/ZNum.lean,Mathlib/Data/PSigma/Order.lean,Mathlib/Data/Prod/Lex.lean,Mathlib/Data/Real/Basic.lean,Mathlib/Data/Setoid/Basic.lean,Mathlib/Data/Setoid/Partition.lean,Mathlib/Data/Sigma/Order.lean,Mathlib/Data/String/Basic.lean,Mathlib/Data/Sum/Order.lean,Mathlib/GroupTheory/MonoidLocalization/Order.lean,Mathlib/NumberTheory/Zsqrtd/Basic.lean,Mathlib/Order/Antisymmetrization.lean,Mathlib/Order/Basic.lean,Mathlib/Order/Booleanisation.lean,Mathlib/Order/Defs/LinearOrder.lean,Mathlib/Order/Defs/PartialOrder.lean,Mathlib/Order/RelClasses.lean,Mathlib/Order/WithBot.lean,Mathlib/Probability/Martingale/Upcrossing.lean,Mathlib/RingTheory/UniqueFactorizationDomain/Multiplicity.lean,Mathlib/SetTheory/Game/Basic.lean,Mathlib/SetTheory/Ordinal/Basic.lean,Mathlib/SetTheory/Ordinal/Notation.lean,Mathlib/SetTheory/Surreal/Basic.lean,Mathlib/Tactic/Linarith/Frontend.lean,MathlibTest/linarith.lean |
43 |
5 |
['JovanGerb', 'bryangingechen', 'github-actions', 'leanprover-community-bot-assistant'] |
bryangingechen assignee:bryangingechen |
10-31964 10 days ago |
10-31966 10 days ago |
5-75236 5 days |