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 |
| 32825 |
erdOne author:erdOne |
perf(RingTheory): `attribute [irreducible] KaehlerDifferential` |
---
[](https://gitpod.io/from-referrer/)
|
maintainer-merge
awaiting-author
t-ring-theory
|
5/1 |
Mathlib/Algebra/Category/ModuleCat/Differentials/Basic.lean,Mathlib/AlgebraicGeometry/Morphisms/FormallyUnramified.lean,Mathlib/RingTheory/Kaehler/Basic.lean |
3 |
7 |
['erdOne', 'github-actions', 'jcommelin', 'leanprover-radar', 'robin-carlier'] |
nobody |
39-36665 1 month ago |
39-36665 39 days ago |
1-44258 1 day |
| 33832 |
alreadydone author:alreadydone |
feat(Algebra): localization preserves unique factorization |
---
- [x] depends on: #33851
[](https://gitpod.io/from-referrer/)
|
t-algebra
maintainer-merge
awaiting-author
label:t-algebra$ |
143/12 |
Mathlib.lean,Mathlib/Algebra/BigOperators/Group/Finset/Basic.lean,Mathlib/Algebra/GroupWithZero/Associated.lean,Mathlib/GroupTheory/MonoidLocalization/Basic.lean,Mathlib/GroupTheory/MonoidLocalization/UniqueFactorization.lean,Mathlib/RingTheory/Localization/Defs.lean |
6 |
11 |
['Vierkantor', 'dagurtomas', 'github-actions', 'mathlib4-dependent-issues-bot'] |
Vierkantor and dagurtomas assignee:Vierkantor assignee:dagurtomas |
19-20099 19 days ago |
19-20103 19 days ago |
15-70912 15 days |
| 32374 |
adamtopaz author:adamtopaz |
feat(Tactic/WildcardUniverse): Foo.{*, _, v*, max u v} |
This PR creates an elaborator for syntax of the form `Foo.{*, _, v*, max u v}`. A `*` indicates that a new universe parameter should be created, `_` and `max u v` elaborate using the existing level elaboration (so `_` elaborates to a level mvar). The syntax `v*` creates a level parameter of the form `v_n` for some value of `n`.
The newly created level parameters are ordered in a particular way to match the order in which they appear in the syntax. For example, in `Foo.{*, _, v*, max u v}`, the level parameter associated with `*` will come before the other universes, including the parameter created by `v*`, and the parameters `u` and `v`. Similarly the parameter associated with `v*` will come *after* the one for `*`, and before both `u` and `v`.
Note: Unlike `Category* C`, where we understand exactly how the universes involved in `C` (both in the term and its type) relate to the level parameter of the morphisms, we can't expect such precise control in general. For example, when `C.{u} : Type 0`, `Category* C` places the morphism level `v_1` before `u`, but `Category.{*} C` places it after `u`. In other words, `Foo.{...}` only reorders the level parameters based on the parameters that appear in the (elaborated) `...`, without any regard to the universes that appear in the *arguments* to `Foo.{...}`.
Co-authored-by: Claude
---
[](https://gitpod.io/from-referrer/)
|
t-meta
maintainer-merge
awaiting-author
|
720/0 |
Mathlib.lean,Mathlib/Tactic.lean,Mathlib/Tactic/WildcardLevel.lean,MathlibTest/WildcardLevel.lean |
4 |
49 |
['JovanGerb', 'adamtopaz', 'fpvandoorn', 'github-actions', 'leanprover-radar'] |
JovanGerb and dwrensha assignee:dwrensha assignee:JovanGerb |
14-33576 14 days ago |
14-33576 14 days ago |
63-4802 63 days |
| 31141 |
peabrainiac author:peabrainiac |
feat(Analysis/Calculus): parametric integrals over smooth functions are smooth |
Show that for any smooth function `f : H × ℝ → E`, the parametric integral `fun x ↦ ∫ t in a..b, f (x, t) ∂μ` is smooth too.
The argument proceeds inductively, using the fact that derivatives of parametric integrals can themselves be computed as parametric integrals. The necessary lemmas on derivatives of parametric integrals already existed, but took some work to apply due to their generality; we state some convenient special cases.
---
- [x] depends on: #31077
[](https://gitpod.io/from-referrer/)
|
t-analysis
maintainer-merge
awaiting-author
|
470/12 |
Mathlib/Analysis/Calculus/ParametricIntegral.lean,Mathlib/Analysis/Calculus/ParametricIntervalIntegral.lean,Mathlib/MeasureTheory/Integral/DominatedConvergence.lean,Mathlib/Topology/NhdsWithin.lean,Mathlib/Topology/Separation/Regular.lean |
5 |
36 |
['fpvandoorn', 'github-actions', 'j-loreaux', 'mathlib4-dependent-issues-bot', 'mathlib4-merge-conflict-bot', 'peabrainiac', 'sgouezel'] |
j-loreaux assignee:j-loreaux |
13-41927 13 days ago |
13-41927 13 days ago |
22-14837 22 days |
| 32260 |
jsm28 author:jsm28 |
feat(Geometry/Euclidean/Angle/Oriented/Affine): oriented angle bisection and halving unoriented angles |
Add lemmas relating points bisecting an oriented angle to explicit expressions for one unoriented angle in relation to half another unoriented angle.
---
Feel free to golf.
---
- [x] depends on: #32259
[](https://gitpod.io/from-referrer/)
|
t-euclidean-geometry
maintainer-merge
|
107/0 |
Mathlib/Geometry/Euclidean/Angle/Oriented/Affine.lean,Mathlib/Geometry/Euclidean/Angle/Unoriented/Affine.lean |
2 |
7 |
['github-actions', 'jsm28', 'mathlib4-dependent-issues-bot', 'mathlib4-merge-conflict-bot', 'robin-carlier', 'wwylele'] |
JovanGerb assignee:JovanGerb |
7-27549 7 days ago |
70-2913 70 days ago |
70-4552 70 days |
| 34068 |
leomayer1 author:leomayer1 |
feat: give functor categories an instance of `HasBinaryBiproducts` |
---
[](https://gitpod.io/from-referrer/)
|
t-category-theory
new-contributor
maintainer-merge
|
74/0 |
Mathlib.lean,Mathlib/CategoryTheory/Limits/FunctorCategory/BinaryBiproducts.lean |
2 |
12 |
['dagurtomas', 'github-actions', 'leomayer1'] |
dagurtomas assignee:dagurtomas |
7-9163 7 days ago |
7-8306 7 days ago |
8-1350 8 days |
| 35086 |
kebekus author:kebekus |
feat: add congruence lemmas for integrability |
Add simple congruence lemmas for interval- and circle integrability. Perform very minor golfing.
---
[](https://gitpod.io/from-referrer/)
|
t-measure-probability
maintainer-merge
|
93/34 |
Mathlib/MeasureTheory/Integral/CircleAverage.lean,Mathlib/MeasureTheory/Integral/CircleIntegral.lean,Mathlib/MeasureTheory/Integral/IntervalIntegral/Basic.lean,Mathlib/MeasureTheory/Integral/IntervalIntegral/Periodic.lean |
4 |
26 |
['YaelDillies', 'github-actions', 'kebekus'] |
EtienneC30 assignee:EtienneC30 |
6-79329 6 days ago |
10-28554 10 days ago |
13-23994 13 days |
| 34440 |
grunweg author:grunweg |
feat: linter for name components in uppercase |
Per the naming convention, these are errors (unless they are an abbreviation).
Mathlib has *many* violations at the moment: for this reason, we add this as an environment linter
and automatically add all current exceptions. Once these have been fixed, converting to a syntax linter
is desirable.
Until then, track the number of such exceptions as technical debt.
---
[Zulip discussion](https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/naming.20convention.20linter/with/570617527)
Note to self: wait for CI, then do a final nolints update. and try to implement the follow-up soon
[](https://gitpod.io/from-referrer/)
|
t-linter
large-import
maintainer-merge
awaiting-author
|
1018/9 |
Mathlib/Tactic/Linter/Style.lean,MathlibTest/DoubleUnderscore.lean,MathlibTest/HashLint.lean,MathlibTest/Lint.lean,MathlibTest/LintStyle.lean,scripts/nolints.json,scripts/technical-debt-metrics.sh |
7 |
25 |
['Vierkantor', 'github-actions', 'grunweg', 'joneugster'] |
joneugster assignee:joneugster |
6-50749 6 days ago |
6-50749 6 days ago |
13-63250 13 days |
| 35143 |
SnirBroshi author:SnirBroshi |
fix: restore `#min_imports` and other commands |
Make these commands available across Mathlib:
- `#help`
- `#min_imports`
- `#min_imports in`
- `#find_home`
- `proof_wanted`
Add tests that verify commands work when importing basic files, to prevent regressions.
---
[Zulip](https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/.23lint.20is.20broken/near/573303540)
I also think we should have `#check` (the tactic, not the Core command) and `#simp` and `#find_syntax`, but they import `Mathlib.Init` so it can't import them currently.
I'm not sure which of the above were available everywhere before the shake tool was run, let me know if I should add/remove commands.
~~Also there seems to be a bug in `#help` and the module system where it can't find the names of syntaxes, which affects the `#guard_msgs` in the test file, but it should be fixed independently of this PR.~~
[](https://gitpod.io/from-referrer/)
|
large-import
file-removed
t-meta
maintainer-merge
|
182/23 |
Mathlib/Init.lean,Mathlib/Tactic/Common.lean,MathlibTest/BasicFiles/Init.lean,MathlibTest/BasicFiles/Tactic.lean,MathlibTest/BasicFiles/TacticBasic.lean,MathlibTest/BasicFiles/TacticCommon.lean,MathlibTest/HashLint.lean,MathlibTest/UnusedInstancesInType/Fintype.lean |
8 |
17 |
['JovanGerb', 'SnirBroshi', 'github-actions', 'grunweg', 'joneugster', 'thorimur'] |
joneugster assignee:joneugster |
6-46825 6 days ago |
8-25431 8 days ago |
12-33994 12 days |
| 35409 |
JovanGerb author:JovanGerb |
chore(Translate): use `Term.applyAttributes` |
This PR uses the function `Term.applyAttributes` in `to_additive`/`to_dual` for applying attributes. Previously, the code that was there was a copy-paste of `Term.applyAttributes` (and this was outdated due to changes from the module system).
One advantage of the original implementation was the fact that it only calls `pushInfoLeaf` once, and in the new implementation this will typically be done twice for the same syntax. However, I think that this is not a good enough reason for duplicating so much code.
---
[](https://gitpod.io/from-referrer/)
|
t-meta
maintainer-merge
|
6/23 |
Mathlib/Tactic/Translate/Core.lean |
1 |
3 |
['github-actions', 'joneugster'] |
joneugster assignee:joneugster |
6-44502 6 days ago |
8-23946 8 days ago |
8-23453 8 days |
| 35478 |
JovanGerb author:JovanGerb |
chore: refactor `Lean.MVarId.gcongr` to use a monad |
This PR refactors the implementation of the `gcongr` tactic to use its own monad. This will make it easier to refactor/maintain/read the code.
---
[](https://gitpod.io/from-referrer/)
|
t-meta
maintainer-merge
|
98/62 |
Mathlib/Tactic/GCongr/Core.lean,Mathlib/Tactic/GRewrite/Core.lean |
2 |
3 |
['JovanGerb', 'github-actions', 'joneugster'] |
joneugster assignee:joneugster |
6-24501 6 days ago |
6-32135 6 days ago |
6-31642 6 days |
| 34598 |
A-M-Berns author:A-M-Berns |
feat(Geometry/Polygon): nondegeneracy conditions and interconversion with Affine.Triangle |
This PR implements suggestions provided in [this comment](https://github.com/leanprover-community/mathlib4/pull/34393#issuecomment-3810047384) by @jsm28: interconversion between `Polygon P 3` and `Affine.Triangle` as well as the nondegeneracy conditions `NondegenerateVertices` and `NondegenerateEdges`. I tried to keep typeclass restrictions as minimal as possible.
---
|
new-contributor
t-euclidean-geometry
maintainer-merge
|
109/5 |
Mathlib/Geometry/Polygon/Basic.lean |
1 |
26 |
['A-M-Berns', 'eric-wieser', 'github-actions', 'jcommelin', 'jsm28'] |
jsm28 assignee:jsm28 |
6-8204 6 days ago |
6-8204 6 days ago |
23-62297 23 days |
| 35021 |
SnirBroshi author:SnirBroshi |
chore(Data/Bool/Count): golf using grind |
---
The goal was to get rid of the flexible-linter exception, but I ended up golfing more.
[](https://gitpod.io/from-referrer/)
|
t-data
maintainer-merge
|
6/24 |
Mathlib/Data/Bool/Count.lean |
1 |
9 |
['SnirBroshi', 'github-actions', 'joneugster', 'leanprover-radar', 'mathlib-merge-conflicts'] |
joneugster assignee:joneugster |
5-74449 5 days ago |
5-73888 5 days ago |
14-41532 14 days |
| 34193 |
bwangpj author:bwangpj |
feat(Topology/Algebra/Ring): ContinuousAddEquiv.mulLeft, mulRight |
The additive homeomorphism from a topological ring to itself, induced by left/right multiplication by a unit.
From FLT.
---
[](https://gitpod.io/from-referrer/)
|
t-topology
FLT
maintainer-merge
|
25/0 |
Mathlib/Topology/Algebra/Ring/Basic.lean |
1 |
10 |
['bwangpj', 'dagurtomas', 'eric-wieser', 'github-actions', 'riccardobrasca'] |
dagurtomas assignee:dagurtomas |
5-54793 5 days ago |
34-47760 34 days ago |
34-49624 34 days |
| 34380 |
Rogerhu12 author:Rogerhu12 |
feat(GroupTheory/Focal): add focal subgroup theorem |
Define `focalSubgroup` (denoted `H*`) and prove the Focal Subgroup Theorem.
The main result is `inf_commutator_eq_focalSubgroup`, which states that for a Sylow p-subgroup `P` of a finite group `G`, `P ∩ G' = P*`.
This implementation includes:
- The definition of the focal subgroup.
- The transfer homomorphism `G → P/P*`.
- The proof using the transfer map.
Also add [gorenstein1968] to `docs/references.bib`.
---
[](https://gitpod.io/from-referrer/)
|
t-group-theory
new-contributor
maintainer-merge
|
241/10 |
Mathlib.lean,Mathlib/Data/ZMod/QuotientGroup.lean,Mathlib/GroupTheory/Focal.lean,Mathlib/GroupTheory/Sylow.lean,Mathlib/GroupTheory/Transfer.lean,docs/1000.yaml,docs/references.bib |
7 |
73 |
['Rogerhu12', 'github-actions', 'tb65536', 'wwylele'] |
mattrobball assignee:mattrobball |
4-52230 4 days ago |
4-63140 4 days ago |
23-15106 23 days |
| 34112 |
euprunin author:euprunin |
chore: golf using `grind` (and add one supporting `grind` annotation) |
The goal of this golfing PR is to decrease the number of times lemmas are called explicitly (replacing calls to lemmas with calls to tactics). Any decrease in compilation time is a welcome side effect, although it is not a primary objective.
Trace profiling results (shown if ≥10 ms before or after):
* `Quandle.conj_swap`: 63 ms before, 35 ms after 🎉
This golfing PR is batched under the following guidelines:
* Up to ~5 changed files per PR
* Up to ~25 changed declarations per PR
* Up to ~100 changed lines per PR
---
[](https://gitpod.io/from-referrer/)
|
maintainer-merge |
2/3 |
Mathlib/Algebra/Quandle.lean |
1 |
7 |
['euprunin', 'github-actions', 'leanprover-radar', 'robin-carlier'] |
robin-carlier assignee:robin-carlier |
4-45683 4 days ago |
12-17698 12 days ago |
37-12217 37 days |
| 35019 |
JovanGerb author:JovanGerb |
feat(Algebra/Homology/ComplexShape): use `to_dual` |
This PR uses `to_dual` to dualize `ComplexShape` to itself, swapping `next` to `prev` and `up` to `down`.
If we wait for #34863 to be merged first, the we can get rid of one `to_dual existing`.
---
[](https://gitpod.io/from-referrer/)
|
maintainer-merge |
29/50 |
Mathlib/Algebra/Homology/ComplexShape.lean,Mathlib/Tactic/Translate/ToDual.lean |
2 |
2 |
['github-actions', 'robin-carlier'] |
robin-carlier assignee:robin-carlier |
4-45137 4 days ago |
15-20241 15 days ago |
15-19748 15 days |
| 29996 |
vihdzp author:vihdzp |
chore(Order/Concept): `IsIntent` and `IsExtent` |
We define predicates for a set to be an intent/extent, and use them to define alternate constructors for a concept. Using these, we golf the complete lattice instances.
The fields `Concept.intent` and `Concept.extent` already existed, and these serve as unbundled versions of them.
---
- [x] depends on: #30484
[](https://gitpod.io/from-referrer/)
|
t-order
maintainer-merge
|
161/114 |
Mathlib/Order/Concept.lean |
1 |
50 |
['Vierkantor', 'YaelDillies', 'github-actions', 'linesthatinterlace', 'mathlib-dependent-issues', 'mathlib4-merge-conflict-bot', 'plp127', 'vihdzp'] |
YaelDillies assignee:YaelDillies |
4-14147 4 days ago |
4-85673 4 days ago |
25-34990 25 days |
| 33479 |
zcyemi author:zcyemi |
feat(Geometry/Euclidean/Sphere/Power): Add theorem about cospherical points on two intersecting lines |
---
Add `cospherical_of_mul_dist_eq_mul_dist_of_angle_eq_pi`.
~~This theorem is the converse of `EuclideanGeometry.mul_dist_eq_mul_dist_of_cospherical_of_angle_eq_pi`.
However, the ambient type is required to be two-dimensional, i.e. `Fact (finrank ℝ V = 2)`.
I don‘t think (not entirely sure) that lifting the ambient space from dimension 2 to arbitrary dimension is reasonable for this theorem, since the proof is entirely carried out in a two-dimensional plane.
Therefore, I place this theorem in `Euclidean/Angle/Sphere` rather than `Euclidean/Sphere/Power`.~~
Deps:
- [ ] depends on: #33365
|
large-import
t-euclidean-geometry
maintainer-merge
|
109/4 |
Mathlib/Geometry/Euclidean/Sphere/Basic.lean,Mathlib/Geometry/Euclidean/Sphere/Power.lean |
2 |
15 |
['github-actions', 'jsm28', 'mathlib4-dependent-issues-bot', 'zcyemi'] |
nobody |
3-78478 3 days ago |
4-16928 4 days ago |
7-15136 7 days |
| 35567 |
goliath-klein author:goliath-klein |
refactor(PiTensorProduct/{InjectiveNorm, ProjectiveNorm}): Golfs |
This PR cleans up the proofs in
Analysis/Normed/Module/PiTensorProduct/{InjectiveSeminorm.lean, ProjectiveSeminorm.lean}
In addition, it performs the following minor structural changes:
* Weaken assumptions from `NontriviallyNormedField 𝕜` to `NormedField 𝕜` where possible
* The proofs showing that `projectiveSeminorm` actually defines a `Seminorm` are split off into separate lemmas. This mimics the idiom used e.g. in `Analysis.Normed.Modula.Operator.Basic` to define the operator norm.
* Register a `Nonempty x.lifts` instance in PiTensorProduct.lean, to avoid creating a half-dozen local instances.
This is the first in a series of three PRs with the goal to [deprecate `PiTensorProuduct.injectiveSeminorm`](https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/injectiveSeminorm/with/568798633).
---
Co-authored-by: Davood H. T. Tehrani
[](https://gitpod.io/from-referrer/)
|
maintainer-merge
new-contributor
|
101/158 |
Mathlib/Analysis/Normed/Module/PiTensorProduct/InjectiveSeminorm.lean,Mathlib/Analysis/Normed/Module/PiTensorProduct/ProjectiveSeminorm.lean,Mathlib/LinearAlgebra/PiTensorProduct.lean |
3 |
10 |
['github-actions', 'goliath-klein', 'leanprover-radar', 'tb65536'] |
nobody |
3-16651 3 days ago |
4-30680 4 days ago |
4-30198 4 days |
| 35358 |
wwylele author:wwylele |
feat(Geometry/Euclidean): Simplex.closedInterior is closed |
Intermediate lemma towards #34826. The immediate follow up is that the closed interior is measurable, but I'll leave it till the Measure folder appears under Geometry/Euclidean.
---
~~Not sure if this is the best place to put `isClosed_closedInterior`. It is a bit more general than other lemmas in the file (it needs minimal topological space assumptions instead of inner product space), but it still requires `ℝ` so I don't think it should be in the Topology folder.~~ See the updated location
[](https://gitpod.io/from-referrer/)
|
t-euclidean-geometry
maintainer-merge
|
104/24 |
Mathlib/Analysis/Convex/Combination.lean,Mathlib/Analysis/Convex/StdSimplex.lean,Mathlib/Analysis/Convex/Topology.lean,Mathlib/Analysis/Convex/TotallyBounded.lean |
4 |
12 |
['copilot-pull-request-reviewer', 'github-actions', 'jsm28', 'wwylele'] |
jsm28 assignee:jsm28 |
2-79324 2 days ago |
7-72499 7 days ago |
8-83438 8 days |
| 35486 |
Vierkantor author:Vierkantor |
chore(Tactic): improve `continuity` tactic and attribute docstrings |
This PR (re)writes the docstrings for the `continuity` and `continuity?` tactics, and the `continuity` attribute, to consistently match the official style guide, to make sure they are complete while not getting too long.
---
[](https://gitpod.io/from-referrer/)
|
documentation
t-meta
maintainer-merge
|
15/8 |
Mathlib/Tactic/Continuity.lean |
1 |
2 |
['github-actions', 'joneugster'] |
alexjbest assignee:alexjbest |
2-79317 2 days ago |
6-31480 6 days ago |
6-30987 6 days |
| 35495 |
Vierkantor author:Vierkantor |
chore(Tactic): improve `econstructor` and `fconstructor` tactic docstrings |
This PR (re)writes the docstrings for the `econstructor` and `fconstructor` tactics, to consistently match the official style guide, to make sure they are complete while not getting too long.
---
[](https://gitpod.io/from-referrer/)
|
documentation
t-meta
maintainer-merge
|
6/6 |
Mathlib/Tactic/Constructor.lean |
1 |
4 |
['github-actions', 'joneugster'] |
adamtopaz assignee:adamtopaz |
2-79315 2 days ago |
6-23298 6 days ago |
6-22805 6 days |
| 35502 |
Vierkantor author:Vierkantor |
chore(Tactic): document `existsi`, `use` and `use_discharger` tactics |
This PR (re)writes the docstrings for the `existsi`, `use` and `use_discharger` tactics, to consistently match the official style guide, to make sure they are complete while not getting too long.
In particular, I wanted the difference between these tactics and `exists` to be as clear as possible. (Also, why do we have `existsi`?)
---
[](https://gitpod.io/from-referrer/)
|
documentation
t-meta
maintainer-merge
|
34/21 |
Mathlib/Tactic/ExistsI.lean,Mathlib/Tactic/Use.lean |
2 |
4 |
['github-actions', 'joneugster'] |
alexjbest assignee:alexjbest |
2-79314 2 days ago |
6-17031 6 days ago |
6-16538 6 days |
| 35625 |
vihdzp author:vihdzp |
chore: make `liftFun_antisymmRel` public |
This is used in the statements of public theorems, so I'm not sure why it had been made private.
---
[](https://gitpod.io/from-referrer/)
|
t-order
maintainer-merge
|
2/9 |
Mathlib/Order/Antisymmetrization.lean |
1 |
2 |
['YaelDillies', 'github-actions'] |
nobody |
1-38605 1 day ago |
2-72949 2 days ago |
2-72456 2 days |
| 30872 |
rudynicolop author:rudynicolop |
feat(Computability/NFA): NFA closure under concatenation |
This PR proves that regular languages are closed under concatenation via a direct construction on `NFA`s without `εNFA` nor ε-transitions. The main new definitions and results include:
- `M1.concat M2`, the concatenation of `NFA`s `M1` and `M2`, a direct construction without ε-transitions.
- Theorem `accepts_concat : (M1.concat M2).accepts = M1.accepts * M2.accepts`, showing the correctness of the construction.
- Theorem `IsRegular.mul`, showing that regular languages are closed under concatenation.
---
- [x] depends on: #31038
[](https://gitpod.io/from-referrer/)
|
t-computability
new-contributor
maintainer-merge
awaiting-author
|
104/7 |
Mathlib/Computability/NFA.lean |
1 |
67 |
['YaelDillies', 'ctchou', 'eric-wieser', 'github-actions', 'lambda-fairy', 'mathlib4-dependent-issues-bot', 'mathlib4-merge-conflict-bot', 'rudynicolop'] |
YaelDillies assignee:YaelDillies |
1-24579 1 day ago |
26-11981 26 days ago |
59-48116 59 days |
| 32989 |
kim-em author:kim-em |
fix(Tactic/Simps): skip @[defeq] inference for non-exposed definitions |
This PR makes `@[simps]` check whether the source definition's body is exposed before calling `inferDefEqAttr`. When the body is not exposed, we skip the `@[defeq]` inference to avoid validation errors.
Without this fix, using `@[simps]` on a definition that is not `@[expose]`d produces an error like:
```
Theorem Foo_bar has a `rfl`-proof and was thus inferred to be `@[defeq]`, but validating that attribute failed:
Not a definitional equality: the left-hand side ... is not definitionally equal to the right-hand side ...
Note: This theorem is exported from the current module. This requires that all definitions that need to be unfolded to prove this theorem must be exposed.
```
The fix checks `(← getEnv).setExporting true |>.find? cfg.srcDeclName |>.any (·.hasValue)` to determine if the definition body is visible in the public scope, and only calls `inferDefEqAttr` if it is.
🤖 Prepared with Claude Code |
t-meta
maintainer-merge
awaiting-author
|
51/3 |
Mathlib/CategoryTheory/Galois/EssSurj.lean,Mathlib/CategoryTheory/Triangulated/TStructure/TruncLTGE.lean,Mathlib/Tactic/Simps/Basic.lean,MathlibTest/SimpsModule.lean |
4 |
15 |
['JovanGerb', 'Vierkantor', 'github-actions', 'joneugster', 'kim-em'] |
joneugster assignee:joneugster |
1-20432 1 day ago |
32-40629 32 days ago |
37-2239 37 days |
| 35682 |
chenson2018 author:chenson2018 |
chore(Computability/Partrec): remove `linter.flexible` exceptions |
This removes all `set_option linter.flexible false` from this module. Some proofs simply required moving around the usage of `simp`. For others I used `grind`, which is permitted to follow flexible tactics. In all cases I prioritized leaving the structure of the proof either mostly as-is or slightly improving readability.
---
[](https://gitpod.io/from-referrer/)
|
t-computability
maintainer-merge
|
23/41 |
Mathlib/Computability/Partrec.lean |
1 |
6 |
['chenson2018', 'github-actions', 'grunweg'] |
nobody |
1-1171 1 day ago |
1-591 1 day ago |
1-21963 1 day |
| 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 |
| 32825 |
erdOne author:erdOne |
perf(RingTheory): `attribute [irreducible] KaehlerDifferential` |
---
[](https://gitpod.io/from-referrer/)
|
maintainer-merge
awaiting-author
t-ring-theory
|
5/1 |
Mathlib/Algebra/Category/ModuleCat/Differentials/Basic.lean,Mathlib/AlgebraicGeometry/Morphisms/FormallyUnramified.lean,Mathlib/RingTheory/Kaehler/Basic.lean |
3 |
7 |
['erdOne', 'github-actions', 'jcommelin', 'leanprover-radar', 'robin-carlier'] |
nobody |
39-36665 1 month ago |
39-36665 39 days ago |
1-44258 1 day |
| 33832 |
alreadydone author:alreadydone |
feat(Algebra): localization preserves unique factorization |
---
- [x] depends on: #33851
[](https://gitpod.io/from-referrer/)
|
t-algebra
maintainer-merge
awaiting-author
label:t-algebra$ |
143/12 |
Mathlib.lean,Mathlib/Algebra/BigOperators/Group/Finset/Basic.lean,Mathlib/Algebra/GroupWithZero/Associated.lean,Mathlib/GroupTheory/MonoidLocalization/Basic.lean,Mathlib/GroupTheory/MonoidLocalization/UniqueFactorization.lean,Mathlib/RingTheory/Localization/Defs.lean |
6 |
11 |
['Vierkantor', 'dagurtomas', 'github-actions', 'mathlib4-dependent-issues-bot'] |
Vierkantor and dagurtomas assignee:Vierkantor assignee:dagurtomas |
19-20099 19 days ago |
19-20103 19 days ago |
15-70912 15 days |
| 32374 |
adamtopaz author:adamtopaz |
feat(Tactic/WildcardUniverse): Foo.{*, _, v*, max u v} |
This PR creates an elaborator for syntax of the form `Foo.{*, _, v*, max u v}`. A `*` indicates that a new universe parameter should be created, `_` and `max u v` elaborate using the existing level elaboration (so `_` elaborates to a level mvar). The syntax `v*` creates a level parameter of the form `v_n` for some value of `n`.
The newly created level parameters are ordered in a particular way to match the order in which they appear in the syntax. For example, in `Foo.{*, _, v*, max u v}`, the level parameter associated with `*` will come before the other universes, including the parameter created by `v*`, and the parameters `u` and `v`. Similarly the parameter associated with `v*` will come *after* the one for `*`, and before both `u` and `v`.
Note: Unlike `Category* C`, where we understand exactly how the universes involved in `C` (both in the term and its type) relate to the level parameter of the morphisms, we can't expect such precise control in general. For example, when `C.{u} : Type 0`, `Category* C` places the morphism level `v_1` before `u`, but `Category.{*} C` places it after `u`. In other words, `Foo.{...}` only reorders the level parameters based on the parameters that appear in the (elaborated) `...`, without any regard to the universes that appear in the *arguments* to `Foo.{...}`.
Co-authored-by: Claude
---
[](https://gitpod.io/from-referrer/)
|
t-meta
maintainer-merge
awaiting-author
|
720/0 |
Mathlib.lean,Mathlib/Tactic.lean,Mathlib/Tactic/WildcardLevel.lean,MathlibTest/WildcardLevel.lean |
4 |
49 |
['JovanGerb', 'adamtopaz', 'fpvandoorn', 'github-actions', 'leanprover-radar'] |
JovanGerb and dwrensha assignee:dwrensha assignee:JovanGerb |
14-33576 14 days ago |
14-33576 14 days ago |
63-4802 63 days |
| 31141 |
peabrainiac author:peabrainiac |
feat(Analysis/Calculus): parametric integrals over smooth functions are smooth |
Show that for any smooth function `f : H × ℝ → E`, the parametric integral `fun x ↦ ∫ t in a..b, f (x, t) ∂μ` is smooth too.
The argument proceeds inductively, using the fact that derivatives of parametric integrals can themselves be computed as parametric integrals. The necessary lemmas on derivatives of parametric integrals already existed, but took some work to apply due to their generality; we state some convenient special cases.
---
- [x] depends on: #31077
[](https://gitpod.io/from-referrer/)
|
t-analysis
maintainer-merge
awaiting-author
|
470/12 |
Mathlib/Analysis/Calculus/ParametricIntegral.lean,Mathlib/Analysis/Calculus/ParametricIntervalIntegral.lean,Mathlib/MeasureTheory/Integral/DominatedConvergence.lean,Mathlib/Topology/NhdsWithin.lean,Mathlib/Topology/Separation/Regular.lean |
5 |
36 |
['fpvandoorn', 'github-actions', 'j-loreaux', 'mathlib4-dependent-issues-bot', 'mathlib4-merge-conflict-bot', 'peabrainiac', 'sgouezel'] |
j-loreaux assignee:j-loreaux |
13-41927 13 days ago |
13-41927 13 days ago |
22-14837 22 days |
| 32260 |
jsm28 author:jsm28 |
feat(Geometry/Euclidean/Angle/Oriented/Affine): oriented angle bisection and halving unoriented angles |
Add lemmas relating points bisecting an oriented angle to explicit expressions for one unoriented angle in relation to half another unoriented angle.
---
Feel free to golf.
---
- [x] depends on: #32259
[](https://gitpod.io/from-referrer/)
|
t-euclidean-geometry
maintainer-merge
|
107/0 |
Mathlib/Geometry/Euclidean/Angle/Oriented/Affine.lean,Mathlib/Geometry/Euclidean/Angle/Unoriented/Affine.lean |
2 |
7 |
['github-actions', 'jsm28', 'mathlib4-dependent-issues-bot', 'mathlib4-merge-conflict-bot', 'robin-carlier', 'wwylele'] |
JovanGerb assignee:JovanGerb |
7-27549 7 days ago |
70-2913 70 days ago |
70-4552 70 days |
| 34068 |
leomayer1 author:leomayer1 |
feat: give functor categories an instance of `HasBinaryBiproducts` |
---
[](https://gitpod.io/from-referrer/)
|
t-category-theory
new-contributor
maintainer-merge
|
74/0 |
Mathlib.lean,Mathlib/CategoryTheory/Limits/FunctorCategory/BinaryBiproducts.lean |
2 |
12 |
['dagurtomas', 'github-actions', 'leomayer1'] |
dagurtomas assignee:dagurtomas |
7-9163 7 days ago |
7-8306 7 days ago |
8-1350 8 days |
| 35086 |
kebekus author:kebekus |
feat: add congruence lemmas for integrability |
Add simple congruence lemmas for interval- and circle integrability. Perform very minor golfing.
---
[](https://gitpod.io/from-referrer/)
|
t-measure-probability
maintainer-merge
|
93/34 |
Mathlib/MeasureTheory/Integral/CircleAverage.lean,Mathlib/MeasureTheory/Integral/CircleIntegral.lean,Mathlib/MeasureTheory/Integral/IntervalIntegral/Basic.lean,Mathlib/MeasureTheory/Integral/IntervalIntegral/Periodic.lean |
4 |
26 |
['YaelDillies', 'github-actions', 'kebekus'] |
EtienneC30 assignee:EtienneC30 |
6-79329 6 days ago |
10-28554 10 days ago |
13-23994 13 days |
| 34440 |
grunweg author:grunweg |
feat: linter for name components in uppercase |
Per the naming convention, these are errors (unless they are an abbreviation).
Mathlib has *many* violations at the moment: for this reason, we add this as an environment linter
and automatically add all current exceptions. Once these have been fixed, converting to a syntax linter
is desirable.
Until then, track the number of such exceptions as technical debt.
---
[Zulip discussion](https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/naming.20convention.20linter/with/570617527)
Note to self: wait for CI, then do a final nolints update. and try to implement the follow-up soon
[](https://gitpod.io/from-referrer/)
|
t-linter
large-import
maintainer-merge
awaiting-author
|
1018/9 |
Mathlib/Tactic/Linter/Style.lean,MathlibTest/DoubleUnderscore.lean,MathlibTest/HashLint.lean,MathlibTest/Lint.lean,MathlibTest/LintStyle.lean,scripts/nolints.json,scripts/technical-debt-metrics.sh |
7 |
25 |
['Vierkantor', 'github-actions', 'grunweg', 'joneugster'] |
joneugster assignee:joneugster |
6-50749 6 days ago |
6-50749 6 days ago |
13-63250 13 days |
| 35143 |
SnirBroshi author:SnirBroshi |
fix: restore `#min_imports` and other commands |
Make these commands available across Mathlib:
- `#help`
- `#min_imports`
- `#min_imports in`
- `#find_home`
- `proof_wanted`
Add tests that verify commands work when importing basic files, to prevent regressions.
---
[Zulip](https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/.23lint.20is.20broken/near/573303540)
I also think we should have `#check` (the tactic, not the Core command) and `#simp` and `#find_syntax`, but they import `Mathlib.Init` so it can't import them currently.
I'm not sure which of the above were available everywhere before the shake tool was run, let me know if I should add/remove commands.
~~Also there seems to be a bug in `#help` and the module system where it can't find the names of syntaxes, which affects the `#guard_msgs` in the test file, but it should be fixed independently of this PR.~~
[](https://gitpod.io/from-referrer/)
|
large-import
file-removed
t-meta
maintainer-merge
|
182/23 |
Mathlib/Init.lean,Mathlib/Tactic/Common.lean,MathlibTest/BasicFiles/Init.lean,MathlibTest/BasicFiles/Tactic.lean,MathlibTest/BasicFiles/TacticBasic.lean,MathlibTest/BasicFiles/TacticCommon.lean,MathlibTest/HashLint.lean,MathlibTest/UnusedInstancesInType/Fintype.lean |
8 |
17 |
['JovanGerb', 'SnirBroshi', 'github-actions', 'grunweg', 'joneugster', 'thorimur'] |
joneugster assignee:joneugster |
6-46825 6 days ago |
8-25431 8 days ago |
12-33994 12 days |
| 35409 |
JovanGerb author:JovanGerb |
chore(Translate): use `Term.applyAttributes` |
This PR uses the function `Term.applyAttributes` in `to_additive`/`to_dual` for applying attributes. Previously, the code that was there was a copy-paste of `Term.applyAttributes` (and this was outdated due to changes from the module system).
One advantage of the original implementation was the fact that it only calls `pushInfoLeaf` once, and in the new implementation this will typically be done twice for the same syntax. However, I think that this is not a good enough reason for duplicating so much code.
---
[](https://gitpod.io/from-referrer/)
|
t-meta
maintainer-merge
|
6/23 |
Mathlib/Tactic/Translate/Core.lean |
1 |
3 |
['github-actions', 'joneugster'] |
joneugster assignee:joneugster |
6-44502 6 days ago |
8-23946 8 days ago |
8-23453 8 days |
| 35478 |
JovanGerb author:JovanGerb |
chore: refactor `Lean.MVarId.gcongr` to use a monad |
This PR refactors the implementation of the `gcongr` tactic to use its own monad. This will make it easier to refactor/maintain/read the code.
---
[](https://gitpod.io/from-referrer/)
|
t-meta
maintainer-merge
|
98/62 |
Mathlib/Tactic/GCongr/Core.lean,Mathlib/Tactic/GRewrite/Core.lean |
2 |
3 |
['JovanGerb', 'github-actions', 'joneugster'] |
joneugster assignee:joneugster |
6-24501 6 days ago |
6-32135 6 days ago |
6-31642 6 days |
| 34598 |
A-M-Berns author:A-M-Berns |
feat(Geometry/Polygon): nondegeneracy conditions and interconversion with Affine.Triangle |
This PR implements suggestions provided in [this comment](https://github.com/leanprover-community/mathlib4/pull/34393#issuecomment-3810047384) by @jsm28: interconversion between `Polygon P 3` and `Affine.Triangle` as well as the nondegeneracy conditions `NondegenerateVertices` and `NondegenerateEdges`. I tried to keep typeclass restrictions as minimal as possible.
---
|
new-contributor
t-euclidean-geometry
maintainer-merge
|
109/5 |
Mathlib/Geometry/Polygon/Basic.lean |
1 |
26 |
['A-M-Berns', 'eric-wieser', 'github-actions', 'jcommelin', 'jsm28'] |
jsm28 assignee:jsm28 |
6-8204 6 days ago |
6-8204 6 days ago |
23-62297 23 days |
| 35021 |
SnirBroshi author:SnirBroshi |
chore(Data/Bool/Count): golf using grind |
---
The goal was to get rid of the flexible-linter exception, but I ended up golfing more.
[](https://gitpod.io/from-referrer/)
|
t-data
maintainer-merge
|
6/24 |
Mathlib/Data/Bool/Count.lean |
1 |
9 |
['SnirBroshi', 'github-actions', 'joneugster', 'leanprover-radar', 'mathlib-merge-conflicts'] |
joneugster assignee:joneugster |
5-74449 5 days ago |
5-73888 5 days ago |
14-41532 14 days |
| 34193 |
bwangpj author:bwangpj |
feat(Topology/Algebra/Ring): ContinuousAddEquiv.mulLeft, mulRight |
The additive homeomorphism from a topological ring to itself, induced by left/right multiplication by a unit.
From FLT.
---
[](https://gitpod.io/from-referrer/)
|
t-topology
FLT
maintainer-merge
|
25/0 |
Mathlib/Topology/Algebra/Ring/Basic.lean |
1 |
10 |
['bwangpj', 'dagurtomas', 'eric-wieser', 'github-actions', 'riccardobrasca'] |
dagurtomas assignee:dagurtomas |
5-54793 5 days ago |
34-47760 34 days ago |
34-49624 34 days |
| 34380 |
Rogerhu12 author:Rogerhu12 |
feat(GroupTheory/Focal): add focal subgroup theorem |
Define `focalSubgroup` (denoted `H*`) and prove the Focal Subgroup Theorem.
The main result is `inf_commutator_eq_focalSubgroup`, which states that for a Sylow p-subgroup `P` of a finite group `G`, `P ∩ G' = P*`.
This implementation includes:
- The definition of the focal subgroup.
- The transfer homomorphism `G → P/P*`.
- The proof using the transfer map.
Also add [gorenstein1968] to `docs/references.bib`.
---
[](https://gitpod.io/from-referrer/)
|
t-group-theory
new-contributor
maintainer-merge
|
241/10 |
Mathlib.lean,Mathlib/Data/ZMod/QuotientGroup.lean,Mathlib/GroupTheory/Focal.lean,Mathlib/GroupTheory/Sylow.lean,Mathlib/GroupTheory/Transfer.lean,docs/1000.yaml,docs/references.bib |
7 |
73 |
['Rogerhu12', 'github-actions', 'tb65536', 'wwylele'] |
mattrobball assignee:mattrobball |
4-52230 4 days ago |
4-63140 4 days ago |
23-15106 23 days |
| 34112 |
euprunin author:euprunin |
chore: golf using `grind` (and add one supporting `grind` annotation) |
The goal of this golfing PR is to decrease the number of times lemmas are called explicitly (replacing calls to lemmas with calls to tactics). Any decrease in compilation time is a welcome side effect, although it is not a primary objective.
Trace profiling results (shown if ≥10 ms before or after):
* `Quandle.conj_swap`: 63 ms before, 35 ms after 🎉
This golfing PR is batched under the following guidelines:
* Up to ~5 changed files per PR
* Up to ~25 changed declarations per PR
* Up to ~100 changed lines per PR
---
[](https://gitpod.io/from-referrer/)
|
maintainer-merge |
2/3 |
Mathlib/Algebra/Quandle.lean |
1 |
7 |
['euprunin', 'github-actions', 'leanprover-radar', 'robin-carlier'] |
robin-carlier assignee:robin-carlier |
4-45683 4 days ago |
12-17698 12 days ago |
37-12217 37 days |
| 35019 |
JovanGerb author:JovanGerb |
feat(Algebra/Homology/ComplexShape): use `to_dual` |
This PR uses `to_dual` to dualize `ComplexShape` to itself, swapping `next` to `prev` and `up` to `down`.
If we wait for #34863 to be merged first, the we can get rid of one `to_dual existing`.
---
[](https://gitpod.io/from-referrer/)
|
maintainer-merge |
29/50 |
Mathlib/Algebra/Homology/ComplexShape.lean,Mathlib/Tactic/Translate/ToDual.lean |
2 |
2 |
['github-actions', 'robin-carlier'] |
robin-carlier assignee:robin-carlier |
4-45137 4 days ago |
15-20241 15 days ago |
15-19748 15 days |
| 29996 |
vihdzp author:vihdzp |
chore(Order/Concept): `IsIntent` and `IsExtent` |
We define predicates for a set to be an intent/extent, and use them to define alternate constructors for a concept. Using these, we golf the complete lattice instances.
The fields `Concept.intent` and `Concept.extent` already existed, and these serve as unbundled versions of them.
---
- [x] depends on: #30484
[](https://gitpod.io/from-referrer/)
|
t-order
maintainer-merge
|
161/114 |
Mathlib/Order/Concept.lean |
1 |
50 |
['Vierkantor', 'YaelDillies', 'github-actions', 'linesthatinterlace', 'mathlib-dependent-issues', 'mathlib4-merge-conflict-bot', 'plp127', 'vihdzp'] |
YaelDillies assignee:YaelDillies |
4-14147 4 days ago |
4-85673 4 days ago |
25-34990 25 days |
| 33479 |
zcyemi author:zcyemi |
feat(Geometry/Euclidean/Sphere/Power): Add theorem about cospherical points on two intersecting lines |
---
Add `cospherical_of_mul_dist_eq_mul_dist_of_angle_eq_pi`.
~~This theorem is the converse of `EuclideanGeometry.mul_dist_eq_mul_dist_of_cospherical_of_angle_eq_pi`.
However, the ambient type is required to be two-dimensional, i.e. `Fact (finrank ℝ V = 2)`.
I don‘t think (not entirely sure) that lifting the ambient space from dimension 2 to arbitrary dimension is reasonable for this theorem, since the proof is entirely carried out in a two-dimensional plane.
Therefore, I place this theorem in `Euclidean/Angle/Sphere` rather than `Euclidean/Sphere/Power`.~~
Deps:
- [ ] depends on: #33365
|
large-import
t-euclidean-geometry
maintainer-merge
|
109/4 |
Mathlib/Geometry/Euclidean/Sphere/Basic.lean,Mathlib/Geometry/Euclidean/Sphere/Power.lean |
2 |
15 |
['github-actions', 'jsm28', 'mathlib4-dependent-issues-bot', 'zcyemi'] |
nobody |
3-78478 3 days ago |
4-16928 4 days ago |
7-15136 7 days |
| 35567 |
goliath-klein author:goliath-klein |
refactor(PiTensorProduct/{InjectiveNorm, ProjectiveNorm}): Golfs |
This PR cleans up the proofs in
Analysis/Normed/Module/PiTensorProduct/{InjectiveSeminorm.lean, ProjectiveSeminorm.lean}
In addition, it performs the following minor structural changes:
* Weaken assumptions from `NontriviallyNormedField 𝕜` to `NormedField 𝕜` where possible
* The proofs showing that `projectiveSeminorm` actually defines a `Seminorm` are split off into separate lemmas. This mimics the idiom used e.g. in `Analysis.Normed.Modula.Operator.Basic` to define the operator norm.
* Register a `Nonempty x.lifts` instance in PiTensorProduct.lean, to avoid creating a half-dozen local instances.
This is the first in a series of three PRs with the goal to [deprecate `PiTensorProuduct.injectiveSeminorm`](https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/injectiveSeminorm/with/568798633).
---
Co-authored-by: Davood H. T. Tehrani
[](https://gitpod.io/from-referrer/)
|
maintainer-merge
new-contributor
|
101/158 |
Mathlib/Analysis/Normed/Module/PiTensorProduct/InjectiveSeminorm.lean,Mathlib/Analysis/Normed/Module/PiTensorProduct/ProjectiveSeminorm.lean,Mathlib/LinearAlgebra/PiTensorProduct.lean |
3 |
10 |
['github-actions', 'goliath-klein', 'leanprover-radar', 'tb65536'] |
nobody |
3-16651 3 days ago |
4-30680 4 days ago |
4-30198 4 days |
| 35358 |
wwylele author:wwylele |
feat(Geometry/Euclidean): Simplex.closedInterior is closed |
Intermediate lemma towards #34826. The immediate follow up is that the closed interior is measurable, but I'll leave it till the Measure folder appears under Geometry/Euclidean.
---
~~Not sure if this is the best place to put `isClosed_closedInterior`. It is a bit more general than other lemmas in the file (it needs minimal topological space assumptions instead of inner product space), but it still requires `ℝ` so I don't think it should be in the Topology folder.~~ See the updated location
[](https://gitpod.io/from-referrer/)
|
t-euclidean-geometry
maintainer-merge
|
104/24 |
Mathlib/Analysis/Convex/Combination.lean,Mathlib/Analysis/Convex/StdSimplex.lean,Mathlib/Analysis/Convex/Topology.lean,Mathlib/Analysis/Convex/TotallyBounded.lean |
4 |
12 |
['copilot-pull-request-reviewer', 'github-actions', 'jsm28', 'wwylele'] |
jsm28 assignee:jsm28 |
2-79324 2 days ago |
7-72499 7 days ago |
8-83438 8 days |
| 35486 |
Vierkantor author:Vierkantor |
chore(Tactic): improve `continuity` tactic and attribute docstrings |
This PR (re)writes the docstrings for the `continuity` and `continuity?` tactics, and the `continuity` attribute, to consistently match the official style guide, to make sure they are complete while not getting too long.
---
[](https://gitpod.io/from-referrer/)
|
documentation
t-meta
maintainer-merge
|
15/8 |
Mathlib/Tactic/Continuity.lean |
1 |
2 |
['github-actions', 'joneugster'] |
alexjbest assignee:alexjbest |
2-79317 2 days ago |
6-31480 6 days ago |
6-30987 6 days |
| 35495 |
Vierkantor author:Vierkantor |
chore(Tactic): improve `econstructor` and `fconstructor` tactic docstrings |
This PR (re)writes the docstrings for the `econstructor` and `fconstructor` tactics, to consistently match the official style guide, to make sure they are complete while not getting too long.
---
[](https://gitpod.io/from-referrer/)
|
documentation
t-meta
maintainer-merge
|
6/6 |
Mathlib/Tactic/Constructor.lean |
1 |
4 |
['github-actions', 'joneugster'] |
adamtopaz assignee:adamtopaz |
2-79315 2 days ago |
6-23298 6 days ago |
6-22805 6 days |
| 35502 |
Vierkantor author:Vierkantor |
chore(Tactic): document `existsi`, `use` and `use_discharger` tactics |
This PR (re)writes the docstrings for the `existsi`, `use` and `use_discharger` tactics, to consistently match the official style guide, to make sure they are complete while not getting too long.
In particular, I wanted the difference between these tactics and `exists` to be as clear as possible. (Also, why do we have `existsi`?)
---
[](https://gitpod.io/from-referrer/)
|
documentation
t-meta
maintainer-merge
|
34/21 |
Mathlib/Tactic/ExistsI.lean,Mathlib/Tactic/Use.lean |
2 |
4 |
['github-actions', 'joneugster'] |
alexjbest assignee:alexjbest |
2-79314 2 days ago |
6-17031 6 days ago |
6-16538 6 days |
| 35625 |
vihdzp author:vihdzp |
chore: make `liftFun_antisymmRel` public |
This is used in the statements of public theorems, so I'm not sure why it had been made private.
---
[](https://gitpod.io/from-referrer/)
|
t-order
maintainer-merge
|
2/9 |
Mathlib/Order/Antisymmetrization.lean |
1 |
2 |
['YaelDillies', 'github-actions'] |
nobody |
1-38605 1 day ago |
2-72949 2 days ago |
2-72456 2 days |
| 30872 |
rudynicolop author:rudynicolop |
feat(Computability/NFA): NFA closure under concatenation |
This PR proves that regular languages are closed under concatenation via a direct construction on `NFA`s without `εNFA` nor ε-transitions. The main new definitions and results include:
- `M1.concat M2`, the concatenation of `NFA`s `M1` and `M2`, a direct construction without ε-transitions.
- Theorem `accepts_concat : (M1.concat M2).accepts = M1.accepts * M2.accepts`, showing the correctness of the construction.
- Theorem `IsRegular.mul`, showing that regular languages are closed under concatenation.
---
- [x] depends on: #31038
[](https://gitpod.io/from-referrer/)
|
t-computability
new-contributor
maintainer-merge
awaiting-author
|
104/7 |
Mathlib/Computability/NFA.lean |
1 |
67 |
['YaelDillies', 'ctchou', 'eric-wieser', 'github-actions', 'lambda-fairy', 'mathlib4-dependent-issues-bot', 'mathlib4-merge-conflict-bot', 'rudynicolop'] |
YaelDillies assignee:YaelDillies |
1-24579 1 day ago |
26-11981 26 days ago |
59-48116 59 days |
| 32989 |
kim-em author:kim-em |
fix(Tactic/Simps): skip @[defeq] inference for non-exposed definitions |
This PR makes `@[simps]` check whether the source definition's body is exposed before calling `inferDefEqAttr`. When the body is not exposed, we skip the `@[defeq]` inference to avoid validation errors.
Without this fix, using `@[simps]` on a definition that is not `@[expose]`d produces an error like:
```
Theorem Foo_bar has a `rfl`-proof and was thus inferred to be `@[defeq]`, but validating that attribute failed:
Not a definitional equality: the left-hand side ... is not definitionally equal to the right-hand side ...
Note: This theorem is exported from the current module. This requires that all definitions that need to be unfolded to prove this theorem must be exposed.
```
The fix checks `(← getEnv).setExporting true |>.find? cfg.srcDeclName |>.any (·.hasValue)` to determine if the definition body is visible in the public scope, and only calls `inferDefEqAttr` if it is.
🤖 Prepared with Claude Code |
t-meta
maintainer-merge
awaiting-author
|
51/3 |
Mathlib/CategoryTheory/Galois/EssSurj.lean,Mathlib/CategoryTheory/Triangulated/TStructure/TruncLTGE.lean,Mathlib/Tactic/Simps/Basic.lean,MathlibTest/SimpsModule.lean |
4 |
15 |
['JovanGerb', 'Vierkantor', 'github-actions', 'joneugster', 'kim-em'] |
joneugster assignee:joneugster |
1-20432 1 day ago |
32-40629 32 days ago |
37-2239 37 days |
| 35682 |
chenson2018 author:chenson2018 |
chore(Computability/Partrec): remove `linter.flexible` exceptions |
This removes all `set_option linter.flexible false` from this module. Some proofs simply required moving around the usage of `simp`. For others I used `grind`, which is permitted to follow flexible tactics. In all cases I prioritized leaving the structure of the proof either mostly as-is or slightly improving readability.
---
[](https://gitpod.io/from-referrer/)
|
t-computability
maintainer-merge
|
23/41 |
Mathlib/Computability/Partrec.lean |
1 |
6 |
['chenson2018', 'github-actions', 'grunweg'] |
nobody |
1-1171 1 day ago |
1-591 1 day ago |
1-21963 1 day |
| 30640 |
SnirBroshi author:SnirBroshi |
feat(Combinatorics/SimpleGraph/Acyclic): acyclic and bridge theorems + golfing |
---
- [x] depends on: #30542
- [x] depends on: #30570
[](https://gitpod.io/from-referrer/)
|
t-combinatorics
maintainer-merge
|
76/80 |
Mathlib/Combinatorics/SimpleGraph/Acyclic.lean,Mathlib/Combinatorics/SimpleGraph/Connectivity/Connected.lean |
2 |
14 |
['SnirBroshi', 'b-mehta', 'github-actions', 'mathlib-merge-conflicts', 'mathlib4-dependent-issues-bot', 'mathlib4-merge-conflict-bot', 'ocfnash'] |
b-mehta assignee:b-mehta |
0-30573 8 hours ago |
0-30993 8 hours ago |
71-50516 71 days |
| 33364 |
BoltonBailey author:BoltonBailey |
feat(Analysis/Convex/SimplicialComplex): add AbstractSimplicialComplex + constructions |
This adds the concept of [abstract simplicial complex](https://en.wikipedia.org/wiki/Abstract_simplicial_complex) (and refactors SimplicialComplex in terms of it).
It also adds constructions that makes it easy to define a simplicial complex for any index family of points which is downward closed and which is affinely independent. I also include a construction of (abstract and geometric) simplicial complexes associated with a SimpleGraph, where vertices become 0-faces and edges become 1-faces, which could be useful later in defining the topological notion of a graph embedding.
Co-authored-by: Claude Opus 4.5
---
- [x] depends on: #35115
[](https://gitpod.io/from-referrer/)
|
t-analysis
t-algebraic-topology
maintainer-merge
|
450/15 |
Mathlib.lean,Mathlib/AlgebraicTopology/SimplicialComplex/Basic.lean,Mathlib/Analysis/Convex/SimplicialComplex/AffineIndependentUnion.lean,Mathlib/Analysis/Convex/SimplicialComplex/Basic.lean,Mathlib/Data/Sym/Sym2.lean,Mathlib/LinearAlgebra/AffineSpace/Independent.lean,Mathlib/Tactic/Linter/DirectoryDependency.lean |
7 |
28 |
['BoltonBailey', 'denisgorod', 'eric-wieser', 'github-actions', 'j-loreaux', 'mathlib-dependent-issues', 'mathlib-merge-conflicts', 'peabrainiac'] |
j-loreaux assignee:j-loreaux |
0-25160 6 hours ago |
10-74222 10 days ago |
11-67989 11 days |
| 35711 |
joelriou author:joelriou |
chore(CategoryTheory/Sites): fix IsSheaf.isSheafFor |
The parameter `J : GrothendieckTopology _` is made implicit, which eases the use of dot notation.
---
[](https://gitpod.io/from-referrer/)
|
t-category-theory
maintainer-merge
|
15/14 |
Mathlib/CategoryTheory/Sites/Descent/DescentData.lean,Mathlib/CategoryTheory/Sites/Descent/Precoverage.lean,Mathlib/CategoryTheory/Sites/PrecoverageToGrothendieck.lean,Mathlib/CategoryTheory/Sites/SheafOfTypes.lean,Mathlib/CategoryTheory/Sites/Types.lean,Mathlib/Topology/Sheaves/Sheaf.lean |
6 |
2 |
['chrisflav', 'github-actions'] |
nobody |
0-19817 5 hours ago |
0-48383 13 hours ago |
0-47890 13 hours |
| 34932 |
erdOne author:erdOne |
feat(AlgebraicGeometry): formally etale morphisms |
---
[](https://gitpod.io/from-referrer/)
|
t-algebraic-geometry
maintainer-merge
|
163/12 |
Mathlib.lean,Mathlib/AlgebraicGeometry/Morphisms/Etale.lean,Mathlib/AlgebraicGeometry/Morphisms/FormallyEtale.lean,Mathlib/AlgebraicGeometry/Morphisms/RingHomProperties.lean,Mathlib/RingTheory/RingHom/Etale.lean |
5 |
14 |
['chrisflav', 'erdOne', 'github-actions', 'joneugster'] |
alexjbest assignee:alexjbest |
0-8979 2 hours ago |
9-4159 9 days ago |
11-33900 11 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 |
461-38749 1 year ago |
unknown |
unknown |
| 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 |
merge-conflict
t-analysis
awaiting-zulip
|
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 |
305-80526 9 months ago |
unknown |
unknown |
| 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 |
295-2026 9 months ago |
unknown |
unknown |
| 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
|
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 |
262-11628 8 months ago |
262-11629 262 days ago |
0-37135 10 hours |
| 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 |
234-68775 7 months ago |
unknown |
unknown |
| 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 |
234-67613 7 months ago |
unknown |
unknown |
| 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 |
174-83258 5 months ago |
183-34412 183 days ago |
0-16864 4 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 |
131-60468 4 months ago |
unknown |
unknown |
| 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'] |
EtienneC30 assignee:EtienneC30 |
112-70158 3 months ago |
unknown |
unknown |
| 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 |
103-71342 3 months ago |
143-50008 143 days ago |
0-29227 8 hours |
| 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 |
99-2074 3 months ago |
unknown |
unknown |
| 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 |
98-18315 3 months ago |
unknown |
unknown |
| 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'] |
EtienneC30 assignee:EtienneC30 |
98-17405 3 months ago |
unknown |
unknown |
| 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 |
97-55483 3 months ago |
unknown |
unknown |
| 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 |
97-27349 3 months ago |
unknown |
unknown |
| 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 |
76-9195 2 months ago |
unknown |
unknown |
| 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 |
48-63908 1 month ago |
49-24241 49 days ago |
5-70690 5 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 |
33-26343 1 month ago |
33-26343 33 days ago |
40-36049 40 days |
| 34396 |
dupuisf author:dupuisf |
feat: notation for `Ring.inverse` |
This PR adds the global notation `x⁻¹ʳ` for `Ring.inverse x`, and a few extra API lemmas about it.
---
[](https://gitpod.io/from-referrer/)
|
t-algebra
awaiting-zulip
label:t-algebra$ |
58/19 |
Mathlib/Algebra/GroupWithZero/Units/Basic.lean |
1 |
1 |
['github-actions'] |
nobody |
30-65774 30 days ago |
unknown |
unknown |
| 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 |
26-31161 26 days ago |
26-31161 26 days ago |
42-19879 42 days |
| 34656 |
vihdzp author:vihdzp |
refactor: review `exists_irreducible_of_degree_pos` theorems |
This PR does the following:
- Rename `exists_irreducible_of_degree_pos` to `exists_irreducible_dvd_of_degree_pos`. The previous name reads as if this were proving that an irreducible polynomial of any positive degree exists.
- Deprecate variants which differ only in the spelling of `0 < f.degree`. We already have quite a lot of API for converting between `natDegree` and `degree`, and we should just use that instead.
---
[](https://gitpod.io/from-referrer/)
|
t-ring-theory
t-algebra
awaiting-zulip
label:t-algebra$ |
9/4 |
Mathlib/RingTheory/Polynomial/UniqueFactorization.lean |
1 |
4 |
['github-actions', 'tb65536', 'vihdzp'] |
nobody |
23-53227 23 days ago |
23-53227 23 days ago |
0-48545 13 hours |
| 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'] |
dagurtomas assignee:dagurtomas |
23-43766 23 days ago |
64-20668 64 days ago |
10-64694 10 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 |
23-43571 23 days ago |
49-27703 49 days ago |
11-6345 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 |
15-3180 15 days ago |
unknown |
unknown |
| 34649 |
peabrainiac author:peabrainiac |
feat(Analysis/Calculus/ContDiff): add notation `ℕ∞ω` for `WithTop ℕ∞` |
Add a `ContDiff`-scoped notation `ℕ∞ω` for `WithTop ℕ∞`, accompanying the existing notations `∞` and `ω` for `(⊤ : ℕ∞) : ℕ∞ω` and `⊤ : ℕ∞ω`.
---
I've also replaced `WithTop ℕ∞` with this new notation already in the files that mention it the most, but not in all files yet; many mention `WithTop ℕ∞` just a couple of times but don't open the `ContDiff` namespace. I'm not sure whether that should be taken as a sign to not make the notation scoped, or whether the solution is just to `open scoped ContDiff` in these files or not use the notation there.
[](https://gitpod.io/from-referrer/)
|
t-differential-geometry
t-analysis
awaiting-author
awaiting-zulip
|
221/218 |
Mathlib/Analysis/Calculus/BumpFunction/FiniteDimension.lean,Mathlib/Analysis/Calculus/ContDiff/Basic.lean,Mathlib/Analysis/Calculus/ContDiff/Bounds.lean,Mathlib/Analysis/Calculus/ContDiff/CPolynomial.lean,Mathlib/Analysis/Calculus/ContDiff/Comp.lean,Mathlib/Analysis/Calculus/ContDiff/Defs.lean,Mathlib/Analysis/Calculus/ContDiff/Deriv.lean,Mathlib/Analysis/Calculus/ContDiff/FTaylorSeries.lean,Mathlib/Analysis/Calculus/ContDiff/Operations.lean,Mathlib/Analysis/Calculus/FDeriv/Symmetric.lean,Mathlib/Analysis/Calculus/ImplicitContDiff.lean,Mathlib/Analysis/Calculus/IteratedDeriv/Defs.lean,Mathlib/Analysis/Calculus/VectorField.lean,Mathlib/Analysis/Distribution/ContDiffMapSupportedIn.lean,Mathlib/Analysis/SpecialFunctions/Log/Deriv.lean,Mathlib/Analysis/SpecialFunctions/Trigonometric/InverseDeriv.lean,Mathlib/Geometry/Manifold/Algebra/LieGroup.lean,Mathlib/Geometry/Manifold/Algebra/Monoid.lean,Mathlib/Geometry/Manifold/Algebra/SmoothFunctions.lean,Mathlib/Geometry/Manifold/Algebra/Structures.lean,Mathlib/Geometry/Manifold/ContMDiff/Atlas.lean,Mathlib/Geometry/Manifold/ContMDiff/Basic.lean,Mathlib/Geometry/Manifold/ContMDiff/Defs.lean,Mathlib/Geometry/Manifold/Instances/Sphere.lean,Mathlib/Geometry/Manifold/Instances/UnitsOfNormedAlgebra.lean,Mathlib/Geometry/Manifold/IsManifold/Basic.lean,Mathlib/Geometry/Manifold/VectorBundle/Basic.lean,Mathlib/Geometry/Manifold/VectorBundle/FiberwiseLinear.lean |
28 |
4 |
['github-actions', 'j-loreaux', 'mathlib-merge-conflicts', 'peabrainiac'] |
sgouezel assignee:sgouezel |
10-16250 10 days ago |
14-2510 14 days ago |
8-4053 8 days |
| 30750 |
SnirBroshi author:SnirBroshi |
feat(Data/Quot): `toSet` and `equivClassOf` |
Define `toSet` which gets the set corresponding to an element of a quotient, and `equivClassOf` which gets the equivalence class of an element under a quotient.
---
I found these definitions helpful when working with quotients, specifically `ConnectedComponents` of a `TopologicalSpace`.
[](https://gitpod.io/from-referrer/)
|
t-data
awaiting-author
awaiting-zulip
merge-conflict
|
162/0 |
Mathlib/Data/Quot.lean,Mathlib/Data/Set/Image.lean,Mathlib/Data/SetLike/Basic.lean,Mathlib/Data/Setoid/Basic.lean |
4 |
5 |
['SnirBroshi', 'TwoFX', 'eric-wieser', 'github-actions', 'mathlib-merge-conflicts'] |
TwoFX assignee:TwoFX |
6-74079 6 days ago |
89-54271 89 days ago |
35-75966 35 days |
| 33441 |
dupuisf author:dupuisf |
feat: add `LawfulInv` class for types with an inverse that behaves like `Ring.inverse` |
This PR introduces a new typeclass `LawfulInv` for types which have an `Inv` instance that is equal to zero on non-invertible elements. This is meant to replace `Ring.inverse`. The current plan is to do this refactor in several steps:
1. This PR, which only introduces the class and adds instances for matrices and continuous linear maps.
2. Add instances for all C*-algebras, and make `CStarAlgebra` extend this.
3. Deprecate `Ring.inverse`.
---
[](https://gitpod.io/from-referrer/)
|
awaiting-zulip
t-algebra
merge-conflict
label:t-algebra$ |
185/27 |
Mathlib/Algebra/GroupWithZero/Defs.lean,Mathlib/Algebra/GroupWithZero/Invertible.lean,Mathlib/Algebra/GroupWithZero/Units/Basic.lean,Mathlib/LinearAlgebra/Matrix/NonsingularInverse.lean,Mathlib/LinearAlgebra/Matrix/PosDef.lean,Mathlib/RingTheory/DividedPowers/Padic.lean,Mathlib/Topology/Algebra/Module/Equiv.lean |
7 |
35 |
['dupuisf', 'eric-wieser', 'github-actions', 'j-loreaux', 'mathlib-merge-conflicts', 'mathlib4-merge-conflict-bot', 'plp127'] |
nobody |
6-61919 6 days ago |
35-8654 35 days ago |
7-22559 7 days |
| 34245 |
staroperator author:staroperator |
feat(Data/Set): add `Set.Uncountable` |
There are `Set` specialized shortcuts `Set.Finite`, `Set.Infinite` and `Set.Countable`, but lacking `Set.Uncountable`. I find this useful in #34246.
---
[](https://gitpod.io/from-referrer/)
|
t-data
awaiting-zulip
|
82/4 |
Mathlib/Analysis/Real/Cardinality.lean,Mathlib/Data/Set/Countable.lean,Mathlib/SetTheory/Cardinal/Basic.lean |
3 |
16 |
['github-actions', 'joneugster', 'staroperator', 'vihdzp'] |
joneugster assignee:joneugster |
6-57585 6 days ago |
21-20191 21 days ago |
12-11217 12 days |
| 34077 |
kbuzzard author:kbuzzard |
perf: increase priority of instSMulOfMul |
#31040 deprecated `Mul.toSMul` in place of the core instance `instSMulOfMul`, which is at a lowered priority of 910. This PR undeprecates it and makes it a higher priority instance (1100) which seems better for mathlib.
---
[](https://gitpod.io/from-referrer/)
This PR follows the philosophy seen in Mathlib's `Algebra.id : Algebra R R`, which also has raised priority. The idea is the same as `Algebra.id`: if you're looking for an instance of `Algebra R S` with R not equal to S then `Algebra.id` is extremely likely to fail quickly in practice, and if you're looking for an instance of `Algebra R R` then `Algebra.id` is unambiguously the right answer so should be tried ASAP. However the instance is defined so early in mathlib that in in practice it is tried last unless the priority is raised. The same philosophy holds here; if you're looking for an instance of `SMul X X` then you absolutely want to try `Mul.toSMul` first and if you're looking for an instance of `SMul X Y` with Y not X then `Mul.toSMul` will in practice be quick to fail.
This PR was inspired by #33908 (another "this should be quick to fail and if it fits then it's almost certainly what we want" prio change) which made an instance of `IsScalarTower R A A` high priority and gave a performance boost. This PR also gives a performance boost.
Note that the performance in #31040 looks very bad but the radar output is incorrect; there was a hardware change between the two runs. In fact #31040 produced no changes in profiling, as one might expect.
I don't know the correct way to change the priority of a core instance in mathlib, and I didn't know if just changing the priority naively would work repo-wide rather than just file-wide, which was why this PR introduces a second instance.
Zulip discussion at [#mathlib4 > priority hacks](https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/priority.20hacks/with/574353616)
|
t-algebra
awaiting-zulip
label:t-algebra$ |
3/9 |
Mathlib/Algebra/Group/Action/Defs.lean,Mathlib/Algebra/Group/Action/Units.lean |
2 |
25 |
['alreadydone', 'github-actions', 'kbuzzard', 'leanprover-radar'] |
jcommelin assignee:jcommelin |
6-55670 6 days ago |
6-55670 6 days ago |
0-51849 14 hours |
| 26299 |
adomani author:adomani |
perf: the `whitespace` linter only acts on modified files |
Introduces an `IO.Ref` to allow the `commandStart` linter to only run on files that git considers modified with respect to `master`.
The linter is also active on files that have had some error, as these are likely being modified!
The PR should also mitigate the speed-up that the linter introduced:
[#mathlib4 > A whitespace linter @ 💬](https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/A.20whitespace.20linter/near/525091877)
Assuming that this goes well, a similar mechanism could be applied to several linters that do not need to run on all code, just on the modified code.
Implementation detail: the linter is currently either on or off in "whole" files. It may be also a future development to make this more granular and only run the linter on "modifed commands in modified files", but this is not currently the plan for this modification!
---
[](https://gitpod.io/from-referrer/)
|
t-linter
awaiting-zulip
awaiting-author
|
55/7 |
Mathlib/Tactic/Linter/Whitespace.lean |
1 |
19 |
['adomani', 'eric-wieser', 'github-actions', 'grunweg', 'joneugster', 'kim-em', 'leanprover-bot', 'leanprover-radar', 'mathlib-bors', 'mathlib4-merge-conflict-bot'] |
grunweg assignee:grunweg |
6-54345 6 days ago |
179-50663 179 days ago |
66-67660 66 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
|
23/2 |
Mathlib/Tactic/Linter/TextBased.lean |
1 |
4 |
['github-actions', 'grunweg', 'joneugster', 'vihdzp'] |
nobody |
4-24964 4 days ago |
unknown |
unknown |
| 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
|
10/10 |
Mathlib/Control/Monad/Cont.lean,Mathlib/Control/Monad/Writer.lean |
2 |
4 |
['Shreyas4991', 'eric-wieser', 'github-actions'] |
nobody |
4-3478 4 days ago |
4-3479 4 days ago |
0-18022 5 hours |
| 33972 |
YuvalFilmus author:YuvalFilmus |
feat(Analysis/Polynomial/Order): polynomial has fixed sign beyond largest root |
We prove that a polynomial has fixed sign beyond its largest root.
One could also prove similar results about the smallest root, but they will be more awkward since they will depend on the parity of the (natural) degree; suggestions welcome (perhaps for a future PR).
---
[](https://gitpod.io/from-referrer/)
|
t-analysis
awaiting-zulip
|
134/0 |
Mathlib.lean,Mathlib/Analysis/Polynomial/Order.lean |
2 |
13 |
['YuvalFilmus', 'artie2000', 'github-actions', 'mathlib-merge-conflicts', 'urkud', 'vihdzp'] |
ADedecker and urkud assignee:urkud assignee:ADedecker |
1-22124 1 day ago |
1-24110 1 day ago |
38-83172 38 days |