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 |
32-43358 1 month ago |
32-43358 32 days ago |
1-44258 1 day |
| 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
|
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 |
19-4072 19 days ago |
19-18674 19 days ago |
59-48116 59 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
maintainer-merge
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 |
14-26884 14 days ago |
14-26884 14 days ago |
12-11217 12 days |
| 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 |
12-26792 12 days ago |
12-26796 12 days ago |
15-70912 15 days |
| 32367 |
BoltonBailey author:BoltonBailey |
feat(Computability): add FinEncodings for List Bool and pairs of types |
This PR contains `finEncoding`s relevant to developing complexity theory in downstream libraries. It is adapted from [this](https://leanprover.zulipchat.com/#narrow/channel/116395-maths/topic/Formalise.20the.20proposition.20P.20.E2.89.A0NP/near/451765788)[#maths > Formalise the proposition P ≠NP @ 💬](https://leanprover.zulipchat.com/#narrow/channel/116395-maths/topic/Formalise.20the.20proposition.20P.20.E2.89.A0NP/near/451765788) comment.
Co-authored-by: Daniel Weber
---
[](https://gitpod.io/from-referrer/)
|
maintainer-merge
t-computability
|
54/21 |
Mathlib/Computability/Encoding.lean,Mathlib/Data/List/Basic.lean |
2 |
15 |
['BoltonBailey', 'MichaelStollBayreuth', 'Vierkantor', 'YaelDillies', 'github-actions'] |
Vierkantor and YaelDillies assignee:Vierkantor assignee:YaelDillies |
8-25104 8 days ago |
12-16869 12 days ago |
75-72128 75 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 |
7-40269 7 days ago |
7-40269 7 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 |
6-48620 6 days ago |
6-48620 6 days ago |
22-14837 22 days |
| 34783 |
Jun2M author:Jun2M |
feat(Combinatorics/Graph): add Compatible definition and API |
Preliminary PR for #26770 (subgraph). Adds the `Compatible` predicate and basic API to `Mathlib.Combinatorics.Graph.Basic`.
- **Compatible**: two graphs are compatible if they agree on incidence for every edge in the intersection of their edge sets.
- Includes `Compatible.isLink_iff`, reflexivity/symmetry instances, `IsLink.of_compatible`, `Compatible.of_disjoint_edgeSet`, and the `Inc`/`IsLoopAt`/`IsNonloopAt` variants.
- **copy** API for copying a graph with new vertex/edge sets and `IsLink`.
---
[](https://gitpod.io/from-referrer/)
|
t-combinatorics
maintainer-merge
|
101/1 |
Mathlib/Combinatorics/Graph/Basic.lean |
1 |
10 |
['Jun2M', 'YaelDillies', 'eric-wieser', 'github-actions'] |
kmill assignee:kmill |
5-86032 5 days ago |
14-16402 14 days ago |
14-20195 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 |
9 |
['bwangpj', 'dagurtomas', 'eric-wieser', 'github-actions'] |
dagurtomas assignee:dagurtomas |
5-26208 5 days ago |
27-54453 27 days ago |
27-56541 27 days |
| 34915 |
smmercuri author:smmercuri |
feat(Topology/Algebra/RestrictedProduct): the units of a restricted product are isomorphic to the restricted product of the units |
---
[](https://gitpod.io/from-referrer/)
|
t-topology
FLT
maintainer-merge
|
94/0 |
Mathlib.lean,Mathlib/Topology/Algebra/RestrictedProduct/Units.lean |
2 |
5 |
['dagurtomas', 'github-actions', 'smmercuri'] |
dagurtomas assignee:dagurtomas |
4-51073 4 days ago |
4-50248 4 days ago |
11-32598 11 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
|
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 |
21 |
['github-actions', 'grunweg', 'joneugster'] |
joneugster assignee:joneugster |
4-48611 4 days ago |
11-31863 11 days ago |
13-34023 13 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'] |
nobody |
3-27886 3 days ago |
3-35247 3 days ago |
6-30911 6 days |
| 32440 |
thorimur author:thorimur |
feat: make the `unusedInstancesInType` linters fire when instances are not used outside of proofs in the type |
This PR adjusts the `unusedDecidableInType` to prevent false negatives on declarations that only use `Decidable*` hypotheses in proofs that appear in the type. That is, the linter now fires when the `Decidable*` linter is unused outside of proofs.
This PR also changes the warning message to be more direct, and indicates when the instance appears only in a proof (vs. not appearing at all).
We exempt some deprecated lemmas in `Mathlib.Analysis.Order.Matrix` which the linter now fires on. (Presumably, most prior violations had been cleaned up by #10235, which also detected such lemmas.)
Note that this took some tinkering to achieve sufficient performance. We use the following novel(?) "dolorous telescope" strategy (so named due to introducing `sorry`s) to avoid traversing the whole type:
- when encountering an instance binder of concern, telescope to create an fvar.
- when encountering any other binder, instantiate it with `sorry`.
- as we proceed, collect the free variables from these expressions which do not appear in proofs. Since the instances of concern are the only free variables, free variable collection avoids traversing many subexpressions by checking for `hasFVar`, which is a computed field accessible in constant time.
Perhaps surprisingly, this is (on net) more performant than using `eraseProofs` and then detecting dependence via bvars.
We also implement an `Expr`-level early exit for most types by checking if they bind any instance of concern first. (This adds a very small overhead to types which *do* have an instance of concern, but the check is very fast.)
This also adds a profiler category to this linter.
Note: we still have yet to optimize (pre)-infotree traversal performance, and have yet to avoid proofs that appear in the value of definitions. However, this PR sets us up to do so.
---
- [x] depends on: #35102
---
## Notes on performance
You might be wondering if this *is* actually a faster strategy, seeing as the bench is quite noisy. To determine this, I made a copy of the linter which I could vary without rebuilding mathlib, and profiled the relevant component locally on all imported declarations in Mathlib by linting the `eoi` token:
```lean
module
public meta import Lean
public import Mathlib.Tactic.Linter.UnusedInstancesInTypeCopy
import all Mathlib.Tactic.Linter.UnusedInstancesInTypeCopy
open Lean Meta Elab Term Command Mathlib.Linter.UnusedInstancesInType
meta section
local instance : Insert Name NameSet where
insert := fun n s => s.insert n
def runCopy : Linter where run stx := do
if stx.isOfKind ``Parser.Command.eoi then
let opts := (← getOptions).setBool `profiler true
let consts := (← getEnv).constants.map₁
-- The following expose private decls in their types, so break `MetaM` methods:
let badRecs : NameSet := {`IO.Promise.casesOn, `IO.Promise.recOn, `IO.Promise.rec}
profileitM Exception "control" opts do
for (n,_) in consts do
liftTermElabM do unless n.isInternalDetail || badRecs.contains n do pure ()
profileitM Exception "bench" opts do
for (n,cinfo) in consts do
unless n.isInternalDetail || badRecs.contains n do
cinfo.toConstantVal.onUnusedInstancesInTypeWhere isDecidableVariant
fun _ _ => pure ()
initialize addLinter runCopy
```
(This could have been done in a `run_cmd`, but I wanted to replicate the circumstances of linting as closely as possible, just in case it introduced mysterious async effects.)
Then, in a separate file, I imported `Mathlib` and the above linter, and cycled through reading out the result and editing the underlying component then rebuilding. The control was reliably ~1.07-1.12s. The different strategies came out as follows (the following values are not averaged, but are representative):
| | without early exit | with early exit |
| ---: | :---: | :---: |
| `eraseProofs` | 97.4s | 6.82s |
| dolorous telescope | 20.3s | 3.99s |
As you can see, the early exit cuts the absolute value (and therefore the absolute difference) down dramatically. But seeing as this lays the groundwork for linting defs and will be used for more linters (with wider scopes, and less early exit opportunities), I think we should opt for the more performant version even though there's some extra complexity. :)
[](https://gitpod.io/from-referrer/)
|
t-linter
maintainer-merge
|
233/62 |
Mathlib/Analysis/Matrix/Order.lean,Mathlib/Lean/Expr/Basic.lean,Mathlib/Tactic/Linter/UnusedInstancesInType.lean,MathlibTest/UnusedInstancesInType/Basic.lean,MathlibTest/UnusedInstancesInType/Decidable.lean,MathlibTest/UnusedInstancesInType/Fintype.lean,MathlibTest/UnusedInstancesInType/FintypeNeedingImport.lean,MathlibTest/UnusedInstancesInType/SetOption.lean |
8 |
39 |
['github-actions', 'grunweg', 'joneugster', 'leanprover-radar', 'mathlib-dependent-issues', 'mathlib4-merge-conflict-bot', 'thorimur'] |
joneugster assignee:joneugster |
3-23218 3 days ago |
3-20175 3 days ago |
38-80497 38 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
|
117/5 |
Mathlib/Geometry/Polygon/Basic.lean |
1 |
18 |
['A-M-Berns', 'eric-wieser', 'github-actions', 'jcommelin', 'jsm28'] |
jsm28 assignee:jsm28 |
3-18439 3 days ago |
4-21542 4 days ago |
17-26395 17 days |
| 35187 |
bilichboris author:bilichboris |
feat(GroupTheory): establish that every finite left cancellative monoid is a group |
This PR closes a todo in the GroupTheory module.
---
[](https://gitpod.io/from-referrer/)
|
t-group-theory
new-contributor
maintainer-merge
|
8/1 |
Mathlib/GroupTheory/OrderOfElement.lean |
1 |
8 |
['bilichboris', 'github-actions', 'riccardobrasca', 'robin-carlier'] |
nobody |
2-40512 2 days ago |
4-38480 4 days ago |
5-23245 5 days |
| 35044 |
b-mehta author:b-mehta |
feat(RingTheory/Radical): positivity extension for radical of natural |
A follow-up from #25335 which I forgot to make at the time.
---
[](https://gitpod.io/from-referrer/)
|
t-ring-theory
maintainer-merge
|
20/0 |
Mathlib/RingTheory/Radical.lean |
1 |
4 |
['b-mehta', 'chrisflav', 'github-actions'] |
chrisflav assignee:chrisflav |
1-21118 1 day ago |
8-19293 8 days ago |
8-19024 8 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 |
| 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 |
32-43358 1 month ago |
32-43358 32 days ago |
1-44258 1 day |
| 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
|
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 |
19-4072 19 days ago |
19-18674 19 days ago |
59-48116 59 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
maintainer-merge
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 |
14-26884 14 days ago |
14-26884 14 days ago |
12-11217 12 days |
| 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 |
12-26792 12 days ago |
12-26796 12 days ago |
15-70912 15 days |
| 32367 |
BoltonBailey author:BoltonBailey |
feat(Computability): add FinEncodings for List Bool and pairs of types |
This PR contains `finEncoding`s relevant to developing complexity theory in downstream libraries. It is adapted from [this](https://leanprover.zulipchat.com/#narrow/channel/116395-maths/topic/Formalise.20the.20proposition.20P.20.E2.89.A0NP/near/451765788)[#maths > Formalise the proposition P ≠NP @ 💬](https://leanprover.zulipchat.com/#narrow/channel/116395-maths/topic/Formalise.20the.20proposition.20P.20.E2.89.A0NP/near/451765788) comment.
Co-authored-by: Daniel Weber
---
[](https://gitpod.io/from-referrer/)
|
maintainer-merge
t-computability
|
54/21 |
Mathlib/Computability/Encoding.lean,Mathlib/Data/List/Basic.lean |
2 |
15 |
['BoltonBailey', 'MichaelStollBayreuth', 'Vierkantor', 'YaelDillies', 'github-actions'] |
Vierkantor and YaelDillies assignee:Vierkantor assignee:YaelDillies |
8-25104 8 days ago |
12-16869 12 days ago |
75-72128 75 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 |
7-40269 7 days ago |
7-40269 7 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 |
6-48620 6 days ago |
6-48620 6 days ago |
22-14837 22 days |
| 34783 |
Jun2M author:Jun2M |
feat(Combinatorics/Graph): add Compatible definition and API |
Preliminary PR for #26770 (subgraph). Adds the `Compatible` predicate and basic API to `Mathlib.Combinatorics.Graph.Basic`.
- **Compatible**: two graphs are compatible if they agree on incidence for every edge in the intersection of their edge sets.
- Includes `Compatible.isLink_iff`, reflexivity/symmetry instances, `IsLink.of_compatible`, `Compatible.of_disjoint_edgeSet`, and the `Inc`/`IsLoopAt`/`IsNonloopAt` variants.
- **copy** API for copying a graph with new vertex/edge sets and `IsLink`.
---
[](https://gitpod.io/from-referrer/)
|
t-combinatorics
maintainer-merge
|
101/1 |
Mathlib/Combinatorics/Graph/Basic.lean |
1 |
10 |
['Jun2M', 'YaelDillies', 'eric-wieser', 'github-actions'] |
kmill assignee:kmill |
5-86032 5 days ago |
14-16402 14 days ago |
14-20195 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 |
9 |
['bwangpj', 'dagurtomas', 'eric-wieser', 'github-actions'] |
dagurtomas assignee:dagurtomas |
5-26208 5 days ago |
27-54453 27 days ago |
27-56541 27 days |
| 34915 |
smmercuri author:smmercuri |
feat(Topology/Algebra/RestrictedProduct): the units of a restricted product are isomorphic to the restricted product of the units |
---
[](https://gitpod.io/from-referrer/)
|
t-topology
FLT
maintainer-merge
|
94/0 |
Mathlib.lean,Mathlib/Topology/Algebra/RestrictedProduct/Units.lean |
2 |
5 |
['dagurtomas', 'github-actions', 'smmercuri'] |
dagurtomas assignee:dagurtomas |
4-51073 4 days ago |
4-50248 4 days ago |
11-32598 11 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
|
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 |
21 |
['github-actions', 'grunweg', 'joneugster'] |
joneugster assignee:joneugster |
4-48611 4 days ago |
11-31863 11 days ago |
13-34023 13 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'] |
nobody |
3-27886 3 days ago |
3-35247 3 days ago |
6-30911 6 days |
| 32440 |
thorimur author:thorimur |
feat: make the `unusedInstancesInType` linters fire when instances are not used outside of proofs in the type |
This PR adjusts the `unusedDecidableInType` to prevent false negatives on declarations that only use `Decidable*` hypotheses in proofs that appear in the type. That is, the linter now fires when the `Decidable*` linter is unused outside of proofs.
This PR also changes the warning message to be more direct, and indicates when the instance appears only in a proof (vs. not appearing at all).
We exempt some deprecated lemmas in `Mathlib.Analysis.Order.Matrix` which the linter now fires on. (Presumably, most prior violations had been cleaned up by #10235, which also detected such lemmas.)
Note that this took some tinkering to achieve sufficient performance. We use the following novel(?) "dolorous telescope" strategy (so named due to introducing `sorry`s) to avoid traversing the whole type:
- when encountering an instance binder of concern, telescope to create an fvar.
- when encountering any other binder, instantiate it with `sorry`.
- as we proceed, collect the free variables from these expressions which do not appear in proofs. Since the instances of concern are the only free variables, free variable collection avoids traversing many subexpressions by checking for `hasFVar`, which is a computed field accessible in constant time.
Perhaps surprisingly, this is (on net) more performant than using `eraseProofs` and then detecting dependence via bvars.
We also implement an `Expr`-level early exit for most types by checking if they bind any instance of concern first. (This adds a very small overhead to types which *do* have an instance of concern, but the check is very fast.)
This also adds a profiler category to this linter.
Note: we still have yet to optimize (pre)-infotree traversal performance, and have yet to avoid proofs that appear in the value of definitions. However, this PR sets us up to do so.
---
- [x] depends on: #35102
---
## Notes on performance
You might be wondering if this *is* actually a faster strategy, seeing as the bench is quite noisy. To determine this, I made a copy of the linter which I could vary without rebuilding mathlib, and profiled the relevant component locally on all imported declarations in Mathlib by linting the `eoi` token:
```lean
module
public meta import Lean
public import Mathlib.Tactic.Linter.UnusedInstancesInTypeCopy
import all Mathlib.Tactic.Linter.UnusedInstancesInTypeCopy
open Lean Meta Elab Term Command Mathlib.Linter.UnusedInstancesInType
meta section
local instance : Insert Name NameSet where
insert := fun n s => s.insert n
def runCopy : Linter where run stx := do
if stx.isOfKind ``Parser.Command.eoi then
let opts := (← getOptions).setBool `profiler true
let consts := (← getEnv).constants.map₁
-- The following expose private decls in their types, so break `MetaM` methods:
let badRecs : NameSet := {`IO.Promise.casesOn, `IO.Promise.recOn, `IO.Promise.rec}
profileitM Exception "control" opts do
for (n,_) in consts do
liftTermElabM do unless n.isInternalDetail || badRecs.contains n do pure ()
profileitM Exception "bench" opts do
for (n,cinfo) in consts do
unless n.isInternalDetail || badRecs.contains n do
cinfo.toConstantVal.onUnusedInstancesInTypeWhere isDecidableVariant
fun _ _ => pure ()
initialize addLinter runCopy
```
(This could have been done in a `run_cmd`, but I wanted to replicate the circumstances of linting as closely as possible, just in case it introduced mysterious async effects.)
Then, in a separate file, I imported `Mathlib` and the above linter, and cycled through reading out the result and editing the underlying component then rebuilding. The control was reliably ~1.07-1.12s. The different strategies came out as follows (the following values are not averaged, but are representative):
| | without early exit | with early exit |
| ---: | :---: | :---: |
| `eraseProofs` | 97.4s | 6.82s |
| dolorous telescope | 20.3s | 3.99s |
As you can see, the early exit cuts the absolute value (and therefore the absolute difference) down dramatically. But seeing as this lays the groundwork for linting defs and will be used for more linters (with wider scopes, and less early exit opportunities), I think we should opt for the more performant version even though there's some extra complexity. :)
[](https://gitpod.io/from-referrer/)
|
t-linter
maintainer-merge
|
233/62 |
Mathlib/Analysis/Matrix/Order.lean,Mathlib/Lean/Expr/Basic.lean,Mathlib/Tactic/Linter/UnusedInstancesInType.lean,MathlibTest/UnusedInstancesInType/Basic.lean,MathlibTest/UnusedInstancesInType/Decidable.lean,MathlibTest/UnusedInstancesInType/Fintype.lean,MathlibTest/UnusedInstancesInType/FintypeNeedingImport.lean,MathlibTest/UnusedInstancesInType/SetOption.lean |
8 |
39 |
['github-actions', 'grunweg', 'joneugster', 'leanprover-radar', 'mathlib-dependent-issues', 'mathlib4-merge-conflict-bot', 'thorimur'] |
joneugster assignee:joneugster |
3-23218 3 days ago |
3-20175 3 days ago |
38-80497 38 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
|
117/5 |
Mathlib/Geometry/Polygon/Basic.lean |
1 |
18 |
['A-M-Berns', 'eric-wieser', 'github-actions', 'jcommelin', 'jsm28'] |
jsm28 assignee:jsm28 |
3-18439 3 days ago |
4-21542 4 days ago |
17-26395 17 days |
| 35187 |
bilichboris author:bilichboris |
feat(GroupTheory): establish that every finite left cancellative monoid is a group |
This PR closes a todo in the GroupTheory module.
---
[](https://gitpod.io/from-referrer/)
|
t-group-theory
new-contributor
maintainer-merge
|
8/1 |
Mathlib/GroupTheory/OrderOfElement.lean |
1 |
8 |
['bilichboris', 'github-actions', 'riccardobrasca', 'robin-carlier'] |
nobody |
2-40512 2 days ago |
4-38480 4 days ago |
5-23245 5 days |
| 35044 |
b-mehta author:b-mehta |
feat(RingTheory/Radical): positivity extension for radical of natural |
A follow-up from #25335 which I forgot to make at the time.
---
[](https://gitpod.io/from-referrer/)
|
t-ring-theory
maintainer-merge
|
20/0 |
Mathlib/RingTheory/Radical.lean |
1 |
4 |
['b-mehta', 'chrisflav', 'github-actions'] |
chrisflav assignee:chrisflav |
1-21118 1 day ago |
8-19293 8 days ago |
8-19024 8 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
|
51/3 |
Mathlib/CategoryTheory/Galois/EssSurj.lean,Mathlib/CategoryTheory/Triangulated/TStructure/TruncLTGE.lean,Mathlib/Tactic/Simps/Basic.lean,MathlibTest/SimpsModule.lean |
4 |
11 |
['JovanGerb', 'github-actions', 'joneugster', 'kim-em'] |
joneugster assignee:joneugster |
0-81924 22 hours ago |
25-47322 25 days ago |
37-2239 37 days |
| 34699 |
tb65536 author:tb65536 |
feat(RingTheory/Lasker): prove first uniqueness theorem for primary decomposition |
This PR proves the first uniqueness theorem for primary decomposition: In any minimal primary decomposition `I = ⨅ i, q_i`, the ideals `√(q_i : M)` are exactly the associated primes of `I`.
---
[](https://gitpod.io/from-referrer/)
|
t-ring-theory
t-algebra
maintainer-merge
label:t-algebra$ |
38/6 |
Mathlib/RingTheory/IsPrimary.lean,Mathlib/RingTheory/Lasker.lean |
2 |
10 |
['erdOne', 'github-actions', 'mariainesdff', 'tb65536'] |
mariainesdff assignee:mariainesdff |
0-53991 14 hours ago |
0-53236 14 hours ago |
16-5711 16 days |
| 34400 |
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):
* `SubMulAction.ofStabilizer.isMultiplyPretransitive`: 207 ms before, 232 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/)
|
t-group-theory
maintainer-merge
|
4/14 |
Mathlib/GroupTheory/GroupAction/Defs.lean,Mathlib/GroupTheory/GroupAction/MultipleTransitivity.lean |
2 |
8 |
['euprunin', 'github-actions', 'leanprover-radar', 'mattrobball', 'tb65536', 'vihdzp'] |
mattrobball assignee:mattrobball |
0-52633 14 hours ago |
6-15577 6 days ago |
20-24641 20 days |
| 27100 |
staroperator author:staroperator |
feat(ModelTheory): Presburger definability and semilinear sets |
This PR formalizes the classical result that Presburger definable sets are the same as semilinear sets. As an application of this result, we show that the graph of multiplication is not Presburger definable.
---
- [x] depends on: #26896
- [x] depends on: #27081
- [x] depends on: #27087
- [x] depends on: #27414
- [x] depends on: #32123
---
[](https://gitpod.io/from-referrer/)
|
t-logic
large-import
maintainer-merge
|
278/0 |
Mathlib.lean,Mathlib/ModelTheory/Arithmetic/Presburger/Definability.lean,Mathlib/ModelTheory/Arithmetic/Presburger/Semilinear/Defs.lean,docs/references.bib |
4 |
10 |
['awainverse', 'github-actions', 'leanprover-community-bot-assistant', 'mathlib4-dependent-issues-bot', 'mathlib4-merge-conflict-bot', 'staroperator'] |
fpvandoorn assignee:fpvandoorn |
0-38037 10 hours ago |
19-20936 19 days ago |
80-69020 80 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 |
0-34242 9 hours ago |
23-36580 23 days ago |
63-10530 63 days |
| 33909 |
YaelDillies author:YaelDillies |
feat(SetTheory/Cardinal): more lemmas about `ENat` |
and deduplicate a few pairs.
From ProofBench
---
[](https://gitpod.io/from-referrer/)
|
t-set-theory
maintainer-merge
|
81/49 |
Mathlib/Data/Finite/Card.lean,Mathlib/Data/Set/Card.lean,Mathlib/GroupTheory/CoprodI.lean,Mathlib/LinearAlgebra/Matrix/Rank.lean,Mathlib/RingTheory/Length.lean,Mathlib/SetTheory/Cardinal/Basic.lean,Mathlib/SetTheory/Cardinal/ENat.lean,Mathlib/SetTheory/Cardinal/Finite.lean,Mathlib/SetTheory/Cardinal/NatCount.lean,Mathlib/SetTheory/Cardinal/ToNat.lean |
10 |
5 |
['github-actions', 'mathlib4-merge-conflict-bot', 'tb65536', 'vihdzp'] |
alreadydone assignee:alreadydone |
0-29770 8 hours ago |
0-27634 7 hours ago |
30-22468 30 days |
| 35037 |
sgouezel author:sgouezel |
refactor: change definition of distance in normed group |
The current definition of the distance in a normed group is `dist x y = ||x / y||`. With this definition, the distance is right-invariant. This does not correspond to the convention in geometric group theory where the distance is given by `||x^{-1} * y||` to make sure it is left-invariant -- this corresponds to the fact that, in a Cayley graph, we put an edge between `x` and `xs` and declare these to be at distance one.
We refactor the definition to make sure it follows the standard convention. A pain point is that, in additive commutative groups, which is arguably the most important case, it becomes `||-x + y||` instead of `||x - y||` (which is propositionally the same, but not definitionally). To minimize the hassle, we keep all the lemmas that use `||x - y||`, with their current names, and add new versions in terms of `||-x + y||` when useful.
---
- [x] depends on: #35252
- [x] depends on: #35384
[](https://gitpod.io/from-referrer/)
|
t-analysis
maintainer-merge
|
705/444 |
Mathlib/Algebra/Order/Hom/Basic.lean,Mathlib/Analysis/Asymptotics/Lemmas.lean,Mathlib/Analysis/CStarAlgebra/lpSpace.lean,Mathlib/Analysis/Calculus/BumpFunction/Normed.lean,Mathlib/Analysis/Calculus/FDeriv/Extend.lean,Mathlib/Analysis/Calculus/UniformLimitsDeriv.lean,Mathlib/Analysis/Complex/AbsMax.lean,Mathlib/Analysis/Complex/Basic.lean,Mathlib/Analysis/Complex/Liouville.lean,Mathlib/Analysis/Complex/LocallyUniformLimit.lean,Mathlib/Analysis/Complex/Norm.lean,Mathlib/Analysis/Complex/OpenMapping.lean,Mathlib/Analysis/Complex/Schwarz.lean,Mathlib/Analysis/Complex/TaylorSeries.lean,Mathlib/Analysis/Complex/UpperHalfPlane/Metric.lean,Mathlib/Analysis/Fourier/RiemannLebesgueLemma.lean,Mathlib/Analysis/InnerProductSpace/Subspace.lean,Mathlib/Analysis/LocallyConvex/BalancedCoreHull.lean,Mathlib/Analysis/LocallyConvex/WithSeminorms.lean,Mathlib/Analysis/Normed/Algebra/UnitizationL1.lean,Mathlib/Analysis/Normed/Field/Basic.lean,Mathlib/Analysis/Normed/Field/Lemmas.lean,Mathlib/Analysis/Normed/Group/Basic.lean,Mathlib/Analysis/Normed/Group/Bounded.lean,Mathlib/Analysis/Normed/Group/Completion.lean,Mathlib/Analysis/Normed/Group/Constructions.lean,Mathlib/Analysis/Normed/Group/Continuity.lean,Mathlib/Analysis/Normed/Group/ControlledClosure.lean,Mathlib/Analysis/Normed/Group/Defs.lean,Mathlib/Analysis/Normed/Group/Int.lean,Mathlib/Analysis/Normed/Group/Pointwise.lean,Mathlib/Analysis/Normed/Group/Quotient.lean,Mathlib/Analysis/Normed/Group/Rat.lean,Mathlib/Analysis/Normed/Group/Real.lean,Mathlib/Analysis/Normed/Group/Ultra.lean,Mathlib/Analysis/Normed/Group/Uniform.lean,Mathlib/Analysis/Normed/Lp/PiLp.lean,Mathlib/Analysis/Normed/Lp/ProdLp.lean,Mathlib/Analysis/Normed/Lp/lpSpace.lean,Mathlib/Analysis/Normed/Module/Basic.lean,Mathlib/Analysis/Normed/Module/FiniteDimension.lean,Mathlib/Analysis/Normed/Module/Multilinear/Basic.lean,Mathlib/Analysis/Normed/MulAction.lean,Mathlib/Analysis/Normed/Operator/Basic.lean,Mathlib/Analysis/Normed/Operator/Completeness.lean,Mathlib/Analysis/Normed/Order/Hom/Basic.lean,Mathlib/Analysis/Normed/Order/Hom/Ultra.lean,Mathlib/Analysis/Normed/Ring/Basic.lean,Mathlib/Analysis/Normed/Unbundled/SpectralNorm.lean,Mathlib/Analysis/Seminorm.lean,Mathlib/Analysis/SpecialFunctions/Elliptic/Weierstrass.lean,Mathlib/Analysis/SpecialFunctions/Exp.lean,Mathlib/InformationTheory/Hamming.lean,Mathlib/MeasureTheory/Function/ConvergenceInMeasure.lean,Mathlib/MeasureTheory/Function/LpSpace/Basic.lean,Mathlib/MeasureTheory/Function/LpSpace/DomAct/Basic.lean,Mathlib/MeasureTheory/Integral/CircleIntegral.lean,Mathlib/MeasureTheory/Integral/CircleTransform.lean,Mathlib/MeasureTheory/Integral/CurveIntegral/Basic.lean,Mathlib/MeasureTheory/Measure/Haar/NormedSpace.lean,Mathlib/NumberTheory/NumberField/CanonicalEmbedding/ConvexBody.lean,Mathlib/NumberTheory/NumberField/InfinitePlace/Basic.lean,Mathlib/NumberTheory/Padics/MahlerBasis.lean,Mathlib/NumberTheory/Padics/PadicIntegers.lean,Mathlib/NumberTheory/Padics/PadicNumbers.lean,Mathlib/Topology/Algebra/IsUniformGroup/Basic.lean,Mathlib/Topology/Algebra/IsUniformGroup/Defs.lean,Mathlib/Topology/Algebra/Module/Multilinear/Bounded.lean,Mathlib/Topology/Algebra/Valued/NormedValued.lean,Mathlib/Topology/Algebra/Valued/ValuationTopology.lean,Mathlib/Topology/ContinuousMap/Bounded/Normed.lean,Mathlib/Topology/ContinuousMap/Compact.lean,Mathlib/Topology/MetricSpace/Kuratowski.lean,MathlibTest/hintAll.lean,scripts/nolints_prime_decls.txt |
75 |
11 |
['YaelDillies', 'github-actions', 'mathlib-dependent-issues', 'mathlib-merge-conflicts', 'sgouezel', 'themathqueen'] |
YaelDillies assignee:YaelDillies |
0-28024 7 hours ago |
0-41855 11 hours ago |
0-41600 11 hours |
| 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
|
75/79 |
Mathlib/Combinatorics/SimpleGraph/Acyclic.lean,Mathlib/Combinatorics/SimpleGraph/Connectivity/Connected.lean |
2 |
10 |
['SnirBroshi', 'b-mehta', 'github-actions', 'mathlib-merge-conflicts', 'mathlib4-dependent-issues-bot', 'mathlib4-merge-conflict-bot', 'ocfnash'] |
b-mehta assignee:b-mehta |
0-21078 5 hours ago |
3-84958 3 days ago |
69-56239 69 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 |
0-15856 4 hours ago |
0-14999 4 hours ago |
1-8267 1 day |
| 35461 |
vihdzp author:vihdzp |
chore(Order/Types/Arithmetic): golf addition/multiplication instances |
We also make the universe heterogeneous instances lower priority, so Lean can more easily elaborate universes.
---
[](https://gitpod.io/from-referrer/)
|
t-order
maintainer-merge
|
8/12 |
Mathlib/Order/Types/Arithmetic.lean |
1 |
2 |
['YaelDillies', 'github-actions'] |
nobody |
0-9656 2 hours ago |
0-8991 2 hours ago |
0-8722 2 hours |
| 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 |
454-45442 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 |
299-819 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 |
288-8719 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 |
255-18321 8 months ago |
255-18322 255 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 |
227-75468 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 |
227-74306 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 |
168-3551 5 months ago |
176-41105 176 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 |
124-67161 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 |
105-76851 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 |
96-78035 3 months ago |
136-56701 136 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 |
92-8767 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 |
91-25008 2 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 |
91-24098 2 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 |
90-62176 2 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 |
90-34042 2 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 |
69-15888 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 |
41-70601 1 month ago |
42-30934 42 days ago |
5-70690 5 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
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 |
34 |
['dupuisf', 'eric-wieser', 'github-actions', 'j-loreaux', 'mathlib4-merge-conflict-bot', 'plp127'] |
nobody |
28-14280 28 days ago |
28-15347 28 days ago |
7-54144 7 days |
| 32828 |
Hagb author:Hagb |
feat(Algebra/Order/Group/Defs): add `IsOrderedAddMonoid.toIsOrderedCancelAddMonoid'` |
It is similar to `IsOrderedAddMonoid.toIsOrderedCancelAddMonoid`, while with different hypotheses.
The conclusion `IsOrderedCancelMonoid α` on
`IsOrderedAddMonoid.toIsOrderedCancelAddMonoid` still holds when the hypothesis `CommGroup α` is weakened to `CancelCommMonoid α` while `PartialOrder α` is strengthened to `LinearOrder α`.
---
[`IsOrderedAddMonoid.toIsOrderedCancelAddMonoid`](https://leanprover-community.github.io/mathlib4_docs/find/?pattern=IsOrderedAddMonoid.toIsOrderedCancelAddMonoid#doc) and `IsOrderedAddMonoid.toIsOrderedCancelAddMonoid'`:
https://github.com/leanprover-community/mathlib4/blob/97f78b1a4311fed1844b94f1c069219a48a098e1/Mathlib/Algebra/Order/Group/Defs.lean#L52-L62
[](https://gitpod.io/from-referrer/)
|
awaiting-zulip
t-algebra
label:t-algebra$ |
4/0 |
Mathlib/Algebra/Order/Group/Defs.lean |
1 |
8 |
['Garmelon', 'Vierkantor', 'artie2000', 'github-actions', 'leanprover-radar'] |
eric-wieser assignee:eric-wieser |
26-33036 26 days ago |
26-33036 26 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 |
23-72467 23 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 |
19-37854 19 days ago |
19-37854 19 days ago |
42-19879 42 days |
| 26299 |
adomani author:adomani |
perf: the `whitespace` linter only acts on modified files |
Introduces an `IO.Ref` to allow the `commandStart` linter to only run on files that git considers modified with respect to `master`.
The linter is also active on files that have had some error, as these are likely being modified!
The PR should also mitigate the speed-up that the linter introduced:
[#mathlib4 > A whitespace linter @ 💬](https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/A.20whitespace.20linter/near/525091877)
Assuming that this goes well, a similar mechanism could be applied to several linters that do not need to run on all code, just on the modified code.
Implementation detail: the linter is currently either on or off in "whole" files. It may be also a future development to make this more granular and only run the linter on "modifed commands in modified files", but this is not currently the plan for this modification!
---
[](https://gitpod.io/from-referrer/)
|
t-linter
awaiting-zulip
|
55/7 |
Mathlib/Tactic/Linter/Whitespace.lean |
1 |
18 |
['adomani', 'eric-wieser', 'github-actions', 'grunweg', 'kim-em', 'leanprover-bot', 'leanprover-radar', 'mathlib-bors', 'mathlib4-merge-conflict-bot'] |
grunweg assignee:grunweg |
18-83964 18 days ago |
172-57356 172 days ago |
66-67660 66 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 |
16-59920 16 days ago |
16-59920 16 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 |
16-50459 16 days ago |
57-27361 57 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 |
16-50264 16 days ago |
42-34396 42 days ago |
11-6345 11 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
maintainer-merge
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 |
14-26884 14 days ago |
14-26884 14 days ago |
12-11217 12 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 |
8-9873 8 days ago |
unknown |
unknown |
| 30750 |
SnirBroshi author:SnirBroshi |
feat(Data/Quot): `toSet` and `equivClassOf` |
Define `toSet` which gets the set corresponding to an element of a quotient, and `equivClassOf` which gets the equivalence class of an element under a quotient.
---
I found these definitions helpful when working with quotients, specifically `ConnectedComponents` of a `TopologicalSpace`.
[](https://gitpod.io/from-referrer/)
|
t-data
awaiting-author
awaiting-zulip
|
162/0 |
Mathlib/Data/Quot.lean,Mathlib/Data/Set/Image.lean,Mathlib/Data/SetLike/Basic.lean,Mathlib/Data/Setoid/Basic.lean |
4 |
4 |
['SnirBroshi', 'TwoFX', 'eric-wieser', 'github-actions'] |
TwoFX assignee:TwoFX |
3-24848 3 days ago |
82-60964 82 days ago |
35-75966 35 days |
| 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 |
3-22943 3 days ago |
7-9203 7 days ago |
8-4053 8 days |