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 |
| 21270 |
GabinKolly author:GabinKolly |
feat(ModelTheory/Bundled): first-order embeddings and equivalences from equalities |
Add first-order embeddings and equivalences from equalities between bundled structures.
---
Add two definitions to get embeddings and equivalences from equalities between bundled structures, and simple properties.
This is some preparatory work for #18876
[](https://gitpod.io/from-referrer/)
|
large-import
t-logic
|
98/0 |
Mathlib/ModelTheory/Bundled.lean |
1 |
15 |
['GabinKolly', 'Vierkantor', 'YaelDillies', 'github-actions'] |
nobody |
45-61630 1 month ago |
45-69226 1 month ago |
45-81292 45 days |
| 21837 |
yu-yama author:yu-yama |
feat(GroupExtension/Abelian): define `conjClassesEquivH1` |
As the third part of #19582, this PR adds the first part of the `Abelian` file.
It mainly:
- defines `SemidirectProduct.conjClassesEquivH1`, a bijection between the conjugacy classes of splittings of a group extension associated to a semidirect product and $H^1 (G, N)$.
---
[](https://gitpod.io/from-referrer/)
|
t-algebra label:t-algebra$ |
129/3 |
Mathlib.lean,Mathlib/GroupTheory/GroupExtension/Abelian.lean,Mathlib/GroupTheory/GroupExtension/Defs.lean,docs/references.bib |
4 |
1 |
['github-actions'] |
erdOne assignee:erdOne |
40-36276 1 month ago |
40-45426 1 month ago |
40-45474 40 days |
| 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 |
39-80063 1 month ago |
39-80124 1 month ago |
39-80113 39 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 |
37-82642 1 month ago |
38-80158 1 month ago |
38-80205 38 days |
| 21960 |
jsm28 author:jsm28 |
feat(Geometry/Euclidean/Simplex): simplex angle properties |
Show that the angles of an equilateral simplex in a Euclidean space are `π / 3`, and define the property of a simplex (typically a triangle) being acute-angled. (This property is more common and more useful than the alternatives of "has a right angle" and "has an obtuse angle", since when it's given that a triangle has one of the latter properties, normally it's stated *which* angle is a right angle or an obtuse angle, in which case you just have an equation or inequality for a given angle. So while those other properties will be wanted eventually - occasionally a problem does involve such properties without stating which angle is involved - they are lower priority.)
---
[](https://gitpod.io/from-referrer/)
|
t-euclidean-geometry |
86/0 |
Mathlib.lean,Mathlib/Geometry/Euclidean/Simplex.lean |
2 |
1 |
['github-actions'] |
nobody |
37-36138 1 month ago |
37-37343 1 month ago |
37-37332 37 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 |
35-51054 1 month ago |
35-51054 1 month ago |
36-71712 36 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 |
35-17764 1 month ago |
35-17777 1 month ago |
35-19577 35 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 |
34-77234 1 month ago |
35-79728 1 month ago |
35-79860 35 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$ |
377/3 |
Mathlib/Algebra/SkewMonoidAlgebra/Basic.lean |
1 |
2 |
['Louddy', 'github-actions'] |
nobody |
34-61405 1 month ago |
34-61458 1 month ago |
34-62277 34 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 |
33-64482 1 month ago |
33-65308 1 month ago |
36-28079 36 days |
| 21260 |
chrisflav author:chrisflav |
feat(RingTheory/Presentation): reindex presentations |
Constructs induced presentations from equivalent indexing types for generators and relations. This will be used in a follow-up to fix the universes of the generators and relations in `Algebra.IsStandardSmooth` to `0`.
---
- [x] depends on: #21259
[](https://gitpod.io/from-referrer/)
|
t-algebra label:t-algebra$ |
125/6 |
Mathlib/Algebra/MvPolynomial/Rename.lean,Mathlib/RingTheory/Generators.lean,Mathlib/RingTheory/Ideal/Maps.lean,Mathlib/RingTheory/MvPolynomial/Symmetric/Defs.lean,Mathlib/RingTheory/Presentation.lean,Mathlib/RingTheory/Smooth/StandardSmooth.lean |
6 |
2 |
['github-actions', 'mathlib4-dependent-issues-bot'] |
nobody |
31-26239 1 month ago |
33-50644 1 month ago |
0-5053 1 hour |
| 22216 |
Rida-Hamadani author:Rida-Hamadani |
chore(SimpleGraph): remove redundant import and improve style for `StronglyRegular.lean` |
---
[](https://gitpod.io/from-referrer/)
|
t-combinatorics |
11/14 |
Mathlib/Combinatorics/SimpleGraph/StronglyRegular.lean |
1 |
1 |
['Parcly-Taxel', 'github-actions'] |
nobody |
30-22605 1 month ago |
30-44784 1 month ago |
30-44836 30 days |
| 16733 |
pechersky author:pechersky |
feat(Topology/Algebra/Valued/LocallyCompact): locally compact nonarchimedean field iff complete and DVR and finite field |
---
- [x] depends on: #16731
- [x] depends on: #15777
- [x] depends on: #16619
- [x] depends on: #15424
- [x] depends on: #20373
[](https://gitpod.io/from-referrer/)
|
large-import
t-algebra
label:t-algebra$ |
213/3 |
Mathlib/Topology/Algebra/Valued/LocallyCompact.lean,Mathlib/Topology/Algebra/Valued/ValuationTopology.lean |
2 |
n/a |
['github-actions', 'kbuzzard', 'mathlib4-dependent-issues-bot', 'pechersky'] |
nobody |
28-51431 1 month ago |
unknown |
unknown |
| 21829 |
Whysoserioushah author:Whysoserioushah |
feat(LinearAlgebra/TensorProduct/HomTensor): Add TensorProduct of Hom-modules |
co-authored by: @erdOne
---
[](https://gitpod.io/from-referrer/)
|
t-algebra label:t-algebra$ |
174/0 |
Mathlib.lean,Mathlib/LinearAlgebra/TensorProduct/HomTensor.lean |
2 |
24 |
['Whysoserioushah', 'YaelDillies', 'erdOne', 'github-actions', 'kbuzzard'] |
nobody |
28-45946 1 month ago |
28-46320 1 month ago |
40-43338 40 days |
| 22299 |
chrisflav author:chrisflav |
chore(Order/RelSeries): induction principle for `RelSeries` |
Adds many small API lemmas for the transition between `List` and `RelSeries` and an induction principle. Currently, the induction principle is only really useful for proofs, but with a more ambitious refactor of the basic definitions, it could also be used to construct data.
Co-authored by: Sihan Su
Co-authored by: Yi Song
---
[](https://gitpod.io/from-referrer/)
|
t-order |
133/0 |
Mathlib/Data/List/Chain.lean,Mathlib/Order/RelSeries.lean |
2 |
1 |
['github-actions'] |
nobody |
28-36569 1 month ago |
28-39065 1 month ago |
28-39055 28 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 |
28-24929 1 month ago |
28-24929 1 month ago |
30-35340 30 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 |
27-55346 27 days ago |
27-76615 27 days ago |
27-76671 27 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/IsBaseChangePi.lean |
3 |
1 |
['github-actions'] |
nobody |
27-37832 27 days ago |
27-38677 27 days ago |
27-39874 27 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 |
26-58406 26 days ago |
39-66922 1 month ago |
39-66971 39 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 |
24-38669 24 days ago |
24-39131 24 days ago |
24-39120 24 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 |
2 |
['github-actions', 'mathlib4-dependent-issues-bot'] |
nobody |
23-72130 23 days ago |
24-52518 24 days ago |
47-51913 47 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 |
21-79328 21 days ago |
21-80035 21 days ago |
23-23914 23 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 |
21-59192 21 days ago |
21-71383 21 days ago |
21-71373 21 days |
| 18397 |
YaelDillies author:YaelDillies |
chore: Rename `RestrictGenTopology` to `IsRestrictGen` |
Rename `Topology.RestrictGenTopology` to `Topology.IsRestrictGen` since
* the `Topology` part is understood
* the name should be prefixed with `Is` to show it's Prop-valued
---
[](https://gitpod.io/from-referrer/)
|
t-topology |
33/30 |
Mathlib/Topology/Algebra/Module/Alternating/Topology.lean,Mathlib/Topology/Algebra/Module/Multilinear/Topology.lean,Mathlib/Topology/Algebra/Module/StrongTopology.lean,Mathlib/Topology/Defs/Induced.lean,Mathlib/Topology/RestrictGen.lean,Mathlib/Topology/UniformSpace/CompactConvergence.lean,Mathlib/Topology/UniformSpace/UniformConvergenceTopology.lean |
7 |
9 |
['ADedecker', 'YaelDillies', 'github-actions', 'grunweg', 'urkud'] |
nobody |
21-56425 21 days ago |
21-56425 21 days ago |
26-62901 26 days |
| 22565 |
chrisflav author:chrisflav |
feat(RingTheory/Flat): descent along faithfully flat ring maps |
---
[](https://gitpod.io/from-referrer/)
|
t-algebra label:t-algebra$ |
28/0 |
Mathlib/RingTheory/Flat/FaithfullyFlat/Basic.lean |
1 |
1 |
['github-actions'] |
nobody |
21-40800 21 days ago |
21-40857 21 days ago |
21-40847 21 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 |
21-37948 21 days ago |
35-48026 1 month ago |
35-57183 35 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 |
21-26957 21 days ago |
21-26963 21 days ago |
21-27014 21 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 |
20-65826 20 days ago |
20-71293 20 days ago |
20-71283 20 days |
| 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 |
20-58823 20 days ago |
20-58823 20 days ago |
21-13518 21 days |
| 22639 |
b-reinke author:b-reinke |
feat(Mathlib/GroupTheory/FreeGroup): theory of (cyclically) reduced words |
Upstreamed from the [EquationalTheories](https://github.com/teorth/equational_theories) project.
This PR defines in the new file `Mathlib/GroupTheory/FreeGroup/ReducedWords.lean` some extra lemmas for free groups, in particular about (cyclically) reduced words.
## Main declarations
* `FreeGroup.Red.reduced`: the predicate for reduced words
* `FreeGroup.Red.cyclicallyReduced`: the predicate for cyclically reduced words
## Main statements
* `FreeGroup.infinite_order`: nontrivial elements of a free group have infinite order
* `FreeGroup.zpow_left_injective`: taking n-th powers is an injective function on the free group
Co-authored-by: Amir Livne Bar-on
---
[](https://gitpod.io/from-referrer/)
|
new-contributor
t-algebra
label:t-algebra$ |
429/0 |
Mathlib.lean,Mathlib/GroupTheory/FreeGroup/Basic.lean,Mathlib/GroupTheory/FreeGroup/Reduce.lean,Mathlib/GroupTheory/FreeGroup/ReducedWords.lean |
4 |
1 |
['github-actions'] |
nobody |
19-58219 19 days ago |
19-59287 19 days ago |
19-59343 19 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 |
19-56201 19 days ago |
19-56215 19 days ago |
43-41336 43 days |
| 22633 |
YaelDillies author:YaelDillies |
feat: other form of the LYM inequality |
and use semantic names for the existing lemmas.
Moves:
* `card_mul_le_card_shadow_mul` → `local_lubell_yamamoto_meshalkin_inequality_mul`
* `card_div_choose_le_card_shadow_div_choose` → `local_lubell_yamamoto_meshalkin_inequality_div`
* `sum_card_slice_div_choose_le_one` → `lubell_yamamoto_meshalkin_inequality_sum_card_div_choose`
From PlainCombi (LeanCamCombi)
---
[](https://gitpod.io/from-referrer/)
|
t-combinatorics |
53/45 |
Mathlib/Combinatorics/SetFamily/AhlswedeZhang.lean,Mathlib/Combinatorics/SetFamily/LYM.lean,docs/overview.yaml |
3 |
2 |
['b-mehta', 'github-actions'] |
nobody |
19-50099 19 days ago |
19-63950 19 days ago |
19-64000 19 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 |
19-48297 19 days ago |
19-48312 19 days ago |
29-57911 29 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 |
19-42445 19 days ago |
19-42445 19 days ago |
19-42502 19 days |
| 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 |
19-38364 19 days ago |
unknown |
unknown |
| 22657 |
Xmask19 author:Xmask19 |
feat: a graph is maximally acyclic iff it is a tree |
---
[](https://gitpod.io/from-referrer/)
|
new-contributor
t-combinatorics
|
86/0 |
Mathlib/Combinatorics/SimpleGraph/Acyclic.lean |
1 |
2 |
['Rida-Hamadani', 'github-actions'] |
nobody |
19-32411 19 days ago |
19-40585 19 days ago |
19-40635 19 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 |
19-31163 19 days ago |
29-32885 1 month ago |
29-32873 29 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 |
19-856 19 days ago |
27-54735 27 days ago |
27-56156 27 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 |
18-76733 18 days ago |
18-76733 18 days ago |
41-64405 41 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 |
18-61539 18 days ago |
21-45940 21 days ago |
34-33103 34 days |
| 21822 |
joneugster author:joneugster |
feat(Cache): extend argument-parsing to allow module names and file names |
Accept both `Mathlib.Init` and `Mathlib/Init.lean` as arguments.
---
Note: I noticed a bug in walking directories which will not be present after #21834, so I put an error message "not implemented yet" here and will add the feature in the PR following #21834
- [x] depends on: #21815
[](https://gitpod.io/from-referrer/)
|
CI
t-meta
|
110/21 |
Cache/Hashing.lean,Cache/IO.lean,Cache/Main.lean |
3 |
4 |
['eric-wieser', 'github-actions', 'joneugster', 'mathlib4-dependent-issues-bot'] |
nobody |
18-49773 18 days ago |
18-79064 18 days ago |
19-76617 19 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 |
18-36092 18 days ago |
18-36716 18 days ago |
18-36767 18 days |
| 22361 |
rudynicolop author:rudynicolop |
feat(Computability/NFA): nfa closure properties |
Add the closure properties union, intersection and reversal for NFA.
---
[](https://gitpod.io/from-referrer/)
|
t-computability
new-contributor
|
315/0 |
Mathlib/Computability/NFA.lean |
1 |
2 |
['github-actions', 'rudynicolop'] |
EtienneC30 assignee:EtienneC30 |
17-36590 17 days ago |
26-75270 26 days ago |
26-75317 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 |
16-73268 16 days ago |
18-68551 18 days ago |
18-68550 18 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 |
16-54530 16 days ago |
17-41499 17 days ago |
48-3751 48 days |
| 22745 |
jsm28 author:jsm28 |
feat(LinearAlgebra/AffineSpace/Independent): `faceOpposite` |
Add a convenience definition for the face of a simplex opposite a given vertex (the face with all but that one vertex of the original simplex).
---
[](https://gitpod.io/from-referrer/)
|
t-algebra label:t-algebra$ |
19/0 |
Mathlib/LinearAlgebra/AffineSpace/Independent.lean |
1 |
1 |
['github-actions'] |
nobody |
16-41872 16 days ago |
16-41929 16 days ago |
16-41919 16 days |
| 22747 |
jsm28 author:jsm28 |
feat(LinearAlgebra/AffineSpace/Combination): affine combinations where points take only two values |
Add a lemma relating `affineCombination` to `lineMap` in the case where the points in the combination take only two values (although the `Finset` used for the sum may have any cardinality).
---
[](https://gitpod.io/from-referrer/)
|
t-algebra label:t-algebra$ |
13/0 |
Mathlib/LinearAlgebra/AffineSpace/Combination.lean |
1 |
1 |
['github-actions'] |
nobody |
16-41593 16 days ago |
16-41649 16 days ago |
16-41639 16 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 |
16-36915 16 days ago |
16-39165 16 days ago |
16-39155 16 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 |
16-34210 16 days ago |
16-34210 16 days ago |
16-50460 16 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 |
16-28291 16 days ago |
25-53844 25 days ago |
25-53833 25 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/TranscendenceBasis.lean**, we show:
+ The AlgebraicIndependent sets in a domain form a Matroid, which is used to show all transcendence bases have the same cardinality. Provide algebraic characterizations of the matroid notions `Indep`, `Base`, `cRank`, `Basis`, `closure`, `Flat`, and `Spanning`.
+ Transcendence bases are exactly algebraic independent families that are spanning (i.e. the whole algebra is algebraic over the algebra generated by the family). On the other hand, a spanning set in a domain contains a transcendence basis.
+ There always exists an transcendence basis between an arbitrary AlgebraicIndependent set and an "almost generating" set in a domain.
+ `trdeg R S + trdeg S A = trdeg R A` in a domain, which depends on `AlgebraicIndependent/IsTranscendenceBasis.sumElim_comp`.
+ A finite AlgebraicIndependent family or spanning family in a domain that has the same cardinality as `trdeg` must be a transcendence basis.
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/)
|
t-algebra label:t-algebra$ |
721/68 |
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 |
46 |
['acmepjz', 'alreadydone', 'apnelson1', 'github-actions', 'mathlib4-dependent-issues-bot'] |
nobody |
15-64631 15 days ago |
18-9189 18 days ago |
27-16552 27 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 |
15-59959 15 days ago |
19-69258 19 days ago |
19-69314 19 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 |
15-52756 15 days ago |
15-52843 15 days ago |
15-52902 15 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 |
15-11068 15 days ago |
15-11081 15 days ago |
38-60663 38 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 |
14-72463 14 days ago |
48-74924 1 month ago |
57-56235 57 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 |
14-62937 14 days ago |
20-7044 20 days ago |
20-7094 20 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 |
14-41382 14 days ago |
19-27778 19 days ago |
19-27826 19 days |
| 22483 |
jsm28 author:jsm28 |
feat(Geometry/Euclidean/Sphere/Tangent): tangents to spheres |
Add various basic definitions and lemmas relating to spheres being tangent to affine subspaces and other spheres. (Material involving angles, such as the alternate segment theorem, is expected to be added separately in followups.)
---
- [ ] depends on: #22472
[](https://gitpod.io/from-referrer/)
|
t-euclidean-geometry |
406/0 |
Mathlib.lean,Mathlib/Geometry/Euclidean/Sphere/Tangent.lean |
2 |
2 |
['github-actions', 'mathlib4-dependent-issues-bot'] |
nobody |
14-23562 14 days ago |
14-23564 14 days ago |
14-25436 14 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 |
14-1180 14 days ago |
14-1194 14 days ago |
18-42942 18 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 |
206/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 |
13-64618 13 days ago |
13-72179 13 days ago |
32-61280 32 days |
| 22851 |
apnelson1 author:apnelson1 |
feat(LinearIndepOn): a bit more LinearIndepOn api |
We add some more API for `LinearIndepOn`. The large import is so a lemma about dimension can be stated with `Set.encard` - it is unclear where such a lemma belongs if not where it is.
---
[](https://gitpod.io/from-referrer/)
|
large-import
t-algebra
label:t-algebra$ |
56/20 |
Mathlib/LinearAlgebra/Dimension/Basic.lean,Mathlib/LinearAlgebra/Dimension/StrongRankCondition.lean,Mathlib/LinearAlgebra/LinearIndependent/Defs.lean,Mathlib/LinearAlgebra/LinearIndependent/Lemmas.lean |
4 |
7 |
['apnelson1', 'github-actions', 'leanprover-bot', 'madvorak'] |
nobody |
13-58409 13 days ago |
14-33306 14 days ago |
14-33358 14 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 |
13-17172 13 days ago |
13-17233 13 days ago |
13-17223 13 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 |
13-1666 13 days ago |
14-18220 14 days ago |
14-18269 14 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 |
12-78543 12 days ago |
12-78560 12 days ago |
21-32080 21 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 |
12-69690 12 days ago |
12-69711 12 days ago |
15-65400 15 days |
| 21583 |
j-loreaux author:j-loreaux |
feat: Hölder combinations of `MeasureTheory.Lp` functions, including heterogeneous scalar multiplication |
Given a continuous bilinear map `B : E →L[𝕜] F →L[𝕜] G`, we define an associated map `ContinuousLinearMap.holder : Lp E p μ → Lp F q μ → Lp G r μ` where `p q r` are a Hölder triple. We bundle this into a bilinear map `ContinuousLinearMap.holderₗ` and a continuous bilinear map `ContinuousLinearMap.holderL` under some additional assumptions.
We also declare a heterogeneous scalar multiplication (`HSMul`) instance on `MeasureTheory.Lp` spaces. Although this could use the `ContinuousLinearMap.holder` construction above, we opt not to do so in order to minimize the necessary type class assumptions.
When `p q : ℝ≥0∞` are Hölder conjugate (i.e., `HolderConjugate p q`), we also construct the natural map `ContinuousLinearMap.lpPairing : Lp E p μ →L[𝕜] Lp F q μ →L[𝕜] G` given by `fun f g ↦ ∫ x, B (f x) (g x) ∂μ`.
Note: this makes the second example (the first being matrices) of a true heterogeneous (scalar, in this case) multiplication occurring in practice. Right now, none of our distributivity lemmas can be stated for in that context. Moreover, we can't have `IsScalarTower` or `SMulCommClass` instances for these.
---
- [x] depends on: #21792
- [x] depends on: #21854
This PR can be split once the design decisions are approved.
[](https://gitpod.io/from-referrer/)
|
t-analysis |
257/0 |
Mathlib.lean,Mathlib/MeasureTheory/Function/Holder.lean |
2 |
26 |
['ADedecker', 'YaelDillies', 'eric-wieser', 'github-actions', 'j-loreaux', 'mathlib4-dependent-issues-bot'] |
nobody |
12-52556 12 days ago |
12-52556 12 days ago |
29-56699 29 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 |
5 |
['Paul-Lez', 'YaelDillies', 'github-actions'] |
nobody |
12-41301 12 days ago |
12-41301 12 days ago |
19-63169 19 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$ |
102/0 |
Mathlib/Algebra/Module/FinitePresentation.lean,Mathlib/LinearAlgebra/Pi.lean |
2 |
1 |
['github-actions'] |
nobody |
11-71996 11 days ago |
11-72140 11 days ago |
11-72130 11 days |
| 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
|
707/674 |
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 |
11-66484 11 days ago |
11-66499 11 days ago |
18-39535 18 days |
| 22903 |
YaelDillies author:YaelDillies |
feat: limsups in `ℝ≥0` and `ℝ` agree |
---
[](https://gitpod.io/from-referrer/)
|
t-order |
128/0 |
Mathlib/Order/Filter/ENNReal.lean |
1 |
3 |
['YaelDillies', 'b-mehta', 'github-actions'] |
nobody |
11-56088 11 days ago |
12-44233 12 days ago |
12-44287 12 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 |
11-51764 11 days ago |
11-58520 11 days ago |
11-58579 11 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 |
11-51041 11 days ago |
11-51048 11 days ago |
11-51091 11 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$ |
215/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 |
11-50981 11 days ago |
11-50996 11 days ago |
23-43179 23 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 |
11 |
['Paul-Lez', 'erdOne', 'github-actions', 'jcommelin', 'maddycrim'] |
nobody |
10-73621 10 days ago |
36-17773 1 month ago |
36-17827 36 days |
| 22355 |
xyzw12345 author:xyzw12345 |
feat(Algebra/RingQuot): Some lemmas about `RingQuot.mkAlgHom` and `RingQuot.mkRingHom` |
This PR provides a few basic lemmas about `RingQuot.mkRingHom` and `RingQuot.mkAlgHom`. These lemmas are about when are two elements mapped to the same one under these two maps, and they correspond to the lemma `Quot.eq`.
PR #22279 depends on these lemmas.
---
[](https://gitpod.io/from-referrer/)
|
new-contributor
t-algebra
label:t-algebra$ |
16/0 |
Mathlib/Algebra/RingQuot.lean |
1 |
10 |
['Paul-Lez', 'github-actions', 'ocfnash', 'xyzw12345'] |
nobody |
10-63723 10 days ago |
24-71248 24 days ago |
26-23560 26 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 |
10-62057 10 days ago |
10-74701 10 days ago |
10-74751 10 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 |
10-55592 10 days ago |
31-11976 1 month ago |
31-11975 31 days |
| 22959 |
ScottCarnahan author:ScottCarnahan |
chore (RingTheory/HahnSeries/SummableFamily): refactor HahnSeries.SummableFamily.powers to take junk values |
This PR removes the positive order condition on the function `HahnSeries.SummableFamily.powers`, and instead takes the junk value zero when the input has non-positive order. This follows a reviewer suggestion from #20205.
---
[](https://gitpod.io/from-referrer/)
|
t-algebra label:t-algebra$ |
148/95 |
Mathlib/RingTheory/HahnSeries/HEval.lean,Mathlib/RingTheory/HahnSeries/Summable.lean |
2 |
1 |
['github-actions'] |
nobody |
10-53908 10 days ago |
10-53972 10 days ago |
10-53962 10 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$ |
63/27 |
Mathlib/Algebra/Group/Submonoid/Operations.lean,Mathlib/GroupTheory/Finiteness.lean,Mathlib/RingTheory/FiniteType.lean |
3 |
4 |
['YaelDillies', 'b-mehta', 'github-actions', 'mathlib4-dependent-issues-bot'] |
nobody |
10-22368 10 days ago |
10-22368 10 days ago |
11-37427 11 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 |
10-22360 10 days ago |
10-22360 10 days ago |
10-51974 10 days |
| 22970 |
YaelDillies author:YaelDillies |
feat: monoid algebras over domains are domains |
From Toric
---
[](https://gitpod.io/from-referrer/)
|
toric
t-algebra
label:t-algebra$ |
25/3 |
Mathlib/Algebra/MonoidAlgebra/NoZeroDivisors.lean |
1 |
1 |
['github-actions'] |
nobody |
10-19598 10 days ago |
10-19645 10 days ago |
10-19648 10 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 |
10-861 10 days ago |
10-876 10 days ago |
11-60331 11 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 |
9-57975 9 days ago |
9-58013 9 days ago |
22-33043 22 days |
| 20668 |
gio256 author:gio256 |
refactor(AlgebraicTopology/SimplicialSet): truncated paths |
We refactor the `StrictSegal` infrastructure, making two notable changes:
- The `StrictSegal` class is redefined as a structure, and the class `IsStrictSegal X : Prop` is added in its place.
- `Path`, `StrictSegal`, and related constructions are defined for truncated simplicial sets. A path in a simplicial set `X` is then defined as a 1-truncated path in the 1-truncation of `X`.
---
- [X] depends on: #21090
[](https://gitpod.io/from-referrer/)
|
infinity-cosmos
t-category-theory
|
645/189 |
Mathlib/AlgebraicTopology/Quasicategory/Nerve.lean,Mathlib/AlgebraicTopology/Quasicategory/StrictSegal.lean,Mathlib/AlgebraicTopology/SimplexCategory/Defs.lean,Mathlib/AlgebraicTopology/SimplicialObject/Basic.lean,Mathlib/AlgebraicTopology/SimplicialSet/Basic.lean,Mathlib/AlgebraicTopology/SimplicialSet/Coskeletal.lean,Mathlib/AlgebraicTopology/SimplicialSet/Path.lean,Mathlib/AlgebraicTopology/SimplicialSet/StrictSegal.lean |
8 |
34 |
['emilyriehl', 'gio256', 'github-actions', 'joelriou', 'mathlib4-dependent-issues-bot'] |
nobody |
9-48270 9 days ago |
11-49816 11 days ago |
11-60323 11 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 |
1 |
['github-actions'] |
nobody |
9-33216 9 days ago |
11-71949 11 days ago |
11-72004 11 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/)
|
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 |
9-13853 9 days ago |
9-14020 9 days ago |
13-33496 13 days |
| 22027 |
vihdzp author:vihdzp |
chore(SetTheory/Ordinal/FixedPoint); review `Ordinal.nfp` API |
This PR does the following:
- add `iff` variants of various theorems, renaming some in the process
- weaken some assumptions slightly
- golf throughout
---
- [x] depends on: #22017
[](https://gitpod.io/from-referrer/)
|
t-set-theory |
64/61 |
Mathlib/Logic/Equiv/List.lean,Mathlib/SetTheory/Ordinal/FixedPoint.lean |
2 |
2 |
['github-actions', 'mathlib4-dependent-issues-bot'] |
nobody |
9-7831 9 days ago |
35-67677 1 month ago |
35-67949 35 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 |
8-84414 8 days ago |
41-43833 1 month ago |
41-56040 41 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 |
8-83399 8 days ago |
8-83399 8 days ago |
8-83524 8 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 |
8-71049 8 days ago |
14-72270 14 days ago |
14-72479 14 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 |
8-70938 8 days ago |
12-31200 12 days ago |
14-55011 14 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 |
8-70743 8 days ago |
30-67568 1 month ago |
30-67735 30 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 |
8-68539 8 days ago |
30-65675 1 month ago |
30-65664 30 days |
| 22231 |
pechersky author:pechersky |
feat(Algebra/Valued): `AdicExpansion` initial defns |
---
[](https://gitpod.io/from-referrer/)
|
t-algebra
t-topology
label:t-algebra$ |
268/0 |
Mathlib.lean,Mathlib/Topology/Algebra/Valued/AdicExpansion.lean |
2 |
2 |
['Thmoas-Guan', 'github-actions'] |
nobody |
8-61354 8 days ago |
30-11846 1 month ago |
30-11979 30 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 |
8-55497 8 days ago |
10-24234 10 days ago |
15-24778 15 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 |
8-51110 8 days ago |
8-51213 8 days ago |
14-1727 14 days |
| 21488 |
imbrem author:imbrem |
feat(CategoryTheory/Monoidal): premonoidal categories |
Add support for premonoidal categories
---
Still want to add support for:
- Premonoidal braided/symmetric categories
- The monoidal coherence theorem, which I've already ported in my `discretion` library
- The `coherence` tactic, which should work fine for premonoidal categories too
but wanted to get this in front of reviewers ASAP to make sure my general approach was alright
[](https://gitpod.io/from-referrer/)
|
new-contributor
t-category-theory
|
893/354 |
Mathlib/Algebra/Category/ModuleCat/Presheaf/Monoidal.lean,Mathlib/CategoryTheory/Bicategory/End.lean,Mathlib/CategoryTheory/GradedObject/Monoidal.lean,Mathlib/CategoryTheory/Localization/Monoidal.lean,Mathlib/CategoryTheory/Monoidal/Braided/Basic.lean,Mathlib/CategoryTheory/Monoidal/Category.lean,Mathlib/CategoryTheory/Monoidal/Center.lean,Mathlib/CategoryTheory/Monoidal/CoherenceLemmas.lean,Mathlib/CategoryTheory/Monoidal/Discrete.lean,Mathlib/CategoryTheory/Monoidal/End.lean,Mathlib/CategoryTheory/Monoidal/Free/Basic.lean,Mathlib/CategoryTheory/Monoidal/Functor.lean,Mathlib/CategoryTheory/Monoidal/FunctorCategory.lean,Mathlib/CategoryTheory/Monoidal/Mon_.lean,Mathlib/CategoryTheory/Monoidal/Opposite.lean,Mathlib/CategoryTheory/Monoidal/Transport.lean,Mathlib/Tactic/CategoryTheory/Monoidal/Datatypes.lean,Mathlib/Tactic/CategoryTheory/Monoidal/Normalize.lean,Mathlib/Tactic/CategoryTheory/Monoidal/PureCoherence.lean,Mathlib/Tactic/CategoryTheory/MonoidalComp.lean,MathlibTest/StringDiagram.lean |
21 |
3 |
['YaelDillies', 'github-actions', 'imbrem'] |
nobody |
8-48864 8 days ago |
44-55798 1 month ago |
48-17125 48 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 |
8-44053 8 days ago |
8-44875 8 days ago |
8-45055 8 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 |
8-43664 8 days ago |
8-51909 8 days ago |
70-77086 70 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 |
['LeoDog896', 'github-actions', 'tannerduve'] |
nobody |
8-43160 8 days ago |
13-45257 13 days ago |
13-45308 13 days |
| 22281 |
robin-carlier author:robin-carlier |
feat(CategoryTheory/DiscreteCategory): binary sums and products of discrete categories |
We show that if `C` and `D` are discrete categories, then `C ⊕ D` and `C × D` are also discrete categories. This is stated both in terms of equivalences `Discrete (J × K) ≌ Discrete J × Discrete K` and `Discrete (J ⊕ K) ≌ Discrete J ⊕ Discrete K`, and in terms of the `IsDiscrete` typeclass.
We also implement a small refactor by creating a directory `CategoryTheory/DiscreteCategory` and moving `CategoryTheory/DiscreteCategory.lean` to `CategoryTheory/DiscreteCategory/Basic.lean`.
---
I opted for the creation of a separate directory about `DiscreteCategory` so that one could still import `DiscreteCategory.Basic` but not necessarily the content of this PR, which imports `CategoryTheory.Sums.Basic` and `CategoryTheory.Products.Basic`.
[](https://gitpod.io/from-referrer/)
|
t-category-theory |
99/14 |
Mathlib.lean,Mathlib/CategoryTheory/Bicategory/LocallyDiscrete.lean,Mathlib/CategoryTheory/Category/Cat.lean,Mathlib/CategoryTheory/Discrete/Basic.lean,Mathlib/CategoryTheory/Discrete/SumsProducts.lean,Mathlib/CategoryTheory/FinCategory/Basic.lean,Mathlib/CategoryTheory/Groupoid/Discrete.lean,Mathlib/CategoryTheory/Limits/Cones.lean,Mathlib/CategoryTheory/Limits/Opposites.lean,Mathlib/CategoryTheory/Limits/Shapes/BinaryProducts.lean,Mathlib/CategoryTheory/Limits/Shapes/Products.lean,Mathlib/CategoryTheory/Monoidal/Discrete.lean,Mathlib/CategoryTheory/Monoidal/Free/Coherence.lean,Mathlib/CategoryTheory/PEmpty.lean,Mathlib/CategoryTheory/PUnit.lean,Mathlib/CategoryTheory/Products/Unitor.lean |
16 |
8 |
['callesonne', 'github-actions', 'joelriou', 'robin-carlier'] |
nobody |
8-39749 8 days ago |
11-65015 11 days ago |
21-62428 21 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 |
8-38979 8 days ago |
21-26182 21 days ago |
28-25781 28 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 |
8-38904 8 days ago |
8-38910 8 days ago |
55-28763 55 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 |
8-36763 8 days ago |
8-39594 8 days ago |
8-39584 8 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 |
8-13457 8 days ago |
25-56313 25 days ago |
25-56364 25 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 |
7-85697 7 days ago |
27-60778 27 days ago |
28-82977 28 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 |
7-85413 7 days ago |
8-5132 8 days ago |
8-5122 8 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 |
7-80048 7 days ago |
7-80063 7 days ago |
15-27106 15 days |
| 23034 |
plp127 author:plp127 |
feat: `AddMonoidWithOne.toCharZero` |
This replaces `StrictOrderedSemiring.toCharZero`.
Requested by @vihdzp in [#Is there code for X? > OrderedAddCommGroup has CharZero](https://leanprover.zulipchat.com/#narrow/channel/217875-Is-there-code-for-X.3F/topic/OrderedAddCommGroup.20has.20CharZero)
---
[](https://gitpod.io/from-referrer/)
|
t-algebra label:t-algebra$ |
7/2 |
Mathlib/Algebra/Order/Ring/Defs.lean |
1 |
7 |
['eric-wieser', 'github-actions', 'leanprover-bot', 'leanprover-community-mathlib4-bot', 'plp127'] |
nobody |
7-70712 7 days ago |
8-9808 8 days ago |
8-17293 8 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 |
7-64408 7 days ago |
7-65014 7 days ago |
7-65066 7 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 |
7-63383 7 days ago |
21-47787 21 days ago |
21-47784 21 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 |
7-58728 7 days ago |
7-58728 7 days ago |
7-58786 7 days |
| 23055 |
FLDutchmann author:FLDutchmann |
feat(Analysis/Asymptotics): `=O[atTop]` for sequences implies `=O[l]` for any filter `l` |
Prove that `a =O[atTop] b` implies `a =O[l] b` for `a` and `b` natural sequences such that `b n = 0 -> a n = 0` eventually in `l`. I've found this result helpful for deducing uniform bounds from tail bounds.
---
[](https://gitpod.io/from-referrer/)
|
t-analysis |
9/0 |
Mathlib/Analysis/Asymptotics/Lemmas.lean |
1 |
1 |
['github-actions'] |
nobody |
7-54861 7 days ago |
7-54928 7 days ago |
7-54918 7 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 |
7-48770 7 days ago |
7-48771 7 days ago |
7-51821 7 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 |
7-46853 7 days ago |
7-46955 7 days ago |
7-46963 7 days |
| 22832 |
xroblot author:xroblot |
feat(Ring/Divisibility): add `Equiv.dvd` and two instances about `CancelMonoid` |
We add the equivalence between `G` and the set of elements of `G` divisible by `g` where `G` is a `LeftCancelSemiGroup` and `g : G`.
We also add instances saying that, if the monoid with zero `M` is `LeftCancelMulZero` (resp. `RightCancelMulZero`), then the submonoid of nonzero divisors is a `LeftCancelMonoid` (resp. `RightCancelMonoid`). This is needed (well, the left version one) so that we can apply the above equivalence to the monoid of nonzero integral ideals of a Dedekind ring.
This PR is part of the proof of the Analytic Class Number Formula.
---
[](https://gitpod.io/from-referrer/)
|
t-algebra label:t-algebra$ |
29/0 |
Mathlib/Algebra/GroupWithZero/NonZeroDivisors.lean,Mathlib/Algebra/Ring/Divisibility/Basic.lean |
2 |
12 |
['github-actions', 'leanprover-bot', 'urkud', 'xroblot'] |
nobody |
7-45245 7 days ago |
8-76083 8 days ago |
14-32800 14 days |
| 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
|
276/15 |
Mathlib.lean,Mathlib/Data/Nat/Factorization/Basic.lean,Mathlib/Data/Nat/Factorization/Multiplicity.lean,Mathlib/Data/Nat/Multiplicity.lean |
4 |
25 |
['Kevew', 'Paul-Lez', 'github-actions'] |
Kevew assignee:Kevew |
7-40474 7 days ago |
12-20990 12 days ago |
22-51344 22 days |
| 23069 |
JovanGerb author:JovanGerb |
perf: use `singlePass := true` in main loop of `ring_nf` |
TODO: the same change for `abel_nf`.
In the current situation, ring normalization is tried again on each already normalized expression, because `simp` wants to be sure it doesn't simplify any further. `singlePass := true` bypasses this.
Besides performance, there is another reason to use `singlePass := true`:
when there are bound variables, and `simp` does multiple passes, then in the second pass, the bound variable is introduced as a different fresh variable, which confuses the `AtomM` equality of atoms used by `ring`. So I need this for #22956
I also noticed that `Context.simp` only needs a `MetaM` monad and not a `SimpM` monad.
---
[](https://gitpod.io/from-referrer/)
|
t-meta |
5/5 |
Mathlib/Tactic/Ring/RingNF.lean |
1 |
4 |
['github-actions', 'leanprover-bot', 'leanprover-community-mathlib4-bot'] |
nobody |
7-37672 7 days ago |
7-37672 7 days ago |
7-37666 7 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 |
6-79338 6 days ago |
8-38040 8 days ago |
20-16438 20 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 |
6-77591 6 days ago |
6-77591 6 days ago |
10-31697 10 days |
| 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
|
248/21 |
Mathlib/CategoryTheory/Subobject/Basic.lean,Mathlib/CategoryTheory/Subobject/Presheaf.lean,Mathlib/CategoryTheory/Topos/Classifier.lean |
3 |
18 |
['Champitoad', 'github-actions', 'joelriou'] |
nobody |
6-73323 6 days ago |
6-73323 6 days ago |
9-2492 9 days |
| 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
|
246/1 |
Mathlib/NumberTheory/SelbergSieve.lean |
1 |
2 |
['github-actions', 'mathlib4-dependent-issues-bot'] |
nobody |
6-54674 6 days ago |
6-55869 6 days ago |
6-55858 6 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 |
6-51755 6 days ago |
7-44297 7 days ago |
7-44350 7 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 |
6-45872 6 days ago |
7-60751 7 days ago |
8-72551 8 days |
| 23102 |
YaelDillies author:YaelDillies |
chore(Set): strengthen `encard_lt_encard` |
and make `Finite.eq_of_subset_of_encard_le` be more immediately general than `Finite.eq_of_subset_of_encard_le'` rather than the other way around to ensure people don't accidentally write undergeneralised proofs using it.
From my PhD (MiscYD)
---
[](https://gitpod.io/from-referrer/)
|
t-data |
12/12 |
Mathlib/Data/Matroid/Rank/Cardinal.lean,Mathlib/Data/Set/Card.lean |
2 |
12 |
['YaelDillies', 'b-mehta', 'github-actions'] |
nobody |
6-30713 6 days ago |
6-46795 6 days ago |
6-46844 6 days |
| 23105 |
YaelDillies author:YaelDillies |
chore: make sure that simp can prove that a finite set is relatively compact |
Make `Set.Finite.isClosed`, `IsClosed.closure_eq` and `Set.Finite.isCompact` simp lemmas so that the following works:
```
import Mathlib
example {X : Type*} [TopologicalSpace X] {s : Set X} (hs : s.Finite) : IsCompact (closure s) := by simp
```
From my PhD (MiscYD)
---
[](https://gitpod.io/from-referrer/)
|
t-topology |
5/10 |
Mathlib/Topology/Basic.lean,Mathlib/Topology/Compactness/Compact.lean,Mathlib/Topology/Order.lean,Mathlib/Topology/Separation/Basic.lean |
4 |
1 |
['github-actions'] |
nobody |
6-24045 6 days ago |
6-24045 6 days ago |
6-38075 6 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 |
6-22697 6 days ago |
8-38876 8 days ago |
45-21059 45 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 |
6-5739 6 days ago |
6-72255 6 days ago |
6-74158 6 days |
| 23132 |
urkud author:urkud |
feat: the separation quotient of a finite module is a finite module |
---
[](https://gitpod.io/from-referrer/)
|
t-algebra
t-topology
label:t-algebra$ |
21/0 |
Mathlib.lean,Mathlib/Topology/Algebra/SeparationQuotient/FiniteDimensional.lean |
2 |
1 |
['github-actions'] |
nobody |
5-86166 5 days ago |
5-86230 5 days ago |
5-86240 5 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 |
120/0 |
Mathlib.lean,Mathlib/Topology/Sets/Closeds.lean,Mathlib/Topology/UniformSpace/CoveringProfinite.lean |
3 |
5 |
['github-actions', 'loefflerd', 'mathlib4-dependent-issues-bot', 'urkud'] |
nobody |
5-79851 5 days ago |
22-35257 22 days ago |
22-36194 22 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 |
5-76203 5 days ago |
16-27343 16 days ago |
16-27330 16 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 |
5-74604 5 days ago |
6-27563 6 days ago |
6-27610 6 days |
| 23020 |
YaelDillies author:YaelDillies |
feat(Finset): extra `toLeft`/`toRight` API |
Add the API that I independently came up with in https://github.com/leanprover-community/mathlib4/pull/20433#issuecomment-2607541838.
---
[](https://gitpod.io/from-referrer/)
|
t-data |
61/17 |
Mathlib/Data/Finset/Sum.lean,Mathlib/Data/Fintype/Sum.lean |
2 |
18 |
['YaelDillies', 'b-mehta', 'eric-wieser', 'fpvandoorn', 'github-actions'] |
nobody |
5-71316 5 days ago |
6-76047 6 days ago |
7-45570 7 days |
| 23137 |
grunweg author:grunweg |
chore(Topology): some more fun_prop tagging |
---
[](https://gitpod.io/from-referrer/)
|
|
12/8 |
Mathlib/Dynamics/Flow.lean,Mathlib/Topology/Algebra/Monoid.lean,Mathlib/Topology/Homotopy/Basic.lean |
3 |
1 |
['github-actions'] |
nobody |
5-69710 5 days ago |
5-69772 5 days ago |
5-69762 5 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 |
5-69133 5 days ago |
19-67478 19 days ago |
19-67525 19 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 |
5-67447 5 days ago |
5-67465 5 days ago |
5-75388 5 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 |
5-55657 5 days ago |
5-57943 5 days ago |
5-58002 5 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 |
5-51355 5 days ago |
5-54843 5 days ago |
5-54896 5 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 |
5-49408 5 days ago |
5-51003 5 days ago |
5-51057 5 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 |
5-47859 5 days ago |
6-42753 6 days ago |
6-44007 6 days |
| 23113 |
pechersky author:pechersky |
feat(Order/Filter/Finite): generate_image_preimage_le_comap |
---
[](https://gitpod.io/from-referrer/)
|
t-order
easy
|
9/0 |
Mathlib/Order/Filter/Finite.lean |
1 |
2 |
['Ruben-VandeVelde', 'github-actions'] |
nobody |
5-35290 5 days ago |
6-37321 6 days ago |
6-37380 6 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 |
5-34206 5 days ago |
9-75893 9 days ago |
14-52001 14 days |
| 23131 |
j-loreaux author:j-loreaux |
feat: adds `Real.nnreal_dichotomy` for principled case splits into nonnegative and nonpositive options |
---
[](https://gitpod.io/from-referrer/)
|
t-data |
30/0 |
Mathlib/Data/NNReal/Defs.lean |
1 |
4 |
['Ruben-VandeVelde', 'github-actions'] |
nobody |
5-29409 5 days ago |
6-5129 6 days ago |
6-5139 6 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$ |
223/0 |
Mathlib.lean,Mathlib/LinearAlgebra/SymmetricAlgebra/Basic.lean,Mathlib/LinearAlgebra/SymmetricAlgebra/MvPolynomial.lean |
3 |
8 |
['ADedecker', 'Raph-DG', 'github-actions', 'xyzw12345'] |
nobody |
5-23496 5 days ago |
46-71301 1 month ago |
46-71351 46 days |
| 23126 |
kim-em author:kim-em |
chore: rename `Set.dual_Ixx` to `Ixx_toDual`, and add `Set.Ixx_ofDual` |
This is an excursion during the `erw`-killing quest. |
t-order |
114/46 |
Mathlib/MeasureTheory/Constructions/BorelSpace/Order.lean,Mathlib/Order/Bounds/Basic.lean,Mathlib/Order/Interval/Basic.lean,Mathlib/Order/Interval/Set/Basic.lean,Mathlib/Order/Interval/Set/Disjoint.lean,Mathlib/Order/Interval/Set/OrdConnected.lean,Mathlib/Order/Interval/Set/OrdConnectedComponent.lean,Mathlib/Order/Interval/Set/UnorderedInterval.lean,Mathlib/Order/SuccPred/IntervalSucc.lean,Mathlib/Topology/Order/Basic.lean,Mathlib/Topology/Order/Compact.lean,Mathlib/Topology/Order/DenselyOrdered.lean,Mathlib/Topology/Order/ExtendFrom.lean,Mathlib/Topology/Order/IsLUB.lean,Mathlib/Topology/Order/LeftRightNhds.lean |
15 |
1 |
['github-actions'] |
nobody |
5-22827 5 days ago |
6-21426 6 days ago |
6-21482 6 days |
| 23086 |
qawbecrdtey author:qawbecrdtey |
feat(Mathlib/Dynamics/PeriodicPts/Lemmas): Added lemmas about `periodicPts` on `Fintype` |
---
There is one auxiliary lemma added in `Mathlib/Dynamics/PeriodicPts/Basic`, which is `periodicPts_subset_image`.
All other lemmas are placed in `Mathlib/Dynamics/PeriodicPts/Lemmas`.
[](https://gitpod.io/from-referrer/)
|
t-dynamics |
58/0 |
Mathlib/Dynamics/PeriodicPts/Defs.lean,Mathlib/Dynamics/PeriodicPts/Lemmas.lean |
2 |
7 |
['Ruben-VandeVelde', 'b-mehta', 'github-actions', 'qawbecrdtey'] |
nobody |
5-20772 5 days ago |
6-80999 6 days ago |
6-81053 6 days |
| 22038 |
euprunin author:euprunin |
feat: add `aesop` annotations for `dvd_mul_of_dvd_left`/`right` |
Example:
```
import Mathlib
example (x y z : ℕ) : x ∣ y * x * z := by aesop
``` |
t-algebra label:t-algebra$ |
2/0 |
Mathlib/Algebra/Divisibility/Basic.lean |
1 |
14 |
['Parcly-Taxel', 'euprunin', 'github-actions', 'leanprover-bot', 'urkud'] |
nobody |
5-3073 5 days ago |
35-70173 1 month ago |
35-70283 35 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 |
5-313 5 days ago |
7-33133 7 days ago |
7-33183 7 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 |
4-86211 4 days ago |
32-58912 1 month ago |
32-58965 32 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
|
68/3 |
Mathlib/Combinatorics/SimpleGraph/Clique.lean,Mathlib/Combinatorics/SimpleGraph/Coloring.lean,Mathlib/Combinatorics/SimpleGraph/Triangle/Basic.lean |
3 |
14 |
['IvanRenison', 'b-mehta', 'github-actions', 'jt496', 'kbuzzard'] |
nobody |
4-78338 4 days ago |
4-78339 4 days ago |
45-78416 45 days |
| 22116 |
smmercuri author:smmercuri |
feat: `Fin.castPred_ne_zero` and `Pairwise.forall_fin_two` |
---
[](https://gitpod.io/from-referrer/)
|
|
5/0 |
Mathlib/Data/Fin/Basic.lean |
1 |
7 |
['github-actions', 'kbuzzard', 'smmercuri', 'urkud'] |
nobody |
4-77036 4 days ago |
4-77125 4 days ago |
29-64089 29 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 |
6 |
['github-actions', 'leanprover-bot', 'smmercuri', 'urkud'] |
nobody |
4-70358 4 days ago |
22-76985 22 days ago |
22-77033 22 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 |
37/37 |
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/Real/IsNonarchimedean.lean,Mathlib/Data/Set/MulAntidiagonal.lean,Mathlib/Data/ZMod/Basic.lean |
15 |
8 |
['eric-wieser', 'github-actions', 'leanprover-bot', 'vlad902'] |
nobody |
4-64441 4 days ago |
5-57970 5 days ago |
5-58039 5 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 |
4-64439 4 days ago |
4-66288 4 days ago |
4-66342 4 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 |
4-61322 4 days ago |
4-62484 4 days ago |
6-15039 6 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 |
92/0 |
Mathlib/CategoryTheory/Equivalence.lean |
1 |
1 |
['github-actions'] |
nobody |
4-49749 4 days ago |
4-49749 4 days ago |
4-49760 4 days |
| 23204 |
mariainesdff author:mariainesdff |
feat(Data/List/MinMax): add le_max_of_le' |
---
[](https://gitpod.io/from-referrer/)
|
t-data |
11/0 |
Mathlib/Data/List/MinMax.lean |
1 |
1 |
['github-actions'] |
nobody |
4-47804 4 days ago |
4-47863 4 days ago |
4-47853 4 days |
| 23189 |
vlad902 author:vlad902 |
feat: generalize Mathlib.Analysis |
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-analysis |
42/37 |
Mathlib/Analysis/Analytic/Constructions.lean,Mathlib/Analysis/Analytic/IsolatedZeros.lean,Mathlib/Analysis/Asymptotics/Lemmas.lean,Mathlib/Analysis/Asymptotics/SpecificAsymptotics.lean,Mathlib/Analysis/Asymptotics/TVS.lean,Mathlib/Analysis/Calculus/Deriv/Mul.lean,Mathlib/Analysis/Complex/UpperHalfPlane/FunctionsBoundedAtInfty.lean,Mathlib/Analysis/Convex/Combination.lean,Mathlib/Analysis/Hofer.lean,Mathlib/Analysis/InnerProductSpace/PiL2.lean,Mathlib/Analysis/LocallyConvex/Bounded.lean,Mathlib/Analysis/Matrix.lean,Mathlib/Analysis/MellinTransform.lean,Mathlib/Analysis/Normed/Algebra/Spectrum.lean,Mathlib/Analysis/Normed/Group/Hom.lean,Mathlib/Analysis/Normed/Operator/Banach.lean,Mathlib/Analysis/Normed/Ring/Basic.lean,Mathlib/Analysis/Normed/Unbundled/RingSeminorm.lean,Mathlib/Analysis/RCLike/Basic.lean,Mathlib/Analysis/SpecialFunctions/ContinuousFunctionalCalculus/Rpow/Basic.lean |
20 |
7 |
['github-actions', 'j-loreaux', 'leanprover-bot', 'vlad902'] |
nobody |
4-46751 4 days ago |
4-55137 4 days ago |
4-55191 4 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 |
4-46022 4 days ago |
4-55771 4 days ago |
4-55830 4 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 |
4-45659 4 days ago |
4-54629 4 days ago |
4-54687 4 days |
| 23178 |
mariainesdff author:mariainesdff |
feat: add iSup lemmas |
---
[](https://gitpod.io/from-referrer/)
|
large-import
t-order
|
77/1 |
Mathlib/Data/Real/Pointwise.lean,Mathlib/Order/ConditionallyCompleteLattice/Finset.lean,Mathlib/Order/ConditionallyCompleteLattice/Indexed.lean |
3 |
3 |
['D-Thomine', 'github-actions'] |
nobody |
4-45503 4 days ago |
4-60290 4 days ago |
4-60332 4 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 |
4-44992 4 days ago |
4-55114 4 days ago |
4-55165 4 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 |
4-43761 4 days ago |
4-55128 4 days ago |
4-55178 4 days |
| 23193 |
vlad902 author:vlad902 |
feat: generalize Mathlib.Topology |
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-topology |
67/49 |
Mathlib/Topology/Algebra/Algebra.lean,Mathlib/Topology/Algebra/Group/Basic.lean,Mathlib/Topology/Algebra/InfiniteSum/Module.lean,Mathlib/Topology/Algebra/Module/Cardinality.lean,Mathlib/Topology/Algebra/Module/Star.lean,Mathlib/Topology/Algebra/Module/StrongTopology.lean,Mathlib/Topology/Algebra/Monoid.lean,Mathlib/Topology/Algebra/ProperAction/Basic.lean,Mathlib/Topology/Algebra/Support.lean,Mathlib/Topology/Algebra/UniformMulAction.lean,Mathlib/Topology/ContinuousMap/Periodic.lean,Mathlib/Topology/ContinuousMap/StoneWeierstrass.lean,Mathlib/Topology/DenseEmbedding.lean,Mathlib/Topology/EMetricSpace/Basic.lean,Mathlib/Topology/List.lean,Mathlib/Topology/MetricSpace/Basic.lean,Mathlib/Topology/PartitionOfUnity.lean,Mathlib/Topology/Separation/Basic.lean,Mathlib/Topology/Separation/CompletelyRegular.lean,Mathlib/Topology/UniformSpace/Cauchy.lean |
20 |
4 |
['github-actions', 'leanprover-bot', 'vlad902'] |
nobody |
4-41714 4 days ago |
4-54197 4 days ago |
4-54248 4 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 |
4-39895 4 days ago |
4-53798 4 days ago |
4-53856 4 days |
| 23195 |
vlad902 author:vlad902 |
feat: generalize Mathlib.Algebra.BigOperators + CharP + Star + misc others |
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$ |
44/44 |
Mathlib/Algebra/AddConstMap/Basic.lean,Mathlib/Algebra/AlgebraicCard.lean,Mathlib/Algebra/BigOperators/Fin.lean,Mathlib/Algebra/BigOperators/Finprod.lean,Mathlib/Algebra/BigOperators/GroupWithZero/Action.lean,Mathlib/Algebra/BigOperators/Pi.lean,Mathlib/Algebra/BigOperators/Ring/List.lean,Mathlib/Algebra/BigOperators/RingEquiv.lean,Mathlib/Algebra/CharP/Algebra.lean,Mathlib/Algebra/CharP/Defs.lean,Mathlib/Algebra/DirectSum/Basic.lean,Mathlib/Algebra/GeomSum.lean,Mathlib/Algebra/RingQuot.lean,Mathlib/Algebra/Star/Basic.lean,Mathlib/Algebra/Star/NonUnitalSubalgebra.lean,Mathlib/Algebra/Star/Pointwise.lean,Mathlib/Algebra/Star/SelfAdjoint.lean |
17 |
4 |
['github-actions', 'leanprover-bot', 'vlad902'] |
nobody |
4-38959 4 days ago |
4-52705 4 days ago |
4-52772 4 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 |
4-37411 4 days ago |
5-39528 5 days ago |
5-39527 5 days |
| 22278 |
robin-carlier author:robin-carlier |
feat(CategoryTheory/Sums/Basic): functors out of `Sum` |
We prove that the category structure defined in `CategoryTheory/Sums/Basic` satisfies a universal property that exhibits it as the binary coproduct of categories. In practive, this means that we construct an equivalence of categories `(A ⊕ A') ⥤ B ≌ (A ⥤ B) × (A' ⥤ B)`, which we characterize via its compositions in both directions with `Sum.inl_`, `Sum.inr_`, `Prod.fst` and `Prod.snd`.
---
I was unsure whether or not this should go in a separate new file in the `CategoryTheory/Sum` directory, as it brings the product as import, but it seems that this file was almost never imported anyways, so that it would be harmless to keep fragmentation to a minimum here.
[](https://gitpod.io/from-referrer/)
|
t-category-theory |
168/2 |
Mathlib.lean,Mathlib/CategoryTheory/Sums/Basic.lean,Mathlib/CategoryTheory/Sums/Products.lean |
3 |
15 |
['b-mehta', 'github-actions', 'joelriou', 'robin-carlier'] |
nobody |
4-31521 4 days ago |
4-31521 4 days ago |
23-30494 23 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
|
55/0 |
Mathlib/Analysis/SpecialFunctions/ImproperIntegrals.lean |
1 |
1 |
['github-actions'] |
nobody |
4-14903 4 days ago |
4-15054 4 days ago |
4-15109 4 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 |
4-14485 4 days ago |
unknown |
unknown |
| 22705 |
Thmoas-Guan author:Thmoas-Guan |
feat(Algebra/DirectSum): add lemma about ker and range of DirectSum.map |
Add lemma about ker and range of DirectSum.map.
---
[](https://gitpod.io/from-referrer/)
|
t-algebra label:t-algebra$ |
80/0 |
Mathlib/Algebra/DirectSum/Basic.lean,Mathlib/Algebra/DirectSum/Module.lean |
2 |
22 |
['Thmoas-Guan', 'eric-wieser', 'github-actions'] |
nobody |
4-7830 4 days ago |
4-7830 4 days ago |
17-26374 17 days |
| 23188 |
riccardobrasca author:riccardobrasca |
feat: generalize coercion from polynomial to power series to semirings |
We generalize the coercion `R[X] → R⟦X⟧` from `CommSemiring R` to `Semiring R`.
---
[](https://gitpod.io/from-referrer/)
|
t-algebra label:t-algebra$ |
26/22 |
Mathlib/RingTheory/PowerSeries/Basic.lean |
1 |
8 |
['github-actions', 'leanprover-bot', 'leanprover-community-mathlib4-bot', 'riccardobrasca'] |
nobody |
3-67455 3 days ago |
3-67589 3 days ago |
4-55644 4 days |
| 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 |
3-64291 3 days ago |
3-67909 3 days ago |
3-67963 3 days |
| 23198 |
robin-carlier author:robin-carlier |
feat(CategoryTheory/Equivalence): functoriality of symmetry of equivalences |
We introduce a file `CategoryTheory/Equivalence/Symmetry` in which we continue to provide basic API for the category structure on equivalences defined in #23197. We prove that symmetry of equivalences defines an equivalence `(C ≌ D) ≌ (D ≌ C)ᵒᵖ`, and we use this to construct `Equivalence.inverseFunctor: (C ≌ D) ⥤ (D ⥤ C)ᵒᵖ` that takes an equivalence to its inverse functor, and to promote `Equivalence.congrLeft` to a functor.
---
- [ ] depends of: #23197
[](https://gitpod.io/from-referrer/)
|
t-category-theory |
216/0 |
Mathlib.lean,Mathlib/CategoryTheory/Equivalence.lean,Mathlib/CategoryTheory/Equivalence/Symmetry.lean |
3 |
1 |
['github-actions'] |
nobody |
3-62695 3 days ago |
3-62695 3 days ago |
3-62727 3 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 |
3-57260 3 days ago |
3-60805 3 days ago |
3-60855 3 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 |
3-19486 3 days ago |
3-35979 3 days ago |
3-36033 3 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 |
3-16281 3 days ago |
22-25075 22 days ago |
23-53852 23 days |
| 22967 |
j-loreaux author:j-loreaux |
refactor: default to left modules for `CStarModule` |
When `CStarModule` was introduced, the hypotheses assumed a *right* action of the C⋆-algebra `A` on the module `E` (i.e., a `SMul Aᵐᵒᵖ E` instance). On the one hand, this is consistent with the literature (which also defaults to right-actions), but on the other hand, it will cause problems in the future. In particular, we will need to consider C⋆-bimodules, but if we default to right actions, then to get a left C⋆-module structure we would need a `SMul (Aᵐᵒᵖ)ᵐᵒᵖ E` instance.
In this PR we switch so that the default for `CStarModule`s are left-actions, consistent with the rest of Mathlib.
In addition, we remove the `outParam` condition on `A` in the `CStarModule` class. Indeed, we may need to consider C⋆-modules over multiple C⋆-algebras simultaneously (the canonical example is `A` and its unitization `A⁺¹`, which arises frequently). This necessitates a change to the type synonym `WithCStarModule` so that `A` is an explicit parameter. In addition, the variable `A` is now explicit in a few declarations which otherwise only mention terms of `E` and their norms (e.g., `CStarModule.norm_sq_eq`).
---
- [ ] depends on: #23047
[](https://gitpod.io/from-referrer/)
|
t-analysis |
330/310 |
Mathlib/Analysis/CStarAlgebra/Basic.lean,Mathlib/Analysis/CStarAlgebra/CStarMatrix.lean,Mathlib/Analysis/CStarAlgebra/Module/Constructions.lean,Mathlib/Analysis/CStarAlgebra/Module/Defs.lean,Mathlib/Analysis/CStarAlgebra/Module/Synonym.lean,Mathlib/Analysis/Matrix.lean,Mathlib/Analysis/Normed/Lp/lpSpace.lean,Mathlib/Topology/ContinuousMap/Bounded/Star.lean,Mathlib/Topology/ContinuousMap/Compact.lean,Mathlib/Topology/ContinuousMap/ZeroAtInfty.lean |
10 |
2 |
['github-actions', 'mathlib4-dependent-issues-bot'] |
nobody |
3-16092 3 days ago |
3-16094 3 days ago |
3-16917 3 days |
| 19865 |
mitchell-horner author:mitchell-horner |
feat(Combinatorics/SimpleGraph): define extremalNumber |
Define the extremal number `extremalNumber n H` of a natural number `n` and a simple graph `H`: `extremalNumber n H` is the maximum number of edges in a `H`-free simple graph on `n` vertices, if `H` is contained in all simple graphs on `n` vertices, then this is `0`.
Also define the predicate that a simple graph is an extremal graph `IsExtremal` satisfying some predicate.
---
- [x] depends on: #20658
[](https://gitpod.io/from-referrer/)
|
new-contributor
t-combinatorics
|
174/5 |
Mathlib.lean,Mathlib/Combinatorics/SimpleGraph/Copy.lean,Mathlib/Combinatorics/SimpleGraph/Extremal/Basic.lean |
3 |
13 |
['YaelDillies', 'b-mehta', 'github-actions', 'kim-em', 'mathlib4-dependent-issues-bot', 'mitchell-horner'] |
nobody |
3-6262 3 days ago |
3-72855 3 days ago |
40-11076 40 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 |
2-74012 2 days ago |
3-2814 3 days ago |
3-2804 3 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 |
2-72661 2 days ago |
2-72675 2 days ago |
25-82542 25 days |
| 23082 |
Parcly-Taxel author:Parcly-Taxel |
chore: clear `docBlame` nolints in `CategoryTheory` |
Split from #22754.
---
@joelriou and other competent people are hereby allowed to edit this PR directly to improve the docstrings or add them in places I missed. |
tech debt
t-category-theory
documentation
|
84/90 |
Mathlib/CategoryTheory/Action/Basic.lean,Mathlib/CategoryTheory/Bicategory/Basic.lean,Mathlib/CategoryTheory/Bicategory/Free.lean,Mathlib/CategoryTheory/Comma/Basic.lean,Mathlib/CategoryTheory/Enriched/Basic.lean,Mathlib/CategoryTheory/GlueData.lean,Mathlib/CategoryTheory/Groupoid/Subgroupoid.lean,Mathlib/CategoryTheory/Limits/Shapes/DisjointCoproduct.lean,Mathlib/CategoryTheory/Limits/Shapes/Multiequalizer.lean,Mathlib/CategoryTheory/Monad/Monadicity.lean,Mathlib/CategoryTheory/Monoidal/Bimod.lean,Mathlib/CategoryTheory/Monoidal/Center.lean,Mathlib/CategoryTheory/Monoidal/Mod_.lean,Mathlib/CategoryTheory/Monoidal/Mon_.lean,Mathlib/CategoryTheory/Preadditive/Mat.lean,Mathlib/CategoryTheory/Preadditive/Projective/Basic.lean,Mathlib/CategoryTheory/Shift/CommShift.lean,Mathlib/CategoryTheory/Sites/Pretopology.lean,Mathlib/CategoryTheory/Sites/SheafOfTypes.lean,Mathlib/CategoryTheory/Triangulated/Basic.lean,Mathlib/CategoryTheory/Triangulated/Triangulated.lean,Mathlib/Topology/Gluing.lean,Mathlib/Topology/Sheaves/CommRingCat.lean,scripts/nolints.json |
24 |
5 |
['Parcly-Taxel', 'b-mehta', 'github-actions'] |
nobody |
2-68706 2 days ago |
7-12830 7 days ago |
7-12820 7 days |
| 22864 |
urkud author:urkud |
chore(TorusIntegral): fix porting note |
Use the superscript macro for notation like `ℝⁿ` etc
---
[](https://gitpod.io/from-referrer/) |
t-measure-probability |
6/7 |
Mathlib/MeasureTheory/Integral/TorusIntegral.lean |
1 |
2 |
['github-actions', 'urkud'] |
nobody |
2-60591 2 days ago |
14-9081 14 days ago |
14-9144 14 days |
| 23231 |
urkud author:urkud |
feat(LinearPMap): more lemmas about `supSpanSingleton` |
Also get rid of `erw`.
---
[](https://gitpod.io/from-referrer/)
|
t-algebra label:t-algebra$ |
26/5 |
Mathlib/LinearAlgebra/LinearPMap.lean,Mathlib/LinearAlgebra/Span/Defs.lean |
2 |
1 |
['github-actions'] |
nobody |
2-56181 2 days ago |
2-56240 2 days ago |
2-56230 2 days |
| 23232 |
urkud author:urkud |
chore(Dimension/Finrank): golf, reuse `variable`s |
---
[](https://gitpod.io/from-referrer/) |
t-algebra label:t-algebra$ |
6/12 |
Mathlib/LinearAlgebra/Dimension/Finrank.lean,Mathlib/LinearAlgebra/Dual/Lemmas.lean |
2 |
1 |
['github-actions'] |
nobody |
2-54287 2 days ago |
2-55984 2 days ago |
2-56041 2 days |
| 23228 |
jhanschoo author:jhanschoo |
feat(Data/Int): `m/n/k=m/(n*k)` |
Add a lemma that `m/n/k=m/(n*k)` under `ediv` and `fdiv` for positive divisors. The proof uses basic tactics but uses some lemmas from `Init`, and so imports several files from there.
---
[](https://gitpod.io/from-referrer/)
|
t-data |
34/0 |
Mathlib/Data/Int/DivMod.lean |
1 |
2 |
['Ruben-VandeVelde', 'github-actions'] |
nobody |
2-53199 2 days ago |
2-53205 2 days ago |
3-13449 3 days |
| 23234 |
Ruben-VandeVelde author:Ruben-VandeVelde |
chore: rename round_add_int and related declarations |
---
[](https://gitpod.io/from-referrer/)
|
t-algebra label:t-algebra$ |
34/16 |
Mathlib/Algebra/Order/Round.lean |
1 |
1 |
['github-actions'] |
nobody |
2-52178 2 days ago |
2-52179 2 days ago |
2-52230 2 days |
| 23235 |
urkud author:urkud |
feat(StrongRankCondition): linear combinations with bounded number of terms |
We can represent an element of `Submodule.span K s`
as a linear combination
of at most `Module.finrank K (Submodule.span K s)`
elements of `s`.
---
[](https://gitpod.io/from-referrer/) |
t-algebra label:t-algebra$ |
40/3 |
Mathlib/LinearAlgebra/Dimension/StrongRankCondition.lean |
1 |
1 |
['github-actions'] |
nobody |
2-50292 2 days ago |
2-50292 2 days ago |
2-50345 2 days |
| 22178 |
jsm28 author:jsm28 |
feat(Analysis/Convex/BetweenList): betweenness for lists of points |
Define the notions of a list of points in an affine space being weakly or strictly in order on a line.
---
- [ ] depends on: #21936
[](https://gitpod.io/from-referrer/)
|
t-analysis |
318/0 |
Mathlib.lean,Mathlib/Analysis/Convex/BetweenList.lean |
2 |
2 |
['github-actions', 'mathlib4-dependent-issues-bot'] |
nobody |
2-48602 2 days ago |
20-32299 20 days ago |
20-33899 20 days |
| 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) |
t-combinatorics |
186/2 |
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 |
20 |
['YaelDillies', 'github-actions', 'mathlib4-dependent-issues-bot', 'pimotte'] |
nobody |
2-44098 2 days ago |
3-70795 3 days ago |
3-79080 3 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 |
2-39574 2 days ago |
2-39591 2 days ago |
50-59288 50 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 |
2-38150 2 days ago |
2-38165 2 days ago |
32-81998 32 days |
| 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.
---
[](https://gitpod.io/from-referrer/)
|
t-algebra label:t-algebra$ |
115/86 |
Mathlib/GroupTheory/Congruence/Defs.lean,Mathlib/GroupTheory/Congruence/Hom.lean |
2 |
1 |
['github-actions'] |
nobody |
2-27871 2 days ago |
2-28101 2 days ago |
2-28151 2 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,Mathlib/Combinatorics/SimpleGraph/Walk.lean |
2 |
2 |
['github-actions', 'urkud'] |
nobody |
2-24391 2 days ago |
2-24391 2 days ago |
28-72038 28 days |
| 23245 |
kbuzzard author:kbuzzard |
doc(Algebra/Ring/Action/Invariant): add module docstring |
---
[](https://gitpod.io/from-referrer/)
Currently the module docstring for `Mathlib.Algebra.Ring.Action.Basic` claims that the file contains the "corresponding typeclass of invariant subrings". This has not been true since the mathlib3 PR https://github.com/leanprover-community/mathlib3/pull/17786 which moved the typeclass into its own file (now called `Mathlib.Algebra.Ring.Action.Invariant` in mathlib4). I add a docstring to `Invariant.lean` and remove the incorrect claim from `Basic.lean`.
|
t-algebra
documentation
label:t-algebra$ |
17/5 |
Mathlib/Algebra/Ring/Action/Basic.lean,Mathlib/Algebra/Ring/Action/Invariant.lean |
2 |
1 |
['github-actions'] |
nobody |
2-19961 2 days ago |
2-19964 2 days ago |
2-20012 2 days |
| 23247 |
jsm28 author:jsm28 |
feat(LinearAlgebra/AffineSpace/AffineSubspace/Basic): vector span of union |
Add a variant of `direction_sup` for the case of two affine subspaces with a common point, and deduce:
```lean
lemma vectorSpan_union_of_mem_of_mem {s₁ s₂ : Set P} {p : P} (hp₁ : p ∈ s₁) (hp₂ : p ∈ s₂) :
vectorSpan k (s₁ ∪ s₂) = vectorSpan k s₁ ⊔ vectorSpan k s₂ := by
```
---
[](https://gitpod.io/from-referrer/)
|
t-algebra
easy
label:t-algebra$ |
14/0 |
Mathlib/LinearAlgebra/AffineSpace/AffineSubspace/Basic.lean |
1 |
1 |
['github-actions'] |
nobody |
2-15608 2 days ago |
2-15666 2 days ago |
2-15657 2 days |
| 22847 |
BoltonBailey author:BoltonBailey |
feat(Algebra/Polynomial/BigOperators): Add lemma `degree_list_sum_le_of_forall_degree_le` |
Adds a lemma relating the degree of the sum of a list of polynomials to the degree of the polynomials (unlike `degree_list_sum_le`, which only relates this to the `natDegree` of the polynomials in the list).
Found while trying to contribute to [zkLib](https://github.com/Verified-zkEVM/ZKLib)
---
[](https://gitpod.io/from-referrer/)
|
t-algebra label:t-algebra$ |
20/10 |
Mathlib/Algebra/Polynomial/BigOperators.lean |
1 |
5 |
['BoltonBailey', 'Ruben-VandeVelde', 'github-actions', 'urkud'] |
nobody |
2-13427 2 days ago |
14-41014 14 days ago |
14-41266 14 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$ |
591/0 |
Mathlib.lean,Mathlib/RingTheory/WeierstrassPreparation.lean |
2 |
9 |
['Thmoas-Guan', 'acmepjz', 'github-actions', 'mathlib4-dependent-issues-bot', 'riccardobrasca'] |
riccardobrasca assignee:riccardobrasca |
1-70753 1 day ago |
24-62625 24 days ago |
31-57860 31 days |
| 23252 |
mariainesdff author:mariainesdff |
feat(Algebra/Polynomial): add lemmas |
---
[](https://gitpod.io/from-referrer/)
|
t-algebra label:t-algebra$ |
74/0 |
Mathlib/Algebra/Polynomial/Basic.lean,Mathlib/Algebra/Polynomial/BigOperators.lean,Mathlib/Algebra/Polynomial/Lifts.lean,Mathlib/Algebra/Polynomial/RingDivision.lean,Mathlib/Algebra/Polynomial/Splits.lean |
5 |
1 |
['github-actions'] |
nobody |
1-70594 1 day ago |
1-70652 1 day ago |
1-70642 1 day |
| 23253 |
mariainesdff author:mariainesdff |
feat(Data/Real/IsNonarchimedean): add powerset_image_add lemmas |
---
[](https://gitpod.io/from-referrer/)
|
t-analysis
t-number-theory
|
45/1 |
Mathlib/Data/Real/IsNonarchimedean.lean |
1 |
1 |
['github-actions'] |
nobody |
1-66165 1 day ago |
1-66223 1 day ago |
1-66213 1 day |
| 23255 |
jsm28 author:jsm28 |
refactor(LinearAlgebra/AffineSpace/AffineSubspace): `affineSpan` analogues of `spanPoints` lemmas |
The `spanPoints` definition is only meant to be used for setting up `affineSpan`; once the bundled `affineSpan` is set up, that's what should be used.
Ensure that all `spanPoints` lemmas have `affineSpan` analogues, and move users to using `affineSpan` as far as possible (in particular, all uses outside
`Mathlib/LinearAlgebra/AffineSpace/AffineSubspace/Defs.lean` now use `affineSpan`, where previously some used `spanPoints` lemmas relying on defeq to `affineSpan`).
This would facilitate a potential future cleanup (that I'm not planning to work on), possibly as part of general work on consistency of closure operators in mathlib, to eliminate `spanPoints` (and thus `coe_affineSpan`). I've added a lemma `mem_affineSpan_iff_exists` that provides the mathematical content of the definition of `spanPoints` as a lemma about `affineSpan` that could remain (with a proof that would no longer be `Iff.rfl`) if `spanPoints` is removed.
---
[](https://gitpod.io/from-referrer/)
|
t-algebra label:t-algebra$ |
37/14 |
Mathlib/Geometry/Euclidean/Circumcenter.lean,Mathlib/Geometry/Euclidean/MongePoint.lean,Mathlib/LinearAlgebra/AffineSpace/AffineSubspace/Basic.lean,Mathlib/LinearAlgebra/AffineSpace/AffineSubspace/Defs.lean,Mathlib/LinearAlgebra/AffineSpace/Independent.lean |
5 |
1 |
['github-actions'] |
nobody |
1-63323 1 day ago |
1-63381 1 day ago |
1-63371 1 day |
| 22823 |
b-reinke author:b-reinke |
feat(Mathlib/Algebra/Ring): associator of a non-associative ring |
If `R` is a non-associative ring, then `(x * y) * z - x * (y * z)` is called the `associator` of
ring elements `x y z : R`. We realize the associator as a map that is an `AddMonoidHom` in each
argument. The associator vanishes exactly when `R` is associative. We prove a similar statement for
semirings by directly comparing the maps `mull₃` and `mulr₃`, the `AddMonoidHom` versions of the
multiplications `(x * y) * z` and `x * (y * z)`.
---
[](https://gitpod.io/from-referrer/)
|
new-contributor
t-algebra
label:t-algebra$ |
90/0 |
Mathlib.lean,Mathlib/Algebra/Ring/Associator.lean |
2 |
6 |
['Paul-Lez', 'github-actions'] |
nobody |
1-58271 1 day ago |
14-71956 14 days ago |
14-71998 14 days |
| 23257 |
eric-wieser author:eric-wieser |
fix(Tactic/Use): do not allow unprotected cdot |
Zulip thread: [#mathlib4 > `use ·` @ 💬](https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/.60use.20.C2.B7.60/near/448279748)
---
[](https://gitpod.io/from-referrer/)
|
large-import
t-meta
|
72/4 |
Mathlib.lean,Mathlib/Tactic.lean,Mathlib/Tactic/CongrM.lean,Mathlib/Tactic/Use.lean,Mathlib/Tactic/WithoutCDot.lean,MathlibTest/Use.lean,scripts/noshake.json |
7 |
1 |
['github-actions'] |
nobody |
1-56206 1 day ago |
1-61457 1 day ago |
1-61503 1 day |
| 23265 |
jcommelin author:jcommelin |
chore(scripts/merge-lean-testing-pr): push to github after successful merge |
---
[](https://gitpod.io/from-referrer/)
|
|
3/1 |
scripts/merge-lean-testing-pr.sh |
1 |
1 |
['github-actions'] |
nobody |
1-53893 1 day ago |
1-53955 1 day ago |
1-53945 1 day |
| 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 |
1-53262 1 day ago |
1-65960 1 day ago |
1-65950 1 day |
| 23268 |
mariainesdff author:mariainesdff |
feat(Analysis/Normed/Unbundled/RingSeminorm): add RingNorm.to_normedRing |
---
[](https://gitpod.io/from-referrer/)
|
t-analysis |
25/0 |
Mathlib/Analysis/Normed/Unbundled/RingSeminorm.lean |
1 |
1 |
['github-actions'] |
nobody |
1-50026 1 day ago |
1-50088 1 day ago |
1-50078 1 day |
| 23261 |
Vierkantor author:Vierkantor |
chore(*): replace `@[simp, nolint simpNF]` with `@[simp high]` for specialized lemmas |
These are specialized lemmas and should therefore apply faster than the more general lemmas introduced later (which need to look for typeclass instances). If we raise their `simp` priority, we can remove the `simpNF` annotation. On the other hand, `simp?` output will look more ugly...
Since `simp` now prefers lemmas declared lower down in the hierarchy, it looks like we can get in a bit of shaking!
From the "specialized high priority simp lemma" library note:
```
It sometimes happens that a `@[simp]` lemma declared early in the library can be proved by `simp`
using later, more general simp lemmas. In that case, the following reasons might be arguments for
the early lemma to be tagged `@[simp high]` (rather than `@[simp, nolint simpNF]` or
un``@[simp]``ed):
1. There is a significant portion of the library which needs the early lemma to be available via
`simp` and which doesn't have access to the more general lemmas.
2. The more general lemmas have more complicated typeclass assumptions, causing rewrites with them
to be slower.
```
---
[](https://gitpod.io/from-referrer/)
|
tech debt |
25/36 |
Mathlib/Algebra/Group/Int/Even.lean,Mathlib/Algebra/Order/Ring/Basic.lean,Mathlib/Data/Int/Init.lean,Mathlib/Data/Multiset/AddSub.lean,Mathlib/Data/Nat/Init.lean,Mathlib/Data/Rat/Defs.lean,Mathlib/Order/Nat.lean,Mathlib/RingTheory/Coprime/Basic.lean |
8 |
4 |
['github-actions', 'leanprover-bot', 'leanprover-community-mathlib4-bot'] |
nobody |
1-46836 1 day ago |
1-46837 1 day ago |
1-49594 1 day |
| 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
new-contributor
|
34/0 |
Mathlib/Data/Int/Order/Lemmas.lean |
1 |
1 |
['github-actions'] |
nobody |
1-43843 1 day ago |
1-43843 1 day ago |
1-43895 1 day |
| 23049 |
YaelDillies author:YaelDillies |
feat: kill copies of a graph |
Show that, for `G` and `H` two graphs, such that `G` appears as a subgraph of `H` `n` times, one can remove at most `n` edges from `H` such that the resulting graph is `G`-free.
From ExtrProbCombi (LeanCamCombi)
---
- [x] depends on: #23091
[](https://gitpod.io/from-referrer/)
|
t-combinatorics |
217/2 |
Mathlib/Combinatorics/SimpleGraph/Copy.lean |
1 |
77 |
['YaelDillies', 'b-mehta', 'github-actions', 'mathlib4-dependent-issues-bot', 'mitchell-horner'] |
nobody |
1-41518 1 day ago |
2-29954 2 days ago |
2-49533 2 days |
| 23238 |
YaelDillies author:YaelDillies |
feat: extended floor and ceil |
My motivation for this is to prove `ENat.toENNReal (⨆ i, f i) = ⨆ i, ENat.toENNReal (f i)` and `ENat.toENNReal (⨅ i, f i) = ⨅ i, ENat.toENNReal (f i)`.
From MiscYD
---
See #15269 for a past attempt.
[](https://gitpod.io/from-referrer/)
|
t-algebra label:t-algebra$ |
269/0 |
Mathlib.lean,Mathlib/Algebra/Order/Floor.lean,Mathlib/Algebra/Order/Floor/Extended.lean |
3 |
3 |
['YaelDillies', 'eric-wieser', 'github-actions'] |
nobody |
1-40729 1 day ago |
1-40729 1 day ago |
1-50565 1 day |
| 22912 |
AntoineChambert-Loir author:AntoineChambert-Loir |
feat(RingTheory/PolynomialLaw/Basic): definition and elementary properties of polynomial laws |
Let `M` and `N` be a modules over a commutative ring `R`.
A polynomial law `f : PolynomialLaw R M N`, with notation `f : M →ₚ[R] N`,
is a “law” that assigns, to every `R`-algebra `S`,
* a map `PolynomialLaw.toFun' f S : S ⊗[R] M → S ⊗[R] N`,
* compatibly with morphisms of `R`-algebras, as expressed by `PolynomialLaw.isCompat' f`
These expressions behave as “polynomials from `M` to `N`“.
This PR is the first of a series that formalizes their properties.
They will be used for the study of the universal divided power algebra.
Coauthored with @mariainesdff
---
[](https://gitpod.io/from-referrer/)
|
large-import
t-algebra
label:t-algebra$ |
285/1 |
Mathlib.lean,Mathlib/Algebra/Algebra/Hom.lean,Mathlib/LinearAlgebra/TensorProduct/Associator.lean,Mathlib/RingTheory/PolynomialLaw/Basic.lean,scripts/noshake.json |
5 |
10 |
['AntoineChambert-Loir', 'github-actions', 'joelriou'] |
nobody |
1-32203 1 day ago |
1-32203 1 day ago |
11-85273 11 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₂`.
---
- [ ] 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 |
1-31047 1 day ago |
9-77019 9 days ago |
9-79473 9 days |
| 23284 |
kbuzzard author:kbuzzard |
feat(Algebra/BigOperators/Finprod): add some API |
Add `finprod_mem_eq_prod'` (and docstrings explaining the prime) and `smul_finsum_mem`.
---
[](https://gitpod.io/from-referrer/)
|
t-algebra label:t-algebra$ |
22/1 |
Mathlib/Algebra/BigOperators/Finprod.lean |
1 |
1 |
['github-actions'] |
nobody |
1-29325 1 day ago |
1-29325 1 day ago |
1-29382 1 day |
| 22911 |
AntoineChambert-Loir author:AntoineChambert-Loir |
feat(RingTheory/Finiteness/Small): smallness properties of modules and algebras |
Basic smallness properties (with respect to universe) for modules and algebras.
---
[](https://gitpod.io/from-referrer/)
|
large-import
t-algebra
label:t-algebra$ |
112/6 |
Mathlib.lean,Mathlib/Data/DFinsupp/Small.lean,Mathlib/RingTheory/Finiteness/Cardinality.lean,Mathlib/RingTheory/Finiteness/Small.lean,Mathlib/RingTheory/Flat/Basic.lean,Mathlib/RingTheory/MvPolynomial/Basic.lean |
6 |
13 |
['ADedecker', 'AntoineChambert-Loir', 'github-actions'] |
nobody |
1-26905 1 day ago |
1-32846 1 day ago |
12-25080 12 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 |
1-22101 1 day ago |
1-22115 1 day ago |
2-43814 2 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 |
1-19031 1 day ago |
2-49549 2 days ago |
2-49539 2 days |
| 23274 |
jcommelin author:jcommelin |
chore(ci): report dependency changes in lake update notifications |
Add Python script to parse lake-manifest.json changes and include the
dependency version changes in the Zulip notifications for lake update
success/failure.
The script detects which packages were updated and shows their old and new
git revisions in a readable format.
---
[](https://gitpod.io/from-referrer/)
|
CI |
161/1 |
.github/workflows/update_dependencies_zulip.yml,scripts/README.md,scripts/parse_lake_manifest_changes.py |
3 |
7 |
['bryangingechen', 'eric-wieser', 'github-actions'] |
bryangingechen assignee:bryangingechen |
1-2947 1 day ago |
1-46307 1 day ago |
1-46356 1 day |
| 23206 |
urkud author:urkud |
feat(EGauge): add `egauge_pi` and `egauge_prod` |
---
- [ ] depends on: #22573
[](https://gitpod.io/from-referrer/)
|
t-analysis |
127/20 |
Mathlib/Analysis/Convex/EGauge.lean |
1 |
14 |
['eric-wieser', 'github-actions', 'mathlib4-dependent-issues-bot', 'urkud'] |
nobody |
1-1412 1 day ago |
3-62206 3 days ago |
3-69392 3 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 |
0-81569 22 hours ago |
0-84438 23 hours ago |
0-84492 23 hours |
| 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/Shapes/Types.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-74555 20 hours ago |
1-30204 1 day ago |
1-30195 1 day |
| 22687 |
RemyDegenne author:RemyDegenne |
feat: the restriction of a closed compact set to a subset of coordinates is closed |
Part of the formalization of Kolmogorov's extension theorem.
Co-authored-by: Peter Pfaffelhuber
---
[](https://gitpod.io/from-referrer/)
|
t-topology |
147/0 |
Mathlib.lean,Mathlib/Topology/IsClosedRestrict.lean |
2 |
7 |
['RemyDegenne', 'github-actions', 'sgouezel'] |
nobody |
0-74418 20 hours ago |
0-74422 20 hours ago |
17-74817 17 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 |
0-73742 20 hours ago |
0-74591 20 hours ago |
0-74581 20 hours |
| 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 |
0-69896 19 hours ago |
0-69896 19 hours ago |
0-69947 19 hours |
| 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 |
0-69710 19 hours ago |
5-37698 5 days ago |
5-37748 5 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 |
0-67977 18 hours ago |
1-50685 1 day ago |
1-50733 1 day |
| 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 |
140/16 |
Mathlib.lean,Mathlib/Analysis/SpecialFunctions/Log/Summable.lean,Mathlib/Topology/UniformSpace/MultipliableTendstoUniformly.lean,Mathlib/Topology/UniformSpace/UniformConvergence.lean |
4 |
28 |
['ADedecker', 'CBirkbeck', 'github-actions', 'j-loreaux', 'loefflerd', 'mathlib4-dependent-issues-bot'] |
nobody |
0-66479 18 hours ago |
7-37571 7 days ago |
26-16557 26 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 |
0-57816 16 hours ago |
5-67402 5 days ago |
6-51866 6 days |
| 23167 |
fbarroero author:fbarroero |
feat(Analysis/SpecialFunctions/Complex/Log): some basic facts about `circleMap` |
We prove some very basic facts about `circleMap`.
---
[](https://gitpod.io/from-referrer/)
|
t-measure-probability
t-analysis
|
59/7 |
Mathlib/Analysis/SpecialFunctions/Complex/Log.lean,Mathlib/Analysis/SpecialFunctions/Exp.lean,Mathlib/MeasureTheory/Integral/CircleIntegral.lean |
3 |
6 |
['EtienneC30', 'fbarroero', 'github-actions', 'mans0954'] |
nobody |
0-57367 15 hours ago |
0-57447 15 hours ago |
2-83735 2 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 |
0-57229 15 hours ago |
0-57232 15 hours ago |
35-83624 35 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 |
0-56983 15 hours ago |
6-2179 6 days ago |
24-72923 24 days |
| 21963 |
fbarroero author:fbarroero |
feat(Algebra/Order/Ring/IsNonarchimedean.lean): Nonarchimedean functions and APIs |
We generalize the definition of nonarchimedean real-valued function to
``` def IsNonarchimedean {α : Type*} [Add α] (f : α → R) : Prop := ∀ a b : α, f (a + b) ≤ f a ⊔ f b```
where `R` is any `LinearOrderedSemiring R` and some related APIs.
---
[](https://gitpod.io/from-referrer/)
|
t-algebra label:t-algebra$ |
188/123 |
Mathlib.lean,Mathlib/Algebra/Order/Ring/Basic.lean,Mathlib/Algebra/Order/Ring/IsNonarchimedean.lean,Mathlib/Analysis/Normed/Group/Ultra.lean,Mathlib/Analysis/Normed/Unbundled/RingSeminorm.lean,Mathlib/Data/Real/Basic.lean,Mathlib/Data/Real/IsNonarchimedean.lean |
7 |
21 |
['Ruben-VandeVelde', 'fbarroero', 'github-actions', 'mariainesdff', 'mistarro', 'riccardobrasca'] |
nobody |
0-56781 15 hours ago |
12-49409 12 days ago |
29-36865 29 days |
| 23088 |
Vierkantor author:Vierkantor |
feat(Tactic/Linter): a linter for directory dependencies |
This is a linter that enforces that modules in certain directories should not import modules in certain others. For example, `Mathlib.Algebra.Notation` can only import `Mathlib.Algebra` files that are also in `Mathlib.Algebra.Notation`. The goal is that this improves modularity and organization in where we put files. At least it should force us to think a bit more about the directory structure of Mathlib.
There are certainly things to improve: the prefix search can probably be optimized using a trie or similar, and the list of directories is autogenerated based on the current state. But it works, so I want to make this PR and at least start the discussion.
---
[](https://gitpod.io/from-referrer/)
|
large-import
t-linter
RFC
|
513/15 |
Mathlib.lean,Mathlib/Init.lean,Mathlib/Tactic.lean,Mathlib/Tactic/Linter/DirectoryDependency.lean,Mathlib/Tactic/Linter/Header.lean,Mathlib/Util/AssertExists.lean,MathlibTest/Header.lean,scripts/lint-style.lean |
8 |
18 |
['Vierkantor', 'github-actions', 'grunweg', 'leanprover-bot'] |
nobody |
0-54842 15 hours ago |
1-51704 1 day ago |
1-62984 1 day |
| 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 |
0-54632 15 hours ago |
0-54649 15 hours ago |
34-39754 34 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 |
0-54128 15 hours ago |
0-54128 15 hours ago |
1-34026 1 day |
| 23305 |
jcommelin author:jcommelin |
chore(Algebra/BigOperators/Finsupp): add Finsupp.sum_apply'' |
Part of an attempt to factor some reusable bits out of
`Mathlib/Topology/Category/Profinite/Nobeling.lean`
This lemma applies in situations where `Finsupp.sum_apply'` does not,
because coercions are getting in the way.
We currently don't have a typeclass to express
"addition on this FunLike is pointwise"
so I have expressed that with explicit arguments.
---
[](https://gitpod.io/from-referrer/)
|
t-algebra label:t-algebra$ |
15/0 |
Mathlib/Algebra/BigOperators/Finsupp/Basic.lean |
1 |
1 |
['github-actions'] |
nobody |
0-54073 15 hours ago |
0-54073 15 hours ago |
0-54182 15 hours |
| 23306 |
jcommelin author:jcommelin |
chore(Data/FunLike): add `dite_apply` and `ite_apply` theorems |
Part of an attempt to factor some reusable bits out of
`Mathlib/Topology/Category/Profinite/Nobeling.lean`
---
[](https://gitpod.io/from-referrer/)
|
t-data |
8/0 |
Mathlib/Data/FunLike/Basic.lean |
1 |
1 |
['github-actions'] |
nobody |
0-53725 14 hours ago |
0-53783 14 hours ago |
0-53832 14 hours |
| 23294 |
Parcly-Taxel author:Parcly-Taxel |
chore: split `Data.WSeq.Basic` |
* `Data.WSeq.Basic` contains basic definitions and lemmas.
* `Data.WSeq.Defs` contains definitions not used anywhere else.
* `Data.WSeq.Productive` contains the `Productive` property and `toSeq`. They too are not used anywhere else.
* `Data.WSeq.Relation` defines relations and equivalence on weak sequences. This file **is** needed by `Data.Seq.Parallel`. |
t-data
tech debt
|
882/825 |
Mathlib.lean,Mathlib/Data/Seq/Parallel.lean,Mathlib/Data/WSeq/Basic.lean,Mathlib/Data/WSeq/Defs.lean,Mathlib/Data/WSeq/Productive.lean,Mathlib/Data/WSeq/Relation.lean |
6 |
4 |
['Parcly-Taxel', 'github-actions', 'grunweg'] |
nobody |
0-53129 14 hours ago |
0-58796 16 hours ago |
0-58786 16 hours |
| 23286 |
kbuzzard author:kbuzzard |
feat(Data/Set/Function): add BijOn API |
This PR adds two results about `BijOn` for the image of a set.
---
[](https://gitpod.io/from-referrer/)
|
t-data |
38/0 |
Mathlib/Data/Set/Function.lean |
1 |
9 |
['eric-wieser', 'github-actions', 'kbuzzard', 'urkud'] |
nobody |
0-52122 14 hours ago |
0-52467 14 hours ago |
0-55088 15 hours |
| 23270 |
Vierkantor author:Vierkantor |
refactor(MeasureTheory): fix `simp` not applying `measurableSet_inf` |
Apparently this theorem is sensitive to the order in which its parameters are given, since it calls typeclass synthesis to find them rather than unification for some reason. In this case, we want `m_1` to be found, so we should order it after `m_2` which has the same type.
---
[](https://gitpod.io/from-referrer/)
|
tech debt
t-measure-probability
|
4/3 |
Mathlib/MeasureTheory/MeasurableSpace/Defs.lean |
1 |
5 |
['Vierkantor', 'github-actions', 'jcommelin'] |
nobody |
0-51747 14 hours ago |
1-48662 1 day ago |
1-48652 1 day |
| 21803 |
erdOne author:erdOne |
feat(Order): `LTSeries` can be extended to `CovBy`-`RelSeries` |
---
[](https://gitpod.io/from-referrer/)
|
large-import
t-order
|
58/0 |
Mathlib/Order/OrderIsoNat.lean,Mathlib/Order/RelSeries.lean |
2 |
5 |
['alreadydone', 'b-mehta', 'erdOne', 'github-actions'] |
nobody |
0-51659 14 hours ago |
41-15424 1 month ago |
41-15476 41 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 |
0-51275 14 hours ago |
0-51275 14 hours ago |
7-44696 7 days |
| 12290 |
yoh-tanimoto author:yoh-tanimoto |
feat(MeasureTheory/Integral): the Riesz-Markov-Kakutani theorem for `Real`-linear functionals |
Prove that `rieszContent` gives a measure `rieszMeasure` such that, under `Λ : C(X, ℝ) →ₗ[ℝ] ℝ) (hΛ : ∀ (f : C(X, ℝ)), 0 ≤ f → 0 ≤ Λ f)`, it holds that `∀ (f : C_c(X, ℝ≥0)), ∫ (x : X), f x ∂ (rieszMeasure Λ hΛ) = Λ f`. The measure is defined through `rieszContent` for `toNNRealLinear`-version of `Λ`. The result is first proved for `Real`-linear `Λ` because in a standard proof one has to prove the inequalities by considering `Λ f` and `Λ (-f)` for all functions `f`, yet on `C_c(X, ℝ≥0)` there is no negation.
---
Motivation : This will be a basis for example, of the spectral decomposition of self-adjoint operators on Hilbert spaces.
The `NNReal`-version is ~300 lines away.
https://github.com/leanprover-community/mathlib4/compare/yoh-tanimoto-linearRMK...yoh-tanimoto-NNRealRMK
- [x] depends on: #12266 for a variation of Urysohn's lemma.
- [x] depends on: #20040 for `rieszContentRegular`
- [x] depends on: #20257 for `toNNRealLinear`
- [x] depends on: #20258 for `MeasureTheory.integral_tsupport`
- [x] depends on: #21572 for renaming |
new-contributor
t-measure-probability
|
493/2 |
Mathlib.lean,Mathlib/MeasureTheory/Integral/RieszMarkovKakutani/Basic.lean,Mathlib/MeasureTheory/Integral/RieszMarkovKakutani/Real.lean |
3 |
139 |
['YaelDillies', 'github-actions', 'j-loreaux', 'kkytola', 'mathlib4-dependent-issues-bot', 'oliver-butterley', 'sgouezel', 'yoh-tanimoto'] |
nobody |
0-50813 14 hours ago |
0-63942 17 hours ago |
3-8889 3 days |
| 23309 |
kkytola author:kkytola |
feat: add order-continuity of adjoints and left-or-right-continuity of order-continuous functions. |
Results about left/right-order-continuous functions:
* left/right adjoints in Galois connections are order-left/right-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 |
121/0 |
Mathlib.lean,Mathlib/Order/GaloisConnection/OrdContinuous.lean |
2 |
2 |
['github-actions', 'kkytola'] |
nobody |
0-49017 13 hours ago |
0-50506 14 hours ago |
0-50496 14 hours |
| 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 |
0-48224 13 hours ago |
0-48226 13 hours ago |
0-50451 14 hours |
| 23100 |
miguelmarco author:miguelmarco |
feat: add rewriting lemmas about naturals |
This PR includes some equalities and equivalences about expressions with natural numbers.
They can be useful as rewriting lemmas to simplify expressions.
[](https://gitpod.io/from-referrer/)
|
new-contributor
t-algebra
label:t-algebra$ |
52/0 |
Mathlib/Data/Nat/Init.lean |
1 |
17 |
['YaelDillies', 'github-actions', 'miguelmarco'] |
nobody |
0-44346 12 hours ago |
0-44365 12 hours ago |
1-29465 1 day |
| 23264 |
bsubercaseaux author:bsubercaseaux |
feat(Combinatorics/SimpleGraph/Diam): add basic (e)diam facts |
Add converses of some `diam` and `ediam` lemmas.
These should improve the experience of working with diam/ediam by providing more direct relations between the terms `G.ediam = \top`, `G.diam = 0`, `G.Preconnected`, etc.
---
[](https://gitpod.io/from-referrer/)
|
new-contributor
t-combinatorics
|
31/0 |
Mathlib/Combinatorics/SimpleGraph/Diam.lean |
1 |
9 |
['Rida-Hamadani', 'bsubercaseaux', 'github-actions'] |
nobody |
0-44232 12 hours ago |
1-55636 1 day ago |
1-55686 1 day |
| 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 |
0-44058 12 hours ago |
2-50430 2 days ago |
8-74211 8 days |
| 23318 |
robin-carlier author:robin-carlier |
chore(CategoryTheory/Functor/ReflectsIso): split `ReflectsIso.lean` |
The file `CategoryTheory.Functor.ReflectsIso` is split in two files:
- `CategoryTheory.Functor.ReflectsIso.Basic`: contains the definition, the fact that whiskeringRight respects Iso, and that fully faithful functors are conservative.
- `CategoryTheory.Functor.ReflectsIso.Balanced`: contains the relation between `ReflectsIsomorphisms` and Epi/Mono and Balanced Categories
---
It’s been a bit of a mess to fix the imports in the various files that were broken by this, so I hope I did not something too radical here...
[](https://gitpod.io/from-referrer/)
|
t-category-theory |
74/35 |
Mathlib.lean,Mathlib/Algebra/Category/Grp/ForgetCorepresentable.lean,Mathlib/Algebra/Category/ModuleCat/Presheaf/Sheafification.lean,Mathlib/Algebra/Category/MonCat/Adjunctions.lean,Mathlib/Algebra/Category/MonCat/Basic.lean,Mathlib/Algebra/Category/MonCat/ForgetCorepresentable.lean,Mathlib/Algebra/Category/Semigrp/Basic.lean,Mathlib/CategoryTheory/Comma/StructuredArrow/Basic.lean,Mathlib/CategoryTheory/ConcreteCategory/ReflectsIso.lean,Mathlib/CategoryTheory/Endofunctor/Algebra.lean,Mathlib/CategoryTheory/FiberedCategory/BasedCategory.lean,Mathlib/CategoryTheory/Functor/ReflectsIso/Balanced.lean,Mathlib/CategoryTheory/Functor/ReflectsIso/Basic.lean,Mathlib/CategoryTheory/Limits/Cones.lean,Mathlib/CategoryTheory/Limits/Creates.lean,Mathlib/CategoryTheory/Limits/HasLimits.lean,Mathlib/CategoryTheory/Localization/Composition.lean,Mathlib/CategoryTheory/Monad/Basic.lean,Mathlib/CategoryTheory/Monoidal/Center.lean,Mathlib/CategoryTheory/MorphismProperty/IsInvertedBy.lean,Mathlib/CategoryTheory/Sites/Subsheaf.lean,Mathlib/CategoryTheory/Subobject/MonoOver.lean,Mathlib/CategoryTheory/Topos/Classifier.lean,Mathlib/RepresentationTheory/GroupCohomology/Resolution.lean,Mathlib/Topology/Category/CompHausLike/Basic.lean,Mathlib/Topology/Sheaves/MayerVietoris.lean |
26 |
2 |
['github-actions', 'robin-carlier'] |
nobody |
0-31969 8 hours ago |
0-31969 8 hours ago |
0-31986 8 hours |
| 23295 |
loefflerd author:loefflerd |
feat(Analysis/Normed/Ring): generalise some `NormMulClass` results to seminorms |
---
- [ ] depends on: #22842
[](https://gitpod.io/from-referrer/)
|
t-analysis |
33/12 |
Mathlib/Analysis/Normed/Ring/Basic.lean |
1 |
19 |
['eric-wieser', 'github-actions', 'leanprover-bot', 'loefflerd', 'mathlib4-dependent-issues-bot'] |
nobody |
0-31786 8 hours ago |
0-71875 19 hours ago |
0-73153 20 hours |
| 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 |
11 |
['eric-wieser', 'github-actions', 'mathlib4-dependent-issues-bot', 'xroblot'] |
nobody |
0-30732 8 hours ago |
0-32222 8 hours ago |
3-33883 3 days |
| 23288 |
eric-wieser author:eric-wieser |
chore: use `dist_eq_norm_sub` not `dist_eq` |
This is extracted from #9642
---
[](https://gitpod.io/from-referrer/)
|
t-topology
easy
|
2/2 |
Mathlib/Topology/ContinuousMap/Bounded/Basic.lean |
1 |
1 |
['github-actions'] |
nobody |
0-26965 7 hours ago |
1-17564 1 day ago |
1-17613 1 day |
| 23076 |
miguelmarco author:miguelmarco |
feat: add rewriting lemmas for euclidean domains |
This PR includes some equalities and equivalences about expressions in euclidean domains.
They can be useful as rewriting lemmas to simplify expressions.
---
[](https://gitpod.io/from-referrer/)
|
new-contributor
t-algebra
enhancement
label:t-algebra$ |
60/0 |
Mathlib/Algebra/EuclideanDomain/Basic.lean |
1 |
21 |
['eric-wieser', 'github-actions', 'miguelmarco', 'tb65536'] |
nobody |
0-26581 7 hours ago |
7-29742 7 days ago |
7-29744 7 days |
| 23251 |
mariainesdff author:mariainesdff |
feat(FieldTheory/IntermediateField/Adjoin): add lemmas |
---
[](https://gitpod.io/from-referrer/)
|
t-algebra label:t-algebra$ |
67/0 |
Mathlib/FieldTheory/IntermediateField/Adjoin/Basic.lean,Mathlib/FieldTheory/IsAlgClosed/AlgebraicClosure.lean |
2 |
5 |
['github-actions', 'tb65536'] |
nobody |
0-26341 7 hours ago |
1-72237 1 day ago |
1-72227 1 day |
| 22703 |
D-Thomine author:D-Thomine |
feat(Analysis/Asymptotics/ExpGrowth): Exponential growth and composition |
This PR adds lemmas about the exponential growth of a composition `u ∘ v` depending on the exponential growth of `u` and the linear growth of `v`.
Most new stuff is in `Analysis.Asymptotics.ExpGrowth` (mostly sections _Composition_ and _Monotone sequences_). I also slightly modified the four lemmas `expGrowthInf_le_iff`, `le_expGrowthInf_iff`, etc. to use large inequalities instead of strict inequalities (it's more comfortable for me).
In `Data.Real.EReal`: A new lemma (the inversion is antitone on the positives), and a small tweak to three lemmas (`exists_lt_mul_left_of_nonneg`...), making them slightly stronger; their old use is not impacted, and the improvement makes some new proofs slightly nicer.
In `Order.LiminfLimsup`: A few new lemmas about: liminf and limsup of compositions, versions with large inequalities of `limsup_le_iff` and friends, and a way to compare liminf & limsup of two functions. I've also squeezed some life out of `isBoundedUnder_le_mul_of_nonneg` by replacing an eventual condition with a frequent condition; the new version is not _strictly_ more general, but the cases which are not covered anymore don't seem really interesting (empty filter or weird structures), so the trade-off feels favorable.
In `Topology.Algebra.Order.LiminfLimsup`: Again, some eventual conditions are replaced by frequent conditions (about the limsup of a product on the reals).
In `Topology.Instances.EReal.Lemmas`: Again, some eventual conditions are replaced by frequent conditions (about the limsup of a product on the extended reals).
---
[](https://gitpod.io/from-referrer/)
|
t-analysis |
578/178 |
Mathlib/Analysis/Asymptotics/ExpGrowth.lean,Mathlib/Analysis/Normed/Unbundled/SmoothingSeminorm.lean,Mathlib/Data/Real/EReal.lean,Mathlib/Order/Filter/IsBounded.lean,Mathlib/Order/LiminfLimsup.lean,Mathlib/Topology/Algebra/Order/LiminfLimsup.lean,Mathlib/Topology/Instances/EReal/Lemmas.lean |
7 |
9 |
['D-Thomine', 'github-actions', 'sgouezel'] |
nobody |
0-22741 6 hours ago |
0-22741 6 hours ago |
16-34840 16 days |
| 23320 |
Whysoserioushah author:Whysoserioushah |
feat(Mathlib/RingTheory/TwoSidedIdeal/SpanAsSum): span of set as finsum |
co-authored by: @jjaassoonn
splited from [#23216](https://github.com/leanprover-community/mathlib4/pull/23216) following @eric-wieser advice
---
[](https://gitpod.io/from-referrer/)
|
t-algebra label:t-algebra$ |
91/0 |
Mathlib.lean,Mathlib/RingTheory/TwoSidedIdeal/SpanAsSum.lean |
2 |
10 |
['Whysoserioushah', 'eric-wieser', 'github-actions'] |
nobody |
0-17079 4 hours ago |
0-23846 6 hours ago |
0-23898 6 hours |
| 16596 |
urkud author:urkud |
feat: orbits of an irrational rotation are dense |
---
This PR makes `Topology.Algebra.Order.Archimedean` import `Topology.Algebra.Order.Group` which makes sense IMO.
See also #23321
[](https://gitpod.io/from-referrer/)
|
large-import
t-dynamics
t-topology
|
172/28 |
Mathlib.lean,Mathlib/Topology/Algebra/Order/Archimedean.lean,Mathlib/Topology/Instances/AddCircle/DenseSubgroup.lean |
3 |
n/a |
['github-actions', 'pechersky', 'urkud', 'vihdzp'] |
nobody |
0-16897 4 hours ago |
unknown |
unknown |
| 22944 |
j-loreaux author:j-loreaux |
refactor: merge API for `ENNReal.HolderConjugate` and `{E}{NN}Real.IsConjExponent` |
This PR adds `{NN}Real.HolderTriple` and refactors `{NN}Real.IsConjExponent` to be defined in term of those, while renaming the latter to `{NN}Real.HolderConjugate` to match the existing `ENNReal.HolderConjugate` (we also deprecate `ENNReal.IsConjExponent` to `ENNReal.HolderConjugate` because these are duplicates).
In a future PR, we will merge the contents of `Data.ENNReal.Holder` and this file. For now, we import the former into the latter.
---
[](https://gitpod.io/from-referrer/)
|
t-analysis |
639/261 |
Mathlib/Analysis/FunctionalSpaces/SobolevInequality.lean,Mathlib/Analysis/InnerProductSpace/l2Space.lean,Mathlib/Analysis/MeanInequalities.lean,Mathlib/Analysis/Normed/Lp/lpSpace.lean,Mathlib/Analysis/SpecialFunctions/Gamma/BohrMollerup.lean,Mathlib/Data/ENNReal/Holder.lean,Mathlib/Data/Real/ConjExponents.lean,Mathlib/MeasureTheory/Integral/Bochner.lean,Mathlib/MeasureTheory/Integral/MeanInequalities.lean,Mathlib/NumberTheory/Rayleigh.lean |
10 |
6 |
['Parcly-Taxel', 'RemyDegenne', 'github-actions', 'j-loreaux', 'leanprover-bot'] |
nobody |
0-16035 4 hours ago |
10-55128 10 days ago |
10-55118 10 days |
| 23325 |
yuma-mizuno author:yuma-mizuno |
chore(RingTheory/LocalRing/Module) remove unused `letI` hypothesis |
---
[](https://gitpod.io/from-referrer/)
|
t-algebra label:t-algebra$ |
0/2 |
Mathlib/RingTheory/LocalRing/Module.lean |
1 |
1 |
['github-actions'] |
nobody |
0-11860 3 hours ago |
0-11919 3 hours ago |
0-11909 3 hours |
| 23327 |
kim-em author:kim-em |
chore: an erw in CategoryTheory |
|
t-category-theory |
1/3 |
Mathlib/CategoryTheory/Limits/Opposites.lean |
1 |
2 |
['github-actions', 'kim-em'] |
nobody |
0-3762 1 hour ago |
0-3762 1 hour ago |
0-3813 1 hour |