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 |
| 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 |
59-41951 2 months ago |
59-41964 2 months ago |
59-43760 59 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 |
51-79533 1 month ago |
52-14402 1 month ago |
52-14454 52 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 |
45-83379 1 month ago |
46-9170 1 month ago |
46-9156 46 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 |
45-3613 1 month ago |
45-9080 1 month ago |
45-9066 45 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 |
43-55350 1 month ago |
53-57072 1 month ago |
53-57055 53 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 |
40-78717 1 month ago |
41-65686 1 month ago |
72-27937 72 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 |
40-58397 1 month ago |
40-58397 1 month ago |
40-74643 40 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 |
40-52478 1 month ago |
49-78031 1 month ago |
49-78016 49 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 |
39-84146 1 month ago |
44-7045 1 month ago |
44-7097 44 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 |
39-10250 1 month ago |
73-12711 2 months ago |
81-80418 81 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 |
37-16330 1 month ago |
37-16347 1 month ago |
45-56263 45 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 |
37-7477 1 month ago |
37-7498 1 month ago |
40-3183 40 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 |
34-86244 1 month ago |
35-12488 1 month ago |
35-12534 35 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 |
34-79779 1 month ago |
55-36163 1 month ago |
55-36158 55 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 |
34-46547 1 month ago |
34-46547 1 month ago |
34-76157 34 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 |
33-8725 1 month ago |
36-55387 1 month ago |
38-79194 38 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 |
32-79684 1 month ago |
34-48421 1 month ago |
39-48961 39 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 |
32-68240 1 month ago |
32-69062 1 month ago |
32-69238 32 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 |
32-17835 1 month ago |
32-17850 1 month ago |
39-51289 39 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 |
32-1170 1 month ago |
45-71974 1 month ago |
45-71967 45 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 |
31-82915 1 month ago |
31-82915 1 month ago |
31-82969 31 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 |
31-15378 1 month ago |
31-15378 1 month ago |
34-55880 34 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 |
30-70059 30 days ago |
31-84938 1 month ago |
33-10334 33 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 |
30-29926 30 days ago |
31-10042 1 month ago |
31-11941 31 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 |
28-85509 28 days ago |
29-271 29 days ago |
30-39222 30 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 |
28-2078 28 days ago |
28-5696 28 days ago |
28-5746 28 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 |
27-81447 27 days ago |
27-84992 27 days ago |
27-85038 27 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 |
27-43673 27 days ago |
27-60166 27 days ago |
27-60216 27 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 |
27-40468 27 days ago |
46-49262 1 month ago |
47-78035 47 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 |
26-63761 26 days ago |
26-63778 26 days ago |
74-83471 74 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 |
26-62337 26 days ago |
26-62352 26 days ago |
57-19781 57 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 |
24-82003 24 days ago |
30-5189 30 days ago |
30-76049 30 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 |
24-81416 24 days ago |
24-81419 24 days ago |
60-21410 60 days |
| 22069 |
Raph-DG author:Raph-DG |
feat(LinearMap): Added lemmas relating kernels of linear maps to Submodule.map |
Added the lemma ne_map_or_ne_kernel_inter_of_lt stating that if A < B as submodules, then for any linear map f, `ker f ⊓ A ≠ ker f ⊓ B ∨ Submodule.map f A ≠ Submodule.map f B`. We also prove the corollaries ker_inter_mono_of_map_eq and map_mono_of_ker_inter_eq.
Co-authored-by: Raphael Douglas Giles (raphaeldouglasgiles@gmail.com)
---
[](https://gitpod.io/from-referrer/)
|
new-contributor
t-algebra
label:t-algebra$ |
28/0 |
Mathlib/LinearAlgebra/Span/Basic.lean |
1 |
14 |
['Paul-Lez', 'Raph-DG', 'github-actions', 'j-loreaux'] |
nobody |
24-78819 24 days ago |
24-78836 24 days ago |
58-63937 58 days |
| 23205 |
xroblot author:xroblot |
feat(QuotientGroup): surjectivity and kernel of `QuotientGroup.map` |
Prove formulas for the kernel of `QuotientGroup.lift` and `QuotientGroup.map` and that these maps are surjective if the corresponding functions are surjective.
---
- [x] depends on: #23269
[](https://gitpod.io/from-referrer/)
|
t-algebra label:t-algebra$ |
26/0 |
Mathlib/GroupTheory/QuotientGroup/Defs.lean |
1 |
12 |
['eric-wieser', 'github-actions', 'mathlib4-dependent-issues-bot', 'xroblot'] |
nobody |
24-18776 24 days ago |
24-56409 24 days ago |
27-58066 27 days |
| 22488 |
smmercuri author:smmercuri |
fix: lower priority for `UniformSpace.Completion.instSMul` |
Following the introduction of the `WithVal` type synonym in #22055 the following instance takes a long time to synthesise in FLT, and times out in the default heartbeats
```lean
import Mathlib
namespace IsDedekindDomain.HeightOneSpectrum
variable (A K : Type*) [CommRing A] [Field K] [Algebra A K] [IsFractionRing A K]
[IsDedekindDomain A] (v : HeightOneSpectrum A)
#synth SMul (v.adicCompletionIntegers K) (v.adicCompletion K)
```
The issue is that `UniformSpace.Completion.instSMul (v.adicCompletionIntegers K) (v.adicCompletion K)` now fires during the start of instance search (because we now have `UniformSpace (WithVal (v.valuation K))` whereas previously this would be `UniformSpace K`, which was not automatic), and this takes a long time to fail (leading to ~1400 entries in the trace). The first few lines of the new trace is
```lean
[Meta.synthInstance] [5.512418] ✅️ SMul (↥(adicCompletionIntegers K v)) (adicCompletion K v) ▼
[] [0.000118] new goal SMul (↥(adicCompletionIntegers K v)) (adicCompletion K v) ▶
[] [0.000537] ✅️ apply UniformSpace.Completion.instSMul to SMul (↥(adicCompletionIntegers K v)) (adicCompletion K v) ▶
[] [0.004411] ✅️ apply @WithVal.instSMul to SMul (↥(adicCompletionIntegers K v)) (WithVal (valuation K v)) ▶
[] [0.000765] ❌️ apply @GradedMonoid.GradeZero.smul to SMul (↥(adicCompletionIntegers K v)) K ▶
[] [0.000378] ✅️ apply @Algebra.toSMul to SMul (↥(adicCompletionIntegers K v)) K ▶
...
[] 1339 more entries... ▶
```
Lowering the priority of `UniformSpace.Completion.instSMul` fixes this particular issue, leading to a trace that matches that seen prior to the introduction of `WithVal`:
```lean
[Meta.synthInstance] [0.016405] ✅️ SMul (↥(adicCompletionIntegers K v)) (adicCompletion K v) ▼
[] [0.000119] new goal SMul (↥(adicCompletionIntegers K v)) (adicCompletion K v) ▶
[] [0.000491] ❌️ apply @GradedMonoid.GradeZero.smul to SMul (↥(adicCompletionIntegers K v)) (adicCompletion K v) ▶
[] [0.000403] ✅️ apply @Algebra.toSMul to SMul (↥(adicCompletionIntegers K v)) (adicCompletion K v) ▶
[] [0.000134] ❌️ apply inst✝⁴ to Algebra (↥(adicCompletionIntegers K v)) (adicCompletion K v) ▶
[] [0.000093] ❌️ apply inst✝⁵ to Algebra (↥(adicCompletionIntegers K v)) (adicCompletion K v) ▶
[] [0.000077] ❌️ apply inst✝⁷ to Algebra (↥(adicCompletionIntegers K v)) (adicCompletion K v) ▶
[] [0.000082] ❌️ apply inst✝⁹ to Algebra (↥(adicCompletionIntegers K v)) (adicCompletion K v) ▶
[] [0.000075] ❌️ apply inst✝¹² to Algebra (↥(adicCompletionIntegers K v)) (adicCompletion K v) ▶
[] [0.000220] ❌️ apply Algebra.id to Algebra (↥(adicCompletionIntegers K v)) (adicCompletion K v) ▶
[] [0.001015] ✅️ apply @ValuationSubring.instAlgebraSubtypeMem to Algebra (↥(adicCompletionIntegers K v))
(adicCompletion K v) ▶
[resume] [0.000038] propagating Algebra (↥(adicCompletionIntegers K v))
(adicCompletion K
v) to subgoal Algebra (↥(adicCompletionIntegers K v))
(adicCompletion K v) of SMul (↥(adicCompletionIntegers K v)) (adicCompletion K v) ▶
[check] [0.013358] ✅️ Algebra.toSMul
[] result Algebra.toSMul
```
---
[](https://gitpod.io/from-referrer/)
|
FLT
t-topology
|
1/1 |
Mathlib/Topology/Algebra/UniformMulAction.lean |
1 |
7 |
['github-actions', 'leanprover-bot', 'smmercuri', 'urkud'] |
nobody |
23-62192 23 days ago |
47-14772 1 month ago |
47-14816 47 days |
| 22884 |
tannerduve author:tannerduve |
feat(Computability/TuringDegrees): define oracle computability and Turing degrees |
### Description
Define a model of **oracle computability**, introducing Turing reducibility (`≤ᵀ`), Turing equivalence (`≡ᵀ`), and Turing degrees as the quotient under Turing equivalence.
- `RecursiveIn O f`: A function `f` is recursive in a set of oracles `O` if it can be computed using `O` via basic operations (zero, successor, pairing, composition, primitive recursion, and μ-recursion).
- `TuringReducible`: The relation that `f` is recursive in `{g}`, i.e., `f ≤ᵀ g`.
- `TuringEquivalent`: A relation defining Turing equivalence between partial functions.
- `TuringDegree`: The set of equivalence classes under `TuringEquivalent`, forming a **partially ordered structure**.
Additionally:
- Prove that `TuringReducible` is a **preorder** (reflexive, transitive).
- Show that `TuringEquivalent` is an **equivalence relation**.
- Establish that **partial recursive functions** correspond to functions recursive in the empty oracle set.
This formalization follows classical recursion theory (Odifreddi, Soare) and extends previous work by Carneiro.
### Breaking Changes
None.
### Dependencies
None. |
t-computability
new-contributor
|
221/0 |
Mathlib.lean,Mathlib/Computability/TuringDegrees.lean |
2 |
8 |
['github-actions', 'tannerduve', 'tristan-f-r'] |
nobody |
23-52962 23 days ago |
37-69444 1 month ago |
37-69491 37 days |
| 23336 |
kim-em author:kim-em |
chore: `erw` in `Topology/Order/` |
|
t-topology |
6/7 |
Mathlib/Topology/Order/LawsonTopology.lean,Mathlib/Topology/Order/LowerUpperTopology.lean,Mathlib/Topology/Order/ScottTopology.lean,Mathlib/Topology/Order/UpperLowerSetTopology.lean |
4 |
4 |
['github-actions', 'kim-em', 'urkud'] |
nobody |
23-50011 23 days ago |
24-2763 24 days ago |
24-2811 24 days |
| 22655 |
YaelDillies author:YaelDillies |
refactor: make use of `FunLike` for `Submonoid.LocalizationMap` |
From Toric
---
[](https://gitpod.io/from-referrer/)
|
toric
t-algebra
label:t-algebra$ |
156/140 |
Mathlib/GroupTheory/MonoidLocalization/Away.lean,Mathlib/GroupTheory/MonoidLocalization/Basic.lean,Mathlib/GroupTheory/MonoidLocalization/MonoidWithZero.lean,Mathlib/RingTheory/Localization/Defs.lean |
4 |
1 |
['github-actions'] |
nobody |
23-10433 23 days ago |
23-10447 23 days ago |
40-36607 40 days |
| 23367 |
b-reinke author:b-reinke |
feat(GroupTheory/FreeGroup/Reduce): add lemmas for toWord and reduce |
Upstreamed from the [EquationalTheories](https://github.com/teorth/equational_theories) project.
This PR adds some simple helper lemmas for the interaction of `toWord` and `reduce` and basic list / group operations.
The RHS of the lemmas often contains more appearances of `reduce`, so they are not marked as `simp` lemmas.
---
[](https://gitpod.io/from-referrer/)
|
t-geometric-group-theory
t-algebra
label:t-algebra$ |
24/0 |
Mathlib/GroupTheory/FreeGroup/Reduce.lean |
1 |
1 |
['github-actions'] |
nobody |
23-372 23 days ago |
23-372 23 days ago |
23-9051 23 days |
| 23368 |
b-reinke author:b-reinke |
feat(GroupTheory/FreeGroup/ReducedWords): add theory of reduced words |
Upstreamed from the [EquationalTheories](https://github.com/teorth/equational_theories) project.
This PR adds the file `GroupTheory/FreeGroup/ReducedWords.lean`, where the predicate of reduced words is defined. It is shown that `reduce` and `toWord` produce reduced words.
This is done in preparation for the theory of cyclically reduced words.
---
[](https://gitpod.io/from-referrer/)
|
t-geometric-group-theory
t-algebra
label:t-algebra$ |
124/0 |
Mathlib.lean,Mathlib/GroupTheory/FreeGroup/ReducedWords.lean |
2 |
1 |
['github-actions'] |
nobody |
23-352 23 days ago |
23-352 23 days ago |
23-8186 23 days |
| 23197 |
robin-carlier author:robin-carlier |
feat(CategoryTheory/Equivalences): category structure on equivalences |
We put a category structure on `(C ≌ D)`. The morphisms are simply natural transformations between the underlying functor. We also provide various API for this structure.
---
While this PR contains functoriality of the operation that maps an equivalence to its underlying functor, functoriality of inverses will be in a different PR and recorded in a different file : I feel the most natural way to do this is to bring in the results from `Adjunction.Mates`, but this imports quite a lot of stuff.
[](https://gitpod.io/from-referrer/)
|
t-category-theory |
69/0 |
Mathlib/CategoryTheory/Equivalence.lean |
1 |
7 |
['github-actions', 'joelriou', 'robin-carlier'] |
nobody |
22-67375 22 days ago |
22-67375 22 days ago |
28-45578 28 days |
| 22870 |
kebekus author:kebekus |
feat: behavior of MeromorphicAt.order under powers and inverses |
Establish the behavior of `MeromorphicAt.order` under standard operations, including powers and inverses. The results are completely analogous to the existing theorems for `AnalyticAt.order`.
This material is used in [Project VD](https://github.com/kebekus/ProjectVD), which aims to formalize Value Distribution Theory for meromorphic functions on the complex plane.
---
[](https://gitpod.io/from-referrer/)
|
t-analysis |
26/12 |
Mathlib/Analysis/Meromorphic/Order.lean,Mathlib/Order/WithBot.lean |
2 |
1 |
['github-actions'] |
nobody |
22-64917 22 days ago |
22-64932 22 days ago |
37-31877 37 days |
| 22050 |
IvanRenison author:IvanRenison |
feat(Combinatorics/SimpleGraph): Add `SimpleGraph.Preconnected.support_eq_univ` |
Co-authored-by: Kyle Miller kmill31415@gmail.com
---
Suggested in [zulip](https://leanprover.zulipchat.com/#narrow/channel/252551-graph-theory/topic/Way.20ConnectedComponent.20definition.20uses.20Quot.3F)
[](https://gitpod.io/from-referrer/)
|
t-combinatorics |
44/0 |
Mathlib/Combinatorics/SimpleGraph/Path.lean |
1 |
4 |
['b-mehta', 'github-actions', 'urkud'] |
b-mehta assignee:b-mehta |
20-80613 20 days ago |
20-80626 20 days ago |
52-13636 52 days |
| 23309 |
kkytola author:kkytola |
feat: left/right order-continuous functions are left/right topology-continuous |
Order left/right-continuous functions on (densely ordered) conditionally complete linear orders are topologically left/right-continuous.
Co-authored-by: Yaël Dillies
---
[](https://gitpod.io/from-referrer/)
|
t-order |
27/3 |
Mathlib/Topology/Order/Basic.lean |
1 |
3 |
['YaelDillies', 'github-actions', 'kkytola'] |
nobody |
20-80112 20 days ago |
24-74693 24 days ago |
24-74679 24 days |
| 23334 |
Ruben-VandeVelde author:Ruben-VandeVelde |
feat: add lemmas about Field.toEuclideanDomain |
The behaviour of mod and gcd in a field are somewhat unexpected. I think that adding simp lemmas to reduce them to more well-understood notions will be helpful for people who accidentally end up using them, even if the right-hand side is not necessarily "simp"ler on first sight.
---
[](https://gitpod.io/from-referrer/)
|
t-algebra label:t-algebra$ |
21/2 |
Mathlib/Algebra/EuclideanDomain/Field.lean |
1 |
6 |
['Ruben-VandeVelde', 'acmepjz', 'github-actions'] |
nobody |
20-59166 20 days ago |
24-10562 24 days ago |
24-10618 24 days |
| 23446 |
acmepjz author:acmepjz |
feat(Algebra/Exact): add `Function.Exact.[iff_]rangeFactorization` etc |
Two maps `f : M → N` and `g : N → P` are exact if and only if the induced maps `Set.range f → N → Set.range g` are exact. Same for `AddMonoidHom` and `LinearMap`.
---
[](https://gitpod.io/from-referrer/)
Discussion: [#Is there code for X? > Function.Exact.rangeFactorization](https://leanprover.zulipchat.com/#narrow/channel/217875-Is-there-code-for-X.3F/topic/Function.2EExact.2ErangeFactorization) |
t-algebra label:t-algebra$ |
41/2 |
Mathlib/Algebra/Exact.lean |
1 |
1 |
['github-actions'] |
nobody |
20-22019 20 days ago |
20-22019 20 days ago |
20-22005 20 days |
| 23461 |
xroblot author:xroblot |
feat(GroupTheory/Cyclic): formula for the card & index of kernel & range of powMonoidHom on a cyclic group |
We prove formula for the cardinal and index of the kernel and range of `powMonoidHom : x ↦ x ^ d` on a finite cyclic group.
---
[](https://gitpod.io/from-referrer/)
|
t-algebra label:t-algebra$ |
48/0 |
Mathlib/GroupTheory/Index.lean,Mathlib/GroupTheory/SpecificGroups/Cyclic.lean |
2 |
1 |
['github-actions'] |
nobody |
19-61390 19 days ago |
19-61540 19 days ago |
19-61586 19 days |
| 21283 |
erdOne author:erdOne |
feat: topology on Hom(R, S) in `CommRingCat` |
Co-authored-by: Christian Merten
---
[](https://gitpod.io/from-referrer/)
|
t-algebra
t-topology
label:t-algebra$ |
227/0 |
Mathlib.lean,Mathlib/Algebra/Category/Ring/Constructions.lean,Mathlib/Algebra/Category/Ring/Topology.lean,Mathlib/Topology/Constructions.lean,Mathlib/Topology/Homeomorph/Lemmas.lean,scripts/noshake.json |
6 |
5 |
['dagurtomas', 'erdOne', 'github-actions'] |
nobody |
19-59401 19 days ago |
19-59401 19 days ago |
58-15054 58 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 |
19-15659 19 days ago |
25-74872 25 days ago |
25-74916 25 days |
| 23498 |
Ruben-VandeVelde author:Ruben-VandeVelde |
chore(Topology.MetricSpace.Lipschitz): stop depending on Topology.Algebra |
Noticed while playing with the new `directoryDependency` linter. Not sure if these could be proved without assuming the continuity of real multiplication.
Copyright from https://github.com/leanprover-community/mathlib3/pull/1921 and https://github.com/leanprover-community/mathlib4/pull/11840.
---
[](https://gitpod.io/from-referrer/)
|
|
60/34 |
Mathlib.lean,Mathlib/Analysis/Normed/Group/AddTorsor.lean,Mathlib/Analysis/NormedSpace/Multilinear/Basic.lean,Mathlib/Analysis/SpecialFunctions/Exp.lean,Mathlib/Topology/Algebra/MetricSpace/Lipschitz.lean,Mathlib/Topology/MetricSpace/Algebra.lean,Mathlib/Topology/MetricSpace/IsometricSMul.lean,Mathlib/Topology/MetricSpace/Lipschitz.lean,Mathlib/Topology/MetricSpace/PiNat.lean |
9 |
1 |
['github-actions'] |
nobody |
19-450 19 days ago |
19-510 19 days ago |
19-496 19 days |
| 23425 |
vasnesterov author:vasnesterov |
feat(Algebra/BigOperators): simprocify `prod_univ_one/two/three/...` |
Add a simproc `prod_univ_many` that rewrites `∏ (i : Fin n), f i` as `f 0 * f 1 * ... * f (n - 1)`, generalizing `prod_univ_one`, `prod_univ_two`, ..., `prod_univ_eight`.
---
It seems impossible to use to_additive here to avoid reimplementing the same simproc for additive goals. Just wanted to hear your ideas, before doing it.
- [x] depends on: #23427
[](https://gitpod.io/from-referrer/)
|
t-meta |
51/0 |
Mathlib/Data/Fin/Tuple/Reflection.lean |
1 |
9 |
['eric-wieser', 'github-actions', 'mathlib4-dependent-issues-bot', 'vasnesterov'] |
nobody |
18-79830 18 days ago |
19-33602 19 days ago |
19-82474 19 days |
| 23502 |
Timeroot author:Timeroot |
feat(ModelTheory/Semantics): BoundedFormula.realize_foldr_imp |
Two lemmas for `realize`ing a `BoundedFormula`.
---
Pulled out from #19695.
[](https://gitpod.io/from-referrer/)
|
t-logic |
20/0 |
Mathlib/ModelTheory/Semantics.lean,Mathlib/ModelTheory/Syntax.lean |
2 |
1 |
['github-actions'] |
nobody |
18-76643 18 days ago |
18-77543 18 days ago |
18-77598 18 days |
| 23470 |
erdOne author:erdOne |
feat(AlgebraicGeometry): section of a k-scheme is a closed immersion |
Co-authored-by: Christian Merten
---
[](https://gitpod.io/from-referrer/)
|
t-algebraic-geometry |
89/3 |
Mathlib/AlgebraicGeometry/Limits.lean,Mathlib/AlgebraicGeometry/Morphisms/ClosedImmersion.lean,Mathlib/AlgebraicGeometry/OpenImmersion.lean,Mathlib/AlgebraicGeometry/PullbackCarrier.lean,Mathlib/AlgebraicGeometry/Pullbacks.lean,Mathlib/AlgebraicGeometry/Scheme.lean |
6 |
7 |
['chrisflav', 'github-actions'] |
nobody |
18-65282 18 days ago |
19-36292 19 days ago |
19-36322 19 days |
| 21909 |
erdOne author:erdOne |
feat(RingTheory/Invariants): Generalize to profinite groups |
---
[](https://gitpod.io/from-referrer/)
|
t-algebra label:t-algebra$ |
350/5 |
Mathlib.lean,Mathlib/Algebra/Algebra/Subalgebra/Operations.lean,Mathlib/NumberTheory/RamificationInertia/Galois.lean,Mathlib/RingTheory/Frobenius.lean,Mathlib/RingTheory/Invariant/Basic.lean,Mathlib/RingTheory/Invariant/Profinite.lean |
6 |
2 |
['TwoFX', 'github-actions'] |
nobody |
18-51783 18 days ago |
18-51783 18 days ago |
22-39962 22 days |
| 22265 |
Timeroot author:Timeroot |
feat(Geometry/Euclidean/Angle/Unoriented): triangle inequality |
filled in a `proof_wanted`
---
[](https://gitpod.io/from-referrer/)
|
t-euclidean-geometry |
78/12 |
Mathlib.lean,Mathlib/Geometry/Euclidean/Angle/Unoriented/Affine.lean,Mathlib/Geometry/Euclidean/Angle/Unoriented/Basic.lean,Mathlib/Geometry/Euclidean/Angle/Unoriented/TriangleInequality.lean,Mathlib/LinearAlgebra/Matrix/PosDef.lean |
5 |
7 |
['Timeroot', 'github-actions', 'jsm28', 'urkud'] |
nobody |
18-35282 18 days ago |
18-72196 18 days ago |
38-75977 38 days |
| 23527 |
erdOne author:erdOne |
feat(Topology): subspace of quotient topology is quotient of subspace topology |
---
[](https://gitpod.io/from-referrer/)
|
t-topology |
69/0 |
Mathlib/Topology/Maps/OpenQuotient.lean |
1 |
1 |
['github-actions'] |
nobody |
18-16192 18 days ago |
18-16281 18 days ago |
18-16267 18 days |
| 23528 |
Ruben-VandeVelde author:Ruben-VandeVelde |
feat: add isOpen_setOf_affineIndependent |
From sphere-eversion.
---
[](https://gitpod.io/from-referrer/)
|
t-analysis |
15/0 |
Mathlib/Analysis/Normed/Module/FiniteDimension.lean |
1 |
1 |
['github-actions'] |
nobody |
18-13876 18 days ago |
18-13876 18 days ago |
18-13923 18 days |
| 22635 |
Kiolt author:Kiolt |
feat: submonoid of pairs with quotient in a submonoid |
This submonoid is part of the definition of toric ideals.
From Toric
---
[](https://gitpod.io/from-referrer/)
|
toric
new-contributor
t-algebra
label:t-algebra$ |
36/0 |
Mathlib.lean,Mathlib/GroupTheory/MonoidLocalization/DivPairs.lean |
2 |
10 |
['Paul-Lez', 'YaelDillies', 'erdOne', 'github-actions'] |
nobody |
18-11500 18 days ago |
18-11553 18 days ago |
43-84886 43 days |
| 22151 |
alreadydone author:alreadydone |
feat(RingTheory): a semiprimary ring is Noetherian/Artinian iff its Jacobson radical is fg |
A key fact used is `Module.FG.smul`: if `I` is a two-sided ideal of `R` that is f.g. as a left ideal and `N` is a f.g. `R`-module, then `I • M` is also a f.g. `R`-module.
Many lemmas about coprimality of ideals are also generalized to the noncommutative, two-sided setting.
---
- [x] depends on: #21904
[](https://gitpod.io/from-referrer/)
|
t-algebra label:t-algebra$ |
216/156 |
Mathlib/Algebra/Algebra/Operations.lean,Mathlib/AlgebraicGeometry/EllipticCurve/Group.lean,Mathlib/RingTheory/Extension.lean,Mathlib/RingTheory/Finiteness/Basic.lean,Mathlib/RingTheory/Finiteness/Ideal.lean,Mathlib/RingTheory/HopkinsLevitzki.lean,Mathlib/RingTheory/Ideal/Maps.lean,Mathlib/RingTheory/Ideal/Operations.lean |
8 |
4 |
['alreadydone', 'github-actions', 'leanprover-bot', 'mathlib4-dependent-issues-bot'] |
nobody |
18-304 18 days ago |
18-77447 18 days ago |
45-85513 45 days |
| 22089 |
sgouezel author:sgouezel |
feat: composing a continuous multilinear map with continuous linear maps is analytic in both variables |
Also prove that the composition of continuously polynomial functions is continuously polynomial.
---
- [x] depends on: #22102
- [x] depends on: #22789
[](https://gitpod.io/from-referrer/)
|
t-analysis |
209/3 |
Mathlib/Analysis/Analytic/CPolynomial.lean,Mathlib/Analysis/Analytic/Composition.lean,Mathlib/Analysis/NormedSpace/Multilinear/Basic.lean,Mathlib/Data/Multiset/DershowitzManna.lean,Mathlib/Order/KrullDimension.lean |
5 |
7 |
['github-actions', 'grunweg', 'mathlib4-dependent-issues-bot', 'sgouezel'] |
nobody |
17-65550 17 days ago |
17-65564 17 days ago |
56-32115 56 days |
| 22279 |
xyzw12345 author:xyzw12345 |
feat(RingTheory/GradedAlgebra): homogeneous relation |
In this PR, we defined the concept of a homogeneous relation and proved some properties about homogeneous relations. The main result of this PR is showing that taking `RingQuot` by a homogeneous relation can give a graded structure on the quotient ring. This result can be used to define graded structures on rings obtained using `RingQuot`, e.g. the Symmetric Algebra defined in #21539 can be verified to have such a structure.
Co-authored-by:
Zhixuan Dai @atstarrysky <22300180006@m.fudan.edu.cn>
Yiming Fu @pelicanhere
Zhenyan Fu @pumpkin678
Raphael Douglas Giles @Raph-DG
Jiedong Jiang @jjdishere
- [x] depends on: #22354
---
[](https://gitpod.io/from-referrer/)
|
new-contributor
t-algebra
label:t-algebra$ |
455/0 |
Mathlib.lean,Mathlib/Algebra/Algebra/Equiv.lean,Mathlib/Algebra/DirectSum/Basic.lean,Mathlib/Algebra/DirectSum/Module.lean,Mathlib/Algebra/Module/LinearMap/Defs.lean,Mathlib/Algebra/RingQuot.lean,Mathlib/RingTheory/GradedAlgebra/Basic.lean,Mathlib/RingTheory/GradedAlgebra/HomogeneousRelation.lean |
8 |
6 |
['Paul-Lez', 'github-actions', 'mathlib4-dependent-issues-bot', 'ocfnash', 'xyzw12345'] |
nobody |
17-26083 17 days ago |
17-26086 17 days ago |
18-57877 18 days |
| 23496 |
chrisflav author:chrisflav |
chore(Algebra): the five lemma for modules |
We reprove the five lemma for modules for universe generality, avoiding the import of `Mathlib.CategoryTheory.Abelian.DiagramLemmas.Four` in otherwise non-category-theoretic files and for ease of application.
---
See #23497 for a golf using this.
[](https://gitpod.io/from-referrer/)
|
t-algebra label:t-algebra$ |
158/0 |
Mathlib.lean,Mathlib/Algebra/FiveLemma.lean |
2 |
7 |
['acmepjz', 'chrisflav', 'erdOne', 'github-actions'] |
nobody |
17-25441 17 days ago |
19-1088 19 days ago |
19-1074 19 days |
| 23531 |
fpvandoorn author:fpvandoorn |
refactor: generalize `unbounded_of_tendsto_atTop` |
---
Not sure if I like this style of proofs with `aesop` for future PRs. It's short, though.
[](https://gitpod.io/from-referrer/)
|
t-topology |
13/19 |
Mathlib/Order/Filter/AtTopBot/Basic.lean |
1 |
2 |
['github-actions', 'sgouezel'] |
nobody |
17-5746 17 days ago |
18-8180 18 days ago |
18-8166 18 days |
| 21182 |
joneugster author:joneugster |
fix(Util/CountHeartbeats): move elaboration in #count_heartbeats inside a namespace |
Currently the `#count_heartbeat` linter reported the heartbeats until it concluded `error: [declaration] has already been declared` instead of re-elaborating the declaration.
---
[Zulip report](https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/count_heartbeats.20for.20all.20declarations.20in.20a.20file.3F/near/496303652)
[](https://gitpod.io/from-referrer/)
|
t-meta |
72/5 |
Mathlib/Util/CountHeartbeats.lean,MathlibTest/CountHeartbeats.lean |
2 |
16 |
['adomani', 'github-actions', 'joneugster', 'mathlib-bors'] |
nobody |
16-84341 16 days ago |
16-84826 16 days ago |
19-31830 19 days |
| 23282 |
joelriou author:joelriou |
feat(CategoryTheory): monomorphisms in Type are stable under transfinite compositions |
`monomorphisms (Type u)` is stable under cobase change, filtered colimits and transfinite compositions.
(The file `CategoryTheory.Types` is also moved to `CategoryTheory.Types.Basic`.)
(This is extended to presheaves of types in #23298.)
---
[](https://gitpod.io/from-referrer/)
|
t-category-theory |
159/15 |
Mathlib.lean,Mathlib/CategoryTheory/Category/Cat.lean,Mathlib/CategoryTheory/Category/RelCat.lean,Mathlib/CategoryTheory/ConcreteCategory/Basic.lean,Mathlib/CategoryTheory/ConcreteCategory/EpiMono.lean,Mathlib/CategoryTheory/Core.lean,Mathlib/CategoryTheory/Functor/Hom.lean,Mathlib/CategoryTheory/IsomorphismClasses.lean,Mathlib/CategoryTheory/Limits/Types/Shapes.lean,Mathlib/CategoryTheory/Monad/Types.lean,Mathlib/CategoryTheory/MorphismProperty/TransfiniteComposition.lean,Mathlib/CategoryTheory/SmallObject/WellOrderInductionData.lean,Mathlib/CategoryTheory/Subobject/Types.lean,Mathlib/CategoryTheory/Types/Basic.lean,Mathlib/CategoryTheory/Types/Monomorphisms.lean,Mathlib/CategoryTheory/UnivLE.lean,Mathlib/Control/Fold.lean,Mathlib/Data/Set/FunctorToTypes.lean |
18 |
1 |
['github-actions'] |
nobody |
16-71300 16 days ago |
16-72292 16 days ago |
25-51153 25 days |
| 17802 |
vihdzp author:vihdzp |
feat(SetTheory/Ordinal/Veblen): epsilon and gamma ordinals |
We define the epsilon function `ε_ o = veblen 1 o`, and the gamma function `Γ_ o` which enumerates the fixed points of `veblen · 0`.
---
- [x] depends on: #17751
- [x] depends on: #18611
[](https://gitpod.io/from-referrer/)
|
t-set-theory
maintainer-merge
|
146/7 |
Mathlib/SetTheory/Ordinal/FixedPoint.lean,Mathlib/SetTheory/Ordinal/Veblen.lean |
2 |
15 |
['YaelDillies', 'github-actions', 'mathlib4-dependent-issues-bot', 'vihdzp'] |
nobody |
16-40787 16 days ago |
16-40787 16 days ago |
48-53174 48 days |
| 19946 |
vihdzp author:vihdzp |
feat(SetTheory/ZFC/Basic): order instances |
Sets form a partial order under the subset relation.
---
[](https://gitpod.io/from-referrer/)
|
t-set-theory |
38/2 |
Mathlib/SetTheory/ZFC/Basic.lean,Mathlib/SetTheory/ZFC/Class.lean,Mathlib/SetTheory/ZFC/PSet.lean |
3 |
8 |
['alreadydone', 'b-mehta', 'github-actions', 'vihdzp'] |
nobody |
16-25005 16 days ago |
16-29367 16 days ago |
47-30097 47 days |
| 23370 |
kebekus author:kebekus |
feat: taking the divisor of a meromorphic function commutes with restriction |
Deliver on a very simple TODO, show that taking the divisor of a meromorphic function commutes with restriction.
This material is used in [Project VD](https://github.com/kebekus/ProjectVD), which aims to formalize Value Distribution Theory for meromorphic functions on the complex plane.
---
[](https://gitpod.io/from-referrer/)
|
t-analysis |
12/1 |
Mathlib/Analysis/Meromorphic/Divisor.lean |
1 |
1 |
['github-actions'] |
nobody |
16-21303 16 days ago |
16-21318 16 days ago |
22-86277 22 days |
| 23363 |
kebekus author:kebekus |
feat: congruence lemmas for divisors of meromorphic functions |
Deliver on open TODO and state elementary congruence lemmas for divisors of meromorphic functions.
This material is used in [Project VD](https://github.com/kebekus/ProjectVD), which aims to formalize Value Distribution Theory for meromorphic functions on the complex plane.
---
[](https://gitpod.io/from-referrer/)
|
t-analysis |
78/1 |
Mathlib/Analysis/Meromorphic/Basic.lean,Mathlib/Analysis/Meromorphic/Divisor.lean |
2 |
1 |
['github-actions'] |
nobody |
16-21061 16 days ago |
16-21076 16 days ago |
23-12121 23 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 |
16-13138 16 days ago |
16-13154 16 days ago |
50-9653 50 days |
| 23627 |
kebekus author:kebekus |
feat: add logarithmic counting function of Value Distribution Theory |
Implement the logarithmic counting function of Value Distribution Theory and provide supporting API.
This material is used in [Project VD](https://github.com/kebekus/ProjectVD), which aims to formalize Value Distribution Theory for meromorphic functions on the complex plane.
---
[](https://gitpod.io/from-referrer/)
|
t-analysis |
217/0 |
Mathlib.lean,Mathlib/Analysis/Complex/ValueDistribution/CountingFunction.lean |
2 |
1 |
['github-actions'] |
nobody |
16-5052 16 days ago |
16-5322 16 days ago |
16-5379 16 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
|
247/1 |
Mathlib/Data/Nat/GCD/Basic.lean,Mathlib/NumberTheory/SelbergSieve.lean |
2 |
6 |
['Ruben-VandeVelde', 'github-actions', 'mathlib4-dependent-issues-bot'] |
nobody |
16-1523 16 days ago |
30-80056 30 days ago |
30-80041 30 days |
| 23632 |
JovanGerb author:JovanGerb |
perf(CategoryTheory/Subobject/Lattice): reorder instance arguments |
The `HasImages C` type class fails more quickly, so I set it as the first type class argument.
---
[](https://gitpod.io/from-referrer/)
|
t-category-theory |
4/5 |
Mathlib/CategoryTheory/Subobject/Lattice.lean |
1 |
4 |
['JovanGerb', 'github-actions', 'leanprover-bot'] |
nobody |
15-84757 15 days ago |
16-411 16 days ago |
16-461 16 days |
| 21838 |
joneugster author:joneugster |
feat(Cache): Allow arguments of the form `Mathlib.Data` which correspond to a folder but not a file |
---
- [x] depends on: #21834
[](https://gitpod.io/from-referrer/)
|
CI
t-meta
|
34/11 |
Cache/IO.lean,Cache/Main.lean |
2 |
9 |
['eric-wieser', 'github-actions', 'joneugster', 'mathlib4-dependent-issues-bot', 'mergify'] |
nobody |
14-82908 14 days ago |
14-82908 14 days ago |
17-66300 17 days |
| 23657 |
grunweg author:grunweg |
feat: euclidean half spaces and quadrants have convex interior |
These lemmas are a prerequisite for #23658, which will impose that real or complex models with corners have convex interior.
---
[](https://gitpod.io/from-referrer/)
|
t-differential-geometry |
48/0 |
Mathlib/Geometry/Manifold/Instances/Real.lean |
1 |
9 |
['Ruben-VandeVelde', 'github-actions', 'grunweg'] |
nobody |
14-79523 14 days ago |
15-18288 15 days ago |
15-18274 15 days |
| 23603 |
YaelDillies author:YaelDillies |
feat: distributive Haar characters |
The name is made up in analogy with modular characters.
From FLT
Co-authored-by: Andrew Yang
Co-authored-by: Javier López-Contreras <38789151+javierlcontreras@users.noreply.github.com>
---
[](https://gitpod.io/from-referrer/)
|
FLT
t-measure-probability
|
87/0 |
Mathlib.lean,Mathlib/MeasureTheory/Measure/Haar/DistribChar.lean |
2 |
5 |
['AntoineChambert-Loir', 'YaelDillies', 'github-actions', 'tb65536'] |
nobody |
14-77785 14 days ago |
16-2853 16 days ago |
16-63376 16 days |
| 23673 |
erdOne author:erdOne |
feat(AlgebraicGeometry): delaborator for coercing schemes to types |
Co-authored-by: Christian Merten
---
[](https://gitpod.io/from-referrer/)
|
t-algebraic-geometry |
21/0 |
Mathlib/AlgebraicGeometry/Scheme.lean |
1 |
1 |
['github-actions'] |
nobody |
14-75372 14 days ago |
14-75372 14 days ago |
14-75423 14 days |
| 23440 |
xroblot author:xroblot |
chore(NumberField/Units): make `torsionOrder` a `Nat` |
Originally, the order of the torsion subgroup of units of a number field was defined as a `PNat` since `rootsOfUnity` was using `PNat`. This is not the case anymore since `rootsOfUnity` is now using `NeZero` instead. Thus, we change the type of `torsionOrder` to `Nat` and change to an `abbrev` so that it gets a `NeZero` instance automatically.
As a bonus, we also prove that `torsionOrder` is even.
---
[](https://gitpod.io/from-referrer/)
|
t-number-theory |
17/6 |
Mathlib/NumberTheory/NumberField/CanonicalEmbedding/FundamentalCone.lean,Mathlib/NumberTheory/NumberField/Units/Basic.lean |
2 |
1 |
['github-actions'] |
nobody |
14-75081 14 days ago |
20-70045 20 days ago |
20-70089 20 days |
| 23424 |
YaelDillies author:YaelDillies |
chore: move `StrictMonoOn f s → InjOn f s` earlier |
This is motivated by the need to have these lemmas early in #23177.
---
[](https://gitpod.io/from-referrer/)
|
large-import
t-order
|
29/34 |
Mathlib/Algebra/Order/Field/Basic.lean,Mathlib/Data/Int/Lemmas.lean,Mathlib/Data/Set/Monotone.lean,Mathlib/Order/Hom/Basic.lean,Mathlib/Order/Hom/Set.lean,Mathlib/Order/Interval/Set/Monotone.lean,Mathlib/Order/ModularLattice.lean,Mathlib/Order/Monotone/Basic.lean,Mathlib/Order/Monotone/Defs.lean,Mathlib/Order/Monotone/Extension.lean |
10 |
1 |
['github-actions'] |
nobody |
14-67542 14 days ago |
14-67556 14 days ago |
20-80241 20 days |
| 23676 |
Parcly-Taxel author:Parcly-Taxel |
chore: deprime `induction'` for localizations and quotients |
All these removed instances of `induction'` generate only one subgoal. In some cases `obtain` can be used.
The relevant instances were identified by adding the following to `Mathlib.Tactic.Cases`
```diff
diff --git a/Mathlib/Tactic/Cases.lean b/Mathlib/Tactic/Cases.lean
index 4a60db6c551..08c06520879 100644
--- a/Mathlib/Tactic/Cases.lean
+++ b/Mathlib/Tactic/Cases.lean
@@ -122,6 +122,16 @@ elab (name := induction') "induction' " tgts:(Parser.Tactic.elimTarget,+)
g.assign result.elimApp
let subgoals ← ElimApp.evalNames elimInfo result.alts withArg
(generalized := fvarIds) (toClear := targetFVarIds) (toTag := toTag)
+ let body ← inferType targets[0]!
+ let names : Array Format := if withArg.1.getArgs.size > 1 then
+ (withArg.1.getArgs[1]!).getArgs.map Syntax.prettyPrint else Array.empty
+ let gens : Array Format := if genArg.1.getArgs.size > 1 then
+ (genArg.1.getArgs[1]!).getArgs.map Syntax.prettyPrint else Array.empty
+ let inductor : Format := if usingArg.1.getArgs.size > 1 then
+ Syntax.prettyPrint usingArg.1.getArgs[1]! else "~"
+ if subgoals.toList.length ≤ 1 then
+ logInfoAt tgts m!"{body.getAppFn.setPPExplicit true} {inductor} {gens} {names} \
+ {subgoals.toList.length}"
setGoals <| (subgoals ++ result.others).toList ++ gs
/-- The `cases'` tactic is similar to the `cases` tactic in Lean 4 core, but the syntax for giving
```
and then examining [the output](https://github.com/leanprover-community/mathlib4/actions/runs/14270845291/job/40003467676). |
tech debt |
87/108 |
Mathlib/Algebra/Module/LocalizedModule/Basic.lean,Mathlib/Algebra/Pointwise/Stabilizer.lean,Mathlib/Analysis/SpecialFunctions/Complex/Circle.lean,Mathlib/Analysis/SpecialFunctions/Pow/NNReal.lean,Mathlib/CategoryTheory/Action/Concrete.lean,Mathlib/CategoryTheory/Galois/EssSurj.lean,Mathlib/CategoryTheory/Limits/Types/Colimits.lean,Mathlib/CategoryTheory/Subobject/Basic.lean,Mathlib/CategoryTheory/Subobject/FactorThru.lean,Mathlib/CategoryTheory/Subobject/Lattice.lean,Mathlib/Data/Finset/NoncommProd.lean,Mathlib/Data/Finsupp/BigOperators.lean,Mathlib/Data/Fintype/Quotient.lean,Mathlib/Data/List/Cycle.lean,Mathlib/Data/Nat/ChineseRemainder.lean,Mathlib/Data/Setoid/Partition.lean,Mathlib/FieldTheory/RatFunc/Basic.lean,Mathlib/GroupTheory/GroupAction/Quotient.lean,Mathlib/GroupTheory/OreLocalization/Basic.lean,Mathlib/GroupTheory/Perm/Cycle/Concrete.lean,Mathlib/GroupTheory/Perm/Sign.lean,Mathlib/GroupTheory/Torsion.lean,Mathlib/RingTheory/OreLocalization/Basic.lean,Mathlib/RingTheory/OreLocalization/Ring.lean,Mathlib/SetTheory/Surreal/Basic.lean |
25 |
7 |
['Parcly-Taxel', 'apnelson1', 'eric-wieser', 'github-actions'] |
nobody |
14-43843 14 days ago |
14-64885 14 days ago |
14-64871 14 days |
| 23678 |
plp127 author:plp127 |
feat: recursor for nonempty lists |
Adds `List.recNeNil` and `List.recOnNeNil` for motives that depend on the list being nonempty. Taken from [Zulip](https://leanprover.zulipchat.com/#narrow/channel/217875-Is-there-code-for-X.3F/topic/accessing.20the.20source.20case.20during.20induction/near/502101211).
---
[](https://gitpod.io/from-referrer/)
|
t-data |
40/0 |
Mathlib/Data/List/Induction.lean |
1 |
5 |
['eric-wieser', 'github-actions', 'plp127'] |
nobody |
14-42522 14 days ago |
14-63081 14 days ago |
14-63136 14 days |
| 23681 |
Timeroot author:Timeroot |
feat(Algebra/Polynomial): Descartes' Rule of signs |
Proof of Descartes' Rule of Signs. Last PR from https://github.com/Timeroot/lean-descartes-signs , now that #9085 is merged. Defines `Polynomial.SignVariations` as the relevant quantity, and `descartes_rule_of_signs` as the headline theorem.
---
I tried to clean it up + golf it down and did shrink it a good deal. The lemma `signvar_mul_eraseLead_le_of_nextCoeff` is still 142 lines, and `succ_sign_lin_mul` is ~140 lines of code as well. Those are the ugly ones. I welcome ideas if someone wants to try to clean them up more! But the proof really does require an annoying bit of case-splitting, as far as I can tell.
[](https://gitpod.io/from-referrer/)
|
t-algebra label:t-algebra$ |
661/3 |
Mathlib.lean,Mathlib/Algebra/Polynomial/CoeffList.lean,Mathlib/Algebra/Polynomial/Degree/Operations.lean,Mathlib/Algebra/Polynomial/EraseLead.lean,Mathlib/Algebra/Polynomial/RuleOfSigns.lean |
5 |
1 |
['github-actions'] |
nobody |
14-41006 14 days ago |
14-57096 14 days ago |
14-57147 14 days |
| 23687 |
plp127 author:plp127 |
feat: clopen characterization of connected spaces |
Proves that a space is connected iff it contains no nontrivial clopen sets.
---
[](https://gitpod.io/from-referrer/)
|
t-topology |
13/0 |
Mathlib/Topology/Connected/Clopen.lean |
1 |
1 |
['github-actions'] |
nobody |
14-35095 14 days ago |
14-35096 14 days ago |
14-35153 14 days |
| 23684 |
alreadydone author:alreadydone |
feat(RingTheory): integral extensions of comm. rings are local homs |
---
The import increase only affects one file so I hope it's okay.
[](https://gitpod.io/from-referrer/)
|
large-import
t-algebra
label:t-algebra$ |
57/64 |
Mathlib/Algebra/Field/Equiv.lean,Mathlib/Algebra/Group/Invertible/Basic.lean,Mathlib/AlgebraicGeometry/Morphisms/Proper.lean,Mathlib/FieldTheory/LinearDisjoint.lean,Mathlib/LinearAlgebra/Dimension/Localization.lean,Mathlib/RingTheory/Artinian/Ring.lean,Mathlib/RingTheory/IntegralClosure/Algebra/Defs.lean,Mathlib/RingTheory/IntegralClosure/IsIntegralClosure/Basic.lean,Mathlib/RingTheory/LinearDisjoint.lean,Mathlib/RingTheory/Localization/FractionRing.lean,Mathlib/RingTheory/Localization/Integral.lean,Mathlib/RingTheory/SimpleRing/Field.lean |
12 |
4 |
['alreadydone', 'github-actions', 'xroblot'] |
nobody |
14-15370 14 days ago |
14-46768 14 days ago |
14-46792 14 days |
| 23669 |
erdOne author:erdOne |
feat(FieldTheory): abelian extensions |
---
[](https://gitpod.io/from-referrer/)
|
t-algebra label:t-algebra$ |
74/0 |
Mathlib.lean,Mathlib/FieldTheory/Galois/Abelian.lean,Mathlib/NumberTheory/Cyclotomic/Gal.lean |
3 |
4 |
['alreadydone', 'erdOne', 'github-actions', 'xroblot'] |
nobody |
14-15290 14 days ago |
14-78038 14 days ago |
14-78037 14 days |
| 18754 |
FR-vdash-bot author:FR-vdash-bot |
feat: `IsometryClass` |
---
- [ ] depends on: #18689
[](https://gitpod.io/from-referrer/)
|
t-analysis
t-topology
|
99/3 |
Mathlib/Analysis/Normed/Group/Uniform.lean,Mathlib/Topology/MetricSpace/Isometry.lean,scripts/nolints_prime_decls.txt |
3 |
2 |
['github-actions', 'j-loreaux', 'mathlib4-dependent-issues-bot'] |
nobody |
14-13030 14 days ago |
14-13030 14 days ago |
41-51878 41 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$ |
24/0 |
Mathlib/LinearAlgebra/LinearPMap.lean,Mathlib/LinearAlgebra/Span/Defs.lean |
2 |
1 |
['github-actions'] |
nobody |
13-66247 13 days ago |
13-66377 13 days ago |
23-35947 23 days |
| 23360 |
kim-em author:kim-em |
chore: review of `erw` in `Algebra/Homology/DerivedCategory` |
|
|
21/15 |
Mathlib/Algebra/Homology/DerivedCategory/Basic.lean,Mathlib/Algebra/Homology/DerivedCategory/Ext/ExtClass.lean,Mathlib/Algebra/Homology/DerivedCategory/SingleTriangle.lean,Mathlib/Algebra/Homology/HomotopyCategory/SingleFunctors.lean,Mathlib/CategoryTheory/Shift/SingleFunctors.lean |
5 |
2 |
['Ruben-VandeVelde', 'github-actions'] |
nobody |
13-62783 13 days ago |
23-32242 23 days ago |
23-32228 23 days |
| 15906 |
grunweg author:grunweg |
feat: define singular manifolds |
These are used to define bordism groups: the `n`th bordism group of a topological space `X` is the space of cobordism classes of all singular manifolds on `X`.
---
This PR can best be seen in context in #23138 - which also proves that this definition is usable.
(Older branches in this direction are [this branch](https://github.com/leanprover-community/mathlib4/compare/master...MR-bordism-theory) (my first iteration) and [this one](https://github.com/leanprover-community/mathlib4/compare/master...MR-bordism-theory-v2) (second iteration); #23138 has a bit less progress on the boundary data, but pushes bordisms further.
[](https://gitpod.io/from-referrer/)
|
t-differential-geometry |
255/1 |
Mathlib.lean,Mathlib/Geometry/Manifold/Bordisms.lean,Mathlib/Geometry/Manifold/IsManifold/Basic.lean |
3 |
69 |
['YaelDillies', 'alreadydone', 'github-actions', 'grunweg', 'sgouezel'] |
sgouezel assignee:sgouezel |
13-57863 13 days ago |
24-13911 24 days ago |
111-65142 111 days |
| 23715 |
jsm28 author:jsm28 |
feat(Geometry/Euclidean/Basic): make `orthogonalProjection` a continuous affine map |
Change `EuclideanGeometry.orthogonalProjection` from a bundled `AffineMap` to a bundled `ContinuousAffineMap` (I think I'll end up wanting continuity for some things related to `incenter`).
Note 1: I think the new import is reasonable in the context for anything much doing Euclidean geometry / using orthogonal projections, but we'll see from CI how many imports it adds.
Note 2: this now means the previous `orthogonalProjection` is a `private` definition `orthogonalProjectionAux`, in order for the continuity proof using `AffineMap.continuous_linear_iff` to work. Is there a better way to refer directly to a structure projection to a parent within the `where` definition without having such an extra definition of the parent structure? I couldn't get it to work without the extra definition.
Note 3: the actual motivation is to make `signedDist` a bundled continuous affine map. I've left that change to be done separately (a) to avoid conflicts with #23646 and (b) because I think it will need a few other definitions elsewhere in mathlib to be set up (not everything in the definition of `signedDist` has analogues for `ContinuousAffineMap` at present).
Note 4: I think it would be a good idea to refactor orthogonal projections further so there is only *one* definition, `orthogonalProjection` set up directly as a composition of continuous affine maps (move to vector space via an arbitrary choice of base point, apply the orthogonal projection there, move back to affine space), without needing either `orthogonalProjectionFn` or `orthogonalProjectionAux` (and then `orthogonalProjectionFn` would be deprecated with a view to removal). But that composition also requires a few new definitions not currently in mathlib (including but not limited to `ContinuousAffineEquiv.vaddConst` from #22583). Since we've had `orthogonalProjectionFn` for a long time, I don't think that cleanup is particularly urgent.
---
[](https://gitpod.io/from-referrer/)
|
t-euclidean-geometry |
26/10 |
Mathlib/Geometry/Euclidean/Basic.lean,Mathlib/Geometry/Euclidean/Circumcenter.lean |
2 |
1 |
['github-actions'] |
nobody |
13-35621 13 days ago |
13-35683 13 days ago |
13-35669 13 days |
| 21944 |
Thmoas-Guan author:Thmoas-Guan |
feat(RingTheory/Powerseries): Weierstrass preparation for complete local ring |
Weierstrass preparation theorem for complete local ring
---
- [x] depends on: #21900
- [x] depends on: #22369
[](https://gitpod.io/from-referrer/)
|
t-algebra label:t-algebra$ |
532/0 |
Mathlib.lean,Mathlib/RingTheory/WeierstrassPreparation.lean |
2 |
15 |
['Thmoas-Guan', 'acmepjz', 'github-actions', 'mathlib4-dependent-issues-bot', 'riccardobrasca'] |
riccardobrasca assignee:riccardobrasca |
13-27391 13 days ago |
49-412 1 month ago |
55-82043 55 days |
| 21969 |
peabrainiac author:peabrainiac |
feat(Geometry/Diffeology): basics of diffeological spaces |
Introduces diffeological spaces, smooth maps between them, the D-topology and the standard diffeology on finite-dimensional normed spaces.
---
This is the first of hopefully many PRs upstreaming work that I have done on diffeological spaces in [my orbifolds repo](https://github.com/peabrainiac/lean-orbifolds), containing the first half of `Diffeology/Basic.lean`.
[](https://gitpod.io/from-referrer/)
|
t-differential-geometry |
472/0 |
Mathlib.lean,Mathlib/Geometry/Diffeology/Basic.lean,docs/references.bib,scripts/noshake.json |
4 |
22 |
['github-actions', 'grunweg', 'lecopivo', 'peabrainiac'] |
nobody |
13-18355 13 days ago |
30-13353 30 days ago |
11-19972 11 days |
| 23594 |
YaelDillies author:YaelDillies |
refactor: merge `DomMulAct` and `DomAddAct` into `DomAct` |
This has several advantages:
* Less API surface with a single definition instead of two
* Better match the existing `ConjAct` type synonym
* We get to use a better name for the multiplication by an element of the type synonym: Previously `dmaSMul`, now `domSMul`.
and no inconvenient because the instances for `DomMulAct` and `DomAddAct` are by definition disjoint.
---
[](https://gitpod.io/from-referrer/)
|
|
337/335 |
Mathlib.lean,Mathlib/Algebra/Group/Translate.lean,Mathlib/Algebra/Module/CharacterModule.lean,Mathlib/Algebra/Module/Hom.lean,Mathlib/Algebra/Module/LinearMap/Basic.lean,Mathlib/Algebra/Module/LinearMap/Defs.lean,Mathlib/GroupTheory/GroupAction/DomAct/ActionHom.lean,Mathlib/GroupTheory/GroupAction/DomAct/Basic.lean,Mathlib/GroupTheory/Perm/Centralizer.lean,Mathlib/GroupTheory/Perm/DomAct.lean,Mathlib/MeasureTheory/Function/AEEqFun/DomAct.lean,Mathlib/MeasureTheory/Function/LpSpace/DomAct/Basic.lean,Mathlib/MeasureTheory/Function/LpSpace/DomAct/Continuous.lean,Mathlib/MeasureTheory/Group/MeasurableEquiv.lean,Mathlib/Topology/Algebra/Constructions/DomAct.lean,Mathlib/Topology/Algebra/Constructions/DomMulAct.lean |
16 |
4 |
['YaelDillies', 'eric-wieser', 'github-actions', 'urkud'] |
nobody |
13-14111 13 days ago |
16-75807 16 days ago |
16-75793 16 days |
| 23711 |
alreadydone author:alreadydone |
chore(RingTheory): generalize primeSpectrumProdHomeo to CommSemiring |
---
[](https://gitpod.io/from-referrer/)
|
t-algebra
t-algebraic-geometry
label:t-algebra$ |
33/9 |
Mathlib/RingTheory/Spectrum/Prime/Topology.lean |
1 |
14 |
['Ruben-VandeVelde', 'alreadydone', 'erdOne', 'github-actions'] |
nobody |
12-50706 12 days ago |
12-69778 12 days ago |
13-43972 13 days |
| 23762 |
Parcly-Taxel author:Parcly-Taxel |
feat: relative upper/lower sets |
From a comment by @b-mehta [on Zulip](https://leanprover.zulipchat.com/#narrow/channel/217875-Is-there-code-for-X.3F/topic/Finset.20sum.20bounds/near/506567011) in response to me formalising IMO 2015 Q6 (#23038). |
t-order |
171/0 |
Mathlib.lean,Mathlib/Order/Defs/Unbundled.lean,Mathlib/Order/UpperLower/Relative.lean |
3 |
1 |
['github-actions'] |
nobody |
12-19313 12 days ago |
12-19377 12 days ago |
12-19363 12 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 |
12-7821 12 days ago |
35-75235 1 month ago |
35-75274 35 days |
| 23752 |
jsm28 author:jsm28 |
feat(Geometry/Euclidean/Incenter): incenters and excenters |
Define the exspheres and insphere of a simplex (in dimension 1 and greater), and corresponding definitions for their center and radius. Give necessary and sufficient conditions for them to exist (in terms of the barycentric coordinates, being signed versions of the inverses of the distances between vertices and opposite faces, having a nonzero sum) and show that they do always exist in the case of the incenter and of the excenter opposite a single vertex (the latter in dimensions 2 and greater), and that any point lying in the span of the vertices and equidistant from the faces opposite the vertices is an excenter (and, when signs of the equal distances are given, is the excenter with corresponding signs).
Some major pieces are deferred to followups, in particular definitions of touchpoints, tangency of exspheres and insphere to faces, and the relation to angle bisectors in various forms. But since the file is already over 600 lines, I think this is a reasonable starting point (and since the lemmas do show that the definitions have their characteristic properties of points being equidistant from the faces on the desired sides, I think it sufficiently justifies that the definitions are correct and usable as-is).
Feel free to golf; the calculations involved in showing that the excenter opposite a vertex always exists (in dimensions 2 and greater) are rather long.
---
[](https://gitpod.io/from-referrer/)
- [x] depends on: #23712
- [x] depends on: #23751 |
t-euclidean-geometry |
620/0 |
Mathlib.lean,Mathlib/Geometry/Euclidean/Incenter.lean |
2 |
7 |
['eric-wieser', 'github-actions', 'jsm28', 'mathlib4-dependent-issues-bot'] |
nobody |
11-82107 11 days ago |
12-19755 12 days ago |
12-20311 12 days |
| 23732 |
jsm28 author:jsm28 |
feat(LinearAlgebra/AffineSpace/ContinuousAffineEquiv): `toContinuousAffineMap` |
Add the conversion from `ContinuousAffineEquiv` to `ContinuousAffineMap`, which seems to be missing from mathlib.
I'm not sure exactly what API such conversions are meant to have - `toHomeomorph` doesn't have any - but I added `rfl` lemmas about converting to a function either directly or via
`toContinuousAffineMap`, and about different pairs of conversion paths involving `toContinuousAffineMap` producing the same result, as well as injectivity of `toContinuousAffineMap`.
---
[](https://gitpod.io/from-referrer/)
|
t-algebra
t-topology
label:t-algebra$ |
34/0 |
Mathlib/LinearAlgebra/AffineSpace/ContinuousAffineEquiv.lean |
1 |
3 |
['eric-wieser', 'github-actions', 'jsm28'] |
nobody |
11-74716 11 days ago |
12-73422 12 days ago |
12-73408 12 days |
| 22415 |
pechersky author:pechersky |
feat(Algebra/Order/Hom/Monoid): order iso versions of unitsWithZero and friends |
---
- [ ] depends on: #22402
[](https://gitpod.io/from-referrer/)
|
t-algebra label:t-algebra$ |
27/15 |
Mathlib/Algebra/GroupWithZero/WithZero.lean,Mathlib/Algebra/Order/Hom/Monoid.lean,Mathlib/GroupTheory/ArchimedeanDensely.lean |
3 |
2 |
['github-actions', 'mathlib4-dependent-issues-bot'] |
nobody |
11-66743 11 days ago |
11-72755 11 days ago |
11-72990 11 days |
| 22420 |
pechersky author:pechersky |
feat(Order/Prod/Lex/{Hom,Monoid,GroupWithZero}): ordered inclusions and projections of prod of ordered groups |
---
- [ ] depends on: #22402
[](https://gitpod.io/from-referrer/)
|
t-order
t-algebra
label:t-algebra$ |
256/0 |
Mathlib.lean,Mathlib/Order/Prod/Lex/GroupWithZero.lean,Mathlib/Order/Prod/Lex/Hom.lean,Mathlib/Order/Prod/Lex/Monoid.lean |
4 |
2 |
['github-actions', 'mathlib4-dependent-issues-bot'] |
nobody |
11-66717 11 days ago |
11-72756 11 days ago |
11-74551 11 days |
| 23804 |
hanwenzhu author:hanwenzhu |
feat(Analysis/SpecialFunctions): extend `tendsto_one_plus_div_rpow_exp` |
This PR
- Proves 12 theorems (they are stated separately because of differences in `rexp` vs `cexp` and `pow` vs `rpow` vs `cpow`):
- The limit of `x * log (1 + t/x + o(1/x))` as `x → ∞` is `t` for `t : ℂ` or `ℝ` and `x : ℝ` or `ℕ`.
- The limit of `(1 + t/x + o(1/x)) ^ x` as `x → ∞` is `t` for `t : ℂ` or `ℝ` and `x : ℝ` or `ℕ`.
- The limit of `(1 + t/x) ^ x` as `x → ∞` is `t` for `t : ℂ` or `ℝ` and `x : ℝ` or `ℕ`.
- (Note: the last row of theorems for `t : ℝ` already exist and are now replaced)
- Renames `plus` to `add` in affected theorems
The little-o theorem for `t : ℂ` is needed for [CLT](https://github.com/RemyDegenne/CLT).
Moves:
- tendsto_one_plus_div_rpow_exp -> Real.tendsto_one_add_div_rpow_exp
- tendsto_one_plus_div_pow_exp -> Real.tendsto_one_add_div_pow_exp
- tendsto_integral_mul_one_plus_inv_smul_sq_pow -> tendsto_integral_mul_one_add_inv_smul_sq_pow
---
[](https://gitpod.io/from-referrer/)
|
t-analysis |
187/41 |
Mathlib/Analysis/SpecialFunctions/Complex/LogBounds.lean,Mathlib/Analysis/SpecialFunctions/Gamma/Beta.lean,Mathlib/Analysis/SpecialFunctions/Log/Deriv.lean,Mathlib/Analysis/SpecialFunctions/MulExpNegMulSqIntegral.lean,Mathlib/Analysis/SpecialFunctions/Pow/Deriv.lean |
5 |
1 |
['github-actions'] |
nobody |
11-50658 11 days ago |
11-51081 11 days ago |
11-51068 11 days |
| 23756 |
urkud author:urkud |
feat(Asymptotics): define `IsBigOTVS` |
- Turn `IsLittleOTVS` into a 1-field `structure`. We may want to replace the definition with "the ratio of `egauge`s tends to zero". In `ENNReal`, it's the right definition.
- Define `IsBigOTVS`, prove basic API lemmas.
- Prove lemmas about `IsLittleOTVS` in (indexed) products.
---
[](https://gitpod.io/from-referrer/)
|
t-analysis |
208/59 |
Mathlib/Analysis/Asymptotics/TVS.lean |
1 |
6 |
['eric-wieser', 'github-actions', 'urkud'] |
nobody |
11-36104 11 days ago |
11-36156 11 days ago |
11-80883 11 days |
| 23690 |
mbkybky author:mbkybky |
refactor(Algebra/Category/ModuleCat): generalize the universe of `ModuleCat.enoughProjectives` |
Generalize the universe in the statement of `ModuleCat.enoughProjectives` and `ModuleCat.enoughInjectives`.
---
[](https://gitpod.io/from-referrer/)
|
t-algebra label:t-algebra$ |
27/39 |
Mathlib/Algebra/Category/ModuleCat/EnoughInjectives.lean,Mathlib/Algebra/Category/ModuleCat/Projective.lean,Mathlib/Algebra/Homology/LocalCohomology.lean,Mathlib/RepresentationTheory/GroupCohomology/Resolution.lean,scripts/nolints_prime_decls.txt |
5 |
1 |
['github-actions'] |
nobody |
11-27387 11 days ago |
14-12292 14 days ago |
14-12345 14 days |
| 22365 |
euprunin author:euprunin |
feat: register more tactics for `hint` |
The following example shows test cases that `hint` now supports, which were unsupported prior to this PR:
```
import Mathlib
-- The tactics registered in this PR
register_hint abel
register_hint bound
register_hint group
register_hint noncomm_ring
register_hint norm_num
register_hint positivity
register_hint ring
-- "hint" now correctly suggests "abel" which closes the goal (no closing tactic suggested prior to this PR)
example {α} [AddCommMonoid α] (a b c d: α) : a + b + c + d + 0 = d + (c + b) + (0 + 0 + a) := by hint
-- "hint" now correctly suggests "bound" which closes the goal (no closing tactic suggested prior to this PR)
example (a b : ℝ) (h1 : ‖a‖ ≤ ‖b‖) (h2 : 3 ≤ ‖b‖) : ‖b ^ 2 + a‖ ≥ ‖b ^ 2‖ - ‖a‖ ∧ ‖b ^ 2‖ - ‖a‖ ≥ ‖b ^ 2‖ - ‖b‖ ∧ (‖b‖ - 1) * ‖b‖ ≥ 2 * ‖b‖ := by hint
-- "hint" now correctly suggests "group" which closes the goal (no closing tactic suggested prior to this PR)
example (G : Type) (a b c : G) [Group G] : c⁻¹ * (b * c⁻¹) * c * (a * b) * (b⁻¹ * a⁻¹ * b⁻¹) * c = 1 := by hint
-- "hint" now correctly suggests "noncomm_ring" which closes the goal (no closing tactic suggested prior to this PR)
example (R : Type) (a b : R) [Ring R] : (a + b) ^ 3 = a ^ 3 + a ^ 2 * b + a * b * a + a * b ^ 2 + b * a ^ 2 + b * a * b + b ^ 2 * a + b ^ 3 := by hint
-- "hint" now correctly suggests "norm_num" which closes the goal (no closing tactic suggested prior to this PR)
example : (2 : ℝ) < 5 / 2 ∧ 5 / 2 < 3 := by hint
-- "hint" now correctly suggests "positivity" which closes the goal (no closing tactic suggested prior to this PR)
example (a : ℤ) : 0 < |a| + 3 := by hint
-- "hint" now correctly suggests "ring" which closes the goal (no closing tactic suggested prior to this PR)
example (α : Type) (a b c : α) [LinearOrderedField α] : a * (-c / b) * (-c / b) + -c + c = a * (c / b * (c / b)) := by hint
``` |
t-meta |
60/1 |
Mathlib/Tactic/Abel.lean,Mathlib/Tactic/Bound.lean,Mathlib/Tactic/Group.lean,Mathlib/Tactic/NoncommRing.lean,Mathlib/Tactic/NormNum.lean,Mathlib/Tactic/Positivity/Core.lean,Mathlib/Tactic/Ring.lean,MathlibTest/hint.lean |
8 |
6 |
['euprunin', 'github-actions', 'j-loreaux'] |
nobody |
11-23116 11 days ago |
11-23116 11 days ago |
12-63323 12 days |
| 23365 |
vasnesterov author:vasnesterov |
feat(Tactic/Simproc): nested quantifiers in `existsAndEq` |
Generalize the `existsAndEq` simproc to nested existential quantifiers.
For example `∃ a, p a ∧ ∃ b, a = f b ∧ q b` now simplifies to `∃ b, p (f b) ∧ q b`.
---
[](https://gitpod.io/from-referrer/)
|
large-import
t-meta
|
440/73 |
Mathlib/Tactic/Simproc/ExistsAndEq.lean,MathlibTest/Simproc/ExistsAndEq.lean |
2 |
40 |
['JovanGerb', 'b-mehta', 'eric-wieser', 'github-actions', 'kim-em', 'leanprover-bot', 'leanprover-community-mathlib4-bot', 'vasnesterov'] |
nobody |
11-19467 11 days ago |
16-48611 16 days ago |
21-75256 21 days |
| 23810 |
b-reinke author:b-reinke |
chore(Order/Interval): generalize succ/pred lemmas to partial orders |
Many lemmas in `Mathlib/Order/Interval/Set/SuccPred.lean`and `Mathlib/Order/Interval/Finset/SuccPred.lean` also work for partial orders. They are generalized in this PR by introducing different sections for `PartialOrder` and `LinearOrder` assumptions in the respective files.
---
[](https://gitpod.io/from-referrer/)
|
t-order |
231/89 |
Mathlib/Order/Interval/Finset/SuccPred.lean,Mathlib/Order/Interval/Set/SuccPred.lean |
2 |
1 |
['github-actions'] |
nobody |
11-18064 11 days ago |
11-18064 11 days ago |
11-18121 11 days |
| 23252 |
mariainesdff author:mariainesdff |
feat(Algebra/Polynomial): add lemmas |
---
[](https://gitpod.io/from-referrer/)
|
t-algebra label:t-algebra$ |
49/1 |
Mathlib/Algebra/Polynomial/Basic.lean,Mathlib/Algebra/Polynomial/BigOperators.lean,Mathlib/Algebra/Polynomial/Lifts.lean,Mathlib/Algebra/Polynomial/Monic.lean,Mathlib/Algebra/Polynomial/RingDivision.lean,Mathlib/Algebra/Polynomial/Roots.lean,Mathlib/Algebra/Polynomial/Splits.lean |
7 |
8 |
['alreadydone', 'github-actions', 'mariainesdff'] |
nobody |
10-81016 10 days ago |
16-79033 16 days ago |
26-865 26 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$ |
28/0 |
Mathlib/RingTheory/Localization/Pi.lean |
1 |
24 |
['Paul-Lez', 'alreadydone', 'erdOne', 'github-actions', 'grunweg', 'jcommelin', 'maddycrim'] |
nobody |
10-78589 10 days ago |
12-73657 12 days ago |
59-60486 59 days |
| 23838 |
FordUniver author:FordUniver |
feat(SimpleGraph): added completeGraph.adjDecidable |
added completeGraph.adjDecidable
---
Strangely `DecidableRel (completeGraph V).Adj` does not seem to be automatically inferred from `Top.adjDecidable` even though `⊤ : SimpleGraph V` is defined as `completeGraph V`. Am I missing something here or is it as simple as adding these two lines to mathlib? |
new-contributor
t-combinatorics
|
4/1 |
Mathlib/Combinatorics/SimpleGraph/Basic.lean |
1 |
8 |
['FordUniver', 'YaelDillies', 'github-actions'] |
nobody |
10-63054 10 days ago |
10-74030 10 days ago |
10-74085 10 days |
| 23371 |
grunweg author:grunweg |
chore: mark `Disjoint.{eq_bot, inter_eq}` simp |
And add the analogous lemma to `Finset`.
Spun out from #22964, hence transitively part of my bordism theory project.
Some lemmas there are more conveniently stated with `Disjoint`, which requires tagging at least `inter_eq` with simp.
---
[](https://gitpod.io/from-referrer/)
|
t-order |
12/11 |
Mathlib/Data/Finset/Lattice/Basic.lean,Mathlib/Data/Finset/Lattice/Lemmas.lean,Mathlib/Data/Set/Basic.lean,Mathlib/Data/Set/Disjoint.lean,Mathlib/Order/Disjoint.lean,Mathlib/Topology/Compactification/OnePoint.lean,Mathlib/Topology/Order/OrderClosed.lean |
7 |
29 |
['YaelDillies', 'eric-wieser', 'github-actions', 'grunweg', 'leanprover-bot', 'leanprover-community-mathlib4-bot'] |
nobody |
10-60370 10 days ago |
11-74779 11 days ago |
12-35258 12 days |
| 20897 |
yuma-mizuno author:yuma-mizuno |
feat(CategoryTheory/Bicategory): add lemmas about mates in bicategories |
Continued from #20891. This PR completes the bicategorical proofs for the lemmas whose Cat versions are provided in `Mathlib/CategoryTheory/Adjunction/Mates.lean`.
---
- [x] depends on: #20891
[](https://gitpod.io/from-referrer/)
|
t-category-theory |
366/0 |
Mathlib/CategoryTheory/Bicategory/Adjunction/Mate.lean |
1 |
6 |
['github-actions', 'joelriou', 'kim-em', 'mathlib4-dependent-issues-bot', 'yuma-mizuno'] |
nobody |
10-53234 10 days ago |
10-53234 10 days ago |
33-1801 33 days |
| 23849 |
chrisflav author:chrisflav |
feat(Data/Set): add `Set.encard_iUnion` |
---
[](https://gitpod.io/from-referrer/)
|
large-import
t-data
|
61/0 |
Mathlib/Algebra/BigOperators/Finprod.lean,Mathlib/Data/Set/Card/Arithmetic.lean,Mathlib/Data/Set/Finite/Lattice.lean |
3 |
1 |
['github-actions'] |
nobody |
10-49713 10 days ago |
10-49720 10 days ago |
10-49765 10 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: Zhixuan Dai <22300180006@m.fudan.edu.cn>
Co-authored-by: Zhenyan Fu
Co-authored-by: Yiming Fu
Co-authored-by: Wang Jingting
---
[](https://gitpod.io/from-referrer/)
|
maintainer-merge
new-contributor
t-algebra
label:t-algebra$ |
223/0 |
Mathlib.lean,Mathlib/Algebra/Symmetrized.lean,Mathlib/LinearAlgebra/SymmetricAlgebra/Basic.lean,Mathlib/LinearAlgebra/SymmetricAlgebra/MvPolynomial.lean |
4 |
47 |
['ADedecker', 'Raph-DG', 'YaelDillies', 'eric-wieser', 'github-actions', 'xyzw12345'] |
nobody |
10-44915 10 days ago |
11-16749 11 days ago |
66-74745 66 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$ |
81/0 |
Mathlib.lean,Mathlib/RingTheory/TwoSidedIdeal/SpanAsSum.lean |
2 |
42 |
['Paul-Lez', 'Whysoserioushah', 'eric-wieser', 'github-actions', 'kbuzzard'] |
nobody |
10-44090 10 days ago |
24-48033 24 days ago |
24-48081 24 days |
| 18266 |
bjoernkjoshanssen author:bjoernkjoshanssen |
feat: Second-derivative test from calculus |
We prove the Second-Derivative test from calculus using the First-Derivative test.
Source: [Wikipedia](https://en.wikipedia.org/wiki/Derivative_test#Proof_of_the_second-derivative_test).
---
[](https://gitpod.io/from-referrer/)
|
t-analysis |
149/0 |
Mathlib.lean,Mathlib/Analysis/Calculus/SecondDerivativeTest.lean |
2 |
37 |
['bjoernkjoshanssen', 'eric-wieser', 'fpvandoorn', 'github-actions', 'j-loreaux'] |
nobody |
10-43660 10 days ago |
10-43660 10 days ago |
62-23245 62 days |
| 23459 |
Timeroot author:Timeroot |
feat: Definition of `Clone` notations and typeclasses |
Definitions and notation typeclasses for #20051
---
[](https://gitpod.io/from-referrer/)
|
t-algebra label:t-algebra$ |
84/0 |
Mathlib.lean,Mathlib/Algebra/Clone/Defs.lean |
2 |
17 |
['Timeroot', 'YaelDillies', 'eric-wieser', 'github-actions', 'urkud'] |
YaelDillies assignee:YaelDillies |
10-38583 10 days ago |
11-78329 11 days ago |
14-41035 14 days |
| 23381 |
vlad902 author:vlad902 |
feat: copy Subgroup lemma for Submonoid |
This is an exact copy of `Subgroup.map_top_of_surjective`, copied for Submonoid. |
t-algebra label:t-algebra$ |
8/0 |
Mathlib/Algebra/Group/Submonoid/Operations.lean |
1 |
5 |
['eric-wieser', 'github-actions', 'urkud', 'vlad902'] |
nobody |
10-37584 10 days ago |
22-61363 22 days ago |
22-61645 22 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/1 |
Mathlib.lean,Mathlib/Algebra/Order/Floor/Extended.lean,Mathlib/Algebra/Order/Floor/Semiring.lean,Mathlib/Data/Int/CardIntervalMod.lean |
4 |
17 |
['YaelDillies', 'eric-wieser', 'github-actions', 'urkud'] |
nobody |
10-25520 10 days ago |
13-70970 13 days ago |
25-40204 25 days |
| 22961 |
xroblot author:xroblot |
feat(ZLattice/Covolume): add `covolume_div_covolume_eq_relindex` |
Add the following result:
Let `L₁` be a sub-`ℤ`-lattice of `L₂`. Then the index of `L₁` inside `L₂` is equal to `covolume L₁ / covolume L₂`.
---
- [x] depends on: #22940
- [x] depends on: #23759
[](https://gitpod.io/from-referrer/)
|
t-algebra label:t-algebra$ |
64/1 |
Mathlib/Algebra/Module/ZLattice/Basic.lean,Mathlib/Algebra/Module/ZLattice/Covolume.lean,Mathlib/GroupTheory/Index.lean,Mathlib/LinearAlgebra/Determinant.lean |
4 |
8 |
['Ruben-VandeVelde', 'github-actions', 'mathlib4-dependent-issues-bot', 'xroblot'] |
nobody |
10-24398 10 days ago |
10-26119 10 days ago |
32-23684 32 days |
| 23705 |
YaelDillies author:YaelDillies |
chore: move `Module.End`-related decls to the `Module.End` namespace |
No deprecations, since they would clash across namespaces.
From Toric
---
[](https://gitpod.io/from-referrer/)
|
toric
t-algebra
label:t-algebra$ |
314/328 |
Mathlib/Algebra/Algebra/Basic.lean,Mathlib/Algebra/Algebra/Bilinear.lean,Mathlib/Algebra/Group/ForwardDiff.lean,Mathlib/Algebra/Lie/CartanExists.lean,Mathlib/Algebra/Lie/Derivation/Basic.lean,Mathlib/Algebra/Lie/Engel.lean,Mathlib/Algebra/Lie/EngelSubalgebra.lean,Mathlib/Algebra/Lie/LieTheorem.lean,Mathlib/Algebra/Lie/Nilpotent.lean,Mathlib/Algebra/Lie/OfAssociative.lean,Mathlib/Algebra/Lie/Sl2.lean,Mathlib/Algebra/Lie/TraceForm.lean,Mathlib/Algebra/Lie/Weights/Basic.lean,Mathlib/Algebra/Lie/Weights/Cartan.lean,Mathlib/Algebra/Lie/Weights/Chain.lean,Mathlib/Algebra/Lie/Weights/Killing.lean,Mathlib/Algebra/Module/Equiv/Basic.lean,Mathlib/Algebra/Module/FinitePresentation.lean,Mathlib/Algebra/Module/LinearMap/End.lean,Mathlib/Algebra/Module/LocalizedModule/Basic.lean,Mathlib/Algebra/Module/LocalizedModule/Submodule.lean,Mathlib/Algebra/Module/Submodule/Ker.lean,Mathlib/Algebra/Module/Submodule/LinearMap.lean,Mathlib/Algebra/Module/Submodule/Map.lean,Mathlib/Algebra/Module/Submodule/Range.lean,Mathlib/Algebra/Polynomial/Derivative.lean,Mathlib/Algebra/Polynomial/Module/Basic.lean,Mathlib/AlgebraicGeometry/Modules/Tilde.lean,Mathlib/Analysis/Calculus/LagrangeMultipliers.lean,Mathlib/Analysis/InnerProductSpace/Adjoint.lean,Mathlib/Analysis/InnerProductSpace/Symmetric.lean,Mathlib/Data/Matrix/Bilinear.lean,Mathlib/FieldTheory/JacobsonNoether.lean,Mathlib/LinearAlgebra/Charpoly/Basic.lean,Mathlib/LinearAlgebra/Eigenspace/Basic.lean,Mathlib/LinearAlgebra/Eigenspace/Minpoly.lean,Mathlib/LinearAlgebra/Eigenspace/Pi.lean,Mathlib/LinearAlgebra/Eigenspace/Triangularizable.lean,Mathlib/LinearAlgebra/Eigenspace/Zero.lean,Mathlib/LinearAlgebra/FiniteDimensional/Basic.lean,Mathlib/LinearAlgebra/Matrix/InvariantBasisNumber.lean,Mathlib/LinearAlgebra/Matrix/ToLin.lean,Mathlib/LinearAlgebra/Projection.lean,Mathlib/LinearAlgebra/QuadraticForm/Basic.lean,Mathlib/LinearAlgebra/QuadraticForm/Dual.lean,Mathlib/LinearAlgebra/Quotient/Basic.lean,Mathlib/LinearAlgebra/Reflection.lean,Mathlib/LinearAlgebra/RootSystem/Defs.lean,Mathlib/LinearAlgebra/RootSystem/Hom.lean,Mathlib/LinearAlgebra/Semisimple.lean,Mathlib/LinearAlgebra/Span/Basic.lean,Mathlib/LinearAlgebra/TensorProduct/Basic.lean,Mathlib/LinearAlgebra/Trace.lean,Mathlib/RepresentationTheory/Basic.lean,Mathlib/RepresentationTheory/FDRep.lean,Mathlib/RepresentationTheory/GroupCohomology/LowDegree.lean,Mathlib/RepresentationTheory/GroupCohomology/Resolution.lean,Mathlib/RepresentationTheory/Invariants.lean,Mathlib/RepresentationTheory/Rep.lean,Mathlib/RingTheory/Artinian/Module.lean,Mathlib/RingTheory/CotangentLocalizationAway.lean,Mathlib/RingTheory/Derivation/Lie.lean,Mathlib/RingTheory/Finiteness/Nilpotent.lean,Mathlib/RingTheory/IsTensorProduct.lean,Mathlib/RingTheory/Kaehler/TensorProduct.lean,Mathlib/RingTheory/LocalProperties/Projective.lean,Mathlib/RingTheory/Localization/Algebra.lean,Mathlib/RingTheory/Nilpotent/Exp.lean,Mathlib/RingTheory/Nilpotent/Lemmas.lean,Mathlib/RingTheory/Noetherian/Defs.lean,Mathlib/RingTheory/Polynomial/Basic.lean,Mathlib/RingTheory/Polynomial/Bernstein.lean,Mathlib/RingTheory/SimpleModule/Basic.lean,Mathlib/RingTheory/Spectrum/Prime/FreeLocus.lean,Mathlib/RingTheory/TensorProduct/Basic.lean |
75 |
4 |
['github-actions', 'urkud'] |
nobody |
10-22533 10 days ago |
10-24451 10 days ago |
13-57653 13 days |
| 23748 |
vasnesterov author:vasnesterov |
feat(Analysis/Analytic): `HasFPowerSeriesOnBall.comp_sub` variations |
Prove `HasFPowerSeriesOnBall.comp_sub` variations for `HasFPowerSeriesOnBall`'s friend structures.
---
[](https://gitpod.io/from-referrer/)
|
t-analysis |
52/0 |
Mathlib/Analysis/Analytic/Basic.lean |
1 |
4 |
['github-actions', 'urkud', 'vasnesterov'] |
nobody |
10-17577 10 days ago |
12-46883 12 days ago |
12-46959 12 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 |
10-13959 10 days ago |
46-17822 1 month ago |
47-48097 47 days |
| 13649 |
FR-vdash-bot author:FR-vdash-bot |
chore: redefine `Nat.div2` `Nat.bodd` |
The new definitions are faster than the old ones. `Nat.binaryRec` will be moved to batteries (https://github.com/leanprover-community/batteries/pull/799) or core (https://github.com/leanprover/lean4/pull/3756), so relevant contents are moved to a new file temporarily.
---
- [x] depends on: #15567
- [x] depends on: #19666
[](https://gitpod.io/from-referrer/)
|
|
63/88 |
Mathlib/Computability/Primrec.lean,Mathlib/Data/Int/Bitwise.lean,Mathlib/Data/Nat/Bits.lean,Mathlib/Data/Nat/Bitwise.lean,Mathlib/Data/Nat/Size.lean,Mathlib/Logic/Denumerable.lean,Mathlib/Logic/Encodable/Basic.lean,Mathlib/Logic/Equiv/Nat.lean |
8 |
14 |
['FR-vdash-bot', 'digama0', 'eric-wieser', 'github-actions', 'mathlib4-dependent-issues-bot', 'urkud'] |
digama0 assignee:digama0 |
10-5012 10 days ago |
10-23141 10 days ago |
74-12428 74 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 |
6 |
['alreadydone', 'eric-wieser', 'github-actions', 'leanprover-community-bot-assistant'] |
nobody |
9-82897 9 days ago |
9-82914 9 days ago |
26-69933 26 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.
- [x] depends on: #21134
[](https://gitpod.io/from-referrer/)
|
t-topology |
332/0 |
Mathlib.lean,Mathlib/Topology/Compactness/KSpace.lean,docs/references.bib |
3 |
15 |
['StevenClontz', 'github-actions', 'jzxia', 'mathlib4-dependent-issues-bot', 'scholzhannah', 'urkud'] |
nobody |
9-75617 9 days ago |
10-2439 10 days ago |
51-40932 51 days |
| 23890 |
erdOne author:erdOne |
refactor(AlgebraicGeometry): add `supportSet` field to `IdealSheafData` |
---
[](https://gitpod.io/from-referrer/)
|
t-algebraic-geometry |
280/169 |
Mathlib/AlgebraicGeometry/IdealSheaf.lean,Mathlib/AlgebraicGeometry/Scheme.lean |
2 |
1 |
['github-actions'] |
nobody |
9-57565 9 days ago |
9-58234 9 days ago |
9-58288 9 days |
| 23648 |
wwylele author:wwylele |
feat(Topology/Order): add `Dense.exists_seq_strict{Mono/Anti}_tendsto` |
Add `Dense.exists_seq_strict{Mono/Anti}_tendsto{'}` that restricts the sequence to a dense subset. This is useful for e.g. finding a monotone rational sequence approaching a real number.
Co-authored-by: Jireh Loreaux
---
[](https://gitpod.io/from-referrer/)
|
new-contributor
t-topology
|
62/0 |
Mathlib/Topology/Instances/Real/Lemmas.lean,Mathlib/Topology/Order/IsLUB.lean |
2 |
10 |
['github-actions', 'j-loreaux', 'wwylele'] |
nobody |
9-32277 9 days ago |
13-64811 13 days ago |
15-34373 15 days |
| 21950 |
erdOne author:erdOne |
feat(NumberTheory/Padics): the completion of `ℚ` at a finite place is `ℚ_[p]` |
---
[](https://gitpod.io/from-referrer/)
|
t-number-theory |
255/1 |
Mathlib.lean,Mathlib/Algebra/GroupWithZero/WithZero.lean,Mathlib/NumberTheory/Padics/HeightOneSpectrum.lean,Mathlib/NumberTheory/Padics/PadicNumbers.lean,Mathlib/Topology/Algebra/Valued/WithVal.lean,Mathlib/Topology/Algebra/WithZeroMulInt.lean,Mathlib/Topology/Algebra/WithZeroTopology.lean |
7 |
17 |
['Ruben-VandeVelde', 'erdOne', 'github-actions', 'xroblot'] |
nobody |
9-9607 9 days ago |
19-55670 19 days ago |
20-58190 20 days |
| 23913 |
kebekus author:kebekus |
feat: introduce factorized rational functions |
Discuss functions `𝕜 → 𝕜` of the form `∏ᶠ u, (· - u) ^ d u`, where `d : 𝕜 → ℤ` is integer-valued. Show that these "factorized rational functions" are meromorphic in normal form, with divisor equal to `d`. Factorized rational functions will be used in a follow-up PR to extract poles and zeros from meromorphic functions. This, in turn, will be useful to show prove integrability of functions of type log |meromorphic| that frequently appear in complex analysis.
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 |
170/2 |
Mathlib.lean,Mathlib/Analysis/Analytic/Constructions.lean,Mathlib/Analysis/Meromorphic/FactorizedRational.lean |
3 |
2 |
['github-actions', 'kebekus'] |
nobody |
9-5511 9 days ago |
9-6220 9 days ago |
9-6282 9 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$ |
39/0 |
Mathlib/Algebra/Module/ZLattice/Basic.lean,Mathlib/LinearAlgebra/Dimension/Finite.lean,Mathlib/Topology/Homeomorph/Defs.lean |
3 |
2 |
['github-actions', 'leanprover-community-bot-assistant'] |
nobody |
9-4799 9 days ago |
9-4816 9 days ago |
31-50175 31 days |
| 22823 |
b-reinke author:b-reinke |
feat(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`.
The associator vanishes exactly when `R` is associative.
We prove variants of this statement also for the `AddMonoidHom` bundled version of the associator,
as well as the bundled version of `mulLeft₃` and `mulRight₃`, the multiplications `(x * y) * z` and
`x * (y * z)`.
---
[](https://gitpod.io/from-referrer/)
|
large-import
maintainer-merge
new-contributor
t-algebra
label:t-algebra$ |
133/8 |
Mathlib.lean,Mathlib/Algebra/DirectSum/Ring.lean,Mathlib/Algebra/Ring/Associator.lean |
3 |
46 |
['Paul-Lez', 'YaelDillies', 'b-reinke', 'eric-wieser', 'github-actions', 'leanprover-community-bot-assistant'] |
nobody |
9-4661 9 days ago |
9-12198 9 days ago |
32-73547 32 days |
| 23472 |
erdOne author:erdOne |
feat(Topology): Continuous open maps with irreducible fibers induce bijections between irreducible components |
Co-authored-by: Christian Merten
---
[](https://gitpod.io/from-referrer/)
|
t-topology |
77/0 |
Mathlib/Topology/Irreducible.lean |
1 |
3 |
['ADedecker', 'erdOne', 'github-actions'] |
nobody |
9-3513 9 days ago |
19-32398 19 days ago |
19-32444 19 days |
| 23777 |
joelriou author:joelriou |
feat(CategoryTheory): the center of a category |
This PR introduces an abbrevation `CatCenter C` for the center of a category `C`, i.e. the type of endomorphisms of the identity functor of `C`.
---
[](https://gitpod.io/from-referrer/)
|
t-category-theory |
53/0 |
Mathlib.lean,Mathlib/CategoryTheory/Center/Basic.lean |
2 |
1 |
['github-actions'] |
nobody |
9-2937 9 days ago |
9-2937 9 days ago |
11-78216 11 days |
| 22882 |
xroblot author:xroblot |
feat(NumberField/Units): add `regOfFamily` and refactor `regulator` |
This is a refactor of `NumberField.regulator`.
We introduce `regOfFamily` which is the regulator of a family of units indexed by `Fin (Units.rank K)`. It is equal to `0` if the family is not `isMaxRank`. This a `Prop` that says that the image of the family in the `logSpace K` is linearly independent and thus generates a full lattice. All the results about computing the `regulator` by some matrix determinant computation are now proved more generally for `regOfFamily`.
The `regulator` of a number field is still defined as the covolume of the `unitLattice` and we prove that is is also equal to `regOfFamily` of the system of fundamental units `fundSystem K`. Together with the results about computing `regOfFamily`, we recover that way the results about computing the regulator.
---
- [x] depends on: #22868
[](https://gitpod.io/from-referrer/)
|
t-number-theory |
186/56 |
Mathlib/LinearAlgebra/Matrix/Determinant/Basic.lean,Mathlib/NumberTheory/NumberField/CanonicalEmbedding/NormLeOne.lean,Mathlib/NumberTheory/NumberField/Units/Regulator.lean |
3 |
4 |
['alreadydone', 'github-actions', 'leanprover-community-bot-assistant', 'mathlib4-dependent-issues-bot'] |
nobody |
8-82109 8 days ago |
8-82125 8 days ago |
33-3522 33 days |
| 23729 |
alreadydone author:alreadydone |
chore(LinearAlgebra): generalize some lemmas |
and move them to earlier files.
`rank_subsingleton'`, `rank_punit` and `rank_bot` are generalized from Ring to Semiring.
`linearIndependent_subsingleton_iff` is generalized to Semiring and an extraneous NoZeroSMulDivisors condition is removed.
`ENat.card_ne_zero_iff_nonempty` is added.
---
[](https://gitpod.io/from-referrer/)
|
t-algebra label:t-algebra$ |
57/45 |
Mathlib.lean,Mathlib/Algebra/Algebra/Subalgebra/Rank.lean,Mathlib/LinearAlgebra/Dimension/Basic.lean,Mathlib/LinearAlgebra/Dimension/Constructions.lean,Mathlib/LinearAlgebra/Dimension/Finite.lean,Mathlib/LinearAlgebra/Dimension/FreeAndStrongRankCondition.lean,Mathlib/LinearAlgebra/Dimension/Subsingleton.lean,Mathlib/LinearAlgebra/Dimension/Torsion/Basic.lean,Mathlib/LinearAlgebra/FreeAlgebra.lean,Mathlib/LinearAlgebra/LinearIndependent/Basic.lean,Mathlib/LinearAlgebra/LinearIndependent/Defs.lean,Mathlib/RingTheory/Ideal/Cotangent.lean,Mathlib/SetTheory/Cardinal/Finite.lean |
13 |
10 |
['alreadydone', 'erdOne', 'github-actions', 'leanprover-bot', 'leanprover-community-mathlib4-bot'] |
nobody |
8-81372 8 days ago |
8-81421 8 days ago |
9-13679 9 days |
| 23181 |
YaelDillies author:YaelDillies |
chore(UniformSpace/Defs): move entourages to their own file |
What's left in `UniformSpace.Defs` is precisely the theory of the uniformity filter.
The motivation is that the theory of coverings and packings in both high dimensional probability and dynamics can be based on entourages, while they have little to do with the uniformity filter (indeed, entourages are in a sense a quantitative version of the uniformity filter).
---
[](https://gitpod.io/from-referrer/)
|
t-topology |
180/207 |
Mathlib.lean,Mathlib/Topology/Metrizable/Uniformity.lean,Mathlib/Topology/UniformSpace/Defs.lean,Mathlib/Topology/UniformSpace/Entourage.lean |
4 |
12 |
['ADedecker', 'PatrickMassot', 'YaelDillies', 'b-mehta', 'github-actions'] |
nobody |
8-81176 8 days ago |
23-9176 23 days ago |
26-29607 26 days |
| 23888 |
j-loreaux author:j-loreaux |
feat: properties of graded rings indexed by canonically linearly ordered additive monoids |
---
- [ ] depends on: #23883
- [ ] depends on: #23886
[](https://gitpod.io/from-referrer/)
|
t-algebra label:t-algebra$ |
100/0 |
Mathlib/Algebra/DirectSum/Internal.lean |
1 |
9 |
['eric-wieser', 'github-actions', 'j-loreaux', 'leanprover-community-bot-assistant', 'mathlib4-dependent-issues-bot'] |
nobody |
8-71603 8 days ago |
8-72200 8 days ago |
8-73002 8 days |
| 23251 |
mariainesdff author:mariainesdff |
feat(FieldTheory/IntermediateField/Adjoin): add lemmas |
---
[](https://gitpod.io/from-referrer/)
|
t-algebra label:t-algebra$ |
57/0 |
Mathlib/FieldTheory/IntermediateField/Adjoin/Basic.lean,Mathlib/FieldTheory/IsAlgClosed/AlgebraicClosure.lean |
2 |
16 |
['alreadydone', 'github-actions', 'mariainesdff', 'tb65536'] |
nobody |
8-58229 8 days ago |
26-10024 26 days ago |
26-10010 26 days |
| 23718 |
syur2 author:syur2 |
feat(Algebra): hom localize equiv localize hom |
Add the linear equiv of `S^{-1}(M =>[R] N)` equiv `(S^{-1} M) =>[S^{-1}R] (S^{-1} N)` for finitely presented module `M`.
---
[](https://gitpod.io/from-referrer/)
|
new-contributor
t-algebra
label:t-algebra$ |
21/0 |
Mathlib/Algebra/Module/FinitePresentation.lean |
1 |
1 |
['github-actions'] |
nobody |
8-41977 8 days ago |
13-21522 13 days ago |
13-21520 13 days |
| 23930 |
Vtec234 author:Vtec234 |
feat(Tactic): dependent rewriting |
Add dependent rewrite tactics `rw!` and `rewrite!`.
These operate by inserting casts in front of terms that would otherwise become type-incorrect after the rewrite.
In the default mode, only proof terms are casted, so that (by proof irrelevance) no observable complexity is added.
In the most liberal mode, the tactics never encounter the 'motive is not type correct' error,
but may add casts that make the goal or other term very complex.
Co-authored-by: Aaron Liu
---
This has been discussed on Zulip [here](https://leanprover.zulipchat.com/#narrow/channel/239415-metaprogramming-.2F-tactics/topic/dependent.20rewrite.20tactic/with/504228516). See the included test file for example rewrites that this tactic can do.
[](https://gitpod.io/from-referrer/)
|
t-meta |
706/0 |
Mathlib.lean,Mathlib/Tactic.lean,Mathlib/Tactic/DepRewrite.lean,MathlibTest/depRewrite.lean |
4 |
1 |
['github-actions'] |
nobody |
8-38635 8 days ago |
8-44884 8 days ago |
8-44937 8 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 |
8-36489 8 days ago |
59-72213 2 months ago |
59-81366 59 days |
| 23923 |
YaelDillies author:YaelDillies |
feat: a discrete monoid has compact Pontryagin dual |
From LeanAPAP
---
[](https://gitpod.io/from-referrer/)
|
t-topology |
47/10 |
Mathlib/Topology/Algebra/Group/CompactOpen.lean,Mathlib/Topology/Algebra/PontryaginDual.lean,Mathlib/Topology/CompactOpen.lean,Mathlib/Topology/ContinuousMap/Basic.lean,Mathlib/Topology/Separation/NotNormal.lean |
5 |
9 |
['YaelDillies', 'b-mehta', 'github-actions'] |
nobody |
8-7679 8 days ago |
8-7679 8 days ago |
8-12746 8 days |
| 19591 |
joelriou author:joelriou |
feat(CategoryTheory/Abelian): Ext^0 and Ext-groups when there are enough projectives |
Let `C : Type u` be an abelian category (`Category.{v} C`). We deduce from #19585 that `Ext X Y 0` identifies to the type of morphisms from `X` to `Y`. Moreover, assuming that `C` has enough projectives and is locally `w`-small, i.e. the type of morphisms in `C` are `Small.{w}`, we show that the condition `HasExt.{w}` holds, which means that for `X` and `Y` in `C`, and `n : ℕ`, we may define `Ext X Y n : Type w`. In particular, this holds for `w = v`.
This is an important step in order to get a reasonably usable API for Ext-groups.
---
- [x] depends on: #19585
- [x] depends on: #19584
- [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 |
233/24 |
Mathlib.lean,Mathlib/Algebra/Homology/DerivedCategory/Basic.lean,Mathlib/Algebra/Homology/DerivedCategory/Ext/Basic.lean,Mathlib/Algebra/Homology/DerivedCategory/Ext/EnoughProjectives.lean,Mathlib/Algebra/Homology/DerivedCategory/Fractions.lean,Mathlib/Algebra/Homology/Embedding/CochainComplex.lean,Mathlib/CategoryTheory/Abelian/Projective/Dimension.lean |
7 |
n/a |
['github-actions', 'joelriou', 'kbuzzard', 'leanprover-community-bot-assistant', 'mathlib4-dependent-issues-bot', 'mbkybky'] |
nobody |
7-83508 7 days ago |
unknown |
unknown |
| 23940 |
YaelDillies author:YaelDillies |
feat: polytopes |
From Toric
Co-authored-by: Matthew Johnson
---
[](https://gitpod.io/from-referrer/)
|
toric
t-analysis
|
59/0 |
Mathlib.lean,Mathlib/Analysis/Convex/Polytope.lean |
2 |
5 |
['Parcly-Taxel', 'YaelDillies', 'eric-wieser', 'github-actions'] |
nobody |
7-80543 7 days ago |
8-7646 8 days ago |
8-21273 8 days |
| 23893 |
eric-wieser author:eric-wieser |
chore: add missing rfl lemmas for the tensor product of coalgebras |
These are taken from https://github.com/ImperialCollegeLondon/FLT/blob/eef74b4538c8852363936dfaad23e6ffba72eca5/FLT/mathlibExperiments/Coalgebra/TensorProduct.lean
`simps` previously generated the `def` lemmas, but they were badly-named, and probably not actually convenient as `simp` lemmas.
---
[](https://gitpod.io/from-referrer/)
|
t-algebra label:t-algebra$ |
27/8 |
Mathlib/Algebra/Category/CoalgebraCat/ComonEquivalence.lean,Mathlib/RingTheory/Coalgebra/Basic.lean,Mathlib/RingTheory/Coalgebra/TensorProduct.lean,Mathlib/RingTheory/HopfAlgebra/TensorProduct.lean |
4 |
1 |
['github-actions'] |
nobody |
7-77321 7 days ago |
9-53815 9 days ago |
9-53870 9 days |
| 23338 |
WilliamCoram author:WilliamCoram |
feat: restricted power series form a ring |
We define restricted powerseries over a normed ring R, and show they form a ring when R has the ultrametric property.
---
[](https://gitpod.io/from-referrer/)
|
new-contributor
t-number-theory
|
186/0 |
Mathlib.lean,Mathlib/RingTheory/PowerSeries/Restricted.lean |
2 |
17 |
['Paul-Lez', 'WilliamCoram', 'github-actions', 'grunweg'] |
nobody |
7-75600 7 days ago |
23-84953 23 days ago |
23-85078 23 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
|
562/360 |
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 |
3 |
['github-actions', 'leanprover-community-bot-assistant', 'mathlib4-dependent-issues-bot'] |
grunweg assignee:grunweg |
7-72572 7 days ago |
7-72588 7 days ago |
48-43426 48 days |
| 23324 |
Parcly-Taxel author:Parcly-Taxel |
chore: deprime `induction'` with 5+ variables, part 3 |
Based on a comment by @apnelson1 on [Zulip](https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/The.20plan.20to.20remove.20induction'/near/508274747).
The relevant instances were identified by adding the following to `Mathlib.Tactic.Cases`
```diff
diff --git a/Mathlib/Tactic/Cases.lean b/Mathlib/Tactic/Cases.lean
index 4a60db6c551..29ec70424c7 100644
--- a/Mathlib/Tactic/Cases.lean
+++ b/Mathlib/Tactic/Cases.lean
@@ -122,6 +122,16 @@ elab (name := induction') "induction' " tgts:(Parser.Tactic.elimTarget,+)
g.assign result.elimApp
let subgoals ← ElimApp.evalNames elimInfo result.alts withArg
(generalized := fvarIds) (toClear := targetFVarIds) (toTag := toTag)
+ let body ← inferType targets[0]!
+ let names : Array Format := if withArg.1.getArgs.size > 1 then
+ (withArg.1.getArgs[1]!).getArgs.map Syntax.prettyPrint else Array.empty
+ let gens : Array Format := if genArg.1.getArgs.size > 1 then
+ (genArg.1.getArgs[1]!).getArgs.map Syntax.prettyPrint else Array.empty
+ let inductor : Format := if usingArg.1.getArgs.size > 1 then
+ Syntax.prettyPrint usingArg.1.getArgs[1]! else "~"
+ if 5 ≤ names.size then
+ logInfoAt tgts m!"{body.getAppFn.setPPExplicit true} {inductor} {gens} {names} \
+ {subgoals.toList.length}"
setGoals <| (subgoals ++ result.others).toList ++ gs
/-- The `cases'` tactic is similar to the `cases` tactic in Lean 4 core, but the syntax for giving
```
and then examining [the output](https://github.com/leanprover-community/mathlib4/actions/runs/14085064444/job/39446843657). |
tech debt |
168/119 |
Mathlib/Probability/Kernel/Defs.lean,Mathlib/Probability/Moments/Basic.lean,Mathlib/RingTheory/EssentialFiniteness.lean,Mathlib/RingTheory/FiniteType.lean,Mathlib/RingTheory/Flat/Equalizer.lean,Mathlib/RingTheory/IsTensorProduct.lean,Mathlib/RingTheory/Kaehler/JacobiZariski.lean,Mathlib/RingTheory/Kaehler/Polynomial.lean,Mathlib/RingTheory/Multiplicity.lean,Mathlib/RingTheory/Nakayama.lean,Mathlib/RingTheory/Polynomial/Ideal.lean,Mathlib/RingTheory/PowerSeries/Order.lean,Mathlib/RingTheory/Presentation.lean,Mathlib/RingTheory/Smooth/StandardSmooth.lean,Mathlib/RingTheory/TensorProduct/MvPolynomial.lean,Mathlib/RingTheory/Unramified/Finite.lean,Mathlib/SetTheory/Lists.lean,Mathlib/SetTheory/Ordinal/FixedPoint.lean,Mathlib/SetTheory/Ordinal/Notation.lean,Mathlib/SetTheory/Ordinal/Principal.lean,Mathlib/SetTheory/PGame/Algebra.lean,Mathlib/SetTheory/PGame/Order.lean |
22 |
12 |
['Parcly-Taxel', 'apnelson1', 'eric-wieser', 'github-actions'] |
nobody |
7-46858 7 days ago |
14-70996 14 days ago |
22-70372 22 days |
| 23961 |
FR-vdash-bot author:FR-vdash-bot |
refactor: unbundle algebra from `ENormed*` |
Further speed up the search in the algebraic typeclass hierarchy by avoiding searching for `TopologicalSpace`.
---
[](https://gitpod.io/from-referrer/)
|
slow-typeclass-synthesis
maintainer-merge
t-algebra
t-analysis
label:t-algebra$ |
32/25 |
Mathlib/Analysis/CStarAlgebra/CStarMatrix.lean,Mathlib/Analysis/Normed/Group/Basic.lean,Mathlib/Analysis/Normed/Group/Continuity.lean,Mathlib/Analysis/NormedSpace/IndicatorFunction.lean,Mathlib/MeasureTheory/Function/LpSeminorm/Basic.lean |
5 |
8 |
['FR-vdash-bot', 'github-actions', 'grunweg', 'leanprover-bot'] |
nobody |
7-16866 7 days ago |
7-16867 7 days ago |
7-61112 7 days |
| 23137 |
grunweg author:grunweg |
chore(Topology): some more fun_prop tagging |
---
[](https://gitpod.io/from-referrer/)
|
t-topology |
8/4 |
Mathlib/Dynamics/Flow.lean,Mathlib/Topology/Algebra/Monoid.lean |
2 |
8 |
['github-actions', 'grunweg', 'j-loreaux'] |
nobody |
7-10587 7 days ago |
7-10587 7 days ago |
14-1662 14 days |
| 21276 |
GabinKolly author:GabinKolly |
feat(ModelTheory/Substructures): define equivalences between equal substructures |
Define first-order equivalences between equal substructures, and prove related properties.
---
This is some preparatory work for #18876
[](https://gitpod.io/from-referrer/)
|
t-logic |
62/0 |
Mathlib/ModelTheory/Substructures.lean |
1 |
12 |
['GabinKolly', 'YaelDillies', 'fpvandoorn', 'github-actions'] |
nobody |
6-72960 6 days ago |
6-72960 6 days ago |
26-41785 26 days |
| 23329 |
ScottCarnahan author:ScottCarnahan |
feat (LinearAlgebra/RootSystem): nondegeneracy for subrings |
This PR adds generalized versions of existing results, where the original base ring is no longer necessarily linearly ordered, but is an algebra over a LinearOrderedCommRing.
---
[](https://gitpod.io/from-referrer/)
|
t-algebra label:t-algebra$ |
657/289 |
Mathlib.lean,Mathlib/Algebra/Module/Submodule/LinearMap.lean,Mathlib/LinearAlgebra/BilinearMap.lean,Mathlib/LinearAlgebra/PerfectPairing/Restrict.lean,Mathlib/LinearAlgebra/RootSystem/Base.lean,Mathlib/LinearAlgebra/RootSystem/BaseChange.lean,Mathlib/LinearAlgebra/RootSystem/Defs.lean,Mathlib/LinearAlgebra/RootSystem/Finite/CanonicalBilinear.lean,Mathlib/LinearAlgebra/RootSystem/Finite/Lemmas.lean,Mathlib/LinearAlgebra/RootSystem/Finite/Nondegenerate.lean,Mathlib/LinearAlgebra/RootSystem/Irreducible.lean,Mathlib/LinearAlgebra/RootSystem/IsValuedIn.lean,Mathlib/LinearAlgebra/RootSystem/Reduced.lean,Mathlib/LinearAlgebra/RootSystem/RootPositive.lean |
14 |
9 |
['ScottCarnahan', 'github-actions', 'leanprover-community-bot-assistant', 'ocfnash'] |
nobody |
6-59599 6 days ago |
6-62563 6 days ago |
11-80358 11 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$ |
44/0 |
Mathlib/RepresentationTheory/Tannaka.lean |
1 |
15 |
['github-actions', 'kbuzzard', 'ybenmeur'] |
nobody |
6-29716 6 days ago |
31-68484 1 month ago |
31-68533 31 days |
| 23969 |
grunweg author:grunweg |
feat: add LinearEquiv.ofInjectiveOfFinrankEq |
This is used in #22611.
---
[](https://gitpod.io/from-referrer/)
|
t-algebra label:t-algebra$ |
20/0 |
Mathlib/LinearAlgebra/FiniteDimensional/Basic.lean |
1 |
7 |
['eric-wieser', 'github-actions', 'grunweg'] |
nobody |
6-20867 6 days ago |
7-8108 7 days ago |
7-8165 7 days |
| 23981 |
robertmaxton42 author:robertmaxton42 |
feat (Equiv) : sigmas indexed by products are sigmas; pinning down the base of a sigma gives the fiber |
Add some convenience defs for working with sigma types that appear frequently when working with hom-like objects:
- `Equiv.sigmaAssocProd`, for sigmas of the form `(a : α) × (b : β) × γ a b`
- `Equiv.sigmaSubtype` and `Equiv.sigmaSigmaSubtype`, for subtypes of sigmas that "cancel"
Also add a convenience lemma for moving conjugations ( $\varepsilon\^{-1} f \varepsilon$ ) from one side of an equation of functions to the other.
---
[](https://gitpod.io/from-referrer/)
|
new-contributor
t-logic
|
49/0 |
Mathlib/Logic/Equiv/Basic.lean,Mathlib/Logic/Equiv/Sum.lean |
2 |
1 |
['github-actions'] |
nobody |
6-18670 6 days ago |
6-43381 6 days ago |
6-43438 6 days |
| 23990 |
robertmaxton42 author:robertmaxton42 |
feat (Types.Colimits): Quot is functorial and colimitEquivQuot is natural |
Add `Functor.quotFunctor` to parallel `Functor.sectionsFunctor`, witnessing that `Quot` is functorial; add `colimNatIsoQuotFunctor` to parallel `limNatIsoSectionsFunctor`, witnessing that `colimitEquivQuot` is natural in the diagram $F$.
---
[](https://gitpod.io/from-referrer/)
|
new-contributor
t-category-theory
|
33/0 |
Mathlib/CategoryTheory/Limits/Types/Colimits.lean |
1 |
3 |
['github-actions', 'joelriou', 'robertmaxton42'] |
nobody |
6-14195 6 days ago |
6-17943 6 days ago |
6-17998 6 days |
| 23552 |
AntoineChambert-Loir author:AntoineChambert-Loir |
feat(RingTheory/PowerSeries/Substitution): define substitution of power series in power series |
This is the second part of the PR defining substitution of indeterminates by power series in power series.
This one is specific to univariate power series. Basically, the matter is just to remove `Unit ->` in definitions
and make the necessary adjustments.
---
- [x] depends on: #15158
- [x] depends on: #23607 (minor chore)
- [x] depends on: #23642
[](https://gitpod.io/from-referrer/)
|
t-algebra label:t-algebra$ |
327/18 |
Mathlib.lean,Mathlib/RingTheory/MvPowerSeries/Substitution.lean,Mathlib/RingTheory/PowerSeries/Evaluation.lean,Mathlib/RingTheory/PowerSeries/Substitution.lean |
4 |
n/a |
['AntoineChambert-Loir', 'b-mehta', 'github-actions', 'mathlib4-dependent-issues-bot', 'riccardobrasca'] |
riccardobrasca assignee:riccardobrasca |
6-7557 6 days ago |
unknown |
unknown |
| 23904 |
YaelDillies author:YaelDillies |
feat: a finitely generated submonoid has a minimal generating set |
From Toric
---
[](https://gitpod.io/from-referrer/)
|
toric
large-import
t-algebra
label:t-algebra$ |
27/0 |
Mathlib/Data/Finset/Powerset.lean,Mathlib/GroupTheory/Finiteness.lean |
2 |
1 |
['github-actions'] |
nobody |
6-3096 6 days ago |
9-18823 9 days ago |
9-18863 9 days |
| 23539 |
alreadydone author:alreadydone |
feat(Algebra): transcendence degree is well-defined |
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 a spanning 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.
---
- [x] depends on: #20887
[](https://gitpod.io/from-referrer/)
|
t-algebra label:t-algebra$ |
408/28 |
Mathlib/FieldTheory/IsAlgClosed/Classification.lean,Mathlib/FieldTheory/SeparableDegree.lean,Mathlib/RingTheory/AlgebraicIndependent/RankAndCardinality.lean,Mathlib/RingTheory/AlgebraicIndependent/TranscendenceBasis.lean |
4 |
5 |
['alreadydone', 'erdOne', 'github-actions', 'mathlib4-dependent-issues-bot'] |
nobody |
5-74524 5 days ago |
12-61906 12 days ago |
12-62803 12 days |
| 18379 |
oeb25 author:oeb25 |
feat(Topology/ENNReal): Add `ENNReal.tsum_biUnion` |
This adds infinite versions of `Finset.sum_biUnion` to `ENNReal`s.
---
One notable difference from the `Finset` version is that for `tsum` we have two ways for selecting the summands: `∑' x : ⋃ i ∈ S` or `∑' x : ⋃ i, t i`. This PR adds both.
I tried to extend this beyond `ENNReal`, but didn't find a clean way to do it.
[](https://gitpod.io/from-referrer/)
|
new-contributor
t-topology
|
26/0 |
Mathlib/Topology/Instances/ENNReal/Lemmas.lean |
1 |
5 |
['github-actions', 'grunweg', 'j-loreaux', 'oeb25'] |
nobody |
5-69839 5 days ago |
5-79787 5 days ago |
82-14467 82 days |
| 22243 |
luigi-massacci author:luigi-massacci |
feat(Topology/MetricSpace/Gluing): Inductive limits of separable spaces are separable |
---
[](https://gitpod.io/from-referrer/)
|
new-contributor
t-topology
|
23/0 |
Mathlib/Topology/MetricSpace/Gluing.lean |
1 |
9 |
['Paul-Lez', 'github-actions', 'j-loreaux', 'luigi-massacci', 'mathlib-bors'] |
nobody |
5-69663 5 days ago |
11-75923 11 days ago |
2-23272 2 days |
| 24008 |
meithecatte author:meithecatte |
chore(EpsilonNFA): replace manual lemmas with @[simps] |
---
[](https://gitpod.io/from-referrer/)
|
t-computability
new-contributor
|
2/24 |
Mathlib/Computability/EpsilonNFA.lean |
1 |
1 |
['github-actions'] |
nobody |
5-62314 5 days ago |
5-63861 5 days ago |
5-63918 5 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$ |
51/46 |
Mathlib/Algebra/AddConstMap/Basic.lean,Mathlib/Algebra/Algebra/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 |
18 |
9 |
['github-actions', 'grunweg', 'leanprover-bot', 'leanprover-community-bot-assistant', 'urkud', 'vlad902'] |
nobody |
5-60947 5 days ago |
5-60973 5 days ago |
16-10877 16 days |
| 23991 |
grunweg author:grunweg |
feat(pr_summary.yml): mentioned moved files without module deprecation in the summary comment |
If a PR's diff contains files which were moved or deleted that are not module deprecations, mention these in the PR's summary comment (as an indication to reviewers).
Also add or remove a `file-removed` label if such moves without deprecations are present in the diff.
---
Tested with no, one and two files removed without deprecations: the summary comment behaved as expected.
TODOs: the label managing step fails
TODO: tweak the grep syntax, to search for `deprecated_module ` (with a space)
[](https://gitpod.io/from-referrer/)
|
CI |
44/2 |
.github/workflows/PR_summary.yml |
1 |
7 |
['adomani', 'github-actions', 'grunweg', 'leanprover-community-bot-assistant'] |
nobody |
5-56117 5 days ago |
5-56152 5 days ago |
5-56139 5 days |
| 23439 |
YaelDillies author:YaelDillies |
chore(SimpleGraph/Prod): correct lemma names |
The head function should come first in the name even if dot notation is used.
---
In the future, we might want to rename `boxProd_adj` to `adj_boxProd`:
1. If we apply the basic algorithm from Std (https://github.com/leanprover/lean4/blob/master/doc/std/naming.md#naming-algorithm-for-theorems-and-some-definitions), we encounter `Adj` first, so we write it first.
2. The mathlib-specific algorithm says that most predicates should be prefixed: https://leanprover-community.github.io/contribute/naming.html#predicates-as-suffixes
3. Dot notation isn't an infix operator, although we can of course decide on a case by case basis that a specific function we are dot notating on is actually an infix.
[](https://gitpod.io/from-referrer/)
|
t-combinatorics |
18/7 |
Mathlib/Combinatorics/SimpleGraph/Prod.lean |
1 |
15 |
['YaelDillies', 'b-mehta', 'eric-wieser', 'github-actions'] |
nobody |
5-56025 5 days ago |
6-21732 6 days ago |
18-29919 18 days |
| 23920 |
YaelDillies author:YaelDillies |
feat: entourage-separated sets |
Define a notion of separation of a set relative to an entourage. This will be used to unify metric and dynamical separation.
From MiscYD and LeanAPAP
---
[](https://gitpod.io/from-referrer/)
|
t-topology |
61/0 |
Mathlib.lean,Mathlib/Topology/UniformSpace/Separated.lean |
2 |
13 |
['D-Thomine', 'YaelDillies', 'b-mehta', 'github-actions'] |
nobody |
5-52363 5 days ago |
5-52363 5 days ago |
5-61319 5 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 |
17 |
['Paul-Lez', 'github-actions', 'grunweg', 'peabrainiac', 'vlad902'] |
nobody |
5-48739 5 days ago |
43-6338 1 month ago |
43-6333 43 days |
| 22450 |
joelriou author:joelriou |
feat(CategoryTheory): left derivability structures |
Using the duality result from #22447, we dualise the notion of right derivability structure introduced in #12633 in order to formalize left derivability structures. This shall be used in order to construct left derived functors.
---
- [x] depends on: #22447
[](https://gitpod.io/from-referrer/)
|
t-category-theory |
66/2 |
Mathlib/CategoryTheory/GuitartExact/Opposite.lean,Mathlib/CategoryTheory/Localization/DerivabilityStructure/Basic.lean,Mathlib/CategoryTheory/Localization/Resolution.lean |
3 |
3 |
['github-actions', 'leanprover-community-bot-assistant', 'mathlib4-dependent-issues-bot'] |
nobody |
5-20784 5 days ago |
5-21374 5 days ago |
5-23647 5 days |
| 24003 |
eric-wieser author:eric-wieser |
refactor: mixin class for `norm_smul` with strict equality |
Define a typeclass for normed modules where the norm is exactly multiplicative (not just sub-multiplicative).
This is a subset of #23787, leaving out the change to `NormedSpace`.
---
[](https://gitpod.io/from-referrer/)
|
|
89/44 |
Mathlib/Analysis/Asymptotics/Lemmas.lean,Mathlib/Analysis/LocallyConvex/Basic.lean,Mathlib/Analysis/Normed/Affine/AddTorsor.lean,Mathlib/Analysis/Normed/Module/Basic.lean,Mathlib/Analysis/Normed/Module/Span.lean,Mathlib/Analysis/Normed/MulAction.lean,Mathlib/Analysis/NormedSpace/Pointwise.lean,Mathlib/Dynamics/BirkhoffSum/NormedSpace.lean,Mathlib/MeasureTheory/Function/LpSeminorm/Basic.lean,Mathlib/Topology/ContinuousMap/Compact.lean,Mathlib/Topology/MetricSpace/Holder.lean,Mathlib/Topology/MetricSpace/HolderNorm.lean,docs/overview.yaml,docs/undergrad.yaml |
14 |
6 |
['eric-wieser', 'github-actions', 'kbuzzard', 'leanprover-bot', 'loefflerd'] |
nobody |
5-19953 5 days ago |
5-20038 5 days ago |
5-80124 5 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 |
7 |
['Ruben-VandeVelde', 'github-actions', 'kim-em', 'leanprover-bot', 'plp127', 'vlad902'] |
nobody |
5-19432 5 days ago |
31-57320 1 month ago |
31-57366 31 days |
| 23933 |
alreadydone author:alreadydone |
chore(LinearAlgebra/Dual): generalize to semirings |
---
[](https://gitpod.io/from-referrer/)
|
t-algebra label:t-algebra$ |
102/100 |
Archive/Sensitivity.lean,Mathlib/Data/Finsupp/Basic.lean,Mathlib/LinearAlgebra/Dual/Basis.lean,Mathlib/LinearAlgebra/Dual/Defs.lean,Mathlib/LinearAlgebra/Dual/Lemmas.lean,Mathlib/LinearAlgebra/Finsupp/Defs.lean,Mathlib/LinearAlgebra/InvariantBasisNumber.lean |
7 |
14 |
['alreadydone', 'eric-wieser', 'github-actions'] |
nobody |
5-11291 5 days ago |
8-39325 8 days ago |
8-39531 8 days |
| 23826 |
javra author:javra |
feat(CategoryTheory): linear categories as `ModuleCat R`-enriched categories |
---
[](https://gitpod.io/from-referrer/)
|
large-import
t-category-theory
|
195/0 |
Mathlib.lean,Mathlib/Algebra/Category/ModuleCat/Monoidal/Basic.lean,Mathlib/CategoryTheory/Enriched/Linear.lean,Mathlib/CategoryTheory/Linear/Basic.lean,Mathlib/CategoryTheory/Monoidal/Linear.lean |
5 |
2 |
['github-actions', 'leanprover-community-bot-assistant'] |
nobody |
5-11208 5 days ago |
5-11219 5 days ago |
5-11206 5 days |
| 23584 |
mariainesdff author:mariainesdff |
chore(RingTheory/Valuation/Extension): rename IsValExtension to Valuation.IsExtension |
This change is to remove `IsValExtension` from the root namespace and to allow dot notation.
---
[](https://gitpod.io/from-referrer/)
|
t-algebra label:t-algebra$ |
21/15 |
Mathlib.lean,Mathlib/RingTheory/Valuation/Extension.lean |
2 |
4 |
['erdOne', 'github-actions', 'leanprover-community-bot-assistant', 'mariainesdff'] |
nobody |
5-1158 5 days ago |
5-1178 5 days ago |
13-63112 13 days |
| 24041 |
YuvalFilmus author:YuvalFilmus |
feat: add support for bigop binders of the form "not in" and "not equal" |
feat: add support for bigop binders of the form "not in" and "not equal"
Added two new binders which can be used with big operators (product and summation).
The first, "not in", translates into "in ... complement".
The second, "not equal to", translates to `univ.erase ...`.
Also, improved documentation in the file header.
Delaboration updates can be considered next if wanted (to be coordinated with #22048).
---
[](https://gitpod.io/from-referrer/)
|
new-contributor
t-algebra
label:t-algebra$ |
7/0 |
Mathlib/Algebra/BigOperators/Group/Finset/Defs.lean |
1 |
1 |
['github-actions'] |
nobody |
4-79369 4 days ago |
4-80670 4 days ago |
4-80729 4 days |
| 23725 |
faenuccio author:faenuccio |
feat(Order/Group/Cyclic): provide basic properties of cyclic linearly ordered commutative groups |
Co-authored with @mariainesdff |
t-order
t-algebra
label:t-algebra$ |
67/0 |
Mathlib.lean,Mathlib/Algebra/Order/Group/Cyclic.lean |
2 |
16 |
['Ruben-VandeVelde', 'erdOne', 'faenuccio', 'github-actions', 'kbuzzard'] |
nobody |
4-77370 4 days ago |
4-78600 4 days ago |
9-17683 9 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 |
17 |
['eric-wieser', 'github-actions', 'grunweg', 'leanprover-bot', 'leanprover-community-bot-assistant', 'leanprover-community-mathlib4-bot', 'plp127'] |
nobody |
4-66208 4 days ago |
4-69549 4 days ago |
28-59004 28 days |
| 23929 |
meithecatte author:meithecatte |
feat(Computability/NFA): improve bound on pumping lemma |
---
[](https://gitpod.io/from-referrer/)
|
t-computability
new-contributor
|
203/20 |
Mathlib/Computability/EpsilonNFA.lean,Mathlib/Computability/NFA.lean |
2 |
1 |
['github-actions'] |
nobody |
4-56552 4 days ago |
8-45662 8 days ago |
8-45718 8 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
|
127/63 |
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 |
29 |
['github-actions', 'grunweg', 'j-loreaux', 'leanprover-bot', 'leanprover-community-mathlib4-bot', 'plp127', 'urkud'] |
nobody |
4-52193 4 days ago |
45-50369 1 month ago |
52-49964 52 days |
| 24053 |
plp127 author:plp127 |
feat(Topology): Priestley spaces are totally separated |
This generalizes `PriestleySpace.toT2Space`
---
[](https://gitpod.io/from-referrer/)
|
t-topology |
9/5 |
Mathlib/Topology/Order/Priestley.lean |
1 |
3 |
['github-actions', 'plp127', 'urkud'] |
nobody |
4-51821 4 days ago |
4-55633 4 days ago |
4-55620 4 days |
| 24045 |
vlad902 author:vlad902 |
chore(scripts/install_macos): Fix 2 PATH resolution issues |
A fresh local install fails with this script due to PATH resolution issues in two places.
---
[](https://gitpod.io/from-referrer/)
|
|
6/0 |
scripts/install_macos.sh |
1 |
2 |
['eric-wieser', 'github-actions'] |
nobody |
4-34886 4 days ago |
4-69409 4 days ago |
4-69396 4 days |
| 24066 |
urkud author:urkud |
refactor(Path): turn `Path.extend` into a `ContinuousMap` |
---
[](https://gitpod.io/from-referrer/)
|
t-topology |
44/47 |
Mathlib/AlgebraicTopology/FundamentalGroupoid/Basic.lean,Mathlib/Topology/Path.lean |
2 |
1 |
['github-actions'] |
nobody |
4-24983 4 days ago |
4-24984 4 days ago |
4-25044 4 days |
| 24065 |
kim-em author:kim-em |
chore: script to give topological sort of modules |
This script is not useful by itself: it just gives a topological sort of Mathlib's import graph. But I've several times found it useful when I want to modify many files systematically with minimal rebuilding: just work backwards through the list.
|
|
96/0 |
scripts/README.md,scripts/topological_sort.py |
2 |
4 |
['github-actions', 'jcommelin', 'kim-em'] |
nobody |
4-20750 4 days ago |
4-31788 4 days ago |
4-31775 4 days |
| 24069 |
jcommelin author:jcommelin |
doc(Topology/CWComplex): cross-reference abstract and classical approaches |
* Add implementation notes to both Abstract/Basic.lean and Classical/Basic.lean
explaining the relationship between the two approaches to CW complexes
* Add TODO noting the missing connection between the approaches
* Clarify that Abstract/Basic.lean uses a categorical approach while
Classical/Basic.lean uses Whitehead's classical approach
---
[](https://gitpod.io/from-referrer/)
|
maintainer-merge
t-topology
|
23/2 |
Mathlib/Topology/CWComplex/Abstract/Basic.lean,Mathlib/Topology/CWComplex/Classical/Basic.lean |
2 |
3 |
['github-actions', 'grunweg'] |
nobody |
4-14056 4 days ago |
4-14057 4 days ago |
4-19030 4 days |
| 23997 |
YaelDillies author:YaelDillies |
feat: `ι →₀ R` is a finite `R`-module iff `ι` is finite |
---
[](https://gitpod.io/from-referrer/)
|
t-algebra label:t-algebra$ |
81/42 |
Mathlib/Data/Finsupp/Single.lean,Mathlib/Data/Matrix/Rank.lean,Mathlib/LinearAlgebra/Basis/Cardinality.lean,Mathlib/LinearAlgebra/Dimension/Finite.lean,Mathlib/LinearAlgebra/Dimension/FreeAndStrongRankCondition.lean,Mathlib/LinearAlgebra/Dimension/StrongRankCondition.lean,Mathlib/LinearAlgebra/Finsupp/Supported.lean,Mathlib/LinearAlgebra/Finsupp/VectorSpace.lean,Mathlib/LinearAlgebra/StdBasis.lean,Mathlib/RingTheory/Finiteness/Cardinality.lean |
10 |
17 |
['YaelDillies', 'alreadydone', 'eric-wieser', 'github-actions'] |
nobody |
4-10880 4 days ago |
6-4329 6 days ago |
6-4391 6 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 |
4-3563 4 days ago |
43-51965 1 month ago |
43-52009 43 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$ |
443/42 |
Mathlib/Algebra/SkewMonoidAlgebra/Basic.lean |
1 |
38 |
['AntoineChambert-Loir', 'Louddy', 'github-actions', 'kbuzzard'] |
nobody |
4-2609 4 days ago |
10-76276 10 days ago |
47-39992 47 days |
| 23547 |
chrisflav author:chrisflav |
feat(AlgebraicGeometry): codescent implies descent |
Let `P` and `P'` be morphism properties of schemes. We show some results to deduce
that `P` descends along `P'` from a codescent property of ring homomorphisms.
---
[](https://gitpod.io/from-referrer/)
|
t-algebraic-geometry |
260/1 |
Mathlib.lean,Mathlib/AlgebraicGeometry/Morphisms/AffineAnd.lean,Mathlib/AlgebraicGeometry/Morphisms/Descent.lean,Mathlib/RingTheory/RingHomProperties.lean |
4 |
12 |
['chrisflav', 'erdOne', 'github-actions'] |
nobody |
3-85401 3 days ago |
17-82656 17 days ago |
17-82642 17 days |
| 23722 |
YaelDillies author:YaelDillies |
feat(Bialgebra/MonoidAlgebra): `mapDomain` as a `BialgHom` |
From Toric
Co-authored-by: Michał Mrugała
---
[](https://gitpod.io/from-referrer/)
|
toric
maintainer-merge
t-algebra
label:t-algebra$ |
64/16 |
Mathlib/RingTheory/Bialgebra/Hom.lean,Mathlib/RingTheory/Bialgebra/MonoidAlgebra.lean |
2 |
9 |
['YaelDillies', 'erdOne', 'eric-wieser', 'github-actions'] |
nobody |
3-78457 3 days ago |
4-10961 4 days ago |
13-11289 13 days |
| 23964 |
BoltonBailey author:BoltonBailey |
docs: Add documentation arbitrarily |
@mattrobball asked in the Mathlib Community meeting today what it would look like if we asked Claude code to give us improved documentation. I made this draft PR by selecting five declarations arbitrarily from `nolints.json` and asking Cursor to document them.
---
[](https://gitpod.io/from-referrer/)
|
documentation |
49/1 |
Mathlib/Algebra/Homology/Homotopy.lean,Mathlib/Analysis/BoxIntegral/Partition/Filter.lean,Mathlib/Control/Monad/Cont.lean,Mathlib/Data/Stream/Defs.lean,Mathlib/LinearAlgebra/AffineSpace/AffineMap.lean |
5 |
8 |
['ADedecker', 'BoltonBailey', 'eric-wieser', 'github-actions', 'jcommelin', 'mattrobball'] |
nobody |
3-73725 3 days ago |
6-61065 6 days ago |
7-37687 7 days |
| 21026 |
joelriou author:joelriou |
feat(CategoryTheory/Limits): certain multicoequalizers are pushouts |
In this file, we show that a multicoequalizer for for `I : MultispanIndex (.ofLinearOrder ι) C` is also a pushout when `ι` has exactly two elements.
---
- [x] depends on: #22203
- [x] depends on: #20988
[](https://gitpod.io/from-referrer/)
|
t-category-theory |
95/0 |
Mathlib.lean,Mathlib/CategoryTheory/Limits/Shapes/MultiequalizerPullback.lean |
2 |
2 |
['github-actions', 'mathlib4-dependent-issues-bot'] |
nobody |
3-70003 3 days ago |
3-70010 3 days ago |
16-74630 16 days |
| 24082 |
AntoineChambert-Loir author:AntoineChambert-Loir |
feat(Algebra/Group/End) : add MulAut.inv_apply and some simp lemmas |
---
[](https://gitpod.io/from-referrer/)
|
t-algebra label:t-algebra$ |
23/5 |
Mathlib/Algebra/Group/End.lean,Mathlib/GroupTheory/GroupAction/ConjAct.lean |
2 |
6 |
['AntoineChambert-Loir', 'eric-wieser', 'github-actions'] |
nobody |
3-68092 3 days ago |
3-83464 3 days ago |
3-83524 3 days |
| 23339 |
joelriou author:joelriou |
feat(CategoryTheory): the colimit type of a functor to types |
Given a category `J` (with `J : Type u` and `[Category.{v} J]`) and a functor `F : J ⥤ Type w`, we introduce a type `F.ColimitType : Type (max u w)`, which satisfies a certain universal property of the colimit: it is defined as a suitable quotient of `Σ j, F.obj j`. This universal property is not expressed in a categorical way (as in general `Type (max u w)` is not the same as `Type u`).
(This type `F.ColimitType` is basically the same as `CategoryTheory.Limits.Types.Quot` that is defined in `CategoryTheory.Limits.Types`, but we expand the API (with minimal imports to category theory) so that it may be used in future PRs to refactor both `DirectedSystem` and the construction of colimits in `Type`.)
---
[](https://gitpod.io/from-referrer/)
|
t-category-theory |
272/0 |
Mathlib.lean,Mathlib/CategoryTheory/Limits/Types/ColimitType.lean |
2 |
3 |
['AntoineChambert-Loir', 'github-actions', 'joelriou'] |
nobody |
3-67107 3 days ago |
16-71634 16 days ago |
23-54774 23 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
---
- [ ] depends on: #24071
[](https://gitpod.io/from-referrer/)
|
t-algebra label:t-algebra$ |
158/4 |
Mathlib.lean,Mathlib/RingTheory/FilteredAlgebra/AssociatedGraded.lean,Mathlib/RingTheory/FilteredAlgebra/Basic.lean |
3 |
16 |
['AntoineChambert-Loir', 'Thmoas-Guan', 'eric-wieser', 'github-actions', 'kbuzzard', 'mathlib4-dependent-issues-bot'] |
nobody |
3-65561 3 days ago |
3-65564 3 days ago |
43-59176 43 days |
| 24023 |
robin-carlier author:robin-carlier |
feat(Data/List/Sort): ext lemma for strictly sorted lists |
Add a theorem stating that two strictly sorted lists are equal if they have the same set of elements.
---
Suggested by @joelriou in #21744.
[](https://gitpod.io/from-referrer/)
|
t-data |
5/1 |
Mathlib/Data/List/Sort.lean |
1 |
8 |
['b-mehta', 'github-actions', 'joelriou', 'robin-carlier'] |
nobody |
3-60209 3 days ago |
5-10580 5 days ago |
5-16269 5 days |
| 23857 |
urkud author:urkud |
chore(Group/Pointwise/Interval): generalize some lemmas |
.. from a linear ordered field to a linear ordered semifield or a group with zero.
---
- [ ] depends on: #23901
- [ ] depends on: #23922
[](https://gitpod.io/from-referrer/)
|
t-algebra label:t-algebra$ |
192/146 |
Mathlib/Algebra/Order/Group/Pointwise/Interval.lean |
1 |
5 |
['eric-wieser', 'github-actions', 'leanprover-community-bot-assistant', 'mathlib4-dependent-issues-bot', 'urkud'] |
nobody |
3-57701 3 days ago |
7-77310 7 days ago |
8-26435 8 days |
| 23643 |
AntoineChambert-Loir author:AntoineChambert-Loir |
chore(RingTheory/MvPowerSeries/PiTopology): limit of truncation of power series |
Extract a lemma that says that for a multivariate power series, `trunc' R d f` converges to `f` when `d` converges to infinity.
Prove the analogous lemma for `MvPowerSeries.trunc` (if the set of indeterminates is nonempty).
Move this lemma and the denseness of polynomials to the `PiTopology` file.
---
[](https://gitpod.io/from-referrer/)
|
t-algebra label:t-algebra$ |
44/13 |
Mathlib/RingTheory/MvPowerSeries/Evaluation.lean,Mathlib/RingTheory/MvPowerSeries/PiTopology.lean,Mathlib/RingTheory/PowerSeries/PiTopology.lean |
3 |
17 |
['AntoineChambert-Loir', 'b-mehta', 'github-actions', 'leanprover-community-bot-assistant', 'pechersky'] |
nobody |
3-57648 3 days ago |
4-1898 4 days ago |
15-55223 15 days |
| 23951 |
apnelson1 author:apnelson1 |
feat(Matroid/Rank): more rank API |
We add some more API for matroid rank and its interactions with monotonicity, duality, finiteness and submodularity.
---
[](https://gitpod.io/from-referrer/)
|
t-data |
186/55 |
Mathlib/Data/Matroid/Rank/ENat.lean,Mathlib/Data/Matroid/Rank/Finite.lean,scripts/noshake.json |
3 |
15 |
['apnelson1', 'b-mehta', 'github-actions'] |
b-mehta assignee:b-mehta |
3-53796 3 days ago |
3-53796 3 days ago |
7-64347 7 days |
| 24098 |
plp127 author:plp127 |
feat(Topology): R1 separation |
Adds a new lemma `r1_separation`.
---
[](https://gitpod.io/from-referrer/)
|
t-topology
easy
|
7/0 |
Mathlib/Topology/Separation/Basic.lean |
1 |
1 |
['github-actions'] |
nobody |
3-46742 3 days ago |
3-47024 3 days ago |
3-47011 3 days |
| 24042 |
eric-wieser author:eric-wieser |
feat: add `ULiftable.up'` and `ULiftable.down'` |
These are handy when working with `m PUnit`
---
[](https://gitpod.io/from-referrer/)
|
t-data
t-meta
|
10/0 |
Mathlib/Control/ULiftable.lean |
1 |
1 |
['github-actions'] |
nobody |
3-42147 3 days ago |
4-77936 4 days ago |
4-79395 4 days |
| 24094 |
FR-vdash-bot author:FR-vdash-bot |
chore: remove `CanonicallyOrdered{Mul, Add}.toOrderBot` |
This will allow us to use `CanonicallyOrdered{Mul, Add}` with order typeclasses that extend `Bot`.
Co-authored-by: Peter Nelson <71660771+apnelson1@users.noreply.github.com>
---
[](https://gitpod.io/from-referrer/)
[Zulip](https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/bot_eq_zero.20in.20complete.20lattice/with/512387701)
|
t-order
t-algebra
label:t-algebra$ |
51/29 |
Mathlib/Algebra/Order/Antidiag/Prod.lean,Mathlib/Algebra/Order/Group/Finset.lean,Mathlib/Algebra/Order/Monoid/Canonical/Basic.lean,Mathlib/Algebra/Order/Monoid/Canonical/Defs.lean,Mathlib/Algebra/Order/Ring/Finset.lean,Mathlib/Algebra/Order/Ring/Nat.lean,Mathlib/Algebra/Order/Ring/WithTop.lean,Mathlib/Algebra/Order/SuccPred.lean,Mathlib/Data/DFinsupp/Interval.lean,Mathlib/Data/DFinsupp/Order.lean,Mathlib/Data/Finsupp/Interval.lean,Mathlib/Data/Finsupp/Order.lean,Mathlib/Data/NNReal/Defs.lean,Mathlib/Data/Nat/WithBot.lean,Mathlib/RingTheory/MvPolynomial/WeightedHomogeneous.lean,Mathlib/SetTheory/Cardinal/Order.lean |
16 |
8 |
['FR-vdash-bot', 'eric-wieser', 'github-actions', 'leanprover-bot'] |
nobody |
3-41440 3 days ago |
3-41440 3 days ago |
3-61129 3 days |
| 23936 |
Parcly-Taxel author:Parcly-Taxel |
chore: deprecate stub files left over from #20676 |
As I noted [on Zulip](https://leanprover.zulipchat.com/#narrow/channel/144837-PR-reviews/topic/.2320676.20unbundling.20ordered.20algebra/near/511192094):
* `Mathlib/Algebra/Order/Field/InjSurj.lean` (deprecated stuff only)
* `Mathlib/Algebra/Order/Group/InjSurj.lean` (ditto)
* `Mathlib/Algebra/Order/Group/Instances.lean` (no declarations)
* `Mathlib/Algebra/Order/Group/Prod.lean` (ditto)
* `Mathlib/Algebra/Order/Group/TypeTags.lean` (ditto) |
t-algebra label:t-algebra$ |
22/42 |
Mathlib/Algebra/Order/Field/InjSurj.lean,Mathlib/Algebra/Order/Group/InjSurj.lean,Mathlib/Algebra/Order/Group/Instances.lean,Mathlib/Algebra/Order/Group/Prod.lean,Mathlib/Algebra/Order/Group/TypeTags.lean,Mathlib/Algebra/Order/Monoid/Basic.lean,Mathlib/Algebra/Order/Ring/InjSurj.lean |
7 |
3 |
['Parcly-Taxel', 'github-actions', 'grunweg'] |
nobody |
3-39751 3 days ago |
3-43087 3 days ago |
8-24670 8 days |
| 23767 |
grunweg author:grunweg |
refactor: make library notes a definition |
Make library notes a definition of `Unit` type, whose doc-string is the note's content. As a consequence,
- doc-gen will display all library notes without any custom logic,
- library notes are shown upon hover (via the use of the doc-string),
- go do definition for library notes is easy
Automate this using a macro, which also enforces that all library notes are inside the Mathlib.LibraryNote namespace.
*Temporarily*, we use the `library_note2` name; if/when the batteries version is changed, we can reclaim the original name.
This PR does not address how to *refer* to library notes nicely (in a way that is shown in the documentation, checked for typos, with sufficient imports ensured etc.). That is left to a future PR.
This is proposal 2a from this [zulip discussion]([#mathlib4 > library notes @ 💬](https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/library.20notes/near/510614740))
------------
Open questions/TODOs:
- should this go in batteries instead? can the old definition just be overwritten?
- otherwise, what's the best place for the `LibraryNote` definition? A single file just for this feels overkill; I put it in Mathlib.Tactic.Basic for now. I could use Mathlib.Init, of course (but that might be excessive)
---
[](https://gitpod.io/from-referrer/)
|
large-import
t-meta
|
48/48 |
Archive/Imo/Imo2019Q2.lean,Mathlib/Algebra/BigOperators/Group/Finset/Defs.lean,Mathlib/Algebra/Category/Ring/Limits.lean,Mathlib/Algebra/Group/Action/Defs.lean,Mathlib/Algebra/Group/Conj.lean,Mathlib/Algebra/Group/Defs.lean,Mathlib/Algebra/Group/Hom/Defs.lean,Mathlib/Algebra/Group/Pointwise/Set/Basic.lean,Mathlib/Algebra/Group/Pointwise/Set/Scalar.lean,Mathlib/Algebra/Group/Submonoid/Operations.lean,Mathlib/Algebra/HierarchyDesign.lean,Mathlib/Algebra/Order/Hom/Basic.lean,Mathlib/Analysis/CStarAlgebra/ContinuousFunctionalCalculus/Note.lean,Mathlib/Analysis/RCLike/Lemmas.lean,Mathlib/CategoryTheory/Category/Basic.lean,Mathlib/Data/NNRat/Defs.lean,Mathlib/Data/Nat/Cast/Defs.lean,Mathlib/Data/Nat/Init.lean,Mathlib/Geometry/Manifold/Algebra/Monoid.lean,Mathlib/Geometry/Manifold/ChartedSpace.lean,Mathlib/Logic/Basic.lean,Mathlib/Tactic/Basic.lean,Mathlib/Tactic/NormNum/Basic.lean,Mathlib/Tactic/Simps/Basic.lean,Mathlib/Topology/Algebra/Nonarchimedean/Bases.lean,Mathlib/Topology/Continuous.lean |
26 |
8 |
['adomani', 'github-actions', 'grunweg', 'leanprover-community-bot-assistant'] |
nobody |
3-34542 3 days ago |
3-34542 3 days ago |
11-66798 11 days |
| 24093 |
AntoineChambert-Loir author:AntoineChambert-Loir |
feat(RingTheory/MvPowerSeries/NoZeroDivisors): prove order_mul |
Prove multiplicativity of order of multivariate power series
---
[](https://gitpod.io/from-referrer/)
|
t-algebra label:t-algebra$ |
213/5 |
Mathlib/Algebra/Order/Monoid/Unbundled/Basic.lean,Mathlib/RingTheory/MvPowerSeries/NoZeroDivisors.lean,Mathlib/RingTheory/MvPowerSeries/Order.lean |
3 |
5 |
['AntoineChambert-Loir', 'github-actions'] |
nobody |
3-24015 3 days ago |
3-69676 3 days ago |
3-69735 3 days |
| 24056 |
lecopivo author:lecopivo |
feat: fun_prop for ContDiff |
Marks `ContDiff/At/On/WithinAt` with `fun_prop` and reformulates certain theorems such they work better with `fun_prop`. In particular
- `_id` and `_comp` without using `id` and `Function.comp`. It works with the normal versions but it fails once you start using `fun_prop` as discharger in `simp` as `simp` runs in reducible transparency and can't see through `id` and `Function.comp` as they are `def`
- Theorems like `ContDiff.fderiv` are formulated with `m=n+1`. `fun_prop` can't handle the metavariable `?m` when applying such theorem. The reformulation of the theorem just bumps the differentiability by one and the final differentiability is resolved with `ContDiff.of_le`. |
t-analysis
t-meta
|
378/191 |
Mathlib.lean,Mathlib/Analysis/Calculus/ContDiff/Basic.lean,Mathlib/Analysis/Calculus/ContDiff/Defs.lean,Mathlib/Analysis/Calculus/ContDiff/Operations.lean,Mathlib/Analysis/Calculus/ContDiff/WithLp.lean,Mathlib/Analysis/Calculus/IteratedDeriv/Defs.lean,Mathlib/Analysis/FunctionalSpaces/SobolevInequality.lean,Mathlib/Analysis/SpecialFunctions/Arsinh.lean,Mathlib/Analysis/SpecialFunctions/ExpDeriv.lean,Mathlib/Analysis/SpecialFunctions/Gamma/Deriv.lean,Mathlib/Analysis/SpecialFunctions/Log/Deriv.lean,Mathlib/Analysis/SpecialFunctions/Pow/Deriv.lean,Mathlib/Analysis/SpecialFunctions/SmoothTransition.lean,Mathlib/Analysis/SpecialFunctions/Sqrt.lean,Mathlib/Tactic.lean,Mathlib/Tactic/FunProp/ContDiff.lean,MathlibTest/fun_prop2.lean |
17 |
3 |
['github-actions', 'lecopivo'] |
nobody |
3-23479 3 days ago |
3-69652 3 days ago |
3-70277 3 days |
| 23768 |
loefflerd author:loefflerd |
feat(Analysis/SpecialFunctions): multipliability lemmas |
Prove that in any complete normed ring, a product `∏' i, (1 + f i)` is convergent if the sum of real numbers
`∑' i, ‖f i‖` is convergent.
As part of this, move some lemmas about summability of logs out of `SpecialFunctions.Log` to `Log.Summable` and rework results in the latter file to minimize non-vanishing / positivity conditions.
---
[](https://gitpod.io/from-referrer/)
|
t-analysis |
171/71 |
Mathlib/Analysis/SpecialFunctions/Complex/Log.lean,Mathlib/Analysis/SpecialFunctions/Log/Summable.lean |
2 |
12 |
['CBirkbeck', 'github-actions', 'loefflerd'] |
nobody |
3-18512 3 days ago |
3-18512 3 days ago |
3-18498 3 days |
| 24092 |
jt496 author:jt496 |
feat(Combinatorics/SimpleGraph): add IsCompleteMultipartite definition and related results |
A graph is complete multipartite if non-adjacency is transitive.
We add this definition, the associated Setoid, and the graph isomorphism to the corresponding completeMultipartiteGraph.
We also add the definition of a minimal witness to non-complete-multipartiteness: IsP2Complement.
We will need this for our proof of the Andrásfai–Erdős–Sós theorem, where the interesting case is when the graph is not complete-multipartite.
Co-authored-by: Lian Tattersall
---
[](https://gitpod.io/from-referrer/)
|
t-combinatorics |
153/0 |
Mathlib.lean,Mathlib/Combinatorics/SimpleGraph/CompleteMultipartite.lean |
2 |
7 |
['b-mehta', 'github-actions', 'jt496'] |
nobody |
3-10402 3 days ago |
3-10996 3 days ago |
3-22375 3 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 |
58 |
['FLDutchmann', 'Paul-Lez', 'YaelDillies', 'eric-wieser', 'github-actions', 'kim-em', 'leanprover-community-bot-assistant', 'mathlib4-dependent-issues-bot', 'urkud'] |
nobody |
3-10002 3 days ago |
3-10020 3 days ago |
58-57146 58 days |
| 23903 |
Thmoas-Guan author:Thmoas-Guan |
feat(Algebra): add Submodule.submoduleOf |
In this PR we added the definition `Submodule.submoduleOf` and `Submodule.submoduleOfEquivOfLe` as the corrsponding version for `Subgroup.subgroupOf`
---
[](https://gitpod.io/from-referrer/)
|
t-algebra label:t-algebra$ |
17/0 |
Mathlib/Algebra/Module/Submodule/Map.lean |
1 |
2 |
['Thmoas-Guan', 'github-actions'] |
nobody |
3-7349 3 days ago |
9-21034 9 days ago |
9-21089 9 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 |
169/0 |
Mathlib/Data/List/Chain.lean,Mathlib/Order/RelSeries.lean |
2 |
2 |
['github-actions', 'xyzw12345'] |
nobody |
3-7316 3 days ago |
8-41552 8 days ago |
42-56424 42 days |
| 23935 |
Thmoas-Guan author:Thmoas-Guan |
feat(RingTheory/IsSMulRegular): categorical constructions for IsSMulRegular |
The categorical constructions for `IsSMulRegular` for later use related to `Ext` in a separate file.
---
[](https://gitpod.io/from-referrer/)
|
t-algebra
t-category-theory
label:t-algebra$ |
58/0 |
Mathlib.lean,Mathlib/Algebra/Homology/ExactSequence.lean,Mathlib/RingTheory/Regular/Category.lean |
3 |
16 |
['Thmoas-Guan', 'github-actions', 'joelriou'] |
nobody |
3-7155 3 days ago |
5-17993 5 days ago |
5-57427 5 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
|
251/22 |
Mathlib/CategoryTheory/Subobject/Basic.lean,Mathlib/CategoryTheory/Subobject/Presheaf.lean,Mathlib/CategoryTheory/Topos/Classifier.lean |
3 |
21 |
['Champitoad', 'github-actions', 'joelriou'] |
nobody |
3-6607 3 days ago |
16-78748 16 days ago |
31-12354 31 days |
| 24036 |
Louddy author:Louddy |
feat: add `HeightOneSpectrum.ofPrime` |
Add a definition relating elements of type `HeightOneSpectrum R` with the (nonzero) prime elements of the monoid with zero `Ideal R`. (Note the distinction between `Prime` and `Ideal.IsPrime`).
The documentation string is inspired from [Ideal.prime_iff_isPrime](https://leanprover-community.github.io/mathlib4_docs/Mathlib/RingTheory/DedekindDomain/Ideal.html#Ideal.prime_iff_isPrime).
This was discussed [#mathlib4 > Placing a definition in `DedekindDomain.Ideal` @ 💬](https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/Placing.20a.20definition.20in.20.60DedekindDomain.2EIdeal.60/near/511647129).
---
[](https://gitpod.io/from-referrer/)
|
new-contributor
t-algebra
label:t-algebra$ |
11/1 |
Mathlib/RingTheory/DedekindDomain/Ideal.lean |
1 |
5 |
['Louddy', 'Ruben-VandeVelde', 'github-actions'] |
nobody |
3-5123 3 days ago |
5-4061 5 days ago |
5-4119 5 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
|
159/0 |
Mathlib.lean,Mathlib/AlgebraicTopology/SimplexCategory/GeneratorsRelations/NormalForms.lean |
2 |
14 |
['github-actions', 'joelriou', 'mathlib4-dependent-issues-bot', 'robin-carlier'] |
nobody |
2-79103 2 days ago |
2-79107 2 days ago |
52-82217 52 days |
| 23955 |
Louddy author:Louddy |
feat: Ideal.count_associates_eq |
Add variant of `UniqueFactorizationMonoid.count_normalizedFactors_eq` for associated Ideals.
This is convenient when you need to talk about an element as `a₀ = x ^ n * a`.
Note the file is slightly over the 1500 lines limit, I hope that is ok.
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/)
|
new-contributor
t-algebra
label:t-algebra$ |
35/1 |
Mathlib/RingTheory/DedekindDomain/Ideal.lean |
1 |
5 |
['Louddy', 'Ruben-VandeVelde', 'alreadydone', 'github-actions'] |
nobody |
2-78972 2 days ago |
7-76526 7 days ago |
7-76586 7 days |
| 24117 |
AntoineChambert-Loir author:AntoineChambert-Loir |
feat(GroupTheory/GroupAction/FixingSubgroup): additivize |
Additivize what wasn't.
---
[](https://gitpod.io/from-referrer/)
|
t-algebra label:t-algebra$ |
24/0 |
Mathlib/Algebra/Group/Subgroup/Actions.lean,Mathlib/Algebra/Group/Submonoid/MulAction.lean,Mathlib/GroupTheory/GroupAction/FixedPoints.lean,Mathlib/GroupTheory/GroupAction/FixingSubgroup.lean |
4 |
1 |
['github-actions'] |
nobody |
2-72717 2 days ago |
2-75767 2 days ago |
2-75823 2 days |
| 24121 |
smorel394 author:smorel394 |
feat(RingTheory/Coalgebra/Equiv, RingTheory/Bialgebra/Equiv): constructors for coalgebra and bialgebra equivalences |
Add constructors for equivalences of coalgebras and bialgebras, similar to what already exists for equivalences of algebras:
- `CoalgEquiv.ofCoalgHom` constructs a `CoalgEquiv` from a `CoalgHom` that has an inverse;
- `CoalgEquiv.ofBijective` constructs a `CoalgEquiv` from a bijective `CoalgHom`;
- `BialgEquiv.ofBialgHom` constructs a `BialgEquiv` from a `CoalgHom` that has an inverse;
- `BialgEquiv.ofBijective` constructs a `BialgEquiv` from a bijective `BialgHom`.
Also add some `apply` and `coe` lemmas, following the same model as for `AlgEquiv`s.
From Toric
---
[](https://gitpod.io/from-referrer/)
|
toric
t-algebra
label:t-algebra$ |
72/0 |
Mathlib/RingTheory/Bialgebra/Equiv.lean,Mathlib/RingTheory/Coalgebra/Equiv.lean |
2 |
1 |
['github-actions'] |
nobody |
2-69640 2 days ago |
2-69929 2 days ago |
2-70001 2 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$ |
42/32 |
Mathlib/Algebra/Polynomial/Roots.lean,Mathlib/RingTheory/Polynomial/Cyclotomic/Basic.lean,Mathlib/RingTheory/RootsOfUnity/PrimitiveRoots.lean |
3 |
4 |
['github-actions', 'leanprover-community-bot-assistant', 'mans0954', 'urkud'] |
nobody |
2-68939 2 days ago |
8-75250 8 days ago |
25-17740 25 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 |
2-68838 2 days ago |
29-63715 29 days ago |
29-63710 29 days |
| 24102 |
ScottCarnahan author:ScottCarnahan |
feat (RingTheory/HahnSeries): Powers of a binomial |
This PR introduces powers of a binomial `single g 1 - single g' 1` in a Hahn series, where the powers take values in a binomial ring. These series behave as one would expect with respect to addition of powers, and comparison with natural number powers. They are often used in the theory of vertex algebras.
---
[](https://gitpod.io/from-referrer/)
|
t-algebra label:t-algebra$ |
142/11 |
Mathlib.lean,Mathlib/RingTheory/HahnSeries/Addition.lean,Mathlib/RingTheory/HahnSeries/Binomial.lean,Mathlib/RingTheory/HahnSeries/HEval.lean,Mathlib/RingTheory/HahnSeries/Multiplication.lean,Mathlib/RingTheory/HahnSeries/Summable.lean,Mathlib/RingTheory/PowerSeries/Binomial.lean |
7 |
1 |
['github-actions'] |
nobody |
2-66017 2 days ago |
3-42602 3 days ago |
3-42589 3 days |
| 24119 |
alreadydone author:alreadydone |
feat: preliminaries for Wedderburn–Artin |
---
[](https://gitpod.io/from-referrer/)
|
t-algebra label:t-algebra$ |
212/116 |
Mathlib/Algebra/Algebra/Opposite.lean,Mathlib/Algebra/Azumaya/Basic.lean,Mathlib/Algebra/Equiv/TransferInstance.lean,Mathlib/Algebra/Lie/Semisimple/Basic.lean,Mathlib/Algebra/Module/Equiv/Basic.lean,Mathlib/Algebra/Module/LinearMap/Defs.lean,Mathlib/Algebra/Module/LinearMap/End.lean,Mathlib/Algebra/Module/Submodule/Ker.lean,Mathlib/Data/Matrix/Basic.lean,Mathlib/FieldTheory/IsAlgClosed/Basic.lean,Mathlib/LinearAlgebra/Matrix/ToLin.lean,Mathlib/LinearAlgebra/Projection.lean,Mathlib/LinearAlgebra/Span/Basic.lean,Mathlib/Logic/Equiv/Defs.lean,Mathlib/Order/Atoms.lean,Mathlib/RingTheory/Congruence/Basic.lean,Mathlib/RingTheory/Ideal/Defs.lean,Mathlib/RingTheory/Jacobson/Ideal.lean,Mathlib/RingTheory/LocalRing/RingHom/Basic.lean,Mathlib/RingTheory/Nullstellensatz.lean,Mathlib/RingTheory/SimpleRing/Congr.lean,Mathlib/RingTheory/SimpleRing/Defs.lean,Mathlib/RingTheory/TwoSidedIdeal/Operations.lean,Mathlib/RingTheory/Unramified/Field.lean |
24 |
1 |
['github-actions'] |
nobody |
2-63053 2 days ago |
2-70132 2 days ago |
2-70125 2 days |
| 24064 |
kim-em author:kim-em |
chore: replace `norm_num` with `simp` where applicable |
Consider replacing a tactic with a (ahem) simpler alternative.
Fairly neutral performance implications, just depends on whether we would like to encourage people to use `simp` where applicable. |
|
346/346 |
Archive/Examples/MersennePrimes.lean,Archive/Imo/Imo1959Q2.lean,Archive/Imo/Imo1960Q1.lean,Archive/Imo/Imo1962Q1.lean,Archive/Imo/Imo1962Q4.lean,Archive/Imo/Imo1981Q3.lean,Archive/Imo/Imo1982Q1.lean,Archive/Imo/Imo2001Q2.lean,Archive/Imo/Imo2005Q4.lean,Archive/Imo/Imo2006Q3.lean,Archive/Imo/Imo2008Q4.lean,Archive/Imo/Imo2024Q1.lean,Archive/Imo/Imo2024Q5.lean,Archive/Imo/Imo2024Q6.lean,Archive/Wiedijk100Theorems/AbelRuffini.lean,Archive/Wiedijk100Theorems/CubingACube.lean,Archive/Wiedijk100Theorems/SumOfPrimeReciprocalsDiverges.lean,Counterexamples/Cyclotomic105.lean,Counterexamples/Phillips.lean,Mathlib/Algebra/Field/NegOnePow.lean,Mathlib/Algebra/Homology/HomotopyCategory/MappingCone.lean,Mathlib/Algebra/Order/CauSeq/BigOperators.lean,Mathlib/Algebra/Polynomial/FieldDivision.lean,Mathlib/Algebra/Polynomial/Roots.lean,Mathlib/Algebra/Polynomial/SpecificDegree.lean,Mathlib/Algebra/Ring/BooleanRing.lean,Mathlib/Algebra/Star/CHSH.lean,Mathlib/AlgebraicGeometry/EllipticCurve/IsomOfJ.lean,Mathlib/AlgebraicTopology/DoldKan/Faces.lean,Mathlib/Analysis/Analytic/Inverse.lean,Mathlib/Analysis/Asymptotics/AsymptoticEquivalent.lean,Mathlib/Analysis/BoxIntegral/UnitPartition.lean,Mathlib/Analysis/CStarAlgebra/ContinuousFunctionalCalculus/Basic.lean,Mathlib/Analysis/CStarAlgebra/ContinuousFunctionalCalculus/Order.lean,Mathlib/Analysis/CStarAlgebra/Module/Defs.lean,Mathlib/Analysis/Calculus/FDeriv/Measurable.lean,Mathlib/Analysis/Calculus/FDeriv/Norm.lean,Mathlib/Analysis/Calculus/FDeriv/Symmetric.lean,Mathlib/Analysis/Calculus/MeanValue.lean,Mathlib/Analysis/Complex/AbelLimit.lean,Mathlib/Analysis/Convex/Between.lean,Mathlib/Analysis/Convex/Function.lean,Mathlib/Analysis/Convolution.lean,Mathlib/Analysis/Fourier/AddCircle.lean,Mathlib/Analysis/Fourier/AddCircleMulti.lean,Mathlib/Analysis/Fourier/Inversion.lean,Mathlib/Analysis/Fourier/RiemannLebesgueLemma.lean,Mathlib/Analysis/InnerProductSpace/NormPow.lean,Mathlib/Analysis/InnerProductSpace/Projection.lean,Mathlib/Analysis/InnerProductSpace/l2Space.lean,Mathlib/Analysis/MeanInequalities.lean,Mathlib/Analysis/MellinInversion.lean,Mathlib/Analysis/Normed/Affine/Simplex.lean,Mathlib/Analysis/Normed/Algebra/TrivSqZeroExt.lean,Mathlib/Analysis/Normed/Group/ControlledClosure.lean,Mathlib/Analysis/Normed/Lp/lpSpace.lean,Mathlib/Analysis/Normed/Operator/Banach.lean,Mathlib/Analysis/Normed/Ring/Units.lean,Mathlib/Analysis/NormedSpace/HahnBanach/Separation.lean,Mathlib/Analysis/NormedSpace/MStructure.lean,Mathlib/Analysis/NormedSpace/RieszLemma.lean,Mathlib/Analysis/Oscillation.lean,Mathlib/Analysis/SpecialFunctions/BinaryEntropy.lean,Mathlib/Analysis/SpecialFunctions/Complex/Log.lean,Mathlib/Analysis/SpecialFunctions/ContinuousFunctionalCalculus/Rpow/Basic.lean,Mathlib/Analysis/SpecialFunctions/ContinuousFunctionalCalculus/Rpow/Isometric.lean,Mathlib/Analysis/SpecialFunctions/ExpDeriv.lean,Mathlib/Analysis/SpecialFunctions/Gamma/Beta.lean,Mathlib/Analysis/SpecialFunctions/Gamma/BohrMollerup.lean,Mathlib/Analysis/SpecialFunctions/Gamma/Deligne.lean,Mathlib/Analysis/SpecialFunctions/Gaussian/GaussianIntegral.lean,Mathlib/Analysis/SpecialFunctions/Integrals.lean,Mathlib/Analysis/SpecialFunctions/Log/Monotone.lean,Mathlib/Analysis/SpecialFunctions/Pow/Real.lean,Mathlib/Analysis/SpecialFunctions/Trigonometric/Angle.lean,Mathlib/Analysis/SpecialFunctions/Trigonometric/Basic.lean,Mathlib/Analysis/SpecialFunctions/Trigonometric/Complex.lean,Mathlib/Analysis/SpecialFunctions/Trigonometric/Inverse.lean,Mathlib/Combinatorics/Additive/AP/Three/Behrend.lean,Mathlib/Combinatorics/Additive/SmallTripling.lean,Mathlib/Combinatorics/Extremal/RuzsaSzemeredi.lean,Mathlib/Combinatorics/SimpleGraph/Density.lean,Mathlib/Combinatorics/SimpleGraph/Regularity/Bound.lean,Mathlib/Combinatorics/SimpleGraph/Regularity/Chunk.lean,Mathlib/Combinatorics/SimpleGraph/Regularity/Increment.lean,Mathlib/Combinatorics/SimpleGraph/Regularity/Lemma.lean,Mathlib/Combinatorics/SimpleGraph/Triangle/Basic.lean,Mathlib/Combinatorics/SimpleGraph/Triangle/Counting.lean,Mathlib/Computability/Ackermann.lean,Mathlib/Computability/AkraBazzi/AkraBazzi.lean,Mathlib/Computability/DFA.lean,Mathlib/Data/Complex/Basic.lean,Mathlib/Data/Complex/Trigonometric.lean,Mathlib/Data/Nat/Bits.lean,Mathlib/Data/Nat/Choose/Central.lean,Mathlib/Data/Nat/Choose/Sum.lean,Mathlib/Data/Nat/Digits.lean,Mathlib/Data/Nat/Prime/Defs.lean,Mathlib/Data/Real/GoldenRatio.lean,Mathlib/Data/Real/Pi/Bounds.lean |
172 |
7 |
['github-actions', 'leanprover-bot', 'leanprover-community-mathlib4-bot'] |
nobody |
2-51841 2 days ago |
2-51841 2 days ago |
4-31937 4 days |
| 24127 |
DavidLedvinka author:DavidLedvinka |
feat(MeasureTheory/Measure/WithDensity): density of product of measures |
Add a lemma which states that the density of the product of measures is given by the product of the densities. |
new-contributor
t-measure-probability
|
29/1 |
Mathlib/MeasureTheory/Group/Convolution.lean,Mathlib/MeasureTheory/Measure/Prod.lean,Mathlib/MeasureTheory/Measure/WithDensity.lean |
3 |
1 |
['github-actions'] |
nobody |
2-51202 2 days ago |
2-51213 2 days ago |
2-51276 2 days |
| 24135 |
madvorak author:madvorak |
chore(Data/Matrix/Def): `Matrix.submatrix` naming convention |
---
[](https://gitpod.io/from-referrer/)
|
t-data |
11/11 |
Mathlib/Data/Matrix/ConjTranspose.lean,Mathlib/Data/Matrix/Defs.lean |
2 |
1 |
['github-actions'] |
nobody |
2-6583 2 days ago |
2-6590 2 days ago |
2-6646 2 days |
| 22779 |
xroblot author:xroblot |
feat(NumberField/CanonicalEmbedding/NormLeOne): prove that the frontier of `normLeOne` has zero-volume |
This is the last PR about `normLeOne K`.
We prove that it is a bounded set and that its frontier has volume zero.
This PR is part of the proof of the Analytic Class Number Formula.
---
- [x] depends on: #22777
[](https://gitpod.io/from-referrer/)
|
t-number-theory |
214/1 |
Mathlib/NumberTheory/NumberField/CanonicalEmbedding/Basic.lean,Mathlib/NumberTheory/NumberField/CanonicalEmbedding/NormLeOne.lean |
2 |
2 |
['github-actions', 'mathlib4-dependent-issues-bot'] |
nobody |
2-5824 2 days ago |
2-78772 2 days ago |
2-79175 2 days |
| 24137 |
xroblot author:xroblot |
feat(NumberField): add `ComplexEmbedding.lift` |
---
[](https://gitpod.io/from-referrer/)
|
t-number-theory |
19/3 |
Mathlib/NumberTheory/NumberField/Embeddings.lean |
1 |
1 |
['github-actions'] |
nobody |
2-4173 2 days ago |
2-5931 2 days ago |
2-5992 2 days |
| 24015 |
alreadydone author:alreadydone |
feat(RingTheory): lemmas on finiteness of `LinearMap` and `Module.End` |
---
One less lemma than #24012, but with the advantage of not depending on #23963.
- [x] depends on: #24115
[](https://gitpod.io/from-referrer/)
|
t-algebra label:t-algebra$ |
91/32 |
Mathlib/Algebra/Module/LinearMap/End.lean,Mathlib/GroupTheory/GroupAction/SubMulAction.lean,Mathlib/LinearAlgebra/BilinearMap.lean,Mathlib/LinearAlgebra/Dual/Lemmas.lean,Mathlib/LinearAlgebra/Projection.lean,Mathlib/RingTheory/Finiteness/Basic.lean,Mathlib/RingTheory/SimpleModule/Basic.lean |
7 |
9 |
['alreadydone', 'eric-wieser', 'github-actions', 'leanprover-bot', 'leanprover-community-mathlib4-bot', 'mathlib4-dependent-issues-bot'] |
nobody |
2-2494 2 days ago |
2-2494 2 days ago |
5-9619 5 days |
| 24142 |
joelriou author:joelriou |
feat(CategoryTheory): left derived functors |
The definitions in the file `CategoryTheory.Functor.Derived.RightDerived` are dualized in order to define left derived functors.
---
[](https://gitpod.io/from-referrer/)
|
t-category-theory |
213/0 |
Mathlib.lean,Mathlib/CategoryTheory/Functor/Derived/LeftDerived.lean |
2 |
1 |
['github-actions'] |
nobody |
1-81831 1 day ago |
1-81896 1 day ago |
1-81883 1 day |
| 24122 |
apnelson1 author:apnelson1 |
feat(Combinatorics): multigraphs |
This PR defines multigraphs via a structure `Graph a b` consisting of a vertex set, an edge set, and a 'binary incidence' predicate describing which edges are incident with which vertices. The definition uses the same 'embedded set' design as `Matroid`: the vertex and edge sets are modelled as `Set`s rather than types.
We give basic API for incidence, adjacency and extensionality.
[Zulip discussion.](https://leanprover.zulipchat.com/#narrow/stream/144837-PR-reviews/topic/.2324122.20Multigraphs)
---
[](https://gitpod.io/from-referrer/)
|
t-combinatorics |
291/0 |
Mathlib.lean,Mathlib/Combinatorics/Graph/Basic.lean,scripts/noshake.json |
3 |
12 |
['Parcly-Taxel', 'apnelson1', 'b-mehta', 'github-actions', 'kmill', 'madvorak'] |
nobody |
1-79512 1 day ago |
2-69070 2 days ago |
2-69130 2 days |
| 23909 |
grunweg author:grunweg |
chore: various fixes for the flexible linter |
---
[](https://gitpod.io/from-referrer/)
|
|
120/85 |
Mathlib/Condensed/Light/Epi.lean,Mathlib/Control/EquivFunctor/Instances.lean,Mathlib/Control/Monad/Cont.lean,Mathlib/Data/FinEnum.lean,Mathlib/Data/Finsupp/MonomialOrder.lean,Mathlib/Data/List/Sigma.lean,Mathlib/Data/List/SplitBy.lean,Mathlib/Data/Matroid/Sum.lean,Mathlib/Data/Ordmap/Invariants.lean,Mathlib/Data/Real/Pi/Irrational.lean,Mathlib/Data/Seq/Parallel.lean,Mathlib/Data/Vector3.lean,Mathlib/Data/WSeq/Relation.lean,Mathlib/Geometry/Manifold/VectorBundle/Tangent.lean,Mathlib/GroupTheory/CoprodI.lean,Mathlib/GroupTheory/Coxeter/Basic.lean,Mathlib/GroupTheory/Coxeter/Inversion.lean,Mathlib/GroupTheory/Goursat.lean,Mathlib/GroupTheory/HNNExtension.lean,Mathlib/GroupTheory/Nilpotent.lean,Mathlib/NumberTheory/Dioph.lean,Mathlib/NumberTheory/FLT/Polynomial.lean,Mathlib/NumberTheory/LSeries/Injectivity.lean,Mathlib/NumberTheory/NumberField/Embeddings.lean,Mathlib/Probability/Kernel/Condexp.lean,Mathlib/RingTheory/Derivation/MapCoeffs.lean,Mathlib/RingTheory/Frobenius.lean,Mathlib/SetTheory/Ordinal/Notation.lean,Mathlib/SetTheory/ZFC/Rank.lean,Mathlib/Tactic/NormNum/NatFactorial.lean |
30 |
8 |
['b-mehta', 'github-actions', 'grunweg'] |
nobody |
1-77916 1 day ago |
9-13403 9 days ago |
9-13390 9 days |
| 24141 |
loefflerd author:loefflerd |
feat(NumberTheory/Padics): parametrization of cts add chars of Z_[p] |
Another step towards defining the Mahler / Amice transform for p-adic measures.
---
[](https://gitpod.io/from-referrer/)
|
t-number-theory |
108/0 |
Mathlib.lean,Mathlib/NumberTheory/Padics/AddChar.lean |
2 |
1 |
['github-actions'] |
nobody |
1-72588 1 day ago |
1-82170 1 day ago |
1-82169 1 day |
| 24134 |
sgouezel author:sgouezel |
feat: drop measurability assumption in `norm_setIntegral_le_of_norm_le_const_ae'` |
---
[](https://gitpod.io/from-referrer/)
|
maintainer-merge
t-measure-probability
|
46/47 |
Mathlib/Analysis/Fourier/RiemannLebesgueLemma.lean,Mathlib/Analysis/SpecialFunctions/MulExpNegMulSqIntegral.lean,Mathlib/MeasureTheory/Integral/Bochner/FundThmCalculus.lean,Mathlib/MeasureTheory/Integral/Bochner/Set.lean,Mathlib/MeasureTheory/Integral/DivergenceTheorem.lean,Mathlib/MeasureTheory/Integral/IntervalIntegral/Basic.lean,Mathlib/MeasureTheory/Integral/TorusIntegral.lean,Mathlib/NumberTheory/Transcendental/Lindemann/AnalyticalPart.lean |
8 |
3 |
['Ruben-VandeVelde', 'github-actions', 'grunweg'] |
nobody |
1-71771 1 day ago |
1-71772 1 day ago |
2-10815 2 days |
| 22576 |
Ruben-VandeVelde author:Ruben-VandeVelde |
feat: more lemmas about alternatingGroup |
---
[](https://gitpod.io/from-referrer/)
cc @AntoineChambert-Loir (whose code this is) |
maintainer-merge
t-algebra
label:t-algebra$ |
55/0 |
Mathlib/GroupTheory/SpecificGroups/Alternating/Centralizer.lean |
1 |
4 |
['b-mehta', 'github-actions'] |
nobody |
1-67992 1 day ago |
1-70783 1 day ago |
45-51197 45 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
maintainer-merge
t-meta
|
206/10 |
Mathlib/Util/Superscript.lean,MathlibTest/superscript.lean |
2 |
36 |
['eric-wieser', 'gio256', 'github-actions', 'joneugster'] |
nobody |
1-65022 1 day ago |
1-66232 1 day ago |
30-68190 30 days |
| 24138 |
smorel394 author:smorel394 |
feat(RingTheory/Bialgebra/Basic): injectivity of `algebraMap` and nontriviality of bialgebras |
If `A` is a bialgebra over a commutative semiring `R`, prove that `algebraMap R A` is injective. Deduce that `A` is nontrivial if `R` is nontrivial.
---
[](https://gitpod.io/from-referrer/)
|
toric
t-algebra
label:t-algebra$ |
17/0 |
Mathlib/RingTheory/Bialgebra/Basic.lean |
1 |
1 |
['github-actions'] |
nobody |
1-63008 1 day ago |
2-5288 2 days ago |
2-5292 2 days |
| 22974 |
YaelDillies author:YaelDillies |
refactor: use a junk value for the analytic order of a non-analytic function |
Currently, the order of an analytic function is called `AnalyticAt.order` and has a single explicit argument `hf : AnalyticAt 𝕜 f z₀`. This means that working with analytic functions results in contexts full of `hf.order` or, worse, `⋯.order`.
This PR makes the `f` and `z₀` arguments explicit, and drops the `hf` one by introducing a junk value of `0` for non-analytic functions. The resulting function is called `eanalyticOrderAt` and I am also adding a `Nat`-valued version `analyticOrderAt` since `(eanalyticOrderAt f z₀).toNat` was appearing in quite a few lemmas.
---
The same change could be performed for meromorphic functions once you are convinced.
[](https://gitpod.io/from-referrer/)
|
t-analysis |
187/101 |
Mathlib/Analysis/Analytic/Order.lean,Mathlib/Analysis/Meromorphic/NormalForm.lean,Mathlib/Analysis/Meromorphic/Order.lean,Mathlib/Data/ENat/Basic.lean |
4 |
7 |
['YaelDillies', 'github-actions', 'loefflerd', 'urkud'] |
nobody |
1-59890 1 day ago |
16-82097 16 days ago |
31-43411 31 days |
| 23546 |
JovanGerb author:JovanGerb |
feat(LinearAlgebra/AffineSpace/AffineSubspace): rename `AffineSubspace.mk'` to `Submodule.shift` |
In addition to renaming, I've refactored the code a bit:
- `mem_mk'_iff_vsub_mem` was obsolete since it was the same as `mem_mk'`, so I removed it (this is due to a change in the definition I made recently)
- I added a nonempty instance for `shift`
- I added a simp lemma that `shift` isn't equal to `⊥` (the empty affine subspace). I need this for the next point.
- Edit: I'll leave this for a later PR.
~I proved a simp lemma that a `shift` is parallel to a `shift` if and only if the linear subspaces are the same.~
- I renamed `mk'_eq` to `shift_direction_eq_self `.
- I renamed `eq_or_eq_secondInter_of_mem_mk'_span_singleton_iff_mem` to `eq_or_eq_secondInter_iff_mem_of_mem_shift_span_singleton`. I think it is better to put the `of_mem_mk'_span_singleton` at the end of the name.
---
[](https://gitpod.io/from-referrer/)
|
t-algebraic-geometry |
128/99 |
Mathlib/Algebra/Module/ZLattice/Basic.lean,Mathlib/Geometry/Euclidean/Basic.lean,Mathlib/Geometry/Euclidean/MongePoint.lean,Mathlib/Geometry/Euclidean/PerpBisector.lean,Mathlib/Geometry/Euclidean/Sphere/SecondInter.lean,Mathlib/Geometry/Euclidean/Sphere/Tangent.lean,Mathlib/LinearAlgebra/AffineSpace/AffineSubspace/Defs.lean |
7 |
2 |
['JovanGerb', 'github-actions'] |
nobody |
1-59723 1 day ago |
1-59723 1 day ago |
17-83191 17 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
t-algebra
t-analysis
label:t-algebra$ |
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 |
11 |
['github-actions', 'urkud', 'vlad902'] |
urkud assignee:urkud |
1-59685 1 day ago |
1-59685 1 day ago |
44-40621 44 days |
| 23758 |
erdOne author:erdOne |
feat(Topology/Algebra): linearly topologized iff non-archimedian |
...for topological modules over compact rings or `ℤ`-finite rings
---
[](https://gitpod.io/from-referrer/)
|
large-import
t-algebra
t-topology
label:t-algebra$ |
138/3 |
Mathlib/LinearAlgebra/Span/Basic.lean,Mathlib/Topology/Algebra/LinearTopology.lean |
2 |
20 |
['ADedecker', 'AntoineChambert-Loir', 'erdOne', 'github-actions'] |
nobody |
1-59645 1 day ago |
1-59645 1 day ago |
12-22066 12 days |
| 22792 |
madvorak author:madvorak |
feat(Mathlib/Data/Fin/Pigeonhole): 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 |
1-58695 1 day ago |
39-77030 1 month ago |
39-77085 39 days |
| 23677 |
upobir author:upobir |
feat(Mathlib/RingTheory/Int/Basic): add eq_pow_of_mul_eq_pow for Nat |
---
This pr adds theorems analogous to [Int.sq_of_isCoprime](https://leanprover-community.github.io/mathlib4_docs/Mathlib/RingTheory/Int/Basic.html#Int.sq_of_isCoprime), but with generic power and both left and right versions. I had asked in [this zulip thread](https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/Nat.20and.20left.2C.20right.20version.20of.20Int.2Esq_of_isCoprime) before to make sure this theorem was missing.
[](https://gitpod.io/from-referrer/)
|
new-contributor
t-algebra
label:t-algebra$ |
20/3 |
Mathlib/RingTheory/Int/Basic.lean |
1 |
1 |
['github-actions'] |
nobody |
1-58503 1 day ago |
14-64446 14 days ago |
14-64505 14 days |
| 23844 |
pechersky author:pechersky |
feat(CI): build gitpod container in github CI |
And push to ghcr.io
---
[](https://gitpod.io/from-referrer/)
|
CI |
64/0 |
.github/workflows/docker_build.yml |
1 |
9 |
['bryangingechen', 'github-actions', 'pechersky'] |
nobody |
1-58468 1 day ago |
10-64190 10 days ago |
10-64247 10 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/)
|
t-data |
15/14 |
Mathlib/Data/Finsupp/Basic.lean,Mathlib/LinearAlgebra/Finsupp/Defs.lean |
2 |
1 |
['github-actions'] |
nobody |
1-55447 1 day ago |
1-55447 1 day ago |
32-63767 32 days |
| 22100 |
smmercuri author:smmercuri |
feat: two inequivalent absolute values have a `< 1` and `> 1` value |
- Two absolute values `v` and `w` are equivalent if and only if `v x < 1` exactly when `w x < 1`
- Two inequivalent absolute values `v` and `w` have a point `x` at which `1 < v x` and `w x < 1`
---
[](https://gitpod.io/from-referrer/)
|
t-algebra
t-analysis
label:t-algebra$ |
174/0 |
Mathlib/Algebra/Order/AbsoluteValue/Basic.lean,Mathlib/Analysis/AbsoluteValue/Equivalence.lean |
2 |
6 |
['Paul-Lez', 'github-actions', 'smmercuri'] |
nobody |
1-55437 1 day ago |
1-55437 1 day ago |
32-42786 32 days |
| 23926 |
b-reinke author:b-reinke |
feat(Algebra/BigOperators/Finprod): add powerset projection lemmas |
This PR adds lemmas in `Mathlib/Algebra/BigOperators/Finprod.lean` related to products/sums over the powerset `𝒫 s` when we add or remove an element of `s`.
We also add the lemmas `mul_finsum_mem` and `finsum_mem_mul`, the analogues of `mul_finsum` and `finsum_mul` for sums over a subset
The motivation comes from the proof of the deletion/contraction properties of matroids.
---
[](https://gitpod.io/from-referrer/)
|
t-algebra label:t-algebra$ |
38/0 |
Mathlib/Algebra/BigOperators/Finprod.lean,Mathlib/Data/Set/Image.lean |
2 |
3 |
['b-reinke', 'eric-wieser', 'github-actions'] |
nobody |
1-55387 1 day ago |
1-55387 1 day ago |
8-54993 8 days |
| 23530 |
YaelDillies author:YaelDillies |
feat(.devcontainer): use prebuilt Docker image |
... instead of building it every time we open a codespace. This makes opening a codespace much faster.
The image can be found here: https://hub.docker.com/r/leanprovercommunity/gitpod4. I am the one maintaining it.
---
[](https://gitpod.io/from-referrer/)
|
maintainer-merge
CI
|
1/3 |
.devcontainer/devcontainer.json |
1 |
3 |
['github-actions', 'joneugster'] |
nobody |
1-54956 1 day ago |
1-54956 1 day ago |
18-10669 18 days |
| 11968 |
JovanGerb author:JovanGerb |
feat: improvements to RefinedDiscrTree |
This PR defines `RefinedDiscrTree`, which is an improved version of `DiscrTree` with many new features, such as
- indexing lambda terms, dependent forall terms, and bound variables.
- giving a score to matches, in order to sort them
- indexing star patterns so that `a+b` and `a+a` are indexed differently
- taking into account eta reductions, so that `exp` can still be matched with the library pattern `fun x => exp (f x)`.
This PR makes `RefinedDiscrTree` into a lazy data structure, meaning that it can be used without a cache, just like `LazyDiscrTree`.
This PR also removes these features:
- indexing `fun x => x` as `id`
- indexing `fun x => f x + g x` as `f + g`, and similarly for `-`, `*`, `/`, `⁻¹`, `^`.
- indexing `fun _ => 42` as `42`
These equivalent indexings do not hold definitionally in the `reducible` transparency, which is the transparency that is used for unification when using a discrimination tree. Therefore, indexing these different expressions the same is actually inefficient rather than helpful.
This is part of the bigger #11768, which uses this discrimination tree for a library rewriting tactic.
This replaces an older version of `RefinedDiscrTree`.
---
[](https://gitpod.io/from-referrer/)
|
new-contributor
t-meta
|
1631/1242 |
Mathlib.lean,Mathlib/Lean/Meta/RefinedDiscrTree.lean,Mathlib/Lean/Meta/RefinedDiscrTree/Basic.lean,Mathlib/Lean/Meta/RefinedDiscrTree/Encode.lean,Mathlib/Lean/Meta/RefinedDiscrTree/Initialize.lean,Mathlib/Lean/Meta/RefinedDiscrTree/Lookup.lean,Mathlib/Lean/Meta/RefinedDiscrTree/Pi.lean,Mathlib/Tactic.lean,Mathlib/Tactic/FunProp.lean,Mathlib/Tactic/FunProp/Elab.lean,Mathlib/Tactic/FunProp/StateList.lean,Mathlib/Tactic/FunProp/Theorems.lean,Mathlib/Tactic/FunProp/Types.lean,Mathlib/Topology/Defs/Basic.lean,MathlibTest/RefinedDiscrTree.lean,scripts/noshake.json |
16 |
78 |
['0art0', 'JovanGerb', 'eric-wieser', 'github-actions', 'grunweg', 'joneugster', 'leanprover-bot', 'rosborn'] |
nobody |
1-54206 1 day ago |
12-52109 12 days ago |
186-76875 186 days |
| 24113 |
ADedecker author:ADedecker |
chore: reorganize and rename the Embedding --> Homeomorph constructions |
This is the updated version of #12994
- rename [Homeomorph.ofIsEmbedding](https://leanprover-community.github.io/mathlib4_docs/Mathlib/Topology/Homeomorph/Lemmas.html#Homeomorph.ofIsEmbedding) to `IsEmbedding.toHomeomorph`
- move [Topology.IsEmbedding.toHomeomorph_of_surjective](https://leanprover-community.github.io/mathlib4_docs/Mathlib/Topology/IsLocalHomeomorph.html#Topology.IsEmbedding.toHomeomorph_of_surjective) earlier (and PascalCase it)
- rename [Homeomorph.homeomorphOfContinuousOpen](https://leanprover-community.github.io/mathlib4_docs/Mathlib/Topology/Homeomorph/Defs.html#Homeomorph.homeomorphOfContinuousOpen) to `Equiv.toHomeomorphOfContinuousOpen`, and similarly for the closed version.
---
[](https://gitpod.io/from-referrer/)
|
t-topology |
96/70 |
Mathlib/AlgebraicGeometry/Fiber.lean,Mathlib/AlgebraicGeometry/Morphisms/FiniteType.lean,Mathlib/AlgebraicGeometry/Morphisms/IsIso.lean,Mathlib/AlgebraicGeometry/Morphisms/QuasiSeparated.lean,Mathlib/AlgebraicGeometry/OpenImmersion.lean,Mathlib/AlgebraicGeometry/Properties.lean,Mathlib/Geometry/RingedSpace/OpenImmersion.lean,Mathlib/MeasureTheory/Constructions/BorelSpace/Basic.lean,Mathlib/Topology/Category/Profinite/Nobeling/Induction.lean,Mathlib/Topology/Category/TopCat/Basic.lean,Mathlib/Topology/Category/TopCat/Limits/Products.lean,Mathlib/Topology/Category/TopCat/Limits/Pullbacks.lean,Mathlib/Topology/Constructions/SumProd.lean,Mathlib/Topology/Gluing.lean,Mathlib/Topology/Homeomorph/Defs.lean,Mathlib/Topology/Homeomorph/Lemmas.lean,Mathlib/Topology/IsLocalHomeomorph.lean,Mathlib/Topology/LocalAtTarget.lean,Mathlib/Topology/TietzeExtension.lean |
19 |
4 |
['ADedecker', 'github-actions', 'grunweg'] |
grunweg assignee:grunweg |
1-52529 1 day ago |
1-52529 1 day ago |
1-68919 1 day |
| 24155 |
eric-wieser author:eric-wieser |
feat: add a "rw_proc" for fin vectors |
This seems a little nicer than an elaborator, since it means I can use the default elaboration rules to handle my first few variables.
Ideally there would be something like
```lean
rw_procQ {A : Type u} {B : A -> Type v} (a : A) (b : B a) : b = ?rhs => do
/-- Context:
u v : Level
A : Q(Type u)
B : Q($A -> Type v)
a : Q($A)
b : Q($B $a)
rhs : Q($B $a) -- metavariable to assign
|- MetaM Q($b = ?rhs)
-/
```
or
```lean
rw_proc {A : Type u} {B : A -> Type v} (a : A) (b : B a) : b = ?rhs => do
/-- Context:
u v : Level
A B a b : Expr
rhs : MVarId
|- MetaM Expr
-/
```
which would generate the code I wrote here
---
[](https://gitpod.io/from-referrer/)
|
t-data
RFC
|
27/2 |
Mathlib/Data/Fin/Tuple/Reflection.lean |
1 |
1 |
['github-actions'] |
nobody |
1-46551 1 day ago |
1-46900 1 day ago |
1-46955 1 day |
| 23822 |
eric-wieser author:eric-wieser |
fix: missing `noWs` in notations |
Also removed the `9000` priority, since this was probably chosen randomly, and there is no comment justifying it.
---
[](https://gitpod.io/from-referrer/)
|
t-algebra label:t-algebra$ |
21/5 |
Mathlib/Algebra/Module/Torsion.lean,Mathlib/Algebra/MonoidAlgebra/Defs.lean |
2 |
4 |
['eric-wieser', 'github-actions', 'urkud'] |
nobody |
1-46202 1 day ago |
11-6413 11 days ago |
11-6552 11 days |
| 24158 |
urkud author:urkud |
feat(Asymptotics/Completion): new file |
---
[](https://gitpod.io/from-referrer/)
|
t-analysis |
50/0 |
Mathlib.lean,Mathlib/Analysis/Asymptotics/Completion.lean |
2 |
1 |
['github-actions'] |
nobody |
1-28325 1 day ago |
1-28325 1 day ago |
1-28395 1 day |
| 24145 |
grunweg author:grunweg |
chore: rename LinearEquiv.prod to prodCongr |
[Zulip discussion]([#mathlib4 > Naming convention @ 💬](https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/Naming.20convention/near/512683092))
As a bonus, replace some outdated `prod.map` in module doc-strings by `Prod.map`.
---
Best reviewed commit by commit.
[](https://gitpod.io/from-referrer/)
|
|
58/48 |
Mathlib/Algebra/Group/Prod.lean,Mathlib/Algebra/Module/PID.lean,Mathlib/Analysis/Calculus/LagrangeMultipliers.lean,Mathlib/Analysis/Normed/Lp/PiLp.lean,Mathlib/LinearAlgebra/Basis/Prod.lean,Mathlib/LinearAlgebra/Basis/VectorSpace.lean,Mathlib/LinearAlgebra/Dimension/Constructions.lean,Mathlib/LinearAlgebra/Prod.lean,Mathlib/LinearAlgebra/QuadraticForm/Dual.lean,Mathlib/LinearAlgebra/QuadraticForm/Prod.lean,Mathlib/LinearAlgebra/TensorProduct/Prod.lean,Mathlib/LinearAlgebra/Trace.lean,Mathlib/Order/Hom/Basic.lean,Mathlib/RingTheory/TensorProduct/IsBaseChangePi.lean,Mathlib/Topology/Algebra/Module/Equiv.lean |
15 |
3 |
['github-actions', 'grunweg'] |
nobody |
1-19306 1 day ago |
1-19306 1 day ago |
1-22205 1 day |
| 23881 |
YaelDillies author:YaelDillies |
feat: `ℝ≥0`-valued Lᵖ norm |
This is useful when inputting the Lp norm in places that expect a real number, like an exponent.
From LeanAPAP
---
[](https://gitpod.io/from-referrer/)
|
t-measure-probability |
220/9 |
Mathlib.lean,Mathlib/MeasureTheory/Function/LpSeminorm/Defs.lean,Mathlib/MeasureTheory/Function/LpSeminorm/NNLpNorm.lean,Mathlib/MeasureTheory/Function/LpSeminorm/TriangleInequality.lean |
4 |
13 |
['YaelDillies', 'b-mehta', 'github-actions', 'leanprover-community-bot-assistant', 'sgouezel'] |
nobody |
1-16821 1 day ago |
1-16870 1 day ago |
8-75972 8 days |
| 16408 |
Parcly-Taxel author:Parcly-Taxel |
chore: deprecate `Order.Nat` |
* Move the two `Nat` instances and `bot_eq_zero` to `Order.BoundedOrder.Basic`. We also remove the TODO relating to #13092, as it was tried and it was agreed not to be a good idea.
* Move the other two lemmas in `Order.Nat` to `Data.Nat.Find`. |
tech debt |
35/54 |
Mathlib/Algebra/IsPrimePow.lean,Mathlib/Data/Finset/Grade.lean,Mathlib/Data/Finset/Lattice/Fold.lean,Mathlib/Data/Nat/Basic.lean,Mathlib/Data/Nat/Cast/SetInterval.lean,Mathlib/Data/Nat/Find.lean,Mathlib/Data/Nat/SuccPred.lean,Mathlib/Data/Rat/Cast/Defs.lean,Mathlib/Order/BoundedOrder/Basic.lean,Mathlib/Order/Filter/AtTopBot/Basic.lean,Mathlib/Order/Nat.lean,Mathlib/RingTheory/Multiplicity.lean,Mathlib/SetTheory/Cardinal/Order.lean |
13 |
8 |
['Parcly-Taxel', 'YaelDillies', 'github-actions', 'grunweg'] |
nobody |
1-14495 1 day ago |
3-40576 3 days ago |
5-75686 5 days |
| 24164 |
ADedecker author:ADedecker |
chore: use `trichotomy_of_add_eq_add` to prove `MvPowerSeries.lexOrder_mul` |
---
[](https://gitpod.io/from-referrer/)
|
t-algebra label:t-algebra$ |
15/29 |
Mathlib/RingTheory/MvPowerSeries/LexOrder.lean,Mathlib/RingTheory/MvPowerSeries/NoZeroDivisors.lean |
2 |
1 |
['github-actions'] |
nobody |
1-12811 1 day ago |
1-12881 1 day ago |
1-12868 1 day |
| 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 |
10 |
['girving', 'github-actions', 'kebekus', 'loefflerd'] |
nobody |
1-10875 1 day ago |
38-25381 1 month ago |
42-67125 42 days |
| 22085 |
IvanRenison author:IvanRenison |
feat(Combinatorics/SimpleGraph): introduce `ConnectedComponent.toSimpleGraph` |
---
I don't know if `ConnectedComponent.Graph` is the best name for this
[](https://gitpod.io/from-referrer/)
|
t-combinatorics |
73/32 |
Mathlib/Combinatorics/SimpleGraph/Matching.lean,Mathlib/Combinatorics/SimpleGraph/Path.lean |
2 |
6 |
['IvanRenison', 'github-actions', 'leanprover-community-bot-assistant', 'pimotte'] |
nobody |
1-9146 1 day ago |
1-9340 1 day ago |
49-2659 49 days |
| 24167 |
AntoineChambert-Loir author:AntoineChambert-Loir |
Feat(Data/Fin/Tuple/Embedding): create embeddings of Fin Nat to types |
Define
* `Fin.Embedding.cons`, `Fin.Embedding.tail`
* `Fin.Embedding.snoc`, `Fin.Embedding.init`
* `Fin.Embedding.append`
analogously to `Fin.cons`, `Fin.snoc`, `Fin.append`.
---
[](https://gitpod.io/from-referrer/)
|
t-data |
160/0 |
Mathlib.lean,Mathlib/Data/Fin/Tuple/Basic.lean,Mathlib/Data/Fin/Tuple/Embedding.lean |
3 |
1 |
['github-actions'] |
nobody |
0-85806 23 hours ago |
1-8794 1 day ago |
1-8852 1 day |
| 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 |
0-83629 23 hours ago |
37-41420 1 month ago |
37-41406 37 days |
| 23542 |
kbuzzard author:kbuzzard |
chore(RingTheory/DedekindDomain/FiniteAdeleRing): refactor finite adeles |
Now we have a general theory of restricted products, we can refactor mathlib's finite adele file, removing the auxiliary results which are unused outside this file and replacing everything with much slicker proofs. Crucially, we also have a far more conceptual definition of the topology on the finite adele ring -- this is the big win. The motivation for this refactor is that the FLT project needs many more results about finite adeles (for example local compactness in the number field case) and this will be very easy to prove with this new definition (using `RestrictedProduct.locallyCompactSpace_of_addGroup`), whereas it took an entire project https://github.com/smmercuri/adele-ring_locally-compact with our current approach.
---
[](https://gitpod.io/from-referrer/)
The diff should not be taken too seriously: the file is rewritten from scratch and is a quarter the size.
I have no idea what to do about deprecations here. I have removed several results (and two definitions) because we don't want them, they were just auxiliary results needed in the old proof of `IsTopologicalRing` and were not used anywhere else; after Anatole's complete rethink of the topology he gets this result for free so my proposal pretty clearly is just to nuke the old results and constructions, while keeping the key constructions (namely the structure of topological ring). The key deletions are `FiniteIntegralAdeles` (which we can still have as `∀ v : HeightOneSpectrum R, v.adicCompletionIntegers K`) and `ProdAdicCompletions` (an auxiliary construction, which we can still have as `∀ v : HeightOneSpectrum R, v.adicCompletion K`). These auxiliary definitions were also used a little in the FLT project; https://github.com/ImperialCollegeLondon/FLT/pull/399 is the accompanying PR which is waiting on this. |
maintainer-merge
t-algebra
t-number-theory
label:t-algebra$ |
79/409 |
Mathlib/RingTheory/DedekindDomain/FiniteAdeleRing.lean,Mathlib/Topology/Algebra/RestrictedProduct.lean |
2 |
21 |
['ADedecker', 'Ruben-VandeVelde', 'github-actions', 'kbuzzard', 'loefflerd', 'mariainesdff', 'smmercuri'] |
nobody |
0-80000 22 hours ago |
0-80001 22 hours ago |
17-85503 17 days |
| 24173 |
YaelDillies author:YaelDillies |
feat: the composition of open relations is open |
[Zulip](https://leanprover.zulipchat.com/#narrow/channel/217875-Is-there-code-for-X.3F/topic/.60IsOpen.60.20and.20.60compRel.60)
---
[](https://gitpod.io/from-referrer/)
|
t-topology |
50/1 |
Mathlib/Topology/Bases.lean,Mathlib/Topology/UniformSpace/Basic.lean,Mathlib/Topology/UniformSpace/Defs.lean |
3 |
2 |
['ADedecker', 'github-actions'] |
nobody |
0-71839 19 hours ago |
0-73733 20 hours ago |
0-73786 20 hours |
| 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
|
261/2 |
Mathlib/CategoryTheory/ChosenFiniteProducts.lean |
1 |
13 |
['TwoFX', 'github-actions', 'imbrem', 'joelriou'] |
nobody |
0-66661 18 hours ago |
12-978 12 days ago |
67-40758 67 days |
| 24172 |
LessnessRandomness author:LessnessRandomness |
feat: specialize rational root theorem to usual rational numbers and integers |
Rational root theorem and integral root theorem - the special case for usual rational numbers and integers.
--- |
new-contributor
t-algebra
label:t-algebra$ |
123/0 |
Mathlib.lean,Mathlib/RingTheory/Polynomial/OfRationalNumbers/RationalRootTheorem.lean |
2 |
1 |
['github-actions'] |
nobody |
0-65184 18 hours ago |
0-75145 20 hours ago |
0-75203 20 hours |
| 24160 |
urkud author:urkud |
feat: `(-1) ^ m = (-1) ^ n` |
- add `neg_one_pow_congr`;
- prove a lemma about parity of `Fin.succAbove i j + Fin.predAbove j i`.
Backported (with adjusted API) from https://github.com/urkud/DeRhamCohomology
---
- [x] depends on: #24153
[](https://gitpod.io/from-referrer/)
|
|
24/4 |
Mathlib/Algebra/Ring/Parity.lean,Mathlib/Data/Fin/Parity.lean |
2 |
4 |
['github-actions', 'leanprover-community-bot-assistant', 'mathlib4-dependent-issues-bot', 'urkud'] |
nobody |
0-63146 17 hours ago |
0-63146 17 hours ago |
1-7625 1 day |
| 24162 |
urkud author:urkud |
feat(Calculus/BumpFunction/SmoothApprox): new file |
Reformulate theorems about density of smooth functions without measures.
---
[](https://gitpod.io/from-referrer/)
|
t-analysis |
66/0 |
Mathlib.lean,Mathlib/Analysis/Calculus/BumpFunction/SmoothApprox.lean |
2 |
1 |
['github-actions'] |
nobody |
0-62915 17 hours ago |
0-64892 18 hours ago |
1-28145 1 day |
| 24104 |
dwrensha author:dwrensha |
feat: add the strict triangle inequality for non-Wbtw points, and related lemmas |
See [this zulip thread](https://leanprover.zulipchat.com/#narrow/channel/217875-Is-there-code-for-X.3F/topic/strict.20triangle.20inequality.20in.20Euclidean.20space/near/512427539).
Co-authored-by: Eric Wieser
---
[](https://gitpod.io/from-referrer/)
|
t-analysis |
17/0 |
Mathlib/Analysis/Convex/Between.lean,Mathlib/Analysis/Convex/StrictConvexBetween.lean |
2 |
22 |
['dwrensha', 'eric-wieser', 'fpvandoorn', 'github-actions'] |
nobody |
0-62263 17 hours ago |
3-41223 3 days ago |
3-41278 3 days |
| 24182 |
mistarro author:mistarro |
refactor(FieldTheory/IntermediateField): remove instance `IntermediateField.instCoeOutSubtypeMem` |
Zulip discussion: [Working with intermediate fields of intermediate fields](https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/.E2.9C.94.20Working.20with.20intermediate.20fields.20of.20intermediate.20fields)
---
[](https://gitpod.io/from-referrer/)
|
t-algebra label:t-algebra$ |
13/21 |
Mathlib/FieldTheory/Galois/Infinite.lean,Mathlib/FieldTheory/Galois/Profinite.lean,Mathlib/FieldTheory/IntermediateField/Basic.lean |
3 |
1 |
['github-actions'] |
nobody |
0-61378 17 hours ago |
0-61378 17 hours ago |
0-61441 17 hours |
| 23558 |
JovanGerb author:JovanGerb |
feat: don't delaborate to `⊔` or `⊓` if we have a `LinearOrder` |
This PR changes the `⊔` and `⊓` notations to only be used by the delaborator if the type in question is not a linear order.
This was suggested here [#mathlib4 > max and min delaborators @ 💬](https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/max.20and.20min.20delaborators/near/500701449)
---
[](https://gitpod.io/from-referrer/)
|
large-import
maintainer-merge
t-order
t-meta
|
154/8 |
Mathlib/Order/Notation.lean,MathlibTest/Delab/SupInf.lean |
2 |
41 |
['JovanGerb', 'eric-wieser', 'fpvandoorn', 'github-actions', 'kmill'] |
kmill assignee:kmill |
0-59691 16 hours ago |
0-59691 16 hours ago |
17-50329 17 days |
| 23876 |
Thmoas-Guan author:Thmoas-Guan |
chore(RingTheory/Ideal): move associated prime |
Move associated prime into a folder for further developments.
---
[](https://gitpod.io/from-referrer/)
|
t-algebra label:t-algebra$ |
2/2 |
Mathlib.lean,Mathlib/RingTheory/Ideal/AssociatedPrime/Basic.lean,Mathlib/RingTheory/Regular/IsSMulRegular.lean |
3 |
5 |
['Ruben-VandeVelde', 'Thmoas-Guan', 'adomani', 'github-actions'] |
nobody |
0-58911 16 hours ago |
9-75032 9 days ago |
9-75104 9 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 |
118/5 |
Mathlib/AlgebraicTopology/SimplexCategory/Basic.lean,Mathlib/AlgebraicTopology/SimplicialSet/Degenerate.lean |
2 |
4 |
['gio256', 'github-actions', 'leanprover-community-bot-assistant', 'mathlib4-dependent-issues-bot'] |
nobody |
0-57838 16 hours ago |
0-58076 16 hours ago |
39-3283 39 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 |
0-56560 15 hours ago |
43-66632 1 month ago |
43-66685 43 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 |
0-56173 15 hours ago |
35-82707 1 month ago |
35-82762 35 days |
| 23972 |
Paul-Lez author:Paul-Lez |
feat(CategoryTheory/Monoidal/Mod_): add a class version of modules over monoid objects |
From Toric
---
[](https://gitpod.io/from-referrer/)
|
toric
maintainer-merge
t-category-theory
|
73/3 |
Mathlib.lean,Mathlib/CategoryTheory/Monoidal/Cartesian/Mod_.lean,Mathlib/CategoryTheory/Monoidal/Mod_.lean |
3 |
25 |
['Paul-Lez', 'YaelDillies', 'erdOne', 'github-actions'] |
nobody |
0-55372 15 hours ago |
1-49846 1 day ago |
3-68232 3 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 |
0-55147 15 hours ago |
40-63352 1 month ago |
40-63338 40 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) |
maintainer-merge
t-combinatorics
|
195/11 |
Mathlib.lean,Mathlib/Combinatorics/SimpleGraph/Connectivity/Represents.lean,Mathlib/Combinatorics/SimpleGraph/Matching.lean,Mathlib/Combinatorics/SimpleGraph/Tutte.lean,Mathlib/Combinatorics/SimpleGraph/UniversalVerts.lean,Mathlib/Data/Set/Card.lean |
6 |
47 |
['YaelDillies', 'b-mehta', 'github-actions', 'mathlib4-dependent-issues-bot', 'pimotte'] |
nobody |
0-54710 15 hours ago |
1-3475 1 day ago |
23-45238 23 days |
| 22919 |
plp127 author:plp127 |
feat(Data/Fintype/Pi): Make `Fintype` instance for `RelHom`s computable |
Makes the `Fintype` instance for rel homs 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-data |
118/32 |
Mathlib/Combinatorics/SimpleGraph/Basic.lean,Mathlib/Combinatorics/SimpleGraph/Coloring.lean,Mathlib/Combinatorics/SimpleGraph/Maps.lean,Mathlib/Data/Fintype/Pi.lean,Mathlib/Order/RelIso/Basic.lean |
5 |
17 |
['IvanRenison', 'b-mehta', 'github-actions', 'plp127'] |
b-mehta assignee:b-mehta |
0-54318 15 hours ago |
0-54318 15 hours ago |
36-2376 36 days |
| 19668 |
YaelDillies author:YaelDillies |
refactor: define `≤`/`<` on `WithBot`/`WithTop` by induction |
The motivation for this change is that it is really confusing to run `intro r s shouldnthaveintroedthat` on a goal of the form `∀ r s : ℝ≥0∞, r ≤ s` and get the nonsense-looking goal `r = ↑shouldnthaveintroedthat → ∃ b : α, s = ↑b ∧ shouldnthaveintroedthat ≤ b⟩` instead of an error, and similarly when destructing something of the form `∃ r s : ℝ≥0∞, r < s`.
Furthermore, I suspect this improves performance.
---
- [x] depends on: #20317
- [x] depends on: #20318
- [x] depends on: #21274
- [x] depends on: #22109
[](https://gitpod.io/from-referrer/)
|
t-order |
65/47 |
Mathlib/Analysis/Analytic/OfScalars.lean,Mathlib/Analysis/Oscillation.lean,Mathlib/Data/Finset/Lattice/Fold.lean,Mathlib/Data/Finset/Max.lean,Mathlib/LinearAlgebra/Eigenspace/Triangularizable.lean,Mathlib/MeasureTheory/Integral/Lebesgue/Countable.lean,Mathlib/MeasureTheory/Measure/LevyProkhorovMetric.lean,Mathlib/Order/Interval/Basic.lean,Mathlib/Order/Interval/Set/WithBotTop.lean,Mathlib/Order/WithBot.lean,Mathlib/Probability/Variance.lean,Mathlib/RingTheory/PowerBasis.lean,Mathlib/Topology/MetricSpace/Holder.lean,Mathlib/Topology/MetricSpace/HolderNorm.lean |
14 |
17 |
['YaelDillies', 'b-mehta', 'eric-wieser', 'github-actions', 'leanprover-bot', 'leanprover-community-bot-assistant', 'mathlib4-dependent-issues-bot', 'urkud'] |
nobody |
0-52453 14 hours ago |
10-26054 10 days ago |
22-60331 22 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.
---
- [x] depends on: #20825
- [x] depends on: #23808
[](https://gitpod.io/from-referrer/)
|
new-contributor
t-combinatorics
|
108/3 |
Mathlib/Combinatorics/SimpleGraph/Basic.lean,Mathlib/Combinatorics/SimpleGraph/DeleteEdges.lean,Mathlib/Combinatorics/SimpleGraph/Finite.lean |
3 |
8 |
['github-actions', 'grunweg', 'leanprover-community-bot-assistant', 'mathlib4-dependent-issues-bot', 'mitchell-horner'] |
nobody |
0-51594 14 hours ago |
0-51601 14 hours ago |
50-78030 50 days |
| 24150 |
urkud author:urkud |
refactor(Deriv/ZPow): change RHS of `iter_deriv_inv` |
---
- [ ] depends on: #24146
[](https://gitpod.io/from-referrer/)
|
|
13/4 |
Mathlib/Algebra/BigOperators/Ring/Finset.lean,Mathlib/Analysis/Calculus/Deriv/ZPow.lean |
2 |
2 |
['github-actions', 'mathlib4-dependent-issues-bot'] |
nobody |
0-51322 14 hours ago |
1-50414 1 day ago |
1-50824 1 day |
| 23413 |
robin-carlier author:robin-carlier |
feat(CategoryTheory/Join): Pseudofunctoriality of joins of categories |
Promote the constructions `C ↦ C ⋆ D` and `D ↦ C ⋆ D` to pseudofunctors from `Cat` to `Cat`. The construction is carried in a new file `CategoryTheory/Join/Pseudofunctor.lean` to reduce imports.
---
- [x] depends on: #23412
The pseudofunctoriality statements here are not the most general. The "right" statements would be
1) "pseudobifunctoriality".
2) pseudofunctoriality with values in slice bicategories.
Unfortunately, the two-categorical machinery in mathlib is not advanced enough yet to even make sense of the statements (first would require at least product bicategories, or 2-categories of pseudofunctors for a curried version, second would require slice bicategories.).
The content of this file should be upgraded once said constructions in bicategories are available, but for now I want at least to have statements that recover what we already have for `WithInitial` and `WithTerminal` rather than conditioning everything on a (probably rather long) bicategorical sidequest.
[](https://gitpod.io/from-referrer/)
|
t-category-theory |
251/0 |
Mathlib.lean,Mathlib/CategoryTheory/Join/Pseudofunctor.lean |
2 |
3 |
['github-actions', 'leanprover-community-bot-assistant', 'mathlib4-dependent-issues-bot'] |
nobody |
0-47847 13 hours ago |
0-53998 14 hours ago |
0-56556 15 hours |
| 24186 |
j-loreaux author:j-loreaux |
perf: lower priority of `ℝ≥0∞`-induced actions |
---
[](https://gitpod.io/from-referrer/)
|
awaiting-bench
t-data
|
15/10 |
Mathlib/Data/ENNReal/Action.lean |
1 |
4 |
['github-actions', 'j-loreaux', 'leanprover-bot'] |
nobody |
0-47806 13 hours ago |
0-49392 13 hours ago |
0-50930 14 hours |
| 24149 |
YaelDillies author:YaelDillies |
refactor: define the dual of a cone as a pointed cone |
We currently have two definitions of the dual of a cone:
* `Set.innerDualCone : Set H → ConvexCone ℝ H`, which is a `ConvexCone`
* `PointedCone.dual : PointedCone ℝ H → PointedCone ℝ H`
But in fact `Set.innerDualCone` is always pointed, and it's useful to talk about the dual of an arbitrary set as a `PointedCone`.
This PR unifies those constructions under a single function `PointedCone.innerDual : Set H → ConvexCone ℝ H`.
The `inner` in the name corresponds to the fact that we are turning a cone in an inner product space `H` into another cone in `H`, rather than a cone in `M` into a cone in its dual `N`. We will soon need the latter generality in the Toric project.
From Toric
---
[](https://gitpod.io/from-referrer/)
|
large-import
t-analysis
|
129/170 |
Mathlib/Analysis/Convex/Cone/Basic.lean,Mathlib/Analysis/Convex/Cone/Closure.lean,Mathlib/Analysis/Convex/Cone/InnerDual.lean,Mathlib/Analysis/Convex/Cone/Pointed.lean,Mathlib/Analysis/Convex/Cone/Proper.lean |
5 |
2 |
['YaelDillies', 'github-actions'] |
nobody |
0-46596 12 hours ago |
0-48157 13 hours ago |
0-48976 13 hours |
| 24118 |
YaelDillies author:YaelDillies |
feat: Yoneda for (comm) group objects |
And make the API between monoid and group objects more alike.
From Toric
Co-authored-by: Andrew Yang
Co-authored-by: Michał Mrugała
---
[](https://gitpod.io/from-referrer/)
|
toric
large-import
t-category-theory
|
386/227 |
Mathlib.lean,Mathlib/CategoryTheory/Monoidal/Cartesian/CommGrp.lean,Mathlib/CategoryTheory/Monoidal/Cartesian/CommMon_.lean,Mathlib/CategoryTheory/Monoidal/Cartesian/Grp_.lean,Mathlib/CategoryTheory/Monoidal/Cartesian/Mon_.lean,Mathlib/CategoryTheory/Monoidal/Yoneda.lean |
6 |
8 |
['erdOne', 'github-actions'] |
nobody |
0-44428 12 hours ago |
0-44829 12 hours ago |
1-43224 1 day |
| 24139 |
yuanyi-350 author:yuanyi-350 |
feat: add `Fin.cycleIcc` which rotates `range(i, j)` |
---
[](https://gitpod.io/from-referrer/)
|
new-contributor
t-algebra
label:t-algebra$ |
104/1 |
Mathlib/Data/Fin/Basic.lean,Mathlib/GroupTheory/Perm/Fin.lean |
2 |
7 |
['github-actions', 'mbkybky', 'yuanyi-350'] |
nobody |
0-42903 11 hours ago |
1-71999 1 day ago |
2-3645 2 days |
| 24185 |
urkud author:urkud |
feat(Prod/Lex): prove `Prod.Lex.covBy_iff` |
Also
- move the definitions of `CovBy` and `WCovBy` to `Defs/PartialOrder`;
- rename instances to use `inst*`;
- golf a proof using `aesop`.
---
[](https://gitpod.io/from-referrer/)
|
maintainer-merge
t-order
|
77/66 |
Mathlib/Algebra/Module/LinearMap/Defs.lean,Mathlib/Algebra/Module/Submodule/Map.lean,Mathlib/Data/Fin/FlagRange.lean,Mathlib/Data/Prod/Lex.lean,Mathlib/Order/Cover.lean,Mathlib/Order/Defs/PartialOrder.lean |
6 |
5 |
['YaelDillies', 'github-actions'] |
nobody |
0-41704 11 hours ago |
0-41704 11 hours ago |
0-46029 12 hours |
| 23811 |
upobir author:upobir |
feat(Data/Set/Card): add powerset cardinality formula |
---
There is no theorem in mathlbi for formula of ncard of finite powerset, but there are related formulas for finset, multiset, cardinals. This pr adds the theorem for this.
[](https://gitpod.io/from-referrer/)
|
t-data
new-contributor
|
8/0 |
Mathlib/Data/Set/Card.lean |
1 |
3 |
['b-mehta', 'github-actions', 'upobir'] |
nobody |
0-28042 7 hours ago |
0-28042 7 hours ago |
10-64475 10 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 |
180/176 |
Mathlib/AlgebraicGeometry/EllipticCurve/Affine.lean,Mathlib/AlgebraicGeometry/EllipticCurve/IsomOfJ.lean,Mathlib/AlgebraicGeometry/EllipticCurve/NormalForms.lean,Mathlib/AlgebraicGeometry/EllipticCurve/VariableChange.lean |
4 |
25 |
['Multramate', 'acmepjz', 'github-actions'] |
nobody |
0-24622 6 hours ago |
27-27001 27 days ago |
27-26987 27 days |
| 24114 |
xroblot author:xroblot |
feat(FieldTheory): add the class `IsQuadraticExtension` |
---
[](https://gitpod.io/from-referrer/)
|
t-algebra label:t-algebra$ |
71/7 |
Mathlib/FieldTheory/Fixed.lean,Mathlib/FieldTheory/Galois/Basic.lean,Mathlib/FieldTheory/Normal/Basic.lean,Mathlib/LinearAlgebra/Dimension/Finrank.lean,Mathlib/LinearAlgebra/FiniteDimensional/Basic.lean |
5 |
11 |
['faenuccio', 'github-actions', 'xroblot'] |
faenuccio assignee:faenuccio |
0-20053 5 hours ago |
2-80491 2 days ago |
2-80559 2 days |
| 24177 |
j-loreaux author:j-loreaux |
feat: generalize order properties of the Bochner integral to real ordered Banach spaces |
Currently, Mathlib only has order properties of the Bochner integral for `ℝ`-valued functions. This generalizes the fundamental results to real ordered Banach spaces. The motivation is to allow for:
```lean
variable {A : Type*} [NonUnitalCStarAlgebra A] [PartialOrder A] [StarOrderedRing A]
example {f : ℝ → A} (hf : 0 ≤ᵐ[volume] f) : 0 ≤ ∫ x, f x ∂(volume) :=
integral_nonneg_of_ae hf
```
---
- [x] depends on: #24175
- [x] depends on: #24176
[](https://gitpod.io/from-referrer/)
|
t-analysis |
72/47 |
Mathlib/MeasureTheory/Integral/Bochner/Basic.lean |
1 |
2 |
['github-actions', 'mathlib4-dependent-issues-bot'] |
nobody |
0-19868 5 hours ago |
0-20661 5 hours ago |
0-22511 6 hours |
| 24190 |
urkud author:urkud |
refactor(Calculus/MeanValue): move some theorems to `Deriv/` |
---
The code is moved as is, modulo `open` and `variable` lines. I also wrote a module docstring for the new file.
What should I do about deprecating imports etc?
[](https://gitpod.io/from-referrer/)
|
t-analysis |
536/487 |
Mathlib.lean,Mathlib/Analysis/Calculus/Deriv/MeanValue.lean,Mathlib/Analysis/Calculus/FirstDerivativeTest.lean,Mathlib/Analysis/Calculus/LHopital.lean,Mathlib/Analysis/Calculus/MeanValue.lean,Mathlib/Analysis/Calculus/Taylor.lean,Mathlib/Analysis/Convex/Deriv.lean,Mathlib/Analysis/SpecialFunctions/Pochhammer.lean,Mathlib/Analysis/SpecialFunctions/Trigonometric/Deriv.lean |
9 |
2 |
['github-actions', 'grunweg'] |
nobody |
0-17317 4 hours ago |
0-32337 8 hours ago |
0-32337 8 hours |
| 24171 |
grunweg author:grunweg |
chore: fix more mis-indented list items in doc-strings |
Continuation of #24166: this PR fixes several actually mis-formatted doc-string.
---
Best reviewed commit by commit; most diffs should be empty/very short when hiding whitespace changes.
I tried to make commit messages explain roughly what happens.
Most commits are "indent a list item, where this doesn't change formatting" (called "harmless" sometimes);
most others are "add a newline to clarify a new paragraph starts (just for easier reading).
The remaining commits either edit a doc-string very slightly, or fix actual misformatted doc-strings.
[](https://gitpod.io/from-referrer/)
|
|
589/559 |
Mathlib/Algebra/Category/Grp/EpiMono.lean,Mathlib/Algebra/Category/ModuleCat/Sheaf/Limits.lean,Mathlib/Algebra/CharZero/Defs.lean,Mathlib/Algebra/Exact.lean,Mathlib/Algebra/Module/ZLattice/Basic.lean,Mathlib/Algebra/Module/ZLattice/Covolume.lean,Mathlib/Algebra/Polynomial/EraseLead.lean,Mathlib/Algebra/Polynomial/Inductions.lean,Mathlib/Algebra/Polynomial/Laurent.lean,Mathlib/Algebra/Polynomial/Lifts.lean,Mathlib/Algebra/Polynomial/Smeval.lean,Mathlib/Analysis/BoxIntegral/UnitPartition.lean,Mathlib/Analysis/CStarAlgebra/PositiveLinearMap.lean,Mathlib/Analysis/Calculus/Rademacher.lean,Mathlib/Analysis/Calculus/Taylor.lean,Mathlib/Analysis/Complex/Conformal.lean,Mathlib/Analysis/Distribution/SchwartzSpace.lean,Mathlib/Analysis/Fourier/PoissonSummation.lean,Mathlib/Analysis/InnerProductSpace/Symmetric.lean,Mathlib/Analysis/LocallyConvex/Bounded.lean,Mathlib/Analysis/LocallyConvex/WeakDual.lean,Mathlib/Analysis/LocallyConvex/WithSeminorms.lean,Mathlib/Analysis/Normed/Group/CocompactMap.lean,Mathlib/Analysis/Normed/Group/Completeness.lean,Mathlib/Analysis/Normed/Group/SeparationQuotient.lean,Mathlib/Analysis/Normed/Module/Span.lean,Mathlib/Analysis/NormedSpace/PiTensorProduct/InjectiveSeminorm.lean,Mathlib/Analysis/NormedSpace/PiTensorProduct/ProjectiveSeminorm.lean,Mathlib/CategoryTheory/ConcreteCategory/Basic.lean,Mathlib/CategoryTheory/Distributive/Monoidal.lean,Mathlib/CategoryTheory/Equivalence.lean,Mathlib/CategoryTheory/Filtered/Basic.lean,Mathlib/CategoryTheory/Generator/Basic.lean,Mathlib/CategoryTheory/Limits/FilteredColimitCommutesFiniteLimit.lean,Mathlib/CategoryTheory/Limits/Preserves/FunctorCategory.lean,Mathlib/CategoryTheory/Limits/Shapes/Pullback/HasPullback.lean,Mathlib/CategoryTheory/Limits/Shapes/Pullback/PullbackCone.lean,Mathlib/CategoryTheory/Localization/DerivabilityStructure/Constructor.lean,Mathlib/CategoryTheory/Localization/Resolution.lean,Mathlib/CategoryTheory/Monoidal/Category.lean,Mathlib/CategoryTheory/Monoidal/Functor.lean,Mathlib/CategoryTheory/Monoidal/Limits.lean,Mathlib/CategoryTheory/MorphismProperty/Representable.lean,Mathlib/CategoryTheory/NatIso.lean,Mathlib/CategoryTheory/ObjectProperty/Basic.lean,Mathlib/CategoryTheory/Sites/ConstantSheaf.lean,Mathlib/CategoryTheory/Sites/Continuous.lean,Mathlib/CategoryTheory/Sites/CoverPreserving.lean,Mathlib/CategoryTheory/Sites/Monoidal.lean,Mathlib/CategoryTheory/Sites/NonabelianCohomology/H1.lean,Mathlib/CategoryTheory/Sites/Pullback.lean,Mathlib/CategoryTheory/SmallObject/Basic.lean,Mathlib/CategoryTheory/SmallObject/TransfiniteCompositionLifting.lean,Mathlib/CategoryTheory/Triangulated/Subcategory.lean,Mathlib/Combinatorics/Configuration.lean,Mathlib/Combinatorics/Enumerative/DyckWord.lean,Mathlib/Computability/AkraBazzi/AkraBazzi.lean,Mathlib/Data/Bracket.lean,Mathlib/Data/DFinsupp/NeLocus.lean,Mathlib/Data/List/Range.lean,Mathlib/Data/Nat/Choose/Basic.lean,Mathlib/Data/Nat/Choose/Factorization.lean,Mathlib/Data/Nat/Choose/Lucas.lean,Mathlib/Data/Nat/Factorization/Defs.lean,Mathlib/Data/Nat/PartENat.lean,Mathlib/Data/Part.lean,Mathlib/Data/Set/Basic.lean,Mathlib/Data/Setoid/Partition/Card.lean,Mathlib/Data/Sigma/Order.lean,Mathlib/Data/ZMod/Basic.lean,Mathlib/FieldTheory/AbelRuffini.lean,Mathlib/FieldTheory/AxGrothendieck.lean,Mathlib/FieldTheory/Minpoly/IsConjRoot.lean,Mathlib/FieldTheory/Separable.lean,Mathlib/Geometry/Manifold/ContMDiff/Basic.lean,Mathlib/Geometry/Manifold/IntegralCurve/Basic.lean,Mathlib/Geometry/Manifold/IntegralCurve/ExistUnique.lean,Mathlib/Geometry/Manifold/IntegralCurve/UniformTime.lean,Mathlib/Geometry/Manifold/IsManifold/ExtChartAt.lean,Mathlib/Geometry/Manifold/LocalDiffeomorph.lean,Mathlib/Geometry/Manifold/MFDeriv/UniqueDifferential.lean,Mathlib/Geometry/Manifold/VectorBundle/Tangent.lean,Mathlib/GroupTheory/Coset/Card.lean,Mathlib/GroupTheory/Finiteness.lean,Mathlib/GroupTheory/Frattini.lean,Mathlib/GroupTheory/FreeAbelianGroup.lean,Mathlib/GroupTheory/PushoutI.lean,Mathlib/GroupTheory/SpecificGroups/Alternating/Centralizer.lean,Mathlib/Lean/Meta/CongrTheorems.lean,Mathlib/LinearAlgebra/ExteriorPower/Basic.lean,Mathlib/LinearAlgebra/Lagrange.lean,Mathlib/LinearAlgebra/LinearIndependent/Defs.lean,Mathlib/LinearAlgebra/Orientation.lean,Mathlib/LinearAlgebra/Ray.lean,Mathlib/Logic/Equiv/PartialEquiv.lean,Mathlib/MeasureTheory/Category/MeasCat.lean,Mathlib/MeasureTheory/Covering/VitaliFamily.lean,Mathlib/MeasureTheory/Function/AEEqOfIntegral.lean,Mathlib/MeasureTheory/Function/ConditionalExpectation/CondexpL2.lean,Mathlib/MeasureTheory/Group/FundamentalDomain.lean |
177 |
7 |
['b-mehta', 'github-actions', 'grunweg'] |
nobody |
0-14923 4 hours ago |
0-62672 17 hours ago |
0-62667 17 hours |
| 24107 |
AntoineChambert-Loir author:AntoineChambert-Loir |
feat(GroupTheory/GroupAction/Basic): equivalences between stabilizers |
Define equivalence between stabilizers.
This is concurrent PR to #24039
with a diffferent syntax that fits better my later applications.
This one a `MulEquiv`from `stabilizer G a` to `stabilizer G b` associated with `g : G`
and an equality `hg : b = g · a`.
(The first commit gave the other direction, this one looks preferable.)
---
[](https://gitpod.io/from-referrer/)
|
t-algebra label:t-algebra$ |
93/17 |
Mathlib/Algebra/Group/End.lean,Mathlib/GroupTheory/GroupAction/Basic.lean,Mathlib/GroupTheory/GroupAction/ConjAct.lean |
3 |
1 |
['github-actions'] |
nobody |
0-12981 3 hours ago |
3-20293 3 days ago |
3-20348 3 days |
| 24184 |
YaelDillies author:YaelDillies |
feat: `[G : H]` notation for the index of `H : Subgroup G` |
This is a cute notation which I wrote for FLT. Not sure whether we want it in mathlib nor how to include `relindex` in the picture.
---
[](https://gitpod.io/from-referrer/)
|
t-algebra label:t-algebra$ |
5/0 |
Mathlib/GroupTheory/Index.lean |
1 |
4 |
['YaelDillies', 'erdOne', 'github-actions', 'j-loreaux'] |
nobody |
0-9138 2 hours ago |
0-56417 15 hours ago |
0-56482 15 hours |
| 23487 |
YaelDillies author:YaelDillies |
refactor: spell results using `Minimal`/`MinimalFor` |
From Toric
---
- [x] depends on: #23586
- [x] depends on: #23592
- [x] depends on: #23624
- [x] depends on: #23706
- [x] depends on: #23737
[](https://gitpod.io/from-referrer/)
|
toric
large-import
t-data
|
119/108 |
Mathlib/Combinatorics/Additive/Dissociation.lean,Mathlib/Combinatorics/Additive/RuzsaCovering.lean,Mathlib/Combinatorics/Colex.lean,Mathlib/Data/Fintype/EquivFin.lean,Mathlib/Data/Fintype/Order.lean,Mathlib/Data/Matroid/IndepAxioms.lean,Mathlib/Data/Set/Finite/Basic.lean,Mathlib/Order/Atoms/Finite.lean,Mathlib/Order/Birkhoff.lean,Mathlib/Order/Interval/Finset/Basic.lean,Mathlib/Order/Interval/Finset/Nat.lean,Mathlib/Order/Lattice.lean,Mathlib/Order/Minimal.lean,Mathlib/RingTheory/Polynomial/Basic.lean,Mathlib/Topology/ShrinkingLemma.lean |
15 |
10 |
['YaelDillies', 'b-mehta', 'github-actions', 'leanprover-community-bot-assistant', 'mathlib4-dependent-issues-bot'] |
nobody |
0-4974 1 hour ago |
0-4976 1 hour ago |
0-64779 17 hours |
| 24170 |
ADedecker author:ADedecker |
chore: start semilinearizing LinearAlgebra.Finsupp |
---
[](https://gitpod.io/from-referrer/)
|
t-algebra label:t-algebra$ |
63/44 |
Mathlib/Data/Finsupp/SMulWithZero.lean,Mathlib/LinearAlgebra/Finsupp/Defs.lean,Mathlib/LinearAlgebra/Finsupp/LSum.lean |
3 |
5 |
['ADedecker', 'github-actions', 'leanprover-bot'] |
nobody |
0-1224 20 minutes ago |
0-82145 22 hours ago |
0-82132 22 hours |