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 |
25945 |
adomani author:adomani |
feat: the empty line in commands linter |
This linter flags empty lines within a command.
It allows empty lines within doc-strings, module-docs and a couple of other "sensible" places.
It also skips files that are likely to contain meta-code, since there the use of empty lines in definition is more widespread.
This PR continues the work from #25236. |
large-import
t-linter
maintainer-merge
awaiting-author
|
375/7 |
Mathlib.lean,Mathlib/Analysis/Meromorphic/FactorizedRational.lean,Mathlib/CategoryTheory/Comma/StructuredArrow/CommaMap.lean,Mathlib/Init.lean,Mathlib/RepresentationTheory/Homological/GroupHomology/LowDegree.lean,Mathlib/Tactic.lean,Mathlib/Tactic/Linter/EmptyLine.lean,MathlibTest/EmptyLine.lean |
8 |
12 |
['adomani', 'bryangingechen', 'eric-wieser', 'github-actions'] |
bryangingechen assignee:bryangingechen |
67-45839 2 months ago |
67-45839 2 months ago |
42-26074 42 days |
24669 |
qawbecrdtey author:qawbecrdtey |
feat(Analysis/Normed/Operator/LinearIsometry): added definition `LinearIsometryEquiv.prodComm` |
---
[](https://gitpod.io/from-referrer/)
This commit defines a `LinearIsometryEquiv`, and states some trivial theorems about it.
```lean
def prodComm [Module R E₂] : E × E₂ ≃ₗᵢ[R] E₂ × E
```
|
maintainer-merge
t-analysis
awaiting-author
|
8/1 |
Mathlib/Analysis/Normed/Operator/LinearIsometry.lean |
1 |
12 |
['Ruben-VandeVelde', 'eric-wieser', 'faenuccio', 'github-actions', 'j-loreaux', 'jcommelin', 'qawbecrdtey'] |
faenuccio assignee:faenuccio |
26-6041 26 days ago |
115-80273 3 months ago |
32-83569 32 days |
27292 |
gasparattila author:gasparattila |
feat: asymptotic cone of a set |
This PR defines the asymptotic cone of a set in a normed affine space and proves its main properties. This is partial progress towards showing that an unbounded finite-dimensional convex set contains a ray.
---
- [x] depends on: #27221
[](https://gitpod.io/from-referrer/)
|
maintainer-merge
new-contributor
t-analysis
|
466/0 |
Mathlib.lean,Mathlib/Analysis/Normed/Affine/AsymptoticCone.lean,Mathlib/Order/Filter/Map.lean,Mathlib/Topology/Algebra/AsymptoticCone.lean |
4 |
45 |
['AntoineChambert-Loir', 'YaelDillies', 'gasparattila', 'github-actions', 'mathlib4-dependent-issues-bot'] |
YaelDillies assignee:YaelDillies |
16-75947 16 days ago |
59-37840 1 month ago |
73-55374 73 days |
26660 |
strihanje01 author:strihanje01 |
feat(Combinatorics/Additive/VerySmallDoubling): weak non-commutative Kneser's theorem |
add theorem about the structure of a doubling smaller than the golden ratio
---
- [x] depends on: #28653
[](https://gitpod.io/from-referrer/)
|
large-import
maintainer-merge
new-contributor
t-combinatorics
|
215/41 |
Mathlib/Algebra/Group/Action/Pointwise/Finset.lean,Mathlib/Combinatorics/Additive/VerySmallDoubling.lean |
2 |
79 |
['YaelDillies', 'github-actions', 'mathlib4-dependent-issues-bot', 'mathlib4-merge-conflict-bot', 'strihanje01'] |
YaelDillies assignee:YaelDillies |
10-50518 10 days ago |
10-83167 10 days ago |
52-25145 52 days |
28295 |
artie2000 author:artie2000 |
feat(Algebra/Order/Ring/Ordering): basic results about ring (pre)orderings |
* Basic automation for membership of ring orderings
* Alternative constructors for ring preorderings and ring orderings
* Basic results about ring preorderings and their supports, including the special case over a field
---
[](https://gitpod.io/from-referrer/)
- [x] depends on: #27282 |
maintainer-merge
t-algebra
label:t-algebra$ |
203/0 |
Mathlib.lean,Mathlib/Algebra/Group/Subgroup/Defs.lean,Mathlib/Algebra/Order/Ring/Ordering/Basic.lean |
3 |
57 |
['Rob23oba', 'YaelDillies', 'artie2000', 'github-actions', 'mathlib4-dependent-issues-bot', 'mathlib4-merge-conflict-bot', 'vihdzp'] |
joneugster assignee:joneugster |
9-7999 9 days ago |
16-74338 16 days ago |
22-37474 22 days |
26259 |
Raph-DG author:Raph-DG |
feat(Topology): Connecting different notions of locally finite |
In this PR we connect the notions of local finiteness of an indexed family of sets (as in LocallyFinite) and of a set of sets (as in Function.locallyFinsuppWithin)
---
[](https://gitpod.io/from-referrer/)
|
maintainer-merge
t-topology
|
38/0 |
Mathlib/Topology/LocallyFinsupp.lean |
1 |
18 |
['Raph-DG', 'chrisflav', 'github-actions', 'jcommelin', 'kckennylau'] |
jcommelin assignee:jcommelin |
8-38676 8 days ago |
8-63992 8 days ago |
97-27982 97 days |
29275 |
wwylele author:wwylele |
feat(GroupTheory): add DivisibleHull |
This is part of Hahn embedding theorem #27268, where an a ordered group is first embedded in a divisible group / Q-module. I am aware at #25662 there is also an ongoing rewrite of `LocalizedModule` that this PR uses. Hopefully I avoided interfering it by using mostly with public API.
---
- [x] depends on: #29277
- [x] depends on: #29388
- [x] depends on: #29386
[](https://gitpod.io/from-referrer/)
|
t-group-theory
maintainer-merge
|
451/3 |
Mathlib.lean,Mathlib/Algebra/Order/Monoid/Defs.lean,Mathlib/Algebra/Order/Monoid/PNat.lean,Mathlib/Algebra/Order/Monoid/Unbundled/Pow.lean,Mathlib/Data/NNRat/Defs.lean,Mathlib/GroupTheory/DivisibleHull.lean |
6 |
106 |
['YaelDillies', 'github-actions', 'mathlib4-dependent-issues-bot', 'vihdzp', 'wwylele'] |
tb65536 assignee:tb65536 |
8-7999 8 days ago |
15-33876 15 days ago |
25-11078 25 days |
29110 |
NotWearingPants author:NotWearingPants |
feat(Counterexamples): Euler's sum of powers conjecture |
feat(Counterexamples): Euler's sum of powers conjecture
---
[](https://gitpod.io/from-referrer/)
|
awaiting-zulip
maintainer-merge
new-contributor
|
158/0 |
Counterexamples.lean,Counterexamples/EulerSumOfPowers.lean |
2 |
43 |
['MichaelStollBayreuth', 'NotWearingPants', 'eric-wieser', 'github-actions', 'tb65536', 'urkud'] |
MichaelStollBayreuth assignee:MichaelStollBayreuth |
7-26967 7 days ago |
7-27023 7 days ago |
24-25032 24 days |
29513 |
grunweg author:grunweg |
fix(lint-style): parse linter options and load environment extensions correctly |
Parse options and load linter set extension correctly.
This fixes two issues:
- We never called the `toOptions` function that parses Lakefile options into a `Lean.Options` structure: the function we use instead is only meant for command-line options and doesn't handle the `weak.` prefix correctly.
- The way we load linter sets was incorrect: `withImportModules` stopped updating environment extensions since [lean4#6325](https://github.com/leanprover/lean4/pull/6325), and that is exactly what we use to store linter sets. At the time of writing, `importModules` might be a suitable replacement (but this is not very safe, and not documented to be stable). Instead, write a small elaborator returning the environment at the point of elaboration, and use that instead.
---
- [x] depends on: #29584
- [x] depends on: #29585
- [x] depends on: #29586
[](https://gitpod.io/from-referrer/)
|
maintainer-merge
t-meta
|
28/12 |
scripts/lint-style.lean |
1 |
13 |
['Vierkantor', 'adomani', 'github-actions', 'grunweg', 'mathlib4-dependent-issues-bot'] |
nobody |
6-48651 6 days ago |
6-61968 6 days ago |
15-48370 15 days |
29693 |
kckennylau author:kckennylau |
feat(RingTheory): make Euclidean domain from DVR |
---
Zulip: https://leanprover.zulipchat.com/#narrow/channel/116395-maths/topic/Leading.20term.20of.20valuation/near/539666529
[](https://gitpod.io/from-referrer/)
|
t-ring-theory
maintainer-merge
|
82/0 |
Mathlib/RingTheory/DiscreteValuationRing/Basic.lean |
1 |
6 |
['github-actions', 'kckennylau', 'pechersky'] |
chrisflav assignee:chrisflav |
6-7986 6 days ago |
17-48607 17 days ago |
18-8110 18 days |
29501 |
Vierkantor author:Vierkantor |
test(TacticAnalysis): ensure `classical`'s effects are picked up |
This test case used to fail, and needed a fix to the `classical` tactic in the standard library:
- [x] depends on: https://github.com/leanprover/lean4/pull/10332
---
[](https://gitpod.io/from-referrer/)
|
maintainer-merge
t-meta
|
10/0 |
MathlibTest/TacticAnalysis.lean |
1 |
6 |
['Vierkantor', 'github-actions', 'grunweg', 'mathlib4-dependent-issues-bot', 'mathlib4-merge-conflict-bot'] |
nobody |
4-67319 4 days ago |
6-59796 6 days ago |
8-66691 8 days |
28395 |
joelriou author:joelriou |
feat(AlgebraicTopology/SimplicialSet): nondegenerate simplices in the standard simplex |
In this PR, we show that `d`-dimensional nondegenerate simplices in `Δ[n]` identify to `Fin (d + 1) ↪o Fin (n + 1)`.
(This PR also contains some general additional API for (non)degenerate simplices. For this reason, three definitions related to subcomplexes generated by a simplex had to be moved from `StdSimplex.lean` to `Subcomplex.lean`.)
---
- [x] depends on: #28337
[](https://gitpod.io/from-referrer/)
|
t-algebraic-topology
maintainer-merge
|
247/20 |
Mathlib/AlgebraicTopology/SimplicialSet/Degenerate.lean,Mathlib/AlgebraicTopology/SimplicialSet/Simplices.lean,Mathlib/AlgebraicTopology/SimplicialSet/StdSimplex.lean,Mathlib/AlgebraicTopology/SimplicialSet/Subcomplex.lean,Mathlib/Order/Hom/Basic.lean |
5 |
24 |
['github-actions', 'joelriou', 'mathlib4-dependent-issues-bot', 'mathlib4-merge-conflict-bot', 'robin-carlier'] |
robin-carlier assignee:robin-carlier |
4-39647 4 days ago |
4-44993 4 days ago |
23-16427 23 days |
24965 |
erdOne author:erdOne |
refactor: Make `IsLocalHom` take unbundled map |
---
[](https://gitpod.io/from-referrer/)
|
maintainer-merge
t-algebra
merge-conflict
awaiting-author
label:t-algebra$ |
16/7 |
Mathlib/Algebra/Group/Units/Hom.lean,Mathlib/AlgebraicGeometry/Scheme.lean,Mathlib/Geometry/RingedSpace/LocallyRingedSpace.lean,Mathlib/Geometry/RingedSpace/LocallyRingedSpace/HasColimits.lean,Mathlib/Geometry/RingedSpace/OpenImmersion.lean |
5 |
6 |
['alreadydone', 'erdOne', 'eric-wieser', 'github-actions', 'leanprover-community-bot-assistant'] |
nobody |
123-2026 4 months ago |
123-2027 4 months ago |
10-26015 10 days |
26912 |
pechersky author:pechersky |
chore(Algebra/Ring/Subring): simp tag `Subring.smul_def` |
s-multiplying by a subtype is easiest to manipulate when both terms are in the ambient type. Many places that had to use the _def lemma for a rewrite, or to include it in a simp set, no longer have to.
Ported from #25308
---
[](https://gitpod.io/from-referrer/)
I found this being not-simp frustrating when talking about submodules over a valuation subring. |
maintainer-merge
t-algebra
merge-conflict
label:t-algebra$ |
68/67 |
Mathlib/Algebra/Algebra/Subalgebra/Basic.lean,Mathlib/Algebra/Field/Subfield/Basic.lean,Mathlib/Algebra/Group/Subgroup/Actions.lean,Mathlib/Algebra/Group/Submonoid/MulAction.lean,Mathlib/Algebra/Module/LocalizedModule/Basic.lean,Mathlib/Algebra/Module/LocalizedModule/Exact.lean,Mathlib/Algebra/Module/LocalizedModule/IsLocalization.lean,Mathlib/Algebra/Module/LocalizedModule/Submodule.lean,Mathlib/Algebra/Ring/Periodic.lean,Mathlib/Algebra/Ring/Subring/Basic.lean,Mathlib/Algebra/Ring/Subsemiring/Basic.lean,Mathlib/Analysis/CStarAlgebra/Basic.lean,Mathlib/FieldTheory/KummerExtension.lean,Mathlib/GroupTheory/GroupAction/Defs.lean,Mathlib/GroupTheory/GroupAction/MultiplePrimitivity.lean,Mathlib/GroupTheory/GroupAction/MultipleTransitivity.lean,Mathlib/GroupTheory/GroupAction/SubMulAction/OfFixingSubgroup.lean,Mathlib/GroupTheory/GroupAction/SubMulAction/OfStabilizer.lean,Mathlib/LinearAlgebra/RootSystem/Irreducible.lean,Mathlib/LinearAlgebra/RootSystem/RootPositive.lean,Mathlib/LinearAlgebra/RootSystem/WeylGroup.lean,Mathlib/RingTheory/Etale/Kaehler.lean,Mathlib/RingTheory/LocalProperties/Projective.lean,Mathlib/RingTheory/Localization/InvSubmonoid.lean,Mathlib/RingTheory/OreLocalization/Basic.lean |
25 |
19 |
['artie2000', 'eric-wieser', 'github-actions', 'j-loreaux', 'linesthatinterlace', 'mathlib4-merge-conflict-bot', 'pechersky'] |
joelriou assignee:joelriou |
32-49917 1 month ago |
32-49918 1 month ago |
51-74059 51 days |
28737 |
astrainfinita author:astrainfinita |
refactor: deprecate `MulEquivClass` |
This PR continues the work from #18806.
Original PR: https://github.com/leanprover-community/mathlib4/pull/18806 |
maintainer-merge
t-algebra
merge-conflict
awaiting-author
label:t-algebra$ |
67/77 |
Mathlib/Algebra/BigOperators/Finprod.lean,Mathlib/Algebra/Group/Equiv/Basic.lean,Mathlib/Algebra/Group/Equiv/Defs.lean,Mathlib/Algebra/Group/Irreducible/Lemmas.lean,Mathlib/Algebra/Group/Subgroup/Map.lean,Mathlib/Algebra/Group/Submonoid/Operations.lean,Mathlib/Algebra/Group/Units/Equiv.lean,Mathlib/Algebra/GroupWithZero/Equiv.lean,Mathlib/Algebra/GroupWithZero/NonZeroDivisors.lean,Mathlib/Algebra/Module/Equiv/Defs.lean,Mathlib/Algebra/Order/CauSeq/Basic.lean,Mathlib/Algebra/Order/Hom/Monoid.lean,Mathlib/Algebra/Prime/Lemmas.lean,Mathlib/Algebra/Ring/Divisibility/Basic.lean,Mathlib/Algebra/Ring/Equiv.lean,Mathlib/Algebra/Star/MonoidHom.lean,Mathlib/Combinatorics/Additive/FreimanHom.lean,Mathlib/GroupTheory/GroupExtension/Defs.lean,Mathlib/GroupTheory/Submonoid/Center.lean,Mathlib/LinearAlgebra/FreeModule/Finite/CardQuotient.lean,Mathlib/RingTheory/Bialgebra/Equiv.lean,Mathlib/RingTheory/Ideal/Norm/AbsNorm.lean,Mathlib/RingTheory/Multiplicity.lean,Mathlib/RingTheory/UniqueFactorizationDomain/NormalizedFactors.lean,Mathlib/Topology/Algebra/ContinuousMonoidHom.lean,Mathlib/Topology/Algebra/InfiniteSum/Basic.lean |
26 |
20 |
['Vierkantor', 'alreadydone', 'astrainfinita', 'github-actions', 'grunweg', 'leanprover-bot', 'leanprover-community-mathlib4-bot', 'mathlib4-merge-conflict-bot'] |
Vierkantor assignee:Vierkantor |
23-53777 23 days ago |
23-53778 23 days ago |
4-17723 4 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 |
25945 |
adomani author:adomani |
feat: the empty line in commands linter |
This linter flags empty lines within a command.
It allows empty lines within doc-strings, module-docs and a couple of other "sensible" places.
It also skips files that are likely to contain meta-code, since there the use of empty lines in definition is more widespread.
This PR continues the work from #25236. |
large-import
t-linter
maintainer-merge
awaiting-author
|
375/7 |
Mathlib.lean,Mathlib/Analysis/Meromorphic/FactorizedRational.lean,Mathlib/CategoryTheory/Comma/StructuredArrow/CommaMap.lean,Mathlib/Init.lean,Mathlib/RepresentationTheory/Homological/GroupHomology/LowDegree.lean,Mathlib/Tactic.lean,Mathlib/Tactic/Linter/EmptyLine.lean,MathlibTest/EmptyLine.lean |
8 |
12 |
['adomani', 'bryangingechen', 'eric-wieser', 'github-actions'] |
bryangingechen assignee:bryangingechen |
67-45839 2 months ago |
67-45839 2 months ago |
42-26074 42 days |
24669 |
qawbecrdtey author:qawbecrdtey |
feat(Analysis/Normed/Operator/LinearIsometry): added definition `LinearIsometryEquiv.prodComm` |
---
[](https://gitpod.io/from-referrer/)
This commit defines a `LinearIsometryEquiv`, and states some trivial theorems about it.
```lean
def prodComm [Module R E₂] : E × E₂ ≃ₗᵢ[R] E₂ × E
```
|
maintainer-merge
t-analysis
awaiting-author
|
8/1 |
Mathlib/Analysis/Normed/Operator/LinearIsometry.lean |
1 |
12 |
['Ruben-VandeVelde', 'eric-wieser', 'faenuccio', 'github-actions', 'j-loreaux', 'jcommelin', 'qawbecrdtey'] |
faenuccio assignee:faenuccio |
26-6041 26 days ago |
115-80273 3 months ago |
32-83569 32 days |
27292 |
gasparattila author:gasparattila |
feat: asymptotic cone of a set |
This PR defines the asymptotic cone of a set in a normed affine space and proves its main properties. This is partial progress towards showing that an unbounded finite-dimensional convex set contains a ray.
---
- [x] depends on: #27221
[](https://gitpod.io/from-referrer/)
|
maintainer-merge
new-contributor
t-analysis
|
466/0 |
Mathlib.lean,Mathlib/Analysis/Normed/Affine/AsymptoticCone.lean,Mathlib/Order/Filter/Map.lean,Mathlib/Topology/Algebra/AsymptoticCone.lean |
4 |
45 |
['AntoineChambert-Loir', 'YaelDillies', 'gasparattila', 'github-actions', 'mathlib4-dependent-issues-bot'] |
YaelDillies assignee:YaelDillies |
16-75947 16 days ago |
59-37840 1 month ago |
73-55374 73 days |
26660 |
strihanje01 author:strihanje01 |
feat(Combinatorics/Additive/VerySmallDoubling): weak non-commutative Kneser's theorem |
add theorem about the structure of a doubling smaller than the golden ratio
---
- [x] depends on: #28653
[](https://gitpod.io/from-referrer/)
|
large-import
maintainer-merge
new-contributor
t-combinatorics
|
215/41 |
Mathlib/Algebra/Group/Action/Pointwise/Finset.lean,Mathlib/Combinatorics/Additive/VerySmallDoubling.lean |
2 |
79 |
['YaelDillies', 'github-actions', 'mathlib4-dependent-issues-bot', 'mathlib4-merge-conflict-bot', 'strihanje01'] |
YaelDillies assignee:YaelDillies |
10-50518 10 days ago |
10-83167 10 days ago |
52-25145 52 days |
28295 |
artie2000 author:artie2000 |
feat(Algebra/Order/Ring/Ordering): basic results about ring (pre)orderings |
* Basic automation for membership of ring orderings
* Alternative constructors for ring preorderings and ring orderings
* Basic results about ring preorderings and their supports, including the special case over a field
---
[](https://gitpod.io/from-referrer/)
- [x] depends on: #27282 |
maintainer-merge
t-algebra
label:t-algebra$ |
203/0 |
Mathlib.lean,Mathlib/Algebra/Group/Subgroup/Defs.lean,Mathlib/Algebra/Order/Ring/Ordering/Basic.lean |
3 |
57 |
['Rob23oba', 'YaelDillies', 'artie2000', 'github-actions', 'mathlib4-dependent-issues-bot', 'mathlib4-merge-conflict-bot', 'vihdzp'] |
joneugster assignee:joneugster |
9-7999 9 days ago |
16-74338 16 days ago |
22-37474 22 days |
26259 |
Raph-DG author:Raph-DG |
feat(Topology): Connecting different notions of locally finite |
In this PR we connect the notions of local finiteness of an indexed family of sets (as in LocallyFinite) and of a set of sets (as in Function.locallyFinsuppWithin)
---
[](https://gitpod.io/from-referrer/)
|
maintainer-merge
t-topology
|
38/0 |
Mathlib/Topology/LocallyFinsupp.lean |
1 |
18 |
['Raph-DG', 'chrisflav', 'github-actions', 'jcommelin', 'kckennylau'] |
jcommelin assignee:jcommelin |
8-38676 8 days ago |
8-63992 8 days ago |
97-27982 97 days |
29275 |
wwylele author:wwylele |
feat(GroupTheory): add DivisibleHull |
This is part of Hahn embedding theorem #27268, where an a ordered group is first embedded in a divisible group / Q-module. I am aware at #25662 there is also an ongoing rewrite of `LocalizedModule` that this PR uses. Hopefully I avoided interfering it by using mostly with public API.
---
- [x] depends on: #29277
- [x] depends on: #29388
- [x] depends on: #29386
[](https://gitpod.io/from-referrer/)
|
t-group-theory
maintainer-merge
|
451/3 |
Mathlib.lean,Mathlib/Algebra/Order/Monoid/Defs.lean,Mathlib/Algebra/Order/Monoid/PNat.lean,Mathlib/Algebra/Order/Monoid/Unbundled/Pow.lean,Mathlib/Data/NNRat/Defs.lean,Mathlib/GroupTheory/DivisibleHull.lean |
6 |
106 |
['YaelDillies', 'github-actions', 'mathlib4-dependent-issues-bot', 'vihdzp', 'wwylele'] |
tb65536 assignee:tb65536 |
8-7999 8 days ago |
15-33876 15 days ago |
25-11078 25 days |
29110 |
NotWearingPants author:NotWearingPants |
feat(Counterexamples): Euler's sum of powers conjecture |
feat(Counterexamples): Euler's sum of powers conjecture
---
[](https://gitpod.io/from-referrer/)
|
awaiting-zulip
maintainer-merge
new-contributor
|
158/0 |
Counterexamples.lean,Counterexamples/EulerSumOfPowers.lean |
2 |
43 |
['MichaelStollBayreuth', 'NotWearingPants', 'eric-wieser', 'github-actions', 'tb65536', 'urkud'] |
MichaelStollBayreuth assignee:MichaelStollBayreuth |
7-26967 7 days ago |
7-27023 7 days ago |
24-25032 24 days |
29513 |
grunweg author:grunweg |
fix(lint-style): parse linter options and load environment extensions correctly |
Parse options and load linter set extension correctly.
This fixes two issues:
- We never called the `toOptions` function that parses Lakefile options into a `Lean.Options` structure: the function we use instead is only meant for command-line options and doesn't handle the `weak.` prefix correctly.
- The way we load linter sets was incorrect: `withImportModules` stopped updating environment extensions since [lean4#6325](https://github.com/leanprover/lean4/pull/6325), and that is exactly what we use to store linter sets. At the time of writing, `importModules` might be a suitable replacement (but this is not very safe, and not documented to be stable). Instead, write a small elaborator returning the environment at the point of elaboration, and use that instead.
---
- [x] depends on: #29584
- [x] depends on: #29585
- [x] depends on: #29586
[](https://gitpod.io/from-referrer/)
|
maintainer-merge
t-meta
|
28/12 |
scripts/lint-style.lean |
1 |
13 |
['Vierkantor', 'adomani', 'github-actions', 'grunweg', 'mathlib4-dependent-issues-bot'] |
nobody |
6-48651 6 days ago |
6-61968 6 days ago |
15-48370 15 days |
29693 |
kckennylau author:kckennylau |
feat(RingTheory): make Euclidean domain from DVR |
---
Zulip: https://leanprover.zulipchat.com/#narrow/channel/116395-maths/topic/Leading.20term.20of.20valuation/near/539666529
[](https://gitpod.io/from-referrer/)
|
t-ring-theory
maintainer-merge
|
82/0 |
Mathlib/RingTheory/DiscreteValuationRing/Basic.lean |
1 |
6 |
['github-actions', 'kckennylau', 'pechersky'] |
chrisflav assignee:chrisflav |
6-7986 6 days ago |
17-48607 17 days ago |
18-8110 18 days |
29501 |
Vierkantor author:Vierkantor |
test(TacticAnalysis): ensure `classical`'s effects are picked up |
This test case used to fail, and needed a fix to the `classical` tactic in the standard library:
- [x] depends on: https://github.com/leanprover/lean4/pull/10332
---
[](https://gitpod.io/from-referrer/)
|
maintainer-merge
t-meta
|
10/0 |
MathlibTest/TacticAnalysis.lean |
1 |
6 |
['Vierkantor', 'github-actions', 'grunweg', 'mathlib4-dependent-issues-bot', 'mathlib4-merge-conflict-bot'] |
nobody |
4-67319 4 days ago |
6-59796 6 days ago |
8-66691 8 days |
28395 |
joelriou author:joelriou |
feat(AlgebraicTopology/SimplicialSet): nondegenerate simplices in the standard simplex |
In this PR, we show that `d`-dimensional nondegenerate simplices in `Δ[n]` identify to `Fin (d + 1) ↪o Fin (n + 1)`.
(This PR also contains some general additional API for (non)degenerate simplices. For this reason, three definitions related to subcomplexes generated by a simplex had to be moved from `StdSimplex.lean` to `Subcomplex.lean`.)
---
- [x] depends on: #28337
[](https://gitpod.io/from-referrer/)
|
t-algebraic-topology
maintainer-merge
|
247/20 |
Mathlib/AlgebraicTopology/SimplicialSet/Degenerate.lean,Mathlib/AlgebraicTopology/SimplicialSet/Simplices.lean,Mathlib/AlgebraicTopology/SimplicialSet/StdSimplex.lean,Mathlib/AlgebraicTopology/SimplicialSet/Subcomplex.lean,Mathlib/Order/Hom/Basic.lean |
5 |
24 |
['github-actions', 'joelriou', 'mathlib4-dependent-issues-bot', 'mathlib4-merge-conflict-bot', 'robin-carlier'] |
robin-carlier assignee:robin-carlier |
4-39647 4 days ago |
4-44993 4 days ago |
23-16427 23 days |
28484 |
euprunin author:euprunin |
chore(Data): golf entire `toReal_eq_toReal`, `count_eq_of_nodup` and `smul_mat_cons` |
---
[](https://gitpod.io/from-referrer/)
|
t-data
maintainer-merge
|
6/11 |
Mathlib/Data/ENNReal/Real.lean,Mathlib/Data/List/Nodup.lean,Mathlib/LinearAlgebra/Matrix/Notation.lean |
3 |
11 |
['bryangingechen', 'github-actions', 'leanprover-bot', 'leanprover-community-mathlib4-bot', 'mathlib4-merge-conflict-bot', 'pechersky', 'qawbecrdtey'] |
pechersky assignee:pechersky |
0-81207 22 hours ago |
1-5098 1 day ago |
48-80807 48 days |
30111 |
sgouezel author:sgouezel |
feat: composing a continuous multilinear map with continuous linear maps is analytic in both variables |
---
[](https://gitpod.io/from-referrer/)
|
maintainer-merge
t-analysis
|
133/0 |
Mathlib/Analysis/Analytic/CPolynomial.lean,Mathlib/Analysis/NormedSpace/Multilinear/Basic.lean |
2 |
15 |
['github-actions', 'loefflerd', 'sgouezel'] |
nobody |
0-59746 16 hours ago |
0-59746 16 hours ago |
1-2916 1 day |
27465 |
erdOne author:erdOne |
feat: the definition of nonarchimedean local fields |
---
- [x] depends on: #27430
- [x] depends on: #27412
- [x] depends on: #27213
[](https://gitpod.io/from-referrer/)
|
maintainer-merge
t-number-theory
|
214/25 |
Mathlib.lean,Mathlib/NumberTheory/LocalField/Basic.lean,Mathlib/RingTheory/Valuation/RankOne.lean,Mathlib/RingTheory/Valuation/ValuativeRel/Basic.lean,Mathlib/Topology/Algebra/Valued/ValuativeRel.lean |
5 |
61 |
['erdOne', 'faenuccio', 'github-actions', 'kbuzzard', 'kckennylau', 'mathlib4-dependent-issues-bot', 'mathlib4-merge-conflict-bot', 'pechersky', 'riccardobrasca'] |
tb65536 assignee:tb65536 |
0-50956 14 hours ago |
1-60246 1 day ago |
14-71314 14 days |
29759 |
NotWearingPants author:NotWearingPants |
feat(Analysis/SpecificLimits/Fibonacci): prove that the ratio of consecutive Fibonacci numbers tends to the golden ratio |
---
[](https://gitpod.io/from-referrer/)
|
maintainer-merge
new-contributor
t-analysis
|
36/0 |
Mathlib.lean,Mathlib/Analysis/SpecificLimits/Fibonacci.lean |
2 |
7 |
['NotWearingPants', 'Ruben-VandeVelde', 'github-actions', 'kckennylau'] |
nobody |
0-45099 12 hours ago |
0-45100 12 hours ago |
8-14078 8 days |
26282 |
AntoineChambert-Loir author:AntoineChambert-Loir |
feat: a theorem of Jordan on primitive subgroups of the permutation group |
A theorem of Jordan on the primitive subgroups of a permutation group:
* if it contains a swap, it is equal to the permutation group,
* if it contains a 3-cycle, it contains the alternating group.
This PR continues the work from #24131.
---
- [x] depends on: #26281
- [x] depends on: #26280
- [x] depends on: #26279
Original PR: https://github.com/leanprover-community/mathlib4/pull/24131
[](https://gitpod.io/from-referrer/) |
t-group-theory
large-import
maintainer-merge
|
939/137 |
Mathlib.lean,Mathlib/Data/Set/Card.lean,Mathlib/GroupTheory/GroupAction/FixingSubgroup.lean,Mathlib/GroupTheory/GroupAction/Jordan.lean,Mathlib/GroupTheory/GroupAction/MultiplePrimitivity.lean,Mathlib/GroupTheory/GroupAction/MultipleTransitivity.lean,Mathlib/GroupTheory/GroupAction/Primitive.lean,Mathlib/GroupTheory/GroupAction/SubMulAction/OfFixingSubgroup.lean,Mathlib/GroupTheory/GroupAction/SubMulAction/OfStabilizer.lean,Mathlib/GroupTheory/Perm/Cycle/Type.lean,Mathlib/SetTheory/Cardinal/Embedding.lean |
11 |
n/a |
['AntoineChambert-Loir', 'adomani', 'github-actions', 'leanprover-community-bot-assistant', 'mathlib4-dependent-issues-bot', 'mathlib4-merge-conflict-bot', 'tb65536'] |
nobody |
0-30339 8 hours ago |
unknown |
unknown |
27844 |
CBirkbeck author:CBirkbeck |
Add q-expansion identities for Eisenstein series. |
This is PR contains some q-expansion identities that are needed to give the q-expansions of Eisenstein series, which will be added as part of #27606.
---
- [x] depends on: #27212
- [x] depends on: #27837
- [x] depends on: #27839
- [x] depends on: #27840
- [x] depends on: #27841
- [x] depends on: #26016
[](https://gitpod.io/from-referrer/)
|
maintainer-merge
t-number-theory
|
257/0 |
Mathlib.lean,Mathlib/Analysis/Complex/Exponential.lean,Mathlib/Analysis/Complex/SummableUniformlyOn.lean,Mathlib/Analysis/Normed/Module/FiniteDimension.lean,Mathlib/NumberTheory/LSeries/RiemannZeta.lean,Mathlib/NumberTheory/ModularForms/EisensteinSeries/Defs.lean,Mathlib/NumberTheory/ModularForms/EisensteinSeries/QExpansion.lean |
7 |
44 |
['CBirkbeck', 'MichaelStollBayreuth', 'github-actions', 'mathlib4-dependent-issues-bot', 'mathlib4-merge-conflict-bot'] |
nobody |
0-15380 4 hours ago |
0-26969 7 hours ago |
0-61485 17 hours |
24965 |
erdOne author:erdOne |
refactor: Make `IsLocalHom` take unbundled map |
---
[](https://gitpod.io/from-referrer/)
|
maintainer-merge
t-algebra
merge-conflict
awaiting-author
label:t-algebra$ |
16/7 |
Mathlib/Algebra/Group/Units/Hom.lean,Mathlib/AlgebraicGeometry/Scheme.lean,Mathlib/Geometry/RingedSpace/LocallyRingedSpace.lean,Mathlib/Geometry/RingedSpace/LocallyRingedSpace/HasColimits.lean,Mathlib/Geometry/RingedSpace/OpenImmersion.lean |
5 |
6 |
['alreadydone', 'erdOne', 'eric-wieser', 'github-actions', 'leanprover-community-bot-assistant'] |
nobody |
123-2026 4 months ago |
123-2027 4 months ago |
10-26015 10 days |
26912 |
pechersky author:pechersky |
chore(Algebra/Ring/Subring): simp tag `Subring.smul_def` |
s-multiplying by a subtype is easiest to manipulate when both terms are in the ambient type. Many places that had to use the _def lemma for a rewrite, or to include it in a simp set, no longer have to.
Ported from #25308
---
[](https://gitpod.io/from-referrer/)
I found this being not-simp frustrating when talking about submodules over a valuation subring. |
maintainer-merge
t-algebra
merge-conflict
label:t-algebra$ |
68/67 |
Mathlib/Algebra/Algebra/Subalgebra/Basic.lean,Mathlib/Algebra/Field/Subfield/Basic.lean,Mathlib/Algebra/Group/Subgroup/Actions.lean,Mathlib/Algebra/Group/Submonoid/MulAction.lean,Mathlib/Algebra/Module/LocalizedModule/Basic.lean,Mathlib/Algebra/Module/LocalizedModule/Exact.lean,Mathlib/Algebra/Module/LocalizedModule/IsLocalization.lean,Mathlib/Algebra/Module/LocalizedModule/Submodule.lean,Mathlib/Algebra/Ring/Periodic.lean,Mathlib/Algebra/Ring/Subring/Basic.lean,Mathlib/Algebra/Ring/Subsemiring/Basic.lean,Mathlib/Analysis/CStarAlgebra/Basic.lean,Mathlib/FieldTheory/KummerExtension.lean,Mathlib/GroupTheory/GroupAction/Defs.lean,Mathlib/GroupTheory/GroupAction/MultiplePrimitivity.lean,Mathlib/GroupTheory/GroupAction/MultipleTransitivity.lean,Mathlib/GroupTheory/GroupAction/SubMulAction/OfFixingSubgroup.lean,Mathlib/GroupTheory/GroupAction/SubMulAction/OfStabilizer.lean,Mathlib/LinearAlgebra/RootSystem/Irreducible.lean,Mathlib/LinearAlgebra/RootSystem/RootPositive.lean,Mathlib/LinearAlgebra/RootSystem/WeylGroup.lean,Mathlib/RingTheory/Etale/Kaehler.lean,Mathlib/RingTheory/LocalProperties/Projective.lean,Mathlib/RingTheory/Localization/InvSubmonoid.lean,Mathlib/RingTheory/OreLocalization/Basic.lean |
25 |
19 |
['artie2000', 'eric-wieser', 'github-actions', 'j-loreaux', 'linesthatinterlace', 'mathlib4-merge-conflict-bot', 'pechersky'] |
joelriou assignee:joelriou |
32-49917 1 month ago |
32-49918 1 month ago |
51-74059 51 days |
28737 |
astrainfinita author:astrainfinita |
refactor: deprecate `MulEquivClass` |
This PR continues the work from #18806.
Original PR: https://github.com/leanprover-community/mathlib4/pull/18806 |
maintainer-merge
t-algebra
merge-conflict
awaiting-author
label:t-algebra$ |
67/77 |
Mathlib/Algebra/BigOperators/Finprod.lean,Mathlib/Algebra/Group/Equiv/Basic.lean,Mathlib/Algebra/Group/Equiv/Defs.lean,Mathlib/Algebra/Group/Irreducible/Lemmas.lean,Mathlib/Algebra/Group/Subgroup/Map.lean,Mathlib/Algebra/Group/Submonoid/Operations.lean,Mathlib/Algebra/Group/Units/Equiv.lean,Mathlib/Algebra/GroupWithZero/Equiv.lean,Mathlib/Algebra/GroupWithZero/NonZeroDivisors.lean,Mathlib/Algebra/Module/Equiv/Defs.lean,Mathlib/Algebra/Order/CauSeq/Basic.lean,Mathlib/Algebra/Order/Hom/Monoid.lean,Mathlib/Algebra/Prime/Lemmas.lean,Mathlib/Algebra/Ring/Divisibility/Basic.lean,Mathlib/Algebra/Ring/Equiv.lean,Mathlib/Algebra/Star/MonoidHom.lean,Mathlib/Combinatorics/Additive/FreimanHom.lean,Mathlib/GroupTheory/GroupExtension/Defs.lean,Mathlib/GroupTheory/Submonoid/Center.lean,Mathlib/LinearAlgebra/FreeModule/Finite/CardQuotient.lean,Mathlib/RingTheory/Bialgebra/Equiv.lean,Mathlib/RingTheory/Ideal/Norm/AbsNorm.lean,Mathlib/RingTheory/Multiplicity.lean,Mathlib/RingTheory/UniqueFactorizationDomain/NormalizedFactors.lean,Mathlib/Topology/Algebra/ContinuousMonoidHom.lean,Mathlib/Topology/Algebra/InfiniteSum/Basic.lean |
26 |
20 |
['Vierkantor', 'alreadydone', 'astrainfinita', 'github-actions', 'grunweg', 'leanprover-bot', 'leanprover-community-mathlib4-bot', 'mathlib4-merge-conflict-bot'] |
Vierkantor assignee:Vierkantor |
23-53777 23 days ago |
23-53778 23 days ago |
4-17723 4 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 |
15649 |
TpmKranz author:TpmKranz |
feat(Computability): introduce Generalised NFA as bridge to Regular Expression |
Lays the groundwork for a proof of equivalence of NFA and RE, w.r.t. described language. Actual connection to NFA comes later, after the groundwork for the opposite direction has been laid.
Second chunk of #12648
---
- [x] depends on: #15647 [Data.FinEnum.Option unchanged since then]
[](https://gitpod.io/from-referrer/)
|
awaiting-zulip
t-computability
new-contributor
awaiting-author
|
298/0 |
Mathlib.lean,Mathlib/Computability/GNFA.lean,Mathlib/Computability/Language.lean,Mathlib/Computability/RegularExpressions.lean,docs/references.bib |
5 |
6 |
['github-actions', 'mathlib4-dependent-issues-bot', 'meithecatte', 'trivial1711'] |
nobody |
151-17165 4 months ago |
151-17174 4 months ago |
23-54870 23 days |
20648 |
anthonyde author:anthonyde |
feat: formalize regular expression -> εNFA |
The file `Computability/RegularExpressionsToEpsilonNFA.lean` contains a formal definition of Thompson's method for constructing an `εNFA` from a `RegularExpression` and a proof of its correctness.
---
- [x] depends on: #20644
- [x] depends on: #20645
[](https://gitpod.io/from-referrer/)
|
awaiting-zulip
t-computability
new-contributor
|
490/0 |
Mathlib.lean,Mathlib/Computability/RegularExpressionsToEpsilonNFA.lean,docs/references.bib |
3 |
5 |
['github-actions', 'mathlib4-dependent-issues-bot', 'meithecatte', 'qawbecrdtey'] |
nobody |
151-16476 4 months ago |
151-17111 4 months ago |
75-77754 75 days |
20238 |
maemre author:maemre |
feat(Computability/DFA): Closure of regular languages under some set operations |
This shows that regular languages are closed under complement and intersection by constructing DFAs for them.
---
Closure under all other operations will be proved when someone adds the proof for DFA<->regular expression equivalence, so they are not part of this PR.
[](https://gitpod.io/from-referrer/)
|
awaiting-zulip
t-computability
new-contributor
awaiting-author
|
159/0 |
Mathlib/Computability/DFA.lean,Mathlib/Computability/Language.lean |
2 |
59 |
['EtienneC30', 'YaelDillies', 'github-actions', 'maemre', 'meithecatte', 'urkud'] |
EtienneC30 assignee:EtienneC30 |
121-69336 3 months ago |
151-17075 4 months ago |
48-67492 48 days |
23929 |
meithecatte author:meithecatte |
feat(Computability/NFA): improve bound on pumping lemma |
---
- [x] depends on: #25321
[](https://gitpod.io/from-referrer/)
|
awaiting-zulip
t-computability
new-contributor
|
101/10 |
Mathlib/Computability/EpsilonNFA.lean,Mathlib/Computability/NFA.lean |
2 |
41 |
['YaelDillies', 'github-actions', 'leanprover-community-bot-assistant', 'mathlib4-dependent-issues-bot', 'meithecatte'] |
nobody |
118-26727 3 months ago |
118-26728 3 months ago |
34-10595 34 days |
29072 |
yury-harmonic author:yury-harmonic |
feat({Nat,Int}/ModEq): add lemmas |
---
I'm not sure that I named these lemmas correctly. Suggestions about better names are welcome!
[](https://gitpod.io/from-referrer/)
|
t-data
awaiting-zulip
|
171/15 |
Mathlib/Data/Int/ModEq.lean,Mathlib/Data/Nat/ModEq.lean |
2 |
5 |
['eric-wieser', 'github-actions', 'yury-harmonic'] |
nobody |
35-70609 1 month ago |
35-70609 1 month ago |
0-55232 15 hours |
29582 |
YaelDillies author:YaelDillies |
chore: rename `_root_.prop` to `Prop.finite` |
This was a surprising name!
---
[](https://gitpod.io/from-referrer/)
|
t-data
awaiting-zulip
|
1/1 |
Mathlib/Data/Fintype/EquivFin.lean |
1 |
11 |
['YaelDillies', 'bryangingechen', 'eric-wieser', 'github-actions', 'grunweg', 'plp127'] |
nobody |
10-82851 10 days ago |
10-82852 10 days ago |
3-1360 3 days |
29110 |
NotWearingPants author:NotWearingPants |
feat(Counterexamples): Euler's sum of powers conjecture |
feat(Counterexamples): Euler's sum of powers conjecture
---
[](https://gitpod.io/from-referrer/)
|
awaiting-zulip
maintainer-merge
new-contributor
|
158/0 |
Counterexamples.lean,Counterexamples/EulerSumOfPowers.lean |
2 |
43 |
['MichaelStollBayreuth', 'NotWearingPants', 'eric-wieser', 'github-actions', 'tb65536', 'urkud'] |
MichaelStollBayreuth assignee:MichaelStollBayreuth |
7-26967 7 days ago |
7-27023 7 days ago |
24-25032 24 days |
24754 |
urkud author:urkud |
feat: define `pathIntegral` |
This is a step towards formalizing of the Poincaré lemma for 1-forms.
---
- [x] depends on: #24831
- [x] depends on: #25047
- [x] depends on: #25048
[](https://gitpod.io/from-referrer/)
|
awaiting-zulip
t-analysis
awaiting-author
|
580/9 |
Mathlib.lean,Mathlib/Analysis/Convex/PathConnected.lean,Mathlib/Analysis/Normed/Module/Basic.lean,Mathlib/MeasureTheory/Integral/IntervalIntegral/Basic.lean,Mathlib/MeasureTheory/Integral/IntervalIntegral/ContDiff.lean,Mathlib/MeasureTheory/Integral/PathIntegral/Basic.lean |
6 |
42 |
['github-actions', 'mathlib4-dependent-issues-bot', 'mathlib4-merge-conflict-bot', 'sgouezel', 'urkud'] |
j-loreaux assignee:j-loreaux |
6-31548 6 days ago |
6-31548 6 days ago |
17-56980 17 days |
29002 |
grunweg author:grunweg |
chore: move Data/Real/Irrational to RingTheory |
It certainly has nothing to do with data (structures).
---
I'm less sure where to put it instead.
[zulip discussion](https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/Cleaning.20up.20.60Data.60/with/536301893) suggested this place; in the future, this could also be split.
[](https://gitpod.io/from-referrer/)
|
file-removed
awaiting-zulip
|
10/10 |
Counterexamples/IrrationalPowerOfIrrational.lean,Mathlib.lean,Mathlib/Analysis/Real/Pi/Irrational.lean,Mathlib/Data/Real/GoldenRatio.lean,Mathlib/NumberTheory/DiophantineApproximation/Basic.lean,Mathlib/NumberTheory/Rayleigh.lean,Mathlib/NumberTheory/Transcendental/Liouville/Basic.lean,Mathlib/RingTheory/Real/Irrational.lean,Mathlib/Tactic/NormNum/Irrational.lean,Mathlib/Topology/Instances/AddCircle/DenseSubgroup.lean,Mathlib/Topology/Instances/Irrational.lean |
11 |
2 |
['github-actions', 'mathlib4-merge-conflict-bot'] |
nobody |
5-63422 5 days ago |
5-63505 5 days ago |
0-67 1 minute |
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/)
|
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 |
3 |
['euprunin', 'github-actions', 'grunweg'] |
nobody |
5-34986 5 days ago |
39-20894 1 month ago |
0-1 1 second |
11800 |
JADekker author:JADekker |
feat : Define KappaLindelöf spaces |
Define KappaLindelöf spaces by following the first one-third of the API for Lindelöf spaces. The remainder will be added in a future PR.
---
[](https://gitpod.io/from-referrer/)
|
awaiting-zulip
t-topology
merge-conflict
please-adopt
|
301/2 |
Mathlib.lean,Mathlib/Topology/Compactness/KappaLindelof.lean,Mathlib/Topology/Compactness/Lindelof.lean |
3 |
38 |
['ADedecker', 'JADekker', 'PatrickMassot', 'StevenClontz', 'adomani', 'github-actions', 'grunweg', 'kim-em', 'urkud'] |
nobody |
382-80598 1 year ago |
383-16173 1 year ago |
119-10687 119 days |
17623 |
FR-vdash-bot author:FR-vdash-bot |
feat(Algebra/Order/GroupWithZero/Unbundled): add some lemmas |
Some lemmas in `Algebra.Order.GroupWithZero.Unbundled` have incorrect or unsatisfactory names, or assumptions that can be omitted using `ZeroLEOneClass`. The lemmas added in this PR are versions of existing lemmas that use the correct or better name or `ZeroLEOneClass` to omit an assumption. The original lemmas will be deprecated in #17593.
| New name | Old name |
|-------------------------|-------------------------|
| `mul_le_one_left₀` | `Left.mul_le_one_of_le_of_le` |
| `mul_lt_one_of_le_of_lt_left₀` (`0 ≤ ·` version) / `mul_lt_one_of_le_of_lt_of_pos_left` | `Left.mul_lt_of_le_of_lt_one_of_pos` |
| `mul_lt_one_of_lt_of_le_left₀` | `Left.mul_lt_of_lt_of_le_one_of_nonneg` |
| `mul_le_one_right₀` | `Right.mul_le_one_of_le_of_le` |
| `mul_lt_one_of_lt_of_le_right₀` (`0 ≤ ·` version) / `mul_lt_one_of_lt_of_le_of_pos_right` | `Right.mul_lt_one_of_lt_of_le_of_pos` |
| `mul_lt_one_of_le_of_lt_right₀` | `Right.mul_lt_one_of_le_of_lt_of_nonneg` |
The following lemmas use `ZeroLEOneClass`.
| New name | Old name |
|-------------------------|-------------------------|
| `(Left.)one_le_mul₀` | `Left.one_le_mul_of_le_of_le` |
| `Left.one_lt_mul_of_le_of_lt₀` | `Left.one_lt_mul_of_le_of_lt_of_pos` |
| `Left.one_lt_mul_of_lt_of_le₀` | `Left.lt_mul_of_lt_of_one_le_of_nonneg` / `one_lt_mul_of_lt_of_le` (still there) |
| `(Left.)one_lt_mul₀` | |
| `Right.one_le_mul₀` | `Right.one_le_mul_of_le_of_le` |
| `Right.one_lt_mul_of_lt_of_le₀` | `Right.one_lt_mul_of_lt_of_le_of_pos` |
| `Right.one_lt_mul_of_le_of_lt₀` | `Right.one_lt_mul_of_le_of_lt_of_nonneg` / `one_lt_mul_of_le_of_lt` (still there) / `one_lt_mul` (still there) |
| `Right.one_lt_mul₀` | `Right.one_lt_mul_of_lt_of_lt` |
---
Split from #17593.
[](https://gitpod.io/from-referrer/)
|
awaiting-zulip
t-order
t-algebra
merge-conflict
label:t-algebra$ |
146/44 |
Mathlib/Algebra/Order/GroupWithZero/Canonical.lean,Mathlib/Algebra/Order/GroupWithZero/Unbundled.lean |
2 |
11 |
['FR-vdash-bot', 'YaelDillies', 'github-actions', 'j-loreaux'] |
nobody |
317-53848 10 months ago |
317-53848 10 months ago |
33-64877 33 days |
8370 |
eric-wieser author:eric-wieser |
refactor(Analysis/NormedSpace/Exponential): remove the `𝕂` argument from `exp` |
This argument is still needed for almost all the lemmas, which means it can longer be found by unification.
We keep around `expSeries 𝕂 A`, as it's needed for talking about the radius of convergence over different base fields.
This is a prerequisite for #8372, as we can't merge the functions until they have the same interface.\
Zulip thread: [#mathlib4 > Real.exp @ 💬](https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/Real.2Eexp/near/401602245)
---
[](https://gitpod.io/from-referrer/)
This is started from the mathport output on https://github.com/leanprover-community/mathlib/pull/19244 |
awaiting-zulip
t-analysis
merge-conflict
|
432/387 |
Mathlib/Analysis/CStarAlgebra/Exponential.lean,Mathlib/Analysis/CStarAlgebra/Spectrum.lean,Mathlib/Analysis/Normed/Algebra/Exponential.lean,Mathlib/Analysis/Normed/Algebra/MatrixExponential.lean,Mathlib/Analysis/Normed/Algebra/QuaternionExponential.lean,Mathlib/Analysis/Normed/Algebra/Spectrum.lean,Mathlib/Analysis/Normed/Algebra/TrivSqZeroExt.lean,Mathlib/Analysis/NormedSpace/DualNumber.lean,Mathlib/Analysis/SpecialFunctions/ContinuousFunctionalCalculus/ExpLog.lean,Mathlib/Analysis/SpecialFunctions/Exponential.lean,Mathlib/Analysis/SpecialFunctions/Trigonometric/Series.lean |
11 |
29 |
['YaelDillies', 'eric-wieser', 'girving', 'github-actions', 'j-loreaux', 'kbuzzard', 'leanprover-community-bot-assistant', 'urkud'] |
nobody |
162-9225 5 months ago |
173-37855 5 months ago |
29-60989 29 days |
15651 |
TpmKranz author:TpmKranz |
feat(Computability/NFA): operations for Thompson's construction |
Lays the groundwork for a proof of equivalence of RE and NFA, w.r.t. described language. Actual connection to REs comes later, after the groundwork for the opposite direction has been laid.
Third chunk of #12648
---
[](https://gitpod.io/from-referrer/)
|
awaiting-zulip
t-computability
new-contributor
merge-conflict
awaiting-author
|
307/5 |
Mathlib/Computability/NFA.lean |
1 |
15 |
['TpmKranz', 'YaelDillies', 'dupuisf', 'github-actions', 'leanprover-community-bot-assistant', 'meithecatte'] |
nobody |
137-39731 4 months ago |
137-39732 4 months ago |
45-84611 45 days |
22361 |
rudynicolop author:rudynicolop |
feat(Computability/NFA): nfa closure properties |
Add the closure properties union, intersection and reversal for NFA.
---
[](https://gitpod.io/from-referrer/)
|
awaiting-zulip
t-computability
new-contributor
merge-conflict
awaiting-author
|
218/2 |
Mathlib/Computability/Language.lean,Mathlib/Computability/NFA.lean |
2 |
90 |
['EtienneC30', 'b-mehta', 'github-actions', 'leanprover-community-bot-assistant', 'meithecatte', 'rudynicolop'] |
EtienneC30 assignee:EtienneC30 |
137-38805 4 months ago |
137-38807 4 months ago |
39-67601 39 days |
17458 |
urkud author:urkud |
refactor(Algebra/Group): make `IsUnit` a typeclass |
Also change some lemmas to assume `[IsUnit _]` instead of `[Invertible _]`.
Motivated by potential non-defeq diamonds in #14986, see also [Zulip](https://leanprover.zulipchat.com/#narrow/stream/116395-maths/topic/Invertible.20and.20data)
I no longer plan to merge this PR, but I'm going to cherry-pick some changes to a new PR before closing this one.
---
[](https://gitpod.io/from-referrer/)
|
awaiting-zulip
t-algebra
merge-conflict
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 |
90-83874 2 months ago |
90-83874 2 months ago |
0-66650 18 hours |
25218 |
kckennylau author:kckennylau |
feat(AlgebraicGeometry): Tate normal form of elliptic curves |
---
[](https://gitpod.io/from-referrer/)
|
awaiting-zulip
new-contributor
t-algebraic-geometry
merge-conflict
|
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 |
90-82712 2 months ago |
90-82713 2 months ago |
6-51040 6 days |
28298 |
thorimur author:thorimur |
chore: dedent `to_additive` docstrings |
This PR uses automation to dedent `to_additive` docstrings throughout Mathlib. It does not lint against indentation or in any way enforce indentation standards for future docstrings. The convention was chosen in accordance with the discussion and polls at [this Zulip thread](https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/Poll.3A.20Indentation.20style.20for.20.60to_additive.60.20docstrings/with/534285603).
---
[](https://gitpod.io/from-referrer/)
|
awaiting-zulip
merge-conflict
documentation
|
949/949 |
Mathlib/Algebra/BigOperators/Fin.lean,Mathlib/Algebra/BigOperators/Finprod.lean,Mathlib/Algebra/BigOperators/Finsupp/Basic.lean,Mathlib/Algebra/BigOperators/Group/Finset/Lemmas.lean,Mathlib/Algebra/BigOperators/Group/List/Basic.lean,Mathlib/Algebra/BigOperators/Group/Multiset/Defs.lean,Mathlib/Algebra/BigOperators/Pi.lean,Mathlib/Algebra/Category/Grp/Basic.lean,Mathlib/Algebra/Category/Grp/FilteredColimits.lean,Mathlib/Algebra/Category/Grp/Limits.lean,Mathlib/Algebra/Category/Grp/Ulift.lean,Mathlib/Algebra/Category/MonCat/Basic.lean,Mathlib/Algebra/Category/MonCat/FilteredColimits.lean,Mathlib/Algebra/Category/MonCat/Limits.lean,Mathlib/Algebra/Category/Semigrp/Basic.lean,Mathlib/Algebra/Free.lean,Mathlib/Algebra/FreeMonoid/Basic.lean,Mathlib/Algebra/Group/Action/Defs.lean,Mathlib/Algebra/Group/Action/Pi.lean,Mathlib/Algebra/Group/Action/Pointwise/Finset.lean,Mathlib/Algebra/Group/Basic.lean,Mathlib/Algebra/Group/Defs.lean,Mathlib/Algebra/Group/Embedding.lean,Mathlib/Algebra/Group/Equiv/Basic.lean,Mathlib/Algebra/Group/Equiv/Defs.lean,Mathlib/Algebra/Group/Equiv/Opposite.lean,Mathlib/Algebra/Group/Even.lean,Mathlib/Algebra/Group/Hom/Basic.lean,Mathlib/Algebra/Group/Hom/Defs.lean,Mathlib/Algebra/Group/Hom/Instances.lean,Mathlib/Algebra/Group/Indicator.lean,Mathlib/Algebra/Group/Pi/Lemmas.lean,Mathlib/Algebra/Group/Pi/Units.lean,Mathlib/Algebra/Group/Pointwise/Finset/Basic.lean,Mathlib/Algebra/Group/Pointwise/Set/Basic.lean,Mathlib/Algebra/Group/Prod.lean,Mathlib/Algebra/Group/Subgroup/Basic.lean,Mathlib/Algebra/Group/Subgroup/Defs.lean,Mathlib/Algebra/Group/Subgroup/Ker.lean,Mathlib/Algebra/Group/Subgroup/Lattice.lean,Mathlib/Algebra/Group/Subgroup/Map.lean,Mathlib/Algebra/Group/Subgroup/Pointwise.lean,Mathlib/Algebra/Group/Submonoid/Basic.lean,Mathlib/Algebra/Group/Submonoid/BigOperators.lean,Mathlib/Algebra/Group/Submonoid/Defs.lean,Mathlib/Algebra/Group/Submonoid/Membership.lean,Mathlib/Algebra/Group/Submonoid/MulAction.lean,Mathlib/Algebra/Group/Submonoid/Operations.lean,Mathlib/Algebra/Group/Subsemigroup/Basic.lean,Mathlib/Algebra/Group/Subsemigroup/Operations.lean,Mathlib/Algebra/Group/UniqueProds/Basic.lean,Mathlib/Algebra/Group/Units/Defs.lean,Mathlib/Algebra/Group/Units/Equiv.lean,Mathlib/Algebra/Group/Units/Hom.lean,Mathlib/Algebra/Group/Units/Opposite.lean,Mathlib/Algebra/Notation/Pi/Basic.lean,Mathlib/Algebra/Opposites.lean,Mathlib/Algebra/Order/BigOperators/Group/List.lean,Mathlib/Algebra/Order/Group/Abs.lean,Mathlib/Algebra/Order/Group/Basic.lean,Mathlib/Algebra/Order/Group/Cone.lean,Mathlib/Algebra/Order/Group/OrderIso.lean,Mathlib/Algebra/Order/Group/Units.lean,Mathlib/Algebra/Order/Hom/Monoid.lean,Mathlib/Algebra/Order/Monoid/Basic.lean,Mathlib/Algebra/Order/Monoid/Canonical/Defs.lean,Mathlib/Algebra/Order/Monoid/Submonoid.lean,Mathlib/Algebra/Order/Monoid/Unbundled/Basic.lean,Mathlib/Algebra/Order/Monoid/Unbundled/WithTop.lean,Mathlib/Algebra/Order/Monoid/Units.lean,Mathlib/Algebra/Order/Pi.lean,Mathlib/Algebra/Regular/Defs.lean,Mathlib/Analysis/Normed/Group/Basic.lean,Mathlib/CategoryTheory/Monoidal/Discrete.lean,Mathlib/Data/Finset/NoncommProd.lean,Mathlib/Data/Fintype/BigOperators.lean,Mathlib/Data/Set/MulAntidiagonal.lean,Mathlib/Data/Set/SMulAntidiagonal.lean,Mathlib/Data/Vector/Basic.lean,Mathlib/Dynamics/Ergodic/Action/OfMinimal.lean,Mathlib/Dynamics/FixedPoints/Prufer.lean,Mathlib/Geometry/Manifold/Algebra/SmoothFunctions.lean,Mathlib/GroupTheory/Complement.lean,Mathlib/GroupTheory/Congruence/Basic.lean,Mathlib/GroupTheory/Congruence/Defs.lean,Mathlib/GroupTheory/Coprod/Basic.lean,Mathlib/GroupTheory/Coset/Basic.lean,Mathlib/GroupTheory/Divisible.lean,Mathlib/GroupTheory/EckmannHilton.lean,Mathlib/GroupTheory/FreeGroup/Basic.lean,Mathlib/GroupTheory/FreeGroup/Reduce.lean,Mathlib/GroupTheory/GroupAction/Basic.lean,Mathlib/GroupTheory/GroupAction/Blocks.lean,Mathlib/GroupTheory/GroupAction/Defs.lean,Mathlib/GroupTheory/GroupAction/FixedPoints.lean,Mathlib/GroupTheory/GroupAction/Hom.lean,Mathlib/GroupTheory/GroupAction/MultipleTransitivity.lean,Mathlib/GroupTheory/GroupAction/Primitive.lean,Mathlib/GroupTheory/GroupAction/Quotient.lean,Mathlib/GroupTheory/GroupAction/SubMulAction.lean |
141 |
10 |
['eric-wieser', 'github-actions', 'grunweg', 'mathlib4-merge-conflict-bot', 'thorimur'] |
nobody |
50-24806 1 month ago |
51-12178 1 month ago |
0-61617 17 hours |
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 |
awaiting-zulip
slow-typeclass-synthesis
t-algebra
t-analysis
merge-conflict
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 |
31-11957 1 month ago |
31-11958 1 month ago |
0-20585 5 hours |
17518 |
grunweg author:grunweg |
feat: lint on declarations mentioning `Invertible` or `Unique` |
Using the same infrastructure as for #10235. Depends on that PR to land first, and also (for the first lint) a zulip discussion if that change is desired/about the best way to enact it.
---
- [ ] depends on: #10235 |
awaiting-zulip
t-linter
merge-conflict
blocked-by-other-PR
|
149/7 |
Mathlib.lean,Mathlib/Algebra/MvPolynomial/PDeriv.lean,Mathlib/Computability/Halting.lean,Mathlib/Computability/TuringMachine.lean,Mathlib/Data/Fintype/Card.lean,Mathlib/GroupTheory/Perm/DomMulAct.lean,Mathlib/Logic/Basic.lean,Mathlib/Logic/Encodable/Basic.lean,Mathlib/NumberTheory/JacobiSum/Basic.lean,Mathlib/Order/Heyting/Regular.lean,Mathlib/RingTheory/MvPolynomial/Symmetric/FundamentalTheorem.lean,Mathlib/Tactic.lean,Mathlib/Tactic/Linter/UnusedAssumptionInType.lean |
13 |
3 |
['github-actions', 'mathlib4-dependent-issues-bot', 'mergify'] |
nobody |
335-34317 11 months ago |
361-22839 11 months ago* |
0-0 0 seconds* |
15654 |
TpmKranz author:TpmKranz |
feat(Computability): language-preserving maps between NFA and RE |
Map REs to NFAs via Thompson's construction and NFAs to REs using GNFAs
Last chunk of #12648
---
- [ ] depends on: #15651
- [ ] depends on: #15649
[](https://gitpod.io/from-referrer/)
|
awaiting-zulip
t-computability
new-contributor
merge-conflict
blocked-by-other-PR
|
985/2 |
Mathlib.lean,Mathlib/Computability/GNFA.lean,Mathlib/Computability/Language.lean,Mathlib/Computability/NFA.lean,Mathlib/Computability/RegularExpressions.lean,Mathlib/Data/FinEnum/Option.lean,docs/references.bib |
7 |
3 |
['github-actions', 'leanprover-community-mathlib4-bot', 'meithecatte'] |
nobody |
151-17125 4 months ago |
151-17130 4 months ago |
0-179 2 minutes |