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 |
38-85310 1 month ago |
42-34534 1 month ago |
44-34960 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 |
38-85300 1 month ago |
44-77610 1 month ago |
44-77653 44 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 |
37-85296 1 month ago |
41-75375 1 month ago |
41-78000 41 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-23061 1 month ago |
33-23180 1 month ago |
38-17613 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-7119 1 month ago |
39-10321 1 month ago |
39-13275 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 |
32-85302 1 month ago |
36-5233 1 month ago |
37-9834 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-47449 1 month ago |
32-47478 1 month ago |
32-55058 32 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 |
31-85301 1 month ago |
35-72616 1 month ago |
35-72607 35 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-16258 29 days ago |
29-30444 29 days ago |
49-76998 49 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-32093 28 days ago |
32-46298 1 month ago |
32-46589 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 |
26-85287 26 days ago |
31-71732 1 month ago |
35-16615 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 |
26-69430 26 days ago |
33-15873 1 month ago |
33-15916 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-27901 26 days ago |
31-22769 1 month ago |
31-23034 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-34441 24 days ago |
30-54341 30 days ago |
54-31317 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 |
23-85309 23 days ago |
27-74659 27 days ago |
27-74694 27 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-22631 23 days ago |
23-22634 23 days ago |
29-19889 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 |
22-85301 22 days ago |
28-68256 28 days ago |
28-68233 28 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 |
22-73951 22 days ago |
33-14595 1 month ago |
33-14628 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 |
22-73491 22 days ago |
32-77794 1 month ago |
32-77838 32 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-10515 22 days ago |
22-10579 22 days ago |
30-41578 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-3168 22 days ago |
22-3660 22 days ago |
32-8276 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 |
21-49497 21 days ago |
22-77908 22 days ago |
22-77953 22 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-35784 21 days ago |
46-63847 1 month ago |
47-8339 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-7132 21 days ago |
21-7158 21 days ago |
33-62508 33 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-6867 21 days ago |
21-73722 21 days ago |
39-85625 39 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 |
20-85317 20 days ago |
24-10480 24 days ago |
24-12988 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 |
20-85313 20 days ago |
27-78427 27 days ago |
27-78435 27 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 |
20-51048 20 days ago |
20-51107 20 days ago |
42-30031 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-29038 20 days ago |
21-53222 21 days ago |
35-54143 35 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 |
19-85287 19 days ago |
30-11181 30 days ago |
30-11218 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 |
19-85286 19 days ago |
29-33308 29 days ago |
29-33389 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 |
19-85283 19 days ago |
25-34859 25 days ago |
25-35188 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 |
19-85282 19 days ago |
23-76089 23 days ago |
23-76128 23 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 |
19-85279 19 days ago |
23-9382 23 days ago |
23-9358 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 |
19-79313 19 days ago |
19-79337 19 days ago |
29-35005 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 |
18-85289 18 days ago |
22-30221 22 days ago |
22-37547 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 |
18-54503 18 days ago |
20-2772 20 days ago |
158-34464 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 |
17-85305 17 days ago |
21-24915 21 days ago |
21-24977 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 |
17-85302 17 days ago |
22-62827 22 days ago |
22-62870 22 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 |
17-85300 17 days ago |
21-9727 21 days ago |
21-71475 21 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 |
17-85299 17 days ago |
21-2369 21 days ago |
21-48315 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 |
17-85297 17 days ago |
21-43819 21 days ago |
21-43865 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 |
17-85292 17 days ago |
21-12224 21 days ago |
21-12208 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 |
17-79539 17 days ago |
17-81305 17 days ago |
22-78426 22 days |
| 33126 |
CoolRmal author:CoolRmal |
feat: function composition preserves boundedness |
This PR adds the following theorem: if the range of a function `g` is bounded above, then `g ∘ f` is bounded above for
all functions `f`.
---
[](https://gitpod.io/from-referrer/)
|
t-order |
12/0 |
Mathlib/Order/Bounds/Basic.lean |
1 |
1 |
['github-actions'] |
bryangingechen assignee:bryangingechen |
16-85293 16 days ago |
20-42936 20 days ago |
20-42978 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 |
16-85292 16 days ago |
20-8988 20 days ago |
20-33524 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-43733 16 days ago |
16-43745 16 days ago |
16-43781 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-30049 16 days ago |
20-3674 20 days ago |
37-22818 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-20515 16 days ago |
16-43221 16 days ago |
16-43259 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-14555 16 days ago |
43-82923 1 month ago |
43-82956 43 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 |
15-85307 15 days ago |
19-78441 19 days ago |
19-78488 19 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 |
15-60675 15 days ago |
15-60699 15 days ago |
41-57331 41 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-46876 15 days ago |
20-54894 20 days ago |
20-54936 20 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 |
14-85296 14 days ago |
18-2482 18 days ago |
18-2461 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 |
13-85305 13 days ago |
24-27637 24 days ago |
24-27676 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 |
13-85302 13 days ago |
17-28552 17 days ago |
17-28594 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 |
13-85301 13 days ago |
17-296 17 days ago |
17-335 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 |
13-66391 13 days ago |
14-36539 14 days ago |
15-4979 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 |
12-85271 12 days ago |
24-17 23 days ago |
23-86393 23 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-24992 12 days ago |
12-25017 12 days ago |
17-43981 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-5714 12 days ago |
12-5741 12 days ago |
12-5783 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-1497 12 days ago |
12-1910 12 days ago |
70-45417 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 |
11-85284 11 days ago |
15-25509 15 days ago |
15-25548 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 |
11-74202 11 days ago |
21-5743 21 days ago |
86-57474 86 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 |
11-51161 11 days ago |
25-50296 25 days ago |
45-50124 45 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-4083 11 days ago |
21-7107 21 days ago |
22-8864 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 |
10-85302 10 days ago |
14-19295 14 days ago |
14-19756 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 |
10-85301 10 days ago |
14-81301 14 days ago |
14-81278 14 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 |
10-55425 10 days ago |
13-54407 13 days ago |
13-54448 13 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 |
9-85292 9 days ago |
13-56886 13 days ago |
20-23360 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-22527 8 days ago |
8-22534 8 days ago |
8-22572 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-7202 8 days ago |
8-7202 8 days ago |
17-76288 17 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-14238 7 days ago |
15-8485 15 days ago |
15-8534 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-15238 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 |
6-69056 6 days ago |
7-51474 7 days ago |
7-51513 7 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 |
6-61936 6 days ago |
13-60506 13 days ago |
28-80996 28 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 |
6-50747 6 days ago |
31-25970 1 month ago |
31-26005 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-36095 6 days ago |
6-48392 6 days ago |
6-48429 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-28814 6 days ago |
6-31393 6 days ago |
6-31371 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-14066 6 days ago |
10-83146 10 days ago |
27-75291 27 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 |
5-85285 5 days ago |
20-80893 20 days ago |
22-37908 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 |
5-85284 5 days ago |
9-16295 9 days ago |
10-74858 10 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 |
5-85280 5 days ago |
9-82424 9 days ago |
9-82409 9 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 |
5-85278 5 days ago |
9-7541 9 days ago |
9-7583 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 |
5-82833 5 days ago |
6-72484 6 days ago |
6-75675 6 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 |
5-57257 5 days ago |
7-10991 7 days ago |
7-79963 7 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-39538 5 days ago |
5-39538 5 days ago |
5-42579 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-13178 5 days ago |
9-34938 9 days ago |
9-34926 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-11302 5 days ago |
25-78089 25 days ago |
25-78067 25 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 |
4-86377 4 days ago |
51-49867 1 month ago |
56-6697 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 |
4-85275 4 days ago |
8-8524 8 days ago |
8-8501 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 |
4-85274 4 days ago |
8-8180 8 days ago |
8-8157 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 |
4-85274 4 days ago |
8-8125 8 days ago |
8-8102 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 |
4-78155 4 days ago |
4-83632 4 days ago |
72-54212 72 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 |
4-50769 4 days ago |
15-9605 15 days ago |
15-77375 15 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-32774 4 days ago |
4-43235 4 days ago |
4-43280 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-17648 4 days ago |
7-19518 7 days ago |
7-19497 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-15828 4 days ago |
4-15856 4 days ago |
21-20938 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-1336 4 days ago |
4-25874 4 days ago |
63-65075 63 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 |
3-85295 3 days ago |
8-29828 8 days ago |
8-29869 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 |
3-85292 3 days ago |
7-80103 7 days ago |
7-80087 7 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 |
3-85290 3 days ago |
7-31739 7 days ago |
7-31782 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 |
3-85289 3 days ago |
7-2940 7 days ago |
7-2930 7 days |
| 33643 |
vihdzp author:vihdzp |
feat: `r < stdPart x → r < x` |
---
[](https://gitpod.io/from-referrer/)
|
t-algebra label:t-algebra$ |
25/4 |
Mathlib/Algebra/Order/Ring/StandardPart.lean |
1 |
1 |
['github-actions'] |
nobody |
3-81681 3 days ago |
3-83010 3 days ago |
3-83047 3 days |
| 33649 |
vihdzp author:vihdzp |
feat(Analysis/Real/Hyperreal): more lemmas on `ω` and `ε` |
I've moved these around a bit, so as to ensure the lemmas about each constant are next to each other.
---
[](https://gitpod.io/from-referrer/)
|
t-algebra
large-import
label:t-algebra$ |
116/30 |
Mathlib/Algebra/Order/AddGroupWithTop.lean,Mathlib/Algebra/Order/Ring/Archimedean.lean,Mathlib/Algebra/Order/Ring/StandardPart.lean,Mathlib/Analysis/Real/Hyperreal.lean |
4 |
6 |
['github-actions', 'vihdzp', 'wwylele'] |
nobody |
3-69098 3 days ago |
3-75413 3 days ago |
3-76895 3 days |
| 33657 |
vihdzp author:vihdzp |
chore(SetTheory/Cardinal/Arithmetic): switch `lift.{max u w} x = lift.{max v w} y` to `lift.{u} x = lift.{v} y` |
---
Lean can't often infer the extra `w` universe otherwise. Oh, if only we had some sort of `liftEq` predicate so we didn't have to bother with `lift` at all.
[](https://gitpod.io/from-referrer/)
|
t-set-theory |
13/13 |
Mathlib/SetTheory/Cardinal/Arithmetic.lean,Mathlib/SetTheory/Cardinal/Basic.lean |
2 |
1 |
['github-actions'] |
nobody |
3-63636 3 days ago |
3-63638 3 days ago |
3-63678 3 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 |
3-56219 3 days ago |
3-56796 3 days ago |
7-60114 7 days |
| 33662 |
Pjotr5 author:Pjotr5 |
feat(Algebra/Order/BigOperators/Expect): add lemmas and strict variants |
### Summary
- Combine `le_expect_nonempty_of_subadditive` and `le_expect_of_subadditive` into a single lemma `le_expect_of_subadditive`.
The extra assumptions `(hs : s.Nonempty)` and `(h_zero : m 0 = 0)` are unnecessary (since `m 0 = 0` follows from `h_div`).
This requires a small downstream update to `Mathlib/Analysis/RCLike/Basic.lean` (`norm_expect_le`).
- Add strict-inequality variants:
`expect_lt_expect`, `expect_lt`, `lt_expect`.
- Add existence lemmas:
`exists_le_of_expect_le_expect`, `exists_le_of_le_expect`, `exists_le_of_expect_le`,
and `exists_lt_of_expect_lt_expect`.
---
[](https://gitpod.io/from-referrer/)
|
new-contributor |
46/16 |
Mathlib/Algebra/Order/BigOperators/Expect.lean,Mathlib/Analysis/RCLike/Basic.lean |
2 |
1 |
['github-actions'] |
nobody |
3-53036 3 days ago |
3-55613 3 days ago |
3-55599 3 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-47478 3 days ago |
39-45442 1 month ago |
49-3793 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-45960 3 days ago |
11-51660 11 days ago |
11-77454 11 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-40409 3 days ago |
3-41331 3 days ago |
24-37076 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-38587 3 days ago |
5-41862 5 days ago |
9-43546 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-34408 3 days ago |
4-43782 4 days ago |
4-44311 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-3442 22 days ago |
22-3666 22 days ago |
30-7526 30 days |
| 33672 |
euprunin author:euprunin |
chore: golf using `grind`. add `grind` annotations. |
---
The goal of this golfing PR is to decrease the number of times lemmas are called explicitly (replacing calls to lemmas with calls to tactics). Any decrease in compilation time is a welcome side effect, although it is not a primary objective.
Trace profiling results (shown if ≥10 ms before or after):
* `Orientation.nonneg_inner_and_areaForm_eq_zero_iff_sameRay`: 287 ms before, 336 ms after
* `PFunctor.liftr_iff`: 49 ms before, 93 ms after
* `IsAdjoinRootMonic.coeff_root_pow`: 119 ms before, 267 ms after
This golfing PR is batched under the following guidelines:
* Up to ~5 changed files per PR
* Up to ~25 changed declarations per PR
* Up to ~100 changed lines per PR
---
[](https://gitpod.io/from-referrer/)
|
|
9/33 |
Mathlib/Analysis/InnerProductSpace/TwoDim.lean,Mathlib/Data/PFunctor/Univariate/Basic.lean,Mathlib/RingTheory/IsAdjoinRoot.lean |
3 |
3 |
['euprunin', 'github-actions', 'leanprover-radar'] |
nobody |
3-24087 3 days ago |
3-25886 3 days ago |
3-25863 3 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-20559 3 days ago |
3-21178 3 days ago |
14-80851 14 days |
| 32735 |
Jlh18 author:Jlh18 |
refactor: move `CategoryTheory.Category.Grpd` to `CategoryTheory.Groupoid.Grpd.Basic` |
Step one of several PRs, stemming from #29283
---
[](https://gitpod.io/from-referrer/)
|
file-removed |
3/4 |
Mathlib.lean,Mathlib/AlgebraicTopology/FundamentalGroupoid/Basic.lean,Mathlib/CategoryTheory/Groupoid/FreeGroupoidOfCategory.lean,Mathlib/CategoryTheory/Groupoid/Grpd/Basic.lean |
4 |
3 |
['Jlh18', 'github-actions', 'mathlib4-merge-conflict-bot'] |
nobody |
3-19076 3 days ago |
3-19095 3 days ago |
9-42462 9 days |
| 33668 |
Citronhat author:Citronhat |
feat(PMF): add lintegral formulas for PMF |
This PR introduces two lemmas describing the `lintegral` of a function with respect to the measure induced by a probability mass function:
- `PMF.lintegral_eq_tsum`
- `PMF.lintegral_eq_sum`
These are the `ℝ≥0∞` analogues of the existing Bochner `integral` formulas `integral_eq_tsum` and `integral_eq_sum`. They could be useful for reasoning about expectations and integrability.
In addition, the proof of `integral_eq_sum` is simplified by deriving it directly from `integral_eq_tsum` using `tsum_fintype`. |
t-measure-probability
new-contributor
|
14/5 |
Mathlib/Probability/ProbabilityMassFunction/Integrals.lean |
1 |
1 |
['github-actions'] |
nobody |
3-4041 3 days ago |
3-37468 3 days ago |
3-37513 3 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 |
2-85291 2 days ago |
6-14553 6 days ago |
6-67357 6 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'] |
nobody |
2-83654 2 days ago |
3-17707 3 days ago |
3-17704 3 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'] |
nobody |
2-82962 2 days ago |
3-59520 3 days ago |
3-59558 3 days |
| 33501 |
SnirBroshi author:SnirBroshi |
feat(Combinatorics/SimpleGraph/Finite): degrees for infinite graphs |
- Redefine degrees using `Set.ncard` to avoid `Fintype` and enable talking about degrees in infinite graphs.
- Define `ENat` versions of `degree`/`minDegree`/`maxDegree` called `edegree`/`eminDegree`/`emaxDegree` respectively.
- Remove `LocallyFinite` assumption from `IsRegularOfDegree`, and change it to use `edegree = k` instead of `degree = k` to retain the meaning of the case `k = 0`.
---
The `e` prefix matches the existing `edist` and `ediam`.
To make reviewing easier, this PR intentionally does not:
- Add theorems about the new definitions
- Reorder theorems to avoid `omit`s
- Move theorems to a new `Degree.lean` file
This is so that the diff shows the old/new versions side-by-side, and to avoid a bigger PR.
Consequently a few proofs are a bit longer, but that'll be fixed after this PR by adding API lemmas for the new definitions (e.g. `edegree ≠ ⊤ → edegree = degree`).
Regarding computability: If computability of degrees is useful, we can introduce a separate `findegree` in the future (similar to `neighborSet` vs `neighborFinset`), but I think degrees are a basic graph definition that should be defined for any `SimpleGraph`. As for theorems, such a `findegree` can use a lemma `findegree = degree` to access all the degree theorems, instead of duplicating everything to both versions.
This PR was motivated by wanting to talk about infinite graphs with a finite max-degree.
[](https://gitpod.io/from-referrer/)
|
t-combinatorics
large-import
|
302/243 |
Archive/Wiedijk100Theorems/FriendshipGraphs.lean,Archive/Wiedijk100Theorems/Konigsberg.lean,Counterexamples/HeawoodUnitDistance.lean,Mathlib/Combinatorics/SimpleGraph/Acyclic.lean,Mathlib/Combinatorics/SimpleGraph/AdjMatrix.lean,Mathlib/Combinatorics/SimpleGraph/Bipartite.lean,Mathlib/Combinatorics/SimpleGraph/Circulant.lean,Mathlib/Combinatorics/SimpleGraph/Connectivity/Connected.lean,Mathlib/Combinatorics/SimpleGraph/DegreeSum.lean,Mathlib/Combinatorics/SimpleGraph/Extremal/Turan.lean,Mathlib/Combinatorics/SimpleGraph/Finite.lean,Mathlib/Combinatorics/SimpleGraph/FiveWheelLike.lean,Mathlib/Combinatorics/SimpleGraph/LapMatrix.lean,Mathlib/Combinatorics/SimpleGraph/Maps.lean,Mathlib/Combinatorics/SimpleGraph/Prod.lean,Mathlib/Combinatorics/SimpleGraph/StronglyRegular.lean,Mathlib/Combinatorics/SimpleGraph/Subgraph.lean,Mathlib/Combinatorics/SimpleGraph/Trails.lean,Mathlib/Data/Set/Card.lean,Mathlib/Data/Set/Insert.lean,Mathlib/Order/ConditionallyCompleteLattice/Finset.lean |
21 |
1 |
['github-actions'] |
adamtopaz assignee:adamtopaz |
2-82655 2 days ago |
2-82655 2 days ago |
6-79013 6 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 |
2-67078 2 days ago |
2-67109 2 days ago |
4-24030 4 days |
| 33676 |
YuvalFilmus author:YuvalFilmus |
feat(Chebyshev/Orthogonality): Chebyshev T polynomials are orthogonal |
We prove that the Chebyshev T polynomials are orthogonal with respect to `1 / √ (1 - x ^ 2)`.
Similarly, one could show that the Chebyshev U polynomials are orthogonal with respect to `√ (1 - x ^ 2)`, which I will do once this PR is approved.
More generally, one defines an inner product space on the space of all real polynomials, where the inner product is as defined above.
I will be happy to add this to the present or a future PR.
---
[](https://gitpod.io/from-referrer/)
|
t-analysis |
138/0 |
Mathlib.lean,Mathlib/Analysis/SpecialFunctions/Trigonometric/Chebyshev/Orthogonality.lean |
2 |
2 |
['github-actions', 'wwylele'] |
nobody |
2-64362 2 days ago |
3-22269 3 days ago |
3-22310 3 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 |
2-58750 2 days ago |
2-58750 2 days ago |
3-44220 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-48827 2 days ago |
2-49615 2 days ago |
2-49602 2 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-43917 2 days ago |
2-43917 2 days ago |
34-80218 34 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-42028 2 days ago |
2-42047 2 days ago |
4-5471 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-37973 2 days ago |
7-19365 7 days ago |
7-19356 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-33086 2 days ago |
18-47950 18 days ago |
18-47989 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-31303 2 days ago |
2-31306 2 days ago |
2-31350 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-26409 2 days ago |
2-26504 2 days ago |
3-83130 3 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-26385 2 days ago |
25-23539 25 days ago |
28-10502 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-24359 2 days ago |
2-24430 2 days ago |
2-80788 2 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-18954 2 days ago |
2-18994 2 days ago |
13-65932 13 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-10837 2 days ago |
18-46639 18 days ago |
18-46689 18 days |
| 33679 |
DavidLedvinka author:DavidLedvinka |
feat(MeasureTheory): add formulas for the measures formed by a density with respect to counting or dirac measures. |
Like with most theorems that ultimately rely on application of dirac measures, there are primed versions for when the function (or set in other cases) is measurable, and unprimed versions for when `MeasurableSingletonClass` is assumed. |
t-measure-probability |
21/0 |
Mathlib/MeasureTheory/Measure/WithDensity.lean |
1 |
1 |
['github-actions'] |
nobody |
2-9429 2 days ago |
3-18785 3 days ago |
3-18826 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'] |
nobody |
2-8149 2 days ago |
3-7940 3 days ago |
3-7978 3 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-7426 2 days ago |
2-74205 2 days ago |
2-74242 2 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-6324 2 days ago |
2-6344 2 days ago |
5-43268 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-3752 2 days ago |
2-5719 2 days ago |
2-11489 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-2034 2 days ago |
2-81491 2 days ago |
2-81529 2 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-377 2 days ago |
6-26463 6 days ago |
9-31218 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 |
1-85842 1 day ago |
1-85911 1 day ago |
4-5779 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 |
1-85306 1 day ago |
5-11157 5 days ago |
6-2756 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 |
1-85304 1 day ago |
5-73069 5 days ago |
6-56336 6 days |
| 33312 |
YuvalFilmus author:YuvalFilmus |
feat(Polynomial/Chebyshev): formulas for iterated derivatives of T and U at 1 |
The main results are `iterate_derivative_T_eval_one` and `iterate_derivative_U_eval_one`.
These are derived using recurrences which for at every point, and in particular, `iterate_derivative_T_eval_zero` and `iterate_derivative_U_eval_zero` gives the recurrences at zero.
In principle, by combining with #33311, one can compute the explicit formula for the derivative at zero.
A subsequent PR will derive consequences for these polynomials over the reals (these should work for every field).
The file is getting rather long — not sure what to do about it.
---
- [ ] depends on: #33283
- [ ] depends on: #33306
[](https://gitpod.io/from-referrer/)
|
|
110/0 |
Mathlib/RingTheory/Polynomial/Chebyshev.lean |
1 |
3 |
['github-actions', 'mathlib4-dependent-issues-bot', 'mathlib4-merge-conflict-bot'] |
RemyDegenne assignee:RemyDegenne |
1-85302 1 day ago |
2-22723 2 days ago |
2-24196 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 |
1-85300 1 day ago |
5-38359 5 days ago |
5-44226 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 |
1-85299 1 day ago |
5-13845 5 days ago |
8-4125 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 |
1-85298 1 day ago |
5-20852 5 days ago |
6-13722 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 |
1-85297 1 day ago |
5-86285 5 days ago |
5-86273 5 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 |
1-85294 1 day ago |
5-53706 5 days ago |
5-53692 5 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 |
1-81526 1 day ago |
12-44727 12 days ago |
12-44763 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 |
1-79442 1 day ago |
1-79503 1 day ago |
12-28282 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 |
1-78170 1 day ago |
1-78170 1 day ago |
56-24317 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 |
1-74633 1 day ago |
1-75103 1 day ago |
1-75154 1 day |
| 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 |
1-69114 1 day ago |
21-9706 21 days ago |
21-80507 21 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 |
1-55601 1 day ago |
1-55685 1 day ago |
1-55662 1 day |
| 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 |
1-53797 1 day ago |
2-58851 2 days ago |
2-59793 2 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 |
1-49871 1 day ago |
2-84755 2 days ago |
73-47571 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-45975 1 day ago |
1-45975 1 day ago |
1-46021 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-45834 1 day ago |
1-45834 1 day ago |
1-45883 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-44993 1 day ago |
1-44993 1 day ago |
8-38432 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-42860 1 day ago |
1-61274 1 day ago |
1-61314 1 day |
| 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-41948 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-41875 1 day ago |
1-43591 1 day ago |
8-64386 8 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-39837 1 day ago |
1-39905 1 day ago |
1-39882 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-32175 1 day ago |
6-21904 6 days ago |
6-29492 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-30531 1 day ago |
1-30531 1 day ago |
1-30580 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-29959 1 day ago |
5-7360 5 days ago |
48-36985 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-29293 1 day ago |
42-22663 1 month ago |
42-23758 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-26793 1 day ago |
1-26793 1 day ago |
1-26838 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-26303 1 day ago |
3-63829 3 days ago |
47-68269 47 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-26165 1 day ago |
1-26165 1 day ago |
7-26866 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-26120 1 day ago |
3-21023 3 days ago |
103-39992 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-16662 1 day ago |
1-16662 1 day ago |
1-16786 1 day |
| 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 |
18 |
['dupuisf', 'eric-wieser', 'github-actions', 'mathlib4-merge-conflict-bot'] |
nobody |
1-15647 1 day ago |
1-15647 1 day ago |
1-15625 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-15116 1 day ago |
1-77169 1 day ago |
1-77210 1 day |
| 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-14849 1 day ago |
1-19361 1 day ago |
1-19406 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-14135 1 day ago |
26-19850 26 days ago |
29-69356 29 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-12201 1 day ago |
1-39217 1 day ago |
45-62294 45 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-10172 1 day ago |
1-10180 1 day ago |
1-47004 1 day |
| 33753 |
SnO2WMaN author:SnO2WMaN |
doc(1000.yaml): Mention Tarski's Undefinability Theorem in FFL |
---
[](https://gitpod.io/from-referrer/)
|
new-contributor |
2/0 |
docs/1000.yaml |
1 |
3 |
['SnO2WMaN', 'SnirBroshi', 'github-actions'] |
nobody |
1-7708 1 day ago |
1-45485 1 day ago |
1-45471 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-7604 1 day ago |
1-13004 1 day ago |
1-13060 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-6068 1 day ago |
6-15498 6 days ago |
6-15535 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-5263 1 day ago |
1-5265 1 day ago |
1-5307 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-2478 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-1902 1 day ago |
1-1902 1 day ago |
1-1881 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-1310 1 day ago |
1-1310 1 day ago |
1-1288 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-666 1 day ago |
1-5405 1 day ago |
1-5384 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 |
0-85667 23 hours ago |
2-1464 2 days ago |
2-57458 2 days |
| 25841 |
mitchell-horner author:mitchell-horner |
feat(Combinatorics/SimpleGraph): prove the Kővári–Sós–Turán theorem |
Prove the Kővári–Sós–Turán theorem (an upper bound on the Zarankiewicz function)
---
- [x] depends on: #19865
- [x] depends on: #20738
- [x] depends on: #27602
[](https://gitpod.io/from-referrer/)
---
*This PR continues the work from #20240.*
*Original PR: https://github.com/leanprover-community/mathlib4/pull/20240* |
t-combinatorics |
484/0 |
Mathlib.lean,Mathlib/Combinatorics/SimpleGraph/Bipartite.lean,Mathlib/Combinatorics/SimpleGraph/Extremal/KovariSosTuran.lean,Mathlib/Combinatorics/SimpleGraph/Extremal/Zarankiewicz.lean,Mathlib/Combinatorics/SimpleGraph/Maps.lean,docs/1000.yaml |
6 |
11 |
['SnirBroshi', 'github-actions', 'mathlib4-dependent-issues-bot', 'mathlib4-merge-conflict-bot', 'mitchell-horner'] |
kmill assignee:kmill |
0-85300 23 hours ago |
4-65158 4 days ago |
49-80554 49 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 |
0-85297 23 hours ago |
4-27387 4 days ago |
25-42846 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 |
17-67625 17 days ago |
17-79225 17 days ago |
17-79268 17 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 |
0-85291 23 hours ago |
4-75435 4 days ago |
4-75481 4 days |
| 33607 |
xgenereux author:xgenereux |
feat: primeSpectrum_eq_of_KrullDimLEOne |
Given a local ring `R` which is also a domain with `Ring.KrullDimLE 1 R` (or equivalently `Ring.DimensionLEOne`) a prime is either `⊥` or`⊤`.
The application I have in mind is `IsDiscreteValuationRing R`.
---
[](https://gitpod.io/from-referrer/)
|
t-ring-theory |
13/0 |
Mathlib/RingTheory/Spectrum/Prime/Topology.lean |
1 |
1 |
['github-actions'] |
nobody |
4-28304 4 days ago |
4-28304 4 days ago |
4-28353 4 days |
| 33609 |
xgenereux author:xgenereux |
refactor: Ideal.bot_prime as an instance |
---
[](https://gitpod.io/from-referrer/)
|
t-ring-theory |
14/18 |
Mathlib/Algebra/Order/Ring/Ordering/Basic.lean,Mathlib/RingTheory/DedekindDomain/Ideal/Lemmas.lean,Mathlib/RingTheory/Ideal/GoingUp.lean,Mathlib/RingTheory/Ideal/Maps.lean,Mathlib/RingTheory/Ideal/Maximal.lean,Mathlib/RingTheory/Ideal/MinimalPrime/Basic.lean,Mathlib/RingTheory/Ideal/NatInt.lean,Mathlib/RingTheory/Ideal/Prime.lean,Mathlib/RingTheory/Jacobson/Ring.lean,Mathlib/RingTheory/KrullDimension/Basic.lean,Mathlib/RingTheory/KrullDimension/Zero.lean,Mathlib/RingTheory/LocalRing/ResidueField/Fiber.lean,Mathlib/RingTheory/Localization/Ideal.lean,Mathlib/RingTheory/Spectrum/Prime/Basic.lean,Mathlib/RingTheory/Spectrum/Prime/Topology.lean |
15 |
5 |
['github-actions', 'leanprover-radar', 'vihdzp', 'xgenereux'] |
chrisflav assignee:chrisflav |
0-85286 23 hours ago |
4-16952 4 days ago |
4-16937 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 |
0-85285 23 hours ago |
4-25679 4 days ago |
4-25721 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 |
0-85283 23 hours ago |
4-7186 4 days ago |
4-7170 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 |
0-85282 23 hours ago |
4-4541 4 days ago |
4-4588 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 |
0-85281 23 hours ago |
4-1837 4 days ago |
4-1883 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 |
0-85018 23 hours ago |
1-36576 1 day ago |
1-36553 1 day |
| 33504 |
ldct author:ldct |
feat: Add lemmas for DihedralGroup.fintypeHelper |
Using `fin_cases` to reason about `DihedralGroup` elements exposes the internal `fintypeHelper` instances, which has no exported API
```
example (g : DihedralGroup 3) : (g^6 = 1) := by
fin_cases g
<;> dsimp
--
6 goals
case «0»
⊢ DihedralGroup.fintypeHelper✝ (Sum.inl 0) ^ 6 = 1
...
```
this PR adds simp lemma that convert them to constructors, which do have API
```
6 goals
case «0»
⊢ 1 ^ 6 = 1
case «1»
⊢ DihedralGroup.r 1 ^ 6 = 1
case «2»
⊢ DihedralGroup.r 2 ^ 6 = 1
```
---
[](https://gitpod.io/from-referrer/)
|
t-group-theory |
8/0 |
Mathlib/GroupTheory/SpecificGroups/Dihedral.lean |
1 |
1 |
['github-actions', 'tb65536'] |
nobody |
0-83903 23 hours ago |
6-71081 6 days ago |
6-71123 6 days |
| 33771 |
plp127 author:plp127 |
feat: prove `Prod.wellFoundedLT` directly |
Prove `Prod.wellFoundedLT` without going through `Antisymmetrization`. This makes the instance accessible without having to import antisymmetrization.
---
[](https://gitpod.io/from-referrer/)
|
t-order |
19/26 |
Mathlib/Algebra/Lie/Weights/Basic.lean,Mathlib/GroupTheory/Solvable.lean,Mathlib/GroupTheory/SpecificGroups/ZGroup.lean,Mathlib/Order/Antisymmetrization.lean,Mathlib/Order/RelClasses.lean |
5 |
4 |
['alreadydone', 'github-actions', 'plp127', 'vihdzp'] |
nobody |
0-81951 22 hours ago |
1-9383 1 day ago |
1-9427 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 |
0-81795 22 hours ago |
0-81795 22 hours ago |
0-81773 22 hours |
| 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 |
0-81658 22 hours ago |
2-7229 2 days ago |
2-7207 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 |
0-80739 22 hours ago |
0-80766 22 hours ago |
0-80793 22 hours |
| 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 |
0-78859 21 hours ago |
0-78876 21 hours ago |
88-26672 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 |
0-76683 21 hours ago |
2-67521 2 days ago |
9-61895 9 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 |
0-64541 17 hours ago |
0-64565 17 hours ago |
28-63770 28 days |
| 31325 |
joelriou author:joelriou |
feat(AlgebraicTopology): a computable monoidal functor instance for `hoFunctor` |
We construct a computable equivalence of categories `(X ⊗ Y).HomotopyCategory ≌ X.HomotopyCategory × Y.HomotopyCategory` for `2`-truncated simplicial sets `X` and `Y`. This allows to make the bicategory instance on quasicategories computable.
---
- [x] depends on: #33201
- [x] depends on: #31174
- [x] depends on: #31250
- [x] depends on: #31254
- [x] depends on: #31274
- [x] depends on: #31265
[](https://gitpod.io/from-referrer/)
|
t-algebraic-topology |
298/28 |
Mathlib/AlgebraicTopology/Quasicategory/StrictBicategory.lean,Mathlib/AlgebraicTopology/SimplicialSet/HoFunctorMonoidal.lean,Mathlib/AlgebraicTopology/SimplicialSet/NerveAdjunction.lean |
3 |
16 |
['github-actions', 'joelriou', 'mathlib4-dependent-issues-bot', 'mathlib4-merge-conflict-bot', 'robin-carlier'] |
robin-carlier assignee:robin-carlier |
7-53662 7 days ago |
7-53662 7 days ago |
14-15797 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 |
0-51623 14 hours ago |
0-51623 14 hours ago |
0-51717 14 hours |
| 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 |
0-49577 13 hours ago |
1-53199 1 day ago |
2-39086 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 |
0-49444 13 hours ago |
5-19982 5 days ago |
5-20020 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-48593 13 hours ago |
2-21138 2 days ago |
12-10541 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-47517 13 hours ago |
0-47517 13 hours ago |
0-50776 14 hours |
| 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-46679 12 hours ago |
20-28374 20 days ago |
20-31406 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-45517 12 hours ago |
2-18449 2 days ago |
2-19727 2 days |
| 33358 |
joelriou author:joelriou |
feat(Algebra/Homology): functoriality of `ProjectiveResolution.extMk` |
Given a fixed projective (resp. injective) resolution `R`, we obtain the functoriality of the constructor `R.extMk`.
---
- [x] depends on: #32816
[](https://gitpod.io/from-referrer/)
|
t-category-theory |
126/8 |
Mathlib/Algebra/Homology/HomotopyCategory/HomComplex.lean,Mathlib/Algebra/Homology/HomotopyCategory/HomComplexShift.lean,Mathlib/Algebra/Homology/HomotopyCategory/HomComplexSingle.lean,Mathlib/CategoryTheory/Abelian/Injective/Ext.lean,Mathlib/CategoryTheory/Abelian/Projective/Ext.lean |
5 |
5 |
['github-actions', 'joelriou', 'mathlib4-dependent-issues-bot', 'mathlib4-merge-conflict-bot', 'robin-carlier'] |
nobody |
6-38890 6 days ago |
6-38890 6 days ago |
6-54801 6 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-47602 11 days ago |
13-44627 13 days ago |
13-44670 13 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-41376 11 hours ago |
4-41318 4 days ago |
4-41324 4 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-40098 11 hours ago |
1-11835 1 day ago |
1-11814 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-39857 11 hours ago |
1-24801 1 day ago |
1-24844 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-39499 10 hours ago |
1-28951 1 day ago |
1-31639 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-38983 10 hours ago |
0-38983 10 hours ago |
2-37093 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-38241 10 hours ago |
0-38241 10 hours ago |
23-28567 23 days |
| 33403 |
xroblot author:xroblot |
feat(GroupTheory/FiniteAbelian): prove that the restriction map is surjective |
Let `G` be a finite commutative group and let `H` be a subgroup. If `M` is a commutative monoid
such that `G →* Mˣ` and `H →* Mˣ` are both finite (this is the case for example if `M` is a
commutative domain), then any homomorphism `H →* Mˣ` can be extended to an homomorphism `G →* Mˣ`.
---
[](https://gitpod.io/from-referrer/)
|
t-group-theory |
90/13 |
Mathlib/Algebra/Group/Submonoid/Operations.lean,Mathlib/GroupTheory/Exponent.lean,Mathlib/GroupTheory/FiniteAbelian/Duality.lean,Mathlib/GroupTheory/QuotientGroup/Basic.lean,Mathlib/NumberTheory/MulChar/Duality.lean,Mathlib/RingTheory/RootsOfUnity/Basic.lean |
6 |
7 |
['Ruben-VandeVelde', 'github-actions', 'xroblot'] |
urkud assignee:urkud |
0-37141 10 hours ago |
0-37141 10 hours ago |
10-45948 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-35437 9 hours ago |
0-41896 11 hours ago |
6-3214 6 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-34409 9 hours ago |
0-70118 19 hours ago |
0-70159 19 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-39911 1 day ago |
1-39911 1 day ago |
2-21500 2 days |
| 33113 |
sinhp author:sinhp |
feat(Category Theory): A natural isomorphism connecting Over.iteratedSlice and Over.map |
This PR provides the following useful nat iso:
```
def iteratedSliceForwardNaturalityIso {g : Over X} (p : f ⟶ g) :
iteratedSliceForward f ⋙ Over.map p.left ≅ Over.map p ⋙ iteratedSliceForward g := ...
def iteratedSliceEquivOverMapIso {f g : Over X} (p : f ⟶ g) :
f.iteratedSliceForward ⋙ Over.map p.left ⋙ g.iteratedSliceBackward ≅ Over.map p := ...
```
And it proves `post forget` is the same thing as `iteratedSliceForward`, thereby unlocking api of `Over.post` for iterated slice functor.
---
[](https://gitpod.io/from-referrer/)
|
t-category-theory
maintainer-merge
|
22/0 |
Mathlib/CategoryTheory/Comma/Over/Basic.lean |
1 |
12 |
['dagurtomas', 'github-actions', 'robin-carlier', 'sinhp'] |
nobody |
0-30925 8 hours ago |
0-30925 8 hours ago |
3-28705 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-29993 8 hours ago |
0-29993 8 hours ago |
0-29981 8 hours |
| 33794 |
Kha author:Kha |
perf(RingTheory/Polynomial/DegreeLT): optimize proof for kernel checking |
`Polynomial.taylorLinearEquiv_symm` used to take ~9s in the kernel on a fast machine and an astounding 2hrs when checked externally, without the module system restrictions. Making definitional rewrites explicit reduces type checking to <100ms in both scenarios. |
t-algebra label:t-algebra$ |
1/1 |
Mathlib/Algebra/Polynomial/Derivative.lean |
1 |
3 |
['Kha', 'github-actions', 'leanprover-radar'] |
nobody |
0-29771 8 hours ago |
0-31289 8 hours ago |
0-31333 8 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-29741 8 hours ago |
3-64132 3 days ago |
3-64178 3 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-29435 8 hours ago |
0-29501 8 hours ago |
0-29478 8 hours |
| 33551 |
metakunt author:metakunt |
feat(Data/Nat/Factorization/PrimePow): Add Nat.primeFactors_nontrivial_of_two_le_of_not_isPrimePow |
|
awaiting-author
t-data
|
11/0 |
Mathlib/Data/Nat/Factorization/PrimePow.lean |
1 |
3 |
['Ruben-VandeVelde', 'github-actions'] |
nobody |
1-14289 1 day ago |
1-14289 1 day ago |
4-18027 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-28696 7 hours ago |
0-28696 7 hours ago |
5-54170 5 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-27028 7 hours ago |
17-72694 17 days ago |
17-72737 17 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-26964 7 hours ago |
0-26964 7 hours ago |
1-24003 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-26922 7 hours ago |
0-26930 7 hours ago |
0-26969 7 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-25388 7 hours ago |
0-31243 8 hours ago |
0-31222 8 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-25074 6 hours ago |
3-2490 3 days ago |
15-76823 15 days |
| 33796 |
JohnnyTeutonic author:JohnnyTeutonic |
feat(LinearAlgebra/Matrix/Trace): trace map surjectivity |
This PR adds a surjectivity theorem for the matrix trace map.
### Summary
Proves that the matrix trace is surjective when the index type is nonempty, using single matrices as witnesses.
### Motivation
This is a building block for computing dimensions of classical Lie algebras (sl, so, sp) via rank-nullity. Since `sl n R = ker(trace)`, knowing trace is surjective allows us to compute `finrank(sl) = finrank(Matrix) - 1 = n² - 1`.
### Changes
- Add `trace_surjective` theorem in a new `Surjective` section
---
[](https://gitpod.io/from-referrer/)
|
easy
t-algebra
label:t-algebra$ |
6/0 |
Mathlib/LinearAlgebra/Matrix/Trace.lean |
1 |
4 |
['JohnnyTeutonic', 'github-actions', 'themathqueen'] |
nobody |
0-24842 6 hours ago |
0-24842 6 hours ago |
0-29758 8 hours |
| 32984 |
artie2000 author:artie2000 |
refactor: remove order instances from `SetLike` |
* Remove order instances from `SetLike`
* Add class `IsConcreteLE` for `SetLike` instances whose map is order-preserving
See discussion at https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/Abstracting.20the.20substructure.20lattice.20construction/with/563952738
---
[](https://gitpod.io/from-referrer/)
|
awaiting-author
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 |
27 |
['Vierkantor', 'alreadydone', 'artie2000', 'github-actions'] |
nobody |
0-78755 21 hours ago |
0-78755 21 hours ago |
21-70082 21 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-23299 6 hours ago |
0-23299 6 hours ago |
1-16144 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 |
1-85296 1 day ago |
5-75367 5 days ago |
5-75409 5 days |
| 33693 |
yoh-tanimoto author:yoh-tanimoto |
feat(Mathlib/Analysis/Normed/Module): add instances of `CompleteSpace` for `Submodules` and `ClosedSubmodule` |
add an instance of `CompleteSpace` for a `Submodule` of a Banach space `[NormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [CompleteSpace E]` which `IsClosed`.
In this relation, convert a lemma showing `IsClosed` to an instance for `ClosedSubmodule`.
motivation: Together with #28709, this makes it automatic that a `ClosedSubmodule` in a Hilbert space `HasOrthogonalProjection`.
discussion: https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/.60CompleteSpace.60.20for.20closed.20subtypes.20in.20a.20.60CompleteSpace.60 |
|
10/9 |
Mathlib/Analysis/InnerProductSpace/Orthogonal.lean,Mathlib/Analysis/InnerProductSpace/l2Space.lean,Mathlib/Analysis/Normed/Module/Basic.lean,Mathlib/Topology/Algebra/Module/ClosedSubmodule.lean |
4 |
2 |
['github-actions'] |
nobody |
0-20020 5 hours ago |
2-85755 2 days ago |
2-85732 2 days |
| 32856 |
stepan2698-cpu author:stepan2698-cpu |
feat: definition of an irreducible representation |
Define irreducible monoid representations over a field and prove that a monoid representation is irreducible iff the corresponding module over the monoid algebra is simple. |
t-algebra
new-contributor
label:t-algebra$ |
129/10 |
Mathlib.lean,Mathlib/RepresentationTheory/Irreducible.lean,Mathlib/RepresentationTheory/Subrepresentation.lean |
3 |
21 |
['Whysoserioushah', 'erdOne', 'github-actions', 'stepan2698-cpu'] |
kim-em assignee:kim-em |
3-11574 3 days ago |
27-10326 27 days ago |
27-10363 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-16742 4 hours ago |
0-16742 4 hours ago |
0-16720 4 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-16365 4 hours ago |
0-16365 4 hours ago |
0-16343 4 hours |
| 33804 |
tb65536 author:tb65536 |
feat(RingTheory/Localization/Ideal): `map` distributes over `inf` |
This PR proves that mapping ideals to the localization distributes over finite intersections, following the design of the analogous statements for `Ideal.radical`.
---
[](https://gitpod.io/from-referrer/)
|
t-algebra
t-ring-theory
label:t-algebra$ |
23/0 |
Mathlib/RingTheory/Localization/Ideal.lean |
1 |
1 |
['github-actions'] |
nobody |
0-15714 4 hours ago |
0-15714 4 hours ago |
0-15692 4 hours |
| 33271 |
jano-wol author:jano-wol |
feat: prove invtSubmoduleToLieIdeal_top |
---
[](https://gitpod.io/from-referrer/)
|
t-algebra label:t-algebra$ |
54/3 |
Mathlib/Algebra/Lie/Weights/Cartan.lean,Mathlib/Algebra/Lie/Weights/IsSimple.lean,Mathlib/Algebra/Lie/Weights/Killing.lean,Mathlib/Algebra/Lie/Weights/RootSystem.lean |
4 |
5 |
['github-actions', 'ocfnash'] |
chrisflav and ocfnash assignee:ocfnash assignee:chrisflav |
0-15011 4 hours ago |
0-15011 4 hours ago |
13-43334 13 days |
| 30640 |
SnirBroshi author:SnirBroshi |
feat(Combinatorics/SimpleGraph/Acyclic): acyclic and bridge theorems |
---
- [x] depends on: #30542
- [x] depends on: #30570
[](https://gitpod.io/from-referrer/)
|
t-combinatorics |
76/82 |
Mathlib/Combinatorics/SimpleGraph/Acyclic.lean,Mathlib/Combinatorics/SimpleGraph/Connectivity/Connected.lean |
2 |
7 |
['SnirBroshi', 'b-mehta', 'github-actions', 'mathlib4-dependent-issues-bot', 'mathlib4-merge-conflict-bot'] |
b-mehta assignee:b-mehta |
0-14006 3 hours ago |
1-82031 1 day ago |
31-43712 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-42795 1 day ago |
1-42797 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-10816 3 hours ago |
1-56099 1 day ago |
1-56144 1 day |
| 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-9286 2 hours ago |
0-72043 20 hours ago |
0-72087 20 hours |
| 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-31731 3 days ago |
4-29885 4 days ago |
4-29922 4 days |
| 33409 |
jsm28 author:jsm28 |
feat(LinearAlgebra/AffineSpace/Ceva): Ceva's theorem |
Add Ceva's theorem. Unlike various previous attempts, I think this in appropriate generality for mathlib; it starts with a version for an arbitary (possibly infinite) affinely independent family of points (not necessarily spanning the whole space), in any affine space over any ring, and with the second point given on each line not necessarily being on the opposite face, then deduces a simpler version for a finite family, then deduces versions for a triangle, now with actual cevians (lines between a vertex and a point on the opposite side), either just multiplying weights (here the ring requires no zero divisors) or expressed with a product of divisions equal to 1 (here it becomes a field).
This doesn't include any form of the converse (with a "concurrent or parallel" conclusion, and note that you don't need affine independence for the converse), or variants of the forward direction where you're given parallel lines rather than concurrent lines, but I think those things can reasonably be done in followups.
---
[](https://gitpod.io/from-referrer/)
|
t-algebra
t-euclidean-geometry
label:t-algebra$ |
243/0 |
Mathlib.lean,Mathlib/LinearAlgebra/AffineSpace/AffineSubspace/Basic.lean,Mathlib/LinearAlgebra/AffineSpace/Ceva.lean,docs/100.yaml,docs/1000.yaml |
5 |
10 |
['github-actions', 'jsm28', 'ocfnash', 'plby'] |
mariainesdff and ocfnash assignee:ocfnash assignee:mariainesdff |
0-38790 10 hours ago |
0-40024 11 hours ago |
10-8973 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 |
0-85290 23 hours ago |
4-56910 4 days ago |
4-56950 4 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-2825 47 minutes ago |
0-20524 5 hours ago |
0-20573 5 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 |
1-1888 1 day ago |
5-60708 5 days ago |
5-60744 5 days |