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 |
| 36216 |
michaellee94 author:michaellee94 |
feat(CategoryTheory): characterize pullback squares via the `Over` category |
---
[](https://gitpod.io/from-referrer/)
|
t-category-theory
new-contributor
maintainer-merge
awaiting-author
|
47/0 |
Mathlib/CategoryTheory/Limits/Shapes/Pullback/IsPullback/Basic.lean |
1 |
18 |
['dagurtomas', 'github-actions', 'joelriou', 'michaellee94'] |
robin-carlier assignee:robin-carlier |
32-60510 1 month ago |
32-60510 32 days ago |
2-50782 2 days |
| 37057 |
erdOne author:erdOne |
feat(AlgebraicTopology): `SimplexCategory.toTop_map_δ_apply` |
---
[](https://gitpod.io/from-referrer/)
|
t-algebraic-topology
maintainer-merge
awaiting-author
merge-conflict
|
48/2 |
Mathlib/AlgebraicTopology/CechNerve.lean,Mathlib/AlgebraicTopology/SimplexCategory/Basic.lean,Mathlib/AlgebraicTopology/SimplexCategory/Defs.lean,Mathlib/AlgebraicTopology/TopologicalSimplex.lean,Mathlib/Data/Fin/SuccPred.lean |
5 |
17 |
['Raph-DG', 'dagurtomas', 'erdOne', 'github-actions', 'joelriou', 'mathlib-merge-conflicts', 'riccardobrasca'] |
robin-carlier assignee:robin-carlier |
20-27313 20 days ago |
21-74953 21 days ago |
4-49805 4 days |
| 37603 |
Parcly-Taxel author:Parcly-Taxel |
refactor: review of `SetSemiring` |
* Rename `Set.up` and `SetSemiring.down` to `SetSemiring.ofSet` and `SetSemiring.toSet` respectively. Unprotect both and make them equivalences, following `FreeMonoid`.
* Derive `CompleteAtomicBooleanAlgebra` for `SetSemiring` immediately.
* Add `imageHom_id` and `imageHom_comp`. The three existing lemmas about `imageHom` are coalesced into `imageHom_apply`.
Ultimately inspired by https://github.com/leanprover-community/mathlib4/pull/36934#issuecomment-4183475568. |
maintainer-merge |
120/165 |
Mathlib/Algebra/Algebra/Operations.lean,Mathlib/Data/Set/Semiring.lean |
2 |
41 |
['Parcly-Taxel', 'YaelDillies', 'eric-wieser', 'github-actions', 'mathlib-merge-conflicts', 'sgouezel'] |
nobody |
19-83700 19 days ago |
19-83958 19 days ago |
21-24753 21 days |
| 33443 |
sahanwijetunga author:sahanwijetunga |
feat: Define Isometries of Bilinear Spaces |
---
We define Isometries of Bilinear Spaces, closely following the implementation of isometries of quadratic spaces.
[](https://gitpod.io/from-referrer/)
|
t-algebra
new-contributor
maintainer-merge
label:t-algebra$ |
278/0 |
Mathlib.lean,Mathlib/LinearAlgebra/BilinearForm/Isometry.lean,Mathlib/LinearAlgebra/BilinearForm/IsometryEquiv.lean |
3 |
25 |
['github-actions', 'robin-carlier', 'sahanwijetunga'] |
mattrobball assignee:mattrobball |
18-21547 18 days ago |
18-21706 18 days ago |
66-48605 66 days |
| 37846 |
grunweg author:grunweg |
fix(positivity): still prove non-negativity in the `Nat.cast` extension if positivity fails |
---
[](https://gitpod.io/from-referrer/)
|
t-meta
maintainer-merge
|
11/2 |
Mathlib/Tactic/Positivity/Basic.lean,MathlibTest/positivity.lean |
2 |
4 |
['dwrensha', 'github-actions'] |
dwrensha assignee:dwrensha |
17-43594 17 days ago |
18-5814 18 days ago |
18-5607 18 days |
| 37053 |
artie2000 author:artie2000 |
refactor(Analysis/Convex/Cone): use `PointedCone` in Riesz extension theorem |
Change the statement of the Riesz extension theorem to take a `PointedCone` rather than a `ConvexCone`.
This PR is part of a series replacing `ConvexCone` with `PointedCone`. https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/Replacing.20.60ConvexCone.60.20with.20.60PointedCone.60/near/581184307
---
[](https://gitpod.io/from-referrer/)
|
t-convex-geometry
maintainer-merge
|
15/12 |
Mathlib/Analysis/Convex/Cone/Extension.lean,Mathlib/Geometry/Convex/Cone/Pointed.lean |
2 |
8 |
['YaelDillies', 'artie2000', 'github-actions', 'mathlib-merge-conflicts', 'ocfnash'] |
nobody |
14-855 14 days ago |
14-883 14 days ago |
33-42111 33 days |
| 36308 |
SnirBroshi author:SnirBroshi |
feat(Combinatorics/SimpleGraph/Subgraph): a couple of `subgraphOfAdj` lemmas |
Also golf a lemma (it's one line longer but it looks simpler to me).
---
[](https://gitpod.io/from-referrer/)
|
t-combinatorics
maintainer-merge
|
14/5 |
Mathlib/Combinatorics/SimpleGraph/Subgraph.lean |
1 |
4 |
['SnirBroshi', 'YaelDillies', 'github-actions'] |
b-mehta assignee:b-mehta |
13-45402 13 days ago |
52-25060 52 days ago |
52-24851 52 days |
| 37400 |
SnirBroshi author:SnirBroshi |
feat(Combinatorics/SimpleGraph/Acyclic): endpoints of a path have at most one neighbor in the path |
---
[](https://gitpod.io/from-referrer/)
|
t-combinatorics
maintainer-merge
|
15/0 |
Mathlib/Combinatorics/SimpleGraph/Acyclic.lean |
1 |
5 |
['Rida-Hamadani', 'Ruben-VandeVelde', 'SnirBroshi', 'github-actions'] |
nobody |
12-40123 12 days ago |
28-39687 28 days ago |
28-39478 28 days |
| 37420 |
artie2000 author:artie2000 |
refactor: change definitions to avoid `ConvexCone` |
Change the definitions of `PointedCone.positive` and `PointedCone.closure` to avoid mentioning `ConvexCone`.
This PR is part of a series deprecating `ConvexCone`: https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/Replacing.20.60ConvexCone.60.20with.20.60PointedCone.60/with/582738985
---
[](https://gitpod.io/from-referrer/)
|
t-convex-geometry
maintainer-merge
|
10/4 |
Mathlib/Analysis/Convex/Cone/Closure.lean,Mathlib/Geometry/Convex/Cone/Pointed.lean |
2 |
3 |
['YaelDillies', 'github-actions', 'mathlib-merge-conflicts', 'ooovi', 'vihdzp'] |
nobody |
12-6907 12 days ago |
12-6871 12 days ago |
27-27225 27 days |
| 37588 |
Vierkantor author:Vierkantor |
feat(Linter/DocString): ignore Verso linter errors about links and LaTeX |
I went through [the weekly linting log](https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/Weekly.20linting.20log/near/582485221) and found most of the warnings come from three sources. All of these are sensical syntax in our current Markdown dialect, and should be fixed automatically by a script, instead of manually. I expect after these changes we'll be down to hundreds of linter errors rather than two thousand.
* References [between square brackets] without a following link URL. Verso has different implementations for references depending on what kind they are, and since there are a thousand references we should be using a script to fix these.
* Autolinks: bare URLs or URLs between . Autolinks are intentionally not supported by Verso but replacing every `https://...` with `[https://...](https://...)` would be too noisy.
* LaTeX blocks: Verso does have TeX blocks but with an incompatible syntax. Better to fix it with a script.
I ended up using preprocessing in addition to postprocessing to filter out errors: using the error message we can determine whether it is a reference, but for errors caused by autolinks and LaTeX blocks I couldn't figure out how to do so easily: the information about the parse error does report a string position but this is always the last character of the docstring. So instead we modify the docstring before it is passed into Verso to get rid of the offending syntax.
---
[](https://gitpod.io/from-referrer/)
|
t-linter
large-import
maintainer-merge
|
113/5 |
Mathlib/Tactic/Linter/DocString.lean,MathlibTest/DocString.lean |
2 |
18 |
['Vierkantor', 'github-actions', 'thorimur'] |
thorimur assignee:thorimur |
11-3133 11 days ago |
11-3191 11 days ago |
13-85063 13 days |
| 37808 |
JovanGerb author:JovanGerb |
feat(Translate): locally modify name guessing dictionaries |
This PR adds the feature to `to_dual` and `to_additive` that you can now locally modify the name translation dictionary.
With this change, we run the risk of having the automated translations being harder to predict. For this reason, the changes to the dictionary do not persisted through imports. Instead, the change lasts until the end of the file (though it ignores sections).
See https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/Order.20dual.20tactic/near/580834166
---
[](https://gitpod.io/from-referrer/)
|
t-meta
maintainer-merge
|
111/39 |
Mathlib/Order/GaloisConnection/Basic.lean,Mathlib/Order/GaloisConnection/Defs.lean,Mathlib/Order/Interval/Set/Basic.lean,Mathlib/Order/Interval/Set/Disjoint.lean,Mathlib/Tactic/Translate/Core.lean,Mathlib/Tactic/Translate/GuessName.lean,Mathlib/Tactic/Translate/ToAdditive.lean,Mathlib/Tactic/Translate/ToDual.lean,MathlibTest/ToDual.lean |
9 |
4 |
['JovanGerb', 'bryangingechen', 'github-actions', 'joneugster'] |
joneugster assignee:joneugster |
11-3000 11 days ago |
15-85380 15 days ago |
16-6005 16 days |
| 38179 |
wwylele author:wwylele |
feat(Combinatorics): Pentagonal numbers |
Introduces definition of pentagonal number https://en.wikipedia.org/wiki/Pentagonal_number in preparation for pentagonal number theorem.
---
This is extracted from #33143 as suggested. I only put a few elementary properties here to limit the code change size.
The future file structure will be
- Combinatorics/Enumerative/Pentagonal.lean (this PR)
- Topology/Algebra/InfiniteSum/Pentagonal.lean + RingTheory/PowerSeries/Pentagonal.lean (#33143, depends on previous one) pentagonal theorem in generic form and for power series
- Combinatorics/Enumerative/Partition/Pentagonal.lean (future PR, depends on the previous one): connection between partition and pentagonal numbers
This originally comes from my own repo https://github.com/wwylele/PentagonalNumberTheorem. In the past, there were also PR #31156 and #31362 independently worked by @BeibeiX0 on the same topic, and I tried avoiding stepping on each other's toes when making #33143. Then #31156 and #31362 were closed for unclear reason.
As I mostly rewrote the code based on my own repo, I only put my name here, but given that I unavoidably took inspiration from other PRs, if @BeibeiX0 would like his name to be added to co-author and copyright notice, I am happy to do so.
[](https://gitpod.io/from-referrer/)
|
t-combinatorics
maintainer-merge
|
75/0 |
Mathlib.lean,Mathlib/Combinatorics/Enumerative/Pentagonal.lean |
2 |
27 |
['copilot-pull-request-reviewer', 'github-actions', 'tb65536', 'wwylele'] |
nobody |
10-53042 10 days ago |
10-53726 10 days ago |
10-62303 10 days |
| 37931 |
Vierkantor author:Vierkantor |
chore(Tactic): make the (deprecated) `replace` syntax a `@[tactic_alt]` |
This PR replaces the tactic docstring for Mathlib's version of `replace` with a `@[tactic_alt]` attribute + `tactic_extension`. Also update the module docs which did not get updated when `replace` got upstreamed to core Lean.
---
[](https://gitpod.io/from-referrer/)
|
documentation
t-meta
maintainer-merge
|
7/31 |
Mathlib/Tactic/Replace.lean |
1 |
2 |
['github-actions', 'joneugster'] |
dwrensha assignee:dwrensha |
9-45299 9 days ago |
14-82287 14 days ago |
14-82800 14 days |
| 37868 |
Jun2M author:Jun2M |
feat(Combinatorics/Graph): map on `Graph` |
This PR introduces vertex map on graphs, `map`.
This creates a new file `Maps` which will be home to `map` and morphisms between `Graph`s.
Co-authored-by: Peter Nelson [apn.uni@gmail.com](mailto:apn.uni@gmail.com)
---
[](https://gitpod.io/from-referrer/)
|
t-combinatorics
maintainer-merge
|
108/0 |
Mathlib.lean,Mathlib/Combinatorics/Graph/Maps.lean |
2 |
8 |
['Jun2M', 'YaelDillies', 'b-mehta', 'github-actions', 'mathlib-merge-conflicts'] |
nobody |
7-72250 7 days ago |
7-72250 7 days ago |
18-249 18 days |
| 38301 |
SnirBroshi author:SnirBroshi |
feat(Algebra/Group/Commutator): tag `addCommutatorElement` as a scoped instance |
#34784 additivized commutators and made the multiplicative commutator instance available under `open scoped commutatorElement`.
This makes the additive instance available under `open scoped addCommutatorElement`.
---
~~Should we instead make it scoped under the `addCommutatorElement` namespace?
The existing usages of additive commutators come from decls marked with `open scoped commutatorElement in @[to_additive]`, and `to_additive` seemingly doesn't mind that the additivized version is not an instance. So I think they don't have to live in the same namespace.~~
[](https://gitpod.io/from-referrer/)
|
t-algebra
maintainer-merge
label:t-algebra$ |
6/0 |
Mathlib/Algebra/Group/Commutator.lean |
1 |
6 |
['SnirBroshi', 'github-actions', 'tb65536'] |
nobody |
7-70591 7 days ago |
7-73046 7 days ago |
7-73251 7 days |
| 38172 |
joelriou author:joelriou |
feat(AlgebraicTopology/SimplicialSet): Mulstruct.mulOne and oneMul |
We introduce definitions `SSet.PtSimplex.MulStruct.oneMul/mulOne` which shall later be interpreted as an explanation for the relations satisfied by the neutral element for the multiplication on homotopy groups of Kan complexes.
---
[](https://gitpod.io/from-referrer/)
|
t-algebraic-topology
maintainer-merge
|
53/0 |
Mathlib/AlgebraicTopology/SimplicialSet/KanComplex/MulStruct.lean |
1 |
6 |
['github-actions', 'joelriou', 'robin-carlier'] |
robin-carlier assignee:robin-carlier |
7-4802 7 days ago |
7-5671 7 days ago |
10-74991 10 days |
| 38184 |
tb65536 author:tb65536 |
chore(Algebra/Algebra/Tower): make `Algebra.algHom` an alias of `IsScalarTower.toAlgHom` |
`Algebra.algHom` is a duplicate of `IsScalarTower.ofAlgHom` so I've made it an alias to make this clearer.
Zulip thread: [#mathlib4 > duplication: Algebra.algHom = IsScalarTower.toAlgHom](https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/duplication.3A.20Algebra.2EalgHom.20.3D.20IsScalarTower.2EtoAlgHom/with/569828872)
---
[](https://gitpod.io/from-referrer/)
|
t-ring-theory
t-algebra
maintainer-merge
label:t-algebra$ |
27/26 |
Mathlib/Algebra/Algebra/Hom.lean,Mathlib/Algebra/Algebra/Tower.lean |
2 |
14 |
['acmepjz', 'github-actions', 'tb65536', 'themathqueen'] |
nobody |
6-57697 6 days ago |
6-72871 6 days ago |
10-55753 10 days |
| 37291 |
IvanRenison author:IvanRenison |
refactor(Combinatorics/SimpleGraph): move `chromaticNumber_le_two_iff_isBipartite` and `chromaticNumber_eq_two_iff` to `Bipartite` file |
---
[](https://gitpod.io/from-referrer/)
|
t-combinatorics
maintainer-merge
|
10/12 |
Mathlib/Combinatorics/SimpleGraph/Bipartite.lean,Mathlib/Combinatorics/SimpleGraph/Coloring/Constructions.lean |
2 |
3 |
['Ruben-VandeVelde', 'github-actions', 'mathlib-merge-conflicts'] |
nobody |
6-51930 6 days ago |
6-51952 6 days ago |
31-49705 31 days |
| 37738 |
khwilson author:khwilson |
feat(Topology/Order/Bornology): generalize `cobounded_eq` |
`Real.cobounded_eq` and `Int.cobounded_eq` are used in several places throughout Mathlib. They are currently proved in terms of the Metric topology on `Int` and `Real`, but they're really properties of the order bornology on those objects.
Generalize those constructions to `IsOrderBornology` for `LinearOrder`'s and add a few more constructions that are true in other circumstances, e.g., `cobounded NNReal = .atTop` follows from the fact that `NNReal` is both `NoMaxOrder` and `OrderBot`.
---
[](https://gitpod.io/from-referrer/)
|
maintainer-merge
t-order
|
57/18 |
Mathlib/Analysis/Polynomial/Basic.lean,Mathlib/Analysis/SpecialFunctions/Complex/LogBounds.lean,Mathlib/Topology/Instances/Int.lean,Mathlib/Topology/Instances/Real/Lemmas.lean,Mathlib/Topology/Order/Bornology.lean |
5 |
14 |
['YaelDillies', 'github-actions', 'khwilson', 'vihdzp'] |
bryangingechen assignee:bryangingechen |
6-45568 6 days ago |
21-3772 21 days ago |
21-4406 21 days |
| 34854 |
GrigorenkoPV author:GrigorenkoPV |
chore(Combinatorics/Enumerative/Catalan): split into `Basic` & `Tree` |
---
Split off from #34853
[](https://gitpod.io/from-referrer/)
|
new-contributor
t-combinatorics
maintainer-merge
awaiting-author
|
225/194 |
Mathlib.lean,Mathlib/Combinatorics/Enumerative/Catalan.lean,Mathlib/Combinatorics/Enumerative/Catalan/Basic.lean,Mathlib/Combinatorics/Enumerative/Catalan/Tree.lean,Mathlib/Combinatorics/Enumerative/DyckWord.lean,Mathlib/RingTheory/PowerSeries/Catalan.lean |
6 |
7 |
['SnirBroshi', 'Vierkantor', 'YaelDillies', 'github-actions', 'mathlib-merge-conflicts', 'vihdzp'] |
nobody |
5-66484 5 days ago |
16-9630 16 days ago |
45-59230 45 days |
| 37985 |
Raph-DG author:Raph-DG |
feat(Topology): intersections preserve Notherian-ness and Quasisober-ness |
In this PR we prove some basic topology lemmas about the preservation of noetherianness and quasisoberness under intersections.
---
[](https://gitpod.io/from-referrer/)
|
t-topology
maintainer-merge
|
25/0 |
Mathlib/Topology/NoetherianSpace.lean,Mathlib/Topology/Sober.lean |
2 |
23 |
['Raph-DG', 'chrisflav', 'github-actions', 'grunweg', 'vihdzp'] |
PatrickMassot assignee:PatrickMassot |
5-65736 5 days ago |
5-65759 5 days ago |
14-40776 14 days |
| 38257 |
joelriou author:joelriou |
feat(CategoryTheory): MorphismProperty.single |
---
[](https://gitpod.io/from-referrer/)
|
t-category-theory
maintainer-merge
|
63/1 |
Mathlib/CategoryTheory/MorphismProperty/Basic.lean,Mathlib/CategoryTheory/MorphismProperty/IsSmall.lean,Mathlib/CategoryTheory/ObjectProperty/Local.lean |
3 |
6 |
['github-actions', 'joelriou', 'robin-carlier'] |
robin-carlier assignee:robin-carlier |
5-45248 5 days ago |
6-85151 6 days ago |
8-67943 8 days |
| 38381 |
euprunin author:euprunin |
chore: golf using `grind` |
The goal of this PR is to decrease the number of times lemmas are called explicitly. Any decrease in compilation time is a welcome side effect, although it is not a primary objective.
Trace profiling results (differences <30 ms considered measurement noise):
* `✅️ SimpleGraph.Walk.takeUntil_eq_take`: 258 ms before, 206 ms after 🎉
Profiled using `set_option trace.profiler true in`.
---
[](https://gitpod.io/from-referrer/)
|
t-combinatorics
maintainer-merge
|
2/6 |
Mathlib/Combinatorics/SimpleGraph/Walk/Decomp.lean |
1 |
5 |
['SnirBroshi', 'euprunin', 'github-actions', 'grunweg'] |
nobody |
5-9801 5 days ago |
5-58888 5 days ago |
5-58679 5 days |
| 36416 |
j-loreaux author:j-loreaux |
feat(Analysis/CStarAlgebra): norms of sums of orthogonal selfadjoint elements |
---
- [ ] depends on: #36407
- [ ] depends on: #37569
[](https://gitpod.io/from-referrer/)
|
t-analysis
maintainer-merge
|
126/1 |
Mathlib/Algebra/Star/BigOperators.lean,Mathlib/Algebra/Star/SelfAdjoint.lean,Mathlib/Analysis/CStarAlgebra/Fuglede.lean,Mathlib/Analysis/CStarAlgebra/GelfandDuality.lean |
4 |
22 |
['github-actions', 'grunweg', 'j-loreaux', 'loefflerd', 'mathlib-dependent-issues', 'mathlib-merge-conflicts', 'themathqueen'] |
loefflerd assignee:loefflerd |
4-73350 4 days ago |
4-73422 4 days ago |
22-70299 22 days |
| 36451 |
SnirBroshi author:SnirBroshi |
feat(Combinatorics/SimpleGraph/Matching): `edgeSet` is injective and strictly monotonic on matchings, and more API |
---
[](https://gitpod.io/from-referrer/)
|
t-combinatorics
maintainer-merge
|
36/10 |
Mathlib/Combinatorics/SimpleGraph/Matching.lean,Mathlib/Combinatorics/SimpleGraph/Subgraph.lean |
2 |
13 |
['SnirBroshi', 'YaelDillies', 'github-actions', 'mathlib-merge-conflicts'] |
nobody |
4-69286 4 days ago |
4-74287 4 days ago |
33-25628 33 days |
| 37864 |
JovanGerb author:JovanGerb |
chore: reorder arguments of `AddMonoidHom.map_zsmul` |
This PR modifies `AddMonoidHom.map_nsmul`, `AddMonoidHom.map_zsmul` and `AddMonoidHom.map_zsmul'` so that their order of arguments is as expected. This is then consistent with `map_nsmul`/`map_zsmul`.
---
[](https://gitpod.io/from-referrer/)
|
t-algebra
maintainer-merge
label:t-algebra$ |
21/22 |
Mathlib/Algebra/Category/Grp/ZModuleEquivalence.lean,Mathlib/Algebra/Group/Hom/Defs.lean,Mathlib/Algebra/GroupWithZero/Action/Defs.lean,Mathlib/Algebra/Module/CharacterModule.lean,Mathlib/Algebra/Module/Equiv/Basic.lean,Mathlib/Analysis/Complex/Circle.lean,Mathlib/Analysis/SpecialFunctions/Trigonometric/Angle.lean,Mathlib/CategoryTheory/Linear/Basic.lean,Mathlib/CategoryTheory/Linear/LinearFunctor.lean |
9 |
8 |
['JovanGerb', 'github-actions', 'mathlib-merge-conflicts', 'themathqueen'] |
nobody |
4-40574 4 days ago |
11-16430 11 days ago |
16-27518 16 days |
| 38233 |
mbkybky author:mbkybky |
feat(Algebra/Module/Projective): add `ULift` and `Shrink` lemmas for `Module.Projective` |
Add `ULift` and `Shrink` lemmas for `Module.Projective`.
---
[](https://gitpod.io/from-referrer/)
|
t-algebra
maintainer-merge
label:t-algebra$ |
15/3 |
Mathlib/Algebra/Category/ModuleCat/Ulift.lean,Mathlib/Algebra/Module/Projective.lean |
2 |
7 |
['github-actions', 'mbkybky', 'robin-carlier'] |
nobody |
4-22615 4 days ago |
4-22751 4 days ago |
6-63208 6 days |
| 30185 |
alreadydone author:alreadydone |
feat(MathlibTest): kernel reduction of nsmul on elliptic curve over ZMod |
Co-authored-by: @SteffenReith
---
- [x] depends on: #30144
- [x] depends on: #30181
[](https://gitpod.io/from-referrer/)
|
t-algebra
t-number-theory
t-algebraic-geometry
maintainer-merge
label:t-algebra$ |
29/0 |
MathlibTest/EllipticCurve.lean |
1 |
11 |
['alreadydone', 'github-actions', 'joneugster', 'mathlib4-dependent-issues-bot', 'mathlib4-merge-conflict-bot'] |
joneugster assignee:joneugster |
4-22020 4 days ago |
10-12891 10 days ago |
11-28204 11 days |
| 36401 |
JovanGerb author:JovanGerb |
feat(positivity): positivity extension for `a - b` |
This PR adds support in `positivity` for proving things about subtraction. For example, if the goal is `0 < a - b`, and there is a local hypothesis of type `b < a`, then we close the goal.
The motivation is that we want `positivity` to be a flexible tactic. So, when trying to prove `0 < a - b` using a local hypothesis, we should look for the simp normal form of this, which is `b < a`.
---
[Zulip discussion](https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/Can.20I.20make.20positivity.20work.20for.20this.3F/near/578277240)
[](https://gitpod.io/from-referrer/)
|
t-meta
maintainer-merge
|
63/26 |
Mathlib/Analysis/Calculus/Taylor.lean,Mathlib/Analysis/Complex/AbelLimit.lean,Mathlib/Analysis/Complex/BorelCaratheodory.lean,Mathlib/Analysis/Complex/Hadamard.lean,Mathlib/Analysis/Convex/BetweenList.lean,Mathlib/Analysis/SpecialFunctions/Log/Deriv.lean,Mathlib/Analysis/SpecificLimits/FloorPow.lean,Mathlib/Geometry/Manifold/Riemannian/PathELength.lean,Mathlib/Tactic/Positivity/Basic.lean,MathlibTest/positivity.lean |
10 |
13 |
['JovanGerb', 'Vierkantor', 'github-actions', 'hrmacbeth', 'j-loreaux', 'joneugster', 'leanprover-radar'] |
joneugster assignee:joneugster |
4-19548 4 days ago |
6-85741 6 days ago |
35-69923 35 days |
| 37439 |
ADedecker author:ADedecker |
feat: UniformConvergenceCLM version of ContinuousLinearEquiv.arrowCongr |
The absence of `@[simp]` attribute comes from the fact that the generated lemmas would break the API boundary.
I think the solution to all of this will eventually be to define generic type aliases `Topology.WithUniform` / `Topology.WithUniformOn` / `Topology.WithPointwise`... which will behave like [WithLp](https://leanprover-community.github.io/mathlib4_docs/Mathlib/Analysis/Normed/Lp/WithLp.html#WithLp) (thus disabling the very-abused defeqs around here).
---
- [x] depends on: #37614
[](https://gitpod.io/from-referrer/)
|
t-topology
maintainer-merge
|
182/3 |
Mathlib/Topology/Algebra/Module/Equiv.lean,Mathlib/Topology/Algebra/Module/Spaces/CompactConvergenceCLM.lean,Mathlib/Topology/Algebra/Module/Spaces/ContinuousLinearMap.lean,Mathlib/Topology/Algebra/Module/Spaces/UniformConvergenceCLM.lean |
4 |
9 |
['ADedecker', 'github-actions', 'loefflerd', 'mathlib-dependent-issues', 'mathlib-merge-conflicts'] |
loefflerd assignee:loefflerd |
4-17465 4 days ago |
4-17509 4 days ago |
20-77993 20 days |
| 36423 |
kim-em author:kim-em |
perf: decompress already-cached files concurrently with downloads |
This PR builds on https://github.com/leanprover-community/mathlib4/pull/32987 (pipeline downloads and decompression) and https://github.com/leanprover-community/mathlib4/pull/36367 (fix: decompress already downloaded files).
Previously, already-cached `.ltar` files were only decompressed after all downloads completed, in the final `unpackCache` sweep. This PR starts decompressing them concurrently with downloads by spawning `leantar` as a background task before the download phase begins.
The two decompression paths operate on disjoint file sets (pre-cached vs newly downloaded), so there is no conflict. In the common case where a user has most files cached but a few hundred to download, this overlaps several seconds of decompression with network I/O.
🤖 Prepared with Claude Code |
LLM-generated
CI
t-meta
maintainer-merge
|
79/27 |
Cache/IO.lean,Cache/Requests.lean |
2 |
7 |
['github-actions', 'joneugster', 'kim-em'] |
joneugster assignee:joneugster |
4-15915 4 days ago |
7-48182 7 days ago |
35-37970 35 days |
| 36201 |
themathqueen author:themathqueen |
feat(Analysis/CStarAlgebra): set of star projections equals the extreme points of the nonnegative closed unit ball |
An element in a non-unital C⋆-algebra is a projection iff it is an extreme point of the nonnegative closed unit ball. This is from 1.6.2 in Sakai's C⋆-algebras and W⋆-algebras (the proof is different though).
Co-authored-by: Jon Bannon <59937998+JonBannon@users.noreply.github.com>
---
- [x] depends on: #35997
[](https://gitpod.io/from-referrer/)
|
t-analysis
maintainer-merge
|
103/0 |
Mathlib.lean,Mathlib/Algebra/Ring/Defs.lean,Mathlib/Analysis/CStarAlgebra/Extreme.lean,docs/references.bib |
4 |
16 |
['github-actions', 'j-loreaux', 'loefflerd', 'mathlib-dependent-issues', 'mathlib-merge-conflicts', 'mcdoll', 'themathqueen'] |
mcdoll assignee:mcdoll |
4-14386 4 days ago |
18-53091 18 days ago |
47-81960 47 days |
| 37171 |
SnirBroshi author:SnirBroshi |
chore(Data/Int/Init): generalize `le_induction` from `Prop` to `Sort*` + def lemmas |
---
- Generallise `le_induction` from `Prop` to `Sort*` and rename to `leInduction`
- Add a few lemmas
- Simplify proofs using `lia`
- Move `inductionOn'_add_one`
[Zulip 💬](https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/Add.20note.20to.20help.20search.20similar.20thms/near/535331432)
[](https://gitpod.io/from-referrer/)
|
t-data
large-import
maintainer-merge
|
56/48 |
Mathlib/Data/Int/Basic.lean,Mathlib/Data/Int/Init.lean,Mathlib/GroupTheory/CoprodI.lean |
3 |
9 |
['SnirBroshi', 'github-actions', 'joneugster', 'mathlib-merge-conflicts', 'plp127'] |
joneugster assignee:joneugster |
3-74775 3 days ago |
27-34624 27 days ago |
28-42117 28 days |
| 37347 |
JovanGerb author:JovanGerb |
feat: implementation of `@[use_set_notation_for_order]` |
This PR allows the use of `⊆` notation while the underlying constant is `≤`.
Similarly for `⊂`/`<`, `⊇`/`≥` and `⊃`/`>`.
- The idea is to later extend this feature to other set notation constants, such as union/intersection.
- There are some types for which we cannot use `LE.le` as the underlying constant, such as `List` and `Multiset`. So, the elaborator for the `⊆` notation needs to make a decision which underlying constant to elaborate to, depending on the type. Sometimes the type is not known yet, which makes things awkward. Most of these cases are solved by delaying the elaboration until later when the type is known.
- However, in some cases this doesn't work either, such as `simp_rw [and_comm (_ ⊆ _)]`, where it is impossible to tell the type when elaborating the term. So, some such cases need to be fixed by making it `simp_rw [and_comm (_ ≤ _)]`. This is because `simp_rw`, unlike `rw`, fully elaborates the rewrite rules before using them. So, when we get the new rewrite tactic, this problem will mostly go away.
See also https://leanprover.zulipchat.com/#narrow/channel/113488-general/topic/Any.20infimum.20based.20version.20of.20.60OmegaCompletePartialOrder.60.3F/near/579333629
---
[](https://gitpod.io/from-referrer/)
|
t-meta
maintainer-merge
|
345/0 |
Mathlib.lean,Mathlib/Tactic.lean,Mathlib/Tactic/SetNotationForOrder.lean,MathlibTest/SetNotationForOrder.lean |
4 |
50 |
['JovanGerb', 'Vierkantor', 'github-actions', 'thorimur'] |
alexjbest and thorimur assignee:alexjbest assignee:thorimur |
3-64949 3 days ago |
15-51260 15 days ago |
28-78538 28 days |
| 36442 |
SnirBroshi author:SnirBroshi |
feat(Data/Sym/Sym2/Card): cardinality theorems about `Sym2 α` |
---
[](https://gitpod.io/from-referrer/)
|
t-data
maintainer-merge
|
100/0 |
Mathlib.lean,Mathlib/Data/Set/Image.lean,Mathlib/Data/Sym/Sym2/Card.lean |
3 |
17 |
['SnirBroshi', 'github-actions', 'joneugster', 'themathqueen'] |
joneugster assignee:joneugster |
3-54758 3 days ago |
3-57011 3 days ago |
35-26994 35 days |
| 38314 |
pedroscortes author:pedroscortes |
feat(CategoryTheory/Monoidal): tensorμ_braid_swap and tensor-product IsCommComonObj |
## Summary
Two symmetric-monoidal coherence results:
1. `MonoidalCategory.tensorμ_braid_swap` (in `Monoidal/Braided/Basic.lean`) —
canonical rearrangement `tensorμ A A Y Y` intertwines the braiding on `A ⊗ Y`
with the pair of braidings on `A` and `Y`. Sibling of
`CategoryTheory.MonObj.mul_braiding`.
2. Tensor-product instance for `IsCommComonObj` (in `Monoidal/CommComon_.lean`):
if `A, B` carry commutative comonoid structures in a symmetric monoidal
category, so does `A ⊗ B`. Fills a gap alongside the existing
`instCommComonObjUnit` and `instIsCommComonObjOfCartesian`.
## Downstream consumer
The `IsCommComonObj` tensor-product instance is load-bearing for an external
library (markovcat, formalising Fritz–Klingler Markov categories). |
t-category-theory
new-contributor
maintainer-merge
|
15/0 |
Mathlib/CategoryTheory/Monoidal/Braided/Basic.lean,Mathlib/CategoryTheory/Monoidal/CommComon_.lean |
2 |
17 |
['dagurtomas', 'github-actions', 'pedroscortes', 'robin-carlier'] |
dagurtomas assignee:dagurtomas |
3-45553 3 days ago |
3-77562 3 days ago |
6-60404 6 days |
| 38468 |
Vierkantor author:Vierkantor |
chore(*): triage `simpNF` adaptation notes |
This PR reinstates some `@[simp]` attributes that were removed due to various adaptation. At least if I run `#lint` in the files, the `simpNF` linter does not complain. So hopefully we should be able to add those lemmas to the simp set again.
---
[](https://gitpod.io/from-referrer/)
|
tech debt
maintainer-merge
|
14/39 |
Mathlib/Algebra/Algebra/Opposite.lean,Mathlib/Algebra/Algebra/Unitization.lean,Mathlib/Algebra/Category/FGModuleCat/Basic.lean,Mathlib/Algebra/Star/StarAlgHom.lean,Mathlib/Analysis/SpecialFunctions/Complex/LogBounds.lean,Mathlib/Analysis/SpecialFunctions/Exp.lean,Mathlib/Geometry/Manifold/MFDeriv/FDeriv.lean,Mathlib/GroupTheory/Coset/Basic.lean,Mathlib/RepresentationTheory/Coinvariants.lean,Mathlib/Topology/Instances/Real/Lemmas.lean |
10 |
2 |
['github-actions', 'grunweg'] |
jcommelin assignee:jcommelin |
3-45544 3 days ago |
3-83765 3 days ago |
3-83556 3 days |
| 38457 |
yuanyi-350 author:yuanyi-350 |
refactor(NumberTheory): golf `Mathlib/NumberTheory/Dioph` |
- golfs `Mathlib/NumberTheory/Dioph` by replacing the arithmetic proof in `sub_dioph` with `grind`
- simplifies `div_dioph` by splitting on `y = 0 ∨ 0 < y`, then closing the positive case with `Nat.div_eq_iff` and `grind`
Extracted from #38144
[](https://gitpod.io/from-referrer/) |
codex
t-number-theory
LLM-generated
maintainer-merge
|
7/18 |
Mathlib/NumberTheory/Dioph.lean |
1 |
12 |
['github-actions', 'grunweg', 'leanprover-radar', 'yuanyi-350'] |
tb65536 assignee:tb65536 |
2-45170 2 days ago |
3-42959 3 days ago |
3-44862 3 days |
| 38093 |
mortarsanjaya author:mortarsanjaya |
feat(Algebra/Order/Ring/Unbundled/Basic): add a generalization of `two_mul_le_add_of_sq_eq_mul` |
The equality `r^2 = a * b` in the hypothesis can be weakened to `r^2 ≤ a * b`.
The implementation requires adding an appropriate `ZeroLEOneClass` instance.
---
[](https://gitpod.io/from-referrer/)
|
t-algebra
new-contributor
maintainer-merge
label:t-algebra$ |
16/7 |
Mathlib/Algebra/Order/BigOperators/Ring/Finset.lean,Mathlib/Algebra/Order/Ring/Unbundled/Basic.lean |
2 |
13 |
['github-actions', 'leanprover-radar', 'mortarsanjaya', 'themathqueen'] |
themathqueen assignee:themathqueen |
1-68160 1 day ago |
7-57526 7 days ago |
12-20512 12 days |
| 34797 |
vlad902 author:vlad902 |
feat(SimpleGraph): `cycleGraph.cycle` is a cycle |
(A follow-up PR will show that `cycleGraph.cycle` is also hamiltonian.)
---
- [x] depends on: #35360
- [x] depends on: #34766
- [x] depends on: #34796
[](https://gitpod.io/from-referrer/)
|
t-combinatorics
maintainer-merge
|
32/1 |
Mathlib/Combinatorics/SimpleGraph/Circulant.lean |
1 |
8 |
['Ruben-VandeVelde', 'YaelDillies', 'github-actions', 'mathlib-dependent-issues', 'vlad902'] |
nobody |
1-19968 1 day ago |
39-71715 39 days ago |
41-14025 41 days |
| 38345 |
emlis42 author:emlis42 |
feat(NumberTheory): add Int.divisors |
This PR adds `Int.divisors` in `Mathlib/NumberTheory/Divisors.lean`.
Defines `Int.divisors` as the disjoint union of positive and negative `Nat.divisors`.
Basic lemmas:
* `mem_divisors`
* `divisors_zero`, `divisors_eq_empty`, `divisors_one`
* `one_mem_divisors`, `neg_one_mem_divisors`
* `nonempty_divisors`
* `mem_divisors_self`
* `divisors_neg`
Lemmas relating to `divisorsAntidiag`:
* `image_fst_divisorsAntidiag`
* `image_snd_divisorsAntidiag` |
t-number-theory
new-contributor
maintainer-merge
|
61/2 |
Mathlib/NumberTheory/Divisors.lean |
1 |
21 |
['Multramate', 'SnirBroshi', 'emlis42', 'github-actions', 'tb65536'] |
tb65536 assignee:tb65536 |
1-4300 1 day ago |
5-81816 5 days ago |
6-44948 6 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 |
| 36216 |
michaellee94 author:michaellee94 |
feat(CategoryTheory): characterize pullback squares via the `Over` category |
---
[](https://gitpod.io/from-referrer/)
|
t-category-theory
new-contributor
maintainer-merge
awaiting-author
|
47/0 |
Mathlib/CategoryTheory/Limits/Shapes/Pullback/IsPullback/Basic.lean |
1 |
18 |
['dagurtomas', 'github-actions', 'joelriou', 'michaellee94'] |
robin-carlier assignee:robin-carlier |
32-60510 1 month ago |
32-60510 32 days ago |
2-50782 2 days |
| 37057 |
erdOne author:erdOne |
feat(AlgebraicTopology): `SimplexCategory.toTop_map_δ_apply` |
---
[](https://gitpod.io/from-referrer/)
|
t-algebraic-topology
maintainer-merge
awaiting-author
merge-conflict
|
48/2 |
Mathlib/AlgebraicTopology/CechNerve.lean,Mathlib/AlgebraicTopology/SimplexCategory/Basic.lean,Mathlib/AlgebraicTopology/SimplexCategory/Defs.lean,Mathlib/AlgebraicTopology/TopologicalSimplex.lean,Mathlib/Data/Fin/SuccPred.lean |
5 |
17 |
['Raph-DG', 'dagurtomas', 'erdOne', 'github-actions', 'joelriou', 'mathlib-merge-conflicts', 'riccardobrasca'] |
robin-carlier assignee:robin-carlier |
20-27313 20 days ago |
21-74953 21 days ago |
4-49805 4 days |
| 37603 |
Parcly-Taxel author:Parcly-Taxel |
refactor: review of `SetSemiring` |
* Rename `Set.up` and `SetSemiring.down` to `SetSemiring.ofSet` and `SetSemiring.toSet` respectively. Unprotect both and make them equivalences, following `FreeMonoid`.
* Derive `CompleteAtomicBooleanAlgebra` for `SetSemiring` immediately.
* Add `imageHom_id` and `imageHom_comp`. The three existing lemmas about `imageHom` are coalesced into `imageHom_apply`.
Ultimately inspired by https://github.com/leanprover-community/mathlib4/pull/36934#issuecomment-4183475568. |
maintainer-merge |
120/165 |
Mathlib/Algebra/Algebra/Operations.lean,Mathlib/Data/Set/Semiring.lean |
2 |
41 |
['Parcly-Taxel', 'YaelDillies', 'eric-wieser', 'github-actions', 'mathlib-merge-conflicts', 'sgouezel'] |
nobody |
19-83700 19 days ago |
19-83958 19 days ago |
21-24753 21 days |
| 33443 |
sahanwijetunga author:sahanwijetunga |
feat: Define Isometries of Bilinear Spaces |
---
We define Isometries of Bilinear Spaces, closely following the implementation of isometries of quadratic spaces.
[](https://gitpod.io/from-referrer/)
|
t-algebra
new-contributor
maintainer-merge
label:t-algebra$ |
278/0 |
Mathlib.lean,Mathlib/LinearAlgebra/BilinearForm/Isometry.lean,Mathlib/LinearAlgebra/BilinearForm/IsometryEquiv.lean |
3 |
25 |
['github-actions', 'robin-carlier', 'sahanwijetunga'] |
mattrobball assignee:mattrobball |
18-21547 18 days ago |
18-21706 18 days ago |
66-48605 66 days |
| 37846 |
grunweg author:grunweg |
fix(positivity): still prove non-negativity in the `Nat.cast` extension if positivity fails |
---
[](https://gitpod.io/from-referrer/)
|
t-meta
maintainer-merge
|
11/2 |
Mathlib/Tactic/Positivity/Basic.lean,MathlibTest/positivity.lean |
2 |
4 |
['dwrensha', 'github-actions'] |
dwrensha assignee:dwrensha |
17-43594 17 days ago |
18-5814 18 days ago |
18-5607 18 days |
| 37053 |
artie2000 author:artie2000 |
refactor(Analysis/Convex/Cone): use `PointedCone` in Riesz extension theorem |
Change the statement of the Riesz extension theorem to take a `PointedCone` rather than a `ConvexCone`.
This PR is part of a series replacing `ConvexCone` with `PointedCone`. https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/Replacing.20.60ConvexCone.60.20with.20.60PointedCone.60/near/581184307
---
[](https://gitpod.io/from-referrer/)
|
t-convex-geometry
maintainer-merge
|
15/12 |
Mathlib/Analysis/Convex/Cone/Extension.lean,Mathlib/Geometry/Convex/Cone/Pointed.lean |
2 |
8 |
['YaelDillies', 'artie2000', 'github-actions', 'mathlib-merge-conflicts', 'ocfnash'] |
nobody |
14-855 14 days ago |
14-883 14 days ago |
33-42111 33 days |
| 36308 |
SnirBroshi author:SnirBroshi |
feat(Combinatorics/SimpleGraph/Subgraph): a couple of `subgraphOfAdj` lemmas |
Also golf a lemma (it's one line longer but it looks simpler to me).
---
[](https://gitpod.io/from-referrer/)
|
t-combinatorics
maintainer-merge
|
14/5 |
Mathlib/Combinatorics/SimpleGraph/Subgraph.lean |
1 |
4 |
['SnirBroshi', 'YaelDillies', 'github-actions'] |
b-mehta assignee:b-mehta |
13-45402 13 days ago |
52-25060 52 days ago |
52-24851 52 days |
| 37400 |
SnirBroshi author:SnirBroshi |
feat(Combinatorics/SimpleGraph/Acyclic): endpoints of a path have at most one neighbor in the path |
---
[](https://gitpod.io/from-referrer/)
|
t-combinatorics
maintainer-merge
|
15/0 |
Mathlib/Combinatorics/SimpleGraph/Acyclic.lean |
1 |
5 |
['Rida-Hamadani', 'Ruben-VandeVelde', 'SnirBroshi', 'github-actions'] |
nobody |
12-40123 12 days ago |
28-39687 28 days ago |
28-39478 28 days |
| 37420 |
artie2000 author:artie2000 |
refactor: change definitions to avoid `ConvexCone` |
Change the definitions of `PointedCone.positive` and `PointedCone.closure` to avoid mentioning `ConvexCone`.
This PR is part of a series deprecating `ConvexCone`: https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/Replacing.20.60ConvexCone.60.20with.20.60PointedCone.60/with/582738985
---
[](https://gitpod.io/from-referrer/)
|
t-convex-geometry
maintainer-merge
|
10/4 |
Mathlib/Analysis/Convex/Cone/Closure.lean,Mathlib/Geometry/Convex/Cone/Pointed.lean |
2 |
3 |
['YaelDillies', 'github-actions', 'mathlib-merge-conflicts', 'ooovi', 'vihdzp'] |
nobody |
12-6907 12 days ago |
12-6871 12 days ago |
27-27225 27 days |
| 37588 |
Vierkantor author:Vierkantor |
feat(Linter/DocString): ignore Verso linter errors about links and LaTeX |
I went through [the weekly linting log](https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/Weekly.20linting.20log/near/582485221) and found most of the warnings come from three sources. All of these are sensical syntax in our current Markdown dialect, and should be fixed automatically by a script, instead of manually. I expect after these changes we'll be down to hundreds of linter errors rather than two thousand.
* References [between square brackets] without a following link URL. Verso has different implementations for references depending on what kind they are, and since there are a thousand references we should be using a script to fix these.
* Autolinks: bare URLs or URLs between . Autolinks are intentionally not supported by Verso but replacing every `https://...` with `[https://...](https://...)` would be too noisy.
* LaTeX blocks: Verso does have TeX blocks but with an incompatible syntax. Better to fix it with a script.
I ended up using preprocessing in addition to postprocessing to filter out errors: using the error message we can determine whether it is a reference, but for errors caused by autolinks and LaTeX blocks I couldn't figure out how to do so easily: the information about the parse error does report a string position but this is always the last character of the docstring. So instead we modify the docstring before it is passed into Verso to get rid of the offending syntax.
---
[](https://gitpod.io/from-referrer/)
|
t-linter
large-import
maintainer-merge
|
113/5 |
Mathlib/Tactic/Linter/DocString.lean,MathlibTest/DocString.lean |
2 |
18 |
['Vierkantor', 'github-actions', 'thorimur'] |
thorimur assignee:thorimur |
11-3133 11 days ago |
11-3191 11 days ago |
13-85063 13 days |
| 37808 |
JovanGerb author:JovanGerb |
feat(Translate): locally modify name guessing dictionaries |
This PR adds the feature to `to_dual` and `to_additive` that you can now locally modify the name translation dictionary.
With this change, we run the risk of having the automated translations being harder to predict. For this reason, the changes to the dictionary do not persisted through imports. Instead, the change lasts until the end of the file (though it ignores sections).
See https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/Order.20dual.20tactic/near/580834166
---
[](https://gitpod.io/from-referrer/)
|
t-meta
maintainer-merge
|
111/39 |
Mathlib/Order/GaloisConnection/Basic.lean,Mathlib/Order/GaloisConnection/Defs.lean,Mathlib/Order/Interval/Set/Basic.lean,Mathlib/Order/Interval/Set/Disjoint.lean,Mathlib/Tactic/Translate/Core.lean,Mathlib/Tactic/Translate/GuessName.lean,Mathlib/Tactic/Translate/ToAdditive.lean,Mathlib/Tactic/Translate/ToDual.lean,MathlibTest/ToDual.lean |
9 |
4 |
['JovanGerb', 'bryangingechen', 'github-actions', 'joneugster'] |
joneugster assignee:joneugster |
11-3000 11 days ago |
15-85380 15 days ago |
16-6005 16 days |
| 38179 |
wwylele author:wwylele |
feat(Combinatorics): Pentagonal numbers |
Introduces definition of pentagonal number https://en.wikipedia.org/wiki/Pentagonal_number in preparation for pentagonal number theorem.
---
This is extracted from #33143 as suggested. I only put a few elementary properties here to limit the code change size.
The future file structure will be
- Combinatorics/Enumerative/Pentagonal.lean (this PR)
- Topology/Algebra/InfiniteSum/Pentagonal.lean + RingTheory/PowerSeries/Pentagonal.lean (#33143, depends on previous one) pentagonal theorem in generic form and for power series
- Combinatorics/Enumerative/Partition/Pentagonal.lean (future PR, depends on the previous one): connection between partition and pentagonal numbers
This originally comes from my own repo https://github.com/wwylele/PentagonalNumberTheorem. In the past, there were also PR #31156 and #31362 independently worked by @BeibeiX0 on the same topic, and I tried avoiding stepping on each other's toes when making #33143. Then #31156 and #31362 were closed for unclear reason.
As I mostly rewrote the code based on my own repo, I only put my name here, but given that I unavoidably took inspiration from other PRs, if @BeibeiX0 would like his name to be added to co-author and copyright notice, I am happy to do so.
[](https://gitpod.io/from-referrer/)
|
t-combinatorics
maintainer-merge
|
75/0 |
Mathlib.lean,Mathlib/Combinatorics/Enumerative/Pentagonal.lean |
2 |
27 |
['copilot-pull-request-reviewer', 'github-actions', 'tb65536', 'wwylele'] |
nobody |
10-53042 10 days ago |
10-53726 10 days ago |
10-62303 10 days |
| 37931 |
Vierkantor author:Vierkantor |
chore(Tactic): make the (deprecated) `replace` syntax a `@[tactic_alt]` |
This PR replaces the tactic docstring for Mathlib's version of `replace` with a `@[tactic_alt]` attribute + `tactic_extension`. Also update the module docs which did not get updated when `replace` got upstreamed to core Lean.
---
[](https://gitpod.io/from-referrer/)
|
documentation
t-meta
maintainer-merge
|
7/31 |
Mathlib/Tactic/Replace.lean |
1 |
2 |
['github-actions', 'joneugster'] |
dwrensha assignee:dwrensha |
9-45299 9 days ago |
14-82287 14 days ago |
14-82800 14 days |
| 37868 |
Jun2M author:Jun2M |
feat(Combinatorics/Graph): map on `Graph` |
This PR introduces vertex map on graphs, `map`.
This creates a new file `Maps` which will be home to `map` and morphisms between `Graph`s.
Co-authored-by: Peter Nelson [apn.uni@gmail.com](mailto:apn.uni@gmail.com)
---
[](https://gitpod.io/from-referrer/)
|
t-combinatorics
maintainer-merge
|
108/0 |
Mathlib.lean,Mathlib/Combinatorics/Graph/Maps.lean |
2 |
8 |
['Jun2M', 'YaelDillies', 'b-mehta', 'github-actions', 'mathlib-merge-conflicts'] |
nobody |
7-72250 7 days ago |
7-72250 7 days ago |
18-249 18 days |
| 38301 |
SnirBroshi author:SnirBroshi |
feat(Algebra/Group/Commutator): tag `addCommutatorElement` as a scoped instance |
#34784 additivized commutators and made the multiplicative commutator instance available under `open scoped commutatorElement`.
This makes the additive instance available under `open scoped addCommutatorElement`.
---
~~Should we instead make it scoped under the `addCommutatorElement` namespace?
The existing usages of additive commutators come from decls marked with `open scoped commutatorElement in @[to_additive]`, and `to_additive` seemingly doesn't mind that the additivized version is not an instance. So I think they don't have to live in the same namespace.~~
[](https://gitpod.io/from-referrer/)
|
t-algebra
maintainer-merge
label:t-algebra$ |
6/0 |
Mathlib/Algebra/Group/Commutator.lean |
1 |
6 |
['SnirBroshi', 'github-actions', 'tb65536'] |
nobody |
7-70591 7 days ago |
7-73046 7 days ago |
7-73251 7 days |
| 38172 |
joelriou author:joelriou |
feat(AlgebraicTopology/SimplicialSet): Mulstruct.mulOne and oneMul |
We introduce definitions `SSet.PtSimplex.MulStruct.oneMul/mulOne` which shall later be interpreted as an explanation for the relations satisfied by the neutral element for the multiplication on homotopy groups of Kan complexes.
---
[](https://gitpod.io/from-referrer/)
|
t-algebraic-topology
maintainer-merge
|
53/0 |
Mathlib/AlgebraicTopology/SimplicialSet/KanComplex/MulStruct.lean |
1 |
6 |
['github-actions', 'joelriou', 'robin-carlier'] |
robin-carlier assignee:robin-carlier |
7-4802 7 days ago |
7-5671 7 days ago |
10-74991 10 days |
| 38184 |
tb65536 author:tb65536 |
chore(Algebra/Algebra/Tower): make `Algebra.algHom` an alias of `IsScalarTower.toAlgHom` |
`Algebra.algHom` is a duplicate of `IsScalarTower.ofAlgHom` so I've made it an alias to make this clearer.
Zulip thread: [#mathlib4 > duplication: Algebra.algHom = IsScalarTower.toAlgHom](https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/duplication.3A.20Algebra.2EalgHom.20.3D.20IsScalarTower.2EtoAlgHom/with/569828872)
---
[](https://gitpod.io/from-referrer/)
|
t-ring-theory
t-algebra
maintainer-merge
label:t-algebra$ |
27/26 |
Mathlib/Algebra/Algebra/Hom.lean,Mathlib/Algebra/Algebra/Tower.lean |
2 |
14 |
['acmepjz', 'github-actions', 'tb65536', 'themathqueen'] |
nobody |
6-57697 6 days ago |
6-72871 6 days ago |
10-55753 10 days |
| 37291 |
IvanRenison author:IvanRenison |
refactor(Combinatorics/SimpleGraph): move `chromaticNumber_le_two_iff_isBipartite` and `chromaticNumber_eq_two_iff` to `Bipartite` file |
---
[](https://gitpod.io/from-referrer/)
|
t-combinatorics
maintainer-merge
|
10/12 |
Mathlib/Combinatorics/SimpleGraph/Bipartite.lean,Mathlib/Combinatorics/SimpleGraph/Coloring/Constructions.lean |
2 |
3 |
['Ruben-VandeVelde', 'github-actions', 'mathlib-merge-conflicts'] |
nobody |
6-51930 6 days ago |
6-51952 6 days ago |
31-49705 31 days |
| 37738 |
khwilson author:khwilson |
feat(Topology/Order/Bornology): generalize `cobounded_eq` |
`Real.cobounded_eq` and `Int.cobounded_eq` are used in several places throughout Mathlib. They are currently proved in terms of the Metric topology on `Int` and `Real`, but they're really properties of the order bornology on those objects.
Generalize those constructions to `IsOrderBornology` for `LinearOrder`'s and add a few more constructions that are true in other circumstances, e.g., `cobounded NNReal = .atTop` follows from the fact that `NNReal` is both `NoMaxOrder` and `OrderBot`.
---
[](https://gitpod.io/from-referrer/)
|
maintainer-merge
t-order
|
57/18 |
Mathlib/Analysis/Polynomial/Basic.lean,Mathlib/Analysis/SpecialFunctions/Complex/LogBounds.lean,Mathlib/Topology/Instances/Int.lean,Mathlib/Topology/Instances/Real/Lemmas.lean,Mathlib/Topology/Order/Bornology.lean |
5 |
14 |
['YaelDillies', 'github-actions', 'khwilson', 'vihdzp'] |
bryangingechen assignee:bryangingechen |
6-45568 6 days ago |
21-3772 21 days ago |
21-4406 21 days |
| 34854 |
GrigorenkoPV author:GrigorenkoPV |
chore(Combinatorics/Enumerative/Catalan): split into `Basic` & `Tree` |
---
Split off from #34853
[](https://gitpod.io/from-referrer/)
|
new-contributor
t-combinatorics
maintainer-merge
awaiting-author
|
225/194 |
Mathlib.lean,Mathlib/Combinatorics/Enumerative/Catalan.lean,Mathlib/Combinatorics/Enumerative/Catalan/Basic.lean,Mathlib/Combinatorics/Enumerative/Catalan/Tree.lean,Mathlib/Combinatorics/Enumerative/DyckWord.lean,Mathlib/RingTheory/PowerSeries/Catalan.lean |
6 |
7 |
['SnirBroshi', 'Vierkantor', 'YaelDillies', 'github-actions', 'mathlib-merge-conflicts', 'vihdzp'] |
nobody |
5-66484 5 days ago |
16-9630 16 days ago |
45-59230 45 days |
| 37985 |
Raph-DG author:Raph-DG |
feat(Topology): intersections preserve Notherian-ness and Quasisober-ness |
In this PR we prove some basic topology lemmas about the preservation of noetherianness and quasisoberness under intersections.
---
[](https://gitpod.io/from-referrer/)
|
t-topology
maintainer-merge
|
25/0 |
Mathlib/Topology/NoetherianSpace.lean,Mathlib/Topology/Sober.lean |
2 |
23 |
['Raph-DG', 'chrisflav', 'github-actions', 'grunweg', 'vihdzp'] |
PatrickMassot assignee:PatrickMassot |
5-65736 5 days ago |
5-65759 5 days ago |
14-40776 14 days |
| 38257 |
joelriou author:joelriou |
feat(CategoryTheory): MorphismProperty.single |
---
[](https://gitpod.io/from-referrer/)
|
t-category-theory
maintainer-merge
|
63/1 |
Mathlib/CategoryTheory/MorphismProperty/Basic.lean,Mathlib/CategoryTheory/MorphismProperty/IsSmall.lean,Mathlib/CategoryTheory/ObjectProperty/Local.lean |
3 |
6 |
['github-actions', 'joelriou', 'robin-carlier'] |
robin-carlier assignee:robin-carlier |
5-45248 5 days ago |
6-85151 6 days ago |
8-67943 8 days |
| 38381 |
euprunin author:euprunin |
chore: golf using `grind` |
The goal of this PR is to decrease the number of times lemmas are called explicitly. Any decrease in compilation time is a welcome side effect, although it is not a primary objective.
Trace profiling results (differences <30 ms considered measurement noise):
* `✅️ SimpleGraph.Walk.takeUntil_eq_take`: 258 ms before, 206 ms after 🎉
Profiled using `set_option trace.profiler true in`.
---
[](https://gitpod.io/from-referrer/)
|
t-combinatorics
maintainer-merge
|
2/6 |
Mathlib/Combinatorics/SimpleGraph/Walk/Decomp.lean |
1 |
5 |
['SnirBroshi', 'euprunin', 'github-actions', 'grunweg'] |
nobody |
5-9801 5 days ago |
5-58888 5 days ago |
5-58679 5 days |
| 36416 |
j-loreaux author:j-loreaux |
feat(Analysis/CStarAlgebra): norms of sums of orthogonal selfadjoint elements |
---
- [ ] depends on: #36407
- [ ] depends on: #37569
[](https://gitpod.io/from-referrer/)
|
t-analysis
maintainer-merge
|
126/1 |
Mathlib/Algebra/Star/BigOperators.lean,Mathlib/Algebra/Star/SelfAdjoint.lean,Mathlib/Analysis/CStarAlgebra/Fuglede.lean,Mathlib/Analysis/CStarAlgebra/GelfandDuality.lean |
4 |
22 |
['github-actions', 'grunweg', 'j-loreaux', 'loefflerd', 'mathlib-dependent-issues', 'mathlib-merge-conflicts', 'themathqueen'] |
loefflerd assignee:loefflerd |
4-73350 4 days ago |
4-73422 4 days ago |
22-70299 22 days |
| 36451 |
SnirBroshi author:SnirBroshi |
feat(Combinatorics/SimpleGraph/Matching): `edgeSet` is injective and strictly monotonic on matchings, and more API |
---
[](https://gitpod.io/from-referrer/)
|
t-combinatorics
maintainer-merge
|
36/10 |
Mathlib/Combinatorics/SimpleGraph/Matching.lean,Mathlib/Combinatorics/SimpleGraph/Subgraph.lean |
2 |
13 |
['SnirBroshi', 'YaelDillies', 'github-actions', 'mathlib-merge-conflicts'] |
nobody |
4-69286 4 days ago |
4-74287 4 days ago |
33-25628 33 days |
| 37864 |
JovanGerb author:JovanGerb |
chore: reorder arguments of `AddMonoidHom.map_zsmul` |
This PR modifies `AddMonoidHom.map_nsmul`, `AddMonoidHom.map_zsmul` and `AddMonoidHom.map_zsmul'` so that their order of arguments is as expected. This is then consistent with `map_nsmul`/`map_zsmul`.
---
[](https://gitpod.io/from-referrer/)
|
t-algebra
maintainer-merge
label:t-algebra$ |
21/22 |
Mathlib/Algebra/Category/Grp/ZModuleEquivalence.lean,Mathlib/Algebra/Group/Hom/Defs.lean,Mathlib/Algebra/GroupWithZero/Action/Defs.lean,Mathlib/Algebra/Module/CharacterModule.lean,Mathlib/Algebra/Module/Equiv/Basic.lean,Mathlib/Analysis/Complex/Circle.lean,Mathlib/Analysis/SpecialFunctions/Trigonometric/Angle.lean,Mathlib/CategoryTheory/Linear/Basic.lean,Mathlib/CategoryTheory/Linear/LinearFunctor.lean |
9 |
8 |
['JovanGerb', 'github-actions', 'mathlib-merge-conflicts', 'themathqueen'] |
nobody |
4-40574 4 days ago |
11-16430 11 days ago |
16-27518 16 days |
| 38233 |
mbkybky author:mbkybky |
feat(Algebra/Module/Projective): add `ULift` and `Shrink` lemmas for `Module.Projective` |
Add `ULift` and `Shrink` lemmas for `Module.Projective`.
---
[](https://gitpod.io/from-referrer/)
|
t-algebra
maintainer-merge
label:t-algebra$ |
15/3 |
Mathlib/Algebra/Category/ModuleCat/Ulift.lean,Mathlib/Algebra/Module/Projective.lean |
2 |
7 |
['github-actions', 'mbkybky', 'robin-carlier'] |
nobody |
4-22615 4 days ago |
4-22751 4 days ago |
6-63208 6 days |
| 30185 |
alreadydone author:alreadydone |
feat(MathlibTest): kernel reduction of nsmul on elliptic curve over ZMod |
Co-authored-by: @SteffenReith
---
- [x] depends on: #30144
- [x] depends on: #30181
[](https://gitpod.io/from-referrer/)
|
t-algebra
t-number-theory
t-algebraic-geometry
maintainer-merge
label:t-algebra$ |
29/0 |
MathlibTest/EllipticCurve.lean |
1 |
11 |
['alreadydone', 'github-actions', 'joneugster', 'mathlib4-dependent-issues-bot', 'mathlib4-merge-conflict-bot'] |
joneugster assignee:joneugster |
4-22020 4 days ago |
10-12891 10 days ago |
11-28204 11 days |
| 36401 |
JovanGerb author:JovanGerb |
feat(positivity): positivity extension for `a - b` |
This PR adds support in `positivity` for proving things about subtraction. For example, if the goal is `0 < a - b`, and there is a local hypothesis of type `b < a`, then we close the goal.
The motivation is that we want `positivity` to be a flexible tactic. So, when trying to prove `0 < a - b` using a local hypothesis, we should look for the simp normal form of this, which is `b < a`.
---
[Zulip discussion](https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/Can.20I.20make.20positivity.20work.20for.20this.3F/near/578277240)
[](https://gitpod.io/from-referrer/)
|
t-meta
maintainer-merge
|
63/26 |
Mathlib/Analysis/Calculus/Taylor.lean,Mathlib/Analysis/Complex/AbelLimit.lean,Mathlib/Analysis/Complex/BorelCaratheodory.lean,Mathlib/Analysis/Complex/Hadamard.lean,Mathlib/Analysis/Convex/BetweenList.lean,Mathlib/Analysis/SpecialFunctions/Log/Deriv.lean,Mathlib/Analysis/SpecificLimits/FloorPow.lean,Mathlib/Geometry/Manifold/Riemannian/PathELength.lean,Mathlib/Tactic/Positivity/Basic.lean,MathlibTest/positivity.lean |
10 |
13 |
['JovanGerb', 'Vierkantor', 'github-actions', 'hrmacbeth', 'j-loreaux', 'joneugster', 'leanprover-radar'] |
joneugster assignee:joneugster |
4-19548 4 days ago |
6-85741 6 days ago |
35-69923 35 days |
| 37439 |
ADedecker author:ADedecker |
feat: UniformConvergenceCLM version of ContinuousLinearEquiv.arrowCongr |
The absence of `@[simp]` attribute comes from the fact that the generated lemmas would break the API boundary.
I think the solution to all of this will eventually be to define generic type aliases `Topology.WithUniform` / `Topology.WithUniformOn` / `Topology.WithPointwise`... which will behave like [WithLp](https://leanprover-community.github.io/mathlib4_docs/Mathlib/Analysis/Normed/Lp/WithLp.html#WithLp) (thus disabling the very-abused defeqs around here).
---
- [x] depends on: #37614
[](https://gitpod.io/from-referrer/)
|
t-topology
maintainer-merge
|
182/3 |
Mathlib/Topology/Algebra/Module/Equiv.lean,Mathlib/Topology/Algebra/Module/Spaces/CompactConvergenceCLM.lean,Mathlib/Topology/Algebra/Module/Spaces/ContinuousLinearMap.lean,Mathlib/Topology/Algebra/Module/Spaces/UniformConvergenceCLM.lean |
4 |
9 |
['ADedecker', 'github-actions', 'loefflerd', 'mathlib-dependent-issues', 'mathlib-merge-conflicts'] |
loefflerd assignee:loefflerd |
4-17465 4 days ago |
4-17509 4 days ago |
20-77993 20 days |
| 36423 |
kim-em author:kim-em |
perf: decompress already-cached files concurrently with downloads |
This PR builds on https://github.com/leanprover-community/mathlib4/pull/32987 (pipeline downloads and decompression) and https://github.com/leanprover-community/mathlib4/pull/36367 (fix: decompress already downloaded files).
Previously, already-cached `.ltar` files were only decompressed after all downloads completed, in the final `unpackCache` sweep. This PR starts decompressing them concurrently with downloads by spawning `leantar` as a background task before the download phase begins.
The two decompression paths operate on disjoint file sets (pre-cached vs newly downloaded), so there is no conflict. In the common case where a user has most files cached but a few hundred to download, this overlaps several seconds of decompression with network I/O.
🤖 Prepared with Claude Code |
LLM-generated
CI
t-meta
maintainer-merge
|
79/27 |
Cache/IO.lean,Cache/Requests.lean |
2 |
7 |
['github-actions', 'joneugster', 'kim-em'] |
joneugster assignee:joneugster |
4-15915 4 days ago |
7-48182 7 days ago |
35-37970 35 days |
| 36201 |
themathqueen author:themathqueen |
feat(Analysis/CStarAlgebra): set of star projections equals the extreme points of the nonnegative closed unit ball |
An element in a non-unital C⋆-algebra is a projection iff it is an extreme point of the nonnegative closed unit ball. This is from 1.6.2 in Sakai's C⋆-algebras and W⋆-algebras (the proof is different though).
Co-authored-by: Jon Bannon <59937998+JonBannon@users.noreply.github.com>
---
- [x] depends on: #35997
[](https://gitpod.io/from-referrer/)
|
t-analysis
maintainer-merge
|
103/0 |
Mathlib.lean,Mathlib/Algebra/Ring/Defs.lean,Mathlib/Analysis/CStarAlgebra/Extreme.lean,docs/references.bib |
4 |
16 |
['github-actions', 'j-loreaux', 'loefflerd', 'mathlib-dependent-issues', 'mathlib-merge-conflicts', 'mcdoll', 'themathqueen'] |
mcdoll assignee:mcdoll |
4-14386 4 days ago |
18-53091 18 days ago |
47-81960 47 days |
| 37171 |
SnirBroshi author:SnirBroshi |
chore(Data/Int/Init): generalize `le_induction` from `Prop` to `Sort*` + def lemmas |
---
- Generallise `le_induction` from `Prop` to `Sort*` and rename to `leInduction`
- Add a few lemmas
- Simplify proofs using `lia`
- Move `inductionOn'_add_one`
[Zulip 💬](https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/Add.20note.20to.20help.20search.20similar.20thms/near/535331432)
[](https://gitpod.io/from-referrer/)
|
t-data
large-import
maintainer-merge
|
56/48 |
Mathlib/Data/Int/Basic.lean,Mathlib/Data/Int/Init.lean,Mathlib/GroupTheory/CoprodI.lean |
3 |
9 |
['SnirBroshi', 'github-actions', 'joneugster', 'mathlib-merge-conflicts', 'plp127'] |
joneugster assignee:joneugster |
3-74775 3 days ago |
27-34624 27 days ago |
28-42117 28 days |
| 37347 |
JovanGerb author:JovanGerb |
feat: implementation of `@[use_set_notation_for_order]` |
This PR allows the use of `⊆` notation while the underlying constant is `≤`.
Similarly for `⊂`/`<`, `⊇`/`≥` and `⊃`/`>`.
- The idea is to later extend this feature to other set notation constants, such as union/intersection.
- There are some types for which we cannot use `LE.le` as the underlying constant, such as `List` and `Multiset`. So, the elaborator for the `⊆` notation needs to make a decision which underlying constant to elaborate to, depending on the type. Sometimes the type is not known yet, which makes things awkward. Most of these cases are solved by delaying the elaboration until later when the type is known.
- However, in some cases this doesn't work either, such as `simp_rw [and_comm (_ ⊆ _)]`, where it is impossible to tell the type when elaborating the term. So, some such cases need to be fixed by making it `simp_rw [and_comm (_ ≤ _)]`. This is because `simp_rw`, unlike `rw`, fully elaborates the rewrite rules before using them. So, when we get the new rewrite tactic, this problem will mostly go away.
See also https://leanprover.zulipchat.com/#narrow/channel/113488-general/topic/Any.20infimum.20based.20version.20of.20.60OmegaCompletePartialOrder.60.3F/near/579333629
---
[](https://gitpod.io/from-referrer/)
|
t-meta
maintainer-merge
|
345/0 |
Mathlib.lean,Mathlib/Tactic.lean,Mathlib/Tactic/SetNotationForOrder.lean,MathlibTest/SetNotationForOrder.lean |
4 |
50 |
['JovanGerb', 'Vierkantor', 'github-actions', 'thorimur'] |
alexjbest and thorimur assignee:alexjbest assignee:thorimur |
3-64949 3 days ago |
15-51260 15 days ago |
28-78538 28 days |
| 36442 |
SnirBroshi author:SnirBroshi |
feat(Data/Sym/Sym2/Card): cardinality theorems about `Sym2 α` |
---
[](https://gitpod.io/from-referrer/)
|
t-data
maintainer-merge
|
100/0 |
Mathlib.lean,Mathlib/Data/Set/Image.lean,Mathlib/Data/Sym/Sym2/Card.lean |
3 |
17 |
['SnirBroshi', 'github-actions', 'joneugster', 'themathqueen'] |
joneugster assignee:joneugster |
3-54758 3 days ago |
3-57011 3 days ago |
35-26994 35 days |
| 38314 |
pedroscortes author:pedroscortes |
feat(CategoryTheory/Monoidal): tensorμ_braid_swap and tensor-product IsCommComonObj |
## Summary
Two symmetric-monoidal coherence results:
1. `MonoidalCategory.tensorμ_braid_swap` (in `Monoidal/Braided/Basic.lean`) —
canonical rearrangement `tensorμ A A Y Y` intertwines the braiding on `A ⊗ Y`
with the pair of braidings on `A` and `Y`. Sibling of
`CategoryTheory.MonObj.mul_braiding`.
2. Tensor-product instance for `IsCommComonObj` (in `Monoidal/CommComon_.lean`):
if `A, B` carry commutative comonoid structures in a symmetric monoidal
category, so does `A ⊗ B`. Fills a gap alongside the existing
`instCommComonObjUnit` and `instIsCommComonObjOfCartesian`.
## Downstream consumer
The `IsCommComonObj` tensor-product instance is load-bearing for an external
library (markovcat, formalising Fritz–Klingler Markov categories). |
t-category-theory
new-contributor
maintainer-merge
|
15/0 |
Mathlib/CategoryTheory/Monoidal/Braided/Basic.lean,Mathlib/CategoryTheory/Monoidal/CommComon_.lean |
2 |
17 |
['dagurtomas', 'github-actions', 'pedroscortes', 'robin-carlier'] |
dagurtomas assignee:dagurtomas |
3-45553 3 days ago |
3-77562 3 days ago |
6-60404 6 days |
| 38468 |
Vierkantor author:Vierkantor |
chore(*): triage `simpNF` adaptation notes |
This PR reinstates some `@[simp]` attributes that were removed due to various adaptation. At least if I run `#lint` in the files, the `simpNF` linter does not complain. So hopefully we should be able to add those lemmas to the simp set again.
---
[](https://gitpod.io/from-referrer/)
|
tech debt
maintainer-merge
|
14/39 |
Mathlib/Algebra/Algebra/Opposite.lean,Mathlib/Algebra/Algebra/Unitization.lean,Mathlib/Algebra/Category/FGModuleCat/Basic.lean,Mathlib/Algebra/Star/StarAlgHom.lean,Mathlib/Analysis/SpecialFunctions/Complex/LogBounds.lean,Mathlib/Analysis/SpecialFunctions/Exp.lean,Mathlib/Geometry/Manifold/MFDeriv/FDeriv.lean,Mathlib/GroupTheory/Coset/Basic.lean,Mathlib/RepresentationTheory/Coinvariants.lean,Mathlib/Topology/Instances/Real/Lemmas.lean |
10 |
2 |
['github-actions', 'grunweg'] |
jcommelin assignee:jcommelin |
3-45544 3 days ago |
3-83765 3 days ago |
3-83556 3 days |
| 38457 |
yuanyi-350 author:yuanyi-350 |
refactor(NumberTheory): golf `Mathlib/NumberTheory/Dioph` |
- golfs `Mathlib/NumberTheory/Dioph` by replacing the arithmetic proof in `sub_dioph` with `grind`
- simplifies `div_dioph` by splitting on `y = 0 ∨ 0 < y`, then closing the positive case with `Nat.div_eq_iff` and `grind`
Extracted from #38144
[](https://gitpod.io/from-referrer/) |
codex
t-number-theory
LLM-generated
maintainer-merge
|
7/18 |
Mathlib/NumberTheory/Dioph.lean |
1 |
12 |
['github-actions', 'grunweg', 'leanprover-radar', 'yuanyi-350'] |
tb65536 assignee:tb65536 |
2-45170 2 days ago |
3-42959 3 days ago |
3-44862 3 days |
| 38093 |
mortarsanjaya author:mortarsanjaya |
feat(Algebra/Order/Ring/Unbundled/Basic): add a generalization of `two_mul_le_add_of_sq_eq_mul` |
The equality `r^2 = a * b` in the hypothesis can be weakened to `r^2 ≤ a * b`.
The implementation requires adding an appropriate `ZeroLEOneClass` instance.
---
[](https://gitpod.io/from-referrer/)
|
t-algebra
new-contributor
maintainer-merge
label:t-algebra$ |
16/7 |
Mathlib/Algebra/Order/BigOperators/Ring/Finset.lean,Mathlib/Algebra/Order/Ring/Unbundled/Basic.lean |
2 |
13 |
['github-actions', 'leanprover-radar', 'mortarsanjaya', 'themathqueen'] |
themathqueen assignee:themathqueen |
1-68160 1 day ago |
7-57526 7 days ago |
12-20512 12 days |
| 34797 |
vlad902 author:vlad902 |
feat(SimpleGraph): `cycleGraph.cycle` is a cycle |
(A follow-up PR will show that `cycleGraph.cycle` is also hamiltonian.)
---
- [x] depends on: #35360
- [x] depends on: #34766
- [x] depends on: #34796
[](https://gitpod.io/from-referrer/)
|
t-combinatorics
maintainer-merge
|
32/1 |
Mathlib/Combinatorics/SimpleGraph/Circulant.lean |
1 |
8 |
['Ruben-VandeVelde', 'YaelDillies', 'github-actions', 'mathlib-dependent-issues', 'vlad902'] |
nobody |
1-19968 1 day ago |
39-71715 39 days ago |
41-14025 41 days |
| 38345 |
emlis42 author:emlis42 |
feat(NumberTheory): add Int.divisors |
This PR adds `Int.divisors` in `Mathlib/NumberTheory/Divisors.lean`.
Defines `Int.divisors` as the disjoint union of positive and negative `Nat.divisors`.
Basic lemmas:
* `mem_divisors`
* `divisors_zero`, `divisors_eq_empty`, `divisors_one`
* `one_mem_divisors`, `neg_one_mem_divisors`
* `nonempty_divisors`
* `mem_divisors_self`
* `divisors_neg`
Lemmas relating to `divisorsAntidiag`:
* `image_fst_divisorsAntidiag`
* `image_snd_divisorsAntidiag` |
t-number-theory
new-contributor
maintainer-merge
|
61/2 |
Mathlib/NumberTheory/Divisors.lean |
1 |
21 |
['Multramate', 'SnirBroshi', 'emlis42', 'github-actions', 'tb65536'] |
tb65536 assignee:tb65536 |
1-4300 1 day ago |
5-81816 5 days ago |
6-44948 6 days |
| 37346 |
euprunin author:euprunin |
chore: golf using `grind` |
The goal of this PR is to decrease the number of times lemmas are called explicitly. Any decrease in compilation time is a welcome side effect, although it is not a primary objective.
Trace profiling results (differences <30 ms considered measurement noise):
* `✅️ SimpleGraph.Walk.IsPath.getVert_injOn`: unchanged 🎉
* `✅️ SimpleGraph.Walk.length_bypass_le`: unchanged 🎉
* `✅️ Rat.floor_intCast_div_natCast`: unchanged 🎉
* `✅️ InnerProductGeometry.norm_eq_of_angle_sub_eq_angle_sub_rev_of_angle_ne_pi`: unchanged 🎉
* `✅️ padicNorm.zero_of_padicNorm_eq_zero`: unchanged 🎉
Profiled using `set_option trace.profiler true in`.
---
[](https://gitpod.io/from-referrer/)
|
maintainer-merge |
7/45 |
Mathlib/Combinatorics/SimpleGraph/Paths.lean,Mathlib/Data/Rat/Floor.lean,Mathlib/Geometry/Euclidean/Triangle.lean,Mathlib/NumberTheory/Padics/PadicNorm.lean |
4 |
21 |
['FernandoChu', 'chenson2018', 'euprunin', 'faenuccio', 'github-actions', 'grunweg'] |
nobody |
0-57867 16 hours ago |
29-55789 29 days ago |
29-55580 29 days |
| 37709 |
j-loreaux author:j-loreaux |
feat: add some missing convenience lemmas about ordered modules |
---
[](https://gitpod.io/from-referrer/)
|
t-algebra
maintainer-merge
label:t-algebra$ |
32/0 |
Mathlib/Algebra/Order/Module/Defs.lean |
1 |
3 |
['dagurtomas', 'github-actions', 'themathqueen'] |
nobody |
0-45862 12 hours ago |
21-66599 21 days ago |
21-66390 21 days |
| 38360 |
joelriou author:joelriou |
feat(AlgebraicTopology/SimplexCategory): iterations of `δ 0` and `σ 0` |
---
[](https://gitpod.io/from-referrer/)
|
t-algebraic-topology
maintainer-merge
|
278/0 |
Mathlib.lean,Mathlib/AlgebraicTopology/SimplexCategory/DeltaZeroIter.lean |
2 |
21 |
['github-actions', 'joelriou', 'robin-carlier'] |
robin-carlier assignee:robin-carlier |
0-22673 6 hours ago |
3-70279 3 days ago |
6-14601 6 days |
| 37355 |
Thmoas-Guan author:Thmoas-Guan |
feat(RingTheory): refactor `smulShortComplex` |
Use `LinearMap.lsmul` for the `f` of `ModuleCat.smulShortComplex`, also providing new APIs for it.
---
[](https://gitpod.io/from-referrer/)
|
t-ring-theory
maintainer-merge
|
18/21 |
Mathlib/RingTheory/Regular/Category.lean |
1 |
21 |
['Thmoas-Guan', 'chrisflav', 'github-actions', 'robin-carlier'] |
chrisflav assignee:chrisflav |
0-21310 5 hours ago |
6-78193 6 days ago |
27-82385 27 days |
| 37592 |
erdOne author:erdOne |
feat: set up API for `ConvexSpace` |
We introduce `sConvexCombo` and the indexed version `iConvexCombo` as the main API for `ConvexSpace` and prove lemmas around the new definitions.
---
[](https://gitpod.io/from-referrer/)
|
t-algebra
large-import
maintainer-merge
label:t-algebra$ |
471/142 |
Mathlib/Analysis/Convex/MetricSpace.lean,Mathlib/LinearAlgebra/ConvexSpace.lean,Mathlib/LinearAlgebra/ConvexSpace/AffineSpace.lean |
3 |
71 |
['ADedecker', 'YaelDillies', 'erdOne', 'faenuccio', 'github-actions', 'grunweg', 'kbuzzard'] |
nobody |
0-6824 1 hour ago |
0-13315 3 hours ago |
5-47925 5 days |
| 38543 |
joelriou author:joelriou |
feat(AlgebraicTopology/DoldKan): morphisms which vanishes on degeneracies |
---
[](https://gitpod.io/from-referrer/)
|
t-algebraic-topology
maintainer-merge
|
58/3 |
Mathlib/AlgebraicTopology/DoldKan/Degeneracies.lean |
1 |
4 |
['github-actions', 'joelriou', 'robin-carlier'] |
nobody |
0-6686 1 hour ago |
2-17357 2 days ago |
2-17149 2 days |
| 36621 |
quantumsnow author:quantumsnow |
feat: add the category of topological pairs |
This is needed for the Eilenberg-Steenrod axioms for a homology theory.
---
- [x] depends on: #37540
[](https://gitpod.io/from-referrer/)
|
t-topology
new-contributor
maintainer-merge
|
264/9 |
Mathlib.lean,Mathlib/Topology/Category/TopCat/Basic.lean,Mathlib/Topology/Category/TopCat/Limits/Basic.lean,Mathlib/Topology/Category/TopPair.lean,Mathlib/Topology/Homotopy/TopCat/Basic.lean |
5 |
109 |
['chrisflav', 'dagurtomas', 'erdOne', 'github-actions', 'joelriou', 'mathlib-dependent-issues', 'quantumsnow', 'vlad902'] |
dagurtomas assignee:dagurtomas |
0-6306 1 hour ago |
0-6384 1 hour ago |
13-82242 13 days |
| 38577 |
chrisflav author:chrisflav |
chore(CategoryTheory): rename `Mon_` to `Mon`, `Grp_` to `Grp`, `Mod_` to `Mod` |
Deprecated modules coming in follow-up PR.
---
[](https://gitpod.io/from-referrer/)
|
t-category-theory
file-removed
maintainer-merge
|
32/32 |
Mathlib.lean,Mathlib/Algebra/Category/CommBialgCat.lean,Mathlib/AlgebraicGeometry/Group/Abelian.lean,Mathlib/AlgebraicGeometry/Group/Smooth.lean,Mathlib/CategoryTheory/Monad/EquivMon.lean,Mathlib/CategoryTheory/Monoidal/Bimod.lean,Mathlib/CategoryTheory/Monoidal/Cartesian/CommGrp_.lean,Mathlib/CategoryTheory/Monoidal/Cartesian/CommMon_.lean,Mathlib/CategoryTheory/Monoidal/Cartesian/Grp.lean,Mathlib/CategoryTheory/Monoidal/Cartesian/Mod.lean,Mathlib/CategoryTheory/Monoidal/Cartesian/Mon.lean,Mathlib/CategoryTheory/Monoidal/Cartesian/Over.lean,Mathlib/CategoryTheory/Monoidal/Cartesian/ShrinkYoneda.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/Module.lean,Mathlib/CategoryTheory/Monoidal/Internal/Types/CommGrp_.lean,Mathlib/CategoryTheory/Monoidal/Internal/Types/Grp.lean,Mathlib/CategoryTheory/Monoidal/Mod.lean,Mathlib/CategoryTheory/Monoidal/Mon.lean,Mathlib/CategoryTheory/Monoidal/Opposite/Mon.lean,Mathlib/CategoryTheory/Monoidal/Ring.lean,MathlibTest/CategoryTheory/Mon.lean,MathlibTest/CategoryTheory/Monoidal/MonTauto.lean |
26 |
2 |
['github-actions', 'robin-carlier'] |
nobody |
0-5897 1 hour ago |
1-1631 1 day ago |
1-1918 1 day |
| 36794 |
vihdzp author:vihdzp |
doc(SetTheory/Ordinal/Principal): improve documentation |
The module docstring now contains a description of what an `op`-principal actually is. I've also added some additional names for discoverability.
---
[](https://gitpod.io/from-referrer/)
|
t-set-theory
documentation
maintainer-merge
|
24/18 |
Mathlib/SetTheory/Ordinal/Principal.lean,Mathlib/SetTheory/Ordinal/Veblen.lean |
2 |
12 |
['SnirBroshi', 'Vierkantor', 'YaelDillies', 'github-actions', 'mathlib-merge-conflicts', 'vihdzp'] |
nobody |
0-4117 1 hour ago |
0-4170 1 hour ago |
40-65170 40 days |
| 36891 |
vihdzp author:vihdzp |
feat(SetTheory/Ordinal/Exponential): characterization of `a ^ b = 1` |
Used in the CGT repo.
---
[](https://gitpod.io/from-referrer/)
|
t-set-theory
maintainer-merge
|
12/0 |
Mathlib/SetTheory/Ordinal/Exponential.lean |
1 |
7 |
['SnirBroshi', 'YaelDillies', 'github-actions', 'vihdzp'] |
nobody |
0-4019 1 hour ago |
34-51648 34 days ago |
39-20247 39 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 |
| 17623 |
astrainfinita author:astrainfinita |
feat(Algebra/Order/GroupWithZero/Unbundled): add some lemmas |
Some lemmas in `Algebra.Order.GroupWithZero.Unbundled` have incorrect or unsatisfactory names, or assumptions that can be omitted using `ZeroLEOneClass`. The lemmas added in this PR are versions of existing lemmas that use the correct or better name or `ZeroLEOneClass` to omit an assumption. The original lemmas will be deprecated in #17593.
| New name | Old name |
|-------------------------|-------------------------|
| `mul_le_one_left₀` | `Left.mul_le_one_of_le_of_le` |
| `mul_lt_one_of_le_of_lt_left₀` (`0 ≤ ·` version) / `mul_lt_one_of_le_of_lt_of_pos_left` | `Left.mul_lt_of_le_of_lt_one_of_pos` |
| `mul_lt_one_of_lt_of_le_left₀` | `Left.mul_lt_of_lt_of_le_one_of_nonneg` |
| `mul_le_one_right₀` | `Right.mul_le_one_of_le_of_le` |
| `mul_lt_one_of_lt_of_le_right₀` (`0 ≤ ·` version) / `mul_lt_one_of_lt_of_le_of_pos_right` | `Right.mul_lt_one_of_lt_of_le_of_pos` |
| `mul_lt_one_of_le_of_lt_right₀` | `Right.mul_lt_one_of_le_of_lt_of_nonneg` |
The following lemmas use `ZeroLEOneClass`.
| New name | Old name |
|-------------------------|-------------------------|
| `(Left.)one_le_mul₀` | `Left.one_le_mul_of_le_of_le` |
| `Left.one_lt_mul_of_le_of_lt₀` | `Left.one_lt_mul_of_le_of_lt_of_pos` |
| `Left.one_lt_mul_of_lt_of_le₀` | `Left.lt_mul_of_lt_of_one_le_of_nonneg` / `one_lt_mul_of_lt_of_le` (still there) |
| `(Left.)one_lt_mul₀` | |
| `Right.one_le_mul₀` | `Right.one_le_mul_of_le_of_le` |
| `Right.one_lt_mul_of_lt_of_le₀` | `Right.one_lt_mul_of_lt_of_le_of_pos` |
| `Right.one_lt_mul_of_le_of_lt₀` | `Right.one_lt_mul_of_le_of_lt_of_nonneg` / `one_lt_mul_of_le_of_lt` (still there) / `one_lt_mul` (still there) |
| `Right.one_lt_mul₀` | `Right.one_lt_mul_of_lt_of_lt` |
---
Split from #17593.
[](https://gitpod.io/from-referrer/)
|
merge-conflict
t-algebra
awaiting-zulip
t-order
label:t-algebra$ |
146/44 |
Mathlib/Algebra/Order/GroupWithZero/Canonical.lean,Mathlib/Algebra/Order/GroupWithZero/Unbundled.lean |
2 |
11 |
['YaelDillies', 'astrainfinita', 'github-actions', 'j-loreaux'] |
nobody |
524-5245 1 year ago |
530-84204 530 days ago |
33-53295 33 days |
| 15654 |
TpmKranz author:TpmKranz |
feat(Computability): language-preserving maps between NFA and RE |
Map REs to NFAs via Thompson's construction and NFAs to REs using GNFAs
Last chunk of #12648
---
- [ ] depends on: #15651
- [ ] depends on: #15649
[](https://gitpod.io/from-referrer/)
|
blocked-by-other-PR
new-contributor
t-computability
merge-conflict
awaiting-zulip
|
985/2 |
Mathlib.lean,Mathlib/Computability/GNFA.lean,Mathlib/Computability/Language.lean,Mathlib/Computability/NFA.lean,Mathlib/Computability/RegularExpressions.lean,Mathlib/Data/FinEnum/Option.lean,docs/references.bib |
7 |
3 |
['github-actions', 'leanprover-community-mathlib4-bot', 'meithecatte'] |
nobody |
357-54922 11 months ago |
626-78107 626 days ago |
0-179 2 minutes |
| 17458 |
urkud author:urkud |
refactor(Algebra/Group): make `IsUnit` a typeclass |
Also change some lemmas to assume `[IsUnit _]` instead of `[Invertible _]`.
Motivated by potential non-defeq diamonds in #14986, see also [Zulip](https://leanprover.zulipchat.com/#narrow/stream/116395-maths/topic/Invertible.20and.20data)
I no longer plan to merge this PR, but I'm going to cherry-pick some changes to a new PR before closing this one.
---
[](https://gitpod.io/from-referrer/)
|
merge-conflict
t-algebra
awaiting-zulip
label:t-algebra$ |
82/72 |
Mathlib/Algebra/CharP/Invertible.lean,Mathlib/Algebra/Group/Invertible/Basic.lean,Mathlib/Algebra/Group/Units/Defs.lean,Mathlib/Algebra/GroupWithZero/Invertible.lean,Mathlib/Algebra/GroupWithZero/Units/Basic.lean,Mathlib/Algebra/Polynomial/Degree/Units.lean,Mathlib/Algebra/Polynomial/Splits.lean,Mathlib/Analysis/Convex/Segment.lean,Mathlib/Analysis/Normed/Affine/Isometry.lean,Mathlib/Analysis/Normed/Ring/Units.lean,Mathlib/CategoryTheory/Linear/Basic.lean,Mathlib/FieldTheory/Finite/Basic.lean,Mathlib/FieldTheory/Separable.lean,Mathlib/FieldTheory/SeparableDegree.lean,Mathlib/GroupTheory/Submonoid/Inverses.lean,Mathlib/LinearAlgebra/AffineSpace/AffineEquiv.lean,Mathlib/LinearAlgebra/AffineSpace/Combination.lean,Mathlib/LinearAlgebra/CliffordAlgebra/Contraction.lean,Mathlib/LinearAlgebra/CliffordAlgebra/Inversion.lean,Mathlib/LinearAlgebra/CliffordAlgebra/SpinGroup.lean,Mathlib/LinearAlgebra/Eigenspace/Minpoly.lean,Mathlib/NumberTheory/MulChar/Basic.lean,Mathlib/RingTheory/Localization/NumDen.lean,Mathlib/RingTheory/Polynomial/Content.lean,Mathlib/RingTheory/Polynomial/GaussLemma.lean,Mathlib/RingTheory/Valuation/Basic.lean |
26 |
12 |
['MichaelStollBayreuth', 'acmepjz', 'eric-wieser', 'github-actions', 'leanprover-bot', 'leanprover-community-bot-assistant', 'urkud'] |
nobody |
297-35271 9 months ago |
568-69314 568 days ago |
0-66650 18 hours |
| 25218 |
kckennylau author:kckennylau |
feat(AlgebraicGeometry): Tate normal form of elliptic curves |
---
[](https://gitpod.io/from-referrer/)
|
merge-conflict
t-algebraic-geometry
awaiting-zulip
new-contributor
|
291/26 |
Mathlib.lean,Mathlib/AlgebraicGeometry/EllipticCurve/IsomOfJ.lean,Mathlib/AlgebraicGeometry/EllipticCurve/Modular/TateNormalForm.lean,Mathlib/AlgebraicGeometry/EllipticCurve/NormalForms.lean,Mathlib/AlgebraicGeometry/EllipticCurve/VariableChange.lean |
5 |
31 |
['MichaelStollBayreuth', 'Multramate', 'acmepjz', 'github-actions', 'grunweg', 'kckennylau', 'leanprover-community-bot-assistant'] |
nobody |
297-34109 9 months ago |
330-9226 330 days ago |
6-44784 6 days |
| 28803 |
astrainfinita author:astrainfinita |
refactor: unbundle algebra from `ENormed*` |
Further speed up the search in the algebraic typeclass hierarchy by avoiding searching for `TopologicalSpace`.
This PR continues the work from #23961.
- Change `ESeminormed(Add)Monoid` and `ENormed(Add)Monoid` so they no longer carry algebraic data.
- Deprecate `ESeminormed(Add)CommMonoid` and `ENormed(Add)CommMonoid` in favor of `ESeminormed(Add)Monoid` and `ENormed(Add)Monoid` with a commutative algebraic typeclass.
|Old|New|
|---|---|
| `[ESeminormed(Add)(Comm)Monoid E]` | `[(Add)(Comm)Monoid E] [ESeminormed(Add)Monoid E]` |
| `[ENormed(Add)(Comm)Monoid]` | `[(Add)(Comm)Monoid E] [ENormed(Add)Monoid]` |
See [Zulip discussion](https://leanprover.zulipchat.com/#narrow/channel/144837-PR-reviews/topic/.2328803.20refactor.3A.20unbundle.20algebra.20from.20.60ENormed*.60/with/536024350)
------------
- [x] depends on: #28813 |
t-algebra
merge-conflict
slow-typeclass-synthesis
awaiting-zulip
t-analysis
label:t-algebra$ |
80/63 |
Mathlib/Analysis/CStarAlgebra/CStarMatrix.lean,Mathlib/Analysis/Normed/Group/Basic.lean,Mathlib/Analysis/Normed/Group/Continuity.lean,Mathlib/Analysis/Normed/Group/InfiniteSum.lean,Mathlib/Analysis/NormedSpace/IndicatorFunction.lean,Mathlib/MeasureTheory/Function/L1Space/AEEqFun.lean,Mathlib/MeasureTheory/Function/L1Space/HasFiniteIntegral.lean,Mathlib/MeasureTheory/Function/L1Space/Integrable.lean,Mathlib/MeasureTheory/Function/LocallyIntegrable.lean,Mathlib/MeasureTheory/Function/LpSeminorm/Basic.lean,Mathlib/MeasureTheory/Function/LpSeminorm/CompareExp.lean,Mathlib/MeasureTheory/Function/LpSeminorm/TriangleInequality.lean,Mathlib/MeasureTheory/Integral/IntegrableOn.lean,Mathlib/MeasureTheory/Integral/IntervalIntegral/Basic.lean |
14 |
28 |
['astrainfinita', 'bryangingechen', 'github-actions', 'grunweg', 'kbuzzard', 'leanprover-bot', 'leanprover-community-mathlib4-bot', 'mathlib-bors', 'mathlib4-dependent-issues-bot', 'mathlib4-merge-conflict-bot', 'sgouezel'] |
grunweg assignee:grunweg |
237-49754 7 months ago |
246-908 246 days ago |
0-19882 5 hours |
| 28925 |
grunweg author:grunweg |
chore: remove `linear_combination'` tactic |
When `linear_combination` was refactored in #15899, the old code was kept as the `linear_combination'` tactic, for easier migration. The consensus of the zulip discussion ([#mathlib4 > Narrowing the scope of `linear_combination` @ 💬](https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/Narrowing.20the.20scope.20of.20.60linear_combination.60/near/470237816)) was to wait, and "revisit this once people have experienced the various tactics in practice".
One year later, the old tactic has almost no uses: it is unused in mathlib; [searching on github](https://github.com/search?q=linear_combination%27%20path%3A*.lean&type=code) yields 37 hits --- all of which are in various forks of mathlib. Thus, removing this tactic seems appropriate.
---
Do not merge before the zulip discussion has concluded!
[](https://gitpod.io/from-referrer/)
|
merge-conflict
file-removed
awaiting-zulip
|
0/564 |
Mathlib.lean,Mathlib/Tactic.lean,Mathlib/Tactic/LinearCombination'.lean,Mathlib/Tactic/Linter/UnusedTactic.lean,MathlibTest/linear_combination'.lean |
5 |
4 |
['euprunin', 'github-actions', 'grunweg', 'mathlib4-merge-conflict-bot'] |
nobody |
194-26964 6 months ago |
245-58761 245 days ago |
0-1 1 second |
| 30150 |
imbrem author:imbrem |
feat(CategoryTheory/Monoidal): to_additive for MonoidalCategory |
Add `AddMonoidalCategory`, the additive version of `MonoidalCategory`.
To get this to work, I needed to _remove_ the `to_additive` attributes in `Discrete.lean`, since existing code relies on the `AddMonoid M → MonoidalCategory M` instance. For now, we simply implement the additive variants by hand instead.
---
As discussed in #28718; I added an `AddMonoidalCategory` struct and tagged `MonoidalCategory` with `to_additive`, along with the lemmas in `Category.lean`.
I think this is the right approach, since under this framework the "correct" additive version of `Discrete.lean` would be mapping an `AddMonoid` to an `AddMonoidalCategory`.
Next steps would be to:
- Make `monoidal_coherence` and `coherence` support `AddMonoidalCategory`
- Add `CocartesianMonoidalCategory` extending `AddMonoidalCategory`
[](https://gitpod.io/from-referrer/)
|
t-category-theory
large-import
new-contributor
merge-conflict
awaiting-zulip
t-meta
|
444/125 |
Mathlib/CategoryTheory/Monoidal/Category.lean,Mathlib/CategoryTheory/Monoidal/Discrete.lean,Mathlib/Tactic/ToAdditive/GuessName.lean |
3 |
22 |
['JovanGerb', 'YaelDillies', 'github-actions', 'imbrem', 'mathlib4-merge-conflict-bot'] |
nobody |
166-37838 5 months ago |
206-16504 206 days ago |
1-160 1 day |
| 15651 |
TpmKranz author:TpmKranz |
feat(Computability/NFA): operations for Thompson's construction |
Lays the groundwork for a proof of equivalence of RE and NFA, w.r.t. described language. Actual connection to REs comes later, after the groundwork for the opposite direction has been laid.
Third chunk of #12648
---
[](https://gitpod.io/from-referrer/)
|
new-contributor
t-computability
merge-conflict
awaiting-author
awaiting-zulip
|
307/5 |
Mathlib/Computability/NFA.lean |
1 |
27 |
['TpmKranz', 'YaelDillies', 'dupuisf', 'github-actions', 'leanprover-community-bot-assistant', 'meithecatte', 'rudynicolop'] |
nobody |
161-54970 5 months ago |
580-82358 580 days ago |
45-84611 45 days |
| 15649 |
TpmKranz author:TpmKranz |
feat(Computability): introduce Generalised NFA as bridge to Regular Expression |
Lays the groundwork for a proof of equivalence of NFA and RE, w.r.t. described language. Actual connection to NFA comes later, after the groundwork for the opposite direction has been laid.
Second chunk of #12648
---
- [x] depends on: #15647 [Data.FinEnum.Option unchanged since then]
[](https://gitpod.io/from-referrer/)
|
new-contributor
t-computability
merge-conflict
awaiting-author
awaiting-zulip
|
298/0 |
Mathlib.lean,Mathlib/Computability/GNFA.lean,Mathlib/Computability/Language.lean,Mathlib/Computability/RegularExpressions.lean,docs/references.bib |
5 |
7 |
['github-actions', 'mathlib4-dependent-issues-bot', 'mathlib4-merge-conflict-bot', 'meithecatte', 'trivial1711'] |
nobody |
160-71211 5 months ago |
506-34741 506 days ago |
23-54870 23 days |
| 20648 |
anthonyde author:anthonyde |
feat: formalize regular expression -> εNFA |
The file `Computability/RegularExpressionsToEpsilonNFA.lean` contains a formal definition of Thompson's method for constructing an `εNFA` from a `RegularExpression` and a proof of its correctness.
---
- [x] depends on: #20644
- [x] depends on: #20645
[](https://gitpod.io/from-referrer/)
|
merge-conflict
t-computability
awaiting-zulip
new-contributor
|
490/0 |
Mathlib.lean,Mathlib/Computability/RegularExpressionsToEpsilonNFA.lean,docs/references.bib |
3 |
7 |
['anthonyde', 'github-actions', 'mathlib4-dependent-issues-bot', 'mathlib4-merge-conflict-bot', 'meithecatte', 'qawbecrdtey'] |
nobody |
160-21979 5 months ago |
357-54908 357 days ago |
75-77754 75 days |
| 11800 |
JADekker author:JADekker |
feat: KappaLindelöf spaces |
Define KappaLindelöf spaces by following the first one-third of the API for Lindelöf spaces. The remainder will be added in a future PR.
---
[](https://gitpod.io/from-referrer/)
|
please-adopt
merge-conflict
t-topology
awaiting-zulip
|
301/2 |
Mathlib.lean,Mathlib/Topology/Compactness/KappaLindelof.lean,Mathlib/Topology/Compactness/Lindelof.lean |
3 |
38 |
['ADedecker', 'JADekker', 'PatrickMassot', 'StevenClontz', 'adomani', 'github-actions', 'grunweg', 'kim-em', 'urkud'] |
nobody |
159-80245 5 months ago |
635-14127 635 days ago |
123-25636 123 days |
| 30668 |
astrainfinita author:astrainfinita |
feat: `QuotType` |
This typeclass is primarily for use by type synonyms of `Quot` and `Quotient`. Using `QuotType` API for type synonyms of `Quot` and `Quotient` will avoid defeq abuse caused by directly using `Quot` and `Quotient` APIs.
This PR also adds some typeclasses to support different ways to find the quotient map that should be used. See the documentation comments of these typeclasses for examples of usage.
---
It's not a typical design to use these auxiliary typeclasses and term elaborators, but I haven't found a better way to support these notations.
Some of the naming may need to be discussed. For example:
- `⟦·⟧` is currently called `mkQ` in names. This distinguishes it from other `.mk`s and makes it possible to write the quotient map as `mkQ` `mkQ'` ~~`mkQ_ h`~~. But this will also require changing the old lemma names.
- It would be helpful if the names of new type classes explained their functionality better.
[Zulip](https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/migrate.20to.20.60QuotLike.60.20API)
This PR continues the work from #16421.
Original PR: https://github.com/leanprover-community/mathlib4/pull/16421 |
RFC
t-data
awaiting-zulip
|
629/0 |
Mathlib.lean,Mathlib/Data/QuotType.lean,MathlibTest/QuotType.lean |
3 |
20 |
['YaelDillies', 'astrainfinita', 'github-actions', 'mathlib4-merge-conflict-bot', 'plp127', 'vihdzp'] |
nobody |
138-62091 4 months ago |
191-30944 191 days ago |
0-81 1 minute |
| 33368 |
urkud author:urkud |
feat: define `Complex.UnitDisc.shift` |
Also review the existing API
UPD: I'm going to define a `PSL(2, Real)` action instead.
---
[](https://gitpod.io/from-referrer/) |
t-analysis
awaiting-zulip
merge-conflict
|
273/39 |
Mathlib.lean,Mathlib/Analysis/Complex/UnitDisc/Basic.lean,Mathlib/Analysis/Complex/UnitDisc/Shift.lean |
3 |
7 |
['github-actions', 'j-loreaux', 'mathlib4-merge-conflict-bot', 'sgouezel', 'urkud'] |
j-loreaux assignee:j-loreaux |
111-30404 3 months ago |
111-77137 111 days ago |
7-33574 7 days |
| 32828 |
Hagb author:Hagb |
feat(Algebra/Order/Group/Defs): add `IsOrderedAddMonoid.toIsOrderedCancelAddMonoid'` |
It is similar to `IsOrderedAddMonoid.toIsOrderedCancelAddMonoid`, while with different hypotheses.
The conclusion `IsOrderedCancelMonoid α` on
`IsOrderedAddMonoid.toIsOrderedCancelAddMonoid` still holds when the hypothesis `CommGroup α` is weakened to `CancelCommMonoid α` while `PartialOrder α` is strengthened to `LinearOrder α`.
---
[`IsOrderedAddMonoid.toIsOrderedCancelAddMonoid`](https://leanprover-community.github.io/mathlib4_docs/find/?pattern=IsOrderedAddMonoid.toIsOrderedCancelAddMonoid#doc) and `IsOrderedAddMonoid.toIsOrderedCancelAddMonoid'`:
https://github.com/leanprover-community/mathlib4/blob/97f78b1a4311fed1844b94f1c069219a48a098e1/Mathlib/Algebra/Order/Group/Defs.lean#L52-L62
[](https://gitpod.io/from-referrer/)
|
awaiting-zulip
t-algebra
label:t-algebra$ |
4/0 |
Mathlib/Algebra/Order/Group/Defs.lean |
1 |
8 |
['Garmelon', 'Vierkantor', 'artie2000', 'github-actions', 'leanprover-radar'] |
eric-wieser assignee:eric-wieser |
95-79239 3 months ago |
95-79239 95 days ago |
40-42357 40 days |
| 33031 |
chiyunhsu author:chiyunhsu |
feat(Combinatorics/Enumerative/Partition): add combinatorial proof of Euler's partition theorem |
The new file EulerComb.lean contains the combinatorial proof of Euler's partition theorem. The analytic proof of the theorem and its generalization of Glaisher's Theorem has already been formalized in [Glaisher.lean](https://github.com/leanprover-community/mathlib4/blob/master/Mathlib/Combinatorics/Enumerative/Partition/Glaisher.lean). The generalization of the combinatorial proof from this file to Glaisher's Theorem is within reach.
---
Zulip discussion: [#mathlib4 > Glaisher’s Bijection on integer partitions](https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/Glaisher.E2.80.99s.20Bijection.20on.20integer.20partitions/with/570808111)
[](https://gitpod.io/from-referrer/)
|
t-combinatorics
new-contributor
awaiting-zulip
|
531/0 |
Mathlib.lean,Mathlib/Combinatorics/Enumerative/Partition/EulerComb.lean |
2 |
5 |
['chiyunhsu', 'github-actions', 'tb65536', 'vihdzp'] |
b-mehta assignee:b-mehta |
88-84057 2 months ago |
88-84057 88 days ago |
42-22427 42 days |
| 32742 |
LTolDe author:LTolDe |
feat(MeasureTheory/Constructions/Polish/Basic): add class SuslinSpace |
add new class `SuslinSpace` for a topological space that is an analytic set in itself
This will be useful to prove the **Effros Theorem**, see [zulip thread](https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/Effros.20Theorem/with/558712441).
---
[](https://gitpod.io/from-referrer/)
|
new-contributor
awaiting-zulip
t-measure-probability
|
4/0 |
Mathlib/MeasureTheory/Constructions/Polish/Basic.lean |
1 |
9 |
['ADedecker', 'LTolDe', 'dupuisf', 'github-actions', 'jcommelin'] |
PatrickMassot assignee:PatrickMassot |
86-10067 2 months ago |
111-80599 111 days ago |
11-7507 11 days |
| 34720 |
Paul-Lez author:Paul-Lez |
feat(RingTheory/PowerSeries/Composition): define composition of power series |
This PR defines the composition of two power series, and adds various pieces of API lemmas (this is mostly fixing up and upstreaming code from [this repo](https://github.com/rmhi/formal_deriv)).
This is the first of a series of PRs upstreaming work that was done at the CFT workshop in Oxford last summer, working towards proving some results about the `exp` and `log` power series (and their composition!), and constructing the isomorphism $(\mathfrak{m}_K ^ n, +) \cong (1 + \mathfrak{m}_K ^ n, \times)$ for sufficiently large $n$, where $K$ is a characteristic zero local field.
Co-authored-by: Richard Hill
Co-authored-by: Calle Sönne
---
[](https://gitpod.io/from-referrer/)
|
t-ring-theory
awaiting-zulip
|
844/0 |
Mathlib.lean,Mathlib/RingTheory/PowerSeries/Composition.lean |
2 |
3 |
['Paul-Lez', 'github-actions', 'vihdzp'] |
nobody |
77-56076 2 months ago |
85-7996 85 days ago |
0-10 10 seconds |
| 20238 |
maemre author:maemre |
feat(Computability/DFA): Closure of regular languages under some set operations |
This shows that regular languages are closed under complement and intersection by constructing DFAs for them.
---
Closure under all other operations will be proved when someone adds the proof for DFA<->regular expression equivalence, so they are not part of this PR.
[](https://gitpod.io/from-referrer/)
|
new-contributor
t-computability
merge-conflict
awaiting-author
awaiting-zulip
|
159/0 |
Mathlib/Computability/DFA.lean,Mathlib/Computability/Language.lean |
2 |
60 |
['EtienneC30', 'YaelDillies', 'github-actions', 'maemre', 'mathlib4-merge-conflict-bot', 'meithecatte', 'urkud'] |
nobody |
61-15213 2 months ago |
406-79552 406 days ago |
48-67492 48 days |
| 22361 |
rudynicolop author:rudynicolop |
feat(Computability/NFA): nfa closure properties |
Add the closure properties union, intersection and reversal for NFA.
---
[](https://gitpod.io/from-referrer/)
|
new-contributor
t-computability
merge-conflict
awaiting-author
awaiting-zulip
|
218/2 |
Mathlib/Computability/Language.lean,Mathlib/Computability/NFA.lean |
2 |
91 |
['EtienneC30', 'b-mehta', 'ctchou', 'github-actions', 'leanprover-community-bot-assistant', 'meithecatte', 'rudynicolop'] |
nobody |
61-15197 2 months ago |
357-83491 357 days ago |
39-61332 39 days |
| 23929 |
meithecatte author:meithecatte |
feat(Computability/NFA): improve bound on pumping lemma |
---
- [x] depends on: #25321
[](https://gitpod.io/from-referrer/)
|
t-computability
awaiting-zulip
new-contributor
awaiting-author
|
101/10 |
Mathlib/Computability/EpsilonNFA.lean,Mathlib/Computability/NFA.lean |
2 |
42 |
['YaelDillies', 'dagurtomas', 'github-actions', 'leanprover-community-bot-assistant', 'mathlib4-dependent-issues-bot', 'meithecatte'] |
nobody |
60-35226 2 months ago |
324-64525 324 days ago |
34-10092 34 days |
| 35524 |
grunweg author:grunweg |
feat: text-based linter against \t followed by tactic mode |
Wait for the zulip discussion to converge. **If** there is consensus in favour of this change, summarise the motivation here.
[zulip discuss](https://leanprover.zulipchat.com/#narrow/channel/345428-mathlib-reviewers/topic/proposal.3A.20no.20more.20use.20of.20.60.E2.96.B8.60.20in.20Mathlib.3F/with/574680826)
---
There are currently 80 remaining exceptions in mathlib: ideally, these would get fixed before merging this.
Works best when combined with #35523.
[](https://gitpod.io/from-referrer/)
|
t-linter
awaiting-zulip
merge-conflict
|
23/2 |
Mathlib/Tactic/Linter/TextBased.lean |
1 |
5 |
['github-actions', 'grunweg', 'joneugster', 'mathlib-merge-conflicts', 'vihdzp'] |
nobody |
41-52978 1 month ago |
68-14140 68 days ago |
0-187 3 minutes |
| 32608 |
PrParadoxy author:PrParadoxy |
feat(LinearAlgebra/PiTensorProduct): API for PiTensorProducts indexed by sets |
This PR addresses a TODO item in LinearAlgebra/PiTensorProduct.lean:
* API for the various ways ι can be split into subsets; connect this
with the binary tensor product
-- specifically by describing tensors of type ⨂ (i : S), M i, for S : Set ι.
Our primary motivation is to formalise the notion of "restricted tensor
products". This will be the content of a follow-up PR.
Beyond that, the Set API is natural in contexts where the index type has
an independent interpretation. An example is quantum physics, where ι
ranges over distinguishable degrees of freedom, and where its is common
practice to annotate objects by the set of indices they are defined on.
---
Stub file with preliminary definition of the restricted tensor product as a direct limit of tensors indexed by finite subsets of an index type:
https://github.com/PrParadoxy/mathlib4/blob/restricted-stub/Mathlib/LinearAlgebra/PiTensorProduct/Restricted.lean
---
- [x] depends on: #32598
[](https://gitpod.io/from-referrer/)
|
new-contributor
awaiting-zulip
t-algebra
label:t-algebra$ |
300/2 |
Mathlib.lean,Mathlib/LinearAlgebra/PiTensorProduct.lean,Mathlib/LinearAlgebra/PiTensorProduct/Set.lean |
3 |
28 |
['PrParadoxy', 'dagurtomas', 'eric-wieser', 'github-actions', 'goliath-klein', 'leanprover-radar', 'mathlib4-dependent-issues-bot', 'mathlib4-merge-conflict-bot'] |
nobody |
40-74373 1 month ago |
126-73564 126 days ago |
10-66980 10 days |
| 36890 |
vihdzp author:vihdzp |
chore(SetTheory): `le_mul_left` → `le_mul_of_pos_left` |
The new theorem names/statements match [`Nat.le_mul_of_pos_left`](https://leanprover-community.github.io/mathlib4_docs/Init/Data/Nat/Lemmas.html#Nat.le_mul_of_pos_left). The cardinal one has also been moved to an earlier file.
---
[](https://gitpod.io/from-referrer/)
|
t-set-theory
awaiting-zulip
merge-conflict
|
28/23 |
Mathlib/SetTheory/Cardinal/Arithmetic.lean,Mathlib/SetTheory/Cardinal/Basic.lean,Mathlib/SetTheory/Cardinal/Free.lean,Mathlib/SetTheory/Ordinal/Arithmetic.lean,Mathlib/SetTheory/Ordinal/Exponential.lean,Mathlib/SetTheory/Ordinal/Notation.lean |
6 |
2 |
['github-actions', 'mathlib-merge-conflicts'] |
nobody |
36-25382 1 month ago |
39-12122 39 days ago |
0-10825 3 hours |
| 35578 |
Shreyas4991 author:Shreyas4991 |
fix: writer monad should use an additive logging type |
The Writer monad's w type is supposed to be additive, not multiplicative. This is how it is conceptually used in Haskell (as a logging type). Haskell uses `Monoid` because it doesn't make a distinction between `AddMonoid` and `Monoid`.
[#mathlib4 > Writer should use an additive monoid @ 💬](https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/Writer.20should.20use.20an.20additive.20monoid/near/574990415)
---
[](https://gitpod.io/from-referrer/)
|
t-data
awaiting-zulip
merge-conflict
|
10/10 |
Mathlib/Control/Monad/Cont.lean,Mathlib/Control/Monad/Writer.lean |
2 |
5 |
['Shreyas4991', 'eric-wieser', 'github-actions', 'mathlib-merge-conflicts'] |
nobody |
32-35857 1 month ago |
66-56375 66 days ago |
0-18707 5 hours |
| 30750 |
SnirBroshi author:SnirBroshi |
feat(Data/Quot): `toSet` and `equivClassOf` |
Define `toSet` which gets the set corresponding to an element of a quotient, and `equivClassOf` which gets the equivalence class of an element under a quotient.
---
I found these definitions helpful when working with quotients, specifically `ConnectedComponents` of a `TopologicalSpace`.
[](https://gitpod.io/from-referrer/)
|
t-data
awaiting-author
awaiting-zulip
|
162/0 |
Mathlib/Data/Quot.lean,Mathlib/Data/Set/Image.lean,Mathlib/Data/SetLike/Basic.lean,Mathlib/Data/Setoid/Basic.lean |
4 |
8 |
['SnirBroshi', 'TwoFX', 'eric-wieser', 'github-actions', 'linesthatinterlace', 'mathlib-merge-conflicts'] |
TwoFX assignee:TwoFX |
14-7366 14 days ago |
152-20767 152 days ago |
35-84279 35 days |
| 26299 |
adomani author:adomani |
perf: the `whitespace` linter only acts on modified files |
Introduces an `IO.Ref` to allow the `commandStart` linter to only run on files that git considers modified with respect to `master`.
The linter is also active on files that have had some error, as these are likely being modified!
The PR should also mitigate the speed-up that the linter introduced:
[#mathlib4 > A whitespace linter @ 💬](https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/A.20whitespace.20linter/near/525091877)
Assuming that this goes well, a similar mechanism could be applied to several linters that do not need to run on all code, just on the modified code.
Implementation detail: the linter is currently either on or off in "whole" files. It may be also a future development to make this more granular and only run the linter on "modifed commands in modified files", but this is not currently the plan for this modification!
---
[](https://gitpod.io/from-referrer/)
|
t-linter
awaiting-zulip
awaiting-author
|
55/7 |
Mathlib/Tactic/Linter/Whitespace.lean |
1 |
20 |
['adomani', 'eric-wieser', 'github-actions', 'grunweg', 'joneugster', 'kim-em', 'leanprover-bot', 'leanprover-radar', 'mathlib-bors', 'mathlib4-merge-conflict-bot'] |
grunweg assignee:grunweg |
11-26081 11 days ago |
242-17159 242 days ago |
66-73556 66 days |
| 34963 |
Parcly-Taxel author:Parcly-Taxel |
feat(Archive): proof of the Robbins conjecture |
Cf. [#mathlib4 > Alternative axiomatization of boolean algebras @ 💬](https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/Alternative.20axiomatization.20of.20boolean.20algebras/near/558900960) and #31924. |
t-algebra
awaiting-zulip
label:t-algebra$ |
610/0 |
Archive.lean,Archive/Robbins.lean |
2 |
2 |
['chrisflav', 'github-actions'] |
chrisflav assignee:chrisflav |
7-73642 7 days ago |
7-73642 7 days ago |
71-52828 71 days |
| 38272 |
yuanyi-350 author:yuanyi-350 |
refactor(Analysis): golf `Mathlib/Analysis/Normed/Operator/Mul` |
- refactors `Normed/Operator/Mul` by defining `ring_lmap_equiv_selfₗ` as the symmetry of `ContinuousLinearMap.toSpanSingletonLE`
- shortens the norm proof for `ring_lmap_equiv_self` to `ContinuousLinearMap.norm_toSpanSingleton`
Extracted from #37968
[](https://gitpod.io/from-referrer/) |
t-analysis
LLM-generated
codex
awaiting-zulip
|
25/21 |
Mathlib/Analysis/Fourier/FourierTransformDeriv.lean,Mathlib/Analysis/Normed/Operator/Mul.lean,Mathlib/Topology/Algebra/Module/LinearMap.lean |
3 |
14 |
['github-actions', 'themathqueen', 'yuanyi-350'] |
j-loreaux assignee:j-loreaux |
3-81784 3 days ago |
3-81784 3 days ago |
1-45886 1 day |
| 38546 |
yhx-12243 author:yhx-12243 |
fix: universe issue in injective module |
Change the definition of
```lean
class Module.Injective : Prop where
out : ∀ ⦃X Y : Type v⦄ [AddCommGroup X] [AddCommGroup Y] [Module R X] [Module R Y]
(f : X →ₗ[R] Y) (_ : Function.Injective f) (g : X →ₗ[R] Q),
∃ h : Y →ₗ[R] Q, ∀ x, h (f x) = g x
```
into
```lean
class Module.Injective : Prop where
out : ∀ ⦃X Y : Type u⦄ [AddCommGroup X] [AddCommGroup Y] [Module R X] [Module R Y]
(f : X →ₗ[R] Y) (_ : Function.Injective f) (g : X →ₗ[R] Q),
∃ h : Y →ₗ[R] Q, ∀ x, h (f x) = g x
```
to make it agree with `Module.Baer` and real mathematical definition, **without universe issues**.
Since the criterion `Module.Flat` also uses `Type u` on testing modules.
See discussions in https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/Universe.20issue.20about.20injective.20module .
---
[](https://gitpod.io/from-referrer/)
|
t-algebra
new-contributor
awaiting-zulip
label:t-algebra$ |
57/43 |
Mathlib/Algebra/Category/ModuleCat/Injective.lean,Mathlib/Algebra/Category/ModuleCat/Ulift.lean,Mathlib/Algebra/Module/Injective.lean,Mathlib/RepresentationTheory/FinGroupCharZero.lean,Mathlib/RingTheory/Flat/Tensor.lean,Mathlib/RingTheory/LocalProperties/Injective.lean |
6 |
5 |
['github-actions', 'grunweg', 'mathlib-bors', 'wwylele'] |
nobody |
1-60331 1 day ago |
1-60342 1 day ago |
0-26133 7 hours |
| 37934 |
Thmoas-Guan author:Thmoas-Guan |
feat(FieldTheory): definition of transcendental separable field extension |
In this PR, we introduce the concept of separably generated field extension and transcendental separable field extension.
Further properties will be in #37838
---
[](https://gitpod.io/from-referrer/)
|
t-algebra
awaiting-zulip
label:t-algebra$ |
69/0 |
Mathlib.lean,Mathlib/FieldTheory/TranscendentalSeparable.lean |
2 |
3 |
['Thmoas-Guan', 'github-actions', 'robin-carlier'] |
robin-carlier assignee:robin-carlier |
1-30323 1 day ago |
7-14159 7 days ago |
8-18177 8 days |