Welcome to the mathlib review page. Everybody's help with reviewing is appreciated. Reviewing contributions is important, and everybody is welcome to review pull requests! If you're not sure how, the pull request review guide is there to help you.
This page contains tables of
| 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 |
| 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 |
298/0 |
Mathlib.lean,Mathlib/ModelTheory/Arithmetic/Presburger/Definability.lean,Mathlib/ModelTheory/Arithmetic/Presburger/Semilinear/Defs.lean,docs/references.bib |
4 |
6 |
['github-actions', 'leanprover-community-bot-assistant', 'mathlib4-dependent-issues-bot', 'mathlib4-merge-conflict-bot'] |
fpvandoorn assignee:fpvandoorn |
40-59712 1 month ago |
44-8936 1 month ago |
46-9363 46 days |
| 32124 |
SnirBroshi author:SnirBroshi |
feat(SimpleGraph/Walks/Operations): expand basic drop/take/reverse API |
---
[](https://gitpod.io/from-referrer/)
|
t-combinatorics |
44/0 |
Mathlib/Combinatorics/SimpleGraph/Walks/Operations.lean |
1 |
1 |
['github-actions'] |
awainverse assignee:awainverse |
40-59702 1 month ago |
46-52012 1 month ago |
46-52056 46 days |
| 29393 |
staroperator author:staroperator |
feat(SetTheory/ZFC): `card (V_ o) = preBeth o` |
---
- [x] depends on: #26544
- [x] depends on: #29351
- [x] depends on: #29365
[](https://gitpod.io/from-referrer/)
|
t-set-theory
large-import
|
37/4 |
Mathlib/SetTheory/ZFC/Ordinal.lean,Mathlib/SetTheory/ZFC/VonNeumann.lean |
2 |
5 |
['github-actions', 'mathlib4-dependent-issues-bot', 'mathlib4-merge-conflict-bot', 'staroperator', 'vihdzp'] |
alreadydone assignee:alreadydone |
39-59698 1 month ago |
43-49777 1 month ago |
43-52402 43 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/)
|
t-computability |
58/3 |
Mathlib/Computability/Encoding.lean,Mathlib/Data/List/Basic.lean,Mathlib/Data/Sum/Basic.lean |
3 |
2 |
['MichaelStollBayreuth', 'github-actions'] |
nobody |
34-83863 1 month ago |
34-83982 1 month ago |
39-78415 39 days |
| 31610 |
rudynicolop author:rudynicolop |
feat(Computability/NFA): Kleene star closure for Regular Languages via NFA |
This PR constructs a Kleene star closure for non-epsilon NFAs, and proves that regular languages are closed under Kleene star. The NFA construction is `NFA.kstar`. The main theorems are:
- `NFA.accepts_kstar`: demonstrates that `M.kstar` accepts the Kleene star closure of the language of `M`.
- `IsRegular.kstar`: demonstrates that regular languages are closed under Kleene star.
There is an onging zulip discussion about regular languages in Mathlib: https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/Regular.20languages.3A.20the.20review.20queue/with/553759136
This discussion is also tracked at #24205.
Furthermore, the construction and proofs in this PR are heavily inspired by @TpmKranz from his #15651. #15651 supersedes this PR, so if it is accepted then this PR is not needed.
---
- [x] depends on: #31038
[](https://gitpod.io/from-referrer/)
|
new-contributor
t-computability
|
405/7 |
Mathlib/Computability/NFA.lean |
1 |
5 |
['ctchou', 'github-actions', 'mathlib4-dependent-issues-bot', 'mathlib4-merge-conflict-bot'] |
nobody |
34-67921 1 month ago |
40-71123 1 month ago |
40-74077 40 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 |
703/0 |
Mathlib.lean,Mathlib/Tactic.lean,Mathlib/Tactic/WildcardLevel.lean,MathlibTest/WildcardLevel.lean |
4 |
25 |
['JovanGerb', 'adamtopaz', 'github-actions'] |
dwrensha assignee:dwrensha |
34-59704 1 month ago |
37-66035 1 month ago |
38-70636 38 days |
| 32273 |
jsm28 author:jsm28 |
feat(Analysis/Convex/Side): affine combinations on same / opposite side of face of a simplex as a vertex |
Build on #31205 by providing lemmas about when an affine combination of the vertices of a simplex is on the same / opposite side of a face (opposite a vertex) of the simplex as that vertex (a specific case of the lemmas from #31205 which involve two arbitrary affine combinations).
---
- [ ] depends on: #31205
[](https://gitpod.io/from-referrer/)
|
t-analysis
t-convex-geometry
|
62/0 |
Mathlib/Analysis/Convex/Side.lean |
1 |
3 |
['github-actions', 'mathlib4-dependent-issues-bot', 'mathlib4-merge-conflict-bot'] |
nobody |
34-21851 1 month ago |
34-21880 1 month ago |
34-29460 34 days |
| 32455 |
vihdzp author:vihdzp |
feat: order topologies of successor orders |
---
Co-authored by @j-loreaux
[](https://gitpod.io/from-referrer/)
|
t-topology
t-order
|
124/43 |
Mathlib.lean,Mathlib/Order/Cover.lean,Mathlib/SetTheory/Ordinal/Topology.lean,Mathlib/Topology/Order/SuccPred.lean |
4 |
1 |
['github-actions'] |
pechersky assignee:pechersky |
33-59703 1 month ago |
37-47018 1 month ago |
37-47009 37 days |
| 31059 |
gasparattila author:gasparattila |
feat(Topology/Sets): define the Vietoris topology on `(Nonempty)Compacts` |
This PR defines the Vietoris topology on `Compacts` and `NonemptyCompacts`, and proves that it is induced by the Hausdorff uniformity.
---
- [x] depends on: #31031
- [x] depends on: #31058
[](https://gitpod.io/from-referrer/)
|
t-topology |
257/29 |
Mathlib.lean,Mathlib/Data/Rel.lean,Mathlib/Topology/MetricSpace/Closeds.lean,Mathlib/Topology/Sets/Compacts.lean,Mathlib/Topology/Sets/VietorisTopology.lean,Mathlib/Topology/UniformSpace/Closeds.lean,docs/references.bib |
7 |
6 |
['github-actions', 'mathlib4-dependent-issues-bot', 'mathlib4-merge-conflict-bot', 'robin-carlier'] |
ADedecker assignee:ADedecker |
30-77060 30 days ago |
31-4846 1 month ago |
51-51401 51 days |
| 30112 |
gaetanserre author:gaetanserre |
feat(Probability.Kernel): add representation of kernel as a map of a uniform measure |
Add results about isolation of kernels randomness. In particular, it shows that one
can write a Markov kernel as the map by a deterministic of a uniform measure on `[0, 1]`.
It corresponds to Lemma 4.22 in "[Foundations of Modern Probability](https://link.springer.com/book/10.1007/978-3-030-61871-1)" by Olav Kallenberg, 2021.
---
[](https://gitpod.io/from-referrer/)
|
t-measure-probability |
149/0 |
Mathlib.lean,Mathlib/Probability/Kernel/Representation.lean |
2 |
4 |
['RemyDegenne', 'gaetanserre', 'github-actions', 'mathlib4-merge-conflict-bot'] |
RemyDegenne assignee:RemyDegenne |
30-6495 30 days ago |
34-20700 1 month ago |
34-20992 34 days |
| 32552 |
ksenono author:ksenono |
feat(SetTheory/Cardinal): helpers for Konig's theorem |
---
[](https://gitpod.io/from-referrer/)
|
new-contributor
t-set-theory
|
70/0 |
Mathlib/SetTheory/Cardinal/Arithmetic.lean,Mathlib/SetTheory/Cardinal/Basic.lean |
2 |
33 |
['SnirBroshi', 'b-mehta', 'github-actions', 'ksenono', 'staroperator', 'vihdzp'] |
b-mehta assignee:b-mehta |
28-43832 28 days ago |
34-76675 1 month ago |
34-76718 34 days |
| 32600 |
PrParadoxy author:PrParadoxy |
feat(LinearAlgebra/Multilinear): composition of multilinear maps |
The composition of a multilinear map with a family of multilinear maps
is a multilinear map indexed by a dependent sum.
The result reduces to a lemma about the interaction of function
application, `Sigma.curry`, and `Function.update`. This variant of
`Function.apply_update` is included as `Sigma.apply_curry_update`.
[](https://gitpod.io/from-referrer/)
|
new-contributor |
40/0 |
Mathlib/Data/Sigma/Basic.lean,Mathlib/LinearAlgebra/Multilinear/Basic.lean |
2 |
4 |
['github-actions', 'goliath-klein', 'kbuzzard'] |
dwrensha assignee:dwrensha |
28-2303 28 days ago |
32-83571 1 month ago |
32-83836 32 days |
| 26608 |
vihdzp author:vihdzp |
feat(SetTheory/Cardinal/Aleph): `o.card ≤ ℵ_ o` and variants |
---
[](https://gitpod.io/from-referrer/)
|
t-set-theory |
24/0 |
Mathlib/SetTheory/Cardinal/Aleph.lean |
1 |
4 |
['artie2000', 'github-actions', 'kckennylau', 'leanprover-community-bot-assistant', 'vihdzp'] |
alreadydone assignee:alreadydone |
26-8843 26 days ago |
32-28743 1 month ago |
56-5719 56 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/)
|
t-algebra label:t-algebra$ |
4/0 |
Mathlib/Algebra/Order/Group/Defs.lean |
1 |
1 |
['artie2000', 'github-actions'] |
eric-wieser assignee:eric-wieser |
25-59711 25 days ago |
29-49061 29 days ago |
29-49096 29 days |
| 31364 |
YaelDillies author:YaelDillies |
feat: binomial random graphs |
From LeanCamCombi and formal-conjectures
---
- [x] depends on: #31391
- [x] depends on: #31392
- [x] depends on: #31393
- [x] depends on: #31394
- [x] depends on: #31396
- [x] depends on: #31397
- [x] depends on: #31398
- [x] depends on: #31442
- [x] depends on: #31443
- [x] depends on: #31445
- [x] depends on: #31908
[](https://gitpod.io/from-referrer/)
|
t-combinatorics
t-measure-probability
|
158/0 |
Mathlib.lean,Mathlib/Probability/Combinatorics/BinomialRandomGraph/Defs.lean,Mathlib/Probability/Combinatorics/README.md |
3 |
9 |
['LibertasSpZ', 'YaelDillies', 'github-actions', 'mathlib4-dependent-issues-bot', 'mathlib4-merge-conflict-bot'] |
EtienneC30 assignee:EtienneC30 |
24-83433 24 days ago |
24-83436 24 days ago |
30-80691 30 days |
| 32772 |
tb65536 author:tb65536 |
feat(Data/Set/Card): criterion for `s.ncard ≤ (f '' s).ncard + 1` |
This PR gives a criterion `s.ncard ≤ (f '' s).ncard + 1` (note that we always have the inequality `(f '' s).ncard ≤ s.ncard`).
---
[](https://gitpod.io/from-referrer/)
|
t-data |
31/0 |
Mathlib/Data/Set/Card.lean |
1 |
1 |
['github-actions'] |
pechersky assignee:pechersky |
24-59703 24 days ago |
30-42658 30 days ago |
30-42635 30 days |
| 32555 |
ksenono author:ksenono |
feat(Combinatorics/SimpleGraph/Matching): maximum and maximal matchings for Konig's theorem |
---
[](https://gitpod.io/from-referrer/)
|
t-combinatorics
new-contributor
|
127/1 |
Mathlib/Combinatorics/SimpleGraph/DegreeSum.lean,Mathlib/Combinatorics/SimpleGraph/Matching.lean |
2 |
8 |
['SnirBroshi', 'github-actions', 'ksenono'] |
awainverse assignee:awainverse |
24-48353 24 days ago |
34-75397 1 month ago |
34-75430 34 days |
| 32570 |
ksenono author:ksenono |
feat(Combinatorics/SimpleGraph): bipartite subgraphs and vertex-disjoint graphs for Konig's theorem |
---
[](https://gitpod.io/from-referrer/)
|
t-combinatorics
new-contributor
|
22/0 |
Mathlib/Combinatorics/SimpleGraph/Bipartite.lean,Mathlib/Combinatorics/SimpleGraph/Subgraph.lean |
2 |
10 |
['SnirBroshi', 'github-actions'] |
kmill assignee:kmill |
24-47893 24 days ago |
34-52196 1 month ago |
34-52240 34 days |
| 32679 |
YaelDillies author:YaelDillies |
chore(Data/Sym2): improve defeq of `diagSet` |
#30559 introduced a regression on the defeqs in the `SimpleGraph` API. This PR fixes it.
From LeanCamCombi
---
I personally think this new `diagSet` definition is unnecessary: `{e | e.IsDiag}` is not much longer to write than `Sym2.diagSet` and more transparent, but whatever.
[](https://gitpod.io/from-referrer/)
|
t-data |
52/41 |
Mathlib/Combinatorics/SimpleGraph/Basic.lean,Mathlib/Combinatorics/SimpleGraph/DeleteEdges.lean,Mathlib/Combinatorics/SimpleGraph/Operations.lean,Mathlib/Data/Sym/Card.lean,Mathlib/Data/Sym/Sym2.lean |
5 |
9 |
['SnirBroshi', 'YaelDillies', 'b-mehta', 'github-actions', 'mathlib4-merge-conflict-bot', 'vihdzp'] |
pechersky assignee:pechersky |
23-71317 23 days ago |
23-71381 23 days ago |
32-15980 32 days |
| 32355 |
bjornsolheim author:bjornsolheim |
feat(Geometry/Convex/Cone): define and characterize simplicial pointed cones |
Define finitely generated and simplicial pointed cones.
Prove lemmas about simplicial (and generating simplicial) cones
# Notes
* I have tried alternative implementations (finite, finset, structure) If one can live with the extensional quantifier the finset seems better.
---
[](https://gitpod.io/from-referrer/)
|
new-contributor
t-convex-geometry
|
118/0 |
Mathlib.lean,Mathlib/Geometry/Convex/Cone/Simplicial.lean |
2 |
1 |
['github-actions'] |
nobody |
23-63970 23 days ago |
23-64462 23 days ago |
33-69078 33 days |
| 33028 |
bjornsolheim author:bjornsolheim |
feat(Geometry/Convex/Cone): minimal and maximal cone tensor products are commutative |
Prove that the minimal and maximal cone tensor products are commutative.
---
[](https://gitpod.io/from-referrer/)
|
t-convex-geometry |
57/0 |
Mathlib/Geometry/Convex/Cone/TensorProduct.lean |
1 |
1 |
['github-actions'] |
nobody |
23-23899 23 days ago |
24-52310 24 days ago |
24-52355 24 days |
| 31425 |
robertmaxton42 author:robertmaxton42 |
feat(Topology): implement delaborators for non-standard topology notation |
Add delaborators for unary and binary notation related to non-standard topologies in the TopologicalSpace namespace.
---
[](https://gitpod.io/from-referrer/)
|
t-topology |
104/0 |
Mathlib.lean,Mathlib/Topology/Defs/Basic.lean,Mathlib/Util/DelabNonCanonical.lean,MathlibTest/Delab/TopologicalSpace.lean |
4 |
31 |
['eric-wieser', 'github-actions', 'jcommelin', 'kckennylau', 'robertmaxton42'] |
PatrickMassot assignee:PatrickMassot |
23-10186 23 days ago |
48-38249 1 month ago |
48-69141 48 days |
| 32532 |
SnirBroshi author:SnirBroshi |
feat(Combinatorics/SimpleGraph/Connectivity): connected components are maximally connected subsets/subgraphs |
---
[](https://gitpod.io/from-referrer/)
|
t-combinatorics |
32/0 |
Mathlib/Combinatorics/SimpleGraph/Connectivity/Connected.lean,Mathlib/Combinatorics/SimpleGraph/Connectivity/Subgraph.lean |
2 |
2 |
['github-actions', 'mathlib4-merge-conflict-bot'] |
awainverse assignee:awainverse |
22-67934 22 days ago |
22-67960 22 days ago |
35-36910 35 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/)
|
new-contributor
t-computability
maintainer-merge
|
104/7 |
Mathlib/Computability/NFA.lean |
1 |
63 |
['YaelDillies', 'ctchou', 'github-actions', 'lambda-fairy', 'mathlib4-dependent-issues-bot', 'mathlib4-merge-conflict-bot', 'rudynicolop'] |
YaelDillies assignee:YaelDillies |
22-67669 22 days ago |
23-48124 23 days ago |
41-60028 41 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.
---
- [ ] depends on: #32259
[](https://gitpod.io/from-referrer/)
|
t-euclidean-geometry |
157/0 |
Mathlib/Geometry/Euclidean/Angle/Oriented/Affine.lean |
1 |
3 |
['github-actions', 'mathlib4-dependent-issues-bot', 'mathlib4-merge-conflict-bot'] |
JovanGerb assignee:JovanGerb |
22-59719 22 days ago |
25-71282 25 days ago |
25-73790 25 days |
| 32826 |
felixpernegger author:felixpernegger |
feat(Data/Tuple/Sort): Permutation is monotone iff its the identity |
Sort of permutation is its inverse + Permutation is monotone iff its the identity |
new-contributor
t-data
|
19/0 |
Mathlib/Data/Fin/Tuple/Sort.lean |
1 |
1 |
['github-actions'] |
TwoFX assignee:TwoFX |
22-59715 22 days ago |
29-52829 29 days ago |
29-52837 29 days |
| 32127 |
CoolRmal author:CoolRmal |
feat: use IndexedPartition.piecewise to create simple/measurable/strongly measurable functions |
The lemmas proved in this PR are needed in https://github.com/RemyDegenne/brownian-motion/pull/304.
---
[](https://gitpod.io/from-referrer/)
|
t-measure-probability
large-import
brownian
|
111/4 |
Mathlib/Data/Setoid/Partition.lean,Mathlib/MeasureTheory/Function/SimpleFunc.lean,Mathlib/MeasureTheory/Function/StronglyMeasurable/Basic.lean,Mathlib/MeasureTheory/MeasurableSpace/Basic.lean |
4 |
21 |
['CoolRmal', 'EtienneC30', 'github-actions', 'hanwenzhu', 'mathlib4-merge-conflict-bot'] |
EtienneC30 assignee:EtienneC30 |
22-25450 22 days ago |
22-25509 22 days ago |
44-4434 44 days |
| 32739 |
Rida-Hamadani author:Rida-Hamadani |
chore(SimpleGraph): golf and improve style of `Subwalks.lean` |
maintaining the sub-walks file after the walk split, golfing some proofs
---
[](https://gitpod.io/from-referrer/)
|
t-combinatorics |
11/18 |
Mathlib/Combinatorics/SimpleGraph/Walks/Subwalks.lean |
1 |
1 |
['github-actions', 'vlad902'] |
awainverse assignee:awainverse |
21-59688 21 days ago |
31-7710 1 month ago |
31-7791 31 days |
| 32910 |
felixpernegger author:felixpernegger |
feat(Data/Nat/Choose): two binomial coefficient sum identities |
This PR proves two well-known sum identities around binomial coefficients.
While there are probably hundreds of such identities, these two seem to be well known enough to be in mathlib (i.e. are mentioned in the Wikipedia [article](https://en.wikipedia.org/wiki/Binomial_coefficient#math_8) about binomial coefficients). |
new-contributor
t-data
|
31/0 |
Mathlib/Data/Nat/Choose/Sum.lean,Mathlib/Data/Nat/Choose/Vandermonde.lean |
2 |
1 |
['github-actions'] |
TwoFX assignee:TwoFX |
21-59685 21 days ago |
27-9261 27 days ago |
27-9590 27 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 |
40/2 |
Mathlib/Tactic/Simps/Basic.lean,MathlibTest/SimpsModule.lean |
2 |
8 |
['JovanGerb', 'github-actions', 'kim-em'] |
eric-wieser assignee:eric-wieser |
21-59684 21 days ago |
25-50491 25 days ago |
25-50530 25 days |
| 33016 |
xgenereux author:xgenereux |
feat: RingHom.adjoinAlgebraMap |
Consider a tower of rings `A / B / C` and `b : B`, then there is a natural map from
`A[b]` to `A[algebraMap B C b]` (adjoin `b` viewed as an element of `C`).
This PR adds 3 versions, depending on whether we use `Algebra.adjoin` or `IntermediateField.adjoin`:
- `Algebra.RingHom.adjoinAlgebraMap : Algebra.adjoin A {b} →+* Algebra.adjoin A {(algebraMap B C) b}`
- `IntermediateField.RingHom.adjoinAlgebraMapOfAlgebra : Algebra.adjoin A {b} →+* A⟮((algebraMap B C) b)⟯`
- `IntermediateField.RingHom.adjoinAlgebraMap : A⟮b⟯ →+* A⟮((algebraMap B C) b)⟯`
Note:
We create a new file for `Algebra.RingHom.adjoinAlgebraMap`, which is intended for results about adjoining singletons, because it is convenient to import `Algebra.Adjoin.Polynomial`.
Co-authored-by: María Inés de Frutos Fernández <[mariaines.dff@gmail.com](mailto:mariaines.dff@gmail.com)>
---
[](https://gitpod.io/from-referrer/)
|
|
103/0 |
Mathlib.lean,Mathlib/FieldTheory/IntermediateField/Adjoin/Algebra.lean,Mathlib/FieldTheory/IntermediateField/Adjoin/Defs.lean,Mathlib/RingTheory/Adjoin/Singleton.lean |
4 |
1 |
['github-actions'] |
bryangingechen assignee:bryangingechen |
21-59681 21 days ago |
24-70184 24 days ago |
24-70160 24 days |
| 30898 |
vihdzp author:vihdzp |
feat: characterization of `List.splitBy` |
---
- [x] depends on: #30892
Moved from #16837.
[](https://gitpod.io/from-referrer/)
|
t-data |
110/10 |
Mathlib/Data/List/Flatten.lean,Mathlib/Data/List/SplitBy.lean |
2 |
6 |
['github-actions', 'mathlib4-dependent-issues-bot', 'mathlib4-merge-conflict-bot', 'vihdzp'] |
TwoFX assignee:TwoFX |
21-53715 21 days ago |
21-53739 21 days ago |
31-9408 31 days |
| 28796 |
grunweg author:grunweg |
feat: immersions are smooth |
The conventional textbook definition demands that an immersion be smooth.
When asking for the immersion to have local slice charts (as we do), this implies smoothness automatically.
---
- [x] depends on: #28701
- [x] depends on: #28793
- [x] depends on: #30356
- [x] depends on: #28853 (for simplicity)
[](https://gitpod.io/from-referrer/)
|
t-differential-geometry |
198/15 |
Mathlib/Analysis/Calculus/ContDiff/Basic.lean,Mathlib/Geometry/Manifold/ContMDiff/Atlas.lean,Mathlib/Geometry/Manifold/Immersion.lean,Mathlib/Geometry/Manifold/IsManifold/ExtChartAt.lean,Mathlib/Geometry/Manifold/LocalSourceTargetProperty.lean,Mathlib/Geometry/Manifold/SmoothEmbedding.lean |
6 |
25 |
['chrisflav', 'github-actions', 'grunweg', 'mathlib4-dependent-issues-bot', 'mathlib4-merge-conflict-bot'] |
PatrickMassot assignee:PatrickMassot |
20-59691 20 days ago |
24-4623 24 days ago |
24-11949 24 days |
| 26484 |
peabrainiac author:peabrainiac |
feat(Geometry/Diffeology): basics of diffeological spaces |
Introduces diffeological spaces, smooth maps between them, the D-topology and the standard diffeology on finite-dimensional normed spaces.
---
This PR continues the work from #21969. |
t-differential-geometry |
491/0 |
Mathlib.lean,Mathlib/Geometry/Diffeology/Basic.lean,docs/references.bib |
3 |
12 |
['JovanGerb', 'github-actions', 'grunweg', 'lecopivo', 'mathlib4-merge-conflict-bot', 'peabrainiac'] |
ocfnash assignee:ocfnash |
20-28905 20 days ago |
21-63574 21 days ago |
160-8866 160 days |
| 32021 |
jsm28 author:jsm28 |
feat(Geometry/Euclidean/Altitude): `map` and `restrict` lemmas |
Add lemmas about `altitude`, `altitudeFoot` and `height` for simplices mapped under an affine isometry or restricted to an affine subspace.
---
- [x] depends on: #32016
- [x] depends on: #32017
- [ ] depends on: #32019
[](https://gitpod.io/from-referrer/)
|
t-euclidean-geometry |
75/0 |
Mathlib/Geometry/Euclidean/Altitude.lean |
1 |
4 |
['github-actions', 'mathlib4-dependent-issues-bot', 'mathlib4-merge-conflict-bot'] |
JovanGerb assignee:JovanGerb |
19-59707 19 days ago |
22-85717 22 days ago |
22-85780 22 days |
| 33031 |
chiyunhsu author:chiyunhsu |
feat(Combinatorics/Enumerative/Partition): add combinatorial proof of Euler's partition theorem |
The new file EulerComb.lean contains the combinatorial proof of Euler's partition theorem. The analytic proof of the theorem and its generalization of Glaisher's Theorem has already been formalized in [Glaisher.lean](https://github.com/leanprover-community/mathlib4/blob/master/Mathlib/Combinatorics/Enumerative/Partition/Glaisher.lean). The generalization of the combinatorial proof from this file to Glaisher's Theorem is within reach.
---
[](https://gitpod.io/from-referrer/)
|
t-combinatorics
new-contributor
|
531/0 |
Mathlib.lean,Mathlib/Combinatorics/Enumerative/Partition/EulerComb.lean |
2 |
5 |
['chiyunhsu', 'github-actions', 'tb65536', 'vihdzp'] |
b-mehta assignee:b-mehta |
19-59704 19 days ago |
24-37229 24 days ago |
24-37272 24 days |
| 33044 |
bryangingechen author:bryangingechen |
ci: also get cache for parent commit |
cf. https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/Mathlib.20has.20moved.20to.20the.20new.20module.20system/near/563452000
---
[](https://gitpod.io/from-referrer/)
|
CI |
84/8 |
.github/build.in.yml,.github/workflows/bors.yml,.github/workflows/build.yml,.github/workflows/build_fork.yml |
4 |
7 |
['bryangingechen', 'github-actions', 'jcommelin', 'mathlib-bors'] |
joneugster assignee:joneugster |
19-59702 19 days ago |
22-70529 22 days ago |
23-45877 23 days |
| 33063 |
DavidLedvinka author:DavidLedvinka |
chore(Probability): Rename Adapted to StronglyAdapted |
See discussion at: https://leanprover.zulipchat.com/#narrow/channel/509433-Brownian-motion/topic/Adapted.20Filtrations.20for.20Markov.20Chains.20and.20Markov.20Processes
|
t-measure-probability |
328/224 |
Mathlib/Probability/Kernel/Disintegration/Density.lean,Mathlib/Probability/Martingale/Basic.lean,Mathlib/Probability/Martingale/BorelCantelli.lean,Mathlib/Probability/Martingale/Centering.lean,Mathlib/Probability/Martingale/Convergence.lean,Mathlib/Probability/Martingale/OptionalSampling.lean,Mathlib/Probability/Martingale/OptionalStopping.lean,Mathlib/Probability/Martingale/Upcrossing.lean,Mathlib/Probability/Moments/SubGaussian.lean,Mathlib/Probability/Process/Adapted.lean,Mathlib/Probability/Process/HittingTime.lean,Mathlib/Probability/Process/Predictable.lean,Mathlib/Probability/Process/Stopping.lean |
13 |
9 |
['DavidLedvinka', 'EtienneC30', 'github-actions'] |
EtienneC30 assignee:EtienneC30 |
19-59701 19 days ago |
22-63171 22 days ago |
23-22717 23 days |
| 33082 |
AntoineChambert-Loir author:AntoineChambert-Loir |
feat(GroupTheory/SpecificGroups/Alternating/Simple): the alternating group on at least 5 letters is simple. |
This is the conclusion of the story of the proof of simplicity of the alternating group using the
Iwasawa criterion.
* `Equiv.Perm.iwasawaStructure_two`:
the natural `IwasawaStructure` of `Equiv.Perm α` acting on `Nat.Combination α 2`
Its commutative subgroups consist of the permutations with support
in a given element of `Nat.Combination α 2`.
They are cyclic of order 2.
* `alternatingGroup_of_le_of_normal`:
If `α` has at least 5 elements, then a nontrivial normal subgroup
of `Equiv.Perm α` contains the alternating group.
* `alternatingGroup.iwasawaStructure_three`:
the natural `IwasawaStructure` of `alternatingGroup α` acting on `Nat.Combination α 3`
Its commutative subgroups consist of the permutations with support
in a given element of `Nat.Combination α 2`.
They are cyclic of order 3.
* `alternatingGroup.iwasawaStructure_three`:
the natural `IwasawaStructure` of `alternatingGroup α` acting on `Nat.Combination α 4`
Its commutative subgroups consist of the permutations of
cycleType (2, 2) with support in a given element of `Nat.Combination α 2`.
They have order 4 and exponent 2 (`IsKleinFour`).
* `alternatingGroup.normal_subgroup_eq_bot_or_eq_top`:
If `α` has at least 5 elements, then a nontrivial normal subgroup of `alternatingGroup` is `⊤`.
* `alternatingGroup.isSimpleGroup`:
If `α` has at least 5 elements, then `alternatingGroup α`
is a simple group.
---
[](https://gitpod.io/from-referrer/)
|
large-import
t-group-theory
|
821/13 |
Mathlib.lean,Mathlib/GroupTheory/GroupAction/SubMulAction/Combination.lean,Mathlib/GroupTheory/Perm/Cycle/Type.lean,Mathlib/GroupTheory/Perm/Support.lean,Mathlib/GroupTheory/SpecificGroups/Alternating.lean,Mathlib/GroupTheory/SpecificGroups/Alternating/Simple.lean,Mathlib/GroupTheory/SpecificGroups/KleinFour.lean |
7 |
1 |
['github-actions'] |
mattrobball assignee:mattrobball |
19-59699 19 days ago |
23-18221 23 days ago |
23-18267 23 days |
| 33109 |
felixpernegger author:felixpernegger |
feat(Data/Nat/Choose): Binomial inversion |
This PR adds binomial inversion (also called binomial transform), which is a useful method for proving binomial identities.
It is tricky to find direct references to binomial inversion, but for example [this](https://en.wikipedia.org/wiki/Binomial_transform#Binomial_convolution) Wikipedia article mentions it ("The formula").
The first theorem ```alternating_sum_choose_mul_of_alternating_sum_choose_mul``` could be refined (we only need the hypothesis ```h``` up to some point), but this seems to needlessly complicate it. |
new-contributor |
107/0 |
Mathlib.lean,Mathlib/Data/Nat/Choose/Inversion.lean |
2 |
4 |
['felixpernegger', 'github-actions', 'wwylele'] |
dagurtomas assignee:dagurtomas |
19-59694 19 days ago |
22-73026 22 days ago |
22-73010 22 days |
| 33126 |
CoolRmal author:CoolRmal |
feat: function composition preserves boundedness |
This PR adds the following theorem: if the range of a function `g` is bounded above, then `g ∘ f` is bounded above for
all functions `f`.
---
[](https://gitpod.io/from-referrer/)
|
t-order |
12/0 |
Mathlib/Order/Bounds/Basic.lean |
1 |
1 |
['github-actions'] |
bryangingechen assignee:bryangingechen |
18-59695 18 days ago |
22-17338 22 days ago |
22-17380 22 days |
| 33128 |
gasparattila author:gasparattila |
feat(Topology/UniformSpace): generalize `TotallyBounded` to filters |
Some of these generalizations will be useful for showing the completeness of `TopologicalSpace.Compacts` in a non-metrizable setting.
---
[](https://gitpod.io/from-referrer/)
|
t-topology |
156/54 |
Mathlib/Data/Rel.lean,Mathlib/Topology/UniformSpace/Cauchy.lean,Mathlib/Topology/UniformSpace/UniformEmbedding.lean |
3 |
1 |
['github-actions'] |
dagurtomas assignee:dagurtomas |
18-59694 18 days ago |
21-69790 21 days ago |
22-7926 22 days |
| 33253 |
SnirBroshi author:SnirBroshi |
feat(Combinatorics/SimpleGraph/Clique): avoid `Fintype`/`Finite` assumptions where possible |
Also prove `G.cliqueNum ≤ G.chromaticNumber` without any finiteness assumptions.
---
[](https://gitpod.io/from-referrer/)
|
t-combinatorics |
39/40 |
Mathlib/Combinatorics/SimpleGraph/Clique.lean,Mathlib/Combinatorics/SimpleGraph/Coloring.lean |
2 |
1 |
['github-actions'] |
nobody |
18-18135 18 days ago |
18-18147 18 days ago |
18-18184 18 days |
| 33254 |
SnirBroshi author:SnirBroshi |
feat(Data/Nat/Lattice): `¬BddAbove s → sSup s = 0` |
---
Note that it can also be proven `by simp [h]` after the `ConditionallyCompleteLinearOrderBot` instance below it.
The theorem name matches the same theorems for other types: `Int.csSup_of_not_bdd_above`, `Real.sSup_of_not_bddAbove`, `NNReal.sSup_of_not_bddAbove`.
Also renamed related `Int` theorems to conform to the naming conventions.
[Zulip](https://leanprover.zulipchat.com/#narrow/channel/217875-Is-there-code-for-X.3F/topic/.60.C2.ACBddAbove.20s.20.E2.86.92.20sSup.20s.20.3D.200.60/with/565275221)
[](https://gitpod.io/from-referrer/)
|
t-data |
15/4 |
Mathlib/Data/Int/ConditionallyCompleteOrder.lean,Mathlib/Data/Nat/Lattice.lean |
2 |
3 |
['SnirBroshi', 'github-actions', 'vihdzp'] |
nobody |
17-81317 17 days ago |
18-17623 18 days ago |
18-17662 18 days |
| 32160 |
SnirBroshi author:SnirBroshi |
feat(Combinatorics/SimpleGraph/Walks): helper theorems about `darts` and `support` |
---
[](https://gitpod.io/from-referrer/)
|
t-combinatorics |
33/1 |
Mathlib/Combinatorics/SimpleGraph/Walks/Basic.lean,Mathlib/Combinatorics/SimpleGraph/Walks/Traversal.lean |
2 |
1 |
['github-actions'] |
kmill assignee:kmill |
17-75357 17 days ago |
45-57325 1 month ago |
45-57359 45 days |
| 33147 |
SnirBroshi author:SnirBroshi |
feat(Combinatorics/SimpleGraph/Coloring): add a few missing instances (`IsEmpty`/`Nontrivial`/`Infinite`) |
---
[](https://gitpod.io/from-referrer/)
|
t-combinatorics |
22/0 |
Mathlib/Combinatorics/SimpleGraph/Coloring.lean,Mathlib/Combinatorics/SimpleGraph/Maps.lean |
2 |
1 |
['github-actions'] |
b-mehta assignee:b-mehta |
17-59709 17 days ago |
21-52843 21 days ago |
21-52891 21 days |
| 31092 |
FlAmmmmING author:FlAmmmmING |
feat(Algebra/Group/ForwardDiff.lean): Add theorem `sum_shift_eq_fwdDiff_iter`. |
---
[](https://gitpod.io/from-referrer/)
|
t-algebra
new-contributor
label:t-algebra$ |
17/1 |
Mathlib/Algebra/Group/ForwardDiff.lean |
1 |
18 |
['BeibeiX0', 'FlAmmmmING', 'Ruben-VandeVelde', 'dagurtomas', 'github-actions', 'mathlib4-merge-conflict-bot'] |
dagurtomas assignee:dagurtomas |
17-35077 17 days ago |
17-35101 17 days ago |
43-31734 43 days |
| 33121 |
SnirBroshi author:SnirBroshi |
feat(Combinatorics/SimpleGraph/Hasse): paths in a graph are isomorphic to path graphs |
---
[](https://gitpod.io/from-referrer/)
|
t-combinatorics
large-import
|
38/1 |
Mathlib/Combinatorics/SimpleGraph/Hasse.lean |
1 |
1 |
['github-actions'] |
b-mehta assignee:b-mehta |
17-21278 17 days ago |
22-29296 22 days ago |
22-29338 22 days |
| 33211 |
Komyyy author:Komyyy |
doc(Order/Filter/*): outdated documents |
`f ×ˢ g` is not an notation of `Filter.prod` anymore, but [a notation class](https://leanprover-community.github.io/mathlib4_docs/Mathlib/Order/Filter/Defs.html#Filter.instSProd).
Also, some definitions were moved to `Mathlib.Order.Filter.Defs`.
---
[](https://gitpod.io/from-referrer/)
|
documentation
t-order
|
6/10 |
Mathlib/Order/Filter/Curry.lean,Mathlib/Order/Filter/Pi.lean,Mathlib/Order/Filter/Prod.lean |
3 |
6 |
['Komyyy', 'github-actions', 'plp127'] |
bryangingechen assignee:bryangingechen |
16-59698 16 days ago |
19-63284 19 days ago |
19-63264 19 days |
| 32971 |
Paul-Lez author:Paul-Lez |
feat(Data/Finsupp/Pointwise): generalise pointwise scalar multiplication of finsupps |
This PR continues the work from #24050.
Original PR: https://github.com/leanprover-community/mathlib4/pull/24050 |
t-data |
7/4 |
Mathlib/Data/Finsupp/Pointwise.lean |
1 |
2 |
['Paul-Lez', 'github-actions'] |
pechersky assignee:pechersky |
15-59707 15 days ago |
26-2039 26 days ago |
26-2078 26 days |
| 33248 |
vihdzp author:vihdzp |
refactor(MeasureTheory/Measure/Stieltjes): simpler definition of `botSet` |
---
Arguably we could get rid of `botSet` altogether, but in either case this is still an improvement.
[](https://gitpod.io/from-referrer/)
|
t-measure-probability |
13/19 |
Mathlib/MeasureTheory/Measure/Stieltjes.lean |
1 |
1 |
['github-actions'] |
EtienneC30 assignee:EtienneC30 |
15-59703 15 days ago |
18-61098 18 days ago |
18-61138 18 days |
| 33292 |
SnirBroshi author:SnirBroshi |
feat(Combinatorics/SimpleGraph/LineGraph): lift copies/isomorphisms to line-graph |
---
Non-injective homomorphisms (`G →g G'`) cannot be lifted to a homomorphism on line-graphs (`G.lineGraph →g G'.lineGraph`) because e.g. `∀ k > 1` there is a homomorphism from `pathGraph k` to `G'` iff `G'` has an edge, and `∀ n > 0, (pathGraph (n + 1)).lineGraph ≃ pathGraph n`, but there is no homomorphism from `pathGraph k` to `pathGraph 1` because it has no edges.
So for `G := pathGraph 3` and `G' := pathGraph 2` there is a `G →g G'` but no `G.lineGraph →g G'.lineGraph`.
But we can lift `Copy`/`Embedding`/`Iso`.
[](https://gitpod.io/from-referrer/)
|
t-combinatorics
large-import
|
47/4 |
Mathlib/Combinatorics/SimpleGraph/LineGraph.lean,Mathlib/Data/Sym/Sym2.lean |
2 |
1 |
['github-actions'] |
nobody |
15-40793 15 days ago |
16-10941 16 days ago |
16-65782 16 days |
| 32987 |
kim-em author:kim-em |
feat: pipeline downloads and decompression in `cache get` |
This PR modifies `lake exe cache get` to decompress files as they download, rather than waiting for all downloads to complete first.
Previously the cache system had two sequential phases: download all files using `curl --parallel`, then decompress all files using a single `leantar` call. Now a background task spawns sequential batched `leantar` calls to decompress files as downloads complete, pipelining network I/O and disk I/O.
🤖 Prepared with Claude Code |
|
194/30 |
Cache/Requests.lean |
1 |
1 |
['github-actions'] |
dagurtomas assignee:dagurtomas |
14-59673 14 days ago |
25-60819 25 days ago |
25-60795 25 days |
| 33206 |
lua-vr author:lua-vr |
feat(Integral.Bochner.Set): add `tendsto_setIntegral_of_monotone₀` |
Adds the lemma `tendsto_setIntegral_of_monotone₀`, a version of `tendsto_setIntegral_of_monotone` requiring only `AEMeasurableSet` in the hypothesis. The previous version is redefined as a specialization.
Also renames `integral_union_ae` to `setIntegral_union₀` for consistency with the rest of the library (it matches the existing `setIntegral_union`).
---
[](https://gitpod.io/from-referrer/)
|
t-measure-probability |
27/13 |
Mathlib/MeasureTheory/Integral/Bochner/Set.lean |
1 |
2 |
['github-actions', 'mathlib4-merge-conflict-bot'] |
RemyDegenne assignee:RemyDegenne |
13-85794 13 days ago |
13-85819 13 days ago |
19-18384 19 days |
| 33363 |
BoltonBailey author:BoltonBailey |
feat: add `empty_eq_image` simp lemmas |
Creates new simp lemmas `image_eq_empty`, similar to existing simp lemmas, but with the LHS equality reversed, so that simp can identify these when in this form.
---
[](https://gitpod.io/from-referrer/)
|
t-data |
7/0 |
Mathlib/Data/Finset/Image.lean,Mathlib/Data/Set/Image.lean |
2 |
1 |
['github-actions'] |
nobody |
13-66516 13 days ago |
13-66543 13 days ago |
13-66585 13 days |
| 29788 |
robertmaxton42 author:robertmaxton42 |
feat(Topology): adds bundled continuous maps for sum, sigma, subtype, mapsto, inclusion |
Adds a collection of bundled continuous maps and homeomorphisms, and helper lemmas for working with their compositions.
Bundling of existing continuity lemmas:
* `ContinuousMap.subtypeVal`
* `ContinuousMap.inl` and `.inr`; `ContinuousMap.sum` bundles `Continuous.sumElim`; `ContinuousMap.sumMap`, which is a quotient map when both components are quotient maps
* `ContinuousMap.sigmaMap`, which is a quotient map when given a family of quotient maps
* `ContinuousMap.mapsTo` bundles `ContinuousOn.restrict_mapsTo`
New functions:
* `ContinuousMap.preimageValIncl : C(s ↓∩ t, t)` and `.inclPreimageVal C(s, t ↓∩ s)`, and their unbundled functions in `Set`
* `Homeomorph.Set.preimageVal` witnesses that the two are opposite directions of a homeomorphism
* Descending from a coherent set of subspaces is a quotient map
The primary use for these bundled maps is easy composition and the ability to introduce them by rewriting right-to-left: it is much more convenient to write `subtypeVal.comp _` than to use either the anonymous constructor (which doesn't work in any position without an expected type) or `ContinuousMap.mk` (which will disappear as soon as it is coerced to a function, making it difficult to use in mixed-categorical contexts where many maps can only be reduced by introducing a composition with some other map.)
This PR is part of a family of PRs that ultimately construct transformations in both directions between the concrete `Topology.RelCWComplex` and abstract `TopCat.RelativeCWComplex`. `.mapsTo` in particular bundles together a couple of potentially nontrivial proofs in a way that makes them easy to refer to later; I use it and `.subtypeVal` particularly heavily later in a dependent PR to build the cell inclusion maps on both sides of the equivalence.
---
[](https://gitpod.io/from-referrer/)
|
large-import |
227/2 |
Mathlib/Data/Set/Subset.lean,Mathlib/Topology/Category/TopCat/Limits/Products.lean,Mathlib/Topology/Coherent.lean,Mathlib/Topology/Constructions.lean,Mathlib/Topology/Constructions/SumProd.lean,Mathlib/Topology/ContinuousMap/Basic.lean,scripts/noshake.json |
7 |
15 |
['adamtopaz', 'github-actions', 'mathlib4-merge-conflict-bot', 'robertmaxton42'] |
adamtopaz assignee:adamtopaz |
13-62299 13 days ago |
13-62712 13 days ago |
72-19819 72 days |
| 33280 |
michelsol author:michelsol |
feat(MeasureTheory/Integral/IntervalIntegral): add variant `integral_deriv_eq_sub_uIoo` of 2nd theorem of calculus. |
Add a continuous on uIcc, differentiable on uIoo, deriv version of the 2nd fundamental theorem of calculus.
This corresponds to what is written [here](https://en.wikipedia.org/wiki/Fundamental_theorem_of_calculus#Second_part).
For example it makes it easier to compute the integral :
```lean4
∫ x : ℝ in 0..1, (√(1 - x ^ 2))⁻¹ = ∫ x : ℝ in 0..1, deriv arcsin x = arcsin 1 - arcsin 0
```
It is not possible to use [`interval_deriv_eq_sub`](https://leanprover-community.github.io/mathlib4_docs/Mathlib/MeasureTheory/Integral/IntervalIntegral/FundThmCalculus.html#intervalIntegral.integral_deriv_eq_sub) which requires differentiability on all of [0,1], as `arcsin` isn't differentiable at 1.
---
[](https://gitpod.io/from-referrer/)
|
t-measure-probability
new-contributor
|
14/0 |
Mathlib/MeasureTheory/Integral/IntervalIntegral/FundThmCalculus.lean |
1 |
1 |
['github-actions'] |
EtienneC30 assignee:EtienneC30 |
13-59686 13 days ago |
16-86311 16 days ago |
16-86351 16 days |
| 30391 |
rudynicolop author:rudynicolop |
feat(Data/List): list splitting definitions and lemmas |
This PR continues the work from #24395.
Original PR: https://github.com/leanprover-community/mathlib4/pull/24395 |
new-contributor
t-data
|
108/2 |
Mathlib/Data/List/Perm/Lattice.lean,Mathlib/Data/List/TakeDrop.lean |
2 |
45 |
['BoltonBailey', 'IlPreteRosso', 'TwoFX', 'github-actions', 'kckennylau', 'mathlib4-merge-conflict-bot', 'rudynicolop'] |
TwoFX assignee:TwoFX |
13-48604 13 days ago |
22-66545 22 days ago |
88-31876 88 days |
| 30962 |
WangYiran01 author:WangYiran01 |
feat(Combinatorics/Enumerative): add lattice path lemmas and counts |
This PR adds definitions and theorems about monotone lattice paths:
- Defines `pathCount`, `pathCountFrom`, `SubdiagProp`, and related structures.
- Proves closed forms such as `pathCount_eq_closed`.
- Adds Dyck/ballot subdiagonal property (`SubdiagProp`).
All code builds successfully with `lake build`. |
t-combinatorics
new-contributor
|
76/0 |
Mathlib.lean,Mathlib/Combinatorics/Enumerative/RecLatticePath.lean |
2 |
3 |
['github-actions', 'mathlib4-merge-conflict-bot'] |
awainverse assignee:awainverse |
13-25563 13 days ago |
27-24698 27 days ago |
47-24527 47 days |
| 33064 |
DavidLedvinka author:DavidLedvinka |
feat(Probability): Add `condLExp`, conditional expectation with the Lebesgue integral |
Add definition of `condLExp`, conditional expectation using the Lebesgue integral. Also add basic API. |
t-measure-probability |
275/0 |
Mathlib.lean,Mathlib/MeasureTheory/Function/ConditionalLExpectation.lean,Mathlib/MeasureTheory/Integral/Lebesgue/Add.lean,Mathlib/MeasureTheory/MeasurableSpace/CountablyGenerated.lean,Mathlib/MeasureTheory/MeasurableSpace/Defs.lean,Mathlib/MeasureTheory/Measure/AEMeasurable.lean |
6 |
3 |
['DavidLedvinka', 'github-actions', 'leanprover-radar'] |
EtienneC30 assignee:EtienneC30 |
12-64885 12 days ago |
22-67909 22 days ago |
23-69666 23 days |
| 33143 |
wwylele author:wwylele |
feat(PowerSeries): pentagonal number theorem |
The proof is split in two files: `Mathlib/Topology/Algebra/InfiniteSum/Pentagonal.lean` for the algebraic part, and `Mathlib/RingTheory/PowerSeries/Pentagonal.lean` for the summability part. In the near future, I also plan to prove the real/complex version that branches off from the algebraic part.
---
- [ ] depends on: #30436
[](https://gitpod.io/from-referrer/)
|
|
324/1 |
Mathlib.lean,Mathlib/RingTheory/PowerSeries/Pentagonal.lean,Mathlib/Topology/Algebra/InfiniteSum/Pentagonal.lean,docs/1000.yaml |
4 |
12 |
['copilot-pull-request-reviewer', 'github-actions', 'mathlib4-dependent-issues-bot', 'vihdzp'] |
kex-y assignee:kex-y |
12-59704 12 days ago |
15-80097 15 days ago |
15-80559 15 days |
| 33297 |
tb65536 author:tb65536 |
feat(Algebra/Polynomial/Roots): add `card_rootSet_le` |
This PR adds a lemma stating that `Set.ncard (p.rootSet B) ≤ p.natDegree` (we already have similar lemmas for `Polynomial.roots`.
---
[](https://gitpod.io/from-referrer/)
|
t-algebra
large-import
label:t-algebra$ |
7/0 |
Mathlib/Algebra/Polynomial/Roots.lean |
1 |
1 |
['github-actions'] |
dagurtomas assignee:dagurtomas |
12-59703 12 days ago |
16-55703 16 days ago |
16-55681 16 days |
| 33335 |
YaelDillies author:YaelDillies |
feat(Combinatorics/SimpleGraph): more about two-reachability |
---
[](https://gitpod.io/from-referrer/)
|
t-combinatorics |
51/51 |
Mathlib/Combinatorics/SimpleGraph/Connectivity/Connected.lean,Mathlib/Combinatorics/SimpleGraph/Connectivity/EdgeConnectivity.lean,Mathlib/Combinatorics/SimpleGraph/DeleteEdges.lean |
3 |
3 |
['SnirBroshi', 'YaelDillies', 'github-actions'] |
nobody |
12-29827 12 days ago |
15-28809 15 days ago |
15-28851 15 days |
| 33084 |
joelriou author:joelriou |
feat(CategoryTheory): MorphismProperty induced on a quotient category |
Let `W : MorphismProperty C` and `homRel : HomRel C`. We assume that `homRel` is stable under pre- and postcomposition. We introduce a property `W.HasQuotient homRel` expressing that `W` induces a property of morphisms on the quotient category.
---
[](https://gitpod.io/from-referrer/)
|
t-category-theory
maintainer-merge
|
181/79 |
Mathlib.lean,Mathlib/Algebra/Homology/HomotopyCategory.lean,Mathlib/CategoryTheory/Groupoid/FreeGroupoid.lean,Mathlib/CategoryTheory/MorphismProperty/Quotient.lean,Mathlib/CategoryTheory/PathCategory/Basic.lean,Mathlib/CategoryTheory/Quotient.lean,Mathlib/CategoryTheory/Quotient/Linear.lean,Mathlib/CategoryTheory/Quotient/Preadditive.lean |
8 |
11 |
['dagurtomas', 'github-actions', 'jcommelin', 'joelriou', 'robin-carlier'] |
joneugster assignee:joneugster |
11-59694 11 days ago |
15-31288 15 days ago |
21-84162 21 days |
| 33465 |
SnirBroshi author:SnirBroshi |
chore(Data/Finset/Insert): golf `eq_singleton_iff_nonempty_unique_mem` using grind |
---
[](https://gitpod.io/from-referrer/)
|
t-data |
1/8 |
Mathlib/Data/Finset/Insert.lean |
1 |
1 |
['github-actions'] |
nobody |
9-83329 9 days ago |
9-83336 9 days ago |
9-83374 9 days |
| 32803 |
erdOne author:erdOne |
feat(RIngTheory): more-linear version of `tensorKaehlerEquiv` |
---
[](https://gitpod.io/from-referrer/)
|
t-ring-theory |
83/7 |
Mathlib/RingTheory/Kaehler/TensorProduct.lean |
1 |
16 |
['Ruben-VandeVelde', 'erdOne', 'github-actions', 'mattrobball', 'robin-carlier'] |
mattrobball assignee:mattrobball |
9-68004 9 days ago |
9-68004 9 days ago |
19-50690 19 days |
| 33291 |
BoltonBailey author:BoltonBailey |
refactor(Computability): File for state transition systems |
This PR makes a new file to contain content having to do with state transition systems defined by a function `σ → Option σ`. This content was previously split over `PostTuringMachine.lean` and `TMComputable.lean`, but since these definitions don't only apply to Turing machines in particular, it seems sensible to refactor them and remove them from the `Turing` namespace and put them in a new `StateTransition` namespace.
---
[](https://gitpod.io/from-referrer/)
|
t-computability |
320/233 |
Mathlib.lean,Mathlib/Computability/PostTuringMachine.lean,Mathlib/Computability/StateTransition.lean,Mathlib/Computability/TMConfig.lean,Mathlib/Computability/TMToPartrec.lean,Mathlib/Computability/TuringMachine.lean |
6 |
1 |
['github-actions'] |
nobody |
8-75040 8 days ago |
16-69287 16 days ago |
16-69337 16 days |
| 30758 |
Timeroot author:Timeroot |
chore: tag abs_inv and abs_div with grind= |
---
[](https://gitpod.io/from-referrer/)
|
t-algebra label:t-algebra$ |
2/1 |
Mathlib/Algebra/Order/Field/Basic.lean |
1 |
n/a |
['github-actions'] |
nobody |
81-76040 2 months ago |
unknown |
unknown |
| 33481 |
NoneMore author:NoneMore |
feat(ModelTheory/Encoding): add `Countable` instances for (bounded) formulas in countable languages |
Prepare for the OTT proof.
---
[](https://gitpod.io/from-referrer/)
|
t-logic
new-contributor
|
27/0 |
Mathlib/ModelTheory/Encoding.lean |
1 |
1 |
['github-actions'] |
nobody |
8-43458 8 days ago |
9-25876 9 days ago |
9-25915 9 days |
| 31121 |
jessealama author:jessealama |
feat: add ComplexShape.EulerCharSigns for generalized Euler characteristic |
Add `ComplexShape.EulerCharSigns` typeclass providing the alternating signs `χ : ι → ℤˣ` for Euler characteristic computations. Instances are provided for `up ℕ`, `down ℕ`, `up ℤ`, and `down ℤ`.
The Euler characteristic definitions (`eulerChar` and `eulerCharTsum`) are defined on `GradedObject` with `ComplexShape` as an explicit parameter. The `HomologicalComplex` versions are abbreviations that apply these to `C.X` and `C.homology`. Both finite and infinite sum versions are provided.
Split from #29713 as suggested by @joelriou. |
t-category-theory
t-algebra
label:t-algebra$ |
188/0 |
Mathlib.lean,Mathlib/Algebra/Homology/EulerCharacteristic.lean |
2 |
10 |
['github-actions', 'jessealama', 'joelriou', 'mathlib4-merge-conflict-bot'] |
mattrobball assignee:mattrobball |
8-36338 8 days ago |
15-34908 15 days ago |
30-55399 30 days |
| 32654 |
YaelDillies author:YaelDillies |
feat(Combinatorics): a clique has size at most the chromatic number |
There already exists a version of this lemma for cliques given by a set, but it's impractical to provide an explicit clique on an explicit graph as a set, rather than an indexed family, especially because computing the size of the set would then involve proving that it is the range of an injective function, even though being a clique already implies being injective!
Application: google-deepmind/formal-conjectures#1369
Also rename `coloringOfIsEmpty` and `colorable_of_isEmpty` to leverage anonymous dot notation, and make more arguments implicit.
From FormalConjectures
---
[](https://gitpod.io/from-referrer/)
|
t-combinatorics |
51/40 |
Mathlib/Combinatorics/SimpleGraph/Basic.lean,Mathlib/Combinatorics/SimpleGraph/Coloring.lean |
2 |
20 |
['SnirBroshi', 'YaelDillies', 'github-actions'] |
b-mehta assignee:b-mehta |
8-25149 8 days ago |
33-372 1 month ago |
33-407 33 days |
| 33520 |
NoneMore author:NoneMore |
feat(ModelTheory/ElementarySubstructures): add a variant of Tarski-Vaught test taking sets as input |
There should exist an `ElementarySubstructure.copy` such that we can directly bundle the set itself instaed of its closure as an elementary substructure.
The other direction depends on #33458.
---
[](https://gitpod.io/from-referrer/)
|
t-logic
new-contributor
|
63/0 |
Mathlib/ModelTheory/ElementarySubstructures.lean |
1 |
1 |
['github-actions'] |
nobody |
8-10497 8 days ago |
8-22794 8 days ago |
8-22831 8 days |
| 33523 |
jsm28 author:jsm28 |
feat(Combinatorics/Tiling/Tile): tiles and protosets for tilings |
Start setting up definitions for tilings in a discrete context with definitions of tiles and protosets (indexed families of tiles, predicates meaning such a family is a tiling, and various other properties of such families, are to follow in subsequent PRs).
The module doc string discusses some of the overall design and different definitions that appear in the literature (not strictly limited to the concepts defined in this one file). Here are some overall design choices from a mathlib perspective:
* The discrete and continuous theories are to be developed separately rather than attempting to have a single set of definitions and lemmas that works in both places, so that topological concepts don't need to be involved when working in a discrete context. While some very basic API lemmas might work with analogous proofs for both versions (and the API for continuous tilings *should* follow the lemmas and lemma naming for the discrete case where that makes sense), they would rapidly diverge as soon as even slight mathematical content is involved. For example, in the discrete case, relating weak and strong periodicity typically follows from straightforward properties of the group action, whereas for isometries in Euclidean n-space it needs Bieberbach's first theorem on space groups to show that strongly periodic tilings are also weakly n-periodic.
* The discrete theory is here placed in `Mathlib.Combinatorics.Tiling`, and in a namespace `Discrete`, with the expectation that the continuous theory might them go in `Mathlib.Combinatorics.Tiling.Continuous` with corresponding definitions in a namespace `Continuous` (though other names could be used if preferred).
* The theory is set up in the context of a multiplicative group action (which of course includes but is more general than the case of a group acting on itself). The expectation is that if it's desired to apply it in future with additive group actions, then `to_additive` would be used to set up a corresponding additive version of the theory.
* As discussed in the module doc string, markings on tiles are handled by the combination of defining a protoset as an indexed family (not a set) of prototiles so that otherwise identical prototiles can be distinguished, and each prototile coming with a subgroup of its stablizer so that tiles can be considered to have asymmetrical markings when required. Matching rules are to be handled as predicates on what tilings are considered valid in a given context (together with predicates on those predicates so that results can be stated, for example, as applying with any tiling predicate that only looks at local properties of bounded regions of the tiling).
Zulip discussion: https://leanprover.zulipchat.com/#narrow/channel/116395-maths/topic/Discussion.20-.20Definition.20of.20tilings
From AperiodicMonotilesLean.
---
[](https://gitpod.io/from-referrer/)
|
t-combinatorics |
311/0 |
Mathlib.lean,Mathlib/Combinatorics/Tiling/Tile.lean,docs/references.bib |
3 |
15 |
['Ruben-VandeVelde', 'github-actions', 'jsm28'] |
nobody |
8-3216 8 days ago |
8-5795 8 days ago |
8-5773 8 days |
| 33397 |
themathqueen author:themathqueen |
feat(Topology/Algebra/Star/LinearMap): intrinsic star for continuous linear maps |
---
[](https://gitpod.io/from-referrer/)
|
t-topology
t-algebra
label:t-algebra$ |
100/0 |
Mathlib.lean,Mathlib/Topology/Algebra/Star/LinearMap.lean |
2 |
2 |
['github-actions', 'j-loreaux'] |
ocfnash assignee:ocfnash |
7-59686 7 days ago |
10-77097 10 days ago |
12-49260 12 days |
| 33416 |
vihdzp author:vihdzp |
chore(Order/GameAdd): add `elab_as_elim` attributes |
This PR does three things:
- Rename `GameAdd.fix` to the more illustrative `GameAdd.recursion`
- Add `elab_as_elim` attributes on `GameAdd.recursion`
- Deprecate the duplicate `GameAdd.induction`
---
[](https://gitpod.io/from-referrer/)
|
t-order |
24/14 |
Mathlib/Order/GameAdd.lean,Mathlib/SetTheory/PGame/Order.lean,Mathlib/SetTheory/ZFC/Ordinal.lean |
3 |
1 |
['github-actions'] |
Vierkantor assignee:Vierkantor |
7-59682 7 days ago |
11-56826 11 days ago |
11-56811 11 days |
| 33443 |
sahanwijetunga author:sahanwijetunga |
feat: Define Isometries of Bilinear Spaces |
---
We define Isometries of Bilinear Spaces, closely following the implementation of isometries of quadratic spaces.
[](https://gitpod.io/from-referrer/)
|
t-algebra
new-contributor
label:t-algebra$ |
275/0 |
Mathlib.lean,Mathlib/LinearAlgebra/BilinearForm/Isometry.lean,Mathlib/LinearAlgebra/BilinearForm/IsometryEquiv.lean |
3 |
1 |
['github-actions'] |
dagurtomas assignee:dagurtomas |
7-59680 7 days ago |
10-68343 10 days ago |
10-68385 10 days |
| 33118 |
thomaskwaring author:thomaskwaring |
feat(Combinatorics/SimpleGraph/Acyclic): every graph has a spanning forest. |
We show that every graph has a spanning forest: defined to be an acyclic subgraph with the same reachability relation as the larger graph. As a special case, every connected graph has a spanning tree.
---
Each of these results (spanning forest & spanning tree) are proved in two versions: a general case where the forest / tree is found by extending a given acyclic subgraph, and the special case where that subgraph is empty.
- [ ] depends on: #32043 |
t-combinatorics
new-contributor
|
29/5 |
Mathlib/Combinatorics/SimpleGraph/Acyclic.lean |
1 |
6 |
['SnirBroshi', 'github-actions', 'mathlib4-dependent-issues-bot', 'mathlib4-merge-conflict-bot', 'thomaskwaring', 'vlad902'] |
nobody |
7-57235 7 days ago |
8-46886 8 days ago |
8-50077 8 days |
| 33475 |
BoltonBailey author:BoltonBailey |
feat(Logic/IsEmpty): add theorems relating surjectivity and emptiness |
In particular, this adds a lemma saying that with an empty domain, a function is surjective iff its range is empty, and various forms of this.
---
[](https://gitpod.io/from-referrer/)
|
t-logic |
11/2 |
Mathlib/Logic/IsEmpty.lean |
1 |
13 |
['BoltonBailey', 'SnirBroshi', 'eric-wieser', 'github-actions'] |
nobody |
7-31659 7 days ago |
8-71793 8 days ago |
9-54365 9 days |
| 33435 |
astrainfinita author:astrainfinita |
feat: algebra automorphisms of monoid algebras |
---
[](https://gitpod.io/from-referrer/)
|
t-algebra label:t-algebra$ |
53/3 |
Mathlib/Algebra/MonoidAlgebra/Basic.lean |
1 |
1 |
['github-actions'] |
kbuzzard assignee:kbuzzard |
6-73980 6 days ago |
11-9340 11 days ago |
11-9328 11 days |
| 32886 |
alreadydone author:alreadydone |
refactor(Algebra/Order): change `MulArchimedeanClass.subgroup` to `FiniteArchimedeanClass.subgroup` |
This gets rid of a junk value without much modification the main HahnEmbedding application.
---
[](https://gitpod.io/from-referrer/)
|
t-algebra
t-order
label:t-algebra$ |
298/157 |
Mathlib/Algebra/Order/Archimedean/Class.lean,Mathlib/Algebra/Order/Module/Archimedean.lean,Mathlib/Algebra/Order/Module/HahnEmbedding.lean |
3 |
7 |
['alreadydone', 'github-actions', 'vihdzp', 'wwylele'] |
Vierkantor assignee:Vierkantor |
6-72104 6 days ago |
27-52491 27 days ago |
27-52469 27 days |
| 30981 |
jsm28 author:jsm28 |
feat(Geometry/Euclidean/Angle/Bisector): oriented angle bisection mod π |
Add lemmas relating equal distance to two lines to bisecting the angle between them mod π (expressed as usual as equality of twice angles), building on the previous lemmas (#30477) dealing with bisection mod 2π.
Existing lemmas have hypotheses of the form `(hp' : p' ∈ s₁ ⊓ s₂)` changed to `(hp'₁ : p' ∈ s₁) (hp'₂ : p' ∈ s₂)`, matching new lemmas, on the basis that the natural way to prove the first form is to use proofs of the two separate hypotheses.
---
- [ ] depends on: #30474
- [ ] depends on: #30477
- [ ] depends on: #30600
- [ ] depends on: #30703
[](https://gitpod.io/from-referrer/)
|
t-euclidean-geometry |
207/56 |
Mathlib/Geometry/Euclidean/Angle/Bisector.lean,Mathlib/Geometry/Euclidean/Projection.lean |
2 |
27 |
['JovanGerb', 'eric-wieser', 'github-actions', 'jsm28', 'mathlib4-dependent-issues-bot', 'mathlib4-merge-conflict-bot'] |
JovanGerb assignee:JovanGerb |
6-60779 6 days ago |
53-24269 1 month ago |
57-67500 57 days |
| 33467 |
euprunin author:euprunin |
chore: golf using `grind`. add `grind` annotations. |
---
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):
* `CategoryTheory.Limits.Pi.ι_π`: <10 ms before, 40 ms after
* `CategoryTheory.Limits.Sigma.ι_π`: <10 ms before, 39 ms after
* `Stream'.Seq.head_eq_none_iff`: <10 ms before, 87 ms after
* `Part.mem_ωSup`: 37 ms before, <10 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/)
|
|
10/24 |
Mathlib/CategoryTheory/EqToHom.lean,Mathlib/CategoryTheory/Limits/Shapes/ZeroMorphisms.lean,Mathlib/Data/Seq/Defs.lean,Mathlib/Order/OmegaCompletePartialOrder.lean |
4 |
3 |
['euprunin', 'github-actions', 'leanprover-radar'] |
alexjbest assignee:alexjbest |
6-59677 6 days ago |
9-69326 9 days ago |
9-69303 9 days |
| 33469 |
erdOne author:erdOne |
feat(LinearAlgebra): make TensorProduct.finsuppLeft and friends heterobasic |
---
[](https://gitpod.io/from-referrer/)
|
|
77/137 |
Mathlib/LinearAlgebra/DirectSum/Finsupp.lean,Mathlib/LinearAlgebra/DirectSum/TensorProduct.lean,Mathlib/LinearAlgebra/TensorProduct/Basis.lean,Mathlib/LinearAlgebra/TensorProduct/Submodule.lean,Mathlib/RepresentationTheory/Coinvariants.lean,Mathlib/RepresentationTheory/Rep.lean,Mathlib/RingTheory/Flat/FaithfullyFlat/Basic.lean,Mathlib/RingTheory/Ideal/Quotient/Index.lean,Mathlib/RingTheory/LocalRing/Module.lean,Mathlib/RingTheory/Localization/BaseChange.lean,Mathlib/RingTheory/PicardGroup.lean,Mathlib/RingTheory/TensorProduct/IsBaseChangeFree.lean,Mathlib/RingTheory/TensorProduct/MvPolynomial.lean |
13 |
1 |
['github-actions'] |
mariainesdff assignee:mariainesdff |
6-59676 6 days ago |
9-68982 9 days ago |
9-68959 9 days |
| 33470 |
erdOne author:erdOne |
feat: generalize `Polynomial.freeMonic` |
---
[](https://gitpod.io/from-referrer/)
|
|
80/52 |
Mathlib.lean,Mathlib/Algebra/Polynomial/FreeMonic.lean,Mathlib/RingTheory/Polynomial/UniversalFactorizationRing.lean |
3 |
1 |
['github-actions'] |
thorimur assignee:thorimur |
6-59676 6 days ago |
9-68927 9 days ago |
9-68904 9 days |
| 29235 |
yoh-tanimoto author:yoh-tanimoto |
feat(Topology/Algebra/Module/ClosedSubmodule): add `mapEquiv`, a variation of `ClosedSubmodule.map` for CLE |
add `ClosedSubmodule.mapEquiv` for continuous linear equivalence. In this case, a closed submodule is mapped to a closed submodule, so the definitions are easier and behave nicely with `closure` and `⊔`.
motivation: needed to define standard subspaces in a Hilbert space (scalar multiplication by `Complex.I`) #29251
https://ems.press/content/serial-article-files/48171
- [x] depends on: #29230 for `Lattice` `CompleteLattice` |
t-topology |
76/1 |
Mathlib/Topology/Algebra/Module/ClosedSubmodule.lean |
1 |
3 |
['github-actions', 'mathlib4-dependent-issues-bot', 'mathlib4-merge-conflict-bot'] |
fpvandoorn assignee:fpvandoorn |
6-52557 6 days ago |
6-58034 6 days ago |
74-28615 74 days |
| 33039 |
euprunin author:euprunin |
chore(Data/List): deprecate `ext_get_iff` |
---
[](https://gitpod.io/from-referrer/)
|
t-data |
1/7 |
Mathlib/Data/List/Basic.lean |
1 |
5 |
['euprunin', 'github-actions', 'jcommelin'] |
pechersky assignee:pechersky |
6-25171 6 days ago |
16-70407 16 days ago |
17-51777 17 days |
| 33599 |
nielstron author:nielstron |
feat(Computability/ContextFreeGrammar): closure under union |
---
This PR picks up https://github.com/leanprover-community/mathlib4/pull/13514 and resolves the outstanding errors.
- [ ] depends on #33592
[](https://gitpod.io/from-referrer/)
|
new-contributor
t-computability
|
506/0 |
Mathlib/Computability/ContextFreeGrammar.lean |
1 |
1 |
['github-actions'] |
nobody |
6-7176 6 days ago |
6-17637 6 days ago |
6-17682 6 days |
| 33490 |
YaelDillies author:YaelDillies |
refactor(Data/Finsupp): remove `DecidableEq` argument from `curry` |
This is motivated by it spuriously requiring extra decidability assumptions in group cohomology.
This partially reverts #24746. No motivation was given there for why computability was necessary. `Finsupp.curry` will be made computable again anyway once `Finsupp` is redefined to be `DFinsupp`.
From ClassFieldTheory
---
[](https://gitpod.io/from-referrer/)
|
t-data
CFT
|
15/21 |
Mathlib/Data/Finsupp/Basic.lean,Mathlib/LinearAlgebra/Finsupp/Defs.lean,Mathlib/LinearAlgebra/Finsupp/LinearCombination.lean,Mathlib/RepresentationTheory/Homological/GroupCohomology/Basic.lean,Mathlib/RepresentationTheory/Homological/GroupCohomology/FiniteCyclic.lean,Mathlib/RepresentationTheory/Homological/GroupCohomology/Shapiro.lean,Mathlib/RepresentationTheory/Homological/Resolution.lean,Mathlib/RepresentationTheory/Rep.lean,Mathlib/RingTheory/AlgebraTower.lean |
9 |
5 |
['YaelDillies', 'eric-wieser', 'github-actions', 'tb65536'] |
nobody |
5-78450 5 days ago |
8-80320 8 days ago |
8-80299 8 days |
| 33100 |
themathqueen author:themathqueen |
refactor(Algebra/Order/Field/Basic): generalize file from `LinearOrder` to `PartialOrder` and `PosMulReflectLT` |
It's a well-known easy fact that there is no way to equip `ℂ` with a *linear* order satisfying `IsStrictOrderedRing`. However, it is equipped with a partial order (available in the `ComplexOrder` namespace) given by `a ≤ b ↔ a.re ≤ b.re ∧ a.im = b.im`. This order satisfies `IsStrictOrderedRing`. However, it has some other nice properties, for instance `0 < a⁻¹ ↔ 0 < a` (because it is a `GroupWithZero` satisfying `PosMulReflectLT` so `inv_pos` applies), and moreover, in this PR we also show that a (partially) ordered field with this property satisfies `a⁻¹ < 0 ↔ a < 0`. This means that the field operation is well-behaved in regards to elements comparable with zero.
This PR refactors `Algebra/Order/Field/Basic.lean` so that it applies to *partially* ordered fields that in addition satisfy `PosMulReflectLT` (e.g., `ℂ`). The vast majority of the lemmas are applicable in this more general setting, albeit with refactored proofs.
The diff is a bit messy, but it's easy to understand with the right point-of-view:
1. lemmas which require linear orders are grouped into their own sections below the corresponding sections for partially ordered fields
2. proofs are refactored with the weaker hypotheses
3. a few lemmas near the top didn't actually need `IsStrictOrderedRing`, so those are grouped at the top.
4. The only new declarations added are `inv_lt_zero'` and `inv_nonpos'`, no others were deleted or changed (aside from weakening type class assumptions).
5. The positivity extension at the bottom of the file has its type class requirements weakened so that it applies in more contexts.
Co-authored-by: Jireh Loreaux
---
[](https://gitpod.io/from-referrer/)
|
t-algebra label:t-algebra$ |
180/131 |
Mathlib/Algebra/Order/Field/Basic.lean |
1 |
6 |
['github-actions', 'j-loreaux', 'leanprover-radar', 'mathlib4-merge-conflict-bot', 'themathqueen'] |
dagurtomas assignee:dagurtomas |
5-76630 5 days ago |
5-76658 5 days ago |
22-81740 22 days |
| 30144 |
alreadydone author:alreadydone |
feat(Data/Nat): kernel reducible binaryRec |
+ Redefine `Nat.binaryRec` to allow kernel reduction.
+ Move some lemmas from Data/Nat/Bitwise to Data/Nat/BinaryRec.
+ Use `nsmulBinRec` for nsmul/zsmul on elliptic curves.
---
[](https://gitpod.io/from-referrer/)
|
t-algebra
t-data
label:t-algebra$ |
119/60 |
Mathlib/Algebra/Group/Defs.lean,Mathlib/Algebra/Group/Prod.lean,Mathlib/AlgebraicGeometry/EllipticCurve/Affine/Point.lean,Mathlib/Data/Nat/BinaryRec.lean,Mathlib/Data/Nat/BitIndices.lean,Mathlib/Data/Nat/Bits.lean,Mathlib/Data/Nat/Bitwise.lean,Mathlib/Data/Nat/Digits/Defs.lean,Mathlib/Data/Nat/Size.lean |
9 |
12 |
['alreadydone', 'astrainfinita', 'github-actions', 'leanprover-bot', 'leanprover-community-mathlib4-bot', 'mathlib4-merge-conflict-bot'] |
pechersky assignee:pechersky |
5-62138 5 days ago |
6-276 6 days ago |
65-39478 65 days |
| 33458 |
NoneMore author:NoneMore |
feat(ModelTheory): add lifting for embeddings to languages with constants |
Prepare for a generalized Tarski-Vaught test with a set as input instead of a substructure.
---
[](https://gitpod.io/from-referrer/)
|
t-logic
new-contributor
|
46/0 |
Mathlib/ModelTheory/ElementaryMaps.lean,Mathlib/ModelTheory/LanguageMap.lean |
2 |
1 |
['github-actions'] |
fpvandoorn assignee:fpvandoorn |
5-59697 5 days ago |
10-4230 10 days ago |
10-4271 10 days |
| 33487 |
gasparattila author:gasparattila |
feat(Topology/UniformSpace): `SetRel.{inv,image,preimage}` of `entourageProd` |
---
[](https://gitpod.io/from-referrer/)
|
t-topology |
15/0 |
Mathlib/Topology/UniformSpace/Basic.lean |
1 |
1 |
['github-actions'] |
dagurtomas assignee:dagurtomas |
5-59692 5 days ago |
9-6141 9 days ago |
9-6184 9 days |
| 33494 |
vihdzp author:vihdzp |
feat(RingTheory/HahnSeries/Basic): more theorems on `order`/`orderTop` |
We also deprecate various badly named or overspecific theorems relating to `ofSuppBddBelow`.
---
[](https://gitpod.io/from-referrer/)
|
t-ring-theory |
64/32 |
Mathlib/Algebra/Vertex/VertexOperator.lean,Mathlib/RingTheory/HahnSeries/Basic.lean,Mathlib/RingTheory/LaurentSeries.lean |
3 |
1 |
['github-actions'] |
mattrobball assignee:mattrobball |
5-59691 5 days ago |
8-63742 8 days ago |
8-63732 8 days |
| 31046 |
Thmoas-Guan author:Thmoas-Guan |
feat(Homology) : compatibility of map between `Ext` |
In this PR, we proved the compatibility of map between `Ext` induced by exact functor with
1: `mk_0` 2: `comp` 3: `extClass`
---
- [ ] depends on: #31707
[](https://gitpod.io/from-referrer/) |
t-category-theory |
210/0 |
Mathlib/Algebra/Homology/DerivedCategory/Ext/Map.lean,Mathlib/Algebra/Homology/DerivedCategory/ShortExact.lean,Mathlib/Algebra/Homology/HomotopyCategory/Pretriangulated.lean,Mathlib/Algebra/Homology/HomotopyCategory/ShortExact.lean |
4 |
7 |
['Thmoas-Guan', 'github-actions', 'joelriou', 'mathlib4-dependent-issues-bot', 'mathlib4-merge-conflict-bot'] |
eric-wieser assignee:eric-wieser |
5-30621 5 days ago |
5-31198 5 days ago |
9-34517 9 days |
| 31891 |
jsm28 author:jsm28 |
feat(Geometry/Euclidean/Sphere/OrthRadius): lemmas for setting up and using polars |
Add further lemmas about `orthRadius` that are of use in setting up and using poles and polars. In particular,
`ncard_inter_orthRadius_eq_two_of_dist_lt_radius` is the key part of showing that, in two dimensions, there are exactly two tangents to a circle from a point outside that circle (where the points of tangency lie on the polar of the point from which the two tangents are drawn).
---
Feel free to golf the proof of `ncard_inter_orthRadius_eq_two_of_dist_lt_radius`, it could probably be rather shorter.
---
- [ ] depends on: #32296
[](https://gitpod.io/from-referrer/)
|
t-euclidean-geometry |
185/7 |
Mathlib/Geometry/Euclidean/Sphere/OrthRadius.lean,Mathlib/Geometry/Euclidean/Sphere/Tangent.lean |
2 |
26 |
['eric-wieser', 'github-actions', 'jsm28', 'mathlib4-dependent-issues-bot'] |
JovanGerb assignee:JovanGerb |
5-21880 5 days ago |
41-19844 1 month ago |
50-64595 50 days |
| 32316 |
Thmoas-Guan author:Thmoas-Guan |
feat(Homology/ModuleCat): Dimension Shifting tools in ModuleCat |
In this PR we present some dimension shifting tools in `ModuleCat`.
---
- [x] depends on: #32312
[](https://gitpod.io/from-referrer/)
|
t-category-theory
t-algebra
label:t-algebra$ |
132/0 |
Mathlib.lean,Mathlib/Algebra/Category/ModuleCat/Ext/DimensionShifting.lean,Mathlib/Algebra/Homology/DerivedCategory/Ext/EnoughInjectives.lean,Mathlib/Algebra/Homology/DerivedCategory/Ext/EnoughProjectives.lean,Mathlib/Algebra/Homology/ShortComplex/ModuleCat.lean,Mathlib/RingTheory/Noetherian/Basic.lean |
6 |
20 |
['Thmoas-Guan', 'erdOne', 'github-actions', 'jcommelin', 'joelriou', 'mathlib4-dependent-issues-bot', 'mathlib4-merge-conflict-bot'] |
joelriou assignee:joelriou |
5-20362 5 days ago |
13-26062 13 days ago |
13-51856 13 days |
| 32959 |
CBirkbeck author:CBirkbeck |
feat(NumberTheory/ModularForms/QExpansion): define qExpansion ring hom and some more API |
We construct the ring homomorphism from the graded ring of modular forms to power series. We prove develop some basic API for this and also prove the qExpansion coefficients are unique, which is useful to extracting the actual qExpansions of Eisenstein series.
---
[](https://gitpod.io/from-referrer/)
|
t-number-theory |
410/6 |
Mathlib/Analysis/Calculus/Deriv/Mul.lean,Mathlib/Analysis/Calculus/IteratedDeriv/Lemmas.lean,Mathlib/NumberTheory/ModularForms/QExpansion.lean |
3 |
1 |
['github-actions'] |
loefflerd assignee:loefflerd |
5-14811 5 days ago |
5-15733 5 days ago |
26-11478 26 days |
| 33431 |
gululu996-ui author:gululu996-ui |
feat(Combinatorics/SimpleGraph/Bipartite): characterize bipartite simplegraphs by even cycles |
Add the classical characterization of bipartite simple graphs: a simple graph is bipartite if and only if every cycle has even length.
Previously, mathlib has the definition of `IsBipartite` for `SimpleGraph` and various lemmas about bipartite graphs, but it does not provide this equivalence in a single theorem, so users have to reprove or reassemble it from existing results.
Prove the forward direction by showing a 2-coloring alternates along any walk, so every cycle must have even length. Prove the converse by showing that if an odd cycle exists then no bipartition is possible, hence if all cycles are even the graph admits a bipartition.
|
t-combinatorics
new-contributor
|
185/1 |
Mathlib/Combinatorics/SimpleGraph/Bipartite.lean |
1 |
3 |
['NickAdfor', 'github-actions'] |
nobody |
5-12989 5 days ago |
7-16264 7 days ago |
11-17948 11 days |
| 33592 |
nielstron author:nielstron |
feat(Computability/ContextFreeGrammar): mapping between two types of nonterminal symbols |
---
This PR picks up https://github.com/leanprover-community/mathlib4/pull/15895 and resolves the failing lemma by redefining Good symbols. I checked that https://github.com/leanprover-community/mathlib4/pull/13514 builds correctly when based on this build. PR for that is #33599
This is my first contribution please let me know of any changes I should outline.
[](https://gitpod.io/from-referrer/)
|
new-contributor
t-computability
|
162/0 |
Mathlib/Computability/ContextFreeGrammar.lean |
1 |
1 |
['github-actions', 'madvorak'] |
nobody |
5-8810 5 days ago |
6-18184 6 days ago |
6-18713 6 days |
| 31560 |
AntoineChambert-Loir author:AntoineChambert-Loir |
feat(Topology/Sion): the minimax theorem of von Neumann - Sion |
Prove `Sion.exists_isSaddlePointOn` :
Let X and Y be convex subsets of topological vector spaces E and F,
X being moreover compact,
and let f : X × Y → ℝ be a function such that
- for all x, f(x, ⬝) is upper semicontinuous and quasiconcave
- for all y, f(⬝, y) is lower semicontinuous and quasiconvex
Then inf_x sup_y f(x,y) = sup_y inf_x f(x,y).
The classical case of the theorem assumes that f is continuous,
f(x, ⬝) is concave, f(⬝, y) is convex.
As a particular case, one get the von Neumann theorem where
f is bilinear and E, F are finite dimensional.
We follow the proof of Komiya (1988).
## Remark on implementation
* The essential part of the proof holds for a function
`f : X → Y → β`, where `β` is a complete dense linear order.
* We have written part of it for just a dense linear order,
* On the other hand, if the theorem holds for such `β`,
it must hold for any linear order, for the reason that
any linear order embeds into a complete dense linear order.
However, this result does not seem to be known to Mathlib.
* When `β` is `ℝ`, one can use `Real.toEReal` and one gets a proof for `ℝ`.
## TODO
Give particular important cases (eg, bilinear maps in finite dimension).
Co-authored with @ADedecker
---
- [x] depends on: #31548
- [x] depends on: #31547
- [x] depends on: #31558
[](https://gitpod.io/from-referrer/)
|
t-topology |
741/0 |
Mathlib.lean,Mathlib/Data/EReal/Basic.lean,Mathlib/Topology/Semicontinuity/Basic.lean,Mathlib/Topology/Sion.lean,docs/references.bib |
5 |
8 |
['AntoineChambert-Loir', 'github-actions', 'mathlib4-dependent-issues-bot', 'mathlib4-merge-conflict-bot', 'thorimur'] |
dwrensha and kmill assignee:kmill assignee:dwrensha |
5-43 5 days ago |
23-64468 23 days ago |
31-68328 31 days |
| 33286 |
euprunin author:euprunin |
chore: golf using `grind` |
---
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):
* `Finset.memberSubfamily_union_nonMemberSubfamily`: 11 ms before, 116 ms after
* `AkraBazziRecurrence.GrowsPolynomially.eventually_atTop_nonneg_or_nonpos`: 1181 ms before, 1194 ms after
* `Equiv.Perm.support_congr`: <10 ms before, 38 ms after
* `Equiv.Perm.subtypeCongr.trans`: 13 ms before, 35 ms after
* `preCantorSet_antitone`: 766 ms before, 371 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/)
|
|
6/28 |
Mathlib/Computability/AkraBazzi/GrowsPolynomially.lean,Mathlib/GroupTheory/Perm/Support.lean,Mathlib/Logic/Equiv/Basic.lean,Mathlib/Topology/Instances/CantorSet.lean |
4 |
5 |
['euprunin', 'github-actions', 'vihdzp'] |
thorimur assignee:thorimur |
4-81361 4 days ago |
4-81980 4 days ago |
16-55254 16 days |
| 33492 |
YaelDillies author:YaelDillies |
feat(Algebra/MonoidAlgebra): `R[M][N] ≃+* R[N][M]` |
Prove that `R[M × N] ≃+* R[N][M]` and deduce that `R[M][N] ≃+* R[N][M]`. Add supporting `Finsupp` lemmas.
The ugly proofs are transitional and will be reworked in and after #25273.
---
- [x] depends on: #33516
- [x] depends on: #33521
[](https://gitpod.io/from-referrer/)
|
t-algebra label:t-algebra$ |
125/12 |
Mathlib/Algebra/BigOperators/Finsupp/Basic.lean,Mathlib/Algebra/Group/Finsupp.lean,Mathlib/Algebra/MonoidAlgebra/Basic.lean,Mathlib/Algebra/MonoidAlgebra/Defs.lean,Mathlib/Algebra/MonoidAlgebra/MapDomain.lean |
5 |
21 |
['YaelDillies', 'eric-wieser', 'github-actions', 'mathlib4-dependent-issues-bot', 'mathlib4-merge-conflict-bot'] |
mattrobball assignee:mattrobball |
4-59693 4 days ago |
7-75355 7 days ago |
8-41759 8 days |
| 32134 |
mitchell-horner author:mitchell-horner |
feat(Topology/Real): theorems linking `IsGLB` with `BddBelow`, `Antitone`, `Tendsto _ atTop` |
Implement theorems linking `IsGLB` (`IsLUB`) with `BddBelow` (`BddAbove`), `Antitone` (`Monotone`), `Tendsto _ atTop`
---
[](https://gitpod.io/from-referrer/)
|
t-topology
maintainer-merge
large-import
|
124/69 |
Mathlib/Algebra/Order/Monoid/Canonical/Basic.lean,Mathlib/Analysis/Normed/Unbundled/SeminormFromConst.lean,Mathlib/Analysis/Normed/Unbundled/SpectralNorm.lean,Mathlib/Topology/Instances/NNReal/Lemmas.lean,Mathlib/Topology/Instances/Real/Lemmas.lean |
5 |
24 |
['YaelDillies', 'github-actions', 'mitchell-horner'] |
YaelDillies assignee:YaelDillies |
4-18319 4 days ago |
4-18319 4 days ago |
36-54621 36 days |
| 33192 |
linesthatinterlace author:linesthatinterlace |
refactor(Data/List/Induction): improve definition of `reverseRecOn` |
This PR improves the definition of `List.reverseRecOn`.
---
This improved approach aims to give identical behavior but give a somewhat nicer proof of `List.reverseRecOn_concat`. I do not believe it is a regression in terms of performance.
The approach is inspired by `biDirectionalRec`, for which I have also tweaked the definitions and proofs, albeit in a much more minor way.
[](https://gitpod.io/from-referrer/)
|
t-data |
32/27 |
Mathlib/Data/List/Induction.lean |
1 |
6 |
['github-actions', 'linesthatinterlace', 'vihdzp'] |
pechersky assignee:pechersky |
4-7488 4 days ago |
20-22352 20 days ago |
20-22392 20 days |
| 32811 |
erdOne author:erdOne |
feat(RingTheory): predicate on satisfying Zariski's main theorem |
---
[](https://gitpod.io/from-referrer/)
|
t-ring-theory |
179/0 |
Mathlib.lean,Mathlib/Algebra/Algebra/Subalgebra/Lattice.lean,Mathlib/RingTheory/Localization/Away/Basic.lean,Mathlib/RingTheory/ZariskisMainTheorem.lean |
4 |
9 |
['erdOne', 'github-actions', 'joelriou'] |
alreadydone assignee:alreadydone |
4-787 4 days ago |
26-84341 26 days ago |
29-71304 29 days |
| 33194 |
YuvalFilmus author:YuvalFilmus |
feat(LinearAlgebra/Lagrange): refactored proof of leadingCoeff_eq_sum |
The proof of `leadingCoeff_eq_sum` was slightly refactored.
A subsequent PR will use the refactored parts to prove a formula for the iterated derivative of a polynomial at a point.
---
[](https://gitpod.io/from-referrer/)
|
t-algebra label:t-algebra$ |
22/22 |
Mathlib/LinearAlgebra/Lagrange.lean |
1 |
6 |
['Ruben-VandeVelde', 'YuvalFilmus', 'github-actions'] |
dagurtomas assignee:dagurtomas |
3-71639 3 days ago |
20-21041 20 days ago |
20-21092 20 days |
| 33288 |
vihdzp author:vihdzp |
chore(Combinatorics/SimpleGraph/Paths): review API |
This PR does the following:
- Add `grind` annotations.
- Rename theorems `X_isY` to the more idiomatic `isY_X`.
- Remove many redundant namespaces.
- Golf accordingly.
---
[](https://gitpod.io/from-referrer/)
|
t-combinatorics |
154/122 |
Mathlib/Combinatorics/SimpleGraph/Acyclic.lean,Mathlib/Combinatorics/SimpleGraph/Connectivity/Connected.lean,Mathlib/Combinatorics/SimpleGraph/Matching.lean,Mathlib/Combinatorics/SimpleGraph/Metric.lean,Mathlib/Combinatorics/SimpleGraph/Paths.lean,Mathlib/Combinatorics/SimpleGraph/Walks/Maps.lean |
6 |
2 |
['github-actions', 'mathlib4-merge-conflict-bot'] |
nobody |
3-67126 3 days ago |
3-67146 3 days ago |
7-17671 7 days |
| 33336 |
fbarroero author:fbarroero |
feat(NumberTheory/MahlerMeasure): Kronecker's Theorem for the Mahler Measure |
This PR adds Kronecker's Theorem for the Mahler Measure, which characterizes integer polynomials with Mahler measure equal to 1. The key mathematical contribution is proving that such polynomials have all their nonzero complex roots as roots of unity, and consequently must be divisible by cyclotomic polynomials.
Main result
```
Polynomial.pow_eq_one_of_mahlerMeasure_eq_one {p : ℤ[X]} (h : (map (castRingHom ℂ) p).mahlerMeasure = 1)
{z : ℂ} (hz₀ : z ≠ 0) (hz : z ∈ p.aroots ℂ) : ∃ n, 0 < n ∧ z ^ n = 1
```
---
[](https://gitpod.io/from-referrer/)
|
|
128/9 |
Mathlib/Algebra/Order/BigOperators/Ring/Multiset.lean,Mathlib/NumberTheory/MahlerMeasure.lean |
2 |
11 |
['copilot-pull-request-reviewer', 'github-actions', 'mathlib4-merge-conflict-bot'] |
tb65536 assignee:tb65536 |
3-61179 3 days ago |
8-865 8 days ago |
11-5621 11 days |
| 33633 |
mcdoll author:mcdoll |
chore(Analysis/Fourier): split type class, add continuity one |
The combined type-class `FourierModule` causes problems when using `fourier_add` since it needs a `Semiring R`, which does not appear in the statement. Therefore, we split `FourierModule` into `FourierAdd` and `FourierSMul` (similar to the case of `LineDeriv`.
Moreover, we add the class `ContinuousFourier` which states that the Fourier transform is continuous.
---
[](https://gitpod.io/from-referrer/)
|
t-analysis
large-import
|
195/77 |
Mathlib/Analysis/Distribution/FourierSchwartz.lean,Mathlib/Analysis/Distribution/TemperedDistribution.lean,Mathlib/Analysis/Fourier/LpSpace.lean,Mathlib/Analysis/Fourier/Notation.lean |
4 |
1 |
['github-actions'] |
nobody |
3-60244 3 days ago |
3-60313 3 days ago |
5-66581 5 days |
| 28708 |
sjh227 author:sjh227 |
feat(LinearAlgebra): define row- and column-stochastic matrices |
This PR defines row- and column-stochastic matrices, and relates them to doubly stochastic matrices (which are already in mathlib).
---
|
new-contributor
t-data
|
255/6 |
Mathlib.lean,Mathlib/Algebra/Group/Submonoid/Defs.lean,Mathlib/Analysis/Convex/DoublyStochasticMatrix.lean,Mathlib/LinearAlgebra/Matrix/Stochastic.lean |
4 |
29 |
['dupuisf', 'github-actions', 'j-loreaux', 'mathlib4-merge-conflict-bot', 'sjh227'] |
pechersky assignee:pechersky |
3-59708 3 days ago |
6-71959 6 days ago |
7-63558 7 days |
| 31854 |
erdOne author:erdOne |
chore(AlgebraicGeometry): API for `𝒪ₓ`-modules |
---
[](https://gitpod.io/from-referrer/)
|
t-algebraic-geometry |
430/18 |
Mathlib/Algebra/Category/ModuleCat/ChangeOfRings.lean,Mathlib/Algebra/Category/ModuleCat/Presheaf/Colimits.lean,Mathlib/Algebra/Category/ModuleCat/Presheaf/Limits.lean,Mathlib/Algebra/Category/ModuleCat/Sheaf/Colimits.lean,Mathlib/Algebra/Category/ModuleCat/Sheaf/PullbackContinuous.lean,Mathlib/Algebra/Category/ModuleCat/Sheaf/PushforwardContinuous.lean,Mathlib/AlgebraicGeometry/Modules/Sheaf.lean,Mathlib/AlgebraicGeometry/OpenImmersion.lean |
8 |
4 |
['erdOne', 'github-actions', 'joelriou', 'mathlib4-merge-conflict-bot'] |
dagurtomas assignee:dagurtomas |
3-59706 3 days ago |
7-47471 7 days ago |
8-30738 8 days |
| 33372 |
kex-y author:kex-y |
feat(Probability): Countable infimum of stopping times is a stopping time |
---
- [x] depends on: #33371
[](https://gitpod.io/from-referrer/)
|
t-measure-probability
brownian
|
83/0 |
Mathlib/Probability/Process/Stopping.lean |
1 |
3 |
['github-actions', 'mathlib4-dependent-issues-bot', 'mathlib4-merge-conflict-bot'] |
RemyDegenne assignee:RemyDegenne |
3-59702 3 days ago |
7-12761 7 days ago |
7-18628 7 days |
| 33436 |
astrainfinita author:astrainfinita |
feat: lemmas about `(Add)MonoidAlgebra.mapRangeRingHom` |
---
[](https://gitpod.io/from-referrer/)
|
t-algebra label:t-algebra$ |
21/0 |
Mathlib/Algebra/MonoidAlgebra/Basic.lean,Mathlib/Algebra/MonoidAlgebra/MapDomain.lean |
2 |
2 |
['github-actions', 'mathlib4-merge-conflict-bot'] |
chrisflav assignee:chrisflav |
3-59701 3 days ago |
6-74647 6 days ago |
9-64927 9 days |
| 33544 |
YaelDillies author:YaelDillies |
chore(LinearAlgebra): make one more argument implicit in `ker_toSpanSingleton` |
`M` can be inferred from `x : M` which can be inferred from `h : x ≠ 0`. Similarly for `ker_toSpanSingleton_eq_bot_iff`.
---
[](https://gitpod.io/from-referrer/)
|
t-algebra label:t-algebra$ |
5/5 |
Mathlib/LinearAlgebra/Span/Basic.lean,Mathlib/RingTheory/SimpleModule/Basic.lean,Mathlib/RingTheory/WittVector/Isocrystal.lean,Mathlib/Topology/Algebra/Module/FiniteDimension.lean |
4 |
2 |
['artie2000', 'github-actions'] |
joelriou assignee:joelriou |
3-59696 3 days ago |
7-28108 7 days ago |
7-28094 7 days |
| 32617 |
erdOne author:erdOne |
feat(RingTheory): field extension over perfect fields are smooth |
---
[](https://gitpod.io/from-referrer/)
|
t-ring-theory |
150/18 |
Mathlib.lean,Mathlib/FieldTheory/IntermediateField/Adjoin/Algebra.lean,Mathlib/FieldTheory/IntermediateField/Adjoin/Defs.lean,Mathlib/FieldTheory/SeparableClosure.lean,Mathlib/FieldTheory/SeparablyGenerated.lean,Mathlib/RingTheory/EssentialFiniteness.lean,Mathlib/RingTheory/Smooth/Field.lean |
7 |
6 |
['chrisflav', 'erdOne', 'github-actions', 'robin-carlier'] |
chrisflav assignee:chrisflav |
3-53844 3 days ago |
3-53905 3 days ago |
14-2684 14 days |
| 33741 |
mcdoll author:mcdoll |
feat(Analysis/SchwartzSpace): additional lemmas for `smulLeftCLM` |
Add various lemmas for `smulLeftCLM`.
---
The lemma for the sum could be proved with induction, but that proof is slightly longer.
[](https://gitpod.io/from-referrer/)
|
t-analysis |
58/3 |
Mathlib/Analysis/Distribution/SchwartzSpace.lean |
1 |
1 |
['github-actions'] |
nobody |
3-49035 3 days ago |
3-49505 3 days ago |
3-49556 3 days |
| 33033 |
kim-em author:kim-em |
feat(Tactic/Choose): add type annotation support |
This PR adds support for type annotations in the `choose` tactic, similar to how `intro` supports them. This allows writing:
```lean
choose (n : ℕ) (hn : n > 0) using h
```
instead of just `choose n hn using h`. The type annotation is checked against the actual type from the existential, and an error is raised if they don't match.
This is useful for pedagogical purposes and for catching mistakes early.
Requested on Zulip: https://leanprover.zulipchat.com/#narrow/channel/187764-Lean-for-teaching/topic/adding.20type.20annotation.20to.20.60choose.60/near/564323626
🤖 Prepared with Claude Code |
t-meta |
170/22 |
Mathlib/Tactic/Choose.lean,MathlibTest/choose.lean |
2 |
20 |
['AlexKontorovich', 'eric-wieser', 'fpvandoorn', 'github-actions', 'kim-em'] |
joneugster assignee:joneugster |
3-43516 3 days ago |
22-70508 22 days ago |
23-54909 23 days |
| 33745 |
euprunin author:euprunin |
chore: golf proofs |
---
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):
* `LinearGrowth.linearGrowthInf_comp_nonneg`: 29 ms before, 17 ms after 🎉
* `CategoryTheory.Limits.preservesLimit_of_preservesEqualizers_and_product`: 821 ms before, 530 ms after 🎉
* `CategoryTheory.Limits.Pi.map_eq_prod_map`: 161 ms before, 101 ms after 🎉
* `CategoryTheory.isCardinalPresentable_of_equivalence`: 116 ms before, 107 ms after 🎉
* `SimpleGraph.nontrivial_of_diam_ne_zero`: <10 ms before, <10 ms after 🎉
* `univ_eq_singleton_of_card_one`: 14 ms before, <10 ms after 🎉
* `CoxeterSystem.getElem_leftInvSeq_alternatingWord`: 41 ms before, 40 ms after 🎉
* `Matrix.SpecialLinearGroup.mapGL_inj`: 73 ms before, 45 ms after 🎉
* `PiTensorProduct.reindex_refl`: 88 ms before, 65 ms after 🎉
* `MeasureTheory.continuous_diracProbaEquivSymm`: 17 ms before, <10 ms after 🎉
* `Representation.ofModule_asModule_act`: 78 ms before, 61 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/)
|
|
6/21 |
Mathlib/Analysis/Asymptotics/LinearGrowth.lean,Mathlib/CategoryTheory/Limits/Constructions/LimitsOfProductsAndEqualizers.lean,Mathlib/CategoryTheory/Limits/Shapes/PiProd.lean,Mathlib/CategoryTheory/Presentable/Basic.lean,Mathlib/Combinatorics/SimpleGraph/Diam.lean,Mathlib/Data/Fintype/Card.lean,Mathlib/GroupTheory/Coxeter/Inversion.lean,Mathlib/LinearAlgebra/Matrix/GeneralLinearGroup/Defs.lean,Mathlib/LinearAlgebra/PiTensorProduct.lean,Mathlib/RepresentationTheory/Basic.lean |
10 |
1 |
['github-actions'] |
nobody |
3-30003 3 days ago |
3-30087 3 days ago |
3-30064 3 days |
| 27599 |
mitchell-horner author:mitchell-horner |
feat(Combinatorics/SimpleGraph): define `CompleteEquipartiteSubgraph` |
Define the complete equipartite subgraphs in `r` parts each of size `t` in `G` as the `r` subsets of vertices each of size `t` such that vertices in distinct subsets are adjacent.
In this case `Nonempty (G.CompleteEquipartiteSubgraph r t)` is equivalent to `completeEquipartiteGraph r t ⊑ G`, that is, finding `r` subsets of vertices each of size `t` in `G` such that vertices in distinct subsets are adjacent is equivalent to finding an injective homomorphism from `completeEquipartiteGraph r t` to `G`.
---
- [x] depends on: #27597
- [x] depends on: #30287
[](https://gitpod.io/from-referrer/)
|
t-combinatorics |
173/7 |
Mathlib/Combinatorics/SimpleGraph/CompleteMultipartite.lean |
1 |
34 |
['YaelDillies', 'b-mehta', 'github-actions', 'mathlib4-dependent-issues-bot', 'mathlib4-merge-conflict-bot', 'mitchell-horner'] |
YaelDillies assignee:YaelDillies |
3-24273 3 days ago |
4-59157 4 days ago |
75-21973 75 days |
| 33751 |
mcdoll author:mcdoll |
feat(Analysis/FourierSchwartz): self-adjointness for the inverse Fourier transform |
This follows trivially from the facts about the Fourier transform and the inversion formula.
In passing, we fix a doc-string.
---
[](https://gitpod.io/from-referrer/)
|
t-analysis |
20/1 |
Mathlib/Analysis/Distribution/FourierSchwartz.lean |
1 |
1 |
['github-actions'] |
nobody |
3-20377 3 days ago |
3-20377 3 days ago |
3-20423 3 days |
| 33752 |
mcdoll author:mcdoll |
feat(Analysis/FourierSchwartz): the derivative of the Fourier transform |
Calculate the derivative (`fderiv` and `lineDerivOp`) of the (inverse) Fourier transform.
We also generalize `evalCLM` slightly and make it's arguments explicit.
---
[](https://gitpod.io/from-referrer/)
|
t-analysis |
90/9 |
Mathlib/Analysis/Distribution/FourierSchwartz.lean,Mathlib/Analysis/Distribution/SchwartzSpace.lean |
2 |
1 |
['github-actions'] |
nobody |
3-20236 3 days ago |
3-20236 3 days ago |
3-20285 3 days |
| 33743 |
jcommelin author:jcommelin |
ci: add automated commit verification |
This PR adds verification for "x: " commits that checks whether re-running the command produces the same tree.
Written with the help of Claude Code.
---
[](https://gitpod.io/from-referrer/)
|
CI |
406/28 |
.github/workflows/commit_verification.yml,scripts/README.md,scripts/verify_commits.sh,scripts/verify_commits_summary.sh |
4 |
6 |
['Vierkantor', 'github-actions', 'jcommelin'] |
nobody |
3-17262 3 days ago |
3-35676 3 days ago |
3-35716 3 days |
| 33449 |
yuanyi-350 author:yuanyi-350 |
feat(ProbabilityTheory): Add Poisson limit theorem |
---
[](https://gitpod.io/from-referrer/)
|
t-measure-probability |
145/2 |
Mathlib.lean,Mathlib/Probability/Distributions/Poisson.lean,Mathlib/Probability/Distributions/PoissonLimitThm.lean,docs/1000.yaml |
4 |
4 |
['github-actions', 'vihdzp'] |
EtienneC30 assignee:EtienneC30 |
3-16277 3 days ago |
3-17993 3 days ago |
10-38788 10 days |
| 33754 |
euprunin author:euprunin |
chore: golf proofs |
---
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):
* `balancedHull_subset_convexHull_union_neg`: 181 ms before, 160 ms after 🎉
* `schnirelmannDensity_setOf_Odd`: 28 ms before, 16 ms after 🎉
* `List.nodupKeys_flatten`: 134 ms before, 110 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/)
|
|
1/5 |
Mathlib/Analysis/LocallyConvex/AbsConvex.lean,Mathlib/Combinatorics/Schnirelmann.lean,Mathlib/Data/List/Sigma.lean |
3 |
1 |
['github-actions'] |
nobody |
3-14239 3 days ago |
3-14307 3 days ago |
3-14284 3 days |
| 33763 |
smmercuri author:smmercuri |
doc: add note in `Asymptotics` docstring about the existential pattern |
see [Zulip chat](https://leanprover.zulipchat.com/#narrow/channel/116395-maths/topic/Use.20of.20embedded.20Landau.20notation/with/566790160)
---
[](https://gitpod.io/from-referrer/)
|
t-analysis |
6/0 |
Mathlib/Analysis/Asymptotics/Defs.lean |
1 |
1 |
['github-actions'] |
nobody |
3-4933 3 days ago |
3-4933 3 days ago |
3-4982 3 days |
| 29942 |
smmercuri author:smmercuri |
feat(InfinitePlace/Completion): embeddings of `w.Completion` factor through embeddings of `v.Completion` when `w` extends `v` |
If `w : InfinitePlace L` is an extension of `v : InfinitePlace K` to `L` (i.e. we have `w.1.LiesOver v.1`), then `extensionEmbedding w : L →+* ℂ` factors through `extensionEmbedding v : K →+* ℂ`.
---
- [x] depends on: #27978
- [x] depends on: #29969
- [x] depends on: #29944
[](https://gitpod.io/from-referrer/)
|
FLT |
88/14 |
Mathlib/Analysis/Normed/Field/WithAbs.lean,Mathlib/NumberTheory/NumberField/InfinitePlace/Completion.lean,Mathlib/NumberTheory/NumberField/InfinitePlace/Embeddings.lean,Mathlib/Topology/MetricSpace/Completion.lean |
4 |
5 |
['github-actions', 'mathlib4-dependent-issues-bot', 'mathlib4-merge-conflict-bot'] |
joelriou assignee:joelriou |
3-3695 3 days ago |
43-83465 1 month ago |
43-84561 43 days |
| 30484 |
vihdzp author:vihdzp |
refactor: override `≤` and `<` in `Function.Injective.semilatticeSup`, etc. |
These constructors now take `LE` and `LT` instance arguments, and proofs that the "induced" relations are equal. This matches the behavior for all other data fields of the same constructors, which avoids diamonds which could otherwise arise.
To recover the old behavior, you can instantiate `LE` and `LT` instances through `PartialOrder.lift` (if they don't exist already), and set the `le` and `lt` fields to `Iff.rfl`.
---
I seem to have (somehow?) changed a syntactic equality on fractional ideals - given that this golfs various proofs and even removes a porting note, I think this change is desirable.
[](https://gitpod.io/from-referrer/)
|
t-order |
396/380 |
Mathlib/Algebra/Lie/Submodule.lean,Mathlib/Algebra/Module/Injective.lean,Mathlib/Algebra/Order/Group/Ideal.lean,Mathlib/Algebra/Order/Kleene.lean,Mathlib/Analysis/Convex/Cone/Dual.lean,Mathlib/Analysis/Normed/Group/Seminorm.lean,Mathlib/Analysis/Seminorm.lean,Mathlib/CategoryTheory/Sites/Precoverage.lean,Mathlib/Combinatorics/Digraph/Basic.lean,Mathlib/Combinatorics/SimpleGraph/Basic.lean,Mathlib/Combinatorics/SimpleGraph/Finsubgraph.lean,Mathlib/Combinatorics/SimpleGraph/Subgraph.lean,Mathlib/Combinatorics/Young/YoungDiagram.lean,Mathlib/FieldTheory/Galois/GaloisClosure.lean,Mathlib/GroupTheory/GroupAction/SubMulAction.lean,Mathlib/MeasureTheory/MeasurableSpace/MeasurablyGenerated.lean,Mathlib/ModelTheory/Definability.lean,Mathlib/NumberTheory/NumberField/FractionalIdeal.lean,Mathlib/Order/BooleanAlgebra/Basic.lean,Mathlib/Order/BooleanSubalgebra.lean,Mathlib/Order/CompleteBooleanAlgebra.lean,Mathlib/Order/CompleteLattice/Basic.lean,Mathlib/Order/CompleteLattice/Lemmas.lean,Mathlib/Order/CompleteSublattice.lean,Mathlib/Order/Concept.lean,Mathlib/Order/Disjoint.lean,Mathlib/Order/Heyting/Basic.lean,Mathlib/Order/Heyting/Regular.lean,Mathlib/Order/Hom/Bounded.lean,Mathlib/Order/Hom/BoundedLattice.lean,Mathlib/Order/Hom/Lattice.lean,Mathlib/Order/Interval/Basic.lean,Mathlib/Order/Lattice.lean,Mathlib/Order/Nucleus.lean,Mathlib/Order/Sublattice.lean,Mathlib/Order/UpperLower/CompleteLattice.lean,Mathlib/RepresentationTheory/Subrepresentation.lean,Mathlib/RingTheory/DedekindDomain/Different.lean,Mathlib/RingTheory/DedekindDomain/Factorization.lean,Mathlib/RingTheory/DedekindDomain/Ideal/Basic.lean,Mathlib/RingTheory/DividedPowers/SubDPIdeal.lean,Mathlib/RingTheory/Filtration.lean,Mathlib/RingTheory/FractionalIdeal/Basic.lean,Mathlib/RingTheory/FractionalIdeal/Extended.lean,Mathlib/RingTheory/FractionalIdeal/Inverse.lean,Mathlib/RingTheory/FractionalIdeal/Operations.lean,Mathlib/RingTheory/GradedAlgebra/Homogeneous/Ideal.lean,Mathlib/Topology/Algebra/Group/ClosedSubgroup.lean,Mathlib/Topology/Algebra/Group/GroupTopology.lean,Mathlib/Topology/Algebra/Module/ClosedSubmodule.lean,Mathlib/Topology/Algebra/OpenSubgroup.lean,Mathlib/Topology/ContinuousMap/Bounded/Normed.lean,Mathlib/Topology/ContinuousMap/CompactlySupported.lean,Mathlib/Topology/ContinuousMap/Ordered.lean,Mathlib/Topology/DiscreteQuotient.lean,Mathlib/Topology/Sets/Closeds.lean,Mathlib/Topology/Sets/Compacts.lean,Mathlib/Topology/Sets/Opens.lean,Mathlib/Topology/Sets/Order.lean |
59 |
44 |
['Vierkantor', 'YaelDillies', 'github-actions', 'jcommelin', 'leanprover-bot', 'leanprover-radar', 'mathlib4-merge-conflict-bot', 'plp127', 'vihdzp'] |
bryangingechen assignee:bryangingechen |
3-705 3 days ago |
5-38231 5 days ago |
49-42671 49 days |
| 33359 |
sun123zxy author:sun123zxy |
feat(Algebra/Module/SpanRank): add comparing lemmas for span rank |
---
Split from PR #33247
[](https://gitpod.io/from-referrer/)
|
t-algebra
new-contributor
label:t-algebra$ |
55/6 |
Mathlib/Algebra/Module/SpanRank.lean |
1 |
9 |
['erdOne', 'eric-wieser', 'github-actions', 'sun123zxy'] |
eric-wieser assignee:eric-wieser |
3-567 3 days ago |
3-567 3 days ago |
9-1268 9 days |
| 29186 |
winstonyin author:winstonyin |
feat: IsIntegralCurve for solutions to ODEs |
I define `IsIntegralCurve` etc. for solutions to ODEs on vector spaces. The translation and scaling lemmas are also included. This parallels `IsMIntegralCurve` etc. for manifolds.
Moved from #26534.
- [x] depends on: #26563
---
[](https://gitpod.io/from-referrer/)
|
t-differential-geometry
t-analysis
t-dynamics
|
305/100 |
Mathlib.lean,Mathlib/Analysis/ODE/Basic.lean,Mathlib/Analysis/ODE/Transform.lean,Mathlib/Geometry/Manifold/IntegralCurve/Basic.lean,Mathlib/Geometry/Manifold/IntegralCurve/Transform.lean |
5 |
11 |
['github-actions', 'grunweg', 'mathlib4-dependent-issues-bot', 'mathlib4-merge-conflict-bot', 'mcdoll', 'sgouezel', 'winstonyin'] |
sgouezel assignee:sgouezel |
3-522 3 days ago |
4-81825 4 days ago |
105-14395 105 days |
| 33740 |
SnirBroshi author:SnirBroshi |
chore(Order/CompleteLattice/Basic): generalize many theorems to `CompleteSemilattice{Sup/Inf}` |
---
I believe some of these can be generalized further, this PR takes a small step.
This might also allow half of these to be deleted thanks to `to_dual` somehow.
[](https://gitpod.io/from-referrer/)
|
t-order |
212/178 |
Mathlib/Order/CompleteLattice/Basic.lean,Mathlib/Order/Interval/Set/Disjoint.lean |
2 |
8 |
['JovanGerb', 'SnirBroshi', 'github-actions', 'vihdzp'] |
nobody |
2-75918 2 days ago |
3-51571 3 days ago |
3-51612 3 days |
| 33768 |
vihdzp author:vihdzp |
chore(Order/RelClasses): remove redundant instances |
---
[](https://gitpod.io/from-referrer/)
|
t-order |
0/20 |
Mathlib/Order/RelClasses.lean |
1 |
3 |
['github-actions', 'leanprover-radar', 'vihdzp'] |
nobody |
2-75651 2 days ago |
2-80163 2 days ago |
2-80208 2 days |
| 32672 |
tb65536 author:tb65536 |
feat: haar measures on short exact sequences |
This PR defines the notion of a short exact sequence of topological groups, and proves that if `1 → A → B → C → 1` is a short exact sequence of topological groups, then Haar measures on `A` and `C` induce a Haar measure on `B`.
The final result of the file is a consequence needed for FLT: If `B → C` is injective on an open set `U`, then `U` has bounded measure.
---
[](https://gitpod.io/from-referrer/)
|
t-topology
t-measure-probability
FLT
|
374/0 |
Mathlib.lean,Mathlib/MeasureTheory/Measure/Haar/Extension.lean,Mathlib/Topology/Algebra/Group/Extension.lean |
3 |
6 |
['RemyDegenne', 'github-actions', 'kbuzzard', 'tb65536'] |
urkud assignee:urkud |
2-74937 2 days ago |
27-80652 27 days ago |
31-43758 31 days |
| 32042 |
chrisflav author:chrisflav |
feat(AlgebraicGeometry): quasi compact covers |
This will be used to define the fpqc topology on `Scheme`.
From Proetale.
---
[](https://gitpod.io/from-referrer/)
|
t-algebraic-geometry |
311/13 |
Mathlib.lean,Mathlib/AlgebraicGeometry/Cover/QuasiCompact.lean,Mathlib/AlgebraicGeometry/Morphisms/Affine.lean,Mathlib/AlgebraicGeometry/Morphisms/QuasiCompact.lean,Mathlib/AlgebraicGeometry/Morphisms/UnderlyingMap.lean,Mathlib/AlgebraicGeometry/Sites/MorphismProperty.lean,Mathlib/Topology/Sets/CompactOpenCovered.lean,Mathlib/Topology/Spectral/Prespectral.lean |
8 |
15 |
['chrisflav', 'erdOne', 'github-actions'] |
joneugster assignee:joneugster |
2-73003 2 days ago |
3-13619 3 days ago |
47-36697 47 days |
| 33749 |
plp127 author:plp127 |
feat: `NNRat` is countable |
We provide an `Encodable NNRat` instance. As a consequence we also get the instance `Countable NNRat`.
See also [Zulip](https://leanprover.zulipchat.com/#narrow/channel/113489-new-members/topic/NNRat.20not.20countable.3F/near/566916284)
---
[](https://gitpod.io/from-referrer/)
|
t-data
large-import
|
13/0 |
Mathlib/Data/Rat/Encodable.lean |
1 |
4 |
['eric-wieser', 'github-actions', 'grunweg', 'leanprover-radar'] |
nobody |
2-70974 2 days ago |
2-70982 2 days ago |
3-21406 3 days |
| 33769 |
alreadydone author:alreadydone |
feat(LinearAlgebra): add `Module.IsPrincipal` |
---
[](https://gitpod.io/from-referrer/)
|
t-algebra label:t-algebra$ |
36/0 |
Mathlib/LinearAlgebra/Span/Defs.lean |
1 |
1 |
['github-actions'] |
nobody |
2-68406 2 days ago |
2-73806 2 days ago |
2-73862 2 days |
| 33527 |
SnirBroshi author:SnirBroshi |
feat(Combinatorics/SimpleGraph/Connectivity/Subgraph): `w.toSubgraph ≤ G' ↔ w.edgeSet ⊆ G'.edgeSet` |
---
[](https://gitpod.io/from-referrer/)
|
t-combinatorics |
9/1 |
Mathlib/Combinatorics/SimpleGraph/Connectivity/Subgraph.lean |
1 |
4 |
['Rida-Hamadani', 'SnirBroshi', 'github-actions'] |
nobody |
2-66870 2 days ago |
7-76300 7 days ago |
7-76337 7 days |
| 33776 |
mcdoll author:mcdoll |
feat(MeasureTheory): every bounded continuous function is in `L∞` |
As opposed to the lemma right below we use `MemLp` and not `f.toContinuousMap.toAEEqFun μ ∈ Lp`, because
the later seems rather unergonomic and with `MemLp` it is possible to obtain a `Lp` function using `MemLp.toLp`.
---
[](https://gitpod.io/from-referrer/)
|
t-measure-probability |
4/0 |
Mathlib/MeasureTheory/Function/LpSpace/ContinuousFunctions.lean |
1 |
1 |
['github-actions'] |
nobody |
2-66065 2 days ago |
2-66067 2 days ago |
2-66109 2 days |
| 33780 |
ooovi author:ooovi |
feat(Geometry/Convex/Cone): lineality space of pointed cones |
Define the lineality space `PointedCone.lineal` as the submodule `C ⊓ -C`. Prove that it is the largest submodule of the cone, which is sometimes used as an alternative definition.
Co-authored-by: Martin Winter
---
- [ ] depends on #33761
[](https://gitpod.io/from-referrer/)
|
t-convex-geometry |
79/4 |
Mathlib/Algebra/Module/Submodule/RestrictScalars.lean,Mathlib/Geometry/Convex/Cone/Pointed.lean,Mathlib/RingTheory/Ideal/Maps.lean |
3 |
1 |
['github-actions'] |
nobody |
2-63401 2 days ago |
2-63401 2 days ago |
2-63602 2 days |
| 25841 |
mitchell-horner author:mitchell-horner |
feat(Combinatorics/SimpleGraph): prove the Kővári–Sós–Turán theorem |
Prove the Kővári–Sós–Turán theorem (an upper bound on the Zarankiewicz function)
---
- [x] depends on: #19865
- [x] depends on: #20738
- [x] depends on: #27602
[](https://gitpod.io/from-referrer/)
---
*This PR continues the work from #20240.*
*Original PR: https://github.com/leanprover-community/mathlib4/pull/20240* |
t-combinatorics |
484/0 |
Mathlib.lean,Mathlib/Combinatorics/SimpleGraph/Bipartite.lean,Mathlib/Combinatorics/SimpleGraph/Extremal/KovariSosTuran.lean,Mathlib/Combinatorics/SimpleGraph/Extremal/Zarankiewicz.lean,Mathlib/Combinatorics/SimpleGraph/Maps.lean,docs/1000.yaml |
6 |
11 |
['SnirBroshi', 'github-actions', 'mathlib4-dependent-issues-bot', 'mathlib4-merge-conflict-bot', 'mitchell-horner'] |
kmill assignee:kmill |
2-59702 2 days ago |
6-39560 6 days ago |
51-54957 51 days |
| 33214 |
JJYYY-JJY author:JJYYY-JJY |
chore(Data/List/Rotate): add simp attributes |
* Refs #7987 (SC: Data/List/Rotate)
* Add `@[simp]` to: `rotate_mod`, `rotate'_nil`, `rotate'_rotate'`, `rotate'_mod`, `rotate_rotate`, `getElem?_rotate`, `getElem_rotate`, `head?_rotate`, `map_rotate`.
* Verification: `lake build Mathlib.Data.List.Rotate`. |
new-contributor
t-data
|
7/0 |
Mathlib/Data/List/Rotate.lean |
1 |
1 |
['github-actions'] |
TwoFX assignee:TwoFX |
2-59698 2 days ago |
19-53627 19 days ago |
19-53671 19 days |
| 33582 |
urkud author:urkud |
feat(ContDiffHolder/Moreira): define $C^{k+(α)}$ maps |
From https://github.com/urkud/SardMoreira
---
[](https://gitpod.io/from-referrer/)
|
t-analysis |
288/0 |
Mathlib.lean,Mathlib/Analysis/Calculus/ContDiffHolder/Moreira.lean,Mathlib/Analysis/SpecialFunctions/Pow/Asymptotics.lean,docs/references.bib |
4 |
1 |
['github-actions'] |
ADedecker assignee:ADedecker |
2-59693 2 days ago |
6-49837 6 days ago |
6-49883 6 days |
| 33635 |
plp127 author:plp127 |
feat(Tactic/Set): use `binderIdent` instead of `ident` |
This let both `a` and `h` be replaced with `_` in the syntax `set a := val with ← h`
---
[](https://gitpod.io/from-referrer/)
|
t-meta |
16/2 |
Mathlib/Tactic/Set.lean,MathlibTest/Set.lean |
2 |
3 |
['JovanGerb', 'github-actions', 'plp127'] |
kim-em assignee:kim-em |
2-59685 2 days ago |
5-67988 5 days ago |
5-67972 5 days |
| 33636 |
mcdoll author:mcdoll |
feat(Analysis/Distribution): the Laplacian on Schwartz functions |
We introduce a notation type-class for the Laplacian, change the definition of `InnerProductSpace.laplacian` to `Laplacian.laplacian` and define the Laplacian using the sum of second derivatives on Schwartz functions.
We define an abstract Laplacian for any space with `LineDeriv` in order to avoid duplication for other function spaces (in particular, this will be reused for the tempered distribution Laplacian).
---
[](https://gitpod.io/from-referrer/)
|
t-analysis |
197/12 |
Mathlib.lean,Mathlib/Analysis/Distribution/DerivNotation.lean,Mathlib/Analysis/Distribution/Laplacian.lean,Mathlib/Analysis/Distribution/SchwartzSpace.lean,Mathlib/Analysis/InnerProductSpace/Harmonic/Basic.lean,Mathlib/Analysis/InnerProductSpace/Laplacian.lean |
6 |
3 |
['github-actions', 'mcdoll'] |
urkud assignee:urkud |
2-59684 2 days ago |
5-65343 5 days ago |
5-65390 5 days |
| 33757 |
fpvandoorn author:fpvandoorn |
feat: remove decidability instances on sets or ideals |
* We have the rule that you should assume decidability instead of opening the classical locale. However, in places where there cannot ever be a reasonable decidable instance, I think we can relax this rule.
* This PR updates the corresponding library note, and removes `DecidableEq` instances on `Set` and `Ideal`
* This looks a lot cleaner IMO, and the decidability assumptions are silly: assuming that `Set α` has decidable for an inhabited type `α` is equivalent to assuming that all propositions are decidable. Similarly for `Ideal R` for a nontrivial ring `R`.
* This has one downside: if a lemma uses classical logic to infer decidability for its statement, then all lemmas that use this lemma also have to do this, otherwise they will deal with decidability type mismatches
---
This was motivated by seeing some code from @mariainesdff's repos with such decidability arguments. @mariainesdff, do you think this PR would make your code a bit nicer?
[](https://gitpod.io/from-referrer/)
|
|
57/32 |
Mathlib/Algebra/Module/DedekindDomain.lean,Mathlib/Algebra/Module/PID.lean,Mathlib/Logic/Basic.lean,Mathlib/MeasureTheory/SetSemiring.lean,Mathlib/NumberTheory/RamificationInertia/Basic.lean,Mathlib/Order/PartialSups.lean,Mathlib/RingTheory/DedekindDomain/Factorization.lean,Mathlib/RingTheory/DedekindDomain/Ideal/Lemmas.lean,Mathlib/RingTheory/Ideal/Basic.lean,Mathlib/RingTheory/Invariant/Basic.lean,Mathlib/RingTheory/Lasker.lean,Mathlib/RingTheory/Valuation/ValuationRing.lean |
12 |
5 |
['github-actions', 'plp127', 'vihdzp'] |
nobody |
2-59420 2 days ago |
3-10978 3 days ago |
3-10955 3 days |
| 33771 |
plp127 author:plp127 |
feat: prove `Prod.wellFoundedLT` directly |
Prove `Prod.wellFoundedLT` without going through `Antisymmetrization`. This makes the instance accessible without having to import antisymmetrization.
---
[](https://gitpod.io/from-referrer/)
|
t-order |
19/26 |
Mathlib/Algebra/Lie/Weights/Basic.lean,Mathlib/GroupTheory/Solvable.lean,Mathlib/GroupTheory/SpecificGroups/ZGroup.lean,Mathlib/Order/Antisymmetrization.lean,Mathlib/Order/RelClasses.lean |
5 |
4 |
['alreadydone', 'github-actions', 'plp127', 'vihdzp'] |
nobody |
2-56353 2 days ago |
2-70185 2 days ago |
2-70229 2 days |
| 33784 |
tb65536 author:tb65536 |
refactor(Topology/Irreducible): weaken assumptions of `preimage_mem_irreducibleComponents_of_isPreirreducible_fiber` |
This PR weakens the surjectivity assumption of `preimage_mem_irreducibleComponents_of_isPreirreducible_fiber` to `(t ∩ Set.range f).Nonempty`. I also took the liberty of systematizing the file slightly, so that now there are 6 lemmas: preimage of (preirreducible / irreducible / irreducible component) assuming (preirreducible fibers / open embedding).
---
[](https://gitpod.io/from-referrer/)
|
t-topology |
36/26 |
Mathlib/Topology/Irreducible.lean |
1 |
1 |
['github-actions'] |
nobody |
2-56197 2 days ago |
2-56197 2 days ago |
2-56175 2 days |
| 33542 |
yuanyi-350 author:yuanyi-350 |
feat(integral): Error Estimation for the Rectangle Rule in Numerical Integration |
---
[](https://gitpod.io/from-referrer/)
|
t-analysis |
113/0 |
Mathlib.lean,Mathlib/Analysis/Calculus/ContDiff/Defs.lean,Mathlib/Analysis/Calculus/Midpoint.lean |
3 |
1 |
['github-actions'] |
nobody |
2-55141 2 days ago |
2-55168 2 days ago |
2-55195 2 days |
| 28546 |
Sfgangloff author:Sfgangloff |
feat(SymbolicDynamics): basic setup of Zd, full shift, cylinders, pat… |
This PR adds a **group-generic** foundation for symbolic dynamics over an arbitrary group `G`, together with convenient specializations for `ℤ` and `ℤ^d`.
Summary of additions:
- **Full shift and shift action**
- `abbrev FullShift (A G) := G → A` (inherits product topology from the Π-type).
- Right shift `shift g x` with convention `(shift g x) h = x (h * g)`.
- **Cylinders and topology**
- `cylinder U x : Set (G → A)` for finite `U : Finset G`.
- Cylinders are open under `[DiscreteTopology A]`; with a finite alphabet they are also closed.
- Equality with dependent products:
`cylinder U x = Set.pi (↑U) (fun i => ({x i} : Set A))`, enabling use of the `Set.pi` API.
- **Patterns, occurrences, and subshifts**
- `Pattern A G` with finite `support : Finset G` and `data : support → A`.
- `Pattern.occursIn p x g` (occurrence at translate `g`) and the expected shift law.
- `forbids F` and `Subshift A G` (closed, shift-invariant subsets).
- `FixedSupport A G U` with an equivalence to `(U → A)` to obtain finiteness.
- **Language on finite shapes and counting**
- `languageOn X U`, `languageCardOn X U`, and `patternCountOn Y U`.
- **Entropy along a shape sequence**
- `limsupAtTop` (as an `sInf` of eventual upper bounds).
- `entropyAlong X F hF := limsup (log (patternCountOn X (F n) + 1) / |F n|)`
for any nonempty finite shapes `F : ℕ → Finset G` (the `+ 1` avoids `log 0`).
- **Specializations**
- `IntShapes`: segments `[-n,n]` on `Multiplicative ℤ`, with `entropy_Z`.
- `ZdShapes`: boxes `[-n,n]^d` on `ℤ^d` (as functions `Fin d → ℤ`), with `entropy_Zd`.
Mathematical remarks:
- The API is **shape-parametric**: entropy is defined along user-provided finite shapes.
- On **amenable** groups, using a **Følner** sequence yields a canonical value (Ornstein–Weiss).
This PR does not assume amenability; the family of shapes is an explicit input.
Motivation:
Provide a clean, reusable base for symbolic dynamics on groups in mathlib.
Future work:
- Add a Følner predicate and prove shape-independence / limit existence on amenable groups.
- Expand the `ℤ`/`ℤ^d` toolkit (alternative shapes, mixing, factors).
- Develop 1D theory and, longer-term, multidimensional SFT results (e.g. along the lines of Hochman–Meyerovitch).
|
t-dynamics
new-contributor
|
757/0 |
Mathlib.lean,Mathlib/Dynamics/SymbolicDynamics/Basic.lean,Mathlib/Tactic/Translate/ToAdditive.lean |
3 |
157 |
['Sfgangloff', 'eric-wieser', 'github-actions', 'kckennylau', 'mathlib4-merge-conflict-bot', 'sgouezel'] |
sgouezel assignee:sgouezel |
2-53261 2 days ago |
2-53278 2 days ago |
90-1074 90 days |
| 32744 |
NoneMore author:NoneMore |
feat(ModelTheory/Definablity): add `DefinableFun` definition and lemmas |
This PR adds two basic shapes of definable sets and `DefinableFun` definition with relevant lemmas.
The main result is `Set.Definable.preimage_of_map` asserting that the preimage of a definable set under a definable map is definable.
There are also some tool lemmas derived by the preimage lemma.
---
[](https://gitpod.io/from-referrer/)
|
t-logic
new-contributor
|
147/0 |
Mathlib/ModelTheory/Definability.lean |
1 |
59 |
['NoneMore', 'github-actions', 'mathlib4-merge-conflict-bot', 'staroperator'] |
fpvandoorn assignee:fpvandoorn |
2-38943 2 days ago |
2-38967 2 days ago |
30-38172 30 days |
| 31325 |
joelriou author:joelriou |
feat(AlgebraicTopology): a computable monoidal functor instance for `hoFunctor` |
We construct a computable equivalence of categories `(X ⊗ Y).HomotopyCategory ≌ X.HomotopyCategory × Y.HomotopyCategory` for `2`-truncated simplicial sets `X` and `Y`. This allows to make the bicategory instance on quasicategories computable.
---
- [x] depends on: #33201
- [x] depends on: #31174
- [x] depends on: #31250
- [x] depends on: #31254
- [x] depends on: #31274
- [x] depends on: #31265
[](https://gitpod.io/from-referrer/)
|
maintainer-merge
t-algebraic-topology
|
298/28 |
Mathlib/AlgebraicTopology/Quasicategory/StrictBicategory.lean,Mathlib/AlgebraicTopology/SimplicialSet/HoFunctorMonoidal.lean,Mathlib/AlgebraicTopology/SimplicialSet/NerveAdjunction.lean |
3 |
17 |
['github-actions', 'joelriou', 'mathlib4-dependent-issues-bot', 'mathlib4-merge-conflict-bot', 'robin-carlier'] |
robin-carlier assignee:robin-carlier |
2-30123 2 days ago |
2-30123 2 days ago |
15-76599 15 days |
| 33787 |
LTolDe author:LTolDe |
doc(Topology/Baire/BaireMeasurable): add naming convention for notation `residualEq` |
---
[](https://gitpod.io/from-referrer/)
|
easy
t-topology
new-contributor
|
2/1 |
Mathlib/Topology/Baire/BaireMeasurable.lean |
1 |
2 |
['LTolDe', 'github-actions'] |
nobody |
2-26025 2 days ago |
2-26025 2 days ago |
2-26119 2 days |
| 33714 |
idontgetoutmuch author:idontgetoutmuch |
Riemannian metrics exist II |
Supersedes https://github.com/leanprover-community/mathlib4/pull/33519
---
[](https://gitpod.io/from-referrer/)
|
t-differential-geometry
new-contributor
|
1269/0 |
Mathlib.lean,Mathlib/Geometry/Manifold/ExistsRiemannianMetricTangentSpace.lean,Mathlib/Geometry/Manifold/PartitionOfUnity.lean |
3 |
3 |
['github-actions', 'grunweg', 'idontgetoutmuch'] |
nobody |
2-23979 2 days ago |
3-27601 3 days ago |
4-13488 4 days |
| 33555 |
erdOne author:erdOne |
feat(RingTheory): standard smooth = etale over mvpolynomial |
---
[](https://gitpod.io/from-referrer/)
|
large-import |
79/2 |
Mathlib/Algebra/MvPolynomial/Equiv.lean,Mathlib/Algebra/MvPolynomial/PDeriv.lean,Mathlib/RingTheory/RingHom/StandardSmooth.lean |
3 |
3 |
['erdOne', 'github-actions', 'robin-carlier'] |
robin-carlier assignee:robin-carlier |
2-23846 2 days ago |
6-80784 6 days ago |
6-80822 6 days |
| 33788 |
harahu author:harahu |
chore(Algebra): move `LinearMap.ker_restrictScalars` |
Resolve an old TODO by moving `LinearMap.ker_restrictScalars` to a location in `Mathlib/Algebra/Module/Submodule`.
The TODO referenced lemmas in plural, but only `LinearMap.ker_restrictScalars` seemed to fit. I assume any other lemmas might already have been moved at an earlier point.
---
Notes for reviewers:
- The new location in `Mathlib/Algebra/Module/Submodule/Ker.lean` was chosen somewhat arbitrarily in favor of `Mathlib/Algebra/Module/Submodule/RestrictScalars.lean`. Please consider whether `Ker.lean` is the optimal location for this lemma.
- I haven't moved content in mathlib before – do I need to add a deprecation alias in the original file, or is the way I've done it fine?
[](https://gitpod.io/from-referrer/)
|
t-algebra label:t-algebra$ |
14/17 |
Mathlib/Algebra/Algebra/Basic.lean,Mathlib/Algebra/Module/Submodule/Ker.lean |
2 |
1 |
['github-actions'] |
nobody |
2-21919 2 days ago |
2-21919 2 days ago |
2-25178 2 days |
| 33129 |
Paul-Lez author:Paul-Lez |
feat(Tactic/Simproc/VecPerm): Add simproc for permuting entries of a vector |
---
[](https://gitpod.io/from-referrer/)
|
t-meta |
127/0 |
Mathlib.lean,Mathlib/Tactic.lean,Mathlib/Tactic/Simproc/VecPerm.lean,MathlibTest/Simproc/VecPerm.lean |
4 |
9 |
['JovanGerb', 'Paul-Lez', 'github-actions', 'ocfnash'] |
thorimur assignee:thorimur |
2-21081 2 days ago |
22-2776 22 days ago |
22-5808 22 days |
| 32481 |
ADedecker author:ADedecker |
feat: add `PolynormableSpace.banach_steinhaus` |
---
- [x] depends on: #32480
[](https://gitpod.io/from-referrer/)
|
t-analysis |
121/24 |
Mathlib/Analysis/LocallyConvex/AbsConvexOpen.lean,Mathlib/Analysis/LocallyConvex/Barrelled.lean,Mathlib/Analysis/LocallyConvex/WithSeminorms.lean,Mathlib/Analysis/Normed/Operator/BanachSteinhaus.lean |
4 |
2 |
['github-actions', 'mathlib4-dependent-issues-bot'] |
sgouezel assignee:sgouezel |
2-19919 2 days ago |
3-79251 3 days ago |
3-80529 3 days |
| 33339 |
Ruben-VandeVelde author:Ruben-VandeVelde |
feat: small lemmas about LeftInverse and image/preimage |
From sphere-eversion.
---
[](https://gitpod.io/from-referrer/)
|
maintainer-merge
t-data
|
9/1 |
Mathlib/Data/Set/Image.lean |
1 |
4 |
['Ruben-VandeVelde', 'github-actions', 'robin-carlier', 'vihdzp'] |
nobody |
2-15981 2 days ago |
2-15981 2 days ago |
15-19073 15 days |
| 33767 |
Whysoserioushah author:Whysoserioushah |
chore(RingTheory/Morita/Matrix): Finish the morita equivalence between matrix ring and the ring itself |
---
[](https://gitpod.io/from-referrer/)
|
large-import
t-ring-theory
|
79/1 |
Mathlib/RingTheory/Morita/Matrix.lean |
1 |
11 |
['Whysoserioushah', 'eric-wieser', 'github-actions'] |
nobody |
2-14259 2 days ago |
2-85603 2 days ago |
2-85646 2 days |
| 33761 |
ooovi author:ooovi |
feat(Algebra/Module/Submodule): behaviour of `restrictScalars` under lattice operations |
Add lemmas about how `restrictScalars` interacts with `sup`, `inf`, `sSup`, `sInf`, `iSup` and `iInf`.
Co-authored-by: Martin Winter
---
We need this for https://github.com/leanprover-community/mathlib4/pull/33664.
[](https://gitpod.io/from-referrer/)
|
t-algebra label:t-algebra$ |
44/3 |
Mathlib/Algebra/Module/Submodule/RestrictScalars.lean,Mathlib/RingTheory/Ideal/Maps.lean |
2 |
7 |
['YaelDillies', 'eric-wieser', 'github-actions', 'ooovi'] |
nobody |
2-13901 2 days ago |
3-3353 3 days ago |
3-6041 3 days |
| 33613 |
DavidLedvinka author:DavidLedvinka |
feat(Probability): `UniformOn_univ_instIsProbabilityMeasure` |
It is convenient to have an instance of `IsProbabilityMeasure` on a uniform distribution on `.univ` (to avoid the need for `haveI` statements). There is perhaps an argument for `abbrev uniform := uniformOn (.univ : Set Ω)` but I have not implemented this in this PR. |
t-measure-probability |
11/0 |
Mathlib/Probability/UniformOn.lean |
1 |
5 |
['DavidLedvinka', 'Ruben-VandeVelde', 'github-actions'] |
nobody |
2-13385 2 days ago |
2-13385 2 days ago |
4-11495 4 days |
| 31706 |
Thmoas-Guan author:Thmoas-Guan |
feat(Algebra/ModuleCat): `ModuleCat.uliftFunctor` |
Add `ModuleCat.uliftFunctor`
---
[](https://gitpod.io/from-referrer/)
|
t-algebra
maintainer-merge
label:t-algebra$ |
108/0 |
Mathlib.lean,Mathlib/Algebra/Category/ModuleCat/Ulift.lean |
2 |
20 |
['Thmoas-Guan', 'dagurtomas', 'erdOne', 'github-actions', 'mathlib4-merge-conflict-bot', 'robin-carlier'] |
mattrobball assignee:mattrobball |
2-12643 2 days ago |
2-12643 2 days ago |
25-2969 25 days |
| 33793 |
LTolDe author:LTolDe |
feat(MeasureTheory/Constructions/Polish/Basic): add lemma AnalyticSet.inter_nonempty_of_nowhereMeagre |
add lemma AnalyticSet.inter_nonempty_of_nowhereMeagre, the main ingredient for the proof of the **Effros' Theorem**, see [#mathlib4 > Effros Theorem](https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/Effros.20Theorem/with/566543328)
introduce definition of a nowhere meagre set
---
[](https://gitpod.io/from-referrer/)
|
new-contributor |
37/0 |
Mathlib/MeasureTheory/Constructions/Polish/Basic.lean,Mathlib/Order/Filter/Basic.lean,Mathlib/Topology/GDelta/Basic.lean |
3 |
1 |
['github-actions'] |
nobody |
2-12099 2 days ago |
2-12198 2 days ago |
2-12224 2 days |
| 33403 |
xroblot author:xroblot |
feat(GroupTheory/FiniteAbelian): prove that the restriction map is surjective |
Let `G` be a finite commutative group and let `H` be a subgroup. If `M` is a commutative monoid
such that `G →* Mˣ` and `H →* Mˣ` are both finite (this is the case for example if `M` is a
commutative domain), then any homomorphism `H →* Mˣ` can be extended to an homomorphism `G →* Mˣ`.
---
[](https://gitpod.io/from-referrer/)
|
t-group-theory |
90/13 |
Mathlib/Algebra/Group/Submonoid/Operations.lean,Mathlib/GroupTheory/Exponent.lean,Mathlib/GroupTheory/FiniteAbelian/Duality.lean,Mathlib/GroupTheory/QuotientGroup/Basic.lean,Mathlib/NumberTheory/MulChar/Duality.lean,Mathlib/RingTheory/RootsOfUnity/Basic.lean |
6 |
7 |
['Ruben-VandeVelde', 'github-actions', 'xroblot'] |
urkud assignee:urkud |
2-11543 2 days ago |
2-11543 2 days ago |
12-20350 12 days |
| 33531 |
harahu author:harahu |
doc(CategoryTheory): fix typos |
Fix typos and staleness in docs. The issues were found and corrected by Codex.
---
[](https://gitpod.io/from-referrer/)
|
t-category-theory
maintainer-merge
|
210/208 |
Mathlib/CategoryTheory/Abelian/Basic.lean,Mathlib/CategoryTheory/Abelian/DiagramLemmas/Four.lean,Mathlib/CategoryTheory/Abelian/DiagramLemmas/KernelCokernelComp.lean,Mathlib/CategoryTheory/Abelian/Exact.lean,Mathlib/CategoryTheory/Abelian/Ext.lean,Mathlib/CategoryTheory/Abelian/FreydMitchell.lean,Mathlib/CategoryTheory/Abelian/GrothendieckAxioms/Connected.lean,Mathlib/CategoryTheory/Abelian/GrothendieckAxioms/FunctorCategory.lean,Mathlib/CategoryTheory/Abelian/GrothendieckCategory/ColimCoyoneda.lean,Mathlib/CategoryTheory/Abelian/GrothendieckCategory/Subobject.lean,Mathlib/CategoryTheory/Abelian/Injective/Basic.lean,Mathlib/CategoryTheory/Abelian/Monomorphisms.lean,Mathlib/CategoryTheory/Abelian/NonPreadditive.lean,Mathlib/CategoryTheory/Abelian/Opposite.lean,Mathlib/CategoryTheory/Abelian/Projective/Ext.lean,Mathlib/CategoryTheory/Abelian/Projective/Extend.lean,Mathlib/CategoryTheory/Abelian/Projective/Resolution.lean,Mathlib/CategoryTheory/Abelian/Pseudoelements.lean,Mathlib/CategoryTheory/Abelian/Refinements.lean,Mathlib/CategoryTheory/Abelian/SerreClass/Basic.lean,Mathlib/CategoryTheory/Action/Basic.lean,Mathlib/CategoryTheory/Action/Limits.lean,Mathlib/CategoryTheory/Adjunction/Evaluation.lean,Mathlib/CategoryTheory/Bicategory/Adjunction/Basic.lean,Mathlib/CategoryTheory/Bicategory/Functor/Cat/ObjectProperty.lean,Mathlib/CategoryTheory/Bicategory/Functor/Lax.lean,Mathlib/CategoryTheory/Bicategory/Functor/LocallyDiscrete.lean,Mathlib/CategoryTheory/Bicategory/Functor/Prelax.lean,Mathlib/CategoryTheory/Bicategory/Functor/StrictlyUnitary.lean,Mathlib/CategoryTheory/Bicategory/LocallyGroupoid.lean,Mathlib/CategoryTheory/Bicategory/NaturalTransformation/Oplax.lean,Mathlib/CategoryTheory/Bicategory/Product.lean,Mathlib/CategoryTheory/CatCommSq.lean,Mathlib/CategoryTheory/Category/ULift.lean,Mathlib/CategoryTheory/Comma/CardinalArrow.lean,Mathlib/CategoryTheory/Comma/Presheaf/Basic.lean,Mathlib/CategoryTheory/ComposableArrows/Basic.lean,Mathlib/CategoryTheory/ConcreteCategory/Basic.lean,Mathlib/CategoryTheory/Core.lean,Mathlib/CategoryTheory/Enriched/Basic.lean,Mathlib/CategoryTheory/Enriched/Limits/HasConicalPullbacks.lean,Mathlib/CategoryTheory/FiberedCategory/Fiber.lean,Mathlib/CategoryTheory/FinCategory/AsType.lean,Mathlib/CategoryTheory/Functor/KanExtension/Basic.lean,Mathlib/CategoryTheory/Functor/ReflectsIso/Balanced.lean,Mathlib/CategoryTheory/Functor/Trifunctor.lean,Mathlib/CategoryTheory/Galois/Basic.lean,Mathlib/CategoryTheory/Galois/GaloisObjects.lean,Mathlib/CategoryTheory/Galois/Prorepresentability.lean,Mathlib/CategoryTheory/Generator/Basic.lean,Mathlib/CategoryTheory/GradedObject/Bifunctor.lean,Mathlib/CategoryTheory/GradedObject/Trifunctor.lean,Mathlib/CategoryTheory/Groupoid/Subgroupoid.lean,Mathlib/CategoryTheory/Groupoid/VertexGroup.lean,Mathlib/CategoryTheory/Idempotents/FunctorExtension.lean,Mathlib/CategoryTheory/IsomorphismClasses.lean,Mathlib/CategoryTheory/Limits/ConcreteCategory/WithAlgebraicStructures.lean,Mathlib/CategoryTheory/Limits/Constructions/Equalizers.lean,Mathlib/CategoryTheory/Limits/Creates.lean,Mathlib/CategoryTheory/Limits/ExactFunctor.lean,Mathlib/CategoryTheory/Limits/FilteredColimitCommutesFiniteLimit.lean,Mathlib/CategoryTheory/Limits/FintypeCat.lean,Mathlib/CategoryTheory/Limits/FormalCoproducts.lean,Mathlib/CategoryTheory/Limits/FunctorCategory/Shapes/Pullbacks.lean,Mathlib/CategoryTheory/Limits/MonoCoprod.lean,Mathlib/CategoryTheory/Limits/Preorder.lean,Mathlib/CategoryTheory/Limits/Preserves/Shapes/Images.lean,Mathlib/CategoryTheory/Limits/Preserves/Shapes/Pullbacks.lean,Mathlib/CategoryTheory/Limits/Preserves/Shapes/Square.lean,Mathlib/CategoryTheory/Limits/Shapes/ConcreteCategory.lean,Mathlib/CategoryTheory/Limits/Shapes/Images.lean,Mathlib/CategoryTheory/Limits/Shapes/Opposites/Filtered.lean,Mathlib/CategoryTheory/Limits/Shapes/Preorder/PrincipalSeg.lean,Mathlib/CategoryTheory/Limits/Shapes/Preorder/WellOrderContinuous.lean,Mathlib/CategoryTheory/Limits/Shapes/Pullback/PullbackCone.lean,Mathlib/CategoryTheory/Limits/Shapes/Pullback/Square.lean,Mathlib/CategoryTheory/Limits/Shapes/Reflexive.lean,Mathlib/CategoryTheory/Limits/Shapes/RegularMono.lean,Mathlib/CategoryTheory/Limits/Shapes/SplitCoequalizer.lean,Mathlib/CategoryTheory/Limits/Shapes/WidePullbacks.lean,Mathlib/CategoryTheory/Limits/Types/ColimitType.lean,Mathlib/CategoryTheory/Limits/Types/ColimitTypeFiltered.lean,Mathlib/CategoryTheory/Limits/Types/Pushouts.lean,Mathlib/CategoryTheory/Linear/Yoneda.lean,Mathlib/CategoryTheory/Localization/Construction.lean,Mathlib/CategoryTheory/Localization/DerivabilityStructure/Basic.lean,Mathlib/CategoryTheory/Localization/DerivabilityStructure/OfFunctorialResolutions.lean,Mathlib/CategoryTheory/Localization/Predicate.lean,Mathlib/CategoryTheory/Localization/Quotient.lean,Mathlib/CategoryTheory/Monoidal/Action/LinearFunctor.lean,Mathlib/CategoryTheory/Monoidal/Braided/Basic.lean,Mathlib/CategoryTheory/Monoidal/Closed/Basic.lean,Mathlib/CategoryTheory/Monoidal/Closed/FunctorCategory/Groupoid.lean,Mathlib/CategoryTheory/Monoidal/Conv.lean,Mathlib/CategoryTheory/Monoidal/DayConvolution.lean,Mathlib/CategoryTheory/Monoidal/DayConvolution/DayFunctor.lean,Mathlib/CategoryTheory/Monoidal/Discrete.lean,Mathlib/CategoryTheory/Monoidal/Limits/Preserves.lean,Mathlib/CategoryTheory/MorphismProperty/Composition.lean,Mathlib/CategoryTheory/MorphismProperty/Concrete.lean |
132 |
16 |
['github-actions', 'harahu', 'jcommelin', 'joelriou', 'robin-carlier'] |
jcommelin assignee:jcommelin |
2-9839 2 days ago |
2-16298 2 days ago |
7-64016 7 days |
| 33786 |
hdmkindom author:hdmkindom |
feat(Analysis/Matrix): add Jacobian matrix for matrix-valued functions |
This PR introduces the Jacobian matrix for matrix-valued functions `F : Matrix m n ℝ → Matrix p q ℝ`.
The Jacobian matrix `jacobianMatrix F X` at point `X` is indexed by `(p × q) × (m × n)`, where each entry represents the partial derivative with respect to a basis element. To handle instance-mismatch issues with matrix norms, we use local Frobenius norm instances.
mkdir Analysis/Matrix/Jacobian.lean
## Main definitions
- `jacobianMatrix F X`: The Jacobian matrix at point `X`, defined by `jacobianMatrix F X (i, k) (j, l) = (fderiv ℝ F X (Matrix.single j l 1)) i k`
## Main theorems
- `fderiv_eq_jacobian_mul`: Express the Fréchet derivative as a contraction with the Jacobian
- `jacobianMatrix_comp`: Chain rule for Jacobian matrices
- `jacobianMatrix_linear`, `jacobianMatrix_id`, `jacobianMatrix_const`: Basic properties
- `jacobianMatrix_add`, `jacobianMatrix_smul`: Linearity properties
|
t-analysis
new-contributor
|
219/0 |
Mathlib.lean,Mathlib/Analysis/Matrix/Jacobian.lean |
2 |
1 |
['github-actions'] |
nobody |
2-8811 2 days ago |
2-44520 2 days ago |
2-44561 2 days |
| 33113 |
sinhp author:sinhp |
feat(Category Theory): A natural isomorphism connecting Over.iteratedSlice and Over.map |
This PR provides the following useful nat iso:
```
def iteratedSliceForwardNaturalityIso {g : Over X} (p : f ⟶ g) :
iteratedSliceForward f ⋙ Over.map p.left ≅ Over.map p ⋙ iteratedSliceForward g := ...
def iteratedSliceEquivOverMapIso {f g : Over X} (p : f ⟶ g) :
f.iteratedSliceForward ⋙ Over.map p.left ⋙ g.iteratedSliceBackward ≅ Over.map p := ...
```
And it proves `post forget` is the same thing as `iteratedSliceForward`, thereby unlocking api of `Over.post` for iterated slice functor.
---
[](https://gitpod.io/from-referrer/)
|
t-category-theory
maintainer-merge
|
22/0 |
Mathlib/CategoryTheory/Comma/Over/Basic.lean |
1 |
12 |
['dagurtomas', 'github-actions', 'robin-carlier', 'sinhp'] |
nobody |
2-5327 2 days ago |
2-5327 2 days ago |
5-3107 5 days |
| 33736 |
fbarroero author:fbarroero |
feat(RingTheory/Polynomial/GaussNorm): The `gaussNorm` is an absolute value if `v` is a nonarchimedean absolute value |
We prove
```
Polynomial.gaussNorm_isAbsoluteValue {c : ℝ} {R : Type*} [Ring R] {v : AbsoluteValue R ℝ}
(hna : IsNonarchimedean v) (hc : 0 < c) : IsAbsoluteValue (gaussNorm v c)
```
---
[](https://gitpod.io/from-referrer/)
|
|
194/7 |
Mathlib/Algebra/Order/AbsoluteValue/Basic.lean,Mathlib/Algebra/Order/Ring/IsNonarchimedean.lean,Mathlib/RingTheory/Polynomial/GaussNorm.lean |
3 |
4 |
['copilot-pull-request-reviewer', 'github-actions'] |
nobody |
2-4395 2 days ago |
2-4395 2 days ago |
2-4383 2 days |
| 33656 |
metakunt author:metakunt |
feat(Data/Nat/Choose): Add sum_range_multichoose |
|
t-data |
11/0 |
Mathlib/Data/Nat/Choose/Sum.lean |
1 |
6 |
['eric-wieser', 'github-actions', 'metakunt'] |
nobody |
2-4143 2 days ago |
5-38534 5 days ago |
5-38580 5 days |
| 33551 |
metakunt author:metakunt |
feat(Data/Nat/Factorization/PrimePow): Add Nat.nontrivial_primeFactors_of_two_le_of_not_isPrimePow |
|
t-data |
6/0 |
Mathlib/Data/Nat/Factorization/PrimePow.lean |
1 |
4 |
['Ruben-VandeVelde', 'github-actions', 'metakunt'] |
nobody |
2-3664 2 days ago |
2-3973 2 days ago |
6-21977 6 days |
| 33538 |
JohnnyTeutonic author:JohnnyTeutonic |
feat(Data/Matrix/Cartan): non-simply-laced theorems for F and G |
B/C are left for follow-up
---
[](https://gitpod.io/from-referrer/)
|
maintainer-merge
t-data
|
13/0 |
Mathlib/Data/Matrix/Cartan.lean |
1 |
8 |
['JohnnyTeutonic', 'github-actions', 'robin-carlier'] |
nobody |
2-3098 2 days ago |
2-3098 2 days ago |
7-28572 7 days |
| 33221 |
stepan2698-cpu author:stepan2698-cpu |
feat: definition of an intertwining map |
Adds the definition of an intertwining map of representations, with an instance of an A-module structure. Proves that a multiplication by a central element is an intertwining map.
---
[](https://gitpod.io/from-referrer/)
|
t-algebra
new-contributor
label:t-algebra$ |
162/11 |
Mathlib.lean,Mathlib/RepresentationTheory/Intertwining.lean,Mathlib/RepresentationTheory/Subrepresentation.lean |
3 |
1 |
['github-actions'] |
ocfnash assignee:ocfnash |
2-1430 2 days ago |
19-47096 19 days ago |
19-47140 19 days |
| 33447 |
urkud author:urkud |
feat(FundamentalGroupoid): define simply connected sets |
---
- [x] depends on: #33445
[](https://gitpod.io/from-referrer/)
|
maintainer-merge
t-algebraic-topology
|
102/21 |
Mathlib/AlgebraicTopology/FundamentalGroupoid/Product.lean,Mathlib/AlgebraicTopology/FundamentalGroupoid/SimplyConnected.lean,Mathlib/Topology/Connected/PathConnected.lean |
3 |
15 |
['github-actions', 'mathlib4-dependent-issues-bot', 'mathlib4-merge-conflict-bot', 'robin-carlier', 'urkud'] |
nobody |
2-1366 2 days ago |
2-1366 2 days ago |
2-84805 2 days |
| 33800 |
bryangingechen author:bryangingechen |
ci(lint_and_suggest.yml): rename job |
The previous name "Lint style" is the same as the "Lint style" job in the main CI, which is confusing.
---
[](https://gitpod.io/from-referrer/)
|
easy
CI
|
2/2 |
.github/workflows/lint_and_suggest_pr.yml |
1 |
1 |
['github-actions'] |
nobody |
2-1324 2 days ago |
2-1332 2 days ago |
2-1371 2 days |
| 33795 |
alreadydone author:alreadydone |
feat(Topology/Sheaves): LocalPredicate prerequisite for étalé spaces |
---
[](https://gitpod.io/from-referrer/)
|
t-topology |
417/145 |
Mathlib/AlgebraicGeometry/Modules/Tilde.lean,Mathlib/AlgebraicGeometry/ProjectiveSpectrum/StructureSheaf.lean,Mathlib/Geometry/Manifold/Sheaf/Smooth.lean,Mathlib/Logic/Equiv/Basic.lean,Mathlib/Topology/Sheaves/LocalPredicate.lean,Mathlib/Topology/Sheaves/Sheafify.lean,Mathlib/Topology/Sheaves/Stalks.lean |
7 |
1 |
['github-actions'] |
nobody |
1-86190 1 day ago |
2-5645 2 days ago |
2-5624 2 days |
| 29241 |
yoh-tanimoto author:yoh-tanimoto |
feat(Analysis/InnerProductSpace/Orthogonal): add duplicates for `ClosedSubmodule` |
add duplicates of definitions and API's for `ClosedSubmodule` in an `InnerProductSpace`.
motivation: when one considers a Hilbert space (`CompleteSpace`), it is more natural to consider `ClosedSubmodule`s. They form a complete lattice and satisfy `sup_orthogonal` #29243.
- [x] depends on: #29230 for `Lattice` `CompleteLattice` |
|
161/9 |
Mathlib/Analysis/Convex/Cone/Basic.lean,Mathlib/Analysis/Convex/Cone/Dual.lean,Mathlib/Analysis/InnerProductSpace/Orthogonal.lean,Mathlib/Topology/Algebra/Module/ClosedSubmodule.lean |
4 |
19 |
['github-actions', 'mathlib4-dependent-issues-bot', 'mathlib4-merge-conflict-bot', 'sgouezel', 'yoh-tanimoto'] |
sgouezel assignee:sgouezel |
1-85876 1 day ago |
4-63292 4 days ago |
17-51226 17 days |
| 33723 |
erdOne author:erdOne |
feat(Analytic): `℘'(z)² = 4 ℘(z)³ - g₂ ℘(z) - g₃` |
---
[](https://gitpod.io/from-referrer/)
|
t-analysis |
437/40 |
Mathlib/Algebra/Module/ZLattice/Basic.lean,Mathlib/Analysis/Analytic/Order.lean,Mathlib/Analysis/Calculus/ContDiff/Basic.lean,Mathlib/Analysis/Calculus/ContDiff/Operations.lean,Mathlib/Analysis/Calculus/IteratedDeriv/Defs.lean,Mathlib/Analysis/Calculus/IteratedDeriv/Lemmas.lean,Mathlib/Analysis/Meromorphic/Basic.lean,Mathlib/Analysis/Meromorphic/Order.lean,Mathlib/Analysis/SpecialFunctions/Elliptic/Weierstrass.lean,Mathlib/Analysis/SpecialFunctions/Trigonometric/Cotangent.lean,Mathlib/Geometry/Manifold/Instances/Sphere.lean |
11 |
60 |
['erdOne', 'github-actions', 'loefflerd', 'vihdzp'] |
nobody |
1-84101 1 day ago |
1-84101 1 day ago |
2-76946 2 days |
| 33535 |
erdOne author:erdOne |
feat(Algebra/Category): `Under.pushout` preserves finite limits for flat homomorphisms |
---
[](https://gitpod.io/from-referrer/)
|
t-algebra label:t-algebra$ |
157/5 |
Mathlib.lean,Mathlib/Algebra/Category/AlgCat/Basic.lean,Mathlib/Algebra/Category/AlgCat/Limits.lean,Mathlib/Algebra/Category/CommAlgCat/BaseChange.lean,Mathlib/Algebra/Category/CommAlgCat/Basic.lean,Mathlib/Algebra/Category/ModuleCat/ChangeOfRings.lean,Mathlib/Algebra/Category/ModuleCat/Limits.lean,Mathlib/Algebra/Category/Ring/Flat.lean |
8 |
2 |
['github-actions', 'robin-carlier'] |
eric-wieser assignee:eric-wieser |
1-83965 1 day ago |
1-83965 1 day ago |
7-40771 7 days |
| 32856 |
stepan2698-cpu author:stepan2698-cpu |
feat: definition of an irreducible representation |
Define irreducible monoid representations over a field and prove that a monoid representation is irreducible iff the corresponding module over the monoid algebra is simple. |
t-algebra
new-contributor
label:t-algebra$ |
129/10 |
Mathlib.lean,Mathlib/RepresentationTheory/Irreducible.lean,Mathlib/RepresentationTheory/Subrepresentation.lean |
3 |
23 |
['Whysoserioushah', 'erdOne', 'github-actions', 'stepan2698-cpu'] |
kim-em assignee:kim-em |
1-80230 1 day ago |
28-71128 28 days ago |
28-71165 28 days |
| 30640 |
SnirBroshi author:SnirBroshi |
feat(Combinatorics/SimpleGraph/Acyclic): acyclic and bridge theorems |
---
- [x] depends on: #30542
- [x] depends on: #30570
[](https://gitpod.io/from-referrer/)
|
t-combinatorics |
76/82 |
Mathlib/Combinatorics/SimpleGraph/Acyclic.lean,Mathlib/Combinatorics/SimpleGraph/Connectivity/Connected.lean |
2 |
7 |
['SnirBroshi', 'b-mehta', 'github-actions', 'mathlib4-dependent-issues-bot', 'mathlib4-merge-conflict-bot'] |
b-mehta assignee:b-mehta |
1-74808 1 day ago |
3-56433 3 days ago |
33-18114 33 days |
| 33726 |
alreadydone author:alreadydone |
feat(Analysis): (complex) polynomials as branched coverings |
originally proposed by @urkud in #33425
---
[](https://gitpod.io/from-referrer/)
|
t-topology
t-analysis
large-import
|
123/1 |
Mathlib/Algebra/Polynomial/Roots.lean,Mathlib/Analysis/Complex/CoveringMap.lean,Mathlib/Topology/Algebra/Polynomial.lean,Mathlib/Topology/Covering/Basic.lean |
4 |
n/a |
['alreadydone', 'github-actions', 'mathlib4-merge-conflict-bot'] |
nobody |
1-64917 1 day ago |
unknown |
unknown |
| 33409 |
jsm28 author:jsm28 |
feat(LinearAlgebra/AffineSpace/Ceva): Ceva's theorem |
Add Ceva's theorem. Unlike various previous attempts, I think this in appropriate generality for mathlib; it starts with a version for an arbitary (possibly infinite) affinely independent family of points (not necessarily spanning the whole space), in any affine space over any ring, and with the second point given on each line not necessarily being on the opposite face, then deduces a simpler version for a finite family, then deduces versions for a triangle, now with actual cevians (lines between a vertex and a point on the opposite side), either just multiplying weights (here the ring requires no zero divisors) or expressed with a product of divisions equal to 1 (here it becomes a field).
This doesn't include any form of the converse (with a "concurrent or parallel" conclusion, and note that you don't need affine independence for the converse), or variants of the forward direction where you're given parallel lines rather than concurrent lines, but I think those things can reasonably be done in followups.
---
[](https://gitpod.io/from-referrer/)
|
t-algebra
t-euclidean-geometry
label:t-algebra$ |
311/0 |
Mathlib.lean,Mathlib/Analysis/Normed/Affine/Ceva.lean,Mathlib/LinearAlgebra/AffineSpace/AffineSubspace/Basic.lean,Mathlib/LinearAlgebra/AffineSpace/Ceva.lean,docs/100.yaml,docs/1000.yaml |
6 |
11 |
['github-actions', 'jsm28', 'ocfnash', 'plby'] |
mariainesdff and ocfnash assignee:ocfnash assignee:mariainesdff |
1-64036 1 day ago |
2-14426 2 days ago |
11-69775 11 days |
| 33588 |
JovanGerb author:JovanGerb |
chore(Geometry/Euclidean/SignedDist): remove `privateInPublic` |
When I originally PRed `signedDistLinear`, I wasn't sure whether it should be marked `private`. It seems now that it should not have been private, because this violates `privateInPublic`. This PR fixes that.
---
[](https://gitpod.io/from-referrer/)
|
t-euclidean-geometry
maintainer-merge
|
4/14 |
Mathlib/Geometry/Euclidean/SignedDist.lean |
1 |
5 |
['JovanGerb', 'github-actions', 'jsm28', 'vihdzp'] |
jsm28 assignee:jsm28 |
1-63891 1 day ago |
1-63891 1 day ago |
6-31352 6 days |
| 33802 |
stepan2698-cpu author:stepan2698-cpu |
feat: Schur's lemma for monoid representations |
Adds an algebra instance on the set of intertwining maps. Proves various versions of Schur's lemma for monoid representations and proves that a finite-dimensional irreducible representation of a commutative monoid is one-dimensional.
- depends on: #32856
- depends on: #33221
---
[](https://gitpod.io/from-referrer/)
|
t-algebra
new-contributor
label:t-algebra$ |
458/11 |
Mathlib.lean,Mathlib/RepresentationTheory/Intertwining.lean,Mathlib/RepresentationTheory/Irreducible.lean,Mathlib/RepresentationTheory/Subrepresentation.lean |
4 |
2 |
['alreadydone', 'github-actions'] |
nobody |
1-63627 1 day ago |
1-81326 1 day ago |
1-81375 1 day |
| 33491 |
themathqueen author:themathqueen |
feat(Analysis/InnerProductSpace): linear map is positive iff it equals the sum of rank-one operators |
... and equality of nonzero rank-one operators means the elements are colinear.
---
The proof of `rankOne_normalize_eq_rankOne_normalize_iff` is kinda messy. Feel free to golf.
- [x] depends on: #33439
[](https://gitpod.io/from-referrer/)
|
t-analysis |
97/5 |
Mathlib/Analysis/InnerProductSpace/LinearMap.lean,Mathlib/Analysis/InnerProductSpace/Positive.lean,Mathlib/Analysis/InnerProductSpace/Symmetric.lean |
3 |
3 |
['github-actions', 'mathlib4-dependent-issues-bot', 'themathqueen'] |
urkud assignee:urkud |
1-59706 1 day ago |
4-78509 4 days ago |
4-78506 4 days |
| 33594 |
smmercuri author:smmercuri |
feat: `HeightOneSpectrum.valuation` is rank one for number fields |
- If `K` is a number field and `v` is a height-one prime ideal then `v.valuation K` is rank one.
- In general, if `v` is a rank one valuation of `K`, then its extension to the `v`-adic completion `v.Completion` is also rank one, provided in `Valuation.instRankOneCompletion`
- Together these refactor and deprecate `instRankOneValuedAdicCompletion`.
---
[](https://gitpod.io/from-referrer/)
|
large-import |
18/8 |
Mathlib/NumberTheory/NumberField/FinitePlaces.lean,Mathlib/RingTheory/Valuation/RankOne.lean |
2 |
2 |
['github-actions', 'smmercuri'] |
jcommelin assignee:jcommelin |
1-59704 1 day ago |
6-15720 6 days ago |
6-15726 6 days |
| 33643 |
vihdzp author:vihdzp |
feat: `r < stdPart x → r < x` |
---
[](https://gitpod.io/from-referrer/)
|
t-algebra label:t-algebra$ |
25/4 |
Mathlib/Algebra/Order/Ring/StandardPart.lean |
1 |
1 |
['github-actions'] |
dagurtomas assignee:dagurtomas |
1-59703 1 day ago |
5-57412 5 days ago |
5-57449 5 days |
| 33657 |
vihdzp author:vihdzp |
chore(SetTheory/Cardinal/Arithmetic): switch `lift.{max u w} x = lift.{max v w} y` to `lift.{u} x = lift.{v} y` |
---
Lean can't often infer the extra `w` universe otherwise. Oh, if only we had some sort of `liftEq` predicate so we didn't have to bother with `lift` at all.
[](https://gitpod.io/from-referrer/)
|
t-set-theory |
13/13 |
Mathlib/SetTheory/Cardinal/Arithmetic.lean,Mathlib/SetTheory/Cardinal/Basic.lean |
2 |
1 |
['github-actions'] |
alreadydone assignee:alreadydone |
1-59701 1 day ago |
5-38040 5 days ago |
5-38080 5 days |
| 33662 |
Pjotr5 author:Pjotr5 |
feat(Algebra/Order/BigOperators/Expect): add lemmas and strict variants |
### Summary
- Combine `le_expect_nonempty_of_subadditive` and `le_expect_of_subadditive` into a single lemma `le_expect_of_subadditive`.
The extra assumptions `(hs : s.Nonempty)` and `(h_zero : m 0 = 0)` are unnecessary (since `m 0 = 0` follows from `h_div`).
This requires a small downstream update to `Mathlib/Analysis/RCLike/Basic.lean` (`norm_expect_le`).
- Add strict-inequality variants:
`expect_lt_expect`, `expect_lt`, `lt_expect`.
- Add existence lemmas:
`exists_le_of_expect_le_expect`, `exists_le_of_le_expect`, `exists_le_of_expect_le`,
and `exists_lt_of_expect_lt_expect`.
---
[](https://gitpod.io/from-referrer/)
|
new-contributor |
46/16 |
Mathlib/Algebra/Order/BigOperators/Expect.lean,Mathlib/Analysis/RCLike/Basic.lean |
2 |
1 |
['github-actions'] |
dagurtomas assignee:dagurtomas |
1-59700 1 day ago |
5-30015 5 days ago |
5-30001 5 days |
| 33668 |
Citronhat author:Citronhat |
feat(PMF): add lintegral formulas for PMF |
This PR introduces two lemmas describing the `lintegral` of a function with respect to the measure induced by a probability mass function:
- `PMF.lintegral_eq_tsum`
- `PMF.lintegral_eq_sum`
These are the `ℝ≥0∞` analogues of the existing Bochner `integral` formulas `integral_eq_tsum` and `integral_eq_sum`. They could be useful for reasoning about expectations and integrability.
In addition, the proof of `integral_eq_sum` is simplified by deriving it directly from `integral_eq_tsum` using `tsum_fintype`. |
t-measure-probability
new-contributor
|
14/5 |
Mathlib/Probability/ProbabilityMassFunction/Integrals.lean |
1 |
1 |
['github-actions'] |
kex-y assignee:kex-y |
1-59699 1 day ago |
5-11870 5 days ago |
5-11915 5 days |
| 33672 |
euprunin author:euprunin |
chore: golf using `grind`. add `grind` annotations. |
---
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):
* `Orientation.nonneg_inner_and_areaForm_eq_zero_iff_sameRay`: 287 ms before, 336 ms after
* `PFunctor.liftr_iff`: 49 ms before, 93 ms after
* `IsAdjoinRootMonic.coeff_root_pow`: 119 ms before, 267 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/)
|
|
9/33 |
Mathlib/Analysis/InnerProductSpace/TwoDim.lean,Mathlib/Data/PFunctor/Univariate/Basic.lean,Mathlib/RingTheory/IsAdjoinRoot.lean |
3 |
3 |
['euprunin', 'github-actions', 'leanprover-radar'] |
dwrensha assignee:dwrensha |
1-59698 1 day ago |
5-288 5 days ago |
5-265 5 days |
| 33676 |
YuvalFilmus author:YuvalFilmus |
feat(Chebyshev/Orthogonality): Chebyshev T polynomials are orthogonal |
We prove that the Chebyshev T polynomials are orthogonal with respect to `1 / √ (1 - x ^ 2)`.
Similarly, one could show that the Chebyshev U polynomials are orthogonal with respect to `√ (1 - x ^ 2)`, which I will do once this PR is approved.
More generally, one defines an inner product space on the space of all real polynomials, where the inner product is as defined above.
I will be happy to add this to the present or a future PR.
---
[](https://gitpod.io/from-referrer/)
|
t-analysis |
138/0 |
Mathlib.lean,Mathlib/Analysis/SpecialFunctions/Trigonometric/Chebyshev/Orthogonality.lean |
2 |
2 |
['github-actions', 'wwylele'] |
j-loreaux assignee:j-loreaux |
1-59697 1 day ago |
4-83071 4 days ago |
4-83112 4 days |
| 33679 |
DavidLedvinka author:DavidLedvinka |
feat(MeasureTheory): add formulas for the measures formed by a density with respect to counting or dirac measures. |
Like with most theorems that ultimately rely on application of dirac measures, there are primed versions for when the function (or set in other cases) is measurable, and unprimed versions for when `MeasurableSingletonClass` is assumed. |
t-measure-probability |
21/0 |
Mathlib/MeasureTheory/Measure/WithDensity.lean |
1 |
1 |
['github-actions'] |
urkud assignee:urkud |
1-59696 1 day ago |
4-79587 4 days ago |
4-79628 4 days |
| 33688 |
Citronhat author:Citronhat |
feat(PMF): add expectation lemmas for Poisson PMF |
This PR adds some basic results about the Poisson distribution, its `PMF`, and its expectation.
**New lemmas:**
* `poissonPMF_apply` — an unfolding lemma for `poissonPMF`.
* `poissonPMFReal_mul_eq_succ_mul` — the standard recursion identity for the Poisson mass function.
* `poissonPMFReal_hasSum_nmul` — shows that `fun n ↦ poissonPMFReal r n * n` has sum `r`.
* `poissonPMF_tsum_nmul` — the corresponding identity at the level of the `PMF`.
* `poissonPMF_coe_tsum_nmul` — the same result after coercion to `ℝ`.
Both `ℝ`-valued and `ℝ≥0∞`-valued formulations are included so that these results can be used conveniently in both Lebesgue and Bochner integration contexts. |
t-measure-probability
new-contributor
|
21/0 |
Mathlib/Probability/Distributions/Poisson.lean |
1 |
2 |
['Citronhat', 'github-actions'] |
urkud assignee:urkud |
1-59696 1 day ago |
4-68742 4 days ago |
4-68780 4 days |
| 33801 |
artie2000 author:artie2000 |
chore: add missing mem lemmas |
* Add missing `simp` lemmas `mem_foo` where a `simp` lemma `coe_foo` already exists
---
[](https://gitpod.io/from-referrer/)
|
t-meta |
21/5 |
Mathlib/AlgebraicGeometry/OpenImmersion.lean,Mathlib/AlgebraicGeometry/Scheme.lean,Mathlib/RingTheory/DedekindDomain/Different.lean,Mathlib/RingTheory/FractionalIdeal/Basic.lean,Mathlib/RingTheory/FractionalIdeal/Extended.lean,Mathlib/Topology/Category/TopCat/Opens.lean,Mathlib/Topology/Sets/Opens.lean |
7 |
2 |
['artie2000', 'github-actions'] |
nobody |
1-52467 1 day ago |
1-52467 1 day ago |
2-380 2 days |
| 32186 |
urkud author:urkud |
feat(Integral): estimate displacement by the integral of the speed |
This PR adds yet another form of the Mean Value Theorem.
---
[](https://gitpod.io/from-referrer/)
|
t-measure-probability |
207/0 |
Mathlib.lean,Mathlib/MeasureTheory/Integral/IntervalIntegral/DistLEIntegral.lean |
2 |
1 |
['github-actions'] |
nobody |
1-41200 1 day ago |
1-41221 1 day ago |
44-78427 44 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/)
|
t-algebra label:t-algebra$ |
161/22 |
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 |
20 |
['dupuisf', 'eric-wieser', 'github-actions', 'mathlib4-merge-conflict-bot', 'plp127'] |
nobody |
1-39728 1 day ago |
2-76449 2 days ago |
2-76427 2 days |
| 32541 |
YaelDillies author:YaelDillies |
chore: import Tactic.Attr.Register privately |
This is mostly to start a discussion: Should basic tactic files like this one be re-exported by all files out of them being basic, or whether they should be explicitly imported by the few files that actually need it.
Eg in #32245 Andrew and I are adding a new simp attribute, and it's a bit silly that we have to rebuild all of mathlib because that file is re-exported everywhere.
---
[](https://gitpod.io/from-referrer/)
|
large-import |
39/6 |
Mathlib/Algebra/Free.lean,Mathlib/Algebra/Group/Units/Basic.lean,Mathlib/CategoryTheory/Monoidal/Mon_.lean,Mathlib/Control/Applicative.lean,Mathlib/Control/Basic.lean,Mathlib/Control/Functor.lean,Mathlib/Control/Monad/Basic.lean,Mathlib/Control/Traversable/Basic.lean,Mathlib/Control/Traversable/Equiv.lean,Mathlib/Control/Traversable/Lemmas.lean,Mathlib/Data/Prod/Basic.lean,Mathlib/Data/Set/Operations.lean,Mathlib/Logic/Basic.lean,Mathlib/Logic/Equiv/Defs.lean,Mathlib/Logic/Function/Basic.lean,Mathlib/Logic/Function/Defs.lean,Mathlib/Logic/Nontrivial/Basic.lean,Mathlib/Tactic/Attr/Core.lean,Mathlib/Tactic/HigherOrder.lean,Mathlib/Tactic/Zify.lean |
20 |
6 |
['EtienneC30', 'YaelDillies', 'artie2000', 'github-actions', 'mathlib4-merge-conflict-bot'] |
kex-y assignee:kex-y |
1-29228 1 day ago |
1-33349 1 day ago |
34-63823 34 days |
| 33774 |
SnO2WMaN author:SnO2WMaN |
doc(100.yaml, 1000.yaml): Update about Gödel's Incompleteness Theorem |
---
[](https://gitpod.io/from-referrer/)
|
new-contributor |
4/4 |
docs/100.yaml,docs/1000.yaml |
2 |
2 |
['github-actions'] |
nobody |
1-28514 1 day ago |
2-67583 2 days ago |
2-67572 2 days |
| 33753 |
SnO2WMaN author:SnO2WMaN |
doc(1000.yaml): Mention Tarski's Undefinability Theorem in FFL |
---
[](https://gitpod.io/from-referrer/)
|
new-contributor |
3/0 |
docs/1000.yaml |
1 |
3 |
['SnO2WMaN', 'SnirBroshi', 'github-actions'] |
nobody |
1-28307 1 day ago |
3-19887 3 days ago |
3-19873 3 days |
| 32745 |
LTolDe author:LTolDe |
feat(Topology/Algebra): add MulActionConst.lean |
add Topology/Algebra/MulActionConst.lean
introduce class `ContinuousSMulConst` for a scalar multiplication that is continuous in the first argument, in analogy to `ContinuousConstSMul`
define `MulAction.ball x U` as the set `U • {x}` given `[SMul G X] (x : X) (U : Set G)`
The lemmas shown here will be useful to prove the **Effros Theorem**, see [zulip](https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/Effros.20Theorem/with/558712441).
---
[](https://gitpod.io/from-referrer/)
|
t-topology
new-contributor
|
98/0 |
Mathlib.lean,Mathlib/Topology/Algebra/MulActionConst.lean |
2 |
1 |
['github-actions'] |
dagurtomas assignee:dagurtomas |
1-27150 1 day ago |
31-3035 1 month ago |
31-3088 31 days |
| 31653 |
ster99 author:ster99 |
feat(MeasureTheory): Foelner filters |
Define a predicate for a filter to be Foelner. Prove that if a measure space with a G-action has a Foelner filter then there is a left-invariant finitely additive probability measure on it (amenability).
Define the maximal Foelner filter and prove that if the maximal Foelner filter is nontrivial, then the amenability condition above holds.
Closes #29213.
---
depends on : #32117.
[](https://gitpod.io/from-referrer/)
|
new-contributor |
188/0 |
Mathlib.lean,Mathlib/MeasureTheory/Group/FoelnerFilter.lean,Mathlib/MeasureTheory/Measure/MeasureSpace.lean |
3 |
68 |
['ADedecker', 'YaelDillies', 'github-actions', 'mathlib4-merge-conflict-bot', 'ster99'] |
nobody |
1-24040 1 day ago |
2-12226 2 days ago |
3-34270 3 days |
| 33770 |
eric-wieser author:eric-wieser |
chore(RingTheory/Morita/Matrix): remove uses of `default` |
Using `default` here just makes the spelling longer and less general. The docstring already say `Eᵢᵢ`, so these functions should take `i`.
---
[](https://gitpod.io/from-referrer/)
|
t-ring-theory |
23/22 |
Mathlib/RingTheory/Morita/Matrix.lean |
1 |
1 |
['Whysoserioushah', 'github-actions'] |
nobody |
1-21759 1 day ago |
2-72637 2 days ago |
2-72616 2 days |
| 32757 |
AntoineChambert-Loir author:AntoineChambert-Loir |
feat(LinearAlgebra/Transvection): the determinant of a transvection is equal to 1. |
Prove that the determinant of a transvection is equal to 1
The proof goes by showing that the determinant of `LinearMap.transvection f v` is `1 + f v` (even if `f v` is nonzero).
I first treat the case of a field, distinguishing whether `f v = 0` (so that we get
a transvection) or not (so that we have a dilation).
Then, by base change to the field of fractions, I can handle the case of a domain. Finally, the general case is treated by base change from the “universal case” where the base ring is the ring of polynomials in $$2n$$ indeterminates corresponding to the coefficients of $$f$$ and $$v$$.
---
- [x] depends on: #31138
[](https://gitpod.io/from-referrer/)
|
|
255/0 |
Mathlib/LinearAlgebra/Determinant.lean,Mathlib/LinearAlgebra/Transvection.lean |
2 |
n/a |
['AntoineChambert-Loir', 'alreadydone', 'github-actions', 'mathlib4-dependent-issues-bot', 'mathlib4-merge-conflict-bot'] |
nobody |
1-19936 1 day ago |
unknown |
unknown |
| 33347 |
AntoineChambert-Loir author:AntoineChambert-Loir |
feat(LinearAlgebra/Transvection/Basic): define dilatransvections |
Define `LinearEquiv.dilatransvections`.
These are linear equivalences whose associated linear map is a transvection.
This definition has the interest of being usable without any assumption on the base ring.
Over a division ring, they correspond exactly to those linear equivalences `e` such that `e - LinearMap.id` has rank at most one.
They (will) appear in Dieudonné's theorem that describes the generation of elements of the general linear group as products of several transvections and one additional dilatransvection.
---
[](https://gitpod.io/from-referrer/)
|
t-algebra label:t-algebra$ |
204/32 |
Mathlib/LinearAlgebra/Transvection.lean |
1 |
n/a |
['AntoineChambert-Loir', 'eric-wieser', 'github-actions', 'mathlib4-merge-conflict-bot'] |
nobody |
1-15596 1 day ago |
unknown |
unknown |
| 33812 |
urkud author:urkud |
feat: define `List.offDiag` |
Use it to drop decidability assumption in `Finset.offDiag`. Also redefine `Finset.diag`.
---
Built on top of #12632, reopened from a fork.
[](https://gitpod.io/from-referrer/)
|
t-data |
187/60 |
Mathlib.lean,Mathlib/Algebra/BigOperators/Group/Finset/Basic.lean,Mathlib/Data/Finite/Prod.lean,Mathlib/Data/Finset/Prod.lean,Mathlib/Data/Finset/Sym.lean,Mathlib/Data/Fintype/Prod.lean,Mathlib/Data/List/Flatten.lean,Mathlib/Data/List/Nodup.lean,Mathlib/Data/List/OffDiag.lean,Mathlib/Tactic/GCongr/CoreAttrs.lean,Mathlib/Topology/MetricSpace/Infsep.lean |
11 |
3 |
['eric-wieser', 'github-actions', 'urkud'] |
nobody |
1-11318 1 day ago |
1-34343 1 day ago |
1-51746 1 day |
| 33772 |
urkud author:urkud |
chore(*): rename `EMetric.infEdist` -> `Metric.infEDist` etc |
Moves:
- ConvexBody.hausdorffEdist_coe -> ConvexBody.hausdorffEDist_coe
- ConvexBody.hausdorffEdist_ne_top -> ConvexBody.hausdorffEDist_ne_top
- EMetric.Closeds.edist_eq -> TopologicalSpace.Closeds.edist_eq
- EMetric.Closeds.isometry_singleton -> TopologicalSpace.Closeds.isometry_singleton
- EMetric.Closeds.lipschitz_sup -> TopologicalSpace.Closeds.lipschitz_sup
- EMetric.NonemptyCompacts.isClosed_in_closeds -> TopologicalSpace.NonemptyCompacts.isClosed_in_closeds
- EMetric.NonemptyCompacts.isometry_singleton -> TopologicalSpace.NonemptyCompacts.isometry_singleton
- EMetric.NonemptyCompacts.isometry_toCloseds -> TopologicalSpace.NonemptyCompacts.isometry_toCloseds
- EMetric.NonemptyCompacts.lipschitz_prod -> TopologicalSpace.NonemptyCompacts.lipschitz_prod
- EMetric.NonemptyCompacts.lipschitz_sup -> TopologicalSpace.NonemptyCompacts.lipschitz_sup
- EMetric.continuous_infEdist -> Metric.continuous_infEDist
- EMetric.continuous_infEdist_hausdorffEdist -> TopologicalSpace.Closeds.continuous_infEDist_hausdorffEDist
- EMetric.disjoint_closedBall_of_lt_infEdist -> Metric.disjoint_closedEBall_of_lt_infEDist
- EMetric.edist_le_infEdist_add_ediam -> Metric.edist_le_infEDist_add_ediam
- EMetric.empty_or_nonempty_of_hausdorffEdist_ne_top -> Metric.empty_or_nonempty_of_hausdorffEDist_ne_top
- EMetric.exists_edist_lt_of_hausdorffEdist_lt -> Metric.exists_edist_lt_of_hausdorffEDist_lt
- EMetric.exists_pos_forall_lt_edist -> Metric.exists_pos_forall_lt_edist
- EMetric.exists_real_pos_lt_infEdist_of_notMem_closure -> Metric.exists_real_pos_lt_infEDist_of_notMem_closure
- EMetric.hausdorffEdist -> Metric.hausdorffEDist
- EMetric.hausdorffEdist_closure -> Metric.hausdorffEDist_closure
- EMetric.hausdorffEdist_closure₁ -> Metric.hausdorffEDist_closure_left
- EMetric.hausdorffEdist_closure₂ -> Metric.hausdorffEDist_closure_right
- EMetric.hausdorffEdist_comm -> Metric.hausdorffEDist_comm
- EMetric.hausdorffEdist_def -> Metric.hausdorffEDist_def
- EMetric.hausdorffEdist_empty -> Metric.hausdorffEDist_empty
- EMetric.hausdorffEdist_iUnion_le -> Metric.hausdorffEDist_iUnion_le
- EMetric.hausdorffEdist_image -> Metric.hausdorffEDist_image
- EMetric.hausdorffEdist_le_ediam -> Metric.hausdorffEDist_le_ediam
- EMetric.hausdorffEdist_le_of_infEdist -> Metric.hausdorffEDist_le_of_infEDist
- EMetric.hausdorffEdist_le_of_mem_edist -> Metric.hausdorffEDist_le_of_mem_edist
- EMetric.hausdorffEdist_le_of_mem_hausdorffEntourage -> Metric.hausdorffEDist_le_of_mem_hausdorffEntourage
- EMetric.hausdorffEdist_prod_le -> Metric.hausdorffEDist_prod_le
- EMetric.hausdorffEdist_self -> Metric.hausdorffEDist_self
- EMetric.hausdorffEdist_self_closure -> Metric.hausdorffEDist_self_closure
- EMetric.hausdorffEdist_singleton -> Metric.hausdorffEDist_singleton
- EMetric.hausdorffEdist_triangle -> Metric.hausdorffEDist_triangle
- EMetric.hausdorffEdist_union_le -> Metric.hausdorffEDist_union_le
- EMetric.hausdorffEdist_zero_iff_closure_eq_closure -> Metric.hausdorffEDist_zero_iff_closure_eq_closure
- EMetric.hausdorffEdist_zero_iff_eq_of_closed -> IsClosed.hausdorffEDist_zero_iff
- EMetric.infEdist -> Metric.infEDist
- EMetric.infEdist_anti -> Metric.infEDist_anti
- EMetric.infEdist_biUnion -> Metric.infEDist_biUnion
- EMetric.infEdist_closure -> Metric.infEDist_closure
- EMetric.infEdist_closure_pos_iff_notMem_closure -> Metric.infEDist_closure_pos_iff_notMem_closure
- EMetric.infEdist_empty -> Metric.infEDist_empty
- EMetric.infEdist_iUnion -> Metric.infEDist_iUnion
- EMetric.infEdist_image -> Metric.infEDist_image
- EMetric.infEdist_le_edist_add_infEdist -> Metric.infEDist_le_edist_add_infEDist
- EMetric.infEdist_le_edist_of_mem -> Metric.infEDist_le_edist_of_mem
- EMetric.infEdist_le_hausdorffEdist_of_mem -> Metric.infEDist_le_hausdorffEDist_of_mem
- EMetric.infEdist_le_infEdist_add_edist -> Metric.infEDist_le_infEDist_add_edist
- EMetric.infEdist_le_infEdist_add_hausdorffEdist -> Metric.infEDist_le_infEDist_add_hausdorffEDist
- EMetric.infEdist_lt_iff -> Metric.infEDist_lt_iff
- EMetric.infEdist_pos_iff_notMem_closure -> Metric.infEDist_pos_iff_notMem_closure
- EMetric.infEdist_prod -> Metric.infEDist_prod
- EMetric.infEdist_singleton -> Metric.infEDist_singleton
- EMetric.infEdist_smul -> Metric.infEDist_smul
- EMetric.infEdist_union -> Metric.infEDist_union
- EMetric.infEdist_vadd -> Metric.infEDist_vadd
- EMetric.infEdist_zero_of_mem -> Metric.infEDist_zero_of_mem
- EMetric.le_infEdist -> Metric.le_infEDist
- EMetric.mem_closure_iff_infEdist_zero -> Metric.mem_closure_iff_infEDist_zero
- EMetric.mem_hausdorffEntourage_of_hausdorffEdist_lt -> Metric.mem_hausdorffEntourage_of_hausdorffEDist_lt
- EMetric.mem_iff_infEdist_zero_of_closed -> Metric.mem_iff_infEDist_zero_of_closed
- EMetric.nonempty_of_hausdorffEdist_ne_top -> Metric.nonempty_of_hausdorffEDist_ne_top
- EmetricSpace.ofRiemannianMetric -> EMetricSpace.ofRiemannianMetric
- IsCompact.exists_infEdist_eq_edist -> IsCompact.exists_infEDist_eq_edist
- Measurable.infEdist -> Measurable.infEDist
- Metric.cthickening_eq_preimage_infEdist -> Metric.cthickening_eq_preimage_infEDist
- Metric.eventually_notMem_cthickening_of_infEdist_pos -> Metric.eventually_notMem_cthickening_of_infEDist_pos
- Metric.eventually_notMem_thickening_of_infEdist_pos -> Metric.eventually_notMem_thickening_of_infEDist_pos
- Metric.hausdorffEdist_ne_top_of_nonempty_of_bounded -> Metric.hausdorffEDist_ne_top_of_nonempty_of_bounded
- Metric.infEdist_eq_top_iff -> Metric.infEDist_eq_top_iff
- Metric.infEdist_le_infEdist_cthickening_add -> Metric.infEDist_le_infEDist_cthickening_add
- Metric.infEdist_le_infEdist_thickening_add -> Metric.infEDist_le_infEDist_thickening_add
- Metric.infEdist_ne_top -> Metric.infEDist_ne_top
- Metric.mem_thickening_iff_infEdist_lt -> Metric.mem_thickening_iff_infEDist_lt
- Metric.thickening_eq_preimage_infEdist -> Metric.thickening_eq_preimage_infEDist
- PseudoEmetricSpace.ofEdistOfTopology -> PseudoEMetricSpace.ofEDistOfTopology
- PseudoEmetricSpace.ofRiemannianMetric -> PseudoEMetricSpace.ofRiemannianMetric
- infEdist_cthickening -> infEDist_cthickening
- infEdist_inv -> infEDist_inv
- infEdist_inv_inv -> infEDist_inv_inv
- infEdist_neg -> infEDist_neg
- infEdist_neg_neg -> infEDist_neg_neg
- infEdist_smul₀ -> infEDist_smul₀
- infEdist_thickening -> infEDist_thickening
- measurable_infEdist -> measurable_infEDist
- thickenedIndicatorAux_mono_infEdist -> thickenedIndicatorAux_mono_infEDist
- thickenedIndicator_mono_infEdist -> thickenedIndicator_mono_infEDist
Also renames some instances.
---
[](https://gitpod.io/from-referrer/) |
|
708/480 |
Mathlib/Analysis/Convex/Body.lean,Mathlib/Analysis/Normed/Group/Pointwise.lean,Mathlib/Analysis/Normed/Lp/PiLp.lean,Mathlib/Analysis/Normed/Module/Ball/Pointwise.lean,Mathlib/Analysis/SpecificLimits/Basic.lean,Mathlib/Geometry/Manifold/Riemannian/Basic.lean,Mathlib/MeasureTheory/Constructions/BorelSpace/Metric.lean,Mathlib/MeasureTheory/Measure/Hausdorff.lean,Mathlib/Topology/EMetricSpace/Defs.lean,Mathlib/Topology/MetricSpace/Closeds.lean,Mathlib/Topology/MetricSpace/GromovHausdorff.lean,Mathlib/Topology/MetricSpace/HausdorffDistance.lean,Mathlib/Topology/MetricSpace/ThickenedIndicator.lean,Mathlib/Topology/MetricSpace/Thickening.lean,docs/overview.yaml |
15 |
13 |
['gasparattila', 'github-actions', 'urkud'] |
nobody |
1-11126 1 day ago |
2-69494 2 days ago |
2-69471 2 days |
| 33552 |
YaelDillies author:YaelDillies |
feat: a non-domain cannot act faithfully on a domain |
---
[](https://gitpod.io/from-referrer/)
|
t-algebra
maintainer-merge
label:t-algebra$ |
8/0 |
Mathlib/Algebra/Algebra/Basic.lean |
1 |
8 |
['YaelDillies', 'erdOne', 'github-actions', 'tb65536'] |
nobody |
1-10742 1 day ago |
1-10742 1 day ago |
6-82671 6 days |
| 33312 |
YuvalFilmus author:YuvalFilmus |
feat(Polynomial/Chebyshev): formulas for iterated derivatives of T and U at 1 |
The main results are `iterate_derivative_T_eval_one` and `iterate_derivative_U_eval_one`.
These are derived using recurrences which for at every point, and in particular, `iterate_derivative_T_eval_zero` and `iterate_derivative_U_eval_zero` gives the recurrences at zero.
In principle, by combining with #33311, one can compute the explicit formula for the derivative at zero.
A subsequent PR will derive consequences for these polynomials over the reals (these should work for every field).
The file is getting rather long — not sure what to do about it.
---
- [ ] depends on: #33283
- [ ] depends on: #33306
[](https://gitpod.io/from-referrer/)
|
|
110/0 |
Mathlib/RingTheory/Polynomial/Chebyshev.lean |
1 |
3 |
['github-actions', 'mathlib4-dependent-issues-bot', 'mathlib4-merge-conflict-bot'] |
nobody |
1-10058 1 day ago |
3-83525 3 days ago |
3-84999 3 days |
| 33493 |
michelsol author:michelsol |
feat(RingTheory/Polynomial): An explicit formula for the Chebyshev polynomials of the first kind |
Adds the following explicit formula on the Chebyshev polynomial of the first kind of order n.
${ T_{n}(x)\ =\ \sum \limits _{k=0}^{\lfloor {\frac {n}{2}}\rfloor } {\binom {n}{2k}} \left(\ X^{2}-1\ \right)^{k}\ X^{n-2k}}$
This explicit formula can be found [here](https://en.wikipedia.org/wiki/Chebyshev_polynomials#Explicit_expressions). There is a proof using complex numbers but it only works if the ring R = ℂ.
The proof here is by induction and works in a commutative ring R.
Mathlib seems to extend the definition of Chebyshev polynomials for $n \in \mathbb{Z}$ but this would make the formula more cumbersome with `n.natAbs` in place of `n`'s, so I expressed it on `n : ℕ` directly.
---
[](https://gitpod.io/from-referrer/)
|
new-contributor
t-ring-theory
|
51/1 |
Mathlib/RingTheory/Polynomial/Chebyshev.lean |
1 |
8 |
['YuvalFilmus', 'erdOne', 'github-actions', 'metakunt', 'michelsol'] |
erdOne assignee:erdOne |
1-9736 1 day ago |
6-81654 6 days ago |
7-74524 7 days |
| 33411 |
IlPreteRosso author:IlPreteRosso |
feat(Analysis/DiscreteConvolution): Discrete convolution API basics |
This is the first PR is a series of PRs towards the proposed API and ℓ1 Banach algebra.
Defines discrete convolution of functions `f : M → E` and `g : M → E'` over a monoid `M`
using a bilinear map `L : E →ₗ[S] E' →ₗ[S] F`:
`(f ⋆[L] g) x = ∑' (a, b) : mulFiber x, L (f a) (g b)`
where `abbrev mulFiber (x : M) : Set (M × M) := Set.mulAntidiagonal Set.univ Set.univ x`
|
t-analysis
new-contributor
|
486/0 |
Mathlib.lean,Mathlib/Analysis/DiscreteConvolution/Basic.lean |
2 |
11 |
['IlPreteRosso', 'github-actions', 'j-loreaux'] |
urkud assignee:urkud |
1-7199 1 day ago |
4-41923 4 days ago |
11-36297 11 days |
| 33818 |
JohnnyTeutonic author:JohnnyTeutonic |
feat(Algebra/Lie/Classical): finrank of sl(n) equals n² - 1 |
Proves `finrank R (sl n R) = Fintype.card n ^ 2 - 1` using rank-nullity and `Matrix.trace_surjective`.
---
[](https://gitpod.io/from-referrer/)
|
t-algebra label:t-algebra$ |
10/2 |
Mathlib/Algebra/Lie/Classical.lean |
1 |
8 |
['JohnnyTeutonic', 'github-actions', 'themathqueen'] |
nobody |
1-7029 1 day ago |
1-17580 1 day ago |
1-17622 1 day |
| 33782 |
tb65536 author:tb65536 |
refactor(RingTheory/Lasker): create structure for primary decomposition |
This PR extracts the conclusion of the Lasker-Noether theorem into a separate predicate, so that (in a follow-up PR), the various properties of the primary decomposition don't have to rewrite the entire three-line predicate each time.
---
[](https://gitpod.io/from-referrer/)
|
t-algebra
t-ring-theory
label:t-algebra$ |
19/6 |
Mathlib/RingTheory/Lasker.lean |
1 |
4 |
['erdOne', 'github-actions', 'tb65536'] |
nobody |
1-5779 1 day ago |
1-77167 1 day ago |
1-77145 1 day |
| 33798 |
Paul-Lez author:Paul-Lez |
feat(Combinatorics/SimpleGraph/Basic): decidability instance for `fromRel.Adj` |
This might be better as a definition - I'll let the reviewers weigh in on this.
---
[](https://gitpod.io/from-referrer/)
|
t-combinatorics
maintainer-merge
|
4/0 |
Mathlib/Combinatorics/SimpleGraph/Basic.lean |
1 |
3 |
['YaelDillies', 'github-actions'] |
nobody |
1-833 1 day ago |
1-833 1 day ago |
1-4420 1 day |
| 33612 |
xgenereux author:xgenereux |
feat(ValuationSubring): fieldTop |
Given a field `K`, the top element of `ValuationSubring K` is `K`, so top is also a field.
Note: I fear this would be a bad instance so I have marked this as an abbrev for now.
---
[](https://gitpod.io/from-referrer/)
|
t-ring-theory |
4/0 |
Mathlib/RingTheory/Valuation/ValuationSubring.lean |
1 |
8 |
['erdOne', 'github-actions', 'vihdzp', 'xgenereux'] |
mattrobball assignee:mattrobball |
0-85820 23 hours ago |
0-85839 23 hours ago |
5-79729 5 days |
| 33823 |
SnirBroshi author:SnirBroshi |
chore(GroupTheory/GroupAction/Defs): golf `orbitRel.iseqv` |
---
[](https://gitpod.io/from-referrer/)
|
t-group-theory |
1/3 |
Mathlib/GroupTheory/GroupAction/Defs.lean |
1 |
1 |
['github-actions'] |
nobody |
0-85215 23 hours ago |
0-85219 23 hours ago |
0-85258 23 hours |
| 32984 |
artie2000 author:artie2000 |
refactor: remove order instances from `SetLike` |
* Remove order instances from `SetLike`
* Add class `IsConcreteLE` for `SetLike` instances whose map is order-preserving
See discussion at https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/Abstracting.20the.20substructure.20lattice.20construction/with/563952738
---
- [ ] depends on #33801
[](https://gitpod.io/from-referrer/)
|
t-meta
t-data
|
375/146 |
Mathlib/Algebra/Algebra/NonUnitalSubalgebra.lean,Mathlib/Algebra/Algebra/Subalgebra/Basic.lean,Mathlib/Algebra/Field/Subfield/Defs.lean,Mathlib/Algebra/Group/Subgroup/Defs.lean,Mathlib/Algebra/Group/Submonoid/Defs.lean,Mathlib/Algebra/Group/Subsemigroup/Defs.lean,Mathlib/Algebra/Lie/Subalgebra.lean,Mathlib/Algebra/Lie/Submodule.lean,Mathlib/Algebra/Module/Submodule/Defs.lean,Mathlib/Algebra/Order/Group/Cone.lean,Mathlib/Algebra/Order/Group/Ideal.lean,Mathlib/Algebra/Order/Ring/Cone.lean,Mathlib/Algebra/Order/Ring/Ordering/Defs.lean,Mathlib/Algebra/Ring/Subring/Defs.lean,Mathlib/Algebra/Ring/Subsemiring/Defs.lean,Mathlib/Algebra/Star/NonUnitalSubalgebra.lean,Mathlib/Algebra/Star/Subalgebra.lean,Mathlib/Algebra/Star/Subsemiring.lean,Mathlib/AlgebraicGeometry/AffineScheme.lean,Mathlib/AlgebraicGeometry/Cover/Open.lean,Mathlib/AlgebraicGeometry/Limits.lean,Mathlib/AlgebraicGeometry/Morphisms/Basic.lean,Mathlib/AlgebraicGeometry/Morphisms/Separated.lean,Mathlib/AlgebraicGeometry/ProjectiveSpectrum/Basic.lean,Mathlib/AlgebraicGeometry/Scheme.lean,Mathlib/AlgebraicGeometry/StructureSheaf.lean,Mathlib/Analysis/Convex/Body.lean,Mathlib/Analysis/Convex/Cone/Basic.lean,Mathlib/Analysis/Convex/Cone/Dual.lean,Mathlib/Analysis/InnerProductSpace/Projection/FiniteDimensional.lean,Mathlib/Analysis/VonNeumannAlgebra/Basic.lean,Mathlib/CategoryTheory/Groupoid/Subgroupoid.lean,Mathlib/Combinatorics/SimpleGraph/Ends/Defs.lean,Mathlib/Combinatorics/Young/YoungDiagram.lean,Mathlib/Data/Finset/Defs.lean,Mathlib/Data/SetLike/Basic.lean,Mathlib/Data/Sym/Sym2.lean,Mathlib/FieldTheory/IntermediateField/Basic.lean,Mathlib/Geometry/Convex/Cone/Basic.lean,Mathlib/Geometry/Euclidean/Sphere/Power.lean,Mathlib/Geometry/Euclidean/Sphere/Tangent.lean,Mathlib/Geometry/Manifold/ChartedSpace.lean,Mathlib/Geometry/RingedSpace/Basic.lean,Mathlib/GroupTheory/GroupAction/SubMulAction.lean,Mathlib/GroupTheory/GroupAction/SubMulAction/Combination.lean,Mathlib/GroupTheory/Sylow.lean,Mathlib/LinearAlgebra/AffineSpace/AffineSubspace/Defs.lean,Mathlib/LinearAlgebra/Projectivization/Subspace.lean,Mathlib/ModelTheory/Definability.lean,Mathlib/ModelTheory/ElementarySubstructures.lean,Mathlib/ModelTheory/Substructures.lean,Mathlib/ModelTheory/Types.lean,Mathlib/NumberTheory/NumberField/FractionalIdeal.lean,Mathlib/Order/Atoms.lean,Mathlib/Order/BooleanSubalgebra.lean,Mathlib/Order/BourbakiWitt.lean,Mathlib/Order/Closure.lean,Mathlib/Order/CompleteSublattice.lean,Mathlib/Order/Ideal.lean,Mathlib/Order/PFilter.lean,Mathlib/Order/Partition/Basic.lean,Mathlib/Order/Preorder/Chain.lean,Mathlib/Order/Sublattice.lean,Mathlib/Order/Sublocale.lean,Mathlib/Order/UpperLower/CompleteLattice.lean,Mathlib/Order/UpperLower/Relative.lean,Mathlib/RepresentationTheory/Subrepresentation.lean,Mathlib/RingTheory/DedekindDomain/Different.lean,Mathlib/RingTheory/DedekindDomain/Factorization.lean,Mathlib/RingTheory/DedekindDomain/Ideal/Basic.lean,Mathlib/RingTheory/DividedPowers/SubDPIdeal.lean,Mathlib/RingTheory/FilteredAlgebra/Basic.lean,Mathlib/RingTheory/FractionalIdeal/Basic.lean,Mathlib/RingTheory/FractionalIdeal/Extended.lean,Mathlib/RingTheory/FractionalIdeal/Inverse.lean,Mathlib/RingTheory/FractionalIdeal/Operations.lean,Mathlib/RingTheory/GradedAlgebra/Homogeneous/Ideal.lean,Mathlib/RingTheory/GradedAlgebra/Homogeneous/Submodule.lean,Mathlib/RingTheory/GradedAlgebra/Homogeneous/Subsemiring.lean,Mathlib/RingTheory/NonUnitalSubring/Defs.lean,Mathlib/RingTheory/NonUnitalSubsemiring/Defs.lean,Mathlib/RingTheory/TwoSidedIdeal/Basic.lean,Mathlib/RingTheory/Valuation/ValuationSubring.lean,Mathlib/SetTheory/Descriptive/Tree.lean,Mathlib/SetTheory/ZFC/Basic.lean,Mathlib/Topology/Algebra/Group/ClosedSubgroup.lean,Mathlib/Topology/Algebra/Module/ClosedSubmodule.lean,Mathlib/Topology/Algebra/OpenSubgroup.lean,Mathlib/Topology/CWComplex/Classical/Basic.lean,Mathlib/Topology/Category/TopCat/OpenNhds.lean,Mathlib/Topology/Sets/Closeds.lean,Mathlib/Topology/Sets/Compacts.lean,Mathlib/Topology/Sets/Opens.lean,Mathlib/Topology/Sets/Order.lean,Mathlib/Topology/Sheaves/SheafCondition/Sites.lean,Mathlib/Topology/Sheaves/Stalks.lean,Mathlib/Topology/Spectral/Prespectral.lean,MathlibTest/FBinop.lean |
98 |
29 |
['Vierkantor', 'alreadydone', 'artie2000', 'github-actions'] |
nobody |
0-83524 23 hours ago |
0-83524 23 hours ago |
23-68682 23 days |
| 33360 |
joelriou author:joelriou |
feat(Algebra/Homology): functoriality of `extMk` with respect to the injective resolution |
The dual statement for projective resolutions is also obtained.
---
- [x] depends on: #33358
- [x] depends on: #32816
[](https://gitpod.io/from-referrer/)
|
t-category-theory |
206/7 |
Mathlib/Algebra/Homology/HomotopyCategory/HomComplexSingle.lean,Mathlib/CategoryTheory/Abelian/Injective/Ext.lean,Mathlib/CategoryTheory/Abelian/Injective/Extend.lean,Mathlib/CategoryTheory/Abelian/Projective/Ext.lean,Mathlib/CategoryTheory/Abelian/Projective/Extend.lean,Mathlib/CategoryTheory/Preadditive/Injective/Resolution.lean,Mathlib/CategoryTheory/Preadditive/Projective/Resolution.lean |
7 |
n/a |
['github-actions', 'mathlib4-dependent-issues-bot', 'mathlib4-merge-conflict-bot'] |
nobody |
0-79420 22 hours ago |
unknown |
unknown |
| 33825 |
euprunin author:euprunin |
chore: golf using `grind` |
---
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):
* `Finset.prod_insert_of_eq_one_if_notMem`: <10 ms before, 23 ms after
* `Finset.sym2_mono`: <10 ms before, 64 ms after
* `Finsupp.support_onFinset_subset`: <10 ms before, 14 ms after
* `Disjoint.ne_top_of_ne_bot`: <10 ms before, <10 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/)
|
|
4/10 |
Mathlib/Algebra/BigOperators/Group/Finset/Basic.lean,Mathlib/Data/Finset/Sym.lean,Mathlib/Data/Finsupp/Defs.lean,Mathlib/Order/Disjoint.lean |
4 |
1 |
['github-actions'] |
nobody |
0-75872 21 hours ago |
0-75940 21 hours ago |
0-75917 21 hours |
| 33826 |
euprunin author:euprunin |
chore: golf using `grind` |
---
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):
* `List.IsChain.tail`: <10 ms before, 12 ms after
* `List.IsChain.cons_of_ne_nil`: 12 ms before, 21 ms after
* `List.isChain_attachWith`: 148 ms before, 186 ms after
* `List.orderedInsert_erase`: 35 ms before, 73 ms after
* `PFunctor.Approx.head_succ'`: 24 ms before, 57 ms after
* `not_monotone_not_antitone_iff_exists_le_le`: 40 ms before, 119 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/)
|
|
7/76 |
Mathlib/Data/List/Chain.lean,Mathlib/Data/List/Sort.lean,Mathlib/Data/PFunctor/Univariate/M.lean,Mathlib/Order/Monotone/Basic.lean |
4 |
1 |
['github-actions'] |
nobody |
0-73374 20 hours ago |
0-73447 20 hours ago |
0-73424 20 hours |
| 33804 |
tb65536 author:tb65536 |
feat(RingTheory/Localization/Ideal): `map` distributes over `inf` |
This PR proves that mapping ideals to the localization distributes over finite intersections, following the design of the analogous statements for `Ideal.radical`.
---
[](https://gitpod.io/from-referrer/)
|
t-algebra
t-ring-theory
label:t-algebra$ |
24/0 |
Mathlib/RingTheory/Localization/Ideal.lean |
1 |
6 |
['erdOne', 'github-actions', 'plp127', 'tb65536'] |
nobody |
0-70671 19 hours ago |
0-70671 19 hours ago |
1-65587 1 day |
| 25889 |
plp127 author:plp127 |
fix(Tactic/Widget/Conv): fix various issues |
Fixes various issues with the `conv?` widget. Closes #25162.
([Zulip thread](https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/bug.20in.20.60conv.3F.60))
Specifically, fixes issues with `conv?` where
- when converting a `SubExpr.Pos` to conv directions, it always uses the goal expression as reference, even when working on a hypothesis, this often leads to bad results and makes it unusable on hypotheses
- it refuses to go all the way in to a function (for example in `Nat.succ 0`, you can't access `Nat.succ`)
- it refuses to enter binders where the name of the bound variable contains the character `0` (try it on `∀ (x0 : Nat), x0 = x0`)
- it panics if it can't find a binder name instead of just coming up with one itself, this also means usually you can't enter either side of a non-dependent arrow since those usually don't have binder names (try it on `False → False`)
- you can't enter the type of a binder, you end up going into the body instead (try it on `fun (x : False) => (x.elim : False → Nat) x.elim`)
- you can't partially enter a function, you end up going to the top argument after instead (for example, in the expression `id (id id) 0`, when you click on `id (id id)`, you end up going to `id id`)
---
[](https://gitpod.io/from-referrer/)
|
t-meta |
795/104 |
Mathlib/Lean/Name.lean,Mathlib/Tactic/Widget/Conv.lean,MathlibTest/conv_widget.lean,MathlibTest/willRoundTrip.lean |
4 |
42 |
['Vierkantor', 'bryangingechen', 'github-actions', 'mathlib4-merge-conflict-bot', 'plp127', 'thorimur'] |
bryangingechen, kmill, thorimur assignee:kmill assignee:bryangingechen assignee:thorimur |
0-68661 19 hours ago |
0-68671 19 hours ago |
80-78194 80 days |
| 33236 |
JovanGerb author:JovanGerb |
refactor(translate): merge `expand` into `applyReplacementFun` |
This PR refactors the main translation loop (`applyReplacementFun`) of `to_additive `/`to_dual` so that it operates on free variables instead of loose bound variables. This will make it much easier to implement the reordering of arguments of arguments, which is something we need for `to_dual`. The other loop that was run beforehand, `expand`, was separate because it required free variables instead of loose bound variables, but now it won't make sense anymore to have it be a separate loop, so I've merged it into the `applyReplacementFun` implementation.
Ideally, we would want to use `Meta.transform` for this, but unfortunately this isn't good enough, because we need more control over when to do recursive calls. So, we copy/inline the implementation of `Meta.transform`.
---
[](https://gitpod.io/from-referrer/)
|
t-meta |
95/78 |
Mathlib/Tactic/Translate/Core.lean,MathlibTest/toAdditive.lean |
2 |
4 |
['JovanGerb', 'github-actions', 'leanprover-radar'] |
joneugster assignee:joneugster |
0-67535 18 hours ago |
19-2954 19 days ago |
19-2997 19 days |
| 33658 |
vihdzp author:vihdzp |
refactor(RingTheory/Valuation/ValuativeRel/Basic): fix theorem names for multiplication |
We rename `vle_mul_right` to `mul_vle_mul_left` and reorder its arguments to match `mul_le_mul_left`, and other analogous changes.
---
[](https://gitpod.io/from-referrer/)
|
t-ring-theory |
63/64 |
Mathlib/RingTheory/Valuation/ValuativeRel/Basic.lean,Mathlib/RingTheory/Valuation/ValuativeRel/Trivial.lean |
2 |
7 |
['JovanGerb', 'erdOne', 'github-actions'] |
erdOne assignee:erdOne |
0-66955 18 hours ago |
0-66957 18 hours ago |
5-19449 5 days |
| 33819 |
bjornsolheim author:bjornsolheim |
feat(Analysis/Convex): diameter of a standard simplex |
diameter of a standard simplex
---
[](https://gitpod.io/from-referrer/)
|
t-analysis |
41/0 |
Mathlib/Analysis/Convex/StdSimplex.lean |
1 |
5 |
['bjornsolheim', 'github-actions', 'themathqueen'] |
nobody |
0-66771 18 hours ago |
1-16973 1 day ago |
1-17014 1 day |
| 33830 |
seewoo5 author:seewoo5 |
feat(Manifold/MFDeriv): `MDifferentiable.pow` and variants |
---
Add `MDifferentiableWithinAt.pow` and similar theorems for `MDifferentiableAt`, `MDifferentiableOn`, `MDifferentiable`.
[](https://gitpod.io/from-referrer/)
|
t-differential-geometry |
16/0 |
Mathlib/Geometry/Manifold/MFDeriv/SpecificFunctions.lean |
1 |
1 |
['github-actions'] |
nobody |
0-61947 17 hours ago |
0-61947 17 hours ago |
0-61988 17 hours |
| 30378 |
mans0954 author:mans0954 |
refactor(Order/Hom/Lattice): Use default `initialize_simps_projections` configuration for `LatticeHom`. |
Use default `initialize_simps_projections` configuration for `LatticeHom`.
I'm not sure what was originally intended by the TODO, but this appears to work.
---
[](https://gitpod.io/from-referrer/)
|
t-order |
4/7 |
Mathlib/Order/Hom/Lattice.lean,Mathlib/Order/Hom/WithTopBot.lean |
2 |
4 |
['bryangingechen', 'fpvandoorn', 'github-actions', 'vihdzp'] |
bryangingechen assignee:bryangingechen |
0-60862 16 hours ago |
0-60922 16 hours ago |
18-72499 18 days |
| 26614 |
Rida-Hamadani author:Rida-Hamadani |
feat(SimpleGraph): add more API for `take`/`drop` |
The main lemma proves that taking `n` vertices of a walk results in a sub-walk of taking `k` vertices when `n` is less than or equal to `k`, alongside a similar lemma for dropping vertices.
---
- [x] depends on: #26655
[](https://gitpod.io/from-referrer/)
|
t-combinatorics |
58/0 |
Mathlib/Combinatorics/SimpleGraph/Walks/Operations.lean,Mathlib/Combinatorics/SimpleGraph/Walks/Subwalks.lean |
2 |
20 |
['Rida-Hamadani', 'b-mehta', 'github-actions', 'leanprover-community-bot-assistant', 'mathlib4-dependent-issues-bot', 'mathlib4-merge-conflict-bot'] |
kmill assignee:kmill |
0-59687 16 hours ago |
19-55707 19 days ago |
24-52828 24 days |
| 32734 |
Vierkantor author:Vierkantor |
chore(Tactic): document remaining undocumented tactics |
Write documentation for the few tactics in Mathlib that have no documentation at all. After this PR and a few related ones are merged, every tactic defined in Mathlib should now have a docstring or a `@[tactic_alt]` attribute.
~~The documentation for `mem_tac` is pending a Zulip discussion: https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/Proj.20as.20a.20scheme.3A.20.60mem_tac.60.20works.20accidentally.3F/with/563193768~~ Zulip discussion now applies to the independent PR #33711. This PR can be merged before or after #33711 (or #33711 can be closed).
---
[](https://gitpod.io/from-referrer/)
|
documentation
t-meta
|
28/0 |
Mathlib/Tactic/Conv.lean,Mathlib/Tactic/GCongr/Core.lean |
2 |
3 |
['Vierkantor', 'github-actions', 'mathlib4-merge-conflict-bot'] |
dwrensha assignee:dwrensha |
0-59686 16 hours ago |
3-79796 3 days ago |
15-40334 15 days |
| 32735 |
Jlh18 author:Jlh18 |
refactor: move `CategoryTheory.Category.Grpd` to `CategoryTheory.Groupoid.Grpd.Basic` |
Step one of several PRs, stemming from #29283
---
[](https://gitpod.io/from-referrer/)
|
file-removed |
3/4 |
Mathlib.lean,Mathlib/AlgebraicTopology/FundamentalGroupoid/Basic.lean,Mathlib/CategoryTheory/Groupoid/FreeGroupoidOfCategory.lean,Mathlib/CategoryTheory/Groupoid/Grpd/Basic.lean |
4 |
3 |
['Jlh18', 'github-actions', 'mathlib4-merge-conflict-bot'] |
alexjbest assignee:alexjbest |
0-59686 16 hours ago |
4-79897 4 days ago |
11-16864 11 days |
| 33185 |
alreadydone author:alreadydone |
feat(Algebra): MulAction/SMulWithZero by Nat/Int |
---
[](https://gitpod.io/from-referrer/)
|
t-algebra label:t-algebra$ |
22/2 |
Mathlib/Algebra/Group/Basic.lean,Mathlib/Algebra/Group/Defs.lean,Mathlib/Algebra/Module/NatInt.lean |
3 |
3 |
['alreadydone', 'github-actions', 'leanprover-radar'] |
ocfnash assignee:ocfnash |
0-59684 16 hours ago |
3-66521 3 days ago |
3-72292 3 days |
| 33504 |
ldct author:ldct |
feat: Add lemmas for DihedralGroup.fintypeHelper |
Using `fin_cases` to reason about `DihedralGroup` elements exposes the internal `fintypeHelper` instances, which has no exported API
```
example (g : DihedralGroup 3) : (g^6 = 1) := by
fin_cases g
<;> dsimp
--
6 goals
case «0»
⊢ DihedralGroup.fintypeHelper✝ (Sum.inl 0) ^ 6 = 1
...
```
this PR adds simp lemma that convert them to constructors, which do have API
```
6 goals
case «0»
⊢ 1 ^ 6 = 1
case «1»
⊢ DihedralGroup.r 1 ^ 6 = 1
case «2»
⊢ DihedralGroup.r 2 ^ 6 = 1
```
---
[](https://gitpod.io/from-referrer/)
|
t-group-theory |
8/0 |
Mathlib/GroupTheory/SpecificGroups/Dihedral.lean |
1 |
1 |
['github-actions', 'tb65536'] |
tb65536 assignee:tb65536 |
0-59683 16 hours ago |
8-45483 8 days ago |
8-45525 8 days |
| 33611 |
urkud author:urkud |
feat(ImplicitFunction): add a parametric version |
---
I'm not sure if the supporting linear algebra lemmas are in the form we want to see them in Mathlib.
- [x] depends on: #33585
[](https://gitpod.io/from-referrer/)
|
t-analysis |
191/0 |
Mathlib.lean,Mathlib/Analysis/Calculus/FDeriv/Prod.lean,Mathlib/Analysis/Calculus/ImplicitFunction/Parametric.lean,Mathlib/LinearAlgebra/Prod.lean |
4 |
3 |
['github-actions', 'mathlib4-dependent-issues-bot', 'mathlib4-merge-conflict-bot'] |
ADedecker assignee:ADedecker |
0-59682 16 hours ago |
4-41511 4 days ago |
5-84832 5 days |
| 33642 |
themathqueen author:themathqueen |
feat(Analysis/Matrix/Order): polar decomposition for {invertible, Hermitian} matrices |
For an invertible (resp., Hermitian) matrix `A`, there exists unitary `U` and a positive definite (resp., semidefinite) matrix `P` such that `A = U * P`.
---
[](https://gitpod.io/from-referrer/)
|
t-analysis |
41/4 |
Mathlib/Analysis/Matrix/Order.lean |
1 |
3 |
['github-actions', 'mathlib4-merge-conflict-bot', 'themathqueen'] |
j-loreaux assignee:j-loreaux |
0-59681 16 hours ago |
4-906 4 days ago |
5-57532 5 days |
| 33649 |
vihdzp author:vihdzp |
feat(Analysis/Real/Hyperreal): more lemmas on `ω` and `ε` |
I've moved these around a bit, so as to ensure the lemmas about each constant are next to each other.
---
[](https://gitpod.io/from-referrer/)
|
t-algebra
large-import
label:t-algebra$ |
116/30 |
Mathlib/Algebra/Order/AddGroupWithTop.lean,Mathlib/Algebra/Order/Ring/Archimedean.lean,Mathlib/Algebra/Order/Ring/StandardPart.lean,Mathlib/Analysis/Real/Hyperreal.lean |
4 |
6 |
['github-actions', 'vihdzp', 'wwylele'] |
kim-em assignee:kim-em |
0-59680 16 hours ago |
5-49815 5 days ago |
5-51297 5 days |
| 33693 |
yoh-tanimoto author:yoh-tanimoto |
feat(Mathlib/Analysis/Normed/Module): add instances of `CompleteSpace` for `Submodules` and `ClosedSubmodule` |
add an instance of `CompleteSpace` for a `Submodule` of a Banach space `[NormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [CompleteSpace E]` which `IsClosed`.
In this relation, convert a lemma showing `IsClosed` to an instance for `ClosedSubmodule`.
motivation: Together with #28709, this makes it automatic that a `ClosedSubmodule` in a Hilbert space `HasOrthogonalProjection`.
discussion: https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/.60CompleteSpace.60.20for.20closed.20subtypes.20in.20a.20.60CompleteSpace.60 |
|
10/9 |
Mathlib/Analysis/InnerProductSpace/Orthogonal.lean,Mathlib/Analysis/InnerProductSpace/l2Space.lean,Mathlib/Analysis/Normed/Module/Basic.lean,Mathlib/Topology/Algebra/Module/ClosedSubmodule.lean |
4 |
2 |
['github-actions'] |
jcommelin assignee:jcommelin |
0-59678 16 hours ago |
4-60157 4 days ago |
4-60134 4 days |
| 33698 |
artie2000 author:artie2000 |
feat(Algebra/Ring): characteristic of semireal ring |
* Prove that a semireal ring has characteristic zero
* Prove that natural numbers are sums of squares
---
[](https://gitpod.io/from-referrer/)
|
t-algebra label:t-algebra$ |
16/0 |
Mathlib/Algebra/Ring/Semireal/Defs.lean,Mathlib/Algebra/Ring/SumsOfSquares.lean |
2 |
3 |
['github-actions', 'vihdzp'] |
riccardobrasca assignee:riccardobrasca |
0-59676 16 hours ago |
3-85232 3 days ago |
4-55190 4 days |
| 33699 |
artie2000 author:artie2000 |
chore(Algebra/Ring): semireal definition lemmas |
* Add converse to `IsSemireal.not_isSumSq_neg_one `
---
[](https://gitpod.io/from-referrer/)
|
t-algebra label:t-algebra$ |
9/2 |
Mathlib/Algebra/Ring/Semireal/Defs.lean |
1 |
4 |
['artie2000', 'github-actions', 'vihdzp'] |
riccardobrasca assignee:riccardobrasca |
0-59676 16 hours ago |
4-55893 4 days ago |
4-55931 4 days |
| 33700 |
vihdzp author:vihdzp |
feat: dense orders have elements lying between two finite sets |
Used in the CGT repo, and will be used not too long in the future to show dense orders are η₀-sets.
Co-authored-by: Kenny Lau
---
See [Zulip](https://leanprover.zulipchat.com/#narrow/channel/217875-Is-there-code-for-X.3F/topic/.60exists_between.60.20for.20finite.20sets/near/526965677).
Is the import increase a problem? If so, would a new file for these theorems be desirable? Or where else should they go?
[](https://gitpod.io/from-referrer/)
|
t-order
large-import
|
30/0 |
Mathlib/Data/Finset/Max.lean |
1 |
1 |
['github-actions'] |
Vierkantor assignee:Vierkantor |
0-59675 16 hours ago |
4-48607 4 days ago |
4-48644 4 days |
| 33709 |
wangying11123 author:wangying11123 |
feat（Analysis/Convex/Between）:Add wbtw_of_sameRay_vsub_left |
add wbtw_of_sameRay_vsub_left
Main additions
`wbtw_of_sameRay_vsub_left` if the vectors from a point x to points y and z lie on the same ray, then y is weakly between x and z, or z is weakly between x and y. |
new-contributor |
24/0 |
Mathlib/Analysis/Convex/Between.lean |
1 |
2 |
['github-actions'] |
MichaelStollBayreuth assignee:MichaelStollBayreuth |
0-59674 16 hours ago |
4-24017 4 days ago |
4-24004 4 days |
| 33722 |
erdOne author:erdOne |
feat(RingTheory): Add `RingHom.QuasiFinite` |
---
[](https://gitpod.io/from-referrer/)
|
t-ring-theory |
128/0 |
Mathlib.lean,Mathlib/RingTheory/RingHom/QuasiFinite.lean |
2 |
1 |
['github-actions'] |
chrisflav assignee:chrisflav |
0-59673 16 hours ago |
4-5708 4 days ago |
4-5752 4 days |
| 33724 |
alreadydone author:alreadydone |
chore(Algebra): deprecate `DistribMulAction.toAddMonoidHom` |
which is simply a specialized version of `DistribSMul.toAddMonoidHom`.
`MulDistribMulAction.toMonoidHom` has to be kept, since there is no `MulDistribSMul` yet.
also deprecate `AddMonoidHom.smulLeft` (same situation) and generalize `DistribMulAction.toLinearMap`
---
- [x] depends on: #33721
[](https://gitpod.io/from-referrer/)
|
t-algebra label:t-algebra$ |
111/99 |
Mathlib/Algebra/Algebra/Hom.lean,Mathlib/Algebra/Algebra/Tower.lean,Mathlib/Algebra/BigOperators/Finprod.lean,Mathlib/Algebra/Category/ModuleCat/Tannaka.lean,Mathlib/Algebra/DirectSum/Algebra.lean,Mathlib/Algebra/GroupWithZero/Action/Basic.lean,Mathlib/Algebra/GroupWithZero/Action/Defs.lean,Mathlib/Algebra/GroupWithZero/Action/End.lean,Mathlib/Algebra/Module/Basic.lean,Mathlib/Algebra/Module/Equiv/Basic.lean,Mathlib/Algebra/Module/Hom.lean,Mathlib/Algebra/Module/LinearMap/Defs.lean,Mathlib/Algebra/Module/LinearMap/End.lean,Mathlib/Algebra/Module/Rat.lean,Mathlib/Algebra/Module/Submodule/Invariant.lean,Mathlib/Algebra/Module/Submodule/Pointwise.lean,Mathlib/Algebra/Module/Torsion/Basic.lean,Mathlib/Algebra/Polynomial/HasseDeriv.lean,Mathlib/Algebra/QuadraticAlgebra/NormDeterminant.lean,Mathlib/Algebra/Ring/Action/Basic.lean,Mathlib/Analysis/SpecialFunctions/Gamma/BohrMollerup.lean,Mathlib/LinearAlgebra/AffineSpace/Pointwise.lean,Mathlib/LinearAlgebra/BilinearMap.lean,Mathlib/LinearAlgebra/Matrix/ToLin.lean,Mathlib/LinearAlgebra/TensorProduct/Basic.lean,Mathlib/LinearAlgebra/TensorProduct/Graded/External.lean,Mathlib/RingTheory/DiscreteValuationRing/TFAE.lean,Mathlib/RingTheory/FractionalIdeal/Basic.lean,Mathlib/RingTheory/IntegralClosure/Algebra/Basic.lean,Mathlib/RingTheory/Jacobson/Ideal.lean,Mathlib/RingTheory/Morita/Matrix.lean,Mathlib/RingTheory/Regular/IsSMulRegular.lean,Mathlib/Topology/Algebra/InfiniteSum/Module.lean,Mathlib/Topology/Algebra/Ring/Real.lean,Mathlib/Topology/Algebra/UniformMulAction.lean |
35 |
2 |
['github-actions', 'mathlib4-dependent-issues-bot'] |
jcommelin assignee:jcommelin |
0-59673 16 hours ago |
3-68031 3 days ago |
3-68009 3 days |
| 33501 |
SnirBroshi author:SnirBroshi |
feat(Combinatorics/SimpleGraph/Finite): degrees for infinite graphs |
- Redefine degrees using `Set.ncard` to avoid `Fintype` and enable talking about degrees in infinite graphs.
- Define `ENat` versions of `degree`/`minDegree`/`maxDegree` called `edegree`/`eminDegree`/`emaxDegree` respectively.
- Remove `LocallyFinite` assumption from `IsRegularOfDegree`, and change it to use `edegree = k` instead of `degree = k` to retain the meaning of the case `k = 0`.
---
The `e` prefix matches the existing `edist` and `ediam`.
To make reviewing easier, this PR intentionally does not:
- Add theorems about the new definitions
- Reorder theorems to avoid `omit`s
- Move theorems to a new `Degree.lean` file
This is so that the diff shows the old/new versions side-by-side, and to avoid a bigger PR.
Consequently a few proofs are a bit longer, but that'll be fixed after this PR by adding API lemmas for the new definitions (e.g. `edegree ≠ ⊤ → edegree = degree`).
Regarding computability: If computability of degrees is useful, we can introduce a separate `findegree` in the future (similar to `neighborSet` vs `neighborFinset`), but I think degrees are a basic graph definition that should be defined for any `SimpleGraph`. As for theorems, such a `findegree` can use a lemma `findegree = degree` to access all the degree theorems, instead of duplicating everything to both versions.
This PR was motivated by wanting to talk about infinite graphs with a finite max-degree.
[](https://gitpod.io/from-referrer/)
|
t-combinatorics
large-import
|
302/243 |
Archive/Wiedijk100Theorems/FriendshipGraphs.lean,Archive/Wiedijk100Theorems/Konigsberg.lean,Counterexamples/HeawoodUnitDistance.lean,Mathlib/Combinatorics/SimpleGraph/Acyclic.lean,Mathlib/Combinatorics/SimpleGraph/AdjMatrix.lean,Mathlib/Combinatorics/SimpleGraph/Bipartite.lean,Mathlib/Combinatorics/SimpleGraph/Circulant.lean,Mathlib/Combinatorics/SimpleGraph/Connectivity/Connected.lean,Mathlib/Combinatorics/SimpleGraph/DegreeSum.lean,Mathlib/Combinatorics/SimpleGraph/Extremal/Turan.lean,Mathlib/Combinatorics/SimpleGraph/Finite.lean,Mathlib/Combinatorics/SimpleGraph/FiveWheelLike.lean,Mathlib/Combinatorics/SimpleGraph/LapMatrix.lean,Mathlib/Combinatorics/SimpleGraph/Maps.lean,Mathlib/Combinatorics/SimpleGraph/Prod.lean,Mathlib/Combinatorics/SimpleGraph/StronglyRegular.lean,Mathlib/Combinatorics/SimpleGraph/Subgraph.lean,Mathlib/Combinatorics/SimpleGraph/Trails.lean,Mathlib/Data/Set/Card.lean,Mathlib/Data/Set/Insert.lean,Mathlib/Order/ConditionallyCompleteLattice/Finset.lean |
21 |
1 |
['github-actions'] |
nobody |
0-59597 16 hours ago |
4-57057 4 days ago |
8-53415 8 days |
| 33828 |
themathqueen author:themathqueen |
chore(Algebra/Group/Center): golf some stuff |
---
just experimenting with `grind` and `aesop`
[](https://gitpod.io/from-referrer/)
|
t-algebra label:t-algebra$ |
16/61 |
Mathlib/Algebra/Group/Center.lean |
1 |
8 |
['github-actions', 'themathqueen', 'vihdzp'] |
nobody |
0-59418 16 hours ago |
0-68563 19 hours ago |
0-68604 19 hours |
| 33665 |
JovanGerb author:JovanGerb |
fix(addRelatedDecl): support imported theorems in module |
This PR lets `elementwise`, `to_fun`, etc. work on theorems that are imported (and the body of the theorem is not available). These kinds of declarations have the axiom constant info, which was not supported before. As a bonus, I've also made it support unsafe theorems.
I've removed the support for the auxiliary declaration being a `def`, because this is never used, and it wasn't clear to me what the expected behaviour there is exactly (e.g. should it be `reducible`?).
---
[](https://gitpod.io/from-referrer/)
|
t-meta |
3/18 |
Mathlib/CategoryTheory/ConcreteCategory/Elementwise.lean,Mathlib/CategoryTheory/Elementwise.lean,Mathlib/Util/AddRelatedDecl.lean |
3 |
2 |
['adamtopaz', 'github-actions'] |
adamtopaz assignee:adamtopaz |
0-59136 16 hours ago |
4-33152 4 days ago |
5-18622 5 days |
| 33797 |
SnirBroshi author:SnirBroshi |
chore(Order/Defs/Unbundled): deprecate `IsTotal` in favor of core's `Std.Total` |
---
[Mathlib's `IsTotal`](https://leanprover-community.github.io/mathlib4_docs/Mathlib/Order/Defs/Unbundled.html#IsTotal)
[Core's `Std.Total`](https://leanprover-community.github.io/mathlib4_docs/Init/Core.html#Std.Total)
[Zulip](https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/Relation.20properties.20duplication/near/544638270)
[](https://gitpod.io/from-referrer/)
|
|
121/110 |
Mathlib/Algebra/Group/Basic.lean,Mathlib/Algebra/Order/Archimedean/Class.lean,Mathlib/Algebra/Order/GroupWithZero/Canonical.lean,Mathlib/Algebra/Order/Ring/Canonical.lean,Mathlib/Data/DFinsupp/Lex.lean,Mathlib/Data/Finset/Sort.lean,Mathlib/Data/List/Sort.lean,Mathlib/Data/Multiset/Sort.lean,Mathlib/Data/Nat/PartENat.lean,Mathlib/Data/Ordmap/Invariants.lean,Mathlib/Data/Ordmap/Ordset.lean,Mathlib/Data/Prod/Basic.lean,Mathlib/Data/Real/Basic.lean,Mathlib/Data/Sigma/Lex.lean,Mathlib/Data/Sum/Order.lean,Mathlib/Logic/Encodable/Basic.lean,Mathlib/Order/Antisymmetrization.lean,Mathlib/Order/Basic.lean,Mathlib/Order/Comparable.lean,Mathlib/Order/Compare.lean,Mathlib/Order/Defs/Unbundled.lean,Mathlib/Order/Directed.lean,Mathlib/Order/Filter/FilterProduct.lean,Mathlib/Order/Lattice.lean,Mathlib/Order/PropInstances.lean,Mathlib/Order/Quotient.lean,Mathlib/Order/RelClasses.lean,Mathlib/Order/RelIso/Basic.lean,Mathlib/Order/UpperLower/CompleteLattice.lean,Mathlib/Order/WithBot.lean,Mathlib/RingTheory/Valuation/ValuationRing.lean,Mathlib/RingTheory/Valuation/ValuationSubring.lean,Mathlib/Topology/EMetricSpace/BoundedVariation.lean,Mathlib/Topology/Semicontinuity/Basic.lean |
34 |
6 |
['github-actions', 'vihdzp'] |
nobody |
0-58438 16 hours ago |
2-3903 2 days ago |
2-3880 2 days |
| 33239 |
JovanGerb author:JovanGerb |
feat(to_dual): linter for redundant uses of `to_dual`/`to_additive` |
This PR adds a linter that helps avoid unneccessary uses of `to_dual`/`to_additive`. With `to_dual self` it can sometimes be hard to tell if it's actually doing anything or not, so this will help with that.
---
[](https://gitpod.io/from-referrer/)
|
|
70/29 |
Mathlib/Algebra/BigOperators/Finsupp/Basic.lean,Mathlib/Algebra/Group/WithOne/Defs.lean,Mathlib/Analysis/Normed/Group/Continuity.lean,Mathlib/CategoryTheory/Types/Basic.lean,Mathlib/Order/Basic.lean,Mathlib/Order/Defs/PartialOrder.lean,Mathlib/Tactic/Translate/Core.lean,Mathlib/Tactic/Translate/ToAdditive.lean,Mathlib/Topology/Category/Profinite/Basic.lean,MathlibTest/DeprecateTo.lean,MathlibTest/Lint.lean,MathlibTest/ToDual.lean,MathlibTest/toAdditive.lean |
13 |
6 |
['github-actions', 'mathlib4-merge-conflict-bot', 'vihdzp'] |
bryangingechen assignee:bryangingechen |
0-56629 15 hours ago |
0-56647 15 hours ago |
15-82455 15 days |
| 33478 |
anishrajeev author:anishrajeev |
feat(ModelTheory): define a subset of the topology over complete types |
Define a subset of the Stone Space over a language expanded with countably many constants. Define the proposition to indicate if a language is countable. The subset's density and openness is a future goal to prove (have a branch where it is almost finished), in pursuit of formalizing the proof of the Omitting Types Theorem via properties of Baire spaces.
[ ] depends on: #32215
[ ] depends on: #32546 |
new-contributor |
160/1 |
Mathlib.lean,Mathlib/ModelTheory/Topology/Types.lean,Mathlib/ModelTheory/Types.lean,Mathlib/Tactic/Linter/DirectoryDependency.lean |
4 |
5 |
['NoneMore', 'anishrajeev', 'github-actions'] |
nobody |
0-55762 15 hours ago |
9-54505 9 days ago |
9-54489 9 days |
| 33833 |
JovanGerb author:JovanGerb |
feat(reassoc): tag the generated declaration with `to_dual none` |
This PR adds the feature to `@[reassoc]` that it tags the generated declaration with `to_dual none` whenever the original declaration has been tagged with `to_dual`.
In practice, this means that when mixing uses of `to_dual` and `reassoc`, the `to_dual` should come before the `reassoc`, or as `to_dual (attr := reassoc)`.
In the rare case that the original expression is not tagged with `to_dual` because it is entirely self dual, we will need to manually tag the generated lemma with `to_dual none`.
This requires #33773, because otherwise the existing attribute linter will not be happy with this.
---
[](https://gitpod.io/from-referrer/)
|
t-meta |
20/13 |
Mathlib/Tactic/CategoryTheory/Elementwise.lean,Mathlib/Tactic/CategoryTheory/Reassoc.lean,Mathlib/Tactic/CategoryTheory/ToApp.lean,Mathlib/Tactic/ToFun.lean,Mathlib/Tactic/Translate/ToDual.lean,Mathlib/Util/AddRelatedDecl.lean |
6 |
1 |
['github-actions'] |
nobody |
0-53185 14 hours ago |
0-54902 15 hours ago |
0-54959 15 hours |
| 33025 |
JovanGerb author:JovanGerb |
feat(gcongr): beef up `@[gcongr]` tag to accept `↔` & any argument order |
This PR modifies the `@[gcongr]` tag to accept lemmas in more forms.
- Iff lemmas are now accepted, and are turned into an auxiliary lemmas that is simply one of the two implications.
- Implicational gcongr lemmas now don't need to have their arguments given in the "correct" order. An auxiliary lemma is generated if necessary.
The auxiliary lemma generation is done analogously to `simp` which creates little lemmas `Foo._simp_1`.,
I also went throught all lemmas that have `GCongr.` in the name, and removed all but one of them (the remaining one is `GCongr.mem_of_le_of_mem`)
A future PR may introduce the `gcongr at` tactic, which does `gcongr` but at hypotheses. This would be using the reverse direction of the iff lemmas tagged with `gcongr`. For this reason it is preferred to tag the iff lemma if possible.
---
[](https://gitpod.io/from-referrer/)
|
t-meta |
208/278 |
Mathlib/Algebra/Module/Submodule/Basic.lean,Mathlib/Algebra/Order/BigOperators/Expect.lean,Mathlib/Algebra/Order/Pi.lean,Mathlib/Algebra/Order/Ring/Cast.lean,Mathlib/Algebra/Order/Ring/Ordering/Basic.lean,Mathlib/Analysis/SpecialFunctions/Arsinh.lean,Mathlib/Data/Finset/Defs.lean,Mathlib/Data/Finset/Image.lean,Mathlib/Data/Finset/Range.lean,Mathlib/Data/Finsupp/Order.lean,Mathlib/Data/Int/Basic.lean,Mathlib/Data/NNReal/Defs.lean,Mathlib/Data/Set/Insert.lean,Mathlib/Data/SetLike/Basic.lean,Mathlib/MeasureTheory/Function/SimpleFunc.lean,Mathlib/NumberTheory/LucasLehmer.lean,Mathlib/Order/Basic.lean,Mathlib/Order/Filter/Basic.lean,Mathlib/Order/Fin/Basic.lean,Mathlib/Order/Hom/Basic.lean,Mathlib/Order/Hom/Lattice.lean,Mathlib/Order/Interval/Finset/Basic.lean,Mathlib/Order/Interval/Set/Basic.lean,Mathlib/Order/Nucleus.lean,Mathlib/Order/Sublocale.lean,Mathlib/RingTheory/FractionalIdeal/Basic.lean,Mathlib/SetTheory/ZFC/VonNeumann.lean,Mathlib/Tactic/GCongr/Core.lean,Mathlib/Tactic/Translate/Core.lean,MathlibTest/GCongr/GCongr.lean |
30 |
3 |
['github-actions', 'mathlib4-merge-conflict-bot'] |
dwrensha assignee:dwrensha |
0-50638 14 hours ago |
22-55295 22 days ago |
24-12310 24 days |
| 33831 |
vihdzp author:vihdzp |
refactor(RingTheory/Polynomial/SmallDegreeVieta): convert to {p : R[X]} (hp : p.natDegree = 2) |
Co-authored-by: Christopher Hoskin
---
Adopted from #29921. I've applied all pending suggestions.
[](https://gitpod.io/from-referrer/)
|
t-ring-theory |
112/48 |
Mathlib/Algebra/Polynomial/Basic.lean,Mathlib/Algebra/Polynomial/Roots.lean,Mathlib/RingTheory/Polynomial/SmallDegreeVieta.lean |
3 |
1 |
['github-actions'] |
nobody |
0-48329 13 hours ago |
0-61210 16 hours ago |
0-61203 17 hours |
| 33824 |
Komyyy author:Komyyy |
doc: update the doc of Bolzano-Weierstrass |
In #30233, I generalized Bolzano-Weierstrass, but I forgot updating the doc.
---
[](https://gitpod.io/from-referrer/)
|
documentation
t-topology
|
3/3 |
Mathlib/Topology/Sequences.lean |
1 |
2 |
['github-actions', 'vihdzp'] |
nobody |
0-45993 12 hours ago |
0-80275 22 hours ago |
0-80254 22 hours |
| 33835 |
BoltonBailey author:BoltonBailey |
chore(Computability/Primrec): split file |
This PR addresses an instance of the tech debt linter by splitting the file Computability/Primrec, currently the longest file in mathlib. It seems that most of the content after line 750 involves operations over `List`s or `List.Vector`s (or that depend on operations over lists or vectors) and the earlier content does not, so this seems to be the place most natural to split.
---
[](https://gitpod.io/from-referrer/)
|
t-computability
tech debt
|
1592/1556 |
Mathlib.lean,Mathlib/Computability/Partrec.lean,Mathlib/Computability/Primrec.lean,Mathlib/Computability/Primrec/Basic.lean,Mathlib/Computability/Primrec/List.lean |
5 |
2 |
['Komyyy', 'github-actions'] |
nobody |
0-39210 10 hours ago |
0-46918 13 hours ago |
0-48989 13 hours |
| 26377 |
Whysoserioushah author:Whysoserioushah |
feat(RingTheory/SimpleRing/TensorProduct): tensor product of a simple algebra and a central simple algebra is simple |
co-authored-by: @jjaassoonn
---
|
t-ring-theory |
203/0 |
Mathlib.lean,Mathlib/LinearAlgebra/Finsupp/LinearCombination.lean,Mathlib/RingTheory/SimpleRing/TensorProduct.lean,Mathlib/RingTheory/TwoSidedIdeal/Operations.lean |
4 |
48 |
['Ruben-VandeVelde', 'Whysoserioushah', 'eric-wieser', 'github-actions', 'kbuzzard', 'kckennylau', 'mathlib4-merge-conflict-bot', 'vlad902'] |
kbuzzard assignee:kbuzzard |
0-32477 9 hours ago |
7-82706 7 days ago |
8-3895 8 days |
| 33417 |
themathqueen author:themathqueen |
feat: `{Continuous}Linear{Isometry}Equiv.conj{Continuous, Star}AlgEquiv` are "almost" injective |
... "almost" meaning that they are colinear. I.e., `f.conj{Continuous, Star}AlgEquiv S = g.conj{Continuous, Star}AlgEquiv S` iff `f = α • g` for some (unitary) `α`.
Also, the same for `Unitary.conjStarAlgAut`. All in one PR since they all have analogous proofs.
---
- [x] depends on: #33301
[](https://gitpod.io/from-referrer/)
|
t-analysis
t-algebra
label:t-algebra$ |
243/4 |
Mathlib/Algebra/Central/End.lean,Mathlib/Algebra/Module/Equiv/Defs.lean,Mathlib/Algebra/Star/UnitaryStarAlgAut.lean,Mathlib/Analysis/InnerProductSpace/Adjoint.lean,Mathlib/Analysis/Normed/Operator/ContinuousAlgEquiv.lean,Mathlib/Topology/Algebra/Module/Equiv.lean |
6 |
6 |
['github-actions', 'mathlib4-dependent-issues-bot', 'themathqueen'] |
joelriou assignee:joelriou |
0-28037 7 hours ago |
0-28037 7 hours ago |
8-80158 8 days |
| 32974 |
jano-wol author:jano-wol |
feat: golf eq_top_of_invtSubmodule_ne_bot |
---
[](https://gitpod.io/from-referrer/)
|
t-algebra label:t-algebra$ |
111/161 |
Mathlib/Algebra/Lie/Weights/IsSimple.lean,Mathlib/Algebra/Lie/Weights/Killing.lean,Mathlib/LinearAlgebra/RootSystem/Irreducible.lean |
3 |
5 |
['github-actions', 'jano-wol', 'mathlib4-merge-conflict-bot', 'ocfnash'] |
ocfnash assignee:ocfnash |
0-26572 7 hours ago |
0-26572 7 hours ago |
3-84430 3 days |
| 32812 |
harahu author:harahu |
doc(Geometry): fix typos |
Typos found and fixed by Codex.
---
## Reviewer Guide
### `Mathlib/Geometry/Manifold/MFDeriv/Defs.lean`:
1. View https://github.com/leanprover-community/mathlib4/blob/82d02046396588be84bb6a6e116c2dfd9abfe368/Mathlib/Geometry/Manifold/MFDeriv/Defs.lean#L211 to confirm the definition docstring is consistent with our update.
2. View https://github.com/leanprover-community/mathlib4/blob/82d02046396588be84bb6a6e116c2dfd9abfe368/Mathlib/Geometry/Manifold/MFDeriv/Defs.lean#L223 to confirm that usage in code is consistent with our update.
3. See that 𝕜 does not appear in the type of `MDifferentiableWithinAt` in code.
### `Mathlib/Geometry/Manifold/Riemannian/Basic.lean`:
1. View https://github.com/leanprover-community/mathlib4/blob/82d02046396588be84bb6a6e116c2dfd9abfe368/Mathlib/Geometry/Manifold/Riemannian/Basic.lean#L37 This is the code being referenced in the updated sentence. Confirm this reads `[IsManifold I ∞ M]`.
2. View e.g. https://github.com/leanprover-community/mathlib4/blob/d59d8f5af76e0845049c8f57b77c85d80895bfde/Mathlib/Geometry/Manifold/IsManifold/Basic.lean#L846 to verify that the update reflects usage in code.
### `Mathlib/Geometry/Manifold/VectorBundle/Hom.lean`:
1. View https://github.com/leanprover-community/mathlib4/blob/d59d8f5af76e0845049c8f57b77c85d80895bfde/Mathlib/Geometry/Manifold/VectorBundle/Hom.lean#L184 to confirm `ϕ m` is applied to `v m` in `ContMDiffWithinAt.clm_apply_of_inCoordinates`, matching our update.
2. Likewise, view https://github.com/leanprover-community/mathlib4/blob/d59d8f5af76e0845049c8f57b77c85d80895bfde/Mathlib/Geometry/Manifold/VectorBundle/Hom.lean#L225 to confirm `ϕ m` is applied to `v m` in `ContMDiffAt.clm_apply_of_inCoordinates`, matching our update.
### ``:
1. View https://github.com/harahu/mathlib4/blob/3ef873bbd8341f04403f1c961bbf4af2e3f6173e/Mathlib/Geometry/Manifold/Bordism.lean#L41-L42 to confirm our update aligns with the description under Main definitions.
2. View https://github.com/harahu/mathlib4/blob/3ef873bbd8341f04403f1c961bbf4af2e3f6173e/Mathlib/Geometry/Manifold/Bordism.lean#L97-L98 to confirm our update aligns with the docstring of the structure.
3. Notice that `F` is undefined in the updated text.
[](https://gitpod.io/from-referrer/)
|
|
16/16 |
Mathlib/Geometry/Manifold/Bordism.lean,Mathlib/Geometry/Manifold/Immersion.lean,Mathlib/Geometry/Manifold/MFDeriv/Defs.lean,Mathlib/Geometry/Manifold/PartitionOfUnity.lean,Mathlib/Geometry/Manifold/Riemannian/Basic.lean,Mathlib/Geometry/Manifold/VectorBundle/Hom.lean,Mathlib/Geometry/RingedSpace/PresheafedSpace/Gluing.lean |
7 |
4 |
['erdOne', 'github-actions', 'mathlib4-merge-conflict-bot'] |
ocfnash assignee:ocfnash |
0-21183 5 hours ago |
6-1789 6 days ago |
27-17248 27 days |
| 33817 |
FlAmmmmING author:FlAmmmmING |
fix(Combinatorics/Enumerative/Schroder.lean): Fix the definition and theorem of smallSchroder. |
In the previous definition, the small Schröder numbers were defined as
```LaTeX
s_0 = 1, s_1 = 1, s_2 = 1, s_3 = 3...
```
, which does not match the sequence listed in OEIS A006318. Moreover, this definition makes it difficult to correctly write the generating function for the small Schröder numbers. This PR fixes this issue.
---
[](https://gitpod.io/from-referrer/)
|
t-combinatorics
new-contributor
large-import
|
52/35 |
Mathlib/Combinatorics/Enumerative/Schroder.lean |
1 |
5 |
['github-actions', 'vihdzp'] |
nobody |
0-20413 5 hours ago |
1-20387 1 day ago |
1-20436 1 day |
| 33836 |
VagelisKitsios author:VagelisKitsios |
feat: add lemma `le_abs_of_dvd` |
---
Add the lemma `le_abs_of_dvd {a b : ℤ} (h₁ : b ≠ 0) (h₂ : a ∣ b) : a ≤ |b|`. For the relevant discussion, see [this zulip conversation](https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/Where.20should.20I.20add.20this.20lemma.3F/with/566459906).
[](https://gitpod.io/from-referrer/)
|
easy
t-algebra
new-contributor
label:t-algebra$ |
4/0 |
Mathlib/Algebra/Order/Ring/Abs.lean |
1 |
2 |
['github-actions', 'vihdzp'] |
nobody |
0-20300 5 hours ago |
0-42774 11 hours ago |
0-43257 12 hours |
| 32403 |
FLDutchmann author:FLDutchmann |
fix(FieldSimp): `declaration has free variables` kernel errors |
Fix a bug in `field_simp` that produces a `(kernel) declaration has free variables '_example'` error which was caused by a misconfigured `simp` call.
---
The first new test produces this error on the current version of mathlib. What I believe is happening is that the discharger is using the `x != 0` hypothesis in the `then` branch, at which point that result is cached by `simp` and used in the `else` branch.
```
import Mathlib
/- (kernel) declaration has free variables '_example' -/
example {x y : ℚ}: (if x ≠ 0 then x / x else x / x) = 1 := by
field_simp
/- ⊢ (if x ≠ 0 then 1 else 1) = 1 -/
sorry
```
Edit: As @__JovanGerb__ pointed out, the correct solution was to set the `wellBehavedDischarge` flag to false, so that `simp` clears the cache more agressively. We might also want to turn on `contextual` in the future, but this would change the behaviour of `field_simp` by adding additional lemmas to the simp context. For now I propose a fix with a minimal change in behaviour.
Marking the simp context that calls the discharger as contextual appears to fix the issue, presumably by more aggressively pruning the cache. What I don't understand at this point, is why the discharger ever even had access to that hypothesis, given that contextual was set to false.
cc @JovanGerb : You understand the simp cache much better than I. Is there another bug here that I'm missing?
[](https://gitpod.io/from-referrer/)
|
t-meta |
55/14 |
Mathlib/Tactic/Abel.lean,Mathlib/Tactic/FieldSimp.lean,Mathlib/Tactic/Ring/RingNF.lean,Mathlib/Util/AtomM/Recurse.lean,MathlibTest/FieldSimp.lean |
5 |
19 |
['FLDutchmann', 'JovanGerb', 'github-actions', 'grunweg', 'leanprover-radar'] |
nobody |
0-19205 5 hours ago |
2-10189 2 days ago |
23-77905 23 days |
| 32795 |
fpvandoorn author:fpvandoorn |
fix: restrict abv positivity extension to variable functions |
* Restrict the `evalAbv` positivity extension to only apply to variable functions.
Note: this extension is called on *all* applications, and uses type-class inference to see whether it applies
* Fix a bug in `evalAbs`, which would return `.none`, even when it could return `.nonneg`.
* Originally hoped that this would improve performance, but that does not seem to be the case.
---
[](https://gitpod.io/from-referrer/)
|
t-meta
t-algebra
maintainer-merge
label:t-algebra$ |
8/2 |
Mathlib/Algebra/Order/AbsoluteValue/Basic.lean,Mathlib/Analysis/Normed/Algebra/GelfandMazur.lean,Mathlib/Tactic/Positivity/Basic.lean |
3 |
10 |
['JovanGerb', 'fpvandoorn', 'github-actions', 'leanprover-radar'] |
joneugster assignee:joneugster |
0-18903 5 hours ago |
0-18904 5 hours ago |
13-71343 13 days |
| 33697 |
artie2000 author:artie2000 |
feat(FieldTheory): real closed field |
* Define real closed fields
* Prove some very basic properties
---
[](https://gitpod.io/from-referrer/)
|
t-algebra label:t-algebra$ |
117/0 |
Mathlib.lean,Mathlib/FieldTheory/IsRealClosed/Basic.lean |
2 |
34 |
['artie2000', 'github-actions', 'vihdzp'] |
dagurtomas assignee:dagurtomas |
0-59677 16 hours ago |
3-62266 3 days ago |
4-31860 4 days |
| 33760 |
JovanGerb author:JovanGerb |
feat(Order/Bounds/Basic): use `to_dual` - part 1 |
This PR uses `to_dual` in the first half of `Order/Bounds/Basic`, and in `Order/Bounds/Defs`, and also tags `Iio`/`Ioi` and `Iic`/`Ici`. This dualization went quite smoothly.
The lemma `HasSubset.Subset.iscofinalfor` has been renamed to use correct capitalization (so that the name can be translated automatically), and has been deprecated.
A new definition defined in this PR is `IsCoinitial` as a dual to `IsCofinal`, because `IsCoinitialFor` already existed as a dual to `IsCofinalFor`.
---
[](https://gitpod.io/from-referrer/)
|
t-order
large-import
|
127/282 |
Mathlib/Order/Bounds/Basic.lean,Mathlib/Order/Bounds/Defs.lean,Mathlib/Order/Interval/Set/Defs.lean,Mathlib/Tactic/Translate/ToDual.lean |
4 |
4 |
['JovanGerb', 'github-actions', 'vihdzp'] |
nobody |
0-15642 4 hours ago |
2-61154 2 days ago |
3-8779 3 days |
| 33838 |
chainstart author:chainstart |
feat(NumberTheory): add unitary divisor sum function |
## Summary
This PR introduces the unitary divisor sum function σ* to Mathlib and proves that no odd unitary perfect numbers exist.
## Main Definitions
- `Nat.UnitaryDivisor d n`: A divisor `d` of `n` is unitary if `gcd(d, n/d) = 1`
- `Nat.unitaryDivisors n`: The `Finset` of all unitary divisors of `n`
- `Nat.unitaryDivisorSum n` (notation `σ*`): Sum of all unitary divisors
- `Nat.UnitaryPerfect n`: `n` is unitary perfect if `σ*(n) = 2n`
## Main Theorems
**Multiplicativity:**
- `unitaryDivisorSum_mul`: For coprime `m`, `n`, `σ*(mn) = σ*(m) · σ*(n)`
- Proved via explicit bijection between unitary divisors of `mn` and pairs of unitary divisors
**Prime Powers:**
- `unitaryDivisors_prime_pow`: The unitary divisors of `p^k` are exactly `{1, p^k}`
- `unitaryDivisorSum_prime_pow`: For prime `p` and `k ≥ 1`, `σ*(p^k) = p^k + 1`
**Unitary Perfect Numbers:**
- `no_odd_unitary_perfect`: There are no odd unitary perfect numbers > 1 (Subbarao-Warren 1966)
- `UnitaryPerfect.even`: Every unitary perfect number is even
- `UnitaryPerfect.eq_two_pow_mul_odd`: Every unitary perfect number has form `2^a · k` with `a ≥ 1`, `k` odd
## Mathematical Background
A unitary perfect number is a positive integer `n` such that the sum of its unitary divisors equals `2n`. This generalizes the classical perfect numbers. Only five unitary perfect numbers are known: 6, 60, 90, 87360, and one with 24 digits.
The main theorem (no odd unitary perfect numbers) was originally proved by Subbarao & Warren (1966) using prime factorization arguments. Our formalization uses `Nat.recOnPrimeCoprime` for structural induction.
## References
- Subbarao, M. V., & Warren, L. J. (1966). Unitary perfect numbers. *Canadian Mathematical Bulletin*, 9(2), 147-153.
- Wall, C. R. (1975). The fifth unitary perfect number. *Canadian Mathematical Bulletin*, 18(1), 115-122.
## Code Statistics
- **Files**: 2
- **Lines**: ~520
- **Theorems**: 21 public declarations
- **Sorry count**: 0
## Checklist
- [x] All theorem names follow mathlib conventions
- [x] All lines ≤ 100 characters
- [x] All public theorems have docstrings
- [x] No `sorry` or `admit`
- [x] Code builds successfully
- [ ] CI tests pass (awaiting verification) |
t-number-theory
new-contributor
|
540/0 |
Mathlib.lean,Mathlib/NumberTheory/UnitaryDivisor.lean,Mathlib/NumberTheory/UnitaryPerfect.lean |
3 |
3 |
['SnirBroshi', 'github-actions'] |
nobody |
0-14311 3 hours ago |
0-38510 10 hours ago |
0-38548 10 hours |
| 32144 |
EtienneC30 author:EtienneC30 |
feat: add a predicate HasGaussianLaw |
Define a predicate `HasGaussianLaw X P`, which states that under the measure `P`, the random variable `X` has a Gaussian distribution, i.e. `IsGaussian (P.map X)`.
---
- [x] depends on: #32280
- [x] depends on: #32719
[](https://gitpod.io/from-referrer/)
|
t-measure-probability
brownian
|
279/0 |
Mathlib.lean,Mathlib/Probability/Distributions/Gaussian/HasGaussianLaw/Basic.lean,Mathlib/Probability/Distributions/Gaussian/HasGaussianLaw/Def.lean |
3 |
7 |
['EtienneC30', 'RemyDegenne', 'github-actions', 'mathlib4-dependent-issues-bot', 'mathlib4-merge-conflict-bot'] |
kex-y assignee:kex-y |
0-13714 3 hours ago |
23-27624 23 days ago |
37-28546 37 days |
| 33637 |
themathqueen author:themathqueen |
feat(Analysis/Matrix/Order): `det (abs A) = |det A|` and `det (sqrt A) = √(det A)` |
... for Hermitian and positive semi-definite, respectively.
---
[](https://gitpod.io/from-referrer/)
|
t-analysis |
22/4 |
Mathlib/Analysis/Matrix/HermitianFunctionalCalculus.lean,Mathlib/Analysis/Matrix/Order.lean,Mathlib/Data/Real/Sqrt.lean |
3 |
5 |
['github-actions', 'sgouezel', 'themathqueen'] |
sgouezel assignee:sgouezel |
1-13321 1 day ago |
5-62639 5 days ago |
5-62685 5 days |
| 33764 |
IvanRenison author:IvanRenison |
feat(Combinatorics/SimpleGraph/Diam): drop `Finite α` from `ediam_le_two_mul_radius` |
---
[](https://gitpod.io/from-referrer/)
|
t-combinatorics |
22/5 |
Mathlib/Combinatorics/SimpleGraph/Diam.lean |
1 |
2 |
['github-actions', 'vlad902'] |
nobody |
0-10792 2 hours ago |
3-1195 3 days ago |
3-1240 3 days |
| 32702 |
SnirBroshi author:SnirBroshi |
chore(Combinatorics/SimpleGraph/Connectivity): move `Finite ConnectedComponent` instance from `WalkCounting.lean` to `Connected.lean` |
---
This moves it near similar instances, and makes it available for more files.
[](https://gitpod.io/from-referrer/)
|
t-combinatorics |
1/2 |
Mathlib/Combinatorics/SimpleGraph/Connectivity/Connected.lean,Mathlib/Combinatorics/SimpleGraph/Connectivity/WalkCounting.lean |
2 |
4 |
['SnirBroshi', 'github-actions', 'vihdzp', 'vlad902'] |
awainverse assignee:awainverse |
0-9367 2 hours ago |
31-71983 1 month ago |
31-72020 31 days |
| 33822 |
robin-carlier author:robin-carlier |
feat(Meta/CategoryTheory): `cancelIso` simproc |
In this PR, we define a `cancelIso` simplification procedure.
The scope of the procedure is to recognize compositions of the form `f ≫ g` or `f ≫ g ≫ h` where `g` is inverse to `f`, and cancel them accordingly.
This is particularly useful as more often than not, simp normal forms for isomorphisms do not easily make inverse pairs recognizable: `F.map (G.map (H.map e.hom))) ≫ F.map (G.map (H.map e.inv)))` is an expression in `simp`normal form, but using `Iso.hom_inv_id` requires backwards rewriting of `Functor.map_comp`.
Because of this, many _ad hoc_ lemmas handling this pattern were added to the library, e.g `CategoryTheory.Iso.inv_hom_id_app_app_app`, `CategoryTheory.MonoidalCategory.hom_inv_whiskerRight`, etc.
This simproc is an attempt at lessening the need for new extra lemmas of this form.
The core working of the simproc is as follows:
1. When encountering a composition `f ≫ g`, check if the target of `g` is the source of `f`
2. If so, Try to synth an `IsIso` instance on `f` (In all the patterns mentioned above, such instances are available). Do nothing and return if there is no such instance.
4. Run `push inv` on both `inv f` and `g`, putting them in "inv-normal form" and compare the results. If they match, build (using the proofs provided by `push`) a proof of `f ≫ g = 𝟙 _`, and return it as the result of the procedure.
In practice, the case where `g` itself is a composition is handled on its own, allowing the simproc to correctly fire on right-associated expressions (which are the chosen simp normal forms in category theory).
Because this simproc relies on `push`, it is naturally extentable by means of rigorous `@[push]` annotations within the library.
:robot: tests were initially generated by Gemini.
---
While the particular problem that this simproc solves might intersect with the capabilities of grind, I believe it is an useful thing
to have. In my experience, the place where its absence is most annoying is when carrying computation heavy proofs in bicategory theory, where I’ve encountered terms of the form `A ◁ B ◁ C ◁ D ◁ e.inv ▷ E ▷ F ▷ G ▷ H ≫ A ◁ B ◁ C ◁ D ◁ e.hom ▷ E ▷ F ▷ G ▷ H `, where `A, B, C' etc might have long names. Doing `show ... = 𝟙 _ by grind` would be very long.
This has also value for goals is not currently solving due to lack of annotations, but whose simp normal forms make such terms appear.
In the future, I think the infrastructure under this simproc might give a nice backend towards a cleaner implementation of the `rotate_iso%` elaborator I proposed in #25747, making it natively extendable via `@[push]` annotations.
I am not very well versed in metaprogramming, so the main questions I would ask are
- Is the `withReducible` useful? I put it as a safe measure to avoid triggering expensive def-eq checks, but I don’t know wether or not being in the `SimpM` monad wraps things with this transparency already?
- Is the file in the right place? Should it be in the folder with other Simprocs despite being specialized to category theory?
- I did not make it as a simproc that should fire by default, as I am slightly wary of the performances here, but maybe I’m overthinking it?
- [ ] depends on: #33820
[](https://gitpod.io/from-referrer/)
|
t-meta
t-category-theory
|
268/20 |
Mathlib.lean,Mathlib/CategoryTheory/Bicategory/Basic.lean,Mathlib/CategoryTheory/Comma/Basic.lean,Mathlib/CategoryTheory/Iso.lean,Mathlib/CategoryTheory/Limits/Shapes/Pullback/Categorical/Basic.lean,Mathlib/CategoryTheory/Monoidal/Category.lean,Mathlib/CategoryTheory/Monoidal/Closed/FunctorCategory/Groupoid.lean,Mathlib/CategoryTheory/NatIso.lean,Mathlib/CategoryTheory/Opposites.lean,Mathlib/Tactic.lean,Mathlib/Tactic/CategoryTheory/CancelIso.lean,MathlibTest/CategoryTheory/CancelIso.lean |
12 |
48 |
['JovanGerb', 'github-actions', 'leanprover-radar', 'mathlib4-dependent-issues-bot', 'plp127', 'robin-carlier'] |
nobody |
0-5967 1 hour ago |
0-6542 1 hour ago |
0-6520 1 hour |
| 33355 |
0xTerencePrime author:0xTerencePrime |
feat(Combinatorics/SimpleGraph/Connectivity): define vertex connectivity |
This PR introduces the foundations of vertex connectivity for simple graphs, providing a counterpart to the edge connectivity theory in #32870.
### Main definitions
- `SimpleGraph.IsVertexReachable`: vertices remain reachable after removing strictly fewer than `k` other vertices.
- `SimpleGraph.IsVertexConnected`: a graph is `k`-vertex-connected if its order is strictly greater than `k` and any two distinct vertices are `k`-vertex-reachable.
Includes basic characterizations for $k=0$ and $k=1$, along with monotonicity lemmas (`anti` and `mono`). |
t-combinatorics
new-contributor
|
152/0 |
Mathlib.lean,Mathlib/Combinatorics/SimpleGraph/Connectivity/VertexConnectivity.lean,Mathlib/Combinatorics/SimpleGraph/IsolateVerts.lean |
3 |
97 |
['0xTerencePrime', 'SnirBroshi', 'github-actions', 'vihdzp'] |
nobody |
0-5604 1 hour ago |
14-19129 14 days ago |
14-19165 14 days |
| 33785 |
vihdzp author:vihdzp |
feat: small lemmas on `ArchimedeanClass` |
---
[](https://gitpod.io/from-referrer/)
|
t-algebra label:t-algebra$ |
34/0 |
Mathlib/Algebra/Order/Archimedean/Class.lean |
1 |
3 |
['github-actions', 'vihdzp', 'wwylele'] |
nobody |
0-3765 1 hour ago |
2-46445 2 days ago |
2-46489 2 days |
| 33845 |
bjornsolheim author:bjornsolheim |
feat(Analysis/Convex): barycenter of a standard simplex |
barycenter of a standard simplex
(There might be a case for not using Finset.centerMass to have a simpler definition. Centroid is another related concept, but I thought it best not to add new imports.)
alternative
def barycenter' : stdSimplex 𝕜 X :=
⟨fun _ => (Fintype.card X : 𝕜)⁻¹,
⟨fun _ => inv_nonneg.mpr (Nat.cast_nonneg _),
by simp [Finset.card_univ]⟩⟩
---
[](https://gitpod.io/from-referrer/)
|
t-analysis |
29/0 |
Mathlib/Analysis/Convex/StdSimplex.lean |
1 |
1 |
['github-actions'] |
nobody |
0-3357 55 minutes ago |
0-3364 55 minutes ago |
0-3403 56 minutes |
| 32880 |
0xTerencePrime author:0xTerencePrime |
feat(Analysis/Asymptotics): define subpolynomial growth |
## Main definitions
* `Asymptotics.IsSubpolynomial l f g`: A function `f` has subpolynomial growth with respect to `g` along filter `l` if `f = O(1 + ‖g‖^k)` for some natural `k`.
## Main results
* `IsSubpolynomial.const`: Constant functions have subpolynomial growth
* `IsSubpolynomial.id`: Identity has subpolynomial growth
* `IsSubpolynomial.add`: Closure under addition
* `IsSubpolynomial.neg`: Closure under negation
* `IsSubpolynomial.sub`: Closure under subtraction
* `IsSubpolynomial.mul`: Closure under multiplication
* `IsSubpolynomial.pow`: Closure under powers
* `isSubpolynomial_iff_one_add`: Equivalence with `(1 + ‖g‖)^k` formulation
* `IsSubpolynomial.uniform`: Uniform bounds for finite families
## Implementation notes
The definition uses `1 + ‖g‖^k` rather than `(1 + ‖g‖)^k` as the primary form, with the equivalence established in `isSubpolynomial_iff_one_add`. Four private auxiliary lemmas handle the key inequalities needed for closure proofs.
Closes #32658
|
awaiting-author
t-analysis
new-contributor
|
289/0 |
Mathlib.lean,Mathlib/Analysis/Asymptotics/Subpolynomial.lean |
2 |
4 |
['ADedecker', 'github-actions', 'j-loreaux'] |
ADedecker assignee:ADedecker |
4-66370 4 days ago |
4-66370 4 days ago |
23-24928 23 days |
| 33837 |
Komyyy author:Komyyy |
feat: `Tendsto (√·) atTop atTop` |
From [CLT](https://github.com/RemyDegenne/CLT/blob/07a49e97b1c745d306d301200a97c48eeb299205/Clt/CLT.lean#L34).
I proved the more strong statements: `map (√·) atTop = atTop` and `comap (√·) atTop = atTop`.
While I'm at it, I added a `fun_prop` attr to `Continuous (√·)`.
---
For reviewers: What I checked
* I [loogled](https://loogle.lean-lang.org/?q=Real.sqrt%2C+Filter.atTop) to make sure these lemmas are not yet in Mathlib.
* I made sure it's unnecessary to make the lemmas of `NNReal.sqrt` version because `NNReal.sqrt` is `OrderIso` and [Mathlib already has the lemma of `OrderIso` version](https://loogle.lean-lang.org/?q=OrderIso%2C+Filter.atTop).
[](https://gitpod.io/from-referrer/)
|
t-topology
t-order
|
15/5 |
Mathlib/Data/Real/Sqrt.lean |
1 |
8 |
['Komyyy', 'eric-wieser', 'github-actions'] |
nobody |
0-1166 19 minutes ago |
0-33935 9 hours ago |
0-40697 11 hours |