Maintainers page: short tasks

Are you a maintainer with just a short amount of time? The following kinds of pull requests could be relevant for you.

If you realise you actually have a bit more time, you can also look at the page for reviewers, or look at the triage page!
This dashboard was last updated on: October 05, 2025 at 20:02 UTC

Stale ready-to-merge'd PRs

There are currently no stale PRs labelled auto-merge-after-CI or ready-to-merge. Congratulations!

Stale maintainer-merge'd PRs

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
25945 adomani
author:adomani
 feat: the empty line in commands linter This linter flags empty lines within a command. It allows empty lines within doc-strings, module-docs and a couple of other "sensible" places. It also skips files that are likely to contain meta-code, since there the use of empty lines in definition is more widespread. This PR continues the work from #25236. large-import t-linter maintainer-merge awaiting-author 375/7 Mathlib.lean,Mathlib/Analysis/Meromorphic/FactorizedRational.lean,Mathlib/CategoryTheory/Comma/StructuredArrow/CommaMap.lean,Mathlib/Init.lean,Mathlib/RepresentationTheory/Homological/GroupHomology/LowDegree.lean,Mathlib/Tactic.lean,Mathlib/Tactic/Linter/EmptyLine.lean,MathlibTest/EmptyLine.lean 8 12 ['adomani', 'bryangingechen', 'eric-wieser', 'github-actions'] bryangingechen
assignee:bryangingechen
69-19925
2 months ago
69-19925
2 months ago
42-26074
42 days
24669 qawbecrdtey
author:qawbecrdtey
 feat(Analysis/Normed/Operator/LinearIsometry): added definition `LinearIsometryEquiv.prodComm` --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) This commit defines a `LinearIsometryEquiv`, and states some trivial theorems about it. ```lean def prodComm [Module R E₂] : E × E₂ ≃ₗᵢ[R] E₂ × E ``` maintainer-merge t-analysis awaiting-author 8/1 Mathlib/Analysis/Normed/Operator/LinearIsometry.lean 1 12 ['Ruben-VandeVelde', 'eric-wieser', 'faenuccio', 'github-actions', 'j-loreaux', 'jcommelin', 'qawbecrdtey'] faenuccio
assignee:faenuccio
27-66527
27 days ago
117-54359
3 months ago
32-83569
32 days
27292 gasparattila
author:gasparattila
 feat: asymptotic cone of a set This PR defines the asymptotic cone of a set in a normed affine space and proves its main properties. This is partial progress towards showing that an unbounded finite-dimensional convex set contains a ray. --- - [x] depends on: #27221 [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) maintainer-merge new-contributor t-analysis 466/0 Mathlib.lean,Mathlib/Analysis/Normed/Affine/AsymptoticCone.lean,Mathlib/Order/Filter/Map.lean,Mathlib/Topology/Algebra/AsymptoticCone.lean 4 45 ['AntoineChambert-Loir', 'YaelDillies', 'gasparattila', 'github-actions', 'mathlib4-dependent-issues-bot'] YaelDillies
assignee:YaelDillies
18-50033
18 days ago
61-11926
2 months ago
75-29458
75 days
26660 strihanje01
author:strihanje01
 feat(Combinatorics/Additive/VerySmallDoubling): weak non-commutative Kneser's theorem add theorem about the structure of a doubling smaller than the golden ratio --- - [x] depends on: #28653 [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) large-import maintainer-merge new-contributor t-combinatorics 215/41 Mathlib/Algebra/Group/Action/Pointwise/Finset.lean,Mathlib/Combinatorics/Additive/VerySmallDoubling.lean 2 79 ['YaelDillies', 'github-actions', 'mathlib4-dependent-issues-bot', 'mathlib4-merge-conflict-bot', 'strihanje01'] YaelDillies
assignee:YaelDillies
12-24604
12 days ago
12-57253
12 days ago
53-85629
53 days
26259 Raph-DG
author:Raph-DG
 feat(Topology): Connecting different notions of locally finite In this PR we connect the notions of local finiteness of an indexed family of sets (as in LocallyFinite) and of a set of sets (as in Function.locallyFinsuppWithin) --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) maintainer-merge t-topology 38/0 Mathlib/Topology/LocallyFinsupp.lean 1 18 ['Raph-DG', 'chrisflav', 'github-actions', 'jcommelin', 'kckennylau'] jcommelin
assignee:jcommelin
10-12762
10 days ago
10-38078
10 days ago
99-2065
99 days
29275 wwylele
author:wwylele
 feat(GroupTheory): add DivisibleHull This is part of Hahn embedding theorem #27268, where an a ordered group is first embedded in a divisible group / Q-module. I am aware at #25662 there is also an ongoing rewrite of `LocalizedModule` that this PR uses. Hopefully I avoided interfering it by using mostly with public API. --- - [x] depends on: #29277 - [x] depends on: #29388 - [x] depends on: #29386 [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) t-group-theory maintainer-merge 451/3 Mathlib.lean,Mathlib/Algebra/Order/Monoid/Defs.lean,Mathlib/Algebra/Order/Monoid/PNat.lean,Mathlib/Algebra/Order/Monoid/Unbundled/Pow.lean,Mathlib/Data/NNRat/Defs.lean,Mathlib/GroupTheory/DivisibleHull.lean 6 106 ['YaelDillies', 'github-actions', 'mathlib4-dependent-issues-bot', 'vihdzp', 'wwylele'] tb65536
assignee:tb65536
9-68485
9 days ago
17-7962
17 days ago
26-71561
26 days
29110 NotWearingPants
author:NotWearingPants
 feat(Counterexamples): Euler's sum of powers conjecture feat(Counterexamples): Euler's sum of powers conjecture --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) awaiting-zulip maintainer-merge new-contributor 158/0 Counterexamples.lean,Counterexamples/EulerSumOfPowers.lean 2 43 ['MichaelStollBayreuth', 'NotWearingPants', 'eric-wieser', 'github-actions', 'tb65536', 'urkud'] MichaelStollBayreuth
assignee:MichaelStollBayreuth
9-1053
9 days ago
9-1109
9 days ago
24-25032
24 days
29693 kckennylau
author:kckennylau
 feat(RingTheory): make Euclidean domain from DVR --- Zulip: https://leanprover.zulipchat.com/#narrow/channel/116395-maths/topic/Leading.20term.20of.20valuation/near/539666529 [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) t-ring-theory maintainer-merge 82/0 Mathlib/RingTheory/DiscreteValuationRing/Basic.lean 1 6 ['github-actions', 'kckennylau', 'pechersky'] chrisflav
assignee:chrisflav
7-68472
7 days ago
19-22693
19 days ago
19-68594
19 days
28395 joelriou
author:joelriou
 feat(AlgebraicTopology/SimplicialSet): nondegenerate simplices in the standard simplex In this PR, we show that `d`-dimensional nondegenerate simplices in `Δ[n]` identify to `Fin (d + 1) ↪o Fin (n + 1)`. (This PR also contains some general additional API for (non)degenerate simplices. For this reason, three definitions related to subcomplexes generated by a simplex had to be moved from `StdSimplex.lean` to `Subcomplex.lean`.) --- - [x] depends on: #28337 [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) t-algebraic-topology maintainer-merge 247/20 Mathlib/AlgebraicTopology/SimplicialSet/Degenerate.lean,Mathlib/AlgebraicTopology/SimplicialSet/Simplices.lean,Mathlib/AlgebraicTopology/SimplicialSet/StdSimplex.lean,Mathlib/AlgebraicTopology/SimplicialSet/Subcomplex.lean,Mathlib/Order/Hom/Basic.lean 5 24 ['github-actions', 'joelriou', 'mathlib4-dependent-issues-bot', 'mathlib4-merge-conflict-bot', 'robin-carlier'] robin-carlier
assignee:robin-carlier
6-13733
6 days ago
6-19079
6 days ago
24-76911
24 days
30111 sgouezel
author:sgouezel
 feat: composing a continuous multilinear map with continuous linear maps is analytic in both variables --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) maintainer-merge t-analysis 133/0 Mathlib/Analysis/Analytic/CPolynomial.lean,Mathlib/Analysis/NormedSpace/Multilinear/Basic.lean 2 15 ['github-actions', 'loefflerd', 'sgouezel'] nobody
2-33832
2 days ago
2-33832
2 days ago
2-63399
2 days
29759 NotWearingPants
author:NotWearingPants
 feat(Analysis/SpecificLimits/Fibonacci): prove that the ratio of consecutive Fibonacci numbers tends to the golden ratio --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) maintainer-merge new-contributor t-analysis 36/0 Mathlib.lean,Mathlib/Analysis/SpecificLimits/Fibonacci.lean 2 7 ['NotWearingPants', 'Ruben-VandeVelde', 'github-actions', 'kckennylau'] nobody
2-19185
2 days ago
2-19186
2 days ago
9-74562
9 days
30101 wwylele
author:wwylele
 feat(Algebra/HahnEmbedding): ArchimedeanStrata is non-empty This is a small part of #27268 (Hahn embedding theorem). Separated out for easy review while waiting for the other dependency. --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) large-import maintainer-merge t-algebra
label:t-algebra$
 8/0 Mathlib/Algebra/Order/Module/HahnEmbedding.lean 1 2 ['YaelDillies', 'github-actions'] nobody
1-38271
1 day ago
1-38271
1 day ago
4-77699
4 days
27370 euprunin
author:euprunin
 chore(Tactic/CancelDenoms): golf entire `cancel_factors_eq` using `grind` ---
Show trace profiling of cancel_factors_eq: 120 ms before, 46 ms after 🎉 ### Trace profiling of `cancel_factors_eq` before PR 27370 ```diff diff --git a/Mathlib/Tactic/CancelDenoms/Core.lean b/Mathlib/Tactic/CancelDenoms/Core.lean index c4b62d3e29..3ec2128994 100644 --- a/Mathlib/Tactic/CancelDenoms/Core.lean +++ b/Mathlib/Tactic/CancelDenoms/Core.lean @@ -80,6 +80,7 @@ theorem cancel_factors_le {α} [Field α] [LinearOrder α] [IsStrictOrderedRing · exact mul_pos had hbd · exact one_div_pos.2 hgcd +set_option trace.profiler true in theorem cancel_factors_eq {α} [Field α] {a b ad bd a' b' gcd : α} (ha : ad * a = a') (hb : bd * b = b') (had : ad ≠ 0) (hbd : bd ≠ 0) (hgcd : gcd ≠ 0) : (a = b) = (1 / gcd * (bd * a') = 1 / gcd * (ad * b')) := by ``` ``` ℹ [436/436] Built Mathlib.Tactic.CancelDenoms.Core (2.8s) info: Mathlib/Tactic/CancelDenoms/Core.lean:84:0: [Elab.command] [0.015258] theorem cancel_factors_eq {α} [Field α] {a b ad bd a' b' gcd : α} (ha : ad * a = a') (hb : bd * b = b') (had : ad ≠ 0) (hbd : bd ≠ 0) (hgcd : gcd ≠ 0) : (a = b) = (1 / gcd * (bd * a') = 1 / gcd * (ad * b')) := by rw [← ha, ← hb, ← mul_assoc bd, ← mul_assoc ad, mul_comm bd] ext; constructor · rintro rfl rfl · intro h simp only [← mul_assoc] at h refine mul_left_cancel₀ (mul_ne_zero ?_ ?_) h on_goal 1 => apply mul_ne_zero on_goal 1 => apply div_ne_zero · exact one_ne_zero all_goals assumption [Elab.definition.header] [0.014988] CancelDenoms.cancel_factors_eq info: Mathlib/Tactic/CancelDenoms/Core.lean:84:0: [Elab.async] [0.122474] elaborating proof of CancelDenoms.cancel_factors_eq [Elab.definition.value] [0.119890] CancelDenoms.cancel_factors_eq [Elab.step] [0.118614] rw [← ha, ← hb, ← mul_assoc bd, ← mul_assoc ad, mul_comm bd] ext; constructor · rintro rfl rfl · intro h simp only [← mul_assoc] at h refine mul_left_cancel₀ (mul_ne_zero ?_ ?_) h on_goal 1 => apply mul_ne_zero on_goal 1 => apply div_ne_zero · exact one_ne_zero all_goals assumption [Elab.step] [0.118601] rw [← ha, ← hb, ← mul_assoc bd, ← mul_assoc ad, mul_comm bd] ext; constructor · rintro rfl rfl · intro h simp only [← mul_assoc] at h refine mul_left_cancel₀ (mul_ne_zero ?_ ?_) h on_goal 1 => apply mul_ne_zero on_goal 1 => apply div_ne_zero · exact one_ne_zero all_goals assumption [Elab.step] [0.010324] rw [← ha, ← hb, ← mul_assoc bd, ← mul_assoc ad, mul_comm bd] [Elab.step] [0.010312] (rewrite [← ha, ← hb, ← mul_assoc bd, ← mul_assoc ad, mul_comm bd]; with_annotate_state"]" (try (with_reducible rfl))) [Elab.step] [0.010299] rewrite [← ha, ← hb, ← mul_assoc bd, ← mul_assoc ad, mul_comm bd]; with_annotate_state"]" (try (with_reducible rfl)) [Elab.step] [0.010291] rewrite [← ha, ← hb, ← mul_assoc bd, ← mul_assoc ad, mul_comm bd]; with_annotate_state"]" (try (with_reducible rfl)) [Elab.step] [0.105805] · intro h simp only [← mul_assoc] at h refine mul_left_cancel₀ (mul_ne_zero ?_ ?_) h on_goal 1 => apply mul_ne_zero on_goal 1 => apply div_ne_zero · exact one_ne_zero all_goals assumption [Elab.step] [0.105661] intro h simp only [← mul_assoc] at h refine mul_left_cancel₀ (mul_ne_zero ?_ ?_) h on_goal 1 => apply mul_ne_zero on_goal 1 => apply div_ne_zero · exact one_ne_zero all_goals assumption [Elab.step] [0.105650] intro h simp only [← mul_assoc] at h refine mul_left_cancel₀ (mul_ne_zero ?_ ?_) h on_goal 1 => apply mul_ne_zero on_goal 1 => apply div_ne_zero · exact one_ne_zero all_goals assumption [Elab.step] [0.043946] refine mul_left_cancel₀ (mul_ne_zero ?_ ?_) h [Elab.step] [0.043859] expected type: a = b, term mul_left_cancel₀ (mul_ne_zero ?_ ?_) h [Elab.step] [0.025447] expected type: ?m.103 * ?m.104 ≠ 0, term (mul_ne_zero ?_ ?_) [Elab.step] [0.025432] expected type: ?m.103 * ?m.104 ≠ 0, term mul_ne_zero ?_ ?_ [Meta.synthInstance] [0.019262] ✅️ NoZeroDivisors α [Elab.step] [0.021441] on_goal 1 => apply mul_ne_zero [Elab.step] [0.019543] apply mul_ne_zero [Elab.step] [0.019530] apply mul_ne_zero [Elab.step] [0.019514] apply mul_ne_zero [Meta.synthInstance] [0.013986] ✅️ NoZeroDivisors α [Elab.step] [0.018650] · exact one_ne_zero [Elab.step] [0.018355] exact one_ne_zero [Elab.step] [0.018309] exact one_ne_zero [Elab.step] [0.018269] exact one_ne_zero [Elab.step] [0.017827] expected type: 1 ≠ 0, term one_ne_zero [Meta.synthInstance] [0.012295] ✅️ NeZero 1 Build completed successfully (436 jobs). ``` ### Trace profiling of `cancel_factors_eq` after PR 27370 ```diff diff --git a/Mathlib/Tactic/CancelDenoms/Core.lean b/Mathlib/Tactic/CancelDenoms/Core.lean index c4b62d3e29..066f915189 100644 --- a/Mathlib/Tactic/CancelDenoms/Core.lean +++ b/Mathlib/Tactic/CancelDenoms/Core.lean @@ -80,20 +80,11 @@ theorem cancel_factors_le {α} [Field α] [LinearOrder α] [IsStrictOrderedRing · exact mul_pos had hbd · exact one_div_pos.2 hgcd +set_option trace.profiler true in theorem cancel_factors_eq {α} [Field α] {a b ad bd a' b' gcd : α} (ha : ad * a = a') (hb : bd * b = b') (had : ad ≠ 0) (hbd : bd ≠ 0) (hgcd : gcd ≠ 0) : (a = b) = (1 / gcd * (bd * a') = 1 / gcd * (ad * b')) := by - rw [← ha, ← hb, ← mul_assoc bd, ← mul_assoc ad, mul_comm bd] - ext; constructor - · rintro rfl - rfl - · intro h - simp only [← mul_assoc] at h - refine mul_left_cancel₀ (mul_ne_zero ?_ ?_) h - on_goal 1 => apply mul_ne_zero - on_goal 1 => apply div_ne_zero - · exact one_ne_zero - all_goals assumption + grind theorem cancel_factors_ne {α} [Field α] {a b ad bd a' b' gcd : α} (ha : ad * a = a') (hb : bd * b = b') (had : ad ≠ 0) (hbd : bd ≠ 0) (hgcd : gcd ≠ 0) : ``` ``` ℹ [436/436] Built Mathlib.Tactic.CancelDenoms.Core (3.1s) info: Mathlib/Tactic/CancelDenoms/Core.lean:84:0: [Elab.command] [0.034809] theorem cancel_factors_eq {α} [Field α] {a b ad bd a' b' gcd : α} (ha : ad * a = a') (hb : bd * b = b') (had : ad ≠ 0) (hbd : bd ≠ 0) (hgcd : gcd ≠ 0) : (a = b) = (1 / gcd * (bd * a') = 1 / gcd * (ad * b')) := by grind [Elab.definition.header] [0.014091] CancelDenoms.cancel_factors_eq info: Mathlib/Tactic/CancelDenoms/Core.lean:84:0: [Elab.async] [0.046425] elaborating proof of CancelDenoms.cancel_factors_eq [Elab.definition.value] [0.045869] CancelDenoms.cancel_factors_eq [Elab.step] [0.045340] grind [Elab.step] [0.045327] grind [Elab.step] [0.045311] grind info: Mathlib/Tactic/CancelDenoms/Core.lean:87:2: [Elab.async] [0.027621] Lean.addDecl [Kernel] [0.027585] ✅️ typechecking declarations [CancelDenoms.cancel_factors_eq._proof_1_1] Build completed successfully (436 jobs). ```
maintainer-merge t-meta easy 1/11 Mathlib/Tactic/CancelDenoms/Core.lean 1 9 ['euprunin', 'github-actions', 'grunweg', 'leanprover-bot', 'leanprover-community-mathlib4-bot'] alexjbest
assignee:alexjbest
1-16514
1 day ago
1-16515
1 day ago
74-75001
74 days
30174 mcdoll
author:mcdoll
 feat: the Hölder conjugate of an `ENNReal` --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) t-data maintainer-merge 4/0 Mathlib/Data/Real/ConjExponents.lean 1 2 ['github-actions', 'grunweg'] nobody
1-15930
1 day ago
1-15930
1 day ago
2-8997
2 days
24965 erdOne
author:erdOne
 refactor: Make `IsLocalHom` take unbundled map --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) maintainer-merge t-algebra merge-conflict awaiting-author
label:t-algebra$
 16/7 Mathlib/Algebra/Group/Units/Hom.lean,Mathlib/AlgebraicGeometry/Scheme.lean,Mathlib/Geometry/RingedSpace/LocallyRingedSpace.lean,Mathlib/Geometry/RingedSpace/LocallyRingedSpace/HasColimits.lean,Mathlib/Geometry/RingedSpace/OpenImmersion.lean 5 6 ['alreadydone', 'erdOne', 'eric-wieser', 'github-actions', 'leanprover-community-bot-assistant'] nobody
124-62512
4 months ago
124-62513
4 months ago
10-26015
10 days
26912 pechersky
author:pechersky
 chore(Algebra/Ring/Subring): simp tag `Subring.smul_def` s-multiplying by a subtype is easiest to manipulate when both terms are in the ambient type. Many places that had to use the _def lemma for a rewrite, or to include it in a simp set, no longer have to. Ported from #25308 --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) I found this being not-simp frustrating when talking about submodules over a valuation subring. maintainer-merge t-algebra merge-conflict
label:t-algebra$
 68/67 Mathlib/Algebra/Algebra/Subalgebra/Basic.lean,Mathlib/Algebra/Field/Subfield/Basic.lean,Mathlib/Algebra/Group/Subgroup/Actions.lean,Mathlib/Algebra/Group/Submonoid/MulAction.lean,Mathlib/Algebra/Module/LocalizedModule/Basic.lean,Mathlib/Algebra/Module/LocalizedModule/Exact.lean,Mathlib/Algebra/Module/LocalizedModule/IsLocalization.lean,Mathlib/Algebra/Module/LocalizedModule/Submodule.lean,Mathlib/Algebra/Ring/Periodic.lean,Mathlib/Algebra/Ring/Subring/Basic.lean,Mathlib/Algebra/Ring/Subsemiring/Basic.lean,Mathlib/Analysis/CStarAlgebra/Basic.lean,Mathlib/FieldTheory/KummerExtension.lean,Mathlib/GroupTheory/GroupAction/Defs.lean,Mathlib/GroupTheory/GroupAction/MultiplePrimitivity.lean,Mathlib/GroupTheory/GroupAction/MultipleTransitivity.lean,Mathlib/GroupTheory/GroupAction/SubMulAction/OfFixingSubgroup.lean,Mathlib/GroupTheory/GroupAction/SubMulAction/OfStabilizer.lean,Mathlib/LinearAlgebra/RootSystem/Irreducible.lean,Mathlib/LinearAlgebra/RootSystem/RootPositive.lean,Mathlib/LinearAlgebra/RootSystem/WeylGroup.lean,Mathlib/RingTheory/Etale/Kaehler.lean,Mathlib/RingTheory/LocalProperties/Projective.lean,Mathlib/RingTheory/Localization/InvSubmonoid.lean,Mathlib/RingTheory/OreLocalization/Basic.lean 25 19 ['artie2000', 'eric-wieser', 'github-actions', 'j-loreaux', 'linesthatinterlace', 'mathlib4-merge-conflict-bot', 'pechersky'] joelriou
assignee:joelriou
34-24003
1 month ago
34-24004
1 month ago
51-74059
51 days
28737 astrainfinita
author:astrainfinita
 refactor: deprecate `MulEquivClass` This PR continues the work from #18806. Original PR: https://github.com/leanprover-community/mathlib4/pull/18806 maintainer-merge t-algebra merge-conflict awaiting-author
label:t-algebra$
 67/77 Mathlib/Algebra/BigOperators/Finprod.lean,Mathlib/Algebra/Group/Equiv/Basic.lean,Mathlib/Algebra/Group/Equiv/Defs.lean,Mathlib/Algebra/Group/Irreducible/Lemmas.lean,Mathlib/Algebra/Group/Subgroup/Map.lean,Mathlib/Algebra/Group/Submonoid/Operations.lean,Mathlib/Algebra/Group/Units/Equiv.lean,Mathlib/Algebra/GroupWithZero/Equiv.lean,Mathlib/Algebra/GroupWithZero/NonZeroDivisors.lean,Mathlib/Algebra/Module/Equiv/Defs.lean,Mathlib/Algebra/Order/CauSeq/Basic.lean,Mathlib/Algebra/Order/Hom/Monoid.lean,Mathlib/Algebra/Prime/Lemmas.lean,Mathlib/Algebra/Ring/Divisibility/Basic.lean,Mathlib/Algebra/Ring/Equiv.lean,Mathlib/Algebra/Star/MonoidHom.lean,Mathlib/Combinatorics/Additive/FreimanHom.lean,Mathlib/GroupTheory/GroupExtension/Defs.lean,Mathlib/GroupTheory/Submonoid/Center.lean,Mathlib/LinearAlgebra/FreeModule/Finite/CardQuotient.lean,Mathlib/RingTheory/Bialgebra/Equiv.lean,Mathlib/RingTheory/Ideal/Norm/AbsNorm.lean,Mathlib/RingTheory/Multiplicity.lean,Mathlib/RingTheory/UniqueFactorizationDomain/NormalizedFactors.lean,Mathlib/Topology/Algebra/ContinuousMonoidHom.lean,Mathlib/Topology/Algebra/InfiniteSum/Basic.lean 26 20 ['Vierkantor', 'alreadydone', 'astrainfinita', 'github-actions', 'grunweg', 'leanprover-bot', 'leanprover-community-mathlib4-bot', 'mathlib4-merge-conflict-bot'] Vierkantor
assignee:Vierkantor
25-27863
25 days ago
25-27864
25 days ago
4-17723
4 days

All maintainer merge'd PRs

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
25945 adomani
author:adomani
 feat: the empty line in commands linter This linter flags empty lines within a command. It allows empty lines within doc-strings, module-docs and a couple of other "sensible" places. It also skips files that are likely to contain meta-code, since there the use of empty lines in definition is more widespread. This PR continues the work from #25236. large-import t-linter maintainer-merge awaiting-author 375/7 Mathlib.lean,Mathlib/Analysis/Meromorphic/FactorizedRational.lean,Mathlib/CategoryTheory/Comma/StructuredArrow/CommaMap.lean,Mathlib/Init.lean,Mathlib/RepresentationTheory/Homological/GroupHomology/LowDegree.lean,Mathlib/Tactic.lean,Mathlib/Tactic/Linter/EmptyLine.lean,MathlibTest/EmptyLine.lean 8 12 ['adomani', 'bryangingechen', 'eric-wieser', 'github-actions'] bryangingechen
assignee:bryangingechen
69-19925
2 months ago
69-19925
2 months ago
42-26074
42 days
24669 qawbecrdtey
author:qawbecrdtey
 feat(Analysis/Normed/Operator/LinearIsometry): added definition `LinearIsometryEquiv.prodComm` --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) This commit defines a `LinearIsometryEquiv`, and states some trivial theorems about it. ```lean def prodComm [Module R E₂] : E × E₂ ≃ₗᵢ[R] E₂ × E ``` maintainer-merge t-analysis awaiting-author 8/1 Mathlib/Analysis/Normed/Operator/LinearIsometry.lean 1 12 ['Ruben-VandeVelde', 'eric-wieser', 'faenuccio', 'github-actions', 'j-loreaux', 'jcommelin', 'qawbecrdtey'] faenuccio
assignee:faenuccio
27-66527
27 days ago
117-54359
3 months ago
32-83569
32 days
27292 gasparattila
author:gasparattila
 feat: asymptotic cone of a set This PR defines the asymptotic cone of a set in a normed affine space and proves its main properties. This is partial progress towards showing that an unbounded finite-dimensional convex set contains a ray. --- - [x] depends on: #27221 [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) maintainer-merge new-contributor t-analysis 466/0 Mathlib.lean,Mathlib/Analysis/Normed/Affine/AsymptoticCone.lean,Mathlib/Order/Filter/Map.lean,Mathlib/Topology/Algebra/AsymptoticCone.lean 4 45 ['AntoineChambert-Loir', 'YaelDillies', 'gasparattila', 'github-actions', 'mathlib4-dependent-issues-bot'] YaelDillies
assignee:YaelDillies
18-50033
18 days ago
61-11926
2 months ago
75-29458
75 days
26660 strihanje01
author:strihanje01
 feat(Combinatorics/Additive/VerySmallDoubling): weak non-commutative Kneser's theorem add theorem about the structure of a doubling smaller than the golden ratio --- - [x] depends on: #28653 [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) large-import maintainer-merge new-contributor t-combinatorics 215/41 Mathlib/Algebra/Group/Action/Pointwise/Finset.lean,Mathlib/Combinatorics/Additive/VerySmallDoubling.lean 2 79 ['YaelDillies', 'github-actions', 'mathlib4-dependent-issues-bot', 'mathlib4-merge-conflict-bot', 'strihanje01'] YaelDillies
assignee:YaelDillies
12-24604
12 days ago
12-57253
12 days ago
53-85629
53 days
26259 Raph-DG
author:Raph-DG
 feat(Topology): Connecting different notions of locally finite In this PR we connect the notions of local finiteness of an indexed family of sets (as in LocallyFinite) and of a set of sets (as in Function.locallyFinsuppWithin) --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) maintainer-merge t-topology 38/0 Mathlib/Topology/LocallyFinsupp.lean 1 18 ['Raph-DG', 'chrisflav', 'github-actions', 'jcommelin', 'kckennylau'] jcommelin
assignee:jcommelin
10-12762
10 days ago
10-38078
10 days ago
99-2065
99 days
29275 wwylele
author:wwylele
 feat(GroupTheory): add DivisibleHull This is part of Hahn embedding theorem #27268, where an a ordered group is first embedded in a divisible group / Q-module. I am aware at #25662 there is also an ongoing rewrite of `LocalizedModule` that this PR uses. Hopefully I avoided interfering it by using mostly with public API. --- - [x] depends on: #29277 - [x] depends on: #29388 - [x] depends on: #29386 [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) t-group-theory maintainer-merge 451/3 Mathlib.lean,Mathlib/Algebra/Order/Monoid/Defs.lean,Mathlib/Algebra/Order/Monoid/PNat.lean,Mathlib/Algebra/Order/Monoid/Unbundled/Pow.lean,Mathlib/Data/NNRat/Defs.lean,Mathlib/GroupTheory/DivisibleHull.lean 6 106 ['YaelDillies', 'github-actions', 'mathlib4-dependent-issues-bot', 'vihdzp', 'wwylele'] tb65536
assignee:tb65536
9-68485
9 days ago
17-7962
17 days ago
26-71561
26 days
29110 NotWearingPants
author:NotWearingPants
 feat(Counterexamples): Euler's sum of powers conjecture feat(Counterexamples): Euler's sum of powers conjecture --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) awaiting-zulip maintainer-merge new-contributor 158/0 Counterexamples.lean,Counterexamples/EulerSumOfPowers.lean 2 43 ['MichaelStollBayreuth', 'NotWearingPants', 'eric-wieser', 'github-actions', 'tb65536', 'urkud'] MichaelStollBayreuth
assignee:MichaelStollBayreuth
9-1053
9 days ago
9-1109
9 days ago
24-25032
24 days
29693 kckennylau
author:kckennylau
 feat(RingTheory): make Euclidean domain from DVR --- Zulip: https://leanprover.zulipchat.com/#narrow/channel/116395-maths/topic/Leading.20term.20of.20valuation/near/539666529 [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) t-ring-theory maintainer-merge 82/0 Mathlib/RingTheory/DiscreteValuationRing/Basic.lean 1 6 ['github-actions', 'kckennylau', 'pechersky'] chrisflav
assignee:chrisflav
7-68472
7 days ago
19-22693
19 days ago
19-68594
19 days
28395 joelriou
author:joelriou
 feat(AlgebraicTopology/SimplicialSet): nondegenerate simplices in the standard simplex In this PR, we show that `d`-dimensional nondegenerate simplices in `Δ[n]` identify to `Fin (d + 1) ↪o Fin (n + 1)`. (This PR also contains some general additional API for (non)degenerate simplices. For this reason, three definitions related to subcomplexes generated by a simplex had to be moved from `StdSimplex.lean` to `Subcomplex.lean`.) --- - [x] depends on: #28337 [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) t-algebraic-topology maintainer-merge 247/20 Mathlib/AlgebraicTopology/SimplicialSet/Degenerate.lean,Mathlib/AlgebraicTopology/SimplicialSet/Simplices.lean,Mathlib/AlgebraicTopology/SimplicialSet/StdSimplex.lean,Mathlib/AlgebraicTopology/SimplicialSet/Subcomplex.lean,Mathlib/Order/Hom/Basic.lean 5 24 ['github-actions', 'joelriou', 'mathlib4-dependent-issues-bot', 'mathlib4-merge-conflict-bot', 'robin-carlier'] robin-carlier
assignee:robin-carlier
6-13733
6 days ago
6-19079
6 days ago
24-76911
24 days
30111 sgouezel
author:sgouezel
 feat: composing a continuous multilinear map with continuous linear maps is analytic in both variables --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) maintainer-merge t-analysis 133/0 Mathlib/Analysis/Analytic/CPolynomial.lean,Mathlib/Analysis/NormedSpace/Multilinear/Basic.lean 2 15 ['github-actions', 'loefflerd', 'sgouezel'] nobody
2-33832
2 days ago
2-33832
2 days ago
2-63399
2 days
29759 NotWearingPants
author:NotWearingPants
 feat(Analysis/SpecificLimits/Fibonacci): prove that the ratio of consecutive Fibonacci numbers tends to the golden ratio --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) maintainer-merge new-contributor t-analysis 36/0 Mathlib.lean,Mathlib/Analysis/SpecificLimits/Fibonacci.lean 2 7 ['NotWearingPants', 'Ruben-VandeVelde', 'github-actions', 'kckennylau'] nobody
2-19185
2 days ago
2-19186
2 days ago
9-74562
9 days
30101 wwylele
author:wwylele
 feat(Algebra/HahnEmbedding): ArchimedeanStrata is non-empty This is a small part of #27268 (Hahn embedding theorem). Separated out for easy review while waiting for the other dependency. --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) large-import maintainer-merge t-algebra
label:t-algebra$
 8/0 Mathlib/Algebra/Order/Module/HahnEmbedding.lean 1 2 ['YaelDillies', 'github-actions'] nobody
1-38271
1 day ago
1-38271
1 day ago
4-77699
4 days
27370 euprunin
author:euprunin
 chore(Tactic/CancelDenoms): golf entire `cancel_factors_eq` using `grind` ---
Show trace profiling of cancel_factors_eq: 120 ms before, 46 ms after 🎉 ### Trace profiling of `cancel_factors_eq` before PR 27370 ```diff diff --git a/Mathlib/Tactic/CancelDenoms/Core.lean b/Mathlib/Tactic/CancelDenoms/Core.lean index c4b62d3e29..3ec2128994 100644 --- a/Mathlib/Tactic/CancelDenoms/Core.lean +++ b/Mathlib/Tactic/CancelDenoms/Core.lean @@ -80,6 +80,7 @@ theorem cancel_factors_le {α} [Field α] [LinearOrder α] [IsStrictOrderedRing · exact mul_pos had hbd · exact one_div_pos.2 hgcd +set_option trace.profiler true in theorem cancel_factors_eq {α} [Field α] {a b ad bd a' b' gcd : α} (ha : ad * a = a') (hb : bd * b = b') (had : ad ≠ 0) (hbd : bd ≠ 0) (hgcd : gcd ≠ 0) : (a = b) = (1 / gcd * (bd * a') = 1 / gcd * (ad * b')) := by ``` ``` ℹ [436/436] Built Mathlib.Tactic.CancelDenoms.Core (2.8s) info: Mathlib/Tactic/CancelDenoms/Core.lean:84:0: [Elab.command] [0.015258] theorem cancel_factors_eq {α} [Field α] {a b ad bd a' b' gcd : α} (ha : ad * a = a') (hb : bd * b = b') (had : ad ≠ 0) (hbd : bd ≠ 0) (hgcd : gcd ≠ 0) : (a = b) = (1 / gcd * (bd * a') = 1 / gcd * (ad * b')) := by rw [← ha, ← hb, ← mul_assoc bd, ← mul_assoc ad, mul_comm bd] ext; constructor · rintro rfl rfl · intro h simp only [← mul_assoc] at h refine mul_left_cancel₀ (mul_ne_zero ?_ ?_) h on_goal 1 => apply mul_ne_zero on_goal 1 => apply div_ne_zero · exact one_ne_zero all_goals assumption [Elab.definition.header] [0.014988] CancelDenoms.cancel_factors_eq info: Mathlib/Tactic/CancelDenoms/Core.lean:84:0: [Elab.async] [0.122474] elaborating proof of CancelDenoms.cancel_factors_eq [Elab.definition.value] [0.119890] CancelDenoms.cancel_factors_eq [Elab.step] [0.118614] rw [← ha, ← hb, ← mul_assoc bd, ← mul_assoc ad, mul_comm bd] ext; constructor · rintro rfl rfl · intro h simp only [← mul_assoc] at h refine mul_left_cancel₀ (mul_ne_zero ?_ ?_) h on_goal 1 => apply mul_ne_zero on_goal 1 => apply div_ne_zero · exact one_ne_zero all_goals assumption [Elab.step] [0.118601] rw [← ha, ← hb, ← mul_assoc bd, ← mul_assoc ad, mul_comm bd] ext; constructor · rintro rfl rfl · intro h simp only [← mul_assoc] at h refine mul_left_cancel₀ (mul_ne_zero ?_ ?_) h on_goal 1 => apply mul_ne_zero on_goal 1 => apply div_ne_zero · exact one_ne_zero all_goals assumption [Elab.step] [0.010324] rw [← ha, ← hb, ← mul_assoc bd, ← mul_assoc ad, mul_comm bd] [Elab.step] [0.010312] (rewrite [← ha, ← hb, ← mul_assoc bd, ← mul_assoc ad, mul_comm bd]; with_annotate_state"]" (try (with_reducible rfl))) [Elab.step] [0.010299] rewrite [← ha, ← hb, ← mul_assoc bd, ← mul_assoc ad, mul_comm bd]; with_annotate_state"]" (try (with_reducible rfl)) [Elab.step] [0.010291] rewrite [← ha, ← hb, ← mul_assoc bd, ← mul_assoc ad, mul_comm bd]; with_annotate_state"]" (try (with_reducible rfl)) [Elab.step] [0.105805] · intro h simp only [← mul_assoc] at h refine mul_left_cancel₀ (mul_ne_zero ?_ ?_) h on_goal 1 => apply mul_ne_zero on_goal 1 => apply div_ne_zero · exact one_ne_zero all_goals assumption [Elab.step] [0.105661] intro h simp only [← mul_assoc] at h refine mul_left_cancel₀ (mul_ne_zero ?_ ?_) h on_goal 1 => apply mul_ne_zero on_goal 1 => apply div_ne_zero · exact one_ne_zero all_goals assumption [Elab.step] [0.105650] intro h simp only [← mul_assoc] at h refine mul_left_cancel₀ (mul_ne_zero ?_ ?_) h on_goal 1 => apply mul_ne_zero on_goal 1 => apply div_ne_zero · exact one_ne_zero all_goals assumption [Elab.step] [0.043946] refine mul_left_cancel₀ (mul_ne_zero ?_ ?_) h [Elab.step] [0.043859] expected type: a = b, term mul_left_cancel₀ (mul_ne_zero ?_ ?_) h [Elab.step] [0.025447] expected type: ?m.103 * ?m.104 ≠ 0, term (mul_ne_zero ?_ ?_) [Elab.step] [0.025432] expected type: ?m.103 * ?m.104 ≠ 0, term mul_ne_zero ?_ ?_ [Meta.synthInstance] [0.019262] ✅️ NoZeroDivisors α [Elab.step] [0.021441] on_goal 1 => apply mul_ne_zero [Elab.step] [0.019543] apply mul_ne_zero [Elab.step] [0.019530] apply mul_ne_zero [Elab.step] [0.019514] apply mul_ne_zero [Meta.synthInstance] [0.013986] ✅️ NoZeroDivisors α [Elab.step] [0.018650] · exact one_ne_zero [Elab.step] [0.018355] exact one_ne_zero [Elab.step] [0.018309] exact one_ne_zero [Elab.step] [0.018269] exact one_ne_zero [Elab.step] [0.017827] expected type: 1 ≠ 0, term one_ne_zero [Meta.synthInstance] [0.012295] ✅️ NeZero 1 Build completed successfully (436 jobs). ``` ### Trace profiling of `cancel_factors_eq` after PR 27370 ```diff diff --git a/Mathlib/Tactic/CancelDenoms/Core.lean b/Mathlib/Tactic/CancelDenoms/Core.lean index c4b62d3e29..066f915189 100644 --- a/Mathlib/Tactic/CancelDenoms/Core.lean +++ b/Mathlib/Tactic/CancelDenoms/Core.lean @@ -80,20 +80,11 @@ theorem cancel_factors_le {α} [Field α] [LinearOrder α] [IsStrictOrderedRing · exact mul_pos had hbd · exact one_div_pos.2 hgcd +set_option trace.profiler true in theorem cancel_factors_eq {α} [Field α] {a b ad bd a' b' gcd : α} (ha : ad * a = a') (hb : bd * b = b') (had : ad ≠ 0) (hbd : bd ≠ 0) (hgcd : gcd ≠ 0) : (a = b) = (1 / gcd * (bd * a') = 1 / gcd * (ad * b')) := by - rw [← ha, ← hb, ← mul_assoc bd, ← mul_assoc ad, mul_comm bd] - ext; constructor - · rintro rfl - rfl - · intro h - simp only [← mul_assoc] at h - refine mul_left_cancel₀ (mul_ne_zero ?_ ?_) h - on_goal 1 => apply mul_ne_zero - on_goal 1 => apply div_ne_zero - · exact one_ne_zero - all_goals assumption + grind theorem cancel_factors_ne {α} [Field α] {a b ad bd a' b' gcd : α} (ha : ad * a = a') (hb : bd * b = b') (had : ad ≠ 0) (hbd : bd ≠ 0) (hgcd : gcd ≠ 0) : ``` ``` ℹ [436/436] Built Mathlib.Tactic.CancelDenoms.Core (3.1s) info: Mathlib/Tactic/CancelDenoms/Core.lean:84:0: [Elab.command] [0.034809] theorem cancel_factors_eq {α} [Field α] {a b ad bd a' b' gcd : α} (ha : ad * a = a') (hb : bd * b = b') (had : ad ≠ 0) (hbd : bd ≠ 0) (hgcd : gcd ≠ 0) : (a = b) = (1 / gcd * (bd * a') = 1 / gcd * (ad * b')) := by grind [Elab.definition.header] [0.014091] CancelDenoms.cancel_factors_eq info: Mathlib/Tactic/CancelDenoms/Core.lean:84:0: [Elab.async] [0.046425] elaborating proof of CancelDenoms.cancel_factors_eq [Elab.definition.value] [0.045869] CancelDenoms.cancel_factors_eq [Elab.step] [0.045340] grind [Elab.step] [0.045327] grind [Elab.step] [0.045311] grind info: Mathlib/Tactic/CancelDenoms/Core.lean:87:2: [Elab.async] [0.027621] Lean.addDecl [Kernel] [0.027585] ✅️ typechecking declarations [CancelDenoms.cancel_factors_eq._proof_1_1] Build completed successfully (436 jobs). ```
maintainer-merge t-meta easy 1/11 Mathlib/Tactic/CancelDenoms/Core.lean 1 9 ['euprunin', 'github-actions', 'grunweg', 'leanprover-bot', 'leanprover-community-mathlib4-bot'] alexjbest
assignee:alexjbest
1-16514
1 day ago
1-16515
1 day ago
74-75001
74 days
30174 mcdoll
author:mcdoll
 feat: the Hölder conjugate of an `ENNReal` --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) t-data maintainer-merge 4/0 Mathlib/Data/Real/ConjExponents.lean 1 2 ['github-actions', 'grunweg'] nobody
1-15930
1 day ago
1-15930
1 day ago
2-8997
2 days
26338 mans0954
author:mans0954
 feat(Order/ScottContinuity): Scott continuity on product spaces Some further results on Scott Continuity: - `scottContinuous_iff_map_sSup`: `f` is Scott continuous if and only if it commutes with `sSup` on directed sets - `ScottContinuous_prod_of_ScottContinuous`: `f` is Scott continuous on a product space if it is Scott continuous in each variable - `ScottContinuousOn.inf₂`: For complete linear orders, the meet operation is Scott continuous --- - [x] depends on: #13201 - I think this is due to the move of the definition of Scott Continuity into its own file rather than a hard dependency. - [x] depends on: #19150 - [x] depends on: #19222 - [x] depends on:#20254 - [x] depends on: #21493 Original PR: https://github.com/leanprover-community/mathlib4/pull/15412 [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) maintainer-merge t-order awaiting-author 136/4 Mathlib.lean,Mathlib/Order/Bounds/Basic.lean,Mathlib/Order/ScottContinuity.lean,Mathlib/Order/ScottContinuity/Complete.lean,Mathlib/Order/ScottContinuity/Prod.lean 5 n/a ['YaelDillies', 'github-actions', 'mans0954', 'mathlib4-dependent-issues-bot'] nobody
0-85941
23 hours ago
unknown
unknown
29501 Vierkantor
author:Vierkantor
 test(TacticAnalysis): ensure `classical`'s effects are picked up This test case used to fail, and needed a fix to the `classical` tactic in the standard library: - [x] depends on: https://github.com/leanprover/lean4/pull/10332 --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) maintainer-merge t-meta 10/0 MathlibTest/TacticAnalysis.lean 1 6 ['Vierkantor', 'github-actions', 'grunweg', 'mathlib4-dependent-issues-bot', 'mathlib4-merge-conflict-bot'] adamtopaz
assignee:adamtopaz
0-68464
19 hours ago
8-33882
8 days ago
10-40775
10 days
29513 grunweg
author:grunweg
 fix(lint-style): parse linter options and load environment extensions correctly Parse options and load linter set extension correctly. This fixes two issues: - We never called the `toOptions` function that parses Lakefile options into a `Lean.Options` structure: the function we use instead is only meant for command-line options and doesn't handle the `weak.` prefix correctly. - The way we load linter sets was incorrect: `withImportModules` stopped updating environment extensions since [lean4#6325](https://github.com/leanprover/lean4/pull/6325), and that is exactly what we use to store linter sets. At the time of writing, `importModules` might be a suitable replacement (but this is not very safe, and not documented to be stable). Instead, write a small elaborator returning the environment at the point of elaboration, and use that instead. --- - [x] depends on: #29584 - [x] depends on: #29585 - [x] depends on: #29586 [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) maintainer-merge t-meta 28/12 scripts/lint-style.lean 1 13 ['Vierkantor', 'adomani', 'github-actions', 'grunweg', 'mathlib4-dependent-issues-bot'] dwrensha
assignee:dwrensha
0-68463
19 hours ago
8-36054
8 days ago
17-22454
17 days
30026 ADedecker
author:ADedecker
 chore: new file for constructions of uniform groups The split between `Defs` and `Basic` was a bit messy (e.g the `Prod` instance was in `Defs` but the `Pi` instance was in `Basic`), and I'm going to make these files longer when introducing left and right uniform groups, so I figured the best solution was to move everything in an intermediate `Constructions` file. --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) maintainer-merge t-topology 112/94 Mathlib.lean,Mathlib/Analysis/CStarAlgebra/Module/Synonym.lean,Mathlib/RingTheory/MvPowerSeries/PiTopology.lean,Mathlib/Topology/Algebra/IsUniformGroup/Basic.lean,Mathlib/Topology/Algebra/IsUniformGroup/Constructions.lean,Mathlib/Topology/Algebra/IsUniformGroup/Defs.lean,Mathlib/Topology/Instances/TrivSqZeroExt.lean,Mathlib/Topology/UniformSpace/Matrix.lean 8 3 ['github-actions', 'mcdoll'] dagurtomas
assignee:dagurtomas
0-59564
16 hours ago
0-59564
16 hours ago
8-22919
8 days
30205 NotWearingPants
author:NotWearingPants
 feat(Combinators/SimpleGraph/Walk): `p.getVert` is `p.support.get` --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) maintainer-merge new-contributor t-combinatorics easy 15/0 Mathlib/Combinatorics/SimpleGraph/Walk.lean 1 3 ['NotWearingPants', 'Ruben-VandeVelde', 'github-actions'] nobody
0-35134
9 hours ago
0-35134
9 hours ago
1-6282
1 day
29916 themathqueen
author:themathqueen
 chore: move some results from `Analysis/Normed/Algebra/Spectrum` to `Analysis/{Real, Complex}/Spectrum` --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) maintainer-merge t-analysis 130/74 Mathlib.lean,Mathlib/Analysis/CStarAlgebra/ContinuousFunctionalCalculus/Instances.lean,Mathlib/Analysis/Complex/Spectrum.lean,Mathlib/Analysis/Normed/Algebra/Spectrum.lean,Mathlib/Analysis/Real/Spectrum.lean 5 6 ['Ruben-VandeVelde', 'github-actions', 'mathlib4-merge-conflict-bot', 'themathqueen'] ADedecker
assignee:ADedecker
0-34996
9 hours ago
0-34996
9 hours ago
11-72352
11 days
30178 EtienneC30
author:EtienneC30
 feat: preimage of Set.pi by uncurry --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) t-data maintainer-merge 10/0 Mathlib/Data/Set/Prod.lean,Mathlib/Data/Set/Sigma.lean 2 2 ['Ruben-VandeVelde', 'github-actions'] nobody
0-34918
9 hours ago
0-34918
9 hours ago
2-8585
2 days
30032 riccardobrasca
author:riccardobrasca
 feat: factorization of cyclotomic polynomial over finite fields We compute the degree of the factors of the `n`-th cyclotomic polynomial over a finite field of characteristic `p` when `p` and `n` are coprime. --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) maintainer-merge t-algebra t-number-theory
label:t-algebra$
 184/3 Mathlib.lean,Mathlib/Algebra/CharP/CharAndCard.lean,Mathlib/NumberTheory/GaussSum.lean,Mathlib/RingTheory/Polynomial/Cyclotomic/Basic.lean,Mathlib/RingTheory/Polynomial/Cyclotomic/Factorization.lean 5 12 ['Ruben-VandeVelde', 'github-actions', 'riccardobrasca'] jcommelin
assignee:jcommelin
0-34520
9 hours ago
0-35663
9 hours ago
8-13986
8 days
30034 yonggyuchoimath
author:yonggyuchoimath
 feat(Mathlib/AlgebraicGeometry/AffineScheme): add preservation of limits of affine schemes This PR adds simple results about affine schemes. Main changes: * `createsLimitsForgetToScheme`: The forgetful functor `AffineScheme ⥤ Scheme` creates small limits. * (written by Andrew Yang) `preservesLimit_rightOp_Γ`: Shows that `Scheme.Γ.rightOp : Scheme ⥤ CommRingCatᵒᵖ` preserves limits of diagrams consisting of affine schemes. * `preservesColimit_Γ`: The dual statement. This PR reopens #30015, which was acidentally closed by myself. --- - [ ] depends on: #30014 maintainer-merge 28/0 Mathlib/AlgebraicGeometry/AffineScheme.lean 1 23 ['chrisflav', 'erdOne', 'github-actions', 'mathlib4-dependent-issues-bot', 'mathlib4-merge-conflict-bot', 'yonggyuchoimath'] nobody
0-6143
1 hour ago
0-6143
1 hour ago
6-77481
6 days
28295 artie2000
author:artie2000
 feat(Algebra/Order/Ring/Ordering): basic results about ring (pre)orderings * Basic automation for membership of ring orderings * Alternative constructors for ring preorderings and ring orderings * Basic results about ring preorderings and their supports, including the special case over a field --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) - [x] depends on: #27282 maintainer-merge t-algebra
label:t-algebra$
 200/0 Mathlib.lean,Mathlib/Algebra/Group/Subgroup/Defs.lean,Mathlib/Algebra/Order/Ring/Ordering/Basic.lean 3 57 ['Rob23oba', 'YaelDillies', 'artie2000', 'github-actions', 'mathlib4-dependent-issues-bot', 'mathlib4-merge-conflict-bot', 'vihdzp'] joneugster
assignee:joneugster
0-1031
17 minutes ago
18-48424
18 days ago
24-11557
24 days
24965 erdOne
author:erdOne
 refactor: Make `IsLocalHom` take unbundled map --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) maintainer-merge t-algebra merge-conflict awaiting-author
label:t-algebra$
 16/7 Mathlib/Algebra/Group/Units/Hom.lean,Mathlib/AlgebraicGeometry/Scheme.lean,Mathlib/Geometry/RingedSpace/LocallyRingedSpace.lean,Mathlib/Geometry/RingedSpace/LocallyRingedSpace/HasColimits.lean,Mathlib/Geometry/RingedSpace/OpenImmersion.lean 5 6 ['alreadydone', 'erdOne', 'eric-wieser', 'github-actions', 'leanprover-community-bot-assistant'] nobody
124-62512
4 months ago
124-62513
4 months ago
10-26015
10 days
26912 pechersky
author:pechersky
 chore(Algebra/Ring/Subring): simp tag `Subring.smul_def` s-multiplying by a subtype is easiest to manipulate when both terms are in the ambient type. Many places that had to use the _def lemma for a rewrite, or to include it in a simp set, no longer have to. Ported from #25308 --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) I found this being not-simp frustrating when talking about submodules over a valuation subring. maintainer-merge t-algebra merge-conflict
label:t-algebra$
 68/67 Mathlib/Algebra/Algebra/Subalgebra/Basic.lean,Mathlib/Algebra/Field/Subfield/Basic.lean,Mathlib/Algebra/Group/Subgroup/Actions.lean,Mathlib/Algebra/Group/Submonoid/MulAction.lean,Mathlib/Algebra/Module/LocalizedModule/Basic.lean,Mathlib/Algebra/Module/LocalizedModule/Exact.lean,Mathlib/Algebra/Module/LocalizedModule/IsLocalization.lean,Mathlib/Algebra/Module/LocalizedModule/Submodule.lean,Mathlib/Algebra/Ring/Periodic.lean,Mathlib/Algebra/Ring/Subring/Basic.lean,Mathlib/Algebra/Ring/Subsemiring/Basic.lean,Mathlib/Analysis/CStarAlgebra/Basic.lean,Mathlib/FieldTheory/KummerExtension.lean,Mathlib/GroupTheory/GroupAction/Defs.lean,Mathlib/GroupTheory/GroupAction/MultiplePrimitivity.lean,Mathlib/GroupTheory/GroupAction/MultipleTransitivity.lean,Mathlib/GroupTheory/GroupAction/SubMulAction/OfFixingSubgroup.lean,Mathlib/GroupTheory/GroupAction/SubMulAction/OfStabilizer.lean,Mathlib/LinearAlgebra/RootSystem/Irreducible.lean,Mathlib/LinearAlgebra/RootSystem/RootPositive.lean,Mathlib/LinearAlgebra/RootSystem/WeylGroup.lean,Mathlib/RingTheory/Etale/Kaehler.lean,Mathlib/RingTheory/LocalProperties/Projective.lean,Mathlib/RingTheory/Localization/InvSubmonoid.lean,Mathlib/RingTheory/OreLocalization/Basic.lean 25 19 ['artie2000', 'eric-wieser', 'github-actions', 'j-loreaux', 'linesthatinterlace', 'mathlib4-merge-conflict-bot', 'pechersky'] joelriou
assignee:joelriou
34-24003
1 month ago
34-24004
1 month ago
51-74059
51 days
28737 astrainfinita
author:astrainfinita
 refactor: deprecate `MulEquivClass` This PR continues the work from #18806. Original PR: https://github.com/leanprover-community/mathlib4/pull/18806 maintainer-merge t-algebra merge-conflict awaiting-author
label:t-algebra$
 67/77 Mathlib/Algebra/BigOperators/Finprod.lean,Mathlib/Algebra/Group/Equiv/Basic.lean,Mathlib/Algebra/Group/Equiv/Defs.lean,Mathlib/Algebra/Group/Irreducible/Lemmas.lean,Mathlib/Algebra/Group/Subgroup/Map.lean,Mathlib/Algebra/Group/Submonoid/Operations.lean,Mathlib/Algebra/Group/Units/Equiv.lean,Mathlib/Algebra/GroupWithZero/Equiv.lean,Mathlib/Algebra/GroupWithZero/NonZeroDivisors.lean,Mathlib/Algebra/Module/Equiv/Defs.lean,Mathlib/Algebra/Order/CauSeq/Basic.lean,Mathlib/Algebra/Order/Hom/Monoid.lean,Mathlib/Algebra/Prime/Lemmas.lean,Mathlib/Algebra/Ring/Divisibility/Basic.lean,Mathlib/Algebra/Ring/Equiv.lean,Mathlib/Algebra/Star/MonoidHom.lean,Mathlib/Combinatorics/Additive/FreimanHom.lean,Mathlib/GroupTheory/GroupExtension/Defs.lean,Mathlib/GroupTheory/Submonoid/Center.lean,Mathlib/LinearAlgebra/FreeModule/Finite/CardQuotient.lean,Mathlib/RingTheory/Bialgebra/Equiv.lean,Mathlib/RingTheory/Ideal/Norm/AbsNorm.lean,Mathlib/RingTheory/Multiplicity.lean,Mathlib/RingTheory/UniqueFactorizationDomain/NormalizedFactors.lean,Mathlib/Topology/Algebra/ContinuousMonoidHom.lean,Mathlib/Topology/Algebra/InfiniteSum/Basic.lean 26 20 ['Vierkantor', 'alreadydone', 'astrainfinita', 'github-actions', 'grunweg', 'leanprover-bot', 'leanprover-community-mathlib4-bot', 'mathlib4-merge-conflict-bot'] Vierkantor
assignee:Vierkantor
25-27863
25 days ago
25-27864
25 days ago
4-17723
4 days

PRs blocked on a zulip discussion

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
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] [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) awaiting-zulip t-computability new-contributor awaiting-author 298/0 Mathlib.lean,Mathlib/Computability/GNFA.lean,Mathlib/Computability/Language.lean,Mathlib/Computability/RegularExpressions.lean,docs/references.bib 5 6 ['github-actions', 'mathlib4-dependent-issues-bot', 'meithecatte', 'trivial1711'] nobody
152-77651
4 months ago
152-77660
4 months ago
23-54870
23 days
20648 anthonyde
author:anthonyde
 feat: formalize regular expression -> εNFA The file `Computability/RegularExpressionsToEpsilonNFA.lean` contains a formal definition of Thompson's method for constructing an `εNFA` from a `RegularExpression` and a proof of its correctness. --- - [x] depends on: #20644 - [x] depends on: #20645 [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) awaiting-zulip t-computability new-contributor 490/0 Mathlib.lean,Mathlib/Computability/RegularExpressionsToEpsilonNFA.lean,docs/references.bib 3 5 ['github-actions', 'mathlib4-dependent-issues-bot', 'meithecatte', 'qawbecrdtey'] nobody
152-76962
4 months ago
152-77597
4 months ago
75-77754
75 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. [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) awaiting-zulip t-computability new-contributor awaiting-author 159/0 Mathlib/Computability/DFA.lean,Mathlib/Computability/Language.lean 2 59 ['EtienneC30', 'YaelDillies', 'github-actions', 'maemre', 'meithecatte', 'urkud'] EtienneC30
assignee:EtienneC30
123-43422
4 months ago
152-77561
4 months ago
48-67492
48 days
23929 meithecatte
author:meithecatte
 feat(Computability/NFA): improve bound on pumping lemma --- - [x] depends on: #25321 [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) awaiting-zulip t-computability new-contributor 101/10 Mathlib/Computability/EpsilonNFA.lean,Mathlib/Computability/NFA.lean 2 41 ['YaelDillies', 'github-actions', 'leanprover-community-bot-assistant', 'mathlib4-dependent-issues-bot', 'meithecatte'] nobody
120-813
3 months ago
120-814
3 months ago
34-10595
34 days
29072 yury-harmonic
author:yury-harmonic
 feat({Nat,Int}/ModEq): add lemmas --- I'm not sure that I named these lemmas correctly. Suggestions about better names are welcome! [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) t-data awaiting-zulip 171/15 Mathlib/Data/Int/ModEq.lean,Mathlib/Data/Nat/ModEq.lean 2 5 ['eric-wieser', 'github-actions', 'yury-harmonic'] nobody
37-44695
1 month ago
37-44695
1 month ago
0-55232
15 hours
29582 YaelDillies
author:YaelDillies
 chore: rename `_root_.prop` to `Prop.finite` This was a surprising name! --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) t-data awaiting-zulip 1/1 Mathlib/Data/Fintype/EquivFin.lean 1 11 ['YaelDillies', 'bryangingechen', 'eric-wieser', 'github-actions', 'grunweg', 'plp127'] nobody
12-56937
12 days ago
12-56938
12 days ago
3-1360
3 days
29110 NotWearingPants
author:NotWearingPants
 feat(Counterexamples): Euler's sum of powers conjecture feat(Counterexamples): Euler's sum of powers conjecture --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) awaiting-zulip maintainer-merge new-contributor 158/0 Counterexamples.lean,Counterexamples/EulerSumOfPowers.lean 2 43 ['MichaelStollBayreuth', 'NotWearingPants', 'eric-wieser', 'github-actions', 'tb65536', 'urkud'] MichaelStollBayreuth
assignee:MichaelStollBayreuth
9-1053
9 days ago
9-1109
9 days ago
24-25032
24 days
24754 urkud
author:urkud
 feat: define `pathIntegral` This is a step towards formalizing of the Poincaré lemma for 1-forms. --- - [x] depends on: #24831 - [x] depends on: #25047 - [x] depends on: #25048 [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) awaiting-zulip t-analysis awaiting-author 580/9 Mathlib.lean,Mathlib/Analysis/Convex/PathConnected.lean,Mathlib/Analysis/Normed/Module/Basic.lean,Mathlib/MeasureTheory/Integral/IntervalIntegral/Basic.lean,Mathlib/MeasureTheory/Integral/IntervalIntegral/ContDiff.lean,Mathlib/MeasureTheory/Integral/PathIntegral/Basic.lean 6 42 ['github-actions', 'mathlib4-dependent-issues-bot', 'mathlib4-merge-conflict-bot', 'sgouezel', 'urkud'] j-loreaux
assignee:j-loreaux
8-5634
8 days ago
8-5634
8 days ago
17-56980
17 days
29002 grunweg
author:grunweg
 chore: move Data/Real/Irrational to RingTheory It certainly has nothing to do with data (structures). --- I'm less sure where to put it instead. [zulip discussion](https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/Cleaning.20up.20.60Data.60/with/536301893) suggested this place; in the future, this could also be split. [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) file-removed awaiting-zulip 10/10 Counterexamples/IrrationalPowerOfIrrational.lean,Mathlib.lean,Mathlib/Analysis/Real/Pi/Irrational.lean,Mathlib/Data/Real/GoldenRatio.lean,Mathlib/NumberTheory/DiophantineApproximation/Basic.lean,Mathlib/NumberTheory/Rayleigh.lean,Mathlib/NumberTheory/Transcendental/Liouville/Basic.lean,Mathlib/RingTheory/Real/Irrational.lean,Mathlib/Tactic/NormNum/Irrational.lean,Mathlib/Topology/Instances/AddCircle/DenseSubgroup.lean,Mathlib/Topology/Instances/Irrational.lean 11 2 ['github-actions', 'mathlib4-merge-conflict-bot'] nobody
7-37508
7 days ago
7-37591
7 days ago
0-67
1 minute
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! [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) 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 3 ['euprunin', 'github-actions', 'grunweg'] nobody
7-9072
7 days ago
40-81380
1 month 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` [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) large-import awaiting-zulip new-contributor 446/125 Mathlib/CategoryTheory/Monoidal/Category.lean,Mathlib/CategoryTheory/Monoidal/Discrete.lean,Mathlib/Tactic/ToAdditive/GuessName.lean 3 18 ['JovanGerb', 'YaelDillies', 'github-actions', 'imbrem'] nobody
0-17449
4 hours ago
0-24681
6 hours ago
1-18384
1 day
11800 JADekker
author:JADekker
 feat : Define 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. --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) awaiting-zulip t-topology merge-conflict please-adopt 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
384-54684
1 year ago
384-76659
1 year ago
119-10687
119 days
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. [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) awaiting-zulip t-order t-algebra merge-conflict
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
319-27934
10 months ago
319-27934
10 months ago
33-64877
33 days
8370 eric-wieser
author:eric-wieser
 refactor(Analysis/NormedSpace/Exponential): remove the `𝕂` argument from `exp` This argument is still needed for almost all the lemmas, which means it can longer be found by unification. We keep around `expSeries 𝕂 A`, as it's needed for talking about the radius of convergence over different base fields. This is a prerequisite for #8372, as we can't merge the functions until they have the same interface.\ Zulip thread: [#mathlib4 > Real.exp @ 💬](https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/Real.2Eexp/near/401602245) --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) This is started from the mathport output on https://github.com/leanprover-community/mathlib/pull/19244 awaiting-zulip t-analysis merge-conflict 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
163-69711
5 months ago
175-11941
5 months ago
29-60989
29 days
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 --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) awaiting-zulip t-computability new-contributor merge-conflict awaiting-author 307/5 Mathlib/Computability/NFA.lean 1 15 ['TpmKranz', 'YaelDillies', 'dupuisf', 'github-actions', 'leanprover-community-bot-assistant', 'meithecatte'] nobody
139-13817
4 months ago
139-13818
4 months ago
45-84611
45 days
22361 rudynicolop
author:rudynicolop
 feat(Computability/NFA): nfa closure properties Add the closure properties union, intersection and reversal for NFA. --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) awaiting-zulip t-computability new-contributor merge-conflict awaiting-author 218/2 Mathlib/Computability/Language.lean,Mathlib/Computability/NFA.lean 2 90 ['EtienneC30', 'b-mehta', 'github-actions', 'leanprover-community-bot-assistant', 'meithecatte', 'rudynicolop'] EtienneC30
assignee:EtienneC30
139-12891
4 months ago
139-12893
4 months ago
39-67601
39 days
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. --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) awaiting-zulip t-algebra merge-conflict
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
92-57960
3 months ago
92-57960
3 months ago
0-66650
18 hours
25218 kckennylau
author:kckennylau
 feat(AlgebraicGeometry): Tate normal form of elliptic curves --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) awaiting-zulip new-contributor t-algebraic-geometry merge-conflict 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
92-56798
3 months ago
92-56799
3 months ago
6-51040
6 days
28298 thorimur
author:thorimur
 chore: dedent `to_additive` docstrings This PR uses automation to dedent `to_additive` docstrings throughout Mathlib. It does not lint against indentation or in any way enforce indentation standards for future docstrings. The convention was chosen in accordance with the discussion and polls at [this Zulip thread](https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/Poll.3A.20Indentation.20style.20for.20.60to_additive.60.20docstrings/with/534285603). --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) awaiting-zulip merge-conflict documentation 949/949 Mathlib/Algebra/BigOperators/Fin.lean,Mathlib/Algebra/BigOperators/Finprod.lean,Mathlib/Algebra/BigOperators/Finsupp/Basic.lean,Mathlib/Algebra/BigOperators/Group/Finset/Lemmas.lean,Mathlib/Algebra/BigOperators/Group/List/Basic.lean,Mathlib/Algebra/BigOperators/Group/Multiset/Defs.lean,Mathlib/Algebra/BigOperators/Pi.lean,Mathlib/Algebra/Category/Grp/Basic.lean,Mathlib/Algebra/Category/Grp/FilteredColimits.lean,Mathlib/Algebra/Category/Grp/Limits.lean,Mathlib/Algebra/Category/Grp/Ulift.lean,Mathlib/Algebra/Category/MonCat/Basic.lean,Mathlib/Algebra/Category/MonCat/FilteredColimits.lean,Mathlib/Algebra/Category/MonCat/Limits.lean,Mathlib/Algebra/Category/Semigrp/Basic.lean,Mathlib/Algebra/Free.lean,Mathlib/Algebra/FreeMonoid/Basic.lean,Mathlib/Algebra/Group/Action/Defs.lean,Mathlib/Algebra/Group/Action/Pi.lean,Mathlib/Algebra/Group/Action/Pointwise/Finset.lean,Mathlib/Algebra/Group/Basic.lean,Mathlib/Algebra/Group/Defs.lean,Mathlib/Algebra/Group/Embedding.lean,Mathlib/Algebra/Group/Equiv/Basic.lean,Mathlib/Algebra/Group/Equiv/Defs.lean,Mathlib/Algebra/Group/Equiv/Opposite.lean,Mathlib/Algebra/Group/Even.lean,Mathlib/Algebra/Group/Hom/Basic.lean,Mathlib/Algebra/Group/Hom/Defs.lean,Mathlib/Algebra/Group/Hom/Instances.lean,Mathlib/Algebra/Group/Indicator.lean,Mathlib/Algebra/Group/Pi/Lemmas.lean,Mathlib/Algebra/Group/Pi/Units.lean,Mathlib/Algebra/Group/Pointwise/Finset/Basic.lean,Mathlib/Algebra/Group/Pointwise/Set/Basic.lean,Mathlib/Algebra/Group/Prod.lean,Mathlib/Algebra/Group/Subgroup/Basic.lean,Mathlib/Algebra/Group/Subgroup/Defs.lean,Mathlib/Algebra/Group/Subgroup/Ker.lean,Mathlib/Algebra/Group/Subgroup/Lattice.lean,Mathlib/Algebra/Group/Subgroup/Map.lean,Mathlib/Algebra/Group/Subgroup/Pointwise.lean,Mathlib/Algebra/Group/Submonoid/Basic.lean,Mathlib/Algebra/Group/Submonoid/BigOperators.lean,Mathlib/Algebra/Group/Submonoid/Defs.lean,Mathlib/Algebra/Group/Submonoid/Membership.lean,Mathlib/Algebra/Group/Submonoid/MulAction.lean,Mathlib/Algebra/Group/Submonoid/Operations.lean,Mathlib/Algebra/Group/Subsemigroup/Basic.lean,Mathlib/Algebra/Group/Subsemigroup/Operations.lean,Mathlib/Algebra/Group/UniqueProds/Basic.lean,Mathlib/Algebra/Group/Units/Defs.lean,Mathlib/Algebra/Group/Units/Equiv.lean,Mathlib/Algebra/Group/Units/Hom.lean,Mathlib/Algebra/Group/Units/Opposite.lean,Mathlib/Algebra/Notation/Pi/Basic.lean,Mathlib/Algebra/Opposites.lean,Mathlib/Algebra/Order/BigOperators/Group/List.lean,Mathlib/Algebra/Order/Group/Abs.lean,Mathlib/Algebra/Order/Group/Basic.lean,Mathlib/Algebra/Order/Group/Cone.lean,Mathlib/Algebra/Order/Group/OrderIso.lean,Mathlib/Algebra/Order/Group/Units.lean,Mathlib/Algebra/Order/Hom/Monoid.lean,Mathlib/Algebra/Order/Monoid/Basic.lean,Mathlib/Algebra/Order/Monoid/Canonical/Defs.lean,Mathlib/Algebra/Order/Monoid/Submonoid.lean,Mathlib/Algebra/Order/Monoid/Unbundled/Basic.lean,Mathlib/Algebra/Order/Monoid/Unbundled/WithTop.lean,Mathlib/Algebra/Order/Monoid/Units.lean,Mathlib/Algebra/Order/Pi.lean,Mathlib/Algebra/Regular/Defs.lean,Mathlib/Analysis/Normed/Group/Basic.lean,Mathlib/CategoryTheory/Monoidal/Discrete.lean,Mathlib/Data/Finset/NoncommProd.lean,Mathlib/Data/Fintype/BigOperators.lean,Mathlib/Data/Set/MulAntidiagonal.lean,Mathlib/Data/Set/SMulAntidiagonal.lean,Mathlib/Data/Vector/Basic.lean,Mathlib/Dynamics/Ergodic/Action/OfMinimal.lean,Mathlib/Dynamics/FixedPoints/Prufer.lean,Mathlib/Geometry/Manifold/Algebra/SmoothFunctions.lean,Mathlib/GroupTheory/Complement.lean,Mathlib/GroupTheory/Congruence/Basic.lean,Mathlib/GroupTheory/Congruence/Defs.lean,Mathlib/GroupTheory/Coprod/Basic.lean,Mathlib/GroupTheory/Coset/Basic.lean,Mathlib/GroupTheory/Divisible.lean,Mathlib/GroupTheory/EckmannHilton.lean,Mathlib/GroupTheory/FreeGroup/Basic.lean,Mathlib/GroupTheory/FreeGroup/Reduce.lean,Mathlib/GroupTheory/GroupAction/Basic.lean,Mathlib/GroupTheory/GroupAction/Blocks.lean,Mathlib/GroupTheory/GroupAction/Defs.lean,Mathlib/GroupTheory/GroupAction/FixedPoints.lean,Mathlib/GroupTheory/GroupAction/Hom.lean,Mathlib/GroupTheory/GroupAction/MultipleTransitivity.lean,Mathlib/GroupTheory/GroupAction/Primitive.lean,Mathlib/GroupTheory/GroupAction/Quotient.lean,Mathlib/GroupTheory/GroupAction/SubMulAction.lean 141 10 ['eric-wieser', 'github-actions', 'grunweg', 'mathlib4-merge-conflict-bot', 'thorimur'] nobody
51-85292
1 month ago
52-72664
1 month ago
0-61617
17 hours
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 awaiting-zulip slow-typeclass-synthesis t-algebra t-analysis merge-conflict
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
32-72443
1 month ago
32-72444
1 month ago
0-20585
5 hours
17518 grunweg
author:grunweg
 feat: lint on declarations mentioning `Invertible` or `Unique` Using the same infrastructure as for #10235. Depends on that PR to land first, and also (for the first lint) a zulip discussion if that change is desired/about the best way to enact it. --- - [ ] depends on: #10235 awaiting-zulip t-linter merge-conflict blocked-by-other-PR 149/7 Mathlib.lean,Mathlib/Algebra/MvPolynomial/PDeriv.lean,Mathlib/Computability/Halting.lean,Mathlib/Computability/TuringMachine.lean,Mathlib/Data/Fintype/Card.lean,Mathlib/GroupTheory/Perm/DomMulAct.lean,Mathlib/Logic/Basic.lean,Mathlib/Logic/Encodable/Basic.lean,Mathlib/NumberTheory/JacobiSum/Basic.lean,Mathlib/Order/Heyting/Regular.lean,Mathlib/RingTheory/MvPolynomial/Symmetric/FundamentalTheorem.lean,Mathlib/Tactic.lean,Mathlib/Tactic/Linter/UnusedAssumptionInType.lean 13 3 ['github-actions', 'mathlib4-dependent-issues-bot', 'mergify'] nobody
337-8403
11 months ago
362-83325
11 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 [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) awaiting-zulip t-computability new-contributor merge-conflict blocked-by-other-PR 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
152-77611
4 months ago
152-77616
4 months ago
0-179
2 minutes

PRs on the review queue labelled 'tech debt' or 'longest-pole'

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
30107 grunweg
author:grunweg
 chore: track occurrences of 'nonrec' as technical debt Matches leanprover-community/leanprover-community.github.io#689: only merge when that is deemed a good idea. -------- TODO: make the count more robust, for instance count all occurrences of "^nonrec " plus those of "^[private|protected] nonrec ". --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) tech debt CI 1/0 scripts/technical-debt-metrics.sh 1 1 ['github-actions'] nobody
4-24120
4 days ago
4-41370
4 days ago
4-41348
4 days