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 |
39-35968 1 month ago |
42-71592 1 month ago |
44-72015 44 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 |
39-35958 1 month ago |
45-28268 1 month ago |
45-28308 45 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 |
38-35954 1 month ago |
42-26033 1 month ago |
42-28654 42 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 |
33-60119 1 month ago |
33-60238 1 month ago |
38-54667 38 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 |
33-44177 1 month ago |
39-47379 1 month ago |
39-50329 39 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 |
33-35960 1 month ago |
36-42291 1 month ago |
37-46888 37 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 |
32-84507 1 month ago |
32-84536 1 month ago |
33-5712 33 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 |
32-35959 1 month ago |
36-23274 1 month ago |
36-23261 36 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 |
29-53316 29 days ago |
29-67502 29 days ago |
50-27653 50 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 |
28-69151 28 days ago |
32-83356 1 month ago |
32-83644 32 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 |
27-35945 27 days ago |
32-22390 1 month ago |
35-53669 35 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 |
27-20088 27 days ago |
33-52931 1 month ago |
33-52970 33 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 |
26-64959 26 days ago |
31-59827 1 month ago |
31-60088 31 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 |
24-71499 24 days ago |
31-4999 1 month ago |
54-68371 54 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 |
24-35967 24 days ago |
28-25317 28 days ago |
28-25348 28 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 |
23-59689 23 days ago |
23-59692 23 days ago |
29-56943 29 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 |
23-35959 23 days ago |
29-18914 29 days ago |
29-18887 29 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 |
23-24609 23 days ago |
33-51653 1 month ago |
33-51682 33 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 |
23-24149 23 days ago |
33-28452 1 month ago |
33-28492 33 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 |
22-47573 22 days ago |
22-47637 22 days ago |
30-78632 30 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 |
22-40226 22 days ago |
22-40718 22 days ago |
32-45330 32 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 |
22-155 22 days ago |
23-28566 23 days ago |
23-28608 23 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 |
21-72842 21 days ago |
47-14505 1 month ago |
47-45393 47 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 |
21-44190 21 days ago |
21-44216 21 days ago |
34-13162 34 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 |
21-43925 21 days ago |
22-24380 22 days ago |
40-36280 40 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 |
21-35975 21 days ago |
24-47538 24 days ago |
24-50042 24 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 |
21-35971 21 days ago |
28-29085 28 days ago |
28-29089 28 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 |
21-1706 21 days ago |
21-1765 21 days ago |
42-67086 42 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 |
20-66096 20 days ago |
22-3880 22 days ago |
36-4798 36 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 |
20-35945 20 days ago |
30-48239 30 days ago |
30-48272 30 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 |
20-35944 20 days ago |
29-70366 29 days ago |
29-70443 29 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 |
20-35941 20 days ago |
25-71917 25 days ago |
25-72243 25 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 |
20-35940 20 days ago |
24-26747 24 days ago |
24-26783 24 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 |
20-35937 20 days ago |
23-46440 23 days ago |
23-46413 23 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 |
20-29971 20 days ago |
20-29995 20 days ago |
29-72060 29 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 |
19-35947 19 days ago |
22-67279 22 days ago |
22-74601 22 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 |
19-5161 19 days ago |
20-39830 20 days ago |
158-71518 158 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 |
18-35963 18 days ago |
21-61973 21 days ago |
21-62032 21 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 |
18-35960 18 days ago |
23-13485 23 days ago |
23-13525 23 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 |
18-35958 18 days ago |
21-46785 21 days ago |
22-22130 22 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 |
18-35957 18 days ago |
21-39427 21 days ago |
21-85370 21 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 |
18-35955 18 days ago |
21-80877 21 days ago |
21-80920 21 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 |
18-35950 18 days ago |
21-49282 21 days ago |
21-49263 21 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 |
18-30197 18 days ago |
18-31963 18 days ago |
23-29080 23 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 |
17-35951 17 days ago |
20-79994 20 days ago |
20-80033 20 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 |
17-35950 17 days ago |
20-46046 20 days ago |
20-70579 20 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 |
16-80791 16 days ago |
16-80803 16 days ago |
16-80836 16 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 |
16-67107 16 days ago |
20-40732 20 days ago |
37-59872 37 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 |
16-57573 16 days ago |
16-80279 16 days ago |
16-80314 16 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 |
16-51613 16 days ago |
44-33581 1 month ago |
44-33611 44 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 |
16-35965 16 days ago |
20-29099 20 days ago |
20-29143 20 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 |
16-11333 16 days ago |
16-11357 16 days ago |
42-7986 42 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 |
15-83934 15 days ago |
21-5552 21 days ago |
21-5591 21 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 |
15-35954 15 days ago |
18-39540 18 days ago |
18-39516 18 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 |
14-35963 14 days ago |
24-64695 24 days ago |
24-64731 24 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 |
14-35960 14 days ago |
17-65610 17 days ago |
17-65649 17 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 |
14-35959 14 days ago |
17-37354 17 days ago |
17-37390 17 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 |
14-17049 14 days ago |
14-73597 14 days ago |
15-42034 15 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 |
13-35929 13 days ago |
24-37075 24 days ago |
24-37048 24 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 |
12-62050 12 days ago |
12-62075 12 days ago |
17-81036 17 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 |
12-42772 12 days ago |
12-42799 12 days ago |
12-42837 12 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 |
12-38555 12 days ago |
12-38968 12 days ago |
70-82471 70 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 |
12-35942 12 days ago |
15-62567 15 days ago |
15-62603 15 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 |
12-24860 12 days ago |
21-42801 21 days ago |
87-8128 87 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 |
12-1819 12 days ago |
26-954 26 days ago |
46-779 46 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 |
11-41141 11 days ago |
21-44165 21 days ago |
22-45919 22 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 |
11-35960 11 days ago |
14-56353 14 days ago |
14-56811 14 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 |
11-35959 11 days ago |
15-31959 15 days ago |
15-31933 15 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 |
11-6083 11 days ago |
14-5065 14 days ago |
14-5103 14 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 |
10-35950 10 days ago |
14-7544 14 days ago |
20-60415 20 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 |
8-59585 8 days ago |
8-59592 8 days ago |
8-59626 8 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 |
8-44260 8 days ago |
8-44260 8 days ago |
18-26942 18 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 |
7-51296 7 days ago |
15-45543 15 days ago |
15-45589 15 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 |
80-52296 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 |
7-19714 7 days ago |
8-2132 8 days ago |
8-2167 8 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 |
7-12594 7 days ago |
14-11164 14 days ago |
29-31651 29 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 |
7-1405 7 days ago |
31-63028 1 month ago |
31-63059 31 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 |
6-73153 6 days ago |
6-85450 6 days ago |
6-85483 6 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 |
6-65872 6 days ago |
6-68451 6 days ago |
6-68425 6 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 |
6-51124 6 days ago |
11-33804 11 days ago |
28-25945 28 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 |
6-35943 6 days ago |
21-31551 21 days ago |
22-74963 22 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 |
6-35942 6 days ago |
9-53353 9 days ago |
11-25512 11 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 |
6-35938 6 days ago |
10-33082 10 days ago |
10-33063 10 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 |
6-35936 6 days ago |
9-44599 9 days ago |
9-44637 9 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 |
6-33491 6 days ago |
7-23142 7 days ago |
7-26330 7 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 |
6-7915 6 days ago |
7-48049 7 days ago |
8-30617 8 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 |
5-76596 5 days ago |
5-76596 5 days ago |
5-79633 5 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 |
5-50236 5 days ago |
9-71996 9 days ago |
9-71980 9 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 |
5-48360 5 days ago |
26-28747 26 days ago |
26-28722 26 days |
| 30981 |
jsm28 author:jsm28 |
feat(Geometry/Euclidean/Angle/Bisector): oriented angle bisection mod π |
Add lemmas relating equal distance to two lines to bisecting the angle between them mod π (expressed as usual as equality of twice angles), building on the previous lemmas (#30477) dealing with bisection mod 2π.
Existing lemmas have hypotheses of the form `(hp' : p' ∈ s₁ ⊓ s₂)` changed to `(hp'₁ : p' ∈ s₁) (hp'₂ : p' ∈ s₂)`, matching new lemmas, on the basis that the natural way to prove the first form is to use proofs of the two separate hypotheses.
---
- [ ] depends on: #30474
- [ ] depends on: #30477
- [ ] depends on: #30600
- [ ] depends on: #30703
[](https://gitpod.io/from-referrer/)
|
t-euclidean-geometry |
207/56 |
Mathlib/Geometry/Euclidean/Angle/Bisector.lean,Mathlib/Geometry/Euclidean/Projection.lean |
2 |
27 |
['JovanGerb', 'eric-wieser', 'github-actions', 'jsm28', 'mathlib4-dependent-issues-bot', 'mathlib4-merge-conflict-bot'] |
JovanGerb assignee:JovanGerb |
5-37035 5 days ago |
52-525 1 month ago |
56-43752 56 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 |
5-35933 5 days ago |
8-45582 8 days ago |
8-45555 8 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 |
5-35932 5 days ago |
8-45238 8 days ago |
8-45211 8 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 |
5-35932 5 days ago |
8-45183 8 days ago |
8-45156 8 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 |
5-28813 5 days ago |
5-34290 5 days ago |
73-4867 73 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 |
5-1427 5 days ago |
15-46663 15 days ago |
16-28030 16 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 |
4-69832 4 days ago |
4-80293 4 days ago |
4-80334 4 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 |
4-54706 4 days ago |
7-56576 7 days ago |
7-56551 7 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 |
4-52886 4 days ago |
4-52914 4 days ago |
21-57993 21 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 |
4-38394 4 days ago |
4-62932 4 days ago |
64-15730 64 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 |
4-35953 4 days ago |
8-66886 8 days ago |
8-66923 8 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 |
4-35950 4 days ago |
8-30761 8 days ago |
8-30741 8 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 |
4-35948 4 days ago |
7-68797 7 days ago |
7-68836 7 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 |
4-35947 4 days ago |
7-39998 7 days ago |
7-39984 7 days |
| 31046 |
Thmoas-Guan author:Thmoas-Guan |
feat(Homology) : compatibility of map between `Ext` |
In this PR, we proved the compatibility of map between `Ext` induced by exact functor with
1: `mk_0` 2: `comp` 3: `extClass`
---
- [ ] depends on: #31707
[](https://gitpod.io/from-referrer/) |
t-category-theory |
210/0 |
Mathlib/Algebra/Homology/DerivedCategory/Ext/Map.lean,Mathlib/Algebra/Homology/DerivedCategory/ShortExact.lean,Mathlib/Algebra/Homology/HomotopyCategory/Pretriangulated.lean,Mathlib/Algebra/Homology/HomotopyCategory/ShortExact.lean |
4 |
7 |
['Thmoas-Guan', 'github-actions', 'joelriou', 'mathlib4-dependent-issues-bot', 'mathlib4-merge-conflict-bot'] |
eric-wieser assignee:eric-wieser |
4-6877 4 days ago |
4-7454 4 days ago |
8-10769 8 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 |
3-84536 3 days ago |
39-82500 1 month ago |
49-40848 49 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 |
3-83018 3 days ago |
12-2318 12 days ago |
12-28108 12 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 |
3-77467 3 days ago |
3-78389 3 days ago |
24-74131 24 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 |
3-75645 3 days ago |
5-78920 5 days ago |
9-80600 9 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 |
3-71466 3 days ago |
4-80840 4 days ago |
4-81365 4 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 |
22-40500 22 days ago |
22-40724 22 days ago |
30-44580 30 days |
| 33286 |
euprunin author:euprunin |
chore: golf using `grind` |
---
The goal of this golfing PR is to decrease the number of times lemmas are called explicitly (replacing calls to lemmas with calls to tactics). Any decrease in compilation time is a welcome side effect, although it is not a primary objective.
Trace profiling results (shown if ≥10 ms before or after):
* `Finset.memberSubfamily_union_nonMemberSubfamily`: 11 ms before, 116 ms after
* `AkraBazziRecurrence.GrowsPolynomially.eventually_atTop_nonneg_or_nonpos`: 1181 ms before, 1194 ms after
* `Equiv.Perm.support_congr`: <10 ms before, 38 ms after
* `Equiv.Perm.subtypeCongr.trans`: 13 ms before, 35 ms after
* `preCantorSet_antitone`: 766 ms before, 371 ms after 🎉
This golfing PR is batched under the following guidelines:
* Up to ~5 changed files per PR
* Up to ~25 changed declarations per PR
* Up to ~100 changed lines per PR
---
[](https://gitpod.io/from-referrer/)
|
|
6/28 |
Mathlib/Computability/AkraBazzi/GrowsPolynomially.lean,Mathlib/GroupTheory/Perm/Support.lean,Mathlib/Logic/Equiv/Basic.lean,Mathlib/Topology/Instances/CantorSet.lean |
4 |
5 |
['euprunin', 'github-actions', 'vihdzp'] |
thorimur assignee:thorimur |
3-57617 3 days ago |
3-58236 3 days ago |
15-31506 15 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 |
3-35949 3 days ago |
6-51611 6 days ago |
7-18011 7 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 |
3-33313 3 days ago |
3-33313 3 days ago |
7-29667 7 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 |
3-17736 3 days ago |
3-17767 3 days ago |
4-61084 4 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 |
3-9408 3 days ago |
3-9408 3 days ago |
3-81274 3 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 |
2-85885 2 days ago |
3-273 3 days ago |
3-256 3 days |
| 32134 |
mitchell-horner author:mitchell-horner |
feat(Topology/Real): theorems linking `IsGLB` with `BddBelow`, `Antitone`, `Tendsto _ atTop` |
Implement theorems linking `IsGLB` (`IsLUB`) with `BddBelow` (`BddAbove`), `Antitone` (`Monotone`), `Tendsto _ atTop`
---
[](https://gitpod.io/from-referrer/)
|
t-topology
maintainer-merge
large-import
|
124/69 |
Mathlib/Algebra/Order/Monoid/Canonical/Basic.lean,Mathlib/Analysis/Normed/Unbundled/SeminormFromConst.lean,Mathlib/Analysis/Normed/Unbundled/SpectralNorm.lean,Mathlib/Topology/Instances/NNReal/Lemmas.lean,Mathlib/Topology/Instances/Real/Lemmas.lean |
5 |
24 |
['YaelDillies', 'github-actions', 'mitchell-horner'] |
YaelDillies assignee:YaelDillies |
2-80975 2 days ago |
2-80975 2 days ago |
35-30873 35 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 |
2-79086 2 days ago |
2-79105 2 days ago |
4-42525 4 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 |
2-75031 2 days ago |
7-56423 7 days ago |
7-56410 7 days |
| 33192 |
linesthatinterlace author:linesthatinterlace |
refactor(Data/List/Induction): improve definition of `reverseRecOn` |
This PR improves the definition of `List.reverseRecOn`.
---
This improved approach aims to give identical behavior but give a somewhat nicer proof of `List.reverseRecOn_concat`. I do not believe it is a regression in terms of performance.
The approach is inspired by `biDirectionalRec`, for which I have also tweaked the definitions and proofs, albeit in a much more minor way.
[](https://gitpod.io/from-referrer/)
|
t-data |
32/27 |
Mathlib/Data/List/Induction.lean |
1 |
6 |
['github-actions', 'linesthatinterlace', 'vihdzp'] |
pechersky assignee:pechersky |
2-70144 2 days ago |
18-85008 18 days ago |
18-85044 18 days |
| 33722 |
erdOne author:erdOne |
feat(RingTheory): Add `RingHom.QuasiFinite` |
---
[](https://gitpod.io/from-referrer/)
|
t-ring-theory |
128/0 |
Mathlib.lean,Mathlib/RingTheory/RingHom/QuasiFinite.lean |
2 |
1 |
['github-actions'] |
nobody |
2-68361 2 days ago |
2-68364 2 days ago |
2-68404 2 days |
| 33642 |
themathqueen author:themathqueen |
feat(Analysis/Matrix/Order): polar decomposition for {invertible, Hermitian} matrices |
For an invertible (resp., Hermitian) matrix `A`, there exists unitary `U` and a positive definite (resp., semidefinite) matrix `P` such that `A = U * P`.
---
[](https://gitpod.io/from-referrer/)
|
t-analysis |
41/4 |
Mathlib/Analysis/Matrix/Order.lean |
1 |
3 |
['github-actions', 'mathlib4-merge-conflict-bot', 'themathqueen'] |
nobody |
2-63467 2 days ago |
2-63562 2 days ago |
4-33784 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 |
2-63443 2 days ago |
25-60597 25 days ago |
28-47556 28 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 |
2-61417 2 days ago |
2-61488 2 days ago |
3-31442 3 days |
| 32734 |
Vierkantor author:Vierkantor |
chore(Tactic): document remaining undocumented tactics |
Write documentation for the few tactics in Mathlib that have no documentation at all. After this PR and a few related ones are merged, every tactic defined in Mathlib should now have a docstring or a `@[tactic_alt]` attribute.
~~The documentation for `mem_tac` is pending a Zulip discussion: https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/Proj.20as.20a.20scheme.3A.20.60mem_tac.60.20works.20accidentally.3F/with/563193768~~ Zulip discussion now applies to the independent PR #33711. This PR can be merged before or after #33711 (or #33711 can be closed).
---
[](https://gitpod.io/from-referrer/)
|
documentation
t-meta
|
28/0 |
Mathlib/Tactic/Conv.lean,Mathlib/Tactic/GCongr/Core.lean |
2 |
3 |
['Vierkantor', 'github-actions', 'mathlib4-merge-conflict-bot'] |
nobody |
2-56012 2 days ago |
2-56052 2 days ago |
14-16586 14 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 |
2-47895 2 days ago |
18-83697 18 days ago |
18-83744 18 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 |
2-44484 2 days ago |
3-24863 3 days ago |
3-24896 3 days |
| 33288 |
vihdzp author:vihdzp |
chore(Combinatorics/SimpleGraph/Paths): review API |
This PR does the following:
- Add `grind` annotations.
- Rename theorems `X_isY` to the more idiomatic `isY_X`.
- Remove many redundant namespaces.
- Golf accordingly.
---
[](https://gitpod.io/from-referrer/)
|
t-combinatorics |
154/122 |
Mathlib/Combinatorics/SimpleGraph/Acyclic.lean,Mathlib/Combinatorics/SimpleGraph/Connectivity/Connected.lean,Mathlib/Combinatorics/SimpleGraph/Matching.lean,Mathlib/Combinatorics/SimpleGraph/Metric.lean,Mathlib/Combinatorics/SimpleGraph/Paths.lean,Mathlib/Combinatorics/SimpleGraph/Walks/Maps.lean |
6 |
2 |
['github-actions', 'mathlib4-merge-conflict-bot'] |
nobody |
2-43382 2 days ago |
2-43402 2 days ago |
5-80323 5 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 |
2-40810 2 days ago |
2-42777 2 days ago |
2-48544 2 days |
| 33699 |
artie2000 author:artie2000 |
chore(Algebra/Ring): semireal definition lemmas |
* Add converse to `IsSemireal.not_isSumSq_neg_one `
---
[](https://gitpod.io/from-referrer/)
|
t-algebra label:t-algebra$ |
9/2 |
Mathlib/Algebra/Ring/Semireal/Defs.lean |
1 |
4 |
['artie2000', 'github-actions', 'vihdzp'] |
nobody |
2-39092 2 days ago |
3-32149 3 days ago |
3-32183 3 days |
| 33336 |
fbarroero author:fbarroero |
feat(NumberTheory/MahlerMeasure): Kronecker's Theorem for the Mahler Measure |
This PR adds Kronecker's Theorem for the Mahler Measure, which characterizes integer polynomials with Mahler measure equal to 1. The key mathematical contribution is proving that such polynomials have all their nonzero complex roots as roots of unity, and consequently must be divisible by cyclotomic polynomials.
Main result
```
Polynomial.pow_eq_one_of_mahlerMeasure_eq_one {p : ℤ[X]} (h : (map (castRingHom ℂ) p).mahlerMeasure = 1)
{z : ℂ} (hz₀ : z ≠ 0) (hz : z ∈ p.aroots ℂ) : ∃ n, 0 < n ∧ z ^ n = 1
```
---
[](https://gitpod.io/from-referrer/)
|
|
128/9 |
Mathlib/Algebra/Order/BigOperators/Ring/Multiset.lean,Mathlib/NumberTheory/MahlerMeasure.lean |
2 |
11 |
['copilot-pull-request-reviewer', 'github-actions', 'mathlib4-merge-conflict-bot'] |
tb65536 assignee:tb65536 |
2-37435 2 days ago |
6-63521 6 days ago |
9-68273 9 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 |
2-36500 2 days ago |
2-36569 2 days ago |
4-42833 4 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 |
2-35964 2 days ago |
5-48215 5 days ago |
6-39810 6 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 |
2-35962 2 days ago |
6-23727 6 days ago |
7-6991 7 days |
| 33312 |
YuvalFilmus author:YuvalFilmus |
feat(Polynomial/Chebyshev): formulas for iterated derivatives of T and U at 1 |
The main results are `iterate_derivative_T_eval_one` and `iterate_derivative_U_eval_one`.
These are derived using recurrences which for at every point, and in particular, `iterate_derivative_T_eval_zero` and `iterate_derivative_U_eval_zero` gives the recurrences at zero.
In principle, by combining with #33311, one can compute the explicit formula for the derivative at zero.
A subsequent PR will derive consequences for these polynomials over the reals (these should work for every field).
The file is getting rather long — not sure what to do about it.
---
- [ ] depends on: #33283
- [ ] depends on: #33306
[](https://gitpod.io/from-referrer/)
|
|
110/0 |
Mathlib/RingTheory/Polynomial/Chebyshev.lean |
1 |
3 |
['github-actions', 'mathlib4-dependent-issues-bot', 'mathlib4-merge-conflict-bot'] |
RemyDegenne assignee:RemyDegenne |
2-35960 2 days ago |
2-59781 2 days ago |
2-61251 2 days |
| 33372 |
kex-y author:kex-y |
feat(Probability): Countable infimum of stopping times is a stopping time |
---
- [x] depends on: #33371
[](https://gitpod.io/from-referrer/)
|
t-measure-probability
brownian
|
83/0 |
Mathlib/Probability/Process/Stopping.lean |
1 |
3 |
['github-actions', 'mathlib4-dependent-issues-bot', 'mathlib4-merge-conflict-bot'] |
RemyDegenne assignee:RemyDegenne |
2-35958 2 days ago |
5-75417 5 days ago |
5-81280 5 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 |
2-35957 2 days ago |
5-50903 5 days ago |
8-41179 8 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'] |
erdOne assignee:erdOne |
2-35956 2 days ago |
5-57910 5 days ago |
6-50776 6 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 |
2-35955 2 days ago |
6-36943 6 days ago |
6-36927 6 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 |
2-35952 2 days ago |
6-4364 6 days ago |
6-4346 6 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 |
92 |
['0xTerencePrime', 'SnirBroshi', 'github-actions', 'vihdzp'] |
nobody |
2-32184 2 days ago |
12-81785 12 days ago |
12-81817 12 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 |
2-30100 2 days ago |
2-30161 2 days ago |
12-65336 12 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 |
2-28828 2 days ago |
2-28828 2 days ago |
56-61372 56 days |
| 33741 |
mcdoll author:mcdoll |
feat(Analysis/SchwartzSpace): additional lemmas for `smulLeftCLM` |
Add various lemmas for `smulLeftCLM`.
---
The lemma for the sum could be proved with induction, but that proof is slightly longer.
[](https://gitpod.io/from-referrer/)
|
t-analysis |
58/3 |
Mathlib/Analysis/Distribution/SchwartzSpace.lean |
1 |
1 |
['github-actions'] |
nobody |
2-25291 2 days ago |
2-25761 2 days ago |
2-25808 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 |
170/22 |
Mathlib/Tactic/Choose.lean,MathlibTest/choose.lean |
2 |
20 |
['AlexKontorovich', 'eric-wieser', 'fpvandoorn', 'github-actions', 'kim-em'] |
joneugster assignee:joneugster |
2-19772 2 days ago |
21-46764 21 days ago |
22-31162 22 days |
| 33745 |
euprunin author:euprunin |
chore: golf proofs |
---
The goal of this golfing PR is to decrease the number of times lemmas are called explicitly (replacing calls to lemmas with calls to tactics). Any decrease in compilation time is a welcome side effect, although it is not a primary objective.
Trace profiling results (shown if ≥10 ms before or after):
* `LinearGrowth.linearGrowthInf_comp_nonneg`: 29 ms before, 17 ms after 🎉
* `CategoryTheory.Limits.preservesLimit_of_preservesEqualizers_and_product`: 821 ms before, 530 ms after 🎉
* `CategoryTheory.Limits.Pi.map_eq_prod_map`: 161 ms before, 101 ms after 🎉
* `CategoryTheory.isCardinalPresentable_of_equivalence`: 116 ms before, 107 ms after 🎉
* `SimpleGraph.nontrivial_of_diam_ne_zero`: <10 ms before, <10 ms after 🎉
* `univ_eq_singleton_of_card_one`: 14 ms before, <10 ms after 🎉
* `CoxeterSystem.getElem_leftInvSeq_alternatingWord`: 41 ms before, 40 ms after 🎉
* `Matrix.SpecialLinearGroup.mapGL_inj`: 73 ms before, 45 ms after 🎉
* `PiTensorProduct.reindex_refl`: 88 ms before, 65 ms after 🎉
* `MeasureTheory.continuous_diracProbaEquivSymm`: 17 ms before, <10 ms after 🎉
* `Representation.ofModule_asModule_act`: 78 ms before, 61 ms after 🎉
This golfing PR is batched under the following guidelines:
* Up to ~5 changed files per PR
* Up to ~25 changed declarations per PR
* Up to ~100 changed lines per PR
---
[](https://gitpod.io/from-referrer/)
|
|
6/21 |
Mathlib/Analysis/Asymptotics/LinearGrowth.lean,Mathlib/CategoryTheory/Limits/Constructions/LimitsOfProductsAndEqualizers.lean,Mathlib/CategoryTheory/Limits/Shapes/PiProd.lean,Mathlib/CategoryTheory/Presentable/Basic.lean,Mathlib/Combinatorics/SimpleGraph/Diam.lean,Mathlib/Data/Fintype/Card.lean,Mathlib/GroupTheory/Coxeter/Inversion.lean,Mathlib/LinearAlgebra/Matrix/GeneralLinearGroup/Defs.lean,Mathlib/LinearAlgebra/PiTensorProduct.lean,Mathlib/RepresentationTheory/Basic.lean |
10 |
1 |
['github-actions'] |
nobody |
2-6259 2 days ago |
2-6343 2 days ago |
2-6316 2 days |
| 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 |
2-4455 2 days ago |
3-9509 3 days ago |
3-10447 3 days |
| 27599 |
mitchell-horner author:mitchell-horner |
feat(Combinatorics/SimpleGraph): define `CompleteEquipartiteSubgraph` |
Define the complete equipartite subgraphs in `r` parts each of size `t` in `G` as the `r` subsets of vertices each of size `t` such that vertices in distinct subsets are adjacent.
In this case `Nonempty (G.CompleteEquipartiteSubgraph r t)` is equivalent to `completeEquipartiteGraph r t ⊑ G`, that is, finding `r` subsets of vertices each of size `t` in `G` such that vertices in distinct subsets are adjacent is equivalent to finding an injective homomorphism from `completeEquipartiteGraph r t` to `G`.
---
- [x] depends on: #27597
- [x] depends on: #30287
[](https://gitpod.io/from-referrer/)
|
t-combinatorics |
173/7 |
Mathlib/Combinatorics/SimpleGraph/CompleteMultipartite.lean |
1 |
34 |
['YaelDillies', 'b-mehta', 'github-actions', 'mathlib4-dependent-issues-bot', 'mathlib4-merge-conflict-bot', 'mitchell-horner'] |
YaelDillies assignee:YaelDillies |
2-529 2 days ago |
3-35413 3 days ago |
73-84625 73 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 |
1-83033 1 day ago |
1-83033 1 day ago |
1-83075 1 day |
| 33752 |
mcdoll author:mcdoll |
feat(Analysis/FourierSchwartz): the derivative of the Fourier transform |
Calculate the derivative (`fderiv` and `lineDerivOp`) of the (inverse) Fourier transform.
We also generalize `evalCLM` slightly and make it's arguments explicit.
---
[](https://gitpod.io/from-referrer/)
|
t-analysis |
90/9 |
Mathlib/Analysis/Distribution/FourierSchwartz.lean,Mathlib/Analysis/Distribution/SchwartzSpace.lean |
2 |
1 |
['github-actions'] |
nobody |
1-82892 1 day ago |
1-82892 1 day ago |
1-82937 1 day |
| 32924 |
chrisflav author:chrisflav |
feat(RingTheory/Smooth): smooth is equivalent to locally standard smooth |
From Pi1.
---
- [ ] depends on: #32925
The import increase is expected. The file `Mathlib.RingTheory.Smooth.StandardSmoothOfFree` is a leaf file that was planned to contain this proof.
[](https://gitpod.io/from-referrer/)
|
large-import
t-ring-theory
|
274/4 |
Mathlib.lean,Mathlib/Algebra/Module/LocalizedModule/Basic.lean,Mathlib/RingTheory/Etale/Basic.lean,Mathlib/RingTheory/Etale/Kaehler.lean,Mathlib/RingTheory/Ideal/Span.lean,Mathlib/RingTheory/LocalRing/Module.lean,Mathlib/RingTheory/Localization/Away/Basic.lean,Mathlib/RingTheory/Localization/Module.lean,Mathlib/RingTheory/RingHom/LocallyStandardSmooth.lean,Mathlib/RingTheory/RingHom/StandardSmooth.lean,Mathlib/RingTheory/Smooth/Basic.lean,Mathlib/RingTheory/Smooth/Locus.lean,Mathlib/RingTheory/Smooth/StandardSmoothOfFree.lean,Mathlib/RingTheory/Support.lean |
14 |
2 |
['github-actions', 'mathlib4-dependent-issues-bot'] |
nobody |
1-82051 1 day ago |
1-82051 1 day ago |
8-75487 8 days |
| 33743 |
jcommelin author:jcommelin |
ci: add automated commit verification |
This PR adds verification for "x: " commits that checks whether re-running the command produces the same tree.
Written with the help of Claude Code.
---
[](https://gitpod.io/from-referrer/)
|
CI |
406/28 |
.github/workflows/commit_verification.yml,scripts/README.md,scripts/verify_commits.sh,scripts/verify_commits_summary.sh |
4 |
6 |
['Vierkantor', 'github-actions', 'jcommelin'] |
nobody |
1-79918 1 day ago |
2-11932 2 days ago |
2-11968 2 days |
| 27542 |
chrisflav author:chrisflav |
feat(RingTheory/KrullDimension): dimension of polynomial ring |
We show that for a Noetherian ring `R`, `dim R[X] = dim R + 1`.
Co-authored by: Sihan Su
Co-authored by: Yi Song
---
- [x] depends on: #27520
- [x] depends on: #27538
- [x] depends on: #27510
- [x] depends on: #32472
[](https://gitpod.io/from-referrer/)
|
large-import
t-ring-theory
|
144/3 |
Mathlib/Order/KrullDimension.lean,Mathlib/RingTheory/Ideal/Height.lean,Mathlib/RingTheory/KrullDimension/Polynomial.lean,Mathlib/RingTheory/Localization/AtPrime/Basic.lean |
4 |
n/a |
['chrisflav', 'erdOne', 'github-actions', 'mathlib4-dependent-issues-bot', 'mathlib4-merge-conflict-bot'] |
nobody |
1-79006 1 day ago |
unknown |
unknown |
| 33449 |
yuanyi-350 author:yuanyi-350 |
feat(ProbabilityTheory): Add Poisson limit theorem |
---
[](https://gitpod.io/from-referrer/)
|
t-measure-probability |
145/2 |
Mathlib.lean,Mathlib/Probability/Distributions/Poisson.lean,Mathlib/Probability/Distributions/PoissonLimitThm.lean,docs/1000.yaml |
4 |
4 |
['github-actions', 'vihdzp'] |
EtienneC30 assignee:EtienneC30 |
1-78933 1 day ago |
1-80649 1 day ago |
9-15040 9 days |
| 33754 |
euprunin author:euprunin |
chore: golf proofs |
---
The goal of this golfing PR is to decrease the number of times lemmas are called explicitly (replacing calls to lemmas with calls to tactics). Any decrease in compilation time is a welcome side effect, although it is not a primary objective.
Trace profiling results (shown if ≥10 ms before or after):
* `balancedHull_subset_convexHull_union_neg`: 181 ms before, 160 ms after 🎉
* `schnirelmannDensity_setOf_Odd`: 28 ms before, 16 ms after 🎉
* `List.nodupKeys_flatten`: 134 ms before, 110 ms after 🎉
This golfing PR is batched under the following guidelines:
* Up to ~5 changed files per PR
* Up to ~25 changed declarations per PR
* Up to ~100 changed lines per PR
---
[](https://gitpod.io/from-referrer/)
|
|
1/5 |
Mathlib/Analysis/LocallyConvex/AbsConvex.lean,Mathlib/Combinatorics/Schnirelmann.lean,Mathlib/Data/List/Sigma.lean |
3 |
1 |
['github-actions'] |
nobody |
1-76895 1 day ago |
1-76963 1 day ago |
1-76936 1 day |
| 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 |
46 |
['Ruben-VandeVelde', 'Whysoserioushah', 'eric-wieser', 'github-actions', 'kbuzzard', 'kckennylau', 'mathlib4-merge-conflict-bot', 'vlad902'] |
kbuzzard assignee:kbuzzard |
1-69233 1 day ago |
6-58962 6 days ago |
6-66547 6 days |
| 33763 |
smmercuri author:smmercuri |
doc: add note in `Asymptotics` docstring about the existential pattern |
see [Zulip chat](https://leanprover.zulipchat.com/#narrow/channel/116395-maths/topic/Use.20of.20embedded.20Landau.20notation/with/566790160)
---
[](https://gitpod.io/from-referrer/)
|
t-analysis |
6/0 |
Mathlib/Analysis/Asymptotics/Defs.lean |
1 |
1 |
['github-actions'] |
nobody |
1-67589 1 day ago |
1-67589 1 day ago |
1-67634 1 day |
| 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
|
321/79 |
Mathlib/Algebra/Algebra/Operations.lean,Mathlib/RingTheory/PicardGroup.lean |
2 |
32 |
['alreadydone', 'erdOne', 'github-actions', 'jcommelin', 'mathlib4-dependent-issues-bot', 'mathlib4-merge-conflict-bot', 'tb65536'] |
mariainesdff assignee:mariainesdff |
1-67017 1 day ago |
5-44418 5 days ago |
48-74039 48 days |
| 29942 |
smmercuri author:smmercuri |
feat(InfinitePlace/Completion): embeddings of `w.Completion` factor through embeddings of `v.Completion` when `w` extends `v` |
If `w : InfinitePlace L` is an extension of `v : InfinitePlace K` to `L` (i.e. we have `w.1.LiesOver v.1`), then `extensionEmbedding w : L →+* ℂ` factors through `extensionEmbedding v : K →+* ℂ`.
---
- [x] depends on: #27978
- [x] depends on: #29969
- [x] depends on: #29944
[](https://gitpod.io/from-referrer/)
|
FLT |
88/14 |
Mathlib/Analysis/Normed/Field/WithAbs.lean,Mathlib/NumberTheory/NumberField/InfinitePlace/Completion.lean,Mathlib/NumberTheory/NumberField/InfinitePlace/Embeddings.lean,Mathlib/Topology/MetricSpace/Completion.lean |
4 |
5 |
['github-actions', 'mathlib4-dependent-issues-bot', 'mathlib4-merge-conflict-bot'] |
joelriou assignee:joelriou |
1-66351 1 day ago |
42-59721 1 month ago |
42-60813 42 days |
| 33764 |
IvanRenison author:IvanRenison |
feat(Combinatorics/SimpleGraph/Diam): drop `Finite α` from `ediam_le_two_mul_radius` |
---
[](https://gitpod.io/from-referrer/)
|
t-combinatorics |
25/5 |
Mathlib/Combinatorics/SimpleGraph/Diam.lean |
1 |
1 |
['github-actions'] |
nobody |
1-63851 1 day ago |
1-63851 1 day ago |
1-63892 1 day |
| 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 |
1-63361 1 day ago |
4-14487 4 days ago |
48-18923 48 days |
| 33359 |
sun123zxy author:sun123zxy |
feat(Algebra/Module/SpanRank): add comparing lemmas for span rank |
---
Split from PR #33247
[](https://gitpod.io/from-referrer/)
|
t-algebra
new-contributor
label:t-algebra$ |
55/6 |
Mathlib/Algebra/Module/SpanRank.lean |
1 |
9 |
['erdOne', 'eric-wieser', 'github-actions', 'sun123zxy'] |
eric-wieser assignee:eric-wieser |
1-63223 1 day ago |
1-63223 1 day ago |
7-63920 7 days |
| 29186 |
winstonyin author:winstonyin |
feat: IsIntegralCurve for solutions to ODEs |
I define `IsIntegralCurve` etc. for solutions to ODEs on vector spaces. The translation and scaling lemmas are also included. This parallels `IsMIntegralCurve` etc. for manifolds.
Moved from #26534.
- [x] depends on: #26563
---
[](https://gitpod.io/from-referrer/)
|
t-differential-geometry
t-analysis
t-dynamics
|
305/100 |
Mathlib.lean,Mathlib/Analysis/ODE/Basic.lean,Mathlib/Analysis/ODE/Transform.lean,Mathlib/Geometry/Manifold/IntegralCurve/Basic.lean,Mathlib/Geometry/Manifold/IntegralCurve/Transform.lean |
5 |
11 |
['github-actions', 'grunweg', 'mathlib4-dependent-issues-bot', 'mathlib4-merge-conflict-bot', 'mcdoll', 'sgouezel', 'winstonyin'] |
sgouezel assignee:sgouezel |
1-63178 1 day ago |
3-58081 3 days ago |
103-77047 103 days |
| 33390 |
farmanb author:farmanb |
feat(RingTheory/Ideal): generalize Submodule.colon to sets |
This PR generalizes `Submodule.colon` to arguments of type `Set M` in the second slot and updates the surrounding API accordingly.
Main changes
* Generalize `Submodule.colon` to take `S : Set M` rather than `P : Submodule R M`.
* Normalize theorems/lemmas to use `Set.univ` instead of `⊤` where appropriate.
* Strengthen `iInf_colon_iSup` by removing an unnecessary commutativity assumption.
* Update monotonicity and inclusion lemmas (e.g. `_root_.Ideal.le_colon`) to use set inclusions.
* Add `colon_bot'` (`CommSemiring`): identify `⊥.colon S` with the annihilator of `Submodule.span R S`.
* Adjust annihilator-related proofs to account for the generalized colon, using explicit coercions such as `Submodule.top_coe`.
---
[](https://gitpod.io/from-referrer/)
|
new-contributor
t-ring-theory
|
109/48 |
Mathlib/RingTheory/Ideal/Colon.lean,Mathlib/RingTheory/Ideal/Oka.lean,Mathlib/RingTheory/Lasker.lean,Mathlib/RingTheory/Noetherian/OfPrime.lean,Mathlib/RingTheory/PrincipalIdealDomainOfPrime.lean,Mathlib/RingTheory/Support.lean |
6 |
2 |
['farmanb', 'github-actions'] |
nobody |
1-53720 1 day ago |
1-53720 1 day ago |
1-53840 1 day |
| 33740 |
SnirBroshi author:SnirBroshi |
chore(Order/CompleteLattice/Basic): generalize many theorems to `CompleteSemilattice{Sup/Inf}` |
---
I believe some of these can be generalized further, this PR takes a small step.
This might also allow half of these to be deleted thanks to `to_dual` somehow.
[](https://gitpod.io/from-referrer/)
|
t-order |
212/178 |
Mathlib/Order/CompleteLattice/Basic.lean,Mathlib/Order/Interval/Set/Disjoint.lean |
2 |
8 |
['JovanGerb', 'SnirBroshi', 'github-actions', 'vihdzp'] |
nobody |
1-52174 1 day ago |
2-27827 2 days ago |
2-27864 2 days |
| 33768 |
vihdzp author:vihdzp |
chore(Order/RelClasses): remove redundant instances |
---
[](https://gitpod.io/from-referrer/)
|
t-order |
0/20 |
Mathlib/Order/RelClasses.lean |
1 |
3 |
['github-actions', 'leanprover-radar', 'vihdzp'] |
nobody |
1-51907 1 day ago |
1-56419 1 day ago |
1-56460 1 day |
| 32672 |
tb65536 author:tb65536 |
feat: haar measures on short exact sequences |
This PR defines the notion of a short exact sequence of topological groups, and proves that if `1 → A → B → C → 1` is a short exact sequence of topological groups, then Haar measures on `A` and `C` induce a Haar measure on `B`.
The final result of the file is a consequence needed for FLT: If `B → C` is injective on an open set `U`, then `U` has bounded measure.
---
[](https://gitpod.io/from-referrer/)
|
t-topology
t-measure-probability
FLT
|
374/0 |
Mathlib.lean,Mathlib/MeasureTheory/Measure/Haar/Extension.lean,Mathlib/Topology/Algebra/Group/Extension.lean |
3 |
6 |
['RemyDegenne', 'github-actions', 'kbuzzard', 'tb65536'] |
urkud assignee:urkud |
1-51193 1 day ago |
26-56908 26 days ago |
30-20010 30 days |
| 32042 |
chrisflav author:chrisflav |
feat(AlgebraicGeometry): quasi compact covers |
This will be used to define the fpqc topology on `Scheme`.
From Proetale.
---
[](https://gitpod.io/from-referrer/)
|
t-algebraic-geometry |
311/13 |
Mathlib.lean,Mathlib/AlgebraicGeometry/Cover/QuasiCompact.lean,Mathlib/AlgebraicGeometry/Morphisms/Affine.lean,Mathlib/AlgebraicGeometry/Morphisms/QuasiCompact.lean,Mathlib/AlgebraicGeometry/Morphisms/UnderlyingMap.lean,Mathlib/AlgebraicGeometry/Sites/MorphismProperty.lean,Mathlib/Topology/Sets/CompactOpenCovered.lean,Mathlib/Topology/Spectral/Prespectral.lean |
8 |
15 |
['chrisflav', 'erdOne', 'github-actions'] |
joneugster assignee:joneugster |
1-49259 1 day ago |
1-76275 1 day ago |
46-12949 46 days |
| 33749 |
plp127 author:plp127 |
feat: `NNRat` is countable |
We provide an `Encodable NNRat` instance. As a consequence we also get the instance `Countable NNRat`.
See also [Zulip](https://leanprover.zulipchat.com/#narrow/channel/113489-new-members/topic/NNRat.20not.20countable.3F/near/566916284)
---
[](https://gitpod.io/from-referrer/)
|
t-data
large-import
|
13/0 |
Mathlib/Data/Rat/Encodable.lean |
1 |
4 |
['eric-wieser', 'github-actions', 'grunweg', 'leanprover-radar'] |
nobody |
1-47230 1 day ago |
1-47238 1 day ago |
1-84058 1 day |
| 33769 |
alreadydone author:alreadydone |
feat(LinearAlgebra): add `Module.IsPrincipal` |
---
[](https://gitpod.io/from-referrer/)
|
t-algebra label:t-algebra$ |
36/0 |
Mathlib/LinearAlgebra/Span/Defs.lean |
1 |
1 |
['github-actions'] |
nobody |
1-44662 1 day ago |
1-50062 1 day ago |
1-50114 1 day |
| 33527 |
SnirBroshi author:SnirBroshi |
feat(Combinatorics/SimpleGraph/Connectivity/Subgraph): `w.toSubgraph ≤ G' ↔ w.edgeSet ⊆ G'.edgeSet` |
---
[](https://gitpod.io/from-referrer/)
|
t-combinatorics |
9/1 |
Mathlib/Combinatorics/SimpleGraph/Connectivity/Subgraph.lean |
1 |
4 |
['Rida-Hamadani', 'SnirBroshi', 'github-actions'] |
nobody |
1-43126 1 day ago |
6-52556 6 days ago |
6-52589 6 days |
| 33776 |
mcdoll author:mcdoll |
feat(MeasureTheory): every bounded continuous function is in `L∞` |
As opposed to the lemma right below we use `MemLp` and not `f.toContinuousMap.toAEEqFun μ ∈ Lp`, because
the later seems rather unergonomic and with `MemLp` it is possible to obtain a `Lp` function using `MemLp.toLp`.
---
[](https://gitpod.io/from-referrer/)
|
t-measure-probability |
4/0 |
Mathlib/MeasureTheory/Function/LpSpace/ContinuousFunctions.lean |
1 |
1 |
['github-actions'] |
nobody |
1-42321 1 day ago |
1-42323 1 day ago |
1-42361 1 day |
| 33780 |
ooovi author:ooovi |
feat(Geometry/Convex/Cone): lineality space of pointed cones |
Define the lineality space `PointedCone.lineal` as the submodule `C ⊓ -C`. Prove that it is the largest submodule of the cone, which is sometimes used as an alternative definition.
Co-authored-by: Martin Winter
---
- [ ] depends on #33761
[](https://gitpod.io/from-referrer/)
|
t-convex-geometry |
79/4 |
Mathlib/Algebra/Module/Submodule/RestrictScalars.lean,Mathlib/Geometry/Convex/Cone/Pointed.lean,Mathlib/RingTheory/Ideal/Maps.lean |
3 |
1 |
['github-actions'] |
nobody |
1-39657 1 day ago |
1-39657 1 day ago |
1-39854 1 day |
| 32757 |
AntoineChambert-Loir author:AntoineChambert-Loir |
feat(LinearAlgebra/Transvection): the determinant of a transvection is equal to 1. |
Prove that the determinant of a transvection is equal to 1
The proof goes by showing that the determinant of `LinearMap.transvection f v` is `1 + f v` (even if `f v` is nonzero).
I first treat the case of a field, distinguishing whether `f v = 0` (so that we get
a transvection) or not (so that we have a dilation).
Then, by base change to the field of fractions, I can handle the case of a domain. Finally, the general case is treated by base change from the “universal case” where the base ring is the ring of polynomials in $$2n$$ indeterminates corresponding to the coefficients of $$f$$ and $$v$$.
---
- [x] depends on: #31138
[](https://gitpod.io/from-referrer/)
|
|
255/0 |
Mathlib/LinearAlgebra/Determinant.lean,Mathlib/LinearAlgebra/Transvection.lean |
2 |
n/a |
['AntoineChambert-Loir', 'github-actions', 'mathlib4-dependent-issues-bot', 'mathlib4-merge-conflict-bot'] |
nobody |
1-39536 1 day ago |
unknown |
unknown |
| 33779 |
tb65536 author:tb65536 |
refactor: generalize `isPrimary_of_isMaximal_radical` to `CommSemiring` |
This PR generalizes `isPrimary_of_isMaximal_radical` to `CommSemiring` and moves it earlier to `IsPrimary.lean`.
---
[](https://gitpod.io/from-referrer/)
|
t-algebra
t-ring-theory
label:t-algebra$ |
15/14 |
Mathlib/RingTheory/Ideal/IsPrimary.lean,Mathlib/RingTheory/Jacobson/Ideal.lean |
2 |
1 |
['github-actions'] |
nobody |
1-38960 1 day ago |
1-38960 1 day ago |
1-38935 1 day |
| 33781 |
tb65536 author:tb65536 |
feat(Ideal/IsPrimary): `Ideal.isPrimary` preserved by `Ideal.comap` |
This PR adds a lemma stating that the preimage of a primary ideal under a ring homomorphism remains a primary ideal.
---
[](https://gitpod.io/from-referrer/)
|
t-algebra
t-ring-theory
label:t-algebra$ |
8/1 |
Mathlib/RingTheory/Ideal/IsPrimary.lean |
1 |
1 |
['github-actions'] |
nobody |
1-38368 1 day ago |
1-38368 1 day ago |
1-38342 1 day |
| 33775 |
alreadydone author:alreadydone |
chore(Algebra): deduplicate `IsReduced` lemmas |
Replace the less general versions (assuming `NoZeroDivisors`) under the root namespace by more general versions assuming `IsReduced`, and deprecate the versions under `IsReduced` namespace.
---
[](https://gitpod.io/from-referrer/)
|
t-algebra label:t-algebra$ |
95/107 |
Mathlib/Algebra/GroupWithZero/Basic.lean,Mathlib/Algebra/GroupWithZero/Torsion.lean,Mathlib/AlgebraicGeometry/EllipticCurve/Weierstrass.lean,Mathlib/LinearAlgebra/Matrix/GeneralLinearGroup/FinTwo.lean,Mathlib/RingTheory/MvPolynomial/MonomialOrder.lean,Mathlib/RingTheory/Nilpotent/Defs.lean |
6 |
1 |
['github-actions'] |
nobody |
1-37724 1 day ago |
1-42463 1 day ago |
1-42438 1 day |
| 33697 |
artie2000 author:artie2000 |
feat(FieldTheory): real closed field |
* Define real closed fields
* Prove some very basic properties
---
[](https://gitpod.io/from-referrer/)
|
t-algebra label:t-algebra$ |
117/0 |
Mathlib.lean,Mathlib/FieldTheory/IsRealClosed/Basic.lean |
2 |
34 |
['artie2000', 'github-actions', 'vihdzp'] |
nobody |
1-36325 1 day ago |
2-38522 2 days ago |
3-8112 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'] |
kmill assignee:kmill |
1-35958 1 day ago |
5-15816 5 days ago |
50-31208 50 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'] |
erdOne assignee:erdOne |
1-35955 1 day ago |
4-64445 4 days ago |
25-79900 25 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 |
18-18283 18 days ago |
18-29883 18 days ago |
18-29923 18 days |
| 33582 |
urkud author:urkud |
feat(ContDiffHolder/Moreira): define $C^{k+(α)}$ maps |
From https://github.com/urkud/SardMoreira
---
[](https://gitpod.io/from-referrer/)
|
t-analysis |
288/0 |
Mathlib.lean,Mathlib/Analysis/Calculus/ContDiffHolder/Moreira.lean,Mathlib/Analysis/SpecialFunctions/Pow/Asymptotics.lean,docs/references.bib |
4 |
1 |
['github-actions'] |
ADedecker assignee:ADedecker |
1-35949 1 day ago |
5-26093 5 days ago |
5-26135 5 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'] |
alreadydone and mariainesdff assignee:alreadydone assignee:mariainesdff |
1-35945 1 day ago |
4-65362 4 days ago |
4-65407 4 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'] |
mattrobball assignee:mattrobball |
1-35943 1 day ago |
4-62737 4 days ago |
4-62775 4 days |
| 33635 |
plp127 author:plp127 |
feat(Tactic/Set): use `binderIdent` instead of `ident` |
This let both `a` and `h` be replaced with `_` in the syntax `set a := val with ← h`
---
[](https://gitpod.io/from-referrer/)
|
t-meta |
16/2 |
Mathlib/Tactic/Set.lean,MathlibTest/Set.lean |
2 |
3 |
['JovanGerb', 'github-actions', 'plp127'] |
kim-em assignee:kim-em |
1-35941 1 day ago |
4-44244 4 days ago |
4-44224 4 days |
| 33636 |
mcdoll author:mcdoll |
feat(Analysis/Distribution): the Laplacian on Schwartz functions |
We introduce a notation type-class for the Laplacian, change the definition of `InnerProductSpace.laplacian` to `Laplacian.laplacian` and define the Laplacian using the sum of second derivatives on Schwartz functions.
We define an abstract Laplacian for any space with `LineDeriv` in order to avoid duplication for other function spaces (in particular, this will be reused for the tempered distribution Laplacian).
---
[](https://gitpod.io/from-referrer/)
|
t-analysis |
197/12 |
Mathlib.lean,Mathlib/Analysis/Distribution/DerivNotation.lean,Mathlib/Analysis/Distribution/Laplacian.lean,Mathlib/Analysis/Distribution/SchwartzSpace.lean,Mathlib/Analysis/InnerProductSpace/Harmonic/Basic.lean,Mathlib/Analysis/InnerProductSpace/Laplacian.lean |
6 |
3 |
['github-actions', 'mcdoll'] |
urkud assignee:urkud |
1-35940 1 day ago |
4-41599 4 days ago |
4-41642 4 days |
| 33637 |
themathqueen author:themathqueen |
feat(Analysis/Matrix/Order): `det (abs A) = |det A|` and `det (sqrt A) = √(det A)` |
... for Hermitian and positive semi-definite, respectively.
---
[](https://gitpod.io/from-referrer/)
|
t-analysis |
22/4 |
Mathlib/Analysis/Matrix/HermitianFunctionalCalculus.lean,Mathlib/Analysis/Matrix/Order.lean,Mathlib/Data/Real/Sqrt.lean |
3 |
3 |
['github-actions', 'themathqueen'] |
sgouezel assignee:sgouezel |
1-35939 1 day ago |
4-38895 4 days ago |
4-38937 4 days |
| 33757 |
fpvandoorn author:fpvandoorn |
feat: remove decidability instances on sets or ideals |
* We have the rule that you should assume decidability instead of opening the classical locale. However, in places where there cannot ever be a reasonable decidable instance, I think we can relax this rule.
* This PR updates the corresponding library note, and removes `DecidableEq` instances on `Set` and `Ideal`
* This looks a lot cleaner IMO, and the decidability assumptions are silly: assuming that `Set α` has decidable for an inhabited type `α` is equivalent to assuming that all propositions are decidable. Similarly for `Ideal R` for a nontrivial ring `R`.
* This has one downside: if a lemma uses classical logic to infer decidability for its statement, then all lemmas that use this lemma also have to do this, otherwise they will deal with decidability type mismatches
---
This was motivated by seeing some code from @mariainesdff's repos with such decidability arguments. @mariainesdff, do you think this PR would make your code a bit nicer?
[](https://gitpod.io/from-referrer/)
|
|
57/32 |
Mathlib/Algebra/Module/DedekindDomain.lean,Mathlib/Algebra/Module/PID.lean,Mathlib/Logic/Basic.lean,Mathlib/MeasureTheory/SetSemiring.lean,Mathlib/NumberTheory/RamificationInertia/Basic.lean,Mathlib/Order/PartialSups.lean,Mathlib/RingTheory/DedekindDomain/Factorization.lean,Mathlib/RingTheory/DedekindDomain/Ideal/Lemmas.lean,Mathlib/RingTheory/Ideal/Basic.lean,Mathlib/RingTheory/Invariant/Basic.lean,Mathlib/RingTheory/Lasker.lean,Mathlib/RingTheory/Valuation/ValuationRing.lean |
12 |
5 |
['github-actions', 'plp127', 'vihdzp'] |
nobody |
1-35676 1 day ago |
1-73634 1 day ago |
1-73607 1 day |
| 33771 |
plp127 author:plp127 |
feat: prove `Prod.wellFoundedLT` directly |
Prove `Prod.wellFoundedLT` without going through `Antisymmetrization`. This makes the instance accessible without having to import antisymmetrization.
---
[](https://gitpod.io/from-referrer/)
|
t-order |
19/26 |
Mathlib/Algebra/Lie/Weights/Basic.lean,Mathlib/GroupTheory/Solvable.lean,Mathlib/GroupTheory/SpecificGroups/ZGroup.lean,Mathlib/Order/Antisymmetrization.lean,Mathlib/Order/RelClasses.lean |
5 |
4 |
['alreadydone', 'github-actions', 'plp127', 'vihdzp'] |
nobody |
1-32609 1 day ago |
1-46441 1 day ago |
1-46481 1 day |
| 33784 |
tb65536 author:tb65536 |
refactor(Topology/Irreducible): weaken assumptions of `preimage_mem_irreducibleComponents_of_isPreirreducible_fiber` |
This PR weakens the surjectivity assumption of `preimage_mem_irreducibleComponents_of_isPreirreducible_fiber` to `(t ∩ Set.range f).Nonempty`. I also took the liberty of systematizing the file slightly, so that now there are 6 lemmas: preimage of (preirreducible / irreducible / irreducible component) assuming (preirreducible fibers / open embedding).
---
[](https://gitpod.io/from-referrer/)
|
t-topology |
36/26 |
Mathlib/Topology/Irreducible.lean |
1 |
1 |
['github-actions'] |
nobody |
1-32453 1 day ago |
1-32453 1 day ago |
1-32427 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 deprecate `AddMonoidHom.smulLeft` (same situation) and generalize `DistribMulAction.toLinearMap`
---
- [x] depends on: #33721
[](https://gitpod.io/from-referrer/)
|
t-algebra label:t-algebra$ |
111/99 |
Mathlib/Algebra/Algebra/Hom.lean,Mathlib/Algebra/Algebra/Tower.lean,Mathlib/Algebra/BigOperators/Finprod.lean,Mathlib/Algebra/Category/ModuleCat/Tannaka.lean,Mathlib/Algebra/DirectSum/Algebra.lean,Mathlib/Algebra/GroupWithZero/Action/Basic.lean,Mathlib/Algebra/GroupWithZero/Action/Defs.lean,Mathlib/Algebra/GroupWithZero/Action/End.lean,Mathlib/Algebra/Module/Basic.lean,Mathlib/Algebra/Module/Equiv/Basic.lean,Mathlib/Algebra/Module/Hom.lean,Mathlib/Algebra/Module/LinearMap/Defs.lean,Mathlib/Algebra/Module/LinearMap/End.lean,Mathlib/Algebra/Module/Rat.lean,Mathlib/Algebra/Module/Submodule/Invariant.lean,Mathlib/Algebra/Module/Submodule/Pointwise.lean,Mathlib/Algebra/Module/Torsion/Basic.lean,Mathlib/Algebra/Polynomial/HasseDeriv.lean,Mathlib/Algebra/QuadraticAlgebra/NormDeterminant.lean,Mathlib/Algebra/Ring/Action/Basic.lean,Mathlib/Analysis/SpecialFunctions/Gamma/BohrMollerup.lean,Mathlib/LinearAlgebra/AffineSpace/Pointwise.lean,Mathlib/LinearAlgebra/BilinearMap.lean,Mathlib/LinearAlgebra/Matrix/ToLin.lean,Mathlib/LinearAlgebra/TensorProduct/Basic.lean,Mathlib/LinearAlgebra/TensorProduct/Graded/External.lean,Mathlib/RingTheory/DiscreteValuationRing/TFAE.lean,Mathlib/RingTheory/FractionalIdeal/Basic.lean,Mathlib/RingTheory/IntegralClosure/Algebra/Basic.lean,Mathlib/RingTheory/Jacobson/Ideal.lean,Mathlib/RingTheory/Morita/Matrix.lean,Mathlib/RingTheory/Regular/IsSMulRegular.lean,Mathlib/Topology/Algebra/InfiniteSum/Module.lean,Mathlib/Topology/Algebra/Ring/Real.lean,Mathlib/Topology/Algebra/UniformMulAction.lean |
35 |
2 |
['github-actions', 'mathlib4-dependent-issues-bot'] |
nobody |
1-32316 1 day ago |
2-44287 2 days ago |
2-44261 2 days |
| 33542 |
yuanyi-350 author:yuanyi-350 |
feat(integral): Error Estimation for the Rectangle Rule in Numerical Integration |
---
[](https://gitpod.io/from-referrer/)
|
t-analysis |
113/0 |
Mathlib.lean,Mathlib/Analysis/Calculus/ContDiff/Defs.lean,Mathlib/Analysis/Calculus/Midpoint.lean |
3 |
1 |
['github-actions'] |
nobody |
1-31397 1 day ago |
1-31424 1 day ago |
1-31447 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
|
757/0 |
Mathlib.lean,Mathlib/Dynamics/SymbolicDynamics/Basic.lean,Mathlib/Tactic/Translate/ToAdditive.lean |
3 |
157 |
['Sfgangloff', 'eric-wieser', 'github-actions', 'kckennylau', 'mathlib4-merge-conflict-bot', 'sgouezel'] |
sgouezel assignee:sgouezel |
1-29517 1 day ago |
1-29534 1 day ago |
88-63726 88 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
|
486/0 |
Mathlib.lean,Mathlib/Analysis/DiscreteConvolution/Basic.lean |
2 |
11 |
['IlPreteRosso', 'github-actions', 'j-loreaux'] |
urkud assignee:urkud |
1-27341 1 day ago |
3-18179 3 days ago |
10-12549 10 days |
| 32744 |
NoneMore author:NoneMore |
feat(ModelTheory/Definablity): add `DefinableFun` definition and lemmas |
This PR adds two basic shapes of definable sets and `DefinableFun` definition with relevant lemmas.
The main result is `Set.Definable.preimage_of_map` asserting that the preimage of a definable set under a definable map is definable.
There are also some tool lemmas derived by the preimage lemma.
---
[](https://gitpod.io/from-referrer/)
|
t-logic
new-contributor
|
147/0 |
Mathlib/ModelTheory/Definability.lean |
1 |
59 |
['NoneMore', 'github-actions', 'mathlib4-merge-conflict-bot', 'staroperator'] |
fpvandoorn assignee:fpvandoorn |
1-15199 1 day ago |
1-15223 1 day ago |
29-14424 29 days |
| 31325 |
joelriou author:joelriou |
feat(AlgebraicTopology): a computable monoidal functor instance for `hoFunctor` |
We construct a computable equivalence of categories `(X ⊗ Y).HomotopyCategory ≌ X.HomotopyCategory × Y.HomotopyCategory` for `2`-truncated simplicial sets `X` and `Y`. This allows to make the bicategory instance on quasicategories computable.
---
- [x] depends on: #33201
- [x] depends on: #31174
- [x] depends on: #31250
- [x] depends on: #31254
- [x] depends on: #31274
- [x] depends on: #31265
[](https://gitpod.io/from-referrer/)
|
maintainer-merge
t-algebraic-topology
|
298/28 |
Mathlib/AlgebraicTopology/Quasicategory/StrictBicategory.lean,Mathlib/AlgebraicTopology/SimplicialSet/HoFunctorMonoidal.lean,Mathlib/AlgebraicTopology/SimplicialSet/NerveAdjunction.lean |
3 |
17 |
['github-actions', 'joelriou', 'mathlib4-dependent-issues-bot', 'mathlib4-merge-conflict-bot', 'robin-carlier'] |
robin-carlier assignee:robin-carlier |
1-6379 1 day ago |
1-6379 1 day ago |
14-52851 14 days |
| 33787 |
LTolDe author:LTolDe |
doc(Topology/Baire/BaireMeasurable): add naming convention for notation `residualEq` |
---
[](https://gitpod.io/from-referrer/)
|
easy
t-topology
new-contributor
|
2/1 |
Mathlib/Topology/Baire/BaireMeasurable.lean |
1 |
2 |
['LTolDe', 'github-actions'] |
nobody |
1-2281 1 day ago |
1-2281 1 day ago |
1-2371 1 day |
| 33714 |
idontgetoutmuch author:idontgetoutmuch |
Riemannian metrics exist II |
Supersedes https://github.com/leanprover-community/mathlib4/pull/33519
---
[](https://gitpod.io/from-referrer/)
|
t-differential-geometry
new-contributor
|
1269/0 |
Mathlib.lean,Mathlib/Geometry/Manifold/ExistsRiemannianMetricTangentSpace.lean,Mathlib/Geometry/Manifold/PartitionOfUnity.lean |
3 |
3 |
['github-actions', 'grunweg', 'idontgetoutmuch'] |
nobody |
1-235 1 day ago |
2-3857 2 days ago |
2-76140 2 days |
| 33555 |
erdOne author:erdOne |
feat(RingTheory): standard smooth = etale over mvpolynomial |
---
[](https://gitpod.io/from-referrer/)
|
large-import |
79/2 |
Mathlib/Algebra/MvPolynomial/Equiv.lean,Mathlib/Algebra/MvPolynomial/PDeriv.lean,Mathlib/RingTheory/RingHom/StandardSmooth.lean |
3 |
3 |
['erdOne', 'github-actions', 'robin-carlier'] |
robin-carlier assignee:robin-carlier |
1-102 1 day ago |
5-57040 5 days ago |
5-57074 5 days |
| 32795 |
fpvandoorn author:fpvandoorn |
fix: restrict abv positivity extension to variable functions |
* Restrict the `evalAbv` positivity extension to only apply to variable functions.
Note: this extension is called on *all* applications, and uses type-class inference to see whether it applies
* Fix a bug in `evalAbs`, which would return `.none`, even when it could return `.nonneg`.
* Originally hoped that this would improve performance, but that does not seem to be the case.
---
[](https://gitpod.io/from-referrer/)
|
t-meta
t-algebra
label:t-algebra$ |
8/2 |
Mathlib/Algebra/Order/AbsoluteValue/Basic.lean,Mathlib/Analysis/Normed/Algebra/GelfandMazur.lean,Mathlib/Tactic/Positivity/Basic.lean |
3 |
8 |
['JovanGerb', 'fpvandoorn', 'github-actions', 'leanprover-radar'] |
joneugster assignee:joneugster |
0-85651 23 hours ago |
2-58196 2 days ago |
12-47595 12 days |
| 33788 |
harahu author:harahu |
chore(Algebra): move `LinearMap.ker_restrictScalars` |
Resolve an old TODO by moving `LinearMap.ker_restrictScalars` to a location in `Mathlib/Algebra/Module/Submodule`.
The TODO referenced lemmas in plural, but only `LinearMap.ker_restrictScalars` seemed to fit. I assume any other lemmas might already have been moved at an earlier point.
---
Notes for reviewers:
- The new location in `Mathlib/Algebra/Module/Submodule/Ker.lean` was chosen somewhat arbitrarily in favor of `Mathlib/Algebra/Module/Submodule/RestrictScalars.lean`. Please consider whether `Ker.lean` is the optimal location for this lemma.
- I haven't moved content in mathlib before – do I need to add a deprecation alias in the original file, or is the way I've done it fine?
[](https://gitpod.io/from-referrer/)
|
t-algebra label:t-algebra$ |
14/17 |
Mathlib/Algebra/Algebra/Basic.lean,Mathlib/Algebra/Module/Submodule/Ker.lean |
2 |
1 |
['github-actions'] |
nobody |
0-84575 23 hours ago |
0-84575 23 hours ago |
1-1430 1 day |
| 33129 |
Paul-Lez author:Paul-Lez |
feat(Tactic/Simproc/VecPerm): Add simproc for permuting entries of a vector |
---
[](https://gitpod.io/from-referrer/)
|
t-meta |
127/0 |
Mathlib.lean,Mathlib/Tactic.lean,Mathlib/Tactic/Simproc/VecPerm.lean,MathlibTest/Simproc/VecPerm.lean |
4 |
9 |
['JovanGerb', 'Paul-Lez', 'github-actions', 'ocfnash'] |
thorimur assignee:thorimur |
0-83737 23 hours ago |
20-65432 20 days ago |
20-68461 20 days |
| 32481 |
ADedecker author:ADedecker |
feat: add `PolynormableSpace.banach_steinhaus` |
---
- [x] depends on: #32480
[](https://gitpod.io/from-referrer/)
|
t-analysis |
121/24 |
Mathlib/Analysis/LocallyConvex/AbsConvexOpen.lean,Mathlib/Analysis/LocallyConvex/Barrelled.lean,Mathlib/Analysis/LocallyConvex/WithSeminorms.lean,Mathlib/Analysis/Normed/Operator/BanachSteinhaus.lean |
4 |
2 |
['github-actions', 'mathlib4-dependent-issues-bot'] |
sgouezel assignee:sgouezel |
0-82575 22 hours ago |
2-55507 2 days ago |
2-56781 2 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 |
11-84660 11 days ago |
13-81685 13 days ago |
13-81725 13 days |
| 33770 |
eric-wieser author:eric-wieser |
chore(RingTheory/Morita/Matrix): remove uses of `default` |
Using `default` here just makes the spelling longer and less general. The docstring already say `Eᵢᵢ`, so these functions should take `i`.
---
[](https://gitpod.io/from-referrer/)
|
t-ring-theory |
23/22 |
Mathlib/RingTheory/Morita/Matrix.lean |
1 |
1 |
['github-actions'] |
nobody |
0-77156 21 hours ago |
1-48893 1 day ago |
1-48868 1 day |
| 33767 |
Whysoserioushah author:Whysoserioushah |
chore(RingTheory/Morita/Matrix): Finish the morita equivalence between matrix ring and the ring itself |
---
[](https://gitpod.io/from-referrer/)
|
large-import
t-ring-theory
|
79/1 |
Mathlib/RingTheory/Morita/Matrix.lean |
1 |
11 |
['Whysoserioushah', 'eric-wieser', 'github-actions'] |
nobody |
0-76915 21 hours ago |
1-61859 1 day ago |
1-61898 1 day |
| 33761 |
ooovi author:ooovi |
feat(Algebra/Module/Submodule): behaviour of `restrictScalars` under lattice operations |
Add lemmas about how `restrictScalars` interacts with `sup`, `inf`, `sSup`, `sInf`, `iSup` and `iInf`.
Co-authored-by: Martin Winter
---
We need this for https://github.com/leanprover-community/mathlib4/pull/33664.
[](https://gitpod.io/from-referrer/)
|
t-algebra label:t-algebra$ |
44/3 |
Mathlib/Algebra/Module/Submodule/RestrictScalars.lean,Mathlib/RingTheory/Ideal/Maps.lean |
2 |
7 |
['YaelDillies', 'eric-wieser', 'github-actions', 'ooovi'] |
nobody |
0-76557 21 hours ago |
1-66009 1 day ago |
1-68693 1 day |
| 33613 |
DavidLedvinka author:DavidLedvinka |
feat(Probability): `UniformOn_univ_instIsProbabilityMeasure` |
It is convenient to have an instance of `IsProbabilityMeasure` on a uniform distribution on `.univ` (to avoid the need for `haveI` statements). There is perhaps an argument for `abbrev uniform := uniformOn (.univ : Set Ω)` but I have not implemented this in this PR. |
t-measure-probability |
11/0 |
Mathlib/Probability/UniformOn.lean |
1 |
5 |
['DavidLedvinka', 'Ruben-VandeVelde', 'github-actions'] |
nobody |
0-76041 21 hours ago |
0-76041 21 hours ago |
2-74147 2 days |
| 31706 |
Thmoas-Guan author:Thmoas-Guan |
feat(Algebra/ModuleCat): `ModuleCat.uliftFunctor` |
Add `ModuleCat.uliftFunctor`
---
[](https://gitpod.io/from-referrer/)
|
t-algebra
maintainer-merge
label:t-algebra$ |
108/0 |
Mathlib.lean,Mathlib/Algebra/Category/ModuleCat/Ulift.lean |
2 |
20 |
['Thmoas-Guan', 'dagurtomas', 'erdOne', 'github-actions', 'mathlib4-merge-conflict-bot', 'robin-carlier'] |
mattrobball assignee:mattrobball |
0-75299 20 hours ago |
0-75299 20 hours ago |
23-65621 23 days |
| 33793 |
LTolDe author:LTolDe |
feat(MeasureTheory/Constructions/Polish/Basic): add lemma AnalyticSet.inter_nonempty_of_nowhereMeagre |
add lemma AnalyticSet.inter_nonempty_of_nowhereMeagre, the main ingredient for the proof of the **Effros' Theorem**, see [#mathlib4 > Effros Theorem](https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/Effros.20Theorem/with/566543328)
introduce definition of a nowhere meagre set
---
[](https://gitpod.io/from-referrer/)
|
new-contributor |
37/0 |
Mathlib/MeasureTheory/Constructions/Polish/Basic.lean,Mathlib/Order/Filter/Basic.lean,Mathlib/Topology/GDelta/Basic.lean |
3 |
1 |
['github-actions'] |
nobody |
0-74755 20 hours ago |
0-74854 20 hours ago |
0-74876 20 hours |
| 33403 |
xroblot author:xroblot |
feat(GroupTheory/FiniteAbelian): prove that the restriction map is surjective |
Let `G` be a finite commutative group and let `H` be a subgroup. If `M` is a commutative monoid
such that `G →* Mˣ` and `H →* Mˣ` are both finite (this is the case for example if `M` is a
commutative domain), then any homomorphism `H →* Mˣ` can be extended to an homomorphism `G →* Mˣ`.
---
[](https://gitpod.io/from-referrer/)
|
t-group-theory |
90/13 |
Mathlib/Algebra/Group/Submonoid/Operations.lean,Mathlib/GroupTheory/Exponent.lean,Mathlib/GroupTheory/FiniteAbelian/Duality.lean,Mathlib/GroupTheory/QuotientGroup/Basic.lean,Mathlib/NumberTheory/MulChar/Duality.lean,Mathlib/RingTheory/RootsOfUnity/Basic.lean |
6 |
7 |
['Ruben-VandeVelde', 'github-actions', 'xroblot'] |
urkud assignee:urkud |
0-74199 20 hours ago |
0-74199 20 hours ago |
10-83002 10 days |
| 33531 |
harahu author:harahu |
doc(CategoryTheory): fix typos |
Fix typos and staleness in docs. The issues were found and corrected by Codex.
---
[](https://gitpod.io/from-referrer/)
|
t-category-theory
maintainer-merge
|
210/208 |
Mathlib/CategoryTheory/Abelian/Basic.lean,Mathlib/CategoryTheory/Abelian/DiagramLemmas/Four.lean,Mathlib/CategoryTheory/Abelian/DiagramLemmas/KernelCokernelComp.lean,Mathlib/CategoryTheory/Abelian/Exact.lean,Mathlib/CategoryTheory/Abelian/Ext.lean,Mathlib/CategoryTheory/Abelian/FreydMitchell.lean,Mathlib/CategoryTheory/Abelian/GrothendieckAxioms/Connected.lean,Mathlib/CategoryTheory/Abelian/GrothendieckAxioms/FunctorCategory.lean,Mathlib/CategoryTheory/Abelian/GrothendieckCategory/ColimCoyoneda.lean,Mathlib/CategoryTheory/Abelian/GrothendieckCategory/Subobject.lean,Mathlib/CategoryTheory/Abelian/Injective/Basic.lean,Mathlib/CategoryTheory/Abelian/Monomorphisms.lean,Mathlib/CategoryTheory/Abelian/NonPreadditive.lean,Mathlib/CategoryTheory/Abelian/Opposite.lean,Mathlib/CategoryTheory/Abelian/Projective/Ext.lean,Mathlib/CategoryTheory/Abelian/Projective/Extend.lean,Mathlib/CategoryTheory/Abelian/Projective/Resolution.lean,Mathlib/CategoryTheory/Abelian/Pseudoelements.lean,Mathlib/CategoryTheory/Abelian/Refinements.lean,Mathlib/CategoryTheory/Abelian/SerreClass/Basic.lean,Mathlib/CategoryTheory/Action/Basic.lean,Mathlib/CategoryTheory/Action/Limits.lean,Mathlib/CategoryTheory/Adjunction/Evaluation.lean,Mathlib/CategoryTheory/Bicategory/Adjunction/Basic.lean,Mathlib/CategoryTheory/Bicategory/Functor/Cat/ObjectProperty.lean,Mathlib/CategoryTheory/Bicategory/Functor/Lax.lean,Mathlib/CategoryTheory/Bicategory/Functor/LocallyDiscrete.lean,Mathlib/CategoryTheory/Bicategory/Functor/Prelax.lean,Mathlib/CategoryTheory/Bicategory/Functor/StrictlyUnitary.lean,Mathlib/CategoryTheory/Bicategory/LocallyGroupoid.lean,Mathlib/CategoryTheory/Bicategory/NaturalTransformation/Oplax.lean,Mathlib/CategoryTheory/Bicategory/Product.lean,Mathlib/CategoryTheory/CatCommSq.lean,Mathlib/CategoryTheory/Category/ULift.lean,Mathlib/CategoryTheory/Comma/CardinalArrow.lean,Mathlib/CategoryTheory/Comma/Presheaf/Basic.lean,Mathlib/CategoryTheory/ComposableArrows/Basic.lean,Mathlib/CategoryTheory/ConcreteCategory/Basic.lean,Mathlib/CategoryTheory/Core.lean,Mathlib/CategoryTheory/Enriched/Basic.lean,Mathlib/CategoryTheory/Enriched/Limits/HasConicalPullbacks.lean,Mathlib/CategoryTheory/FiberedCategory/Fiber.lean,Mathlib/CategoryTheory/FinCategory/AsType.lean,Mathlib/CategoryTheory/Functor/KanExtension/Basic.lean,Mathlib/CategoryTheory/Functor/ReflectsIso/Balanced.lean,Mathlib/CategoryTheory/Functor/Trifunctor.lean,Mathlib/CategoryTheory/Galois/Basic.lean,Mathlib/CategoryTheory/Galois/GaloisObjects.lean,Mathlib/CategoryTheory/Galois/Prorepresentability.lean,Mathlib/CategoryTheory/Generator/Basic.lean,Mathlib/CategoryTheory/GradedObject/Bifunctor.lean,Mathlib/CategoryTheory/GradedObject/Trifunctor.lean,Mathlib/CategoryTheory/Groupoid/Subgroupoid.lean,Mathlib/CategoryTheory/Groupoid/VertexGroup.lean,Mathlib/CategoryTheory/Idempotents/FunctorExtension.lean,Mathlib/CategoryTheory/IsomorphismClasses.lean,Mathlib/CategoryTheory/Limits/ConcreteCategory/WithAlgebraicStructures.lean,Mathlib/CategoryTheory/Limits/Constructions/Equalizers.lean,Mathlib/CategoryTheory/Limits/Creates.lean,Mathlib/CategoryTheory/Limits/ExactFunctor.lean,Mathlib/CategoryTheory/Limits/FilteredColimitCommutesFiniteLimit.lean,Mathlib/CategoryTheory/Limits/FintypeCat.lean,Mathlib/CategoryTheory/Limits/FormalCoproducts.lean,Mathlib/CategoryTheory/Limits/FunctorCategory/Shapes/Pullbacks.lean,Mathlib/CategoryTheory/Limits/MonoCoprod.lean,Mathlib/CategoryTheory/Limits/Preorder.lean,Mathlib/CategoryTheory/Limits/Preserves/Shapes/Images.lean,Mathlib/CategoryTheory/Limits/Preserves/Shapes/Pullbacks.lean,Mathlib/CategoryTheory/Limits/Preserves/Shapes/Square.lean,Mathlib/CategoryTheory/Limits/Shapes/ConcreteCategory.lean,Mathlib/CategoryTheory/Limits/Shapes/Images.lean,Mathlib/CategoryTheory/Limits/Shapes/Opposites/Filtered.lean,Mathlib/CategoryTheory/Limits/Shapes/Preorder/PrincipalSeg.lean,Mathlib/CategoryTheory/Limits/Shapes/Preorder/WellOrderContinuous.lean,Mathlib/CategoryTheory/Limits/Shapes/Pullback/PullbackCone.lean,Mathlib/CategoryTheory/Limits/Shapes/Pullback/Square.lean,Mathlib/CategoryTheory/Limits/Shapes/Reflexive.lean,Mathlib/CategoryTheory/Limits/Shapes/RegularMono.lean,Mathlib/CategoryTheory/Limits/Shapes/SplitCoequalizer.lean,Mathlib/CategoryTheory/Limits/Shapes/WidePullbacks.lean,Mathlib/CategoryTheory/Limits/Types/ColimitType.lean,Mathlib/CategoryTheory/Limits/Types/ColimitTypeFiltered.lean,Mathlib/CategoryTheory/Limits/Types/Pushouts.lean,Mathlib/CategoryTheory/Linear/Yoneda.lean,Mathlib/CategoryTheory/Localization/Construction.lean,Mathlib/CategoryTheory/Localization/DerivabilityStructure/Basic.lean,Mathlib/CategoryTheory/Localization/DerivabilityStructure/OfFunctorialResolutions.lean,Mathlib/CategoryTheory/Localization/Predicate.lean,Mathlib/CategoryTheory/Localization/Quotient.lean,Mathlib/CategoryTheory/Monoidal/Action/LinearFunctor.lean,Mathlib/CategoryTheory/Monoidal/Braided/Basic.lean,Mathlib/CategoryTheory/Monoidal/Closed/Basic.lean,Mathlib/CategoryTheory/Monoidal/Closed/FunctorCategory/Groupoid.lean,Mathlib/CategoryTheory/Monoidal/Conv.lean,Mathlib/CategoryTheory/Monoidal/DayConvolution.lean,Mathlib/CategoryTheory/Monoidal/DayConvolution/DayFunctor.lean,Mathlib/CategoryTheory/Monoidal/Discrete.lean,Mathlib/CategoryTheory/Monoidal/Limits/Preserves.lean,Mathlib/CategoryTheory/MorphismProperty/Composition.lean,Mathlib/CategoryTheory/MorphismProperty/Concrete.lean |
132 |
16 |
['github-actions', 'harahu', 'jcommelin', 'joelriou', 'robin-carlier'] |
jcommelin assignee:jcommelin |
0-72495 20 hours ago |
0-78954 21 hours ago |
6-40268 6 days |
| 32403 |
FLDutchmann author:FLDutchmann |
fix(FieldSimp): `declaration has free variables` kernel errors |
Fix a bug in `field_simp` that produces a `(kernel) declaration has free variables '_example'` error which was caused by a misconfigured `simp` call.
---
The first new test produces this error on the current version of mathlib. What I believe is happening is that the discharger is using the `x != 0` hypothesis in the `then` branch, at which point that result is cached by `simp` and used in the `else` branch.
```
import Mathlib
/- (kernel) declaration has free variables '_example' -/
example {x y : ℚ}: (if x ≠ 0 then x / x else x / x) = 1 := by
field_simp
/- ⊢ (if x ≠ 0 then 1 else 1) = 1 -/
sorry
```
Edit: As @__JovanGerb__ pointed out, the correct solution was to set the `wellBehavedDischarge` flag to false, so that `simp` clears the cache more agressively. We might also want to turn on `contextual` in the future, but this would change the behaviour of `field_simp` by adding additional lemmas to the simp context. For now I propose a fix with a minimal change in behaviour.
Marking the simp context that calls the discharger as contextual appears to fix the issue, presumably by more aggressively pruning the cache. What I don't understand at this point, is why the discharger ever even had access to that hypothesis, given that contextual was set to false.
cc @JovanGerb : You understand the simp cache much better than I. Is there another bug here that I'm missing?
[](https://gitpod.io/from-referrer/)
|
t-meta |
55/14 |
Mathlib/Tactic/Abel.lean,Mathlib/Tactic/FieldSimp.lean,Mathlib/Tactic/Ring/RingNF.lean,Mathlib/Util/AtomM/Recurse.lean,MathlibTest/FieldSimp.lean |
5 |
18 |
['FLDutchmann', 'JovanGerb', 'github-actions', 'grunweg', 'leanprover-radar'] |
nobody |
0-72124 20 hours ago |
0-72845 20 hours ago |
22-54157 22 days |
| 33786 |
hdmkindom author:hdmkindom |
feat(Analysis/Matrix): add Jacobian matrix for matrix-valued functions |
This PR introduces the Jacobian matrix for matrix-valued functions `F : Matrix m n ℝ → Matrix p q ℝ`.
The Jacobian matrix `jacobianMatrix F X` at point `X` is indexed by `(p × q) × (m × n)`, where each entry represents the partial derivative with respect to a basis element. To handle instance-mismatch issues with matrix norms, we use local Frobenius norm instances.
mkdir Analysis/Matrix/Jacobian.lean
## Main definitions
- `jacobianMatrix F X`: The Jacobian matrix at point `X`, defined by `jacobianMatrix F X (i, k) (j, l) = (fderiv ℝ F X (Matrix.single j l 1)) i k`
## Main theorems
- `fderiv_eq_jacobian_mul`: Express the Fréchet derivative as a contraction with the Jacobian
- `jacobianMatrix_comp`: Chain rule for Jacobian matrices
- `jacobianMatrix_linear`, `jacobianMatrix_id`, `jacobianMatrix_const`: Basic properties
- `jacobianMatrix_add`, `jacobianMatrix_smul`: Linearity properties
|
t-analysis
new-contributor
|
219/0 |
Mathlib.lean,Mathlib/Analysis/Matrix/Jacobian.lean |
2 |
1 |
['github-actions'] |
nobody |
0-71467 19 hours ago |
1-20776 1 day ago |
1-20813 1 day |
| 33113 |
sinhp author:sinhp |
feat(Category Theory): A natural isomorphism connecting Over.iteratedSlice and Over.map |
This PR provides the following useful nat iso:
```
def iteratedSliceForwardNaturalityIso {g : Over X} (p : f ⟶ g) :
iteratedSliceForward f ⋙ Over.map p.left ≅ Over.map p ⋙ iteratedSliceForward g := ...
def iteratedSliceEquivOverMapIso {f g : Over X} (p : f ⟶ g) :
f.iteratedSliceForward ⋙ Over.map p.left ⋙ g.iteratedSliceBackward ≅ Over.map p := ...
```
And it proves `post forget` is the same thing as `iteratedSliceForward`, thereby unlocking api of `Over.post` for iterated slice functor.
---
[](https://gitpod.io/from-referrer/)
|
t-category-theory
maintainer-merge
|
22/0 |
Mathlib/CategoryTheory/Comma/Over/Basic.lean |
1 |
12 |
['dagurtomas', 'github-actions', 'robin-carlier', 'sinhp'] |
nobody |
0-67983 18 hours ago |
0-67983 18 hours ago |
3-65760 3 days |
| 33736 |
fbarroero author:fbarroero |
feat(RingTheory/Polynomial/GaussNorm): The `gaussNorm` is an absolute value if `v` is a nonarchimedean absolute value |
We prove
```
Polynomial.gaussNorm_isAbsoluteValue {c : ℝ} {R : Type*} [Ring R] {v : AbsoluteValue R ℝ}
(hna : IsNonarchimedean v) (hc : 0 < c) : IsAbsoluteValue (gaussNorm v c)
```
---
[](https://gitpod.io/from-referrer/)
|
|
194/7 |
Mathlib/Algebra/Order/AbsoluteValue/Basic.lean,Mathlib/Algebra/Order/Ring/IsNonarchimedean.lean,Mathlib/RingTheory/Polynomial/GaussNorm.lean |
3 |
4 |
['copilot-pull-request-reviewer', 'github-actions'] |
nobody |
0-67051 18 hours ago |
0-67051 18 hours ago |
0-67035 18 hours |
| 33656 |
metakunt author:metakunt |
feat(Data/Nat/Choose): Add sum_range_multichoose |
|
t-data |
11/0 |
Mathlib/Data/Nat/Choose/Sum.lean |
1 |
6 |
['eric-wieser', 'github-actions', 'metakunt'] |
nobody |
0-66799 18 hours ago |
4-14790 4 days ago |
4-14832 4 days |
| 33797 |
SnirBroshi author:SnirBroshi |
chore(Order/Defs/Unbundled): deprecate `IsTotal` in favor of core's `Std.Total` |
---
[Mathlib's `IsTotal`](https://leanprover-community.github.io/mathlib4_docs/Mathlib/Order/Defs/Unbundled.html#IsTotal)
[Core's `Std.Total`](https://leanprover-community.github.io/mathlib4_docs/Init/Core.html#Std.Total)
[Zulip](https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/Relation.20properties.20duplication/near/544638270)
[](https://gitpod.io/from-referrer/)
|
|
121/110 |
Mathlib/Algebra/Group/Basic.lean,Mathlib/Algebra/Order/Archimedean/Class.lean,Mathlib/Algebra/Order/GroupWithZero/Canonical.lean,Mathlib/Algebra/Order/Ring/Canonical.lean,Mathlib/Data/DFinsupp/Lex.lean,Mathlib/Data/Finset/Sort.lean,Mathlib/Data/List/Sort.lean,Mathlib/Data/Multiset/Sort.lean,Mathlib/Data/Nat/PartENat.lean,Mathlib/Data/Ordmap/Invariants.lean,Mathlib/Data/Ordmap/Ordset.lean,Mathlib/Data/Prod/Basic.lean,Mathlib/Data/Real/Basic.lean,Mathlib/Data/Sigma/Lex.lean,Mathlib/Data/Sum/Order.lean,Mathlib/Logic/Encodable/Basic.lean,Mathlib/Order/Antisymmetrization.lean,Mathlib/Order/Basic.lean,Mathlib/Order/Comparable.lean,Mathlib/Order/Compare.lean,Mathlib/Order/Defs/Unbundled.lean,Mathlib/Order/Directed.lean,Mathlib/Order/Filter/FilterProduct.lean,Mathlib/Order/Lattice.lean,Mathlib/Order/PropInstances.lean,Mathlib/Order/Quotient.lean,Mathlib/Order/RelClasses.lean,Mathlib/Order/RelIso/Basic.lean,Mathlib/Order/UpperLower/CompleteLattice.lean,Mathlib/Order/WithBot.lean,Mathlib/RingTheory/Valuation/ValuationRing.lean,Mathlib/RingTheory/Valuation/ValuationSubring.lean,Mathlib/Topology/EMetricSpace/BoundedVariation.lean,Mathlib/Topology/Semicontinuity/Basic.lean |
34 |
1 |
['github-actions'] |
nobody |
0-66493 18 hours ago |
0-66559 18 hours ago |
0-66532 18 hours |
| 33551 |
metakunt author:metakunt |
feat(Data/Nat/Factorization/PrimePow): Add Nat.nontrivial_primeFactors_of_two_le_of_not_isPrimePow |
|
t-data |
6/0 |
Mathlib/Data/Nat/Factorization/PrimePow.lean |
1 |
4 |
['Ruben-VandeVelde', 'github-actions', 'metakunt'] |
nobody |
0-66320 18 hours ago |
0-66629 18 hours ago |
4-84629 4 days |
| 33538 |
JohnnyTeutonic author:JohnnyTeutonic |
feat(Data/Matrix/Cartan): non-simply-laced theorems for F and G |
B/C are left for follow-up
---
[](https://gitpod.io/from-referrer/)
|
maintainer-merge
t-data
|
13/0 |
Mathlib/Data/Matrix/Cartan.lean |
1 |
8 |
['JohnnyTeutonic', 'github-actions', 'robin-carlier'] |
nobody |
0-65754 18 hours ago |
0-65754 18 hours ago |
6-4824 6 days |
| 33221 |
stepan2698-cpu author:stepan2698-cpu |
feat: definition of an intertwining map |
Adds the definition of an intertwining map of representations, with an instance of an A-module structure. Proves that a multiplication by a central element is an intertwining map.
---
[](https://gitpod.io/from-referrer/)
|
t-algebra
new-contributor
label:t-algebra$ |
162/11 |
Mathlib.lean,Mathlib/RepresentationTheory/Intertwining.lean,Mathlib/RepresentationTheory/Subrepresentation.lean |
3 |
1 |
['github-actions'] |
ocfnash assignee:ocfnash |
0-64086 17 hours ago |
18-23352 18 days ago |
18-23392 18 days |
| 33447 |
urkud author:urkud |
feat(FundamentalGroupoid): define simply connected sets |
---
- [x] depends on: #33445
[](https://gitpod.io/from-referrer/)
|
maintainer-merge
t-algebraic-topology
|
102/21 |
Mathlib/AlgebraicTopology/FundamentalGroupoid/Product.lean,Mathlib/AlgebraicTopology/FundamentalGroupoid/SimplyConnected.lean,Mathlib/Topology/Connected/PathConnected.lean |
3 |
15 |
['github-actions', 'mathlib4-dependent-issues-bot', 'mathlib4-merge-conflict-bot', 'robin-carlier', 'urkud'] |
nobody |
0-64022 17 hours ago |
0-64022 17 hours ago |
1-61057 1 day |
| 33800 |
bryangingechen author:bryangingechen |
ci(lint_and_suggest.yml): rename job |
The previous name "Lint style" is the same as the "Lint style" job in the main CI, which is confusing.
---
[](https://gitpod.io/from-referrer/)
|
easy
CI
|
2/2 |
.github/workflows/lint_and_suggest_pr.yml |
1 |
1 |
['github-actions'] |
nobody |
0-63980 17 hours ago |
0-63988 17 hours ago |
0-64023 17 hours |
| 33795 |
alreadydone author:alreadydone |
feat(Topology/Sheaves): LocalPredicate prerequisite for étalé spaces |
---
[](https://gitpod.io/from-referrer/)
|
t-topology |
417/145 |
Mathlib/AlgebraicGeometry/Modules/Tilde.lean,Mathlib/AlgebraicGeometry/ProjectiveSpectrum/StructureSheaf.lean,Mathlib/Geometry/Manifold/Sheaf/Smooth.lean,Mathlib/Logic/Equiv/Basic.lean,Mathlib/Topology/Sheaves/LocalPredicate.lean,Mathlib/Topology/Sheaves/Sheafify.lean,Mathlib/Topology/Sheaves/Stalks.lean |
7 |
1 |
['github-actions'] |
nobody |
0-62446 17 hours ago |
0-68301 18 hours ago |
0-68276 18 hours |
| 29241 |
yoh-tanimoto author:yoh-tanimoto |
feat(Analysis/InnerProductSpace/Orthogonal): add duplicates for `ClosedSubmodule` |
add duplicates of definitions and API's for `ClosedSubmodule` in an `InnerProductSpace`.
motivation: when one considers a Hilbert space (`CompleteSpace`), it is more natural to consider `ClosedSubmodule`s. They form a complete lattice and satisfy `sup_orthogonal` #29243.
- [x] depends on: #29230 for `Lattice` `CompleteLattice` |
|
161/9 |
Mathlib/Analysis/Convex/Cone/Basic.lean,Mathlib/Analysis/Convex/Cone/Dual.lean,Mathlib/Analysis/InnerProductSpace/Orthogonal.lean,Mathlib/Topology/Algebra/Module/ClosedSubmodule.lean |
4 |
19 |
['github-actions', 'mathlib4-dependent-issues-bot', 'mathlib4-merge-conflict-bot', 'sgouezel', 'yoh-tanimoto'] |
sgouezel assignee:sgouezel |
0-62132 17 hours ago |
3-39548 3 days ago |
16-27478 16 days |
| 32984 |
artie2000 author:artie2000 |
refactor: remove order instances from `SetLike` |
* Remove order instances from `SetLike`
* Add class `IsConcreteLE` for `SetLike` instances whose map is order-preserving
See discussion at https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/Abstracting.20the.20substructure.20lattice.20construction/with/563952738
---
- [ ] depends on #33801
[](https://gitpod.io/from-referrer/)
|
t-meta
t-data
|
375/146 |
Mathlib/Algebra/Algebra/NonUnitalSubalgebra.lean,Mathlib/Algebra/Algebra/Subalgebra/Basic.lean,Mathlib/Algebra/Field/Subfield/Defs.lean,Mathlib/Algebra/Group/Subgroup/Defs.lean,Mathlib/Algebra/Group/Submonoid/Defs.lean,Mathlib/Algebra/Group/Subsemigroup/Defs.lean,Mathlib/Algebra/Lie/Subalgebra.lean,Mathlib/Algebra/Lie/Submodule.lean,Mathlib/Algebra/Module/Submodule/Defs.lean,Mathlib/Algebra/Order/Group/Cone.lean,Mathlib/Algebra/Order/Group/Ideal.lean,Mathlib/Algebra/Order/Ring/Cone.lean,Mathlib/Algebra/Order/Ring/Ordering/Defs.lean,Mathlib/Algebra/Ring/Subring/Defs.lean,Mathlib/Algebra/Ring/Subsemiring/Defs.lean,Mathlib/Algebra/Star/NonUnitalSubalgebra.lean,Mathlib/Algebra/Star/Subalgebra.lean,Mathlib/Algebra/Star/Subsemiring.lean,Mathlib/AlgebraicGeometry/AffineScheme.lean,Mathlib/AlgebraicGeometry/Cover/Open.lean,Mathlib/AlgebraicGeometry/Limits.lean,Mathlib/AlgebraicGeometry/Morphisms/Basic.lean,Mathlib/AlgebraicGeometry/Morphisms/Separated.lean,Mathlib/AlgebraicGeometry/ProjectiveSpectrum/Basic.lean,Mathlib/AlgebraicGeometry/Scheme.lean,Mathlib/AlgebraicGeometry/StructureSheaf.lean,Mathlib/Analysis/Convex/Body.lean,Mathlib/Analysis/Convex/Cone/Basic.lean,Mathlib/Analysis/Convex/Cone/Dual.lean,Mathlib/Analysis/InnerProductSpace/Projection/FiniteDimensional.lean,Mathlib/Analysis/VonNeumannAlgebra/Basic.lean,Mathlib/CategoryTheory/Groupoid/Subgroupoid.lean,Mathlib/Combinatorics/SimpleGraph/Ends/Defs.lean,Mathlib/Combinatorics/Young/YoungDiagram.lean,Mathlib/Data/Finset/Defs.lean,Mathlib/Data/SetLike/Basic.lean,Mathlib/Data/Sym/Sym2.lean,Mathlib/FieldTheory/IntermediateField/Basic.lean,Mathlib/Geometry/Convex/Cone/Basic.lean,Mathlib/Geometry/Euclidean/Sphere/Power.lean,Mathlib/Geometry/Euclidean/Sphere/Tangent.lean,Mathlib/Geometry/Manifold/ChartedSpace.lean,Mathlib/Geometry/RingedSpace/Basic.lean,Mathlib/GroupTheory/GroupAction/SubMulAction.lean,Mathlib/GroupTheory/GroupAction/SubMulAction/Combination.lean,Mathlib/GroupTheory/Sylow.lean,Mathlib/LinearAlgebra/AffineSpace/AffineSubspace/Defs.lean,Mathlib/LinearAlgebra/Projectivization/Subspace.lean,Mathlib/ModelTheory/Definability.lean,Mathlib/ModelTheory/ElementarySubstructures.lean,Mathlib/ModelTheory/Substructures.lean,Mathlib/ModelTheory/Types.lean,Mathlib/NumberTheory/NumberField/FractionalIdeal.lean,Mathlib/Order/Atoms.lean,Mathlib/Order/BooleanSubalgebra.lean,Mathlib/Order/BourbakiWitt.lean,Mathlib/Order/Closure.lean,Mathlib/Order/CompleteSublattice.lean,Mathlib/Order/Ideal.lean,Mathlib/Order/PFilter.lean,Mathlib/Order/Partition/Basic.lean,Mathlib/Order/Preorder/Chain.lean,Mathlib/Order/Sublattice.lean,Mathlib/Order/Sublocale.lean,Mathlib/Order/UpperLower/CompleteLattice.lean,Mathlib/Order/UpperLower/Relative.lean,Mathlib/RepresentationTheory/Subrepresentation.lean,Mathlib/RingTheory/DedekindDomain/Different.lean,Mathlib/RingTheory/DedekindDomain/Factorization.lean,Mathlib/RingTheory/DedekindDomain/Ideal/Basic.lean,Mathlib/RingTheory/DividedPowers/SubDPIdeal.lean,Mathlib/RingTheory/FilteredAlgebra/Basic.lean,Mathlib/RingTheory/FractionalIdeal/Basic.lean,Mathlib/RingTheory/FractionalIdeal/Extended.lean,Mathlib/RingTheory/FractionalIdeal/Inverse.lean,Mathlib/RingTheory/FractionalIdeal/Operations.lean,Mathlib/RingTheory/GradedAlgebra/Homogeneous/Ideal.lean,Mathlib/RingTheory/GradedAlgebra/Homogeneous/Submodule.lean,Mathlib/RingTheory/GradedAlgebra/Homogeneous/Subsemiring.lean,Mathlib/RingTheory/NonUnitalSubring/Defs.lean,Mathlib/RingTheory/NonUnitalSubsemiring/Defs.lean,Mathlib/RingTheory/TwoSidedIdeal/Basic.lean,Mathlib/RingTheory/Valuation/ValuationSubring.lean,Mathlib/SetTheory/Descriptive/Tree.lean,Mathlib/SetTheory/ZFC/Basic.lean,Mathlib/Topology/Algebra/Group/ClosedSubgroup.lean,Mathlib/Topology/Algebra/Module/ClosedSubmodule.lean,Mathlib/Topology/Algebra/OpenSubgroup.lean,Mathlib/Topology/CWComplex/Classical/Basic.lean,Mathlib/Topology/Category/TopCat/OpenNhds.lean,Mathlib/Topology/Sets/Closeds.lean,Mathlib/Topology/Sets/Compacts.lean,Mathlib/Topology/Sets/Opens.lean,Mathlib/Topology/Sets/Order.lean,Mathlib/Topology/Sheaves/SheafCondition/Sites.lean,Mathlib/Topology/Sheaves/Stalks.lean,Mathlib/Topology/Spectral/Prespectral.lean,MathlibTest/FBinop.lean |
98 |
29 |
['Vierkantor', 'alreadydone', 'artie2000', 'github-actions'] |
nobody |
0-60518 16 hours ago |
0-63036 17 hours ago |
22-46691 22 days |
| 33723 |
erdOne author:erdOne |
feat(Analytic): `℘'(z)² = 4 ℘(z)³ - g₂ ℘(z) - g₃` |
---
[](https://gitpod.io/from-referrer/)
|
t-analysis |
437/40 |
Mathlib/Algebra/Module/ZLattice/Basic.lean,Mathlib/Analysis/Analytic/Order.lean,Mathlib/Analysis/Calculus/ContDiff/Basic.lean,Mathlib/Analysis/Calculus/ContDiff/Operations.lean,Mathlib/Analysis/Calculus/IteratedDeriv/Defs.lean,Mathlib/Analysis/Calculus/IteratedDeriv/Lemmas.lean,Mathlib/Analysis/Meromorphic/Basic.lean,Mathlib/Analysis/Meromorphic/Order.lean,Mathlib/Analysis/SpecialFunctions/Elliptic/Weierstrass.lean,Mathlib/Analysis/SpecialFunctions/Trigonometric/Cotangent.lean,Mathlib/Geometry/Manifold/Instances/Sphere.lean |
11 |
60 |
['erdOne', 'github-actions', 'loefflerd', 'vihdzp'] |
nobody |
0-60357 16 hours ago |
0-60357 16 hours ago |
1-53198 1 day |
| 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 |
2-35954 2 days ago |
6-26025 6 days ago |
6-26063 6 days |
| 33693 |
yoh-tanimoto author:yoh-tanimoto |
feat(Mathlib/Analysis/Normed/Module): add instances of `CompleteSpace` for `Submodules` and `ClosedSubmodule` |
add an instance of `CompleteSpace` for a `Submodule` of a Banach space `[NormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [CompleteSpace E]` which `IsClosed`.
In this relation, convert a lemma showing `IsClosed` to an instance for `ClosedSubmodule`.
motivation: Together with #28709, this makes it automatic that a `ClosedSubmodule` in a Hilbert space `HasOrthogonalProjection`.
discussion: https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/.60CompleteSpace.60.20for.20closed.20subtypes.20in.20a.20.60CompleteSpace.60 |
|
10/9 |
Mathlib/Analysis/InnerProductSpace/Orthogonal.lean,Mathlib/Analysis/InnerProductSpace/l2Space.lean,Mathlib/Analysis/Normed/Module/Basic.lean,Mathlib/Topology/Algebra/Module/ClosedSubmodule.lean |
4 |
2 |
['github-actions'] |
nobody |
0-57078 15 hours ago |
3-36413 3 days ago |
3-36386 3 days |
| 32856 |
stepan2698-cpu author:stepan2698-cpu |
feat: definition of an irreducible representation |
Define irreducible monoid representations over a field and prove that a monoid representation is irreducible iff the corresponding module over the monoid algebra is simple. |
t-algebra
new-contributor
label:t-algebra$ |
129/10 |
Mathlib.lean,Mathlib/RepresentationTheory/Irreducible.lean,Mathlib/RepresentationTheory/Subrepresentation.lean |
3 |
23 |
['Whysoserioushah', 'erdOne', 'github-actions', 'stepan2698-cpu'] |
kim-em assignee:kim-em |
0-56486 15 hours ago |
27-47384 27 days ago |
27-47417 27 days |
| 33806 |
tb65536 author:tb65536 |
feat(RingTheory/Localization/Ideal): generalize `comap_map_of_isPrime_disjoint` to primary ideals |
This PR generalizes `comap_map_of_isPrime_disjoint` to primary ideals, but keeps the existing statement around since it seems to be getting the most use in practice.
---
[](https://gitpod.io/from-referrer/)
|
t-algebra
t-ring-theory
label:t-algebra$ |
19/8 |
Mathlib/RingTheory/Localization/Ideal.lean |
1 |
1 |
['github-actions'] |
nobody |
0-53800 14 hours ago |
0-53800 14 hours ago |
0-53774 14 hours |
| 33782 |
tb65536 author:tb65536 |
refactor(RingTheory/Lasker): create structure for primary decomposition |
This PR extracts the conclusion of the Lasker-Noether theorem into a separate predicate, so that (in a follow-up PR), the various properties of the primary decomposition don't have to rewrite the entire three-line predicate each time.
---
[](https://gitpod.io/from-referrer/)
|
t-algebra
t-ring-theory
label:t-algebra$ |
19/6 |
Mathlib/RingTheory/Lasker.lean |
1 |
1 |
['github-actions'] |
nobody |
0-53423 14 hours ago |
0-53423 14 hours ago |
0-53397 14 hours |
| 30640 |
SnirBroshi author:SnirBroshi |
feat(Combinatorics/SimpleGraph/Acyclic): acyclic and bridge theorems |
---
- [x] depends on: #30542
- [x] depends on: #30570
[](https://gitpod.io/from-referrer/)
|
t-combinatorics |
76/82 |
Mathlib/Combinatorics/SimpleGraph/Acyclic.lean,Mathlib/Combinatorics/SimpleGraph/Connectivity/Connected.lean |
2 |
7 |
['SnirBroshi', 'b-mehta', 'github-actions', 'mathlib4-dependent-issues-bot', 'mathlib4-merge-conflict-bot'] |
b-mehta assignee:b-mehta |
0-51064 14 hours ago |
2-32689 2 days ago |
31-80766 31 days |
| 28208 |
Sebi-Kumar author:Sebi-Kumar |
feat(Topology): add the definition `foldTrans` to concatenate finite sequences of paths |
Add `foldTrans`, which folds the function `Path.trans` across a sequence of paths with compatible endpoints, corresponding to the concatenation of a finite sequence of paths. This is implemented with `Fin.dfoldl` from the Batteries library. Prove basic properties about `foldTrans` (i.e., how it behaves with respect to `Path.refl`, `Path.subpath`, and homotopies).
---
To provide additional context, I am new to contributing to Mathlib, and I am doing so as a part of the Fields Undergraduate Summer Research Program at the University of Western Ontario under the supervision of Chris Kapulkin and Daniel Carranza. My goal is to prove that the `n`-sphere is simply connected for `n > 1`, following the proof from Hatcher's "Algebraic Topology."
- [ ] depends on: #27261
[](https://gitpod.io/from-referrer/)
|
merge-conflict
t-topology
new-contributor
|
259/0 |
Mathlib.lean,Mathlib/Topology/FoldTrans.lean,Mathlib/Topology/Subpath.lean |
3 |
3 |
['github-actions', 'mathlib4-dependent-issues-bot', 'mathlib4-merge-conflict-bot'] |
nobody |
1-79853 1 day ago |
1-79855 1 day ago |
0-2340 39 minutes |
| 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
|
689/0 |
Mathlib.lean,Mathlib/RingTheory/FractionalIdeal/Operations.lean,Mathlib/RingTheory/UniqueFactorizationDomain/ClassGroup.lean |
3 |
7 |
['alreadydone', 'bilichboris', 'github-actions', 'jcommelin', 'kim-em'] |
nobody |
0-47874 13 hours ago |
2-6757 2 days ago |
2-6798 2 days |
| 33785 |
vihdzp author:vihdzp |
feat: small lemmas on `ArchimedeanClass` |
---
[](https://gitpod.io/from-referrer/)
|
t-algebra label:t-algebra$ |
16/0 |
Mathlib/Algebra/Order/Archimedean/Class.lean |
1 |
3 |
['github-actions', 'vihdzp', 'wwylele'] |
nobody |
0-46344 12 hours ago |
1-22701 1 day ago |
1-22741 1 day |
| 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 |
3-68789 3 days ago |
4-66943 4 days ago |
4-66976 4 days |
| 33726 |
alreadydone author:alreadydone |
feat(Analysis): (complex) polynomials as branched coverings |
originally proposed by @urkud in #33425
---
[](https://gitpod.io/from-referrer/)
|
t-topology
t-analysis
large-import
|
123/1 |
Mathlib/Algebra/Polynomial/Roots.lean,Mathlib/Analysis/Complex/CoveringMap.lean,Mathlib/Topology/Algebra/Polynomial.lean,Mathlib/Topology/Covering/Basic.lean |
4 |
n/a |
['alreadydone', 'github-actions', 'mathlib4-merge-conflict-bot'] |
nobody |
0-41173 11 hours ago |
unknown |
unknown |
| 33409 |
jsm28 author:jsm28 |
feat(LinearAlgebra/AffineSpace/Ceva): Ceva's theorem |
Add Ceva's theorem. Unlike various previous attempts, I think this in appropriate generality for mathlib; it starts with a version for an arbitary (possibly infinite) affinely independent family of points (not necessarily spanning the whole space), in any affine space over any ring, and with the second point given on each line not necessarily being on the opposite face, then deduces a simpler version for a finite family, then deduces versions for a triangle, now with actual cevians (lines between a vertex and a point on the opposite side), either just multiplying weights (here the ring requires no zero divisors) or expressed with a product of divisions equal to 1 (here it becomes a field).
This doesn't include any form of the converse (with a "concurrent or parallel" conclusion, and note that you don't need affine independence for the converse), or variants of the forward direction where you're given parallel lines rather than concurrent lines, but I think those things can reasonably be done in followups.
---
[](https://gitpod.io/from-referrer/)
|
t-algebra
t-euclidean-geometry
label:t-algebra$ |
311/0 |
Mathlib.lean,Mathlib/Analysis/Normed/Affine/Ceva.lean,Mathlib/LinearAlgebra/AffineSpace/AffineSubspace/Basic.lean,Mathlib/LinearAlgebra/AffineSpace/Ceva.lean,docs/100.yaml,docs/1000.yaml |
6 |
11 |
['github-actions', 'jsm28', 'ocfnash', 'plby'] |
mariainesdff and ocfnash assignee:ocfnash assignee:mariainesdff |
0-40292 11 hours ago |
0-77082 21 hours ago |
10-46027 10 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'] |
jsm28 assignee:jsm28 |
1-35948 1 day ago |
5-7568 5 days ago |
5-7604 5 days |
| 33802 |
stepan2698-cpu author:stepan2698-cpu |
feat: Schur's lemma for monoid representations |
Adds an algebra instance on the set of intertwining maps. Proves various versions of Schur's lemma for monoid representations and proves that a finite-dimensional irreducible representation of a commutative monoid is one-dimensional.
- depends on: #32856
- depends on: #33221
---
[](https://gitpod.io/from-referrer/)
|
t-algebra
new-contributor
label:t-algebra$ |
458/11 |
Mathlib.lean,Mathlib/RepresentationTheory/Intertwining.lean,Mathlib/RepresentationTheory/Irreducible.lean,Mathlib/RepresentationTheory/Subrepresentation.lean |
4 |
2 |
['alreadydone', 'github-actions'] |
nobody |
0-39883 11 hours ago |
0-57582 15 hours ago |
0-57627 16 hours |
| 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-38061 10 hours ago |
6-11366 6 days ago |
6-11398 6 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'] |
RemyDegenne assignee:RemyDegenne |
0-35965 9 hours ago |
3-56153 3 days ago |
9-79516 9 days |
| 33491 |
themathqueen author:themathqueen |
feat(Analysis/InnerProductSpace): linear map is positive iff it equals the sum of rank-one operators |
... and equality of nonzero rank-one operators means the elements are colinear.
---
The proof of `rankOne_normalize_eq_rankOne_normalize_iff` is kinda messy. Feel free to golf.
- [x] depends on: #33439
[](https://gitpod.io/from-referrer/)
|
t-analysis |
97/5 |
Mathlib/Analysis/InnerProductSpace/LinearMap.lean,Mathlib/Analysis/InnerProductSpace/Positive.lean,Mathlib/Analysis/InnerProductSpace/Symmetric.lean |
3 |
3 |
['github-actions', 'mathlib4-dependent-issues-bot', 'themathqueen'] |
urkud assignee:urkud |
0-35962 9 hours ago |
3-54765 3 days ago |
3-54758 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 |
0-78434 21 hours ago |
4-78376 4 days ago |
4-78378 4 days |
| 33643 |
vihdzp author:vihdzp |
feat: `r < stdPart x → r < x` |
---
[](https://gitpod.io/from-referrer/)
|
t-algebra label:t-algebra$ |
25/4 |
Mathlib/Algebra/Order/Ring/StandardPart.lean |
1 |
1 |
['github-actions'] |
dagurtomas assignee:dagurtomas |
0-35959 9 hours ago |
4-33668 4 days ago |
4-33701 4 days |
| 33657 |
vihdzp author:vihdzp |
chore(SetTheory/Cardinal/Arithmetic): switch `lift.{max u w} x = lift.{max v w} y` to `lift.{u} x = lift.{v} y` |
---
Lean can't often infer the extra `w` universe otherwise. Oh, if only we had some sort of `liftEq` predicate so we didn't have to bother with `lift` at all.
[](https://gitpod.io/from-referrer/)
|
t-set-theory |
13/13 |
Mathlib/SetTheory/Cardinal/Arithmetic.lean,Mathlib/SetTheory/Cardinal/Basic.lean |
2 |
1 |
['github-actions'] |
alreadydone assignee:alreadydone |
0-35957 9 hours ago |
4-14296 4 days ago |
4-14332 4 days |
| 33658 |
vihdzp author:vihdzp |
refactor(RingTheory/Valuation/ValuativeRel/Basic): fix theorem names for multiplication |
We rename `vle_mul_right` to `mul_vle_mul_left` and reorder its arguments to match `mul_le_mul_left`, and other analogous changes.
---
[](https://gitpod.io/from-referrer/)
|
t-ring-theory |
61/62 |
Mathlib/RingTheory/Valuation/ValuativeRel/Basic.lean,Mathlib/RingTheory/Valuation/ValuativeRel/Trivial.lean |
2 |
2 |
['JovanGerb', 'github-actions'] |
erdOne assignee:erdOne |
0-35956 9 hours ago |
4-10178 4 days ago |
4-10212 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'] |
dagurtomas assignee:dagurtomas |
0-35956 9 hours ago |
4-6271 4 days ago |
4-6253 4 days |
| 33668 |
Citronhat author:Citronhat |
feat(PMF): add lintegral formulas for PMF |
This PR introduces two lemmas describing the `lintegral` of a function with respect to the measure induced by a probability mass function:
- `PMF.lintegral_eq_tsum`
- `PMF.lintegral_eq_sum`
These are the `ℝ≥0∞` analogues of the existing Bochner `integral` formulas `integral_eq_tsum` and `integral_eq_sum`. They could be useful for reasoning about expectations and integrability.
In addition, the proof of `integral_eq_sum` is simplified by deriving it directly from `integral_eq_tsum` using `tsum_fintype`. |
t-measure-probability
new-contributor
|
14/5 |
Mathlib/Probability/ProbabilityMassFunction/Integrals.lean |
1 |
1 |
['github-actions'] |
kex-y assignee:kex-y |
0-35955 9 hours ago |
3-74526 3 days ago |
3-74567 3 days |
| 33672 |
euprunin author:euprunin |
chore: golf using `grind`. add `grind` annotations. |
---
The goal of this golfing PR is to decrease the number of times lemmas are called explicitly (replacing calls to lemmas with calls to tactics). Any decrease in compilation time is a welcome side effect, although it is not a primary objective.
Trace profiling results (shown if ≥10 ms before or after):
* `Orientation.nonneg_inner_and_areaForm_eq_zero_iff_sameRay`: 287 ms before, 336 ms after
* `PFunctor.liftr_iff`: 49 ms before, 93 ms after
* `IsAdjoinRootMonic.coeff_root_pow`: 119 ms before, 267 ms after
This golfing PR is batched under the following guidelines:
* Up to ~5 changed files per PR
* Up to ~25 changed declarations per PR
* Up to ~100 changed lines per PR
---
[](https://gitpod.io/from-referrer/)
|
|
9/33 |
Mathlib/Analysis/InnerProductSpace/TwoDim.lean,Mathlib/Data/PFunctor/Univariate/Basic.lean,Mathlib/RingTheory/IsAdjoinRoot.lean |
3 |
3 |
['euprunin', 'github-actions', 'leanprover-radar'] |
dwrensha assignee:dwrensha |
0-35954 9 hours ago |
3-62944 3 days ago |
3-62917 3 days |
| 33676 |
YuvalFilmus author:YuvalFilmus |
feat(Chebyshev/Orthogonality): Chebyshev T polynomials are orthogonal |
We prove that the Chebyshev T polynomials are orthogonal with respect to `1 / √ (1 - x ^ 2)`.
Similarly, one could show that the Chebyshev U polynomials are orthogonal with respect to `√ (1 - x ^ 2)`, which I will do once this PR is approved.
More generally, one defines an inner product space on the space of all real polynomials, where the inner product is as defined above.
I will be happy to add this to the present or a future PR.
---
[](https://gitpod.io/from-referrer/)
|
t-analysis |
138/0 |
Mathlib.lean,Mathlib/Analysis/SpecialFunctions/Trigonometric/Chebyshev/Orthogonality.lean |
2 |
2 |
['github-actions', 'wwylele'] |
j-loreaux assignee:j-loreaux |
0-35953 9 hours ago |
3-59327 3 days ago |
3-59364 3 days |
| 33679 |
DavidLedvinka author:DavidLedvinka |
feat(MeasureTheory): add formulas for the measures formed by a density with respect to counting or dirac measures. |
Like with most theorems that ultimately rely on application of dirac measures, there are primed versions for when the function (or set in other cases) is measurable, and unprimed versions for when `MeasurableSingletonClass` is assumed. |
t-measure-probability |
21/0 |
Mathlib/MeasureTheory/Measure/WithDensity.lean |
1 |
1 |
['github-actions'] |
urkud assignee:urkud |
0-35952 9 hours ago |
3-55843 3 days ago |
3-55880 3 days |
| 33688 |
Citronhat author:Citronhat |
feat(PMF): add expectation lemmas for Poisson PMF |
This PR adds some basic results about the Poisson distribution, its `PMF`, and its expectation.
**New lemmas:**
* `poissonPMF_apply` — an unfolding lemma for `poissonPMF`.
* `poissonPMFReal_mul_eq_succ_mul` — the standard recursion identity for the Poisson mass function.
* `poissonPMFReal_hasSum_nmul` — shows that `fun n ↦ poissonPMFReal r n * n` has sum `r`.
* `poissonPMF_tsum_nmul` — the corresponding identity at the level of the `PMF`.
* `poissonPMF_coe_tsum_nmul` — the same result after coercion to `ℝ`.
Both `ℝ`-valued and `ℝ≥0∞`-valued formulations are included so that these results can be used conveniently in both Lebesgue and Bochner integration contexts. |
t-measure-probability
new-contributor
|
21/0 |
Mathlib/Probability/Distributions/Poisson.lean |
1 |
2 |
['Citronhat', 'github-actions'] |
urkud assignee:urkud |
0-35952 9 hours ago |
3-44998 3 days ago |
3-45032 3 days |
| 27936 |
alreadydone author:alreadydone |
feat(Algebra): additivize Dvd and Prime |
`Prime` can't be directly additivized, so we introduce `Preprime`, which drops the `≠ 0` condition, and additivize it to `AddPrime`. To show that `Preprime` is a reasonable definition, we show its connection to `Irreducible` under `IsPrimal` and `IsRegular` conditions. We also show that an element in a product monoid is preprime iff one component is a unit and the other is preprime, and the same with `Preprime` replaced by `Irreducible`.
Also additivize `IsPrimal`, `IsRelPrime` and `DecompositionMonoid`.
The motivation is that the primality of `single g 1` in `AddMonoidAlgebra k G` is connected to the primality of `g` in `G`.
---
I've checked [all 29 files](https://github.com/search?q=repo%3Aleanprover-community%2Fmathlib4%20%E2%88%A3%20to_additive&type=code) containing the `∣` symbol and the `to_additive` attribute and fixed the wrongly translated (`dvd` to `addDvd`) names.
TODO: connect (Add)Dvd to [ExistsMul/AddOfLE](https://leanprover-community.github.io/mathlib4_docs/Mathlib/Algebra/Order/Monoid/Unbundled/ExistsOfLE.html#ExistsMulOfLE)
[](https://gitpod.io/from-referrer/)
|
merge-conflict
t-algebra
label:t-algebra$ |
400/191 |
Mathlib.lean,Mathlib/Algebra/BigOperators/Group/Finset/Basic.lean,Mathlib/Algebra/BigOperators/Group/Finset/Defs.lean,Mathlib/Algebra/BigOperators/Group/Finset/Piecewise.lean,Mathlib/Algebra/BigOperators/Group/List/Lemmas.lean,Mathlib/Algebra/BigOperators/Group/Multiset/Basic.lean,Mathlib/Algebra/Divisibility/Basic.lean,Mathlib/Algebra/Divisibility/Finite.lean,Mathlib/Algebra/Divisibility/Hom.lean,Mathlib/Algebra/Divisibility/Prod.lean,Mathlib/Algebra/Divisibility/Units.lean,Mathlib/Algebra/Group/Action/Pointwise/Finset.lean,Mathlib/Algebra/Group/Prod.lean,Mathlib/Algebra/GroupWithZero/Associated.lean,Mathlib/Algebra/Notation/Defs.lean,Mathlib/Algebra/Prime/Defs.lean,Mathlib/Algebra/Prime/Lemmas.lean,Mathlib/Algebra/Prime/Prod.lean,Mathlib/Data/Nat/Prime/Defs.lean,Mathlib/Dynamics/PeriodicPts/Defs.lean,Mathlib/GroupTheory/Coset/Card.lean,Mathlib/GroupTheory/Exponent.lean,Mathlib/GroupTheory/GroupAction/Blocks.lean,Mathlib/GroupTheory/GroupAction/Period.lean,Mathlib/GroupTheory/Index.lean,Mathlib/GroupTheory/OrderOfElement.lean,Mathlib/GroupTheory/Perm/Cycle/Type.lean,Mathlib/GroupTheory/Schreier.lean,Mathlib/GroupTheory/SpecificGroups/Cyclic.lean,Mathlib/Tactic/ToAdditive/GuessName.lean |
30 |
13 |
['JovanGerb', 'adomani', 'alreadydone', 'bryangingechen', 'github-actions', 'mathlib4-merge-conflict-bot'] |
bryangingechen assignee:bryangingechen |
58-29692 1 month ago |
58-29693 1 month ago |
98-49698 98 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 |
6 |
['alreadydone', 'github-actions', 'leanprover-radar', 'vihdzp', 'xgenereux'] |
chrisflav assignee:chrisflav |
0-35174 9 hours ago |
4-54010 4 days ago |
4-53991 4 days |
| 33504 |
ldct author:ldct |
feat: Add lemmas for DihedralGroup.fintypeHelper |
Using `fin_cases` to reason about `DihedralGroup` elements exposes the internal `fintypeHelper` instances, which has no exported API
```
example (g : DihedralGroup 3) : (g^6 = 1) := by
fin_cases g
<;> dsimp
--
6 goals
case «0»
⊢ DihedralGroup.fintypeHelper✝ (Sum.inl 0) ^ 6 = 1
...
```
this PR adds simp lemma that convert them to constructors, which do have API
```
6 goals
case «0»
⊢ 1 ^ 6 = 1
case «1»
⊢ DihedralGroup.r 1 ^ 6 = 1
case «2»
⊢ DihedralGroup.r 2 ^ 6 = 1
```
---
[](https://gitpod.io/from-referrer/)
|
t-group-theory |
8/0 |
Mathlib/GroupTheory/SpecificGroups/Dihedral.lean |
1 |
1 |
['github-actions', 'tb65536'] |
nobody |
0-33986 9 hours ago |
7-21739 7 days ago |
7-21777 7 days |
| 33801 |
artie2000 author:artie2000 |
chore: add missing mem lemmas |
* Add missing `simp` lemmas `mem_foo` where a `simp` lemma `coe_foo` already exists
---
[](https://gitpod.io/from-referrer/)
|
t-meta |
21/5 |
Mathlib/AlgebraicGeometry/OpenImmersion.lean,Mathlib/AlgebraicGeometry/Scheme.lean,Mathlib/RingTheory/DedekindDomain/Different.lean,Mathlib/RingTheory/FractionalIdeal/Basic.lean,Mathlib/RingTheory/FractionalIdeal/Extended.lean,Mathlib/Topology/Category/TopCat/Opens.lean,Mathlib/Topology/Sets/Opens.lean |
7 |
2 |
['artie2000', 'github-actions'] |
nobody |
0-28723 7 hours ago |
0-28723 7 hours ago |
0-63032 17 hours |
| 33441 |
dupuisf author:dupuisf |
feat: add `LawfulInv` class for types with an inverse that behaves like `Ring.inverse` |
This PR introduces a new typeclass `LawfulInv` for types which have an `Inv` instance that is equal to zero on non-invertible elements. This is meant to replace `Ring.inverse`. The current plan is to do this refactor in several steps:
1. This PR, which only introduces the class and adds instances for matrices and continuous linear maps.
2. Add instances for all C*-algebras, and make `CStarAlgebra` extend this.
3. Deprecate `Ring.inverse`.
---
[](https://gitpod.io/from-referrer/)
|
t-algebra label:t-algebra$ |
161/22 |
Mathlib/Algebra/GroupWithZero/Defs.lean,Mathlib/Algebra/GroupWithZero/Invertible.lean,Mathlib/Algebra/GroupWithZero/Units/Basic.lean,Mathlib/LinearAlgebra/Matrix/NonsingularInverse.lean,Mathlib/LinearAlgebra/Matrix/PosDef.lean,Mathlib/RingTheory/DividedPowers/Padic.lean,Mathlib/Topology/Algebra/Module/Equiv.lean |
7 |
20 |
['dupuisf', 'eric-wieser', 'github-actions', 'mathlib4-merge-conflict-bot', 'plp127'] |
nobody |
0-15984 4 hours ago |
1-52705 1 day ago |
1-52679 1 day |
| 33804 |
tb65536 author:tb65536 |
feat(RingTheory/Localization/Ideal): `map` distributes over `inf` |
This PR proves that mapping ideals to the localization distributes over finite intersections, following the design of the analogous statements for `Ideal.radical`.
---
[](https://gitpod.io/from-referrer/)
|
t-algebra
t-ring-theory
label:t-algebra$ |
23/0 |
Mathlib/RingTheory/Localization/Ideal.lean |
1 |
2 |
['github-actions', 'plp127'] |
nobody |
0-14938 4 hours ago |
0-52772 14 hours ago |
0-52746 14 hours |
| 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'] |
riccardobrasca assignee:riccardobrasca |
0-35958 9 hours ago |
4-26071 4 days ago |
4-27549 4 days |
| 33812 |
urkud author:urkud |
feat: define `List.offDiag` |
Use it to drop decidability assumption in `Finset.offDiag`. Also redefine `Finset.diag`.
---
Built on top of #12632, reopened from a fork.
[](https://gitpod.io/from-referrer/)
|
t-data |
187/60 |
Mathlib.lean,Mathlib/Algebra/BigOperators/Group/Finset/Basic.lean,Mathlib/Data/Finite/Prod.lean,Mathlib/Data/Finset/Prod.lean,Mathlib/Data/Finset/Sym.lean,Mathlib/Data/Fintype/Prod.lean,Mathlib/Data/List/Flatten.lean,Mathlib/Data/List/Nodup.lean,Mathlib/Data/List/OffDiag.lean,Mathlib/Tactic/GCongr/CoreAttrs.lean,Mathlib/Topology/MetricSpace/Infsep.lean |
11 |
2 |
['eric-wieser', 'github-actions'] |
nobody |
0-736 12 minutes ago |
0-10599 2 hours ago |
0-27998 7 hours |
| 31653 |
ster99 author:ster99 |
feat(MeasureTheory): Foelner filters |
Define a predicate for a filter to be Foelner. Prove that if a measure space with a G-action has a Foelner filter then there is a left-invariant finitely additive probability measure on it (amenability).
Define the maximal Foelner filter and prove that if the maximal Foelner filter is nontrivial, then the amenability condition above holds.
Closes #29213.
---
depends on : #32117.
[](https://gitpod.io/from-referrer/)
|
new-contributor |
177/0 |
Mathlib.lean,Mathlib/MeasureTheory/FoelnerFilter.lean |
2 |
50 |
['ADedecker', 'YaelDillies', 'github-actions', 'mathlib4-merge-conflict-bot', 'ster99'] |
nobody |
1-76969 1 day ago |
1-76969 1 day ago |
2-58554 2 days |
| 33796 |
JohnnyTeutonic author:JohnnyTeutonic |
feat(LinearAlgebra/Matrix/Trace): the trace map is surjective |
---
[](https://gitpod.io/from-referrer/)
|
easy
t-algebra
maintainer-merge
label:t-algebra$ |
6/0 |
Mathlib/LinearAlgebra/Matrix/Trace.lean |
1 |
7 |
['JohnnyTeutonic', 'github-actions', 'grunweg', 'themathqueen'] |
nobody |
0-272 4 minutes ago |
0-272 4 minutes ago |
0-66812 18 hours |