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-72557 1 month ago |
36-39846 1 month ago |
36-39820 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-31171 29 days ago |
29-32694 29 days ago |
38-77442 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-72562 28 days ago |
32-21786 1 month ago |
34-22210 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-72552 28 days ago |
34-64862 1 month ago |
34-64903 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-9945 28 days ago |
32-9915 1 month ago |
32-11007 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-72548 27 days ago |
31-62627 1 month ago |
31-65249 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-72538 27 days ago |
31-23485 1 month ago |
31-23517 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-2680 25 days ago |
55-19656 1 month ago |
55-19610 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-35603 24 days ago |
24-38621 24 days ago |
24-80006 24 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-10313 23 days ago |
23-10432 23 days ago |
28-4862 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 |
22-80771 22 days ago |
28-83973 28 days ago |
29-524 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-72554 22 days ago |
25-78885 25 days ago |
26-83483 26 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-34701 22 days ago |
22-34730 22 days ago |
22-42307 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-72553 21 days ago |
25-59868 25 days ago |
25-59856 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-3510 19 days ago |
19-17696 19 days ago |
39-64248 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-19345 18 days ago |
22-33550 22 days ago |
22-33839 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-72553 17 days ago |
20-84149 20 days ago |
20-84184 20 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-72552 17 days ago |
20-77986 20 days ago |
20-78007 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-72539 16 days ago |
21-58984 21 days ago |
25-3864 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-56682 16 days ago |
23-3125 23 days ago |
23-3165 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-15153 16 days ago |
21-10021 21 days ago |
21-10283 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-72551 15 days ago |
21-13222 21 days ago |
21-13254 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-10439 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-72534 14 days ago |
18-13634 18 days ago |
18-13666 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-62726 14 days ago |
21-70342 21 days ago |
42-66408 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-21693 14 days ago |
20-41593 20 days ago |
44-18566 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-72561 13 days ago |
17-61911 17 days ago |
17-61943 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-72551 13 days ago |
16-83978 16 days ago |
16-84012 16 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-16931 13 days ago |
13-16978 13 days ago |
18-45608 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-9883 13 days ago |
13-9886 13 days ago |
19-7138 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-72559 12 days ago |
16-7102 16 days ago |
19-56605 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-72553 12 days ago |
18-55508 18 days ago |
18-55482 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-72551 12 days ago |
16-33780 16 days ago |
16-65851 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-61203 12 days ago |
23-1847 23 days ago |
23-1877 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-60743 12 days ago |
22-65046 22 days ago |
22-65087 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-9605 12 days ago |
12-13577 12 days ago |
17-9060 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 |
11-84167 11 days ago |
11-84231 11 days ago |
20-28827 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-77094 11 days ago |
11-77318 11 days ago |
19-81175 19 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-76820 11 days ago |
11-77312 11 days ago |
21-81925 21 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-72551 11 days ago |
15-10791 15 days ago |
17-84151 17 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-72550 11 days ago |
15-16865 15 days ago |
17-57222 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-72549 11 days ago |
15-65341 15 days ago |
15-65316 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-36749 11 days ago |
12-65160 12 days ago |
12-65202 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-23036 11 days ago |
36-51099 1 month ago |
36-81988 36 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 |
10-80784 10 days ago |
10-80810 10 days ago |
23-49757 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 |
10-80519 10 days ago |
11-60974 11 days ago |
29-72874 29 days |
| 31960 |
urkud author:urkud |
feat: a lower bound for the volume of a cone on the unit sphere |
---
- [x] depends on: #31956
- [x] depends on: #31957
[](https://gitpod.io/from-referrer/)
|
t-measure-probability |
95/0 |
Mathlib/MeasureTheory/Constructions/HaarToSphere.lean |
1 |
6 |
['PatrickMassot', 'github-actions', 'mathlib4-dependent-issues-bot', 'mathlib4-merge-conflict-bot', 'urkud'] |
hrmacbeth assignee:hrmacbeth |
10-79351 10 days ago |
34-85566 1 month ago |
35-1709 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-72569 10 days ago |
13-84132 13 days ago |
14-237 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-72568 10 days ago |
23-14728 23 days ago |
23-25018 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-72565 10 days ago |
17-65679 17 days ago |
17-65684 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-72563 10 days ago |
14-32652 14 days ago |
14-32987 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-39525 10 days ago |
10-39525 10 days ago |
46-44488 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-38300 10 days ago |
10-38359 10 days ago |
32-17281 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-16290 10 days ago |
11-40474 11 days ago |
25-41393 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-72539 9 days ago |
19-84833 19 days ago |
19-84867 19 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-72538 9 days ago |
19-20560 19 days ago |
19-20638 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-72535 9 days ago |
15-22111 15 days ago |
15-22437 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-72534 9 days ago |
13-63341 13 days ago |
13-63377 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-72531 9 days ago |
12-83034 12 days ago |
12-83007 12 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-66565 9 days ago |
9-66589 9 days ago |
19-22254 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-55743 9 days ago |
18-57210 18 days ago |
19-16113 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-35458 9 days ago |
9-35484 9 days ago |
39-31597 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-72541 8 days ago |
12-17473 12 days ago |
12-24796 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-72540 8 days ago |
11-76826 11 days ago |
33-73906 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-72532 8 days ago |
12-11205 12 days ago |
12-11255 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-72529 8 days ago |
12-3036 12 days ago |
12-3009 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-45482 8 days ago |
8-45710 8 days ago |
112-23269 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-41755 8 days ago |
9-76424 9 days ago |
148-21713 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-34505 8 days ago |
8-34509 8 days ago |
8-34547 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-30243 8 days ago |
14-34759 14 days ago |
14-54507 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-15891 8 days ago |
16-17682 16 days ago |
16-17721 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-15763 8 days ago |
10-42465 10 days ago |
21-59833 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-14905 8 days ago |
41-37119 1 month ago |
45-80347 45 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-77948 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-72557 7 days ago |
11-12167 11 days ago |
11-12226 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-72554 7 days ago |
12-50079 12 days ago |
12-50119 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-72553 7 days ago |
10-83358 10 days ago |
11-67756 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-72552 7 days ago |
10-83379 10 days ago |
11-58724 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-72551 7 days ago |
10-76021 10 days ago |
11-35564 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-72549 7 days ago |
11-31071 11 days ago |
11-31114 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-72547 7 days ago |
11-10691 11 days ago |
11-10977 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-72544 7 days ago |
10-85876 10 days ago |
10-85857 10 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-72543 7 days ago |
10-78602 10 days ago |
10-78576 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-66791 7 days ago |
7-68557 7 days ago |
12-65675 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-54877 7 days ago |
7-66477 7 days ago |
7-66518 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-35940 7 days ago |
13-45565 13 days ago |
20-56159 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-78777 6 days ago |
6-82699 6 days ago |
10-58957 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-72552 6 days ago |
14-59825 14 days ago |
14-59859 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-72550 6 days ago |
10-68145 10 days ago |
12-25157 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-72549 6 days ago |
11-626 11 days ago |
11-8540 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-72546 6 days ago |
10-22681 10 days ago |
10-24442 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-72545 6 days ago |
10-30188 10 days ago |
10-30227 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-72544 6 days ago |
9-82640 9 days ago |
10-20773 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-72543 6 days ago |
10-15626 10 days ago |
10-18655 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-72542 6 days ago |
10-8605 10 days ago |
10-8641 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-72542 6 days ago |
9-85398 9 days ago |
9-85434 9 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-49060 6 days ago |
15-8640 15 days ago |
15-8719 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-30985 6 days ago |
6-30997 6 days ago |
6-31031 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-27230 6 days ago |
6-33172 6 days ago |
6-33210 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-23892 6 days ago |
6-23892 6 days ago |
12-60670 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-17301 6 days ago |
9-77326 9 days ago |
27-10067 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-9002 6 days ago |
17-58409 17 days ago |
21-51787 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-7767 6 days ago |
6-30473 6 days ago |
6-30509 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-1807 6 days ago |
33-70175 1 month ago |
33-70206 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-76293 5 days ago |
5-76293 5 days ago |
51-74802 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-72559 5 days ago |
9-65693 9 days ago |
9-65738 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-72557 5 days ago |
9-9206 9 days ago |
9-9250 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-72555 5 days ago |
8-75275 8 days ago |
8-75313 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-47927 5 days ago |
5-47951 5 days ago |
31-44581 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-34128 5 days ago |
10-42146 10 days ago |
10-42185 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 |
4-83257 4 days ago |
4-83257 4 days ago |
5-64624 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-77349 4 days ago |
5-12865 5 days ago |
7-70799 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-72552 4 days ago |
8-33891 8 days ago |
8-33939 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-72548 4 days ago |
7-76134 7 days ago |
7-76111 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-63333 4 days ago |
4-82137 4 days ago |
4-82184 4 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-58031 4 days ago |
10-45535 10 days ago |
10-67750 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-54169 4 days ago |
4-54169 4 days ago |
6-68195 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-22414 4 days ago |
10-68113 10 days ago |
10-68150 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-19496 4 days ago |
17-28389 17 days ago |
20-56567 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-72562 3 days ago |
4-4024 4 days ago |
4-6346 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-72561 3 days ago |
19-15885 19 days ago |
19-15935 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-72558 3 days ago |
7-988 7 days ago |
7-55855 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-72557 3 days ago |
14-14889 14 days ago |
14-14925 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-72554 3 days ago |
7-15804 7 days ago |
7-15844 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-72553 3 days ago |
6-73948 6 days ago |
6-73985 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-19381 1 day ago |
3-57492 3 days ago |
3-57478 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-53643 3 days ago |
4-23791 4 days ago |
4-78629 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-44138 3 days ago |
3-44138 3 days ago |
10-10609 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-33021 3 days ago |
5-42583 5 days ago |
9-55963 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-18303 3 days ago |
3-20886 3 days ago |
3-33660 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-15970 3 days ago |
3-39386 3 days ago |
3-75519 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-11279 3 days ago |
3-11279 3 days ago |
11-18074 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-9773 3 days ago |
19-19156 19 days ago |
19-19187 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-6902 3 days ago |
3-6902 3 days ago |
8-4511 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-546 3 days ago |
3-546 3 days ago |
10-59232 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-77193 2 days ago |
2-77201 2 days ago |
4-11592 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-75751 2 days ago |
2-75751 2 days ago |
3-40024 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-72525 2 days ago |
19-18018 19 days ago |
19-18001 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-72523 2 days ago |
13-73669 13 days ago |
13-73642 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-72520 2 days ago |
6-13036 6 days ago |
6-13075 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-68812 2 days ago |
17-2025 17 days ago |
17-3327 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-59340 2 days ago |
2-59983 2 days ago |
2-60982 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-59185 2 days ago |
3-24029 3 days ago |
3-24072 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-55589 2 days ago |
2-63803 2 days ago |
2-66360 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-52122 2 days ago |
3-6574 3 days ago |
5-9448 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-49964 2 days ago |
2-49968 2 days ago |
3-66607 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-48833 2 days ago |
5-40756 5 days ago |
37-33975 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-41399 2 days ago |
3-39096 3 days ago |
6-74858 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-37156 2 days ago |
3-42240 3 days ago |
3-44332 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-27286 2 days ago |
2-27286 2 days ago |
9-21010 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-25265 2 days ago |
2-25265 2 days ago |
7-62630 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-13620 2 days ago |
2-19474 2 days ago |
2-19513 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-13522 2 days ago |
2-13527 2 days ago |
2-13563 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-12244 2 days ago |
2-12269 2 days ago |
7-31231 7 days |
| 33363 |
BoltonBailey author:BoltonBailey |
feat: add `empty_eq_image` simp lemmas |
Creates new simp lemmas `image_eq_empty`, similar to existing simp lemmas, but with the LHS equality reversed, so that simp can identify these when in this form.
---
[](https://gitpod.io/from-referrer/)
|
t-data |
7/0 |
Mathlib/Data/Finset/Image.lean,Mathlib/Data/Set/Image.lean |
2 |
1 |
['github-actions'] |
nobody |
1-79366 1 day ago |
1-79393 1 day ago |
1-79432 1 day |
| 33332 |
euprunin author:euprunin |
chore: golf using `grind`. add `grind` annotations. |
---
The goal of this golfing PR is to decrease the number of times lemmas are called explicitly (replacing calls to lemmas with calls to tactics). Any decrease in compilation time is a welcome side effect, although it is not a primary objective.
Trace profiling results (shown if ≥10 ms before or after):
* `SimpleGraph.adj_of_mem_walk_support`: 33 ms before, 46 ms after
* `Finset.mem_of_max`: 13 ms before, 88 ms after
* `Set.eq_of_notMem_uIoc_of_notMem_uIoc`: 59 ms before, 44 ms after 🎉
This golfing PR is batched under the following guidelines:
* Up to ~5 changed files per PR
* Up to ~25 changed declarations per PR
* Up to ~100 changed lines per PR
---
[](https://gitpod.io/from-referrer/)
|
|
8/39 |
Mathlib/Combinatorics/SimpleGraph/Connectivity/Connected.lean,Mathlib/Combinatorics/SimpleGraph/Walks/Basic.lean,Mathlib/Data/Finset/Max.lean,Mathlib/Order/Interval/Set/UnorderedInterval.lean |
4 |
6 |
['SnirBroshi', 'euprunin', 'github-actions', 'vihdzp'] |
nobody |
1-79092 1 day ago |
3-44398 3 days ago |
3-44372 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-75149 1 day ago |
1-75562 1 day ago |
60-32666 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-72542 1 day ago |
2-6427 2 days ago |
2-6401 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-72541 1 day ago |
5-46868 5 days ago |
5-63529 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-72540 1 day ago |
6-78073 6 days ago |
6-78108 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-72539 1 day ago |
5-53764 5 days ago |
5-53800 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-72537 1 day ago |
5-34552 5 days ago |
5-34586 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-72536 1 day ago |
5-12761 5 days ago |
5-12798 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-72535 1 day ago |
5-4957 5 days ago |
5-4931 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-72533 1 day ago |
5-131 5 days ago |
5-105 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-62539 1 day ago |
2-31979 2 days ago |
2-32012 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-61454 1 day ago |
10-79395 10 days ago |
76-44723 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-49253 1 day ago |
1-77867 1 day ago |
5-52267 5 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-41012 1 day ago |
4-84890 4 days ago |
13-19555 13 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-39120 1 day ago |
1-39120 1 day ago |
2-32233 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-38413 1 day ago |
15-37548 15 days ago |
35-37374 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-37253 1 day ago |
6-18186 6 days ago |
6-74273 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-34854 1 day ago |
3-31879 3 days ago |
3-31920 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-33790 1 day ago |
12-38012 12 days ago |
50-34261 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-33638 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-30560 1 day ago |
3-47758 3 days ago |
18-68246 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-29765 1 day ago |
1-29765 1 day ago |
1-33953 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-29751 1 day ago |
1-29751 1 day ago |
1-30579 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-28429 1 day ago |
1-28485 1 day ago |
8-10291 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-28280 1 day ago |
1-38912 1 day ago |
1-64703 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-27731 1 day ago |
1-44471 1 day ago |
4-74450 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-65477 15 days ago |
15-65579 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-36800 4 days ago |
4-47249 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-14474 1 day ago |
3-14525 3 days ago |
3-25757 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-12012 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-10486 1 day ago |
1-10509 1 day ago |
43-68172 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-6750 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 |
0-84337 23 hours ago |
0-84337 23 hours ago |
4-9071 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 |
0-84215 23 hours ago |
8-35202 8 days ago |
8-35239 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-77735 21 hours ago |
10-80759 10 days ago |
11-82513 11 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-75354 20 hours ago |
0-85281 23 hours ago |
0-85316 23 hours |
| 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-72554 20 hours ago |
4-6547 4 days ago |
4-7006 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-72553 20 hours ago |
4-68553 4 days ago |
4-68528 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-72552 20 hours ago |
4-56636 4 days ago |
4-61219 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-72552 20 hours ago |
4-66645 4 days ago |
4-66626 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-72551 20 hours ago |
4-48542 4 days ago |
4-48574 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-72550 20 hours ago |
4-28652 4 days ago |
4-28686 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-72549 20 hours ago |
4-25707 4 days ago |
4-25751 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-72548 20 hours ago |
3-75804 3 days ago |
3-75794 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-70344 19 hours ago |
0-70398 19 hours ago |
17-62540 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-66641 18 hours ago |
0-66641 18 hours ago |
0-67637 18 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-66235 18 hours ago |
7-63038 7 days ago |
7-63076 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-65247 18 hours ago |
1-9988 1 day ago |
1-14073 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-64171 17 hours ago |
0-64546 17 hours ago |
15-8431 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-54646 15 hours ago |
2-65348 2 days ago |
13-25169 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-48127 13 hours ago |
0-66605 18 hours ago |
0-66643 18 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-46414 12 hours ago |
0-62590 17 hours ago |
0-62640 17 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-45844 12 hours ago |
0-45844 12 hours ago |
1-39428 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-45298 12 hours ago |
3-39303 3 days ago |
6-25675 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-44208 12 hours ago |
0-44464 12 hours ago |
0-44511 12 hours |
| 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-38028 10 hours ago |
2-81466 2 days ago |
7-23373 7 days |
| 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-31481 8 hours ago |
13-5125 13 days ago |
17-28296 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-30458 8 hours ago |
0-40574 11 hours ago |
0-40614 11 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-30207 8 hours ago |
0-32850 9 hours ago |
0-32825 9 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-24098 6 hours ago |
1-86188 1 day ago |
1-86229 1 day |
| 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-19276 5 hours ago |
1-22520 1 day ago |
1-22556 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-18703 5 hours ago |
4-17732 4 days ago |
36-9556 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-18522 5 hours ago |
0-18522 5 hours ago |
1-65353 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-17330 4 hours ago |
0-33223 9 hours ago |
0-33197 9 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-58798 16 hours ago |
1-2620 1 day ago |
71-61361 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-64670 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-71199 19 hours ago |
3-5887 3 days ago |
3-5936 3 days |