Are you a maintainer with just a short amount of time? The following kinds of pull requests could be relevant for you.
| 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 |
| 37057 |
erdOne author:erdOne |
feat(AlgebraicTopology): `SimplexCategory.toTop_map_δ_apply` |
---
[](https://gitpod.io/from-referrer/)
|
t-algebraic-topology
maintainer-merge
awaiting-author
merge-conflict
|
48/2 |
Mathlib/AlgebraicTopology/CechNerve.lean,Mathlib/AlgebraicTopology/SimplexCategory/Basic.lean,Mathlib/AlgebraicTopology/SimplexCategory/Defs.lean,Mathlib/AlgebraicTopology/TopologicalSimplex.lean,Mathlib/Data/Fin/SuccPred.lean |
5 |
17 |
['Raph-DG', 'dagurtomas', 'erdOne', 'github-actions', 'joelriou', 'mathlib-merge-conflicts', 'riccardobrasca'] |
robin-carlier assignee:robin-carlier |
30-29262 1 month ago |
unknown |
unknown |
| 37053 |
artie2000 author:artie2000 |
refactor(Analysis/Convex/Cone): use `PointedCone` in Riesz extension theorem |
Change the statement of the Riesz extension theorem to take a `PointedCone` rather than a `ConvexCone`.
This PR is part of a series replacing `ConvexCone` with `PointedCone`. https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/Replacing.20.60ConvexCone.60.20with.20.60PointedCone.60/near/581184307
---
[](https://gitpod.io/from-referrer/)
|
t-convex-geometry
maintainer-merge
|
15/12 |
Mathlib/Analysis/Convex/Cone/Extension.lean,Mathlib/Geometry/Convex/Cone/Pointed.lean |
2 |
8 |
['YaelDillies', 'artie2000', 'github-actions', 'mathlib-merge-conflicts', 'ocfnash'] |
nobody |
24-2804 24 days ago |
unknown |
unknown |
| 37420 |
artie2000 author:artie2000 |
refactor: change definitions to avoid `ConvexCone` |
Change the definitions of `PointedCone.positive` and `PointedCone.closure` to avoid mentioning `ConvexCone`.
This PR is part of a series deprecating `ConvexCone`: https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/Replacing.20.60ConvexCone.60.20with.20.60PointedCone.60/with/582738985
---
[](https://gitpod.io/from-referrer/)
|
t-convex-geometry
maintainer-merge
|
10/4 |
Mathlib/Analysis/Convex/Cone/Closure.lean,Mathlib/Geometry/Convex/Cone/Pointed.lean |
2 |
3 |
['YaelDillies', 'github-actions', 'mathlib-merge-conflicts', 'ooovi', 'vihdzp'] |
nobody |
22-8856 22 days ago |
unknown |
unknown |
| 36451 |
SnirBroshi author:SnirBroshi |
feat(Combinatorics/SimpleGraph/Matching): `edgeSet` is injective and strictly monotonic on matchings, and more API |
---
[](https://gitpod.io/from-referrer/)
|
t-combinatorics
maintainer-merge
|
36/10 |
Mathlib/Combinatorics/SimpleGraph/Matching.lean,Mathlib/Combinatorics/SimpleGraph/Subgraph.lean |
2 |
13 |
['SnirBroshi', 'YaelDillies', 'github-actions', 'mathlib-merge-conflicts'] |
nobody |
14-71235 14 days ago |
unknown |
unknown |
| 38093 |
mortarsanjaya author:mortarsanjaya |
feat(Algebra/Order/Ring/Unbundled/Basic): add a generalization of `two_mul_le_add_of_sq_eq_mul` |
The equality `r^2 = a * b` in the hypothesis can be weakened to `r^2 ≤ a * b`.
The implementation requires adding an appropriate `ZeroLEOneClass` instance.
---
[](https://gitpod.io/from-referrer/)
|
t-algebra
new-contributor
maintainer-merge
label:t-algebra$ |
16/7 |
Mathlib/Algebra/Order/BigOperators/Ring/Finset.lean,Mathlib/Algebra/Order/Ring/Unbundled/Basic.lean |
2 |
13 |
['github-actions', 'leanprover-radar', 'mortarsanjaya', 'themathqueen'] |
themathqueen assignee:themathqueen |
11-70109 11 days ago |
unknown |
unknown |
| 35619 |
SnirBroshi author:SnirBroshi |
feat(Combinatorics/SimpleGraph/Clique): intersection and union of cliques |
Plus a couple of lemmas.
---
[](https://gitpod.io/from-referrer/)
|
t-combinatorics
maintainer-merge
|
45/14 |
Mathlib/Combinatorics/SimpleGraph/Clique.lean,Mathlib/Combinatorics/SimpleGraph/Coloring/VertexColoring.lean,Mathlib/Data/Set/Pairwise/Basic.lean |
3 |
13 |
['SnirBroshi', 'YaelDillies', 'github-actions'] |
nobody |
9-27045 9 days ago |
unknown |
unknown |
| 37346 |
euprunin author:euprunin |
chore: golf using `grind` |
The goal of this PR is to decrease the number of times lemmas are called explicitly. Any decrease in compilation time is a welcome side effect, although it is not a primary objective.
Trace profiling results (differences <30 ms considered measurement noise):
* `✅️ SimpleGraph.Walk.IsPath.getVert_injOn`: unchanged 🎉
* `✅️ SimpleGraph.Walk.length_bypass_le`: unchanged 🎉
* `✅️ Rat.floor_intCast_div_natCast`: unchanged 🎉
* `✅️ InnerProductGeometry.norm_eq_of_angle_sub_eq_angle_sub_rev_of_angle_ne_pi`: unchanged 🎉
* `✅️ padicNorm.zero_of_padicNorm_eq_zero`: unchanged 🎉
Profiled using `set_option trace.profiler true in`.
---
[](https://gitpod.io/from-referrer/)
|
maintainer-merge
awaiting-zulip
|
7/45 |
Mathlib/Combinatorics/SimpleGraph/Paths.lean,Mathlib/Data/Rat/Floor.lean,Mathlib/Geometry/Euclidean/Triangle.lean,Mathlib/NumberTheory/Padics/PadicNorm.lean |
4 |
22 |
['FernandoChu', 'bryangingechen', 'chenson2018', 'euprunin', 'faenuccio', 'github-actions', 'grunweg'] |
nobody |
9-8104 9 days ago |
unknown |
unknown |
| 38269 |
b-mehta author:b-mehta |
feat(Combinatorics/Additive): link Freiman homs and Freiman isos tighter |
---
Some work I had lying around in a forgotten branch, recently resurrected.
[](https://gitpod.io/from-referrer/)
|
t-combinatorics
maintainer-merge
|
118/76 |
Mathlib/Combinatorics/Additive/AP/Three/Behrend.lean,Mathlib/Combinatorics/Additive/AP/Three/Defs.lean,Mathlib/Combinatorics/Additive/FreimanHom.lean |
3 |
15 |
['YaelDillies', 'b-mehta', 'github-actions', 'mathlib-merge-conflicts'] |
nobody |
9-3867 9 days ago |
unknown |
unknown |
| 37603 |
Parcly-Taxel author:Parcly-Taxel |
refactor: review of `SetSemiring` |
* Rename `Set.up` and `SetSemiring.down` to `SetSemiring.ofSet` and `SetSemiring.toSet` respectively. Unprotect both and make them equivalences, following `FreeMonoid`.
* Derive `CompleteAtomicBooleanAlgebra` for `SetSemiring` immediately.
* Add `imageHom_id` and `imageHom_comp`. The three existing lemmas about `imageHom` are coalesced into `imageHom_apply`.
Ultimately inspired by https://github.com/leanprover-community/mathlib4/pull/36934#issuecomment-4183475568. |
maintainer-merge
merge-conflict
|
120/165 |
Mathlib/Algebra/Algebra/Operations.lean,Mathlib/Data/Set/Semiring.lean |
2 |
42 |
['Parcly-Taxel', 'YaelDillies', 'eric-wieser', 'github-actions', 'mathlib-merge-conflicts', 'sgouezel'] |
nobody |
8-50840 8 days ago |
unknown |
unknown |
| 38768 |
yuanyi-350 author:yuanyi-350 |
chore(Condensed/Light/Epi): remove an erw |
Removes an `erw` that is now handled by `simp`.
Extracted from #38415
[](https://gitpod.io/from-referrer/) |
codex
t-condensed
LLM-generated
maintainer-merge
|
2/8 |
Mathlib/Condensed/Light/Epi.lean |
1 |
3 |
['dagurtomas', 'github-actions'] |
nobody |
7-81772 7 days ago |
unknown |
unknown |
| 38662 |
joelriou author:joelriou |
feat(AlgebraicTopology/SimplicialSet): faces of the boundary |
---
[](https://gitpod.io/from-referrer/)
|
t-algebraic-topology
maintainer-merge
|
67/0 |
Mathlib/AlgebraicTopology/SimplicialSet/Boundary.lean |
1 |
3 |
['dagurtomas', 'github-actions'] |
dagurtomas assignee:dagurtomas |
7-79006 7 days ago |
unknown |
unknown |
| 38314 |
pedroscortes author:pedroscortes |
feat(CategoryTheory/Monoidal): tensorμ_braid_swap and tensor-product IsCommComonObj |
## Summary
Two symmetric-monoidal coherence results:
1. `MonoidalCategory.tensorμ_braid_swap` (in `Monoidal/Braided/Basic.lean`) —
canonical rearrangement `tensorμ A A Y Y` intertwines the braiding on `A ⊗ Y`
with the pair of braidings on `A` and `Y`. Sibling of
`CategoryTheory.MonObj.mul_braiding`.
2. Tensor-product instance for `IsCommComonObj` (in `Monoidal/CommComon_.lean`):
if `A, B` carry commutative comonoid structures in a symmetric monoidal
category, so does `A ⊗ B`. Fills a gap alongside the existing
`instCommComonObjUnit` and `instIsCommComonObjOfCartesian`.
## Downstream consumer
The `IsCommComonObj` tensor-product instance is load-bearing for an external
library (markovcat, formalising Fritz–Klingler Markov categories). |
t-category-theory
new-contributor
maintainer-merge
|
15/0 |
Mathlib/CategoryTheory/Monoidal/Braided/Basic.lean,Mathlib/CategoryTheory/Monoidal/CommComon_.lean |
2 |
19 |
['dagurtomas', 'github-actions', 'joelriou', 'pedroscortes', 'robin-carlier'] |
riccardobrasca assignee:riccardobrasca |
7-73418 7 days ago |
unknown |
unknown |
| 37347 |
JovanGerb author:JovanGerb |
feat: implementation of `@[use_set_notation_for_order]` |
This PR allows the use of `⊆` notation while the underlying constant is `≤`.
Similarly for `⊂`/`<`, `⊇`/`≥` and `⊃`/`>`.
- The idea is to later extend this feature to other set notation constants, such as union/intersection.
- There are some types for which we cannot use `LE.le` as the underlying constant, such as `List` and `Multiset`. So, the elaborator for the `⊆` notation needs to make a decision which underlying constant to elaborate to, depending on the type. Sometimes the type is not known yet, which makes things awkward. Most of these cases are solved by delaying the elaboration until later when the type is known.
- However, in some cases this doesn't work either, such as `simp_rw [and_comm (_ ⊆ _)]`, where it is impossible to tell the type when elaborating the term. So, some such cases need to be fixed by making it `simp_rw [and_comm ((_ : Set _) ⊆ _)]`. This is because `simp_rw`, unlike `rw`, fully elaborates the rewrite rules before using them. A linter warns you whever there is such an ambiguity.
See also https://leanprover.zulipchat.com/#narrow/channel/113488-general/topic/Any.20infimum.20based.20version.20of.20.60OmegaCompletePartialOrder.60.3F/near/579333629
---
[](https://gitpod.io/from-referrer/)
|
t-meta
maintainer-merge
|
364/0 |
Mathlib.lean,Mathlib/Tactic.lean,Mathlib/Tactic/SetNotationForOrder.lean,MathlibTest/SetNotationForOrder.lean |
4 |
51 |
['JovanGerb', 'Vierkantor', 'github-actions', 'thorimur'] |
alexjbest and dwrensha assignee:dwrensha assignee:alexjbest |
7-46636 7 days ago |
unknown |
unknown |
| 38597 |
kim-em author:kim-em |
chore: backport robustness changes from bump/nightly-2026-04-27 |
See [#nightly-testing > nightly#213 adaptations for nightly-2026-04-27 @ 💬](https://leanprover.zulipchat.com/#narrow/channel/428973-nightly-testing/topic/nightly.23213.20adaptations.20for.20nightly-2026-04-27/near/591262169).
|
t-category-theory
maintainer-merge
|
91/26 |
Mathlib/AlgebraicTopology/SimplexCategory/Augmented/Monoidal.lean,Mathlib/CategoryTheory/Bicategory/Coherence.lean,Mathlib/CategoryTheory/Limits/Shapes/ConcreteCategory.lean,Mathlib/CategoryTheory/Limits/Shapes/Equalizers.lean,Mathlib/CategoryTheory/Monoidal/Free/Coherence.lean,Mathlib/CategoryTheory/Sites/DenseSubsite/OneHypercoverDense.lean,Mathlib/CategoryTheory/Sites/Hypercover/One.lean |
7 |
8 |
['github-actions', 'kim-em', 'robin-carlier'] |
joelriou assignee:joelriou |
7-46632 7 days ago |
unknown |
unknown |
| 37675 |
vihdzp author:vihdzp |
feat: `Order.cof Ordinal = univ` |
---
[](https://gitpod.io/from-referrer/)
|
t-set-theory
t-order
maintainer-merge
|
11/0 |
Mathlib/SetTheory/Cardinal/Cofinality.lean |
1 |
4 |
['YaelDillies', 'github-actions', 'vihdzp'] |
nobody |
7-19110 7 days ago |
unknown |
unknown |
| 37171 |
SnirBroshi author:SnirBroshi |
chore(Data/Int/Init): generalize `le_induction` from `Prop` to `Sort*` + def lemmas |
---
- Generallise `le_induction` from `Prop` to `Sort*` and rename to `leInduction`
- Add a few lemmas
- Simplify proofs using `lia`
- Move `inductionOn'_add_one`
[Zulip 💬](https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/Add.20note.20to.20help.20search.20similar.20thms/near/535331432)
[](https://gitpod.io/from-referrer/)
|
t-data
large-import
maintainer-merge
|
56/48 |
Mathlib/Data/Int/Basic.lean,Mathlib/Data/Int/Init.lean,Mathlib/GroupTheory/CoprodI.lean |
3 |
9 |
['SnirBroshi', 'github-actions', 'joneugster', 'mathlib-merge-conflicts', 'plp127'] |
joneugster assignee:joneugster |
7-16188 7 days ago |
unknown |
unknown |
| 34015 |
erdOne author:erdOne |
feat(AlgebraicGeometry): category of schemes affine over a base |
---
[](https://gitpod.io/from-referrer/)
|
t-algebraic-geometry
maintainer-merge
|
522/11 |
Mathlib.lean,Mathlib/AlgebraicGeometry/AffineOver.lean,Mathlib/AlgebraicGeometry/Limits.lean,Mathlib/AlgebraicGeometry/Morphisms/Affine.lean,Mathlib/AlgebraicGeometry/OpenImmersion.lean,Mathlib/AlgebraicGeometry/RelativeGluing.lean,Mathlib/AlgebraicGeometry/Sites/SmallAffineZariski.lean,Mathlib/CategoryTheory/Sites/Hypercover/Subcanonical.lean |
8 |
50 |
['chrisflav', 'dagurtomas', 'erdOne', 'github-actions', 'mathlib-merge-conflicts', 'mathlib4-merge-conflict-bot'] |
chrisflav assignee:chrisflav |
6-84640 6 days ago |
unknown |
unknown |
| 38665 |
joelriou author:joelriou |
feat(AlgebraicTopology/SimplicialSet): characterization of Kan complexes |
---
[](https://gitpod.io/from-referrer/)
|
t-algebraic-topology
maintainer-merge
|
92/2 |
Mathlib/AlgebraicTopology/SimplicialSet/CategoryWithFibrations.lean,Mathlib/AlgebraicTopology/SimplicialSet/KanComplex.lean |
2 |
4 |
['dagurtomas', 'github-actions', 'joelriou'] |
robin-carlier assignee:robin-carlier |
6-47096 6 days ago |
unknown |
unknown |
| 38827 |
eric-wieser author:eric-wieser |
feat: `IsEquiv` is equivalent to `Equivalence` |
Ideally we would have only one spelling of this, but in the meantime we should at least have a lemma to transport between the two spellings.
---
[](https://gitpod.io/from-referrer/)
|
easy
t-logic
t-order
maintainer-merge
|
10/0 |
Mathlib/Order/Defs/Unbundled.lean |
1 |
4 |
['SnirBroshi', 'YaelDillies', 'github-actions'] |
nobody |
6-29338 6 days ago |
unknown |
unknown |
| 37831 |
EtienneC30 author:EtienneC30 |
feat: the cardinal of a finset is an ite sum over a bigger finset |
If `s ⊆ t` then `s.card = ∑ i ∈ t, if i ∈ s then 1 else 0`.
---
[](https://gitpod.io/from-referrer/)
|
t-data
t-algebra
maintainer-merge
label:t-algebra$ |
9/2 |
Mathlib/Algebra/BigOperators/Ring/Finset.lean,Mathlib/Data/Finset/BooleanAlgebra.lean,Mathlib/Data/Finset/Filter.lean |
3 |
7 |
['EtienneC30', 'github-actions', 'robin-carlier'] |
nobody |
6-24905 6 days ago |
unknown |
unknown |
| 38794 |
YaelDillies author:YaelDillies |
feat(Algebra/Order): stronger positivity criterion for `expect` |
From AddCombi
---
[](https://gitpod.io/from-referrer/)
|
t-algebra
maintainer-merge
label:t-algebra$ |
9/10 |
Mathlib/Algebra/Order/BigOperators/Expect.lean |
1 |
6 |
['YaelDillies', 'b-mehta', 'eric-wieser', 'github-actions', 'grunweg', 'mathlib-merge-conflicts'] |
nobody |
5-26203 5 days ago |
unknown |
unknown |
| 38854 |
SnirBroshi author:SnirBroshi |
feat(Order/ConditionallyCompleteLattice/Indexed): `ciSup_mono'` for `ConditionallyCompleteLattice` |
Usually a primed version of a sup/inf theorem is the like the unprimed version but for `ConditionallyCompleteLinearOrderBot` which can remove `Nonempty` assumptions.
`ciSup_mono'` is different from its unprimed version and it's missing `ConditionallyCompleteLattice` versions.
We add these and rename `ciSup_mono'` to `ciSup_mono_of_forall_exists'`.
---
I think we should also rename the `CompleteLattice` theorems `iSup_mono'`/`iInf_mono'`/`iSup₂_mono'`/`iInf₂_mono'` to not have a prime, but that'll cause a big diff so maybe later.
[](https://gitpod.io/from-referrer/)
|
t-order
maintainer-merge
|
16/6 |
Mathlib/LinearAlgebra/Dimension/Basic.lean,Mathlib/Order/ConditionallyCompleteLattice/Indexed.lean,Mathlib/SetTheory/Cardinal/Basic.lean |
3 |
2 |
['YaelDillies', 'github-actions'] |
nobody |
5-16755 5 days ago |
unknown |
unknown |
| 38858 |
SnirBroshi author:SnirBroshi |
feat(Order/ConditionallyCompleteLattice/Basic): `ConditionallyCompleteLinearOrderBot` versions of `csSup_union`/`csSup_inter_le`/`csSup_insert` |
`ConditionallyCompleteLinearOrderBot` lets us drop all the `Set.Nonempty` assumptions.
---
[](https://gitpod.io/from-referrer/)
|
t-order
maintainer-merge
|
23/0 |
Mathlib/Order/ConditionallyCompleteLattice/Basic.lean |
1 |
2 |
['YaelDillies', 'github-actions'] |
nobody |
5-15911 5 days ago |
unknown |
unknown |
| 38358 |
yuanyi-350 author:yuanyi-350 |
doc(1000.yaml): note more formalised theorems |
---
[](https://gitpod.io/from-referrer/)
|
documentation
maintainer-merge
|
9/2 |
docs/1000.yaml |
1 |
12 |
['YaelDillies', 'github-actions', 'grunweg', 'vihdzp', 'yuanyi-350'] |
nobody |
5-15858 5 days ago |
unknown |
unknown |
| 38857 |
SnirBroshi author:SnirBroshi |
feat(Order/ConditionallyCompleteLattice/Indexed): conditional versions of `iSup_exists`/`iSup_and` |
For `iSup_exists` we can only get `≤` in `ConditionallyCompleteLattice`, and equality in `ConditionallyCompleteLinearOrderBot`.
---
[](https://gitpod.io/from-referrer/)
|
t-order
maintainer-merge
|
24/0 |
Mathlib/Order/ConditionallyCompleteLattice/Indexed.lean |
1 |
3 |
['YaelDillies', 'github-actions'] |
nobody |
5-10158 5 days ago |
unknown |
unknown |
| 38835 |
yuanyi-350 author:yuanyi-350 |
refactor(NumberTheory): golf `Mathlib/NumberTheory/Zsqrtd/GaussianInt` |
- rewrites `normSq_le_normSq_of_re_le_of_im_le` to reduce to the squared-coordinate inequalities and finish with `nlinarith`
Extracted from #38144
[](https://gitpod.io/from-referrer/) |
codex
t-number-theory
LLM-generated
maintainer-merge
|
3/5 |
Mathlib/NumberTheory/Zsqrtd/GaussianInt.lean |
1 |
9 |
['MichaelStollBayreuth', 'github-actions', 'yuanyi-350'] |
MichaelStollBayreuth assignee:MichaelStollBayreuth |
5-2123 5 days ago |
unknown |
unknown |
| 38832 |
yuanyi-350 author:yuanyi-350 |
refactor(NumberTheory): golf `Mathlib/NumberTheory/FrobeniusNumber` |
- rewrites `frobeniusNumber_pair` to use `Nat.exists_add_mul_eq_of_gcd_dvd_of_mul_pred_le` instead of constructing the witnesses via the Chinese remainder argument
- closes the final witness equality by applying `succ_inj` to the resulting additive decomposition
Extracted from #38144
[](https://gitpod.io/from-referrer/) |
codex
t-number-theory
LLM-generated
maintainer-merge
|
3/12 |
Mathlib/NumberTheory/FrobeniusNumber.lean |
1 |
3 |
['YaelDillies', 'github-actions', 'yuanyi-350'] |
tb65536 assignee:tb65536 |
4-4435 4 days ago |
unknown |
unknown |
| 35753 |
Vilin97 author:Vilin97 |
feat(Topology/Algebra/Order): regular grid helpers and piecewise linear interpolation |
Make API for piecewise linear interpolation on regular grids. I need these to for ODE time-stepping methods, like forward Euler, and later Runge–Kutta methods.
Follow-up PR: #35755 (forward Euler method convergence).
I don't know if these numerical analysis ODE-solving methods even belong in mathlib. If someone could advise me on it, I would appreciate it.
---
The initial proof was produced by [Aristotle](https://aristotle.harmonic.fun). The code was iteratively refined (factoring out lemmas, golfing, simplifying proofs) using Claude Code.
- [ ] depends on: #38091 |
t-topology
new-contributor
LLM-generated
maintainer-merge
|
201/0 |
Mathlib.lean,Mathlib/Topology/Algebra/Order/PiecewiseLinear.lean |
2 |
58 |
['Vilin97', 'YanYablonovskiy', 'adomani', 'botbaki-review', 'copilot-pull-request-reviewer', 'dagurtomas', 'eric-wieser', 'github-actions', 'grunweg', 'j-loreaux', 'mathlib-dependent-issues', 'wwylele'] |
j-loreaux assignee:j-loreaux |
3-71430 3 days ago |
unknown |
unknown |
| 37295 |
wwylele author:wwylele |
feat(Analysis/InnerProductSpace): generalized determinant of a rectangle matrix / linear map |
This is the volume factor of a linear map
---
I have encountered the expression `sqrt(det(T' * T))` a few times in various places but it doesn't look like it has a standard name and entry in mathlib, so this adds it.
Zulip thread [#Is there code for X? > (norm of) "determinant" of map between inner product spaces](https://leanprover.zulipchat.com/#narrow/channel/217875-Is-there-code-for-X.3F/topic/.28norm.20of.29.20.22determinant.22.20of.20map.20between.20inner.20product.20spaces/with/581776873)
One motivation to define this is to state volume formula under transformations. From *Measure theory and fine properties of functions*:
- Lemma 3.1: for linear map $L : \mathbb{R}^n \to \mathbb{R}^m$, we have $\mathcal{H}^n(L(A)) = [ L ] \mathcal{L}^n(A)$. This is proved in this PR at `euclideanHausdorffMeasure_image_eq_normDet_mul_volume`
- Theorem 3.8, for (not necessarily linear) $f : \mathbb{R}^n \to \mathbb{R}^m$ ($n \le m$) and $\mathcal{L}^n$-measurable set $A \subset \mathbb{R}^n$, we have $\int_A J f dx = \int_{\mathbb{R}^m} \mathcal{H}^0(A \cap f\^{-1}\{y\}) d\mathcal{H}^n(y)$, where $J f$ is the `normDet` of the rectangular Jacobian matrix
AI usage disclosure: AI was used in the following parts
- searching for related literature for an appropriate name
- generate draft proofs for some lemma to verify their correctness, though the final code has been completely rewritten by me.
- [ ] depends on: #37918
[](https://gitpod.io/from-referrer/)
|
t-analysis
maintainer-merge
|
480/0 |
Mathlib.lean,Mathlib/Analysis/InnerProductSpace/Adjoint.lean,Mathlib/Analysis/InnerProductSpace/NormDet.lean,docs/references.bib |
4 |
18 |
['copilot-pull-request-reviewer', 'github-actions', 'j-loreaux', 'mathlib-dependent-issues', 'themathqueen', 'wwylele'] |
j-loreaux assignee:j-loreaux |
3-69949 3 days ago |
unknown |
unknown |
| 37676 |
IvanRenison author:IvanRenison |
feat(Data/Finset/Preimage): add lemmas about `Equiv.symm` |
---
`Finset` version of lemmas already existing for `Set`.
[](https://gitpod.io/from-referrer/)
|
t-data
maintainer-merge
|
8/0 |
Mathlib/Data/Finset/Preimage.lean |
1 |
3 |
['github-actions', 'robin-carlier'] |
joneugster assignee:joneugster |
3-47108 3 days ago |
unknown |
unknown |
| 36913 |
joelriou author:joelriou |
feat(CategoryTheory/Monoidal): Yoneda embedding of ring objects |
(This series of PR mostly builds on previous work by the Toric project.)
---
- [x] depends on: #38366
- [x] depends on: #37587
- [x] depends on: #37167
- [x] depends on: #37265
- [x] depends on: #37263
[](https://gitpod.io/from-referrer/)
|
t-category-theory
maintainer-merge
|
84/0 |
Mathlib.lean,Mathlib/CategoryTheory/Monoidal/Cartesian/Ring.lean |
2 |
14 |
['dagurtomas', 'github-actions', 'joelriou', 'mathlib-dependent-issues', 'mathlib-merge-conflicts', 'robin-carlier'] |
robin-carlier assignee:robin-carlier |
3-26595 3 days ago |
unknown |
unknown |
| 38954 |
joelriou author:joelriou |
feat(AlgebraicTopology/DoldKan): the homotopy equivalence given by a splitting |
---
[](https://gitpod.io/from-referrer/)
|
t-algebraic-topology
maintainer-merge
|
77/4 |
Mathlib/AlgebraicTopology/DoldKan/Degeneracies.lean,Mathlib/AlgebraicTopology/DoldKan/SplitSimplicialObject.lean |
2 |
4 |
['github-actions', 'joelriou', 'robin-carlier'] |
nobody |
3-8329 3 days ago |
unknown |
unknown |
| 37858 |
tb65536 author:tb65536 |
feat(RingTheory/LocalRing/ResidueField/Fiber): `Ideal.Fiber` is a quotient of a localization |
This PR proves that `Ideal.Fiber` is a quotient of a localization. This is needed for #37130.
---
- [x] depends on: #37380
[](https://gitpod.io/from-referrer/)
|
t-ring-theory
t-algebra
maintainer-merge
label:t-algebra$ |
16/0 |
Mathlib/RingTheory/LocalRing/ResidueField/Fiber.lean |
1 |
4 |
['github-actions', 'mariainesdff', 'mathlib-dependent-issues'] |
mariainesdff assignee:mariainesdff |
3-2968 3 days ago |
unknown |
unknown |
| 38925 |
yuanyi-350 author:yuanyi-350 |
chore(ModelTheory/ElementaryMaps): remove an erw |
- rewrites `map_boundedFormula` by avoiding the `iff_eq_eq` detour and using the restricted free-variable realization lemma directly
- shortens `isElementary_of_exists` by replacing the `map_rel` `erw` with explicit `simp_rw` and `rw`
Extracted from #38415
[](https://gitpod.io/from-referrer/) |
codex
LLM-generated
t-logic
maintainer-merge
|
9/7 |
Mathlib/ModelTheory/ElementaryMaps.lean |
1 |
3 |
['github-actions', 'j-loreaux', 'loefflerd'] |
nobody |
3-2598 3 days ago |
unknown |
unknown |
| 38005 |
robin-carlier author:robin-carlier |
chore(Algebra): remove simps projections for structures of bundled objects |
I noticed that currently, adding a `@[simps]` tag to a `ModuleCat`-valued definition will generate projections for the `isModule` fields. These projections are removed. Same in `BialgCat` and `HopfAlgCat`.
---
I did not look very hard for all cases of this, but those three should be a starter.
Renaming `carrier` to `coe` will break a few things, so I opted for keeping it like this for now, feel free to disagree, but this will make the diff bigger.
[](https://gitpod.io/from-referrer/)
|
t-algebra
maintainer-merge
label:t-algebra$ |
4/0 |
Mathlib/Algebra/Category/BialgCat/Basic.lean,Mathlib/Algebra/Category/HopfAlgCat/Basic.lean,Mathlib/Algebra/Category/ModuleCat/Basic.lean,Mathlib/Algebra/Category/ModuleCat/Semi.lean |
4 |
5 |
['dagurtomas', 'github-actions', 'leanprover-radar'] |
dagurtomas assignee:dagurtomas |
2-85740 2 days ago |
unknown |
unknown |
| 38833 |
yuanyi-350 author:yuanyi-350 |
refactor(NumberTheory): golf `Mathlib/NumberTheory/EllipticDivisibilitySequence` |
- rewrites `complEDS₂_mul_b` by evaluating the parity split directly with `simp_rw` and `split_ifs`, removing the separate `Int.negInduction` proof
Extracted from #38144
[](https://gitpod.io/from-referrer/) |
codex
t-number-theory
LLM-generated
maintainer-merge
|
3/8 |
Mathlib/NumberTheory/EllipticDivisibilitySequence.lean |
1 |
3 |
['github-actions', 'loefflerd', 'yuanyi-350'] |
loefflerd assignee:loefflerd |
2-84437 2 days ago |
unknown |
unknown |
| 37869 |
mckoen author:mckoen |
feat(AlgebraicTopology/Quasicategory): inner fibrations and inner anodyne morphisms |
Defines inner fibrations, inner anodyne morphisms, and immediate results.
---
[](https://gitpod.io/from-referrer/)
|
t-algebraic-topology
maintainer-merge
|
220/0 |
Mathlib.lean,Mathlib/AlgebraicTopology/Quasicategory/Basic.lean,Mathlib/AlgebraicTopology/Quasicategory/InnerFibration.lean,Mathlib/AlgebraicTopology/SimplicialSet/AnodyneExtensions/Inner/Basic.lean |
4 |
18 |
['github-actions', 'joelriou', 'mckoen', 'robin-carlier'] |
nobody |
2-69680 2 days ago |
unknown |
unknown |
| 38414 |
chrisflav author:chrisflav |
chore(RingTheory): move `IsLocalizedModule.Away` to the `Basic` file and use it everywhere |
---
[](https://gitpod.io/from-referrer/)
|
t-ring-theory
maintainer-merge
|
42/48 |
Mathlib/Algebra/Module/FinitePresentation.lean,Mathlib/Algebra/Module/LocalizedModule/Away.lean,Mathlib/Algebra/Module/LocalizedModule/Basic.lean,Mathlib/AlgebraicGeometry/Modules/Tilde.lean,Mathlib/AlgebraicGeometry/StructureSheaf.lean,Mathlib/RingTheory/LocalProperties/Exactness.lean,Mathlib/RingTheory/LocalProperties/Submodule.lean,Mathlib/RingTheory/Localization/Finiteness.lean,Mathlib/RingTheory/Localization/Free.lean,Mathlib/RingTheory/Spectrum/Prime/FreeLocus.lean,Mathlib/RingTheory/Spectrum/Prime/Module.lean,Mathlib/RingTheory/Support.lean |
12 |
8 |
['chrisflav', 'dagurtomas', 'github-actions', 'grunweg', 'mathlib-merge-conflicts'] |
nobody |
2-65205 2 days ago |
unknown |
unknown |
| 37840 |
tb65536 author:tb65536 |
chore(RingTheory/Localization/AtPrime/Basic): use `under` instead of `comap (algebraMap R S)` |
This PR switches over from `comap (algebraMap R S)` to `under`.
---
[](https://gitpod.io/from-referrer/)
|
t-ring-theory
t-algebra
maintainer-merge
awaiting-CI
label:t-algebra$ |
172/149 |
Mathlib/AlgebraicGeometry/Noetherian.lean,Mathlib/AlgebraicGeometry/ProjectiveSpectrum/Scheme.lean,Mathlib/RingTheory/DedekindDomain/Dvr.lean,Mathlib/RingTheory/Etale/QuasiFinite.lean,Mathlib/RingTheory/Frobenius.lean,Mathlib/RingTheory/Ideal/AssociatedPrime/Localization.lean,Mathlib/RingTheory/Ideal/GoingUp.lean,Mathlib/RingTheory/Ideal/Height.lean,Mathlib/RingTheory/Ideal/KrullsHeightTheorem.lean,Mathlib/RingTheory/Ideal/MinimalPrime/Localization.lean,Mathlib/RingTheory/Ideal/Over.lean,Mathlib/RingTheory/IntegralClosure/GoingDown.lean,Mathlib/RingTheory/Jacobson/Ring.lean,Mathlib/RingTheory/KrullDimension/Polynomial.lean,Mathlib/RingTheory/LocalProperties/Injective.lean,Mathlib/RingTheory/Localization/AtPrime/Basic.lean,Mathlib/RingTheory/Localization/AtPrime/Extension.lean,Mathlib/RingTheory/Localization/Ideal.lean,Mathlib/RingTheory/QuasiFinite/Basic.lean,Mathlib/RingTheory/Spectrum/Prime/Topology.lean |
20 |
14 |
['chrisflav', 'github-actions', 'mathlib-merge-conflicts', 'robin-carlier', 'tb65536'] |
chrisflav and erdOne assignee:erdOne assignee:chrisflav |
2-65068 2 days ago |
unknown |
unknown |
| 38656 |
NoahW314 author:NoahW314 |
feat(Data/Finsupp/Weight): add `Finsupp.degree_mapDomain` |
Generalize a result by removing an unnecessary hypothesis. Also simplifies the proof.
---
[](https://gitpod.io/from-referrer/)
|
t-data
maintainer-merge
|
9/8 |
Mathlib/Data/Finsupp/Weight.lean,Mathlib/Order/Filter/TendstoCofinite.lean |
2 |
4 |
['NoahW314', 'dagurtomas', 'github-actions'] |
nobody |
2-61543 2 days ago |
unknown |
unknown |
| 38971 |
homeowmorphism author:homeowmorphism |
chore(FinitelyPresentedGroup): Use dot notation by default whenever possible and typo fix |
* Changing the usage of `IsNormalClosureFG N` to `N.IsNormalClosureFG` as the idiomatic use of the latter seems easier to read ("N is finitely generated under normal closure") and is in line with using dot notation for terms.
* Fix a typo in the main definition docstring regarding the usage of `map`: it should be `.map` instead of `_map`.
---
I used Copilot + Gemini Pro 3.1 to query about usage and took some of its suggestions.
[](https://gitpod.io/from-referrer/)
|
maintainer-merge
t-group-theory
|
7/7 |
Mathlib/GroupTheory/FinitelyPresentedGroup.lean |
1 |
2 |
['github-actions', 'tb65536'] |
tb65536 assignee:tb65536 |
2-47109 2 days ago |
unknown |
unknown |
| 37355 |
Thmoas-Guan author:Thmoas-Guan |
feat(RingTheory): refactor `smulShortComplex` |
Use `LinearMap.lsmul` for the `f` of `ModuleCat.smulShortComplex`, also providing new APIs for it.
---
[](https://gitpod.io/from-referrer/)
|
t-ring-theory
maintainer-merge
|
18/21 |
Mathlib/RingTheory/Regular/Category.lean |
1 |
21 |
['Thmoas-Guan', 'chrisflav', 'github-actions', 'robin-carlier'] |
chrisflav assignee:chrisflav |
2-44655 2 days ago |
unknown |
unknown |
| 38743 |
eric-wieser author:eric-wieser |
feat: `Finite` instances for `Sym` |
We already have the `Fintype` instances.
I take the liberty of moving these into namespaces in order to produce nicer auto-generated instance names.
---
[](https://gitpod.io/from-referrer/)
|
t-data
maintainer-merge
|
25/3 |
Mathlib/Data/Fintype/Vector.lean |
1 |
3 |
['YaelDillies', 'github-actions'] |
nobody |
2-33534 2 days ago |
unknown |
unknown |
| 38525 |
AntoineChambert-Loir author:AntoineChambert-Loir |
feat(Tactic/Translate/ToAdditive.lean): add conGen/AddConGen to the to_additive tactic |
This PR adds the pair "conGen", "AddConGen" to the additive tactic and capitalizes the second of some pairs that should have been.
---
[](https://gitpod.io/from-referrer/)
|
t-meta
maintainer-merge
|
11/10 |
Mathlib/Algebra/Exact.lean,Mathlib/GroupTheory/Congruence/Defs.lean,Mathlib/Tactic/Translate/ToAdditive.lean |
3 |
15 |
['AntoineChambert-Loir', 'JovanGerb', 'github-actions', 'mathlib-merge-conflicts', 'robin-carlier'] |
JovanGerb and dwrensha assignee:dwrensha assignee:JovanGerb |
2-12263 2 days ago |
unknown |
unknown |
| 38949 |
YaelDillies author:YaelDillies |
chore: untag duplicated `gcongr` lemmas |
Follow-up to #38793
---
[](https://gitpod.io/from-referrer/)
|
maintainer-merge |
11/9 |
Mathlib/Algebra/Module/Submodule/Basic.lean,Mathlib/Algebra/Module/Submodule/RestrictScalars.lean,Mathlib/Algebra/Order/Ring/Ordering/Basic.lean,Mathlib/Analysis/SpecialFunctions/Sigmoid.lean,Mathlib/Data/Finset/Density.lean,Mathlib/RingTheory/Localization/Submodule.lean |
6 |
3 |
['JovanGerb', 'github-actions'] |
nobody |
2-6213 2 days ago |
unknown |
unknown |
| 36376 |
jessealama author:jessealama |
feat(SimpleGraph): hamiltonian cycle from cyclic permutation |
This PR provides `IsHamiltonian.of_perm`, a bridge from `Equiv.Perm.IsCycle` to `SimpleGraph.IsHamiltonian`: if σ is a permutation that is a single cycle with full support on at least 3 elements, and each step `v → σ v` is an edge of `G`, then `G` is Hamiltonian.
### New definitions and lemmas
**`Mathlib/Data/List/Chain.lean`**:
- `IsChain.iterate`: `List.iterate f a n` is a chain under `r` whenever `r a (f a)` holds for all `a`
**`Mathlib/Data/List/Iterate.lean`**:
- `getLast_iterate`: the last element of `List.iterate f a n` is `f^[n - 1] a`
**`Mathlib/Combinatorics/SimpleGraph/Walk/Iterate.lean`** (new file):
- `Walk.iterate`: builds a walk of length `n` from `x` to `f^[n] x` for any function `f` with `G.Adj x (f x)` for all `x`, defined via `Walk.ofSupport`
- `Walk.length_iterate`, `Walk.support_iterate`, `Walk.edges_iterate`: basic API
**`Mathlib/GroupTheory/Perm/Cycle/Basic.lean`**:
- `IsCycleOn.injOn_pow_apply`: the map `n ↦ (f ^ n) a` is injective on `Finset.range #s`
**`Mathlib/GroupTheory/Perm/Cycle/Concrete.lean`**:
- `IsCycleOn.injOn_sym2_pow_apply`: the unordered-pair edge map `k ↦ s((f ^ k) a, (f ^ (k + 1)) a)` is injective on `[0, #s)` when `#s ≠ 2`
- `IsCycleOn.sym2_pow_apply_ne`: edge distinctness for cycle-on permutations — `s((f ^ k) a, (f ^ (k + 1)) a) ≠ s(a, f a)` when `k ≠ 0`, `k < #s`, and `#s ≠ 2`
- `Perm.toList_eq_range_map_pow`: expresses `toList` as a range map over powers
**`Mathlib/Combinatorics/SimpleGraph/Hamiltonian.lean`**:
- `cons_isHamiltonianCycle_iff`: a Hamiltonian path closed by an edge outside its support is a Hamiltonian cycle, and conversely
- `IsHamiltonian.of_perm`: the main theorem
---
- [x] depends on: #36307 |
t-combinatorics
maintainer-merge
|
182/0 |
Mathlib.lean,Mathlib/Combinatorics/SimpleGraph/Hamiltonian.lean,Mathlib/Combinatorics/SimpleGraph/Hamiltonian/Perm.lean,Mathlib/Combinatorics/SimpleGraph/Walk/Iterate.lean,Mathlib/Data/List/Chain.lean,Mathlib/Data/List/Iterate.lean,Mathlib/GroupTheory/Perm/Cycle/Basic.lean,Mathlib/GroupTheory/Perm/Cycle/Concrete.lean |
8 |
75 |
['SnirBroshi', 'YaelDillies', 'github-actions', 'jessealama', 'mathlib-dependent-issues', 'mathlib-merge-conflicts'] |
YaelDillies assignee:YaelDillies |
2-3964 2 days ago |
unknown |
unknown |
| 38889 |
emlis42 author:emlis42 |
chore(NumberTheory/Divisors): golf `Int.mem_divisorsAntidiag` |
This PR merges the case split and removes duplicated proofs in `Int.mem_divisorsAntidiag`. |
t-number-theory
new-contributor
maintainer-merge
|
7/36 |
Mathlib/NumberTheory/Divisors.lean |
1 |
14 |
['MichaelStollBayreuth', 'SnirBroshi', 'emlis42', 'github-actions'] |
MichaelStollBayreuth assignee:MichaelStollBayreuth |
2-1606 2 days ago |
unknown |
unknown |
| 38814 |
sharky564 author:sharky564 |
refactor(LinearAlgebra/Projection): refactor `quotientEquivOfIsCompl` via `LinearEquiv.ofLinear` |
This PR refactors `Submodule.quotientEquivOfIsCompl` to use `LinearEquiv.ofLinear` rather than `LinearEquiv.symm <| LinearEquiv.ofBijective`. The new definition makes both directions of the equivalence explicit: the forward idirection is `Submodule.liftQ` of the projection onto `q` along `p`, and the backward direction is `Submodule.mkQ` composed with the inclusion `q` in `E`.
---
The motivation is work on topological complements of submodules in PR #38547. The proof of `IsCompl.isTopCompl_iff_continuous_quotientEquiv` reduces, via the quotient-map property of `mkQ`, to identifying the composite `quotientEquivOfIsCompl ∘ mkQ` with the linear projection. This identifications feels like it should belong at the algebraic level and not mixed in with the topological reasoning. Additionally, these lemmas seem useful independently. |
t-algebra
new-contributor
maintainer-merge
label:t-algebra$ |
43/22 |
Mathlib/LinearAlgebra/Projection.lean |
1 |
27 |
['ADedecker', 'github-actions', 'sharky564', 'themathqueen'] |
nobody |
1-82498 1 day ago |
unknown |
unknown |
| 36216 |
michaellee94 author:michaellee94 |
feat(CategoryTheory): characterize pullback squares via the `Over` category |
---
[](https://gitpod.io/from-referrer/)
|
t-category-theory
new-contributor
maintainer-merge
|
47/0 |
Mathlib/CategoryTheory/Limits/Shapes/Pullback/IsPullback/Basic.lean |
1 |
18 |
['dagurtomas', 'github-actions', 'joelriou', 'michaellee94'] |
robin-carlier assignee:robin-carlier |
1-77254 1 day ago |
unknown |
unknown |
| 37406 |
vihdzp author:vihdzp |
feat(SetTheory/Cardinal): `IsStrongPrelimit` predicate |
We introduce a predicate for cardinals `c` such that `x < c` implies `x < 2 ^ c`. This is to `IsStrongLimit` as `IsSuccPrelimit` is to `IsSuccLimit`. We then make use of it in a few places where we were writing down `∀ x < c, x < 2 ^ c` explicitly.
---
[](https://gitpod.io/from-referrer/)
|
t-set-theory
maintainer-merge
|
53/26 |
Mathlib/SetTheory/Cardinal/Aleph.lean,Mathlib/SetTheory/Cardinal/Cofinality.lean,Mathlib/SetTheory/Cardinal/Order.lean,Mathlib/SetTheory/Cardinal/Regular.lean |
4 |
4 |
['YaelDillies', 'github-actions', 'mathlib-merge-conflicts', 'vihdzp'] |
alreadydone assignee:alreadydone |
1-55690 1 day ago |
unknown |
unknown |
| 37545 |
vihdzp author:vihdzp |
feat(SetTheory): ℵ_ univ = univ |
---
[](https://gitpod.io/from-referrer/)
|
t-set-theory
maintainer-merge
|
73/7 |
Mathlib/SetTheory/Cardinal/Aleph.lean,Mathlib/SetTheory/Cardinal/Regular.lean |
2 |
16 |
['YaelDillies', 'github-actions', 'mathlib-merge-conflicts', 'mattdiamond', 'plp127', 'vihdzp'] |
nobody |
1-55019 1 day ago |
unknown |
unknown |
| 38846 |
YanYablonovskiy author:YanYablonovskiy |
feat(Order): OrderType cardinality lemmas |
Adding some basic lemmas for the cardinality of an order type.
---
[](https://gitpod.io/from-referrer/)
|
new-contributor
t-order
large-import
maintainer-merge
|
28/4 |
Mathlib/Order/Types/Arithmetic.lean |
1 |
10 |
['YaelDillies', 'YanYablonovskiy', 'github-actions', 'plp127', 'vihdzp', 'wwylele'] |
YaelDillies assignee:YaelDillies |
1-37647 1 day ago |
unknown |
unknown |
| 37400 |
SnirBroshi author:SnirBroshi |
feat(Combinatorics/SimpleGraph/Acyclic): endpoints of a path have at most one neighbor in the path |
---
[](https://gitpod.io/from-referrer/)
|
t-combinatorics
maintainer-merge
|
15/0 |
Mathlib/Combinatorics/SimpleGraph/Acyclic.lean |
1 |
6 |
['Rida-Hamadani', 'Ruben-VandeVelde', 'SnirBroshi', 'bryangingechen', 'github-actions'] |
nobody |
1-35682 1 day ago |
unknown |
unknown |
| 38907 |
YaelDillies author:YaelDillies |
chore(Geometry): move `ConvexSpace` out of `LinearAlgebra` |
`ConvexSpace` is convex geometry, not linear algebra
---
[](https://gitpod.io/from-referrer/)
|
t-convex-geometry
file-removed
maintainer-merge
|
6/7 |
Mathlib.lean,Mathlib/Analysis/Convex/MetricSpace.lean,Mathlib/Geometry/Convex/ConvexSpace/AffineSpace.lean,Mathlib/Geometry/Convex/ConvexSpace/Defs.lean,Mathlib/Geometry/Convex/README.md |
5 |
5 |
['YaelDillies', 'github-actions', 'mathlib-merge-conflicts', 'themathqueen'] |
nobody |
1-31662 1 day ago |
unknown |
unknown |
| 28685 |
mitchell-horner author:mitchell-horner |
feat(Combinatorics/SimpleGraph): prove the minimal-degree version of the Erdős-Stone theorem |
Proves the minimal degree-version of the Erdős-Stone theorem:
If `G` has a minimal degree of at least `(1 - 1 / r + o(1)) * card V`, then `G` contains a copy of a `completeEquipartiteGraph` in `r + 1` parts each of size `t`.
The double-counting construction from the proof is available in `namespace ErdosStone`.
---
- [x] depends on: #25843
- [x] depends on: #27597
- [x] depends on: #27599
- [x] depends on: #28443
- [x] depends on: #28445
- [x] depends on: #28446
- [x] depends on: #28447
This is the first of several pull requests towards the full Erdős-Stone(-Simonovits) theorem, hence the name of the file.
[](https://gitpod.io/from-referrer/) |
t-combinatorics
maintainer-merge
|
329/0 |
Mathlib.lean,Mathlib/Combinatorics/SimpleGraph/Extremal/ErdosStoneSimonovits.lean |
2 |
19 |
['YaelDillies', 'b-mehta', 'github-actions', 'mathlib-dependent-issues', 'mathlib4-merge-conflict-bot', 'mitchell-horner', 'robin-carlier'] |
b-mehta assignee:b-mehta |
1-5983 1 day ago |
unknown |
unknown |
| 38370 |
FordUniver author:FordUniver |
feat(Data/Finset/Powerset): add `filter_powersetCard_subset` |
Adds `Finset.filter_powersetCard_subset` and derives `Finset.card_filter_powersetCard_subset` from it. The hypothesis `s.card ≤ n` is necessary: without it, natural subtraction silently gives `Nat.choose k 0 = 1 ≠ 0`.
Co-authored-by: Malte Jackisch
---
We ran into this while formalizing Goodman's formula on triangle densities in graphs as part of an ongoing flag algebras project in Lean, and it seemed worth upstreaming.
**Disclosure.** *This PR was developed with assistance from LLM code tools, used for Mathlib style alignment and proof compactness. The mathematical content and proof strategy originate from formalization work by Malte Jackisch (co-author) and myself; the final code has been reviewed and vouched for by both of us.* |
t-data
new-contributor
maintainer-merge
|
30/0 |
Mathlib/Data/Finset/Powerset.lean |
1 |
20 |
['FordUniver', 'YaelDillies', 'github-actions', 'mathlib-bors', 'wwylele'] |
YaelDillies assignee:YaelDillies |
1-4433 1 day ago |
unknown |
unknown |
| 38963 |
linesthatinterlace author:linesthatinterlace |
fix: rename `Pi.prod` to `Function.prod` |
Renames `Pi.prod` to `Function.prod` in order to allow for dot notation to work in the non-dependent case.
---
[](https://gitpod.io/from-referrer/)
|
large-import
maintainer-merge
|
88/74 |
Archive/Sensitivity.lean,Mathlib/Algebra/Algebra/NonUnitalHom.lean,Mathlib/Algebra/Algebra/Prod.lean,Mathlib/Algebra/BigOperators/Finprod.lean,Mathlib/Algebra/Exact.lean,Mathlib/Algebra/Group/Prod.lean,Mathlib/Algebra/Lie/Prod.lean,Mathlib/Algebra/MvPolynomial/Equiv.lean,Mathlib/Algebra/MvPolynomial/Eval.lean,Mathlib/Algebra/Notation/Pi/Defs.lean,Mathlib/Algebra/Star/StarAlgHom.lean,Mathlib/Combinatorics/Nullstellensatz.lean,Mathlib/LinearAlgebra/AffineSpace/AffineMap.lean,Mathlib/LinearAlgebra/Dimension/DivisionRing.lean,Mathlib/LinearAlgebra/Goursat.lean,Mathlib/LinearAlgebra/Prod.lean,Mathlib/LinearAlgebra/QuadraticForm/Dual.lean,Mathlib/Logic/Function/Defs.lean,Mathlib/MeasureTheory/Integral/Prod.lean,Mathlib/MeasureTheory/Measure/Prod.lean,Mathlib/NumberTheory/Height/Basic.lean,Mathlib/SetTheory/Cardinal/Finite.lean,Mathlib/Topology/Algebra/ContinuousAffineMap.lean,Mathlib/Topology/Algebra/InfiniteSum/Basic.lean,Mathlib/Topology/Algebra/InfiniteSum/Constructions.lean,Mathlib/Topology/Inseparable.lean,Mathlib/Topology/UniformSpace/LocallyUniformConvergence.lean |
27 |
4 |
['fpvandoorn', 'github-actions'] |
nobody |
1-1963 1 day ago |
unknown |
unknown |
| 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 |
| 37057 |
erdOne author:erdOne |
feat(AlgebraicTopology): `SimplexCategory.toTop_map_δ_apply` |
---
[](https://gitpod.io/from-referrer/)
|
t-algebraic-topology
maintainer-merge
awaiting-author
merge-conflict
|
48/2 |
Mathlib/AlgebraicTopology/CechNerve.lean,Mathlib/AlgebraicTopology/SimplexCategory/Basic.lean,Mathlib/AlgebraicTopology/SimplexCategory/Defs.lean,Mathlib/AlgebraicTopology/TopologicalSimplex.lean,Mathlib/Data/Fin/SuccPred.lean |
5 |
17 |
['Raph-DG', 'dagurtomas', 'erdOne', 'github-actions', 'joelriou', 'mathlib-merge-conflicts', 'riccardobrasca'] |
robin-carlier assignee:robin-carlier |
30-29262 1 month ago |
unknown |
unknown |
| 37053 |
artie2000 author:artie2000 |
refactor(Analysis/Convex/Cone): use `PointedCone` in Riesz extension theorem |
Change the statement of the Riesz extension theorem to take a `PointedCone` rather than a `ConvexCone`.
This PR is part of a series replacing `ConvexCone` with `PointedCone`. https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/Replacing.20.60ConvexCone.60.20with.20.60PointedCone.60/near/581184307
---
[](https://gitpod.io/from-referrer/)
|
t-convex-geometry
maintainer-merge
|
15/12 |
Mathlib/Analysis/Convex/Cone/Extension.lean,Mathlib/Geometry/Convex/Cone/Pointed.lean |
2 |
8 |
['YaelDillies', 'artie2000', 'github-actions', 'mathlib-merge-conflicts', 'ocfnash'] |
nobody |
24-2804 24 days ago |
unknown |
unknown |
| 37420 |
artie2000 author:artie2000 |
refactor: change definitions to avoid `ConvexCone` |
Change the definitions of `PointedCone.positive` and `PointedCone.closure` to avoid mentioning `ConvexCone`.
This PR is part of a series deprecating `ConvexCone`: https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/Replacing.20.60ConvexCone.60.20with.20.60PointedCone.60/with/582738985
---
[](https://gitpod.io/from-referrer/)
|
t-convex-geometry
maintainer-merge
|
10/4 |
Mathlib/Analysis/Convex/Cone/Closure.lean,Mathlib/Geometry/Convex/Cone/Pointed.lean |
2 |
3 |
['YaelDillies', 'github-actions', 'mathlib-merge-conflicts', 'ooovi', 'vihdzp'] |
nobody |
22-8856 22 days ago |
unknown |
unknown |
| 36451 |
SnirBroshi author:SnirBroshi |
feat(Combinatorics/SimpleGraph/Matching): `edgeSet` is injective and strictly monotonic on matchings, and more API |
---
[](https://gitpod.io/from-referrer/)
|
t-combinatorics
maintainer-merge
|
36/10 |
Mathlib/Combinatorics/SimpleGraph/Matching.lean,Mathlib/Combinatorics/SimpleGraph/Subgraph.lean |
2 |
13 |
['SnirBroshi', 'YaelDillies', 'github-actions', 'mathlib-merge-conflicts'] |
nobody |
14-71235 14 days ago |
unknown |
unknown |
| 38093 |
mortarsanjaya author:mortarsanjaya |
feat(Algebra/Order/Ring/Unbundled/Basic): add a generalization of `two_mul_le_add_of_sq_eq_mul` |
The equality `r^2 = a * b` in the hypothesis can be weakened to `r^2 ≤ a * b`.
The implementation requires adding an appropriate `ZeroLEOneClass` instance.
---
[](https://gitpod.io/from-referrer/)
|
t-algebra
new-contributor
maintainer-merge
label:t-algebra$ |
16/7 |
Mathlib/Algebra/Order/BigOperators/Ring/Finset.lean,Mathlib/Algebra/Order/Ring/Unbundled/Basic.lean |
2 |
13 |
['github-actions', 'leanprover-radar', 'mortarsanjaya', 'themathqueen'] |
themathqueen assignee:themathqueen |
11-70109 11 days ago |
unknown |
unknown |
| 35619 |
SnirBroshi author:SnirBroshi |
feat(Combinatorics/SimpleGraph/Clique): intersection and union of cliques |
Plus a couple of lemmas.
---
[](https://gitpod.io/from-referrer/)
|
t-combinatorics
maintainer-merge
|
45/14 |
Mathlib/Combinatorics/SimpleGraph/Clique.lean,Mathlib/Combinatorics/SimpleGraph/Coloring/VertexColoring.lean,Mathlib/Data/Set/Pairwise/Basic.lean |
3 |
13 |
['SnirBroshi', 'YaelDillies', 'github-actions'] |
nobody |
9-27045 9 days ago |
unknown |
unknown |
| 37346 |
euprunin author:euprunin |
chore: golf using `grind` |
The goal of this PR is to decrease the number of times lemmas are called explicitly. Any decrease in compilation time is a welcome side effect, although it is not a primary objective.
Trace profiling results (differences <30 ms considered measurement noise):
* `✅️ SimpleGraph.Walk.IsPath.getVert_injOn`: unchanged 🎉
* `✅️ SimpleGraph.Walk.length_bypass_le`: unchanged 🎉
* `✅️ Rat.floor_intCast_div_natCast`: unchanged 🎉
* `✅️ InnerProductGeometry.norm_eq_of_angle_sub_eq_angle_sub_rev_of_angle_ne_pi`: unchanged 🎉
* `✅️ padicNorm.zero_of_padicNorm_eq_zero`: unchanged 🎉
Profiled using `set_option trace.profiler true in`.
---
[](https://gitpod.io/from-referrer/)
|
maintainer-merge
awaiting-zulip
|
7/45 |
Mathlib/Combinatorics/SimpleGraph/Paths.lean,Mathlib/Data/Rat/Floor.lean,Mathlib/Geometry/Euclidean/Triangle.lean,Mathlib/NumberTheory/Padics/PadicNorm.lean |
4 |
22 |
['FernandoChu', 'bryangingechen', 'chenson2018', 'euprunin', 'faenuccio', 'github-actions', 'grunweg'] |
nobody |
9-8104 9 days ago |
unknown |
unknown |
| 38269 |
b-mehta author:b-mehta |
feat(Combinatorics/Additive): link Freiman homs and Freiman isos tighter |
---
Some work I had lying around in a forgotten branch, recently resurrected.
[](https://gitpod.io/from-referrer/)
|
t-combinatorics
maintainer-merge
|
118/76 |
Mathlib/Combinatorics/Additive/AP/Three/Behrend.lean,Mathlib/Combinatorics/Additive/AP/Three/Defs.lean,Mathlib/Combinatorics/Additive/FreimanHom.lean |
3 |
15 |
['YaelDillies', 'b-mehta', 'github-actions', 'mathlib-merge-conflicts'] |
nobody |
9-3867 9 days ago |
unknown |
unknown |
| 37603 |
Parcly-Taxel author:Parcly-Taxel |
refactor: review of `SetSemiring` |
* Rename `Set.up` and `SetSemiring.down` to `SetSemiring.ofSet` and `SetSemiring.toSet` respectively. Unprotect both and make them equivalences, following `FreeMonoid`.
* Derive `CompleteAtomicBooleanAlgebra` for `SetSemiring` immediately.
* Add `imageHom_id` and `imageHom_comp`. The three existing lemmas about `imageHom` are coalesced into `imageHom_apply`.
Ultimately inspired by https://github.com/leanprover-community/mathlib4/pull/36934#issuecomment-4183475568. |
maintainer-merge
merge-conflict
|
120/165 |
Mathlib/Algebra/Algebra/Operations.lean,Mathlib/Data/Set/Semiring.lean |
2 |
42 |
['Parcly-Taxel', 'YaelDillies', 'eric-wieser', 'github-actions', 'mathlib-merge-conflicts', 'sgouezel'] |
nobody |
8-50840 8 days ago |
unknown |
unknown |
| 38768 |
yuanyi-350 author:yuanyi-350 |
chore(Condensed/Light/Epi): remove an erw |
Removes an `erw` that is now handled by `simp`.
Extracted from #38415
[](https://gitpod.io/from-referrer/) |
codex
t-condensed
LLM-generated
maintainer-merge
|
2/8 |
Mathlib/Condensed/Light/Epi.lean |
1 |
3 |
['dagurtomas', 'github-actions'] |
nobody |
7-81772 7 days ago |
unknown |
unknown |
| 38662 |
joelriou author:joelriou |
feat(AlgebraicTopology/SimplicialSet): faces of the boundary |
---
[](https://gitpod.io/from-referrer/)
|
t-algebraic-topology
maintainer-merge
|
67/0 |
Mathlib/AlgebraicTopology/SimplicialSet/Boundary.lean |
1 |
3 |
['dagurtomas', 'github-actions'] |
dagurtomas assignee:dagurtomas |
7-79006 7 days ago |
unknown |
unknown |
| 38314 |
pedroscortes author:pedroscortes |
feat(CategoryTheory/Monoidal): tensorμ_braid_swap and tensor-product IsCommComonObj |
## Summary
Two symmetric-monoidal coherence results:
1. `MonoidalCategory.tensorμ_braid_swap` (in `Monoidal/Braided/Basic.lean`) —
canonical rearrangement `tensorμ A A Y Y` intertwines the braiding on `A ⊗ Y`
with the pair of braidings on `A` and `Y`. Sibling of
`CategoryTheory.MonObj.mul_braiding`.
2. Tensor-product instance for `IsCommComonObj` (in `Monoidal/CommComon_.lean`):
if `A, B` carry commutative comonoid structures in a symmetric monoidal
category, so does `A ⊗ B`. Fills a gap alongside the existing
`instCommComonObjUnit` and `instIsCommComonObjOfCartesian`.
## Downstream consumer
The `IsCommComonObj` tensor-product instance is load-bearing for an external
library (markovcat, formalising Fritz–Klingler Markov categories). |
t-category-theory
new-contributor
maintainer-merge
|
15/0 |
Mathlib/CategoryTheory/Monoidal/Braided/Basic.lean,Mathlib/CategoryTheory/Monoidal/CommComon_.lean |
2 |
19 |
['dagurtomas', 'github-actions', 'joelriou', 'pedroscortes', 'robin-carlier'] |
riccardobrasca assignee:riccardobrasca |
7-73418 7 days ago |
unknown |
unknown |
| 37347 |
JovanGerb author:JovanGerb |
feat: implementation of `@[use_set_notation_for_order]` |
This PR allows the use of `⊆` notation while the underlying constant is `≤`.
Similarly for `⊂`/`<`, `⊇`/`≥` and `⊃`/`>`.
- The idea is to later extend this feature to other set notation constants, such as union/intersection.
- There are some types for which we cannot use `LE.le` as the underlying constant, such as `List` and `Multiset`. So, the elaborator for the `⊆` notation needs to make a decision which underlying constant to elaborate to, depending on the type. Sometimes the type is not known yet, which makes things awkward. Most of these cases are solved by delaying the elaboration until later when the type is known.
- However, in some cases this doesn't work either, such as `simp_rw [and_comm (_ ⊆ _)]`, where it is impossible to tell the type when elaborating the term. So, some such cases need to be fixed by making it `simp_rw [and_comm ((_ : Set _) ⊆ _)]`. This is because `simp_rw`, unlike `rw`, fully elaborates the rewrite rules before using them. A linter warns you whever there is such an ambiguity.
See also https://leanprover.zulipchat.com/#narrow/channel/113488-general/topic/Any.20infimum.20based.20version.20of.20.60OmegaCompletePartialOrder.60.3F/near/579333629
---
[](https://gitpod.io/from-referrer/)
|
t-meta
maintainer-merge
|
364/0 |
Mathlib.lean,Mathlib/Tactic.lean,Mathlib/Tactic/SetNotationForOrder.lean,MathlibTest/SetNotationForOrder.lean |
4 |
51 |
['JovanGerb', 'Vierkantor', 'github-actions', 'thorimur'] |
alexjbest and dwrensha assignee:dwrensha assignee:alexjbest |
7-46636 7 days ago |
unknown |
unknown |
| 38597 |
kim-em author:kim-em |
chore: backport robustness changes from bump/nightly-2026-04-27 |
See [#nightly-testing > nightly#213 adaptations for nightly-2026-04-27 @ 💬](https://leanprover.zulipchat.com/#narrow/channel/428973-nightly-testing/topic/nightly.23213.20adaptations.20for.20nightly-2026-04-27/near/591262169).
|
t-category-theory
maintainer-merge
|
91/26 |
Mathlib/AlgebraicTopology/SimplexCategory/Augmented/Monoidal.lean,Mathlib/CategoryTheory/Bicategory/Coherence.lean,Mathlib/CategoryTheory/Limits/Shapes/ConcreteCategory.lean,Mathlib/CategoryTheory/Limits/Shapes/Equalizers.lean,Mathlib/CategoryTheory/Monoidal/Free/Coherence.lean,Mathlib/CategoryTheory/Sites/DenseSubsite/OneHypercoverDense.lean,Mathlib/CategoryTheory/Sites/Hypercover/One.lean |
7 |
8 |
['github-actions', 'kim-em', 'robin-carlier'] |
joelriou assignee:joelriou |
7-46632 7 days ago |
unknown |
unknown |
| 37675 |
vihdzp author:vihdzp |
feat: `Order.cof Ordinal = univ` |
---
[](https://gitpod.io/from-referrer/)
|
t-set-theory
t-order
maintainer-merge
|
11/0 |
Mathlib/SetTheory/Cardinal/Cofinality.lean |
1 |
4 |
['YaelDillies', 'github-actions', 'vihdzp'] |
nobody |
7-19110 7 days ago |
unknown |
unknown |
| 37171 |
SnirBroshi author:SnirBroshi |
chore(Data/Int/Init): generalize `le_induction` from `Prop` to `Sort*` + def lemmas |
---
- Generallise `le_induction` from `Prop` to `Sort*` and rename to `leInduction`
- Add a few lemmas
- Simplify proofs using `lia`
- Move `inductionOn'_add_one`
[Zulip 💬](https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/Add.20note.20to.20help.20search.20similar.20thms/near/535331432)
[](https://gitpod.io/from-referrer/)
|
t-data
large-import
maintainer-merge
|
56/48 |
Mathlib/Data/Int/Basic.lean,Mathlib/Data/Int/Init.lean,Mathlib/GroupTheory/CoprodI.lean |
3 |
9 |
['SnirBroshi', 'github-actions', 'joneugster', 'mathlib-merge-conflicts', 'plp127'] |
joneugster assignee:joneugster |
7-16188 7 days ago |
unknown |
unknown |
| 34015 |
erdOne author:erdOne |
feat(AlgebraicGeometry): category of schemes affine over a base |
---
[](https://gitpod.io/from-referrer/)
|
t-algebraic-geometry
maintainer-merge
|
522/11 |
Mathlib.lean,Mathlib/AlgebraicGeometry/AffineOver.lean,Mathlib/AlgebraicGeometry/Limits.lean,Mathlib/AlgebraicGeometry/Morphisms/Affine.lean,Mathlib/AlgebraicGeometry/OpenImmersion.lean,Mathlib/AlgebraicGeometry/RelativeGluing.lean,Mathlib/AlgebraicGeometry/Sites/SmallAffineZariski.lean,Mathlib/CategoryTheory/Sites/Hypercover/Subcanonical.lean |
8 |
50 |
['chrisflav', 'dagurtomas', 'erdOne', 'github-actions', 'mathlib-merge-conflicts', 'mathlib4-merge-conflict-bot'] |
chrisflav assignee:chrisflav |
6-84640 6 days ago |
unknown |
unknown |
| 38665 |
joelriou author:joelriou |
feat(AlgebraicTopology/SimplicialSet): characterization of Kan complexes |
---
[](https://gitpod.io/from-referrer/)
|
t-algebraic-topology
maintainer-merge
|
92/2 |
Mathlib/AlgebraicTopology/SimplicialSet/CategoryWithFibrations.lean,Mathlib/AlgebraicTopology/SimplicialSet/KanComplex.lean |
2 |
4 |
['dagurtomas', 'github-actions', 'joelriou'] |
robin-carlier assignee:robin-carlier |
6-47096 6 days ago |
unknown |
unknown |
| 38827 |
eric-wieser author:eric-wieser |
feat: `IsEquiv` is equivalent to `Equivalence` |
Ideally we would have only one spelling of this, but in the meantime we should at least have a lemma to transport between the two spellings.
---
[](https://gitpod.io/from-referrer/)
|
easy
t-logic
t-order
maintainer-merge
|
10/0 |
Mathlib/Order/Defs/Unbundled.lean |
1 |
4 |
['SnirBroshi', 'YaelDillies', 'github-actions'] |
nobody |
6-29338 6 days ago |
unknown |
unknown |
| 37831 |
EtienneC30 author:EtienneC30 |
feat: the cardinal of a finset is an ite sum over a bigger finset |
If `s ⊆ t` then `s.card = ∑ i ∈ t, if i ∈ s then 1 else 0`.
---
[](https://gitpod.io/from-referrer/)
|
t-data
t-algebra
maintainer-merge
label:t-algebra$ |
9/2 |
Mathlib/Algebra/BigOperators/Ring/Finset.lean,Mathlib/Data/Finset/BooleanAlgebra.lean,Mathlib/Data/Finset/Filter.lean |
3 |
7 |
['EtienneC30', 'github-actions', 'robin-carlier'] |
nobody |
6-24905 6 days ago |
unknown |
unknown |
| 38794 |
YaelDillies author:YaelDillies |
feat(Algebra/Order): stronger positivity criterion for `expect` |
From AddCombi
---
[](https://gitpod.io/from-referrer/)
|
t-algebra
maintainer-merge
label:t-algebra$ |
9/10 |
Mathlib/Algebra/Order/BigOperators/Expect.lean |
1 |
6 |
['YaelDillies', 'b-mehta', 'eric-wieser', 'github-actions', 'grunweg', 'mathlib-merge-conflicts'] |
nobody |
5-26203 5 days ago |
unknown |
unknown |
| 38854 |
SnirBroshi author:SnirBroshi |
feat(Order/ConditionallyCompleteLattice/Indexed): `ciSup_mono'` for `ConditionallyCompleteLattice` |
Usually a primed version of a sup/inf theorem is the like the unprimed version but for `ConditionallyCompleteLinearOrderBot` which can remove `Nonempty` assumptions.
`ciSup_mono'` is different from its unprimed version and it's missing `ConditionallyCompleteLattice` versions.
We add these and rename `ciSup_mono'` to `ciSup_mono_of_forall_exists'`.
---
I think we should also rename the `CompleteLattice` theorems `iSup_mono'`/`iInf_mono'`/`iSup₂_mono'`/`iInf₂_mono'` to not have a prime, but that'll cause a big diff so maybe later.
[](https://gitpod.io/from-referrer/)
|
t-order
maintainer-merge
|
16/6 |
Mathlib/LinearAlgebra/Dimension/Basic.lean,Mathlib/Order/ConditionallyCompleteLattice/Indexed.lean,Mathlib/SetTheory/Cardinal/Basic.lean |
3 |
2 |
['YaelDillies', 'github-actions'] |
nobody |
5-16755 5 days ago |
unknown |
unknown |
| 38858 |
SnirBroshi author:SnirBroshi |
feat(Order/ConditionallyCompleteLattice/Basic): `ConditionallyCompleteLinearOrderBot` versions of `csSup_union`/`csSup_inter_le`/`csSup_insert` |
`ConditionallyCompleteLinearOrderBot` lets us drop all the `Set.Nonempty` assumptions.
---
[](https://gitpod.io/from-referrer/)
|
t-order
maintainer-merge
|
23/0 |
Mathlib/Order/ConditionallyCompleteLattice/Basic.lean |
1 |
2 |
['YaelDillies', 'github-actions'] |
nobody |
5-15911 5 days ago |
unknown |
unknown |
| 38358 |
yuanyi-350 author:yuanyi-350 |
doc(1000.yaml): note more formalised theorems |
---
[](https://gitpod.io/from-referrer/)
|
documentation
maintainer-merge
|
9/2 |
docs/1000.yaml |
1 |
12 |
['YaelDillies', 'github-actions', 'grunweg', 'vihdzp', 'yuanyi-350'] |
nobody |
5-15858 5 days ago |
unknown |
unknown |
| 38857 |
SnirBroshi author:SnirBroshi |
feat(Order/ConditionallyCompleteLattice/Indexed): conditional versions of `iSup_exists`/`iSup_and` |
For `iSup_exists` we can only get `≤` in `ConditionallyCompleteLattice`, and equality in `ConditionallyCompleteLinearOrderBot`.
---
[](https://gitpod.io/from-referrer/)
|
t-order
maintainer-merge
|
24/0 |
Mathlib/Order/ConditionallyCompleteLattice/Indexed.lean |
1 |
3 |
['YaelDillies', 'github-actions'] |
nobody |
5-10158 5 days ago |
unknown |
unknown |
| 38835 |
yuanyi-350 author:yuanyi-350 |
refactor(NumberTheory): golf `Mathlib/NumberTheory/Zsqrtd/GaussianInt` |
- rewrites `normSq_le_normSq_of_re_le_of_im_le` to reduce to the squared-coordinate inequalities and finish with `nlinarith`
Extracted from #38144
[](https://gitpod.io/from-referrer/) |
codex
t-number-theory
LLM-generated
maintainer-merge
|
3/5 |
Mathlib/NumberTheory/Zsqrtd/GaussianInt.lean |
1 |
9 |
['MichaelStollBayreuth', 'github-actions', 'yuanyi-350'] |
MichaelStollBayreuth assignee:MichaelStollBayreuth |
5-2123 5 days ago |
unknown |
unknown |
| 38832 |
yuanyi-350 author:yuanyi-350 |
refactor(NumberTheory): golf `Mathlib/NumberTheory/FrobeniusNumber` |
- rewrites `frobeniusNumber_pair` to use `Nat.exists_add_mul_eq_of_gcd_dvd_of_mul_pred_le` instead of constructing the witnesses via the Chinese remainder argument
- closes the final witness equality by applying `succ_inj` to the resulting additive decomposition
Extracted from #38144
[](https://gitpod.io/from-referrer/) |
codex
t-number-theory
LLM-generated
maintainer-merge
|
3/12 |
Mathlib/NumberTheory/FrobeniusNumber.lean |
1 |
3 |
['YaelDillies', 'github-actions', 'yuanyi-350'] |
tb65536 assignee:tb65536 |
4-4435 4 days ago |
unknown |
unknown |
| 35753 |
Vilin97 author:Vilin97 |
feat(Topology/Algebra/Order): regular grid helpers and piecewise linear interpolation |
Make API for piecewise linear interpolation on regular grids. I need these to for ODE time-stepping methods, like forward Euler, and later Runge–Kutta methods.
Follow-up PR: #35755 (forward Euler method convergence).
I don't know if these numerical analysis ODE-solving methods even belong in mathlib. If someone could advise me on it, I would appreciate it.
---
The initial proof was produced by [Aristotle](https://aristotle.harmonic.fun). The code was iteratively refined (factoring out lemmas, golfing, simplifying proofs) using Claude Code.
- [ ] depends on: #38091 |
t-topology
new-contributor
LLM-generated
maintainer-merge
|
201/0 |
Mathlib.lean,Mathlib/Topology/Algebra/Order/PiecewiseLinear.lean |
2 |
58 |
['Vilin97', 'YanYablonovskiy', 'adomani', 'botbaki-review', 'copilot-pull-request-reviewer', 'dagurtomas', 'eric-wieser', 'github-actions', 'grunweg', 'j-loreaux', 'mathlib-dependent-issues', 'wwylele'] |
j-loreaux assignee:j-loreaux |
3-71430 3 days ago |
unknown |
unknown |
| 37295 |
wwylele author:wwylele |
feat(Analysis/InnerProductSpace): generalized determinant of a rectangle matrix / linear map |
This is the volume factor of a linear map
---
I have encountered the expression `sqrt(det(T' * T))` a few times in various places but it doesn't look like it has a standard name and entry in mathlib, so this adds it.
Zulip thread [#Is there code for X? > (norm of) "determinant" of map between inner product spaces](https://leanprover.zulipchat.com/#narrow/channel/217875-Is-there-code-for-X.3F/topic/.28norm.20of.29.20.22determinant.22.20of.20map.20between.20inner.20product.20spaces/with/581776873)
One motivation to define this is to state volume formula under transformations. From *Measure theory and fine properties of functions*:
- Lemma 3.1: for linear map $L : \mathbb{R}^n \to \mathbb{R}^m$, we have $\mathcal{H}^n(L(A)) = [ L ] \mathcal{L}^n(A)$. This is proved in this PR at `euclideanHausdorffMeasure_image_eq_normDet_mul_volume`
- Theorem 3.8, for (not necessarily linear) $f : \mathbb{R}^n \to \mathbb{R}^m$ ($n \le m$) and $\mathcal{L}^n$-measurable set $A \subset \mathbb{R}^n$, we have $\int_A J f dx = \int_{\mathbb{R}^m} \mathcal{H}^0(A \cap f\^{-1}\{y\}) d\mathcal{H}^n(y)$, where $J f$ is the `normDet` of the rectangular Jacobian matrix
AI usage disclosure: AI was used in the following parts
- searching for related literature for an appropriate name
- generate draft proofs for some lemma to verify their correctness, though the final code has been completely rewritten by me.
- [ ] depends on: #37918
[](https://gitpod.io/from-referrer/)
|
t-analysis
maintainer-merge
|
480/0 |
Mathlib.lean,Mathlib/Analysis/InnerProductSpace/Adjoint.lean,Mathlib/Analysis/InnerProductSpace/NormDet.lean,docs/references.bib |
4 |
18 |
['copilot-pull-request-reviewer', 'github-actions', 'j-loreaux', 'mathlib-dependent-issues', 'themathqueen', 'wwylele'] |
j-loreaux assignee:j-loreaux |
3-69949 3 days ago |
unknown |
unknown |
| 37676 |
IvanRenison author:IvanRenison |
feat(Data/Finset/Preimage): add lemmas about `Equiv.symm` |
---
`Finset` version of lemmas already existing for `Set`.
[](https://gitpod.io/from-referrer/)
|
t-data
maintainer-merge
|
8/0 |
Mathlib/Data/Finset/Preimage.lean |
1 |
3 |
['github-actions', 'robin-carlier'] |
joneugster assignee:joneugster |
3-47108 3 days ago |
unknown |
unknown |
| 36913 |
joelriou author:joelriou |
feat(CategoryTheory/Monoidal): Yoneda embedding of ring objects |
(This series of PR mostly builds on previous work by the Toric project.)
---
- [x] depends on: #38366
- [x] depends on: #37587
- [x] depends on: #37167
- [x] depends on: #37265
- [x] depends on: #37263
[](https://gitpod.io/from-referrer/)
|
t-category-theory
maintainer-merge
|
84/0 |
Mathlib.lean,Mathlib/CategoryTheory/Monoidal/Cartesian/Ring.lean |
2 |
14 |
['dagurtomas', 'github-actions', 'joelriou', 'mathlib-dependent-issues', 'mathlib-merge-conflicts', 'robin-carlier'] |
robin-carlier assignee:robin-carlier |
3-26595 3 days ago |
unknown |
unknown |
| 38954 |
joelriou author:joelriou |
feat(AlgebraicTopology/DoldKan): the homotopy equivalence given by a splitting |
---
[](https://gitpod.io/from-referrer/)
|
t-algebraic-topology
maintainer-merge
|
77/4 |
Mathlib/AlgebraicTopology/DoldKan/Degeneracies.lean,Mathlib/AlgebraicTopology/DoldKan/SplitSimplicialObject.lean |
2 |
4 |
['github-actions', 'joelriou', 'robin-carlier'] |
nobody |
3-8329 3 days ago |
unknown |
unknown |
| 37858 |
tb65536 author:tb65536 |
feat(RingTheory/LocalRing/ResidueField/Fiber): `Ideal.Fiber` is a quotient of a localization |
This PR proves that `Ideal.Fiber` is a quotient of a localization. This is needed for #37130.
---
- [x] depends on: #37380
[](https://gitpod.io/from-referrer/)
|
t-ring-theory
t-algebra
maintainer-merge
label:t-algebra$ |
16/0 |
Mathlib/RingTheory/LocalRing/ResidueField/Fiber.lean |
1 |
4 |
['github-actions', 'mariainesdff', 'mathlib-dependent-issues'] |
mariainesdff assignee:mariainesdff |
3-2968 3 days ago |
unknown |
unknown |
| 38925 |
yuanyi-350 author:yuanyi-350 |
chore(ModelTheory/ElementaryMaps): remove an erw |
- rewrites `map_boundedFormula` by avoiding the `iff_eq_eq` detour and using the restricted free-variable realization lemma directly
- shortens `isElementary_of_exists` by replacing the `map_rel` `erw` with explicit `simp_rw` and `rw`
Extracted from #38415
[](https://gitpod.io/from-referrer/) |
codex
LLM-generated
t-logic
maintainer-merge
|
9/7 |
Mathlib/ModelTheory/ElementaryMaps.lean |
1 |
3 |
['github-actions', 'j-loreaux', 'loefflerd'] |
nobody |
3-2598 3 days ago |
unknown |
unknown |
| 38005 |
robin-carlier author:robin-carlier |
chore(Algebra): remove simps projections for structures of bundled objects |
I noticed that currently, adding a `@[simps]` tag to a `ModuleCat`-valued definition will generate projections for the `isModule` fields. These projections are removed. Same in `BialgCat` and `HopfAlgCat`.
---
I did not look very hard for all cases of this, but those three should be a starter.
Renaming `carrier` to `coe` will break a few things, so I opted for keeping it like this for now, feel free to disagree, but this will make the diff bigger.
[](https://gitpod.io/from-referrer/)
|
t-algebra
maintainer-merge
label:t-algebra$ |
4/0 |
Mathlib/Algebra/Category/BialgCat/Basic.lean,Mathlib/Algebra/Category/HopfAlgCat/Basic.lean,Mathlib/Algebra/Category/ModuleCat/Basic.lean,Mathlib/Algebra/Category/ModuleCat/Semi.lean |
4 |
5 |
['dagurtomas', 'github-actions', 'leanprover-radar'] |
dagurtomas assignee:dagurtomas |
2-85740 2 days ago |
unknown |
unknown |
| 38833 |
yuanyi-350 author:yuanyi-350 |
refactor(NumberTheory): golf `Mathlib/NumberTheory/EllipticDivisibilitySequence` |
- rewrites `complEDS₂_mul_b` by evaluating the parity split directly with `simp_rw` and `split_ifs`, removing the separate `Int.negInduction` proof
Extracted from #38144
[](https://gitpod.io/from-referrer/) |
codex
t-number-theory
LLM-generated
maintainer-merge
|
3/8 |
Mathlib/NumberTheory/EllipticDivisibilitySequence.lean |
1 |
3 |
['github-actions', 'loefflerd', 'yuanyi-350'] |
loefflerd assignee:loefflerd |
2-84437 2 days ago |
unknown |
unknown |
| 37869 |
mckoen author:mckoen |
feat(AlgebraicTopology/Quasicategory): inner fibrations and inner anodyne morphisms |
Defines inner fibrations, inner anodyne morphisms, and immediate results.
---
[](https://gitpod.io/from-referrer/)
|
t-algebraic-topology
maintainer-merge
|
220/0 |
Mathlib.lean,Mathlib/AlgebraicTopology/Quasicategory/Basic.lean,Mathlib/AlgebraicTopology/Quasicategory/InnerFibration.lean,Mathlib/AlgebraicTopology/SimplicialSet/AnodyneExtensions/Inner/Basic.lean |
4 |
18 |
['github-actions', 'joelriou', 'mckoen', 'robin-carlier'] |
nobody |
2-69680 2 days ago |
unknown |
unknown |
| 38414 |
chrisflav author:chrisflav |
chore(RingTheory): move `IsLocalizedModule.Away` to the `Basic` file and use it everywhere |
---
[](https://gitpod.io/from-referrer/)
|
t-ring-theory
maintainer-merge
|
42/48 |
Mathlib/Algebra/Module/FinitePresentation.lean,Mathlib/Algebra/Module/LocalizedModule/Away.lean,Mathlib/Algebra/Module/LocalizedModule/Basic.lean,Mathlib/AlgebraicGeometry/Modules/Tilde.lean,Mathlib/AlgebraicGeometry/StructureSheaf.lean,Mathlib/RingTheory/LocalProperties/Exactness.lean,Mathlib/RingTheory/LocalProperties/Submodule.lean,Mathlib/RingTheory/Localization/Finiteness.lean,Mathlib/RingTheory/Localization/Free.lean,Mathlib/RingTheory/Spectrum/Prime/FreeLocus.lean,Mathlib/RingTheory/Spectrum/Prime/Module.lean,Mathlib/RingTheory/Support.lean |
12 |
8 |
['chrisflav', 'dagurtomas', 'github-actions', 'grunweg', 'mathlib-merge-conflicts'] |
nobody |
2-65205 2 days ago |
unknown |
unknown |
| 37840 |
tb65536 author:tb65536 |
chore(RingTheory/Localization/AtPrime/Basic): use `under` instead of `comap (algebraMap R S)` |
This PR switches over from `comap (algebraMap R S)` to `under`.
---
[](https://gitpod.io/from-referrer/)
|
t-ring-theory
t-algebra
maintainer-merge
awaiting-CI
label:t-algebra$ |
172/149 |
Mathlib/AlgebraicGeometry/Noetherian.lean,Mathlib/AlgebraicGeometry/ProjectiveSpectrum/Scheme.lean,Mathlib/RingTheory/DedekindDomain/Dvr.lean,Mathlib/RingTheory/Etale/QuasiFinite.lean,Mathlib/RingTheory/Frobenius.lean,Mathlib/RingTheory/Ideal/AssociatedPrime/Localization.lean,Mathlib/RingTheory/Ideal/GoingUp.lean,Mathlib/RingTheory/Ideal/Height.lean,Mathlib/RingTheory/Ideal/KrullsHeightTheorem.lean,Mathlib/RingTheory/Ideal/MinimalPrime/Localization.lean,Mathlib/RingTheory/Ideal/Over.lean,Mathlib/RingTheory/IntegralClosure/GoingDown.lean,Mathlib/RingTheory/Jacobson/Ring.lean,Mathlib/RingTheory/KrullDimension/Polynomial.lean,Mathlib/RingTheory/LocalProperties/Injective.lean,Mathlib/RingTheory/Localization/AtPrime/Basic.lean,Mathlib/RingTheory/Localization/AtPrime/Extension.lean,Mathlib/RingTheory/Localization/Ideal.lean,Mathlib/RingTheory/QuasiFinite/Basic.lean,Mathlib/RingTheory/Spectrum/Prime/Topology.lean |
20 |
14 |
['chrisflav', 'github-actions', 'mathlib-merge-conflicts', 'robin-carlier', 'tb65536'] |
chrisflav and erdOne assignee:erdOne assignee:chrisflav |
2-65068 2 days ago |
unknown |
unknown |
| 38656 |
NoahW314 author:NoahW314 |
feat(Data/Finsupp/Weight): add `Finsupp.degree_mapDomain` |
Generalize a result by removing an unnecessary hypothesis. Also simplifies the proof.
---
[](https://gitpod.io/from-referrer/)
|
t-data
maintainer-merge
|
9/8 |
Mathlib/Data/Finsupp/Weight.lean,Mathlib/Order/Filter/TendstoCofinite.lean |
2 |
4 |
['NoahW314', 'dagurtomas', 'github-actions'] |
nobody |
2-61543 2 days ago |
unknown |
unknown |
| 38971 |
homeowmorphism author:homeowmorphism |
chore(FinitelyPresentedGroup): Use dot notation by default whenever possible and typo fix |
* Changing the usage of `IsNormalClosureFG N` to `N.IsNormalClosureFG` as the idiomatic use of the latter seems easier to read ("N is finitely generated under normal closure") and is in line with using dot notation for terms.
* Fix a typo in the main definition docstring regarding the usage of `map`: it should be `.map` instead of `_map`.
---
I used Copilot + Gemini Pro 3.1 to query about usage and took some of its suggestions.
[](https://gitpod.io/from-referrer/)
|
maintainer-merge
t-group-theory
|
7/7 |
Mathlib/GroupTheory/FinitelyPresentedGroup.lean |
1 |
2 |
['github-actions', 'tb65536'] |
tb65536 assignee:tb65536 |
2-47109 2 days ago |
unknown |
unknown |
| 37355 |
Thmoas-Guan author:Thmoas-Guan |
feat(RingTheory): refactor `smulShortComplex` |
Use `LinearMap.lsmul` for the `f` of `ModuleCat.smulShortComplex`, also providing new APIs for it.
---
[](https://gitpod.io/from-referrer/)
|
t-ring-theory
maintainer-merge
|
18/21 |
Mathlib/RingTheory/Regular/Category.lean |
1 |
21 |
['Thmoas-Guan', 'chrisflav', 'github-actions', 'robin-carlier'] |
chrisflav assignee:chrisflav |
2-44655 2 days ago |
unknown |
unknown |
| 38743 |
eric-wieser author:eric-wieser |
feat: `Finite` instances for `Sym` |
We already have the `Fintype` instances.
I take the liberty of moving these into namespaces in order to produce nicer auto-generated instance names.
---
[](https://gitpod.io/from-referrer/)
|
t-data
maintainer-merge
|
25/3 |
Mathlib/Data/Fintype/Vector.lean |
1 |
3 |
['YaelDillies', 'github-actions'] |
nobody |
2-33534 2 days ago |
unknown |
unknown |
| 38525 |
AntoineChambert-Loir author:AntoineChambert-Loir |
feat(Tactic/Translate/ToAdditive.lean): add conGen/AddConGen to the to_additive tactic |
This PR adds the pair "conGen", "AddConGen" to the additive tactic and capitalizes the second of some pairs that should have been.
---
[](https://gitpod.io/from-referrer/)
|
t-meta
maintainer-merge
|
11/10 |
Mathlib/Algebra/Exact.lean,Mathlib/GroupTheory/Congruence/Defs.lean,Mathlib/Tactic/Translate/ToAdditive.lean |
3 |
15 |
['AntoineChambert-Loir', 'JovanGerb', 'github-actions', 'mathlib-merge-conflicts', 'robin-carlier'] |
JovanGerb and dwrensha assignee:dwrensha assignee:JovanGerb |
2-12263 2 days ago |
unknown |
unknown |
| 38949 |
YaelDillies author:YaelDillies |
chore: untag duplicated `gcongr` lemmas |
Follow-up to #38793
---
[](https://gitpod.io/from-referrer/)
|
maintainer-merge |
11/9 |
Mathlib/Algebra/Module/Submodule/Basic.lean,Mathlib/Algebra/Module/Submodule/RestrictScalars.lean,Mathlib/Algebra/Order/Ring/Ordering/Basic.lean,Mathlib/Analysis/SpecialFunctions/Sigmoid.lean,Mathlib/Data/Finset/Density.lean,Mathlib/RingTheory/Localization/Submodule.lean |
6 |
3 |
['JovanGerb', 'github-actions'] |
nobody |
2-6213 2 days ago |
unknown |
unknown |
| 36376 |
jessealama author:jessealama |
feat(SimpleGraph): hamiltonian cycle from cyclic permutation |
This PR provides `IsHamiltonian.of_perm`, a bridge from `Equiv.Perm.IsCycle` to `SimpleGraph.IsHamiltonian`: if σ is a permutation that is a single cycle with full support on at least 3 elements, and each step `v → σ v` is an edge of `G`, then `G` is Hamiltonian.
### New definitions and lemmas
**`Mathlib/Data/List/Chain.lean`**:
- `IsChain.iterate`: `List.iterate f a n` is a chain under `r` whenever `r a (f a)` holds for all `a`
**`Mathlib/Data/List/Iterate.lean`**:
- `getLast_iterate`: the last element of `List.iterate f a n` is `f^[n - 1] a`
**`Mathlib/Combinatorics/SimpleGraph/Walk/Iterate.lean`** (new file):
- `Walk.iterate`: builds a walk of length `n` from `x` to `f^[n] x` for any function `f` with `G.Adj x (f x)` for all `x`, defined via `Walk.ofSupport`
- `Walk.length_iterate`, `Walk.support_iterate`, `Walk.edges_iterate`: basic API
**`Mathlib/GroupTheory/Perm/Cycle/Basic.lean`**:
- `IsCycleOn.injOn_pow_apply`: the map `n ↦ (f ^ n) a` is injective on `Finset.range #s`
**`Mathlib/GroupTheory/Perm/Cycle/Concrete.lean`**:
- `IsCycleOn.injOn_sym2_pow_apply`: the unordered-pair edge map `k ↦ s((f ^ k) a, (f ^ (k + 1)) a)` is injective on `[0, #s)` when `#s ≠ 2`
- `IsCycleOn.sym2_pow_apply_ne`: edge distinctness for cycle-on permutations — `s((f ^ k) a, (f ^ (k + 1)) a) ≠ s(a, f a)` when `k ≠ 0`, `k < #s`, and `#s ≠ 2`
- `Perm.toList_eq_range_map_pow`: expresses `toList` as a range map over powers
**`Mathlib/Combinatorics/SimpleGraph/Hamiltonian.lean`**:
- `cons_isHamiltonianCycle_iff`: a Hamiltonian path closed by an edge outside its support is a Hamiltonian cycle, and conversely
- `IsHamiltonian.of_perm`: the main theorem
---
- [x] depends on: #36307 |
t-combinatorics
maintainer-merge
|
182/0 |
Mathlib.lean,Mathlib/Combinatorics/SimpleGraph/Hamiltonian.lean,Mathlib/Combinatorics/SimpleGraph/Hamiltonian/Perm.lean,Mathlib/Combinatorics/SimpleGraph/Walk/Iterate.lean,Mathlib/Data/List/Chain.lean,Mathlib/Data/List/Iterate.lean,Mathlib/GroupTheory/Perm/Cycle/Basic.lean,Mathlib/GroupTheory/Perm/Cycle/Concrete.lean |
8 |
75 |
['SnirBroshi', 'YaelDillies', 'github-actions', 'jessealama', 'mathlib-dependent-issues', 'mathlib-merge-conflicts'] |
YaelDillies assignee:YaelDillies |
2-3964 2 days ago |
unknown |
unknown |
| 38889 |
emlis42 author:emlis42 |
chore(NumberTheory/Divisors): golf `Int.mem_divisorsAntidiag` |
This PR merges the case split and removes duplicated proofs in `Int.mem_divisorsAntidiag`. |
t-number-theory
new-contributor
maintainer-merge
|
7/36 |
Mathlib/NumberTheory/Divisors.lean |
1 |
14 |
['MichaelStollBayreuth', 'SnirBroshi', 'emlis42', 'github-actions'] |
MichaelStollBayreuth assignee:MichaelStollBayreuth |
2-1606 2 days ago |
unknown |
unknown |
| 38814 |
sharky564 author:sharky564 |
refactor(LinearAlgebra/Projection): refactor `quotientEquivOfIsCompl` via `LinearEquiv.ofLinear` |
This PR refactors `Submodule.quotientEquivOfIsCompl` to use `LinearEquiv.ofLinear` rather than `LinearEquiv.symm <| LinearEquiv.ofBijective`. The new definition makes both directions of the equivalence explicit: the forward idirection is `Submodule.liftQ` of the projection onto `q` along `p`, and the backward direction is `Submodule.mkQ` composed with the inclusion `q` in `E`.
---
The motivation is work on topological complements of submodules in PR #38547. The proof of `IsCompl.isTopCompl_iff_continuous_quotientEquiv` reduces, via the quotient-map property of `mkQ`, to identifying the composite `quotientEquivOfIsCompl ∘ mkQ` with the linear projection. This identifications feels like it should belong at the algebraic level and not mixed in with the topological reasoning. Additionally, these lemmas seem useful independently. |
t-algebra
new-contributor
maintainer-merge
label:t-algebra$ |
43/22 |
Mathlib/LinearAlgebra/Projection.lean |
1 |
27 |
['ADedecker', 'github-actions', 'sharky564', 'themathqueen'] |
nobody |
1-82498 1 day ago |
unknown |
unknown |
| 36216 |
michaellee94 author:michaellee94 |
feat(CategoryTheory): characterize pullback squares via the `Over` category |
---
[](https://gitpod.io/from-referrer/)
|
t-category-theory
new-contributor
maintainer-merge
|
47/0 |
Mathlib/CategoryTheory/Limits/Shapes/Pullback/IsPullback/Basic.lean |
1 |
18 |
['dagurtomas', 'github-actions', 'joelriou', 'michaellee94'] |
robin-carlier assignee:robin-carlier |
1-77254 1 day ago |
unknown |
unknown |
| 37406 |
vihdzp author:vihdzp |
feat(SetTheory/Cardinal): `IsStrongPrelimit` predicate |
We introduce a predicate for cardinals `c` such that `x < c` implies `x < 2 ^ c`. This is to `IsStrongLimit` as `IsSuccPrelimit` is to `IsSuccLimit`. We then make use of it in a few places where we were writing down `∀ x < c, x < 2 ^ c` explicitly.
---
[](https://gitpod.io/from-referrer/)
|
t-set-theory
maintainer-merge
|
53/26 |
Mathlib/SetTheory/Cardinal/Aleph.lean,Mathlib/SetTheory/Cardinal/Cofinality.lean,Mathlib/SetTheory/Cardinal/Order.lean,Mathlib/SetTheory/Cardinal/Regular.lean |
4 |
4 |
['YaelDillies', 'github-actions', 'mathlib-merge-conflicts', 'vihdzp'] |
alreadydone assignee:alreadydone |
1-55690 1 day ago |
unknown |
unknown |
| 37545 |
vihdzp author:vihdzp |
feat(SetTheory): ℵ_ univ = univ |
---
[](https://gitpod.io/from-referrer/)
|
t-set-theory
maintainer-merge
|
73/7 |
Mathlib/SetTheory/Cardinal/Aleph.lean,Mathlib/SetTheory/Cardinal/Regular.lean |
2 |
16 |
['YaelDillies', 'github-actions', 'mathlib-merge-conflicts', 'mattdiamond', 'plp127', 'vihdzp'] |
nobody |
1-55019 1 day ago |
unknown |
unknown |
| 38846 |
YanYablonovskiy author:YanYablonovskiy |
feat(Order): OrderType cardinality lemmas |
Adding some basic lemmas for the cardinality of an order type.
---
[](https://gitpod.io/from-referrer/)
|
new-contributor
t-order
large-import
maintainer-merge
|
28/4 |
Mathlib/Order/Types/Arithmetic.lean |
1 |
10 |
['YaelDillies', 'YanYablonovskiy', 'github-actions', 'plp127', 'vihdzp', 'wwylele'] |
YaelDillies assignee:YaelDillies |
1-37647 1 day ago |
unknown |
unknown |
| 37400 |
SnirBroshi author:SnirBroshi |
feat(Combinatorics/SimpleGraph/Acyclic): endpoints of a path have at most one neighbor in the path |
---
[](https://gitpod.io/from-referrer/)
|
t-combinatorics
maintainer-merge
|
15/0 |
Mathlib/Combinatorics/SimpleGraph/Acyclic.lean |
1 |
6 |
['Rida-Hamadani', 'Ruben-VandeVelde', 'SnirBroshi', 'bryangingechen', 'github-actions'] |
nobody |
1-35682 1 day ago |
unknown |
unknown |
| 38907 |
YaelDillies author:YaelDillies |
chore(Geometry): move `ConvexSpace` out of `LinearAlgebra` |
`ConvexSpace` is convex geometry, not linear algebra
---
[](https://gitpod.io/from-referrer/)
|
t-convex-geometry
file-removed
maintainer-merge
|
6/7 |
Mathlib.lean,Mathlib/Analysis/Convex/MetricSpace.lean,Mathlib/Geometry/Convex/ConvexSpace/AffineSpace.lean,Mathlib/Geometry/Convex/ConvexSpace/Defs.lean,Mathlib/Geometry/Convex/README.md |
5 |
5 |
['YaelDillies', 'github-actions', 'mathlib-merge-conflicts', 'themathqueen'] |
nobody |
1-31662 1 day ago |
unknown |
unknown |
| 28685 |
mitchell-horner author:mitchell-horner |
feat(Combinatorics/SimpleGraph): prove the minimal-degree version of the Erdős-Stone theorem |
Proves the minimal degree-version of the Erdős-Stone theorem:
If `G` has a minimal degree of at least `(1 - 1 / r + o(1)) * card V`, then `G` contains a copy of a `completeEquipartiteGraph` in `r + 1` parts each of size `t`.
The double-counting construction from the proof is available in `namespace ErdosStone`.
---
- [x] depends on: #25843
- [x] depends on: #27597
- [x] depends on: #27599
- [x] depends on: #28443
- [x] depends on: #28445
- [x] depends on: #28446
- [x] depends on: #28447
This is the first of several pull requests towards the full Erdős-Stone(-Simonovits) theorem, hence the name of the file.
[](https://gitpod.io/from-referrer/) |
t-combinatorics
maintainer-merge
|
329/0 |
Mathlib.lean,Mathlib/Combinatorics/SimpleGraph/Extremal/ErdosStoneSimonovits.lean |
2 |
19 |
['YaelDillies', 'b-mehta', 'github-actions', 'mathlib-dependent-issues', 'mathlib4-merge-conflict-bot', 'mitchell-horner', 'robin-carlier'] |
b-mehta assignee:b-mehta |
1-5983 1 day ago |
unknown |
unknown |
| 38370 |
FordUniver author:FordUniver |
feat(Data/Finset/Powerset): add `filter_powersetCard_subset` |
Adds `Finset.filter_powersetCard_subset` and derives `Finset.card_filter_powersetCard_subset` from it. The hypothesis `s.card ≤ n` is necessary: without it, natural subtraction silently gives `Nat.choose k 0 = 1 ≠ 0`.
Co-authored-by: Malte Jackisch
---
We ran into this while formalizing Goodman's formula on triangle densities in graphs as part of an ongoing flag algebras project in Lean, and it seemed worth upstreaming.
**Disclosure.** *This PR was developed with assistance from LLM code tools, used for Mathlib style alignment and proof compactness. The mathematical content and proof strategy originate from formalization work by Malte Jackisch (co-author) and myself; the final code has been reviewed and vouched for by both of us.* |
t-data
new-contributor
maintainer-merge
|
30/0 |
Mathlib/Data/Finset/Powerset.lean |
1 |
20 |
['FordUniver', 'YaelDillies', 'github-actions', 'mathlib-bors', 'wwylele'] |
YaelDillies assignee:YaelDillies |
1-4433 1 day ago |
unknown |
unknown |
| 38963 |
linesthatinterlace author:linesthatinterlace |
fix: rename `Pi.prod` to `Function.prod` |
Renames `Pi.prod` to `Function.prod` in order to allow for dot notation to work in the non-dependent case.
---
[](https://gitpod.io/from-referrer/)
|
large-import
maintainer-merge
|
88/74 |
Archive/Sensitivity.lean,Mathlib/Algebra/Algebra/NonUnitalHom.lean,Mathlib/Algebra/Algebra/Prod.lean,Mathlib/Algebra/BigOperators/Finprod.lean,Mathlib/Algebra/Exact.lean,Mathlib/Algebra/Group/Prod.lean,Mathlib/Algebra/Lie/Prod.lean,Mathlib/Algebra/MvPolynomial/Equiv.lean,Mathlib/Algebra/MvPolynomial/Eval.lean,Mathlib/Algebra/Notation/Pi/Defs.lean,Mathlib/Algebra/Star/StarAlgHom.lean,Mathlib/Combinatorics/Nullstellensatz.lean,Mathlib/LinearAlgebra/AffineSpace/AffineMap.lean,Mathlib/LinearAlgebra/Dimension/DivisionRing.lean,Mathlib/LinearAlgebra/Goursat.lean,Mathlib/LinearAlgebra/Prod.lean,Mathlib/LinearAlgebra/QuadraticForm/Dual.lean,Mathlib/Logic/Function/Defs.lean,Mathlib/MeasureTheory/Integral/Prod.lean,Mathlib/MeasureTheory/Measure/Prod.lean,Mathlib/NumberTheory/Height/Basic.lean,Mathlib/SetTheory/Cardinal/Finite.lean,Mathlib/Topology/Algebra/ContinuousAffineMap.lean,Mathlib/Topology/Algebra/InfiniteSum/Basic.lean,Mathlib/Topology/Algebra/InfiniteSum/Constructions.lean,Mathlib/Topology/Inseparable.lean,Mathlib/Topology/UniformSpace/LocallyUniformConvergence.lean |
27 |
4 |
['fpvandoorn', 'github-actions'] |
nobody |
1-1963 1 day ago |
unknown |
unknown |
| 38604 |
wwylele author:wwylele |
chore(Algebra/Module): remove some `backward.privateInPublic` |
---
[](https://gitpod.io/from-referrer/)
|
t-algebra
tech debt
maintainer-merge
label:t-algebra$ |
14/30 |
Mathlib/Algebra/Module/GradedModule.lean,Mathlib/Algebra/Module/Submodule/Lattice.lean |
2 |
7 |
['dagurtomas', 'github-actions', 'wwylele'] |
dagurtomas assignee:dagurtomas |
0-84544 23 hours ago |
unknown |
unknown |
| 38962 |
sharky564 author:sharky564 |
refactor(Topology/Algebra/Module/LinearMap): rename subtypeL companion lemmas |
This PR renames the companion lemmas of `Submodule.subtypeL` for consistency with `Submodule.mkQL` (introduced in PR #38811). Specifically, `Submodule.coe_subtypeL` is renamed to `Submodule.toLinearMap_subtypeL` (to accurately reflect that it projects to the underlying LinearMap, not a function-level coercion), and `Submodule.coe_subtypeL'` is renamed to `Submodule.coe_subtypeL` (since this is the genuine function-level coercion lemma).
---
This brings the `subtypeL` API in line with the `mkQL` naming convention established in PR #38811. No behavioural changes. |
t-topology
new-contributor
maintainer-merge
|
38/32 |
Mathlib/Analysis/Calculus/Implicit.lean,Mathlib/Analysis/Normed/Operator/Banach.lean,Mathlib/Topology/Algebra/Module/LinearMap.lean,scripts/nolints_prime_decls.txt |
4 |
15 |
['ADedecker', 'github-actions', 'sharky564', 'themathqueen'] |
nobody |
0-82592 22 hours ago |
unknown |
unknown |
| 38999 |
joelriou author:joelriou |
feat(Algebra/Homology): homology sequence and acyclic complexes |
This PR adds lemmas `ShortComplex.ShortExact.acyclic_X₁/₂/₃` which allow to deduce that certain homological complexes in a short exact sequence are acyclic.
---
[](https://gitpod.io/from-referrer/)
|
t-category-theory
t-algebra
maintainer-merge
label:t-algebra$ |
61/2 |
Mathlib/Algebra/Homology/HomologySequenceLemmas.lean |
1 |
6 |
['dagurtomas', 'github-actions', 'joelriou'] |
nobody |
0-76749 21 hours ago |
unknown |
unknown |
| 39025 |
joelriou author:joelriou |
feat(CategoryTheory/Localization): LocalizerMorphism.IsInduced |
If `Φ : LocalizerMorphism W₁ W₂`, the typeclass `Φ.IsInduced` says that `W₂.inverseImage Φ.functor = W₁`.
---
[](https://gitpod.io/from-referrer/)
|
t-category-theory
maintainer-merge
|
67/1 |
Mathlib/CategoryTheory/Equivalence.lean,Mathlib/CategoryTheory/Localization/LocalizerMorphism.lean |
2 |
10 |
['dagurtomas', 'github-actions', 'joelriou'] |
nobody |
0-73438 20 hours ago |
unknown |
unknown |
| 39024 |
joelriou author:joelriou |
feat(CategoryTheory): horizontal composition of Guitart exact squares |
---
[](https://gitpod.io/from-referrer/)
|
t-category-theory
maintainer-merge
|
201/0 |
Mathlib.lean,Mathlib/CategoryTheory/GuitartExact/Basic.lean,Mathlib/CategoryTheory/GuitartExact/HorizontalComposition.lean,Mathlib/CategoryTheory/GuitartExact/VerticalComposition.lean |
4 |
9 |
['dagurtomas', 'github-actions', 'joelriou'] |
nobody |
0-71418 19 hours ago |
unknown |
unknown |
| 38997 |
joelriou author:joelriou |
feat(Algebra/Homology): the homotopy fiber and the path object |
---
- [x] depends on: #38996
[](https://gitpod.io/from-referrer/)
|
t-category-theory
maintainer-merge
|
228/1 |
Mathlib.lean,Mathlib/Algebra/Homology/ComplexShape.lean,Mathlib/Algebra/Homology/HomotopyCofiber.lean,Mathlib/Algebra/Homology/HomotopyFiber.lean,Mathlib/Algebra/Homology/Opposite.lean |
5 |
4 |
['dagurtomas', 'github-actions', 'mathlib-dependent-issues'] |
nobody |
0-64654 17 hours ago |
unknown |
unknown |
| 38442 |
Parcly-Taxel author:Parcly-Taxel |
feat: arbitrary-order induction on `Nat` |
This can be used as e.g.
```lean
induction n using stepInduction 3 with
| base n hn => ...
| step n ih => ...
```
The test file's examples are from a term project I did for an NUS module taught by Olivier Danvy himself. |
t-data
maintainer-merge
|
61/2 |
Mathlib/Data/Nat/Init.lean,MathlibTest/StepInduction.lean |
2 |
7 |
['Parcly-Taxel', 'SnirBroshi', 'dagurtomas', 'github-actions'] |
nobody |
0-62550 17 hours ago |
unknown |
unknown |
| 39020 |
urkud author:urkud |
chore(*): golf while reducing defeq abuse `Set α = α → Prop` |
---
[](https://gitpod.io/from-referrer/)
|
maintainer-merge |
14/30 |
Mathlib/Algebra/Algebra/Subalgebra/Lattice.lean,Mathlib/Algebra/Ring/Subring/MulOpposite.lean,Mathlib/Analysis/Meromorphic/IsolatedZeros.lean,Mathlib/Analysis/Polynomial/MahlerMeasure.lean,Mathlib/Analysis/SpecialFunctions/Pow/Continuity.lean,Mathlib/Data/Nat/Count.lean,Mathlib/Data/Set/Function.lean |
7 |
8 |
['github-actions', 'grunweg', 'leanprover-radar', 'urkud'] |
nobody |
0-59370 16 hours ago |
unknown |
unknown |
| 38957 |
wwylele author:wwylele |
chore(GroupTheory/DivisibleHull): remove `backward.privateInPublic` |
---
[](https://gitpod.io/from-referrer/)
|
tech debt
t-group-theory
maintainer-merge
|
5/12 |
Mathlib/GroupTheory/DivisibleHull.lean |
1 |
3 |
['github-actions', 'grunweg', 'wwylele'] |
jcommelin assignee:jcommelin |
0-46847 13 hours ago |
unknown |
unknown |
| 39036 |
ajhendel author:ajhendel |
doc: fix Lean 3 namespace in DiophantineApproximation |
The implementation notes section references the Lean 3 namespace \`real.contfrac_legendre\`, but this was renamed to \`Real.ContfracLegendre\` during the port. This fixes the reference.
---
Co-Authored-By: Claude Opus 4.6 |
t-number-theory
new-contributor
maintainer-merge
|
1/1 |
Mathlib/NumberTheory/DiophantineApproximation/Basic.lean |
1 |
4 |
['github-actions', 'tb65536'] |
MichaelStollBayreuth assignee:MichaelStollBayreuth |
0-46845 13 hours ago |
unknown |
unknown |
| 39014 |
vihdzp author:vihdzp |
feat(Order/SuccPred/LinearLocallyFinite): `StrictMono toZ` |
We prove that `toZ` is strictly monotonic, and golf/deprecate other theorems in this file using this.
---
[](https://gitpod.io/from-referrer/)
|
t-order
maintainer-merge
|
31/57 |
Mathlib/Order/SuccPred/LinearLocallyFinite.lean |
1 |
5 |
['YaelDillies', 'github-actions'] |
nobody |
0-28259 7 hours ago |
unknown |
unknown |
| 37441 |
lecopivo author:lecopivo |
fix(FunProp): be less strict about the shape of morphism theorems |
Don't be so restrictive about the shape of morphism theorems
Right now, `fun_prop` has a problem with a bundled morphism `Foo α` that coerces to `α → α → α` . The coerced function has two arguments and there is an unnecessary restriction about this. This PR lifts that restriction.
[Zulip discussion](https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/.60fun_prop.60.20in.20.60FunLike.60.20with.20multiple.20arguments/with/582731349)
---
[](https://gitpod.io/from-referrer/)
|
t-meta
delegated
maintainer-merge
|
46/12 |
Mathlib/Tactic/FunProp/Core.lean,Mathlib/Tactic/FunProp/Theorems.lean,MathlibTest/fun_prop_dev.lean |
3 |
10 |
['Vierkantor', 'github-actions', 'joneugster', 'mathlib-bors'] |
joneugster assignee:joneugster |
0-25857 7 hours ago |
unknown |
unknown |
| 37808 |
JovanGerb author:JovanGerb |
feat(Translate): locally modify name guessing dictionaries |
This PR adds the feature to `to_dual` and `to_additive` that you can now locally modify the name translation dictionary.
With this change, we run the risk of having the automated translations being harder to predict. For this reason, the changes to the dictionary do not persisted through imports. Instead, the change lasts until the end of the file (though it ignores sections).
See https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/Order.20dual.20tactic/near/580834166
---
[](https://gitpod.io/from-referrer/)
|
t-meta
maintainer-merge
|
111/39 |
Mathlib/Order/GaloisConnection/Basic.lean,Mathlib/Order/GaloisConnection/Defs.lean,Mathlib/Order/Interval/Set/Basic.lean,Mathlib/Order/Interval/Set/Disjoint.lean,Mathlib/Tactic/Translate/Core.lean,Mathlib/Tactic/Translate/GuessName.lean,Mathlib/Tactic/Translate/ToAdditive.lean,Mathlib/Tactic/Translate/ToDual.lean,MathlibTest/ToDual.lean |
9 |
7 |
['JovanGerb', 'bryangingechen', 'github-actions', 'joneugster', 'mathlib-merge-conflicts'] |
joneugster assignee:joneugster |
0-22015 6 hours ago |
unknown |
unknown |
| 37573 |
vihdzp author:vihdzp |
feat: supremum of `≤ c` ordinals of cardinal `≤ c` has cardinal `≤ c` |
---
[](https://gitpod.io/from-referrer/)
|
t-set-theory
maintainer-merge
|
47/13 |
Mathlib/SetTheory/Cardinal/Ordinal.lean |
1 |
5 |
['YaelDillies', 'github-actions', 'mathlib-merge-conflicts'] |
nobody |
0-19295 5 hours ago |
unknown |
unknown |
| 37561 |
IvanRenison author:IvanRenison |
feat(Data/List): add lemma `List.notMem_subset` |
---
Zulip question: https://leanprover.zulipchat.com/#narrow/channel/217875-Is-there-code-for-X.3F/topic/List.2EnotMem_subset/with/583146215
[](https://gitpod.io/from-referrer/)
|
t-data
maintainer-merge
|
2/0 |
Mathlib/Data/List/Basic.lean |
1 |
3 |
['github-actions', 'joneugster'] |
joneugster assignee:joneugster |
0-19190 5 hours ago |
unknown |
unknown |
| 38807 |
vihdzp author:vihdzp |
feat: `DirSupClosedOn` is preserved under union |
---
[](https://gitpod.io/from-referrer/)
|
t-order
maintainer-merge
|
81/0 |
Mathlib/Order/DirSupClosed.lean |
1 |
10 |
['YaelDillies', 'github-actions', 'vihdzp'] |
nobody |
0-19175 5 hours ago |
unknown |
unknown |
| 35632 |
SnirBroshi author:SnirBroshi |
feat(Data/List/TakeDrop): `take`/`drop` + `tail`/`dropLast` almost commute |
RFC to lean4: https://github.com/leanprover/lean4/issues/12910
---
[Zulip](https://leanprover.zulipchat.com/#narrow/channel/217875-Is-there-code-for-X.3F/topic/List.2Etail.2FList.2EdropLast.20.2B.20List.2Etake/with/572294698)
[](https://gitpod.io/from-referrer/)
|
t-data
maintainer-merge
|
22/0 |
Mathlib/Data/List/TakeDrop.lean |
1 |
10 |
['SnirBroshi', 'github-actions', 'joneugster', 'mathlib-merge-conflicts'] |
nobody |
0-18760 5 hours ago |
unknown |
unknown |
| 38998 |
joelriou author:joelriou |
feat(AlgebraicTopology/ModelCategory): precylinders in full subcategories |
This PR adds basic API for constructing precylinder or pre-path objects in full subcategories and study left/right homotopies in full subcategories.
---
[](https://gitpod.io/from-referrer/)
|
t-algebraic-topology
maintainer-merge
|
80/0 |
Mathlib/AlgebraicTopology/ModelCategory/Cylinder.lean,Mathlib/AlgebraicTopology/ModelCategory/LeftHomotopy.lean,Mathlib/AlgebraicTopology/ModelCategory/PathObject.lean,Mathlib/AlgebraicTopology/ModelCategory/RightHomotopy.lean |
4 |
2 |
['github-actions', 'robin-carlier'] |
nobody |
0-18558 5 hours ago |
unknown |
unknown |
| 38090 |
chrisflav author:chrisflav |
feat(AlgebraicGeometry): rank of finite flat morphism |
From Pi1.
---
- [x] depends on: #38084
[](https://gitpod.io/from-referrer/)
|
t-algebraic-geometry
maintainer-merge
|
484/2 |
Mathlib.lean,Mathlib/Algebra/Algebra/Tower.lean,Mathlib/AlgebraicGeometry/AffineScheme.lean,Mathlib/AlgebraicGeometry/Morphisms/Affine.lean,Mathlib/AlgebraicGeometry/Morphisms/Finite.lean,Mathlib/AlgebraicGeometry/Morphisms/FinitePresentation.lean,Mathlib/AlgebraicGeometry/Morphisms/Flat.lean,Mathlib/AlgebraicGeometry/Morphisms/FlatRank.lean,Mathlib/CategoryTheory/Limits/Shapes/Pullback/IsPullback/Basic.lean,Mathlib/RingTheory/Flat/Rank.lean,Mathlib/RingTheory/Localization/BaseChange.lean |
11 |
27 |
['chrisflav', 'github-actions', 'mathlib-dependent-issues', 'robin-carlier'] |
kim-em and robin-carlier assignee:kim-em assignee:robin-carlier |
0-15343 4 hours ago |
unknown |
unknown |
| 38651 |
joelriou author:joelriou |
feat(CategoryTheory/Triangulated): localizing subcategories |
We show that the functor from the Verdier quotient `A/(A ⊓ B)` to `C/B` is fully faithful when `A` is a `B`-right- or left-localizing triangulated subcategory in the sense of Verdier.
---
- [x] depends on: #38987
- [x] depends on: #38804
- [x] depends on: #38803
- [x] depends on: #38802
- [x] depends on: #38650
[](https://gitpod.io/from-referrer/)
|
t-category-theory
maintainer-merge
|
194/3 |
Mathlib/CategoryTheory/Triangulated/LocalizingSubcategory.lean |
1 |
10 |
['dagurtomas', 'github-actions', 'joelriou', 'mathlib-dependent-issues', 'mathlib-merge-conflicts', 'robin-carlier'] |
nobody |
0-6148 1 hour ago |
unknown |
unknown |
| 36553 |
j-loreaux author:j-loreaux |
feat: add IsMulCommutative instances for directed families of commutative subobjects |
---
- [ ] depends on: #36549
[](https://gitpod.io/from-referrer/)
|
t-algebra
maintainer-merge
label:t-algebra$ |
169/1 |
Mathlib/Algebra/Algebra/NonUnitalSubalgebra.lean,Mathlib/Algebra/Algebra/Subalgebra/Directed.lean,Mathlib/Algebra/Group/Subgroup/Lattice.lean,Mathlib/Algebra/Group/Submonoid/Membership.lean,Mathlib/Algebra/Group/Subsemigroup/Membership.lean,Mathlib/Algebra/Ring/Subring/Basic.lean,Mathlib/Algebra/Ring/Subsemiring/Basic.lean,Mathlib/Algebra/Star/NonUnitalSubalgebra.lean,Mathlib/Algebra/Star/Subalgebra.lean,Mathlib/RingTheory/NonUnitalSubring/Basic.lean,Mathlib/RingTheory/NonUnitalSubsemiring/Basic.lean |
11 |
7 |
['github-actions', 'j-loreaux', 'mathlib-dependent-issues', 'mathlib-merge-conflicts', 'robin-carlier', 'themathqueen'] |
kim-em assignee:kim-em |
0-5565 1 hour ago |
unknown |
unknown |
| 39015 |
vihdzp author:vihdzp |
chore(Order/SuccPred/LinearLocallyFinite): no expose |
The definitions in this file don't give any useful def-eqs, so we opt to not expose them.
---
[](https://gitpod.io/from-referrer/)
|
t-order
maintainer-merge
|
1/2 |
Mathlib/Order/SuccPred/LinearLocallyFinite.lean |
1 |
3 |
['github-actions', 'robin-carlier'] |
nobody |
0-4135 1 hour ago |
unknown |
unknown |
| 39079 |
joelriou author:joelriou |
feat(AlgebraicTopology/SimplicialObject): iterations of δ 0 and σ 0 |
---
[](https://gitpod.io/from-referrer/)
|
t-algebraic-topology
maintainer-merge
|
149/0 |
Mathlib.lean,Mathlib/AlgebraicTopology/SimplicialObject/DeltaZeroIter.lean |
2 |
2 |
['github-actions', 'robin-carlier'] |
nobody |
0-1873 31 minutes ago |
0-2052 27 minutes ago |
0-4546 1 hour |
| 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 |
| 17623 |
astrainfinita author:astrainfinita |
feat(Algebra/Order/GroupWithZero/Unbundled): add some lemmas |
Some lemmas in `Algebra.Order.GroupWithZero.Unbundled` have incorrect or unsatisfactory names, or assumptions that can be omitted using `ZeroLEOneClass`. The lemmas added in this PR are versions of existing lemmas that use the correct or better name or `ZeroLEOneClass` to omit an assumption. The original lemmas will be deprecated in #17593.
| New name | Old name |
|-------------------------|-------------------------|
| `mul_le_one_left₀` | `Left.mul_le_one_of_le_of_le` |
| `mul_lt_one_of_le_of_lt_left₀` (`0 ≤ ·` version) / `mul_lt_one_of_le_of_lt_of_pos_left` | `Left.mul_lt_of_le_of_lt_one_of_pos` |
| `mul_lt_one_of_lt_of_le_left₀` | `Left.mul_lt_of_lt_of_le_one_of_nonneg` |
| `mul_le_one_right₀` | `Right.mul_le_one_of_le_of_le` |
| `mul_lt_one_of_lt_of_le_right₀` (`0 ≤ ·` version) / `mul_lt_one_of_lt_of_le_of_pos_right` | `Right.mul_lt_one_of_lt_of_le_of_pos` |
| `mul_lt_one_of_le_of_lt_right₀` | `Right.mul_lt_one_of_le_of_lt_of_nonneg` |
The following lemmas use `ZeroLEOneClass`.
| New name | Old name |
|-------------------------|-------------------------|
| `(Left.)one_le_mul₀` | `Left.one_le_mul_of_le_of_le` |
| `Left.one_lt_mul_of_le_of_lt₀` | `Left.one_lt_mul_of_le_of_lt_of_pos` |
| `Left.one_lt_mul_of_lt_of_le₀` | `Left.lt_mul_of_lt_of_one_le_of_nonneg` / `one_lt_mul_of_lt_of_le` (still there) |
| `(Left.)one_lt_mul₀` | |
| `Right.one_le_mul₀` | `Right.one_le_mul_of_le_of_le` |
| `Right.one_lt_mul_of_lt_of_le₀` | `Right.one_lt_mul_of_lt_of_le_of_pos` |
| `Right.one_lt_mul_of_le_of_lt₀` | `Right.one_lt_mul_of_le_of_lt_of_nonneg` / `one_lt_mul_of_le_of_lt` (still there) / `one_lt_mul` (still there) |
| `Right.one_lt_mul₀` | `Right.one_lt_mul_of_lt_of_lt` |
---
Split from #17593.
[](https://gitpod.io/from-referrer/)
|
merge-conflict
t-algebra
awaiting-zulip
t-order
label:t-algebra$ |
146/44 |
Mathlib/Algebra/Order/GroupWithZero/Canonical.lean,Mathlib/Algebra/Order/GroupWithZero/Unbundled.lean |
2 |
11 |
['YaelDillies', 'astrainfinita', 'github-actions', 'j-loreaux'] |
nobody |
534-7194 1 year ago |
unknown |
unknown |
| 15654 |
TpmKranz author:TpmKranz |
feat(Computability): language-preserving maps between NFA and RE |
Map REs to NFAs via Thompson's construction and NFAs to REs using GNFAs
Last chunk of #12648
---
- [ ] depends on: #15651
- [ ] depends on: #15649
[](https://gitpod.io/from-referrer/)
|
blocked-by-other-PR
new-contributor
t-computability
merge-conflict
awaiting-zulip
|
985/2 |
Mathlib.lean,Mathlib/Computability/GNFA.lean,Mathlib/Computability/Language.lean,Mathlib/Computability/NFA.lean,Mathlib/Computability/RegularExpressions.lean,Mathlib/Data/FinEnum/Option.lean,docs/references.bib |
7 |
3 |
['github-actions', 'leanprover-community-mathlib4-bot', 'meithecatte'] |
nobody |
367-56871 1 year ago |
unknown |
unknown |
| 17458 |
urkud author:urkud |
refactor(Algebra/Group): make `IsUnit` a typeclass |
Also change some lemmas to assume `[IsUnit _]` instead of `[Invertible _]`.
Motivated by potential non-defeq diamonds in #14986, see also [Zulip](https://leanprover.zulipchat.com/#narrow/stream/116395-maths/topic/Invertible.20and.20data)
I no longer plan to merge this PR, but I'm going to cherry-pick some changes to a new PR before closing this one.
---
[](https://gitpod.io/from-referrer/)
|
merge-conflict
t-algebra
awaiting-zulip
label:t-algebra$ |
82/72 |
Mathlib/Algebra/CharP/Invertible.lean,Mathlib/Algebra/Group/Invertible/Basic.lean,Mathlib/Algebra/Group/Units/Defs.lean,Mathlib/Algebra/GroupWithZero/Invertible.lean,Mathlib/Algebra/GroupWithZero/Units/Basic.lean,Mathlib/Algebra/Polynomial/Degree/Units.lean,Mathlib/Algebra/Polynomial/Splits.lean,Mathlib/Analysis/Convex/Segment.lean,Mathlib/Analysis/Normed/Affine/Isometry.lean,Mathlib/Analysis/Normed/Ring/Units.lean,Mathlib/CategoryTheory/Linear/Basic.lean,Mathlib/FieldTheory/Finite/Basic.lean,Mathlib/FieldTheory/Separable.lean,Mathlib/FieldTheory/SeparableDegree.lean,Mathlib/GroupTheory/Submonoid/Inverses.lean,Mathlib/LinearAlgebra/AffineSpace/AffineEquiv.lean,Mathlib/LinearAlgebra/AffineSpace/Combination.lean,Mathlib/LinearAlgebra/CliffordAlgebra/Contraction.lean,Mathlib/LinearAlgebra/CliffordAlgebra/Inversion.lean,Mathlib/LinearAlgebra/CliffordAlgebra/SpinGroup.lean,Mathlib/LinearAlgebra/Eigenspace/Minpoly.lean,Mathlib/NumberTheory/MulChar/Basic.lean,Mathlib/RingTheory/Localization/NumDen.lean,Mathlib/RingTheory/Polynomial/Content.lean,Mathlib/RingTheory/Polynomial/GaussLemma.lean,Mathlib/RingTheory/Valuation/Basic.lean |
26 |
12 |
['MichaelStollBayreuth', 'acmepjz', 'eric-wieser', 'github-actions', 'leanprover-bot', 'leanprover-community-bot-assistant', 'urkud'] |
nobody |
307-37220 10 months ago |
unknown |
unknown |
| 25218 |
kckennylau author:kckennylau |
feat(AlgebraicGeometry): Tate normal form of elliptic curves |
---
[](https://gitpod.io/from-referrer/)
|
merge-conflict
t-algebraic-geometry
awaiting-zulip
new-contributor
|
291/26 |
Mathlib.lean,Mathlib/AlgebraicGeometry/EllipticCurve/IsomOfJ.lean,Mathlib/AlgebraicGeometry/EllipticCurve/Modular/TateNormalForm.lean,Mathlib/AlgebraicGeometry/EllipticCurve/NormalForms.lean,Mathlib/AlgebraicGeometry/EllipticCurve/VariableChange.lean |
5 |
31 |
['MichaelStollBayreuth', 'Multramate', 'acmepjz', 'github-actions', 'grunweg', 'kckennylau', 'leanprover-community-bot-assistant'] |
nobody |
307-36058 10 months ago |
unknown |
unknown |
| 28803 |
astrainfinita author:astrainfinita |
refactor: unbundle algebra from `ENormed*` |
Further speed up the search in the algebraic typeclass hierarchy by avoiding searching for `TopologicalSpace`.
This PR continues the work from #23961.
- Change `ESeminormed(Add)Monoid` and `ENormed(Add)Monoid` so they no longer carry algebraic data.
- Deprecate `ESeminormed(Add)CommMonoid` and `ENormed(Add)CommMonoid` in favor of `ESeminormed(Add)Monoid` and `ENormed(Add)Monoid` with a commutative algebraic typeclass.
|Old|New|
|---|---|
| `[ESeminormed(Add)(Comm)Monoid E]` | `[(Add)(Comm)Monoid E] [ESeminormed(Add)Monoid E]` |
| `[ENormed(Add)(Comm)Monoid]` | `[(Add)(Comm)Monoid E] [ENormed(Add)Monoid]` |
See [Zulip discussion](https://leanprover.zulipchat.com/#narrow/channel/144837-PR-reviews/topic/.2328803.20refactor.3A.20unbundle.20algebra.20from.20.60ENormed*.60/with/536024350)
------------
- [x] depends on: #28813 |
t-algebra
merge-conflict
slow-typeclass-synthesis
awaiting-zulip
t-analysis
label:t-algebra$ |
80/63 |
Mathlib/Analysis/CStarAlgebra/CStarMatrix.lean,Mathlib/Analysis/Normed/Group/Basic.lean,Mathlib/Analysis/Normed/Group/Continuity.lean,Mathlib/Analysis/Normed/Group/InfiniteSum.lean,Mathlib/Analysis/NormedSpace/IndicatorFunction.lean,Mathlib/MeasureTheory/Function/L1Space/AEEqFun.lean,Mathlib/MeasureTheory/Function/L1Space/HasFiniteIntegral.lean,Mathlib/MeasureTheory/Function/L1Space/Integrable.lean,Mathlib/MeasureTheory/Function/LocallyIntegrable.lean,Mathlib/MeasureTheory/Function/LpSeminorm/Basic.lean,Mathlib/MeasureTheory/Function/LpSeminorm/CompareExp.lean,Mathlib/MeasureTheory/Function/LpSeminorm/TriangleInequality.lean,Mathlib/MeasureTheory/Integral/IntegrableOn.lean,Mathlib/MeasureTheory/Integral/IntervalIntegral/Basic.lean |
14 |
28 |
['astrainfinita', 'bryangingechen', 'github-actions', 'grunweg', 'kbuzzard', 'leanprover-bot', 'leanprover-community-mathlib4-bot', 'mathlib-bors', 'mathlib4-dependent-issues-bot', 'mathlib4-merge-conflict-bot', 'sgouezel'] |
grunweg assignee:grunweg |
247-51703 8 months ago |
unknown |
unknown |
| 28925 |
grunweg author:grunweg |
chore: remove `linear_combination'` tactic |
When `linear_combination` was refactored in #15899, the old code was kept as the `linear_combination'` tactic, for easier migration. The consensus of the zulip discussion ([#mathlib4 > Narrowing the scope of `linear_combination` @ 💬](https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/Narrowing.20the.20scope.20of.20.60linear_combination.60/near/470237816)) was to wait, and "revisit this once people have experienced the various tactics in practice".
One year later, the old tactic has almost no uses: it is unused in mathlib; [searching on github](https://github.com/search?q=linear_combination%27%20path%3A*.lean&type=code) yields 37 hits --- all of which are in various forks of mathlib. Thus, removing this tactic seems appropriate.
---
Do not merge before the zulip discussion has concluded!
[](https://gitpod.io/from-referrer/)
|
merge-conflict
file-removed
awaiting-zulip
|
0/564 |
Mathlib.lean,Mathlib/Tactic.lean,Mathlib/Tactic/LinearCombination'.lean,Mathlib/Tactic/Linter/UnusedTactic.lean,MathlibTest/linear_combination'.lean |
5 |
4 |
['euprunin', 'github-actions', 'grunweg', 'mathlib4-merge-conflict-bot'] |
nobody |
204-28913 6 months ago |
unknown |
unknown |
| 30150 |
imbrem author:imbrem |
feat(CategoryTheory/Monoidal): to_additive for MonoidalCategory |
Add `AddMonoidalCategory`, the additive version of `MonoidalCategory`.
To get this to work, I needed to _remove_ the `to_additive` attributes in `Discrete.lean`, since existing code relies on the `AddMonoid M → MonoidalCategory M` instance. For now, we simply implement the additive variants by hand instead.
---
As discussed in #28718; I added an `AddMonoidalCategory` struct and tagged `MonoidalCategory` with `to_additive`, along with the lemmas in `Category.lean`.
I think this is the right approach, since under this framework the "correct" additive version of `Discrete.lean` would be mapping an `AddMonoid` to an `AddMonoidalCategory`.
Next steps would be to:
- Make `monoidal_coherence` and `coherence` support `AddMonoidalCategory`
- Add `CocartesianMonoidalCategory` extending `AddMonoidalCategory`
[](https://gitpod.io/from-referrer/)
|
t-category-theory
large-import
new-contributor
merge-conflict
awaiting-zulip
t-meta
|
444/125 |
Mathlib/CategoryTheory/Monoidal/Category.lean,Mathlib/CategoryTheory/Monoidal/Discrete.lean,Mathlib/Tactic/ToAdditive/GuessName.lean |
3 |
22 |
['JovanGerb', 'YaelDillies', 'github-actions', 'imbrem', 'mathlib4-merge-conflict-bot'] |
nobody |
176-39787 5 months ago |
unknown |
unknown |
| 15651 |
TpmKranz author:TpmKranz |
feat(Computability/NFA): operations for Thompson's construction |
Lays the groundwork for a proof of equivalence of RE and NFA, w.r.t. described language. Actual connection to REs comes later, after the groundwork for the opposite direction has been laid.
Third chunk of #12648
---
[](https://gitpod.io/from-referrer/)
|
new-contributor
t-computability
merge-conflict
awaiting-author
awaiting-zulip
|
307/5 |
Mathlib/Computability/NFA.lean |
1 |
27 |
['TpmKranz', 'YaelDillies', 'dupuisf', 'github-actions', 'leanprover-community-bot-assistant', 'meithecatte', 'rudynicolop'] |
nobody |
171-56919 5 months ago |
unknown |
unknown |
| 15649 |
TpmKranz author:TpmKranz |
feat(Computability): introduce Generalised NFA as bridge to Regular Expression |
Lays the groundwork for a proof of equivalence of NFA and RE, w.r.t. described language. Actual connection to NFA comes later, after the groundwork for the opposite direction has been laid.
Second chunk of #12648
---
- [x] depends on: #15647 [Data.FinEnum.Option unchanged since then]
[](https://gitpod.io/from-referrer/)
|
new-contributor
t-computability
merge-conflict
awaiting-author
awaiting-zulip
|
298/0 |
Mathlib.lean,Mathlib/Computability/GNFA.lean,Mathlib/Computability/Language.lean,Mathlib/Computability/RegularExpressions.lean,docs/references.bib |
5 |
7 |
['github-actions', 'mathlib4-dependent-issues-bot', 'mathlib4-merge-conflict-bot', 'meithecatte', 'trivial1711'] |
nobody |
170-73160 5 months ago |
unknown |
unknown |
| 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/)
|
merge-conflict
t-computability
awaiting-zulip
new-contributor
|
490/0 |
Mathlib.lean,Mathlib/Computability/RegularExpressionsToEpsilonNFA.lean,docs/references.bib |
3 |
7 |
['anthonyde', 'github-actions', 'mathlib4-dependent-issues-bot', 'mathlib4-merge-conflict-bot', 'meithecatte', 'qawbecrdtey'] |
nobody |
170-23928 5 months ago |
unknown |
unknown |
| 11800 |
JADekker author:JADekker |
feat: KappaLindelöf spaces |
Define KappaLindelöf spaces by following the first one-third of the API for Lindelöf spaces. The remainder will be added in a future PR.
---
[](https://gitpod.io/from-referrer/)
|
please-adopt
merge-conflict
t-topology
awaiting-zulip
|
301/2 |
Mathlib.lean,Mathlib/Topology/Compactness/KappaLindelof.lean,Mathlib/Topology/Compactness/Lindelof.lean |
3 |
38 |
['ADedecker', 'JADekker', 'PatrickMassot', 'StevenClontz', 'adomani', 'github-actions', 'grunweg', 'kim-em', 'urkud'] |
nobody |
169-82194 5 months ago |
unknown |
unknown |
| 33368 |
urkud author:urkud |
feat: define `Complex.UnitDisc.shift` |
Also review the existing API
UPD: I'm going to define a `PSL(2, Real)` action instead.
---
[](https://gitpod.io/from-referrer/) |
t-analysis
awaiting-zulip
merge-conflict
|
273/39 |
Mathlib.lean,Mathlib/Analysis/Complex/UnitDisc/Basic.lean,Mathlib/Analysis/Complex/UnitDisc/Shift.lean |
3 |
7 |
['github-actions', 'j-loreaux', 'mathlib4-merge-conflict-bot', 'sgouezel', 'urkud'] |
j-loreaux assignee:j-loreaux |
121-32353 4 months ago |
unknown |
unknown |
| 34720 |
Paul-Lez author:Paul-Lez |
feat(RingTheory/PowerSeries/Composition): define composition of power series |
This PR defines the composition of two power series, and adds various pieces of API lemmas (this is mostly fixing up and upstreaming code from [this repo](https://github.com/rmhi/formal_deriv)).
This is the first of a series of PRs upstreaming work that was done at the CFT workshop in Oxford last summer, working towards proving some results about the `exp` and `log` power series (and their composition!), and constructing the isomorphism $(\mathfrak{m}_K ^ n, +) \cong (1 + \mathfrak{m}_K ^ n, \times)$ for sufficiently large $n$, where $K$ is a characteristic zero local field.
Co-authored-by: Richard Hill
Co-authored-by: Calle Sönne
---
[](https://gitpod.io/from-referrer/)
|
t-ring-theory
awaiting-zulip
|
844/0 |
Mathlib.lean,Mathlib/RingTheory/PowerSeries/Composition.lean |
2 |
3 |
['Paul-Lez', 'github-actions', 'vihdzp'] |
nobody |
87-58025 2 months ago |
unknown |
unknown |
| 20238 |
maemre author:maemre |
feat(Computability/DFA): Closure of regular languages under some set operations |
This shows that regular languages are closed under complement and intersection by constructing DFAs for them.
---
Closure under all other operations will be proved when someone adds the proof for DFA<->regular expression equivalence, so they are not part of this PR.
[](https://gitpod.io/from-referrer/)
|
new-contributor
t-computability
merge-conflict
awaiting-author
awaiting-zulip
|
159/0 |
Mathlib/Computability/DFA.lean,Mathlib/Computability/Language.lean |
2 |
60 |
['EtienneC30', 'YaelDillies', 'github-actions', 'maemre', 'mathlib4-merge-conflict-bot', 'meithecatte', 'urkud'] |
nobody |
71-17162 2 months ago |
unknown |
unknown |
| 22361 |
rudynicolop author:rudynicolop |
feat(Computability/NFA): nfa closure properties |
Add the closure properties union, intersection and reversal for NFA.
---
[](https://gitpod.io/from-referrer/)
|
new-contributor
t-computability
merge-conflict
awaiting-author
awaiting-zulip
|
218/2 |
Mathlib/Computability/Language.lean,Mathlib/Computability/NFA.lean |
2 |
91 |
['EtienneC30', 'b-mehta', 'ctchou', 'github-actions', 'leanprover-community-bot-assistant', 'meithecatte', 'rudynicolop'] |
nobody |
71-17146 2 months ago |
unknown |
unknown |
| 23929 |
meithecatte author:meithecatte |
feat(Computability/NFA): improve bound on pumping lemma |
---
- [x] depends on: #25321
[](https://gitpod.io/from-referrer/)
|
t-computability
awaiting-zulip
new-contributor
awaiting-author
|
101/10 |
Mathlib/Computability/EpsilonNFA.lean,Mathlib/Computability/NFA.lean |
2 |
42 |
['YaelDillies', 'dagurtomas', 'github-actions', 'leanprover-community-bot-assistant', 'mathlib4-dependent-issues-bot', 'meithecatte'] |
nobody |
70-37175 2 months ago |
unknown |
unknown |
| 35524 |
grunweg author:grunweg |
feat: text-based linter against \t followed by tactic mode |
Wait for the zulip discussion to converge. **If** there is consensus in favour of this change, summarise the motivation here.
[zulip discuss](https://leanprover.zulipchat.com/#narrow/channel/345428-mathlib-reviewers/topic/proposal.3A.20no.20more.20use.20of.20.60.E2.96.B8.60.20in.20Mathlib.3F/with/574680826)
---
There are currently 80 remaining exceptions in mathlib: ideally, these would get fixed before merging this.
Works best when combined with #35523.
[](https://gitpod.io/from-referrer/)
|
t-linter
awaiting-zulip
merge-conflict
|
23/2 |
Mathlib/Tactic/Linter/TextBased.lean |
1 |
5 |
['github-actions', 'grunweg', 'joneugster', 'mathlib-merge-conflicts', 'vihdzp'] |
nobody |
51-54927 1 month ago |
unknown |
unknown |
| 36890 |
vihdzp author:vihdzp |
chore(SetTheory): `le_mul_left` → `le_mul_of_pos_left` |
The new theorem names/statements match [`Nat.le_mul_of_pos_left`](https://leanprover-community.github.io/mathlib4_docs/Init/Data/Nat/Lemmas.html#Nat.le_mul_of_pos_left). The cardinal one has also been moved to an earlier file.
---
[](https://gitpod.io/from-referrer/)
|
t-set-theory
awaiting-zulip
merge-conflict
|
28/23 |
Mathlib/SetTheory/Cardinal/Arithmetic.lean,Mathlib/SetTheory/Cardinal/Basic.lean,Mathlib/SetTheory/Cardinal/Free.lean,Mathlib/SetTheory/Ordinal/Arithmetic.lean,Mathlib/SetTheory/Ordinal/Exponential.lean,Mathlib/SetTheory/Ordinal/Notation.lean |
6 |
2 |
['github-actions', 'mathlib-merge-conflicts'] |
nobody |
46-27331 1 month ago |
unknown |
unknown |
| 35578 |
Shreyas4991 author:Shreyas4991 |
fix: writer monad should use an additive logging type |
The Writer monad's w type is supposed to be additive, not multiplicative. This is how it is conceptually used in Haskell (as a logging type). Haskell uses `Monoid` because it doesn't make a distinction between `AddMonoid` and `Monoid`.
[#mathlib4 > Writer should use an additive monoid @ 💬](https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/Writer.20should.20use.20an.20additive.20monoid/near/574990415)
---
[](https://gitpod.io/from-referrer/)
|
t-data
awaiting-zulip
merge-conflict
|
10/10 |
Mathlib/Control/Monad/Cont.lean,Mathlib/Control/Monad/Writer.lean |
2 |
5 |
['Shreyas4991', 'eric-wieser', 'github-actions', 'mathlib-merge-conflicts'] |
nobody |
42-37806 1 month ago |
unknown |
unknown |
| 30750 |
SnirBroshi author:SnirBroshi |
feat(Data/Quot): `toSet` and `equivClassOf` |
Define `toSet` which gets the set corresponding to an element of a quotient, and `equivClassOf` which gets the equivalence class of an element under a quotient.
---
I found these definitions helpful when working with quotients, specifically `ConnectedComponents` of a `TopologicalSpace`.
[](https://gitpod.io/from-referrer/)
|
t-data
awaiting-author
awaiting-zulip
|
162/0 |
Mathlib/Data/Quot.lean,Mathlib/Data/Set/Image.lean,Mathlib/Data/SetLike/Basic.lean,Mathlib/Data/Setoid/Basic.lean |
4 |
8 |
['SnirBroshi', 'TwoFX', 'eric-wieser', 'github-actions', 'linesthatinterlace', 'mathlib-merge-conflicts'] |
TwoFX assignee:TwoFX |
24-9315 24 days ago |
unknown |
unknown |
| 26299 |
adomani author:adomani |
perf: the `whitespace` linter only acts on modified files |
Introduces an `IO.Ref` to allow the `commandStart` linter to only run on files that git considers modified with respect to `master`.
The linter is also active on files that have had some error, as these are likely being modified!
The PR should also mitigate the speed-up that the linter introduced:
[#mathlib4 > A whitespace linter @ 💬](https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/A.20whitespace.20linter/near/525091877)
Assuming that this goes well, a similar mechanism could be applied to several linters that do not need to run on all code, just on the modified code.
Implementation detail: the linter is currently either on or off in "whole" files. It may be also a future development to make this more granular and only run the linter on "modifed commands in modified files", but this is not currently the plan for this modification!
---
[](https://gitpod.io/from-referrer/)
|
t-linter
awaiting-zulip
awaiting-author
|
55/7 |
Mathlib/Tactic/Linter/Whitespace.lean |
1 |
20 |
['adomani', 'eric-wieser', 'github-actions', 'grunweg', 'joneugster', 'kim-em', 'leanprover-bot', 'leanprover-radar', 'mathlib-bors', 'mathlib4-merge-conflict-bot'] |
grunweg assignee:grunweg |
21-28030 21 days ago |
unknown |
unknown |
| 34963 |
Parcly-Taxel author:Parcly-Taxel |
feat(Archive): proof of the Robbins conjecture |
Cf. [#mathlib4 > Alternative axiomatization of boolean algebras @ 💬](https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/Alternative.20axiomatization.20of.20boolean.20algebras/near/558900960) and #31924. |
t-algebra
awaiting-zulip
label:t-algebra$ |
610/0 |
Archive.lean,Archive/Robbins.lean |
2 |
2 |
['chrisflav', 'github-actions'] |
chrisflav assignee:chrisflav |
17-75591 17 days ago |
unknown |
unknown |
| 38546 |
yhx-12243 author:yhx-12243 |
fix: universe issue in injective module |
Change the definition of
```lean
class Module.Injective : Prop where
out : ∀ ⦃X Y : Type v⦄ [AddCommGroup X] [AddCommGroup Y] [Module R X] [Module R Y]
(f : X →ₗ[R] Y) (_ : Function.Injective f) (g : X →ₗ[R] Q),
∃ h : Y →ₗ[R] Q, ∀ x, h (f x) = g x
```
into
```lean
class Module.Injective : Prop where
out : ∀ ⦃X Y : Type u⦄ [AddCommGroup X] [AddCommGroup Y] [Module R X] [Module R Y]
(f : X →ₗ[R] Y) (_ : Function.Injective f) (g : X →ₗ[R] Q),
∃ h : Y →ₗ[R] Q, ∀ x, h (f x) = g x
```
to make it agree with `Module.Baer` and real mathematical definition, **without universe issues**.
Since the criterion `Module.Flat` also uses `Type u` on testing modules.
See discussions in https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/Universe.20issue.20about.20injective.20module .
---
[](https://gitpod.io/from-referrer/)
|
t-algebra
new-contributor
awaiting-zulip
label:t-algebra$ |
57/43 |
Mathlib/Algebra/Category/ModuleCat/Injective.lean,Mathlib/Algebra/Category/ModuleCat/Ulift.lean,Mathlib/Algebra/Module/Injective.lean,Mathlib/RepresentationTheory/FinGroupCharZero.lean,Mathlib/RingTheory/Flat/Tensor.lean,Mathlib/RingTheory/LocalProperties/Injective.lean |
6 |
5 |
['github-actions', 'grunweg', 'mathlib-bors', 'wwylele'] |
nobody |
11-62280 11 days ago |
unknown |
unknown |
| 37346 |
euprunin author:euprunin |
chore: golf using `grind` |
The goal of this PR is to decrease the number of times lemmas are called explicitly. Any decrease in compilation time is a welcome side effect, although it is not a primary objective.
Trace profiling results (differences <30 ms considered measurement noise):
* `✅️ SimpleGraph.Walk.IsPath.getVert_injOn`: unchanged 🎉
* `✅️ SimpleGraph.Walk.length_bypass_le`: unchanged 🎉
* `✅️ Rat.floor_intCast_div_natCast`: unchanged 🎉
* `✅️ InnerProductGeometry.norm_eq_of_angle_sub_eq_angle_sub_rev_of_angle_ne_pi`: unchanged 🎉
* `✅️ padicNorm.zero_of_padicNorm_eq_zero`: unchanged 🎉
Profiled using `set_option trace.profiler true in`.
---
[](https://gitpod.io/from-referrer/)
|
maintainer-merge
awaiting-zulip
|
7/45 |
Mathlib/Combinatorics/SimpleGraph/Paths.lean,Mathlib/Data/Rat/Floor.lean,Mathlib/Geometry/Euclidean/Triangle.lean,Mathlib/NumberTheory/Padics/PadicNorm.lean |
4 |
22 |
['FernandoChu', 'bryangingechen', 'chenson2018', 'euprunin', 'faenuccio', 'github-actions', 'grunweg'] |
nobody |
9-8104 9 days ago |
unknown |
unknown |
| 37934 |
Thmoas-Guan author:Thmoas-Guan |
feat(FieldTheory): definition of transcendental separable field extension |
In this PR, we introduce the concept of separably generated field extension and transcendental separable field extension.
Further properties will be in #37838
---
[](https://gitpod.io/from-referrer/)
|
t-algebra
awaiting-zulip
label:t-algebra$ |
69/0 |
Mathlib.lean,Mathlib/FieldTheory/TranscendentalSeparable.lean |
2 |
3 |
['Thmoas-Guan', 'github-actions', 'robin-carlier'] |
robin-carlier assignee:robin-carlier |
3-5926 3 days ago |
unknown |
unknown |
| 39027 |
fpvandoorn author:fpvandoorn |
feat: delaborators for inequalities in big operators |
`∏ i < n, f i` was already accepted as valid syntax, but this PR now also prints appropriate sums/products using this notation.
---
[Zulip discussion](https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/missing.20delaborator.20for.20finsum)
[](https://gitpod.io/from-referrer/)
|
t-algebra
t-meta
awaiting-zulip
label:t-algebra$ |
132/49 |
Mathlib/Algebra/BigOperators/Group/Finset/Defs.lean,MathlibTest/BigOps.lean |
2 |
1 |
['github-actions'] |
nobody |
1-2917 1 day ago |
unknown |
unknown |
| 32608 |
PrParadoxy author:PrParadoxy |
feat(LinearAlgebra/PiTensorProduct): API for PiTensorProducts indexed by sets |
This PR addresses a TODO item in LinearAlgebra/PiTensorProduct.lean:
* API for the various ways ι can be split into subsets; connect this
with the binary tensor product
-- specifically by describing tensors of type ⨂ (i : S), M i, for S : Set ι.
Our primary motivation is to formalise the notion of "restricted tensor
products". This will be the content of a follow-up PR.
Beyond that, the Set API is natural in contexts where the index type has
an independent interpretation. An example is quantum physics, where ι
ranges over distinguishable degrees of freedom, and where its is common
practice to annotate objects by the set of indices they are defined on.
---
Stub file with preliminary definition of the restricted tensor product as a direct limit of tensors indexed by finite subsets of an index type:
https://github.com/PrParadoxy/mathlib4/blob/restricted-stub/Mathlib/LinearAlgebra/PiTensorProduct/Restricted.lean
---
- [x] depends on: #32598
[](https://gitpod.io/from-referrer/)
|
new-contributor
awaiting-zulip
t-algebra
awaiting-author
label:t-algebra$ |
300/2 |
Mathlib.lean,Mathlib/LinearAlgebra/PiTensorProduct.lean,Mathlib/LinearAlgebra/PiTensorProduct/Set.lean |
3 |
29 |
['PrParadoxy', 'dagurtomas', 'eric-wieser', 'github-actions', 'goliath-klein', 'leanprover-radar', 'mathlib4-dependent-issues-bot', 'mathlib4-merge-conflict-bot'] |
nobody |
0-64301 17 hours ago |
unknown |
unknown |
| 32742 |
LTolDe author:LTolDe |
feat(MeasureTheory/Constructions/Polish/Basic): add class SuslinSpace |
add new class `SuslinSpace` for a topological space that is an analytic set in itself
This will be useful to prove the **Effros Theorem**, see [zulip thread](https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/Effros.20Theorem/with/558712441).
---
[](https://gitpod.io/from-referrer/)
|
new-contributor
awaiting-zulip
t-measure-probability
awaiting-author
|
4/0 |
Mathlib/MeasureTheory/Constructions/Polish/Basic.lean |
1 |
10 |
['ADedecker', 'LTolDe', 'dagurtomas', 'dupuisf', 'github-actions', 'jcommelin'] |
PatrickMassot assignee:PatrickMassot |
0-63147 17 hours ago |
unknown |
unknown |
| 33031 |
chiyunhsu author:chiyunhsu |
feat(Combinatorics/Enumerative/Partition): add combinatorial proof of Euler's partition theorem |
The new file EulerComb.lean contains the combinatorial proof of Euler's partition theorem. The analytic proof of the theorem and its generalization of Glaisher's Theorem has already been formalized in [Glaisher.lean](https://github.com/leanprover-community/mathlib4/blob/master/Mathlib/Combinatorics/Enumerative/Partition/Glaisher.lean). The generalization of the combinatorial proof from this file to Glaisher's Theorem is within reach.
---
Zulip discussion: [#mathlib4 > Glaisher’s Bijection on integer partitions](https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/Glaisher.E2.80.99s.20Bijection.20on.20integer.20partitions/with/570808111)
[](https://gitpod.io/from-referrer/)
|
t-combinatorics
new-contributor
awaiting-zulip
awaiting-author
|
531/0 |
Mathlib.lean,Mathlib/Combinatorics/Enumerative/Partition/EulerComb.lean |
2 |
7 |
['chiyunhsu', 'dagurtomas', 'github-actions', 'tb65536', 'vihdzp'] |
b-mehta assignee:b-mehta |
0-61979 17 hours ago |
unknown |
unknown |
| 30668 |
astrainfinita author:astrainfinita |
feat: `QuotType` |
This typeclass is primarily for use by type synonyms of `Quot` and `Quotient`. Using `QuotType` API for type synonyms of `Quot` and `Quotient` will avoid defeq abuse caused by directly using `Quot` and `Quotient` APIs.
This PR also adds some typeclasses to support different ways to find the quotient map that should be used. See the documentation comments of these typeclasses for examples of usage.
---
It's not a typical design to use these auxiliary typeclasses and term elaborators, but I haven't found a better way to support these notations.
Some of the naming may need to be discussed. For example:
- `⟦·⟧` is currently called `mkQ` in names. This distinguishes it from other `.mk`s and makes it possible to write the quotient map as `mkQ` `mkQ'` ~~`mkQ_ h`~~. But this will also require changing the old lemma names.
- It would be helpful if the names of new type classes explained their functionality better.
[Zulip](https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/migrate.20to.20.60QuotLike.60.20API)
This PR continues the work from #16421.
Original PR: https://github.com/leanprover-community/mathlib4/pull/16421 |
RFC
t-data
awaiting-zulip
awaiting-author
|
629/0 |
Mathlib.lean,Mathlib/Data/QuotType.lean,MathlibTest/QuotType.lean |
3 |
22 |
['SnirBroshi', 'YaelDillies', 'astrainfinita', 'dagurtomas', 'github-actions', 'mathlib4-merge-conflict-bot', 'plp127', 'vihdzp'] |
nobody |
0-50448 14 hours ago |
unknown |
unknown |
| 39026 |
fpvandoorn author:fpvandoorn |
feat: add assume tactic |
Teaching tactic: `assume p, q, r` is short for `intro (_ : p) (_ : q) (_ : r)`.
---
[Zulip thread](https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/Assume.20tactic/with/593477478)
[](https://gitpod.io/from-referrer/)
|
awaiting-zulip
t-meta
awaiting-author
|
123/0 |
Mathlib.lean,Mathlib/Tactic.lean,Mathlib/Tactic/Assume.lean,MathlibTest/Assume.lean |
4 |
5 |
['fpvandoorn', 'github-actions', 'joneugster'] |
joneugster assignee:joneugster |
0-7651 2 hours ago |
unknown |
unknown |
| 32828 |
Hagb author:Hagb |
feat(Algebra/Order/Group/Defs): add `IsOrderedAddMonoid.toIsOrderedCancelAddMonoid'` |
It is similar to `IsOrderedAddMonoid.toIsOrderedCancelAddMonoid`, while with different hypotheses.
The conclusion `IsOrderedCancelMonoid α` on
`IsOrderedAddMonoid.toIsOrderedCancelAddMonoid` still holds when the hypothesis `CommGroup α` is weakened to `CancelCommMonoid α` while `PartialOrder α` is strengthened to `LinearOrder α`.
---
[`IsOrderedAddMonoid.toIsOrderedCancelAddMonoid`](https://leanprover-community.github.io/mathlib4_docs/find/?pattern=IsOrderedAddMonoid.toIsOrderedCancelAddMonoid#doc) and `IsOrderedAddMonoid.toIsOrderedCancelAddMonoid'`:
https://github.com/leanprover-community/mathlib4/blob/97f78b1a4311fed1844b94f1c069219a48a098e1/Mathlib/Algebra/Order/Group/Defs.lean#L52-L62
[](https://gitpod.io/from-referrer/)
|
awaiting-zulip
t-algebra
awaiting-author
label:t-algebra$ |
4/0 |
Mathlib/Algebra/Order/Group/Defs.lean |
1 |
9 |
['Garmelon', 'Vierkantor', 'artie2000', 'dagurtomas', 'github-actions', 'leanprover-radar'] |
eric-wieser assignee:eric-wieser |
0-1625 27 minutes ago |
unknown |
unknown |