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 |
37-43913 1 month ago |
40-79537 1 month ago |
42-79960 42 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 |
37-43903 1 month ago |
43-36213 1 month ago |
43-36253 43 days |
| 29942 |
smmercuri author:smmercuri |
feat(InfinitePlace/Completion): embeddings of `w.Completion` factor through embeddings of `v.Completion` when `w` extends `v` |
If `w : v.Extension L` is an extension of `v : InfinitePlace K` to `L`, 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 |
89/14 |
Mathlib/Analysis/Normed/Field/WithAbs.lean,Mathlib/NumberTheory/NumberField/InfinitePlace/Completion.lean,Mathlib/NumberTheory/NumberField/InfinitePlace/Embeddings.lean,Mathlib/NumberTheory/NumberField/InfinitePlace/Ramification.lean,Mathlib/Topology/MetricSpace/Completion.lean |
5 |
5 |
['github-actions', 'mathlib4-dependent-issues-bot', 'mathlib4-merge-conflict-bot'] |
joelriou assignee:joelriou |
36-67696 1 month ago |
40-67666 1 month ago |
40-68758 40 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 |
36-43899 1 month ago |
40-33978 1 month ago |
40-36599 40 days |
| 32238 |
YaelDillies author:YaelDillies |
feat(Combinatorics/SimpleGraph): distributivity of box product over sum |
From ProofBench
---
[](https://gitpod.io/from-referrer/)
|
t-combinatorics
large-import
|
21/2 |
Mathlib/Combinatorics/SimpleGraph/Prod.lean |
1 |
1 |
['github-actions'] |
kmill assignee:kmill |
36-43889 1 month ago |
39-81236 1 month ago |
39-81267 39 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 |
31-68064 1 month ago |
31-68183 1 month ago |
36-62612 36 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 |
31-52122 1 month ago |
37-55324 1 month ago |
37-58274 37 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 |
31-43905 1 month ago |
34-50236 1 month ago |
35-54833 35 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 |
31-6052 1 month ago |
31-6081 1 month ago |
31-13657 31 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 |
30-43904 30 days ago |
34-31219 1 month ago |
34-31206 34 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 |
27-61261 27 days ago |
27-75447 27 days ago |
48-35598 48 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 |
26-77096 26 days ago |
31-4901 1 month ago |
31-5189 31 days |
| 32440 |
thorimur author:thorimur |
feat: make the `unusedDecidableInType` linter fire when `Decidable*` instances are used only inside of proofs in the type |
This PR adjusts the `unusedDecidableInType` to prevent false negatives on declarations that only use `Decidable*` hypotheses in proofs that appear in the type. That is, the linter now fires when the `Decidable*` linter is unused outside of proofs.
This PR also changes the warning message to be more direct, and indicates when the instance appears only in a proof (vs. not appearing at all).
We exempt some deprecated lemmas in `Mathlib.Analysis.Order.Matrix` which the linter now fires on. (Presumably, most prior violations had been cleaned up by #10235, which also detected such lemmas.)
Note that this took some tinkering to achieve sufficient performance. We use the following novel(?) "dolorous telescope" strategy (so named due to introducing `sorry`s) to avoid traversing the whole type:
- when encountering an instance binder of concern, telescope to create an fvar.
- when encountering any other binder, instantiate it with `sorry`.
- as we proceed, collect the free variables from these expressions which do not appear in proofs. Since the instances of concern are the only free variables, free variable collection avoids traversing many subexpressions by checking for `hasFVar`, which is a computed field accessible in constant time.
Perhaps surprisingly, this is (on net) more performant than using `eraseProofs` and then detecting dependence via bvars.
We also implement an `Expr`-level early exit for most types by checking if they bind any instance of concern first. (This adds a very small overhead to types which *do* have an instance of concern, but the check is very fast.)
This also adds a profiler category to this linter.
Note: we still have yet to optimize (pre)-infotree traversal performance, and have yet to avoid proofs that appear in the value of definitions. However, this PR sets us up to do so.
---
## Notes on performance
You might be wondering if this *is* actually a faster strategy, seeing as the bench is quite noisy. To determine this, I made a copy of the linter which I could vary without rebuilding mathlib, and profiled the relevant component locally on all imported declarations in Mathlib by linting the `eoi` token:
```lean
module
public meta import Lean
public import Mathlib.Tactic.Linter.UnusedInstancesInTypeCopy
import all Mathlib.Tactic.Linter.UnusedInstancesInTypeCopy
open Lean Meta Elab Term Command Mathlib.Linter.UnusedInstancesInType
meta section
local instance : Insert Name NameSet where
insert := fun n s => s.insert n
def runCopy : Linter where run stx := do
if stx.isOfKind ``Parser.Command.eoi then
let opts := (← getOptions).setBool `profiler true
let consts := (← getEnv).constants.map₁
-- The following expose private decls in their types, so break `MetaM` methods:
let badRecs : NameSet := {`IO.Promise.casesOn, `IO.Promise.recOn, `IO.Promise.rec}
profileitM Exception "control" opts do
for (n,_) in consts do
liftTermElabM do unless n.isInternalDetail || badRecs.contains n do pure ()
profileitM Exception "bench" opts do
for (n,cinfo) in consts do
unless n.isInternalDetail || badRecs.contains n do
cinfo.toConstantVal.onUnusedInstancesInTypeWhere isDecidableVariant
fun _ _ => pure ()
initialize addLinter runCopy
```
(This could have been done in a `run_cmd`, but I wanted to replicate the circumstances of linting as closely as possible, just in case it introduced mysterious async effects.)
Then, in a separate file, I imported `Mathlib` and the above linter, and cycled through reading out the result and editing the underlying component then rebuilding. The control was reliably ~1.07-1.12s. The different strategies came out as follows (the following values are not averaged, but are representative):
| | without early exit | with early exit |
| ---: | :---: | :---: |
| `eraseProofs` | 97.4s | 6.82s |
| dolorous telescope | 20.3s | 3.99s |
As you can see, the early exit cuts the absolute value (and therefore the absolute difference) down dramatically. But seeing as this lays the groundwork for linting defs and will be used for more linters (with wider scopes, and less early exit opportunities), I think we should opt for the more performant version even though there's some extra complexity. :)
[](https://gitpod.io/from-referrer/)
|
t-linter |
199/51 |
Mathlib/Analysis/Matrix/Order.lean,Mathlib/Lean/Expr/Basic.lean,Mathlib/Tactic/Linter/UnusedInstancesInType.lean,MathlibTest/UnusedInstancesInType.lean |
4 |
29 |
['github-actions', 'grunweg', 'leanprover-radar', 'thorimur'] |
joneugster assignee:joneugster |
25-43890 25 days ago |
30-30335 30 days ago |
33-61614 33 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 |
25-28033 25 days ago |
31-60876 1 month ago |
31-60915 31 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 |
24-72904 24 days ago |
29-67772 29 days ago |
29-68033 29 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 |
22-79444 22 days ago |
29-12944 29 days ago |
52-76316 52 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 |
22-43912 22 days ago |
26-33262 26 days ago |
26-33294 26 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 |
21-67634 21 days ago |
21-67637 21 days ago |
27-64888 27 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
|
378/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 |
21-43910 21 days ago |
24-64853 24 days ago |
28-27955 28 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 |
21-43904 21 days ago |
27-26859 27 days ago |
27-26833 27 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 |
21-32554 21 days ago |
31-59598 1 month ago |
31-59627 31 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 |
21-32094 21 days ago |
31-36397 1 month ago |
31-36437 31 days |
| 31925 |
alreadydone author:alreadydone |
feat(Topology): étalé space associated to a predicate on sections |
---
migrated from #22782
[](https://gitpod.io/from-referrer/)
|
t-topology |
899/164 |
Mathlib.lean,Mathlib/AlgebraicGeometry/ProjectiveSpectrum/StructureSheaf.lean,Mathlib/Data/Set/Operations.lean,Mathlib/Geometry/Manifold/Sheaf/Smooth.lean,Mathlib/Logic/Equiv/Basic.lean,Mathlib/Topology/EtaleSpace.lean,Mathlib/Topology/IsLocalHomeomorph.lean,Mathlib/Topology/Sheaves/LocalPredicate.lean,Mathlib/Topology/Sheaves/Sheafify.lean,Mathlib/Topology/Sheaves/Stalks.lean |
10 |
13 |
['adamtopaz', 'alreadydone', 'github-actions', 'mathlib4-merge-conflict-bot'] |
adamtopaz assignee:adamtopaz |
20-67356 20 days ago |
20-71328 20 days ago |
25-66811 25 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 |
20-55518 20 days ago |
20-55582 20 days ago |
29-177 29 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 |
20-48171 20 days ago |
20-48663 20 days ago |
30-53275 30 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 |
20-8100 20 days ago |
21-36511 21 days ago |
21-36553 21 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 |
19-80787 19 days ago |
45-22450 1 month ago |
45-53338 45 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 |
19-52135 19 days ago |
19-52161 19 days ago |
32-21107 32 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 |
19-51870 19 days ago |
20-32325 20 days ago |
38-44225 38 days |
| 31960 |
urkud author:urkud |
feat: a lower bound for the volume of a cone on the unit sphere |
---
- [x] depends on: #31956
- [x] depends on: #31957
[](https://gitpod.io/from-referrer/)
|
t-measure-probability |
95/0 |
Mathlib/MeasureTheory/Constructions/HaarToSphere.lean |
1 |
6 |
['PatrickMassot', 'github-actions', 'mathlib4-dependent-issues-bot', 'mathlib4-merge-conflict-bot', 'urkud'] |
hrmacbeth assignee:hrmacbeth |
19-50702 19 days ago |
43-56917 1 month ago |
43-59460 43 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 |
19-43920 19 days ago |
22-55483 22 days ago |
22-57987 22 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 |
43/9 |
Mathlib/Algebra/Free.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 |
19 |
5 |
['EtienneC30', 'YaelDillies', 'artie2000', 'github-actions'] |
kex-y assignee:kex-y |
19-43919 19 days ago |
31-72479 1 month ago |
31-82768 31 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 |
19-43916 19 days ago |
26-37030 26 days ago |
26-37035 26 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 |
19-9651 19 days ago |
19-9710 19 days ago |
40-75031 40 days |
| 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 |
6 |
['EtienneC30', 'RemyDegenne', 'github-actions', 'mathlib4-dependent-issues-bot', 'mathlib4-merge-conflict-bot'] |
kex-y assignee:kex-y |
18-74041 18 days ago |
20-11825 20 days ago |
34-12743 34 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 |
1 |
['github-actions', 'vlad902'] |
awainverse assignee:awainverse |
18-43890 18 days ago |
28-56184 28 days ago |
28-56218 28 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 |
18-43889 18 days ago |
27-78311 27 days ago |
27-78389 27 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 |
18-43886 18 days ago |
23-79862 23 days ago |
23-80188 23 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 |
18-43885 18 days ago |
22-34692 22 days ago |
22-34728 22 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 |
18-43882 18 days ago |
21-54385 21 days ago |
21-54358 21 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 |
18-37916 18 days ago |
18-37940 18 days ago |
27-80005 27 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 |
17-43892 17 days ago |
20-75224 20 days ago |
20-82546 20 days |
| 31315 |
Parcly-Taxel author:Parcly-Taxel |
feat: IMO 2010 Q5 |
See [#general > Panic in rw: Nat.pow exponent is too big @ 💬](https://leanprover.zulipchat.com/#narrow/channel/113488-general/topic/Panic.20in.20rw.3A.20Nat.2Epow.20exponent.20is.20too.20big/near/513294906) and leanprover/lean4#11713 for why 2010 and 11 are replaced with variables. |
maintainer-merge
IMO
|
245/0 |
Archive.lean,Archive/Imo/Imo2010Q5.lean |
2 |
6 |
['Parcly-Taxel', 'github-actions', 'jsm28', 'nomeata'] |
jsm28 assignee:jsm28 |
17-43891 17 days ago |
20-48177 20 days ago |
42-45256 42 days |
| 33052 |
JovanGerb author:JovanGerb |
feat: replace `rw??` tactic with `#infoview_search` command |
This PR introduces the `#infoview_search` command. It gives an improved way of interacting with the library search from `rw??`, and hence this PR also deprecates `rw??` (`rw??` still works, but it displays a warning message suggesting to use `#infoview_search` instead).
The difference is that `#infoview_search` is a command, so you type it once, and then you can use rewrite search in any tactic state in any place. This is more convenient than having to write out `rw??` every time.
I have many improvements planned for `#infoview_search`, but this PR simply gives it the same capabilities that `rw??` currently has. One of those improvements is to also do `apply` search, and `apply at` search. That is why the name doesn't contain `rw` anymore.
To prepare for more code developments around `#infoview_search`, I've moved the relevant files into a new folder `Mathlib.Tactic.InfoviewSearch`.
Note that one annoyance with writing `#infoview_search` is that there is a linter warning. Should I remove the `#` from the command, or are we happy with this?
```
`#`-commands, such as '#infoview_search', are not allowed in 'Mathlib'
Note: This linter can be disabled with `set_option linter.hashCommand false`
```
---
[](https://gitpod.io/from-referrer/)
|
t-meta
file-removed
|
100/59 |
Mathlib.lean,Mathlib/Tactic.lean,Mathlib/Tactic/Common.lean,Mathlib/Tactic/InfoviewSearch/InteractiveUnfold.lean,Mathlib/Tactic/InfoviewSearch/LibraryRewrite.lean,MathlibTest/LibraryRewrite.lean |
6 |
1 |
['github-actions'] |
adamtopaz assignee:adamtopaz |
17-43883 17 days ago |
20-68956 20 days ago |
20-69006 20 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 |
17-13106 17 days ago |
18-47775 18 days ago |
156-79463 156 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 |
16-43908 16 days ago |
19-69918 19 days ago |
19-69977 19 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 |
16-43905 16 days ago |
21-21430 21 days ago |
21-21470 21 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 |
16-43903 16 days ago |
19-54730 19 days ago |
20-30075 20 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 |
16-43902 16 days ago |
19-47372 19 days ago |
20-6915 20 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 |
16-43900 16 days ago |
20-2422 20 days ago |
20-2465 20 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 |
16-43895 16 days ago |
19-57227 19 days ago |
19-57208 19 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'] |
nobody |
16-38142 16 days ago |
16-39908 16 days ago |
21-37025 21 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'] |
nobody |
16-26228 16 days ago |
16-37828 16 days ago |
16-37868 16 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 |
15-43896 15 days ago |
19-1539 19 days ago |
19-1578 19 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 |
15-43895 15 days ago |
18-53991 18 days ago |
18-78524 18 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 |
7 |
['JovanGerb', 'github-actions'] |
thorimur assignee:thorimur |
15-43894 15 days ago |
18-73377 18 days ago |
18-76406 18 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 |
15-2336 15 days ago |
15-2348 15 days ago |
15-2381 15 days |
| 31794 |
thorimur author:thorimur |
feat: `unusedFintypeInType` linter |
Adds an `UnusedInstancesInType` linter which suggests replacing `Fintype` instances with `Finite` or removing them.
This linter is off by default: it is turned on in #31795.
The violations found by this linter are fixed in #33068 (merged) and #33148 (merged).
Note that the portion of this diff corresponding to the actual linter file is relatively small (+68 -11), and is very similar to the `unusedDecidableInType` linter. The majority of the diff in the linter file itself is factoring out the workaround to lean4#11313 (which is used in both linters); the rest of the diff comes from reorganizing tests and adding tests.
---
- [x] depends on: #31142
[](https://gitpod.io/from-referrer/)
|
file-removed |
304/46 |
Mathlib/Tactic/Linter/UnusedInstancesInType.lean,MathlibTest/UnusedInstancesInType/Basic.lean,MathlibTest/UnusedInstancesInType/Decidable.lean,MathlibTest/UnusedInstancesInType/Fintype.lean,MathlibTest/UnusedInstancesInType/FintypeNeedingImport.lean,MathlibTest/UnusedInstancesInType/SetOption.lean |
6 |
11 |
['JovanGerb', 'github-actions', 'mathlib4-dependent-issues-bot', 'mathlib4-merge-conflict-bot', 'thorimur'] |
JovanGerb assignee:JovanGerb |
14-75052 14 days ago |
18-48677 18 days ago |
35-67818 35 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 |
14-65518 14 days ago |
15-1824 15 days ago |
15-1859 15 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 |
14-59558 14 days ago |
42-41526 1 month ago |
42-41556 42 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 |
14-43910 14 days ago |
18-37044 18 days ago |
18-37088 18 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 |
14-19278 14 days ago |
14-19302 14 days ago |
40-15931 40 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 |
14-5479 14 days ago |
19-13497 19 days ago |
19-13536 19 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 |
13-43899 13 days ago |
16-47485 16 days ago |
16-47461 16 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 |
12-43912 12 days ago |
27-73636 27 days ago |
27-73686 27 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 |
12-43908 12 days ago |
22-72640 22 days ago |
22-72676 22 days |
| 33236 |
JovanGerb author:JovanGerb |
refactor(translate): merge `expand` into `applyReplacementFun` |
This PR refactors the main translation loop 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`.
---
[](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 |
12-43905 12 days ago |
15-73555 15 days ago |
15-73594 15 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 |
12-43904 12 days ago |
15-45299 15 days ago |
15-45335 15 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 |
12-24994 12 days ago |
12-81542 12 days ago |
13-49979 13 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 |
11-43874 11 days ago |
22-45020 22 days ago |
22-44993 22 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 |
10-69995 10 days ago |
10-70020 10 days ago |
16-2581 16 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 |
10-50717 10 days ago |
10-50744 10 days ago |
10-50782 10 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 |
10-46500 10 days ago |
10-46913 10 days ago |
69-4016 69 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 |
10-43887 10 days ago |
13-70512 13 days ago |
13-70548 13 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 |
10-32805 10 days ago |
19-50746 19 days ago |
85-16073 85 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 |
10-9764 10 days ago |
24-8899 24 days ago |
44-8724 44 days |
| 33339 |
Ruben-VandeVelde author:Ruben-VandeVelde |
feat: small lemmas about LeftInverse and image/preimage |
From sphere-eversion.
---
[](https://gitpod.io/from-referrer/)
|
t-data |
9/1 |
Mathlib/Data/Set/Image.lean |
1 |
3 |
['Ruben-VandeVelde', 'github-actions', 'vihdzp'] |
nobody |
10-6205 10 days ago |
12-3230 12 days ago |
12-3270 12 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 |
9-49086 9 days ago |
19-52110 19 days ago |
20-53864 20 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 |
9-43905 9 days ago |
12-64298 12 days ago |
12-64756 12 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 |
9-43904 9 days ago |
13-39904 13 days ago |
13-39878 13 days |
| 33299 |
kingiler author:kingiler |
feat: Add decidable membership for Interval |
Implemented membership and corresponding decidable instance for `Interval`.
Related [#mathlib4 > Proposal: Add decidable membership for Interval](https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/Proposal.3A.20Add.20decidable.20membership.20for.20Interval/with/565438009).
---
[](https://gitpod.io/from-referrer/)
|
t-order
new-contributor
|
16/1 |
Mathlib/Order/Interval/Basic.lean |
1 |
3 |
['eric-wieser', 'github-actions', 'kingiler'] |
Vierkantor assignee:Vierkantor |
9-43903 9 days ago |
13-27987 13 days ago |
13-32569 13 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 |
9-14028 9 days ago |
12-13010 12 days ago |
12-13048 12 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 |
8-43895 8 days ago |
12-15489 12 days ago |
18-68360 18 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
|
151/0 |
Mathlib/ModelTheory/Definability.lean |
1 |
58 |
['NoneMore', 'github-actions', 'staroperator'] |
fpvandoorn assignee:fpvandoorn |
6-75211 6 days ago |
27-28561 27 days ago |
27-73864 27 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 |
6-67530 6 days ago |
6-67537 6 days ago |
6-67571 6 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 |
6-52205 6 days ago |
6-52205 6 days ago |
16-34888 16 days |
| 33278 |
harahu author:harahu |
doc(MeasureTheory): remove stale paragraph |
- Remove a paragraph describing definition of notation that does not happen in this file.
- Also align a scalar multiplication symbol in the docs with the symbol used in the code.
---
[](https://gitpod.io/from-referrer/)
|
t-measure-probability |
1/4 |
Mathlib/MeasureTheory/Integral/Bochner/L1.lean |
1 |
4 |
['bryangingechen', 'github-actions', 'harahu', 'mathlib4-merge-conflict-bot'] |
kex-y assignee:kex-y |
6-46676 6 days ago |
7-46478 7 days ago |
14-3785 14 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/)
|
t-algebraic-topology |
298/28 |
Mathlib/AlgebraicTopology/Quasicategory/StrictBicategory.lean,Mathlib/AlgebraicTopology/SimplicialSet/HoFunctorMonoidal.lean,Mathlib/AlgebraicTopology/SimplicialSet/NerveAdjunction.lean |
3 |
16 |
['github-actions', 'joelriou', 'mathlib4-dependent-issues-bot', 'mathlib4-merge-conflict-bot', 'robin-carlier'] |
robin-carlier assignee:robin-carlier |
6-12265 6 days ago |
6-12265 6 days ago |
12-60796 12 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 |
5-59241 5 days ago |
13-53488 13 days ago |
13-53534 13 days |
| 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 label:t-algebra$ |
243/0 |
Mathlib.lean,Mathlib/LinearAlgebra/AffineSpace/AffineSubspace/Basic.lean,Mathlib/LinearAlgebra/AffineSpace/Ceva.lean,docs/100.yaml,docs/1000.yaml |
5 |
9 |
['github-actions', 'jsm28', 'plby'] |
mariainesdff assignee:mariainesdff |
5-43916 5 days ago |
8-53998 8 days ago |
8-53972 8 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 |
78-60241 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 |
5-27659 5 days ago |
6-10077 6 days ago |
6-10112 6 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 |
5-20539 5 days ago |
12-19109 12 days ago |
27-39596 27 days |
| 32438 |
JovanGerb author:JovanGerb |
feat: unfold-boundaries in `to_dual` |
This PR introduces a new feature to `to_dual` that allows us to have definitions whose dual is not definitionally equal to the dual of the value. This is crucial for many definitions that are dual to something morally but not definitionally. For example, `DecidableLE`, `Set.Ioo`, `Set.Ico`, `CovBy` , `Monotone`.
- [x] Tracing to see what this is doing
- [x] Improve the UI of applying the `to_dual_insert_cast` and `to_dual_insert_cast_fun` attributes.
- [x] Add tests
- [x] Better documentation
---
[](https://gitpod.io/from-referrer/)
|
t-meta |
518/128 |
Mathlib.lean,Mathlib/Combinatorics/Quiver/Basic.lean,Mathlib/Order/Basic.lean,Mathlib/Order/Cover.lean,Mathlib/Order/Defs/LinearOrder.lean,Mathlib/Order/Defs/PartialOrder.lean,Mathlib/Order/GaloisConnection/Defs.lean,Mathlib/Order/Interval/Set/Defs.lean,Mathlib/Order/Monotone/Defs.lean,Mathlib/Order/WithBot.lean,Mathlib/Tactic.lean,Mathlib/Tactic/ToDual.lean,Mathlib/Tactic/Translate/Core.lean,Mathlib/Tactic/Translate/ToDual.lean,Mathlib/Tactic/Translate/UnfoldBoundary.lean,MathlibTest/ToDual.lean |
16 |
12 |
['JovanGerb', 'fpvandoorn', 'github-actions', 'leanprover-radar', 'mathlib4-merge-conflict-bot', 'vihdzp'] |
bryangingechen assignee:bryangingechen |
5-14708 5 days ago |
5-14733 5 days ago |
15-31039 15 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 |
5-9350 5 days ago |
29-70973 29 days ago |
29-71004 29 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 |
4-81098 4 days ago |
5-6995 5 days ago |
5-7028 5 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 |
4-73817 4 days ago |
4-76396 4 days ago |
4-76370 4 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 |
1 |
['github-actions'] |
nobody |
4-60492 4 days ago |
4-60501 4 days ago |
4-60534 4 days |
| 31595 |
astrainfinita author:astrainfinita |
chore: redefine `Ideal.IsPrime` |
Redefine `Ideal.IsPrime` to make it correct for non-commutative cases
---
[](https://gitpod.io/from-referrer/)
|
t-algebra label:t-algebra$ |
330/100 |
Mathlib/Algebra/Order/Ring/Ordering/Defs.lean,Mathlib/AlgebraicGeometry/StructureSheaf.lean,Mathlib/RingTheory/DedekindDomain/Ideal/Lemmas.lean,Mathlib/RingTheory/GradedAlgebra/Radical.lean,Mathlib/RingTheory/Ideal/AssociatedPrime/Basic.lean,Mathlib/RingTheory/Ideal/IsPrimary.lean,Mathlib/RingTheory/Ideal/Maps.lean,Mathlib/RingTheory/Ideal/Maximal.lean,Mathlib/RingTheory/Ideal/Oka.lean,Mathlib/RingTheory/Ideal/Operations.lean,Mathlib/RingTheory/Ideal/Over.lean,Mathlib/RingTheory/Ideal/Pointwise.lean,Mathlib/RingTheory/Ideal/Prime.lean,Mathlib/RingTheory/Ideal/Prod.lean,Mathlib/RingTheory/Ideal/Quotient/Basic.lean,Mathlib/RingTheory/Ideal/Quotient/Operations.lean,Mathlib/RingTheory/Localization/AtPrime/Basic.lean,Mathlib/RingTheory/Localization/Ideal.lean,Mathlib/RingTheory/Polynomial/Basic.lean,Mathlib/RingTheory/PrincipalIdealDomain.lean,Mathlib/RingTheory/Spectrum/Prime/Topology.lean,Mathlib/RingTheory/Valuation/Basic.lean |
22 |
29 |
['alreadydone', 'artie2000', 'astrainfinita', 'erdOne', 'github-actions', 'leanprover-bot', 'leanprover-community-mathlib4-bot', 'mathlib4-merge-conflict-bot'] |
alreadydone assignee:alreadydone |
4-59069 4 days ago |
9-41749 9 days ago |
26-33890 26 days |
| 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 |
206/276 |
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,MathlibTest/GCongr/GCongr.lean |
29 |
3 |
['github-actions', 'mathlib4-merge-conflict-bot'] |
dwrensha assignee:dwrensha |
4-43888 4 days ago |
19-39496 19 days ago |
20-82908 20 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$ |
355/11 |
Mathlib.lean,Mathlib/RepresentationTheory/Intertwining.lean,Mathlib/RepresentationTheory/Irreducible.lean,Mathlib/RepresentationTheory/Subrepresentation.lean |
4 |
1 |
['github-actions'] |
ocfnash assignee:ocfnash |
4-43887 4 days ago |
16-31297 16 days ago |
16-31337 16 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 |
4-43887 4 days ago |
7-61298 7 days ago |
9-33457 9 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 |
4-43883 4 days ago |
8-41027 8 days ago |
8-41008 8 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 |
4-43881 4 days ago |
7-52544 7 days ago |
7-52582 7 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 |
4-41436 4 days ago |
5-31087 5 days ago |
5-34275 5 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/)
|
t-data |
17/0 |
Mathlib/Data/Matrix/Cartan.lean |
1 |
1 |
['github-actions'] |
nobody |
4-22706 4 days ago |
4-22946 4 days ago |
4-22980 4 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 |
4-15860 4 days ago |
5-55994 5 days ago |
6-38562 6 days |
| 27706 |
xroblot author:xroblot |
feat(RingTheory/Localization/AtPrime): inertia degree and ramification index are preserved by localization |
Let `R ⊆ S` be an extension of rings and `p` be a prime ideal of `R`. Denote by `Rₚ` the localization of `R` at the complement of `p` and by `Sₚ` the localization of `S` at the (image) of the complement of `p`.
In this PR, we prove that the bijection between the (nonzero) prime ideals of `Sₚ` and the prime ideals of `S` above `p` preserves the residual degree and the ramification index.
---
- [x] depends on: #27794
- [x] depends on: #27796
- [x] depends on: #27798
- [x] depends on: #28526
- [x] depends on: #29322
- [x] depends on: #32045 |
large-import
t-ring-theory
|
192/9 |
Mathlib/NumberTheory/RamificationInertia/Basic.lean,Mathlib/RingTheory/Localization/AtPrime/Basic.lean,Mathlib/RingTheory/Localization/AtPrime/Extension.lean |
3 |
9 |
['github-actions', 'mathlib4-dependent-issues-bot', 'mathlib4-merge-conflict-bot', 'riccardobrasca', 'xroblot'] |
riccardobrasca assignee:riccardobrasca |
3-84541 3 days ago |
3-84541 3 days ago |
4-1178 4 days |
| 33551 |
metakunt author:metakunt |
feat(Data/Nat/Factorization/PrimePow): Add Nat.primeFactors_nontrivial_of_two_le_of_not_isPrimePow |
|
t-data |
11/0 |
Mathlib/Data/Nat/Factorization/PrimePow.lean |
1 |
1 |
['github-actions'] |
nobody |
3-77248 3 days ago |
3-77248 3 days ago |
3-77292 3 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 |
3-58181 3 days ago |
7-79941 7 days ago |
7-79925 7 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 |
3-56305 3 days ago |
24-36692 24 days ago |
24-36667 24 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π.
---
- [ ] depends on: #30474
- [ ] depends on: #30477
- [ ] depends on: #30600
- [ ] depends on: #30703
[](https://gitpod.io/from-referrer/)
|
t-euclidean-geometry |
193/50 |
Mathlib/Geometry/Euclidean/Angle/Bisector.lean |
1 |
12 |
['JovanGerb', 'github-actions', 'jsm28', 'mathlib4-dependent-issues-bot', 'mathlib4-merge-conflict-bot'] |
JovanGerb assignee:JovanGerb |
16-72656 16 days ago |
50-8470 1 month ago |
54-51697 54 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 |
3-43878 3 days ago |
6-53527 6 days ago |
6-53500 6 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 |
3-43877 3 days ago |
6-53128 6 days ago |
6-53101 6 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 |
3-43877 3 days ago |
6-53183 6 days ago |
6-53156 6 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 |
3-36758 3 days ago |
3-42235 3 days ago |
71-12812 71 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'] |
nobody |
3-34001 3 days ago |
3-34038 3 days ago |
3-34080 3 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'] |
nobody |
3-23707 3 days ago |
3-23761 3 days ago |
48-39153 48 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 |
3-9372 3 days ago |
13-54608 13 days ago |
14-35975 14 days |
| 33589 |
JovanGerb author:JovanGerb |
chore(Lean/Meta/RefinedDiscrTree/Basic): remove `privateInPublic` |
This PR fixes cases of `privateInPublic` in the `RefinedDiscrTree` code. The offending pattern is that an instance is defined using a private definition. The solution is to not mark that definition as private.
Also avoid a use of `nonrec`
---
[](https://gitpod.io/from-referrer/)
|
t-meta |
13/24 |
Mathlib/Lean/Meta/RefinedDiscrTree/Basic.lean |
1 |
1 |
['github-actions'] |
nobody |
3-2121 3 days ago |
3-14613 3 days ago |
3-14650 3 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'] |
nobody |
2-82673 2 days ago |
2-86321 2 days ago |
2-86323 2 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 |
2-77777 2 days ago |
3-1838 3 days ago |
3-1879 3 days |
| 33607 |
xgenereux author:xgenereux |
feat: primeSpectrum_eq_of_KrullDimLEOne |
Given a local ring `R` which is also a domain with `Ring.KrullDimLE 1 R` (or equivalently `Ring.DimensionLEOne`) a prime is either `⊥` or`⊤`.
The application I have in mind is `IsDiscreteValuationRing R`.
---
[](https://gitpod.io/from-referrer/)
|
t-ring-theory |
13/0 |
Mathlib/RingTheory/Spectrum/Prime/Topology.lean |
1 |
1 |
['github-actions'] |
nobody |
2-73307 2 days ago |
2-73307 2 days ago |
2-73352 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/)
|
|
89/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-73092 2 days ago |
9-4574 9 days ago |
9-4547 9 days |
| 32812 |
harahu author:harahu |
doc(Geometry): fix typos |
Typos found and fixed by Codex.
---
[](https://gitpod.io/from-referrer/)
|
|
17/17 |
Mathlib/Geometry/Euclidean/MongePoint.lean,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 |
8 |
3 |
['github-actions', 'mathlib4-merge-conflict-bot'] |
nobody |
2-72356 2 days ago |
2-72390 2 days ago |
24-1446 24 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 |
4/14 |
Mathlib/Geometry/Euclidean/SignedDist.lean |
1 |
3 |
['JovanGerb', 'github-actions', 'vihdzp'] |
nobody |
2-67392 2 days ago |
3-15513 3 days ago |
3-15549 3 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 |
2-62651 2 days ago |
5-64521 5 days ago |
5-64496 5 days |
| 33609 |
xgenereux author:xgenereux |
refactor: Ideal.bot_prime as an instance |
---
[](https://gitpod.io/from-referrer/)
|
t-ring-theory |
14/18 |
Mathlib/Algebra/Order/Ring/Ordering/Basic.lean,Mathlib/RingTheory/DedekindDomain/Ideal/Lemmas.lean,Mathlib/RingTheory/Ideal/GoingUp.lean,Mathlib/RingTheory/Ideal/Maps.lean,Mathlib/RingTheory/Ideal/Maximal.lean,Mathlib/RingTheory/Ideal/MinimalPrime/Basic.lean,Mathlib/RingTheory/Ideal/NatInt.lean,Mathlib/RingTheory/Ideal/Prime.lean,Mathlib/RingTheory/Jacobson/Ring.lean,Mathlib/RingTheory/KrullDimension/Basic.lean,Mathlib/RingTheory/KrullDimension/Zero.lean,Mathlib/RingTheory/LocalRing/ResidueField/Fiber.lean,Mathlib/RingTheory/Localization/Ideal.lean,Mathlib/RingTheory/Spectrum/Prime/Basic.lean,Mathlib/RingTheory/Spectrum/Prime/Topology.lean |
15 |
5 |
['github-actions', 'leanprover-radar', 'vihdzp', 'xgenereux'] |
nobody |
2-61897 2 days ago |
2-61955 2 days ago |
2-61936 2 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 |
2-60831 2 days ago |
2-60859 2 days ago |
19-65938 19 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 |
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 |
5 |
['github-actions', 'harahu', 'joelriou'] |
nobody |
2-60534 2 days ago |
2-60551 2 days ago |
4-50316 4 days |
| 33620 |
harahu author:harahu |
doc(Algebra): fix file refs |
Update some stale file references.
---
[](https://gitpod.io/from-referrer/)
|
t-algebra label:t-algebra$ |
9/7 |
Mathlib/Algebra/Group/Subsemigroup/Operations.lean,Mathlib/Algebra/Group/Units/Defs.lean,Mathlib/Algebra/HierarchyDesign.lean,Mathlib/Algebra/Module/Presentation/Differentials.lean,Mathlib/Algebra/Ring/Action/End.lean |
5 |
1 |
['github-actions'] |
nobody |
2-59517 2 days ago |
2-61214 2 days ago |
2-61257 2 days |
| 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 |
10/0 |
Mathlib/RingTheory/Valuation/ValuationSubring.lean |
1 |
5 |
['github-actions', 'vihdzp', 'xgenereux'] |
nobody |
2-57163 2 days ago |
2-70682 2 days ago |
2-70720 2 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 |
2-46339 2 days ago |
2-70877 2 days ago |
62-23675 62 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 |
2-43898 2 days ago |
6-74831 6 days ago |
6-74868 6 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'] |
RemyDegenne assignee:RemyDegenne |
2-43895 2 days ago |
6-38706 6 days ago |
6-38686 6 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 |
2-43893 2 days ago |
5-76742 5 days ago |
5-76781 5 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 |
2-43892 2 days ago |
5-47943 5 days ago |
5-47929 5 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'] |
nobody |
2-40284 2 days ago |
2-41613 2 days ago |
2-41646 2 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'] |
nobody |
2-27701 2 days ago |
2-34016 2 days ago |
2-35494 2 days |
| 33584 |
kim-em author:kim-em |
fix(Tactic/TacticAnalysis): analyze tactics inside `have ... := by ...` |
This PR fixes TacticAnalysis to correctly process tactics inside term-level `by` blocks such as `have h := by ...`. Previously, these tactics were missed.
The fix is simple: move the sequencing operator check before the `.original` head info check. This is needed because the `tacticSeq` nodes inside `have := by` have synthetic source info rather than `.original`.
See: https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/TacticAnalysis.20ignores.20tactics.20in.20have/near/565486129
🤖 Prepared with Claude Code |
t-meta |
41/7 |
Mathlib/Tactic/TacticAnalysis.lean,MathlibTest/TacticAnalysis.lean |
2 |
50 |
['Vierkantor', 'adomani', 'github-actions', 'kim-em'] |
nobody |
2-26379 2 days ago |
2-26379 2 days ago |
2-46260 2 days |
| 31706 |
Thmoas-Guan author:Thmoas-Guan |
feat(Algebra/ModuleCat): `ModuleCat.uliftFunctor` |
Add `ModuleCat.uliftFunctor`
---
[](https://gitpod.io/from-referrer/)
|
t-algebra label:t-algebra$ |
108/0 |
Mathlib.lean,Mathlib/Algebra/Category/ModuleCat/Ulift.lean |
2 |
15 |
['Thmoas-Guan', 'dagurtomas', 'erdOne', 'github-actions', 'mathlib4-merge-conflict-bot', 'robin-carlier'] |
mattrobball assignee:mattrobball |
2-23202 2 days ago |
10-79855 10 days ago |
21-73567 21 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'] |
nobody |
2-22239 2 days ago |
2-22241 2 days ago |
2-22277 2 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 |
2-20712 2 days ago |
2-22432 2 days ago |
46-26868 46 days |
| 33654 |
vihdzp author:vihdzp |
chore: `LinearOrderedCommMonoidWithZero` extends `ZeroLEOneClass` |
We also remove a duplicate `ZeroLEOneClass` instance on `CanonicallyOrderedAdd`.
---
[](https://gitpod.io/from-referrer/)
|
t-algebra label:t-algebra$ |
2/12 |
Mathlib/Algebra/Order/GroupWithZero/Canonical.lean |
1 |
3 |
['github-actions', 'leanprover-radar', 'vihdzp'] |
nobody |
2-16470 2 days ago |
2-18009 2 days ago |
2-24450 2 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/) |
merge-conflict
t-category-theory
|
409/3 |
Mathlib.lean,Mathlib/Algebra/Homology/DerivedCategory/ExactFunctor.lean,Mathlib/Algebra/Homology/DerivedCategory/Ext/Map.lean,Mathlib/Algebra/Homology/DerivedCategory/ShortExact.lean,Mathlib/Algebra/Homology/HomotopyCategory.lean,Mathlib/Algebra/Homology/HomotopyCategory/Pretriangulated.lean,Mathlib/Algebra/Homology/HomotopyCategory/ShortExact.lean,Mathlib/Algebra/Homology/HomotopyCategory/SingleFunctors.lean,Mathlib/CategoryTheory/Linear/LinearFunctor.lean,Mathlib/CategoryTheory/Shift/CommShift.lean,Mathlib/CategoryTheory/Shift/ShiftedHom.lean |
11 |
7 |
['Thmoas-Guan', 'github-actions', 'joelriou', 'mathlib4-dependent-issues-bot', 'mathlib4-merge-conflict-bot'] |
eric-wieser assignee:eric-wieser |
2-76364 2 days ago |
2-76365 2 days ago |
4-3344 4 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'] |
nobody |
2-11639 2 days ago |
2-14216 2 days ago |
2-14198 2 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 |
2-6081 2 days ago |
38-4045 1 month ago |
47-48793 47 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 |
2-4563 2 days ago |
10-10263 10 days ago |
10-36053 10 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 |
1-85412 1 day ago |
1-86334 1 day ago |
22-82076 22 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 |
1-83590 1 day ago |
4-465 4 days ago |
8-2145 8 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 |
1-79411 1 day ago |
3-2385 3 days ago |
3-2910 3 days |
| 33606 |
ScottCarnahan author:ScottCarnahan |
feat(Algebra/Lie): basics of loop algebras |
This PR introduces the Lie algebra of polynomial loops in a base Lie algebra, together with the 2-cochain induced by a symmetric bilinear form on the base Lie algebra.
---
I am a bit dissatisfied with the restriction of `twoCochain_of_Bilinear` to integers, but I couldn't find a good substitute for `Int.natAbs` that joined elements with their negatives.
[](https://gitpod.io/from-referrer/)
|
t-algebra label:t-algebra$ |
206/1 |
Mathlib.lean,Mathlib/Algebra/BigOperators/Finprod.lean,Mathlib/Algebra/Lie/BaseChange.lean,Mathlib/Algebra/Lie/Extension.lean,Mathlib/Algebra/Lie/Loop.lean |
5 |
1 |
['github-actions'] |
ocfnash assignee:ocfnash |
1-76734 1 day ago |
2-74888 2 days ago |
2-74921 2 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 |
6 |
['github-actions', 'mathlib4-dependent-issues-bot', 'mathlib4-merge-conflict-bot'] |
dwrensha, kmill, thorimur assignee:kmill assignee:dwrensha assignee:thorimur |
20-48445 20 days ago |
20-48669 20 days ago |
28-52525 28 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'] |
nobody |
1-69090 1 day ago |
1-70889 1 day ago |
1-70862 1 day |
| 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 |
1-65562 1 day ago |
1-66181 1 day ago |
13-39451 13 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'] |
nobody |
1-64079 1 day ago |
1-64098 1 day ago |
8-1062 8 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
|
312/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 |
9 |
['github-actions', 'grunweg', 'mathlib4-dependent-issues-bot', 'mathlib4-merge-conflict-bot', 'sgouezel'] |
sgouezel assignee:sgouezel |
1-63884 1 day ago |
1-66026 1 day ago |
101-84992 101 days |
| 33656 |
metakunt author:metakunt |
feat(Data/Nat/Choose): Add sum_range_multichoose |
|
t-data |
11/0 |
Mathlib/Data/Nat/Choose/Sum.lean |
1 |
5 |
['eric-wieser', 'github-actions', 'metakunt'] |
nobody |
1-60356 1 day ago |
2-22735 2 days ago |
2-22777 2 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'] |
nobody |
1-60092 1 day ago |
2-52189 2 days ago |
2-52169 2 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 |
1 |
['github-actions'] |
nobody |
1-58147 1 day ago |
1-58147 1 day ago |
1-58133 1 day |
| 33216 |
stepan2698-cpu author:stepan2698-cpu |
feat: Schur's lemma over an algebraically closed field |
Adds a new file with facts about algebra representations. Proves Schur's lemma (any endomorphism of an algebra representation over an algebraically closed field is scalar) and proves that every finite-dimensional representation of a commutative algebra over an algebraically closed field is one-dimensional.
---
[](https://gitpod.io/from-referrer/)
|
t-algebra
new-contributor
label:t-algebra$ |
80/0 |
Mathlib.lean,Mathlib/RepresentationTheory/AlgebraRepresentation/Basic.lean |
2 |
6 |
['copilot-pull-request-reviewer', 'github-actions'] |
riccardobrasca assignee:riccardobrasca |
1-56606 1 day ago |
16-34389 16 days ago |
16-34426 16 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 |
21 |
['Whysoserioushah', 'erdOne', 'github-actions', 'stepan2698-cpu'] |
kim-em assignee:kim-em |
1-56577 1 day ago |
25-55329 25 days ago |
25-55363 25 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 |
21/1 |
Mathlib/Analysis/Matrix/Order.lean,Mathlib/Data/Real/Sqrt.lean |
2 |
3 |
['github-actions', 'themathqueen'] |
nobody |
1-54958 1 day ago |
2-46840 2 days ago |
2-46882 2 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'] |
nobody |
1-49044 1 day ago |
1-82471 1 day ago |
1-82512 1 day |
| 33358 |
joelriou author:joelriou |
feat(Algebra/Homology): functoriality of `ProjectiveResolution.extMk` |
Given a fixed projective (resp. injective) resolution `R`, we obtain the functoriality of the constructor `R.extMk`.
---
- [x] depends on: #32816
[](https://gitpod.io/from-referrer/)
|
t-category-theory |
126/8 |
Mathlib/Algebra/Homology/HomotopyCategory/HomComplex.lean,Mathlib/Algebra/Homology/HomotopyCategory/HomComplexShift.lean,Mathlib/Algebra/Homology/HomotopyCategory/HomComplexSingle.lean,Mathlib/CategoryTheory/Abelian/Injective/Ext.lean,Mathlib/CategoryTheory/Abelian/Projective/Ext.lean |
5 |
5 |
['github-actions', 'joelriou', 'mathlib4-dependent-issues-bot', 'mathlib4-merge-conflict-bot', 'robin-carlier'] |
nobody |
4-83893 4 days ago |
4-83893 4 days ago |
5-13400 5 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 |
1-43894 1 day ago |
4-59556 4 days ago |
5-25956 5 days |
| 33518 |
joelriou author:joelriou |
feat(CategoryTheory/Sites): fullness of `DescentData.pullFunctor` |
Let `F` be a prestack for a Grothendieck topology `J`, `f : X i ⟶ S` and `f' : X' j ⟶ S` be two families of morphisms.
Assume that `f'` is a covering family for `J`, then functors `F.pullFunctor .. : F.DescentData f ⥤ F.DescentData f'` are full.
(They are also faithful, but this shall be done in a separate PR #33256 where we also deduce characterizations of (pre)stacks for pretopologies.)
---
[](https://gitpod.io/from-referrer/)
|
t-category-theory |
269/0 |
Mathlib.lean,Mathlib/CategoryTheory/Sites/Descent/Precoverage.lean |
2 |
2 |
['github-actions', 'joelriou'] |
jcommelin assignee:jcommelin |
1-43889 1 day ago |
5-14268 5 days ago |
5-14241 5 days |
| 33524 |
ldct author:ldct |
fix: Rename constructors in Irrational.lean docstrings |
The old names have been deprecated and removed from the codebase, but the docstring still refers to them.
---
[](https://gitpod.io/from-referrer/)
|
t-number-theory |
1/1 |
Mathlib/NumberTheory/Real/Irrational.lean |
1 |
1 |
['github-actions', 'vihdzp'] |
riccardobrasca assignee:riccardobrasca |
1-43888 1 day ago |
4-75540 4 days ago |
4-75573 4 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 |
|
5/2 |
Mathlib/Analysis/Normed/Module/Basic.lean,Mathlib/Topology/Algebra/Module/ClosedSubmodule.lean |
2 |
2 |
['github-actions'] |
nobody |
1-42374 1 day ago |
1-44358 1 day ago |
1-44331 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'] |
nobody |
1-42257 1 day ago |
1-62710 1 day ago |
1-62703 1 day |
| 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 |
61/62 |
Mathlib/RingTheory/Valuation/ValuativeRel/Basic.lean,Mathlib/RingTheory/Valuation/ValuativeRel/Trivial.lean |
2 |
2 |
['JovanGerb', 'github-actions'] |
nobody |
1-41565 1 day ago |
2-18123 2 days ago |
2-18157 2 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'] |
adamtopaz assignee:adamtopaz |
1-41258 1 day ago |
1-41258 1 day ago |
5-37612 5 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` |
|
169/8 |
Mathlib/Analysis/Convex/Cone/Basic.lean,Mathlib/Analysis/Convex/Cone/Dual.lean,Mathlib/Analysis/InnerProductSpace/Orthogonal.lean,Mathlib/Topology/Algebra/Module/ClosedSubmodule.lean |
4 |
9 |
['github-actions', 'mathlib4-dependent-issues-bot', 'mathlib4-merge-conflict-bot', 'sgouezel', 'yoh-tanimoto'] |
sgouezel assignee:sgouezel |
1-41108 1 day ago |
1-47493 1 day ago |
14-35423 14 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'] |
nobody |
1-25681 1 day ago |
1-25712 1 day ago |
2-69029 2 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'] |
nobody |
1-22965 1 day ago |
1-67272 1 day ago |
1-67309 1 day |
| 33603 |
JovanGerb author:JovanGerb |
fix(translate): don't unfold aux lemmas, but translate them |
`to_additive` has some troublesome interactions with the module system, because it sometimes relies on unfolding theorems whose value is not exported. This PR fixes that by never unfolding these theorems, and instead creating their translation the first time they appear.
This will help remove some instances of `import all` and instances of `proofsInPublic`.
The only theorems that we still unfold are the auxiliary theorems created by `simp`. These have very small proofs, and these proofs are always exported, so it is fine to unfold them.
---
[](https://gitpod.io/from-referrer/)
|
t-meta |
42/64 |
Mathlib/Lean/Name.lean,Mathlib/MeasureTheory/Function/LpSpace/DomAct/Continuous.lean,Mathlib/Tactic/Translate/Core.lean,MathlibTest/toAdditive.lean |
4 |
2 |
['github-actions', 'mathlib4-merge-conflict-bot'] |
nobody |
1-22411 1 day ago |
1-22430 1 day ago |
2-75250 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 |
5 |
['github-actions', 'mathlib4-merge-conflict-bot', 'vihdzp'] |
bryangingechen assignee:bryangingechen |
1-22345 1 day ago |
1-22363 1 day ago |
14-20359 14 days |
| 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 |
1 |
['github-actions'] |
nobody |
1-17353 1 day ago |
1-17353 1 day ago |
2-2819 2 days |
| 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'] |
nobody |
1-16178 1 day ago |
unknown |
unknown |
| 33666 |
JovanGerb author:JovanGerb |
chore(Tactic): remove duplicate instances |
This PR removes the two duplicate instances that were detected in `Mathlib.Tactic`.
---
[](https://gitpod.io/from-referrer/)
|
t-meta
maintainer-merge
|
30/57 |
Mathlib/Tactic/Linarith/Oracle/FourierMotzkin.lean,Mathlib/Tactic/NormNum/Basic.lean,Mathlib/Tactic/NormNum/Core.lean,Mathlib/Tactic/NormNum/GCD.lean,Mathlib/Tactic/NormNum/NatFactorial.lean,Mathlib/Tactic/NormNum/NatFib.lean,Mathlib/Tactic/NormNum/NatLog.lean,Mathlib/Tactic/NormNum/NatSqrt.lean,Mathlib/Tactic/NormNum/Pow.lean,Mathlib/Tactic/NormNum/Prime.lean,Mathlib/Tactic/NormNum/Result.lean,Mathlib/Tactic/ReduceModChar.lean |
12 |
5 |
['github-actions', 'grunweg', 'leanprover-radar'] |
nobody |
1-14247 1 day ago |
1-16602 1 day ago |
2-1892 2 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'] |
nobody |
1-7430 1 day ago |
1-8218 1 day ago |
1-8201 1 day |
| 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 |
1-2520 1 day ago |
1-2520 1 day ago |
33-38818 33 days |
| 33614 |
eric-wieser author:eric-wieser |
chore: tidy results around Module.Finite |
In particular this replaces many chains of `Module.finite_def` and `Submodule.fg_top` with `Module.Finite.iff_fg`.
This also golfs some `FiniteDimensional` results in terms of their `Finite` counterparts, and adds `Submodule.fg_range` as a shorthand for a common case of `Submodule.fg_map`.
---
[](https://gitpod.io/from-referrer/)
|
t-ring-theory |
50/53 |
Mathlib/Algebra/Module/FinitePresentation.lean,Mathlib/Analysis/Normed/Module/FiniteDimension.lean,Mathlib/LinearAlgebra/FiniteDimensional/Basic.lean,Mathlib/LinearAlgebra/FiniteDimensional/Defs.lean,Mathlib/RingTheory/Finiteness/Basic.lean,Mathlib/RingTheory/FractionalIdeal/Basic.lean,Mathlib/RingTheory/IntegralClosure/Algebra/Basic.lean,Mathlib/RingTheory/IntegralClosure/IsIntegral/AlmostIntegral.lean,Mathlib/RingTheory/IntegralClosure/IsIntegralClosure/Basic.lean,Mathlib/RingTheory/LocalRing/Module.lean,Mathlib/RingTheory/Noetherian/Defs.lean,Mathlib/RingTheory/Smooth/Local.lean |
12 |
1 |
['github-actions'] |
nobody |
1-2022 1 day ago |
2-8868 2 days ago |
2-68374 2 days |
| 33604 |
xgenereux author:xgenereux |
feat(ValuationSubring): eq_top_iff + qol changes |
Given a `A : ValuationSubring K`, this PR adds the lemma `eq_top_iff : A = ⊤ ↔ ¬ A.valuation.IsNontrivial`.
I have also made some small quality of life changes:
1. Added other forms of the basic rewrite lemmas with `Valuation.IsEquiv`:
- `eq_zero`
- `one_le_iff_one_le`
- ~~`neq_one_iff_neq_one`~~
- `one_lt_iff_one_lt`
- removed : `ne_zero`
2. Reorganized section following the `IsEquiv` namespace block in Valuation.Basic
3. Added lemmas `(h : v.IsEquiv v') : v.IsNontrivial ↔ v'.IsNontrivial`
- `isNontrivial_of_isEquiv`
- `isNontrivial_iff_isEquiv_isNontrivial`
4. Added simp tags
5. Added simp lemmas
- `isNontrivial_valuationSubring_valuation_iff`
---
[](https://gitpod.io/from-referrer/)
|
t-ring-theory |
69/38 |
Mathlib/NumberTheory/Padics/ValuativeRel.lean,Mathlib/RingTheory/Valuation/Basic.lean,Mathlib/RingTheory/Valuation/ValuationSubring.lean,Mathlib/RingTheory/Valuation/ValuativeRel/Basic.lean,Mathlib/Topology/Algebra/Valued/WithVal.lean |
5 |
18 |
['github-actions', 'mathlib4-merge-conflict-bot', 'vihdzp', 'xgenereux'] |
nobody |
1-631 1 day ago |
1-650 1 day ago |
2-50470 2 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`
Declaration: AI tools used for debugging/facilitating peripheral commands (e.g. bash commands), docstrings, refactoring and condensing existing formalization. I welcome reviews on humanizing doctrings. Personally speaking, AI does a better job at writing those than what I can do. My brain isn't in the right condition to write human language after coding and debugging for hours and hours. The philosophy of me using AI tools is "hey gather information/spot patterns for me", other than "give me the answer".
|
t-analysis
new-contributor
|
489/0 |
Mathlib.lean,Mathlib/Analysis/DiscreteConvolution/Basic.lean |
2 |
11 |
['IlPreteRosso', 'github-actions', 'j-loreaux'] |
urkud assignee:urkud |
0-83126 23 hours ago |
1-26124 1 day ago |
8-20494 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-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-82976 23 hours ago |
5-64368 5 days ago |
5-64355 5 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$$.
---
- [ ] depends on: #31138
- [ ]
[](https://gitpod.io/from-referrer/)
|
|
255/0 |
Mathlib/LinearAlgebra/Determinant.lean,Mathlib/LinearAlgebra/Transvection.lean |
2 |
n/a |
['AntoineChambert-Loir', 'github-actions', 'mathlib4-dependent-issues-bot', 'mathlib4-merge-conflict-bot'] |
nobody |
0-82026 22 hours ago |
unknown |
unknown |
| 33718 |
erdOne author:erdOne |
feat(RingTheory): predicate for `QuasiFiniteAt` |
---
[](https://gitpod.io/from-referrer/)
|
t-ring-theory |
194/24 |
Mathlib/RingTheory/Etale/QuasiFinite.lean,Mathlib/RingTheory/LocalRing/ResidueField/Ideal.lean,Mathlib/RingTheory/Localization/AtPrime/Basic.lean,Mathlib/RingTheory/QuasiFinite/Basic.lean |
4 |
1 |
['github-actions'] |
nobody |
0-78984 21 hours ago |
0-78984 21 hours ago |
0-79027 21 hours |
| 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 |
0-78089 21 hours ago |
17-6553 17 days ago |
17-6589 17 days |
| 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 |
43 |
['Ruben-VandeVelde', 'Whysoserioushah', 'eric-wieser', 'github-actions', 'kckennylau', 'mathlib4-merge-conflict-bot', 'vlad902'] |
kbuzzard assignee:kbuzzard |
0-72166 20 hours ago |
4-66907 4 days ago |
4-74492 4 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 |
0-71388 19 hours ago |
23-68542 23 days ago |
26-55502 26 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'] |
nobody |
0-69362 19 hours ago |
0-69433 19 hours ago |
1-39387 1 day |
| 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'] |
nobody |
0-63957 17 hours ago |
0-63997 17 hours ago |
12-24532 12 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 |
0-55840 15 hours ago |
17-5242 17 days ago |
17-5289 17 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'] |
nobody |
0-54432 15 hours ago |
1-63788 1 day ago |
1-63825 1 day |
| 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'] |
nobody |
0-53152 14 hours ago |
1-52943 1 day ago |
1-52977 1 day |
| 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
|
756/0 |
Mathlib.lean,Mathlib/Dynamics/SymbolicDynamics/Basic.lean,Mathlib/Tactic/Translate/ToAdditive.lean |
3 |
156 |
['Sfgangloff', 'eric-wieser', 'github-actions', 'kckennylau', 'mathlib4-merge-conflict-bot', 'sgouezel'] |
sgouezel assignee:sgouezel |
0-52560 14 hours ago |
1-24014 1 day ago |
87-32910 87 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'] |
nobody |
0-52429 14 hours ago |
1-32808 1 day ago |
1-32841 1 day |
| 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 deprecates `AddMonoidHom.smulLeft` (same situation)
---
- [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'] |
nobody |
0-52232 14 hours ago |
0-52232 14 hours ago |
0-52206 14 hours |
| 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 |
0-51327 14 hours ago |
0-51347 14 hours ago |
4-1868 4 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'] |
nobody |
0-48755 13 hours ago |
0-50722 14 hours ago |
0-56489 15 hours |
| 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'] |
nobody |
0-47037 13 hours ago |
1-40094 1 day ago |
1-40128 1 day |
| 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 |
0-45380 12 hours ago |
4-71466 4 days ago |
7-76218 7 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 |
0-44445 12 hours ago |
0-44514 12 hours ago |
2-50778 2 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 |
0-43909 12 hours ago |
3-56160 3 days ago |
4-47755 4 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 |
0-43907 12 hours ago |
4-31672 4 days ago |
5-14936 5 days |
| 32481 |
ADedecker author:ADedecker |
feat: add `PolynormableSpace.banach_steinhaus` |
---
- [ ] depends on: #32480
[](https://gitpod.io/from-referrer/)
|
blocked-by-other-PR
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'] |
nobody |
33-68973 1 month ago |
33-71044 1 month ago |
0-1302 21 minutes |
| 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'] |
RemyDegenne assignee:RemyDegenne |
0-43905 12 hours ago |
0-67726 18 hours ago |
0-69196 19 hours |
| 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 |
0-43903 12 hours ago |
3-83362 3 days ago |
4-2825 4 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 |
0-43902 12 hours ago |
3-58848 3 days ago |
6-49124 6 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 |
7 |
['YuvalFilmus', 'erdOne', 'github-actions', 'metakunt', 'michelsol'] |
nobody |
3-65854 3 days ago |
3-65855 3 days ago |
4-58721 4 days |
| 33532 |
vihdzp author:vihdzp |
feat(RingTheory/Valuation/ValuativeRel): introduce `=ᵥ` relation |
Of course, the characterizing property is that for any compatible valuation, `x =ᵥ y` is equivalent to `v x = v y`.
---
I haven't yet introduced too much API. I'll be using this on the CGT repo in order to define a `ValuativeRel Surreal` instance compatible with `ArchimedeanClass.mk`. If there's any API I'm missing, I'll upstream it in a subsequent PR.
[](https://gitpod.io/from-referrer/)
|
t-ring-theory |
67/14 |
Mathlib/RingTheory/Valuation/ValuativeRel/Basic.lean |
1 |
2 |
['github-actions', 'vihdzp'] |
erdOne assignee:erdOne |
0-43900 12 hours ago |
4-44888 4 days ago |
4-44872 4 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$ |
159/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 |
1 |
['github-actions'] |
eric-wieser assignee:eric-wieser |
0-43899 12 hours ago |
4-33970 4 days ago |
4-34008 4 days |
| 33539 |
BryceT233 author:BryceT233 |
feat(RingTheory/MvPolynomial): powers of ideal of variables |
proved some helper results for powers of the ideal of variables in `MvPolynomial`
---
[](https://gitpod.io/from-referrer/)
|
new-contributor
t-ring-theory
|
98/1 |
Mathlib/RingTheory/MvPolynomial/Ideal.lean |
1 |
8 |
['BryceT233', 'erdOne', 'github-actions', 'vihdzp'] |
erdOne assignee:erdOne |
0-43898 12 hours ago |
4-19311 4 days ago |
4-19343 4 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 |
0-43897 12 hours ago |
4-12309 4 days ago |
4-12291 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 |
2 |
['erdOne', 'github-actions'] |
robin-carlier assignee:robin-carlier |
0-43895 12 hours ago |
3-64985 3 days ago |
3-65019 3 days |
| 33562 |
kim-em author:kim-em |
feat(ConvexSpace): complete `proof_wanted` statements |
This PR proves the three `proof_wanted` statements for `convexComboPair`:
- `convexComboPair_zero`: weight 0 on first point gives the second point
- `convexComboPair_one`: weight 1 on first point gives the first point
- `convexComboPair_same`: any convex combo of a point with itself is that point
Also adds supporting lemmas:
- `StdSimplex.ext`: extensionality lemma for `StdSimplex`
- `StdSimplex.mk_single`: simp lemma for constructor applied to single
- `@[simp]` attribute on `ConvexSpace.single`
🤖 Prepared with Claude Code |
t-algebra label:t-algebra$ |
24/7 |
Mathlib/LinearAlgebra/ConvexSpace.lean |
1 |
3 |
['github-actions', 'kim-em', 'themathqueen'] |
riccardobrasca assignee:riccardobrasca |
0-43894 12 hours ago |
3-47223 3 days ago |
3-47263 3 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 |
31 |
['artie2000', 'github-actions', 'vihdzp'] |
nobody |
0-42419 11 hours ago |
0-46467 12 hours ago |
1-16057 1 day |
| 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 |
69/69 |
Mathlib/Combinatorics/SimpleGraph/Acyclic.lean,Mathlib/Combinatorics/SimpleGraph/Connectivity/Connected.lean |
2 |
4 |
['github-actions', 'mathlib4-dependent-issues-bot', 'mathlib4-merge-conflict-bot'] |
b-mehta assignee:b-mehta |
0-40614 11 hours ago |
0-40634 11 hours ago |
30-2311 30 days |
| 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
|
160/0 |
Mathlib.lean,Mathlib/Combinatorics/SimpleGraph/Connectivity/VertexConnectivity.lean,Mathlib/Combinatorics/SimpleGraph/IsolateVerts.lean |
3 |
87 |
['0xTerencePrime', 'SnirBroshi', 'github-actions', 'vihdzp'] |
nobody |
0-72011 20 hours ago |
11-3330 11 days ago |
11-3362 11 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 |
0-38045 10 hours ago |
0-38106 10 hours ago |
10-73281 10 days |
| 29960 |
yonggyuchoimath author:yonggyuchoimath |
feat(Algebra/Category/Ring): equalizers of pushout maps of tensor product inclusions |
This PR defines a ring map `S →ₗ[R] S ⊗[R] S : s ↦ (s ⊗ₜ[R] 1) - (1 ⊗ₜ[R] s)` for an `R`-algebra `S`, and show that its kernel is exactly (the image of) `R` if `S` is faithfully flat over `R`.
Changes:
* `TensorProduct.AlgebraTensorModule.distribBaseChange`: Origianlly takes `M` and `N`, where `M` is an `R`-module with an additional instance `IsScalarTower R A M`. This is unnecessary, so I changed the `M` and `N` into `N` and `Q`, now both of which are merely modules over `R`.
Main results :
* Add compatibility of `Algebra.TensorProduct.includeLeft` (or `Algebra.TensorProduct.includeRight`) with `TensorProduct.AlgebraTensorModule.distribBaseChange` and `LinearMap.lTensor`
* Define `Algebra.TensorProduct.includeLeftSubRight`, which is the `R`-linear map `S →ₗ[R] S ⊗[R] S` sending `s : S` to `(s ⊗ₜ[R] 1) - (1 ⊗ₜ[R] s)`.
* `Algebra.isEffective_of_faithfullyFlat`: the pair `algebraMap : R → S` and `includeLeftSubRight R S : S → S ⊗[R] S` is exact if `S` is a faithfully flat `R`-algebra.
---
- [x] depends on: #30806 |
new-contributor
t-ring-theory
|
214/1 |
Mathlib.lean,Mathlib/LinearAlgebra/TensorProduct/Tower.lean,Mathlib/RingTheory/TensorProduct/IncludeLeftSubRight.lean,Mathlib/RingTheory/TensorProduct/Maps.lean |
4 |
20 |
['erdOne', 'github-actions', 'mathlib4-dependent-issues-bot', 'mathlib4-merge-conflict-bot', 'yonggyuchoimath'] |
PatrickMassot and erdOne assignee:PatrickMassot assignee:erdOne |
0-36773 10 hours ago |
0-36773 10 hours ago |
54-69317 54 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'] |
nobody |
0-33214 9 hours ago |
2-49544 2 days ago |
2-49587 2 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 |
163/22 |
Mathlib/Tactic/Choose.lean,MathlibTest/choose.lean |
2 |
20 |
['AlexKontorovich', 'eric-wieser', 'fpvandoorn', 'github-actions', 'kim-em'] |
joneugster assignee:joneugster |
1-12278 1 day ago |
19-54709 19 days ago |
20-39107 20 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
|
124/4 |
Mathlib/Algebra/Polynomial/Roots.lean,Mathlib/Analysis/Complex/CoveringMap.lean,Mathlib/Topology/Algebra/Polynomial.lean,Mathlib/Topology/Covering/Basic.lean |
4 |
2 |
['alreadydone', 'github-actions'] |
nobody |
0-13178 3 hours ago |
0-51828 14 hours ago |
0-51871 14 hours |
| 33704 |
kebekus author:kebekus |
feat: behavior under addition of the characteristic function of Value Distribution Theory |
Combine results of PR #32311 and #31556 to establish the behavior under addition of the characteristic function of Value Distribution Theory.
This material is used in [Project VD](https://github.com/kebekus/ProjectVD), formalizing Value Distribution Theory for meromorphic functions on the complex plane. The formula established here is part of a larger package discussing the behavior of the Nenvanlinna height under algebraic manipulations of the functions.
---
[](https://gitpod.io/from-referrer/)
|
t-analysis |
61/2 |
Mathlib/Analysis/Complex/ValueDistribution/CharacteristicFunction.lean |
1 |
11 |
['github-actions', 'j-loreaux', 'kebekus'] |
nobody |
0-12400 3 hours ago |
1-17454 1 day ago |
1-18392 1 day |
| 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-43900 12 hours ago |
5-29684 5 days ago |
5-29722 5 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 |
1 |
['github-actions'] |
nobody |
0-11802 3 hours ago |
0-11802 3 hours ago |
0-84085 23 hours |
| 33744 |
bilichboris author:bilichboris |
feat(RingTheory): Class Group of a Unique Factorization Domain is trivial |
Add a theorem that the class group of a unique factorization domain is trivial.
Together with the PR relating `ClassGroup` to `PicardGroup`, this will close a TODO in `Mathlib.RingTheory.PicardGroup` that the Picard Group of a UFD is trivial.
---
[](https://gitpod.io/from-referrer/)
|
new-contributor
t-ring-theory
|
712/0 |
Mathlib.lean,Mathlib/RingTheory/UniqueFactorizationDomain/ClassGroup.lean |
2 |
3 |
['github-actions', 'jcommelin'] |
nobody |
0-9484 2 hours ago |
0-14702 4 hours ago |
0-14743 4 hours |
| 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 |
163/7 |
Mathlib/Combinatorics/SimpleGraph/CompleteMultipartite.lean |
1 |
33 |
['YaelDillies', 'b-mehta', 'github-actions', 'mathlib4-dependent-issues-bot', 'mathlib4-merge-conflict-bot', 'mitchell-horner'] |
YaelDillies assignee:YaelDillies |
0-73217 20 hours ago |
1-43358 1 day ago |
72-6170 72 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 |
0-4578 1 hour ago |
0-4578 1 hour ago |
0-4620 1 hour |
| 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 |
6/0 |
Mathlib/Data/Rat/Encodable.lean |
1 |
4 |
['eric-wieser', 'github-actions', 'grunweg', 'leanprover-radar'] |
nobody |
0-4794 1 hour ago |
0-4851 1 hour ago |
0-5603 1 hour |
| 30736 |
alreadydone author:alreadydone |
feat(RingTheory): Picard group of a domain is isomorphic to ClassGroup |
---
- [x] depends on: #30657
- [x] depends on: #33095
[](https://gitpod.io/from-referrer/)
|
large-import
t-ring-theory
|
310/79 |
Mathlib/RingTheory/PicardGroup.lean |
1 |
32 |
['alreadydone', 'erdOne', 'github-actions', 'jcommelin', 'mathlib4-dependent-issues-bot', 'mathlib4-merge-conflict-bot', 'tb65536'] |
mariainesdff assignee:mariainesdff |
0-2005 33 minutes ago |
3-52363 3 days ago |
46-81985 46 days |
| 30799 |
YaelDillies author:YaelDillies |
refactor: unify the two versions of `pow_eq_one_iff` |
One version is about torsion-free monoids, the other one about linearly ordered monoids. I argue that all linearly ordered monoids of interest are torsion-free, and therefore the correct lemma to keep is the former.
[Zulip](https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/Should.20linear.20ordered.20comm.20monoids.20with.20zero.20be.20torsion-free)
---
- [x] depends on: #30680
- [x] depends on: #31024
- [x] depends on: #31025
- [x] depends on: #31026
- [x] depends on: #31027
- [x] depends on: #31283
- [ ] depends on: #31749
[](https://gitpod.io/from-referrer/)
|
blocked-by-other-PR
t-algebra
large-import
file-removed
label:t-algebra$ |
265/358 |
Counterexamples.lean,Counterexamples/LinearOrderWithPosMulPosEqZero.lean,Mathlib/Algebra/Group/Torsion.lean,Mathlib/Algebra/GroupWithZero/Torsion.lean,Mathlib/Algebra/Order/AddGroupWithTop.lean,Mathlib/Algebra/Order/Field/Canonical.lean,Mathlib/Algebra/Order/GroupWithZero/Canonical.lean,Mathlib/Algebra/Order/Monoid/Unbundled/Pow.lean,Mathlib/Algebra/Order/Nonneg/Ring.lean,Mathlib/Algebra/Order/PUnit.lean,Mathlib/Algebra/Order/Ring/Archimedean.lean,Mathlib/Algebra/Order/Ring/Basic.lean,Mathlib/Algebra/Order/Ring/Nat.lean,Mathlib/Algebra/Order/Ring/StandardPart.lean,Mathlib/Algebra/Ring/NonZeroDivisors.lean,Mathlib/Algebra/Ring/Torsion.lean,Mathlib/Data/ENNReal/Basic.lean,Mathlib/Data/ENNReal/Real.lean,Mathlib/Data/EReal/Operations.lean,Mathlib/Data/Nat/PartENat.lean,Mathlib/Data/Nat/Prime/Pow.lean,Mathlib/FieldTheory/Finite/GaloisField.lean,Mathlib/LinearAlgebra/Dimension/Finite.lean,Mathlib/MeasureTheory/Function/ConditionalExpectation/Real.lean,Mathlib/MeasureTheory/Function/ConvergenceInMeasure.lean,Mathlib/MeasureTheory/Integral/Bochner/Basic.lean,Mathlib/MeasureTheory/Integral/Bochner/Set.lean,Mathlib/MeasureTheory/Integral/Lebesgue/Basic.lean,Mathlib/MeasureTheory/Measure/Decomposition/Exhaustion.lean,Mathlib/MeasureTheory/Measure/Doubling.lean,Mathlib/MeasureTheory/Measure/EverywherePos.lean,Mathlib/MeasureTheory/Measure/LevyProkhorovMetric.lean,Mathlib/MeasureTheory/Measure/TightNormed.lean,Mathlib/MeasureTheory/OuterMeasure/BorelCantelli.lean,Mathlib/NumberTheory/ArithmeticFunction/Moebius.lean,Mathlib/RingTheory/HahnSeries/Valuation.lean,Mathlib/RingTheory/Valuation/Archimedean.lean,Mathlib/RingTheory/Valuation/Basic.lean,Mathlib/RingTheory/Valuation/ValuationRing.lean,Mathlib/RingTheory/Valuation/ValuativeRel/Basic.lean,Mathlib/RingTheory/ZMod/UnitsCyclic.lean,Mathlib/SetTheory/Cardinal/Aleph.lean,Mathlib/SetTheory/Cardinal/Order.lean,Mathlib/Topology/EMetricSpace/BoundedVariation.lean,Mathlib/Topology/Instances/AddCircle/Defs.lean,Mathlib/Topology/MetricSpace/HolderNorm.lean,Mathlib/Topology/UnitInterval.lean |
47 |
19 |
['github-actions', 'mathlib4-dependent-issues-bot', 'mathlib4-merge-conflict-bot'] |
nobody |
8-1913 8 days ago |
9-18749 9 days ago |
0-10164 2 hours |
| 33723 |
erdOne author:erdOne |
feat(Analytic): `℘'(z)² = 4 ℘(z)³ - g₂ ℘(z) - g₃` |
---
[](https://gitpod.io/from-referrer/)
|
t-analysis |
386/13 |
Mathlib/Algebra/Module/ZLattice/Basic.lean,Mathlib/Algebra/Order/Floor/Ring.lean,Mathlib/Analysis/Analytic/Order.lean,Mathlib/Analysis/Calculus/ContDiff/Basic.lean,Mathlib/Analysis/Calculus/ContDiff/Operations.lean,Mathlib/Analysis/Calculus/IteratedDeriv/Lemmas.lean,Mathlib/Analysis/Meromorphic/Basic.lean,Mathlib/Analysis/Meromorphic/Order.lean,Mathlib/Analysis/SpecialFunctions/Elliptic/Weierstrass.lean |
9 |
32 |
['erdOne', 'github-actions', 'loefflerd', 'vihdzp'] |
nobody |
0-11717 3 hours ago |
0-40115 11 hours ago |
0-76056 21 hours |
| 32740 |
LTolDe author:LTolDe |
feat: add IsNowhereDense helpers |
add new lemmas to prove `IsNowhereDense s`
- IsNowhereDense.mono
- Topology.IsInducing.isNowhereDense_image
- IsNowhereDense.image_val
these lemmas will help to prove the **Effros Theorem**, see [zulip thread](https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/Effros.20Theorem/with/558712441)
---
[](https://gitpod.io/from-referrer/)
|
new-contributor
large-import
|
24/1 |
Mathlib/Topology/GDelta/Basic.lean |
1 |
7 |
['ADedecker', 'LTolDe', 'dupuisf', 'github-actions'] |
dupuisf assignee:dupuisf |
0-81071 22 hours ago |
27-76907 27 days ago |
27-76938 27 days |
| 33449 |
yuanyi-350 author:yuanyi-350 |
feat(ProbabilityTheory): Add Poisson limit theorem |
---
[](https://gitpod.io/from-referrer/)
|
t-measure-probability
large-import
|
102/5 |
Mathlib/Probability/Distributions/Poisson.lean,docs/1000.yaml |
2 |
4 |
['github-actions', 'vihdzp'] |
EtienneC30 assignee:EtienneC30 |
1-323 1 day ago |
7-22137 7 days ago |
7-22985 7 days |