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 |
| 21860 |
vihdzp author:vihdzp |
chore(SetTheory/Ordinal/Enum): enumerator function of closed set is normal |
---
This result already exists as `enumOrd_isNormal_iff_isClosed`, however that version of the statement adds a large amount of imports due to the fact that it refers to the topological notion of closedness. This is intended as a more lightweight/convenient substitute.
I intend to eventually golf down `enumOrd_isNormal_iff_isClosed` using this, but the `Ordinal.Topology` file requires large refactoring anyways (in the form of generalizing results to other linear orders, and getting rid of `bsup`). So I'd rather get that out of the way first.
[](https://gitpod.io/from-referrer/)
|
t-set-theory |
14/0 |
Mathlib/SetTheory/Ordinal/Enum.lean |
1 |
1 |
['github-actions'] |
nobody |
48-30298 1 month ago |
48-30359 1 month ago |
48-30346 48 days |
| 21903 |
yhtq author:yhtq |
feat: add from/toList between `FreeSemigroup` and `List` with relative theorems |
Add from/toList between `FreeSemigroup` and `List` with relative theorems, as well as an incidental definition of lexicographic order on `FreeSemigroup`.
---
[](https://gitpod.io/from-referrer/)
|
large-import
new-contributor
t-algebra
label:t-algebra$ |
169/0 |
Mathlib/Algebra/Free.lean |
1 |
1 |
['github-actions'] |
nobody |
46-32877 1 month ago |
47-30393 1 month ago |
47-30438 47 days |
| 21616 |
peabrainiac author:peabrainiac |
feat(Topology): concatenating countably many paths |
Adds `Path.countableConcat`, the concatenation of a sequence of paths leading up to some point `x`.
---
- [x] depends on: #21591
- [x] depends on: #21607
This work is a prerequisite to #20248, where it is used to show that the topology of first-countable locally path-connected spaces is coinduced by all the paths in that space.
[](https://gitpod.io/from-referrer/)
|
t-topology |
186/0 |
Mathlib/Topology/Path.lean |
1 |
10 |
['YaelDillies', 'github-actions', 'mathlib4-dependent-issues-bot', 'peabrainiac'] |
YaelDillies assignee:YaelDillies |
44-1289 1 month ago |
44-1289 1 month ago |
45-21945 45 days |
| 20648 |
anthonyde author:anthonyde |
feat: formalize regular expression -> εNFA |
The file `Computability/RegularExpressionsToEpsilonNFA.lean` contains a formal definition of Thompson's method for constructing an `εNFA` from a `RegularExpression` and a proof of its correctness.
---
- [x] depends on: #20644
- [x] depends on: #20645
[](https://gitpod.io/from-referrer/)
|
t-computability
new-contributor
|
490/0 |
Mathlib.lean,Mathlib/Computability/RegularExpressionsToEpsilonNFA.lean,docs/references.bib |
3 |
2 |
['github-actions', 'mathlib4-dependent-issues-bot'] |
nobody |
43-54399 1 month ago |
43-54412 1 month ago |
43-56210 43 days |
| 22031 |
adomani author:adomani |
feat(zulip): add emoji reaction to first message |
Discussed in [Zulip](https://leanprover.zulipchat.com/#narrow/channel/144837-PR-reviews/topic/.2321995.20deprecate.20.60Complex.2Eabs.60/near/500322749).
---
[](https://gitpod.io/from-referrer/)
|
|
11/3 |
scripts/zulip_emoji_merge_delegate.py |
1 |
12 |
['adomani', 'eric-wieser', 'github-actions', 'mathlib-bors'] |
nobody |
43-27469 1 month ago |
44-29963 1 month ago |
44-30093 44 days |
| 21965 |
JovanGerb author:JovanGerb |
feat: extensible `push`(_neg) tactic - part 1 |
This is the first part of #21769, namely defining the new tactic, and only tagging the lemmas that have to be tagged to match the old behaviour.
This includes
- The `push_neg` tactic, which is a macro for `push Not`
- The `push` tactic
- The `↓pushNeg` simproc that can be used as `simp [↓pushNeg]`
- The `push` and `push_neg` tactics in `conv` mode.
- The `#push_discr_tree` command to help see what lemmas the tactic is using for a given constant.
There are two new files: `Mathlib.Tactic.Push` and `Mathlib.Tactic.Push.Attr`. The latter only introduces the `@[push]` attribute, so that it can be used by early Mathlib files without having to import `Mathlib.Tactic.Push`.
Zulip conversation: https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/I.20made.20an.20extensible.20.60push.60.20tactic.20generalizing.20.60push_neg.60/near/499492535
---
[](https://gitpod.io/from-referrer/)
|
large-import
t-meta
|
310/182 |
Mathlib.lean,Mathlib/Data/Nat/Basic.lean,Mathlib/Data/Set/Basic.lean,Mathlib/Order/Defs/LinearOrder.lean,Mathlib/Tactic.lean,Mathlib/Tactic/Push.lean,Mathlib/Tactic/Push/Attr.lean,MathlibTest/push_neg.lean,scripts/noshake.json |
9 |
7 |
['JovanGerb', 'github-actions', 'grunweg', 'leanprover-bot'] |
nobody |
42-14717 1 month ago |
42-15543 1 month ago |
44-64712 44 days |
| 21744 |
robin-carlier author:robin-carlier |
feat(AlgebraicTopology/SimplexCategory/GeneratorsRelations/NormalForms): admissible lists and simplicial insertion |
We introduce the notion of an `m`-admissible list of natural number: a list `[i₀,…,iₙ]` is said to be `m`-admissible if `iₖ ≤ m + k` for all valid index `k`. These lists are intended to uniquely represents either `P_σ` or `P_δ` morphisms in `SimplexCategoryGenRel`.
We prove basic stability of such lists under some lists operation such as the tail.
We also introduce the notion of simplicial insertion, which is intended to be the algorithm on such normal forms representing composition on the right (for `P_σ` morphisms) or on the left (for `P_δ` morphisms) by a single morphism, and we prove that this preserves admissibility.
Part of a series of PR formalising that `SimplexCategoryGenRel` is equivalent to `SimplexCategory`.
---
- [x] depends on: #21743
[](https://gitpod.io/from-referrer/)
|
t-topology
t-category-theory
|
197/0 |
Mathlib.lean,Mathlib/AlgebraicTopology/SimplexCategory/GeneratorsRelations/NormalForms.lean |
2 |
7 |
['github-actions', 'joelriou', 'mathlib4-dependent-issues-bot', 'robin-carlier'] |
nobody |
36-61564 1 month ago |
36-61564 1 month ago |
38-71973 38 days |
| 22314 |
shetzl author:shetzl |
feat: add leftmost derivations for context-free grammars |
Leftmost derivations are often easier to reason about than arbitrary derivations. This PR adds leftmost variants of Rewrites, Produces and Derives to the existing definition of context-free grammars and proves that a string of terminals can be derived iff it can be leftmost derived.
Co-authored-by: Tobias Leichtfried
---
[](https://gitpod.io/from-referrer/)
|
t-computability
new-contributor
|
383/0 |
Mathlib.lean,Mathlib/Computability/LeftmostDerivation.lean |
2 |
27 |
['github-actions', 'madvorak', 'shetzl'] |
nobody |
36-5581 1 month ago |
36-26850 1 month ago |
36-26905 36 days |
| 21869 |
Raph-DG author:Raph-DG |
feat(Order): Trimmed length of a RelSeries |
In this PR, we define the trimmed length of a relseries rs : RelSeries (· ≤ ·) to be the cardinality of the underlying function rs.toFun of rs minus 1. This models the number of `<` relations occuring in rs. We develop some basic API for this notion, with the main intended application being a proof that module length is additive.
---
[](https://gitpod.io/from-referrer/)
|
new-contributor
t-order
|
236/0 |
Mathlib.lean,Mathlib/Order/RelSeries.lean,Mathlib/Order/TrimmedLength.lean |
3 |
8 |
['Raph-DG', 'github-actions', 'jcommelin'] |
nobody |
35-8641 1 month ago |
48-17157 1 month ago |
48-17204 48 days |
| 22447 |
joelriou author:joelriou |
feat(CategoryTheory): the dual of a Guitart exact `2`-square is Guitart exact |
This shall be used in order to formalize left derivability structures (dual to right derivability structures), and to construct left derived functors.
---
[](https://gitpod.io/from-referrer/)
|
t-category-theory |
119/0 |
Mathlib.lean,Mathlib/CategoryTheory/Functor/TwoSquare.lean,Mathlib/CategoryTheory/GuitartExact/Opposite.lean,Mathlib/CategoryTheory/Opposites.lean |
4 |
1 |
['github-actions'] |
nobody |
32-75304 1 month ago |
32-75766 1 month ago |
32-75754 32 days |
| 22474 |
joelriou author:joelriou |
feat(CategoryTheory/Functor): more API for pointwise Kan extensions |
Transport pointwise Kan extensions via isomorphisms/equivalences.
---
[](https://gitpod.io/from-referrer/)
|
t-category-theory |
157/7 |
Mathlib/CategoryTheory/Functor/KanExtension/Pointwise.lean,Mathlib/CategoryTheory/Limits/HasLimits.lean,Mathlib/CategoryTheory/Limits/Opposites.lean,Mathlib/CategoryTheory/Limits/Shapes/Products.lean |
4 |
1 |
['github-actions'] |
nobody |
30-29563 30 days ago |
30-30270 30 days ago |
31-60548 31 days |
| 22539 |
joelriou author:joelriou |
feat(Algebra/Homology): construction of left resolutions |
Given a fully faithful functor `ι : C ⥤ A` to an abelian category, we introduce a structure `Abelian.LeftResolutions ι` which gives a functor `F : A ⥤ C` and a natural epimorphism `π.app X : ι.obj (F.obj X) ⟶ X` for all `X : A`. This is used in order to construct a resolution functor `LeftResolutions.chainComplexFunctor : A ⥤ ChainComplex C ℕ`.
This shall be used in order to derive the tensor product of modules and sheaves of modules.
---
[](https://gitpod.io/from-referrer/)
|
t-category-theory |
271/19 |
Mathlib.lean,Mathlib/Algebra/Homology/HomologicalComplex.lean,Mathlib/Algebra/Homology/LeftResolutions/Basic.lean,Mathlib/CategoryTheory/Limits/Shapes/Kernels.lean |
4 |
1 |
['github-actions'] |
nobody |
30-9427 30 days ago |
30-21618 30 days ago |
30-21606 30 days |
| 22043 |
YaelDillies author:YaelDillies |
chore: shortcut instance for `Neg ℤˣ` |
This lets us avoid importing `Ring` in downstream files (most of the effect is to come).
---
[](https://gitpod.io/from-referrer/)
|
t-algebra label:t-algebra$ |
19/46 |
Mathlib.lean,Mathlib/Algebra/GCDMonoid/Nat.lean,Mathlib/Algebra/Group/Int/Units.lean,Mathlib/Algebra/Order/Ring/Abs.lean,Mathlib/Algebra/Ring/Int/Units.lean,Mathlib/Algebra/Ring/NegOnePow.lean,Mathlib/Data/Fintype/Units.lean,Mathlib/Data/Int/AbsoluteValue.lean,Mathlib/Data/Int/Associated.lean,Mathlib/GroupTheory/HNNExtension.lean,Mathlib/NumberTheory/NumberField/Basic.lean,MathlibTest/Zify.lean |
12 |
13 |
['YaelDillies', 'eric-wieser', 'github-actions', 'j-loreaux', 'mathlib-bors'] |
nobody |
29-74583 29 days ago |
43-84661 1 month ago |
44-7416 44 days |
| 22576 |
Ruben-VandeVelde author:Ruben-VandeVelde |
feat: more lemmas about alternatingGroup |
---
[](https://gitpod.io/from-referrer/)
cc @AntoineChambert-Loir (whose code this is) |
t-algebra label:t-algebra$ |
55/0 |
Mathlib/GroupTheory/SpecificGroups/Alternating/Centralizer.lean |
1 |
1 |
['github-actions'] |
nobody |
29-63592 29 days ago |
29-63598 29 days ago |
29-63647 29 days |
| 22586 |
joelriou author:joelriou |
feat(CategoryTheory/Localization): the right derivability structure given by functorial resolutions |
---
[](https://gitpod.io/from-referrer/)
|
t-category-theory |
152/0 |
Mathlib.lean,Mathlib/CategoryTheory/Localization/DerivabilityStructure/OfFunctorialResolutions.lean,Mathlib/CategoryTheory/Localization/LocalizerMorphism.lean |
3 |
1 |
['github-actions'] |
nobody |
29-16061 29 days ago |
29-21528 29 days ago |
29-21516 29 days |
| 21603 |
imbrem author:imbrem |
feat(CategoryTheory/ChosenFiniteProducts): Added basic ChosenFiniteCoproducts class |
Added basic `ChosenFiniteCoproducts` class, and started porting some of the lemmas about `ChosenFiniteProducts` suitably translated
---
This, combined with #20182 modified to use chosen finite coproducts and premonoidal categories (#21488), should be enough for me to formalize strong Elgot categories, and hence a lot of categorical iteration theory for my PhD thesis.
[](https://gitpod.io/from-referrer/)
|
new-contributor
t-category-theory
|
260/2 |
Mathlib/CategoryTheory/ChosenFiniteProducts.lean |
1 |
7 |
['TwoFX', 'github-actions'] |
nobody |
28-6436 28 days ago |
28-6450 28 days ago |
51-77969 51 days |
| 21525 |
sinhp author:sinhp |
feat(CategoryTheory): Locally Cartesian Closed Categories (Prelim) |
This PR defines the basic preliminaries for defining locally cartesian closed categories (LCCCs). In particular, using the calculus of mates we define certain natural isomorphisms involving `Over.star` and `Over.pullback` which will be crucial in defining the right adjoint to the pullback functor in the development of LCCCs.
---
[](https://gitpod.io/from-referrer/)
|
large-import
t-category-theory
|
338/24 |
Mathlib/CategoryTheory/Comma/Over/Basic.lean,Mathlib/CategoryTheory/Comma/Over/Pullback.lean,Mathlib/CategoryTheory/Galois/Examples.lean |
3 |
12 |
['b-mehta', 'github-actions', 'joelriou', 'sinhp'] |
nobody |
27-84932 27 days ago |
27-84947 27 days ago |
38-8144 38 days |
| 22651 |
101damnations author:101damnations |
feat(RepresentationTheory/*): subrepresentations, quotients by subrepresentations, and representations of quotient groups |
Given a `G`-representation `(V, ρ)` and a `G`-invariant submodule `W ≤ V`, this PR defines the restriction of `ρ` to `W` as a representation, and the representation on `V / W` induced by `ρ`.
When `S` is a normal subgroup of `G` on which `ρ` is trivial, we also define the `G / S` representation induced by `ρ`.
We use this to define the `G / S` representation on `V^S`.
---
[](https://gitpod.io/from-referrer/)
|
t-algebra label:t-algebra$ |
170/11 |
Mathlib/RepresentationTheory/Basic.lean,Mathlib/RepresentationTheory/Invariants.lean,Mathlib/RepresentationTheory/Rep.lean |
3 |
1 |
['github-actions'] |
nobody |
27-79080 27 days ago |
27-79080 27 days ago |
27-79135 27 days |
| 20230 |
joelriou author:joelriou |
feat(CategoryTheory): categories of homological complexes are Grothendieck abelian |
---
- [x] depends on: #19979
- [x] depends on: #20229
- [x] depends on: #20233
[](https://gitpod.io/from-referrer/)
|
t-category-theory |
73/0 |
Mathlib.lean,Mathlib/Algebra/Homology/GrothendieckAbelian.lean |
2 |
2 |
['callesonne', 'github-actions', 'mathlib4-dependent-issues-bot'] |
nobody |
27-67798 27 days ago |
37-69520 1 month ago |
37-69506 37 days |
| 21237 |
scholzhannah author:scholzhannah |
feat: a weaker definition of compactly generated spaces |
This PR defines compactly generated spaces as a topological space where a set is open iff its intersection with every compact set is open in that compact set. There is a [definition of compactly generated spaces already in mathlib](https://leanprover-community.github.io/mathlib4_docs/Mathlib/Topology/Compactness/CompactlyGeneratedSpace.html#CompactlyGeneratedSpace) but that definition is stronger than the one presented here. They do however agree on Hausdorff spaces. See [this wikipedia page](https://en.wikipedia.org/wiki/Compactly_generated_space) for an explanation for the three different definitions of compactly generated spaces used in literature.
Co-authored-by: Floris van Doorn
---
See also [this discussion on Zulip](https://leanprover.zulipchat.com/#narrow/channel/116395-maths/topic/Compactly.20generated.20spaces) about compactly generated spaces.
- [ ] depends on: #21134
[](https://gitpod.io/from-referrer/)
|
t-topology |
326/0 |
Mathlib.lean,Mathlib/Topology/Compactness/KSpace.lean,docs/references.bib |
3 |
5 |
['github-actions', 'jzxia', 'mathlib4-dependent-issues-bot', 'scholzhannah'] |
nobody |
27-37491 27 days ago |
36-4970 1 month ago |
36-6390 36 days |
| 21624 |
sinhp author:sinhp |
feat(CategoryTheory): The (closed) monoidal structure on the product category of families of (closed) monoidal categories |
Given a family of closed monoidal categories, we show that the product of these categories
is a closed monoidal category with the pointwise monoidal structure.
---
[](https://gitpod.io/from-referrer/)
|
t-category-theory |
135/0 |
Mathlib.lean,Mathlib/CategoryTheory/Pi/Basic.lean,Mathlib/CategoryTheory/Pi/Monoidal.lean,Mathlib/CategoryTheory/Pi/MonoidalClosed.lean |
4 |
15 |
['TwoFX', 'b-mehta', 'github-actions', 'sinhp'] |
nobody |
27-26968 27 days ago |
27-26968 27 days ago |
50-14638 50 days |
| 22039 |
YaelDillies author:YaelDillies |
feat: simproc for computing `Finset.Ixx` of natural numbers |
---
- [x] depends on: #22290
- [x] depends on: #22559
[](https://gitpod.io/from-referrer/)
|
large-import
t-meta
|
315/0 |
Mathlib.lean,Mathlib/Tactic.lean,Mathlib/Tactic/Simproc/FinsetInterval.lean,Mathlib/Util/Qq.lean |
4 |
57 |
['FLDutchmann', 'Paul-Lez', 'YaelDillies', 'eric-wieser', 'github-actions', 'kim-em', 'mathlib4-dependent-issues-bot', 'urkud'] |
nobody |
27-11774 27 days ago |
29-82575 29 days ago |
42-69736 42 days |
| 22701 |
ctchou author:ctchou |
feat(Combinatorics): the Katona circle method |
This file formalizes the Katona circle method.
From PlainCombi (LeanCamCombi): https://github.com/YaelDillies/LeanCamCombi/blob/master/LeanCamCombi/PlainCombi/KatonaCircle.lean
Co-authored-by: Yaël Dillies
|
new-contributor
t-combinatorics
|
121/0 |
Mathlib.lean,Mathlib/Combinatorics/KatonaCircle.lean |
2 |
1 |
['github-actions'] |
nobody |
26-72727 26 days ago |
26-73351 26 days ago |
26-73400 26 days |
| 22684 |
vlad902 author:vlad902 |
feat(Topology): add `ContinuousOn` union API lemmas |
Add two lemmas to allow going from continuity of a union to continuity on the individual sets, and continuity on two open sets to continuity on their union. Note that there is already an existing lemma for continuity of the union of two closed sets. |
new-contributor
t-topology
|
30/3 |
Mathlib/Topology/ContinuousOn.lean |
1 |
11 |
['Paul-Lez', 'github-actions', 'grunweg', 'vlad902'] |
nobody |
25-23503 25 days ago |
27-18786 27 days ago |
27-18783 27 days |
| 8167 |
sebzim4500 author:sebzim4500 |
feat: Add new `grw` tactic for rewriting using inequalities. |
feat: Add new `grw` tactic for rewriting using inequalities.
Co-authored-by: @hrmacbeth, @digama0
---
- [x] depends on: #8796
```lean
example (x y z w : ℝ) (h₁ : x < z) (h₂ : w ≤ y + 4) (h₃ : Real.exp z < 5 * w) :
Real.exp x < 5 * (y + 4) := by
grw [h₁, ← h₂]
exact h₃
```
[](https://gitpod.io/from-referrer/)
|
new-contributor
t-meta
modifies-tactic-syntax
|
552/2 |
Mathlib.lean,Mathlib/Data/Int/ModEq.lean,Mathlib/Tactic.lean,Mathlib/Tactic/GCongr/Core.lean,Mathlib/Tactic/GRW.lean,Mathlib/Tactic/GRW/Core.lean,Mathlib/Tactic/GRW/Lemmas.lean,MathlibTest/GRW.lean,scripts/noshake.json |
9 |
53 |
['Vierkantor', 'digama0', 'eric-wieser', 'fpvandoorn', 'github-actions', 'hrmacbeth', 'kim-em', 'leanprover-community-mathlib4-bot', 'sebzim4500'] |
nobody |
25-4765 25 days ago |
25-78134 25 days ago |
56-40386 56 days |
| 22748 |
joelriou author:joelriou |
feat(CategoryTheory/Localization): the calculus of fractions that is deduced from an adjunction |
If `G ⊣ F` is an adjunction, and `F` is fully faithful, then there is a left calculus of fractions for the inverse image by `G` of the class of isomorphisms.
(The dual statement is also obtained.)
---
[](https://gitpod.io/from-referrer/)
|
t-category-theory |
67/0 |
Mathlib.lean,Mathlib/CategoryTheory/Localization/CalculusOfFractions/OfAdjunction.lean,Mathlib/CategoryTheory/MorphismProperty/Basic.lean |
3 |
1 |
['github-actions'] |
nobody |
24-73550 24 days ago |
24-75800 24 days ago |
24-75788 24 days |
| 22739 |
joelriou author:joelriou |
feat(CategoryTheory/Abelian): isomorphisms modulo a Serre class |
---
[](https://gitpod.io/from-referrer/)
|
t-category-theory |
176/0 |
Mathlib.lean,Mathlib/CategoryTheory/Abelian/SerreClass/MorphismProperty.lean,Mathlib/CategoryTheory/Limits/Shapes/Equalizers.lean,Mathlib/CategoryTheory/Limits/Shapes/Kernels.lean |
4 |
5 |
['TwoFX', 'github-actions', 'joelriou'] |
nobody |
24-70845 24 days ago |
24-70845 24 days ago |
25-693 25 days |
| 22404 |
joelriou author:joelriou |
feat(Algebra/Homology): connecting a chain complex and a cochain complex |
Given a chain complex `K`: `... ⟶ K.X 2 ⟶ K.X 1 ⟶ K.X 0`, a cochain complex `L`: `L.X 0 ⟶ L.X 1 ⟶ L.X 2 ⟶ ...`, a morphism `d₀: K.X 0 ⟶ L.X 0` satisfying the identifies `K.d 1 0 ≫ d₀ = 0` and `d₀ ≫ L.d 0 1 = 0`, we construct a cochain complex indexed by `ℤ` of the form `... ⟶ K.X 2 ⟶ K.X 1 ⟶ K.X 0 ⟶ L.X 0 ⟶ L.X 1 ⟶ L.X 2 ⟶ ...`, where `K.X 0` lies in degree `-1` and `K.X 0` in degree `0`.
---
[](https://gitpod.io/from-referrer/)
|
t-category-theory |
116/0 |
Mathlib.lean,Mathlib/Algebra/Homology/Embedding/Connect.lean |
2 |
2 |
['callesonne', 'github-actions'] |
nobody |
24-64926 24 days ago |
34-4079 1 month ago |
34-4067 34 days |
| 22628 |
scholzhannah author:scholzhannah |
feat: finiteness notions on CW complexes |
This PR defines three finiteness notions on (classical) CW complexes: finite dimensionality, finite type, and finiteness. A CW complex is finite dimensional if the indexing type of cells is empty in all but finitely many dimensions. It is of finite type if the indexing type of cells is finite in every dimension. Lastly, a CW complex is finite if it is both finite dimensional and of finite type.
The PR also provides constructors for CW complexes that are of finite type or finite and proves that a CW complex is finite iff the total number of cells is finite.
Co-authored-by: Floris van Doorn
---
[](https://gitpod.io/from-referrer/)
|
t-topology |
375/0 |
Mathlib.lean,Mathlib/Topology/CWComplex/Classical/Finite.lean |
2 |
5 |
['github-actions', 'grunweg', 'scholzhannah'] |
nobody |
24-10194 24 days ago |
28-19493 28 days ago |
28-19547 28 days |
| 22792 |
madvorak author:madvorak |
Pigeonhole-like results for Fin |
Consider the following settings:
```
import Mathlib
example (X Y : Type) [Fintype X] [Fintype Y] (f : X → Y) (hf : f.Injective) :
Fintype.card X ≤ Fintype.card Y := by
hint
example (m n : ℕ) (f : Fin m → Fin n) (hf : f.Injective) :
m ≤ n := by
hint
example (X Y : Type) [Fintype X] [Fintype Y] (f : X ↪ Y) :
Fintype.card X ≤ Fintype.card Y := by
hint
example (m n : ℕ) (f : Fin m ↪ Fin n) :
m ≤ n := by
hint
```
The 1st and 3rd `hint` succeed, but the 2nd a 4th `hint` fail.
The problem is obviously that `exact?` does not see through `Fintype.card (Fin n) = n` when searching for appropriate lemma.
It may seem to not be a problem, as it will rarely derail experienced Mathlib users — after all, experienced Leaners usually go directly for the `Finset` or `Fintype` version.
However, beginners frequently work with `Fin` and they will expect stuff like
```
theorem le_of_injective (f : Fin m → Fin n) (hf : f.Injective) : m ≤ n
```
to exist; therefore, when `hint` or `exact?` fails, it is a very unpleasant surprise.
This PR addressed this issue; not to provide useful content for advanced users, but to make Mathlib more useful for beginners.
---
[](https://gitpod.io/from-referrer/)
|
t-data |
38/0 |
Mathlib.lean,Mathlib/Data/Fin/Pigeonhole.lean |
2 |
1 |
['github-actions'] |
nobody |
24-2991 24 days ago |
24-3078 24 days ago |
24-3135 24 days |
| 20681 |
mitchell-horner author:mitchell-horner |
feat(Combinatorics/SimpleGraph): define deleteIncidenceSet |
Define the operation `G.deleteIncidenceSet x` deleting the incidence set of the vertex `x` from the edge set of the simple graph `G` and prove theorems in the finite case.
Also move `deleteEdges` and `deleteFar` definitions to a separate file `DeleteEdges.lean` (that includes `deleteIncidenceSet`) to simplify imports.
---
- [x] depends on: #20825
[](https://gitpod.io/from-referrer/)
|
large-import
new-contributor
t-combinatorics
|
228/93 |
Mathlib.lean,Mathlib/Combinatorics/SimpleGraph/Basic.lean,Mathlib/Combinatorics/SimpleGraph/DeleteEdges.lean,Mathlib/Combinatorics/SimpleGraph/Finite.lean,Mathlib/Combinatorics/SimpleGraph/Subgraph.lean,Mathlib/Combinatorics/SimpleGraph/Walk.lean |
6 |
3 |
['github-actions', 'mathlib4-dependent-issues-bot', 'mitchell-horner'] |
nobody |
23-47703 23 days ago |
23-47716 23 days ago |
47-10896 47 days |
| 21129 |
chrisflav author:chrisflav |
perf(RingTheory/Kaehler/JacobiZariski): reorder universe variables |
Naming of universe variables has an impact on universe unification. It seems to matter that the universe variables of `R`, `S` and `T` appear before the universe variables of the generators in alphabetical order.
---
[](https://gitpod.io/from-referrer/)
|
performance-hack
t-algebra
label:t-algebra$ |
18/20 |
Mathlib/RingTheory/Kaehler/JacobiZariski.lean |
1 |
37 |
['chrisflav', 'erdOne', 'github-actions', 'grunweg', 'kbuzzard', 'leanprover-bot', 'mattrobball'] |
nobody |
23-22698 23 days ago |
57-25159 1 month ago |
66-6469 66 days |
| 22620 |
ahhwuhu author:ahhwuhu |
feat: Define shifted Legendre polynomials and prove some basic properties |
Define shifted Legendre polynomials and prove that it is integer polynomial. In the same time, its evaluation on x is equal to the evaluation on 1 - x.
|
new-contributor
t-analysis
|
123/0 |
Mathlib.lean,Mathlib/Analysis/ShiftedLegendrePoly.lean |
2 |
11 |
['acmepjz', 'ahhwuhu', 'github-actions', 'riccardobrasca'] |
nobody |
23-13172 23 days ago |
28-43679 28 days ago |
28-43727 28 days |
| 22662 |
plp127 author:plp127 |
feat: Localization.Away.lift (computably) |
This PR adds `Localization.Away.lift'` and `Localization.Away.lift`, computable alternatives to `Localization.awayLift`.
---
[](https://gitpod.io/from-referrer/)
|
t-algebra label:t-algebra$ |
91/11 |
Mathlib/Algebra/Ring/Units.lean,Mathlib/RingTheory/Localization/Away/Basic.lean |
2 |
8 |
['github-actions', 'plp127', 'vihdzp'] |
nobody |
22-78017 22 days ago |
27-64413 27 days ago |
27-64459 27 days |
| 22680 |
kebekus author:kebekus |
feat: behavior of AnalyticAt.order under addition |
Deliver on one of the open TODOs and establish the behavior of `AnalyticAt.order` under addition. Add missing `fun_prop` lemma on the stability of analytic functions under `HPow.hPow`. Generalize the statement on the behavior of `AnalyticAt.order` under multiplication to scalar multiplication.
This material is used in [Project VD](https://github.com/kebekus/ProjectVD), which aims to formalize Value Distribution Theory for meromorphic functions on the complex plane.
---
[](https://gitpod.io/from-referrer/)
|
t-analysis |
178/24 |
Mathlib/Analysis/Analytic/Constructions.lean,Mathlib/Analysis/Analytic/Order.lean |
2 |
7 |
['girving', 'github-actions', 'kebekus'] |
nobody |
22-37815 22 days ago |
22-37829 22 days ago |
26-79575 26 days |
| 22890 |
BGuillemet author:BGuillemet |
feat: add versions of the Lebesgue number lemma |
Add versions of the Lebesgue number lemma, for coverings by neighborhoods rather than by open subsets (in `Topology/UniformSpace/Compact.lean`).
Add specializations of the Lebesgue number lemma for extended metric spaces (in `Topology/EMetricSpace/Basic.lean`).
---
[](https://gitpod.io/from-referrer/)
|
new-contributor
t-topology
|
87/0 |
Mathlib/Topology/EMetricSpace/Basic.lean,Mathlib/Topology/UniformSpace/Compact.lean |
2 |
1 |
['github-actions'] |
nobody |
21-53807 21 days ago |
21-53868 21 days ago |
21-53856 21 days |
| 22861 |
eric-wieser author:eric-wieser |
feat: add the trace of a bilinear form |
Following the steps at [#Is there code for X? > Laplacian @ 💬](https://leanprover.zulipchat.com/#narrow/channel/217875-Is-there-code-for-X.3F/topic/Laplacian/near/450834505).
---
[](https://gitpod.io/from-referrer/)
Some questions:
* Does this generalize to multilinear maps?
* Is there an `RCLike` generalization?
* Does this generalize to `BilinMap` instead of just `BilinForm`?
Perhaps the approach in [#mathlib4 > Stating Schrodinger's equation @ 💬](https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/Stating.20Schrodinger's.20equation/near/500409890) of using `ContinuousLinearMap.adjoint'` is better.
|
t-algebra label:t-algebra$ |
100/0 |
Mathlib.lean,Mathlib/LinearAlgebra/BilinearForm/Trace.lean |
2 |
3 |
['github-actions', 'jcommelin'] |
nobody |
21-38301 21 days ago |
22-54855 22 days ago |
22-54902 22 days |
| 22531 |
vasnesterov author:vasnesterov |
feat(Analysis): radius of convergence for `FormalMultilinearSeries.compContinuousLinearMap` |
- Add basic lemmas `compContinuousLinearMap_id` and `compContinuousLinearMap_comp`.
- Prove lower and upper bounds for the convergence radius of `f.compContinuousLinearMap`.
- Prove `radius_compNeg`: the convergence radii of `f(x)` and `f(-x)` are equal.
---
[](https://gitpod.io/from-referrer/)
|
t-analysis |
115/6 |
Mathlib/Analysis/Analytic/Basic.lean,Mathlib/Analysis/Calculus/FormalMultilinearSeries.lean,scripts/noshake.json |
3 |
1 |
['github-actions'] |
nobody |
21-28778 21 days ago |
21-28795 21 days ago |
29-68713 29 days |
| 22767 |
robin-carlier author:robin-carlier |
feat(AlgebraicTopology/SimplexCategory): the augmented simplex category |
This PR defines `AugmentedSimplexCategory` as `WithInitial SimplexCategory`. Using the API in `CategoryTheory.WithTerminal`, we check that functors out of this category (resp. out of its opposite) corresponds to cosimplicial (resp. simplicial) objects, and we link various construction about simplicial objects in terms of this category.
---
- [x] depends on : #22658
[](https://gitpod.io/from-referrer/)
|
t-category-theory |
119/0 |
Mathlib.lean,Mathlib/AlgebraicTopology/SimplexCategory/Augmented.lean |
2 |
3 |
['github-actions', 'robin-carlier'] |
nobody |
21-19925 21 days ago |
21-19946 21 days ago |
24-15633 24 days |
| 22929 |
b-mehta author:b-mehta |
feat(Order/Cover): characterise covering in Pi types |
Characterise the covering relation in products of partial orders.
Generalise this characterisation to products of preorders.
Use the characterisation to significantly simplify the characterisation of atoms in products of partial orders.
---
[](https://gitpod.io/from-referrer/)
|
t-order |
137/41 |
Mathlib/Order/Atoms.lean,Mathlib/Order/Cover.lean |
2 |
2 |
['b-mehta', 'github-actions'] |
nobody |
20-1999 20 days ago |
20-8755 20 days ago |
20-8812 20 days |
| 22933 |
chrisflav author:chrisflav |
feat(RingTheory/LocalProperties): constructor for `RingHom.OfLocalizationSpan` |
Adds a constructor for `RingHom.OfLocalizationSpan` where `P (algebraMap (Localization.Away r) (Localization.Away r ⊗[R] S))` has to be shown for a covering family. This is convenient in practice, because the base change API is the more generally applicable framework.
-- -
I think the import increase is fine, but if people are not happy with it, I can instead make a new file `Mathlib.RingTheory.LocalizationAway.BaseChange`.
[](https://gitpod.io/from-referrer/)
|
large-import
t-algebra
label:t-algebra$ |
73/3 |
Mathlib/RingTheory/LocalProperties/Basic.lean,Mathlib/RingTheory/Localization/BaseChange.lean,Mathlib/RingTheory/TensorProduct/Basic.lean |
3 |
1 |
['github-actions'] |
nobody |
20-1276 20 days ago |
20-1283 20 days ago |
20-1324 20 days |
| 22948 |
pelicanhere author:pelicanhere |
feat(Algebra/DirectSum): morphism of directsum decomposition |
Define morphism of directsum decomposition, which would be later used in defineing graded ring hom.
---
[](https://gitpod.io/from-referrer/)
|
new-contributor
t-algebra
label:t-algebra$ |
68/0 |
Mathlib/Algebra/DirectSum/Decomposition.lean |
1 |
1 |
['github-actions'] |
nobody |
19-12292 19 days ago |
19-24936 19 days ago |
19-24984 19 days |
| 22196 |
xyzw12345 author:xyzw12345 |
feat: `lie_ring` tactic and `LieReduce` command |
In this PR, we implement a new tactic that reduces expressions in a `LieRing` to a normal form and checks whether they are equal, and a command which reduces the expression and displays the normal form.
The implementation of this tactic imitates the `ring` tactic, using the `Qq` package to implement a specific reduction algorithm, following the theory of Hall sets and Lyndon words. A reference for the algorithm can be found at, for example, [here](https://personal.math.ubc.ca/~cass/research/pdf/Free.pdf).
This project is the result of a workshop at Peking University, and @siddhartha-gadgil has helped us a lot on understanding the concepts in metaprogramming.
Edit: The changes are reverted to a point where only `AtomM` is used.
Co-authored-by:
@Thmoas-Guan <2300010733@stu.pku.edu.cn>
@yhtq <2100012990@stu.pku.edu.cn>
@Blackfeather007 <2100017455@stu.pku.edu.cn>
---
[](https://gitpod.io/from-referrer/)
|
new-contributor
t-meta
|
821/0 |
Mathlib.lean,Mathlib/Tactic.lean,Mathlib/Tactic/LieAlgebra/Basic.lean,Mathlib/Tactic/LieAlgebra/LieRingNF.lean,Mathlib/Util/AtomM.lean,MathlibTest/lie_ring.lean,scripts/noshake.json |
7 |
5 |
['github-actions', 'ocfnash', 'siddhartha-gadgil', 'xyzw12345'] |
nobody |
19-5827 19 days ago |
39-48611 1 month ago |
39-48608 39 days |
| 22962 |
YaelDillies author:YaelDillies |
feat: torsion-free *monoids* |
Behind this click-baity title, there is the fact that `Monoid.IsTorsionFree` is incorrect for torsion-free monoids. Indeed, if `n ≠ 0` then `∀ a : α, n • a = 0 → a = 0` is equivalent to `∀ a b : α, n • a = n • b → a = b` only if `α` is a group. If `α` is a monoid (possibly even cancellative!), then the `∀ a : α, n • a = 0 → a = 0` condition is quite weak.
This PR introduces this new definition under the names `IsAddTorsionFree`/`IsMulTorsionFree`. Several things to note:
* It is a class, while `Monoid.IsTorsionFree` is not.
* It is outside of the `Monoid`/`AddMonoid` namespace. My thought is that people who care about torsion-free groups will prefer writing `IsAddTorsionFree G` over `Monoid.IsTorsionFree`.
* I am making a new file. This is because the existing definitions talk about order of an element, which is a much more advanced notion than the new one I am offering.
* I am not changing the existing definition in this PR. This will be done in a later PR.
From Toric
Co-authored-by: Patrick Luo
---
[](https://gitpod.io/from-referrer/)
|
toric
large-import
t-algebra
label:t-algebra$ |
83/33 |
Mathlib.lean,Mathlib/Algebra/Group/Torsion.lean,Mathlib/Algebra/Order/Group/Basic.lean,Mathlib/Algebra/Order/Ring/Basic.lean,Mathlib/NumberTheory/Padics/MahlerBasis.lean,Mathlib/RingTheory/Binomial.lean |
6 |
1 |
['github-actions'] |
nobody |
18-58995 18 days ago |
18-58995 18 days ago |
19-2207 19 days |
| 22527 |
LeoDog896 author:LeoDog896 |
feat(Finpartition): ofSetSetoid |
Allows for `Finpartition` to act on a specific set, and makes the `ofSetoid` definition the universal case of `ofSetSetoid`.
Motivation: Partitioning a domineering board into continuous components while preserving `Repr`.
---
- [x] depends on: #21551
[](https://gitpod.io/from-referrer/)
|
t-combinatorics |
33/12 |
Mathlib/Order/Partition/Finpartition.lean |
1 |
2 |
['github-actions', 'mathlib4-dependent-issues-bot'] |
nobody |
18-37496 18 days ago |
18-37511 18 days ago |
20-10564 20 days |
| 22260 |
ldct author:ldct |
feat: Add SampleableExt PNat |
Allow sampling from `PNat`
---
[](https://gitpod.io/from-referrer/)
|
new-contributor |
26/0 |
Mathlib/Testing/Plausible/Sampleable.lean,MathlibTest/slim_check.lean |
2 |
6 |
['github-actions', 'vasnesterov'] |
nobody |
18-8210 18 days ago |
18-8248 18 days ago |
30-69676 30 days |
| 20680 |
joelriou author:joelriou |
feat(CategoryTheory): weak factorization systems |
---
- [x] depends on: #20666
[](https://gitpod.io/from-referrer/)
|
t-category-theory |
68/0 |
Mathlib.lean,Mathlib/CategoryTheory/MorphismProperty/WeakFactorizationSystem.lean |
2 |
4 |
['callesonne', 'github-actions', 'joelriou', 'mathlib4-dependent-issues-bot'] |
nobody |
17-34649 17 days ago |
49-80468 1 month ago |
50-6273 50 days |
| 22833 |
adomani author:adomani |
feat(CI): add comment on merge-conflict to trigger an email |
See the [Zulip discussion](https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/CI.20Bot.20comment.20for.20merge.20conflicts).
Note that this means that everyone who subscribes to email notification for a PR, will also receive an email when the PR acquires a `merge-conflict`.
The Zulip poll [#mathlib4 > CI Bot comment for merge conflicts @ 💬](https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/CI.20Bot.20comment.20for.20merge.20conflicts/near/504862561) shows more votes in favour than against.
---
[](https://gitpod.io/from-referrer/)
|
CI |
1/0 |
.github/workflows/merge_conflicts.yml |
1 |
3 |
['adomani', 'bryangingechen', 'github-actions'] |
nobody |
17-33634 17 days ago |
17-33634 17 days ago |
17-33757 17 days |
| 21103 |
joelriou author:joelriou |
feat(AlgebraicTopology/SimplicialSet): uniqueness of the decomposition involving non-degenerate simplices |
Any simplex `x : X _⦋n⦌` of a simplicial set can be written in a unique way as `X.map f.op y` for an epimorphism `f : ⦋n⦌ ⟶ ⦋m⦌` and a non-degenerate `m`-simplex `y`.
---
- [x] depends on: #21098
[](https://gitpod.io/from-referrer/)
|
t-category-theory |
122/5 |
Mathlib/AlgebraicTopology/SimplexCategory/Basic.lean,Mathlib/AlgebraicTopology/SimplicialSet/Degenerate.lean |
2 |
3 |
['gio256', 'github-actions', 'mathlib4-dependent-issues-bot'] |
nobody |
17-21284 17 days ago |
23-22505 23 days ago |
23-22713 23 days |
| 22828 |
joelriou author:joelriou |
feat(CategoryTheory): parametrized adjunctions |
Given bifunctors `F : C₁ ⥤ C₂ ⥤ C₃` and `G : C₁ᵒᵖ ⥤ C₃ ⥤ C₂`, this PR introduces adjunctions with a parameter `F ⊣₂ G`. In the case of closed monoidal categories, we obtain `curriedTensor C ⊣₂ internalHom`.
---
[](https://gitpod.io/from-referrer/)
|
t-category-theory |
127/0 |
Mathlib.lean,Mathlib/CategoryTheory/Adjunction/Parametrized.lean,Mathlib/CategoryTheory/Closed/Monoidal.lean |
3 |
4 |
['emilyriehl', 'github-actions', 'joelriou', 'mckoen'] |
nobody |
17-21173 17 days ago |
20-67835 20 days ago |
23-5244 23 days |
| 22203 |
joelriou author:joelriou |
feat(CategoryTheory/Limits): multicoequalizers attached to linear orders |
Certain multicoequalizers are defined by coequalizing maps `V ⟨i, j⟩ ⟶ U i` and `V ⟨i, j⟩ ⟶ U j` for `i` and `j` in a type `ι`. When `ι` is linearly ordered and if the objects `V` satisfy a certain symmetry, we show that it suffices to consider the "relations" given by tuples `⟨i, j⟩` such that `i < j`.
---
[](https://gitpod.io/from-referrer/)
|
t-category-theory |
110/3 |
Mathlib/CategoryTheory/Limits/Shapes/Multiequalizer.lean |
1 |
1 |
['github-actions'] |
nobody |
17-20978 17 days ago |
39-17803 1 month ago |
39-17968 39 days |
| 22205 |
joelriou author:joelriou |
feat(CategoryTheory/Limits): preservation of multicoequalizers |
---
[](https://gitpod.io/from-referrer/)
|
t-category-theory |
88/0 |
Mathlib.lean,Mathlib/CategoryTheory/Limits/Preserves/Shapes/Multiequalizer.lean,Mathlib/CategoryTheory/Limits/Shapes/Multiequalizer.lean |
3 |
1 |
['github-actions'] |
nobody |
17-18774 17 days ago |
39-15910 1 month ago |
39-15897 39 days |
| 22794 |
vasnesterov author:vasnesterov |
feat(Tactic/NormNum): `norm_num` extension for `Irrational x^y` |
Add `norm_num` extension for `Irrational x^y`.
---
I don't disprove `Irrational x^y` when `x^y` is, in fact, rational here, because I hope in the future `norm_num` will be able to simplify such expressions to their rational representations (e.g. `(8/27)^(2/3) --> 4/9`), and then apply `Rat.not_irrational`.
[](https://gitpod.io/from-referrer/)
|
t-meta |
446/0 |
Mathlib.lean,Mathlib/Tactic.lean,Mathlib/Tactic/NormNum/Irrational.lean,MathlibTest/norm_num_ext.lean,scripts/noshake.json |
5 |
1 |
['github-actions'] |
nobody |
17-5732 17 days ago |
18-60869 18 days ago |
23-61411 23 days |
| 22844 |
grunweg author:grunweg |
chore(Topology/Constructions): tweak and move `Prod.instNeBotNhdsWithinIoi` |
This does not actually require the order dual, hence can also go into Constructions.SumProd. Follow-up to #22827.
---
[](https://gitpod.io/from-referrer/)
|
t-topology |
6/5 |
Mathlib/Topology/Constructions.lean,Mathlib/Topology/Constructions/SumProd.lean |
2 |
8 |
['github-actions', 'grunweg', 'jcommelin'] |
nobody |
17-1345 17 days ago |
17-1448 17 days ago |
22-38360 22 days |
| 17131 |
joneugster author:joneugster |
feat(Tactic/Linter): add unicode linter for unwanted characters |
Add unicode linter flagging bad unicode characters. In this first form, the linter only flags `\u00A0` (non-breaking space) and replaces it with a normal space. Non-breaking space has been chosen because they keep reappearing in mathlib and it seems to be uncontroversial to lint for these.
The whitelist/blacklist could then be refined in future PRs.
Everything flagged by this linter can be fixed fully automatically with `lake exe lint-style --fix` or by commenting `bot fix style` on the PR.
---
- tracking PR: #16215
## Zulip discussions:
- https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/Whitelist.20for.20Unicode.3F
- https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/Lean.20specific.20font
[](https://gitpod.io/from-referrer/)
|
large-import
t-linter
|
112/8 |
Mathlib.lean,Mathlib/Algebra/Lie/Semisimple/Lemmas.lean,Mathlib/Analysis/Analytic/IsolatedZeros.lean,Mathlib/CategoryTheory/Category/ReflQuiv.lean,Mathlib/LinearAlgebra/Vandermonde.lean,Mathlib/Tactic.lean,Mathlib/Tactic/Linter/TextBased.lean,Mathlib/Tactic/Linter/UnicodeLinter.lean |
8 |
1 |
['github-actions'] |
nobody |
16-80688 16 days ago |
16-81510 16 days ago |
16-81688 16 days |
| 17129 |
joneugster author:joneugster |
feat(Tactic/Linter): add unicode linter for unicode variant-selectors |
Unicode characters can be followed by one of the two "variant-selectors" `\FE0E` (text) or `\FE0F` (emoji).
These appear to the user as a single unicode character and they might copy them by accident. For example `✅️` (`\u2705\uFE0F`), `✅` (`\u2705`) and `✅︎` (`\u2705\uFE0E`) are three variants of the "same" unicode character. The one without variant-selector might display as either emoji or not, depending on the user's device and font.
Add unicode linter ensuring variant-selector only appear on specified characters and also ensuring these characters always have the correct variant selector to avoid confusions.
Everything flagged by this linter can be fixed fully automatically with `lake exe lint-style --fix` or by commenting `bot fix style` on the PR.
---
- tracking PR: #16215
## Zulip discussions:
- https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/Whitelist.20for.20Unicode.3F
- https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/Lean.20specific.20font
## Related PRs:
- leanprover/lean4#5015 added some emoji-variant selectors to Emojis used in `Lean` itself.
[](https://gitpod.io/from-referrer/)
|
large-import
t-linter
|
244/14 |
Mathlib.lean,Mathlib/GroupTheory/GroupExtension/Defs.lean,Mathlib/Tactic.lean,Mathlib/Tactic/Linter/TextBased.lean,Mathlib/Tactic/Linter/UnicodeLinter.lean,Mathlib/Tactic/Widget/Calc.lean,Mathlib/Tactic/Widget/CongrM.lean,Mathlib/Tactic/Widget/Conv.lean,Mathlib/Tactic/Widget/GCongr.lean,Mathlib/Topology/ContinuousMap/Weierstrass.lean,MathlibTest/LintStyleTextBased.lean |
11 |
3 |
['adomani', 'github-actions', 'joneugster'] |
nobody |
16-80299 16 days ago |
17-2144 17 days ago |
79-27319 79 days |
| 22256 |
plp127 author:plp127 |
feat: Metric Spaces are T6 |
This PR shows that metric spaces are T6. It also generalizes the contents of Mathlib/Topology/GDelta/UniformSpace to apply to metrizable spaces.
See this [Zulip](https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/.60IsClosed.2EisG.CE.B4.60) thread.
---
[](https://gitpod.io/from-referrer/)
|
new-contributor
t-topology
|
128/64 |
Mathlib.lean,Mathlib/MeasureTheory/Constructions/BorelSpace/Basic.lean,Mathlib/Order/Interval/Set/Disjoint.lean,Mathlib/Topology/Baire/BaireMeasurable.lean,Mathlib/Topology/GDelta/Basic.lean,Mathlib/Topology/GDelta/MetrizableSpace.lean,Mathlib/Topology/GDelta/UniformSpace.lean,Mathlib/Topology/MetricSpace/HausdorffDistance.lean,Mathlib/Topology/Metrizable/Basic.lean,Mathlib/Topology/Metrizable/Uniformity.lean,Mathlib/Topology/Separation/GDelta.lean |
11 |
28 |
['github-actions', 'j-loreaux', 'leanprover-bot', 'leanprover-community-mathlib4-bot', 'plp127', 'urkud'] |
nobody |
16-75614 16 days ago |
29-62817 29 days ago |
36-62414 36 days |
| 21234 |
sven-manthe author:sven-manthe |
feat: Descriptive.tree basic API |
add API on Descriptive.tree, in particular operations for switching between subtrees
---
The changes in other files are done to replace a lemma added in the previous PR by its proper general form. Taken from https://github.com/sven-manthe/A-formalization-of-Borel-determinacy-in-Lean
[](https://gitpod.io/from-referrer/)
|
maintainer-merge |
113/5 |
Mathlib/Data/SetLike/Basic.lean,Mathlib/Order/CompleteLattice/SetLike.lean,Mathlib/SetTheory/Descriptive/Tree.lean |
3 |
6 |
['fpvandoorn', 'github-actions', 'urkud'] |
nobody |
16-75539 16 days ago |
16-75545 16 days ago |
63-65397 63 days |
| 23021 |
101damnations author:101damnations |
feat(Data/Finsupp/Basic): add `Finsupp.(un)curry_single` and `@[simps]` to `Finsupp.finsuppProd(L)Equiv` |
---
This was raised by @Whysoserioushah regarding #21732. Adding the lemmas and `@[simps]` on their own breaks [this lemma](https://github.com/leanprover-community/mathlib4/blob/eab98761167237d45662033394ebd5ee28613aac/Mathlib/RingTheory/AlgebraTower.lean#L124) and the simplest way to fix it (and justify removing `Finsupp.finsuppProdLEquiv_symm_apply`) is to make the argument to `Finsupp.uncurry_apply_pair` (added in #22939) any term of the product type, but maybe that would be too eager a simp lemma?
[](https://gitpod.io/from-referrer/)
|
|
15/14 |
Mathlib/Data/Finsupp/Basic.lean,Mathlib/LinearAlgebra/Finsupp/Defs.lean |
2 |
1 |
['github-actions'] |
nobody |
16-73398 16 days ago |
16-76229 16 days ago |
16-76217 16 days |
| 22402 |
pechersky author:pechersky |
chore(Algebra/Order/Hom): initliaze simps for Order(Add)MonoidFoo |
and define `Order(Add)MonoidIso.symm`
bringing along a copy of lemmas from MulEquiv
clean up the simps
---
[](https://gitpod.io/from-referrer/)
|
t-algebra label:t-algebra$ |
97/1 |
Mathlib/Algebra/Order/Hom/Monoid.lean |
1 |
3 |
['github-actions', 'pechersky', 'urkud'] |
nobody |
16-50092 16 days ago |
34-6548 1 month ago |
34-6598 34 days |
| 22242 |
pimotte author:pimotte |
feat(Combinatorics/SimpleGraph): miscellaneous walk lemmas |
Adds some miscellaneous lemmas on walks, in preparation for Tutte's theorem.
---
[](https://gitpod.io/from-referrer/)
[Thread on Tutte](https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/Tutte's.20theorem)
[How these lemma's would be used can be found in this commit (marked as In walk_lemmas)](https://github.com/pimotte/TutteLean/blob/28110387bcda3e7c2f4bc137f877420eed30ea49/TutteLean/Part2.lean#L43)
Hopefully the last prequisite PR, after this I expect it all to be the actual proof of Tutte's:D |
maintainer-merge
t-combinatorics
|
127/2 |
Mathlib/Combinatorics/SimpleGraph/Connectivity/Subgraph.lean,Mathlib/Combinatorics/SimpleGraph/Connectivity/WalkDecomp.lean,Mathlib/Combinatorics/SimpleGraph/Metric.lean,Mathlib/Combinatorics/SimpleGraph/Path.lean,Mathlib/Combinatorics/SimpleGraph/Walk.lean |
5 |
17 |
['YaelDillies', 'b-mehta', 'github-actions', 'pimotte'] |
nobody |
16-35932 16 days ago |
36-11013 1 month ago |
37-33210 37 days |
| 23038 |
Parcly-Taxel author:Parcly-Taxel |
feat: IMO 2015 Q6 |
|
IMO |
293/0 |
Archive.lean,Archive/Imo/Imo2015Q6.lean,Mathlib.lean,Mathlib/Data/Int/FinsetSumBounds.lean |
4 |
1 |
['github-actions'] |
nobody |
16-35648 16 days ago |
16-41767 16 days ago |
16-41755 16 days |
| 20071 |
vasnesterov author:vasnesterov |
refactor(Data/Seq): reorganize `Seq.lean` |
The `Seq` API in the `Seq.lean` file was somewhat disorganized. This PR reorganizes the file to make it more structured.
It arranges the API in the following way:
1. Definitions and the `get?` function.
2. Constructors: `nil` and `cons`.
3. Destructors: `head`, `tail`, and `destruct`.
4. Recursion and corecursion principles.
5. Bisimulation.
6. `Terminates` API.
7. `Membership` for sequences.
8. Conversion to and from other types (`List`, `Stream`, `MLList`) and `take` operation as it is required for conversion to `List`.
9. Definitions of other operations on sequences (`append`, `map`, `join`, etc.).
10. Lemmas about conversions and operations, organized into sections by the primary operation of each lemma.
---
I tried not to change any proofs here, but had to rewrite some of them due to dependencies and to avoid importing `apply_fun`. The proofs of the following lemmas were changed:
* `head_eq_some`
* `head_eq_none`
* `cons_ne_nil`
* `cons_eq_cons`
* `ofList`
I found it useful to run `git diff --color-moved` to verify that the actual difference is just these proofs and adding sections.
- [x] depends on: #19859
[](https://gitpod.io/from-referrer/)
|
t-data |
501/441 |
Mathlib/Data/Seq/Seq.lean,scripts/noshake.json |
2 |
2 |
['github-actions', 'mathlib4-dependent-issues-bot'] |
nobody |
16-30283 16 days ago |
16-30298 16 days ago |
23-63740 23 days |
| 23045 |
YaelDillies author:YaelDillies |
chore(LinearIndependent): rename `linearCombination` lemmas |
Follow the naming convention around unnamespacing and appending `_injective` better.
From Toric
---
[](https://gitpod.io/from-referrer/)
|
toric
t-algebra
label:t-algebra$ |
20/9 |
Mathlib/LinearAlgebra/LinearIndependent/Basic.lean,Mathlib/LinearAlgebra/LinearIndependent/Defs.lean,Mathlib/RingTheory/AlgebraicIndependent/Basic.lean |
3 |
1 |
['github-actions'] |
nobody |
16-14643 16 days ago |
16-15249 16 days ago |
16-15299 16 days |
| 22464 |
adomani author:adomani |
feat(CI): declarations diff in Lean |
Rewrites the `declaration_diff` script in Lean.
You can see the effect of the new script in the testing branch #22497.
The new CI step runs in approximately 5mins, but is separate from the `build` step.
---
[](https://gitpod.io/from-referrer/)
|
CI |
151/0 |
.github/workflows/PR_summary_lean.yml,scripts/README.md,scripts/declarations_diff.lean,scripts/declarations_diff_lean_shell_glue.sh |
4 |
3 |
['bryangingechen', 'github-actions'] |
nobody |
16-13618 16 days ago |
29-84422 29 days ago |
29-84418 29 days |
| 23048 |
scholzhannah author:scholzhannah |
feat: PartialEquiv on closed sets restricts to closed map |
This PR shows that a PartialEquiv that is continuous on both source and target restricts to a homeomorphism. It then uses that to show that a PartialEquiv with closed source and target and which is continuous on both the source and target restricts to a closed map.
---
I need the latter statement to prove that one can transport a CW complex along a PartialEquiv. I had trouble finding a good spot for these statements; I hope this solution works.
[](https://gitpod.io/from-referrer/)
|
t-topology |
53/0 |
Mathlib.lean,Mathlib/Topology/PartialEquiv.lean |
2 |
1 |
['github-actions'] |
nobody |
16-8963 16 days ago |
16-8963 16 days ago |
16-9019 16 days |
| 23057 |
JovanGerb author:JovanGerb |
doc: library note about argument order in instances |
This is a follow up on #22953 and #22968.
---
[](https://gitpod.io/from-referrer/)
|
maintainer-merge |
24/2 |
Mathlib/Algebra/HierarchyDesign.lean,Mathlib/CategoryTheory/Limits/Shapes/Countable.lean,Mathlib/CategoryTheory/Limits/Shapes/FiniteLimits.lean,Mathlib/Logic/IsEmpty.lean |
4 |
2 |
['github-actions', 'grunweg'] |
nobody |
15-85405 15 days ago |
15-85406 15 days ago |
16-2054 16 days |
| 23063 |
xroblot author:xroblot |
feat(ZLattice): add `Real.finrank_eq_int_finrank_of_discrete` |
Prove the following result:
```lean
theorem Real.finrank_eq_int_finrank_of_discrete {E : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E]
[FiniteDimensional ℝ E] {s : Set E} (hs : DiscreteTopology (span ℤ s)) :
Set.finrank ℝ s = Set.finrank ℤ s
```
---
[](https://gitpod.io/from-referrer/)
|
t-algebra label:t-algebra$ |
38/0 |
Mathlib/Algebra/Module/ZLattice/Basic.lean,Mathlib/LinearAlgebra/Dimension/Finite.lean,Mathlib/Topology/Homeomorph/Lemmas.lean |
3 |
1 |
['github-actions'] |
nobody |
15-83488 15 days ago |
15-83590 15 days ago |
15-83596 15 days |
| 22582 |
vlad902 author:vlad902 |
feat: generalize theorems with linter fixes |
This is one of a series of PRs that generalizes type classes across Mathlib. These are generated using a new linter that tries to re-elaborate theorem definitions with more general type classes to see if it succeeds. It will accept the generalization if deleting the entire type class causes the theorem to fail to compile. Otherwise, the type class is not being generalized, but can simply be replaced by implicit type class synthesis (or an implicit type class in a variable block being pulled in.)
The linter currently output debug statements indicating source file positions where type classes should be generalized, and a script then makes those edits. This file contains a subset of those generalizations. The linter and the script performing re-writes is available in commit 7b436512017640c3c33aea50b2435b2ee0d995c9.
Note that this PR specifically generalizes theorems across a range of files and type classes, the common theme is that the resulting changes all cause type classes in variable declarations to go unused.
Also see discussion on Zulip here:
https://leanprover.zulipchat.com/#narrow/channel/270676-lean4/topic/Elab.20to.20generalize.20type.20classes.20for.20theorems/near/498862988 https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/Elab.20to.20generalize.20type.20classes.20for.20theorems/near/501288855 |
new-contributor |
30/50 |
Mathlib.lean,Mathlib/Algebra/Algebra/Basic.lean,Mathlib/Algebra/Group/Action/Faithful.lean,Mathlib/Algebra/GroupWithZero/Action/Faithful.lean,Mathlib/Analysis/Convex/Segment.lean,Mathlib/Analysis/Normed/Operator/Compact.lean,Mathlib/GroupTheory/Perm/Subgroup.lean,Mathlib/Topology/Algebra/ConstMulAction.lean |
8 |
10 |
['github-actions', 'urkud', 'vlad902'] |
urkud assignee:urkud |
15-29573 15 days ago |
16-74675 16 days ago |
28-53071 28 days |
| 22824 |
alreadydone author:alreadydone |
chore: generalize universes for (pre)sheaves of types |
---
[](https://gitpod.io/from-referrer/)
|
t-algebraic-geometry |
164/132 |
Mathlib/CategoryTheory/Category/Pairwise.lean,Mathlib/Topology/Sheaves/LocalPredicate.lean,Mathlib/Topology/Sheaves/PresheafOfFunctions.lean,Mathlib/Topology/Sheaves/SheafCondition/OpensLeCover.lean,Mathlib/Topology/Sheaves/SheafCondition/PairwiseIntersections.lean,Mathlib/Topology/Sheaves/SheafCondition/UniqueGluing.lean,Mathlib/Topology/Sheaves/SheafOfFunctions.lean |
7 |
6 |
['alreadydone', 'github-actions', 'joelriou', 'leanprover-bot', 'leanprover-community-mathlib4-bot'] |
nobody |
15-27826 15 days ago |
15-27826 15 days ago |
18-68330 18 days |
| 23066 |
ybenmeur author:ybenmeur |
feat: more lemmas for Tannaka duality for finite groups |
Prove more of the lemmas needed to prove Tannaka duality for finite groups.
---
This is everything that doesn't depend on `eval_of_algHom` (#23065).
[](https://gitpod.io/from-referrer/)
|
new-contributor
t-algebra
label:t-algebra$ |
50/0 |
Mathlib/RepresentationTheory/Tannaka.lean |
1 |
1 |
['github-actions'] |
nobody |
15-1990 15 days ago |
15-80932 15 days ago |
15-80983 15 days |
| 22971 |
mbkybky author:mbkybky |
refactor(FieldTheory/KrullTopology): clean up `KrullTopology.lean` |
Clean up `KrullTopology.lean` by moving some lemmas to their appropriate locations in earlier files.
Also move some lemmas from `IntermediateField/Adjoin/Defs.lean` to `IntermediateField/Basic.lean` since they are used in the proofs of new theorems in `IntermediateField/Algebraic.lean`.
---
[](https://gitpod.io/from-referrer/)
|
t-algebra label:t-algebra$ |
130/126 |
Mathlib/FieldTheory/AbelRuffini.lean,Mathlib/FieldTheory/Galois/Basic.lean,Mathlib/FieldTheory/IntermediateField/Adjoin/Defs.lean,Mathlib/FieldTheory/IntermediateField/Algebraic.lean,Mathlib/FieldTheory/IntermediateField/Basic.lean,Mathlib/FieldTheory/KrullTopology.lean,Mathlib/FieldTheory/SeparableDegree.lean |
7 |
11 |
['Thmoas-Guan', 'github-actions', 'tb65536', 'yhtq'] |
nobody |
14-82507 14 days ago |
16-10986 16 days ago |
17-22784 17 days |
| 21585 |
LeoDog896 author:LeoDog896 |
feat(Computability/CFG): lemmas about nonterminals |
helps with reasoning about CFGs with a language of the empty set
---
[](https://gitpod.io/from-referrer/)
|
maintainer-merge
t-computability
|
30/2 |
Mathlib/Computability/ContextFreeGrammar.lean |
1 |
19 |
['LeoDog896', 'YaelDillies', 'github-actions', 'madvorak'] |
nobody |
14-59332 14 days ago |
16-75511 16 days ago |
53-57692 53 days |
| 22771 |
alreadydone author:alreadydone |
feat(Homotopy/Lifting): monodromy of a covering map and lifting criterion |
Definition 2.1 in https://ncatlab.org/nlab/show/monodromy.
Also:
+ Extract `FundamentalGroupoid.map (f : C(X, Y)) : FundamentalGroupoid X ⥤ FundamentalGroupoid Y` from `fundamentalGroupoidFunctor : TopCat ⥤ CategoryTheory.Grpd`
+ Define `FundamentalGroup.map (f : C(X, Y)) (x : X) : FundamentalGroup X x →* FundamentalGroup Y (f x)` and `mapOfEq : FundamentalGroup X x →* FundamentalGroup Y y` that takes an assumption `f x = y`.
+ Redefine `FundamentalGroup` to be `End` rather than `Aut`: since `FundamentalGroupoid` is a groupoid, `End` already has a group structure.
+ Golf within the file FundamentalGroupoid/Basic.
+ Generalize `toArrow` up to `fromPath` in `FundamentalGroupoid/FundamentalGroup` from `X : TopCat` to `[TopologicalSpace X]`.
Also golfs some proofs and redefines
---
- [x] depends on: #22649
[](https://gitpod.io/from-referrer/)
|
t-topology |
193/147 |
Mathlib/AlgebraicTopology/FundamentalGroupoid/Basic.lean,Mathlib/AlgebraicTopology/FundamentalGroupoid/FundamentalGroup.lean,Mathlib/AlgebraicTopology/FundamentalGroupoid/InducedMaps.lean,Mathlib/AlgebraicTopology/FundamentalGroupoid/SimplyConnected.lean,Mathlib/CategoryTheory/Groupoid.lean,Mathlib/Topology/Covering.lean,Mathlib/Topology/Homotopy/HomotopyGroup.lean,Mathlib/Topology/Homotopy/Lifting.lean,Mathlib/Topology/Homotopy/Product.lean |
9 |
2 |
['github-actions', 'mathlib4-dependent-issues-bot'] |
nobody |
14-42374 14 days ago |
15-22490 15 days ago |
15-24391 15 days |
| 19920 |
grunweg author:grunweg |
chore(overview.yaml): mention more differential geometry items |
---
[](https://gitpod.io/from-referrer/)
|
t-differential-geometry
documentation
|
24/0 |
docs/overview.yaml |
1 |
2 |
['github-actions', 'grunweg'] |
nobody |
14-26438 14 days ago |
24-63978 24 days ago |
24-63963 24 days |
| 23122 |
YaelDillies author:YaelDillies |
feat: grading a flag |
A flag inherits the grading of its ambient order.
From MiscYD
---
[](https://gitpod.io/from-referrer/)
|
t-order |
69/0 |
Mathlib/Order/Grade.lean |
1 |
3 |
['YaelDillies', 'b-mehta', 'github-actions'] |
nobody |
14-24839 14 days ago |
14-64198 14 days ago |
14-64243 14 days |
| 22786 |
sgouezel author:sgouezel |
feat: the equiv between the tangent space of the product and the product of the tangent spaces is smooth |
---
- [x] depends on: #22804
[](https://gitpod.io/from-referrer/)
|
t-differential-geometry |
139/0 |
Mathlib/Geometry/Manifold/ContMDiffMFDeriv.lean |
1 |
2 |
['github-actions', 'mathlib4-dependent-issues-bot'] |
nobody |
14-17682 14 days ago |
14-17700 14 days ago |
14-25621 14 days |
| 23147 |
vlad902 author:vlad902 |
feat: generalize Mathlib.MeasureTheory |
This is one of a series of PRs that generalizes type classes across
Mathlib. These are generated using a new linter that tries to
re-elaborate theorem definitions with more general type classes to see
if it succeeds. It will accept the generalization if deleting the entire
type class causes the theorem to fail to compile, and the old type class
can not simply be re-synthesized with the new declaration. Otherwise, the
generalization is rejected as the type class is not being generalized,
but can simply be replaced by implicit type class synthesis or an
implicit type class in a variable block being pulled in.
The linter currently output debug statements indicating source file
positions where type classes should be generalized, and a script then
makes those edits. This file contains a subset of those generalizations.
The linter and the script performing re-writes is available in commit
5e2b7040be0f73821c1dcb360ffecd61235d87af.
Also see discussion on Zulip here:
https://leanprover.zulipchat.com/#narrow/channel/270676-lean4/topic/Elab.20to.20generalize.20type.20classes.20for.20theorems/near/498862988
https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/Elab.20to.20generalize.20type.20classes.20for.20theorems/near/501288855 |
t-measure-probability |
60/61 |
Mathlib/MeasureTheory/Constructions/BorelSpace/Basic.lean,Mathlib/MeasureTheory/Function/AEMeasurableSequence.lean,Mathlib/MeasureTheory/Function/ConditionalExpectation/AEMeasurable.lean,Mathlib/MeasureTheory/Function/L1Space/Integrable.lean,Mathlib/MeasureTheory/Function/LpSeminorm/Basic.lean,Mathlib/MeasureTheory/Function/SimpleFunc.lean,Mathlib/MeasureTheory/Function/StronglyMeasurable/AEStronglyMeasurable.lean,Mathlib/MeasureTheory/Function/StronglyMeasurable/Basic.lean,Mathlib/MeasureTheory/Group/Arithmetic.lean,Mathlib/MeasureTheory/Group/GeometryOfNumbers.lean,Mathlib/MeasureTheory/Group/Measure.lean,Mathlib/MeasureTheory/Integral/BochnerL1.lean,Mathlib/MeasureTheory/Integral/Prod.lean,Mathlib/MeasureTheory/Integral/SetToL1.lean,Mathlib/MeasureTheory/Measure/AEMeasurable.lean,Mathlib/MeasureTheory/Measure/Content.lean |
16 |
7 |
['github-actions', 'grunweg', 'leanprover-bot', 'vlad902'] |
nobody |
14-5892 14 days ago |
14-8178 14 days ago |
14-8235 14 days |
| 23153 |
vlad902 author:vlad902 |
feat: generalize Mathlib.Algebra.Order + Polynomial |
This is one of a series of PRs that generalizes type classes across
Mathlib. These are generated using a new linter that tries to
re-elaborate theorem definitions with more general type classes to see
if it succeeds. It will accept the generalization if deleting the entire
type class causes the theorem to fail to compile, and the old type class
can not simply be re-synthesized with the new declaration. Otherwise, the
generalization is rejected as the type class is not being generalized,
but can simply be replaced by implicit type class synthesis or an
implicit type class in a variable block being pulled in.
The linter currently output debug statements indicating source file
positions where type classes should be generalized, and a script then
makes those edits. This file contains a subset of those generalizations.
The linter and the script performing re-writes is available in commit
5e2b7040be0f73821c1dcb360ffecd61235d87af.
Also see discussion on Zulip here:
https://leanprover.zulipchat.com/#narrow/channel/270676-lean4/topic/Elab.20to.20generalize.20type.20classes.20for.20theorems/near/498862988
https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/Elab.20to.20generalize.20type.20classes.20for.20theorems/near/501288855 |
t-algebra label:t-algebra$ |
36/36 |
Mathlib/Algebra/Order/AddTorsor.lean,Mathlib/Algebra/Order/BigOperators/Group/List.lean,Mathlib/Algebra/Order/Floor.lean,Mathlib/Algebra/Order/Hom/Basic.lean,Mathlib/Algebra/Order/Monoid/Unbundled/Basic.lean,Mathlib/Algebra/Order/Ring/Idempotent.lean,Mathlib/Algebra/Order/Ring/Star.lean,Mathlib/Algebra/Order/Ring/Unbundled/Basic.lean,Mathlib/Algebra/Order/Sub/Unbundled/Hom.lean,Mathlib/Algebra/Order/WithTop/Untop0.lean,Mathlib/Algebra/Polynomial/Basic.lean,Mathlib/Algebra/Polynomial/Bivariate.lean,Mathlib/Algebra/Polynomial/Derivative.lean,Mathlib/Algebra/Polynomial/Div.lean,Mathlib/Algebra/Polynomial/Eval/Defs.lean,Mathlib/Algebra/Polynomial/Eval/SMul.lean,Mathlib/Algebra/Polynomial/FieldDivision.lean,Mathlib/Algebra/Polynomial/Monic.lean,Mathlib/Algebra/Polynomial/Reverse.lean,Mathlib/Algebra/Polynomial/Roots.lean,Mathlib/Algebra/Polynomial/Sequence.lean |
21 |
4 |
['github-actions', 'leanprover-bot', 'vlad902'] |
nobody |
14-1590 14 days ago |
14-5078 14 days ago |
14-5129 14 days |
| 23154 |
vlad902 author:vlad902 |
feat(Algebra/FreeMonoid): isomorphisms for the free monoid on zero/one generators |
In parallel to FreeGroup.freeGroupEmptyEquivUnit and FreeGroup.freeGroupUnitEquivInt, prove that the free monoid on zero/one generators is isomorphic to Unit/ℕ. |
t-algebra label:t-algebra$ |
18/0 |
Mathlib/Algebra/FreeMonoid/Basic.lean |
1 |
1 |
['github-actions'] |
nobody |
13-86043 13 days ago |
14-1238 14 days ago |
14-1290 14 days |
| 23018 |
gio256 author:gio256 |
feat: subscript and superscript delaborators |
We add the functions `delabSubscript` and `delabSuperscript` in the `Mathlib.Tactic` namespace. These delaborators are triggered only if the entirety of the provided expression can be subscripted (respectively, superscripted).
The delaborators are not exhaustive, in that they will not successfully delaborate every expression that is valid in a subscript or superscript. We instead aim to make them overly conservative, so that any expression which is successfully delaborated must be subscriptable (or superscriptable).
---
This PR is intended to serve as a predecessor to #20719.
[](https://gitpod.io/from-referrer/)
|
infinity-cosmos
t-meta
|
206/10 |
Mathlib/Util/Superscript.lean,MathlibTest/superscript.lean |
2 |
32 |
['eric-wieser', 'gio256', 'github-actions'] |
nobody |
13-84494 13 days ago |
14-79388 14 days ago |
14-80640 14 days |
| 22837 |
joneugster author:joneugster |
feat(Data/Set/Basic): add subset_iff and not_mem_subset_iff |
Add `Set.subset_iff` for consistent API with `Finset.subset_iff`.
Add `Set.not_mem_subset_iff` and `Finset.not_mem_subset_iff`.
---
[](https://gitpod.io/from-referrer/)
|
t-set-theory
t-data
|
9/0 |
Mathlib/Data/Finset/Defs.lean,Mathlib/Data/Set/Basic.lean |
2 |
2 |
['Ruben-VandeVelde', 'github-actions'] |
nobody |
13-70841 13 days ago |
18-26128 18 days ago |
23-2234 23 days |
| 23074 |
plp127 author:plp127 |
feat: `Fact (0 < 1)` and `Fact (0 ≤ 1)` |
Adds `Fact (0 < 1)` and `Fact (0 ≤ 1)`.
---
[](https://gitpod.io/from-referrer/)
|
t-algebra label:t-algebra$ |
7/0 |
Mathlib/Algebra/Order/ZeroLEOne.lean |
1 |
4 |
['Ruben-VandeVelde', 'github-actions', 'plp127', 'vlad902'] |
nobody |
13-36948 13 days ago |
15-69768 15 days ago |
15-69816 15 days |
| 22163 |
kebekus author:kebekus |
feat: canonical tensors in inner product spaces |
Given an `InnerProductSpace ℝ E`, this file defines two canonical tensors.
* `InnerProductSpace.canonicalContravariantTensor E : E ⊗[ℝ] E →ₗ[ℝ] ℝ`. This is the element corresponding to the inner product.
* If `E` is finite-dimensional, then `E ⊗[ℝ] E` is canonically isomorphic to its dual. Accordingly, there exists an element `InnerProductSpace.canonicalCovariantTensor E : E ⊗[ℝ] E` corresponding to `InnerProductSpace.canonicalContravariantTensor E` under this identification.
This material is used in [Project VD](https://github.com/kebekus/ProjectVD), which aims to formalize Value Distribution Theory for meromorphic functions on the complex plane. The canonical tensors are useful for defining the Laplace operator on inner product spaces in a coordinate-free way.
---
[](https://gitpod.io/from-referrer/)
|
t-analysis |
62/0 |
Mathlib.lean,Mathlib/Analysis/InnerProductSpace/CanonicalTensor.lean |
2 |
5 |
['adomani', 'github-actions', 'kebekus', 'loefflerd'] |
nobody |
13-36446 13 days ago |
41-9147 1 month ago |
41-9198 41 days |
| 23173 |
vlad902 author:vlad902 |
feat: generalize half of Mathlib.RingTheory |
This is one of a series of PRs that generalizes type classes across Mathlib. These are generated using a new linter that tries to re-elaborate theorem definitions with more general type classes to see if it succeeds. It will accept the generalization if deleting the entire type class causes the theorem to fail to compile, and the old type class can not simply be re-synthesized with the new declaration. Otherwise, the generalization is rejected as the type class is not being generalized, but can simply be replaced by implicit type class synthesis or an implicit type class in a variable block being pulled in.
The linter currently output debug statements indicating source file positions where type classes should be generalized, and a script then makes those edits. This file contains a subset of those generalizations. The linter and the script performing re-writes is available in commit 5e2b7040be0f73821c1dcb360ffecd61235d87af.
Also see discussion on Zulip here:
https://leanprover.zulipchat.com/#narrow/channel/270676-lean4/topic/Elab.20to.20generalize.20type.20classes.20for.20theorems/near/498862988 https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/Elab.20to.20generalize.20type.20classes.20for.20theorems/near/501288855 |
t-algebra label:t-algebra$ |
56/53 |
Mathlib/RingTheory/Algebraic/Basic.lean,Mathlib/RingTheory/DiscreteValuationRing/Basic.lean,Mathlib/RingTheory/FiniteType.lean,Mathlib/RingTheory/Finiteness/Basic.lean,Mathlib/RingTheory/Ideal/Basis.lean,Mathlib/RingTheory/Ideal/Maps.lean,Mathlib/RingTheory/Ideal/Nonunits.lean,Mathlib/RingTheory/Ideal/Norm/RelNorm.lean,Mathlib/RingTheory/Ideal/Operations.lean,Mathlib/RingTheory/Ideal/Span.lean,Mathlib/RingTheory/MvPolynomial/MonomialOrder.lean,Mathlib/RingTheory/MvPowerSeries/PiTopology.lean,Mathlib/RingTheory/Nilpotent/Defs.lean,Mathlib/RingTheory/Polynomial/Basic.lean,Mathlib/RingTheory/Polynomial/Content.lean,Mathlib/RingTheory/Polynomial/Cyclotomic/Eval.lean,Mathlib/RingTheory/Polynomial/Eisenstein/Basic.lean,Mathlib/RingTheory/Polynomial/Ideal.lean,Mathlib/RingTheory/PowerSeries/PiTopology.lean,Mathlib/RingTheory/PrincipalIdealDomain.lean,Mathlib/RingTheory/RingHom/Finite.lean,Mathlib/RingTheory/RootsOfUnity/Basic.lean,Mathlib/RingTheory/RootsOfUnity/PrimitiveRoots.lean,Mathlib/RingTheory/UniqueFactorizationDomain/Basic.lean,Mathlib/RingTheory/Valuation/Basic.lean,Mathlib/RingTheory/Valuation/ValuationRing.lean |
26 |
4 |
['github-actions', 'leanprover-bot', 'vlad902'] |
nobody |
13-14674 13 days ago |
13-16523 13 days ago |
13-16575 13 days |
| 23111 |
pechersky author:pechersky |
feat(Topology/MetricSpace): pseudometrics as bundled functions |
Preparation for results using families of pseudometrics
---
[](https://gitpod.io/from-referrer/)
|
maintainer-merge
t-topology
|
211/0 |
Mathlib.lean,Mathlib/Topology/MetricSpace/BundledFun.lean |
2 |
35 |
['YaelDillies', 'github-actions', 'pechersky', 'plp127'] |
nobody |
13-11557 13 days ago |
13-12719 13 days ago |
14-51672 14 days |
| 23187 |
vlad902 author:vlad902 |
feat: generalize Mathlib.NumberTheory |
This is one of a series of PRs that generalizes type classes across Mathlib. These are generated using a new linter that tries to re-elaborate theorem definitions with more general type classes to see if it succeeds. It will accept the generalization if deleting the entire type class causes the theorem to fail to compile, and the old type class can not simply be re-synthesized with the new declaration. Otherwise, the generalization is rejected as the type class is not being generalized, but can simply be replaced by implicit type class synthesis or an implicit type class in a variable block being pulled in.
The linter currently output debug statements indicating source file positions where type classes should be generalized, and a script then makes those edits. This file contains a subset of those generalizations. The linter and the script performing re-writes is available in commit 5e2b7040be0f73821c1dcb360ffecd61235d87af.
Also see discussion on Zulip here:
https://leanprover.zulipchat.com/#narrow/channel/270676-lean4/topic/Elab.20to.20generalize.20type.20classes.20for.20theorems/near/498862988 https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/Elab.20to.20generalize.20type.20classes.20for.20theorems/near/501288855
---
[](https://gitpod.io/from-referrer/)
|
t-number-theory |
34/29 |
Mathlib/NumberTheory/ArithmeticFunction.lean,Mathlib/NumberTheory/EulerProduct/Basic.lean,Mathlib/NumberTheory/FLT/Basic.lean,Mathlib/NumberTheory/LSeries/Dirichlet.lean,Mathlib/NumberTheory/LegendreSymbol/JacobiSymbol.lean,Mathlib/NumberTheory/ModularForms/SlashActions.lean,Mathlib/NumberTheory/MulChar/Basic.lean,Mathlib/NumberTheory/Ostrowski.lean,Mathlib/NumberTheory/SmoothNumbers.lean,Mathlib/NumberTheory/WellApproximable.lean,Mathlib/NumberTheory/Zsqrtd/Basic.lean,Mathlib/NumberTheory/Zsqrtd/GaussianInt.lean |
12 |
4 |
['MichaelStollBayreuth', 'github-actions', 'leanprover-bot', 'vlad902'] |
nobody |
12-82657 12 days ago |
13-6006 13 days ago |
13-6063 13 days |
| 23192 |
vlad902 author:vlad902 |
feat: generalize Mathlib.GroupTheory |
This is one of a series of PRs that generalizes type classes across Mathlib. These are generated using a new linter that tries to re-elaborate theorem definitions with more general type classes to see if it succeeds. It will accept the generalization if deleting the entire type class causes the theorem to fail to compile, and the old type class can not simply be re-synthesized with the new declaration. Otherwise, the generalization is rejected as the type class is not being generalized, but can simply be replaced by implicit type class synthesis or an implicit type class in a variable block being pulled in.
The linter currently output debug statements indicating source file positions where type classes should be generalized, and a script then makes those edits. This file contains a subset of those generalizations. The linter and the script performing re-writes is available in commit 5e2b7040be0f73821c1dcb360ffecd61235d87af.
Also see discussion on Zulip here:
https://leanprover.zulipchat.com/#narrow/channel/270676-lean4/topic/Elab.20to.20generalize.20type.20classes.20for.20theorems/near/498862988 https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/Elab.20to.20generalize.20type.20classes.20for.20theorems/near/501288855
---
[](https://gitpod.io/from-referrer/)
|
t-algebra label:t-algebra$ |
12/11 |
Mathlib/GroupTheory/Congruence/BigOperators.lean,Mathlib/GroupTheory/Coxeter/Basic.lean,Mathlib/GroupTheory/FiniteAbelian/Duality.lean,Mathlib/GroupTheory/GroupAction/Basic.lean,Mathlib/GroupTheory/GroupAction/Blocks.lean,Mathlib/GroupTheory/OrderOfElement.lean,Mathlib/GroupTheory/QuotientGroup/Defs.lean,Mathlib/GroupTheory/SpecificGroups/Cyclic.lean,Mathlib/GroupTheory/Subgroup/Saturated.lean,Mathlib/GroupTheory/Torsion.lean |
10 |
4 |
['github-actions', 'leanprover-bot', 'vlad902'] |
nobody |
12-82294 12 days ago |
13-4864 13 days ago |
13-4920 13 days |
| 23191 |
vlad902 author:vlad902 |
feat: generalize Mathlib.FieldTheory |
This is one of a series of PRs that generalizes type classes across Mathlib. These are generated using a new linter that tries to re-elaborate theorem definitions with more general type classes to see if it succeeds. It will accept the generalization if deleting the entire type class causes the theorem to fail to compile, and the old type class can not simply be re-synthesized with the new declaration. Otherwise, the generalization is rejected as the type class is not being generalized, but can simply be replaced by implicit type class synthesis or an implicit type class in a variable block being pulled in.
The linter currently output debug statements indicating source file positions where type classes should be generalized, and a script then makes those edits. This file contains a subset of those generalizations. The linter and the script performing re-writes is available in commit 5e2b7040be0f73821c1dcb360ffecd61235d87af.
Also see discussion on Zulip here:
https://leanprover.zulipchat.com/#narrow/channel/270676-lean4/topic/Elab.20to.20generalize.20type.20classes.20for.20theorems/near/498862988 https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/Elab.20to.20generalize.20type.20classes.20for.20theorems/near/501288855
---
[](https://gitpod.io/from-referrer/)
|
t-algebra label:t-algebra$ |
14/13 |
Mathlib/FieldTheory/Finite/GaloisField.lean,Mathlib/FieldTheory/Fixed.lean,Mathlib/FieldTheory/IntermediateField/Basic.lean,Mathlib/FieldTheory/IsAlgClosed/Basic.lean,Mathlib/FieldTheory/IsPerfectClosure.lean,Mathlib/FieldTheory/Minpoly/Field.lean |
6 |
6 |
['github-actions', 'leanprover-bot', 'tb65536', 'vlad902'] |
nobody |
12-81627 12 days ago |
13-5349 13 days ago |
13-5398 13 days |
| 23190 |
vlad902 author:vlad902 |
feat: generalize Mathlib.Algebra.Algebra + Module |
This is one of a series of PRs that generalizes type classes across Mathlib. These are generated using a new linter that tries to re-elaborate theorem definitions with more general type classes to see if it succeeds. It will accept the generalization if deleting the entire type class causes the theorem to fail to compile, and the old type class can not simply be re-synthesized with the new declaration. Otherwise, the generalization is rejected as the type class is not being generalized, but can simply be replaced by implicit type class synthesis or an implicit type class in a variable block being pulled in.
The linter currently output debug statements indicating source file positions where type classes should be generalized, and a script then makes those edits. This file contains a subset of those generalizations. The linter and the script performing re-writes is available in commit 5e2b7040be0f73821c1dcb360ffecd61235d87af.
Also see discussion on Zulip here:
https://leanprover.zulipchat.com/#narrow/channel/270676-lean4/topic/Elab.20to.20generalize.20type.20classes.20for.20theorems/near/498862988 https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/Elab.20to.20generalize.20type.20classes.20for.20theorems/near/501288855
---
[](https://gitpod.io/from-referrer/)
|
t-algebra label:t-algebra$ |
47/46 |
Mathlib/Algebra/Algebra/Basic.lean,Mathlib/Algebra/Algebra/NonUnitalSubalgebra.lean,Mathlib/Algebra/Algebra/Operations.lean,Mathlib/Algebra/Algebra/Quasispectrum.lean,Mathlib/Algebra/Algebra/Subalgebra/Basic.lean,Mathlib/Algebra/Algebra/Unitization.lean,Mathlib/Algebra/Module/BigOperators.lean,Mathlib/Algebra/Module/Defs.lean,Mathlib/Algebra/Module/LinearMap/Defs.lean,Mathlib/Algebra/Module/LocalizedModule/Basic.lean,Mathlib/Algebra/Module/Submodule/Pointwise.lean,Mathlib/Algebra/Module/Submodule/Range.lean,Mathlib/Algebra/Module/ZLattice/Basic.lean |
13 |
7 |
['eric-wieser', 'github-actions', 'leanprover-bot', 'vlad902'] |
nobody |
12-80396 12 days ago |
13-5363 13 days ago |
13-5411 13 days |
| 23194 |
vlad902 author:vlad902 |
feat: generalize rest of Mathlib.RingTheory |
This is one of a series of PRs that generalizes type classes across Mathlib. These are generated using a new linter that tries to re-elaborate theorem definitions with more general type classes to see if it succeeds. It will accept the generalization if deleting the entire type class causes the theorem to fail to compile, and the old type class can not simply be re-synthesized with the new declaration. Otherwise, the generalization is rejected as the type class is not being generalized, but can simply be replaced by implicit type class synthesis or an implicit type class in a variable block being pulled in.
The linter currently output debug statements indicating source file positions where type classes should be generalized, and a script then makes those edits. This file contains a subset of those generalizations. The linter and the script performing re-writes is available in commit 5e2b7040be0f73821c1dcb360ffecd61235d87af.
Also see discussion on Zulip here:
https://leanprover.zulipchat.com/#narrow/channel/270676-lean4/topic/Elab.20to.20generalize.20type.20classes.20for.20theorems/near/498862988 https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/Elab.20to.20generalize.20type.20classes.20for.20theorems/near/501288855
---
[](https://gitpod.io/from-referrer/)
|
t-algebra label:t-algebra$ |
42/42 |
Mathlib/RingTheory/Adjoin/Field.lean,Mathlib/RingTheory/Adjoin/PowerBasis.lean,Mathlib/RingTheory/Binomial.lean,Mathlib/RingTheory/Congruence/Defs.lean,Mathlib/RingTheory/DedekindDomain/Basic.lean,Mathlib/RingTheory/HahnSeries/Basic.lean,Mathlib/RingTheory/HahnSeries/Multiplication.lean,Mathlib/RingTheory/IntegralClosure/IsIntegral/Basic.lean,Mathlib/RingTheory/IntegralClosure/IsIntegralClosure/Basic.lean,Mathlib/RingTheory/IsTensorProduct.lean,Mathlib/RingTheory/Jacobson/Ring.lean,Mathlib/RingTheory/LaurentSeries.lean,Mathlib/RingTheory/LocalRing/MaximalIdeal/Basic.lean,Mathlib/RingTheory/LocalRing/RingHom/Basic.lean,Mathlib/RingTheory/Localization/Algebra.lean,Mathlib/RingTheory/Localization/Away/Basic.lean,Mathlib/RingTheory/Localization/Defs.lean,Mathlib/RingTheory/Localization/Ideal.lean,Mathlib/RingTheory/Localization/Integral.lean,Mathlib/RingTheory/OreLocalization/OreSet.lean,Mathlib/RingTheory/Regular/RegularSequence.lean,Mathlib/RingTheory/Spectrum/Prime/Topology.lean,Mathlib/RingTheory/TensorProduct/Basic.lean,Mathlib/RingTheory/TensorProduct/Finite.lean,Mathlib/RingTheory/Unramified/Basic.lean |
25 |
4 |
['github-actions', 'leanprover-bot', 'vlad902'] |
nobody |
12-76530 12 days ago |
13-4033 13 days ago |
13-4089 13 days |
| 23161 |
mans0954 author:mans0954 |
feature(Data/Finset/RangeDistance): abs_sub_lt_of_mem_finset_range |
The distance between two elements of `Finset.range N` (i.e. absolute value of the difference as integers) is less than `N`.
A lemma I found useful for something I was working on, so sharing here in case it's of wider interest.
---
[](https://gitpod.io/from-referrer/)
|
t-data |
30/0 |
Mathlib.lean,Mathlib/Algebra/Order/Group/Unbundled/Abs.lean,Mathlib/Data/Finset/RangeDistance.lean |
3 |
3 |
['fbarroero', 'github-actions'] |
nobody |
12-74046 12 days ago |
13-76163 13 days ago |
13-76160 13 days |
| 20495 |
AntoineChambert-Loir author:AntoineChambert-Loir |
feat(Combinatorics/Nullstellensatz): Alon's combinatorial Nullstellensatz |
This is a formalization of Alon's Combinatorial Nullstellensatz.
Meanwhile, prove several results
* a multivariate polynomial that vanishes on a too large product set vanishes identically
Probably, this file should belong to the `RingTheory.MvPolynomial` hierarchy.
---
- [x] depends on: #16177
- [x] depends on: #21546
[](https://gitpod.io/from-referrer/)
|
t-combinatorics |
395/1 |
Mathlib.lean,Mathlib/Algebra/MvPolynomial/Equiv.lean,Mathlib/Combinatorics/Nullstellensatz.lean,Mathlib/Data/Finsupp/Basic.lean,Mathlib/RingTheory/MvPolynomial/Homogeneous.lean,docs/references.bib |
6 |
n/a |
['AntoineChambert-Loir', 'YaelDillies', 'github-actions', 'mathlib4-dependent-issues-bot'] |
YaelDillies assignee:YaelDillies |
12-51120 12 days ago |
unknown |
unknown |
| 23213 |
mattrobball author:mattrobball |
chore(RingTheory.Derivation): add a `LinearMapClass` instance |
Often we want `simp` to call `map_zero` or `map_add` for a `Derivation`. To find the `ZeroHomClass` or `AddHomClass` instance necessary it starts to climb up the type class hierarchy including looking for a `LinearMapClass` instance which didn't exist. Consequently, sythesis would look in a lot of crazy places trying to summon ring structures on the module or on derivations itself. Here we add the missing `LinearMapClass` instance so that `simp` is more efficient.
---
[](https://gitpod.io/from-referrer/)
|
t-algebra label:t-algebra$ |
5/3 |
Mathlib/RingTheory/Derivation/Basic.lean |
1 |
6 |
['github-actions', 'leanprover-bot', 'mattrobball'] |
nobody |
12-14526 12 days ago |
12-18144 12 days ago |
12-18196 12 days |
| 23214 |
mattrobball author:mattrobball |
perf(Module.LinearMap.Defs): deprioritize projections to parents for `SemilinearMapClass` |
Trying to figure out if a given type has a `SemilinearMapClass` instance when all we want is an `AddHomClass` or a `MulActionSemiHomClass` can be quite expensive since there are multiple ways to crawl the algebraic hierarchy to generate `LinearMapClass` instances. If these fail, then they fail slowly. We deprioritize the projections from `SemilinearMapClass` to `AddHomClass` and `MulActionSemiHomClass` to make this one of the last choices.
---
[](https://gitpod.io/from-referrer/)
|
t-algebra label:t-algebra$ |
6/0 |
Mathlib/Algebra/Module/LinearMap/Defs.lean |
1 |
4 |
['github-actions', 'leanprover-bot', 'mattrobball'] |
nobody |
12-7495 12 days ago |
12-11040 12 days ago |
12-11088 12 days |
| 23220 |
mattrobball author:mattrobball |
refactor(Module.LinearMap.Defs): make `SemilinearMapClass` extend `AddMonoidHomClass` |
Currently `SemilinearMapClass` extends `AddHomClass`. As both `SemilinearMapClass.toAddHomClass` and `AddMonoidHomClass.toAddHomClass` are projections, they have the same priority. With `SemilinearMapClass` declared later, it wins causing expensive failed searches in the algebraic hierarchy before `AddMonoidHomClass.toAddHomClass` is found.
The current instance `SemilinearMapClass.toAddMonoidHomClass` has lower priority so we may need to downgrade the priority of the projection also.
---
[](https://gitpod.io/from-referrer/)
|
t-algebra label:t-algebra$ |
6/10 |
Mathlib/Algebra/Module/LinearMap/Defs.lean |
1 |
9 |
['eric-wieser', 'github-actions', 'leanprover-bot', 'mattrobball'] |
nobody |
11-56121 11 days ago |
11-72614 11 days ago |
11-72666 11 days |
| 22457 |
Komyyy author:Komyyy |
feat(Mathlib/Computability/Ackermann): Ackermann function is computable |
It had been proved that Ackermann function is not primitive recursive, but not been proved that it's computable.
I proved that.
---
[](https://gitpod.io/from-referrer/)
|
t-computability |
51/1 |
Mathlib/Computability/Ackermann.lean |
1 |
11 |
['Komyyy', 'github-actions', 'vihdzp'] |
nobody |
11-52916 11 days ago |
30-61710 30 days ago |
32-4086 32 days |
| 11563 |
YaelDillies author:YaelDillies |
feat: `∑ i ∈ s with hi : p i, f i hi` syntax for big operators |
Define new notation for `Finset.sum`/`Finset.prod`. `∑ i ∈ s with hi : p i, f i hi` now is notation for `∑ i : s.filter p, f i.1 (mem_filter.1 i.2).2`.
---
- [x] depends on: #6795
Other notations we could have are
* `∑ hi : i ∈ s, f i hi` as notation for `∑ i : s, f i.1 i.2`
* `∑ hi : i ∈ s with p i, f i hi` as notation for `∑ i : s.filter p, f i.1 (mem_filter.1 i.2).1`
* `∑ hi : i ∈ s with hpi : p i, f i hi hpi` as notation for `∑ i : s.filter p, f i.1 (mem_filter.1 i.2).1 (mem_filter.1 i.2).2`
but Eric seems mildly unhappy about them.
[](https://gitpod.io/from-referrer/)
|
t-algebra
t-meta
label:t-algebra$ |
27/18 |
Mathlib/Algebra/BigOperators/Group/Finset/Defs.lean |
1 |
27 |
['YaelDillies', 'b-mehta', 'eric-wieser', 'github-actions', 'kbuzzard', 'kmill', 'leanprover-community-mathlib4-bot'] |
nobody |
10-76209 10 days ago |
10-76226 10 days ago |
59-9521 59 days |
| 22048 |
YaelDillies author:YaelDillies |
feat: delaborator for `∑ x ∈ s with p x, f x` notation |
Co-authored-by: Kyle Miller
---
[](https://gitpod.io/from-referrer/)
|
t-meta |
142/21 |
Mathlib/Algebra/BigOperators/Group/Finset/Defs.lean,MathlibTest/BigOps.lean |
2 |
20 |
['YaelDillies', 'b-mehta', 'github-actions', 'kmill'] |
nobody |
10-74785 10 days ago |
10-74800 10 days ago |
41-32231 41 days |
| 23254 |
mariainesdff author:mariainesdff |
feat(Data/NNReal/Basic): add multiset_prod_le_pow_card |
---
[](https://gitpod.io/from-referrer/)
|
t-analysis |
17/0 |
Mathlib/Data/NNReal/Basic.lean |
1 |
2 |
['github-actions', 'mariainesdff'] |
nobody |
10-3497 10 days ago |
10-16195 10 days ago |
10-16183 10 days |
| 22966 |
alreadydone author:alreadydone |
feat(RingTheory): rank of rational function field extension |
+ `IsAlgebraic/IsIntegral R S` + `IsPushout R S R' S'` ⇒ `IsAlgebraic/IsIntegral R' S'` (for the "IsAlgebraic" version we currently need to assume `NoZeroDivisor R'` and `FaithfulSMul R R'` (i.e. `Injective (algebraMap R R')`)
+ `IsAlgebraic R S` + `IsFractionRing R R'` + `IsFractionRing S S'` ⇒ `IsPushout R S R' S'` (need to assume `FaithfulSMul R S` + `NonZeroDivisors S`)
As consequences, we have `rank (f R) (f S) = rank R S` for `f = FractionRing (Polynomial ·)` or `FractionRing (MvPolynomial _ ·)` assuming `IsAlgebraic R S` + `IsDomain S` + `FaithfulSMul R S`. (For `f = Polynomial` or `MvPolynomial _`, `NoZeroDivisors R` is enough by #23095.)
---
- [x] depends on: #23095
- [x] depends on: #23096
[](https://gitpod.io/from-referrer/)
|
t-algebra label:t-algebra$ |
270/46 |
Mathlib/RingTheory/AdjoinRoot.lean,Mathlib/RingTheory/Algebraic/Basic.lean,Mathlib/RingTheory/Algebraic/Integral.lean,Mathlib/RingTheory/IntegralClosure/IsIntegralClosure/Basic.lean,Mathlib/RingTheory/TensorProduct/Basic.lean |
5 |
9 |
['Louddy', 'alreadydone', 'github-actions', 'leanprover-bot', 'mathlib4-dependent-issues-bot'] |
nobody |
9-58736 9 days ago |
9-58750 9 days ago |
10-80447 10 days |
| 23293 |
mans0954 author:mans0954 |
refactor(Algebra/Polynomial/Roots): nthRoots as a Finset |
If `nthRoots n a` is defined as the roots of `(X : R[X]) ^ n - C a` as a multiset then surely `nthRootsFinset n a` should be the roots of `(X : R[X]) ^ n - C a` as a Finset?
---
[](https://gitpod.io/from-referrer/)
|
t-algebra label:t-algebra$ |
41/32 |
Mathlib/Algebra/Polynomial/Roots.lean,Mathlib/RingTheory/Polynomial/Cyclotomic/Basic.lean,Mathlib/RingTheory/RootsOfUnity/PrimitiveRoots.lean |
3 |
1 |
['github-actions'] |
nobody |
9-31804 9 days ago |
9-34673 9 days ago |
9-34725 9 days |
| 23298 |
joelriou author:joelriou |
feat(CategoryTheory): stability properties of morphisms properties in functor categories |
Given `W : MorphismProperty C` and a category `J`, we study the stability properties of `W.functorCategory J : MorphismProperty (J ⥤ C)`.
Under suitable assumptions, we also show that if monomorphisms in `C` are stable under transfinite compositions, then the same holds in the category `J ⥤ C`.
---
[](https://gitpod.io/from-referrer/)
|
t-category-theory |
120/0 |
Mathlib.lean,Mathlib/CategoryTheory/MorphismProperty/FunctorCategory.lean |
2 |
1 |
['github-actions'] |
nobody |
9-23977 9 days ago |
9-24826 9 days ago |
9-24814 9 days |
| 23299 |
DavidLedvinka author:DavidLedvinka |
feat(Analysis): add `mlconvolution` and `lconvolution`, Convolution with the Lebesgue integral |
Create LConvolution.lean which defines convolution using the Lebesgue integral. I plan to add more API but wanted to make sure the definition/notation are satisfactory. The main intended application of this is to prove that the pdf of a product (sum) of independent random variables is given by the convolution of their pdfs.
|
new-contributor
t-analysis
|
75/0 |
Mathlib.lean,Mathlib/Analysis/LConvolution.lean |
2 |
1 |
['github-actions'] |
nobody |
9-20131 9 days ago |
9-20131 9 days ago |
9-20180 9 days |
| 23162 |
mans0954 author:mans0954 |
feature(Analysis/SpecialFunctions/Complex/Log): exp_mul_I_injOn |
$e^{θi}$ is injective on `(-π, π]`.
---
[](https://gitpod.io/from-referrer/)
|
t-analysis |
21/0 |
Mathlib/Analysis/SpecialFunctions/Complex/Log.lean,Mathlib/Data/Complex/Basic.lean |
2 |
5 |
['fbarroero', 'github-actions', 'mans0954', 'urkud'] |
nobody |
9-19945 9 days ago |
13-74333 13 days ago |
13-74381 13 days |
| 17627 |
hrmacbeth author:hrmacbeth |
feat: universal properties of vector bundle constructions |
Characterizations for the smoothness of maps into the total spaces of (1) the direct sum of two vector bundles; (2) the pullback of a vector bundle.
This gap in the library was exposed by #17358.
---
- [x] depends on: #22804
[](https://gitpod.io/from-referrer/)
|
t-differential-geometry |
311/9 |
Mathlib/Data/Bundle.lean,Mathlib/Geometry/Manifold/VectorBundle/Basic.lean,Mathlib/Geometry/Manifold/VectorBundle/Pullback.lean,Mathlib/Topology/FiberBundle/Constructions.lean |
4 |
10 |
['github-actions', 'hrmacbeth', 'mathlib4-dependent-issues-bot', 'sgouezel'] |
nobody |
9-8051 9 days ago |
14-17637 14 days ago |
15-2100 15 days |
| 8738 |
grunweg author:grunweg |
feat: differential of a local diffeomorphism is a continuous linear equivalence |
With the `localInverse` definition, this is a straightforward argument using the chain rule.
------
- [x] depends on: #23219 (the `localInverse` API)
- [x] depends on: #8736
Unclear/open question: is there a better solution than these helper lemmas? The current approach feels unelegant.
[](https://gitpod.io/from-referrer/)
|
t-differential-geometry |
92/10 |
Mathlib/Geometry/Manifold/LocalDiffeomorph.lean,Mathlib/Topology/Algebra/Module/LinearMap.lean |
2 |
20 |
['ADedecker', 'alreadydone', 'github-actions', 'grunweg', 'mathlib4-dependent-issues-bot', 'sgouezel', 'winstonyin'] |
nobody |
9-7464 9 days ago |
9-7467 9 days ago |
44-33858 44 days |
| 20704 |
winstonyin author:winstonyin |
feat: existence of local flows of vector fields |
I formalise the existence theorem for local flows of time-dependent vector fields (`IsPicardLindelof.exists_forall_mem_closedBall_eq_hasDerivWithinAt`). Currently, if we wish to show the existence of a family of integral curves indexed by their initial conditions, it is necessary to prove the hypotheses of the vector field (Lipschitz continuity within a closed ball, etc.), centred around each of these initial conditions. I have refactored the current proof of the Picard-Lindelöf theorem to allow the initial point to be different from the point about which the hypotheses on the vector field are stated. This way, integral curves and flows are treated on equal footing.
Credits going to the original author @urkud, I have completely rewritten the file to accommodate different design choices. Many of the proof steps are nevertheless inspired by Yury's formalisation.
* The `PicardLindelof` data structure is removed entirely. It merely bundles the non-Prop arguments into itself. Although it simplifies the assumptions in subsequent proofs, it obscures the (in)dependence on the relevant constants in the type description of theorems. Since `IsPicardLindelof` is already a public facing structure, we should also simply use it internally, without any loss.
* In particular, I remove the completely superficial dependence of `FunSpace` on the `PicardLindelof` structure.
* `FunSpace` no longer specifies the initial condition. It only needs the initial point to lie in a closed ball (which will be the domain of the local flow).
* I avoid defining new non-Prop things that are only used in the proof steps, such as the current `vComp` and `tDist`. The proofs are a little longer as a result, but they are also more readable.
* I place all private (i.e. only internally used) theorems under the namespace `FunSpace`, to guide users to the proper theorems in the public API.
This is part of my effort to show that the solution to an ODE depends smoothly on the initial condition, or on parameters of the ODE. This is in turn needed for many results about manifolds, such as the fact that $C^1$ vector fields on compact manifolds always have global integral curves (or global flows).
I especially welcome any suggestions to rename lemmas or define new structures to simplify the statements.
I'm happy to write up the proof in LaTeX as well, if it's going to help reviewers.
- [x] depends on: #20696
- [x] depends on: #20731
---
[](https://gitpod.io/from-referrer/)
|
t-dynamics
t-analysis
|
561/362 |
Mathlib/Algebra/Order/Group/Abs.lean,Mathlib/Analysis/Normed/Group/Basic.lean,Mathlib/Analysis/ODE/PicardLindelof.lean,Mathlib/Geometry/Manifold/IntegralCurve/ExistUnique.lean,docs/1000.yaml,docs/undergrad.yaml |
6 |
2 |
['github-actions', 'mathlib4-dependent-issues-bot'] |
grunweg assignee:grunweg |
9-7218 9 days ago |
14-38814 14 days ago |
33-23156 33 days |
| 22069 |
Raph-DG author:Raph-DG |
feat(LinearMap): Added lemmas relating kernels of linear maps to Submodule.map |
Added the lemma ne_map_or_ne_kernel_inter_of_lt stating that if A < B as submodules, then for any linear map f, `ker f ⊓ A ≠ ker f ⊓ B ∨ Submodule.map f A ≠ Submodule.map f B`. We also prove the corollaries ker_inter_mono_of_map_eq and map_mono_of_ker_inter_eq.
Co-authored-by: Raphael Douglas Giles (raphaeldouglasgiles@gmail.com)
---
[](https://gitpod.io/from-referrer/)
|
new-contributor
t-algebra
label:t-algebra$ |
28/0 |
Mathlib/LinearAlgebra/Span/Basic.lean |
1 |
14 |
['Paul-Lez', 'Raph-DG', 'github-actions', 'j-loreaux'] |
nobody |
9-4867 9 days ago |
9-4884 9 days ago |
42-76387 42 days |
| 23280 |
mattrobball author:mattrobball |
chore(Ring.Defs): remove `Ring.toSemiring` |
The generic instance `Ring.toSemiring` is superfluous and seems to slow to down the build slightly. Since it serves no purpose, we remove it.
---
[](https://gitpod.io/from-referrer/)
|
t-algebra label:t-algebra$ |
0/7 |
Mathlib/Algebra/Ring/Defs.lean |
1 |
4 |
['github-actions', 'leanprover-bot', 'mattrobball'] |
nobody |
9-4363 9 days ago |
9-4363 9 days ago |
9-70659 9 days |
| 23065 |
ybenmeur author:ybenmeur |
feat: lemma `eval_of_algHom` |
Let `k` be an integral domain and `G` an arbitrary finite set.
Then any algebra morphism `φ : (G → k) →ₐ[k] k` is an evaluation map.
---
I don't know where to put this lemma. Needed for #22176.
Output of `#find_home`:
`[Mathlib.LinearAlgebra.Matrix.ToLin, Mathlib.Algebra.Quaternion, Mathlib.Algebra.Azumaya.Matrix, Mathlib.LinearAlgebra.Dimension.Free, Mathlib.Algebra.Module.FinitePresentation, Mathlib.SetTheory.Cardinal.Free, Mathlib.RingTheory.MvPolynomial.Basic, Mathlib.RingTheory.Polynomial.Basic]`.
[](https://gitpod.io/from-referrer/)
|
new-contributor
t-algebra
label:t-algebra$ |
24/0 |
Mathlib/RepresentationTheory/Tannaka.lean |
1 |
1 |
['github-actions'] |
nobody |
9-1510 9 days ago |
9-1510 9 days ago |
15-81329 15 days |
| 22777 |
xroblot author:xroblot |
feat(NumberField/CanonicalEmbedding/NormLeOne): compute the volume of `NormLeOne` |
We compute the volume of `normLeOne K`.
This PR is part of the proof of the Analytic Class Number Formula.
---
- [x] depends on: #22756
- [x] depends on: #22115
[](https://gitpod.io/from-referrer/)
|
t-number-theory |
198/4 |
Mathlib/Analysis/SpecialFunctions/ImproperIntegrals.lean,Mathlib/Data/ENNReal/Real.lean,Mathlib/MeasureTheory/Constructions/Pi.lean,Mathlib/NumberTheory/NumberField/CanonicalEmbedding/Basic.lean,Mathlib/NumberTheory/NumberField/CanonicalEmbedding/FundamentalCone.lean,Mathlib/NumberTheory/NumberField/CanonicalEmbedding/NormLeOne.lean |
6 |
2 |
['github-actions', 'mathlib4-dependent-issues-bot'] |
nobody |
8-84859 8 days ago |
8-84861 8 days ago |
9-684 9 days |
| 22882 |
xroblot author:xroblot |
feat(NumberField/Units): add `regOfFamily` and refactor `regulator` |
This is a refactor of `NumberField.regulator`.
We introduce `regOfFamily` which is the regulator of a family of units indexed by `Fin (Units.rank K)`. It is equal to `0` if the family is not `isMaxRank`. This a `Prop` that says that the image of the family in the `logSpace K` is linearly independent and thus generates a full lattice. All the results about computing the `regulator` by some matrix determinant computation are now proved more generally for `regOfFamily`.
The `regulator` of a number field is still defined as the covolume of the `unitLattice` and we prove that is is also equal to `regOfFamily` of the system of fundamental units `fundSystem K`. Together with the results about computing `regOfFamily`, we recover that way the results about computing the regulator.
---
- [x] depends on: #22868
[](https://gitpod.io/from-referrer/)
|
t-number-theory |
162/58 |
Mathlib/LinearAlgebra/Matrix/Determinant/Basic.lean,Mathlib/NumberTheory/NumberField/CanonicalEmbedding/NormLeOne.lean,Mathlib/NumberTheory/NumberField/Units/Regulator.lean |
3 |
2 |
['github-actions', 'mathlib4-dependent-issues-bot'] |
nobody |
8-80693 8 days ago |
11-665 11 days ago |
17-24444 17 days |
| 23205 |
xroblot author:xroblot |
feat(QuotientGroup): surjectivity and kernel of `QuotientGroup.map` |
Prove formulas for the kernel of `QuotientGroup.lift` and `QuotientGroup.map` and that these maps are surjective if the corresponding functions are surjective.
---
- [x] depends on: #23269
[](https://gitpod.io/from-referrer/)
|
t-algebra label:t-algebra$ |
26/0 |
Mathlib/GroupTheory/QuotientGroup/Defs.lean |
1 |
12 |
['eric-wieser', 'github-actions', 'mathlib4-dependent-issues-bot', 'xroblot'] |
nobody |
8-31224 8 days ago |
8-68857 8 days ago |
11-70516 11 days |
| 23331 |
kebekus author:kebekus |
feat: define the divisor of an analytic function |
Define the divisor of an analytic function in one variable, in complete analogy with the definition that exists for meromorphic functions.
This material is used in [Project VD](https://github.com/kebekus/ProjectVD), which aims to formalize Value Distribution Theory for meromorphic functions on the complex plane.
---
[](https://gitpod.io/from-referrer/)
|
t-analysis |
157/20 |
Mathlib.lean,Mathlib/Analysis/Analytic/Constructions.lean,Mathlib/Analysis/Analytic/Divisor.lean,Mathlib/Analysis/Analytic/Order.lean |
4 |
1 |
['github-actions'] |
nobody |
8-29807 8 days ago |
8-29815 8 days ago |
8-29961 8 days |
| 21088 |
erdOne author:erdOne |
feat(RingTheory): `dim R + 1 ≤ dim R[X]` |
We add the following results
- `ringKrullDim_quotient_succ_le_of_nonZeroDivisor`: If `r` is not a zero divisor, then
`dim R/r + 1 ≤ dim R`.
- `ringKrullDim_succ_le_ringKrullDim_polynomial`: `dim R + 1 ≤ dim R[X]`.
- `ringKrullDim_add_enatCard_le_ringKrullDim_mvPolynomial`: `dim R + #σ ≤ dim R[σ]`.
---
[](https://gitpod.io/from-referrer/)
|
t-algebra label:t-algebra$ |
218/12 |
Mathlib.lean,Mathlib/Algebra/MvPolynomial/Rename.lean,Mathlib/Algebra/Order/Monoid/WithTop.lean,Mathlib/Algebra/Polynomial/AlgebraMap.lean,Mathlib/Algebra/Polynomial/RingDivision.lean,Mathlib/Order/KrullDimension.lean,Mathlib/Order/WithBot.lean,Mathlib/RingTheory/KrullDimension/NonZeroDivisors.lean,Mathlib/RingTheory/MvPowerSeries/NoZeroDivisors.lean |
9 |
10 |
['erdOne', 'eric-wieser', 'github-actions', 'riccardobrasca'] |
nobody |
8-15133 8 days ago |
8-15133 8 days ago |
26-82334 26 days |
| 21522 |
riccardobrasca author:riccardobrasca |
feat: add Mathlib.RingTheory.DedekindDomain.Instances |
We add a new file `Mathlib.RingTheory.DedekindDomain.Instances` containing various instances that are useful to work with the localization a prime of an extension of Dedekind domains. As a practical example we golf a tedious proof in `Mathlib.RingTheory.Ideal/Norm.RelNorm`
---
[](https://gitpod.io/from-referrer/)
|
large-import
t-algebra
label:t-algebra$ |
234/42 |
Mathlib.lean,Mathlib/RingTheory/DedekindDomain/Instances.lean,Mathlib/RingTheory/DedekindDomain/IntegralClosure.lean,Mathlib/RingTheory/Ideal/Norm/RelNorm.lean,Mathlib/RingTheory/Localization/AtPrime.lean,Mathlib/RingTheory/Localization/Basic.lean,Mathlib/RingTheory/Localization/FractionRing.lean,Mathlib/RingTheory/Localization/LocalizationLocalization.lean,Mathlib/RingTheory/RingHom/Finite.lean |
9 |
2 |
['github-actions', 'riccardobrasca'] |
nobody |
7-79951 7 days ago |
7-82873 7 days ago |
50-17865 50 days |
| 22488 |
smmercuri author:smmercuri |
fix: lower priority for `UniformSpace.Completion.instSMul` |
Following the introduction of the `WithVal` type synonym in #22055 the following instance takes a long time to synthesise in FLT, and times out in the default heartbeats
```lean
import Mathlib
namespace IsDedekindDomain.HeightOneSpectrum
variable (A K : Type*) [CommRing A] [Field K] [Algebra A K] [IsFractionRing A K]
[IsDedekindDomain A] (v : HeightOneSpectrum A)
#synth SMul (v.adicCompletionIntegers K) (v.adicCompletion K)
```
The issue is that `UniformSpace.Completion.instSMul (v.adicCompletionIntegers K) (v.adicCompletion K)` now fires during the start of instance search (because we now have `UniformSpace (WithVal (v.valuation K))` whereas previously this would be `UniformSpace K`, which was not automatic), and this takes a long time to fail (leading to ~1400 entries in the trace). The first few lines of the new trace is
```lean
[Meta.synthInstance] [5.512418] ✅️ SMul (↥(adicCompletionIntegers K v)) (adicCompletion K v) ▼
[] [0.000118] new goal SMul (↥(adicCompletionIntegers K v)) (adicCompletion K v) ▶
[] [0.000537] ✅️ apply UniformSpace.Completion.instSMul to SMul (↥(adicCompletionIntegers K v)) (adicCompletion K v) ▶
[] [0.004411] ✅️ apply @WithVal.instSMul to SMul (↥(adicCompletionIntegers K v)) (WithVal (valuation K v)) ▶
[] [0.000765] ❌️ apply @GradedMonoid.GradeZero.smul to SMul (↥(adicCompletionIntegers K v)) K ▶
[] [0.000378] ✅️ apply @Algebra.toSMul to SMul (↥(adicCompletionIntegers K v)) K ▶
...
[] 1339 more entries... ▶
```
Lowering the priority of `UniformSpace.Completion.instSMul` fixes this particular issue, leading to a trace that matches that seen prior to the introduction of `WithVal`:
```lean
[Meta.synthInstance] [0.016405] ✅️ SMul (↥(adicCompletionIntegers K v)) (adicCompletion K v) ▼
[] [0.000119] new goal SMul (↥(adicCompletionIntegers K v)) (adicCompletion K v) ▶
[] [0.000491] ❌️ apply @GradedMonoid.GradeZero.smul to SMul (↥(adicCompletionIntegers K v)) (adicCompletion K v) ▶
[] [0.000403] ✅️ apply @Algebra.toSMul to SMul (↥(adicCompletionIntegers K v)) (adicCompletion K v) ▶
[] [0.000134] ❌️ apply inst✝⁴ to Algebra (↥(adicCompletionIntegers K v)) (adicCompletion K v) ▶
[] [0.000093] ❌️ apply inst✝⁵ to Algebra (↥(adicCompletionIntegers K v)) (adicCompletion K v) ▶
[] [0.000077] ❌️ apply inst✝⁷ to Algebra (↥(adicCompletionIntegers K v)) (adicCompletion K v) ▶
[] [0.000082] ❌️ apply inst✝⁹ to Algebra (↥(adicCompletionIntegers K v)) (adicCompletion K v) ▶
[] [0.000075] ❌️ apply inst✝¹² to Algebra (↥(adicCompletionIntegers K v)) (adicCompletion K v) ▶
[] [0.000220] ❌️ apply Algebra.id to Algebra (↥(adicCompletionIntegers K v)) (adicCompletion K v) ▶
[] [0.001015] ✅️ apply @ValuationSubring.instAlgebraSubtypeMem to Algebra (↥(adicCompletionIntegers K v))
(adicCompletion K v) ▶
[resume] [0.000038] propagating Algebra (↥(adicCompletionIntegers K v))
(adicCompletion K
v) to subgoal Algebra (↥(adicCompletionIntegers K v))
(adicCompletion K v) of SMul (↥(adicCompletionIntegers K v)) (adicCompletion K v) ▶
[check] [0.013358] ✅️ Algebra.toSMul
[] result Algebra.toSMul
```
---
[](https://gitpod.io/from-referrer/)
|
FLT
t-topology
|
1/1 |
Mathlib/Topology/Algebra/UniformMulAction.lean |
1 |
7 |
['github-actions', 'leanprover-bot', 'smmercuri', 'urkud'] |
nobody |
7-74640 7 days ago |
31-27220 1 month ago |
31-27267 31 days |
| 22884 |
tannerduve author:tannerduve |
feat(Computability/TuringDegrees): define oracle computability and Turing degrees |
### Description
Define a model of **oracle computability**, introducing Turing reducibility (`≤ᵀ`), Turing equivalence (`≡ᵀ`), and Turing degrees as the quotient under Turing equivalence.
- `RecursiveIn O f`: A function `f` is recursive in a set of oracles `O` if it can be computed using `O` via basic operations (zero, successor, pairing, composition, primitive recursion, and μ-recursion).
- `TuringReducible`: The relation that `f` is recursive in `{g}`, i.e., `f ≤ᵀ g`.
- `TuringEquivalent`: A relation defining Turing equivalence between partial functions.
- `TuringDegree`: The set of equivalence classes under `TuringEquivalent`, forming a **partially ordered structure**.
Additionally:
- Prove that `TuringReducible` is a **preorder** (reflexive, transitive).
- Show that `TuringEquivalent` is an **equivalence relation**.
- Establish that **partial recursive functions** correspond to functions recursive in the empty oracle set.
This formalization follows classical recursion theory (Odifreddi, Soare) and extends previous work by Carneiro.
### Breaking Changes
None.
### Dependencies
None. |
t-computability
new-contributor
|
221/0 |
Mathlib.lean,Mathlib/Computability/TuringDegrees.lean |
2 |
8 |
['github-actions', 'tannerduve', 'tristan-f-r'] |
nobody |
7-65410 7 days ago |
21-81892 21 days ago |
21-81941 21 days |
| 23336 |
kim-em author:kim-em |
chore: `erw` in `Topology/Order/` |
|
t-topology |
6/7 |
Mathlib/Topology/Order/LawsonTopology.lean,Mathlib/Topology/Order/LowerUpperTopology.lean,Mathlib/Topology/Order/ScottTopology.lean,Mathlib/Topology/Order/UpperLowerSetTopology.lean |
4 |
4 |
['github-actions', 'kim-em', 'urkud'] |
nobody |
7-62459 7 days ago |
8-15211 8 days ago |
8-15261 8 days |
| 23360 |
kim-em author:kim-em |
chore: review of `erw` in `Algebra/Homology/DerivedCategory` |
|
|
21/15 |
Mathlib/Algebra/Homology/DerivedCategory/Basic.lean,Mathlib/Algebra/Homology/DerivedCategory/Ext/ExtClass.lean,Mathlib/Algebra/Homology/DerivedCategory/SingleTriangle.lean,Mathlib/Algebra/Homology/HomotopyCategory/SingleFunctors.lean,Mathlib/CategoryTheory/Shift/SingleFunctors.lean |
5 |
1 |
['github-actions'] |
nobody |
7-43713 7 days ago |
7-44690 7 days ago |
7-44678 7 days |
| 22961 |
xroblot author:xroblot |
feat(ZLattice/Covolume): add `covolume_div_covolume_eq_relindex` |
Add the following result:
Let `L₁` be a sub-`ℤ`-lattice of `L₂`. Then the index of `L₁` inside `L₂` is equal to `covolume L₁ / covolume L₂`.
---
- [x] depends on: #22940
[](https://gitpod.io/from-referrer/)
|
t-algebra label:t-algebra$ |
69/1 |
Mathlib/Algebra/Module/ZLattice/Basic.lean,Mathlib/Algebra/Module/ZLattice/Covolume.lean,Mathlib/GroupTheory/Index.lean,Mathlib/LinearAlgebra/Determinant.lean |
4 |
2 |
['github-actions', 'mathlib4-dependent-issues-bot'] |
nobody |
7-30219 7 days ago |
18-27254 18 days ago |
18-29706 18 days |
| 18578 |
mans0954 author:mans0954 |
feat(LinearAlgebra/QuadraticForm/Basis): basis expansion of a quadratic map |
Three lemmas about Quadratic maps applied to:
- A finite sum
- A `linearCombination`
- The representation of an element wrt a basis
---
- [x] depends on: #21835
- [x] depends on: #21836
[](https://gitpod.io/from-referrer/)
|
maintainer-merge
t-algebra
label:t-algebra$ |
105/1 |
Mathlib.lean,Mathlib/Data/Sym/Sym2/Finsupp.lean,Mathlib/LinearAlgebra/QuadraticForm/Basis.lean |
3 |
n/a |
['YaelDillies', 'eric-wieser', 'github-actions', 'kbuzzard', 'mans0954', 'mathlib4-dependent-issues-bot', 'riccardobrasca'] |
eric-wieser assignee:eric-wieser |
7-25649 7 days ago |
unknown |
unknown |
| 22655 |
YaelDillies author:YaelDillies |
refactor: make use of `FunLike` for `Submonoid.LocalizationMap` |
From Toric
---
[](https://gitpod.io/from-referrer/)
|
toric
t-algebra
label:t-algebra$ |
156/140 |
Mathlib/GroupTheory/MonoidLocalization/Away.lean,Mathlib/GroupTheory/MonoidLocalization/Basic.lean,Mathlib/GroupTheory/MonoidLocalization/MonoidWithZero.lean,Mathlib/RingTheory/Localization/Defs.lean |
4 |
1 |
['github-actions'] |
nobody |
7-22881 7 days ago |
7-22895 7 days ago |
24-49057 24 days |
| 23181 |
YaelDillies author:YaelDillies |
chore(UniformSpace/Defs): move entourages to their own file |
What's left in `UniformSpace.Defs` is precisely the theory of the uniformity filter.
The motivation is that the theory of coverings and packings in both high dimensional probability and dynamics can be based on entourages, while they have little to do with the uniformity filter (indeed, entourages are in a sense a quantitative version of the uniformity filter).
---
[](https://gitpod.io/from-referrer/)
|
t-topology |
180/207 |
Mathlib.lean,Mathlib/Topology/Metrizable/Uniformity.lean,Mathlib/Topology/UniformSpace/Defs.lean,Mathlib/Topology/UniformSpace/Entourage.lean |
4 |
10 |
['ADedecker', 'YaelDillies', 'b-mehta', 'github-actions'] |
nobody |
7-21569 7 days ago |
7-21624 7 days ago |
10-42057 10 days |
| 19668 |
YaelDillies author:YaelDillies |
refactor: define `≤`/`<` on `WithBot`/`WithTop` by induction |
The motivation for this change is that it is really confusing to run `intro r s shouldnthaveintroedthat` on a goal of the form `∀ r s : ℝ≥0∞, r ≤ s` and get the nonsense-looking goal `r = ↑shouldnthaveintroedthat → ∃ b : α, s = ↑b ∧ shouldnthaveintroedthat ≤ b⟩` instead of an error, and similarly when destructing something of the form `∃ r s : ℝ≥0∞, r < s`.
Furthermore, I suspect this improves performance.
---
- [x] depends on: #20317
- [x] depends on: #20318
- [x] depends on: #21274
- [x] depends on: #22109
[](https://gitpod.io/from-referrer/)
|
t-order |
65/47 |
Mathlib/Analysis/Analytic/OfScalars.lean,Mathlib/Analysis/Oscillation.lean,Mathlib/Data/Finset/Lattice/Fold.lean,Mathlib/Data/Finset/Max.lean,Mathlib/LinearAlgebra/Eigenspace/Triangularizable.lean,Mathlib/MeasureTheory/Integral/Lebesgue.lean,Mathlib/MeasureTheory/Measure/LevyProkhorovMetric.lean,Mathlib/Order/Interval/Basic.lean,Mathlib/Order/Interval/Set/WithBotTop.lean,Mathlib/Order/WithBot.lean,Mathlib/Probability/Variance.lean,Mathlib/RingTheory/PowerBasis.lean,Mathlib/Topology/MetricSpace/Holder.lean,Mathlib/Topology/MetricSpace/HolderNorm.lean |
14 |
10 |
['YaelDillies', 'eric-wieser', 'github-actions', 'mathlib4-dependent-issues-bot', 'urkud'] |
nobody |
7-15242 7 days ago |
7-15242 7 days ago |
7-15307 7 days |
| 23366 |
b-reinke author:b-reinke |
feat(GroupTheory/FreeGroup/Basic): add lemmas for invRev |
Upstreamed from the [EquationalTheories](https://github.com/teorth/equational_theories) project.
This PR adds the lemmas `invRev_append` and `invRev_cons` describing the interaction of `invRev` with the typical list operations. Note that `invRev_append` is a simp lemma, but `invRev_cons` is not, as otherwise there would be an infinite simp loop.
---
[](https://gitpod.io/from-referrer/)
|
t-geometric-group-theory
t-algebra
label:t-algebra$ |
7/0 |
Mathlib/GroupTheory/FreeGroup/Basic.lean |
1 |
1 |
['github-actions'] |
nobody |
7-12855 7 days ago |
7-12855 7 days ago |
7-22067 7 days |
| 23367 |
b-reinke author:b-reinke |
feat(GroupTheory/FreeGroup/Reduce): add lemmas for toWord and reduce |
Upstreamed from the [EquationalTheories](https://github.com/teorth/equational_theories) project.
This PR adds some simple helper lemmas for the interaction of `toWord` and `reduce` and basic list / group operations.
The RHS of the lemmas often contains more appearances of `reduce`, so they are not marked as `simp` lemmas.
---
[](https://gitpod.io/from-referrer/)
|
t-geometric-group-theory
t-algebra
label:t-algebra$ |
24/0 |
Mathlib/GroupTheory/FreeGroup/Reduce.lean |
1 |
1 |
['github-actions'] |
nobody |
7-12820 7 days ago |
7-12820 7 days ago |
7-21501 7 days |
| 23368 |
b-reinke author:b-reinke |
feat(GroupTheory/FreeGroup/ReducedWords): add theory of reduced words |
Upstreamed from the [EquationalTheories](https://github.com/teorth/equational_theories) project.
This PR adds the file `GroupTheory/FreeGroup/ReducedWords.lean`, where the predicate of reduced words is defined. It is shown that `reduce` and `toWord` produce reduced words.
This is done in preparation for the theory of cyclically reduced words.
---
[](https://gitpod.io/from-referrer/)
|
t-geometric-group-theory
t-algebra
label:t-algebra$ |
124/0 |
Mathlib.lean,Mathlib/GroupTheory/FreeGroup/ReducedWords.lean |
2 |
1 |
['github-actions'] |
nobody |
7-12800 7 days ago |
7-12800 7 days ago |
7-20636 7 days |
| 22018 |
maddycrim author:maddycrim |
feat(RingTheory/Localization/Pi): localization of a finite direct product where each semiring in product has maximal nilradical is a projection |
For noncomputable def `surjectivePiNilradicalIsMaximal` : Let `M` be a submonoid of a direct product of commutative rings `R i`.
If each `R i` has maximal nilradical then the direct product `∏ R i` surjects onto the
localization of `∏ R i` at `M`.
---
[](https://gitpod.io/from-referrer/)
|
large-import
new-contributor
t-algebra
label:t-algebra$ |
23/0 |
Mathlib/RingTheory/Localization/Pi.lean |
1 |
13 |
['Paul-Lez', 'erdOne', 'github-actions', 'jcommelin', 'maddycrim'] |
nobody |
7-340 7 days ago |
44-54408 1 month ago |
44-54460 44 days |
| 23197 |
robin-carlier author:robin-carlier |
feat(CategoryTheory/Equivalences): category structure on equivalences |
We put a category structure on `(C ≌ D)`. The morphisms are simply natural transformations between the underlying functor. We also provide various API for this structure.
---
While this PR contains functoriality of the operation that maps an equivalence to its underlying functor, functoriality of inverses will be in a different PR and recorded in a different file : I feel the most natural way to do this is to bring in the results from `Adjunction.Mates`, but this imports quite a lot of stuff.
[](https://gitpod.io/from-referrer/)
|
t-category-theory |
69/0 |
Mathlib/CategoryTheory/Equivalence.lean |
1 |
7 |
['github-actions', 'joelriou', 'robin-carlier'] |
nobody |
6-79823 6 days ago |
6-79823 6 days ago |
12-58028 12 days |
| 22870 |
kebekus author:kebekus |
feat: behavior of MeromorphicAt.order under powers and inverses |
Establish the behavior of `MeromorphicAt.order` under standard operations, including powers and inverses. The results are completely analogous to the existing theorems for `AnalyticAt.order`.
This material is used in [Project VD](https://github.com/kebekus/ProjectVD), which aims to formalize Value Distribution Theory for meromorphic functions on the complex plane.
---
[](https://gitpod.io/from-referrer/)
|
t-analysis |
26/12 |
Mathlib/Analysis/Meromorphic/Order.lean,Mathlib/Order/WithBot.lean |
2 |
1 |
['github-actions'] |
nobody |
6-77365 6 days ago |
6-77380 6 days ago |
21-44327 21 days |
| 23388 |
tristan-f-r author:tristan-f-r |
chore: proof_wanted on conway's 99 graph problem |
adds a proof_wanted of an open graph problem
---
[](https://gitpod.io/from-referrer/)
|
t-combinatorics
easy
|
5/0 |
Mathlib/Combinatorics/SimpleGraph/StronglyRegular.lean |
1 |
1 |
['github-actions'] |
nobody |
6-47966 6 days ago |
6-47966 6 days ago |
6-48210 6 days |
| 23381 |
vlad902 author:vlad902 |
feat: copy Subgroup lemma for Submonoid |
This is an exact copy of `Subgroup.map_top_of_surjective`, copied for Submonoid. |
t-algebra label:t-algebra$ |
8/0 |
Mathlib/Algebra/Group/Submonoid/Operations.lean |
1 |
4 |
['eric-wieser', 'github-actions', 'vlad902'] |
nobody |
6-36731 6 days ago |
6-73811 6 days ago |
6-74095 6 days |
| 23217 |
acmepjz author:acmepjz |
chore(AlgebraicGeometry/EllipticCurve/*): refactor VariableChange |
Drop certain definitions in `VariableChange` in favor of mathlib's built-in notation:
- `VariableChange.id` -> `(1 : VariableChange R)`
- `VariableChange.comp C C'` -> `C * C'`
- `VariableChange.inv C` -> `C⁻¹`
- `W.variableChange C` -> `C • W`
---
[](https://gitpod.io/from-referrer/)
Discussion: [#maths > thoughts on elliptic curves @ 💬](https://leanprover.zulipchat.com/#narrow/channel/116395-maths/topic/thoughts.20on.20elliptic.20curves/near/485467772) |
t-algebraic-geometry |
177/157 |
Mathlib/AlgebraicGeometry/EllipticCurve/Affine.lean,Mathlib/AlgebraicGeometry/EllipticCurve/IsomOfJ.lean,Mathlib/AlgebraicGeometry/EllipticCurve/NormalForms.lean,Mathlib/AlgebraicGeometry/EllipticCurve/VariableChange.lean |
4 |
1 |
['github-actions'] |
nobody |
6-32572 6 days ago |
11-39449 11 days ago |
11-39437 11 days |
| 21479 |
jt496 author:jt496 |
feat(Combinatorics/SimpleGraph): add facts about cliques and colorings of completeMultipartiteGraph |
Add basic lemmas about cliques and chromatic number of completeMultipartiteGraph.
In particular if a completeMultipartiteGraph is CliqueFree n then it is (n - 1) - colorable.
This last result is needed for the Andrasfai-Erdos-Sos theorem.
Co-authored-by: Lian Tattersall
---
[](https://gitpod.io/from-referrer/)
|
large-import
t-combinatorics
|
69/3 |
Mathlib/Combinatorics/SimpleGraph/Clique.lean,Mathlib/Combinatorics/SimpleGraph/Coloring.lean,Mathlib/Combinatorics/SimpleGraph/Triangle/Basic.lean |
3 |
19 |
['IvanRenison', 'b-mehta', 'github-actions', 'jt496', 'kbuzzard'] |
nobody |
6-25778 6 days ago |
13-28574 13 days ago |
54-28649 54 days |
| 23395 |
kim-em author:kim-em |
chore: review erw in Algebra/Homology |
|
t-algebra label:t-algebra$ |
19/13 |
Mathlib/Algebra/Homology/Embedding/Extend.lean,Mathlib/Algebra/Homology/HomotopyCategory/ShiftSequence.lean,Mathlib/Algebra/Homology/ShortComplex/Ab.lean,Mathlib/Algebra/Homology/ShortComplex/Limits.lean |
4 |
1 |
['github-actions'] |
nobody |
6-24688 6 days ago |
6-24688 6 days ago |
6-24743 6 days |
| 22085 |
IvanRenison author:IvanRenison |
feat(Combinatorics/SimpleGraph): introduce `ConnectedComponent.toSimpleGraph` |
---
I don't know if `ConnectedComponent.Graph` is the best name for this
[](https://gitpod.io/from-referrer/)
|
t-combinatorics |
65/10 |
Mathlib/Combinatorics/SimpleGraph/Matching.lean,Mathlib/Combinatorics/SimpleGraph/Path.lean |
2 |
5 |
['IvanRenison', 'github-actions', 'pimotte'] |
nobody |
6-17209 6 days ago |
6-17209 6 days ago |
33-70388 33 days |
| 23396 |
Ruben-VandeVelde author:Ruben-VandeVelde |
chore: split LocallyFinite results out of Compactness.Compact |
Copyright from: https://github.com/leanprover-community/mathlib3/pull/6352 and https://github.com/leanprover-community/mathlib3/pull/6948.
---
Conflicts with #23401.
[](https://gitpod.io/from-referrer/)
|
t-topology |
51/30 |
Mathlib.lean,Mathlib/Topology/Compactness/Compact.lean,Mathlib/Topology/Compactness/LocallyFinite.lean,Mathlib/Topology/Compactness/SigmaCompact.lean |
4 |
1 |
['github-actions'] |
nobody |
6-11937 6 days ago |
6-20711 6 days ago |
6-20768 6 days |
| 23386 |
AntoineChambert-Loir author:AntoineChambert-Loir |
feat(GroupTheory/GroupAction/MultiplePretransitivity): define multiply transitive actions |
This PR defines multiply transitive actions and proves the first basic lemmas about them.
* `MulAction.IsMultiplyPretransitive`:
An multiplicative action of a group `G` on a type `α` is n-transitive
if the action of `G` on `Fin n ↪ α` is pretransitive.
* Any action is 0-pretransitive
* `MulAction.is_one_pretransitive_iff` :
An action is 1-pretransitive iff it is pretransitive
* `MulAction.is_two_pretransitive_iff` :
An action is 2-pretransitive if for any `a`, `b`, `c`, `d`, such that
`a ≠ b` and `c ≠ d`, there exist `g : G` such that `g • a = b` and `g • c = d`.
* `MulAction.isMultiplyPretransitive_of_le` :
If an action is `n`-pretransitive, then it is `m`-pretransitive for all `m ≤ n`.
## Remarks on implementation
These results are results about actions on types `n ↪ α` induced by an action
on `α`, and some results are developed in this context.
---
[](https://gitpod.io/from-referrer/)
|
t-algebra label:t-algebra$ |
356/0 |
Mathlib.lean,Mathlib/Algebra/Group/Action/Pretransitive.lean,Mathlib/GroupTheory/GroupAction/MultipleTransitivity.lean |
3 |
3 |
['AntoineChambert-Loir', 'D-Thomine', 'github-actions'] |
nobody |
6-6179 6 days ago |
6-55074 6 days ago |
6-55077 6 days |
| 23179 |
vlad902 author:vlad902 |
feat: generalize Mathlib.LinearAlgebra |
This is one of a series of PRs that generalizes type classes across Mathlib. These are generated using a new linter that tries to re-elaborate theorem definitions with more general type classes to see if it succeeds. It will accept the generalization if deleting the entire type class causes the theorem to fail to compile, and the old type class can not simply be re-synthesized with the new declaration. Otherwise, the generalization is rejected as the type class is not being generalized, but can simply be replaced by implicit type class synthesis or an implicit type class in a variable block being pulled in.
The linter currently output debug statements indicating source file positions where type classes should be generalized, and a script then makes those edits. This file contains a subset of those generalizations. The linter and the script performing re-writes is available in commit 5e2b7040be0f73821c1dcb360ffecd61235d87af.
Also see discussion on Zulip here:
https://leanprover.zulipchat.com/#narrow/channel/270676-lean4/topic/Elab.20to.20generalize.20type.20classes.20for.20theorems/near/498862988 https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/Elab.20to.20generalize.20type.20classes.20for.20theorems/near/501288855 |
t-algebra label:t-algebra$ |
36/35 |
Mathlib/LinearAlgebra/AffineSpace/MidpointZero.lean,Mathlib/LinearAlgebra/Basis/SMul.lean,Mathlib/LinearAlgebra/BilinearForm/Properties.lean,Mathlib/LinearAlgebra/Dimension/Free.lean,Mathlib/LinearAlgebra/Dimension/StrongRankCondition.lean,Mathlib/LinearAlgebra/Dual/Defs.lean,Mathlib/LinearAlgebra/FiniteSpan.lean,Mathlib/LinearAlgebra/LinearIndependent/Basic.lean,Mathlib/LinearAlgebra/Matrix/Reindex.lean,Mathlib/LinearAlgebra/Multilinear/Basic.lean,Mathlib/LinearAlgebra/Prod.lean,Mathlib/LinearAlgebra/Projectivization/Basic.lean,Mathlib/LinearAlgebra/QuadraticForm/Basic.lean,Mathlib/LinearAlgebra/RootSystem/OfBilinear.lean,Mathlib/LinearAlgebra/Span/Basic.lean,Mathlib/LinearAlgebra/Span/Defs.lean,Mathlib/LinearAlgebra/TensorProduct/Graded/External.lean |
17 |
4 |
['github-actions', 'leanprover-bot', 'vlad902'] |
nobody |
5-83249 5 days ago |
5-83263 5 days ago |
6-30481 6 days |
| 23401 |
Ruben-VandeVelde author:Ruben-VandeVelde |
chore: split IsTopologicalBasis results out of Compactness.Compact |
Copyright from: https://github.com/leanprover-community/mathlib3/pull/15436 and https://github.com/leanprover-community/mathlib4/pull/12986.
---
Conflicts with #23396.
[](https://gitpod.io/from-referrer/)
|
longest-pole
t-topology
|
66/46 |
Mathlib.lean,Mathlib/Topology/ClopenBox.lean,Mathlib/Topology/Compactness/Bases.lean,Mathlib/Topology/Compactness/Compact.lean,Mathlib/Topology/Compactness/SigmaCompact.lean,Mathlib/Topology/Constructible.lean,Mathlib/Topology/QuasiSeparated.lean,Mathlib/Topology/Separation/Basic.lean,Mathlib/Topology/Sets/Opens.lean |
9 |
5 |
['Ruben-VandeVelde', 'github-actions', 'leanprover-bot', 'leanprover-community-mathlib4-bot'] |
nobody |
5-71076 5 days ago |
6-8613 6 days ago |
6-12110 6 days |
| 23411 |
PatrickMassot author:PatrickMassot |
chore: remove finiteness from Order.Filter.Lift |
Co-authored-by: Anatole Dedecker
---
[](https://gitpod.io/from-referrer/)
|
longest-pole
t-topology
|
45/21 |
Mathlib/Dynamics/TopologicalEntropy/DynamicalEntourage.lean,Mathlib/Order/Filter/Basic.lean,Mathlib/Order/Filter/Finite.lean,Mathlib/Order/Filter/Lift.lean,Mathlib/Topology/Algebra/ContinuousMonoidHom.lean,Mathlib/Topology/Basic.lean |
6 |
2 |
['github-actions', 'kim-em'] |
nobody |
5-64063 5 days ago |
5-66558 5 days ago |
5-66554 5 days |
| 23412 |
robin-carlier author:robin-carlier |
feat(CategoryTheory): joins of categories |
Define the join of two categories `C`, `D` as the category `C ⋆ D` characterized by the existence of fully faithful functors
`Join.inclLeft C D : C ⥤ C ⋆ D` and `Join.inclRight C D: D ⥤ C ⋆ D` that are jointly surjective on objects, and such that there is a unique map `edge c d : (inclLeft C D).obj c ⟶ (inclRight C D).obj d` for every `c : C` and `d : D`.
We also provide constructors for functors out of joins, and natural transforms between such functors. The main reference is [Kerodon: section 1.4.3.2](https://kerodon.net/tag/0160).
---
First of a small burst of PRs about joins of categories. Eventually, this construction should replace `WithInitial C` (which is `PUnit ⋆ C`) and `WithTerminal C` (which is `C ⋆ PUnit`).
[](https://gitpod.io/from-referrer/)
|
t-category-theory |
547/0 |
Mathlib.lean,Mathlib/CategoryTheory/Join/Basic.lean |
2 |
2 |
['github-actions', 'joelriou'] |
nobody |
5-62545 5 days ago |
5-72428 5 days ago |
5-72416 5 days |
| 23146 |
vlad902 author:vlad902 |
feat: generalize Mathlib.Data |
This is one of a series of PRs that generalizes type classes across
Mathlib. These are generated using a new linter that tries to
re-elaborate theorem definitions with more general type classes to see
if it succeeds. It will accept the generalization if deleting the entire
type class causes the theorem to fail to compile, and the old type class
can not simply be re-synthesized with the new declaration. Otherwise, the
generalization is rejected as the type class is not being generalized,
but can simply be replaced by implicit type class synthesis or an
implicit type class in a variable block being pulled in.
The linter currently output debug statements indicating source file
positions where type classes should be generalized, and a script then
makes those edits. This file contains a subset of those generalizations.
The linter and the script performing re-writes is available in commit
5e2b7040be0f73821c1dcb360ffecd61235d87af.
Also see discussions on Zulip here:
* https://leanprover.zulipchat.com/#narrow/channel/270676-lean4/topic/Elab.20to.20generalize.20type.20classes.20for.20theorems/near/498862988
* https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/Elab.20to.20generalize.20type.20classes.20for.20theorems/near/501288855 |
t-data |
36/36 |
Mathlib/Data/Complex/Module.lean,Mathlib/Data/Finset/MulAntidiagonal.lean,Mathlib/Data/Finset/NoncommProd.lean,Mathlib/Data/Finset/Pairwise.lean,Mathlib/Data/Finset/SMulAntidiagonal.lean,Mathlib/Data/Holor.lean,Mathlib/Data/Int/Cast/Lemmas.lean,Mathlib/Data/Matrix/Block.lean,Mathlib/Data/Matrix/Mul.lean,Mathlib/Data/Nat/Cast/Basic.lean,Mathlib/Data/Nat/Cast/Defs.lean,Mathlib/Data/Nat/Cast/Order/Ring.lean,Mathlib/Data/Set/MulAntidiagonal.lean,Mathlib/Data/ZMod/Basic.lean |
14 |
8 |
['eric-wieser', 'github-actions', 'leanprover-bot', 'vlad902'] |
nobody |
5-31354 5 days ago |
5-83187 5 days ago |
12-72002 12 days |
| 21162 |
smmercuri author:smmercuri |
feat: add `Valued.WithZeroMulInt.tendsto_zero_pow_of_le_neg_one` and applications to `adicCompletion K v` |
If `K` is a valued ring taking values in the multiplicative integers wth a zero adjoined, then `Valued.WithZeroMulInt.tendsto_zero_pow_of_le_neg_one` is the result that `x ^ n` tends to zero in this ring if `v x` is at most `-1` valued. As a result, in `adicCompletion K v`, we can always find a non-zero divisor that is arbitrarily small across a finite number of `v` (`AdicCompletion.exists_nonZeroDivisor_finset_valued_lt`).
---
- [x] depends on: #21160
- [x] depends on: #22055
[](https://gitpod.io/from-referrer/)
|
t-algebra label:t-algebra$ |
112/0 |
Mathlib.lean,Mathlib/RingTheory/DedekindDomain/AdicValuation.lean,Mathlib/Topology/Algebra/Valued/WithZeroMulInt.lean |
3 |
6 |
['YaelDillies', 'github-actions', 'mathlib4-dependent-issues-bot'] |
nobody |
5-25201 5 days ago |
33-2753 1 month ago |
56-2147 56 days |
| 23419 |
Parcly-Taxel author:Parcly-Taxel |
chore: deprime `induction'` with 5+ variables, part 1 |
Split from #23324 at the behest of @eric-wieser. |
tech debt |
150/125 |
Mathlib/Algebra/Module/Submodule/Pointwise.lean,Mathlib/Algebra/MvPolynomial/Derivation.lean,Mathlib/Algebra/MvPolynomial/Equiv.lean,Mathlib/Algebra/MvPolynomial/Eval.lean,Mathlib/Algebra/MvPolynomial/PDeriv.lean,Mathlib/Algebra/Order/BigOperators/Group/List.lean,Mathlib/Algebra/Polynomial/Module/Basic.lean,Mathlib/Algebra/Polynomial/PartialFractions.lean,Mathlib/Algebra/Squarefree/Basic.lean,Mathlib/Analysis/BoxIntegral/Integrability.lean,Mathlib/Analysis/Complex/UpperHalfPlane/Basic.lean,Mathlib/Analysis/InnerProductSpace/Projection.lean,Mathlib/CategoryTheory/Groupoid/FreeGroupoid.lean,Mathlib/CategoryTheory/IsConnected.lean,Mathlib/CategoryTheory/Localization/Construction.lean,Mathlib/CategoryTheory/PathCategory/Basic.lean,Mathlib/Computability/Ackermann.lean,Mathlib/Computability/EpsilonNFA.lean,Mathlib/Computability/PartrecCode.lean,Mathlib/Computability/PostTuringMachine.lean,Mathlib/RingTheory/UniqueFactorizationDomain/Defs.lean |
21 |
8 |
['Parcly-Taxel', 'apnelson1', 'eric-wieser', 'github-actions', 'urkud'] |
nobody |
5-16236 5 days ago |
5-52750 5 days ago |
5-52738 5 days |
| 23424 |
YaelDillies author:YaelDillies |
chore: move `StrictMonoOn f s → InjOn f s` earlier |
This is motivated by the need to have these lemmas early in #23177.
---
[](https://gitpod.io/from-referrer/)
|
large-import
t-order
|
29/34 |
Mathlib/Algebra/Order/Field/Basic.lean,Mathlib/Data/Int/Lemmas.lean,Mathlib/Data/Set/Monotone.lean,Mathlib/Order/Hom/Basic.lean,Mathlib/Order/Hom/Set.lean,Mathlib/Order/Interval/Set/Monotone.lean,Mathlib/Order/ModularLattice.lean,Mathlib/Order/Monotone/Basic.lean,Mathlib/Order/Monotone/Defs.lean,Mathlib/Order/Monotone/Extension.lean |
10 |
1 |
['github-actions'] |
nobody |
5-7406 5 days ago |
5-7406 5 days ago |
5-7479 5 days |
| 20315 |
erdOne author:erdOne |
feat(RingTheory): homogeneous localization away from an element is of finite type |
Co-authored-by: Patience Ablett
Co-authored-by: Kevin Buzzard
Co-authored-by: Harald Carlens
Co-authored-by: Wayne Ng Kwing King
Co-authored-by: Michael Schlößer
Co-authored-by: Justus Springer
Co-authored-by: Jujian Zhang
This contribution was created as part of the Durham Computational Algebraic Geometry Workshop
---
- [x] depends on: #21795
[](https://gitpod.io/from-referrer/)
|
large-import
t-algebra
label:t-algebra$ |
244/1 |
Mathlib.lean,Mathlib/RingTheory/GradedAlgebra/FiniteType.lean,Mathlib/RingTheory/GradedAlgebra/HomogeneousLocalization.lean |
3 |
14 |
['erdOne', 'github-actions', 'kbuzzard', 'mathlib4-dependent-issues-bot', 'riccardobrasca'] |
nobody |
5-7334 5 days ago |
8-16656 8 days ago |
56-81979 56 days |
| 22050 |
IvanRenison author:IvanRenison |
feat(Combinatorics/SimpleGraph): Add `SimpleGraph.Preconnected.support_eq_univ` |
Co-authored-by: Kyle Miller kmill31415@gmail.com
---
Suggested in [zulip](https://leanprover.zulipchat.com/#narrow/channel/252551-graph-theory/topic/Way.20ConnectedComponent.20definition.20uses.20Quot.3F)
[](https://gitpod.io/from-referrer/)
|
t-combinatorics |
44/0 |
Mathlib/Combinatorics/SimpleGraph/Path.lean |
1 |
4 |
['b-mehta', 'github-actions', 'urkud'] |
b-mehta assignee:b-mehta |
5-6661 5 days ago |
5-6674 5 days ago |
36-26086 36 days |
| 23309 |
kkytola author:kkytola |
feat: left/right order-continuous functions are left/right topology-continuous |
Order left/right-continuous functions on (densely ordered) conditionally complete linear orders are topologically left/right-continuous.
Co-authored-by: Yaël Dillies
---
[](https://gitpod.io/from-referrer/)
|
t-order |
27/3 |
Mathlib/Topology/Order/Basic.lean |
1 |
3 |
['YaelDillies', 'github-actions', 'kkytola'] |
nobody |
5-6160 5 days ago |
9-741 9 days ago |
9-729 9 days |
| 23440 |
xroblot author:xroblot |
chore(NumberField/Units): make `torsionOrder` a `Nat` |
Originally, the order of the torsion subgroup of units of a number field was defined as a `PNat` since `rootsOfUnity` was using `PNat`. This is not the case anymore since `rootsOfUnity` is now using `NeZero` instead. Thus, we change the type of `torsionOrder` to `Nat` and change to an `abbrev` so that it gets a `NeZero` instance automatically.
As a bonus, we also prove that `torsionOrder` is even.
---
[](https://gitpod.io/from-referrer/)
|
t-number-theory |
17/6 |
Mathlib/NumberTheory/NumberField/CanonicalEmbedding/FundamentalCone.lean,Mathlib/NumberTheory/NumberField/Units/Basic.lean |
2 |
1 |
['github-actions'] |
nobody |
4-79407 4 days ago |
4-82493 4 days ago |
4-82539 4 days |
| 23334 |
Ruben-VandeVelde author:Ruben-VandeVelde |
feat: add lemmas about Field.toEuclideanDomain |
The behaviour of mod and gcd in a field are somewhat unexpected. I think that adding simp lemmas to reduce them to more well-understood notions will be helpful for people who accidentally end up using them, even if the right-hand side is not necessarily "simp"ler on first sight.
---
[](https://gitpod.io/from-referrer/)
|
t-algebra label:t-algebra$ |
21/2 |
Mathlib/Algebra/EuclideanDomain/Field.lean |
1 |
6 |
['Ruben-VandeVelde', 'acmepjz', 'github-actions'] |
nobody |
4-71614 4 days ago |
8-23010 8 days ago |
8-23068 8 days |
| 13861 |
BoltonBailey author:BoltonBailey |
feat(Data/Finsupp/Basic): `Finsupp.optionElim'` |
Similar to how `Finsupp.cons` constructs a map `Fin (n + 1) →₀ M` from a map `Fin n →₀ M`,
we define `Finsupp.optionElim'` to construct a map `Option α →₀ M` from a map `α →₀ M`, given an additional value for `none`. As a function, it behaves as `Option.elim'`, hence the name.
We prove a variety of API lemmas, based on those for `Finsupp.cons`, to bring the definitions more in line with the contents of `Data/Finsupp/Fin`.
We also do some light refactoring for succinctness, and put this any related preexisting lemmas in a new file to not trigger the linter.
Needed by #12664
---
[](https://gitpod.io/from-referrer/)
|
t-data |
204/62 |
Mathlib.lean,Mathlib/Algebra/Category/MonCat/Adjunctions.lean,Mathlib/Data/Finsupp/Basic.lean,Mathlib/Data/Finsupp/Option.lean,Mathlib/Data/Finsupp/Single.lean,Mathlib/LinearAlgebra/Finsupp/LinearCombination.lean |
6 |
1 |
['github-actions'] |
nobody |
4-65560 4 days ago |
9-4278 9 days ago |
9-4258 9 days |
| 21539 |
Raph-DG author:Raph-DG |
feat(LinearAlgebra): Symmetric Algebra |
Defined the universal property for the symmetric algebra of a module over a commutative ring, provided an explicit construction and proved that this satisfies the universal property. Also proved that the multivariate polynomial ring generated by a basis of a module satisfies the universal property of the symmetric algebra of that module.
Co-authored-by: Raphael Douglas Giles , Zhixuan Dai <22300180006@m.fudan.edu.cn>, Zhenyan Fu , Yiming Fu , Wang Jingting
---
[](https://gitpod.io/from-referrer/)
|
new-contributor
t-algebra
label:t-algebra$ |
209/0 |
Mathlib.lean,Mathlib/LinearAlgebra/SymmetricAlgebra/Basic.lean,Mathlib/LinearAlgebra/SymmetricAlgebra/MvPolynomial.lean |
3 |
15 |
['ADedecker', 'Raph-DG', 'github-actions', 'xyzw12345'] |
nobody |
4-53295 4 days ago |
4-53447 4 days ago |
52-52559 52 days |
| 23446 |
acmepjz author:acmepjz |
feat(Algebra/Exact): add `Function.Exact.[iff_]rangeFactorization` etc |
Two maps `f : M → N` and `g : N → P` are exact if and only if the induced maps `Set.range f → N → Set.range g` are exact. Same for `AddMonoidHom` and `LinearMap`.
---
[](https://gitpod.io/from-referrer/)
Discussion: [#Is there code for X? > Function.Exact.rangeFactorization](https://leanprover.zulipchat.com/#narrow/channel/217875-Is-there-code-for-X.3F/topic/Function.2EExact.2ErangeFactorization) |
t-algebra label:t-algebra$ |
41/2 |
Mathlib/Algebra/Exact.lean |
1 |
1 |
['github-actions'] |
nobody |
4-34467 4 days ago |
4-34467 4 days ago |
4-34455 4 days |
| 23453 |
xroblot author:xroblot |
feat(RootsOfUnity/Complex): the conjugate of a complex root of unity is its inverse |
---
[](https://gitpod.io/from-referrer/)
|
t-algebra label:t-algebra$ |
5/0 |
Mathlib/RingTheory/RootsOfUnity/Complex.lean |
1 |
1 |
['github-actions'] |
nobody |
4-593 4 days ago |
4-593 4 days ago |
4-649 4 days |
| 22269 |
Thmoas-Guan author:Thmoas-Guan |
chore(Algebra):replace Submodule.quotient.mk with Submodule.mkQ |
Replace Submodule.quotient.mk with Submodule.mkQ as much as possible as it have better composition property and more direct lemmas, making it more similarly with `Ideal.Quotient.mk`
(except Algebra.Lie.Quotient.Basic for ones more familiar with these area)
---
[](https://gitpod.io/from-referrer/)
|
|
431/218 |
Mathlib/Algebra/Exact.lean,Mathlib/Algebra/Module/CharacterModule.lean,Mathlib/Algebra/Module/LocalizedModule/Submodule.lean,Mathlib/Algebra/Module/PID.lean,Mathlib/Algebra/Module/Torsion.lean,Mathlib/Algebra/Module/ZLattice/Basic.lean,Mathlib/LinearAlgebra/Dimension/Constructions.lean,Mathlib/LinearAlgebra/Dimension/RankNullity.lean,Mathlib/LinearAlgebra/Dual/Lemmas.lean,Mathlib/LinearAlgebra/Isomorphisms.lean,Mathlib/LinearAlgebra/Projection.lean,Mathlib/LinearAlgebra/Quotient/Basic.lean,Mathlib/LinearAlgebra/Quotient/Defs.lean,Mathlib/LinearAlgebra/Quotient/Pi.lean,Mathlib/LinearAlgebra/SModEq.lean,Mathlib/LinearAlgebra/Semisimple.lean,Mathlib/LinearAlgebra/TensorProduct/Quotient.lean,Mathlib/LinearAlgebra/TensorProduct/RightExactness.lean,Mathlib/NumberTheory/RamificationInertia/Basic.lean,Mathlib/RepresentationTheory/GroupCohomology/LowDegree.lean,Mathlib/RingTheory/AdicCompletion/Algebra.lean,Mathlib/RingTheory/AdicCompletion/Basic.lean,Mathlib/RingTheory/AdicCompletion/Exactness.lean,Mathlib/RingTheory/AdicCompletion/Functoriality.lean,Mathlib/RingTheory/Flat/FaithfullyFlat/Basic.lean,Mathlib/RingTheory/Ideal/Colon.lean,Mathlib/RingTheory/Ideal/Quotient/Basic.lean,Mathlib/RingTheory/Ideal/Quotient/Defs.lean,Mathlib/RingTheory/Ideal/Quotient/Operations.lean,Mathlib/RingTheory/PowerBasis.lean,Mathlib/RingTheory/QuotSMulTop.lean,Mathlib/RingTheory/Smooth/Basic.lean,Mathlib/RingTheory/TensorProduct/Quotient.lean |
33 |
8 |
['Thmoas-Guan', 'erdOne', 'github-actions', 'leanprover-bot'] |
nobody |
3-86338 3 days ago |
4-13697 4 days ago |
14-71927 14 days |
| 21524 |
Timeroot author:Timeroot |
feat(BigOperators/Finset): prod_comm_3 |
A cyclically permuting version of `Finset.prod_comm`. Sort of like `LinearMap.trace_mul_cycle`. Think you could debate if it's "necessary" but we were using it enough that we wanted to have its own lemma; the alternative would be writing `prod_comm` with implicit arguments a bunch of times.
---
[](https://gitpod.io/from-referrer/)
|
t-algebra label:t-algebra$ |
6/0 |
Mathlib/Algebra/BigOperators/Group/Finset/Sigma.lean |
1 |
1 |
['github-actions'] |
nobody |
3-77812 3 days ago |
3-78018 3 days ago |
25-37171 25 days |
| 23461 |
xroblot author:xroblot |
feat(GroupTheory/Cyclic): formula for the card & index of kernel & range of powMonoidHom on a cyclic group |
We prove formula for the cardinal and index of the kernel and range of `powMonoidHom : x ↦ x ^ d` on a finite cyclic group.
---
[](https://gitpod.io/from-referrer/)
|
t-algebra label:t-algebra$ |
48/0 |
Mathlib/GroupTheory/Index.lean,Mathlib/GroupTheory/SpecificGroups/Cyclic.lean |
2 |
1 |
['github-actions'] |
nobody |
3-73838 3 days ago |
3-73988 3 days ago |
3-74036 3 days |
| 22100 |
smmercuri author:smmercuri |
feat: two inequivalent absolute values have a `< 1` and `> 1` value |
- Two absolute values `v` and `w` are equivalent if and only if `v x < 1` exactly when `w x < 1`
- Two inequivalent absolute values `v` and `w` have a point `x` at which `1 < v x` and `w x < 1`
---
[](https://gitpod.io/from-referrer/)
|
|
174/0 |
Mathlib/Algebra/Order/AbsoluteValue/Basic.lean,Mathlib/Analysis/AbsoluteValue/Equivalence.lean |
2 |
6 |
['Paul-Lez', 'github-actions', 'smmercuri'] |
nobody |
3-71896 3 days ago |
3-74346 3 days ago |
16-55236 16 days |
| 21283 |
erdOne author:erdOne |
feat: topology on Hom(R, S) in `CommRingCat` |
Co-authored-by: Christian Merten
---
[](https://gitpod.io/from-referrer/)
|
t-algebra
t-topology
label:t-algebra$ |
227/0 |
Mathlib.lean,Mathlib/Algebra/Category/Ring/Constructions.lean,Mathlib/Algebra/Category/Ring/Topology.lean,Mathlib/Topology/Constructions.lean,Mathlib/Topology/Homeomorph/Lemmas.lean,scripts/noshake.json |
6 |
5 |
['dagurtomas', 'erdOne', 'github-actions'] |
nobody |
3-71849 3 days ago |
3-71849 3 days ago |
42-27505 42 days |
| 21950 |
erdOne author:erdOne |
feat(NumberTheory/Padics): the completion of `ℚ` at a finite place is `ℚ_[p]` |
---
[](https://gitpod.io/from-referrer/)
|
t-number-theory |
257/1 |
Mathlib.lean,Mathlib/Algebra/GroupWithZero/WithZero.lean,Mathlib/NumberTheory/Padics/HeightOneSpectrum.lean,Mathlib/NumberTheory/Padics/PadicNumbers.lean,Mathlib/Topology/Algebra/Valued/WithVal.lean,Mathlib/Topology/Algebra/WithZeroMulInt.lean,Mathlib/Topology/Algebra/WithZeroTopology.lean |
7 |
14 |
['Ruben-VandeVelde', 'erdOne', 'github-actions'] |
nobody |
3-68118 3 days ago |
3-68118 3 days ago |
4-70640 4 days |
| 23025 |
Paul-Lez author:Paul-Lez |
feat(Lean/ToExpr): add helper functions to create `Expr` for finsets/sets/multisets |
This PR adds some helper functions for building `Expr` terms for finsets/sets/multisets. One application of this is the creation of certain `simproc`s (see e.g. #23026).
The implementation of `List.toExprAux` and `List.toFinsetExpr` was done by @b-mehta.
Co-authored-by: Bhavik Mehta
Co-authored-by: Eric Wieser
---
[](https://gitpod.io/from-referrer/)
|
t-meta |
14/0 |
Mathlib/Util/Qq.lean |
1 |
13 |
['Paul-Lez', 'b-mehta', 'eric-wieser', 'github-actions'] |
nobody |
3-66070 3 days ago |
3-66170 3 days ago |
3-66227 3 days |
| 21673 |
erdOne author:erdOne |
feat: `∑ z ∈ L, ‖z - x‖⁻ʳ` converges for lattices `L` |
---
[](https://gitpod.io/from-referrer/)
|
t-analysis |
329/0 |
Mathlib.lean,Mathlib/Algebra/BigOperators/Group/Finset/Disjoint.lean,Mathlib/Algebra/Module/ZLattice/Summable.lean,Mathlib/Order/Disjointed.lean |
4 |
1 |
['github-actions'] |
nobody |
3-53290 3 days ago |
3-53304 3 days ago |
21-25572 21 days |
| 23472 |
erdOne author:erdOne |
feat(Topology): Continuous open maps with irreducible fibers induce bijections between irreducible components |
Co-authored-by: Christian Merten
---
[](https://gitpod.io/from-referrer/)
|
t-topology |
78/0 |
Mathlib/Topology/Irreducible.lean |
1 |
1 |
['github-actions'] |
nobody |
3-44843 3 days ago |
3-44846 3 days ago |
3-44894 3 days |
| 23467 |
JovanGerb author:JovanGerb |
chore: remove duplicate instance `SMul Mˣ α` |
This instance is accidentally duplicated, and already exists in `Mathlib.Algebra.Group.Action.Units`
---
[](https://gitpod.io/from-referrer/)
|
t-algebra label:t-algebra$ |
1/4 |
Mathlib/Algebra/GroupWithZero/Action/Units.lean,Mathlib/CategoryTheory/Preadditive/Basic.lean |
2 |
1 |
['github-actions'] |
nobody |
3-40570 3 days ago |
3-55655 3 days ago |
3-55710 3 days |
| 22727 |
grunweg author:grunweg |
feat: rewrite the isolated by and colon linters in Lean |
---
- depends on #22726
- depends on: #22728
[](https://gitpod.io/from-referrer/)
|
t-linter |
128/96 |
Mathlib/AlgebraicTopology/SimplexCategory/GeneratorsRelations/Basic.lean,Mathlib/Data/Finsupp/AList.lean,Mathlib/Data/Int/ModEq.lean,Mathlib/Data/List/Nodup.lean,Mathlib/Data/List/TFAE.lean,Mathlib/Data/Matroid/Circuit.lean,Mathlib/Data/Matroid/Minor/Basic.lean,Mathlib/GroupTheory/Perm/Cycle/Factors.lean,Mathlib/LinearAlgebra/TensorProduct/Vanishing.lean,Mathlib/Order/KrullDimension.lean,Mathlib/Probability/Kernel/WithDensity.lean,Mathlib/RingTheory/NoetherNormalization.lean,Mathlib/Tactic/Linter/TextBased.lean,Mathlib/Topology/Sets/OpenCover.lean,scripts/lint-style.py |
15 |
2 |
['adomani', 'github-actions'] |
nobody |
3-29969 3 days ago |
8-69418 8 days ago |
10-50147 10 days |
| 23266 |
mariainesdff author:mariainesdff |
feat(Algebra/Order/BigOperator): add lemmas |
---
[](https://gitpod.io/from-referrer/)
|
large-import
t-order
t-algebra
label:t-algebra$ |
68/1 |
Mathlib/Algebra/Order/BigOperators/Ring/Finset.lean,Mathlib/Algebra/Order/BigOperators/Ring/Multiset.lean,Mathlib/Data/Finset/Max.lean |
3 |
1 |
['github-actions'] |
nobody |
3-28107 3 days ago |
10-920 10 days ago |
10-966 10 days |
| 23251 |
mariainesdff author:mariainesdff |
feat(FieldTheory/IntermediateField/Adjoin): add lemmas |
---
[](https://gitpod.io/from-referrer/)
|
t-algebra label:t-algebra$ |
57/0 |
Mathlib/FieldTheory/IntermediateField/Adjoin/Basic.lean,Mathlib/FieldTheory/IsAlgClosed/AlgebraicClosure.lean |
2 |
14 |
['alreadydone', 'github-actions', 'mariainesdff', 'tb65536'] |
nobody |
3-27356 3 days ago |
10-22472 10 days ago |
10-22460 10 days |
| 23474 |
Parcly-Taxel author:Parcly-Taxel |
chore: clear `docBlame` in `Computability` and `ModelTheory` |
Split from #22754. |
tech debt |
30/30 |
Mathlib/Computability/Encoding.lean,Mathlib/Computability/Partrec.lean,Mathlib/Data/Nat/Find.lean,Mathlib/Data/Seq/Parallel.lean,Mathlib/ModelTheory/Bundled.lean,Mathlib/ModelTheory/ElementaryMaps.lean,Mathlib/ModelTheory/ElementarySubstructures.lean,Mathlib/ModelTheory/LanguageMap.lean,Mathlib/ModelTheory/Quotients.lean,Mathlib/ModelTheory/Substructures.lean,Mathlib/ModelTheory/Syntax.lean,Mathlib/ModelTheory/Types.lean,scripts/nolints.json |
13 |
1 |
['github-actions'] |
nobody |
3-26940 3 days ago |
3-39301 3 days ago |
3-39289 3 days |
| 13349 |
CBirkbeck author:CBirkbeck |
feat: TendstoUniformlyOn for tprod's |
Give conditions for prods to converge uniformly to a tprod.
---
- [x] depends on: #16543
- [x] depends on: #16546
- [x] depends on: #15398
[](https://gitpod.io/from-referrer/)
|
t-analysis |
124/25 |
Mathlib.lean,Mathlib/Analysis/SpecialFunctions/Log/Summable.lean,Mathlib/Topology/UniformSpace/MultipliableTendstoUniformly.lean,Mathlib/Topology/UniformSpace/UniformConvergence.lean,Mathlib/Topology/UniformSpace/UniformConvergenceTopology.lean |
5 |
53 |
['ADedecker', 'CBirkbeck', 'github-actions', 'j-loreaux', 'loefflerd', 'mathlib4-dependent-issues-bot'] |
nobody |
3-24523 3 days ago |
15-74206 15 days ago |
34-53190 34 days |
| 23275 |
miguelmarco author:miguelmarco |
feat: add rewriting lemmas for integers |
This PR includes some equalities and equivalences about expressions with integer numbers.
They can be useful as rewriting lemmas to simplify expressions.
(See #8102 for motivation)
[](https://gitpod.io/from-referrer/)
|
t-data
maintainer-merge
new-contributor
|
117/1 |
Mathlib/Data/Int/Init.lean |
1 |
22 |
['Paul-Lez', 'YaelDillies', 'github-actions', 'kim-em', 'miguelmarco'] |
nobody |
3-24330 3 days ago |
4-83312 4 days ago |
8-44346 8 days |
| 23209 |
wwylele author:wwylele |
feat(Analysis): add improper integral of complex exp |
These are the infinite version of integral_exp_mul_complex.
---
[](https://gitpod.io/from-referrer/)
|
new-contributor
t-analysis
|
66/0 |
Mathlib/Analysis/SpecialFunctions/ImproperIntegrals.lean,Mathlib/MeasureTheory/Measure/Lebesgue/Integral.lean |
2 |
7 |
['github-actions', 'j-loreaux', 'wwylele'] |
nobody |
3-20860 3 days ago |
12-51689 12 days ago |
12-51742 12 days |
| 23498 |
Ruben-VandeVelde author:Ruben-VandeVelde |
chore(Topology.MetricSpace.Lipschitz): stop depending on Topology.Algebra |
Noticed while playing with the new `directoryDependency` linter. Not sure if these could be proved without assuming the continuity of real multiplication.
Copyright from https://github.com/leanprover-community/mathlib3/pull/1921 and https://github.com/leanprover-community/mathlib4/pull/11840.
---
[](https://gitpod.io/from-referrer/)
|
|
60/34 |
Mathlib.lean,Mathlib/Analysis/Normed/Group/AddTorsor.lean,Mathlib/Analysis/NormedSpace/Multilinear/Basic.lean,Mathlib/Analysis/SpecialFunctions/Exp.lean,Mathlib/Topology/Algebra/MetricSpace/Lipschitz.lean,Mathlib/Topology/MetricSpace/Algebra.lean,Mathlib/Topology/MetricSpace/IsometricSMul.lean,Mathlib/Topology/MetricSpace/Lipschitz.lean,Mathlib/Topology/MetricSpace/PiNat.lean |
9 |
1 |
['github-actions'] |
nobody |
3-12898 3 days ago |
3-12958 3 days ago |
3-12946 3 days |
| 23425 |
vasnesterov author:vasnesterov |
feat(Algebra/BigOperators): simprocify `prod_univ_one/two/three/...` |
Add a simproc `prod_univ_many` that rewrites `∏ (i : Fin n), f i` as `f 0 * f 1 * ... * f (n - 1)`, generalizing `prod_univ_one`, `prod_univ_two`, ..., `prod_univ_eight`.
---
It seems impossible to use to_additive here to avoid reimplementing the same simproc for additive goals. Just wanted to hear your ideas, before doing it.
- [x] depends on: #23427
[](https://gitpod.io/from-referrer/)
|
t-meta |
51/0 |
Mathlib/Data/Fin/Tuple/Reflection.lean |
1 |
9 |
['eric-wieser', 'github-actions', 'mathlib4-dependent-issues-bot', 'vasnesterov'] |
nobody |
3-5878 3 days ago |
3-46050 3 days ago |
4-8524 4 days |
| 23236 |
alreadydone author:alreadydone |
chore(Topology/Instances/AddCircle): golf and little lemmas |
---
[](https://gitpod.io/from-referrer/)
|
t-algebra label:t-algebra$ |
44/37 |
Mathlib/Topology/Instances/AddCircle.lean |
1 |
5 |
['alreadydone', 'eric-wieser', 'github-actions'] |
nobody |
3-3448 3 days ago |
3-3462 3 days ago |
10-83952 10 days |
| 23502 |
Timeroot author:Timeroot |
feat(ModelTheory/Semantics): BoundedFormula.realize_foldr_imp |
Two lemmas for `realize`ing a `BoundedFormula`.
---
Pulled out from #19695.
[](https://gitpod.io/from-referrer/)
|
t-logic |
20/0 |
Mathlib/ModelTheory/Semantics.lean,Mathlib/ModelTheory/Syntax.lean |
2 |
1 |
['github-actions'] |
nobody |
3-2691 3 days ago |
3-3591 3 days ago |
3-3648 3 days |
| 23206 |
urkud author:urkud |
feat(EGauge): add `egauge_pi` and `egauge_prod` |
Also change recently introduced `smul_set*pi*` to use unapplied smul in the rhs.
---
- [ ] depends on: #22573
[](https://gitpod.io/from-referrer/)
|
t-analysis |
131/25 |
Mathlib/Algebra/Group/Action/Pointwise/Set/Basic.lean,Mathlib/Algebra/Group/Pointwise/Set/Scalar.lean,Mathlib/Algebra/GroupWithZero/Action/Pointwise/Set.lean,Mathlib/Analysis/Convex/EGauge.lean |
4 |
17 |
['eric-wieser', 'github-actions', 'mathlib4-dependent-issues-bot', 'urkud'] |
nobody |
2-82169 2 days ago |
12-12441 12 days ago |
12-19625 12 days |
| 23470 |
erdOne author:erdOne |
feat(AlgebraicGeometry): section of a k-scheme is a closed immersion |
Co-authored-by: Christian Merten
---
[](https://gitpod.io/from-referrer/)
|
t-algebraic-geometry |
89/3 |
Mathlib/AlgebraicGeometry/Limits.lean,Mathlib/AlgebraicGeometry/Morphisms/ClosedImmersion.lean,Mathlib/AlgebraicGeometry/OpenImmersion.lean,Mathlib/AlgebraicGeometry/PullbackCarrier.lean,Mathlib/AlgebraicGeometry/Pullbacks.lean,Mathlib/AlgebraicGeometry/Scheme.lean |
6 |
7 |
['chrisflav', 'github-actions'] |
nobody |
2-77730 2 days ago |
3-48740 3 days ago |
3-48772 3 days |
| 23503 |
apnelson1 author:apnelson1 |
feat(Topology/Instances/ENat): ENat and tsum |
We give API for the interactions between `tsum` and `ENat`. The type is especially nice, because every function is summable, and there are simplifying lemmas like the statement that a sum is infinite iff either some term is infinite, or the support is infinite.
This provides one of the missing pieces for working painlessly with discrete objects, 'propositional' finiteness and cardinality. For instance, one can sum a function `f : a -> ENat` over an arbitrary set with the term `∑' a : s, 1`, and it will be provable that `∑' a : s, 1 = s.encard` and `(support f).encard ≤ ∑' a, f a` without ever having to split into finite/infinite cases.
As is pointed out in the module docstring for `Data.ENat`, there are strong analogies between `ENat` and `ENNReal`, and the API runs parallel to the API for `tsum`/`ENNReal`. One could call it 'duplication', but I have yet to find a common generalization of the two that saves work, or a third example of a natural type with these same properties.
---
[](https://gitpod.io/from-referrer/)
|
large-import |
205/2 |
Mathlib/Data/ENat/Basic.lean,Mathlib/Data/Set/Card.lean,Mathlib/Topology/Instances/ENat.lean |
3 |
2 |
['eric-wieser', 'github-actions'] |
nobody |
2-67037 2 days ago |
2-78741 2 days ago |
2-78735 2 days |
| 23490 |
erdOne author:erdOne |
feat(Algebra/Category): the category of topological modules |
Co-authored-by: Richard Hill
---
[](https://gitpod.io/from-referrer/)
|
t-algebra label:t-algebra$ |
459/0 |
Mathlib.lean,Mathlib/Algebra/Category/ModuleCat/Topology/Basic.lean |
2 |
1 |
['github-actions'] |
nobody |
2-65902 2 days ago |
3-17747 3 days ago |
3-17804 3 days |
| 21909 |
erdOne author:erdOne |
feat(RingTheory/Invariants): Generalize to profinite groups |
---
[](https://gitpod.io/from-referrer/)
|
t-algebra label:t-algebra$ |
350/5 |
Mathlib.lean,Mathlib/Algebra/Algebra/Subalgebra/Operations.lean,Mathlib/NumberTheory/RamificationInertia/Galois.lean,Mathlib/RingTheory/Frobenius.lean,Mathlib/RingTheory/Invariant/Basic.lean,Mathlib/RingTheory/Invariant/Profinite.lean |
6 |
2 |
['TwoFX', 'github-actions'] |
nobody |
2-64231 2 days ago |
2-64231 2 days ago |
6-52412 6 days |
| 22339 |
chrisflav author:chrisflav |
feat(RingTheory): base change commutes with finite products |
and in particular with localizations of modules.
---
[](https://gitpod.io/from-referrer/)
|
t-algebra label:t-algebra$ |
99/0 |
Mathlib.lean,Mathlib/Algebra/Module/LocalizedModule/Basic.lean,Mathlib/RingTheory/TensorProduct/IsBaseChangePi.lean |
3 |
4 |
['chrisflav', 'erdOne', 'github-actions'] |
nobody |
2-62638 2 days ago |
35-75312 1 month ago |
35-76508 35 days |
| 23504 |
Timeroot author:Timeroot |
feat(ModelTheory/Syntax): substFunc |
Defines `FirstOrder.Language.Term.substFunc`, a way to substitute function definitions inside of a term. Compare this with existing `subst`, which just substitutes variables.
---
Pulled out from #19695
- [ ] depends on #23502
[](https://gitpod.io/from-referrer/)
|
t-logic |
33/0 |
Mathlib/ModelTheory/Semantics.lean,Mathlib/ModelTheory/Syntax.lean |
2 |
1 |
['github-actions'] |
nobody |
2-48037 2 days ago |
3-2777 3 days ago |
3-2827 3 days |
| 22265 |
Timeroot author:Timeroot |
feat(Geometry/Euclidean/Angle/Unoriented): triangle inequality |
filled in a `proof_wanted`
---
[](https://gitpod.io/from-referrer/)
|
t-euclidean-geometry |
78/12 |
Mathlib.lean,Mathlib/Geometry/Euclidean/Angle/Unoriented/Affine.lean,Mathlib/Geometry/Euclidean/Angle/Unoriented/Basic.lean,Mathlib/Geometry/Euclidean/Angle/Unoriented/TriangleInequality.lean,Mathlib/LinearAlgebra/Matrix/PosDef.lean |
5 |
7 |
['Timeroot', 'github-actions', 'jsm28', 'urkud'] |
nobody |
2-47730 2 days ago |
2-84644 2 days ago |
23-2028 23 days |
| 21399 |
erdOne author:erdOne |
feat(CategoryTheory): `ChosenFiniteProducts (Over X)` |
---
[](https://gitpod.io/from-referrer/)
|
t-category-theory |
233/10 |
Mathlib.lean,Mathlib/CategoryTheory/ChosenFiniteProducts/Over.lean,Mathlib/CategoryTheory/Comma/Over/Basic.lean,Mathlib/CategoryTheory/Limits/Constructions/Over/Products.lean,Mathlib/CategoryTheory/Sites/EffectiveEpimorphic.lean |
5 |
21 |
['b-mehta', 'erdOne', 'github-actions', 'joelriou', 'sinhp'] |
nobody |
2-32964 2 days ago |
2-32964 2 days ago |
24-50830 24 days |
| 23527 |
erdOne author:erdOne |
feat(Topology): subspace of quotient topology is quotient of subspace topology |
---
[](https://gitpod.io/from-referrer/)
|
t-topology |
69/0 |
Mathlib/Topology/Maps/OpenQuotient.lean |
1 |
1 |
['github-actions'] |
nobody |
2-28640 2 days ago |
2-28729 2 days ago |
2-28717 2 days |
| 23528 |
Ruben-VandeVelde author:Ruben-VandeVelde |
feat: add isOpen_setOf_affineIndependent |
From sphere-eversion.
---
[](https://gitpod.io/from-referrer/)
|
t-analysis |
15/0 |
Mathlib/Analysis/Normed/Module/FiniteDimension.lean |
1 |
1 |
['github-actions'] |
nobody |
2-26324 2 days ago |
2-26324 2 days ago |
2-26373 2 days |
| 22635 |
Kiolt author:Kiolt |
feat: submonoid of pairs with quotient in a submonoid |
This submonoid is part of the definition of toric ideals.
From Toric
---
[](https://gitpod.io/from-referrer/)
|
toric
new-contributor
t-algebra
label:t-algebra$ |
36/0 |
Mathlib.lean,Mathlib/GroupTheory/MonoidLocalization/DivPairs.lean |
2 |
10 |
['Paul-Lez', 'YaelDillies', 'erdOne', 'github-actions'] |
nobody |
2-23948 2 days ago |
2-24001 2 days ago |
28-10936 28 days |
| 23530 |
YaelDillies author:YaelDillies |
feat(devcontainer): use prebuilt Docker image |
... instead of building it every time we open a codespace. This makes opening a codespace much faster.
The image can be found here: https://hub.docker.com/r/leanprovercommunity/gitpod4. I am the one maintaining it.
---
[](https://gitpod.io/from-referrer/)
|
|
1/3 |
.devcontainer/devcontainer.json |
1 |
1 |
['github-actions'] |
nobody |
2-23069 2 days ago |
2-23131 2 days ago |
2-23119 2 days |
| 23452 |
xroblot author:xroblot |
feat(FieldTheory/Normal): A quadratic extension is normal |
---
[](https://gitpod.io/from-referrer/)
|
t-algebra label:t-algebra$ |
33/0 |
Mathlib/Algebra/Polynomial/Splits.lean,Mathlib/FieldTheory/Normal/Basic.lean |
2 |
6 |
['erdOne', 'github-actions', 'xroblot'] |
nobody |
2-20448 2 days ago |
4-975 4 days ago |
4-1023 4 days |
| 23534 |
RemyDegenne author:RemyDegenne |
feat(MeasureTheory): tightness criterion in finite dimensional inner product spaces |
In a finite-dimensional inner product space with orthonormal basis `b`, a set of measures `S` is tight if and only if the function `r ↦ ⨆ μ ∈ S, μ {x | r < |⟪b i, x⟫|}` tends to `0` at infinity for all `i`.
---
[](https://gitpod.io/from-referrer/)
|
large-import
t-measure-probability
|
94/3 |
Mathlib/Analysis/InnerProductSpace/PiL2.lean,Mathlib/MeasureTheory/Measure/Tight.lean,Mathlib/MeasureTheory/Measure/TightNormed.lean |
3 |
1 |
['github-actions'] |
nobody |
2-18471 2 days ago |
2-18553 2 days ago |
2-18596 2 days |
| 23535 |
RemyDegenne author:RemyDegenne |
feat(MeasureTheory): the map of a tight measure set by a continuous function is tight |
---
[](https://gitpod.io/from-referrer/)
|
t-measure-probability |
18/2 |
Mathlib/MeasureTheory/Measure/Tight.lean |
1 |
1 |
['github-actions'] |
nobody |
2-18013 2 days ago |
2-18487 2 days ago |
2-18475 2 days |
| 22151 |
alreadydone author:alreadydone |
feat(RingTheory): a semiprimary ring is Noetherian/Artinian iff its Jacobson radical is fg |
A key fact used is `Module.FG.smul`: if `I` is a two-sided ideal of `R` that is f.g. as a left ideal and `N` is a f.g. `R`-module, then `I • M` is also a f.g. `R`-module.
Many lemmas about coprimality of ideals are also generalized to the noncommutative, two-sided setting.
---
- [x] depends on: #21904
[](https://gitpod.io/from-referrer/)
|
t-algebra label:t-algebra$ |
216/156 |
Mathlib/Algebra/Algebra/Operations.lean,Mathlib/AlgebraicGeometry/EllipticCurve/Group.lean,Mathlib/RingTheory/Extension.lean,Mathlib/RingTheory/Finiteness/Basic.lean,Mathlib/RingTheory/Finiteness/Ideal.lean,Mathlib/RingTheory/HopkinsLevitzki.lean,Mathlib/RingTheory/Ideal/Maps.lean,Mathlib/RingTheory/Ideal/Operations.lean |
8 |
4 |
['alreadydone', 'github-actions', 'leanprover-bot', 'mathlib4-dependent-issues-bot'] |
nobody |
2-12752 2 days ago |
3-3495 3 days ago |
30-11563 30 days |
| 23549 |
bryangingechen author:bryangingechen |
chore: make dependabot group updates into a single PR |
cf. docs at https://docs.github.com/en/code-security/dependabot/dependabot-version-updates/optimizing-pr-creation-version-updates
---
It was a bit annoying to make a single bors batch for [#23544](https://github.com/leanprover-community/mathlib4/pull/23544) [#23543](https://github.com/leanprover-community/mathlib4/pull/23543) [#23541](https://github.com/leanprover-community/mathlib4/pull/23541) [#23540](https://github.com/leanprover-community/mathlib4/pull/23540). |
CI |
10/0 |
.github/dependabot.yml |
1 |
1 |
['github-actions'] |
nobody |
2-7591 2 days ago |
2-7658 2 days ago |
2-7647 2 days |
| 23513 |
erdOne author:erdOne |
feat(AlgebraicGeometry): subscheme associated to an ideal sheaf |
---
[](https://gitpod.io/from-referrer/)
|
t-algebraic-geometry |
333/15 |
Mathlib/AlgebraicGeometry/IdealSheaf.lean,Mathlib/AlgebraicGeometry/Morphisms/ClosedImmersion.lean,Mathlib/AlgebraicGeometry/Scheme.lean |
3 |
6 |
['Paul-Lez', 'github-actions'] |
nobody |
1-82952 1 day ago |
2-66463 2 days ago |
2-66466 2 days |
| 22089 |
sgouezel author:sgouezel |
feat: composing a continuous multilinear map with continuous linear maps is analytic in both variables |
Also prove that the composition of continuously polynomial functions is continuously polynomial.
---
- [x] depends on: #22102
- [x] depends on: #22789
[](https://gitpod.io/from-referrer/)
|
t-analysis |
209/3 |
Mathlib/Analysis/Analytic/CPolynomial.lean,Mathlib/Analysis/Analytic/Composition.lean,Mathlib/Analysis/NormedSpace/Multilinear/Basic.lean,Mathlib/Data/Multiset/DershowitzManna.lean,Mathlib/Order/KrullDimension.lean |
5 |
7 |
['github-actions', 'grunweg', 'mathlib4-dependent-issues-bot', 'sgouezel'] |
nobody |
1-77998 1 day ago |
1-78012 1 day ago |
40-44565 40 days |
| 22918 |
chrisflav author:chrisflav |
feat(Algebra/Module): a finite product of finitely presented modules is finitely presented |
---
[](https://gitpod.io/from-referrer/)
|
t-algebra label:t-algebra$ |
108/0 |
Mathlib/Algebra/Module/FinitePresentation.lean,Mathlib/LinearAlgebra/Pi.lean |
2 |
8 |
['chrisflav', 'erdOne', 'github-actions'] |
nobody |
1-71034 1 day ago |
2-4215 2 days ago |
19-50003 19 days |
| 23439 |
YaelDillies author:YaelDillies |
chore(SimpleGraph/Prod): correct lemma names |
The head function should come first in the name even if dot notation is used (exceptions to that are structure projections in some special cases, and infix notation).
---
[](https://gitpod.io/from-referrer/)
|
t-combinatorics |
35/18 |
Mathlib/Combinatorics/SimpleGraph/Hasse.lean,Mathlib/Combinatorics/SimpleGraph/Prod.lean |
2 |
7 |
['YaelDillies', 'b-mehta', 'eric-wieser', 'github-actions'] |
nobody |
1-69558 1 day ago |
4-83668 4 days ago |
4-83714 4 days |
| 16603 |
urkud author:urkud |
feat(Dynamics): irrational rotation is ergodic |
---
[](https://gitpod.io/from-referrer/)
|
t-dynamics |
31/0 |
Mathlib.lean,Mathlib/Dynamics/Ergodic/AddCircleAdd.lean |
2 |
n/a |
['github-actions', 'urkud'] |
nobody |
1-63050 1 day ago |
unknown |
unknown |
| 23573 |
erdOne author:erdOne |
chore(RingTheory): reduce imports of `Idempotents.lean` |
---
[](https://gitpod.io/from-referrer/)
|
t-algebra label:t-algebra$ |
12/14 |
Mathlib/RingTheory/Idempotents.lean |
1 |
1 |
['github-actions'] |
nobody |
1-51698 1 day ago |
1-51710 1 day ago |
1-51768 1 day |
| 23558 |
JovanGerb author:JovanGerb |
feat: don't delaborate to `⊔` or `⊓` if we have a `LinearOrder` |
This PR changes the `⊔` and `⊓` notations to only be used by the delaborator if the type in question is not a linear order.
This was suggested here [#mathlib4 > max and min delaborators @ 💬](https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/max.20and.20min.20delaborators/near/500701449)
---
[](https://gitpod.io/from-referrer/)
|
large-import
t-order
t-meta
|
119/8 |
Mathlib/Order/Notation.lean,MathlibTest/Delab/SupInf.lean |
2 |
28 |
['JovanGerb', 'eric-wieser', 'fpvandoorn', 'github-actions'] |
nobody |
1-46400 1 day ago |
1-68884 1 day ago |
1-80247 1 day |
| 22503 |
Kevew author:Kevew |
chore(Nat): Nat factorization multiplicity |
Ported lemmas from `Data/Nat/Multiplicity` to into a new file called `Data/Nat/Factorization/Multiplicity`, re-written in terms of `factorization`.
Also, I'm new to this so is it fine to have a lemma copied over from another file? Like, I copied over
@[simp]
theorem Prime.factorization_self {p : ℕ} (hp : Prime p) : p.factorization p = 1 := by simp [hp]
from Dat/Nat/Factorization/Basic.
---
[](https://gitpod.io/from-referrer/)
|
large-import
t-data
new-contributor
|
269/15 |
Mathlib.lean,Mathlib/Data/Nat/Factorization/Basic.lean,Mathlib/Data/Nat/Factorization/Multiplicity.lean,Mathlib/Data/Nat/Multiplicity.lean |
4 |
29 |
['Kevew', 'Paul-Lez', 'github-actions'] |
Kevew assignee:Kevew |
1-46036 1 day ago |
20-57625 20 days ago |
31-1577 31 days |
| 22279 |
xyzw12345 author:xyzw12345 |
feat(RingTheory/GradedAlgebra): homogeneous relation |
In this PR, we defined the concept of a homogeneous relation and proved some properties about homogeneous relations. The main result of this PR is showing that taking `RingQuot` by a homogeneous relation can give a graded structure on the quotient ring. This result can be used to define graded structures on rings obtained using `RingQuot`, e.g. the Symmetric Algebra defined in #21539 can be verified to have such a structure.
Co-authored-by:
Zhixuan Dai @atstarrysky <22300180006@m.fudan.edu.cn>
Yiming Fu @pelicanhere
Zhenyan Fu @pumpkin678
Raphael Douglas Giles @Raph-DG
Jiedong Jiang @jjdishere
- [x] depends on: #22354
---
[](https://gitpod.io/from-referrer/)
|
new-contributor
t-algebra
label:t-algebra$ |
455/0 |
Mathlib.lean,Mathlib/Algebra/Algebra/Equiv.lean,Mathlib/Algebra/DirectSum/Basic.lean,Mathlib/Algebra/DirectSum/Module.lean,Mathlib/Algebra/Module/LinearMap/Defs.lean,Mathlib/Algebra/RingQuot.lean,Mathlib/RingTheory/GradedAlgebra/Basic.lean,Mathlib/RingTheory/GradedAlgebra/HomogeneousRelation.lean |
8 |
6 |
['Paul-Lez', 'github-actions', 'mathlib4-dependent-issues-bot', 'ocfnash', 'xyzw12345'] |
nobody |
1-38531 1 day ago |
1-38534 1 day ago |
2-70328 2 days |
| 23496 |
chrisflav author:chrisflav |
chore(Algebra): the five lemma for modules |
We reprove the five lemma for modules for universe generality, avoiding the import of `Mathlib.CategoryTheory.Abelian.DiagramLemmas.Four` in otherwise non-category-theoretic files and for ease of application.
---
See #23497 for a golf using this.
[](https://gitpod.io/from-referrer/)
|
t-algebra label:t-algebra$ |
158/0 |
Mathlib.lean,Mathlib/Algebra/FiveLemma.lean |
2 |
7 |
['acmepjz', 'chrisflav', 'erdOne', 'github-actions'] |
nobody |
1-37889 1 day ago |
3-13536 3 days ago |
3-13524 3 days |
| 23580 |
FR-vdash-bot author:FR-vdash-bot |
chore(GroupTheory/Commensurable): remove a `Subgroup.toSubmonoid` |
It's mistranslation. It's `Subgroup.carrier` in mathlib3, but I think there should just be a coeSort here without any additional conversion.
---
[](https://gitpod.io/from-referrer/)
|
t-algebra label:t-algebra$ |
1/1 |
Mathlib/GroupTheory/Commensurable.lean |
1 |
1 |
['github-actions'] |
nobody |
1-27183 1 day ago |
1-27255 1 day ago |
1-27243 1 day |
| 22392 |
mariainesdff author:mariainesdff |
feat(Algebra/Order/Antidiag/Partition): add antidiagonalTwoTwo |
Co-authored-by: AntoineChambert-Loir
---
[](https://gitpod.io/from-referrer/)
|
t-algebra label:t-algebra$ |
59/0 |
Mathlib.lean,Mathlib/Algebra/Order/Antidiag/Partition.lean,Mathlib/Algebra/Order/Antidiag/Prod.lean |
3 |
3 |
['github-actions', 'j-loreaux', 'mariainesdff'] |
nobody |
1-25685 1 day ago |
29-9058 29 days ago |
29-50152 29 days |
| 23574 |
Parcly-Taxel author:Parcly-Taxel |
chore: split `Topology.ContinuousMap.Bounded.Basic` |
Split off
* `Topology.ContinuousMap.Bounded.Normed`, showing that normed algebraic structures can be inherited by bounded continuous functions
* `Topology.ContinuousMap.Bounded.Ascoli`, containing the Arzelà–Ascoli theorem |
tech debt
t-topology
|
742/741 |
Mathlib.lean,Mathlib/Analysis/Normed/Lp/LpEquiv.lean,Mathlib/Analysis/SpecialFunctions/MulExpNegMulSq.lean,Mathlib/MeasureTheory/Integral/BoundedContinuousFunction.lean,Mathlib/Topology/ContinuousMap/Bounded/Ascoli.lean,Mathlib/Topology/ContinuousMap/Bounded/Basic.lean,Mathlib/Topology/ContinuousMap/Bounded/Normed.lean,Mathlib/Topology/ContinuousMap/Bounded/Star.lean,Mathlib/Topology/ContinuousMap/BoundedCompactlySupported.lean,Mathlib/Topology/MetricSpace/GromovHausdorffRealized.lean,Mathlib/Topology/TietzeExtension.lean |
11 |
4 |
['Parcly-Taxel', 'github-actions', 'jcommelin'] |
nobody |
1-21337 1 day ago |
1-50957 1 day ago |
1-50945 1 day |
| 23529 |
Parcly-Taxel author:Parcly-Taxel |
chore: split `Data.Ordmap.Ordset` |
The constituent parts of the invariant have been pushed backwards to `Data.Ordmap.Invariants`. The bundled `Valid` predicate and `Ordset` itself remain in place. |
t-data
tech debt
|
855/844 |
Mathlib.lean,Mathlib/Data/Ordmap/Invariants.lean,Mathlib/Data/Ordmap/Ordset.lean |
3 |
1 |
['github-actions'] |
nobody |
1-21307 1 day ago |
2-24554 2 days ago |
2-24542 2 days |
| 23531 |
fpvandoorn author:fpvandoorn |
refactor: generalize `unbounded_of_tendsto_atTop` |
---
Not sure if I like this style of proofs with `aesop` for future PRs. It's short, though.
[](https://gitpod.io/from-referrer/)
|
t-topology |
13/19 |
Mathlib/Order/Filter/AtTopBot/Basic.lean |
1 |
2 |
['github-actions', 'sgouezel'] |
nobody |
1-18194 1 day ago |
2-20628 2 days ago |
2-20616 2 days |
| 23408 |
faenuccio author:faenuccio |
feat(RingTheory/Valuation): add two lemmas about non-units in valuation subrings |
co-authored with María Inés de Frutos Fernández @mariainesdff |
t-algebra
t-number-theory
label:t-algebra$ |
11/0 |
Mathlib/RingTheory/Valuation/Integers.lean,Mathlib/RingTheory/Valuation/ValuationSubring.lean |
2 |
1 |
['github-actions', 'pechersky'] |
nobody |
1-17791 1 day ago |
5-82946 5 days ago |
5-82936 5 days |
| 19666 |
FR-vdash-bot author:FR-vdash-bot |
chore: redefine `Nat.bit` |
---
split from #13649
[](https://gitpod.io/from-referrer/)
|
t-data |
4/4 |
Mathlib/Data/Nat/BinaryRec.lean,Mathlib/Data/Nat/Bitwise.lean |
2 |
7 |
['FR-vdash-bot', 'TwoFX', 'girving', 'github-actions', 'kbuzzard', 'kim-em'] |
nobody |
1-16359 1 day ago |
1-16407 1 day ago |
64-69983 64 days |
| 23584 |
mariainesdff author:mariainesdff |
chore(RingTheory/Valuation/Extension): rename IsValExtension to Valuation.IsExtension |
This change is to remove `IsValExtension` from the root namespace and to allow dot notation.
---
[](https://gitpod.io/from-referrer/)
|
t-algebra label:t-algebra$ |
21/15 |
Mathlib.lean,Mathlib/RingTheory/Valuation/Extension.lean |
2 |
3 |
['erdOne', 'github-actions', 'mariainesdff'] |
nobody |
1-12057 1 day ago |
1-22087 1 day ago |
1-22136 1 day |
| 23589 |
faenuccio author:faenuccio |
feat(Group/Subgroup/Lattice): the top subgroup is nontrivial when the group is nontrivial, as instance |
|
t-order
t-algebra
label:t-algebra$ |
5/0 |
Mathlib/Algebra/Group/Subgroup/Lattice.lean |
1 |
1 |
['github-actions'] |
nobody |
1-11691 1 day ago |
1-11753 1 day ago |
1-11744 1 day |
| 21182 |
joneugster author:joneugster |
fix(Util/CountHeartbeats): move elaboration in #count_heartbeats inside a namespace |
Currently the `#count_heartbeat` linter reported the heartbeats until it concluded `error: [declaration] has already been declared` instead of re-elaborating the declaration.
---
[Zulip report](https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/count_heartbeats.20for.20all.20declarations.20in.20a.20file.3F/near/496303652)
[](https://gitpod.io/from-referrer/)
|
t-meta |
72/5 |
Mathlib/Util/CountHeartbeats.lean,MathlibTest/CountHeartbeats.lean |
2 |
16 |
['adomani', 'github-actions', 'joneugster', 'mathlib-bors'] |
nobody |
1-10389 1 day ago |
1-10874 1 day ago |
3-44281 3 days |
| 18754 |
FR-vdash-bot author:FR-vdash-bot |
feat: `IsometryClass` |
---
- [ ] depends on: #18689
[](https://gitpod.io/from-referrer/)
|
t-topology |
99/3 |
Mathlib/Analysis/Normed/Group/Uniform.lean,Mathlib/Topology/MetricSpace/Isometry.lean,scripts/nolints_prime_decls.txt |
3 |
2 |
['github-actions', 'j-loreaux', 'mathlib4-dependent-issues-bot'] |
nobody |
1-10330 1 day ago |
1-10330 1 day ago |
25-64329 25 days |
| 22605 |
pechersky author:pechersky |
chore(Analysis): rename pi family from π to X |
Only in files that mentioned such a family, via a script:
```
git grep -e "π : . → Type" --name-only | rg "Analysis" | xargs -I{} sed -i -e 's/π/X/g' {}
```
---
[](https://gitpod.io/from-referrer/)
|
tech debt
t-analysis
|
36/36 |
Mathlib/Analysis/Convex/Extreme.lean,Mathlib/Analysis/Convex/Segment.lean,Mathlib/Analysis/Normed/Group/Constructions.lean,Mathlib/Analysis/Normed/Ring/Lemmas.lean |
4 |
1 |
['github-actions'] |
nobody |
1-9524 1 day ago |
1-9524 1 day ago |
21-70129 21 days |
| 22974 |
YaelDillies author:YaelDillies |
refactor: use a junk value for the analytic order of a non-analytic function |
Currently, the order of an analytic function is called `AnalyticAt.order` and has a single explicit argument `hf : AnalyticAt 𝕜 f z₀`. This means that working with analytic functions results in contexts full of `hf.order` or, worse, `⋯.order`.
This PR makes the `f` and `z₀` arguments explicit, and drops the `hf` one by introducing a junk value of `0` for non-analytic functions. The resulting function is called `eanalyticOrderAt` and I am also adding a `Nat`-valued version `analyticOrderAt` since `(eanalyticOrderAt f z₀).toNat` was appearing in quite a few lemmas.
---
The same change could be performed for meromorphic functions once you are convinced.
[](https://gitpod.io/from-referrer/)
|
t-analysis |
187/101 |
Mathlib/Analysis/Analytic/Order.lean,Mathlib/Analysis/Meromorphic/NormalForm.lean,Mathlib/Analysis/Meromorphic/Order.lean,Mathlib/Data/ENat/Basic.lean |
4 |
2 |
['github-actions', 'urkud'] |
nobody |
1-8131 1 day ago |
1-8145 1 day ago |
15-55861 15 days |
| 23562 |
YaelDillies author:YaelDillies |
feat: the essential image of a finite product-preserving functor is cartesian-monoidal |
From Toric
---
[](https://gitpod.io/from-referrer/)
|
toric
t-category-theory
|
57/4 |
Mathlib/CategoryTheory/ChosenFiniteProducts.lean |
1 |
11 |
['YaelDillies', 'b-mehta', 'erdOne', 'github-actions', 'joelriou'] |
nobody |
1-7457 1 day ago |
1-31227 1 day ago |
1-65660 1 day |
| 22881 |
Champitoad author:Champitoad |
feat(CategoryTheory/Topos): add representability results for subobject classifier |
We add a section `Representability` at the end of `Mathlib.CategoryTheory.Topos.Classifier` where we formalize the necessary lemmas and definitions that lead to the proof of `CategoryTheory.isRepresentable_hasClassifier_iff`, which states that a category `C` has a subobject classifier if and only if the subobjects presheaf `CategoryTheory.Subobject.presheaf C` is representable (Proposition 1 in Section I.3 of Sheaves in Geometry and Logic [MM92]). The toughest part is found in definition `CategoryTheory.Classifier.fromRepresentation`, which formalizes as closely as possible the argument given in [MM92, pp. 33-34].
---
[](https://gitpod.io/from-referrer/)
|
large-import
new-contributor
t-category-theory
|
251/22 |
Mathlib/CategoryTheory/Subobject/Basic.lean,Mathlib/CategoryTheory/Subobject/Presheaf.lean,Mathlib/CategoryTheory/Topos/Classifier.lean |
3 |
21 |
['Champitoad', 'github-actions', 'joelriou'] |
nobody |
1-4796 1 day ago |
1-4796 1 day ago |
15-24804 15 days |
| 23339 |
joelriou author:joelriou |
feat(CategoryTheory): the colimit type of a functor to types |
Given a category `J` (with `J : Type u` and `[Category.{v} J]`) and a functor `F : J ⥤ Type w`, we introduce a type `F.ColimitType : Type (max u w)`, which satisfies a certain universal property of the colimit: it is defined as a suitable quotient of `Σ j, F.obj j`. This universal property is not expressed in a categorical way (as in general `Type (max u w)` is not the same as `Type u`).
(This type `F.ColimitType` is basically the same as `CategoryTheory.Limits.Types.Quot` that is defined in `CategoryTheory.Limits.Types`, but we expand the API (with minimal imports to category theory) so that it may be used in future PRs to refactor both `DirectedSystem` and the construction of colimits in `Type`.)
---
[](https://gitpod.io/from-referrer/)
|
t-category-theory |
272/0 |
Mathlib.lean,Mathlib/CategoryTheory/Limits/Types/ColimitType.lean |
2 |
3 |
['AntoineChambert-Loir', 'github-actions', 'joelriou'] |
nobody |
0-84068 23 hours ago |
0-84082 23 hours ago |
7-67224 7 days |
| 23282 |
joelriou author:joelriou |
feat(CategoryTheory): monomorphisms in Type are stable under transfinite compositions |
`monomorphisms (Type u)` is stable under cobase change, filtered colimits and transfinite compositions.
(The file `CategoryTheory.Types` is also moved to `CategoryTheory.Types.Basic`.)
(This is extended to presheaves of types in #23298.)
---
[](https://gitpod.io/from-referrer/)
|
t-category-theory |
159/15 |
Mathlib.lean,Mathlib/CategoryTheory/Category/Cat.lean,Mathlib/CategoryTheory/Category/RelCat.lean,Mathlib/CategoryTheory/ConcreteCategory/Basic.lean,Mathlib/CategoryTheory/ConcreteCategory/EpiMono.lean,Mathlib/CategoryTheory/Core.lean,Mathlib/CategoryTheory/Functor/Hom.lean,Mathlib/CategoryTheory/IsomorphismClasses.lean,Mathlib/CategoryTheory/Limits/Types/Shapes.lean,Mathlib/CategoryTheory/Monad/Types.lean,Mathlib/CategoryTheory/MorphismProperty/TransfiniteComposition.lean,Mathlib/CategoryTheory/SmallObject/WellOrderInductionData.lean,Mathlib/CategoryTheory/Subobject/Types.lean,Mathlib/CategoryTheory/Types/Basic.lean,Mathlib/CategoryTheory/Types/Monomorphisms.lean,Mathlib/CategoryTheory/UnivLE.lean,Mathlib/Control/Fold.lean,Mathlib/Data/Set/FunctorToTypes.lean |
18 |
1 |
['github-actions'] |
nobody |
0-83748 23 hours ago |
0-84740 23 hours ago |
9-63603 9 days |
| 21080 |
loefflerd author:loefflerd |
feat(Topology/UniformSpace): uniform approximation by locally constant functions |
Show that any function from a profinite space to a uniform space can be uniformly approximated by linear combinations of indicator functions of clopen sets.
---
- [x] depends on: #20687
- [x] depends on: #21079
[](https://gitpod.io/from-referrer/)
|
t-topology |
127/0 |
Mathlib.lean,Mathlib/Topology/Sets/Closeds.lean,Mathlib/Topology/UniformSpace/CoveringProfinite.lean |
3 |
24 |
['faenuccio', 'github-actions', 'loefflerd', 'mathlib4-dependent-issues-bot', 'urkud'] |
nobody |
0-82385 22 hours ago |
30-71892 30 days ago |
30-72827 30 days |
| 23592 |
YaelDillies author:YaelDillies |
chore(Order/Minimal): don't import `CompleteLattice` |
Achieve this by:
* splitting `Order.Chain` into `Order.CompleteLattice.Chain` for the material requiring `CompleteLattice` and `Order.Preorder.Chain` for the rest.
* turning an import around between `Order.Minimal` and `Order.UpperLower.Closure`
---
[](https://gitpod.io/from-referrer/)
|
t-order |
144/113 |
Counterexamples/AharoniKorman.lean,Mathlib.lean,Mathlib/Data/Fin/FlagRange.lean,Mathlib/Data/Matroid/Basic.lean,Mathlib/Order/Antichain.lean,Mathlib/Order/Birkhoff.lean,Mathlib/Order/CompleteLattice/Chain.lean,Mathlib/Order/Minimal.lean,Mathlib/Order/OmegaCompletePartialOrder.lean,Mathlib/Order/Preorder/Chain.lean,Mathlib/Order/UpperLower/Closure.lean,Mathlib/Order/Zorn.lean |
12 |
1 |
['github-actions'] |
nobody |
0-81941 22 hours ago |
0-81941 22 hours ago |
0-85083 23 hours |
| 23599 |
mistarro author:mistarro |
feat(FieldTheory): formula for `minpoly F (iterateFrobenius E q n a)` for separable `a` |
---
[](https://gitpod.io/from-referrer/)
|
t-algebra label:t-algebra$ |
26/0 |
Mathlib/FieldTheory/PurelyInseparable/PerfectClosure.lean |
1 |
1 |
['github-actions'] |
nobody |
0-78391 21 hours ago |
0-78391 21 hours ago |
0-78441 21 hours |
| 23596 |
YaelDillies author:YaelDillies |
feat: typeclass for subgroups of finite relative index |
From FLT
---
[](https://gitpod.io/from-referrer/)
|
FLT
t-algebra
label:t-algebra$ |
45/16 |
Mathlib/GroupTheory/Complement.lean,Mathlib/GroupTheory/CosetCover.lean,Mathlib/GroupTheory/Index.lean |
3 |
1 |
['github-actions'] |
nobody |
0-77775 21 hours ago |
0-82272 22 hours ago |
0-82320 22 hours |
| 23455 |
urkud author:urkud |
feat: ergodic measures as extereme points |
---
- [ ] depends on: #23462
[](https://gitpod.io/from-referrer/)
|
t-dynamics
t-measure-probability
|
111/0 |
Mathlib.lean,Mathlib/Dynamics/Ergodic/Extreme.lean |
2 |
2 |
['github-actions', 'mathlib4-dependent-issues-bot'] |
nobody |
0-74143 20 hours ago |
0-74603 20 hours ago |
0-82048 22 hours |
| 22904 |
YaelDillies author:YaelDillies |
feat: additivise `Irreducible` |
In the Toric project, we need to talk about (additive) irreducible elements of a lattice cone (they generate the cone). There is no definition of additive irreducible elements in mathlib, but luckily the existing definition of multiplicative irreducible elements talks about general monoids (instead of merely monoids with zero).
This PR additivises all the API, except for the parts about divisibility and monoids with zero, and moves it to a new file under `Algebra.Group`. Also rename the fields of `Irreducible` to make them additivisable.
Moves:
* `Irreducible.not_unit` -> `Irreducible.not_isUnit`
* `Irreducible.isUnit_or_isUnit'` -> `Irreducible.isUnit_or_isUnit`
From Toric
---
[](https://gitpod.io/from-referrer/)
|
toric
t-algebra
label:t-algebra$ |
227/188 |
Mathlib.lean,Mathlib/Algebra/CharP/Algebra.lean,Mathlib/Algebra/Group/Irreducible/Defs.lean,Mathlib/Algebra/Group/Irreducible/Lemmas.lean,Mathlib/Algebra/GroupWithZero/Associated.lean,Mathlib/Algebra/Polynomial/Eval/Irreducible.lean,Mathlib/Algebra/Polynomial/FieldDivision.lean,Mathlib/Algebra/Polynomial/Monic.lean,Mathlib/Algebra/Prime/Defs.lean,Mathlib/Algebra/Prime/Lemmas.lean,Mathlib/Algebra/Squarefree/Basic.lean,Mathlib/Data/Nat/Prime/Defs.lean,Mathlib/Data/Nat/Squarefree.lean,Mathlib/FieldTheory/KummerPolynomial.lean,Mathlib/FieldTheory/Separable.lean,Mathlib/NumberTheory/FactorisationProperties.lean,Mathlib/NumberTheory/SumTwoSquares.lean,Mathlib/RingTheory/DedekindDomain/Ideal.lean,Mathlib/RingTheory/DiscreteValuationRing/Basic.lean,Mathlib/RingTheory/Ideal/Norm/AbsNorm.lean,Mathlib/RingTheory/Polynomial/GaussLemma.lean,Mathlib/RingTheory/Polynomial/IrreducibleRing.lean,Mathlib/RingTheory/UniqueFactorizationDomain/Basic.lean,Mathlib/RingTheory/UniqueFactorizationDomain/Defs.lean,Mathlib/RingTheory/UniqueFactorizationDomain/Multiplicity.lean,Mathlib/SetTheory/Cardinal/Divisibility.lean,Mathlib/Tactic/ToAdditive/Frontend.lean,Mathlib/Topology/Algebra/Valued/LocallyCompact.lean |
28 |
2 |
['Ruben-VandeVelde', 'github-actions'] |
nobody |
0-71663 19 hours ago |
7-22610 7 days ago |
19-7781 19 days |
| 23594 |
YaelDillies author:YaelDillies |
refactor: merge `DomMulAct` and `DomAddAct` into `DomAct` |
This has several advantages:
* Less API surface with a single definition instead of two
* Better match the existing `ConjAct` type synonym
* We get to use a better name for the multiplication by an element of the type synonym: Previously `dmaSMul`, now `domSMul`.
and no inconvenient because the instances for `DomMulAct` and `DomAddAct` are by definition disjoint.
---
[](https://gitpod.io/from-referrer/)
|
|
337/335 |
Mathlib.lean,Mathlib/Algebra/Group/Translate.lean,Mathlib/Algebra/Module/CharacterModule.lean,Mathlib/Algebra/Module/Hom.lean,Mathlib/Algebra/Module/LinearMap/Basic.lean,Mathlib/Algebra/Module/LinearMap/Defs.lean,Mathlib/GroupTheory/GroupAction/DomAct/ActionHom.lean,Mathlib/GroupTheory/GroupAction/DomAct/Basic.lean,Mathlib/GroupTheory/Perm/Centralizer.lean,Mathlib/GroupTheory/Perm/DomAct.lean,Mathlib/MeasureTheory/Function/AEEqFun/DomAct.lean,Mathlib/MeasureTheory/Function/LpSpace/DomAct/Basic.lean,Mathlib/MeasureTheory/Function/LpSpace/DomAct/Continuous.lean,Mathlib/MeasureTheory/Group/MeasurableEquiv.lean,Mathlib/Topology/Algebra/Constructions/DomAct.lean,Mathlib/Topology/Algebra/Constructions/DomMulAct.lean |
16 |
3 |
['eric-wieser', 'github-actions', 'urkud'] |
nobody |
0-66940 18 hours ago |
1-1855 1 day ago |
1-1844 1 day |
| 23244 |
eric-wieser author:eric-wieser |
chore(GroupTheory/Congruence): deduplicate `ker` and `mulKer` |
This deprecates `Con.mulKer` and defines it in terms of `ker` (instead of vice versa).
It's not entirely clear to me that `MulHomClass` is the way to go due to a lack of a coherent simp-normal form, but we can always switch to `MulHom` later.
The signature of `Con.mapOfSurjective` has changed as a result.
Zulip thread: [#mathlib4 > Con.ker vs Con.mulKer @ 💬](https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/Con.2Eker.20vs.20Con.2EmulKer/near/505847217)
---
[](https://gitpod.io/from-referrer/)
This is cleanup on the way to defining `RingCon.ker`. |
t-algebra label:t-algebra$ |
115/86 |
Mathlib/GroupTheory/Congruence/Defs.lean,Mathlib/GroupTheory/Congruence/Hom.lean |
2 |
1 |
['github-actions'] |
nobody |
0-65138 18 hours ago |
10-64736 10 days ago |
10-64784 10 days |
| 22078 |
Louddy author:Louddy |
feat(SkewMonoidAlgebra): multiplication and algebraic instances |
# Multiplication and Algebraic Instances
In this PR, we introduce the definition of the skewed convolution product on `SkewMonoidAlgebra k G`. Here, the product of two elements `f g : SkewMonoidAlgebra k G` is the finitely supported function whose value at `a` is the sum of `f x * (x • g y)` over all pairs `x, y` such that `x * y = a`.
We also introduce the associated algebraic instances.
## Context
This is the third part of a planned series of PRs aiming to formalise skew monoid algebras.
The PRs are split to ease the review process. The moral sum of these planned PRs is #10541.
The first and second part were #15878 and #19084.
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/)
|
large-import
new-contributor
t-algebra
label:t-algebra$ |
397/15 |
Mathlib/Algebra/SkewMonoidAlgebra/Basic.lean |
1 |
37 |
['AntoineChambert-Loir', 'Louddy', 'github-actions', 'kbuzzard'] |
nobody |
0-64219 17 hours ago |
1-4365 1 day ago |
36-42445 36 days |
| 23365 |
vasnesterov author:vasnesterov |
feat(Tactic/Simproc): nested quantifiers in `existsAndEq` |
Generalize the `existsAndEq` simproc to nested existential quantifiers.
For example `∃ a, p a ∧ ∃ b, a = f b ∧ q b` now simplifies to `∃ b, p (f b) ∧ q b`.
---
[](https://gitpod.io/from-referrer/)
|
large-import
t-meta
|
462/2 |
Mathlib.lean,Mathlib/Tactic.lean,Mathlib/Tactic/Basic.lean,Mathlib/Tactic/Simproc/ExistsAndEq.lean,Mathlib/Tactic/Simproc/ExistsAndEqNested.lean,MathlibTest/Simproc/ExistsAndEq.lean,scripts/noshake.json |
7 |
37 |
['JovanGerb', 'b-mehta', 'eric-wieser', 'github-actions', 'leanprover-bot', 'leanprover-community-mathlib4-bot', 'vasnesterov'] |
nobody |
0-61058 16 hours ago |
0-61059 16 hours ago |
6-1306 6 days |
| 17802 |
vihdzp author:vihdzp |
feat(SetTheory/Ordinal/Veblen): epsilon and gamma ordinals |
We define the epsilon function `ε_ o = veblen 1 o`, and the gamma function `Γ_ o` which enumerates the fixed points of `veblen · 0`.
---
- [x] depends on: #17751
- [x] depends on: #18611
[](https://gitpod.io/from-referrer/)
|
t-set-theory
maintainer-merge
|
146/7 |
Mathlib/SetTheory/Ordinal/FixedPoint.lean,Mathlib/SetTheory/Ordinal/Veblen.lean |
2 |
15 |
['YaelDillies', 'github-actions', 'mathlib4-dependent-issues-bot', 'vihdzp'] |
nobody |
0-53235 14 hours ago |
0-53235 14 hours ago |
32-65625 32 days |
| 20887 |
alreadydone author:alreadydone |
feat(Algebra): Transcendence degree |
Define transcendence degree `Algebra.trdeg` and proves some basic properties:
In **AlgebraicIndependent/Basic.lean**: define `Algebra.trdeg` to be the supremum of the cardinalities of all AlgebraicIndependent sets, just like `Module.rank` is defined to be the supremum of the cardinalities of all LinearIndependent sets. Add some API lemmas and trivial results about `trdeg`, e.g. that injective/surjective AlgHoms induce inequalities between `trdeg`s, and AlgEquivs induce equalities.
In **AlgebraicIndependent/Transcendental.lean**: add API lemmas and show the inequality `trdeg R S + trdeg S A ≤ trdeg R A` (which does not require a domain).
In **AlgebraicIndependent/Defs.lean**: add Stacks tags and some trivial API lemmas about IsTranscendenceBasis.
Thanks to Chris Hughes and Jz Pan for preliminary works and Peter Nelson for the hint about Finitary and IndepMatroid.
TODO:
+ [The analogue of StrongRankCondition](https://mathoverflow.net/a/484564) in the setting of algebras, which implies `trdeg R (MvPolynomial (Fin n) R) = n` for all Nontrivial CommRing R.
---
- [x] depends on: #20888
- [x] depends on: #21512
- [x] depends on: #21566
[](https://gitpod.io/from-referrer/)
|
maintainer-merge
t-algebra
label:t-algebra$ |
317/51 |
Mathlib/RingTheory/Algebraic/Integral.lean,Mathlib/RingTheory/AlgebraicIndependent/Basic.lean,Mathlib/RingTheory/AlgebraicIndependent/Defs.lean,Mathlib/RingTheory/AlgebraicIndependent/TranscendenceBasis.lean,Mathlib/RingTheory/AlgebraicIndependent/Transcendental.lean |
5 |
59 |
['acmepjz', 'alreadydone', 'apnelson1', 'erdOne', 'github-actions', 'mathlib4-dependent-issues-bot'] |
nobody |
0-48513 13 hours ago |
0-48513 13 hours ago |
35-47437 35 days |
| 23615 |
j-loreaux author:j-loreaux |
feat: alias `Filter.Tendsto.squeeze` for the Squeeze Theorem |
---
[](https://gitpod.io/from-referrer/)
|
t-topology
easy
|
4/0 |
Mathlib/Topology/Order/Basic.lean |
1 |
1 |
['github-actions'] |
nobody |
0-46846 13 hours ago |
0-46889 13 hours ago |
0-46898 13 hours |
| 23616 |
urkud author:urkud |
chore(MeasureTheory/Decomposition): split signed&unsigned |
Move files from `MeasureTheory/Decomposition` to either `MeasureTheory/Measure/Decomposition` or `MeasureTheory/VectorMeasure/Decomposition`.
---
I'm trying to sort material in `MeasureTheory/` by the "main object" (`MeasurableSpace` < `OuterMeasure` < `Measure` < `VectorMeasure`), not yet sure how different integrals fit the picture.
[](https://gitpod.io/from-referrer/)
|
t-measure-probability |
29/29 |
Mathlib.lean,Mathlib/Dynamics/Ergodic/RadonNikodym.lean,Mathlib/InformationTheory/KullbackLeibler/Basic.lean,Mathlib/InformationTheory/KullbackLeibler/KLFun.lean,Mathlib/MeasureTheory/Covering/Differentiation.lean,Mathlib/MeasureTheory/Function/ConditionalExpectation/Real.lean,Mathlib/MeasureTheory/Measure/Decomposition/Exhaustion.lean,Mathlib/MeasureTheory/Measure/Decomposition/Hahn.lean,Mathlib/MeasureTheory/Measure/Decomposition/IntegralRNDeriv.lean,Mathlib/MeasureTheory/Measure/Decomposition/Lebesgue.lean,Mathlib/MeasureTheory/Measure/Decomposition/RadonNikodym.lean,Mathlib/MeasureTheory/Measure/Tilted.lean,Mathlib/MeasureTheory/Measure/WithDensity.lean,Mathlib/MeasureTheory/Measure/WithDensityFinite.lean,Mathlib/MeasureTheory/VectorMeasure/Basic.lean,Mathlib/MeasureTheory/VectorMeasure/Decomposition/Hahn.lean,Mathlib/MeasureTheory/VectorMeasure/Decomposition/Jordan.lean,Mathlib/MeasureTheory/VectorMeasure/Decomposition/Lebesgue.lean,Mathlib/Probability/Density.lean,Mathlib/Probability/Kernel/Composition/MeasureCompProd.lean,Mathlib/Probability/Kernel/Disintegration/CondCDF.lean,Mathlib/Probability/Notation.lean,scripts/noshake.json |
23 |
1 |
['github-actions'] |
nobody |
0-46051 12 hours ago |
0-46164 12 hours ago |
0-46164 12 hours |
| 19946 |
vihdzp author:vihdzp |
feat(SetTheory/ZFC/Basic): order instances |
Sets form a partial order under the subset relation.
---
[](https://gitpod.io/from-referrer/)
|
t-set-theory |
38/2 |
Mathlib/SetTheory/ZFC/Basic.lean,Mathlib/SetTheory/ZFC/Class.lean,Mathlib/SetTheory/ZFC/PSet.lean |
3 |
8 |
['alreadydone', 'b-mehta', 'github-actions', 'vihdzp'] |
nobody |
0-37453 10 hours ago |
0-41815 11 hours ago |
31-42547 31 days |
| 23370 |
kebekus author:kebekus |
feat: taking the divisor of a meromorphic function commutes with restriction |
Deliver on a very simple TODO, show that taking the divisor of a meromorphic function commutes with restriction.
This material is used in [Project VD](https://github.com/kebekus/ProjectVD), which aims to formalize Value Distribution Theory for meromorphic functions on the complex plane.
---
[](https://gitpod.io/from-referrer/)
|
t-analysis |
12/1 |
Mathlib/Analysis/Meromorphic/Divisor.lean |
1 |
1 |
['github-actions'] |
nobody |
0-33751 9 hours ago |
0-33766 9 hours ago |
7-12327 7 days |
| 23363 |
kebekus author:kebekus |
feat: congruence lemmas for divisors of meromorphic functions |
Deliver on open TODO and state elementary congruence lemmas for divisors of meromorphic functions.
This material is used in [Project VD](https://github.com/kebekus/ProjectVD), which aims to formalize Value Distribution Theory for meromorphic functions on the complex plane.
---
[](https://gitpod.io/from-referrer/)
|
t-analysis |
78/1 |
Mathlib/Analysis/Meromorphic/Basic.lean,Mathlib/Analysis/Meromorphic/Divisor.lean |
2 |
1 |
['github-actions'] |
nobody |
0-33509 9 hours ago |
0-33524 9 hours ago |
7-24571 7 days |
| 22631 |
Thmoas-Guan author:Thmoas-Guan |
feat(Algebra): define associated graded structure for abelian group |
In this PR we define the associated graded structure for abelian group when given a filtration and only give some basic lemmas about it.
Further results would be given in #20913
---
[](https://gitpod.io/from-referrer/)
|
t-algebra label:t-algebra$ |
155/0 |
Mathlib.lean,Mathlib/RingTheory/FilteredAlgebra/AssociatedGraded.lean |
2 |
6 |
['Thmoas-Guan', 'eric-wieser', 'github-actions', 'kbuzzard'] |
nobody |
0-31044 8 hours ago |
28-17713 28 days ago |
28-17758 28 days |
| 22932 |
YaelDillies author:YaelDillies |
feat: the product of finitely generated monoids is finitely generated |
From Toric
Co-authored-by: Patrick Luo
---
- [x] depends on: #22937
[](https://gitpod.io/from-referrer/)
|
toric
t-algebra
label:t-algebra$ |
48/27 |
Mathlib/GroupTheory/Finiteness.lean,Mathlib/RingTheory/FiniteType.lean |
2 |
7 |
['YaelDillies', 'b-mehta', 'github-actions', 'mathlib4-dependent-issues-bot'] |
nobody |
0-30744 8 hours ago |
0-30807 8 hours ago |
19-33278 19 days |
| 23448 |
Parcly-Taxel author:Parcly-Taxel |
chore: fix more induction branch names |
Follow-up to #23358. This includes changing the name of the motive variable to `motive` and naming branches as if they were lemmas.
The regex used for finding the branch names was `^\s+\| [hH][^:]*? =>`. |
tech debt |
235/233 |
Mathlib/Algebra/Algebra/Operations.lean,Mathlib/Algebra/BigOperators/Finsupp/Basic.lean,Mathlib/Algebra/BigOperators/GroupWithZero/Action.lean,Mathlib/Algebra/Category/ModuleCat/Adjunctions.lean,Mathlib/Algebra/Group/Submonoid/Basic.lean,Mathlib/Algebra/Group/Submonoid/Membership.lean,Mathlib/Algebra/Group/Submonoid/Pointwise.lean,Mathlib/Algebra/Lie/Submodule.lean,Mathlib/Algebra/Lie/TraceForm.lean,Mathlib/Algebra/Lie/Weights/Chain.lean,Mathlib/Algebra/Lie/Weights/Killing.lean,Mathlib/Algebra/Module/Presentation/RestrictScalars.lean,Mathlib/Algebra/Module/Submodule/Lattice.lean,Mathlib/Algebra/Polynomial/Module/Basic.lean,Mathlib/Analysis/SpecialFunctions/Log/PosLog.lean,Mathlib/Data/Finset/Insert.lean,Mathlib/Data/Finsupp/Basic.lean,Mathlib/Data/Finsupp/Single.lean,Mathlib/LinearAlgebra/CliffordAlgebra/Grading.lean,Mathlib/LinearAlgebra/DirectSum/Finsupp.lean,Mathlib/LinearAlgebra/Finsupp/LinearCombination.lean,Mathlib/LinearAlgebra/Span/Basic.lean,Mathlib/LinearAlgebra/Span/Defs.lean,Mathlib/MeasureTheory/Integral/Bochner.lean,Mathlib/RingTheory/FreeCommRing.lean,Mathlib/RingTheory/Ideal/Maps.lean,Mathlib/RingTheory/Kaehler/Polynomial.lean,Mathlib/RingTheory/MvPolynomial/Symmetric/FundamentalTheorem.lean,Mathlib/RingTheory/UniqueFactorizationDomain/Defs.lean |
29 |
1 |
['github-actions'] |
nobody |
0-29468 8 hours ago |
0-29508 8 hours ago |
4-23135 4 days |
| 23624 |
YaelDillies author:YaelDillies |
chore(Order/Basic): order lemmas according to `Preorder`/`PartialOrder`/`LinearOrder` |
This way, it is much easier to know where to add new lemmas.
---
[](https://gitpod.io/from-referrer/)
|
t-order |
254/342 |
Mathlib/Order/Basic.lean |
1 |
1 |
['github-actions'] |
nobody |
0-27954 7 hours ago |
0-27954 7 hours ago |
0-28008 7 hours |
| 22574 |
joelriou author:joelriou |
refactor(CategoryTheory): redefine full subcategories using `ObjectProperty` |
The type `ObjectProperty` was recently introduced #22286 for predicates on the objects of a category. We redefine `FullSubcategory` as `ObjectProperty.FullSubcategory`. This refactor PR mostly does only minimal changes to take into account that some definitions were renamed. The only significant exception is for the definition of the category of finitely generated modules in `Algebra.Category.FGModuleCat.Basic`, which should become the better practice for defining full subcategories, especially when we want to infer certain type classes: define a property of objects (here `ModuleCat.isFG`) and define the category as an abbreviation (here `abbrev FGModuleCat := (ModuleCat.isFG R).FullSubcategory`). Following this approach, significantly many of the typeclasses on the category `FGModuleCat R` can be inferred automatically.
---
[](https://gitpod.io/from-referrer/)
|
large-import
t-category-theory
|
711/678 |
Mathlib.lean,Mathlib/Algebra/Category/FGModuleCat/Basic.lean,Mathlib/Algebra/Category/FGModuleCat/Limits.lean,Mathlib/Algebra/Category/Grp/LeftExactFunctor.lean,Mathlib/Algebra/Category/ModuleCat/Presheaf/Pullback.lean,Mathlib/Algebra/Homology/LocalCohomology.lean,Mathlib/AlgebraicGeometry/AffineScheme.lean,Mathlib/AlgebraicTopology/SimplexCategory/Defs.lean,Mathlib/AlgebraicTopology/SimplicialSet/HomotopyCat.lean,Mathlib/AlgebraicTopology/SimplicialSet/NerveAdjunction.lean,Mathlib/CategoryTheory/Action/Continuous.lean,Mathlib/CategoryTheory/Adjunction/PartialAdjoint.lean,Mathlib/CategoryTheory/Adjunction/Reflective.lean,Mathlib/CategoryTheory/ConcreteCategory/Basic.lean,Mathlib/CategoryTheory/ConnectedComponents.lean,Mathlib/CategoryTheory/Equivalence.lean,Mathlib/CategoryTheory/EssentialImage.lean,Mathlib/CategoryTheory/EssentiallySmall.lean,Mathlib/CategoryTheory/Filtered/Small.lean,Mathlib/CategoryTheory/FullSubcategory.lean,Mathlib/CategoryTheory/Groupoid.lean,Mathlib/CategoryTheory/InducedCategory.lean,Mathlib/CategoryTheory/Limits/ExactFunctor.lean,Mathlib/CategoryTheory/Limits/FinallySmall.lean,Mathlib/CategoryTheory/Limits/FullSubcategory.lean,Mathlib/CategoryTheory/Limits/Indization/Category.lean,Mathlib/CategoryTheory/Limits/Indization/LocallySmall.lean,Mathlib/CategoryTheory/Linear/Basic.lean,Mathlib/CategoryTheory/Linear/LinearFunctor.lean,Mathlib/CategoryTheory/Localization/Construction.lean,Mathlib/CategoryTheory/Localization/Predicate.lean,Mathlib/CategoryTheory/Monoidal/NaturalTransformation.lean,Mathlib/CategoryTheory/Monoidal/Subcategory.lean,Mathlib/CategoryTheory/MorphismProperty/IsInvertedBy.lean,Mathlib/CategoryTheory/ObjectProperty/Basic.lean,Mathlib/CategoryTheory/ObjectProperty/FullSubcategory.lean,Mathlib/CategoryTheory/Preadditive/AdditiveFunctor.lean,Mathlib/CategoryTheory/Preadditive/Basic.lean,Mathlib/CategoryTheory/Preadditive/Indization.lean,Mathlib/CategoryTheory/Sites/EffectiveEpimorphic.lean,Mathlib/CategoryTheory/Sites/SheafOfTypes.lean,Mathlib/CategoryTheory/Sites/Sieves.lean,Mathlib/CategoryTheory/Subobject/MonoOver.lean,Mathlib/CategoryTheory/Subterminal.lean,Mathlib/Topology/Category/TopCat/OpenNhds.lean,Mathlib/Topology/Sheaves/Alexandrov.lean,Mathlib/Topology/Sheaves/SheafCondition/OpensLeCover.lean,Mathlib/Topology/Sheaves/SheafCondition/PairwiseIntersections.lean |
48 |
1 |
['github-actions'] |
nobody |
0-26861 7 hours ago |
0-29577 8 hours ago |
26-69595 26 days |
| 21966 |
vasnesterov author:vasnesterov |
feat(Tactic/Order): support `⊤`, `⊥`, and lattice operations |
Support `⊤`, `⊥`, and lattice operations in the `order` tactic.
---
- [x] depends on: #21877
[](https://gitpod.io/from-referrer/)
|
large-import
t-meta
|
227/47 |
Mathlib/Tactic/Order.lean,Mathlib/Tactic/Order/CollectFacts.lean,Mathlib/Tactic/Order/Graph/Basic.lean,Mathlib/Tactic/Order/Preprocessing.lean,MathlibTest/order.lean,scripts/noshake.json |
6 |
2 |
['github-actions', 'mathlib4-dependent-issues-bot'] |
nobody |
0-25586 7 hours ago |
0-25602 7 hours ago |
34-22103 34 days |
| 23581 |
YaelDillies author:YaelDillies |
feat: order isomorphisms act on flags |
This is crucial to the study of abstract polytopes. For example, a regular abstract polytope is one whose automorphism group is transitive on its flags.
From MiscYD
---
[](https://gitpod.io/from-referrer/)
|
t-algebra label:t-algebra$ |
31/0 |
Mathlib.lean,Mathlib/Algebra/Order/Group/Action/Flag.lean |
2 |
8 |
['YaelDillies', 'b-mehta', 'github-actions', 'vihdzp'] |
nobody |
0-25260 7 hours ago |
1-25394 1 day ago |
1-25441 1 day |
| 23601 |
YaelDillies author:YaelDillies |
feat(CommAlg): the category of commutative algebras |
Define the category of commutative `R`-algebras. This is the same as `Under R` up to two details:
* `A : CommAlg R` contains the data of both `algebraMap R A : R → A` and `Algebra.smul : R → A → A`. `A : Under R` only contains `algebraMap R A`, meaning that going back and forth between `Under R` and unbundled algebras is painful/nigh impossible.
* If `A : Under R`, then `A` must live in the same universe as `R`
Co-authored-by: Andrew Yang
Co-authored-by: Michał Mrugała
Co-authored-by: Christian Merten
From Toric
---
[](https://gitpod.io/from-referrer/)
|
t-algebra label:t-algebra$ |
320/0 |
Mathlib.lean,Mathlib/Algebra/Category/CommAlg/Basic.lean |
2 |
11 |
['YaelDillies', 'b-mehta', 'erdOne', 'eric-wieser', 'github-actions'] |
nobody |
0-24322 6 hours ago |
0-77938 21 hours ago |
0-77987 21 hours |
| 23597 |
YaelDillies author:YaelDillies |
feat: free abelian groups have unique sums |
From Toric
Co-authored-by: Paul Lezeau
---
[](https://gitpod.io/from-referrer/)
|
toric
t-algebra
label:t-algebra$ |
19/0 |
Mathlib.lean,Mathlib/Algebra/FreeAbelianGroup/UniqueSums.lean |
2 |
9 |
['Vierkantor', 'YaelDillies', 'eric-wieser', 'github-actions'] |
nobody |
0-19586 5 hours ago |
0-26640 7 hours ago |
0-70323 19 hours |
| 23587 |
Paul-Lez author:Paul-Lez |
feat(LinearAlgebra/Dual/Basis): Add two lemmas small about coords and dual bases |
This PR adds two small lemmas about how coordinates behave when moving to the dual space.
These aren't `simp` lemmas since they are not in simp-normal form.
---
[](https://gitpod.io/from-referrer/)
|
t-algebra
easy
label:t-algebra$ |
8/0 |
Mathlib/LinearAlgebra/Dual/Basis.lean |
1 |
6 |
['Paul-Lez', 'erdOne', 'github-actions', 'grunweg'] |
nobody |
0-17916 4 hours ago |
0-17966 4 hours ago |
0-32395 8 hours |
| 22119 |
pimotte author:pimotte |
feat(Combinatorics/SimpleGraph): part of Tutte's theorem |
Adds three key parts of the proof of Tutte's theorem, with some supporting lemma's:
- necessity of the Tutte condition (`not_isTutteViolator`)
- the fact that the empty set violates the Tutte condition if the number of vertices is odd (`IsTutteViolator.empty`)
- the construction of a perfect matching in a graph that decomposes into cliques (`Subgraph.IsPerfectMatching.exists_of_isClique_supp`)
Definitions added: `IsTutteViolator`.
---
- [x] depends on: #22125
[](https://gitpod.io/from-referrer/)
[Zulip thread on Tutte's](https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/Tutte's.20theorem) |
maintainer-merge
t-combinatorics
|
196/11 |
Mathlib.lean,Mathlib/Combinatorics/SimpleGraph/Connectivity/Represents.lean,Mathlib/Combinatorics/SimpleGraph/Matching.lean,Mathlib/Combinatorics/SimpleGraph/Tutte.lean,Mathlib/Combinatorics/SimpleGraph/UniversalVerts.lean,Mathlib/Data/Set/Card.lean |
6 |
40 |
['YaelDillies', 'github-actions', 'mathlib4-dependent-issues-bot', 'pimotte'] |
nobody |
0-17631 4 hours ago |
1-18878 1 day ago |
8-28824 8 days |
| 23627 |
kebekus author:kebekus |
feat: add logarithmic counting function of Value Distribution Theory |
Implement the logarithmic counting function of Value Distribution Theory and provide supporting API.
This material is used in [Project VD](https://github.com/kebekus/ProjectVD), which aims to formalize Value Distribution Theory for meromorphic functions on the complex plane.
---
[](https://gitpod.io/from-referrer/)
|
t-analysis |
217/0 |
Mathlib.lean,Mathlib/Analysis/Complex/ValueDistribution/CountingFunction.lean |
2 |
1 |
['github-actions'] |
nobody |
0-17500 4 hours ago |
0-17770 4 hours ago |
0-17830 4 hours |
| 23628 |
kebekus author:kebekus |
doc: ensure that notation is used in the documentation |
Ensure that the documentation generator uses the notation `log⁺`. Currently, the documentation generator writes `x.posLog` instead of `log⁺ x`.
---
[](https://gitpod.io/from-referrer/)
|
t-analysis |
6/2 |
Mathlib/Analysis/SpecialFunctions/Log/PosLog.lean |
1 |
1 |
['github-actions'] |
nobody |
0-17106 4 hours ago |
0-17106 4 hours ago |
0-17165 4 hours |
| 23542 |
kbuzzard author:kbuzzard |
chore(RingTheory/DedekindDomain/FiniteAdeleRing): refactor finite adeles |
Now we have a general theory of restricted products, we can refactor mathlib's finite adele file, removing
the auxiliary results which are unused outside this file and replacing everything with much slicker proofs. The
motivation for this is that the FLT project needs many more results about finite adeles (for example local
compactness in the number field case) and this will be very easy to prove with this new definition
(using `RestrictedProduct.locallyCompactSpace_of_addGroup`), whereas it
took an entire project https://github.com/smmercuri/adele-ring_locally-compact with our current approach.
---
[](https://gitpod.io/from-referrer/)
The diff should not be taken too seriously: the file is rewritten from scratch and is a quarter the size.
I have no idea what to do about deprecations here. I have removed several results (and two definitions) because we don't want them, they were just auxiliary results needed in the old proof of `IsTopologicalRing` and were not used anywhere else; after Anatole's complete rethink of the topology he gets this result for free so my proposal pretty clearly is just to nuke the old results and constructions, while keeping the key constructions (namely the structure of topological ring). The key deletions are `FiniteIntegralAdeles` (which we can still have as `∀ v : HeightOneSpectrum R, v.adicCompletionIntegers K`) and `ProdAdicCompletions` (an auxiliary construction, which we can still have as `∀ v : HeightOneSpectrum R, v.adicCompletion K`). |
t-algebra
t-number-theory
label:t-algebra$ |
87/405 |
Mathlib/RingTheory/DedekindDomain/FiniteAdeleRing.lean,Mathlib/Topology/Algebra/RestrictedProduct.lean |
2 |
13 |
['Ruben-VandeVelde', 'github-actions', 'kbuzzard', 'mariainesdff', 'smmercuri'] |
nobody |
0-17024 4 hours ago |
1-16685 1 day ago |
2-11553 2 days |
| 23447 |
YaelDillies author:YaelDillies |
chore(Order/Circular): golf |
---
[](https://gitpod.io/from-referrer/)
|
large-import
maintainer-merge
t-order
|
10/14 |
Mathlib/Order/Circular.lean,scripts/noshake.json |
2 |
3 |
['github-actions', 'grunweg'] |
nobody |
0-16709 4 hours ago |
0-16709 4 hours ago |
4-13524 4 days |
| 23547 |
chrisflav author:chrisflav |
feat(AlgebraicGeometry): codescent implies descent |
Let `P` and `P'` be morphism properties of schemes. We show some results to deduce
that `P` descends along `P'` from a codescent property of ring homomorphisms.
---
[](https://gitpod.io/from-referrer/)
|
t-algebraic-geometry |
260/1 |
Mathlib.lean,Mathlib/AlgebraicGeometry/Morphisms/AffineAnd.lean,Mathlib/AlgebraicGeometry/Morphisms/Descent.lean,Mathlib/RingTheory/RingHomProperties.lean |
4 |
6 |
['chrisflav', 'erdOne', 'github-actions'] |
nobody |
0-15575 4 hours ago |
2-8704 2 days ago |
2-8692 2 days |
| 21944 |
Thmoas-Guan author:Thmoas-Guan |
feat(RingTheory/Powerseries): Weierstrass preparation for complete local ring |
Weierstrass preparation theorem for complete local ring
---
- [x] depends on: #21900
- [x] depends on: #22369
[](https://gitpod.io/from-referrer/)
|
t-algebra label:t-algebra$ |
532/0 |
Mathlib.lean,Mathlib/RingTheory/WeierstrassPreparation.lean |
2 |
15 |
['Thmoas-Guan', 'acmepjz', 'github-actions', 'mathlib4-dependent-issues-bot', 'riccardobrasca'] |
riccardobrasca assignee:riccardobrasca |
0-15373 4 hours ago |
33-12860 1 month ago |
40-8093 40 days |
| 21838 |
joneugster author:joneugster |
feat(Cache): Allow arguments of the form `Mathlib.Data` which correspond to a folder but not a file |
---
- [ ] depends on: #21834
[](https://gitpod.io/from-referrer/)
|
CI
t-meta
|
108/102 |
Cache/Hashing.lean,Cache/IO.lean,Cache/Main.lean |
3 |
7 |
['eric-wieser', 'github-actions', 'joneugster', 'mathlib4-dependent-issues-bot', 'mergify'] |
nobody |
0-15357 4 hours ago |
0-50419 14 hours ago |
1-79425 1 day |
| 23603 |
YaelDillies author:YaelDillies |
feat: distributive Haar characters |
The name is made up in analogy with modular characters.
From FLT
Co-authored-by: Andrew Yang
Co-authored-by: Javier López-Contreras <38789151+javierlcontreras@users.noreply.github.com>
---
[](https://gitpod.io/from-referrer/)
|
FLT
t-measure-probability
|
87/0 |
Mathlib.lean,Mathlib/MeasureTheory/Measure/Haar/DistribChar.lean |
2 |
3 |
['YaelDillies', 'github-actions', 'tb65536'] |
nobody |
0-15301 4 hours ago |
0-15301 4 hours ago |
0-75827 21 hours |
| 23625 |
YaelDillies author:YaelDillies |
chore: turn `LieSubmodule.disjoint_iff_toModule` around |
and mark it simp
---
[](https://gitpod.io/from-referrer/)
|
t-algebra label:t-algebra$ |
48/20 |
Mathlib/Algebra/Lie/InvariantForm.lean,Mathlib/Algebra/Lie/Submodule.lean,Mathlib/Algebra/Lie/TraceForm.lean,Mathlib/Algebra/Lie/Weights/Basic.lean,Mathlib/Algebra/Lie/Weights/Chain.lean,Mathlib/Algebra/Lie/Weights/Killing.lean |
6 |
1 |
['github-actions'] |
nobody |
0-14690 4 hours ago |
0-14690 4 hours ago |
0-17473 4 hours |
| 19584 |
joelriou author:joelriou |
feat(Algebra/Homology/DerivedCategory): calculus of fractions |
We obtain various factorization lemmas in the derived category as a consequence of the calculus of fractions (precise versions are obtained using canonical truncation on cochain complexes).
---
- [x] depends on: #19579
- [x] depends on: #19578
- [x] depends on: #19550
- [x] depends on: #19543
- [x] depends on: #19544
- [x] depends on: #19559
- [x] depends on: #19560
- [x] depends on: #19574
- [x] depends on: #19572
- [x] depends on: #19570
- [x] depends on: #19203
- [x] depends on: #18502
- [x] depends on: #19198
[](https://gitpod.io/from-referrer/)
|
t-category-theory |
182/0 |
Mathlib.lean,Mathlib/Algebra/Homology/DerivedCategory/Basic.lean,Mathlib/Algebra/Homology/DerivedCategory/Fractions.lean,Mathlib/Algebra/Homology/DerivedCategory/HomologySequence.lean,Mathlib/Algebra/Homology/HomotopyCategory.lean |
5 |
n/a |
['github-actions', 'mathlib4-dependent-issues-bot'] |
nobody |
0-14384 3 hours ago |
unknown |
unknown |
| 22052 |
FLDutchmann author:FLDutchmann |
feat(NumberTheory/SelbergSieve): define Lambda-squared sieves and prove important properties |
This PR:
* Defines lambda-squared sieves.
* Proves they are upper bound sieves.
* Proves that the corresponding main sum is a quadratic form.
---
- [x] depends on: #21880
[](https://gitpod.io/from-referrer/)
|
t-analysis
t-number-theory
|
247/1 |
Mathlib/Data/Nat/GCD/Basic.lean,Mathlib/NumberTheory/SelbergSieve.lean |
2 |
6 |
['Ruben-VandeVelde', 'github-actions', 'mathlib4-dependent-issues-bot'] |
nobody |
0-13971 3 hours ago |
15-6104 15 days ago |
15-6091 15 days |
| 23630 |
YaelDillies author:YaelDillies |
feat: `insert b (Ico a b) = Ico a (b + 1)` |
and similar lemmas. Copied over from `Order.Interval.Finset.Nat`.
---
[](https://gitpod.io/from-referrer/)
|
|
208/0 |
Mathlib/Algebra/Order/Interval/Finset/SuccPred.lean,Mathlib/Algebra/Order/Interval/Set/SuccPred.lean,Mathlib/Order/Interval/Finset/SuccPred.lean,Mathlib/Order/Interval/Set/SuccPred.lean |
4 |
10 |
['YaelDillies', 'b-mehta', 'github-actions'] |
nobody |
0-12688 3 hours ago |
0-15465 4 hours ago |
0-15454 4 hours |
| 23631 |
mattrobball author:mattrobball |
perf(CategoryTheory.Preorder): reorder typeclass assumptions to avoid useless expensive searches |
Similar to #22968 and #23612, these result in searching the order hiearchy before checking that `C` has a `Category` instance.
---
[](https://gitpod.io/from-referrer/)
|
t-category-theory |
1/1 |
Mathlib/CategoryTheory/Limits/Shapes/Preorder/Basic.lean |
1 |
5 |
['github-actions', 'leanprover-bot', 'mattrobball'] |
nobody |
0-12123 3 hours ago |
0-14062 3 hours ago |
0-14115 3 hours |
| 23632 |
JovanGerb author:JovanGerb |
perf(CategoryTheory/Subobject/Lattice): reorder instance arguments |
The `HasImages C` type class fails more quickly, so I set it as the first type class argument.
---
[](https://gitpod.io/from-referrer/)
|
t-category-theory |
4/5 |
Mathlib/CategoryTheory/Subobject/Lattice.lean |
1 |
4 |
['JovanGerb', 'github-actions', 'leanprover-bot'] |
nobody |
0-10805 3 hours ago |
0-12859 3 hours ago |
0-12912 3 hours |
| 21461 |
erdOne author:erdOne |
feat(RingTheory): zero-dimensional rings |
---
[](https://gitpod.io/from-referrer/)
|
t-algebra label:t-algebra$ |
247/77 |
Mathlib.lean,Mathlib/RingTheory/DualNumber.lean,Mathlib/RingTheory/Extension.lean,Mathlib/RingTheory/Ideal/MinimalPrime/Localization.lean,Mathlib/RingTheory/KrullDimension/Basic.lean,Mathlib/RingTheory/KrullDimension/Zero.lean,Mathlib/RingTheory/LocalProperties/Reduced.lean,Mathlib/RingTheory/LocalRing/MaximalIdeal/Basic.lean,Mathlib/RingTheory/Localization/AtPrime.lean,Mathlib/RingTheory/Spectrum/Prime/Topology.lean |
10 |
20 |
['chrisflav', 'erdOne', 'github-actions'] |
nobody |
0-8782 2 hours ago |
0-8803 2 hours ago |
21-4183 21 days |
| 23491 |
chrisflav author:chrisflav |
feat(RingTheory/Spectrum/Prime): purely inseparable extensions induce universal homeomorphisms |
---
- [x] depends on: #22920
[](https://gitpod.io/from-referrer/)
|
t-algebraic-geometry |
234/7 |
Mathlib.lean,Mathlib/LinearAlgebra/TensorProduct/RightExactness.lean,Mathlib/RingTheory/Spectrum/Prime/Homeomorph.lean,Mathlib/RingTheory/Spectrum/Prime/Topology.lean,Mathlib/RingTheory/TensorProduct/Basic.lean |
5 |
8 |
['erdOne', 'github-actions', 'mathlib4-dependent-issues-bot'] |
nobody |
0-8370 2 hours ago |
0-16026 4 hours ago |
2-2093 2 days |
| 13795 |
FR-vdash-bot author:FR-vdash-bot |
perf(Algebra/{Group, GroupWithZero, Ring}/InjSurj): reduce everything |
---
- [ ] depends on: #15192
- [ ] depends on: #15476
[](https://gitpod.io/from-referrer/)
|
t-algebra label:t-algebra$ |
336/190 |
Mathlib/Algebra/Equiv/TransferInstance.lean,Mathlib/Algebra/Group/InjSurj.lean,Mathlib/Algebra/GroupWithZero/Action/Defs.lean,Mathlib/Algebra/GroupWithZero/Action/End.lean,Mathlib/Algebra/GroupWithZero/InjSurj.lean,Mathlib/Algebra/Module/Defs.lean,Mathlib/Algebra/Module/RingHom.lean,Mathlib/Algebra/Ring/InjSurj.lean,scripts/noshake.json |
9 |
31 |
['FR-vdash-bot', 'MichaelStollBayreuth', 'eric-wieser', 'github-actions', 'leanprover-bot', 'mathlib4-dependent-issues-bot', 'mattrobball'] |
nobody |
0-7824 2 hours ago |
1-31517 1 day ago |
40-75191 40 days |
| 22919 |
plp127 author:plp127 |
feat(Combinatorics/SimpleGraph/Coloring): Make `Fintype` instance for graph colorings computable |
Makes the `Fintype` instance for graph colorings computable.
See this [Zulip](https://leanprover.zulipchat.com/#narrow/channel/113489-new-members/topic/Classical.20vs.20constructive.20logic.20in.20computation/near/496220816) message.
---
[](https://gitpod.io/from-referrer/)
|
t-combinatorics |
95/24 |
Mathlib/Combinatorics/SimpleGraph/Coloring.lean,Mathlib/Combinatorics/SimpleGraph/Maps.lean |
2 |
11 |
['IvanRenison', 'b-mehta', 'github-actions', 'plp127'] |
nobody |
0-7314 2 hours ago |
6-83079 6 days ago |
20-14826 20 days |
| 23546 |
JovanGerb author:JovanGerb |
feat(LinearAlgebra/AffineSpace/AffineSubspace): rename `AffineSubspace.mk'` to `Submodule.shift` |
In addition to renaming, I've refactored the code a bit:
- `mem_mk'_iff_vsub_mem` was obsolete since it was the same as `mem_mk'`, so I removed it (this is due to a change in the definition I made recently)
- I added a nonempty instance for `shift`
- I added a simp lemma that `shift` isn't equal to `⊥` (the empty affine subspace). I need this for the next point.
- Edit: I'll leave this for a later PR.
~I proved a simp lemma that a `shift` is parallel to a `shift` if and only if the linear subspaces are the same.~
- I renamed `mk'_eq` to `shift_direction_eq_self `.
- I renamed `eq_or_eq_secondInter_of_mem_mk'_span_singleton_iff_mem` to `eq_or_eq_secondInter_iff_mem_of_mem_shift_span_singleton`. I think it is better to put the `of_mem_mk'_span_singleton` at the end of the name.
---
[](https://gitpod.io/from-referrer/)
|
|
128/99 |
Mathlib/Algebra/Module/ZLattice/Basic.lean,Mathlib/Geometry/Euclidean/Basic.lean,Mathlib/Geometry/Euclidean/MongePoint.lean,Mathlib/Geometry/Euclidean/PerpBisector.lean,Mathlib/Geometry/Euclidean/Sphere/SecondInter.lean,Mathlib/Geometry/Euclidean/Sphere/Tangent.lean,Mathlib/LinearAlgebra/AffineSpace/AffineSubspace/Defs.lean |
7 |
2 |
['JovanGerb', 'github-actions'] |
nobody |
0-7174 1 hour ago |
2-9253 2 days ago |
2-9241 2 days |
| 23554 |
D-Thomine author:D-Thomine |
refactor(Dynamics/TopologicalEntropy): use expGrowth |
The notions of `coverEntropyEntourage`, `coverEntropyInfEntourage`, `netEntropyEntourage` and `netEntropyInfEntourage` are now defined using `expGrowth`. Some technical intermediate lemmas are no longer needed and are removed.
Some minor golfing around those three files.
---
[](https://gitpod.io/from-referrer/)
|
large-import
t-dynamics
|
171/248 |
Mathlib/Dynamics/TopologicalEntropy/CoverEntropy.lean,Mathlib/Dynamics/TopologicalEntropy/NetEntropy.lean,Mathlib/Dynamics/TopologicalEntropy/Semiconj.lean |
3 |
1 |
['github-actions'] |
nobody |
0-6104 1 hour ago |
2-4632 2 days ago |
2-4883 2 days |
| 23637 |
kirilvino author:kirilvino |
feat(Combinatorics/SimpleGraph): every circuit contains a cycle proof |
circuit to cycle proof
---
This PR uses the bypass definition in a new function for closed walks that removes repeated vertices. Then proves if the closed walk given is a circuit, that the result from this function is a cycle. This is then packaged up similar to the existing ToPath definition, creating a way of transforming a circuit into a cycle.
[](https://gitpod.io/from-referrer/)
|
new-contributor
t-combinatorics
|
35/0 |
Mathlib/Combinatorics/SimpleGraph/Path.lean |
1 |
1 |
['github-actions'] |
nobody |
0-4152 1 hour ago |
0-4152 1 hour ago |
0-4222 1 hour |
| 23500 |
DrLSimon author:DrLSimon |
feat(MeasureTheory/Decomposition): link the clipped sub of positive measures to Jordan decomposition |
This introduces a new file `Mathlib/MeasureTheory/Decomposition/JordanSub.lean` which develops the Jordan decomposition of the signed measure `μ.toSignedMeasure - ν.toSignedMeasure` for finite measures `μ`
and `ν`, expressing it as the pair `(μ - ν, ν - μ)` of mutually singular finite measures.
The key tool is the Hahn decomposition theorem, which yields a measurable partition of the space
where `μ ≥ ν` and `ν ≥ μ`.
Some basic results of `VectorMeasure` are also provided such as `restrict_neg`, `restrict_sub` `restrict_add_restrict_compl` and `Measure.toSignedMeasure_le_iff` within the `JordanSub.lean` file. They could be moved to another more central place (I guess `VectorMeasure/Basic.lean`). Similarly, `Measure.sub_zero` could go to `Sub.lean`.
[](https://gitpod.io/from-referrer/)
|
new-contributor
t-measure-probability
|
265/0 |
Mathlib.lean,Mathlib/MeasureTheory/Decomposition/JordanSub.lean |
2 |
2 |
['DrLSimon', 'github-actions'] |
nobody |
0-3131 52 minutes ago |
3-7343 3 days ago |
3-7392 3 days |
| 23493 |
BoltonBailey author:BoltonBailey |
chore(Control/Combinators): add documentation |
Adds docstrings to this file ([Zulip discussion](https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/Technical.20Debt.20Counters/near/509167582))
---
[](https://gitpod.io/from-referrer/)
|
tech debt
maintainer-merge
t-meta
documentation
|
33/14 |
Mathlib/Control/Combinators.lean,scripts/nolints.json |
2 |
5 |
['Parcly-Taxel', 'b-mehta', 'github-actions', 'joneugster'] |
b-mehta and joneugster assignee:joneugster assignee:b-mehta |
0-2757 45 minutes ago |
0-6572 1 hour ago |
2-5289 2 days |
| 8370 |
eric-wieser author:eric-wieser |
refactor(Analysis/NormedSpace/Exponential): remove the `𝕂` argument from `exp` |
This argument is still needed for almost all the lemmas, which means it can longer be found by unification.
We keep around `expSeries 𝕂 A`, as it's needed for talking about the radius of convergence over different base fields.
This is a prerequisite for #8372, as we can't merge the functions until they have the same interface.
---
[](https://gitpod.io/from-referrer/)
This is started from the mathport output on https://github.com/leanprover-community/mathlib/pull/19244 |
t-analysis |
443/396 |
Mathlib/Analysis/CStarAlgebra/Exponential.lean,Mathlib/Analysis/CStarAlgebra/Spectrum.lean,Mathlib/Analysis/Normed/Algebra/Exponential.lean,Mathlib/Analysis/Normed/Algebra/MatrixExponential.lean,Mathlib/Analysis/Normed/Algebra/QuaternionExponential.lean,Mathlib/Analysis/Normed/Algebra/Spectrum.lean,Mathlib/Analysis/Normed/Algebra/TrivSqZeroExt.lean,Mathlib/Analysis/NormedSpace/DualNumber.lean,Mathlib/Analysis/SpecialFunctions/ContinuousFunctionalCalculus/ExpLog.lean,Mathlib/Analysis/SpecialFunctions/Exponential.lean,Mathlib/Analysis/SpecialFunctions/Trigonometric/Series.lean |
11 |
16 |
['eric-wieser', 'girving', 'github-actions', 'kbuzzard', 'urkud'] |
nobody |
0-164 2 minutes ago |
0-53632 14 hours ago |
24-61767 24 days |