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 |
| 33650 |
vihdzp author:vihdzp |
refactor: deprecate bespoke `Hyperreal` machinery |
Currently, these six definitions are in the `Hyperreal` namespace:
- `IsSt x r`: a predicate for `r` being a standard part of `x`
- `st x`: the standard part of `x`
- `Infinitesimal x`: predicate for infinitesimal elements
- `InfinitePos x`: predicate for infinite and positive elements
- `InfiniteNeg x`: predicate for infinite and negative elements
- `Infinite x`: predicate for infinite (positive or negative) elements.
We deprecate all six of these and all of their API, in favor of reasoning with [`ArchimedeanClass`](https://leanprover-community.github.io/mathlib4_docs/Mathlib/Algebra/Order/Archimedean/Class.html#ArchimedeanClass) and [`ArchimedeanClass.stdPart`](https://leanprover-community.github.io/mathlib4_docs/Mathlib/Algebra/Order/Ring/StandardPart.html#ArchimedeanClass.stdPart). The replacements are as follows:
- `IsSt x r`: `0 ≤ ArchimedeanClass.mk x ∧ stdPart x = r`
- `st x`: `stdPart x`
- `Infinitesimal x`: `0 < ArchimedeanClass.mk x`
- `InfinitePos x`: `0 < x ∧ ArchimedeanClass.mk x < 0`
- `InfiniteNeg x`: `x < 0 ∧ ArchimedeanClass.mk x < 0`
- `Infinite x`: `ArchimedeanClass.mk x < 0`
All of these equivalences are proved within the PR, though these new theorems have also been insta-deprecated.
Most of the existing API on these predicates was largely uninteresting boilerplate, and has been deprecated without replacement. For the few results of mathematical interest (those whose proofs are longer than a few lines), I've golfed their proofs as a stress test to ensure that this new API is capable of easily proving them.
I've kept everything in the same file to minimize the diff. A future PR will move the obsolete material to `Deprecated.Hyperreal`.
---
- [x] depends on: #33644
[](https://gitpod.io/from-referrer/)
|
ready-to-merge
t-algebra
label:t-algebra$ |
387/96 |
Mathlib/Algebra/Order/Ring/StandardPart.lean,Mathlib/Analysis/Real/Hyperreal.lean |
2 |
16 |
['github-actions', 'j-loreaux', 'jcommelin', 'mathlib-bors', 'mathlib-dependent-issues', 'mathlib-merge-conflicts', 'mathlib4-merge-conflict-bot', 'ocfnash', 'vihdzp', 'wwylele'] |
jcommelin assignee:jcommelin |
1-29884 1 day ago |
1-34177 1 day ago |
25-42656 25 days |
| 35847 |
euprunin author:euprunin |
chore: golf proofs |
This PR removes unused `have`/`haveI`/`let`/`letI` calls.
The goal of this PR is to decrease the number of times lemmas are called explicitly (replacing calls to lemmas with calls to tactics). Any decrease in compilation time is a welcome side effect, although it is not a primary objective.
Trace profiling results (differences <30 ms considered measurement noise):
* `GenContFract.compExactValue_correctness_of_stream_eq_some`: unchanged 🎉
* `Finset.disjoint_range_addLeftEmbedding`: unchanged 🎉
* `CategoryTheory.ComposableArrows.IsComplex.epi_cokerToKer'`: unchanged 🎉
* `CategoryTheory.ComposableArrows.IsComplex.mono_cokerToKer'`: unchanged 🎉
* `ComplexShape.QFactorsThroughHomotopy_of_exists_prev`: unchanged 🎉
* `AlgebraicGeometry.IsAffineOpen.primeIdealOf_genericPoint`: unchanged 🎉
* `AlgebraicGeometry.functionField_isFractionRing_of_isAffineOpen`: unchanged 🎉
* `AlgebraicGeometry.smooth_of_grpObj_of_isAlgClosed`: 266 ms before, 232 ms after 🎉
* `AlgebraicGeometry.Scheme.ker_morphismRestrict_ideal`: 570 ms before, 538 ms after 🎉
* `AlgebraicGeometry.Scheme.IdealSheafData.isLocalization_away`: unchanged 🎉
* `AlgebraicGeometry.affineAnd_isLocal`: unchanged 🎉
* `AlgebraicGeometry.IsZariskiLocalAtTarget.of_iSup_eq_top`: unchanged 🎉
* `AlgebraicGeometry.HasAffineProperty.iff_of_isAffine`: unchanged 🎉
* `AlgebraicGeometry.isDominant_of_of_appTop_injective`: unchanged 🎉
* `AlgebraicGeometry.IsPreimmersion.SpecMap_iff`: unchanged 🎉
* `AlgebraicGeometry.quasiCompact_affineProperty_iff_quasiSeparatedSpace`: unchanged 🎉
Profiled using `set_option trace.profiler true in`.
This PR is batched under the following guidelines:
* Up to ~5 changed files per PR
* Up to ~25 changed declarations per PR
* Up to ~100 changed lines per PR
---
[](https://gitpod.io/from-referrer/)
|
ready-to-merge |
0/23 |
Mathlib/Algebra/ContinuedFractions/Computation/CorrectnessTerminating.lean,Mathlib/Algebra/Homology/ExactSequenceFour.lean,Mathlib/Algebra/Homology/Localization.lean,Mathlib/AlgebraicGeometry/FunctionField.lean,Mathlib/AlgebraicGeometry/Group/Smooth.lean,Mathlib/AlgebraicGeometry/IdealSheaf/Basic.lean,Mathlib/AlgebraicGeometry/IdealSheaf/Subscheme.lean,Mathlib/AlgebraicGeometry/Morphisms/AffineAnd.lean,Mathlib/AlgebraicGeometry/Morphisms/Basic.lean,Mathlib/AlgebraicGeometry/Morphisms/ClosedImmersion.lean,Mathlib/AlgebraicGeometry/Morphisms/Preimmersion.lean,Mathlib/AlgebraicGeometry/Morphisms/QuasiSeparated.lean |
12 |
10 |
['JovanGerb', 'euprunin', 'github-actions', 'leanprover-radar', 'mathlib-bors', 'riccardobrasca', 'vihdzp'] |
JovanGerb assignee:JovanGerb |
1-57 1 day ago |
1-2137 1 day ago |
4-28700 4 days |
| 35767 |
kebekus author:kebekus |
feat: asymptotics of the `logCounting` function of Value Distribution Theory |
If `f` is meromorphic over a field `𝕜`, show that the logarithmic counting function for the poles of `f` is asymptotically bounded if and only if `f` has only removable singularities.
---
[](https://gitpod.io/from-referrer/)
|
t-analysis |
150/0 |
Mathlib.lean,Mathlib/Analysis/Complex/ValueDistribution/LogCounting/Asymptotic.lean |
2 |
1 |
['github-actions'] |
j-loreaux assignee:j-loreaux |
3-50012 3 days ago |
6-80915 6 days ago |
6-80888 6 days |
| 35890 |
grunweg author:grunweg |
chore: delete deprecated module Topology/PartialHomeomorph |
This module was deprecated on October 3, and is blocking refactoring of the manifold library.
---
This PR should only be merged on March 3rd: please delegate instead of merging!
[](https://gitpod.io/from-referrer/)
|
easy
t-topology
|
0/11 |
Mathlib.lean,Mathlib/Topology/PartialHomeomorph.lean |
2 |
5 |
['fpvandoorn', 'github-actions', 'mathlib-bors'] |
nobody |
2-12173 2 days ago |
2-12173 2 days ago |
3-82910 3 days |
| 35893 |
b-mehta author:b-mehta |
feat(Data/Nat/Choose/Lucas): add choose_mul_mul and choose_pow_mul_pow_mul modular congruence lemmas |
---
[](https://gitpod.io/from-referrer/)
|
t-data |
32/1 |
Mathlib/Data/Nat/Choose/Lucas.lean |
1 |
1 |
['github-actions'] |
nobody |
3-79765 3 days ago |
3-79765 3 days ago |
3-79821 3 days |
| 35921 |
grunweg author:grunweg |
chore: remove some superfluous parens |
Found by manually auditing the output of regex-searching for '\([A-Za-z0-9_][A-Za-z0-9_]+\)'. Most results are false positives (such as, documentation or export statements), a few are more interesting.
Not exhaustive, I looked at perhaps a fifth or a tenth of all results.
---
[](https://gitpod.io/from-referrer/)
|
t-algebra label:t-algebra$ |
14/14 |
Counterexamples/AharoniKorman.lean,Counterexamples/CanonicallyOrderedCommSemiringTwoMul.lean,Mathlib/Algebra/Category/ModuleCat/Presheaf/Pullback.lean,Mathlib/Algebra/Category/Ring/Basic.lean,Mathlib/Algebra/Group/Pointwise/Finset/BigOperators.lean,Mathlib/Algebra/Group/Subgroup/Basic.lean,Mathlib/Algebra/Lie/Semisimple/Lemmas.lean,Mathlib/Algebra/Order/Antidiag/Nat.lean,Mathlib/Algebra/Order/Archimedean/Class.lean,Mathlib/Algebra/Order/CompleteField.lean,Mathlib/Algebra/SkewMonoidAlgebra/Basic.lean |
11 |
1 |
['github-actions'] |
nobody |
2-84405 2 days ago |
2-84488 2 days ago |
2-84543 2 days |
| 34521 |
huaizhangchu author:huaizhangchu |
feat(MeasureTheory): add measurableEmbedding_natCast |
This PR adds a lemma stating that the coercion from `ℕ` to `ℝ` is a measurable embedding.
```lean
lemma measurableEmbedding_natCast : MeasurableEmbedding (Nat.cast : ℕ → ℝ) :=
Nat.isClosedEmbedding_coe_real.measurableEmbedding
```
This is useful for proving properties about discrete probability distributions on `ℕ` by lifting them to `ℝ` and will be used in #34435. |
awaiting-author
t-measure-probability
new-contributor
|
3/0 |
Mathlib/MeasureTheory/Constructions/BorelSpace/Real.lean |
1 |
2 |
['RemyDegenne', 'github-actions'] |
kex-y assignee:kex-y |
2-16260 2 days ago |
2-16260 2 days ago |
32-77481 32 days |
| 35408 |
MichaelStollBayreuth author:MichaelStollBayreuth |
feat(NumberTheory/Height/Basic): add {mul|log}Height_comp_le, {mul|log}Height_fun_mul_eq |
This adds
* two missing `logHeight` lemmas (their `mulHeight` versions are already there)
* `{mul|log}Height_comp_le`: the height of `x ∘ f` is bounded by the height of `x`
* `{mul|log}Height_fun_mul_eq`: the height of the "multiplication table" `fun (i, j) ↦ x i * y j` is the {product|sum} of the heights of `x` and of `y`
* `{mul|log}Height_fun_prod_eq`: the analogous result for products with arbitrarily many factors
* plus some API lemmas needed for these.
---
[](https://gitpod.io/from-referrer/)
|
t-number-theory
t-algebra
label:t-algebra$ |
168/5 |
Mathlib/Data/Real/Archimedean.lean,Mathlib/NumberTheory/Height/Basic.lean |
2 |
5 |
['CBirkbeck', 'MichaelStollBayreuth', 'github-actions', 'tb65536'] |
tb65536 assignee:tb65536 |
1-80552 1 day ago |
2-65891 2 days ago |
16-459 16 days |
| 34427 |
CoolRmal author:CoolRmal |
feat(MeasureTheory): Strong measurability is preserved under division in a group with zero |
I proved that if `f,g` are two strongly measurable functions taking values in a group with zero, then `f/g` is still strongly measurable.
As mentioned over here [#Is there code for X? > StronglyMeaurable.div₀](https://leanprover.zulipchat.com/#narrow/channel/217875-Is-there-code-for-X.3F/topic/StronglyMeaurable.2Ediv.E2.82.80/with/569988425), I probably should also change the name of [MeasureTheory.StronglyMeasurable.div](https://leanprover-community.github.io/mathlib4_docs/Mathlib/MeasureTheory/Function/StronglyMeasurable/Basic.html#MeasureTheory.StronglyMeasurable.div) into `StronglyMeasurable.div'` according to the docstring of [ContinuousDiv](https://leanprover-community.github.io/mathlib4_docs/Mathlib/Topology/Algebra/Group/Defs.html#ContinuousDiv). If I do this, then @to_additive will generate a theorem named `StronglyMeasurable.sub'`, which is a bit weird, so I am unsure whether I should change these names.
---
[](https://gitpod.io/from-referrer/)
|
t-measure-probability |
37/8 |
Mathlib/MeasureTheory/Function/StronglyMeasurable/AEStronglyMeasurable.lean,Mathlib/MeasureTheory/Function/StronglyMeasurable/Basic.lean,Mathlib/Probability/Process/Adapted.lean |
3 |
3 |
['CoolRmal', 'EtienneC30', 'github-actions'] |
kex-y assignee:kex-y |
27-21244 27 days ago |
27-25014 27 days ago |
35-68576 35 days |
| 35312 |
Komyyy author:Komyyy |
feat(Order/Filter/Pointwise): `((∀ᶠ|∃ᶠ) x in op f, p x) ↔ ((∀ᶠ|∃ᶠ) x in f, p (op x))` |
This lemma is required when I prove that $z \mapsto \sin^{-1} z^{-1}$ is not meromorphic at $0$:
```lean4
@[simp]
lemma Filter.frequently_inv {α : Type*} [Inv α] {f : Filter α} {p : α → Prop} :
(∃ᶠ a in f⁻¹, p a) ↔ (∃ᶠ a in f, p a⁻¹) :=
frequently_map
example : ¬(∀ᶠ z in 𝓝[≠] (0 : ℂ), sin⁻¹ z⁻¹ = 0) ↔ (∃ᶠ z in cobounded ℂ, sin z ≠ 0) := by
simp [← inv_cobounded₀]
```
So I added the simp lemmas of `(∀ᶠ|∃ᶠ) x in op f, p x` for unary operations `op` (`-f`, `f⁻¹` & `a • f`).
While I was at it, I also added the simp lemmas of `∃ᶠ x in pure a, p x` & `∃ᶠ x in (0|1), p x`, which previously existed only for the `∀ᶠ` versions.
Binary operation versions will be added if necessary.
Appendix: Full proof of that $z \mapsto \sin^{-1} z^{-1}$ is not meromorphic at $0$
```lean4
module
import Mathlib.Analysis.Meromorphic.Basic
import Mathlib.Analysis.SpecialFunctions.Trigonometric.Complex
import Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv
import Mathlib.Analysis.SpecificLimits.RCLike
open Complex Filter Bornology
open scoped Real Topology Pointwise
@[simp]
lemma Filter.frequently_inv {α : Type*} [Inv α] {f : Filter α} {p : α → Prop} :
(∃ᶠ a in f⁻¹, p a) ↔ (∃ᶠ a in f, p a⁻¹) :=
frequently_map
example : ¬MeromorphicAt (fun z => sin⁻¹ z⁻¹) 0 := by
apply mt MeromorphicAt.eventually_eq_zero_or_eventually_ne_zero
conv => equals (∃ᶠ z in cobounded ℂ, sin z ≠ 0) ∧ (∃ᶠ z in cobounded ℂ, sin z = 0) =>
simp [← inv_cobounded₀]
constructor
case left =>
have ht : Tendsto (fun x : ℝ ↦ ↑x * I) (cobounded ℝ) (cobounded ℂ) := by
have ht₁ : Tendsto ((↑) : ℝ → ℂ) (cobounded ℝ) (cobounded ℂ) :=
RCLike.tendsto_ofReal_cobounded_cobounded ℂ
have ht₂ : Tendsto (fun z : ℂ ↦ z * I) (cobounded ℂ) (cobounded ℂ) :=
tendsto_mul_right_cobounded (by simp)
exact ht₂.comp ht₁
refine ht.frequently_map _ (fun x ↦ mt ?_) (eventually_ne_cobounded 0).frequently
rw [sin_eq_zero_iff]
rintro ⟨n, hn⟩
simpa using congr_arg im hn
case right =>
suffices ht : Tendsto (fun n : ℤ ↦ (↑n * ↑π : ℂ)) atTop (cobounded ℂ) by
apply ht.frequently; simp [sin_int_mul_pi, atTop_neBot]
have ht₁ : Tendsto ((↑) : ℤ → ℝ) atTop (cobounded ℝ) := tendsto_intCast_atTop_cobounded
have ht₂ : Tendsto ((↑) : ℝ → ℂ) (cobounded ℝ) (cobounded ℂ) :=
RCLike.tendsto_ofReal_cobounded_cobounded ℂ
have ht₃ : Tendsto (fun z : ℂ ↦ z * ↑π) (cobounded ℂ) (cobounded ℂ) :=
tendsto_mul_right_cobounded (by simp)
exact ht₃.comp <| ht₂.comp ht₁
```
---
[](https://gitpod.io/from-referrer/)
|
t-order |
24/0 |
Mathlib/Order/Filter/Map.lean,Mathlib/Order/Filter/Pointwise.lean |
2 |
1 |
['github-actions'] |
Vierkantor assignee:Vierkantor |
10-50099 10 days ago |
17-81203 17 days ago |
17-81238 17 days |
| 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 |
| 33832 |
alreadydone author:alreadydone |
feat(Algebra): localization preserves unique factorization |
---
- [x] depends on: #33851
[](https://gitpod.io/from-referrer/)
|
awaiting-author
t-algebra
maintainer-merge
label:t-algebra$ |
143/12 |
Mathlib.lean,Mathlib/Algebra/BigOperators/Group/Finset/Basic.lean,Mathlib/Algebra/GroupWithZero/Associated.lean,Mathlib/GroupTheory/MonoidLocalization/Basic.lean,Mathlib/GroupTheory/MonoidLocalization/UniqueFactorization.lean,Mathlib/RingTheory/Localization/Defs.lean |
6 |
11 |
['Vierkantor', 'dagurtomas', 'github-actions', 'mathlib4-dependent-issues-bot'] |
Vierkantor assignee:Vierkantor |
26-77272 26 days ago |
26-77276 26 days ago |
17-27113 17 days |
| 31141 |
peabrainiac author:peabrainiac |
feat(Analysis/Calculus): parametric integrals over smooth functions are smooth |
Show that for any smooth function `f : H × ℝ → E`, the parametric integral `fun x ↦ ∫ t in a..b, f (x, t) ∂μ` is smooth too.
The argument proceeds inductively, using the fact that derivatives of parametric integrals can themselves be computed as parametric integrals. The necessary lemmas on derivatives of parametric integrals already existed, but took some work to apply due to their generality; we state some convenient special cases.
---
- [x] depends on: #31077
[](https://gitpod.io/from-referrer/)
|
awaiting-author
t-analysis
maintainer-merge
|
470/12 |
Mathlib/Analysis/Calculus/ParametricIntegral.lean,Mathlib/Analysis/Calculus/ParametricIntervalIntegral.lean,Mathlib/MeasureTheory/Integral/DominatedConvergence.lean,Mathlib/Topology/NhdsWithin.lean,Mathlib/Topology/Separation/Regular.lean |
5 |
36 |
['fpvandoorn', 'github-actions', 'j-loreaux', 'mathlib4-dependent-issues-bot', 'mathlib4-merge-conflict-bot', 'peabrainiac', 'sgouezel'] |
j-loreaux assignee:j-loreaux |
21-12700 21 days ago |
21-12700 21 days ago |
33-85043 33 days |
| 34193 |
bwangpj author:bwangpj |
feat(Topology/Algebra/Ring): ContinuousAddEquiv.mulLeft, mulRight |
The additive homeomorphism from a topological ring to itself, induced by left/right multiplication by a unit.
From FLT.
---
[](https://gitpod.io/from-referrer/)
|
t-topology
maintainer-merge
FLT
|
25/0 |
Mathlib/Topology/Algebra/Ring/Basic.lean |
1 |
10 |
['bwangpj', 'dagurtomas', 'eric-wieser', 'github-actions', 'riccardobrasca'] |
dagurtomas assignee:dagurtomas |
13-25566 13 days ago |
19-76688 19 days ago |
42-27712 42 days |
| 35682 |
chenson2018 author:chenson2018 |
chore(Computability/Partrec): remove `linter.flexible` exceptions |
This removes all `set_option linter.flexible false` from this module. Some proofs simply required moving around the usage of `simp`. For others I used `grind`, which is permitted to follow flexible tactics. In all cases I prioritized leaving the structure of the proof either mostly as-is or slightly improving readability.
---
[](https://gitpod.io/from-referrer/)
|
t-computability
maintainer-merge
|
23/41 |
Mathlib/Computability/Partrec.lean |
1 |
6 |
['chenson2018', 'github-actions', 'grunweg'] |
nobody |
8-58344 8 days ago |
8-61006 8 days ago |
8-80950 8 days |
| 33364 |
BoltonBailey author:BoltonBailey |
feat(Analysis/Convex/SimplicialComplex): add AbstractSimplicialComplex + constructions |
This adds the concept of [abstract simplicial complex](https://en.wikipedia.org/wiki/Abstract_simplicial_complex) (and refactors SimplicialComplex in terms of it).
It also adds constructions that makes it easy to define a simplicial complex for any index family of points which is downward closed and which is affinely independent. I also include a construction of (abstract and geometric) simplicial complexes associated with a SimpleGraph, where vertices become 0-faces and edges become 1-faces, which could be useful later in defining the topological notion of a graph embedding.
Co-authored-by: Claude Opus 4.5
---
- [x] depends on: #35115
[](https://gitpod.io/from-referrer/)
|
t-analysis
maintainer-merge
t-algebraic-topology
|
440/16 |
Mathlib.lean,Mathlib/AlgebraicTopology/SimplicialComplex/Basic.lean,Mathlib/Analysis/Convex/SimplicialComplex/AffineIndependentUnion.lean,Mathlib/Analysis/Convex/SimplicialComplex/Basic.lean,Mathlib/Data/Sym/Sym2.lean,Mathlib/LinearAlgebra/AffineSpace/Independent.lean,Mathlib/Order/UpperLower/Relative.lean,Mathlib/Tactic/Linter/DirectoryDependency.lean |
8 |
30 |
['BoltonBailey', 'denisgorod', 'eric-wieser', 'github-actions', 'j-loreaux', 'mathlib-dependent-issues', 'mathlib-merge-conflicts', 'peabrainiac'] |
j-loreaux assignee:j-loreaux |
7-37670 7 days ago |
7-82333 7 days ago |
19-42742 19 days |
| 33449 |
yuanyi-350 author:yuanyi-350 |
feat(ProbabilityTheory): Add Poisson limit theorem |
---
[](https://gitpod.io/from-referrer/)
|
t-measure-probability
maintainer-merge
file-removed
|
127/3 |
Mathlib.lean,Mathlib/Probability/Distributions/Poisson/Basic.lean,Mathlib/Probability/Distributions/Poisson/PoissonLimitThm.lean,Mathlib/Probability/ProbabilityMassFunction/Binomial.lean,docs/1000.yaml |
5 |
24 |
['EtienneC30', 'github-actions', 'vihdzp'] |
EtienneC30 assignee:EtienneC30 |
5-79344 5 days ago |
5-80452 5 days ago |
62-8891 62 days |
| 35081 |
tb65536 author:tb65536 |
feat(Topology/Algebra/Group/Extension): define short exact sequence of topological groups |
This PR defines a short exact sequence of topological groups to be a closed embedding followed by an open quotient map (extracted from #32672).
---
[](https://gitpod.io/from-referrer/)
|
t-topology
maintainer-merge
|
57/0 |
Mathlib.lean,Mathlib/Topology/Algebra/Group/Extension.lean |
2 |
3 |
['dagurtomas', 'github-actions'] |
dagurtomas assignee:dagurtomas |
5-68428 5 days ago |
5-68429 5 days ago |
22-8563 22 days |
| 35567 |
goliath-klein author:goliath-klein |
refactor(PiTensorProduct/{InjectiveNorm, ProjectiveNorm}): Golfs |
This PR cleans up the proofs in
Analysis/Normed/Module/PiTensorProduct/{InjectiveSeminorm.lean, ProjectiveSeminorm.lean}
In addition, it performs the following minor structural changes:
* Weaken assumptions from `NontriviallyNormedField 𝕜` to `NormedField 𝕜` where possible
* The proofs showing that `projectiveSeminorm` actually defines a `Seminorm` are split off into separate lemmas. This mimics the idiom used e.g. in `Analysis.Normed.Modula.Operator.Basic` to define the operator norm.
* Register a `Nonempty x.lifts` instance in PiTensorProduct.lean, to avoid creating a half-dozen local instances.
This is the first in a series of three PRs with the goal to [deprecate `PiTensorProuduct.injectiveSeminorm`](https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/injectiveSeminorm/with/568798633).
---
Co-authored-by: Davood H. T. Tehrani
[](https://gitpod.io/from-referrer/)
|
new-contributor
maintainer-merge
|
101/158 |
Mathlib/Analysis/Normed/Module/PiTensorProduct/InjectiveSeminorm.lean,Mathlib/Analysis/Normed/Module/PiTensorProduct/ProjectiveSeminorm.lean,Mathlib/LinearAlgebra/PiTensorProduct.lean |
3 |
10 |
['github-actions', 'goliath-klein', 'leanprover-radar', 'tb65536'] |
sgouezel assignee:sgouezel |
3-50021 3 days ago |
11-86097 11 days ago |
12-4043 12 days |
| 35639 |
vihdzp author:vihdzp |
chore(Order/SuccPred/Limit): use `to_dual` on everything that was missing |
---
- [x] depends on: #34882
[](https://gitpod.io/from-referrer/)
|
maintainer-merge |
36/135 |
Mathlib/Data/Fintype/Card.lean,Mathlib/Order/Bounds/Basic.lean,Mathlib/Order/SuccPred/Limit.lean |
3 |
4 |
['JovanGerb', 'github-actions', 'mathlib-dependent-issues'] |
adamtopaz assignee:adamtopaz |
2-59140 2 days ago |
2-59140 2 days ago |
10-2074 10 days |
| 32987 |
kim-em author:kim-em |
feat: pipeline downloads and decompression in `cache get` |
This PR modifies `lake exe cache get` to decompress files as they download, rather than waiting for all downloads to complete first.
Previously the cache system had two sequential phases: download all files using `curl --parallel`, then decompress all files using a single `leantar` call. Now a background task spawns sequential batched `leantar` calls to decompress files as downloads complete, pipelining network I/O and disk I/O.
🤖 Prepared with Claude Code
- [x] depends on: #34667 |
t-meta
maintainer-merge
|
190/35 |
Cache/IO.lean,Cache/Requests.lean |
2 |
65 |
['Vierkantor', 'eric-wieser', 'github-actions', 'joneugster', 'kim-em', 'mathlib-dependent-issues', 'mathlib-merge-conflicts'] |
joneugster assignee:joneugster |
2-27066 2 days ago |
5-15014 5 days ago |
61-13684 61 days |
| 35637 |
vihdzp author:vihdzp |
chore(Topology/Order/LeftRight): use `to_dual` |
This overlaps with #35635, but the overlap is small (and that PR still needs some work, so I'd rather get this out of the way first).
---
[](https://gitpod.io/from-referrer/)
|
maintainer-merge |
32/26 |
Mathlib/Order/Interval/Set/LinearOrder.lean,Mathlib/Tactic/Translate/ToDual.lean,Mathlib/Topology/Order/LeftRight.lean |
3 |
8 |
['JovanGerb', 'github-actions', 'vihdzp'] |
jcommelin assignee:jcommelin |
2-10405 2 days ago |
2-10405 2 days ago |
10-30412 10 days |
| 35974 |
justus-springer author:justus-springer |
feat(Algebra/Polynomial/Bivariate): more API for swap |
---
[](https://gitpod.io/from-referrer/)
|
t-algebra
maintainer-merge
label:t-algebra$ |
10/0 |
Mathlib/Algebra/Polynomial/Bivariate.lean |
1 |
2 |
['github-actions', 'robin-carlier'] |
nobody |
1-76353 1 day ago |
1-76353 1 day ago |
2-8347 2 days |
| 35513 |
vihdzp author:vihdzp |
refactor: redefine `Order.cof` for a preorder |
... instead of using an unbundled relation. This makes it easier to work with, and avoids some `swap rᶜ` incantations.
There are still a bunch of lemmas that make use of unbundled order relations; these will get fixed in follow-up PRs.
---
- [x] depends on: #35517
- [x] depends on: #35519
[](https://gitpod.io/from-referrer/)
|
t-order
maintainer-merge
t-set-theory
|
220/241 |
Mathlib/CategoryTheory/Presentable/IsCardinalFiltered.lean,Mathlib/Order/Cofinal.lean,Mathlib/SetTheory/Cardinal/Cofinality.lean |
3 |
9 |
['SnirBroshi', 'YaelDillies', 'github-actions', 'mathlib-dependent-issues', 'mathlib-merge-conflicts', 'vihdzp'] |
b-mehta assignee:b-mehta |
1-57717 1 day ago |
7-14676 7 days ago |
8-33648 8 days |
| 35850 |
vihdzp author:vihdzp |
refactor: nicer definition for ordinal logarithm |
By leveraging the API on `Order.IsNormal`, we can define the ordinal logarithm in a way that more immediately proves the characterizing Galois connection.
Note that this removes `Ordinal.log_def` and `Ordinal.succ_log_def` without deprecation - these are auxiliary results that should have been private and are tedious to re-prove.
---
- [x] depends on: #35849
[](https://gitpod.io/from-referrer/)
|
maintainer-merge
t-set-theory
|
40/69 |
Mathlib/SetTheory/Ordinal/Exponential.lean |
1 |
8 |
['YaelDillies', 'github-actions', 'mathlib-dependent-issues', 'vihdzp'] |
nobody |
2-21824 2 days ago |
2-28215 2 days ago |
5-13031 5 days |
| 26293 |
RemyDegenne author:RemyDegenne |
feat: tightness from convergence of characteristic functions |
If the characteristic functions of a sequence of measures `μ : ℕ → Measure E` on a finite dimensional inner product space converge pointwise to a function which is continuous at 0, then `{μ n | n}` is tight.
---
- [x] depends on: #24846
- [ ] depends on: #26292
[](https://gitpod.io/from-referrer/)
---
*This PR continues the work from #24949.*
*Original PR: https://github.com/leanprover-community/mathlib4/pull/24949* |
blocked-by-other-PR
t-measure-probability
|
352/2 |
Mathlib.lean,Mathlib/MeasureTheory/Measure/TightCharFun.lean,Mathlib/MeasureTheory/Measure/TightNormed.lean |
3 |
3 |
['github-actions', 'mathlib4-dependent-issues-bot', 'mathlib4-merge-conflict-bot'] |
nobody |
23-20635 23 days ago |
23-21651 23 days ago |
0-2 2 seconds |
| 29996 |
vihdzp author:vihdzp |
chore(Order/Concept): `IsIntent` and `IsExtent` |
We define predicates for a set to be an intent/extent, and use them to define alternate constructors for a concept. Using these, we golf the complete lattice instances.
The fields `Concept.intent` and `Concept.extent` already existed, and these serve as unbundled versions of them.
---
- [x] depends on: #30484
[](https://gitpod.io/from-referrer/)
|
t-order
maintainer-merge
|
161/114 |
Mathlib/Order/Concept.lean |
1 |
50 |
['Vierkantor', 'YaelDillies', 'github-actions', 'linesthatinterlace', 'mathlib-dependent-issues', 'mathlib4-merge-conflict-bot', 'plp127', 'vihdzp'] |
YaelDillies assignee:YaelDillies |
11-71320 11 days ago |
12-29997 12 days ago |
33-37521 33 days |
| 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 |
| 33832 |
alreadydone author:alreadydone |
feat(Algebra): localization preserves unique factorization |
---
- [x] depends on: #33851
[](https://gitpod.io/from-referrer/)
|
awaiting-author
t-algebra
maintainer-merge
label:t-algebra$ |
143/12 |
Mathlib.lean,Mathlib/Algebra/BigOperators/Group/Finset/Basic.lean,Mathlib/Algebra/GroupWithZero/Associated.lean,Mathlib/GroupTheory/MonoidLocalization/Basic.lean,Mathlib/GroupTheory/MonoidLocalization/UniqueFactorization.lean,Mathlib/RingTheory/Localization/Defs.lean |
6 |
11 |
['Vierkantor', 'dagurtomas', 'github-actions', 'mathlib4-dependent-issues-bot'] |
Vierkantor assignee:Vierkantor |
26-77272 26 days ago |
26-77276 26 days ago |
17-27113 17 days |
| 31141 |
peabrainiac author:peabrainiac |
feat(Analysis/Calculus): parametric integrals over smooth functions are smooth |
Show that for any smooth function `f : H × ℝ → E`, the parametric integral `fun x ↦ ∫ t in a..b, f (x, t) ∂μ` is smooth too.
The argument proceeds inductively, using the fact that derivatives of parametric integrals can themselves be computed as parametric integrals. The necessary lemmas on derivatives of parametric integrals already existed, but took some work to apply due to their generality; we state some convenient special cases.
---
- [x] depends on: #31077
[](https://gitpod.io/from-referrer/)
|
awaiting-author
t-analysis
maintainer-merge
|
470/12 |
Mathlib/Analysis/Calculus/ParametricIntegral.lean,Mathlib/Analysis/Calculus/ParametricIntervalIntegral.lean,Mathlib/MeasureTheory/Integral/DominatedConvergence.lean,Mathlib/Topology/NhdsWithin.lean,Mathlib/Topology/Separation/Regular.lean |
5 |
36 |
['fpvandoorn', 'github-actions', 'j-loreaux', 'mathlib4-dependent-issues-bot', 'mathlib4-merge-conflict-bot', 'peabrainiac', 'sgouezel'] |
j-loreaux assignee:j-loreaux |
21-12700 21 days ago |
21-12700 21 days ago |
33-85043 33 days |
| 34193 |
bwangpj author:bwangpj |
feat(Topology/Algebra/Ring): ContinuousAddEquiv.mulLeft, mulRight |
The additive homeomorphism from a topological ring to itself, induced by left/right multiplication by a unit.
From FLT.
---
[](https://gitpod.io/from-referrer/)
|
t-topology
maintainer-merge
FLT
|
25/0 |
Mathlib/Topology/Algebra/Ring/Basic.lean |
1 |
10 |
['bwangpj', 'dagurtomas', 'eric-wieser', 'github-actions', 'riccardobrasca'] |
dagurtomas assignee:dagurtomas |
13-25566 13 days ago |
19-76688 19 days ago |
42-27712 42 days |
| 35682 |
chenson2018 author:chenson2018 |
chore(Computability/Partrec): remove `linter.flexible` exceptions |
This removes all `set_option linter.flexible false` from this module. Some proofs simply required moving around the usage of `simp`. For others I used `grind`, which is permitted to follow flexible tactics. In all cases I prioritized leaving the structure of the proof either mostly as-is or slightly improving readability.
---
[](https://gitpod.io/from-referrer/)
|
t-computability
maintainer-merge
|
23/41 |
Mathlib/Computability/Partrec.lean |
1 |
6 |
['chenson2018', 'github-actions', 'grunweg'] |
nobody |
8-58344 8 days ago |
8-61006 8 days ago |
8-80950 8 days |
| 33364 |
BoltonBailey author:BoltonBailey |
feat(Analysis/Convex/SimplicialComplex): add AbstractSimplicialComplex + constructions |
This adds the concept of [abstract simplicial complex](https://en.wikipedia.org/wiki/Abstract_simplicial_complex) (and refactors SimplicialComplex in terms of it).
It also adds constructions that makes it easy to define a simplicial complex for any index family of points which is downward closed and which is affinely independent. I also include a construction of (abstract and geometric) simplicial complexes associated with a SimpleGraph, where vertices become 0-faces and edges become 1-faces, which could be useful later in defining the topological notion of a graph embedding.
Co-authored-by: Claude Opus 4.5
---
- [x] depends on: #35115
[](https://gitpod.io/from-referrer/)
|
t-analysis
maintainer-merge
t-algebraic-topology
|
440/16 |
Mathlib.lean,Mathlib/AlgebraicTopology/SimplicialComplex/Basic.lean,Mathlib/Analysis/Convex/SimplicialComplex/AffineIndependentUnion.lean,Mathlib/Analysis/Convex/SimplicialComplex/Basic.lean,Mathlib/Data/Sym/Sym2.lean,Mathlib/LinearAlgebra/AffineSpace/Independent.lean,Mathlib/Order/UpperLower/Relative.lean,Mathlib/Tactic/Linter/DirectoryDependency.lean |
8 |
30 |
['BoltonBailey', 'denisgorod', 'eric-wieser', 'github-actions', 'j-loreaux', 'mathlib-dependent-issues', 'mathlib-merge-conflicts', 'peabrainiac'] |
j-loreaux assignee:j-loreaux |
7-37670 7 days ago |
7-82333 7 days ago |
19-42742 19 days |
| 33449 |
yuanyi-350 author:yuanyi-350 |
feat(ProbabilityTheory): Add Poisson limit theorem |
---
[](https://gitpod.io/from-referrer/)
|
t-measure-probability
maintainer-merge
file-removed
|
127/3 |
Mathlib.lean,Mathlib/Probability/Distributions/Poisson/Basic.lean,Mathlib/Probability/Distributions/Poisson/PoissonLimitThm.lean,Mathlib/Probability/ProbabilityMassFunction/Binomial.lean,docs/1000.yaml |
5 |
24 |
['EtienneC30', 'github-actions', 'vihdzp'] |
EtienneC30 assignee:EtienneC30 |
5-79344 5 days ago |
5-80452 5 days ago |
62-8891 62 days |
| 35081 |
tb65536 author:tb65536 |
feat(Topology/Algebra/Group/Extension): define short exact sequence of topological groups |
This PR defines a short exact sequence of topological groups to be a closed embedding followed by an open quotient map (extracted from #32672).
---
[](https://gitpod.io/from-referrer/)
|
t-topology
maintainer-merge
|
57/0 |
Mathlib.lean,Mathlib/Topology/Algebra/Group/Extension.lean |
2 |
3 |
['dagurtomas', 'github-actions'] |
dagurtomas assignee:dagurtomas |
5-68428 5 days ago |
5-68429 5 days ago |
22-8563 22 days |
| 35567 |
goliath-klein author:goliath-klein |
refactor(PiTensorProduct/{InjectiveNorm, ProjectiveNorm}): Golfs |
This PR cleans up the proofs in
Analysis/Normed/Module/PiTensorProduct/{InjectiveSeminorm.lean, ProjectiveSeminorm.lean}
In addition, it performs the following minor structural changes:
* Weaken assumptions from `NontriviallyNormedField 𝕜` to `NormedField 𝕜` where possible
* The proofs showing that `projectiveSeminorm` actually defines a `Seminorm` are split off into separate lemmas. This mimics the idiom used e.g. in `Analysis.Normed.Modula.Operator.Basic` to define the operator norm.
* Register a `Nonempty x.lifts` instance in PiTensorProduct.lean, to avoid creating a half-dozen local instances.
This is the first in a series of three PRs with the goal to [deprecate `PiTensorProuduct.injectiveSeminorm`](https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/injectiveSeminorm/with/568798633).
---
Co-authored-by: Davood H. T. Tehrani
[](https://gitpod.io/from-referrer/)
|
new-contributor
maintainer-merge
|
101/158 |
Mathlib/Analysis/Normed/Module/PiTensorProduct/InjectiveSeminorm.lean,Mathlib/Analysis/Normed/Module/PiTensorProduct/ProjectiveSeminorm.lean,Mathlib/LinearAlgebra/PiTensorProduct.lean |
3 |
10 |
['github-actions', 'goliath-klein', 'leanprover-radar', 'tb65536'] |
sgouezel assignee:sgouezel |
3-50021 3 days ago |
11-86097 11 days ago |
12-4043 12 days |
| 35639 |
vihdzp author:vihdzp |
chore(Order/SuccPred/Limit): use `to_dual` on everything that was missing |
---
- [x] depends on: #34882
[](https://gitpod.io/from-referrer/)
|
maintainer-merge |
36/135 |
Mathlib/Data/Fintype/Card.lean,Mathlib/Order/Bounds/Basic.lean,Mathlib/Order/SuccPred/Limit.lean |
3 |
4 |
['JovanGerb', 'github-actions', 'mathlib-dependent-issues'] |
adamtopaz assignee:adamtopaz |
2-59140 2 days ago |
2-59140 2 days ago |
10-2074 10 days |
| 32987 |
kim-em author:kim-em |
feat: pipeline downloads and decompression in `cache get` |
This PR modifies `lake exe cache get` to decompress files as they download, rather than waiting for all downloads to complete first.
Previously the cache system had two sequential phases: download all files using `curl --parallel`, then decompress all files using a single `leantar` call. Now a background task spawns sequential batched `leantar` calls to decompress files as downloads complete, pipelining network I/O and disk I/O.
🤖 Prepared with Claude Code
- [x] depends on: #34667 |
t-meta
maintainer-merge
|
190/35 |
Cache/IO.lean,Cache/Requests.lean |
2 |
65 |
['Vierkantor', 'eric-wieser', 'github-actions', 'joneugster', 'kim-em', 'mathlib-dependent-issues', 'mathlib-merge-conflicts'] |
joneugster assignee:joneugster |
2-27066 2 days ago |
5-15014 5 days ago |
61-13684 61 days |
| 35637 |
vihdzp author:vihdzp |
chore(Topology/Order/LeftRight): use `to_dual` |
This overlaps with #35635, but the overlap is small (and that PR still needs some work, so I'd rather get this out of the way first).
---
[](https://gitpod.io/from-referrer/)
|
maintainer-merge |
32/26 |
Mathlib/Order/Interval/Set/LinearOrder.lean,Mathlib/Tactic/Translate/ToDual.lean,Mathlib/Topology/Order/LeftRight.lean |
3 |
8 |
['JovanGerb', 'github-actions', 'vihdzp'] |
jcommelin assignee:jcommelin |
2-10405 2 days ago |
2-10405 2 days ago |
10-30412 10 days |
| 35974 |
justus-springer author:justus-springer |
feat(Algebra/Polynomial/Bivariate): more API for swap |
---
[](https://gitpod.io/from-referrer/)
|
t-algebra
maintainer-merge
label:t-algebra$ |
10/0 |
Mathlib/Algebra/Polynomial/Bivariate.lean |
1 |
2 |
['github-actions', 'robin-carlier'] |
nobody |
1-76353 1 day ago |
1-76353 1 day ago |
2-8347 2 days |
| 35513 |
vihdzp author:vihdzp |
refactor: redefine `Order.cof` for a preorder |
... instead of using an unbundled relation. This makes it easier to work with, and avoids some `swap rᶜ` incantations.
There are still a bunch of lemmas that make use of unbundled order relations; these will get fixed in follow-up PRs.
---
- [x] depends on: #35517
- [x] depends on: #35519
[](https://gitpod.io/from-referrer/)
|
t-order
maintainer-merge
t-set-theory
|
220/241 |
Mathlib/CategoryTheory/Presentable/IsCardinalFiltered.lean,Mathlib/Order/Cofinal.lean,Mathlib/SetTheory/Cardinal/Cofinality.lean |
3 |
9 |
['SnirBroshi', 'YaelDillies', 'github-actions', 'mathlib-dependent-issues', 'mathlib-merge-conflicts', 'vihdzp'] |
b-mehta assignee:b-mehta |
1-57717 1 day ago |
7-14676 7 days ago |
8-33648 8 days |
| 32245 |
erdOne author:erdOne |
feat(RingTheory): the `coassoc_simps` simp set |
From Toric
Co-authored-by: Yaël Dillies
---
[](https://gitpod.io/from-referrer/)
|
t-meta
maintainer-merge
toric
t-ring-theory
|
815/0 |
Mathlib.lean,Mathlib/RingTheory/Coalgebra/CoassocSimps.lean,Mathlib/Tactic/Attr/Register.lean,MathlibTest/RingTheory/CoassocSimps.lean |
4 |
22 |
['erdOne', 'github-actions', 'joneugster', 'riccardobrasca'] |
b-mehta, joneugster, mattrobball assignee:joneugster assignee:b-mehta assignee:mattrobball |
0-75109 20 hours ago |
5-5781 5 days ago |
36-57121 36 days |
| 35331 |
SnirBroshi author:SnirBroshi |
feat(SimpleGraph/Subgraph): small things about `spanningCoe` and a small golf |
---
Three unrelated things in the same file, each too small to be its own PR.
[](https://gitpod.io/from-referrer/)
|
t-combinatorics
maintainer-merge
|
13/4 |
Mathlib/Combinatorics/SimpleGraph/Subgraph.lean |
1 |
3 |
['YaelDillies', 'github-actions'] |
YaelDillies assignee:YaelDillies |
0-66232 18 hours ago |
0-85116 23 hours ago |
17-48210 17 days |
| 34881 |
CBirkbeck author:CBirkbeck |
feat(ModularForm/NumberTheory/Delta): Define the delta function |
We define the Delta function on the upper half plane and show how it transforms under the slash operator, this is in preparation to proving it is a modular form.
---
[](https://gitpod.io/from-referrer/)
|
t-number-theory
maintainer-merge
|
251/0 |
Mathlib.lean,Mathlib/Analysis/Complex/SqrtDeriv.lean,Mathlib/Analysis/Complex/UpperHalfPlane/Basic.lean,Mathlib/Analysis/RCLike/Sqrt.lean,Mathlib/NumberTheory/ModularForms/Delta.lean,Mathlib/Topology/Algebra/InfiniteSum/Basic.lean |
6 |
50 |
['CBirkbeck', 'faenuccio', 'github-actions', 'joneugster', 'loefflerd'] |
faenuccio and loefflerd assignee:loefflerd assignee:faenuccio |
0-17740 4 hours ago |
1-17767 1 day ago |
12-61217 12 days |
| 35850 |
vihdzp author:vihdzp |
refactor: nicer definition for ordinal logarithm |
By leveraging the API on `Order.IsNormal`, we can define the ordinal logarithm in a way that more immediately proves the characterizing Galois connection.
Note that this removes `Ordinal.log_def` and `Ordinal.succ_log_def` without deprecation - these are auxiliary results that should have been private and are tedious to re-prove.
---
- [x] depends on: #35849
[](https://gitpod.io/from-referrer/)
|
maintainer-merge
t-set-theory
|
40/69 |
Mathlib/SetTheory/Ordinal/Exponential.lean |
1 |
8 |
['YaelDillies', 'github-actions', 'mathlib-dependent-issues', 'vihdzp'] |
nobody |
2-21824 2 days ago |
2-28215 2 days ago |
5-13031 5 days |
| 36124 |
chrisflav author:chrisflav |
feat(AlgebraicGeometry): `fromTildeΓ` is an isomorphism given a global presentation |
---
[](https://gitpod.io/from-referrer/)
|
t-algebraic-geometry
maintainer-merge
|
13/0 |
Mathlib/AlgebraicGeometry/Modules/Tilde.lean |
1 |
2 |
['erdOne', 'github-actions'] |
nobody |
0-10041 2 hours ago |
0-10041 2 hours ago |
0-10956 3 hours |
| 26293 |
RemyDegenne author:RemyDegenne |
feat: tightness from convergence of characteristic functions |
If the characteristic functions of a sequence of measures `μ : ℕ → Measure E` on a finite dimensional inner product space converge pointwise to a function which is continuous at 0, then `{μ n | n}` is tight.
---
- [x] depends on: #24846
- [ ] depends on: #26292
[](https://gitpod.io/from-referrer/)
---
*This PR continues the work from #24949.*
*Original PR: https://github.com/leanprover-community/mathlib4/pull/24949* |
blocked-by-other-PR
t-measure-probability
|
352/2 |
Mathlib.lean,Mathlib/MeasureTheory/Measure/TightCharFun.lean,Mathlib/MeasureTheory/Measure/TightNormed.lean |
3 |
3 |
['github-actions', 'mathlib4-dependent-issues-bot', 'mathlib4-merge-conflict-bot'] |
nobody |
23-20635 23 days ago |
23-21651 23 days ago |
0-2 2 seconds |
| 29996 |
vihdzp author:vihdzp |
chore(Order/Concept): `IsIntent` and `IsExtent` |
We define predicates for a set to be an intent/extent, and use them to define alternate constructors for a concept. Using these, we golf the complete lattice instances.
The fields `Concept.intent` and `Concept.extent` already existed, and these serve as unbundled versions of them.
---
- [x] depends on: #30484
[](https://gitpod.io/from-referrer/)
|
t-order
maintainer-merge
|
161/114 |
Mathlib/Order/Concept.lean |
1 |
50 |
['Vierkantor', 'YaelDillies', 'github-actions', 'linesthatinterlace', 'mathlib-dependent-issues', 'mathlib4-merge-conflict-bot', 'plp127', 'vihdzp'] |
YaelDillies assignee:YaelDillies |
11-71320 11 days ago |
12-29997 12 days ago |
33-37521 33 days |
| 36013 |
pfaffelh author:pfaffelh |
feat(Topology/Compactness/CompactSystem): introduce compact Systems |
A compact system is a set systems with the property that, whenever a countable intersections of sets in the set system is empty, there is a finite subset of sets with empty intersection. These are needed e.g. in measure theory if one wants to show sigma-additivity of a set function on a ring.
Main result: The set of sets which are either compact and closed, or univ, is a compact system.
Co-authored-by: Rémy Degenne [remydegenne@gmail.com](mailto:remydegenne@gmail.com)
---
Continues work from #25899
[](https://gitpod.io/from-referrer/)
|
|
238/0 |
Mathlib.lean,Mathlib/Data/Set/Dissipate.lean,Mathlib/MeasureTheory/PiSystem.lean,Mathlib/Topology/Compactness/CompactSystem.lean |
4 |
1 |
['github-actions'] |
nobody |
0-18981 5 hours ago |
1-17422 1 day ago |
1-53159 1 day |
| 35233 |
kim-em author:kim-em |
chore: lake shake --add-public --keep-implied --keep-prefix --fix |
This PR runs `lake shake --add-public --keep-implied --keep-prefix --fix` again after https://github.com/leanprover-community/mathlib4/pull/34511, picking up the remaining 28 files that now have suggestions.
🤖 Prepared with Claude Code |
awaiting-author
maintainer-merge
large-import
|
13/12 |
Mathlib/Algebra/Category/ModuleCat/Sheaf/Quasicoherent.lean,Mathlib/Analysis/Distribution/SchwartzSpace/Basic.lean,Mathlib/Data/Nat/Init.lean,Mathlib/LinearAlgebra/Matrix/Kronecker.lean,Mathlib/LinearAlgebra/TensorProduct/Basic.lean,Mathlib/LinearAlgebra/TensorProduct/Defs.lean,Mathlib/LinearAlgebra/TensorProduct/Map.lean,Mathlib/Logic/Basic.lean,Mathlib/Logic/Relation.lean,Mathlib/RingTheory/MatrixAlgebra.lean,Mathlib/Tactic/Hint.lean,Mathlib/Tactic/Linter/FindDeprecations.lean,Mathlib/Tactic/Nontriviality/Core.lean,Mathlib/Tactic/NormNum/Result.lean,Mathlib/Tactic/Order/CollectFacts.lean,Mathlib/Tactic/Tauto.lean |
16 |
16 |
['TwoFX', 'Vierkantor', 'adomani', 'bryangingechen', 'github-actions', 'joneugster', 'kim-em', 'mathlib-merge-conflicts', 'mathlib-splicebot'] |
nobody |
0-4792 1 hour ago |
0-11741 3 hours ago |
11-83992 11 days |
| 36068 |
justus-springer author:justus-springer |
feat(RingTheory/Polynomial/GaussLemma): `mem_lifts` lemma for primitive polynomials |
A lemma that's needed for the proof of Lüroth's theorem.
---
[](https://gitpod.io/from-referrer/)
|
maintainer-merge
t-ring-theory
|
24/0 |
Mathlib/RingTheory/Polynomial/GaussLemma.lean |
1 |
6 |
['erdOne', 'github-actions', 'robin-carlier'] |
nobody |
0-2282 38 minutes ago |
0-2282 37 minutes ago |
0-80994 22 hours |
| 34528 |
Maldooor author:Maldooor |
feat: Reproducing Kernel Hilbert Spaces and Moore's theorem |
We define vector-valued reproducing Kernel Hilbert spaces, which are Hilbert spaces of
functions, as well as characterize these spaces in terms of infinite-dimensional
positive semidefinite matrices.
Co-authored-by: Yaël Dillies
---
[](https://gitpod.io/from-referrer/)
|
t-analysis
maintainer-merge
|
326/5 |
Mathlib.lean,Mathlib/Analysis/InnerProductSpace/Continuous.lean,Mathlib/Analysis/InnerProductSpace/Reproducing.lean,docs/references.bib |
4 |
17 |
['Maldooor', 'YaelDillies', 'faenuccio', 'github-actions'] |
j-loreaux assignee:j-loreaux |
0-8014 2 hours ago |
1-3829 1 day ago |
6-81350 6 days |
| 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 |
FR-vdash-bot author:FR-vdash-bot |
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
t-order
awaiting-zulip
label:t-algebra$ |
146/44 |
Mathlib/Algebra/Order/GroupWithZero/Canonical.lean,Mathlib/Algebra/Order/GroupWithZero/Unbundled.lean |
2 |
11 |
['FR-vdash-bot', 'YaelDillies', 'github-actions', 'j-loreaux'] |
nobody |
469-9522 1 year ago |
469-9522 1 year ago |
0-0 0 seconds |
| 8370 |
eric-wieser author:eric-wieser |
refactor(Analysis/NormedSpace/Exponential): remove the `𝕂` argument from `exp` |
This argument is still needed for almost all the lemmas, which means it can longer be found by unification.
We keep around `expSeries 𝕂 A`, as it's needed for talking about the radius of convergence over different base fields.
This is a prerequisite for #8372, as we can't merge the functions until they have the same interface.\
Zulip thread: [#mathlib4 > Real.exp @ 💬](https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/Real.2Eexp/near/401602245)
---
[](https://gitpod.io/from-referrer/)
This is started from the mathport output on https://github.com/leanprover-community/mathlib/pull/19244 |
merge-conflict
t-analysis
awaiting-zulip
|
432/387 |
Mathlib/Analysis/CStarAlgebra/Exponential.lean,Mathlib/Analysis/CStarAlgebra/Spectrum.lean,Mathlib/Analysis/Normed/Algebra/Exponential.lean,Mathlib/Analysis/Normed/Algebra/MatrixExponential.lean,Mathlib/Analysis/Normed/Algebra/QuaternionExponential.lean,Mathlib/Analysis/Normed/Algebra/Spectrum.lean,Mathlib/Analysis/Normed/Algebra/TrivSqZeroExt.lean,Mathlib/Analysis/NormedSpace/DualNumber.lean,Mathlib/Analysis/SpecialFunctions/ContinuousFunctionalCalculus/ExpLog.lean,Mathlib/Analysis/SpecialFunctions/Exponential.lean,Mathlib/Analysis/SpecialFunctions/Trigonometric/Series.lean |
11 |
29 |
['YaelDillies', 'eric-wieser', 'girving', 'github-actions', 'j-loreaux', 'kbuzzard', 'leanprover-community-bot-assistant', 'urkud'] |
nobody |
313-51299 10 months ago |
324-79929 10 months ago |
0-0 0 seconds |
| 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
merge-conflict
new-contributor
t-computability
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 |
302-59199 9 months ago |
302-59204 9 months ago |
0-0 0 seconds |
| 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 |
242-39548 7 months ago |
242-39548 7 months ago |
0-0 0 seconds |
| 25218 |
kckennylau author:kckennylau |
feat(AlgebraicGeometry): Tate normal form of elliptic curves |
---
[](https://gitpod.io/from-referrer/)
|
merge-conflict
t-algebraic-geometry
new-contributor
awaiting-zulip
|
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 |
242-38386 7 months ago |
242-38387 7 months ago |
0-0 0 seconds |
| 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 |
merge-conflict
t-analysis
t-algebra
slow-typeclass-synthesis
awaiting-zulip
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 |
182-54031 6 months ago |
182-54032 6 months ago |
0-20585 5 hours |
| 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
awaiting-zulip
file-removed
|
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 |
139-31241 4 months ago |
139-31242 4 months ago |
0-1 1 second |
| 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/)
|
merge-conflict
t-meta
t-category-theory
new-contributor
awaiting-zulip
large-import
|
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 |
111-42115 3 months ago |
111-42115 3 months ago |
1-18384 1 day |
| 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/)
|
awaiting-author
merge-conflict
new-contributor
t-computability
awaiting-zulip
|
307/5 |
Mathlib/Computability/NFA.lean |
1 |
27 |
['TpmKranz', 'YaelDillies', 'dupuisf', 'github-actions', 'leanprover-community-bot-assistant', 'meithecatte', 'rudynicolop'] |
nobody |
106-59247 3 months ago |
288-81806 9 months ago |
0-0 0 seconds |
| 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/)
|
awaiting-author
merge-conflict
new-contributor
t-computability
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 |
105-75488 3 months ago |
105-75489 3 months ago |
0-0 0 seconds |
| 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
new-contributor
t-computability
awaiting-zulip
|
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 |
105-26256 3 months ago |
105-26257 3 months ago |
0-0 0 seconds |
| 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 |
104-84522 3 months ago |
534-58247 1 year ago |
0-0 0 seconds |
| 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
awaiting-zulip
t-data
|
629/0 |
Mathlib.lean,Mathlib/Data/QuotType.lean,MathlibTest/QuotType.lean |
3 |
20 |
['YaelDillies', 'astrainfinita', 'github-actions', 'mathlib4-merge-conflict-bot', 'plp127', 'vihdzp'] |
nobody |
83-66368 2 months ago |
84-11434 2 months ago |
0-81 1 minute |
| 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/) |
merge-conflict
t-analysis
awaiting-zulip
|
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 |
56-34681 1 month ago |
56-34682 1 month ago |
8-31111 8 days |
| 32828 |
Hagb author:Hagb |
feat(Algebra/Order/Group/Defs): add `IsOrderedAddMonoid.toIsOrderedCancelAddMonoid'` |
It is similar to `IsOrderedAddMonoid.toIsOrderedCancelAddMonoid`, while with different hypotheses.
The conclusion `IsOrderedCancelMonoid α` on
`IsOrderedAddMonoid.toIsOrderedCancelAddMonoid` still holds when the hypothesis `CommGroup α` is weakened to `CancelCommMonoid α` while `PartialOrder α` is strengthened to `LinearOrder α`.
---
[`IsOrderedAddMonoid.toIsOrderedCancelAddMonoid`](https://leanprover-community.github.io/mathlib4_docs/find/?pattern=IsOrderedAddMonoid.toIsOrderedCancelAddMonoid#doc) and `IsOrderedAddMonoid.toIsOrderedCancelAddMonoid'`:
https://github.com/leanprover-community/mathlib4/blob/97f78b1a4311fed1844b94f1c069219a48a098e1/Mathlib/Algebra/Order/Group/Defs.lean#L52-L62
[](https://gitpod.io/from-referrer/)
|
t-algebra
awaiting-zulip
label:t-algebra$ |
4/0 |
Mathlib/Algebra/Order/Group/Defs.lean |
1 |
8 |
['Garmelon', 'Vierkantor', 'artie2000', 'github-actions', 'leanprover-radar'] |
eric-wieser assignee:eric-wieser |
40-83516 1 month ago |
40-83516 1 month ago |
40-42357 40 days |
| 34396 |
dupuisf author:dupuisf |
feat: notation for `Ring.inverse` |
This PR adds the global notation `x⁻¹ʳ` for `Ring.inverse x`, and a few extra API lemmas about it.
---
[](https://gitpod.io/from-referrer/)
|
t-algebra
awaiting-zulip
label:t-algebra$ |
58/19 |
Mathlib/Algebra/GroupWithZero/Units/Basic.lean |
1 |
1 |
['github-actions'] |
nobody |
38-36547 1 month ago |
38-36564 1 month ago |
0-1 1 second |
| 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
|
531/0 |
Mathlib.lean,Mathlib/Combinatorics/Enumerative/Partition/EulerComb.lean |
2 |
5 |
['chiyunhsu', 'github-actions', 'tb65536', 'vihdzp'] |
b-mehta assignee:b-mehta |
34-1934 1 month ago |
34-1934 1 month ago |
42-25715 42 days |
| 34656 |
vihdzp author:vihdzp |
refactor: review `exists_irreducible_of_degree_pos` theorems |
This PR does the following:
- Rename `exists_irreducible_of_degree_pos` to `exists_irreducible_dvd_of_degree_pos`. The previous name reads as if this were proving that an irreducible polynomial of any positive degree exists.
- Deprecate variants which differ only in the spelling of `0 < f.degree`. We already have quite a lot of API for converting between `natDegree` and `degree`, and we should just use that instead.
---
[](https://gitpod.io/from-referrer/)
|
t-algebra
awaiting-zulip
t-ring-theory
label:t-algebra$ |
9/4 |
Mathlib/RingTheory/Polynomial/UniqueFactorization.lean |
1 |
4 |
['github-actions', 'tb65536', 'vihdzp'] |
nobody |
31-24000 1 month ago |
31-24000 1 month ago |
0-49595 13 hours |
| 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/)
|
t-algebra
new-contributor
awaiting-zulip
label:t-algebra$ |
300/2 |
Mathlib.lean,Mathlib/LinearAlgebra/PiTensorProduct.lean,Mathlib/LinearAlgebra/PiTensorProduct/Set.lean |
3 |
28 |
['PrParadoxy', 'dagurtomas', 'eric-wieser', 'github-actions', 'goliath-klein', 'leanprover-radar', 'mathlib4-dependent-issues-bot', 'mathlib4-merge-conflict-bot'] |
dagurtomas assignee:dagurtomas |
31-14539 1 month ago |
31-14539 1 month ago |
10-66980 10 days |
| 32742 |
LTolDe author:LTolDe |
feat(MeasureTheory/Constructions/Polish/Basic): add class SuslinSpace |
add new class `SuslinSpace` for a topological space that is an analytic set in itself
This will be useful to prove the **Effros Theorem**, see [zulip thread](https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/Effros.20Theorem/with/558712441).
---
[](https://gitpod.io/from-referrer/)
|
t-measure-probability
new-contributor
awaiting-zulip
|
4/0 |
Mathlib/MeasureTheory/Constructions/Polish/Basic.lean |
1 |
9 |
['ADedecker', 'LTolDe', 'dupuisf', 'github-actions', 'jcommelin'] |
PatrickMassot assignee:PatrickMassot |
31-14344 1 month ago |
31-14344 1 month ago |
25-83455 25 days |
| 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/)
|
awaiting-zulip
t-ring-theory
|
844/0 |
Mathlib.lean,Mathlib/RingTheory/PowerSeries/Composition.lean |
2 |
3 |
['Paul-Lez', 'github-actions', 'vihdzp'] |
nobody |
22-60353 22 days ago |
22-60353 22 days ago |
0-10 10 seconds |
| 33441 |
dupuisf author:dupuisf |
feat: add `LawfulInv` class for types with an inverse that behaves like `Ring.inverse` |
This PR introduces a new typeclass `LawfulInv` for types which have an `Inv` instance that is equal to zero on non-invertible elements. This is meant to replace `Ring.inverse`. The current plan is to do this refactor in several steps:
1. This PR, which only introduces the class and adds instances for matrices and continuous linear maps.
2. Add instances for all C*-algebras, and make `CStarAlgebra` extend this.
3. Deprecate `Ring.inverse`.
---
[](https://gitpod.io/from-referrer/)
|
merge-conflict
t-algebra
awaiting-zulip
label:t-algebra$ |
185/27 |
Mathlib/Algebra/GroupWithZero/Defs.lean,Mathlib/Algebra/GroupWithZero/Invertible.lean,Mathlib/Algebra/GroupWithZero/Units/Basic.lean,Mathlib/LinearAlgebra/Matrix/NonsingularInverse.lean,Mathlib/LinearAlgebra/Matrix/PosDef.lean,Mathlib/RingTheory/DividedPowers/Padic.lean,Mathlib/Topology/Algebra/Module/Equiv.lean |
7 |
35 |
['dupuisf', 'eric-wieser', 'github-actions', 'j-loreaux', 'mathlib-merge-conflicts', 'mathlib4-merge-conflict-bot', 'plp127'] |
nobody |
14-32692 14 days ago |
14-32692 14 days ago |
7-54145 7 days |
| 34245 |
staroperator author:staroperator |
feat(Data/Set): add `Set.Uncountable` |
There are `Set` specialized shortcuts `Set.Finite`, `Set.Infinite` and `Set.Countable`, but lacking `Set.Uncountable`. I find this useful in #34246.
---
[](https://gitpod.io/from-referrer/)
|
awaiting-zulip
t-data
|
82/4 |
Mathlib/Analysis/Real/Cardinality.lean,Mathlib/Data/Set/Countable.lean,Mathlib/SetTheory/Cardinal/Basic.lean |
3 |
16 |
['github-actions', 'joneugster', 'staroperator', 'vihdzp'] |
joneugster assignee:joneugster |
14-28358 14 days ago |
14-28358 14 days ago |
12-21583 12 days |
| 34077 |
kbuzzard author:kbuzzard |
perf: increase priority of instSMulOfMul |
#31040 deprecated `Mul.toSMul` in place of the core instance `instSMulOfMul`, which is at a lowered priority of 910. This PR undeprecates it and makes it a higher priority instance (1100) which seems better for mathlib.
---
[](https://gitpod.io/from-referrer/)
This PR follows the philosophy seen in Mathlib's `Algebra.id : Algebra R R`, which also has raised priority. The idea is the same as `Algebra.id`: if you're looking for an instance of `Algebra R S` with R not equal to S then `Algebra.id` is extremely likely to fail quickly in practice, and if you're looking for an instance of `Algebra R R` then `Algebra.id` is unambiguously the right answer so should be tried ASAP. However the instance is defined so early in mathlib that in in practice it is tried last unless the priority is raised. The same philosophy holds here; if you're looking for an instance of `SMul X X` then you absolutely want to try `Mul.toSMul` first and if you're looking for an instance of `SMul X Y` with Y not X then `Mul.toSMul` will in practice be quick to fail.
This PR was inspired by #33908 (another "this should be quick to fail and if it fits then it's almost certainly what we want" prio change) which made an instance of `IsScalarTower R A A` high priority and gave a performance boost. This PR also gives a performance boost.
Note that the performance in #31040 looks very bad but the radar output is incorrect; there was a hardware change between the two runs. In fact #31040 produced no changes in profiling, as one might expect.
I don't know the correct way to change the priority of a core instance in mathlib, and I didn't know if just changing the priority naively would work repo-wide rather than just file-wide, which was why this PR introduces a second instance.
Zulip discussion at [#mathlib4 > priority hacks](https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/priority.20hacks/with/574353616)
|
t-algebra
awaiting-zulip
label:t-algebra$ |
3/9 |
Mathlib/Algebra/Group/Action/Defs.lean,Mathlib/Algebra/Group/Action/Units.lean |
2 |
25 |
['alreadydone', 'github-actions', 'kbuzzard', 'leanprover-radar'] |
jcommelin assignee:jcommelin |
14-26443 14 days ago |
14-26443 14 days ago |
4-19293 4 days |
| 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/)
|
awaiting-author
t-linter
awaiting-zulip
|
55/7 |
Mathlib/Tactic/Linter/Whitespace.lean |
1 |
19 |
['adomani', 'eric-wieser', 'github-actions', 'grunweg', 'joneugster', 'kim-em', 'leanprover-bot', 'leanprover-radar', 'mathlib-bors', 'mathlib4-merge-conflict-bot'] |
grunweg assignee:grunweg |
14-25118 14 days ago |
14-25216 14 days ago |
66-73556 66 days |
| 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
|
23/2 |
Mathlib/Tactic/Linter/TextBased.lean |
1 |
4 |
['github-actions', 'grunweg', 'joneugster', 'vihdzp'] |
nobody |
11-82137 11 days ago |
13-17972 13 days ago |
0-3845 1 hour |
| 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/)
|
awaiting-zulip
t-data
|
10/10 |
Mathlib/Control/Monad/Cont.lean,Mathlib/Control/Monad/Writer.lean |
2 |
4 |
['Shreyas4991', 'eric-wieser', 'github-actions'] |
nobody |
11-60651 11 days ago |
11-60652 11 days ago |
0-18707 5 hours |
| 33972 |
YuvalFilmus author:YuvalFilmus |
feat(Analysis/Polynomial/Order): polynomial has fixed sign beyond largest root |
We prove that a polynomial has fixed sign beyond its largest root.
One could also prove similar results about the smallest root, but they will be more awkward since they will depend on the parity of the (natural) degree; suggestions welcome (perhaps for a future PR).
---
[](https://gitpod.io/from-referrer/)
|
t-analysis
awaiting-zulip
|
134/0 |
Mathlib.lean,Mathlib/Analysis/Polynomial/Order.lean |
2 |
13 |
['YuvalFilmus', 'artie2000', 'github-actions', 'mathlib-merge-conflicts', 'urkud', 'vihdzp'] |
ADedecker and urkud assignee:urkud assignee:ADedecker |
8-79297 8 days ago |
8-81283 8 days ago |
39-75082 39 days |
| 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/)
|
awaiting-author
merge-conflict
new-contributor
t-computability
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 |
6-19490 6 days ago |
105-74579 3 months ago |
0-0 0 seconds |
| 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/)
|
awaiting-author
merge-conflict
new-contributor
t-computability
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 |
6-19474 6 days ago |
288-80881 9 months ago |
0-0 0 seconds |
| 23929 |
meithecatte author:meithecatte |
feat(Computability/NFA): improve bound on pumping lemma |
---
- [x] depends on: #25321
[](https://gitpod.io/from-referrer/)
|
awaiting-author
new-contributor
t-computability
awaiting-zulip
|
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 |
5-39503 5 days ago |
5-39503 5 days ago |
0-0 0 seconds |
| 34649 |
peabrainiac author:peabrainiac |
feat(Analysis/Calculus/ContDiff): add notation `ℕ∞ω` for `WithTop ℕ∞` |
Add a `ContDiff`-scoped notation `ℕ∞ω` for `WithTop ℕ∞`, accompanying the existing notations `∞` and `ω` for `(⊤ : ℕ∞) : ℕ∞ω` and `⊤ : ℕ∞ω`.
---
[Zulip discussion](https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/RFC.3A.20notation.20for.20.60WithTop.20.E2.84.95.E2.88.9E.60/near/573917824)
I've also replaced `WithTop ℕ∞` with this new notation already in the files that mention it the most, but not in all files yet; many mention `WithTop ℕ∞` just a couple of times but don't open the `ContDiff` namespace. I'm not sure whether that should be taken as a sign to not make the notation scoped, or whether the solution is just to `open scoped ContDiff` in these files or not use the notation there.
[](https://gitpod.io/from-referrer/)
|
awaiting-author
merge-conflict
t-differential-geometry
t-analysis
awaiting-zulip
|
221/218 |
Mathlib/Analysis/Calculus/BumpFunction/FiniteDimension.lean,Mathlib/Analysis/Calculus/ContDiff/Basic.lean,Mathlib/Analysis/Calculus/ContDiff/Bounds.lean,Mathlib/Analysis/Calculus/ContDiff/CPolynomial.lean,Mathlib/Analysis/Calculus/ContDiff/Comp.lean,Mathlib/Analysis/Calculus/ContDiff/Defs.lean,Mathlib/Analysis/Calculus/ContDiff/Deriv.lean,Mathlib/Analysis/Calculus/ContDiff/FTaylorSeries.lean,Mathlib/Analysis/Calculus/ContDiff/Operations.lean,Mathlib/Analysis/Calculus/FDeriv/Symmetric.lean,Mathlib/Analysis/Calculus/ImplicitContDiff.lean,Mathlib/Analysis/Calculus/IteratedDeriv/Defs.lean,Mathlib/Analysis/Calculus/VectorField.lean,Mathlib/Analysis/Distribution/ContDiffMapSupportedIn.lean,Mathlib/Analysis/SpecialFunctions/Log/Deriv.lean,Mathlib/Analysis/SpecialFunctions/Trigonometric/InverseDeriv.lean,Mathlib/Geometry/Manifold/Algebra/LieGroup.lean,Mathlib/Geometry/Manifold/Algebra/Monoid.lean,Mathlib/Geometry/Manifold/Algebra/SmoothFunctions.lean,Mathlib/Geometry/Manifold/Algebra/Structures.lean,Mathlib/Geometry/Manifold/ContMDiff/Atlas.lean,Mathlib/Geometry/Manifold/ContMDiff/Basic.lean,Mathlib/Geometry/Manifold/ContMDiff/Defs.lean,Mathlib/Geometry/Manifold/Instances/Sphere.lean,Mathlib/Geometry/Manifold/Instances/UnitsOfNormedAlgebra.lean,Mathlib/Geometry/Manifold/IsManifold/Basic.lean,Mathlib/Geometry/Manifold/VectorBundle/Basic.lean,Mathlib/Geometry/Manifold/VectorBundle/FiberwiseLinear.lean |
28 |
5 |
['github-actions', 'j-loreaux', 'mathlib-merge-conflicts', 'peabrainiac'] |
sgouezel assignee:sgouezel |
2-71442 2 days ago |
14-31367 14 days ago |
8-6287 8 days |
| 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/)
|
awaiting-author
awaiting-zulip
t-data
|
162/0 |
Mathlib/Data/Quot.lean,Mathlib/Data/Set/Image.lean,Mathlib/Data/SetLike/Basic.lean,Mathlib/Data/Setoid/Basic.lean |
4 |
5 |
['SnirBroshi', 'TwoFX', 'eric-wieser', 'github-actions', 'mathlib-merge-conflicts'] |
TwoFX assignee:TwoFX |
1-21704 1 day ago |
1-21704 1 day ago |
36-69524 36 days |