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 |
| 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/1 |
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 |
9 |
['chrisflav', 'erdOne', 'github-actions'] |
joneugster assignee:joneugster |
32-78998 1 month ago |
36-46287 1 month ago |
36-46261 36 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 |
88/1 |
Mathlib/Geometry/Euclidean/Sphere/OrthRadius.lean |
1 |
2 |
['github-actions', 'mathlib4-dependent-issues-bot'] |
JovanGerb assignee:JovanGerb |
29-37612 29 days ago |
29-39135 29 days ago |
38-83884 38 days |
| 27100 |
staroperator author:staroperator |
feat(ModelTheory): Presburger definability and semilinear sets |
This PR formalizes the classical result that Presburger definable sets are the same as semilinear sets. As an application of this result, we show that the graph of multiplication is not Presburger definable.
---
- [x] depends on: #26896
- [x] depends on: #27081
- [x] depends on: #27087
- [x] depends on: #27414
- [x] depends on: #32123
---
[](https://gitpod.io/from-referrer/)
|
t-logic |
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 |
28-79003 28 days ago |
32-28227 1 month ago |
34-28651 34 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 |
28-78993 28 days ago |
34-71303 1 month ago |
34-71344 34 days |
| 29942 |
smmercuri author:smmercuri |
feat(InfinitePlace/Completion): embeddings of `w.Completion` factor through embeddings of `v.Completion` when `w` extends `v` |
If `w : v.Extension L` is an extension of `v : InfinitePlace K` to `L`, then `extensionEmbedding w : L →+* ℂ` factors through `extensionEmbedding v : K →+* ℂ`.
---
- [x] depends on: #27978
- [x] depends on: #29969
- [x] depends on: #29944
[](https://gitpod.io/from-referrer/)
|
FLT |
89/14 |
Mathlib/Analysis/Normed/Field/WithAbs.lean,Mathlib/NumberTheory/NumberField/InfinitePlace/Completion.lean,Mathlib/NumberTheory/NumberField/InfinitePlace/Embeddings.lean,Mathlib/NumberTheory/NumberField/InfinitePlace/Ramification.lean,Mathlib/Topology/MetricSpace/Completion.lean |
5 |
5 |
['github-actions', 'mathlib4-dependent-issues-bot', 'mathlib4-merge-conflict-bot'] |
joelriou assignee:joelriou |
28-16386 28 days ago |
32-16356 1 month ago |
32-17449 32 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 |
27-78989 27 days ago |
31-69068 1 month ago |
31-71691 31 days |
| 32238 |
YaelDillies author:YaelDillies |
feat(Combinatorics/SimpleGraph): distributivity of box product over sum |
From ProofBench
---
[](https://gitpod.io/from-referrer/)
|
t-combinatorics
large-import
|
21/2 |
Mathlib/Combinatorics/SimpleGraph/Prod.lean |
1 |
1 |
['github-actions'] |
kmill assignee:kmill |
27-78979 27 days ago |
31-29926 1 month ago |
31-29958 31 days |
| 13740 |
YaelDillies author:YaelDillies |
feat: more robust ae notation |
Make sure that, when `μ : FiniteMeasure Ω`, `f =ᵐ[μ] g` elaborates to `f =ᵐ[↑μ] g` instead of complaining about `OuterMeasureClass (FiniteMeasure Ω) (Set Ω) ℝ≥0∞` not existing.
[Zulip](https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/ae.20of.20a.20finite.20measure)
---
[](https://gitpod.io/from-referrer/)
|
t-meta
t-measure-probability
|
67/8 |
Mathlib/MeasureTheory/Integral/Bochner/L1.lean,Mathlib/MeasureTheory/Measure/Decomposition/IntegralRNDeriv.lean,Mathlib/MeasureTheory/Measure/MeasureSpaceDef.lean,Mathlib/MeasureTheory/OuterMeasure/AE.lean,Mathlib/MeasureTheory/OuterMeasure/BorelCantelli.lean,Mathlib/Probability/Notation.lean |
6 |
40 |
['YaelDillies', 'eric-wieser', 'github-actions', 'leanprover-community-bot-assistant', 'thorimur', 'urkud'] |
RemyDegenne and thorimur assignee:RemyDegenne assignee:thorimur |
25-9121 25 days ago |
55-26097 1 month ago |
55-26051 55 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
large-import
|
117/63 |
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 |
4 |
18 |
['YaelDillies', 'github-actions', 'mitchell-horner'] |
YaelDillies assignee:YaelDillies |
24-42044 24 days ago |
24-45062 24 days ago |
25-47 25 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 |
23-16754 23 days ago |
23-16873 23 days ago |
28-11304 28 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 |
23-812 23 days ago |
29-4014 29 days ago |
29-6966 29 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 |
22-78995 22 days ago |
25-85326 25 days ago |
27-3525 27 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 |
22-41142 22 days ago |
22-41171 22 days ago |
22-48748 22 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 |
21-78994 21 days ago |
25-66309 25 days ago |
25-66298 25 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 |
19-9951 19 days ago |
19-24137 19 days ago |
39-70689 39 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 |
18-25786 18 days ago |
22-39991 22 days ago |
22-40280 22 days |
| 32660 |
dagurtomas author:dagurtomas |
feat(Topology): sandwich lemmas for profinite sets |
We add two lemmas:
- `exists_clopen_of_closed_subset_open`: in a totally disconnected compact Hausdorff space `X`, if `Z ⊆ U` are subsets with `Z` closed and `U` open, there exists a clopen `C` with `Z ⊆ C ⊆ U`.
- `exists_clopen_partition_of_clopen_cover`: Let `X` be a totally disconnected compact Hausdorff space, `D i ⊆ X` a finite family of clopens, and `Z i ⊆ D i` closed. Assume that the `Z i` are pairwise disjoint. Then there exist clopens `Z i ⊆ C i ⊆ D i` with the `C i` disjoint, and such that `∪ D i ⊆ ∪ C i`.
These are required to prove injectivity of light profinite sets, see #31754
---
[](https://gitpod.io/from-referrer/)
|
t-topology |
94/0 |
Mathlib/Topology/Separation/Profinite.lean |
1 |
1 |
['github-actions'] |
PatrickMassot assignee:PatrickMassot |
17-78994 17 days ago |
21-4190 21 days ago |
21-4226 21 days |
| 32665 |
erdOne author:erdOne |
feat(RingTheory): quasi-finite algebras |
---
[](https://gitpod.io/from-referrer/)
|
t-ring-theory |
341/2 |
Mathlib.lean,Mathlib/RingTheory/LocalRing/ResidueField/Ideal.lean,Mathlib/RingTheory/QuasiFinite/Basic.lean |
3 |
1 |
['github-actions'] |
kbuzzard assignee:kbuzzard |
17-78993 17 days ago |
20-84427 20 days ago |
20-84449 20 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 |
16-78980 16 days ago |
21-65425 21 days ago |
25-10306 25 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 |
16-63123 16 days ago |
23-9566 23 days ago |
23-9607 23 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 |
16-21594 16 days ago |
21-16462 21 days ago |
21-16725 21 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
From FormalConjectures
---
[](https://gitpod.io/from-referrer/)
|
t-combinatorics |
42/30 |
Mathlib/Combinatorics/SimpleGraph/Basic.lean,Mathlib/Combinatorics/SimpleGraph/Coloring.lean |
2 |
1 |
['github-actions'] |
b-mehta assignee:b-mehta |
15-78992 15 days ago |
21-19663 21 days ago |
21-19696 21 days |
| 32401 |
ADedecker author:ADedecker |
feat: monotonicity of D^n(U) in n and in U as CLMs |
---
[](https://gitpod.io/from-referrer/)
|
t-analysis |
170/3 |
Mathlib/Analysis/Distribution/ContDiffMapSupportedIn.lean,Mathlib/Analysis/Distribution/TestFunction.lean |
2 |
n/a |
['ADedecker', 'faenuccio', 'github-actions', 'mathlib4-merge-conflict-bot'] |
nobody |
15-16880 15 days ago |
unknown |
unknown |
| 32806 |
erdOne author:erdOne |
feat(RingTheory): base change of ideal with flat quotients |
---
[](https://gitpod.io/from-referrer/)
|
t-ring-theory |
108/0 |
Mathlib/RingTheory/Flat/Equalizer.lean |
1 |
1 |
['github-actions'] |
kbuzzard assignee:kbuzzard |
14-78975 14 days ago |
18-20075 18 days ago |
18-20108 18 days |
| 31449 |
kim-em author:kim-em |
feat(SemilocallySimplyConnected): definition and alternative formulation |
Note: Proofs in this PR were developed with assistance from Claude. |
|
116/0 |
Mathlib.lean,Mathlib/AlgebraicTopology/FundamentalGroupoid/SemilocallySimplyConnected.lean,Mathlib/Topology/Path.lean |
3 |
4 |
['ADedecker', 'github-actions', 'kim-em', 'mathlib4-merge-conflict-bot'] |
ADedecker assignee:ADedecker |
14-69167 14 days ago |
21-76783 21 days ago |
42-72850 42 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 |
14-28134 14 days ago |
20-48034 20 days ago |
44-25008 44 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 |
13-79002 13 days ago |
17-68352 17 days ago |
17-68385 17 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$ |
118/10 |
Mathlib.lean,Mathlib/RepresentationTheory/Irreducible.lean,Mathlib/RepresentationTheory/Subrepresentation.lean |
3 |
15 |
['Whysoserioushah', 'github-actions', 'stepan2698-cpu'] |
kim-em assignee:kim-em |
13-78992 13 days ago |
17-4019 17 days ago |
17-4054 17 days |
| 32773 |
Hagb author:Hagb |
feat(Algebra/GroupWithZero/NonZeroDivisors): add some lemmas about multiplication |
Similar to `Is{Left,Right,}Regular.mul`.
---
`Is{Left,Right,}Regular.mul`: https://github.com/leanprover-community/mathlib4/blob/c671bc4215d64bd9cc8a84fdec9a12bd33fdcd26/Mathlib/Algebra/Regular/Basic.lean#L59-L76
[](https://gitpod.io/from-referrer/)
|
t-algebra label:t-algebra$ |
23/0 |
Mathlib/Algebra/GroupWithZero/NonZeroDivisors.lean |
1 |
4 |
['Hagb', 'Ruben-VandeVelde', 'github-actions'] |
kim-em assignee:kim-em |
13-23372 13 days ago |
13-23419 13 days ago |
18-52050 18 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 |
13-16324 13 days ago |
13-16327 13 days ago |
19-13580 19 days |
| 32672 |
tb65536 author:tb65536 |
feat: haar measures on short exact sequences |
This PR defines the notion of a short exact sequence of topological groups, and proves that if `1 → A → B → C → 1` is a short exact sequence of topological groups, then Haar measures on `A` and `C` induce a Haar measure on `B`.
The final result of the file is a consequence needed for FLT: If `B → C` is injective on an open set `U`, then `U` has bounded measure.
---
[](https://gitpod.io/from-referrer/)
|
t-topology
t-measure-probability
FLT
|
378/0 |
Mathlib.lean,Mathlib/MeasureTheory/Measure/Haar/Extension.lean,Mathlib/Topology/Algebra/Group/Extension.lean |
3 |
6 |
['RemyDegenne', 'github-actions', 'kbuzzard', 'tb65536'] |
urkud assignee:urkud |
12-79000 12 days ago |
16-13543 16 days ago |
19-63047 19 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 |
12-78994 12 days ago |
18-61949 18 days ago |
18-61924 18 days |
| 32836 |
YaelDillies author:YaelDillies |
feat(Algebra): characterise when a submodule constructor is equal to `⊥` |
---
[](https://gitpod.io/from-referrer/)
|
t-algebra label:t-algebra$ |
36/3 |
Mathlib/Algebra/Algebra/NonUnitalSubalgebra.lean,Mathlib/Algebra/Group/Submonoid/Defs.lean,Mathlib/Algebra/Group/Subsemigroup/Defs.lean,Mathlib/Algebra/Module/Submodule/Lattice.lean |
4 |
7 |
['YaelDillies', 'erdOne', 'github-actions'] |
Vierkantor assignee:Vierkantor |
12-78992 12 days ago |
16-40221 16 days ago |
16-72293 16 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 |
12-67644 12 days ago |
23-8288 23 days ago |
23-8319 23 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 |
12-67184 12 days ago |
22-71487 22 days ago |
22-71529 22 days |
| 31925 |
alreadydone author:alreadydone |
feat(Topology): étalé space associated to a predicate on sections |
---
migrated from #22782
[](https://gitpod.io/from-referrer/)
|
t-topology |
899/164 |
Mathlib.lean,Mathlib/AlgebraicGeometry/ProjectiveSpectrum/StructureSheaf.lean,Mathlib/Data/Set/Operations.lean,Mathlib/Geometry/Manifold/Sheaf/Smooth.lean,Mathlib/Logic/Equiv/Basic.lean,Mathlib/Topology/EtaleSpace.lean,Mathlib/Topology/IsLocalHomeomorph.lean,Mathlib/Topology/Sheaves/LocalPredicate.lean,Mathlib/Topology/Sheaves/Sheafify.lean,Mathlib/Topology/Sheaves/Stalks.lean |
10 |
13 |
['adamtopaz', 'alreadydone', 'github-actions', 'mathlib4-merge-conflict-bot'] |
adamtopaz assignee:adamtopaz |
12-16046 12 days ago |
12-20018 12 days ago |
17-15502 17 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 |
12-4208 12 days ago |
12-4272 12 days ago |
20-35269 20 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 |
11-83535 11 days ago |
11-83759 11 days ago |
20-1217 20 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 |
11-83261 11 days ago |
11-83753 11 days ago |
22-1967 22 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 |
11-78992 11 days ago |
15-17232 15 days ago |
18-4193 18 days |
| 32823 |
erdOne author:erdOne |
feat(RingTheory): construct etale neighborhood that isolates point in fiber |
---
[](https://gitpod.io/from-referrer/)
|
t-ring-theory |
280/1 |
Mathlib.lean,Mathlib/Algebra/Polynomial/Monic.lean,Mathlib/RingTheory/Etale/QuasiFinite.lean,Mathlib/RingTheory/Polynomial/UniversalFactorizationRing.lean,Mathlib/RingTheory/Spectrum/Prime/Noetherian.lean,Mathlib/RingTheory/Spectrum/Prime/RingHom.lean,Mathlib/RingTheory/Spectrum/Prime/Topology.lean |
7 |
2 |
['github-actions', 'jcommelin'] |
chrisflav assignee:chrisflav |
11-78991 11 days ago |
15-23306 15 days ago |
17-63664 17 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$ |
297/156 |
Mathlib/Algebra/Order/Archimedean/Class.lean,Mathlib/Algebra/Order/Module/Archimedean.lean,Mathlib/Algebra/Order/Module/HahnEmbedding.lean |
3 |
3 |
['alreadydone', 'github-actions', 'wwylele'] |
Vierkantor assignee:Vierkantor |
11-78990 11 days ago |
15-71782 15 days ago |
15-71758 15 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 |
11-43190 11 days ago |
12-71601 12 days ago |
12-71644 12 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 |
11-29477 11 days ago |
36-57540 1 month ago |
37-2030 37 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 |
11-825 11 days ago |
11-851 11 days ago |
23-56199 23 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 |
11-560 11 days ago |
11-67415 11 days ago |
29-79316 29 days |
| 31960 |
urkud author:urkud |
feat: a lower bound for the volume of a cone on the unit sphere |
---
- [x] depends on: #31956
- [x] depends on: #31957
[](https://gitpod.io/from-referrer/)
|
t-measure-probability |
95/0 |
Mathlib/MeasureTheory/Constructions/HaarToSphere.lean |
1 |
6 |
['PatrickMassot', 'github-actions', 'mathlib4-dependent-issues-bot', 'mathlib4-merge-conflict-bot', 'urkud'] |
hrmacbeth assignee:hrmacbeth |
10-85792 10 days ago |
35-5607 1 month ago |
35-8151 35 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 |
10-79010 10 days ago |
14-4173 14 days ago |
14-6678 14 days |
| 32541 |
YaelDillies author:YaelDillies |
chore: import Tactic.Attr.Register privately |
This is mostly to start a discussion: Should basic tactic files like this one be re-exported by all files out of them being basic, or whether they should be explicitly imported by the few files that actually need it.
Eg in #32245 Andrew and I are adding a new simp attribute, and it's a bit silly that we have to rebuild all of mathlib because that file is re-exported everywhere.
---
[](https://gitpod.io/from-referrer/)
|
large-import |
43/9 |
Mathlib/Algebra/Free.lean,Mathlib/CategoryTheory/Monoidal/Mon_.lean,Mathlib/Control/Applicative.lean,Mathlib/Control/Basic.lean,Mathlib/Control/Functor.lean,Mathlib/Control/Monad/Basic.lean,Mathlib/Control/Traversable/Basic.lean,Mathlib/Control/Traversable/Equiv.lean,Mathlib/Control/Traversable/Lemmas.lean,Mathlib/Data/Prod/Basic.lean,Mathlib/Data/Set/Operations.lean,Mathlib/Logic/Basic.lean,Mathlib/Logic/Equiv/Defs.lean,Mathlib/Logic/Function/Basic.lean,Mathlib/Logic/Function/Defs.lean,Mathlib/Logic/Nontrivial/Basic.lean,Mathlib/Tactic/Attr/Core.lean,Mathlib/Tactic/HigherOrder.lean,Mathlib/Tactic/Zify.lean |
19 |
5 |
['EtienneC30', 'YaelDillies', 'artie2000', 'github-actions'] |
kex-y assignee:kex-y |
10-79009 10 days ago |
23-21169 23 days ago |
23-31460 23 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 |
10-79006 10 days ago |
17-72120 17 days ago |
17-72126 17 days |
| 32956 |
adomani author:adomani |
fix: `simp_rw` does not hide goals |
Before this change, using `simp_rw` would cause the infoview to show only one goal, instead of all active goals, in the range `simp_rw [`. In particular, with the cursor on `|simp_rw`, if there are several goals, you would only see one.
This PR changes the behaviour to show all goals in the range `simp_rw [`. Once you "step in" the brackets, only a single goal is shown.
[Zulip](https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/.60simp_rw.60.20hides.20a.20goal/with/564020391)
---
[](https://gitpod.io/from-referrer/)
|
t-meta |
2/5 |
Mathlib/Tactic/SimpRw.lean |
1 |
5 |
['adomani', 'github-actions', 'grunweg', 'plp127'] |
adamtopaz assignee:adamtopaz |
10-79004 10 days ago |
14-39093 14 days ago |
14-39429 14 days |
| 31579 |
xroblot author:xroblot |
feat(Data/Nat/Digits): prove the bijection induced by `Nat.ofDigits` and use it to compute the sum of the sum of digits |
We prove that `Nat.ofDigits` induces a bijection between the set of list of natural integers of length `l`
with coefficients `< b` and the set of natural integers `< b ^ l` and develop some API.
As a application, we prove that
```lean
theorem Nat.sum_digits_sum_eq {b : ℕ} (hb : 1 < b) (l : ℕ) :
∑ x ∈ Finset.range (b ^ l), (b.digits x).sum = l * b ^ (l - 1) * b.choose 2
```
---
|
t-data |
215/0 |
Mathlib/Data/Nat/Digits/Lemmas.lean |
1 |
14 |
['TwoFX', 'eric-wieser', 'github-actions', 'mathlib4-merge-conflict-bot', 'xroblot'] |
TwoFX assignee:TwoFX |
10-45966 10 days ago |
10-45966 10 days ago |
46-50930 46 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 |
10-44741 10 days ago |
10-44800 10 days ago |
32-23722 32 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 |
10-22731 10 days ago |
11-46915 11 days ago |
25-47834 25 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 |
9-78980 9 days ago |
20-4874 20 days ago |
20-4909 20 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 |
9-78979 9 days ago |
19-27001 19 days ago |
19-27080 19 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 |
9-78976 9 days ago |
15-28552 15 days ago |
15-28879 15 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 |
9-78975 9 days ago |
13-69782 13 days ago |
13-69819 13 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 |
9-78972 9 days ago |
13-3075 13 days ago |
13-3049 13 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 |
9-73006 9 days ago |
9-73030 9 days ago |
19-28696 19 days |
| 32744 |
NoneMore author:NoneMore |
feat(ModelTheory/Definablity): add `DefinableFun` definition and lemmas |
This PR adds two basic shapes of definable sets and `DefinableFun` definition with relevant lemmas.
The main result is `Set.Definable.preimage_of_map` asserting that the preimage of a definable set under a definable map is definable.
There are also some tool lemmas derived by the preimage lemma.
---
[](https://gitpod.io/from-referrer/)
|
t-logic
new-contributor
|
151/0 |
Mathlib/ModelTheory/Definability.lean |
1 |
58 |
['NoneMore', 'github-actions', 'staroperator'] |
fpvandoorn assignee:fpvandoorn |
9-62184 9 days ago |
18-63651 18 days ago |
19-22555 19 days |
| 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/)
|
t-algebra
large-import
label:t-algebra$ |
310/79 |
Mathlib/RingTheory/PicardGroup.lean |
1 |
23 |
['alreadydone', 'erdOne', 'github-actions', 'jcommelin', 'mathlib4-dependent-issues-bot', 'mathlib4-merge-conflict-bot'] |
mariainesdff assignee:mariainesdff |
9-41899 9 days ago |
9-41925 9 days ago |
39-38039 39 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 |
8-78982 8 days ago |
12-23914 12 days ago |
12-31238 12 days |
| 31315 |
Parcly-Taxel author:Parcly-Taxel |
feat: IMO 2010 Q5 |
See [#general > Panic in rw: Nat.pow exponent is too big @ 💬](https://leanprover.zulipchat.com/#narrow/channel/113488-general/topic/Panic.20in.20rw.3A.20Nat.2Epow.20exponent.20is.20too.20big/near/513294906) and leanprover/lean4#11713 for why 2010 and 11 are replaced with variables. |
maintainer-merge
IMO
|
245/0 |
Archive.lean,Archive/Imo/Imo2010Q5.lean |
2 |
6 |
['Parcly-Taxel', 'github-actions', 'jsm28', 'nomeata'] |
jsm28 assignee:jsm28 |
8-78981 8 days ago |
11-83267 11 days ago |
33-80348 33 days |
| 33052 |
JovanGerb author:JovanGerb |
feat: replace `rw??` tactic with `#infoview_search` command |
This PR introduces the `#infoview_search` command. It gives an improved way of interacting with the library search from `rw??`, and hence this PR also deprecates `rw??` (`rw??` still works, but it displays a warning message suggesting to use `#infoview_search` instead).
The difference is that `#infoview_search` is a command, so you type it once, and then you can use rewrite search in any tactic state in any place. This is more convenient than having to write out `rw??` every time.
I have many improvements planned for `#infoview_search`, but this PR simply gives it the same capabilities that `rw??` currently has. One of those improvements is to also do `apply` search, and `apply at` search. That is why the name doesn't contain `rw` anymore.
To prepare for more code developments around `#infoview_search`, I've moved the relevant files into a new folder `Mathlib.Tactic.InfoviewSearch`.
Note that one annoyance with writing `#infoview_search` is that there is a linter warning. Should I remove the `#` from the command, or are we happy with this?
```
`#`-commands, such as '#infoview_search', are not allowed in 'Mathlib'
Note: This linter can be disabled with `set_option linter.hashCommand false`
```
---
[](https://gitpod.io/from-referrer/)
|
t-meta
file-removed
|
100/59 |
Mathlib.lean,Mathlib/Tactic.lean,Mathlib/Tactic/Common.lean,Mathlib/Tactic/InfoviewSearch/InteractiveUnfold.lean,Mathlib/Tactic/InfoviewSearch/LibraryRewrite.lean,MathlibTest/LibraryRewrite.lean |
6 |
1 |
['github-actions'] |
adamtopaz assignee:adamtopaz |
8-78973 8 days ago |
12-17646 12 days ago |
12-17697 12 days |
| 33060 |
xgenereux author:xgenereux |
feat: nontrivial instances for valuation with `ℤᵐ⁰` as codomain |
Added instances so that `v.IsNontrivial` now implies `Nontrivial (valueMonoid v)` and `Nontrivial (valueGroup v)`.
Also added nontriviality instances for existing `ℤᵐ⁰` valuations. This is particularly useful because it allows [`Valuation.IsRankOneDiscrete.mk'`](https://leanprover-community.github.io/mathlib4_docs/Mathlib/RingTheory/Valuation/Discrete/Basic.html#Valuation.IsRankOneDiscrete.mk') to synthesize `IsRankOneDiscrete`.
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/)
|
|
33/29 |
Mathlib/NumberTheory/FunctionField.lean,Mathlib/RingTheory/DedekindDomain/AdicValuation.lean,Mathlib/RingTheory/Valuation/Basic.lean,Mathlib/RingTheory/Valuation/Discrete/Basic.lean |
4 |
5 |
['github-actions', 'leanprover-radar', 'xgenereux'] |
tb65536 assignee:tb65536 |
8-78970 8 days ago |
12-9477 12 days ago |
12-9451 12 days |
| 26986 |
WangYiran01 author:WangYiran01 |
feat(Partition): add bijection for partitions with max part ≤ r |
This PR adds a new theorem `partition_max_equals_bound` to `Mathlib.Combinatorics.Enumerative.Partition`.
It constructs a bijection between:
- The set of partitions of `n` in which `r ∈ π.parts` and all parts are `≤ r`, and
- The set of partitions of `n - r` whose largest part is at most `r`.
This provides a constructive proof via removing/adding `r` from/to the partition multiset, in line with classical enumerative combinatorics.
Contributed by Yiran Wang.
|
t-combinatorics
new-contributor
|
92/0 |
Mathlib/Combinatorics/Enumerative/Partition/Basic.lean,Mathlib/Data/Multiset/Lattice.lean |
2 |
16 |
['WangYiran01', 'github-actions', 'jcommelin', 'kckennylau', 'kim-em', 'mathlib4-merge-conflict-bot'] |
b-mehta assignee:b-mehta |
8-51923 8 days ago |
8-52151 8 days ago |
112-29710 112 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 |
8-48196 8 days ago |
9-82865 9 days ago |
148-28155 148 days |
| 33193 |
YuvalFilmus author:YuvalFilmus |
feat(Powerset): Results related to image |
Add lemmas regarding relations between image and powerset.
These will be used in a future PR regarding Lagrange interpolants.
---
[](https://gitpod.io/from-referrer/)
|
t-data |
36/0 |
Mathlib/Data/Finset/Powerset.lean |
1 |
1 |
['github-actions'] |
nobody |
8-40946 8 days ago |
8-40950 8 days ago |
8-40988 8 days |
| 32939 |
JovanGerb author:JovanGerb |
fix(to_additive): don't translate into non-existent names |
This PR fixes a problem in `to_additive`/`to_dual` where the function `findPrefixTranslation` can find a translation to a constant that doesn't actually exist. If it doesn't exist, don't do the translation.
I considered instead modifying `findPrefixTranslation` so that it only works for specific declarations. But it turns out that we do rely on this way of translating in a number of ways that are not so easy to get rid of.
---
[](https://gitpod.io/from-referrer/)
|
t-meta |
2/6 |
Mathlib/Algebra/BigOperators/Finsupp/Basic.lean,Mathlib/Tactic/Translate/Core.lean |
2 |
1 |
['github-actions'] |
adamtopaz assignee:adamtopaz |
8-36684 8 days ago |
14-41200 14 days ago |
14-60949 14 days |
| 32880 |
0xTerencePrime author:0xTerencePrime |
feat(Analysis/Asymptotics): define subpolynomial growth |
## Main definitions
* `Asymptotics.IsSubpolynomial l f g`: A function `f` has subpolynomial growth with respect to `g` along filter `l` if `f = O(1 + ‖g‖^k)` for some natural `k`.
## Main results
* `IsSubpolynomial.const`: Constant functions have subpolynomial growth
* `IsSubpolynomial.id`: Identity has subpolynomial growth
* `IsSubpolynomial.add`: Closure under addition
* `IsSubpolynomial.neg`: Closure under negation
* `IsSubpolynomial.sub`: Closure under subtraction
* `IsSubpolynomial.mul`: Closure under multiplication
* `IsSubpolynomial.pow`: Closure under powers
* `isSubpolynomial_iff_one_add`: Equivalence with `(1 + ‖g‖)^k` formulation
* `IsSubpolynomial.uniform`: Uniform bounds for finite families
## Implementation notes
The definition uses `1 + ‖g‖^k` rather than `(1 + ‖g‖)^k` as the primary form, with the equivalence established in `isSubpolynomial_iff_one_add`. Four private auxiliary lemmas handle the key inequalities needed for closure proofs.
Closes #32658
|
t-analysis
new-contributor
|
289/0 |
Mathlib.lean,Mathlib/Analysis/Asymptotics/Subpolynomial.lean |
2 |
2 |
['github-actions', 'j-loreaux'] |
ADedecker assignee:ADedecker |
8-22332 8 days ago |
16-24123 16 days ago |
16-24163 16 days |
| 30129 |
vlad902 author:vlad902 |
feat(SimpleGraph): define and prove basic theory of vertex covers |
Define a predicate `IsVertexCover G C` to state that `C` is a vertex cover of `G`. Furthermore, `G.vertexCoverNum` is the cardinality of the minimum vertex cover of G. Then prove the basic theory of how these definitions relate to the empty and complete graphs and their relationship with graph homs/isos.
---
- [x] depends on: #29833
- [x] depends on: #30136
- [x] depends on: #30137
- [x] depends on: #32267
[](https://gitpod.io/from-referrer/)
|
t-combinatorics |
226/3 |
Mathlib.lean,Mathlib/Combinatorics/SimpleGraph/Basic.lean,Mathlib/Combinatorics/SimpleGraph/Clique.lean,Mathlib/Combinatorics/SimpleGraph/VertexCover.lean |
4 |
66 |
['SnirBroshi', 'YaelDillies', 'github-actions', 'mathlib4-dependent-issues-bot', 'mathlib4-merge-conflict-bot', 'vlad902'] |
YaelDillies assignee:YaelDillies |
8-22204 8 days ago |
10-48906 10 days ago |
21-66274 21 days |
| 30981 |
jsm28 author:jsm28 |
feat(Geometry/Euclidean/Angle/Bisector): oriented angle bisection mod π |
Add lemmas relating equal distance to two lines to bisecting the angle between them mod π (expressed as usual as equality of twice angles), building on the previous lemmas (#30477) dealing with bisection mod 2π.
---
- [ ] depends on: #30474
- [ ] depends on: #30477
- [ ] depends on: #30600
- [ ] depends on: #30703
[](https://gitpod.io/from-referrer/)
|
t-euclidean-geometry |
193/50 |
Mathlib/Geometry/Euclidean/Angle/Bisector.lean |
1 |
12 |
['JovanGerb', 'github-actions', 'jsm28', 'mathlib4-dependent-issues-bot', 'mathlib4-merge-conflict-bot'] |
JovanGerb assignee:JovanGerb |
8-21346 8 days ago |
41-43560 1 month ago |
46-388 46 days |
| 32757 |
AntoineChambert-Loir author:AntoineChambert-Loir |
feat(LinearAlgebra/Transvection): the determinant of a transvection is equal to 1. |
Prove that the determinant of a transvection is equal to 1
The proof goes by showing that the determinant of `LinearMap.transvection f v` is `1 + f v` (even if `f v` is nonzero).
I first treat the case of a field, distinguishing whether `f v = 0` (so that we get
a transvection) or not (so that we have a dilation).
Then, by base change to the field of fractions, I can handle the case of a domain. Finally, the general case is treated by base change from the “universal case” where the base ring is the ring of polynomials in $$2n$$ indeterminates corresponding to the coefficients of $$f$$ and $$v$$.
---
- [ ] depends on: #31138
- [ ]
[](https://gitpod.io/from-referrer/)
|
|
253/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 |
7-84389 7 days ago |
unknown |
unknown |
| 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 |
7-78998 7 days ago |
11-18608 11 days ago |
11-18668 11 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 |
7-78995 7 days ago |
12-56520 12 days ago |
12-56561 12 days |
| 33033 |
kim-em author:kim-em |
feat(Tactic/Choose): add type annotation support |
This PR adds support for type annotations in the `choose` tactic, similar to how `intro` supports them. This allows writing:
```lean
choose (n : ℕ) (hn : n > 0) using h
```
instead of just `choose n hn using h`. The type annotation is checked against the actual type from the existential, and an error is raised if they don't match.
This is useful for pedagogical purposes and for catching mistakes early.
Requested on Zulip: https://leanprover.zulipchat.com/#narrow/channel/187764-Lean-for-teaching/topic/adding.20type.20annotation.20to.20.60choose.60/near/564323626
🤖 Prepared with Claude Code |
t-meta |
157/21 |
Mathlib/Tactic/Choose.lean,MathlibTest/choose.lean |
2 |
17 |
['AlexKontorovich', 'eric-wieser', 'fpvandoorn', 'github-actions', 'kim-em'] |
joneugster assignee:joneugster |
7-78994 7 days ago |
11-3399 11 days ago |
11-74198 11 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 |
7-78993 7 days ago |
11-3420 11 days ago |
11-65166 11 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 |
7-78992 7 days ago |
10-82462 10 days ago |
11-42006 11 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 |
7-78990 7 days ago |
11-37512 11 days ago |
11-37556 11 days |
| 33099 |
YaelDillies author:YaelDillies |
chore(RingTheory/FiniteType): move `MonoidAlgebra` lemmas earlier |
... and deduce them from a missing `Finsupp` lemma
---
[](https://gitpod.io/from-referrer/)
|
t-algebra
large-import
label:t-algebra$ |
56/65 |
Mathlib/Algebra/MonoidAlgebra/Module.lean,Mathlib/LinearAlgebra/Finsupp/Supported.lean,Mathlib/RingTheory/FiniteType.lean |
3 |
1 |
['github-actions'] |
jcommelin assignee:jcommelin |
7-78988 7 days ago |
11-17132 11 days ago |
11-17419 11 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 |
7-78985 7 days ago |
11-5917 11 days ago |
11-5899 11 days |
| 33112 |
alreadydone author:alreadydone |
feat(GroupAction): `(M →[M] M) ≃* Mᵐᵒᵖ` |
This comes up in #33108 in the form that permutations of a group commuting with the left multiplications are the right multiplications.
The Semiring versions are already in mathlib.
---
[](https://gitpod.io/from-referrer/)
|
t-algebra
t-group-theory
label:t-algebra$ |
40/2 |
Mathlib/GroupTheory/GroupAction/Hom.lean |
1 |
1 |
['github-actions'] |
mattrobball assignee:mattrobball |
7-78984 7 days ago |
10-85043 10 days ago |
10-85018 10 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 |
7-73232 7 days ago |
7-74998 7 days ago |
12-72117 12 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 |
7-61318 7 days ago |
7-72918 7 days ago |
7-72959 7 days |
| 32215 |
jonasvanderschaaf author:jonasvanderschaaf |
feat(ModelTheory/Types): Construct a topology on CompleteType and prove the space is TotallySeparated |
---
- [x] depends on: #32213
[](https://gitpod.io/from-referrer/)
|
t-topology
t-logic
new-contributor
|
97/0 |
Mathlib.lean,Mathlib/ModelTheory/Topology/Types.lean,Mathlib/ModelTheory/Types.lean,Mathlib/Tactic/Linter/DirectoryDependency.lean |
4 |
11 |
['Vierkantor', 'anishrajeev', 'dagurtomas', 'github-actions', 'jonasvanderschaaf', 'mathlib4-dependent-issues-bot', 'mathlib4-merge-conflict-bot', 'plp127'] |
dagurtomas assignee:dagurtomas |
7-42381 7 days ago |
13-52006 13 days ago |
20-62600 20 days |
| 33111 |
SnirBroshi author:SnirBroshi |
feat(Order/Monotone/Defs): weaken hypothesis of `injective_of_le_imp_le` |
`injective_of_le_imp_le` requires `∀ x y, f x ≤ f y → x ≤ y`, but `∀ x y, f x = f y → x ≤ y` is sufficient.
Also rename the weakened`injective_of_le_imp_le` to `Function.Injective.of_eq_imp_le` and `injective_of_lt_imp_ne` to `Function.Injective.of_lt_imp_ne` to allow for dot notation.
---
[](https://gitpod.io/from-referrer/)
|
t-order |
19/18 |
Archive/Imo/Imo1994Q1.lean,Archive/Wiedijk100Theorems/AscendingDescendingSequences.lean,Mathlib/Algebra/Prime/Lemmas.lean,Mathlib/Analysis/Convex/Basic.lean,Mathlib/Data/Finset/Powerset.lean,Mathlib/Order/Monotone/Defs.lean,Mathlib/RingTheory/Localization/Submodule.lean,Mathlib/Topology/ClopenBox.lean |
8 |
10 |
['SnirBroshi', 'github-actions', 'j-loreaux', 'themathqueen'] |
Vierkantor assignee:Vierkantor |
6-85218 6 days ago |
7-2740 7 days ago |
10-65399 10 days |
| 32940 |
JovanGerb author:JovanGerb |
perf(to_fun): remove `ofNat(n)` in `Pi.ofNat_def` |
Looking at the `simp` trace of the `@[to_fun]` attribute is quite painful because it tries applying `Pi.ofNat_def` at every subexpression. This is due to the `ofNat(n)` term at the root of the expression. The fact that the tests still work means that the lemma is still applied correctly when needed
---
[](https://gitpod.io/from-referrer/)
|
t-data |
1/1 |
Mathlib/Data/Nat/Cast/Basic.lean |
1 |
6 |
['JovanGerb', 'github-actions', 'grunweg', 'leanprover-radar'] |
pechersky assignee:pechersky |
6-78993 6 days ago |
14-66266 14 days ago |
14-66301 14 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'] |
alexjbest assignee:alexjbest |
6-78991 6 days ago |
10-74586 10 days ago |
12-31599 12 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 |
5 |
['github-actions', 'j-loreaux', 'leanprover-radar', 'themathqueen'] |
dagurtomas assignee:dagurtomas |
6-78990 6 days ago |
11-7067 11 days ago |
11-14982 11 days |
| 33124 |
riccardobrasca author:riccardobrasca |
feat(RepresentationTheory/Homological/GroupCohomology/Hilbert90): add Hilbert 90 for cyclic groups |
Let `L/K` be a finite extension of fields. Noether's generalization of Hilbert's Theorem 90 is that the 1st group cohomology $H^1(Aut_K(L), L^\times)$ is trivial. Hilbert's original statement was that if $L/K$ is Galois, and $Gal(L/K)$ is cyclic, generated by an element `σ`, then for every `x : L` such that $N_{L/K}(x) = 1,$ there exists `y : L` such that $x = y/σ(y)$. We prove that in this PR, using the fact that `H¹(G, A) ≅ Ker(N_A)/(ρ(g) - 1)(A)` for any finite cyclic group `G` with generator `g`, and then applying Noether's generalization.
Co-authored-by: [101damnations](https://github.com/101damnations)
---
This was originally #27366, and Amelia did all the work, I am just adopting the PR.
[](https://gitpod.io/from-referrer/)
|
t-number-theory
large-import
|
108/10 |
Mathlib/RepresentationTheory/Homological/GroupCohomology/Hilbert90.lean,Mathlib/RepresentationTheory/Homological/GroupCohomology/LowDegree.lean,Mathlib/RepresentationTheory/Rep.lean,Mathlib/RingTheory/Norm/Basic.lean |
4 |
4 |
['copilot-pull-request-reviewer', 'github-actions'] |
jcommelin assignee:jcommelin |
6-78987 6 days ago |
10-29122 10 days ago |
10-30884 10 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 |
6-78986 6 days ago |
10-36629 10 days ago |
10-36669 10 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 |
6-78985 6 days ago |
10-2681 10 days ago |
10-27215 10 days |
| 33129 |
Paul-Lez author:Paul-Lez |
feat(Tactic/Simproc/VecPerm): Add simproc for permuting entries of a vector |
---
[](https://gitpod.io/from-referrer/)
|
t-meta |
127/0 |
Mathlib.lean,Mathlib/Tactic.lean,Mathlib/Tactic/Simproc/VecPerm.lean,MathlibTest/Simproc/VecPerm.lean |
4 |
7 |
['JovanGerb', 'github-actions'] |
thorimur assignee:thorimur |
6-78984 6 days ago |
10-22067 10 days ago |
10-25097 10 days |
| 33137 |
YaelDillies author:YaelDillies |
chore(Algebra/MonoidAlgebra): don't use hom classes when bundling `mapDomain` |
---
[](https://gitpod.io/from-referrer/)
|
t-algebra label:t-algebra$ |
20/21 |
Mathlib/Algebra/MonoidAlgebra/Basic.lean |
1 |
1 |
['github-actions'] |
jcommelin assignee:jcommelin |
6-78983 6 days ago |
10-5439 10 days ago |
10-5475 10 days |
| 33133 |
0xTerencePrime author:0xTerencePrime |
feat(Algebra/Group/Center): add Decidable (IsMulCentral a) instance |
This PR adds a `Decidable` instance for `IsMulCentral a`.
### Summary
The structure `IsMulCentral` was missing a `Decidable` instance. This PR provides the instance by leveraging `isMulCentral_iff`, enabling decidability for both multiplicative and additive (via `to_additive`) structures.
### Verification
- `lake build Mathlib.Algebra.Group.Center` passed.
- `lake exe runLinter Mathlib.Algebra.Group.Center` passed. |
t-algebra
new-contributor
label:t-algebra$ |
7/0 |
Mathlib/Algebra/Group/Center.lean |
1 |
1 |
['github-actions'] |
ocfnash assignee:ocfnash |
6-78983 6 days ago |
10-15046 10 days ago |
10-15082 10 days |
| 32918 |
michelsol author:michelsol |
feat: define `supEdist` and `supDist` |
Create a new file Topology.MetricSpace.SupDistance and define the supremal distance in (extended) metric spaces. The defined `supEdist` and `supDist` will have similar theory to the already existing `infEdist` and `infDist`. The motivation is to be able to define the radius of a minimal bounding sphere as the infimum of the supDist later.
[zulip discussion here](https://leanprover.zulipchat.com/#narrow/channel/116395-maths/topic/Formalizing.20Jung's.20theorem.20and.20minimal.20bounding.20spheres) |
t-topology
new-contributor
|
75/0 |
Mathlib.lean,Mathlib/Topology/MetricSpace/SupDistance.lean |
2 |
1 |
['github-actions'] |
RemyDegenne assignee:RemyDegenne |
6-55501 6 days ago |
15-15081 15 days ago |
15-15161 15 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 |
6-37426 6 days ago |
6-37438 6 days ago |
6-37472 6 days |
| 33252 |
SnirBroshi author:SnirBroshi |
feat(Combinatorics/SimpleGraph/Clique): cliques & independent sets are chains & antichains |
---
This translation means that [Dilworth's theorem](https://en.wikipedia.org/wiki/Dilworth%27s_theorem) can be used on graphs.
As Wikipedia notes:
> a clique in a comparability graph corresponds to a chain, and an independent set in a comparability graph corresponds to an antichain
("comparability graph" here refers to a graph where `Adj := (⋅ ≤ ⋅)`)
[](https://gitpod.io/from-referrer/)
|
t-combinatorics |
11/0 |
Mathlib/Combinatorics/SimpleGraph/Clique.lean,Mathlib/Combinatorics/SimpleGraph/Coloring.lean |
2 |
1 |
['github-actions'] |
nobody |
6-33671 6 days ago |
6-39613 6 days ago |
6-39651 6 days |
| 33000 |
loefflerd author:loefflerd |
feat(Analysis/Analytic): analytic order of a composition |
Show that:
- The analytic and/or meromorphic order of a function at a point is well-behaved under composition with an analytic function.
- Local inverses of analytic functions are analytic.
---
[](https://gitpod.io/from-referrer/)
|
t-analysis |
259/1 |
Mathlib.lean,Mathlib/Analysis/Analytic/Order.lean,Mathlib/Analysis/Calculus/InverseFunctionTheorem/Analytic.lean,Mathlib/Analysis/Calculus/InverseFunctionTheorem/Deriv.lean,Mathlib/Analysis/Meromorphic/Basic.lean,Mathlib/Analysis/Meromorphic/Order.lean,Mathlib/Data/ENat/Basic.lean |
7 |
8 |
['github-actions', 'j-loreaux', 'loefflerd'] |
urkud assignee:urkud |
6-30333 6 days ago |
6-30333 6 days ago |
12-67112 12 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 |
6-23742 6 days ago |
9-83767 9 days ago |
27-16509 27 days |
| 30640 |
SnirBroshi author:SnirBroshi |
feat(Combinatorics/SimpleGraph/Acyclic): a maximally acyclic graph is a tree |
---
- [x] depends on: #30542
- [x] depends on: #30570
[](https://gitpod.io/from-referrer/)
|
t-combinatorics |
46/0 |
Mathlib/Combinatorics/SimpleGraph/Acyclic.lean,Mathlib/Combinatorics/SimpleGraph/Connectivity/Connected.lean |
2 |
3 |
['github-actions', 'mathlib4-dependent-issues-bot', 'mathlib4-merge-conflict-bot'] |
b-mehta assignee:b-mehta |
6-15443 6 days ago |
17-64850 17 days ago |
21-58229 21 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 |
6-14208 6 days ago |
6-36914 6 days ago |
6-36950 6 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 |
6-8248 6 days ago |
33-76616 1 month ago |
33-76647 33 days |
| 29877 |
Komyyy author:Komyyy |
feat: inner product of the gradient |
Also, this PR enables the `conj` notation in the file.
---
[](https://gitpod.io/from-referrer/)
|
t-analysis |
39/10 |
Mathlib/Analysis/Calculus/Gradient/Basic.lean |
1 |
4 |
['Komyyy', 'github-actions', 'j-loreaux', 'mathlib4-merge-conflict-bot'] |
hrmacbeth assignee:hrmacbeth |
5-82734 5 days ago |
5-82734 5 days ago |
51-81244 51 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 |
5-79000 5 days ago |
9-72134 9 days ago |
9-72179 9 days |
| 33161 |
YuvalFilmus author:YuvalFilmus |
feat(Polynomial/Derivative): iterated derivative of product of linear factors |
Computed the iterated derivative of a product of linear factors.
This will be used to prove the corresponding formula for Lagrange interpolants, which will in turn be used to prove extremal properties of Chebyshev polynomials.
The proof involves a double counting argument which might already appear in Mathlib.
If not, it might be a good idea to put it somewhere under Combinatorics.
Also, there are instances where grind fails without explicitly applying congr — perhaps someone can fix this.
---
[](https://gitpod.io/from-referrer/)
|
t-algebra label:t-algebra$ |
76/0 |
Mathlib/Algebra/Polynomial/Derivative.lean |
1 |
1 |
['github-actions'] |
jcommelin assignee:jcommelin |
5-78998 5 days ago |
9-15647 9 days ago |
9-15691 9 days |
| 33186 |
Ruben-VandeVelde author:Ruben-VandeVelde |
feat: some lemmas about finsum/finprod |
From sphere-eversion.
Co-authored-by: Patrick Massot
Co-authored-by: Floris van Doorn
---
[](https://gitpod.io/from-referrer/)
|
t-algebra label:t-algebra$ |
40/0 |
Mathlib/Algebra/BigOperators/Finprod.lean,Mathlib/Algebra/Notation/Support.lean |
2 |
1 |
['github-actions'] |
ocfnash assignee:ocfnash |
5-78996 5 days ago |
8-81716 8 days ago |
8-81754 8 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 |
5-54368 5 days ago |
5-54392 5 days ago |
31-51022 31 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 |
5-40569 5 days ago |
10-48587 10 days ago |
10-48627 10 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 |
3 |
['euprunin', 'github-actions', 'jcommelin'] |
nobody |
5-3298 5 days ago |
5-3298 5 days ago |
5-71066 5 days |
| 27668 |
IvanRenison author:IvanRenison |
feat(Analysis/InnerProductSpace): define outer product of linear maps |
Co-authored-by: themathqueen <23701951+themathqueen@users.noreply.github.com>
Co-authored-by: Jam Kabeer Ali Khan
---
I'm not completely sure if this is a good addition or not, and also, I was not sure if to call the definition `outerProduct` or only `outer`.
- [ ] depends on: #28350
- [ ] depends on: #28344
[](https://gitpod.io/from-referrer/)
|
t-analysis |
156/0 |
Mathlib/Analysis/InnerProductSpace/Adjoint.lean,Mathlib/Analysis/InnerProductSpace/Dual.lean,Mathlib/Analysis/InnerProductSpace/LinearMap.lean,Mathlib/Analysis/InnerProductSpace/PiL2.lean,Mathlib/Analysis/InnerProductSpace/Positive.lean,Mathlib/Analysis/InnerProductSpace/Trace.lean |
6 |
73 |
['IvanRenison', 'github-actions', 'j-loreaux', 'mathlib4-dependent-issues-bot', 'mathlib4-merge-conflict-bot', 'themathqueen'] |
themathqueen assignee:themathqueen |
4-83790 4 days ago |
5-19306 5 days ago |
7-77241 7 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$ |
26/18 |
Mathlib/LinearAlgebra/Lagrange.lean |
1 |
4 |
['Ruben-VandeVelde', 'YuvalFilmus', 'github-actions'] |
dagurtomas assignee:dagurtomas |
4-78993 4 days ago |
8-40332 8 days ago |
8-40380 8 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 |
4-78989 4 days ago |
7-82575 7 days ago |
7-82552 7 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 |
4-69774 4 days ago |
5-2178 5 days ago |
5-2225 5 days |
| 33074 |
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):
* `ApplicativeTransformation.ext`: <10 ms before, <10 ms after 🎉
* `Fin.castSucc_ne_zero_of_lt`: <10 ms before, 43 ms after
* `Finset.le_sup_dite_pos`: <10 ms before, 25 ms after
* `Finset.le_sup_dite_neg`: <10 ms before, 33 ms after
* `Finset.noncommProd_lemma`: <10 ms before, <10 ms after 🎉
* `Real.sqrt_two_lt_three_halves`: 67 ms before, 69 ms after
This golfing PR is batched under the following guidelines:
* Up to ~5 changed files per PR
* Up to ~25 changed declarations per PR
* Up to ~100 changed lines per PR
---
[](https://gitpod.io/from-referrer/)
|
t-data |
7/19 |
Mathlib/Control/Traversable/Basic.lean,Mathlib/Data/Fin/SuccPred.lean,Mathlib/Data/Finset/Lattice/Fold.lean,Mathlib/Data/Finset/NoncommProd.lean,Mathlib/Data/Real/Sqrt.lean |
5 |
5 |
['JovanGerb', 'euprunin', 'github-actions', 'jcommelin'] |
nobody |
4-64472 4 days ago |
10-51976 10 days ago |
10-74192 10 days |
| 32896 |
ScottCarnahan author:ScottCarnahan |
feat(Algebra/Lie/Extension): Lie Algebra isomorphism from 2-coboundary, 1-cochain from two splittings |
This PR adds two basic constructions relating Lie algebra extensions to cohomology.
---
[](https://gitpod.io/from-referrer/)
|
t-algebra label:t-algebra$ |
79/8 |
Mathlib/Algebra/Lie/Extension.lean |
1 |
8 |
['ScottCarnahan', 'github-actions', 'ocfnash'] |
ocfnash assignee:ocfnash |
4-60610 4 days ago |
4-60610 4 days ago |
6-74637 6 days |
| 33115 |
JohnnyTeutonic author:JohnnyTeutonic |
feat(Data/Matrix/Cartan): determinants and simply-laced properties |
This PR adds:
- Determinants for G₂ and F₄ Cartan matrices
- `IsSimplyLaced` predicate (symmetric Cartan matrices)
- Simply-laced theorems for E₆, E₇, E₈, A, D families
- Determinant positivity lemmas
Note: E₆/E₇/E₈ determinants are deferred due to `decide` recursion limits.
---
[](https://gitpod.io/from-referrer/)
|
new-contributor
t-data
large-import
|
33/0 |
Mathlib/Data/Matrix/Cartan.lean |
1 |
2 |
['JohnnyTeutonic', 'github-actions'] |
ocfnash assignee:ocfnash |
4-28855 4 days ago |
10-74554 10 days ago |
10-74592 10 days |
| 32671 |
themathqueen author:themathqueen |
chore(LinearAlgebra/GeneralLinearGroup/AlgEquiv): slightly generalize |
Also show `trace (f x) = trace x` and `det (f x) = det x` for algebra equivalence `f`.
---
[](https://gitpod.io/from-referrer/)
|
t-algebra label:t-algebra$ |
64/17 |
Mathlib/LinearAlgebra/Determinant.lean,Mathlib/LinearAlgebra/GeneralLinearGroup/AlgEquiv.lean,Mathlib/LinearAlgebra/Trace.lean |
3 |
5 |
['erdOne', 'github-actions', 'themathqueen'] |
Vierkantor assignee:Vierkantor |
4-25937 4 days ago |
17-34830 17 days ago |
20-63009 20 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 |
303/28 |
Mathlib/AlgebraicTopology/Quasicategory/StrictBicategory.lean,Mathlib/AlgebraicTopology/SimplicialSet/HoFunctorMonoidal.lean,Mathlib/AlgebraicTopology/SimplicialSet/NerveAdjunction.lean |
3 |
7 |
['github-actions', 'mathlib4-dependent-issues-bot', 'mathlib4-merge-conflict-bot'] |
robin-carlier assignee:robin-carlier |
3-79003 3 days ago |
4-10465 4 days ago |
4-12788 4 days |
| 32745 |
LTolDe author:LTolDe |
feat(Topology/Algebra): add MulActionConst.lean |
add Topology/Algebra/MulActionConst.lean
introduce class `ContinuousSMulConst` for a scalar multiplication that is continuous in the first argument, in analogy to `ContinuousConstSMul`
define `MulAction.ball x U` as the set `U • {x}` given `[SMul G X] (x : X) (U : Set G)`
The lemmas shown here will be useful to prove the **Effros Theorem**, see [zulip](https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/Effros.20Theorem/with/558712441).
---
[](https://gitpod.io/from-referrer/)
|
t-topology
new-contributor
|
98/0 |
Mathlib.lean,Mathlib/Topology/Algebra/MulActionConst.lean |
2 |
1 |
['github-actions'] |
dagurtomas assignee:dagurtomas |
3-79002 3 days ago |
19-22326 19 days ago |
19-22377 19 days |
| 32927 |
gasparattila author:gasparattila |
feat(Analysis/InnerProductSpace): orthogonal decomposition as a `LinearIsometryEquiv` |
---
[](https://gitpod.io/from-referrer/)
|
t-analysis |
84/6 |
Mathlib/Analysis/InnerProductSpace/ProdL2.lean,Mathlib/Analysis/InnerProductSpace/Projection/Submodule.lean,Mathlib/LinearAlgebra/Projection.lean |
3 |
20 |
['gasparattila', 'github-actions', 'j-loreaux', 'themathqueen'] |
urkud assignee:urkud |
3-78999 3 days ago |
7-7429 7 days ago |
7-62297 7 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 |
3-78998 3 days ago |
14-21330 14 days ago |
14-21367 14 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 |
3-78995 3 days ago |
7-22245 7 days ago |
7-22285 7 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 |
3-78994 3 days ago |
6-80389 6 days ago |
6-80426 6 days |
| 33320 |
vihdzp author:vihdzp |
chore(Algebra/Order/SuccPred): add `simp` tags |
Note that in particular, this makes `n < m + 1 ↔ n ≤ m` and `n + 1 ≤ m ↔ n < m` into the simp-normal forms for `ℕ` and `ℤ`, which is a somewhat drastic change but seems to have positive effects.
---
If we do want to do this, then we should eventually add the `simp` attributes to core.
[](https://gitpod.io/from-referrer/)
|
t-algebra
t-order
label:t-algebra$ |
47/46 |
Mathlib/Algebra/Order/Floor/Ring.lean,Mathlib/Algebra/Order/Round.lean,Mathlib/Algebra/Order/SuccPred.lean,Mathlib/Algebra/Polynomial/Derivative.lean,Mathlib/Algebra/Polynomial/Div.lean,Mathlib/Algebra/Polynomial/Homogenize.lean,Mathlib/Algebra/Polynomial/SumIteratedDerivative.lean,Mathlib/Analysis/BoxIntegral/UnitPartition.lean,Mathlib/Analysis/Distribution/TemperateGrowth.lean,Mathlib/Analysis/Normed/Unbundled/SmoothingSeminorm.lean,Mathlib/Combinatorics/SetFamily/LYM.lean,Mathlib/MeasureTheory/Measure/Portmanteau.lean,Mathlib/MeasureTheory/Order/Lattice.lean,Mathlib/MeasureTheory/VectorMeasure/Decomposition/Hahn.lean,Mathlib/NumberTheory/Chebyshev.lean,Mathlib/NumberTheory/Divisors.lean,Mathlib/NumberTheory/LegendreSymbol/GaussEisensteinLemmas.lean,Mathlib/NumberTheory/MahlerMeasure.lean,Mathlib/NumberTheory/PrimeCounting.lean,Mathlib/NumberTheory/SmoothNumbers.lean,Mathlib/Order/KrullDimension.lean,Mathlib/RingTheory/Discriminant.lean,Mathlib/RingTheory/IntegralClosure/Algebra/Ideal.lean,Mathlib/RingTheory/Polynomial/Resultant/Basic.lean,Mathlib/RingTheory/Polynomial/ShiftedLegendre.lean,Mathlib/RingTheory/PowerSeries/Trunc.lean |
26 |
2 |
['JovanGerb', 'github-actions'] |
nobody |
1-25822 1 day ago |
3-63933 3 days ago |
3-63919 3 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 |
3-60084 3 days ago |
4-30232 4 days ago |
4-85070 4 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'] |
nobody |
3-50579 3 days ago |
3-50579 3 days ago |
10-17051 10 days |
| 32438 |
JovanGerb author:JovanGerb |
feat: unfold-boundaries in `to_dual` |
This PR introduces a new feature to `to_dual` that allows us to have definitions whose dual is not definitionally equal to the dual of the value. This is crucial for many definitions that are dual to something morally but not definitionally. For example, `DecidableLE`, `Set.Ioo`, `Set.Ico`, `CovBy` , `Monotone`.
- [x] Tracing to see what this is doing
- [x] Improve the UI of applying the `to_dual_insert_cast` and `to_dual_insert_cast_fun` attributes.
- [x] Add tests
- [x] Better documentation
---
[](https://gitpod.io/from-referrer/)
|
t-meta |
517/127 |
Mathlib.lean,Mathlib/Combinatorics/Quiver/Basic.lean,Mathlib/Order/Basic.lean,Mathlib/Order/Cover.lean,Mathlib/Order/Defs/LinearOrder.lean,Mathlib/Order/Defs/PartialOrder.lean,Mathlib/Order/GaloisConnection/Defs.lean,Mathlib/Order/Interval/Set/Defs.lean,Mathlib/Order/Monotone/Defs.lean,Mathlib/Order/WithBot.lean,Mathlib/Tactic.lean,Mathlib/Tactic/ToDual.lean,Mathlib/Tactic/Translate/Core.lean,Mathlib/Tactic/Translate/ToDual.lean,Mathlib/Tactic/Translate/UnfoldBoundary.lean,MathlibTest/ToDual.lean |
16 |
10 |
['JovanGerb', 'fpvandoorn', 'github-actions', 'leanprover-radar', 'mathlib4-merge-conflict-bot', 'vihdzp'] |
bryangingechen assignee:bryangingechen |
3-39462 3 days ago |
5-49024 5 days ago |
9-62405 9 days |
| 32674 |
CoolRmal author:CoolRmal |
feat: a dense Gdelta subset of a Baire space is Baire. |
This PR formalizes:
1. If `s` is dense in `X` and `u` is open and dense in `s`, then `u = v ∩ s` for some `v` that is open and dense in `X`. We then use this lemma to prove that a dense Gδ subset of a Baire space is Baire.
2. A Gδ subset of a locally compact R1 space is Baire.
Formalized with help from Aristotle.
---
- [ ] depends on: #32673
[](https://gitpod.io/from-referrer/)
|
t-topology |
57/2 |
Mathlib/Topology/Baire/Lemmas.lean,Mathlib/Topology/Baire/LocallyCompactRegular.lean,Mathlib/Topology/Constructions.lean,Mathlib/Topology/GDelta/Basic.lean |
4 |
4 |
['CoolRmal', 'github-actions', 'mathlib4-dependent-issues-bot', 'mathlib4-merge-conflict-bot'] |
nobody |
3-24744 3 days ago |
3-27327 3 days ago |
3-40102 3 days |
| 33325 |
SnirBroshi author:SnirBroshi |
chore(Order/Defs/Unbundled): deprecate `IsSymm` in favor of core's `Std.Symm` |
---
[Mathlib's `IsSymm`](https://leanprover-community.github.io/mathlib4_docs/Mathlib/Order/Defs/Unbundled.html#IsSymm)
[Core's `Std.Symm`](https://leanprover-community.github.io/mathlib4_docs/Init/Core.html#Std.Symm)
[Zulip](https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/Relation.20properties.20duplication/near/544638270)
[](https://gitpod.io/from-referrer/)
|
t-order |
42/42 |
Mathlib/Algebra/GroupWithZero/Associated.lean,Mathlib/Analysis/InnerProductSpace/Basic.lean,Mathlib/Analysis/Normed/Module/FiniteDimension.lean,Mathlib/Data/Finset/Pairwise.lean,Mathlib/Data/Fintype/Basic.lean,Mathlib/Data/List/Perm/Basic.lean,Mathlib/Data/Multiset/Count.lean,Mathlib/Data/Rel.lean,Mathlib/Data/Set/Pairwise/Basic.lean,Mathlib/Data/Set/Pairwise/List.lean,Mathlib/Data/Sigma/Lex.lean,Mathlib/GroupTheory/Perm/Support.lean,Mathlib/Logic/Pairwise.lean,Mathlib/ModelTheory/Equivalence.lean,Mathlib/Order/Antichain.lean,Mathlib/Order/Antisymmetrization.lean,Mathlib/Order/Basic.lean,Mathlib/Order/Comparable.lean,Mathlib/Order/Defs/Unbundled.lean,Mathlib/Order/RelClasses.lean,Mathlib/Order/RelIso/Basic.lean,Mathlib/Order/RelIso/Set.lean,Mathlib/Order/WellFoundedSet.lean,Mathlib/SetTheory/PGame/Basic.lean,Mathlib/SetTheory/PGame/Order.lean,Mathlib/Topology/NatEmbedding.lean |
26 |
12 |
['SnirBroshi', 'github-actions', 'jcommelin', 'vihdzp', 'vlad902'] |
nobody |
3-22411 3 days ago |
3-45827 3 days ago |
3-81960 3 days |
| 33040 |
vihdzp author:vihdzp |
refactor: rename `≤ᵥ` to `vle` and `<ᵥ` to `vlt` |
This makes room to later add `=ᵥ` or `veq` defined as `AntisymmRel (· ≤ᵥ ·)`.
---
I've left the names `vle` and `vlt` uncapitalized, which goes against the naming conventions but matches `le` and `lt`.
[](https://gitpod.io/from-referrer/)
|
RFC
maintainer-merge
t-ring-theory
|
314/198 |
Mathlib/RingTheory/Valuation/ValuativeRel/Basic.lean,Mathlib/RingTheory/Valuation/ValuativeRel/Trivial.lean |
2 |
11 |
['erdOne', 'github-actions', 'mathlib4-merge-conflict-bot', 'plp127', 'vihdzp'] |
nobody |
3-17720 3 days ago |
3-17720 3 days ago |
11-24516 11 days |
| 32740 |
LTolDe author:LTolDe |
feat: add IsNowhereDense helpers |
add new lemmas to prove `IsNowhereDense s`
- IsNowhereDense.mono
- Topology.IsInducing.isNowhereDense_image
- IsNowhereDense.image_val
these lemmas will help to prove the **Effros Theorem**, see [zulip thread](https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/Effros.20Theorem/with/558712441)
---
[](https://gitpod.io/from-referrer/)
|
new-contributor
large-import
|
24/1 |
Mathlib/Topology/GDelta/Basic.lean |
1 |
5 |
['LTolDe', 'dupuisf', 'github-actions'] |
dupuisf assignee:dupuisf |
3-16214 3 days ago |
19-25597 19 days ago |
19-25629 19 days |
| 32643 |
vihdzp author:vihdzp |
feat: cardinality of Hahn series inverse |
---
- [x] depends on: #32640
- [x] depends on: #32645
[](https://gitpod.io/from-referrer/)
|
maintainer-merge
large-import
t-ring-theory
|
90/17 |
Mathlib/RingTheory/HahnSeries/Addition.lean,Mathlib/RingTheory/HahnSeries/Basic.lean,Mathlib/RingTheory/HahnSeries/Cardinal.lean,Mathlib/RingTheory/HahnSeries/Multiplication.lean,Mathlib/RingTheory/LaurentSeries.lean |
5 |
13 |
['YaelDillies', 'erdOne', 'github-actions', 'mathlib4-dependent-issues-bot', 'mathlib4-merge-conflict-bot', 'vihdzp', 'wwylele'] |
mariainesdff assignee:mariainesdff |
3-13343 3 days ago |
3-13343 3 days ago |
8-10953 8 days |
| 33091 |
WenrongZou author:WenrongZou |
feat(RingTheory/MvPowerSeries): (mv) PowerSeries version of `expand_char` |
I proved the `expand_char` for (mv) power series. And also unify the `expand` for (mv) polynomial and (mv) power series.
---
[](https://gitpod.io/from-referrer/)
|
large-import
t-ring-theory
|
190/18 |
Mathlib/Algebra/Polynomial/Expand.lean,Mathlib/FieldTheory/Finite/Basic.lean,Mathlib/FieldTheory/Perfect.lean,Mathlib/RingTheory/MvPolynomial/Expand.lean,Mathlib/RingTheory/MvPowerSeries/Basic.lean,Mathlib/RingTheory/MvPowerSeries/Expand.lean,Mathlib/RingTheory/MvPowerSeries/Trunc.lean,Mathlib/RingTheory/PowerSeries/Expand.lean |
8 |
39 |
['WenrongZou', 'erdOne', 'github-actions', 'jcommelin'] |
mariainesdff assignee:mariainesdff |
3-6987 3 days ago |
3-6987 3 days ago |
10-65674 10 days |
| 33300 |
CoolRmal author:CoolRmal |
feat: a finite space is Baire. |
---
[](https://gitpod.io/from-referrer/)
|
t-topology |
24/1 |
Mathlib/Topology/Baire/Lemmas.lean |
1 |
2 |
['github-actions', 'mathlib4-merge-conflict-bot'] |
nobody |
2-83634 2 days ago |
2-83642 2 days ago |
4-18033 4 days |
| 33337 |
themathqueen author:themathqueen |
chore(Analysis/InnerProductSpace/Projection/Submodule): rename lemmas |
---
[](https://gitpod.io/from-referrer/)
|
easy
t-analysis
|
16/9 |
Mathlib/Analysis/InnerProductSpace/Positive.lean,Mathlib/Analysis/InnerProductSpace/Projection/Submodule.lean |
2 |
1 |
['github-actions'] |
nobody |
2-82192 2 days ago |
2-82192 2 days ago |
3-46465 3 days |
| 32742 |
LTolDe author:LTolDe |
feat(MeasureTheory/Constructions/Polish/Basic): add class SuslinSpace |
add new class `SuslinSpace` for a topological space that is an analytic set in itself
This will be useful to prove the **Effros Theorem**, see [zulip thread](https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/Effros.20Theorem/with/558712441).
---
[](https://gitpod.io/from-referrer/)
|
new-contributor |
4/0 |
Mathlib/MeasureTheory/Constructions/Polish/Basic.lean |
1 |
5 |
['ADedecker', 'LTolDe', 'dupuisf', 'github-actions'] |
PatrickMassot assignee:PatrickMassot |
2-78966 2 days ago |
19-24459 19 days ago |
19-24443 19 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 |
2-78964 2 days ago |
13-80110 13 days ago |
13-80084 13 days |
| 33259 |
YuvalFilmus author:YuvalFilmus |
feat(Trigonometric/Chebyshev/RootsExtremal): Chebyshev polynomials are extremal in terms of leading coefficient |
We prove that among all degree n polynomials P such that |P(x)|≤1 for all |x|≤1, the n'th Chebyshev polynomial uniquely maximized the leading coefficient.
A subsequent PR will prove a similar property for iterated derivatives evaluated at points x≥1.
---
[](https://gitpod.io/from-referrer/)
|
t-analysis |
193/0 |
Mathlib.lean,Mathlib/Analysis/SpecialFunctions/Trigonometric/Chebyshev/Extremal.lean |
2 |
1 |
['github-actions'] |
sgouezel assignee:sgouezel |
2-78961 2 days ago |
6-19477 6 days ago |
6-19516 6 days |
| 32851 |
tdwag123 author:tdwag123 |
feat(MeasureTheory/Measure/TypeClass/NoAtoms) add `exists_accPt_of_noAtoms` |
feat(MeasureTheory/Measure/TypeClass/NoAtoms): Added a theorem that states If a set has positive measure under an atomless measure, then it has an accumulation point.
Added a lemma in (Topology/DiscreteSubset): If a subset of a topological space has no accumulation points,
then it carries the discrete topology.
Theorem added: `exists_accPt_of_pos_hausdorffMeasure`
Lemma added: `discreteTopology_of_noAccPts `
**Harmonic's Aristotle gave the initial version of the proofs.**
`---`
[](https://gitpod.io/from-referrer/)
|
t-measure-probability
new-contributor
|
28/0 |
Mathlib/MeasureTheory/Measure/Typeclasses/NoAtoms.lean,Mathlib/Topology/DiscreteSubset.lean |
2 |
23 |
['CoolRmal', 'Vilin97', 'github-actions', 'plp127', 'sgouezel', 'tdwag123'] |
urkud assignee:urkud |
2-75253 2 days ago |
17-8466 17 days ago |
17-9769 17 days |
| 33352 |
themathqueen author:themathqueen |
feat(Analysis/InnerProductSpace/Positive): `f.symm.IsPositive` iff `f.IsPositive` |
... for linear equivalence `f`.
---
[](https://gitpod.io/from-referrer/)
|
easy
t-analysis
|
15/0 |
Mathlib/Analysis/InnerProductSpace/Positive.lean,Mathlib/Analysis/InnerProductSpace/Symmetric.lean |
2 |
3 |
['github-actions', 'themathqueen'] |
nobody |
2-65781 2 days ago |
2-66424 2 days ago |
2-67423 2 days |
| 33341 |
themathqueen author:themathqueen |
chore(Topology/Algebra/Module/LinearMap): deprecate duplicate lemmas |
Now that `range` and `ker` take in a `LinearMap` instead of a `LinearMapClass`, these lemmas are the same thing as the linear map versions.
---
[](https://gitpod.io/from-referrer/)
|
t-topology |
15/23 |
Mathlib/Analysis/InnerProductSpace/Positive.lean,Mathlib/Analysis/InnerProductSpace/Projection/Basic.lean,Mathlib/Analysis/InnerProductSpace/Symmetric.lean,Mathlib/LinearAlgebra/Projection.lean,Mathlib/Topology/Algebra/Module/LinearMap.lean |
5 |
2 |
['github-actions', 'themathqueen'] |
nobody |
2-65626 2 days ago |
3-30470 3 days ago |
3-30513 3 days |
| 33351 |
themathqueen author:themathqueen |
chore(Analysis/LocallyConvex/SeparatingDual): generalize `Algebra.IsCentral.instContinuousLinearMap` |
... to two different scalar fields.
---
[](https://gitpod.io/from-referrer/)
|
t-analysis |
35/22 |
Mathlib/Analysis/LocallyConvex/SeparatingDual.lean,Mathlib/Topology/Algebra/Module/LinearMap.lean |
2 |
5 |
['github-actions', 'leanprover-radar', 'themathqueen'] |
nobody |
2-62030 2 days ago |
2-70244 2 days ago |
2-72801 2 days |
| 33283 |
YuvalFilmus author:YuvalFilmus |
feat(Polynomial/Chebyshev): Differential equations for T and U |
Added the defining differential equations for T and U.
---
[](https://gitpod.io/from-referrer/)
|
maintainer-merge
t-ring-theory
|
33/0 |
Mathlib/RingTheory/Polynomial/Chebyshev.lean |
1 |
5 |
['YuvalFilmus', 'erdOne', 'github-actions'] |
nobody |
2-58563 2 days ago |
3-13015 3 days ago |
5-15889 5 days |
| 33311 |
YuvalFilmus author:YuvalFilmus |
feat(Polynomial/Chebyshev): calculate values of T and U at zero |
Added theorems stating the value of T and U at 0.
The proofs are quite clunky — would appreciate any simplifications.
---
[](https://gitpod.io/from-referrer/)
|
t-ring-theory |
56/0 |
Mathlib/Algebra/Ring/Parity.lean,Mathlib/RingTheory/Polynomial/Chebyshev.lean |
2 |
2 |
['erdOne', 'github-actions'] |
nobody |
2-56405 2 days ago |
2-56409 2 days ago |
3-73048 3 days |
| 30881 |
FlAmmmmING author:FlAmmmmING |
feat(RingTheory/PowerSeries/Schroder.lean): Define the generating function for large Schroder number |
Define the generating function for large Schroder number.
Main result : Prove some lemmas and the generating function of large Schroder.
Todo : Prove the generating function of small Schroder.
---
- [ ] depends on: #30609
---
[](https://gitpod.io/from-referrer/)
|
new-contributor |
120/0 |
Mathlib.lean,Mathlib/RingTheory/PowerSeries/Schroder.lean |
2 |
14 |
['FlAmmmmING', 'github-actions', 'mathlib4-dependent-issues-bot', 'mathlib4-merge-conflict-bot', 'wwylele'] |
dwrensha assignee:dwrensha |
2-55274 2 days ago |
5-47197 5 days ago |
37-40417 37 days |
| 33237 |
JovanGerb author:JovanGerb |
feat(CategoryTheory/Functor): use `@[to_dual]` |
This PR tags `Functor`/`Prefunctor` with `to_dual`. `to_dual` doesn't flip the direction of a functor, only the directions of the morphisms in the categories. So, we don't actually need to tag `Functor`, but we do need to tag `Functor.map` to reorder its arguments `X` and `Y`.
There is some friction between `to_dual` and the asymmetric design of the category theory library, namely the fact that there is a preferred way of associating a chain of compositions. This is reflected in the `to_assoc` attribute which generates a lemma with postfix `_assoc`. `to_dual` will need to also generate all the dual versions of the `_assoc` lemmas that are associated the other way around. I would like to ask how these lemmas should be called (I went for `_assoc'` for now in this PR.
---
[](https://gitpod.io/from-referrer/)
|
t-category-theory |
12/10 |
Mathlib/CategoryTheory/Functor/Basic.lean,Mathlib/Combinatorics/Quiver/Prefunctor.lean |
2 |
5 |
['JovanGerb', 'github-actions', 'mathlib4-merge-conflict-bot', 'vihdzp'] |
nobody |
2-47840 2 days ago |
3-45537 3 days ago |
6-81299 6 days |
| 33333 |
SnirBroshi author:SnirBroshi |
feat(Analysis/Real/Pi/Bounds): `round π = 3` |
---
The same should hold for `e` (`Real.exp 1`) ~~but we don't seem to have bounds for it.~~
[](https://gitpod.io/from-referrer/)
|
t-analysis
maintainer-merge
|
17/0 |
Mathlib/Analysis/Real/Pi/Bounds.lean |
1 |
11 |
['SnirBroshi', 'euprunin', 'github-actions', 'grunweg', 'jcommelin', 'jsm28'] |
nobody |
2-43597 2 days ago |
3-48681 3 days ago |
3-50773 3 days |
| 32803 |
erdOne author:erdOne |
feat(RIngTheory): more-linear version of `tensorKaehlerEquiv` |
---
[](https://gitpod.io/from-referrer/)
|
t-ring-theory |
81/7 |
Mathlib/RingTheory/Kaehler/TensorProduct.lean |
1 |
9 |
['erdOne', 'github-actions', 'mattrobball', 'robin-carlier'] |
mattrobball assignee:mattrobball |
2-33727 2 days ago |
2-33727 2 days ago |
9-27452 9 days |
| 32837 |
erdOne author:erdOne |
feat(RingTheory): noetherian model for etale algebras |
---
[](https://gitpod.io/from-referrer/)
|
large-import
t-ring-theory
|
185/12 |
Mathlib/RingTheory/Extension/Presentation/Core.lean,Mathlib/RingTheory/Smooth/NoetherianDescent.lean |
2 |
7 |
['chrisflav', 'erdOne', 'github-actions'] |
chrisflav assignee:chrisflav |
2-31706 2 days ago |
2-31706 2 days ago |
7-69072 7 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$ |
87/6 |
Mathlib/Algebra/Module/SpanRank.lean |
1 |
2 |
['github-actions'] |
nobody |
2-20061 2 days ago |
2-25915 2 days ago |
2-25954 2 days |
| 33361 |
sun123zxy author:sun123zxy |
feat(RingTheory/Nakayama): refine Nakayama's lemma 00DV (8) |
---
Split from PR #33247
[](https://gitpod.io/from-referrer/)
|
new-contributor
t-ring-theory
|
46/5 |
Mathlib/RingTheory/Nakayama.lean |
1 |
1 |
['github-actions'] |
nobody |
2-19963 2 days ago |
2-19968 2 days ago |
2-20004 2 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 |
2-18685 2 days ago |
2-18710 2 days ago |
7-37672 7 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 |
1-85807 1 day ago |
1-85834 1 day ago |
1-85873 1 day |
| 33332 |
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):
* `SimpleGraph.adj_of_mem_walk_support`: 33 ms before, 46 ms after
* `Finset.mem_of_max`: 13 ms before, 88 ms after
* `Set.eq_of_notMem_uIoc_of_notMem_uIoc`: 59 ms before, 44 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/)
|
|
8/39 |
Mathlib/Combinatorics/SimpleGraph/Connectivity/Connected.lean,Mathlib/Combinatorics/SimpleGraph/Walks/Basic.lean,Mathlib/Data/Finset/Max.lean,Mathlib/Order/Interval/Set/UnorderedInterval.lean |
4 |
6 |
['SnirBroshi', 'euprunin', 'github-actions', 'vihdzp'] |
nobody |
1-85533 1 day ago |
3-50839 3 days ago |
3-50813 3 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 |
1-81590 1 day ago |
1-82003 1 day ago |
60-39108 60 days |
| 32816 |
joelriou author:joelriou |
feat(CategoryTheory): computing Ext-groups using a projective resolution |
This PR dualises #32105.
---
- [x] depends on: #32105
- [x] depends on: #32814
[](https://gitpod.io/from-referrer/)
|
t-category-theory |
204/0 |
Mathlib.lean,Mathlib/CategoryTheory/Abelian/Projective/Ext.lean |
2 |
3 |
['github-actions', 'mathlib4-dependent-issues-bot', 'mathlib4-merge-conflict-bot'] |
robin-carlier assignee:robin-carlier |
1-78983 1 day ago |
2-12868 2 days ago |
2-12843 2 days |
| 32992 |
mcdoll author:mcdoll |
feat(Analysis/Fourier): Fourier transform of the convolution |
We calculate the Fourier transform of the convolution of two functions as the multiplication of
the Fourier transforms of the individual factors.
---
[](https://gitpod.io/from-referrer/)
|
t-analysis |
148/0 |
Mathlib.lean,Mathlib/Analysis/Fourier/Convolution.lean |
2 |
1 |
['github-actions'] |
urkud assignee:urkud |
1-78982 1 day ago |
5-53309 5 days ago |
5-69971 5 days |
| 33244 |
SnirBroshi author:SnirBroshi |
feat(Analysis/Complex/Trigonometric): `tan⁻¹ = cot` |
---
[Zulip](https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/Reciprocal.20trigonometric.20functions/near/564890210)
I think that `funext` versions `tan⁻¹ = cot` without applying to `x` might also be useful, but they don't seem prevalent in the file so I added just the applied versions.
[](https://gitpod.io/from-referrer/)
|
t-analysis |
16/0 |
Mathlib/Analysis/Complex/Trigonometric.lean |
1 |
1 |
['github-actions'] |
sgouezel assignee:sgouezel |
1-78981 1 day ago |
6-84514 6 days ago |
6-84549 6 days |
| 33271 |
jano-wol author:jano-wol |
feat: prove invtSubmoduleToLieIdeal_top |
---
[](https://gitpod.io/from-referrer/)
|
t-algebra label:t-algebra$ |
70/3 |
Mathlib/Algebra/Lie/Weights/Cartan.lean,Mathlib/Algebra/Lie/Weights/IsSimple.lean,Mathlib/Algebra/Lie/Weights/Killing.lean |
3 |
1 |
['github-actions'] |
chrisflav assignee:chrisflav |
1-78980 1 day ago |
5-60205 5 days ago |
5-60241 5 days |
| 33278 |
harahu author:harahu |
doc(MeasureTheory): fix file refs |
Fix some stale documentation file refs.
---
[](https://gitpod.io/from-referrer/)
|
t-measure-probability |
7/6 |
Mathlib/MeasureTheory/Function/L2Space.lean,Mathlib/MeasureTheory/Function/UnifTight.lean,Mathlib/MeasureTheory/Integral/Bochner/L1.lean,Mathlib/MeasureTheory/Integral/IntervalIntegral/FundThmCalculus.lean,Mathlib/MeasureTheory/Measure/Lebesgue/Integral.lean |
5 |
2 |
['bryangingechen', 'github-actions'] |
kex-y assignee:kex-y |
1-78978 1 day ago |
5-40993 5 days ago |
5-41027 5 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 |
1-78977 1 day ago |
5-19202 5 days ago |
5-19239 5 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/36 |
Mathlib/Combinatorics/SetFamily/Compression/Down.lean,Mathlib/Computability/AkraBazzi/GrowsPolynomially.lean,Mathlib/GroupTheory/Perm/Support.lean,Mathlib/Logic/Equiv/Basic.lean,Mathlib/Topology/Instances/CantorSet.lean |
5 |
3 |
['github-actions', 'vihdzp'] |
thorimur assignee:thorimur |
1-78976 1 day ago |
5-11398 5 days ago |
5-11372 5 days |
| 33290 |
euprunin author:euprunin |
chore: golf using `grind` and `simp` |
---
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):
* `MulActionHom.comp_inverse'`: <10 ms before, <10 ms after 🎉
* `MulActionHom.inverse'_comp`: <10 ms before, <10 ms after 🎉
* `DihedralGroup.reciprocalFactors_odd`: <10 ms before, 98 ms after
* `Monoid.CoprodI.NeWord.toList_head?`: <10 ms before, 45 ms after
* `rootsOfUnity_inf_rootsOfUnity`: 33 ms before, 19 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/)
|
|
8/22 |
Mathlib/GroupTheory/CommutingProbability.lean,Mathlib/GroupTheory/CoprodI.lean,Mathlib/GroupTheory/GroupAction/Hom.lean,Mathlib/RingTheory/RootsOfUnity/Basic.lean |
4 |
3 |
['github-actions', 'themathqueen'] |
mariainesdff assignee:mariainesdff |
1-78974 1 day ago |
5-6572 5 days ago |
5-6546 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
|
136/0 |
Mathlib.lean,Mathlib/Combinatorics/SimpleGraph/Connectivity/VertexConnectivity.lean |
2 |
1 |
['github-actions'] |
nobody |
1-68980 1 day ago |
2-38420 2 days ago |
2-38453 2 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 |
1-67895 1 day ago |
10-85836 10 days ago |
76-51165 76 days |
| 32911 |
erdOne author:erdOne |
feat(Analysis): ℘ is analytic |
---
[](https://gitpod.io/from-referrer/)
|
t-analysis |
329/4 |
Mathlib/Analysis/Analytic/Binomial.lean,Mathlib/Analysis/SpecialFunctions/Elliptic/Weierstrass.lean,Mathlib/Order/UpperLower/Closure.lean,Mathlib/Topology/Order/IsLUB.lean |
4 |
15 |
['erdOne', 'github-actions', 'loefflerd'] |
loefflerd assignee:loefflerd |
1-55694 1 day ago |
1-84308 1 day ago |
5-58709 5 days |
| 33324 |
fbarroero author:fbarroero |
feat(RingTheory/DedekindDomain/AdicValuation): introduce `intAdicAbv` |
We introduce
```
def intAdicAbvDef (r : R) : ℝ≥0 := toNNReal (ne_zero_of_lt hb) (v.intValuation r)
```
and the corresponding `AbsoluteValue R ℝ`.
---
[](https://gitpod.io/from-referrer/)
|
t-ring-theory |
66/30 |
Mathlib/RingTheory/DedekindDomain/AdicValuation.lean |
1 |
8 |
['copilot-pull-request-reviewer', 'erdOne', 'fbarroero', 'github-actions'] |
nobody |
1-45561 1 day ago |
1-45561 1 day ago |
2-38674 2 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 |
1-44854 1 day ago |
15-43989 15 days ago |
35-43815 35 days |
| 32000 |
Thmoas-Guan author:Thmoas-Guan |
feat(Algebra): projective dimension equal supremum of localized module |
In this PR, we proved that for finitely generated module over Noetherian ring, projective dimension is equal to the supremum of projective dimension of localized modules over all prime/maximal ideals.
---
- [x] depends on: #31998
[](https://gitpod.io/from-referrer/)
|
|
243/0 |
Mathlib.lean,Mathlib/RingTheory/LocalProperties/ProjectiveDimension.lean |
2 |
3 |
['github-actions', 'mathlib4-dependent-issues-bot', 'mathlib4-merge-conflict-bot'] |
kex-y assignee:kex-y |
1-43694 1 day ago |
6-24627 6 days ago |
6-80715 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 |
1-41295 1 day ago |
3-38320 3 days ago |
3-38361 3 days |
| 28582 |
Thmoas-Guan author:Thmoas-Guan |
feat(Data): some lemmas about WithBot ENat |
Add some lemma about withBot ENat discovered when dealing with `ringKrullDim`
---
[](https://gitpod.io/from-referrer/)
|
t-data |
70/0 |
Mathlib/Algebra/Order/Monoid/Unbundled/WithTop.lean,Mathlib/Data/ENat/Basic.lean |
2 |
18 |
['Ruben-VandeVelde', 'Thmoas-Guan', 'YaelDillies', 'alreadydone', 'erdOne', 'github-actions', 'pechersky', 'urkud'] |
pechersky assignee:pechersky |
1-40231 1 day ago |
12-44453 12 days ago |
50-40703 50 days |
| 26212 |
Thmoas-Guan author:Thmoas-Guan |
feat(Algebra): the Rees theorem for depth |
In this PR we proved the Rees theorem for depth.
Co-authored-by: Hu Yongle
---
- [x] depends on: #27416
[](https://gitpod.io/from-referrer/)
|
t-algebra
large-import
label:t-algebra$ |
219/15 |
Mathlib/RingTheory/Regular/Category.lean,Mathlib/RingTheory/Regular/Depth.lean |
2 |
n/a |
['Thmoas-Guan', 'alreadydone', 'dagurtomas', 'erdOne', 'github-actions', 'mathlib4-dependent-issues-bot', 'mathlib4-merge-conflict-bot'] |
nobody |
1-40079 1 day ago |
unknown |
unknown |
| 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'] |
nobody |
1-37001 1 day ago |
3-54199 3 days ago |
18-74687 18 days |
| 33371 |
kex-y author:kex-y |
feat(Probability): Right continuous filtrations |
---
Co-authored-by: @EtienneC30
[](https://gitpod.io/from-referrer/)
|
t-measure-probability
brownian
|
163/0 |
Mathlib/Probability/Process/Filtration.lean |
1 |
1 |
['github-actions'] |
nobody |
1-36206 1 day ago |
1-36206 1 day ago |
1-40394 1 day |
| 33374 |
kex-y author:kex-y |
feat: Simple lemmas about convergence in WithTop |
---
Some useful lemmas required for #33375
[](https://gitpod.io/from-referrer/)
|
t-topology
brownian
|
32/0 |
Mathlib/Topology/Order/WithTop.lean |
1 |
1 |
['github-actions'] |
nobody |
1-36192 1 day ago |
1-36192 1 day ago |
1-37020 1 day |
| 33139 |
YaelDillies author:YaelDillies |
feat: transfer `Coalgebra.IsCocomm` across an `Equiv` |
---
[](https://gitpod.io/from-referrer/)
|
t-algebra label:t-algebra$ |
53/14 |
Mathlib/LinearAlgebra/TensorProduct/Associator.lean,Mathlib/LinearAlgebra/TensorProduct/Basic.lean,Mathlib/RingTheory/Coalgebra/Basic.lean |
3 |
2 |
['github-actions', 'joelriou'] |
joelriou assignee:joelriou |
1-34870 1 day ago |
1-34926 1 day ago |
8-16732 8 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$ |
124/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/RingTheory/Noetherian/Basic.lean |
5 |
11 |
['Thmoas-Guan', 'github-actions', 'jcommelin', 'joelriou', 'mathlib4-dependent-issues-bot', 'mathlib4-merge-conflict-bot'] |
joelriou assignee:joelriou |
1-34721 1 day ago |
1-45353 1 day ago |
1-71145 1 day |
| 31995 |
Thmoas-Guan author:Thmoas-Guan |
feat(RingTheory): Module being injective is local property |
In this PR, we proved that for module over Noetherian ring, being injective is local property.
---
[](https://gitpod.io/from-referrer/)
|
t-ring-theory |
231/0 |
Mathlib.lean,Mathlib/RingTheory/LocalProperties/Injective.lean |
2 |
5 |
['Thmoas-Guan', 'dagurtomas', 'github-actions'] |
nobody |
1-34172 1 day ago |
1-50912 1 day ago |
4-80892 4 days |
| 30886 |
urkud author:urkud |
feat(DifferentialForm): exterior derivative applied to vector fields |
---
- [x] depends on: #30331
[](https://gitpod.io/from-referrer/)
|
awaiting-author
t-analysis
|
217/0 |
Mathlib.lean,Mathlib/Analysis/Calculus/DifferentialForm/VectorField.lean,Mathlib/Analysis/Calculus/FDeriv/ContinuousAlternatingMap.lean,Mathlib/Topology/Algebra/Module/Alternating/Basic.lean |
4 |
7 |
['github-actions', 'mathlib4-dependent-issues-bot', 'mathlib4-merge-conflict-bot', 'mcdoll'] |
kex-y assignee:kex-y |
15-71918 15 days ago |
15-72020 15 days ago |
27-74832 27 days |
| 30373 |
sinhp author:sinhp |
feat(CategoryTheory): LCCC sections (constructing right adjoint to `Over.ChosenPullback.pullback`) |
In LCCCs development, the `sections` functor is used to define the right adjoint to the pullback functor `Over.ChosenPullback.pullback`.
This PR defines `Over.sections` and proves that it is a right adjoint to the `toOver (I : C) : C ⥤ Over I` (this is the computable analogue of `star`).
This is the computable enhancement of #22319: instead of `Limits.pullback` this PR builds on top of `Over.ChosenPullback` and thus we eliminate any instance of noncomputable constructs.
---
- [x] depends on: #31033
- [x] depends on: #31433
[](https://gitpod.io/from-referrer/)
|
awaiting-author
t-category-theory
|
173/0 |
Mathlib.lean,Mathlib/CategoryTheory/LocallyCartesianClosed/Sections.lean |
2 |
29 |
['dagurtomas', 'edegeltje', 'github-actions', 'joelriou', 'mathlib4-dependent-issues-bot', 'mathlib4-merge-conflict-bot', 'robin-carlier', 'sinhp'] |
robin-carlier assignee:robin-carlier |
4-43241 4 days ago |
4-53690 4 days ago |
5-80161 5 days |
| 33330 |
michael-novak-math author:michael-novak-math |
feat: add arc-length reparametrization of parametrized curves |
add new definitions of arc-length reparametrization and its corresponding parameter transformation and a theorem establishing the desired properties. |
t-analysis
new-contributor
|
309/1 |
Mathlib.lean,Mathlib/Analysis/Calculus/ArcLengthReparametrization.lean,Mathlib/MeasureTheory/Integral/IntervalIntegral/FundThmCalculus.lean,docs/references.bib,lake-manifest.json |
5 |
41 |
['SnirBroshi', 'github-actions', 'grunweg', 'michael-novak-math'] |
nobody |
1-20915 1 day ago |
3-20966 3 days ago |
3-32198 3 days |
| 33179 |
joelriou author:joelriou |
feat(CategoryTheory/Sites): relation between `IsPrestack` and the full faithfulness of `toDescentData` |
We show that a pseudofunctor `F` is a prestack iff the functors `F.toDescentData f` are fully faithful whenever `f` is a covering family. We also introduce predicates `F.IsPrestackFor R` and `F.IsStackFor R` (for a presieve `R`) saying the corresponding functor `F.DescentData (fun (f : R.category) ↦ f.obj.hom)` is fully faithful or an equivalence.
---
- [x] depends on: #33287
- [x] depends on: #30190
[](https://gitpod.io/from-referrer/)
|
t-category-theory |
275/3 |
Mathlib/CategoryTheory/Comma/Over/Basic.lean,Mathlib/CategoryTheory/Functor/FullyFaithful.lean,Mathlib/CategoryTheory/Sites/Descent/DescentData.lean,Mathlib/CategoryTheory/Sites/Descent/IsPrestack.lean |
4 |
n/a |
['dagurtomas', 'github-actions', 'mathlib4-dependent-issues-bot', 'mathlib4-merge-conflict-bot'] |
nobody |
1-18453 1 day ago |
unknown |
unknown |
| 27261 |
Sebi-Kumar author:Sebi-Kumar |
feat(Topology): add definition for subpaths |
Define subpaths as restrictions of paths to subintervals, reparameterized to have domain
`[0, 1]` and possibly with a reverse of direction. Prove their basic properties.
This serves as an alternative to `Path.truncate` which is useful for the explicit construction of certain homotopies, in particular regarding the concatenation of subpaths.
---
To provide additional context, this is my first time contributing to Mathlib,
and I am doing so as a part of the Fields Undergraduate Summer Research Program
hosted at Western University.
My intention for this file is for it to be used when proving that the fundamental group of the sphere is trivial (following the proof from Hatcher's "Algebraic Topology").
[](https://gitpod.io/from-referrer/)
|
t-topology
new-contributor
|
148/0 |
Mathlib.lean,Mathlib/Topology/Subpath.lean |
2 |
27 |
['ADedecker', 'FrankieNC', 'Sebi-Kumar', 'github-actions', 'mathlib4-merge-conflict-bot', 'themathqueen', 'wwylele'] |
ADedecker assignee:ADedecker |
1-16927 1 day ago |
1-16950 1 day ago |
43-74614 43 days |
| 33347 |
AntoineChambert-Loir author:AntoineChambert-Loir |
feat(LinearAlgebra/Transvection/Basic): define dilatransvections |
Define `LinearEquiv.dilatransvections`.
These are linear equivalences whose associated linear map is a transvection.
This definition has the interest of being usable without any assumption on the base ring.
Over a division ring, they correspond exactly to those linear equivalences `e` such that `e - LinearMap.id` has rank at most one.
They (will) appear in Dieudonné's theorem that describes the generation of elements of the general linear group as products of several transvections and one additional dilatransvection.
---
[](https://gitpod.io/from-referrer/)
|
|
143/31 |
Mathlib/LinearAlgebra/Transvection.lean |
1 |
n/a |
['AntoineChambert-Loir', 'github-actions'] |
nobody |
1-13191 1 day ago |
unknown |
unknown |
| 33319 |
vihdzp author:vihdzp |
refactor(SetTheory/Ordinal/Arithmetic): deprecate `boundedLimitRecOn` |
Its function can very easily be accomplished with the `induction` block; I've even gone ahead and replaced its proof so as to demonstrate this.
---
[](https://gitpod.io/from-referrer/)
|
maintainer-merge
t-set-theory
|
24/10 |
Mathlib/SetTheory/Ordinal/Arithmetic.lean |
1 |
2 |
['Ruben-VandeVelde', 'github-actions'] |
nobody |
1-4378 1 day ago |
1-4378 1 day ago |
4-15512 4 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 |
5 |
['github-actions', 'linesthatinterlace', 'vihdzp'] |
nobody |
1-4256 1 day ago |
8-41643 8 days ago |
8-41680 8 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 |
0-84176 23 hours ago |
11-800 11 days ago |
12-2555 12 days |
| 33389 |
khwilson author:khwilson |
feat(Mathlib/Analysis/SpecialFunctions/Log/Base): More log asymptotics |
A common utility in proving asymptotics is `logb b =O[⊤] log` and `(log ∘ (c * ·)) =O[atTop] log` and related lemmas `logb`. This PR fills these in for future use.
[](https://gitpod.io/from-referrer/)
|
t-analysis
new-contributor
|
51/0 |
Mathlib/Analysis/SpecialFunctions/Log/Base.lean |
1 |
2 |
['github-actions'] |
nobody |
0-81795 22 hours ago |
1-5322 1 day ago |
1-5357 1 day |
| 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 |
0-78995 21 hours ago |
4-12988 4 days ago |
4-13447 4 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 |
0-78994 21 hours ago |
4-74994 4 days ago |
4-74969 4 days |
| 33299 |
kingiler author:kingiler |
feat: Add decidable membership for Interval |
Implemented membership and corresponding decidable instance for `Interval`.
Related [#mathlib4 > Proposal: Add decidable membership for Interval](https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/Proposal.3A.20Add.20decidable.20membership.20for.20Interval/with/565438009).
---
[](https://gitpod.io/from-referrer/)
|
t-order
new-contributor
|
16/1 |
Mathlib/Order/Interval/Basic.lean |
1 |
3 |
['eric-wieser', 'github-actions', 'kingiler'] |
Vierkantor assignee:Vierkantor |
0-78993 21 hours ago |
4-63077 4 days ago |
4-67660 4 days |
| 33298 |
vihdzp author:vihdzp |
chore: mark `Ordinal.enumOrd` with `no_expose` |
The definition is an implementation detail, and this function is fully characterized by being an order isomorphism.
---
[](https://gitpod.io/from-referrer/)
|
easy
t-set-theory
|
1/0 |
Mathlib/SetTheory/Ordinal/Enum.lean |
1 |
1 |
['github-actions'] |
alreadydone assignee:alreadydone |
0-78993 21 hours ago |
4-73086 4 days ago |
4-73067 4 days |
| 33301 |
themathqueen author:themathqueen |
chore(Algebra/Central/End): generalize `Algebra.IsCentral.instEnd` |
---
This came up during review of #33282.
[](https://gitpod.io/from-referrer/)
|
t-algebra label:t-algebra$ |
41/11 |
Mathlib/Algebra/Central/End.lean,Mathlib/LinearAlgebra/FreeModule/Basic.lean |
2 |
2 |
['AntoineChambert-Loir', 'github-actions'] |
erdOne assignee:erdOne |
0-78992 21 hours ago |
4-54983 4 days ago |
4-55015 4 days |
| 33306 |
YuvalFilmus author:YuvalFilmus |
feat(Polynomial/Derivative): formulas for iterated derivatives of P * X^m |
Derived formula for the iterated derivative of a polynomial multiplied by a power of X.
These will be used in a subsequent PR about Chebyshev polynomials.
---
[](https://gitpod.io/from-referrer/)
|
t-algebra label:t-algebra$ |
92/0 |
Mathlib/Algebra/Polynomial/Derivative.lean |
1 |
1 |
['github-actions'] |
ocfnash assignee:ocfnash |
0-78991 21 hours ago |
4-35093 4 days ago |
4-35127 4 days |
| 33308 |
LTolDe author:LTolDe |
feat(Topology.GDelta.Basic): add helpers for IsMeagre |
add the following helpers:
- IsNowhereDense.isMeagre
- exists_of_not_meagre_biUnion
- Topology.IsInducing.isMeagre_image
- IsMeagre.image_val
This PR follows #32740, which adds helpers for IsNowhereDense.
These lemmas will help to prove the **Effros Theorem**, see [zulip thread](https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/Effros.20Theorem/with/558712441).
---
[](https://gitpod.io/from-referrer/)
|
t-topology
new-contributor
large-import
|
59/1 |
Mathlib/Topology/GDelta/Basic.lean |
1 |
1 |
['github-actions'] |
jcommelin assignee:jcommelin |
0-78990 21 hours ago |
4-32148 4 days ago |
4-32192 4 days |
| 33327 |
vihdzp author:vihdzp |
doc(Topology/Defs/Filter): mention "Kolmogorov quotient" in docstring |
---
[](https://gitpod.io/from-referrer/)
|
documentation
easy
t-topology
|
4/4 |
Mathlib/Topology/Defs/Filter.lean |
1 |
1 |
['github-actions'] |
dagurtomas assignee:dagurtomas |
0-78989 21 hours ago |
3-82245 3 days ago |
3-82235 3 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 |
28 |
['alreadydone', 'artie2000', 'astrainfinita', 'github-actions', 'leanprover-bot', 'leanprover-community-mathlib4-bot', 'mathlib4-merge-conflict-bot'] |
alreadydone assignee:alreadydone |
0-76785 21 hours ago |
0-76839 21 hours ago |
17-68982 17 days |
| 33394 |
dupuisf author:dupuisf |
feat: add lemmas about doubly stochastic matrices |
This PR adds a few basic lemmas about doubly stochastic matrices.
---
[](https://gitpod.io/from-referrer/)
|
t-analysis |
59/0 |
Mathlib/Analysis/Convex/DoublyStochasticMatrix.lean |
1 |
1 |
['github-actions'] |
nobody |
0-73082 20 hours ago |
0-73082 20 hours ago |
0-74078 20 hours |
| 33216 |
stepan2698-cpu author:stepan2698-cpu |
feat: Schur's lemma over an algebraically closed field |
Adds a new file with facts about algebra representations. Proves Schur's lemma (any endomorphism of an algebra representation over an algebraically closed field is scalar) and proves that every finite-dimensional representation of a commutative algebra over an algebraically closed field is one-dimensional.
---
[](https://gitpod.io/from-referrer/)
|
t-algebra
new-contributor
label:t-algebra$ |
83/0 |
Mathlib.lean,Mathlib/RepresentationTheory/AlgebraRepresentation/Basic.lean |
2 |
1 |
['github-actions'] |
nobody |
0-72676 20 hours ago |
7-69479 7 days ago |
7-69517 7 days |
| 33385 |
peakpoint author:peakpoint |
refactor(Geometry/Euclidean/Projection): revert everything back to metric space |
After #27378 was merged, @jsm28 noted that `[NormedAddCommGroup V] [PseudoMetricSpace P] [NormedAddTorsor V P]` implies `[MetricSpace P]` anyways so there's no point distinguishing between `PseudoMetricSpace` and `MetricSpace`.
---
[](https://gitpod.io/from-referrer/)
|
t-euclidean-geometry
maintainer-merge
|
15/33 |
Mathlib/Geometry/Euclidean/Projection.lean |
1 |
3 |
['github-actions', 'jsm28'] |
nobody |
0-71688 19 hours ago |
1-16429 1 day ago |
1-20514 1 day |
| 28126 |
Sebi-Kumar author:Sebi-Kumar |
feat(AlgebraicTopology/FundamentalGroupoid): relate equality in fundamental groupoid to homotopy |
Prove the theorem `fromPath_eq_iff_homotopic` which shows that two paths are equal in the fundamental groupoid if and only if they are homotopic. This allows one to prove two paths are homotopic by transferring to the fundamental groupoid and using `simp`.
---
I would like to thank Kenny Lau for inspiring this code on Zulip at [#Is there code for X? > Using aesop_cat to prove paths are homotopic](https://leanprover.zulipchat.com/#narrow/channel/217875-Is-there-code-for-X.3F/topic/Using.20aesop_cat.20to.20prove.20paths.20are.20homotopic).
Also, I would like to note that I am a newcomer when it comes to contributing to Mathlib, and that this code was written as a part of a formalization project at the University of Western Ontario under the supervision of Chris Kapulkin and Daniel Carranza (which is happening through the Fields Undergraduate Summer Research Program).
[](https://gitpod.io/from-referrer/)
|
new-contributor
t-algebraic-topology
|
5/0 |
Mathlib/AlgebraicTopology/FundamentalGroupoid/Basic.lean |
1 |
12 |
['Sebi-Kumar', 'alreadydone', 'github-actions', 'mathlib4-merge-conflict-bot', 'mattrobball'] |
mattrobball assignee:mattrobball |
0-70612 19 hours ago |
0-70987 19 hours ago |
15-14872 15 days |
| 32988 |
Whysoserioushah author:Whysoserioushah |
feat(RingTheory/Morita/Matrix) : more on morita equivalence between `R` and `Mn(R)` |
---
[](https://gitpod.io/from-referrer/)
|
t-ring-theory |
110/2 |
Mathlib/RingTheory/Morita/Matrix.lean |
1 |
15 |
['Whysoserioushah', 'erdOne', 'github-actions'] |
nobody |
0-61087 16 hours ago |
2-71789 2 days ago |
13-31611 13 days |
| 33395 |
themathqueen author:themathqueen |
feat(Algebra/Star/LinearMap): `LinearMap.intrinsicStar_{toSpanSingleton, smulRight}` |
---
[](https://gitpod.io/from-referrer/)
|
easy
t-algebra
label:t-algebra$ |
19/2 |
Mathlib/Algebra/Star/LinearMap.lean |
1 |
2 |
['github-actions', 'themathqueen'] |
nobody |
0-54568 15 hours ago |
0-73046 20 hours ago |
0-73084 20 hours |
| 33397 |
themathqueen author:themathqueen |
feat(Algebra/Star/LinearMap): intrinsic star for continuous linear maps |
---
[](https://gitpod.io/from-referrer/)
|
t-algebra
large-import
label:t-algebra$ |
79/0 |
Mathlib/Algebra/Star/LinearMap.lean |
1 |
1 |
['github-actions'] |
nobody |
0-52855 14 hours ago |
0-69031 19 hours ago |
0-69081 19 hours |
| 32725 |
joelriou author:joelriou |
feat(CategoryTheory): presheaves of types which preserve a limit |
Let `F : J ⥤ Cᵒᵖ` be a functor. We show that a presheaf `P : Cᵒᵖ ⥤ Type w` preserves the limit of `F` iff `P` is a local object with respect to a suitable family of morphisms in `Cᵒᵖ ⥤ Type w` (this family contains `1` or `0` morphism depending on whether the limit of `F` exists or not).
---
[](https://gitpod.io/from-referrer/)
|
t-category-theory |
187/0 |
Mathlib.lean,Mathlib/CategoryTheory/MorphismProperty/Basic.lean,Mathlib/CategoryTheory/MorphismProperty/IsSmall.lean,Mathlib/CategoryTheory/ObjectProperty/FunctorCategory/Presheaf.lean,Mathlib/CategoryTheory/ObjectProperty/Local.lean |
5 |
5 |
['github-actions', 'joelriou', 'robin-carlier'] |
nobody |
0-52285 14 hours ago |
0-52285 14 hours ago |
1-45870 1 day |
| 32266 |
joelriou author:joelriou |
feat(AlgebraicTopology): finite simplicial sets are `ℵ₀`-presentable |
In this file, we show that finite simplicial sets are `ℵ₀`-presentable, which will allow the use of the small object argument in `SSet`.
This PR relaxes the import ban of `SetTheory` in `AlgebraicTopology`: almost all constructions of model category structures require the small object argument.
From https://github.com/joelriou/topcat-model-category
---
- [x] depends on: #32201
- [x] depends on: #32202
- [x] depends on: #32237
- [x] depends on: #32251
- [x] depends on: #32265
- [x] depends on: #32085
[](https://gitpod.io/from-referrer/)
|
large-import
t-algebraic-topology
|
157/2 |
Mathlib.lean,Mathlib/AlgebraicTopology/SimplicialSet/FiniteColimits.lean,Mathlib/AlgebraicTopology/SimplicialSet/Presentable.lean,Mathlib/AlgebraicTopology/SimplicialSet/RegularEpi.lean,Mathlib/CategoryTheory/Comma/CardinalArrow.lean,Mathlib/CategoryTheory/Limits/Shapes/Pullback/CommSq.lean,Mathlib/CategoryTheory/Limits/Shapes/RegularMono.lean,Mathlib/CategoryTheory/Limits/Types/Pullbacks.lean,Mathlib/CategoryTheory/Presentable/Presheaf.lean,Mathlib/Tactic/Linter/DirectoryDependency.lean |
10 |
9 |
['github-actions', 'joelriou', 'mathlib4-dependent-issues-bot', 'mathlib4-merge-conflict-bot', 'robin-carlier'] |
dagurtomas assignee:dagurtomas |
0-51739 14 hours ago |
3-45744 3 days ago |
6-32116 6 days |
| 33398 |
vihdzp author:vihdzp |
feat: `IsStrictOrderedRing (Lex R⟦Γ⟧)` |
Used in the CGT repo.
---
I don't know if it's possible to relax `Ring` to `Semiring`.
[](https://gitpod.io/from-referrer/)
|
large-import
t-ring-theory
|
55/17 |
Mathlib/RingTheory/HahnSeries/Lex.lean,Mathlib/RingTheory/HahnSeries/Multiplication.lean |
2 |
1 |
['github-actions'] |
nobody |
0-50649 14 hours ago |
0-50905 14 hours ago |
0-50952 14 hours |
| 32835 |
vasnesterov author:vasnesterov |
fix(Tactic/Order): equal but not syntactically equal types |
When collecting atoms, `order` relies only on syntactic equality of types. This PR replaces this with defeq check and adds a test that failed before.
---
[](https://gitpod.io/from-referrer/)
|
bug
t-meta
maintainer-merge
|
22/3 |
Mathlib/Tactic/Order/CollectFacts.lean,MathlibTest/order.lean |
2 |
5 |
['Vierkantor', 'artie2000', 'github-actions', 'j-loreaux', 'vasnesterov'] |
thorimur assignee:thorimur |
0-37922 10 hours ago |
13-11566 13 days ago |
17-34738 17 days |
| 33401 |
AntoineChambert-Loir author:AntoineChambert-Loir |
chore(Algebra/Group/Subgroup/Pointwise.lean): remove one hypothesis from `Subgroup.closure_pow_le` |
Remove the hypothesis on `n` from `Subgroup.closure_pow_le`
---
[](https://gitpod.io/from-referrer/)
|
easy
t-algebra
t-group-theory
label:t-algebra$ |
4/10 |
Mathlib/Algebra/Group/Subgroup/Pointwise.lean |
1 |
4 |
['github-actions', 'themathqueen'] |
nobody |
0-36899 10 hours ago |
0-47015 13 hours ago |
0-47055 13 hours |
| 33400 |
mcdoll author:mcdoll |
chore(Analysis/SchwartzSpace): add `fun_prop` tag |
---
[](https://gitpod.io/from-referrer/)
|
t-analysis |
9/1 |
Mathlib/Analysis/Distribution/SchwartzSpace.lean |
1 |
5 |
['github-actions', 'grunweg', 'mcdoll'] |
nobody |
0-36648 10 hours ago |
0-39291 10 hours ago |
0-39266 10 hours |
| 33362 |
urkud author:urkud |
feat: weaken assumptions in Schwarz lemma |
Assume that `f` maps an open ball to a closed ball.
Also, generalize the "same radius" versions to any codomain.
---
[](https://gitpod.io/from-referrer/)
|
t-analysis |
42/51 |
Mathlib/Analysis/Complex/Schwarz.lean |
1 |
4 |
['github-actions', 'urkud', 'vihdzp'] |
nobody |
0-30539 8 hours ago |
2-6229 2 days ago |
2-6270 2 days |
| 33383 |
wangying11123 author:wangying11123 |
feat(Geometry/Euclidean/Angle/Unoriented/Affine): Add Theorem about Sbtw.angle_eq and Wbtw.angle_eq |
add some theorems about Sbtw.angle_eq and Wbtw.angle_eq.
Main additions
`_root_.Sbtw.angle_eq_right`
- An Unoriented angle is unchanged by replacing the third point by one strictly further away on the same ray.
`_root_.Sbtw.angle_eq_left`
- An Unoriented angle is unchanged by replacing the first point by one strictly further away on the same ray.
`_root_.Wbtw.angle_eq_right`
- An Unoriented angle is unchanged by replacing the third point by one weakly further away on the same ray.
`_root_.Wbtw.angle_eq_left`
- An Unoriented angle is unchanged by replacing the first point by one weakly further away on the same ray. |
t-euclidean-geometry
new-contributor
|
30/0 |
Mathlib/Geometry/Euclidean/Angle/Unoriented/Affine.lean |
1 |
8 |
['github-actions', 'jsm28', 'wangying11123'] |
nobody |
0-25717 7 hours ago |
1-28961 1 day ago |
1-28997 1 day |
| 28411 |
zcyemi author:zcyemi |
feat(LinearAlgebra/AffineSpace/Simplex/Centroid): define centroid and medians |
---
This file proves several lemmas involving the centroids and medians of a simplex in affine space.
definitions:
- `centroid` is the centroid of a simplex, defined as abbreviation of the `Finset.univ.centroid`.
- `faceOppositeCentroid` is the centroid of the facet obtained as `(Simplex.faceOpposite i).centroid`
- `median` is the line connecting a vertex to the faceOppositeCentroid.
Main Results:
- Commandino's theorem
- The medians of a simplex are concurrent at the centroid
- [ ] depends on #29128 |
t-algebra label:t-algebra$ |
514/7 |
Mathlib/Geometry/Euclidean/MongePoint.lean,Mathlib/Geometry/Euclidean/Simplex.lean,Mathlib/LinearAlgebra/AffineSpace/FiniteDimensional.lean,Mathlib/LinearAlgebra/AffineSpace/Simplex/Centroid.lean,docs/1000.yaml |
5 |
26 |
['github-actions', 'jsm28', 'mathlib4-merge-conflict-bot', 'zcyemi'] |
jsm28 assignee:jsm28 |
0-25144 6 hours ago |
4-24173 4 days ago |
36-15998 36 days |
| 33365 |
zcyemi author:zcyemi |
feat(Geometry/Euclidean/Angle/Oriented/Affine): Add oangle sign lemmas for two intersecting lines |
---
Add oangle sign lemmas for two intersecting lines:
`Sbtw.oangle_sign_eq_of_sbtw` and `Sbtw.oangle_sign_eq_of_sbtw_left`
|
t-euclidean-geometry
maintainer-merge
|
18/0 |
Mathlib/Geometry/Euclidean/Angle/Oriented/Affine.lean |
1 |
6 |
['JovanGerb', 'github-actions', 'jsm28', 'zcyemi'] |
nobody |
0-24963 6 hours ago |
0-24963 6 hours ago |
1-71794 1 day |
| 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/)
|
|
86/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 |
1 |
['github-actions'] |
nobody |
0-23771 6 hours ago |
0-39664 11 hours ago |
0-39638 11 hours |
| 25889 |
plp127 author:plp127 |
fix(Tactic/Widget/Conv): fix various issues |
Fixes various issues with the `conv?` widget. Closes #25162.
([Zulip thread](https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/bug.20in.20.60conv.3F.60))
Specifically, fixes issues with `conv?` where
- when converting a `SubExpr.Pos` to conv directions, it always uses the goal expression as reference, even when working on a hypothesis, this often leads to bad results and makes it unusable on hypotheses
- it refuses to go all the way in to a function (for example in `Nat.succ 0`, you can't access `Nat.succ`)
- it refuses to enter binders where the name of the bound variable contains the character `0` (try it on `∀ (x0 : Nat), x0 = x0`)
- it panics if it can't find a binder name instead of just coming up with one itself, this also means usually you can't enter either side of a non-dependent arrow since those usually don't have binder names (try it on `False → False`)
- you can't enter the type of a binder, you end up going into the body instead (try it on `fun (x : False) => (x.elim : False → Nat) x.elim`)
- you can't partially enter a function, you end up going to the top argument after instead (for example, in the expression `id (id id) 0`, when you click on `id (id id)`, you end up going to `id id`)
---
[](https://gitpod.io/from-referrer/)
|
t-meta |
429/99 |
Mathlib/Tactic/Widget/Conv.lean,MathlibTest/conv_widget.lean |
2 |
6 |
['bryangingechen', 'github-actions', 'mathlib4-merge-conflict-bot', 'plp127'] |
bryangingechen and kmill assignee:kmill assignee:bryangingechen |
0-65239 18 hours ago |
1-9061 1 day ago |
71-67803 71 days |
| 33242 |
mcdoll author:mcdoll |
feat(Analysis/Fourier): `L2` and `TemperedDistribution` Fourier transforms coincide |
The Fourier transform on `L2` is defined via extension of the `SchwartzMap` Fourier transform and the Fourier transform
on `TemperedDistribution` is defined via self-adjointness and every `L2` function defines a tempered distribution. We show that these definitions behave as expected and give the same notion of Fourier transform.
---
- [x] depends on: #33229
- [ ] depends on: #33232
[](https://gitpod.io/from-referrer/)
|
t-analysis |
32/4 |
Mathlib/Analysis/Fourier/LpSpace.lean |
1 |
n/a |
['github-actions', 'mathlib4-dependent-issues-bot'] |
nobody |
4-71111 4 days ago |
unknown |
unknown |
| 33066 |
themathqueen author:themathqueen |
feat(Analysis/Normed/Operator): star-algebra equivalences between continuous endomorphisms are isometrically inner |
This is the star-algebra equivalence version of [AlgEquiv.eq_linearEquivConjAlgEquiv](https://leanprover-community.github.io/mathlib4_docs/Mathlib/LinearAlgebra/GeneralLinearGroup/AlgEquiv.html#AlgEquiv.eq_linearEquivConjAlgEquiv) and [ContinuousAlgEquiv.eq_continuousLinearEquivConjContinuousAlgEquiv](https://leanprover-community.github.io/mathlib4_docs/Mathlib/Analysis/Normed/Operator/ContinuousAlgEquiv.html#ContinuousAlgEquiv.eq_continuousLinearEquivConjContinuousAlgEquiv). So we now have a characterization of algebra, continuous algebra, and star-algebra equivalences between endomorphisms.
The proof follows the same idea as the one in #28972.
---
The proof of this is much longer than the `ContinuousAlgEquiv` and the `AlgEquiv` versions. Please feel free to golf!
The proof has private auxiliary lemmas and definitions because otherwise the proof gets too long and slow.
- [x] depends on: #33017
- [x] depends on: #33022
[](https://gitpod.io/from-referrer/)
|
t-analysis
large-import
|
205/5 |
Mathlib/Analysis/InnerProductSpace/Adjoint.lean,Mathlib/Analysis/Normed/Operator/ContinuousAlgEquiv.lean,Mathlib/LinearAlgebra/GeneralLinearGroup/AlgEquiv.lean,Mathlib/Topology/Algebra/Algebra/Equiv.lean |
4 |
3 |
['github-actions', 'mathlib4-dependent-issues-bot', 'mathlib4-merge-conflict-bot'] |
j-loreaux assignee:j-loreaux |
0-77640 21 hours ago |
3-12328 3 days ago |
3-12378 3 days |
| 32946 |
tb65536 author:tb65536 |
refactor(Algebra/Polynomial/Factors): Deprecate file |
This PR finishes the refactor of `Splits.lean` by moving the new API in `Factors.lean` back into `Splits.lean`.
---
[](https://gitpod.io/from-referrer/)
|
t-algebra label:t-algebra$ |
594/617 |
Mathlib/Algebra/Polynomial/Factors.lean,Mathlib/Algebra/Polynomial/Splits.lean,Mathlib/RingTheory/Polynomial/ScaleRoots.lean |
3 |
4 |
['github-actions', 'mathlib4-merge-conflict-bot', 'vihdzp'] |
dagurtomas assignee:dagurtomas |
6-78993 6 days ago |
10-16586 10 days ago |
14-15906 14 days |
| 33054 |
MichaelStollBayreuth author:MichaelStollBayreuth |
feat(NumberTheory/Height/Basic): first installment of heights |
This is the first PR in a series that aims at providing heights (in the sense of arithmetic geometry).
Here we define a class `Height.AdmissibleAbsValues` that captures a family of "admissible" absolute values (finitely many archimedean ones, an arbitrary family of nonarchimedean ones, satisfying a finiteness condition and a product formula) and define the multiplicative and the logarithmic height of an element of a field `K` endowed with such a family.
The following PRs will add the definitions of heights of tuples of elements of `K` and finitely supported maps to `K`, prove some basic properties, add an instancesof `AdmissibleAbsValues` for number fields, etc.
See the [Heights](https://github.com/MichaelStollBayreuth/Heights) repository.
We need a couple of API lemmas, one of which was put in a new file because no suitable existing home could be found.
---
[](https://gitpod.io/from-referrer/)
|
t-number-theory |
329/9 |
Mathlib.lean,Mathlib/Algebra/BigOperators/Finprod.lean,Mathlib/Algebra/Order/BigOperators/GroupWithZero/Finset.lean,Mathlib/NumberTheory/Height/Basic.lean,Mathlib/NumberTheory/Height/Instances.lean,Mathlib/NumberTheory/NumberField/FinitePlaces.lean,Mathlib/NumberTheory/NumberField/InfinitePlace/Basic.lean |
7 |
17 |
['AntoineChambert-Loir', 'MichaelStollBayreuth', 'Ruben-VandeVelde', 'github-actions', 'tb65536'] |
tb65536 assignee:tb65536 |
0-44469 12 hours ago |
3-1507 3 days ago |
7-29815 7 days |
| 25925 |
BoltonBailey author:BoltonBailey |
feat: file for lemmas about MvPolynomials over NoZeroDivisors |
This PR creates a new file for lemmas about `MvPolynomial`s over rings which are `NoZeroDivisors`, to make modified versions of lemmas like `degreeOf_C_mul`.
Original PR: https://github.com/leanprover-community/mathlib4/pull/11106
- [x] depends on: #11095
- [x] depends on: #11094
- [x] depends on: #25926 [We need this lemma to establish fact about degreeOf n (p + q)]
- [x] depends on: #32558
---
Notes to self:
* Can the results in this file be generalized?
* Perhaps to the assumption `IsCancelMulZero R`?
* Note that when `R` is a ring, `IsCancelMulZero R` is equivalent to
`NoZeroDivisors R`.
* When `R` is only a semiring, `NoZeroDivisors R` is implied by `IsCancelMulZero R`
(although this is not typeclass inferrable, see `IsLeftCancelMulZero.to_noZeroDivisors`),
* When `R` is only a semiring, `IsCancelMulZero R` is not implied by `NoZeroDivisors R`, see https://leanprover.zulipchat.com/#narrow/channel/116395-maths/topic/IsCancelMulZero.20and.20NoZeroDivisors.20for.20semirings/with/562333254
* Thus, we should see if the results in this file can be generalized to
`IsCancelMulZero R`.
* Note that `MvPolynomial.totalDegree_mul_of_isDomain` exists, which proves a related result
under the assumption `IsCancelMulZero R`.
* This seems weaker than it could be!
* I will try to open PR to generalize these results to `NoZeroDivisors R` in a new PR.
* Perhaps to more specific assumptions about cancellation on leadingCoeffs?
This PR continues the work from #11106 and #11073 |
t-algebra label:t-algebra$ |
227/112 |
Mathlib.lean,Mathlib/Algebra/MvPolynomial/Degrees.lean,Mathlib/Algebra/MvPolynomial/NoZeroDivisors.lean,Mathlib/FieldTheory/SeparablyGenerated.lean,Mathlib/RingTheory/MvPolynomial/IrreducibleQuadratic.lean,Mathlib/RingTheory/MvPolynomial/MonomialOrder/DegLex.lean |
6 |
32 |
['BoltonBailey', 'erdOne', 'github-actions', 'leanprover-radar', 'mathlib4-dependent-issues-bot', 'riccardobrasca'] |
riccardobrasca assignee:riccardobrasca |
1-47453 1 day ago |
5-4931 5 days ago |
13-25997 13 days |