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 |
19-36553 19 days ago |
19-36554 19 days ago |
28-41150 28 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 |
9-42165 9 days ago |
10-26745 10 days ago |
17-23952 17 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 |
8-33812 8 days ago |
31-45505 1 month ago* |
44-50226 44 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 |
8-25272 8 days ago |
11-5244 11 days ago |
15-14863 15 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 |
8-19315 8 days ago |
19-29294 19 days ago |
19-70167 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 |
6-39578 6 days ago |
6-40125 6 days ago |
13-1155 13 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 |
6-4078 6 days ago |
6-4078 6 days ago |
19-69901 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 |
5-45234 5 days ago |
5-45234 5 days ago |
6-20767 6 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 |
5-15680 5 days ago |
5-81464 5 days ago |
48-9034 48 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-82351 4 days ago |
4-82351 4 days ago |
5-7839 5 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 |
3-57736 3 days ago |
3-57736 3 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 |
3-33799 3 days ago |
3-33799 3 days ago |
65-47590 65 days |
| 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 |
1-28624 1 day ago |
1-41877 1 day ago |
20-4708 20 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 |
1-5719 1 day ago |
1-5719 1 day 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-82921 1 month ago |
84-61548 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 |
10-65889 10 days ago |
10-65890 10 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 |
6-50107 6 days ago |
6-50107 6 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 |
19-36553 19 days ago |
19-36554 19 days ago |
28-41150 28 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 |
9-42165 9 days ago |
10-26745 10 days ago |
17-23952 17 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 |
8-33812 8 days ago |
31-45505 1 month ago* |
44-50226 44 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 |
8-25272 8 days ago |
11-5244 11 days ago |
15-14863 15 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 |
8-19315 8 days ago |
19-29294 19 days ago |
19-70167 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 |
6-39578 6 days ago |
6-40125 6 days ago |
13-1155 13 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 |
6-4078 6 days ago |
6-4078 6 days ago |
19-69901 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 |
5-45234 5 days ago |
5-45234 5 days ago |
6-20767 6 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 |
5-15680 5 days ago |
5-81464 5 days ago |
48-9034 48 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-82351 4 days ago |
4-82351 4 days ago |
5-7839 5 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 |
3-57736 3 days ago |
3-57736 3 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 |
3-33799 3 days ago |
3-33799 3 days ago |
65-47590 65 days |
| 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 |
1-28624 1 day ago |
1-41877 1 day ago |
20-4708 20 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 |
1-5719 1 day ago |
1-5719 1 day ago |
0-0 0 seconds |
| 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-80961 22 hours ago |
7-85132 7 days ago |
14-64515 14 days |
| 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-80691 22 hours ago |
0-80691 22 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
auto-merge-after-CI
t-meta
|
6/3 |
Mathlib/Tactic/DeprecateTo.lean |
1 |
5 |
['adomani', 'github-actions', 'grunweg', 'mathlib-bors'] |
nobody |
0-28342 7 hours ago |
0-28400 7 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/)
|
maintainer-merge
t-measure-probability
t-analysis
|
116/0 |
Mathlib.lean,Mathlib/Analysis/Normed/Operator/LinearIsometry.lean,Mathlib/MeasureTheory/Integral/IntervalIntegral/ContDiff.lean |
3 |
11 |
['github-actions', 'grunweg', 'sgouezel'] |
grunweg assignee:grunweg |
0-21137 5 hours ago |
0-39142 10 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-82921 1 month ago |
84-61548 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 |
10-65889 10 days ago |
10-65890 10 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 |
6-50107 6 days ago |
6-50107 6 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 |
67-24717 2 months ago |
67-24717 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-83899 1 month ago |
56-83899 1 month 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 |
1-60045 1 day ago |
1-60052 1 day 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 |
1-52543 1 day ago |
1-53634 1 day 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 |
1-49277 1 day ago |
1-49351 1 day 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 |
1-49100 1 day ago |
1-49229 1 day 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 |
1-47404 1 day ago |
1-47404 1 day 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 |
1-46498 1 day ago |
1-47198 1 day 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 |
1-46498 1 day ago |
1-47357 1 day 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 |
1-46496 1 day ago |
1-46497 1 day 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 |
1-46495 1 day ago |
1-47744 1 day 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 |
1-46494 1 day ago |
1-48360 1 day 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 |
1-44715 1 day ago |
1-44784 1 day 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 |
1-43652 1 day ago |
1-44387 1 day 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 |
1-43569 1 day ago |
1-43642 1 day 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 |
1-43324 1 day ago |
1-43391 1 day 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 |
1-42464 1 day ago |
1-42530 1 day 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 |
1-42324 1 day ago |
1-42397 1 day 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 |
1-41805 1 day ago |
1-43863 1 day 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 |
1-41804 1 day ago |
1-43944 1 day 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 |
1-41803 1 day ago |
1-41804 1 day 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 |
1-40152 1 day ago |
1-40214 1 day 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 |
1-39878 1 day ago |
1-39943 1 day 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 |
1-39810 1 day ago |
1-39868 1 day 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 |
1-39722 1 day ago |
1-40155 1 day 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 |
1-39376 1 day ago |
1-39440 1 day 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 |
1-39142 1 day ago |
1-48832 1 day 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 |
1-39141 1 day ago |
1-39209 1 day 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 |
1-38398 1 day ago |
1-38497 1 day 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 |
1-37185 1 day ago |
1-37257 1 day 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 |
1-37027 1 day ago |
1-37092 1 day 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 |
1-36624 1 day ago |
1-36690 1 day 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 |
1-36576 1 day ago |
1-39030 1 day 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 |
1-36563 1 day ago |
1-36564 1 day 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 |
1-35557 1 day ago |
1-35574 1 day 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 |
1-34727 1 day ago |
1-37037 1 day 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 |
1-34015 1 day ago |
1-39526 1 day 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 |
1-33037 1 day ago |
1-33109 1 day 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 |
1-28071 1 day ago |
1-28071 1 day 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 |
1-27603 1 day ago |
1-34302 1 day 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 |
1-26367 1 day ago |
1-40604 1 day 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 |
1-26105 1 day ago |
1-39058 1 day 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 |
1-25015 1 day ago |
1-39062 1 day 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 |
1-24838 1 day ago |
1-24839 1 day 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 |
1-24400 1 day ago |
1-61269 1 day 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 |
1-23510 1 day ago |
1-24054 1 day 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 |
1-21647 1 day ago |
1-21650 1 day 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 |
1-19869 1 day ago |
1-19869 1 day 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 |
1-16547 1 day ago |
1-16547 1 day 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 |
1-13033 1 day ago |
1-13033 1 day 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 |
1-5719 1 day ago |
1-5719 1 day 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 |
1-3357 1 day ago |
1-3535 1 day 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 |
1-3356 1 day ago |
1-3356 1 day 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 |
1-2408 1 day ago |
1-3843 1 day 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 |
1-766 1 day ago |
1-77694 1 day 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-80691 22 hours ago |
0-80691 22 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-77210 21 hours ago |
0-78174 21 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
|
7444/614 |
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 |
n/a |
['github-actions'] |
nobody |
0-64119 17 hours ago |
unknown |
unknown |
| 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
easy
label:t-algebra$ |
15/5 |
Mathlib/RingTheory/KrullDimension/PID.lean |
1 |
2 |
['github-actions', 'kckennylau'] |
nobody |
0-64107 17 hours ago |
0-64107 17 hours ago |
0-0 0 seconds |
| 25830 |
ScottCarnahan author:ScottCarnahan |
refactor (RingTheory/HahnSeries/HEval): remove positive order condition from definition |
This PR removes the positive order condition for substitution (or Hahn evaluation) of a Hahn series into a power series. When the order is not positive, the function substitutes zero. We also add short lemmas for substitution into `PowerSeries.X` and `PowerSeries.C`.
---
[](https://gitpod.io/from-referrer/)
---
*This PR continues the work from #24498.*
*Original PR: https://github.com/leanprover-community/mathlib4/pull/24498* |
t-algebra label:t-algebra$ |
33/13 |
Mathlib/RingTheory/HahnSeries/HEval.lean |
1 |
1 |
['github-actions'] |
nobody |
0-62827 17 hours ago |
0-63700 17 hours ago |
0-0 0 seconds |
| 25831 |
ScottCarnahan author:ScottCarnahan |
feat (RingTheory/HahnSeries): Powers of a binomial |
This PR introduces powers of a binomial `single g 1 - single g' 1` in a Hahn series, where the powers take values in a binomial ring. These series behave as one would expect with respect to addition of powers, and comparison with natural number powers. They are often used in the theory of vertex algebras.
---
- [x] depends on: #25830
[](https://gitpod.io/from-referrer/)
---
*This PR continues the work from #24102.*
*Original PR: https://github.com/leanprover-community/mathlib4/pull/24102* |
t-algebra
blocked-by-other-PR
label:t-algebra$ |
171/23 |
Mathlib.lean,Mathlib/RingTheory/HahnSeries/Binomial.lean,Mathlib/RingTheory/HahnSeries/HEval.lean,Mathlib/RingTheory/HahnSeries/Multiplication.lean,Mathlib/RingTheory/PowerSeries/Binomial.lean |
5 |
2 |
['github-actions', 'mathlib4-dependent-issues-bot'] |
nobody |
0-60441 16 hours ago |
0-60442 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
WIP
|
227/318 |
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-52914 14 hours ago |
0-52914 14 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
|
255/319 |
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-52284 14 hours ago |
1-42840 1 day 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
|
722/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-52105 14 hours ago |
1-48895 1 day 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-51475 14 hours ago |
1-15899 1 day ago |
0-0 0 seconds |
| 25832 |
xroblot author:xroblot |
feat(FieldTheory/LinearDisjoint): `trace` (resp. `norm`) and `algebraMap` commutes |
For `A` and `B` two linearly disjoint extensions of `F` and `b` is a (finite) `F`-basis of `B`, we construct a `A`-basis of `E = A ⊔ B` from `b`. Then, we prove in this situation that `trace` commutes with `algebraMap`, that is:
```lean
Algebra.trace A E (algebraMap B E x) = algebraMap F A (Algebra.trace F B x)
```
and a similar result for the norm
---
[](https://gitpod.io/from-referrer/)
|
t-algebra label:t-algebra$ |
67/1 |
Mathlib/FieldTheory/LinearDisjoint.lean |
1 |
1 |
['github-actions'] |
nobody |
0-47690 13 hours ago |
0-47993 13 hours ago |
0-0 0 seconds |
| 25833 |
loefflerd author:loefflerd |
feat(Counterexamples): topologists' sine curve |
Define the "topologists' sine curve" in R^2, and show that its closure is connected but not path-connected.
This formalization is part of the bachelor thesis of Daniele Bolla at UniDistance Switzerland.
Co-authored-by: Daniele Bolla [daniele.bolla@stu.fernuni.ch](mailto:daniele.bolla@stu.fernuni.ch)
---
[](https://gitpod.io/from-referrer/)
|
t-topology |
219/1 |
Counterexamples.lean,Counterexamples/TopologistsSineCurve.lean,Mathlib/Topology/Connected/PathConnected.lean |
3 |
1 |
['github-actions'] |
nobody |
0-43426 12 hours ago |
0-43438 12 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.
---
- [x] 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 |
380/0 |
Mathlib.lean,Mathlib/CategoryTheory/Limits/Preserves/Bifunctor.lean |
2 |
2 |
['github-actions', 'mathlib4-dependent-issues-bot'] |
nobody |
0-42854 11 hours ago |
0-42940 11 hours ago |
0-0 0 seconds |
| 25834 |
Rida-Hamadani author:Rida-Hamadani |
feat(SimpleGraph): girth-diameter inequality |
This is a useful inequality that comes up in proofs related to Moore graphs, cages, SRGs, and so on.
---
[](https://gitpod.io/from-referrer/)
|
t-combinatorics
WIP
|
969/0 |
Mathlib.lean,Mathlib/Combinatorics/SimpleGraph/GirthDiam.lean |
2 |
1 |
['github-actions'] |
nobody |
0-41855 11 hours ago |
0-41881 11 hours ago |
0-0 0 seconds |
| 25835 |
erdOne author:erdOne |
WIP: Weierstrass elliptic functions |
---
[](https://gitpod.io/from-referrer/)
---
*This PR continues the work from #21662.*
*Original PR: https://github.com/leanprover-community/mathlib4/pull/21662* |
t-analysis
WIP
|
1461/0 |
Mathlib/Analysis/Elliptic/Basic.lean |
1 |
1 |
['github-actions'] |
nobody |
0-41734 11 hours ago |
0-41776 11 hours ago |
0-0 0 seconds |
| 25836 |
jt496 author:jt496 |
feat(SimpleGraph/FiveWheelLike): add the Andrásfai-Erdős-Sós theorem |
Add the Andrásfai-Erdős-Sós theorem `colorable_of_cliqueFree_lt_minDegree` which says that an `r + 1`-cliquefree graph `G` with sufficiently large minimum degree is `r`-colorable.
Co-authored-by: Lian Bremner Tattersall
---
[](https://gitpod.io/from-referrer/)
---
*This PR continues the work from #25313.*
*Original PR: https://github.com/leanprover-community/mathlib4/pull/25313* |
large-import
t-combinatorics
|
307/4 |
Mathlib/Combinatorics/SimpleGraph/FiveWheelLike.lean |
1 |
1 |
['github-actions'] |
nobody |
0-40714 11 hours ago |
0-41563 11 hours ago |
0-0 0 seconds |
| 25739 |
literandltx author:literandltx |
feat(NumberTheory/LegendreSymbol): 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-40187 11 hours ago |
1-47826 1 day 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
|
158/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-39399 10 hours ago |
0-39399 10 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 |
6 |
['Parcly-Taxel', 'eric-wieser', 'github-actions'] |
nobody |
0-39194 10 hours ago |
1-42429 1 day ago |
0-0 0 seconds |
| 25837 |
jt496 author:jt496 |
feat(Combinatorics/SimpleGraph): add homOfConnectedComponents and related results |
Given homomorphisms of each connected component of `G : SimpleGraph α` into `H : SimpleGraph β `give the corresponding `G →g H`
Hence prove that G is n - colorable iff each connected component is n - colorable.
Also prove that G is 2-colorable iff it does not contain an odd length loop (closed walk).
I wasn't sure where to put this - it probably belongs in SimpleGraph.ConcreteColorings?
---
[](https://gitpod.io/from-referrer/)
---
*This PR continues the work from #24546.*
*Original PR: https://github.com/leanprover-community/mathlib4/pull/24546* |
t-combinatorics |
35/0 |
Mathlib/Combinatorics/SimpleGraph/Coloring.lean,Mathlib/Combinatorics/SimpleGraph/ConcreteColorings.lean,Mathlib/Combinatorics/SimpleGraph/Path.lean |
3 |
1 |
['github-actions'] |
nobody |
0-36636 10 hours ago |
0-41446 11 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
auto-merge-after-CI
t-meta
|
6/3 |
Mathlib/Tactic/DeprecateTo.lean |
1 |
5 |
['adomani', 'github-actions', 'grunweg', 'mathlib-bors'] |
nobody |
0-28342 7 hours ago |
0-28400 7 hours ago |
0-0 0 seconds |
| 25843 |
mitchell-horner author:mitchell-horner |
feat(Combinatorics/SimpleGraph): define `between` subgraphs |
The simple graph `G.between s t` is the subgraph of `G` containing edges that connect a vertex in the set `s` to a vertex in the set `t`.
---
[](https://gitpod.io/from-referrer/)
---
*This PR continues the work from #24948.*
*Original PR: https://github.com/leanprover-community/mathlib4/pull/24948* |
t-combinatorics |
91/0 |
Mathlib/Combinatorics/SimpleGraph/Bipartite.lean |
1 |
1 |
['github-actions'] |
nobody |
0-26149 7 hours ago |
0-26219 7 hours ago |
0-0 0 seconds |
| 25844 |
jt496 author:jt496 |
chore(SimpleGraph): split `Combinatorics.SimpleGraph.Path` |
Split the long file `SimpleGraph.Path.lean` into two roughly equal parts.
1. Material on Paths, Cycles, Circuits and Trails is in `Paths.lean`
2. Material on Reachable/Preconnected/Connected/ConnectedComponents is in `Connectivity.Connected`
---
[](https://gitpod.io/from-referrer/)
|
t-combinatorics |
1540/1499 |
Mathlib.lean,Mathlib/Combinatorics/SimpleGraph/Acyclic.lean,Mathlib/Combinatorics/SimpleGraph/Clique.lean,Mathlib/Combinatorics/SimpleGraph/Connectivity/Connected.lean,Mathlib/Combinatorics/SimpleGraph/Connectivity/Subgraph.lean,Mathlib/Combinatorics/SimpleGraph/Connectivity/WalkCounting.lean,Mathlib/Combinatorics/SimpleGraph/Ends/Defs.lean,Mathlib/Combinatorics/SimpleGraph/Hamiltonian.lean,Mathlib/Combinatorics/SimpleGraph/Metric.lean,Mathlib/Combinatorics/SimpleGraph/Path.lean,Mathlib/Combinatorics/SimpleGraph/Paths.lean,Mathlib/Combinatorics/SimpleGraph/Prod.lean,Mathlib/Combinatorics/SimpleGraph/Trails.lean |
13 |
1 |
['github-actions'] |
nobody |
0-24165 6 hours ago |
0-26125 7 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
delegated
|
5/0 |
Mathlib/Data/Int/ModEq.lean |
1 |
3 |
['fpvandoorn', 'github-actions', 'mathlib-bors'] |
nobody |
0-23049 6 hours ago |
0-23050 6 hours ago |
0-0 0 seconds |
| 25841 |
mitchell-horner author:mitchell-horner |
feat(Combinatorics/SimpleGraph): prove the Kővári–Sós–Turán theorem |
Prove the Kővári–Sós–Turán theorem for simple graphs: the `(completeBipartiteGraph α β).Free` simple graphs for `card α ≤ card β` on the vertex type `V` have at most `(card β-1)^(1/(card α))*(card V)^(2-1/(card α))/2 + (card V)*(card α-1)/2` edges.
---
- [x] depends on: #19865
- [x] depends on: #20738
I'd like to make `aux` not private in the `KovariSosTuran` namespace to enable reuse of the double-counting here, but I don't know what to call it.
[](https://gitpod.io/from-referrer/)
---
*This PR continues the work from #20240.*
*Original PR: https://github.com/leanprover-community/mathlib4/pull/20240* |
t-combinatorics |
289/0 |
Mathlib.lean,Mathlib/Combinatorics/SimpleGraph/Bipartite.lean,Mathlib/Combinatorics/SimpleGraph/Extremal/KovariSosTuran.lean |
3 |
2 |
['github-actions', 'mathlib4-dependent-issues-bot'] |
awainverse assignee:awainverse |
0-21541 5 hours ago |
0-26617 7 hours ago |
0-0 0 seconds |
| 25842 |
mitchell-horner author:mitchell-horner |
feat(Combinatorics/SimpleGraph): define turanDensity |
Define the Turán density `turanDensity H` of a simple graph `H`: `turanDensity H` is the limit of `extremalNumber n H / n.choose 2` as `n` approaches `∞`.
Also prove
- the Turán density of a simple graph is well-defined, that is, the limit `extremalNumber n H / n.choose 2` as `n` approaches `∞` exists,
- `extremalNumber n H` is asymptotically equivalent to `turanDensity H * n.choose 2` as `n` approaches `∞`.
---
- [x] depends on: #19865
- [x] depends on: #20681
[](https://gitpod.io/from-referrer/)
---
*This PR continues the work from #20171.*
*Original PR: https://github.com/leanprover-community/mathlib4/pull/20171* |
t-combinatorics |
210/0 |
Mathlib.lean,Mathlib/Combinatorics/SimpleGraph/Extremal/Basic.lean,Mathlib/Combinatorics/SimpleGraph/Extremal/TuranDensity.lean,Mathlib/Combinatorics/SimpleGraph/Finite.lean,Mathlib/Data/Sym/Sym2.lean,Mathlib/Order/Monotone/Basic.lean |
6 |
2 |
['github-actions', 'mathlib4-dependent-issues-bot'] |
b-mehta assignee:b-mehta |
0-21367 5 hours ago |
0-21367 5 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/)
|
maintainer-merge
t-measure-probability
t-analysis
|
116/0 |
Mathlib.lean,Mathlib/Analysis/Normed/Operator/LinearIsometry.lean,Mathlib/MeasureTheory/Integral/IntervalIntegral/ContDiff.lean |
3 |
11 |
['github-actions', 'grunweg', 'sgouezel'] |
grunweg assignee:grunweg |
0-21137 5 hours ago |
0-39142 10 hours 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 |
10 |
['b-mehta', 'eric-wieser', 'github-actions', 'leanprover-bot', 'mattrobball'] |
nobody |
0-20716 5 hours ago |
2-76227 2 days 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 |
large-import
new-contributor
|
698/602 |
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 |
329 |
1 |
['github-actions'] |
nobody |
0-19463 5 hours ago |
0-19471 5 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 |
503/432 |
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 |
8 |
['erdOne', 'github-actions', 'joelriou', 'mathlib4-dependent-issues-bot'] |
nobody |
0-17805 4 hours ago |
1-8976 1 day ago |
0-0 0 seconds |
| 25792 |
erdOne author:erdOne |
feat(NumberTheory): discriminant is norm of different |
---
[](https://gitpod.io/from-referrer/)
---
|
|
304/0 |
Mathlib.lean,Mathlib/Algebra/Module/Submodule/RestrictScalars.lean,Mathlib/LinearAlgebra/Span/Basic.lean,Mathlib/NumberTheory/NumberField/Discriminant/Different.lean,Mathlib/RingTheory/DedekindDomain/Different.lean,Mathlib/RingTheory/DedekindDomain/Factorization.lean,Mathlib/RingTheory/DedekindDomain/Ideal.lean,Mathlib/RingTheory/FractionalIdeal/Basic.lean |
8 |
14 |
['erdOne', 'github-actions', 'riccardobrasca'] |
riccardobrasca assignee:riccardobrasca |
0-16645 4 hours ago |
1-38433 1 day ago |
0-0 0 seconds |
| 25846 |
mattrobball author:mattrobball |
chore: deprioritize some projection instances |
Testing the deprioritizing of some projection instances.
---
[](https://gitpod.io/from-referrer/)
|
|
24/11 |
Mathlib/Algebra/Order/SuccPred.lean,Mathlib/Order/Defs/LinearOrder.lean,Mathlib/Order/Lattice.lean,Mathlib/RingTheory/DedekindDomain/Ideal.lean,Mathlib/RingTheory/FractionalIdeal/Operations.lean |
5 |
9 |
['github-actions', 'leanprover-bot', 'mattrobball'] |
nobody |
0-15855 4 hours ago |
0-25178 6 hours ago |
0-0 0 seconds |
| 25848 |
joelriou author:joelriou |
feat/refactor: redefinition of homology + derived categories |
This PR contains a redefinition of homology, theorems about localization of categories, including triangulated categories, a construction of the derived category of an abelian category, derived functors, spectral sequences, etc. (This is made a PR only to facilitate navigation in the code of this branch.)
This formalization is outlined in the paper _Formalization of derived categories in Lean/mathlib_ https://hal.science/hal-04546712
The homology of `ShortComplex C` (diagrams of two composable morphisms whose composition is zero) is developed in `Algebra.Homology.ShortComplex`. The files in that folder have been added one by one in separate PRs, and then, the current definition of `homology` has been replaced by this new definition in a refactor PR.
Homology refactor:
* #4203
* #4204
* #4388
* #4609
* #4645
* #4787
* #4853
* #5250
* #5674
* #6008
* #6039
* #6089
* #6227
* #6230
* #6231
* #6245
* #6267
* #6279
* #6324
* #6443
* #6586
* #6994
* #7042
* #7047
* #7052
* #7192
* #7193
* #7194
* #7195
* #7197
* #7256
* #7262
* #7280
* #7623
* #7624
* #7806
* #7816
* #7817
* #7821
* #7954
* #7966
* #7993
* #7995
* #7996
* #7997
* #8058
* #8060
* #8069
* #8079
* #8081
* #8084
* #8091
* #8113
* #8114
* #8152
* #8159
* #8174
* #8200
* #8206
* #8208
* #8472
* #8468
* #8475
* #8490
* #8491
* #8507
* #8512
* #8593
* #8595
* #8706
* #8765
* #8766
* #8845
* #9022
* #12649
* #12638
Homological complexes:
* #9333
* #9335
* #9331
Localization of categories:
* #6233
* #6235
* #6236
* #6867
* #6869
* #6887
* #6882
* #8041
* #8055
* #8069
* #8516
* #8864
* #8865
* #9702
* #9692
* #10606
* #10607
* #11721
* #11728
* #11737
* #12728
Shifts on categories:
* #4429
* #6652
* #6653
* #6655
* #7268
* #7270
* #9001
* #11764
Triangulated categories:
* #6377
* #6688
* #6815
* #7053
* #7324
* #7327
* #7336
* #7626
* #7641
* #9049
* #9073
* #10527
* #11738
* #11740
* #11759
* #11786
* #11789
* #11805
* #12619
Construction of the derived category:
* #6626
* #6701
* #6720
* #6894
* #7048
* #7049
* #7050
* #7201
* #7656
* #8937
* #8966
* #8969
* #8970
* #9054
* #9447
* #8951
* #9483
* #9508
* #9509
* #9592
* #9614
* #9615
* #9032
* #9370
* #9550
* #9686
* #9660
* #11760
* #11782
* #11806
Derived functors:
* #10195
* #10270
* #10301
* #10384
* #10413
* #12168
* #12627
* #12631
* #12633
* #12785
* #12788
Refactor of Ext-groups:
* #12607
- [ ] depends on: #24309
- [ ] depends on: #24275
- [ ] depends on: #24191
- [ ] depends on: #23797
- [ ] depends on: #22586
- [ ] depends on: #22556
- [ ] depends on: #22547
- [ ] depends on: #22539
- [ ] depends on: #22508
- [ ] depends on: #22450
- [ ] depends on: #23915
---
[](https://gitpod.io/from-referrer/)
---
*This PR continues the work from #4197.*
*Original PR: https://github.com/leanprover-community/mathlib4/pull/4197* |
large-import
t-topology
t-category-theory
blocked-by-other-PR
WIP
|
41320/489 |
Mathlib.lean,Mathlib/Algebra/Category/ModuleCat/Free.lean,Mathlib/Algebra/Category/ModuleCat/LeftResolutions.lean,Mathlib/Algebra/Homology/Additive.lean,Mathlib/Algebra/Homology/BicomplexColumns.lean,Mathlib/Algebra/Homology/BicomplexRows.lean,Mathlib/Algebra/Homology/Bifunctor.lean,Mathlib/Algebra/Homology/BifunctorColimits.lean,Mathlib/Algebra/Homology/BifunctorCommShift.lean,Mathlib/Algebra/Homology/BifunctorFlip.lean,Mathlib/Algebra/Homology/BifunctorHomotopy.lean,Mathlib/Algebra/Homology/BifunctorMappingCone.lean,Mathlib/Algebra/Homology/BifunctorShift.lean,Mathlib/Algebra/Homology/BifunctorSingle.lean,Mathlib/Algebra/Homology/BifunctorTriangulated.lean,Mathlib/Algebra/Homology/CategoryWithHomology.lean,Mathlib/Algebra/Homology/CochainComplexMinus.lean,Mathlib/Algebra/Homology/ComplexShape.lean,Mathlib/Algebra/Homology/ComplexShapeSigns.lean,Mathlib/Algebra/Homology/ConnectShortExact.lean,Mathlib/Algebra/Homology/DerivedCategory/Basic.lean,Mathlib/Algebra/Homology/DerivedCategory/DerivabilityStructureInjectives.lean,Mathlib/Algebra/Homology/DerivedCategory/Ext/Linear.lean,Mathlib/Algebra/Homology/DerivedCategory/Fractions.lean,Mathlib/Algebra/Homology/DerivedCategory/FullyFaithful.lean,Mathlib/Algebra/Homology/DerivedCategory/HomologySequence.lean,Mathlib/Algebra/Homology/DerivedCategory/Linear.lean,Mathlib/Algebra/Homology/DerivedCategory/Minus.lean,Mathlib/Algebra/Homology/DerivedCategory/Monoidal.lean,Mathlib/Algebra/Homology/DerivedCategory/Plus.lean,Mathlib/Algebra/Homology/DerivedCategory/RightDerivedFunctorPlus.lean,Mathlib/Algebra/Homology/DerivedCategory/SingleTriangle.lean,Mathlib/Algebra/Homology/DerivedCategory/SpectralObject.lean,Mathlib/Algebra/Homology/DerivedCategory/TStructure.lean,Mathlib/Algebra/Homology/Double.lean,Mathlib/Algebra/Homology/DoubleHomology.lean,Mathlib/Algebra/Homology/Embedding/CochainComplex.lean,Mathlib/Algebra/Homology/Embedding/CochainComplexTrunc.lean,Mathlib/Algebra/Homology/Embedding/ComplementaryTrunc.lean,Mathlib/Algebra/Homology/Embedding/ExtendMap.lean,Mathlib/Algebra/Homology/Embedding/HomEquiv.lean,Mathlib/Algebra/Homology/Embedding/StupidFiltration.lean,Mathlib/Algebra/Homology/Embedding/StupidTrunc.lean,Mathlib/Algebra/Homology/Embedding/TruncGE.lean,Mathlib/Algebra/Homology/Embedding/TruncLE.lean,Mathlib/Algebra/Homology/Embedding/TruncLEHomology.lean,Mathlib/Algebra/Homology/ExactSequence.lean,Mathlib/Algebra/Homology/ExactSequenceFour.lean,Mathlib/Algebra/Homology/Factorizations/Basic.lean,Mathlib/Algebra/Homology/Factorizations/CM5a.lean,Mathlib/Algebra/Homology/Factorizations/CM5b.lean,Mathlib/Algebra/Homology/HomologicalBicomplex.lean,Mathlib/Algebra/Homology/HomologicalComplex.lean,Mathlib/Algebra/Homology/HomologicalComplexFunctorEquiv.lean,Mathlib/Algebra/Homology/HomologicalComplexLimits.lean,Mathlib/Algebra/Homology/HomologicalComplexLimitsEventuallyConstant.lean,Mathlib/Algebra/Homology/Homology.lean,Mathlib/Algebra/Homology/HomologySequence.lean,Mathlib/Algebra/Homology/HomologySequenceLemmas.lean,Mathlib/Algebra/Homology/Homotopy.lean,Mathlib/Algebra/Homology/HomotopyCategory.lean,Mathlib/Algebra/Homology/HomotopyCategory/Cylinder.lean,Mathlib/Algebra/Homology/HomotopyCategory/DegreewiseSplit.lean,Mathlib/Algebra/Homology/HomotopyCategory/Devissage.lean,Mathlib/Algebra/Homology/HomotopyCategory/HomComplex.lean,Mathlib/Algebra/Homology/HomotopyCategory/HomComplexShift.lean,Mathlib/Algebra/Homology/HomotopyCategory/KInjective.lean,Mathlib/Algebra/Homology/HomotopyCategory/MappingCone.lean,Mathlib/Algebra/Homology/HomotopyCategory/Minus.lean,Mathlib/Algebra/Homology/HomotopyCategory/Monoidal.lean,Mathlib/Algebra/Homology/HomotopyCategory/MonoidalTriangulated.lean,Mathlib/Algebra/Homology/HomotopyCategory/Plus.lean,Mathlib/Algebra/Homology/HomotopyCategory/PreservesQuasiIso.lean,Mathlib/Algebra/Homology/HomotopyCategory/Pretriangulated.lean,Mathlib/Algebra/Homology/HomotopyCategory/Shift.lean,Mathlib/Algebra/Homology/HomotopyCategory/ShiftSequence.lean,Mathlib/Algebra/Homology/HomotopyCategory/ShortExact.lean,Mathlib/Algebra/Homology/HomotopyCategory/SingleFunctors.lean,Mathlib/Algebra/Homology/HomotopyCategory/SpectralObject.lean,Mathlib/Algebra/Homology/HomotopyFiber.lean,Mathlib/Algebra/Homology/LeftResolutions/Basic.lean,Mathlib/Algebra/Homology/LeftResolutions/CochainComplex.lean,Mathlib/Algebra/Homology/LeftResolutions/CochainComplexMinus.lean,Mathlib/Algebra/Homology/LeftResolutions/Reduced.lean,Mathlib/Algebra/Homology/LeftResolutions/Transport.lean,Mathlib/Algebra/Homology/Localization.lean,Mathlib/Algebra/Homology/Monoidal.lean,Mathlib/Algebra/Homology/ObjectProperty.lean,Mathlib/Algebra/Homology/PreservesQuasiIso.lean,Mathlib/Algebra/Homology/QuasiIso.lean,Mathlib/Algebra/Homology/Refinements.lean,Mathlib/Algebra/Homology/ShortComplex/Abelian.lean,Mathlib/Algebra/Homology/ShortComplex/Basic.lean,Mathlib/Algebra/Homology/ShortComplex/Exact.lean,Mathlib/Algebra/Homology/ShortComplex/FiveLemma.lean,Mathlib/Algebra/Homology/ShortComplex/FourLemma.lean,Mathlib/Algebra/Homology/ShortComplex/HomologicalComplex.lean,Mathlib/Algebra/Homology/ShortComplex/Images.lean,Mathlib/Algebra/Homology/ShortComplex/Preadditive.lean,Mathlib/Algebra/Homology/ShortComplex/PreservesHomology.lean |
290 |
n/a |
['github-actions', 'mathlib4-dependent-issues-bot'] |
nobody |
0-10529 2 hours ago |
unknown |
unknown |
| 25847 |
kckennylau author:kckennylau |
chore: remove simp attribute from variable change formulas for Weierstrass cubics |
---
Zulip: [#mathlib4 > `@[simp]` for variable changes in Elliptic curves](https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/.60.40.5Bsimp.5D.60.20for.20variable.20changes.20in.20Elliptic.20curves/with/521714805)
[](https://gitpod.io/from-referrer/)
|
t-algebraic-geometry |
21/34 |
Mathlib/AlgebraicGeometry/EllipticCurve/IsomOfJ.lean,Mathlib/AlgebraicGeometry/EllipticCurve/NormalForms.lean,Mathlib/AlgebraicGeometry/EllipticCurve/VariableChange.lean |
3 |
1 |
['Multramate', 'github-actions'] |
nobody |
0-10332 2 hours ago |
0-23115 6 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
|
556/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-3733 1 hour ago |
1-43458 1 day 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 |
369/0 |
Mathlib.lean,Mathlib/CategoryTheory/Monoidal/Action/Basic.lean,docs/references.bib |
3 |
1 |
['github-actions'] |
nobody |
0-2792 46 minutes ago |
1-43566 1 day ago |
0-0 0 seconds |
| 25840 |
robin-carlier author:robin-carlier |
feat(CategoryTheory/Monoidal/Action): monoidal right actions |
We introduce the notion of a right action of a monoidal category `C` on a category `D`. This notion is formally conjugate to that of a left action introduced in #25761, and so are every results in this PR. Please refer to #25761 for a more detailed overview of the notion. The notion comes with its set of notations.
We show basic simp lemmas for these objects, and we show that any monoidal category acts on the right on itself.
---
- [ ] depends on: #25761
[](https://gitpod.io/from-referrer/)
|
t-category-theory
blocked-by-other-PR
|
688/0 |
Mathlib.lean,Mathlib/CategoryTheory/Monoidal/Action/Basic.lean,docs/references.bib |
3 |
2 |
['github-actions', 'mathlib4-dependent-issues-bot'] |
nobody |
0-2053 34 minutes ago |
0-36584 10 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
awaiting-author
|
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 |
9 |
['github-actions', 'joelriou'] |
nobody |
0-974 16 minutes ago |
0-974 15 minutes 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 |
57/2 |
Mathlib/Tactic/ComputeDegree.lean,Mathlib/Tactic/FieldSimp.lean,Mathlib/Tactic/Finiteness.lean,MathlibTest/hint.lean |
4 |
2 |
['euprunin', 'fpvandoorn', 'github-actions'] |
nobody |
0-300 5 minutes ago |
0-83139 23 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 |
159-59529 5 months ago |
159-59529 5 months 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 |
65-7151 2 months ago |
65-7240 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-81028 1 month ago |
38-81037 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-80339 1 month ago |
38-80974 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 |
31-18523 1 month ago |
35-25299 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 |
25-66989 25 days ago |
26-1016 26 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 |
9-46799 9 days ago |
38-80938 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-82880 7 days ago |
11-35292 11 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 |
6-4190 6 days ago |
6-4191 6 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 |
1-7544 1 day ago |
1-21246 1 day 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-80846 22 hours ago |
0-80846 22 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 |
270-58061 8 months ago |
270-80036 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 |
223-11780 7 months ago |
249-302 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 |
205-31311 6 months ago |
205-31311 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-73088 1 month ago |
61-15318 2 months 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-80988 1 month ago |
38-80993 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 |
25-17194 25 days ago |
25-17195 25 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 |
25-16268 25 days ago |
25-16270 25 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 |
11-52166 11 days ago |
11-52166 11 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 |
11-14268 11 days ago |
11-14270 11 days ago |
5-75236 5 days |