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-79683 1 month ago |
36-46972 1 month ago |
36-46948 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-38297 29 days ago |
29-39820 29 days ago |
38-84571 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-79688 28 days ago |
32-28912 1 month ago |
34-29339 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-79678 28 days ago |
34-71988 1 month ago |
34-72032 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-17071 28 days ago |
32-17041 1 month ago |
32-18136 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-79674 27 days ago |
31-69753 1 month ago |
31-72378 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-79664 27 days ago |
31-30611 1 month ago |
31-30646 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-9806 25 days ago |
55-26782 1 month ago |
55-26738 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-42729 24 days ago |
24-45747 24 days ago |
25-735 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-17439 23 days ago |
23-17558 23 days ago |
28-11991 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-1497 23 days ago |
29-4699 29 days ago |
29-7653 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-79680 22 days ago |
25-86011 25 days ago |
27-4212 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-41827 22 days ago |
22-41856 22 days ago |
22-49436 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-79679 21 days ago |
25-66994 25 days ago |
25-66985 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-10636 19 days ago |
19-24822 19 days ago |
39-71377 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-26471 18 days ago |
22-40676 22 days ago |
22-40968 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-79679 17 days ago |
21-4875 21 days ago |
21-4913 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-79678 17 days ago |
20-85112 20 days ago |
20-85136 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-79665 16 days ago |
21-66110 21 days ago |
25-10993 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-63808 16 days ago |
23-10251 23 days ago |
23-10294 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-22279 16 days ago |
21-17147 21 days ago |
21-17412 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-79677 15 days ago |
21-20348 21 days ago |
21-20383 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-17565 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-79660 14 days ago |
18-20760 18 days ago |
18-20795 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-69852 14 days ago |
21-77468 21 days ago |
42-73537 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-28819 14 days ago |
20-48719 20 days ago |
44-25695 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-79687 13 days ago |
17-69037 17 days ago |
17-69072 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-79677 13 days ago |
17-4704 17 days ago |
17-4741 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-24057 13 days ago |
13-24104 13 days ago |
18-52737 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-17009 13 days ago |
13-17012 13 days ago |
19-14267 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-79685 12 days ago |
16-14228 16 days ago |
19-63734 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-79679 12 days ago |
18-62634 18 days ago |
18-62611 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-79677 12 days ago |
16-40906 16 days ago |
16-72980 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-68329 12 days ago |
23-8973 23 days ago |
23-9006 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-67869 12 days ago |
22-72172 22 days ago |
22-72216 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-16731 12 days ago |
12-20703 12 days ago |
17-16189 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-4893 12 days ago |
12-4957 12 days ago |
20-35956 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-84220 11 days ago |
11-84444 11 days ago |
20-1904 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-83946 11 days ago |
11-84438 11 days ago |
22-2654 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-79677 11 days ago |
15-17917 15 days ago |
18-4880 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-79676 11 days ago |
15-23991 15 days ago |
17-64351 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-79675 11 days ago |
15-72467 15 days ago |
15-72445 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-43875 11 days ago |
12-72286 12 days ago |
12-72331 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-30162 11 days ago |
36-58225 1 month ago |
37-2717 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-1510 11 days ago |
11-1536 11 days ago |
23-56886 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-1245 11 days ago |
11-68100 11 days ago |
29-80003 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 |
11-77 11 days ago |
35-6292 1 month ago |
35-8838 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-79695 10 days ago |
14-4858 14 days ago |
14-7366 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-79694 10 days ago |
23-21854 23 days ago |
23-32147 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-79691 10 days ago |
17-72805 17 days ago |
17-72813 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-79689 10 days ago |
14-39778 14 days ago |
14-40116 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-46651 10 days ago |
10-46651 10 days ago |
46-51617 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-45426 10 days ago |
10-45485 10 days ago |
32-24410 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-23416 10 days ago |
11-47600 11 days ago |
25-48522 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-79665 9 days ago |
20-5559 20 days ago |
20-5596 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-79664 9 days ago |
19-27686 19 days ago |
19-27767 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-79661 9 days ago |
15-29237 15 days ago |
15-29566 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-79660 9 days ago |
13-70467 13 days ago |
13-70506 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-79657 9 days ago |
13-3760 13 days ago |
13-3736 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-73691 9 days ago |
9-73715 9 days ago |
19-29383 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-62869 9 days ago |
18-64336 18 days ago |
19-23242 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-42584 9 days ago |
9-42610 9 days ago |
39-38726 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-79667 8 days ago |
12-24599 12 days ago |
12-31925 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-79666 8 days ago |
11-83952 11 days ago |
33-81035 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-79658 8 days ago |
12-18331 12 days ago |
12-18384 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-79655 8 days ago |
12-10162 12 days ago |
12-10138 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-52608 8 days ago |
8-52836 8 days ago |
112-30397 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-48881 8 days ago |
9-83550 9 days ago |
148-28842 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-41631 8 days ago |
8-41635 8 days ago |
8-41676 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-37369 8 days ago |
14-41885 14 days ago |
14-61636 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-23017 8 days ago |
16-24808 16 days ago |
16-24850 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-22889 8 days ago |
10-49591 10 days ago |
21-66962 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-22031 8 days ago |
41-44245 1 month ago |
46-1076 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-85074 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-79683 7 days ago |
11-19293 11 days ago |
11-19355 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-79680 7 days ago |
12-57205 12 days ago |
12-57248 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-79679 7 days ago |
11-4084 11 days ago |
11-74885 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-79678 7 days ago |
11-4105 11 days ago |
11-65853 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-79677 7 days ago |
10-83147 10 days ago |
11-42693 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-79675 7 days ago |
11-38197 11 days ago |
11-38243 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-79673 7 days ago |
11-17817 11 days ago |
11-18106 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-79670 7 days ago |
11-6602 11 days ago |
11-6586 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-79669 7 days ago |
10-85728 10 days ago |
10-85705 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-73917 7 days ago |
7-75683 7 days ago |
12-72804 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-62003 7 days ago |
7-73603 7 days ago |
7-73647 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-43066 7 days ago |
13-52691 13 days ago |
20-63288 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-85903 6 days ago |
7-3425 7 days ago |
10-66086 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-79678 6 days ago |
14-66951 14 days ago |
14-66988 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-79676 6 days ago |
10-75271 10 days ago |
12-32286 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-79675 6 days ago |
11-7752 11 days ago |
11-15669 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-79672 6 days ago |
10-29807 10 days ago |
10-31571 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-79671 6 days ago |
10-37314 10 days ago |
10-37356 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-79670 6 days ago |
10-3366 10 days ago |
10-27902 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-79669 6 days ago |
10-22752 10 days ago |
10-25784 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-79668 6 days ago |
10-6124 10 days ago |
10-6162 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-79668 6 days ago |
10-15731 10 days ago |
10-15769 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-56186 6 days ago |
15-15766 15 days ago |
15-15848 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-38111 6 days ago |
6-38123 6 days ago |
6-38160 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-34356 6 days ago |
6-40298 6 days ago |
6-40339 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-31018 6 days ago |
6-31018 6 days ago |
12-67799 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-24427 6 days ago |
9-84452 9 days ago |
27-17196 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-16128 6 days ago |
17-65535 17 days ago |
21-58916 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-14893 6 days ago |
6-37599 6 days ago |
6-37638 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-8933 6 days ago |
33-77301 1 month ago |
33-77335 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-83419 5 days ago |
5-83419 5 days ago |
51-81931 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-79685 5 days ago |
9-72819 9 days ago |
9-72866 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-79683 5 days ago |
9-16332 9 days ago |
9-16378 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-79681 5 days ago |
8-82401 8 days ago |
8-82442 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-55053 5 days ago |
5-55077 5 days ago |
31-51710 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-41254 5 days ago |
10-49272 10 days ago |
10-49314 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-3983 5 days ago |
5-3983 5 days ago |
5-71753 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-84475 4 days ago |
5-19991 5 days ago |
7-77928 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-79678 4 days ago |
8-41017 8 days ago |
8-41068 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-79674 4 days ago |
7-83260 7 days ago |
7-83240 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-70459 4 days ago |
5-2863 5 days ago |
5-2913 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-65157 4 days ago |
10-52661 10 days ago |
10-74879 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-61295 4 days ago |
4-61295 4 days ago |
6-75324 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-29540 4 days ago |
10-75239 10 days ago |
10-75279 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-26622 4 days ago |
17-35515 17 days ago |
20-63696 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-79688 3 days ago |
4-11150 4 days ago |
4-13475 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-79687 3 days ago |
19-23011 19 days ago |
19-23064 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-79684 3 days ago |
7-8114 7 days ago |
7-62984 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-79683 3 days ago |
14-22015 14 days ago |
14-22054 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-79680 3 days ago |
7-22930 7 days ago |
7-22973 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-79679 3 days ago |
6-81074 6 days ago |
6-81114 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-26507 1 day ago |
3-64618 3 days ago |
3-64607 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-60769 3 days ago |
4-30917 4 days ago |
4-85758 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-51264 3 days ago |
3-51264 3 days ago |
10-17738 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-40147 3 days ago |
5-49709 5 days ago |
9-63092 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-25429 3 days ago |
3-28012 3 days ago |
3-40789 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-23096 3 days ago |
3-46512 3 days ago |
3-82648 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-18405 3 days ago |
3-18405 3 days ago |
11-25203 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-16899 3 days ago |
19-26282 19 days ago |
19-26316 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-14028 3 days ago |
3-14028 3 days ago |
8-11640 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-7672 3 days ago |
3-7672 3 days ago |
10-66361 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-84319 2 days ago |
2-84327 2 days ago |
4-18721 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-82877 2 days ago |
2-82877 2 days ago |
3-47153 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-79651 2 days ago |
19-25144 19 days ago |
19-25130 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-79649 2 days ago |
13-80795 13 days ago |
13-80771 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-79646 2 days ago |
6-20162 6 days ago |
6-20204 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-75938 2 days ago |
17-9151 17 days ago |
17-10456 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-66466 2 days ago |
2-67109 2 days ago |
2-68111 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-66311 2 days ago |
3-31155 3 days ago |
3-31201 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-62715 2 days ago |
2-70929 2 days ago |
2-73489 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-59248 2 days ago |
3-13700 3 days ago |
5-16577 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-57090 2 days ago |
2-57094 2 days ago |
3-73736 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-55959 2 days ago |
5-47882 5 days ago |
37-41104 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-48525 2 days ago |
3-46222 3 days ago |
6-81987 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-44282 2 days ago |
3-49366 3 days ago |
3-51461 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-34412 2 days ago |
2-34412 2 days ago |
9-28139 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-32391 2 days ago |
2-32391 2 days ago |
7-69759 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-20746 2 days ago |
2-26600 2 days ago |
2-26642 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-20648 2 days ago |
2-20653 2 days ago |
2-20692 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-19370 2 days ago |
2-19395 2 days ago |
7-38360 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 |
2-92 2 days ago |
2-119 2 days ago |
2-161 2 days |
| 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-86218 1 day ago |
3-51524 3 days ago |
3-51501 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-82275 1 day ago |
1-82688 1 day ago |
60-39795 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-79668 1 day ago |
2-13553 2 days ago |
2-13530 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-79667 1 day ago |
5-53994 5 days ago |
5-70658 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-79666 1 day ago |
6-85199 6 days ago |
6-85237 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-79665 1 day ago |
5-60890 5 days ago |
5-60929 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-79663 1 day ago |
5-41678 5 days ago |
5-41715 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-79662 1 day ago |
5-19887 5 days ago |
5-19927 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-79661 1 day ago |
5-12083 5 days ago |
5-12060 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-79659 1 day ago |
5-7257 5 days ago |
5-7234 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-69665 1 day ago |
2-39105 2 days ago |
2-39141 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-68580 1 day ago |
11-121 11 days ago |
76-51852 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-56379 1 day ago |
1-84993 1 day ago |
5-59396 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-46246 1 day ago |
1-46246 1 day ago |
2-39362 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-45539 1 day ago |
15-44674 15 days ago |
35-44502 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-44379 1 day ago |
6-25312 6 days ago |
6-81402 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-41980 1 day ago |
3-39005 3 days ago |
3-39049 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-40916 1 day ago |
12-45138 12 days ago |
50-41390 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-40764 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-37686 1 day ago |
3-54884 3 days ago |
18-75375 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-36891 1 day ago |
1-36891 1 day ago |
1-41082 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-36877 1 day ago |
1-36877 1 day ago |
1-37708 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-35555 1 day ago |
1-35611 1 day ago |
8-17419 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-35406 1 day ago |
1-46038 1 day ago |
1-71832 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-34857 1 day ago |
1-51597 1 day ago |
4-81579 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-72603 15 days ago |
15-72705 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-43926 4 days ago |
4-54375 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-21600 1 day ago |
3-21651 3 days ago |
3-32886 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-19138 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-17612 1 day ago |
1-17635 1 day ago |
43-75301 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-13876 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-5063 1 day ago |
1-5063 1 day ago |
4-16200 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-4941 1 day ago |
8-42328 8 days ago |
8-42368 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-84861 23 hours ago |
11-1485 11 days ago |
12-3242 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-82480 22 hours ago |
1-6007 1 day ago |
1-6045 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-79680 22 hours ago |
4-13673 4 days ago |
4-14134 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-79679 22 hours ago |
4-75679 4 days ago |
4-75657 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-79678 22 hours ago |
4-63762 4 days ago |
4-68348 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-79678 22 hours ago |
4-73771 4 days ago |
4-73755 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-79677 22 hours ago |
4-55668 4 days ago |
4-55703 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-79676 22 hours ago |
4-35778 4 days ago |
4-35815 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-79675 22 hours ago |
4-32833 4 days ago |
4-32880 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-79674 22 hours ago |
3-82930 3 days ago |
3-82923 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-77470 21 hours ago |
0-77524 21 hours ago |
17-69669 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-73767 20 hours ago |
0-73767 20 hours ago |
0-74766 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-73361 20 hours ago |
7-70164 7 days ago |
7-70205 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-72373 20 hours ago |
1-17114 1 day ago |
1-21202 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-71297 19 hours ago |
0-71672 19 hours ago |
15-15560 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-61772 17 hours ago |
2-72474 2 days ago |
13-32298 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-55253 15 hours ago |
0-73731 20 hours ago |
0-73772 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-53540 14 hours ago |
0-69716 19 hours ago |
0-69769 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-52970 14 hours ago |
0-52970 14 hours ago |
1-46557 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-52424 14 hours ago |
3-46429 3 days ago |
6-32804 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-51334 14 hours ago |
0-51590 14 hours ago |
0-51640 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-38607 10 hours ago |
13-12251 13 days ago |
17-35425 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-37584 10 hours ago |
0-47700 13 hours ago |
0-47743 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-37333 10 hours ago |
0-39976 11 hours ago |
0-39954 11 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-31224 8 hours ago |
2-6914 2 days ago |
2-6958 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-26402 7 hours ago |
1-29646 1 day ago |
1-29685 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-25829 7 hours ago |
4-24858 4 days ago |
36-16685 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-25648 7 hours ago |
0-25648 7 hours ago |
1-72482 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-24456 6 hours ago |
0-40349 11 hours ago |
0-40326 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-65924 18 hours ago |
1-9746 1 day ago |
71-68490 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-71796 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-78325 21 hours ago |
3-13013 3 days ago |
3-13065 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-79678 6 days ago |
10-17271 10 days ago |
14-16593 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-45154 12 hours ago |
3-2192 3 days ago |
7-30502 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-48138 1 day ago |
5-5616 5 days ago |
13-26684 13 days |
| 33409 |
jsm28 author:jsm28 |
feat(LinearAlgebra/AffineSpace/Ceva): Ceva's theorem |
Add Ceva's theorem. Unlike various previous attempts, I think this in appropriate generality for mathlib; it starts with a version for an arbitary (possibly infinite) affinely independent family of points (not necessarily spanning the whole space), in any affine space over any ring, and with the second point given on each line not necessarily being on the opposite face, then deduces a simpler version for a finite family, then deduces versions for a triangle, now with actual cevians (lines between a vertex and a point on the opposite side), either just multiplying weights (here the ring becomes an integral domain) or expressed with a product of divisions equal to 1 (here it becomes a field).
This doesn't include any form of the converse (with a "concurrent or parallel" conclusion, and note that you don't need affine independence for the converse), or variants of the forward direction where you're given parallel lines rather than concurrent lines, but I think those things can reasonably be done in followups.
---
[](https://gitpod.io/from-referrer/)
|
t-algebra label:t-algebra$ |
237/0 |
Mathlib.lean,Mathlib/LinearAlgebra/AffineSpace/AffineSubspace/Basic.lean,Mathlib/LinearAlgebra/AffineSpace/Ceva.lean,docs/100.yaml,docs/1000.yaml |
5 |
1 |
['github-actions'] |
nobody |
0-3307 55 minutes ago |
0-3373 55 minutes ago |
0-3351 55 minutes |