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: August 21, 2025 at 01:25 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
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 10 ['Ruben-VandeVelde', 'eric-wieser', 'faenuccio', 'github-actions', 'j-loreaux', 'jcommelin', 'qawbecrdtey'] faenuccio
assignee:faenuccio
71-73708
2 months ago
71-73708
2 months ago
32-83569
32 days
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
23-39274
23 days ago
23-39274
23 days ago
42-26074
42 days
27257 JovanGerb
author:JovanGerb
 feat(LinearAlgebra/AffineSpace/Ordered): add `lineMap_le_lineMap_iff_of_lt'` I only need `lineMap_le_lineMap_iff_of_lt'`. The other lemmas are added for completeness. --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) maintainer-merge t-algebra awaiting-author
label:t-algebra$
 44/0 Mathlib/LinearAlgebra/AffineSpace/Ordered.lean 1 3 ['Ruben-VandeVelde', 'eric-wieser', 'github-actions'] kbuzzard
assignee:kbuzzard
19-13762
19 days ago
19-13762
19 days ago
14-17781
14 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
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 16 ['eric-wieser', 'github-actions', 'j-loreaux', 'linesthatinterlace', 'pechersky'] joelriou
assignee:joelriou
17-1406
17 days ago
29-16120
29 days ago
40-30994
40 days
27076 Komyyy
author:Komyyy
 refactor: don't require `DecidablePred` to state `PrimrecPred` ```lean def PrimrecPred {α} [Primcodable α] (p : α → Prop) [DecidablePred p] := Primrec fun a => decide (p a) ``` Currently, `DecidablePred` is required to **state** `PrimrecPred`, so this PR changes the definition and adds convenient APIs for this new definition: ```lean def PrimrecPred {α} [Primcodable α] (p : α → Prop) := open scoped Classical in Primrec fun a => decide (p a) ``` --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) maintainer-merge t-computability 117/67 Mathlib/Computability/Halting.lean,Mathlib/Computability/Partrec.lean,Mathlib/Computability/Primrec.lean,Mathlib/Computability/Reduce.lean 4 10 ['Komyyy', 'YaelDillies', 'digama0', 'eric-wieser', 'github-actions'] YaelDillies
assignee:YaelDillies
16-68735
16 days ago
16-68735
16 days ago
38-35434
38 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 453/0 Mathlib.lean,Mathlib/Analysis/Normed/Affine/AsymptoticCone.lean,Mathlib/Order/Filter/Map.lean 3 44 ['AntoineChambert-Loir', 'YaelDillies', 'gasparattila', 'github-actions', 'mathlib4-dependent-issues-bot'] YaelDillies
assignee:YaelDillies
15-27990
15 days ago
15-31275
15 days ago
29-48815
29 days
28139 YaelDillies
author:YaelDillies
 refactor: make the cone explicit in `ConvexCone.toPointedCone` Otherwise it is impossible to know which cone we are talking about from the infoview as proofs are elided. From Toric --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) t-convex-geometry toric maintainer-merge 3/3 Mathlib/Analysis/Convex/Cone/Closure.lean,Mathlib/Geometry/Convex/Cone/Pointed.lean 2 2 ['Ruben-VandeVelde', 'github-actions'] nobody
9-17613
9 days ago
9-17613
9 days ago
11-65907
11 days
28220 kim-em
author:kim-em
 chore: cleanup three #adaptation_notes --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) maintainer-merge 5/26 Mathlib/Data/Bool/Basic.lean,Mathlib/Logic/Function/Defs.lean,Mathlib/Tactic/NormNum/Pow.lean 3 6 ['bryangingechen', 'github-actions', 'grunweg', 'kim-em', 'mathlib4-merge-conflict-bot'] nobody
6-52008
6 days ago
7-6504
7 days ago
9-22406
9 days
26403 riccardobrasca
author:riccardobrasca
 feat: add `isPrincipalIdealRing_of_isPrincipal_of_lt_or_isPrincipal_of_mem_primesOver_of_mem_Icc` This PR continues the work from #25186. Original PR: https://github.com/leanprover-community/mathlib4/pull/25186 maintainer-merge t-number-theory 49/13 Mathlib/NumberTheory/NumberField/ClassNumber.lean 1 8 ['faenuccio', 'github-actions', 'grunweg', 'loefflerd', 'riccardobrasca', 'xroblot'] faenuccio and jcommelin
assignee:jcommelin assignee:faenuccio
6-25482
6 days ago
6-25482
6 days ago
56-40157
56 days
25491 tannerduve
author:tannerduve
 feat(Control/Monad/Free): define free monad, prove it lawful, and implement standard effects This PR introduces the `Free` monad. This implementation uses the "freer monad" approach as the traditional free monad (eg from [Haskell](https://hackage.haskell.org/package/free-5.2/docs/Control-Monad-Free.html)) is not safely definable in Lean due to termination checking (it's not strictly positive). The main contributions are: * Definition of the `Free` monad as an inductive type which generates a monad given any type constructor `F : Type -> Type`. * Functor and Monad instances for `Free F`, along with proofs of the `LawfulFunctor` and `LawfulMonad` laws. * Canonical instances of `Free` with standard effect signatures: * `FreeState s` for stateful computations, defined via a `StateF s` functor with `get` and `put` operations. * `FreeWriter w` for logging computations, defined via a `WriterF w` functor with a `tell` operation. * `FreeCont r` for continuation-passing computations, using the CPS functor `(α → r) → r`. In this construction, computations are represented as **trees of effects**. Each node (`liftBind`) represents a request to perform an effect, accompanied by a continuation specifying how the computation proceeds after the effect. The leaves (`pure`) represent completed computations with final results. A key insight is that `FreeM F` satisfies the **universal property of free monads**: for any monad `M` and effect handler `f : F → M`, there exists a unique way to interpret `FreeM F` computations in `M` that respects the effect semantics given by `f`. This unique interpreter is `liftM f`, which acts as the canonical **fold** for free monads. To execute or interpret these computations, we provide two approaches: 1. **Hand-written interpreters** (`FreeState.run`, `FreeWriter.run`, `FreeCont.run`) that directly pattern-match on the tree structure 2. **Canonical interpreters** (`FreeState.toStateM`, `FreeWriter.toWriteT`, `FreeCont.toContT`) derived from the universal property via `liftM` And then prove that these approaches are equivalent --- This PR adds new files and definitions; no breaking changes. **Tags:** free monad, freer monad, effect systems, state monad, writer monad, continuation monad, operational semantics, verified interpreters t-data maintainer-merge 696/0 Mathlib.lean,Mathlib/Control/Monad/Free.lean,Mathlib/Control/Monad/Free/Effects.lean,MathlibTest/freemonad.lean,docs/references.bib 5 147 ['YaelDillies', 'copilot-pull-request-reviewer', 'eric-wieser', 'github-actions', 'plp127', 'quangvdao', 'srghma', 'tannerduve'] ericrbg
assignee:ericrbg
6-1429
6 days ago
64-37232
2 months ago
74-56314
74 days
28457 euprunin
author:euprunin
 chore(LinearAlgebra/AffineSpace): deprecate `coe_injective` (duplicate) --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) maintainer-merge t-algebra
label:t-algebra$
 2/5 Mathlib/LinearAlgebra/AffineSpace/ContinuousAffineEquiv.lean 1 2 ['Ruben-VandeVelde', 'github-actions'] nobody
5-61477
5 days ago
5-61477
5 days ago
5-68666
5 days
27965 grunweg
author:grunweg
 feat: verify that file names contain no forbidden characters Follow-up to #27588: Windows also forbids certain characters in file names. I snuck in a change to also disallow `!` (which causes problems on Nix OS) and `.` (i.e., #27944) --- that would have caught the error in #27796, and may indicate confusion of file and module names. --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) file-removed t-linter maintainer-merge 72/42 Mathlib/Tactic/Linter/TextBased.lean,MathlibTest/ForbiddenModuleNames.lean,MathlibTest/ForbiddenWindows.lean,scripts/lint-style.lean 4 11 ['YaelDillies', 'adomani', 'github-actions', 'grunweg'] joneugster
assignee:joneugster
5-1444
5 days ago
15-26739
15 days ago
15-59021
15 days
28179 vihdzp
author:vihdzp
 feat: `LinearOrderedAddCommGroupWithTop (ArchimedeanClass R)` We define addition on `ArchimedeanClass R` such that `mk (a * b) = mk a + mk b`, as well as a zero element `0 = mk 1`. This makes `ArchimedeanClass R` into a `LinearOrderedAddCommMonoidWithTop` when `R` is a ring, and a `LinearOrderedAddCommGroupWithTop` when `R` is a field. --- - [x] depends on: #28227 See [Zulip](https://leanprover.zulipchat.com/#narrow/channel/116395-maths/topic/.22Commensurate.22.20elements.20in.20fields/near/533639232) for discussion on this (in particular, why we turn multiplication into addition). [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) maintainer-merge t-algebra
label:t-algebra$
 208/10 Mathlib.lean,Mathlib/Algebra/Order/Archimedean/Class.lean,Mathlib/Algebra/Order/Ring/Archimedean.lean 3 28 ['alreadydone', 'github-actions', 'kckennylau', 'mathlib4-dependent-issues-bot', 'mathlib4-merge-conflict-bot', 'vihdzp', 'wwylele'] nobody
3-31299
3 days ago
3-31299
3 days ago
6-28912
6 days
27856 euprunin
author:euprunin
 chore(RingTheory/PowerSeries): golf entire `trunc_one` using `grind` ---
Show trace profiling of trunc_one: 88 ms before, 87 ms after 🎉 ### Trace profiling of `trunc_one` before PR 27856 ```diff diff --git a/Mathlib/RingTheory/PowerSeries/Trunc.lean b/Mathlib/RingTheory/PowerSeries/Trunc.lean index 7b8a612d49..9e21778c21 100644 --- a/Mathlib/RingTheory/PowerSeries/Trunc.lean +++ b/Mathlib/RingTheory/PowerSeries/Trunc.lean @@ -47,6 +47,7 @@ theorem trunc_zero (n) : trunc n (0 : R⟦X⟧) = 0 := rw [coeff_trunc, LinearMap.map_zero, Polynomial.coeff_zero] split_ifs <;> rfl +set_option trace.profiler true in @[simp] theorem trunc_one (n) : trunc (n + 1) (1 : R⟦X⟧) = 1 := Polynomial.ext fun m => by ``` ``` ℹ [1292/1292] Built Mathlib.RingTheory.PowerSeries.Trunc (3.2s) info: Mathlib/RingTheory/PowerSeries/Trunc.lean:51:0: [Elab.async] [0.089409] elaborating proof of PowerSeries.trunc_one [Elab.definition.value] [0.088361] PowerSeries.trunc_one [Elab.step] [0.086909] rw [coeff_trunc, coeff_one, Polynomial.coeff_one] split_ifs with h _ h' · rfl · rfl · subst h'; simp at h · rfl [Elab.step] [0.086897] rw [coeff_trunc, coeff_one, Polynomial.coeff_one] split_ifs with h _ h' · rfl · rfl · subst h'; simp at h · rfl [Elab.step] [0.038895] split_ifs with h _ h' [Elab.step] [0.043021] · subst h'; simp at h [Elab.step] [0.042999] subst h'; simp at h [Elab.step] [0.042991] subst h'; simp at h [Elab.step] [0.042673] simp at h Build completed successfully (1292 jobs). ``` ### Trace profiling of `trunc_one` after PR 27856 ```diff diff --git a/Mathlib/RingTheory/PowerSeries/Trunc.lean b/Mathlib/RingTheory/PowerSeries/Trunc.lean index 7b8a612d49..d9f8019532 100644 --- a/Mathlib/RingTheory/PowerSeries/Trunc.lean +++ b/Mathlib/RingTheory/PowerSeries/Trunc.lean @@ -47,15 +47,11 @@ theorem trunc_zero (n) : trunc n (0 : R⟦X⟧) = 0 := rw [coeff_trunc, LinearMap.map_zero, Polynomial.coeff_zero] split_ifs <;> rfl +set_option trace.profiler true in @[simp] theorem trunc_one (n) : trunc (n + 1) (1 : R⟦X⟧) = 1 := Polynomial.ext fun m => by - rw [coeff_trunc, coeff_one, Polynomial.coeff_one] - split_ifs with h _ h' - · rfl - · rfl - · subst h'; simp at h - · rfl + grind [PowerSeries.coeff_trunc, PowerSeries.coeff_one, Polynomial.coeff_one] @[simp] theorem trunc_C (n) (a : R) : trunc (n + 1) (C R a) = Polynomial.C a := ``` ``` ℹ [1292/1292] Built Mathlib.RingTheory.PowerSeries.Trunc (3.1s) info: Mathlib/RingTheory/PowerSeries/Trunc.lean:51:0: [Elab.async] [0.087506] elaborating proof of PowerSeries.trunc_one [Elab.definition.value] [0.086697] PowerSeries.trunc_one [Elab.step] [0.083908] grind [PowerSeries.coeff_trunc, PowerSeries.coeff_one, Polynomial.coeff_one] [Elab.step] [0.083856] grind [PowerSeries.coeff_trunc, PowerSeries.coeff_one, Polynomial.coeff_one] [Elab.step] [0.083840] grind [PowerSeries.coeff_trunc, PowerSeries.coeff_one, Polynomial.coeff_one] [Meta.synthInstance] [0.010307] ✅️ Lean.Grind.NatModule (Lean.Grind.Ring.OfSemiring.Q ℕ) [Meta.synthInstance] [0.010255] ❌️ LE (MvPowerSeries PUnit.{1} R) Build completed successfully (1292 jobs). ```
maintainer-merge t-algebra
label:t-algebra$
 1/6 Mathlib/RingTheory/PowerSeries/Trunc.lean 1 8 ['eric-wieser', 'euprunin', 'github-actions', 'grunweg'] adomani
assignee:adomani
2-73084
2 days ago
19-9163
19 days ago
19-9681
19 days
27857 euprunin
author:euprunin
 chore(Analysis/SpecialFunctions): golf entire `rpow_eq_top_of_nonneg` using `simp` ---
Show trace profiling of rpow_eq_top_of_nonneg: <10 ms before, 18 ms after ### Trace profiling of `rpow_eq_top_of_nonneg` before PR 27857 ```diff diff --git a/Mathlib/Analysis/SpecialFunctions/Pow/NNReal.lean b/Mathlib/Analysis/SpecialFunctions/Pow/NNReal.lean index 75b232ee4e..5d2ddf1fce 100644 --- a/Mathlib/Analysis/SpecialFunctions/Pow/NNReal.lean +++ b/Mathlib/Analysis/SpecialFunctions/Pow/NNReal.lean @@ -553,6 +553,7 @@ theorem rpow_eq_top_iff_of_pos {x : ℝ≥0∞} {y : ℝ} (hy : 0 < y) : x ^ y = lemma rpow_lt_top_iff_of_pos {x : ℝ≥0∞} {y : ℝ} (hy : 0 < y) : x ^ y < ∞ ↔ x < ∞ := by simp only [lt_top_iff_ne_top, Ne, rpow_eq_top_iff_of_pos hy] +set_option trace.profiler true in theorem rpow_eq_top_of_nonneg (x : ℝ≥0∞) {y : ℝ} (hy0 : 0 ≤ y) : x ^ y = ⊤ → x = ⊤ := by rw [ENNReal.rpow_eq_top_iff] rintro (h|h) ``` ``` ✔ [1872/1872] Built Mathlib.Analysis.SpecialFunctions.Pow.NNReal (6.0s) Build completed successfully (1872 jobs). ``` ### Trace profiling of `rpow_eq_top_of_nonneg` after PR 27857 ```diff diff --git a/Mathlib/Analysis/SpecialFunctions/Pow/NNReal.lean b/Mathlib/Analysis/SpecialFunctions/Pow/NNReal.lean index 75b232ee4e..68dc37f940 100644 --- a/Mathlib/Analysis/SpecialFunctions/Pow/NNReal.lean +++ b/Mathlib/Analysis/SpecialFunctions/Pow/NNReal.lean @@ -553,13 +553,9 @@ theorem rpow_eq_top_iff_of_pos {x : ℝ≥0∞} {y : ℝ} (hy : 0 < y) : x ^ y = lemma rpow_lt_top_iff_of_pos {x : ℝ≥0∞} {y : ℝ} (hy : 0 < y) : x ^ y < ∞ ↔ x < ∞ := by simp only [lt_top_iff_ne_top, Ne, rpow_eq_top_iff_of_pos hy] +set_option trace.profiler true in theorem rpow_eq_top_of_nonneg (x : ℝ≥0∞) {y : ℝ} (hy0 : 0 ≤ y) : x ^ y = ⊤ → x = ⊤ := by - rw [ENNReal.rpow_eq_top_iff] - rintro (h|h) - · exfalso - rw [lt_iff_not_ge] at h - exact h.right hy0 - · exact h.left + simp +contextual [ENNReal.rpow_eq_top_iff, hy0.not_gt] -- This is an unsafe rule since we want to try `rpow_ne_top_of_ne_zero` if `y < 0`. @[aesop (rule_sets := [finiteness]) unsafe apply] ``` ``` ℹ [1872/1872] Built Mathlib.Analysis.SpecialFunctions.Pow.NNReal (6.0s) info: Mathlib/Analysis/SpecialFunctions/Pow/NNReal.lean:557:0: [Elab.async] [0.018873] elaborating proof of ENNReal.rpow_eq_top_of_nonneg [Elab.definition.value] [0.018350] ENNReal.rpow_eq_top_of_nonneg [Elab.step] [0.018131] simp +contextual [ENNReal.rpow_eq_top_iff, hy0.not_gt] [Elab.step] [0.018118] simp +contextual [ENNReal.rpow_eq_top_iff, hy0.not_gt] [Elab.step] [0.018101] simp +contextual [ENNReal.rpow_eq_top_iff, hy0.not_gt] Build completed successfully (1872 jobs). ```
maintainer-merge t-analysis 1/6 Mathlib/Analysis/SpecialFunctions/Pow/NNReal.lean 1 6 ['eric-wieser', 'euprunin', 'github-actions', 'grunweg', 'kim-em'] ADedecker
assignee:ADedecker
2-72966
2 days ago
19-8801
19 days ago
19-9308
19 days
25832 xroblot
author:xroblot
 feat(FieldTheory/LinearDisjoint): `trace` (resp. `norm`) and `algebraMap` commutes For `A` and `B` two linearly disjoint `R`-subalgebras in a commutative algebra `S` and `b` a `R`-basis of `B`, we construct a `A`-basis of `S = A ⊔ B` from `b` (and a similar construction using a `R`-basis of `A`). Then, we prove in this situation that `trace` commutes with `algebraMap`, that is: ```lean Algebra.trace A S (algebraMap B S x) = algebraMap R A (Algebra.trace R B x) ``` and a similar result for the norm. We also add a similar basis construction for `A` and `B` two linearly disjoint intermediate fields with the hypothesis that `A.toSubalgebra ⊔ B.toSubalgebra = ⊤`. This hypothesis is equivalent to `A ⊔ B = ⊤` in many cases (for example, one of the two extensions is algebraic over the base field) but not always. --- [![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$
 159/9 Mathlib/FieldTheory/LinearDisjoint.lean,Mathlib/RingTheory/LinearDisjoint.lean 2 47 ['acmepjz', 'chrisflav', 'github-actions', 'xroblot'] chrisflav
assignee:chrisflav
1-60530
1 day ago
1-61192
1 day ago
64-26172
64 days
25858 themathqueen
author:themathqueen
 feat(RingTheory/Coalgebra/MulOpposite): coalgebra instance for MulOpposite Adding an instance for `Aᵐᵒᵖ` being an `R`-coalgebra when `A` is. --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) t-ring-theory maintainer-merge new-contributor 69/0 Mathlib.lean,Mathlib/LinearAlgebra/TensorProduct/Basic.lean,Mathlib/RingTheory/Coalgebra/MulOpposite.lean 3 6 ['chrisflav', 'github-actions'] chrisflav
assignee:chrisflav
1-60339
1 day ago
1-60339
1 day ago
67-43110
67 days
28617 kckennylau
author:kckennylau
 feat(AlgebraicGeometry): jointly surjective topology We define `jointlySurjectiveTopology` to have the same condition as `jointlySurjectivePretopology`, which is the new name of the former `surjectiveFamiliesPretopology`. --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) maintainer-merge t-algebraic-geometry 48/3 Mathlib/AlgebraicGeometry/Sites/MorphismProperty.lean,Mathlib/CategoryTheory/Sites/Grothendieck.lean 2 6 ['chrisflav', 'github-actions', 'kckennylau'] chrisflav
assignee:chrisflav
1-54377
1 day ago
1-54727
1 day ago
2-6880
2 days
28615 kckennylau
author:kckennylau
 feat(RingTheory): Standard open immersion We define the ring hom property `RingHom.IsStandardOpenImmersion` which is one that is a localization map away from some element. --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) t-ring-theory maintainer-merge 122/2 Mathlib.lean,Mathlib/RingTheory/Localization/Away/Basic.lean,Mathlib/RingTheory/Localization/BaseChange.lean,Mathlib/RingTheory/RingHom/OpenImmersion.lean 4 15 ['chrisflav', 'github-actions', 'kckennylau'] chrisflav
assignee:chrisflav
1-47865
1 day ago
1-47865
1 day ago
2-7957
2 days
28180 kckennylau
author:kckennylau
 chore(Meta): clean up PiFin.mkLiteralQ Co-authored by Aaron Liu. This PR fixes the resulting type of `loop`, adds a docstring, and removes an unused variable. --- Zulip: [#PR reviews > #28148 Simproc for Matrix Transpose](https://leanprover.zulipchat.com/#narrow/channel/144837-PR-reviews/topic/.2328148.20Simproc.20for.20Matrix.20Transpose) [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) t-data maintainer-merge t-meta 7/4 Mathlib/Data/Fin/VecNotation.lean 1 23 ['JovanGerb', 'eric-wieser', 'github-actions', 'kckennylau', 'plp127'] nobody
1-34091
1 day ago
1-41513
1 day ago
4-35645
4 days
28656 euprunin
author:euprunin
 chore(Data/Int): golf entire `coe_leastOfBdd_eq` and `coe_greatestOfBdd_eq` using `grind` --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) t-data maintainer-merge 2/6 Mathlib/Data/Int/LeastGreatest.lean 1 1 ['github-actions'] nobody
0-16839
4 hours ago
1-28655
1 day ago
1-28701
1 day
28640 euprunin
author:euprunin
 chore(Data/List): golf entire `getElem?_getD_replicate_default_eq` and `getD_append_right` using `grind` --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) t-data maintainer-merge 2/9 Mathlib/Data/List/GetD.lean 1 1 ['github-actions'] nobody
0-16792
4 hours ago
1-40218
1 day ago
1-40266
1 day
25123 eric-wieser
author:eric-wieser
 feat: add rfl lemmas for monoidal categories Making these `simp` opens a can of worms best left to #24823 `simps` would generate bad names here. --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) maintainer-merge t-algebra
label:t-algebra$
 111/0 Mathlib/Algebra/Category/AlgCat/Monoidal.lean,Mathlib/Algebra/Category/ModuleCat/Monoidal/Basic.lean,Mathlib/LinearAlgebra/QuadraticForm/QuadraticModuleCat/Monoidal.lean 3 1 ['github-actions'] dagurtomas
assignee:dagurtomas
0-14384
3 hours ago
90-774
2 months ago
90-824
90 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
78-81861
2 months ago
78-81862
2 months ago
10-26015
10 days
23961 FR-vdash-bot
author:FR-vdash-bot
 refactor: unbundle algebra from `ENormed*` Further speed up the search in the algebraic typeclass hierarchy by avoiding searching for `TopologicalSpace`. --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) slow-typeclass-synthesis maintainer-merge t-algebra t-analysis merge-conflict awaiting-author
label:t-algebra$
 32/25 Mathlib/Analysis/CStarAlgebra/CStarMatrix.lean,Mathlib/Analysis/Normed/Group/Basic.lean,Mathlib/Analysis/Normed/Group/Continuity.lean,Mathlib/Analysis/NormedSpace/IndicatorFunction.lean,Mathlib/MeasureTheory/Function/LpSeminorm/Basic.lean 5 12 ['FR-vdash-bot', 'github-actions', 'grunweg', 'jcommelin', 'leanprover-bot', 'leanprover-community-bot-assistant'] nobody
74-66079
2 months ago
74-66079
2 months ago
17-72244
17 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
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 10 ['Ruben-VandeVelde', 'eric-wieser', 'faenuccio', 'github-actions', 'j-loreaux', 'jcommelin', 'qawbecrdtey'] faenuccio
assignee:faenuccio
71-73708
2 months ago
71-73708
2 months ago
32-83569
32 days
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
23-39274
23 days ago
23-39274
23 days ago
42-26074
42 days
27257 JovanGerb
author:JovanGerb
 feat(LinearAlgebra/AffineSpace/Ordered): add `lineMap_le_lineMap_iff_of_lt'` I only need `lineMap_le_lineMap_iff_of_lt'`. The other lemmas are added for completeness. --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) maintainer-merge t-algebra awaiting-author
label:t-algebra$
 44/0 Mathlib/LinearAlgebra/AffineSpace/Ordered.lean 1 3 ['Ruben-VandeVelde', 'eric-wieser', 'github-actions'] kbuzzard
assignee:kbuzzard
19-13762
19 days ago
19-13762
19 days ago
14-17781
14 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
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 16 ['eric-wieser', 'github-actions', 'j-loreaux', 'linesthatinterlace', 'pechersky'] joelriou
assignee:joelriou
17-1406
17 days ago
29-16120
29 days ago
40-30994
40 days
27076 Komyyy
author:Komyyy
 refactor: don't require `DecidablePred` to state `PrimrecPred` ```lean def PrimrecPred {α} [Primcodable α] (p : α → Prop) [DecidablePred p] := Primrec fun a => decide (p a) ``` Currently, `DecidablePred` is required to **state** `PrimrecPred`, so this PR changes the definition and adds convenient APIs for this new definition: ```lean def PrimrecPred {α} [Primcodable α] (p : α → Prop) := open scoped Classical in Primrec fun a => decide (p a) ``` --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) maintainer-merge t-computability 117/67 Mathlib/Computability/Halting.lean,Mathlib/Computability/Partrec.lean,Mathlib/Computability/Primrec.lean,Mathlib/Computability/Reduce.lean 4 10 ['Komyyy', 'YaelDillies', 'digama0', 'eric-wieser', 'github-actions'] YaelDillies
assignee:YaelDillies
16-68735
16 days ago
16-68735
16 days ago
38-35434
38 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 453/0 Mathlib.lean,Mathlib/Analysis/Normed/Affine/AsymptoticCone.lean,Mathlib/Order/Filter/Map.lean 3 44 ['AntoineChambert-Loir', 'YaelDillies', 'gasparattila', 'github-actions', 'mathlib4-dependent-issues-bot'] YaelDillies
assignee:YaelDillies
15-27990
15 days ago
15-31275
15 days ago
29-48815
29 days
28139 YaelDillies
author:YaelDillies
 refactor: make the cone explicit in `ConvexCone.toPointedCone` Otherwise it is impossible to know which cone we are talking about from the infoview as proofs are elided. From Toric --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) t-convex-geometry toric maintainer-merge 3/3 Mathlib/Analysis/Convex/Cone/Closure.lean,Mathlib/Geometry/Convex/Cone/Pointed.lean 2 2 ['Ruben-VandeVelde', 'github-actions'] nobody
9-17613
9 days ago
9-17613
9 days ago
11-65907
11 days
28220 kim-em
author:kim-em
 chore: cleanup three #adaptation_notes --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) maintainer-merge 5/26 Mathlib/Data/Bool/Basic.lean,Mathlib/Logic/Function/Defs.lean,Mathlib/Tactic/NormNum/Pow.lean 3 6 ['bryangingechen', 'github-actions', 'grunweg', 'kim-em', 'mathlib4-merge-conflict-bot'] nobody
6-52008
6 days ago
7-6504
7 days ago
9-22406
9 days
26403 riccardobrasca
author:riccardobrasca
 feat: add `isPrincipalIdealRing_of_isPrincipal_of_lt_or_isPrincipal_of_mem_primesOver_of_mem_Icc` This PR continues the work from #25186. Original PR: https://github.com/leanprover-community/mathlib4/pull/25186 maintainer-merge t-number-theory 49/13 Mathlib/NumberTheory/NumberField/ClassNumber.lean 1 8 ['faenuccio', 'github-actions', 'grunweg', 'loefflerd', 'riccardobrasca', 'xroblot'] faenuccio and jcommelin
assignee:jcommelin assignee:faenuccio
6-25482
6 days ago
6-25482
6 days ago
56-40157
56 days
25491 tannerduve
author:tannerduve
 feat(Control/Monad/Free): define free monad, prove it lawful, and implement standard effects This PR introduces the `Free` monad. This implementation uses the "freer monad" approach as the traditional free monad (eg from [Haskell](https://hackage.haskell.org/package/free-5.2/docs/Control-Monad-Free.html)) is not safely definable in Lean due to termination checking (it's not strictly positive). The main contributions are: * Definition of the `Free` monad as an inductive type which generates a monad given any type constructor `F : Type -> Type`. * Functor and Monad instances for `Free F`, along with proofs of the `LawfulFunctor` and `LawfulMonad` laws. * Canonical instances of `Free` with standard effect signatures: * `FreeState s` for stateful computations, defined via a `StateF s` functor with `get` and `put` operations. * `FreeWriter w` for logging computations, defined via a `WriterF w` functor with a `tell` operation. * `FreeCont r` for continuation-passing computations, using the CPS functor `(α → r) → r`. In this construction, computations are represented as **trees of effects**. Each node (`liftBind`) represents a request to perform an effect, accompanied by a continuation specifying how the computation proceeds after the effect. The leaves (`pure`) represent completed computations with final results. A key insight is that `FreeM F` satisfies the **universal property of free monads**: for any monad `M` and effect handler `f : F → M`, there exists a unique way to interpret `FreeM F` computations in `M` that respects the effect semantics given by `f`. This unique interpreter is `liftM f`, which acts as the canonical **fold** for free monads. To execute or interpret these computations, we provide two approaches: 1. **Hand-written interpreters** (`FreeState.run`, `FreeWriter.run`, `FreeCont.run`) that directly pattern-match on the tree structure 2. **Canonical interpreters** (`FreeState.toStateM`, `FreeWriter.toWriteT`, `FreeCont.toContT`) derived from the universal property via `liftM` And then prove that these approaches are equivalent --- This PR adds new files and definitions; no breaking changes. **Tags:** free monad, freer monad, effect systems, state monad, writer monad, continuation monad, operational semantics, verified interpreters t-data maintainer-merge 696/0 Mathlib.lean,Mathlib/Control/Monad/Free.lean,Mathlib/Control/Monad/Free/Effects.lean,MathlibTest/freemonad.lean,docs/references.bib 5 147 ['YaelDillies', 'copilot-pull-request-reviewer', 'eric-wieser', 'github-actions', 'plp127', 'quangvdao', 'srghma', 'tannerduve'] ericrbg
assignee:ericrbg
6-1429
6 days ago
64-37232
2 months ago
74-56314
74 days
28457 euprunin
author:euprunin
 chore(LinearAlgebra/AffineSpace): deprecate `coe_injective` (duplicate) --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) maintainer-merge t-algebra
label:t-algebra$
 2/5 Mathlib/LinearAlgebra/AffineSpace/ContinuousAffineEquiv.lean 1 2 ['Ruben-VandeVelde', 'github-actions'] nobody
5-61477
5 days ago
5-61477
5 days ago
5-68666
5 days
27965 grunweg
author:grunweg
 feat: verify that file names contain no forbidden characters Follow-up to #27588: Windows also forbids certain characters in file names. I snuck in a change to also disallow `!` (which causes problems on Nix OS) and `.` (i.e., #27944) --- that would have caught the error in #27796, and may indicate confusion of file and module names. --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) file-removed t-linter maintainer-merge 72/42 Mathlib/Tactic/Linter/TextBased.lean,MathlibTest/ForbiddenModuleNames.lean,MathlibTest/ForbiddenWindows.lean,scripts/lint-style.lean 4 11 ['YaelDillies', 'adomani', 'github-actions', 'grunweg'] joneugster
assignee:joneugster
5-1444
5 days ago
15-26739
15 days ago
15-59021
15 days
28179 vihdzp
author:vihdzp
 feat: `LinearOrderedAddCommGroupWithTop (ArchimedeanClass R)` We define addition on `ArchimedeanClass R` such that `mk (a * b) = mk a + mk b`, as well as a zero element `0 = mk 1`. This makes `ArchimedeanClass R` into a `LinearOrderedAddCommMonoidWithTop` when `R` is a ring, and a `LinearOrderedAddCommGroupWithTop` when `R` is a field. --- - [x] depends on: #28227 See [Zulip](https://leanprover.zulipchat.com/#narrow/channel/116395-maths/topic/.22Commensurate.22.20elements.20in.20fields/near/533639232) for discussion on this (in particular, why we turn multiplication into addition). [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) maintainer-merge t-algebra
label:t-algebra$
 208/10 Mathlib.lean,Mathlib/Algebra/Order/Archimedean/Class.lean,Mathlib/Algebra/Order/Ring/Archimedean.lean 3 28 ['alreadydone', 'github-actions', 'kckennylau', 'mathlib4-dependent-issues-bot', 'mathlib4-merge-conflict-bot', 'vihdzp', 'wwylele'] nobody
3-31299
3 days ago
3-31299
3 days ago
6-28912
6 days
27856 euprunin
author:euprunin
 chore(RingTheory/PowerSeries): golf entire `trunc_one` using `grind` ---
Show trace profiling of trunc_one: 88 ms before, 87 ms after 🎉 ### Trace profiling of `trunc_one` before PR 27856 ```diff diff --git a/Mathlib/RingTheory/PowerSeries/Trunc.lean b/Mathlib/RingTheory/PowerSeries/Trunc.lean index 7b8a612d49..9e21778c21 100644 --- a/Mathlib/RingTheory/PowerSeries/Trunc.lean +++ b/Mathlib/RingTheory/PowerSeries/Trunc.lean @@ -47,6 +47,7 @@ theorem trunc_zero (n) : trunc n (0 : R⟦X⟧) = 0 := rw [coeff_trunc, LinearMap.map_zero, Polynomial.coeff_zero] split_ifs <;> rfl +set_option trace.profiler true in @[simp] theorem trunc_one (n) : trunc (n + 1) (1 : R⟦X⟧) = 1 := Polynomial.ext fun m => by ``` ``` ℹ [1292/1292] Built Mathlib.RingTheory.PowerSeries.Trunc (3.2s) info: Mathlib/RingTheory/PowerSeries/Trunc.lean:51:0: [Elab.async] [0.089409] elaborating proof of PowerSeries.trunc_one [Elab.definition.value] [0.088361] PowerSeries.trunc_one [Elab.step] [0.086909] rw [coeff_trunc, coeff_one, Polynomial.coeff_one] split_ifs with h _ h' · rfl · rfl · subst h'; simp at h · rfl [Elab.step] [0.086897] rw [coeff_trunc, coeff_one, Polynomial.coeff_one] split_ifs with h _ h' · rfl · rfl · subst h'; simp at h · rfl [Elab.step] [0.038895] split_ifs with h _ h' [Elab.step] [0.043021] · subst h'; simp at h [Elab.step] [0.042999] subst h'; simp at h [Elab.step] [0.042991] subst h'; simp at h [Elab.step] [0.042673] simp at h Build completed successfully (1292 jobs). ``` ### Trace profiling of `trunc_one` after PR 27856 ```diff diff --git a/Mathlib/RingTheory/PowerSeries/Trunc.lean b/Mathlib/RingTheory/PowerSeries/Trunc.lean index 7b8a612d49..d9f8019532 100644 --- a/Mathlib/RingTheory/PowerSeries/Trunc.lean +++ b/Mathlib/RingTheory/PowerSeries/Trunc.lean @@ -47,15 +47,11 @@ theorem trunc_zero (n) : trunc n (0 : R⟦X⟧) = 0 := rw [coeff_trunc, LinearMap.map_zero, Polynomial.coeff_zero] split_ifs <;> rfl +set_option trace.profiler true in @[simp] theorem trunc_one (n) : trunc (n + 1) (1 : R⟦X⟧) = 1 := Polynomial.ext fun m => by - rw [coeff_trunc, coeff_one, Polynomial.coeff_one] - split_ifs with h _ h' - · rfl - · rfl - · subst h'; simp at h - · rfl + grind [PowerSeries.coeff_trunc, PowerSeries.coeff_one, Polynomial.coeff_one] @[simp] theorem trunc_C (n) (a : R) : trunc (n + 1) (C R a) = Polynomial.C a := ``` ``` ℹ [1292/1292] Built Mathlib.RingTheory.PowerSeries.Trunc (3.1s) info: Mathlib/RingTheory/PowerSeries/Trunc.lean:51:0: [Elab.async] [0.087506] elaborating proof of PowerSeries.trunc_one [Elab.definition.value] [0.086697] PowerSeries.trunc_one [Elab.step] [0.083908] grind [PowerSeries.coeff_trunc, PowerSeries.coeff_one, Polynomial.coeff_one] [Elab.step] [0.083856] grind [PowerSeries.coeff_trunc, PowerSeries.coeff_one, Polynomial.coeff_one] [Elab.step] [0.083840] grind [PowerSeries.coeff_trunc, PowerSeries.coeff_one, Polynomial.coeff_one] [Meta.synthInstance] [0.010307] ✅️ Lean.Grind.NatModule (Lean.Grind.Ring.OfSemiring.Q ℕ) [Meta.synthInstance] [0.010255] ❌️ LE (MvPowerSeries PUnit.{1} R) Build completed successfully (1292 jobs). ```
maintainer-merge t-algebra
label:t-algebra$
 1/6 Mathlib/RingTheory/PowerSeries/Trunc.lean 1 8 ['eric-wieser', 'euprunin', 'github-actions', 'grunweg'] adomani
assignee:adomani
2-73084
2 days ago
19-9163
19 days ago
19-9681
19 days
27857 euprunin
author:euprunin
 chore(Analysis/SpecialFunctions): golf entire `rpow_eq_top_of_nonneg` using `simp` ---
Show trace profiling of rpow_eq_top_of_nonneg: <10 ms before, 18 ms after ### Trace profiling of `rpow_eq_top_of_nonneg` before PR 27857 ```diff diff --git a/Mathlib/Analysis/SpecialFunctions/Pow/NNReal.lean b/Mathlib/Analysis/SpecialFunctions/Pow/NNReal.lean index 75b232ee4e..5d2ddf1fce 100644 --- a/Mathlib/Analysis/SpecialFunctions/Pow/NNReal.lean +++ b/Mathlib/Analysis/SpecialFunctions/Pow/NNReal.lean @@ -553,6 +553,7 @@ theorem rpow_eq_top_iff_of_pos {x : ℝ≥0∞} {y : ℝ} (hy : 0 < y) : x ^ y = lemma rpow_lt_top_iff_of_pos {x : ℝ≥0∞} {y : ℝ} (hy : 0 < y) : x ^ y < ∞ ↔ x < ∞ := by simp only [lt_top_iff_ne_top, Ne, rpow_eq_top_iff_of_pos hy] +set_option trace.profiler true in theorem rpow_eq_top_of_nonneg (x : ℝ≥0∞) {y : ℝ} (hy0 : 0 ≤ y) : x ^ y = ⊤ → x = ⊤ := by rw [ENNReal.rpow_eq_top_iff] rintro (h|h) ``` ``` ✔ [1872/1872] Built Mathlib.Analysis.SpecialFunctions.Pow.NNReal (6.0s) Build completed successfully (1872 jobs). ``` ### Trace profiling of `rpow_eq_top_of_nonneg` after PR 27857 ```diff diff --git a/Mathlib/Analysis/SpecialFunctions/Pow/NNReal.lean b/Mathlib/Analysis/SpecialFunctions/Pow/NNReal.lean index 75b232ee4e..68dc37f940 100644 --- a/Mathlib/Analysis/SpecialFunctions/Pow/NNReal.lean +++ b/Mathlib/Analysis/SpecialFunctions/Pow/NNReal.lean @@ -553,13 +553,9 @@ theorem rpow_eq_top_iff_of_pos {x : ℝ≥0∞} {y : ℝ} (hy : 0 < y) : x ^ y = lemma rpow_lt_top_iff_of_pos {x : ℝ≥0∞} {y : ℝ} (hy : 0 < y) : x ^ y < ∞ ↔ x < ∞ := by simp only [lt_top_iff_ne_top, Ne, rpow_eq_top_iff_of_pos hy] +set_option trace.profiler true in theorem rpow_eq_top_of_nonneg (x : ℝ≥0∞) {y : ℝ} (hy0 : 0 ≤ y) : x ^ y = ⊤ → x = ⊤ := by - rw [ENNReal.rpow_eq_top_iff] - rintro (h|h) - · exfalso - rw [lt_iff_not_ge] at h - exact h.right hy0 - · exact h.left + simp +contextual [ENNReal.rpow_eq_top_iff, hy0.not_gt] -- This is an unsafe rule since we want to try `rpow_ne_top_of_ne_zero` if `y < 0`. @[aesop (rule_sets := [finiteness]) unsafe apply] ``` ``` ℹ [1872/1872] Built Mathlib.Analysis.SpecialFunctions.Pow.NNReal (6.0s) info: Mathlib/Analysis/SpecialFunctions/Pow/NNReal.lean:557:0: [Elab.async] [0.018873] elaborating proof of ENNReal.rpow_eq_top_of_nonneg [Elab.definition.value] [0.018350] ENNReal.rpow_eq_top_of_nonneg [Elab.step] [0.018131] simp +contextual [ENNReal.rpow_eq_top_iff, hy0.not_gt] [Elab.step] [0.018118] simp +contextual [ENNReal.rpow_eq_top_iff, hy0.not_gt] [Elab.step] [0.018101] simp +contextual [ENNReal.rpow_eq_top_iff, hy0.not_gt] Build completed successfully (1872 jobs). ```
maintainer-merge t-analysis 1/6 Mathlib/Analysis/SpecialFunctions/Pow/NNReal.lean 1 6 ['eric-wieser', 'euprunin', 'github-actions', 'grunweg', 'kim-em'] ADedecker
assignee:ADedecker
2-72966
2 days ago
19-8801
19 days ago
19-9308
19 days
25832 xroblot
author:xroblot
 feat(FieldTheory/LinearDisjoint): `trace` (resp. `norm`) and `algebraMap` commutes For `A` and `B` two linearly disjoint `R`-subalgebras in a commutative algebra `S` and `b` a `R`-basis of `B`, we construct a `A`-basis of `S = A ⊔ B` from `b` (and a similar construction using a `R`-basis of `A`). Then, we prove in this situation that `trace` commutes with `algebraMap`, that is: ```lean Algebra.trace A S (algebraMap B S x) = algebraMap R A (Algebra.trace R B x) ``` and a similar result for the norm. We also add a similar basis construction for `A` and `B` two linearly disjoint intermediate fields with the hypothesis that `A.toSubalgebra ⊔ B.toSubalgebra = ⊤`. This hypothesis is equivalent to `A ⊔ B = ⊤` in many cases (for example, one of the two extensions is algebraic over the base field) but not always. --- [![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$
 159/9 Mathlib/FieldTheory/LinearDisjoint.lean,Mathlib/RingTheory/LinearDisjoint.lean 2 47 ['acmepjz', 'chrisflav', 'github-actions', 'xroblot'] chrisflav
assignee:chrisflav
1-60530
1 day ago
1-61192
1 day ago
64-26172
64 days
25858 themathqueen
author:themathqueen
 feat(RingTheory/Coalgebra/MulOpposite): coalgebra instance for MulOpposite Adding an instance for `Aᵐᵒᵖ` being an `R`-coalgebra when `A` is. --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) t-ring-theory maintainer-merge new-contributor 69/0 Mathlib.lean,Mathlib/LinearAlgebra/TensorProduct/Basic.lean,Mathlib/RingTheory/Coalgebra/MulOpposite.lean 3 6 ['chrisflav', 'github-actions'] chrisflav
assignee:chrisflav
1-60339
1 day ago
1-60339
1 day ago
67-43110
67 days
28617 kckennylau
author:kckennylau
 feat(AlgebraicGeometry): jointly surjective topology We define `jointlySurjectiveTopology` to have the same condition as `jointlySurjectivePretopology`, which is the new name of the former `surjectiveFamiliesPretopology`. --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) maintainer-merge t-algebraic-geometry 48/3 Mathlib/AlgebraicGeometry/Sites/MorphismProperty.lean,Mathlib/CategoryTheory/Sites/Grothendieck.lean 2 6 ['chrisflav', 'github-actions', 'kckennylau'] chrisflav
assignee:chrisflav
1-54377
1 day ago
1-54727
1 day ago
2-6880
2 days
28615 kckennylau
author:kckennylau
 feat(RingTheory): Standard open immersion We define the ring hom property `RingHom.IsStandardOpenImmersion` which is one that is a localization map away from some element. --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) t-ring-theory maintainer-merge 122/2 Mathlib.lean,Mathlib/RingTheory/Localization/Away/Basic.lean,Mathlib/RingTheory/Localization/BaseChange.lean,Mathlib/RingTheory/RingHom/OpenImmersion.lean 4 15 ['chrisflav', 'github-actions', 'kckennylau'] chrisflav
assignee:chrisflav
1-47865
1 day ago
1-47865
1 day ago
2-7957
2 days
28180 kckennylau
author:kckennylau
 chore(Meta): clean up PiFin.mkLiteralQ Co-authored by Aaron Liu. This PR fixes the resulting type of `loop`, adds a docstring, and removes an unused variable. --- Zulip: [#PR reviews > #28148 Simproc for Matrix Transpose](https://leanprover.zulipchat.com/#narrow/channel/144837-PR-reviews/topic/.2328148.20Simproc.20for.20Matrix.20Transpose) [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) t-data maintainer-merge t-meta 7/4 Mathlib/Data/Fin/VecNotation.lean 1 23 ['JovanGerb', 'eric-wieser', 'github-actions', 'kckennylau', 'plp127'] nobody
1-34091
1 day ago
1-41513
1 day ago
4-35645
4 days
27039 Scarlett-le
author:Scarlett-le
 feat(Geometry/Euclidean/Sphere/Basic): add theorems for angles subtended by diameters Add two formulations relating sphere diameters and right angles: * `angle_eq_pi_div_two_iff_mem_sphere_of_isDiameter`: For a diameter of a sphere, the angle subtended by the diameter at any other point on the sphere is a right angle if and only if the point lies on the sphere. * `angle_eq_pi_div_two_iff_mem_sphere_ofDiameter`: For three distinct points, the angle at the second point is a right angle if and only if the second point lies on the sphere having the first and third points as diameter endpoints. --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) maintainer-merge new-contributor t-euclidean-geometry awaiting-author 44/0 Mathlib/Geometry/Euclidean/Angle/Sphere.lean,docs/1000.yaml 2 22 ['JovanGerb', 'Scarlett-le', 'github-actions', 'jcommelin', 'jsm28'] nobody
0-71741
19 hours ago
6-39714
6 days ago
4-32009
4 days
19872 YaelDillies
author:YaelDillies
 chore(GroupTheory/Index): rename `relindex` to `relIndex` Zulip discussion about renaming: [#PR reviews > #19872 rename relindex to relIndex @ 💬](https://leanprover.zulipchat.com/#narrow/channel/144837-PR-reviews/topic/.2319872.20rename.20relindex.20to.20relIndex/near/515908054) --- - [x] depends on: #24044 [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) FLT maintainer-merge t-algebra
label:t-algebra$
 288/182 Mathlib/Algebra/Module/ZLattice/Covolume.lean,Mathlib/FieldTheory/Relrank.lean,Mathlib/GroupTheory/Commensurable.lean,Mathlib/GroupTheory/CosetCover.lean,Mathlib/GroupTheory/GroupAction/Blocks.lean,Mathlib/GroupTheory/Index.lean,Mathlib/GroupTheory/IndexNormal.lean,Mathlib/GroupTheory/PGroup.lean,Mathlib/GroupTheory/Schreier.lean,Mathlib/GroupTheory/SchurZassenhaus.lean,Mathlib/GroupTheory/Sylow.lean,Mathlib/GroupTheory/Transfer.lean,Mathlib/LinearAlgebra/FreeModule/Finite/CardQuotient.lean,Mathlib/NumberTheory/ModularForms/CongruenceSubgroups.lean,Mathlib/NumberTheory/NumberField/Discriminant/Different.lean,Mathlib/NumberTheory/NumberField/Units/Regulator.lean,Mathlib/RingTheory/Ideal/Quotient/Index.lean 17 27 ['Ruben-VandeVelde', 'TwoFX', 'YaelDillies', 'alreadydone', 'eric-wieser', 'github-actions', 'kbuzzard', 'leanprover-community-bot-assistant', 'loefflerd', 'madvorak', 'mathlib4-dependent-issues-bot', 'mathlib4-merge-conflict-bot', 'tb65536'] nobody
0-60235
16 hours ago
7-55242
7 days ago
200-68756
200 days
28663 harahu
author:harahu
 doc(Tactic): hyphenate "right-hand" and "left-hand" where appropriate --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) maintainer-merge t-meta 18/18 Mathlib/Tactic/ApplyCongr.lean,Mathlib/Tactic/CC/Addition.lean,Mathlib/Tactic/CC/Datatypes.lean,Mathlib/Tactic/CategoryTheory/Slice.lean,Mathlib/Tactic/LinearCombination'.lean,Mathlib/Tactic/LinearCombination.lean,Mathlib/Tactic/SetLike.lean,Mathlib/Tactic/Widget/LibraryRewrite.lean 8 3 ['github-actions', 'grunweg'] nobody
0-55983
15 hours ago
0-56113
15 hours ago
1-12237
1 day
27837 CBirkbeck
author:CBirkbeck
 feat(NumberTheory/Divisors): add divisorAntidiagonal equivalence. --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) maintainer-merge t-number-theory 1/0 Mathlib.lean 1 10 ['CBirkbeck', 'github-actions', 'riccardobrasca', 'tb65536'] tb65536
assignee:tb65536
0-50006
13 hours ago
9-8828
9 days ago
17-37630
17 days
28142 YaelDillies
author:YaelDillies
 refactor: state hypotheses of `BialgHom.ofAlgHom` as equalities of `AlgHom`s ... as opposed to equalities of `LinearMap`s, and similarly for `BialgEquiv.ofAlgEquiv`. This way, dedicated `ext` lemmas can fire. From Toric --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) t-ring-theory toric maintainer-merge 34/19 Mathlib/Algebra/Algebra/Equiv.lean,Mathlib/RingTheory/Bialgebra/Equiv.lean,Mathlib/RingTheory/Bialgebra/Hom.lean 3 3 ['chrisflav', 'github-actions'] chrisflav
assignee:chrisflav
0-46289
12 hours ago
0-55519
15 hours ago
11-64575
11 days
27889 astrainfinita
author:astrainfinita
 chore(RingTheory/(Mv)PowerSeries): use implicit parameters in `monomial`, `coeff`, `map`, `C`, and `constantCoeff` Just like what we did for `Polynomial`, `MvPolynomial`, and `HahnSeries`. --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) maintainer-merge t-algebra
label:t-algebra$
 555/572 Archive/Wiedijk100Theorems/Partition.lean,Mathlib/NumberTheory/Bernoulli.lean,Mathlib/NumberTheory/ModularForms/QExpansion.lean,Mathlib/RingTheory/HahnSeries/HEval.lean,Mathlib/RingTheory/HahnSeries/PowerSeries.lean,Mathlib/RingTheory/KrullDimension/NonZeroDivisors.lean,Mathlib/RingTheory/LaurentSeries.lean,Mathlib/RingTheory/MvPowerSeries/Basic.lean,Mathlib/RingTheory/MvPowerSeries/Evaluation.lean,Mathlib/RingTheory/MvPowerSeries/Inverse.lean,Mathlib/RingTheory/MvPowerSeries/LexOrder.lean,Mathlib/RingTheory/MvPowerSeries/LinearTopology.lean,Mathlib/RingTheory/MvPowerSeries/NoZeroDivisors.lean,Mathlib/RingTheory/MvPowerSeries/Order.lean,Mathlib/RingTheory/MvPowerSeries/PiTopology.lean,Mathlib/RingTheory/MvPowerSeries/Substitution.lean,Mathlib/RingTheory/MvPowerSeries/Trunc.lean,Mathlib/RingTheory/Polynomial/Eisenstein/Distinguished.lean,Mathlib/RingTheory/Polynomial/GaussNorm.lean,Mathlib/RingTheory/Polynomial/HilbertPoly.lean,Mathlib/RingTheory/PowerSeries/Basic.lean,Mathlib/RingTheory/PowerSeries/Binomial.lean,Mathlib/RingTheory/PowerSeries/CoeffMulMem.lean,Mathlib/RingTheory/PowerSeries/Derivative.lean,Mathlib/RingTheory/PowerSeries/Evaluation.lean,Mathlib/RingTheory/PowerSeries/GaussNorm.lean,Mathlib/RingTheory/PowerSeries/Inverse.lean,Mathlib/RingTheory/PowerSeries/NoZeroDivisors.lean,Mathlib/RingTheory/PowerSeries/Order.lean,Mathlib/RingTheory/PowerSeries/PiTopology.lean,Mathlib/RingTheory/PowerSeries/Substitution.lean,Mathlib/RingTheory/PowerSeries/Trunc.lean,Mathlib/RingTheory/PowerSeries/WeierstrassPreparation.lean,Mathlib/RingTheory/PowerSeries/WellKnown.lean 34 21 ['alreadydone', 'github-actions', 'leanprover-bot', 'mathlib4-merge-conflict-bot'] nobody
0-38455
10 hours ago
0-47180
13 hours ago
11-23438
11 days
27040 Scarlett-le
author:Scarlett-le
 feat(Geometry/Euclidean/Sphere/Power): add power of a point theorems Add the definition of power of a point and fundamental theorems relating point positions to intersection distances: * `Sphere.power`: The power of a point with respect to a sphere, defined as the square of the distance from the point to the center minus the square of the radius. * `Sphere.power_eq_zero_iff_mem_sphere`: A point lies on the sphere if and only if its power is zero. * `Sphere.power_pos_iff_dist_center_gt_radius`: The power is positive if and only if the point is outside the sphere. * `Sphere.power_neg_iff_dist_center_lt_radius`: The power is negative if and only if the point is inside the sphere. * `Sphere.mul_dist_eq_power_of_dist_center_gt_radius`: For external points, the product of intersection distances equals the power. * `Sphere.mul_dist_eq_neg_power_of_dist_center_lt_radius`: For internal points, the product equals the negative power. * `Sphere.mul_dist_eq_abs_power`: General form relating intersection distance products to absolute power. --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) maintainer-merge new-contributor t-euclidean-geometry awaiting-author 110/1 Mathlib/Geometry/Euclidean/Sphere/Power.lean 1 31 ['JovanGerb', 'Scarlett-le', 'alreadydone', 'github-actions', 'jcommelin', 'jsm28'] jsm28
assignee:jsm28
0-33412
9 hours ago
6-37881
6 days ago
32-72818
32 days
25179 YaelDillies
author:YaelDillies
 feat: `#print sorries`, a command to find usage of `sorry` `#print sorries` returns all sorries in the current file. `#print sorries id1 ... idn` returns all sorries in declarations `id1`, ..., `idn`. Such a command is a recurrent need of the community, see eg [here](https://leanprover.zulipchat.com/#narrow/channel/217875-Is-there-code-for-X.3F/topic/Hunting.20down.20axioms/with/495448595) most recently. From Toric Co-authored-by: Henrik Böving Co-authored-by: Kyle Miller --- An alternative implementation was provided in [#Is there code for X? > ✔ Finding usages of `sorry` in external code @ 💬](https://leanprover.zulipchat.com/#narrow/channel/217875-Is-there-code-for-X.3F/topic/.E2.9C.94.20Finding.20usages.20of.20.60sorry.60.20in.20external.20code/near/430509619) by @kmill. I prefer the current one because it only prints something for uses of `sorry` and not the other three standard axioms. [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) toric maintainer-merge t-meta 121/0 Mathlib.lean,Mathlib/Util/PrintSorries.lean,MathlibTest/Util/PrintSorries.lean 3 29 ['YaelDillies', 'bryangingechen', 'dwrensha', 'eric-wieser', 'github-actions', 'kmill'] dwrensha
assignee:dwrensha
0-23022
6 hours ago
0-45999
12 hours ago
86-60800
86 days
28697 chrisflav
author:chrisflav
 chore(RingTheory/Generators): make type argument in `localizationAway` and `baseChange` explicit The `S` (resp. `T`) argument in `Generators.localizationAway` (resp. `Generators.baseChange`) is not inferable from the other arguments and is currently frequently explicitly provided. Moreover, `Presentation.localizationAway` (resp. `Presentation.baseChange`) already take `S` (resp. `T`) explicitly. --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) t-ring-theory maintainer-merge 21/19 Mathlib/RingTheory/Extension/Cotangent/LocalizationAway.lean,Mathlib/RingTheory/Extension/Generators.lean,Mathlib/RingTheory/Extension/Presentation/Basic.lean 3 2 ['Ruben-VandeVelde', 'github-actions'] nobody
0-17426
4 hours ago
0-17426
4 hours ago
0-39437
10 hours
28656 euprunin
author:euprunin
 chore(Data/Int): golf entire `coe_leastOfBdd_eq` and `coe_greatestOfBdd_eq` using `grind` --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) t-data maintainer-merge 2/6 Mathlib/Data/Int/LeastGreatest.lean 1 1 ['github-actions'] nobody
0-16839
4 hours ago
1-28655
1 day ago
1-28701
1 day
28640 euprunin
author:euprunin
 chore(Data/List): golf entire `getElem?_getD_replicate_default_eq` and `getD_append_right` using `grind` --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) t-data maintainer-merge 2/9 Mathlib/Data/List/GetD.lean 1 1 ['github-actions'] nobody
0-16792
4 hours ago
1-40218
1 day ago
1-40266
1 day
25123 eric-wieser
author:eric-wieser
 feat: add rfl lemmas for monoidal categories Making these `simp` opens a can of worms best left to #24823 `simps` would generate bad names here. --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) maintainer-merge t-algebra
label:t-algebra$
 111/0 Mathlib/Algebra/Category/AlgCat/Monoidal.lean,Mathlib/Algebra/Category/ModuleCat/Monoidal/Basic.lean,Mathlib/LinearAlgebra/QuadraticForm/QuadraticModuleCat/Monoidal.lean 3 1 ['github-actions'] dagurtomas
assignee:dagurtomas
0-14384
3 hours ago
90-774
2 months ago
90-824
90 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
78-81861
2 months ago
78-81862
2 months ago
10-26015
10 days
23961 FR-vdash-bot
author:FR-vdash-bot
 refactor: unbundle algebra from `ENormed*` Further speed up the search in the algebraic typeclass hierarchy by avoiding searching for `TopologicalSpace`. --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) slow-typeclass-synthesis maintainer-merge t-algebra t-analysis merge-conflict awaiting-author
label:t-algebra$
 32/25 Mathlib/Analysis/CStarAlgebra/CStarMatrix.lean,Mathlib/Analysis/Normed/Group/Basic.lean,Mathlib/Analysis/Normed/Group/Continuity.lean,Mathlib/Analysis/NormedSpace/IndicatorFunction.lean,Mathlib/MeasureTheory/Function/LpSeminorm/Basic.lean 5 12 ['FR-vdash-bot', 'github-actions', 'grunweg', 'jcommelin', 'leanprover-bot', 'leanprover-community-bot-assistant'] nobody
74-66079
2 months ago
74-66079
2 months ago
17-72244
17 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
23866 kim-em
author:kim-em
 chore: remove `[AtLeastTwo n]` hypothesis from the `NatCast` to `OfNat` instance This PR observes that we can change ``` instance (priority := 100) instOfNatAtLeastTwo {n : ℕ} [NatCast R] [Nat.AtLeastTwo n] : OfNat R n ``` to ``` instance (priority := 100) instOfNatAtLeastTwo {n : ℕ} [NatCast R] : OfNat R n ``` with minimal fall-out. A follow-up PR #23867 then observes that we can remove nearly all the `[Nat.AtLeastTwo n]` hypotheses in Mathlib. This is slightly dangerous -- it does make it more likely that we'll generate non-defeq instances, but it appears to happen very rarely. However, it will make life slightly easier for something Leo and I are trying to do with `grind` and Grobner bases (we'd like to be able to assume types we consume have `[∀ n, OfNat α n]`, which is possible with this change, but not without...). Zulip thread: [#PR reviews > #23866 and #23867, removing most `[Nat.AtLeastTwo n]` @ 💬](https://leanprover.zulipchat.com/#narrow/channel/144837-PR-reviews/topic/.2323866.20and.20.2323867.2C.20removing.20most.20.60.5BNat.2EAtLeastTwo.20n.5D.60/near/511157297) awaiting-zulip 21/26 Mathlib/AlgebraicTopology/FundamentalGroupoid/Basic.lean,Mathlib/Data/Nat/Cast/Defs.lean,Mathlib/Data/Nat/Cast/Order/Basic.lean 3 3 ['eric-wieser', 'github-actions', 'urkud'] nobody
133-23123
4 months ago
133-23212
4 months ago
0-23929
6 hours
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
107-10600
3 months ago
107-10609
3 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
107-9911
3 months ago
107-10546
3 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
77-62771
2 months ago
107-10510
3 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
74-20162
2 months ago
74-20163
2 months ago
34-10595
34 days
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
338-74033
11 months ago
339-9608
11 months 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
273-47283
9 months ago
273-47283
9 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
118-2660
3 months ago
129-31290
4 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
93-33166
3 months ago
93-33167
3 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
93-32240
3 months ago
93-32242
3 months ago
39-67601
39 days
24409 urkud
author:urkud
 chore(*): fix `nmem` vs `not_mem` names --- There are some missing/buggy deprecations, I'm going to fix them later today or tomorrow. [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) awaiting-zulip tech debt merge-conflict delegated awaiting-author 317/176 Mathlib/Algebra/BigOperators/Finprod.lean,Mathlib/Algebra/BigOperators/Group/Finset/Lemmas.lean,Mathlib/Algebra/Group/Indicator.lean,Mathlib/Algebra/Group/Support.lean,Mathlib/Algebra/GroupWithZero/NonZeroDivisors.lean,Mathlib/Algebra/Order/Group/Indicator.lean,Mathlib/Algebra/Polynomial/AlgebraMap.lean,Mathlib/Algebra/Polynomial/Degree/Operations.lean,Mathlib/Analysis/Calculus/BumpFunction/Basic.lean,Mathlib/Analysis/Calculus/DSlope.lean,Mathlib/Analysis/Calculus/Deriv/Basic.lean,Mathlib/Analysis/Calculus/Deriv/Support.lean,Mathlib/Analysis/Calculus/FDeriv/Basic.lean,Mathlib/Analysis/Calculus/Rademacher.lean,Mathlib/Analysis/Complex/RemovableSingularity.lean,Mathlib/Analysis/Convex/Cone/InnerDual.lean,Mathlib/Analysis/Convex/Cone/Proper.lean,Mathlib/Analysis/Convolution.lean,Mathlib/Analysis/Distribution/AEEqOfIntegralContDiff.lean,Mathlib/Data/LocallyFinsupp.lean,Mathlib/Data/Set/Basic.lean,Mathlib/Data/Set/Insert.lean,Mathlib/Dynamics/Ergodic/Conservative.lean,Mathlib/Dynamics/Ergodic/Ergodic.lean,Mathlib/Dynamics/Ergodic/Function.lean,Mathlib/Dynamics/PeriodicPts/Defs.lean,Mathlib/Geometry/Manifold/ContMDiff/Basic.lean,Mathlib/Geometry/Manifold/PartitionOfUnity.lean,Mathlib/GroupTheory/CosetCover.lean,Mathlib/LinearAlgebra/Dual/Lemmas.lean,Mathlib/LinearAlgebra/FreeModule/PID.lean,Mathlib/LinearAlgebra/PID.lean,Mathlib/LinearAlgebra/RootSystem/Base.lean,Mathlib/LinearAlgebra/RootSystem/Finite/Lemmas.lean,Mathlib/MeasureTheory/Function/ContinuousMapDense.lean,Mathlib/MeasureTheory/Function/ConvergenceInMeasure.lean,Mathlib/MeasureTheory/Function/L2Space.lean,Mathlib/MeasureTheory/Function/LocallyIntegrable.lean,Mathlib/MeasureTheory/Function/LpSpace/Indicator.lean,Mathlib/MeasureTheory/Integral/Average.lean,Mathlib/MeasureTheory/Integral/Bochner/Set.lean,Mathlib/MeasureTheory/Integral/Layercake.lean,Mathlib/MeasureTheory/Integral/Lebesgue/Add.lean,Mathlib/MeasureTheory/Integral/Lebesgue/Basic.lean,Mathlib/MeasureTheory/Integral/RieszMarkovKakutani/Basic.lean,Mathlib/MeasureTheory/Integral/RieszMarkovKakutani/Real.lean,Mathlib/MeasureTheory/Measure/AbsolutelyContinuous.lean,Mathlib/MeasureTheory/Measure/AddContent.lean,Mathlib/MeasureTheory/Measure/DiracProba.lean,Mathlib/MeasureTheory/Measure/Haar/Unique.lean,Mathlib/MeasureTheory/Measure/Restrict.lean,Mathlib/MeasureTheory/Measure/WithDensity.lean,Mathlib/MeasureTheory/OuterMeasure/AE.lean,Mathlib/MeasureTheory/SetSemiring.lean,Mathlib/Order/Filter/AtTopBot/CountablyGenerated.lean,Mathlib/Order/Filter/Cocardinal.lean,Mathlib/Order/Filter/Cofinite.lean,Mathlib/Order/Filter/Tendsto.lean,Mathlib/Order/Filter/Ultrafilter/Basic.lean,Mathlib/Probability/Distributions/Uniform.lean,Mathlib/Probability/Kernel/Basic.lean,Mathlib/Probability/Kernel/Composition/MeasureCompProd.lean,Mathlib/RingTheory/AdicCompletion/LocalRing.lean,Mathlib/RingTheory/Ideal/Maximal.lean,Mathlib/RingTheory/LaurentSeries.lean,Mathlib/RingTheory/MvPolynomial/Symmetric/NewtonIdentities.lean,Mathlib/RingTheory/MvPowerSeries/NoZeroDivisors.lean,Mathlib/RingTheory/Spectrum/Maximal/Localization.lean,Mathlib/RingTheory/Spectrum/Prime/RingHom.lean,Mathlib/RingTheory/Spectrum/Prime/Topology.lean,Mathlib/Topology/Algebra/InfiniteSum/Group.lean,Mathlib/Topology/Algebra/Module/Cardinality.lean,Mathlib/Topology/Algebra/Support.lean,Mathlib/Topology/Bases.lean,Mathlib/Topology/ContinuousMap/BoundedCompactlySupported.lean,Mathlib/Topology/Order/Basic.lean,Mathlib/Topology/UrysohnsLemma.lean 77 4 ['b-mehta', 'github-actions', 'jcommelin', 'leanprover-community-bot-assistant', 'mathlib-bors'] nobody
79-68138
2 months ago
79-68138
2 months ago
0-55045
15 hours
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
46-77309
1 month ago
46-77309
1 month 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
46-76147
1 month ago
46-76148
1 month 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
6-18241
6 days ago
7-5613
7 days ago
0-61617
17 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
291-27752
9 months ago
317-16274
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 [![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
107-10560
3 months ago
107-10565
3 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
25770 Parcly-Taxel
author:Parcly-Taxel
 chore: fix more induction/recursor branch names These were found using the regex `\| h. =>` and `def.*rec.*\(h. :`. tech debt 75/68 Mathlib/Analysis/Convolution.lean,Mathlib/Data/ENat/Basic.lean,Mathlib/Data/Fin/Tuple/Basic.lean,Mathlib/Data/Fin/Tuple/NatAntidiagonal.lean,Mathlib/Data/Seq/Computation.lean,Mathlib/Data/Set/Card.lean,Mathlib/Data/WSeq/Basic.lean,Mathlib/Logic/Function/Iterate.lean,Mathlib/NumberTheory/ArithmeticFunction.lean,Mathlib/Order/SuccPred/Archimedean.lean,Mathlib/Order/Synonym.lean 11 16 ['Parcly-Taxel', 'eric-wieser', 'github-actions', 'leanprover-community-bot-assistant', 'mathlib4-merge-conflict-bot'] Vierkantor
assignee:Vierkantor
11-74432
11 days ago
12-33316
12 days ago
67-60944
67 days
25774 Parcly-Taxel
author:Parcly-Taxel
 chore: deprime `induction` in `AlgebraicTopology/CategoryTheory` Most replacements that are also in #23676 have been copied over, but some have been optimised further. tech debt 130/121 Mathlib/AlgebraicTopology/DoldKan/Decomposition.lean,Mathlib/AlgebraicTopology/DoldKan/Degeneracies.lean,Mathlib/AlgebraicTopology/DoldKan/NCompGamma.lean,Mathlib/AlgebraicTopology/DoldKan/Projections.lean,Mathlib/AlgebraicTopology/SimplexCategory/MorphismProperty.lean,Mathlib/AlgebraicTopology/SimplicialObject/Split.lean,Mathlib/AlgebraicTopology/SimplicialSet/Degenerate.lean,Mathlib/AlgebraicTopology/SimplicialSet/NerveAdjunction.lean,Mathlib/AlgebraicTopology/SimplicialSet/StdSimplex.lean,Mathlib/CategoryTheory/Abelian/GrothendieckCategory/EnoughInjectives.lean,Mathlib/CategoryTheory/Abelian/GrothendieckCategory/Subobject.lean,Mathlib/CategoryTheory/Action/Concrete.lean,Mathlib/CategoryTheory/Action/Monoidal.lean,Mathlib/CategoryTheory/ComposableArrows.lean,Mathlib/CategoryTheory/Extensive.lean,Mathlib/CategoryTheory/Filtered/Basic.lean,Mathlib/CategoryTheory/Galois/Decomposition.lean,Mathlib/CategoryTheory/Galois/EssSurj.lean,Mathlib/CategoryTheory/Limits/Shapes/Equalizers.lean,Mathlib/CategoryTheory/Limits/Shapes/SequentialProduct.lean,Mathlib/CategoryTheory/Limits/VanKampen.lean,Mathlib/CategoryTheory/Quotient.lean,Mathlib/CategoryTheory/Sites/Sheaf.lean,Mathlib/CategoryTheory/Subobject/Basic.lean,Mathlib/CategoryTheory/Subobject/FactorThru.lean,Mathlib/CategoryTheory/Subobject/Lattice.lean,Mathlib/CategoryTheory/Triangulated/TStructure/Basic.lean 27 6 ['Parcly-Taxel', 'eric-wieser', 'github-actions', 'leanprover-community-bot-assistant', 'madvorak'] grunweg
assignee:grunweg
10-1421
10 days ago
22-34783
22 days ago
67-27275
67 days
27455 pechersky
author:pechersky
 chore(NumberTheory/Padics/Hensel): rephrase using `aeval` This is easier to use at call site, because on need not pass `Polynomial.map (algebraMap _ _ )` in the use of `hensels_lemma` --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) tech debt t-algebra t-number-theory
label:t-algebra$
 158/139 Mathlib/NumberTheory/Padics/Hensel.lean 1 2 ['github-actions', 'mathlib4-merge-conflict-bot'] jcommelin
assignee:jcommelin
10-1416
10 days ago
17-13445
17 days ago
26-42458
26 days
27339 pechersky
author:pechersky
 chore(RingTheory/Laurent): use WithZero.exp to golf statements and proofs about valuation on K((X)) Done as part of refactor of Valued in #27314. This PR does not change any definitions. Instead, uses `WithZero.exp` instead of coercion + Multiplicative.ofAdd. And some helper simp lemmas about valuations of RatFunc vis a vis LaurentSeries. --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) tech debt t-algebra t-number-theory
label:t-algebra$
 78/77 Mathlib/FieldTheory/RatFunc/AsPolynomial.lean,Mathlib/RingTheory/LaurentSeries.lean,Mathlib/Topology/Algebra/Valued/WithVal.lean 3 2 ['faenuccio', 'github-actions'] Vierkantor
assignee:Vierkantor
8-27148
8 days ago
29-37705
29 days ago
29-81700
29 days
25776 Parcly-Taxel
author:Parcly-Taxel
 chore: deprime `induction` in `Analysis` I think this is very marginally dependent on #25770. tech debt t-analysis 256/208 Mathlib/Analysis/Analytic/Composition.lean,Mathlib/Analysis/Analytic/Constructions.lean,Mathlib/Analysis/Analytic/Inverse.lean,Mathlib/Analysis/BoxIntegral/Basic.lean,Mathlib/Analysis/BoxIntegral/Box/SubboxInduction.lean,Mathlib/Analysis/BoxIntegral/Partition/Additive.lean,Mathlib/Analysis/BoxIntegral/Partition/Split.lean,Mathlib/Analysis/CStarAlgebra/Basic.lean,Mathlib/Analysis/CStarAlgebra/Multiplier.lean,Mathlib/Analysis/Calculus/ContDiff/Basic.lean,Mathlib/Analysis/Calculus/ContDiff/Bounds.lean,Mathlib/Analysis/Calculus/ContDiff/FTaylorSeries.lean,Mathlib/Analysis/Calculus/ContDiff/Operations.lean,Mathlib/Analysis/Calculus/Deriv/ZPow.lean,Mathlib/Analysis/Calculus/InverseFunctionTheorem/ApproximatesLinearOn.lean,Mathlib/Analysis/Calculus/IteratedDeriv/Lemmas.lean,Mathlib/Analysis/Calculus/SmoothSeries.lean,Mathlib/Analysis/Convex/Combination.lean,Mathlib/Analysis/Convex/Radon.lean,Mathlib/Analysis/InnerProductSpace/Projection/FiniteDimensional.lean,Mathlib/Analysis/Normed/Algebra/Exponential.lean,Mathlib/Analysis/NormedSpace/Multilinear/Basic.lean,Mathlib/Analysis/Seminorm.lean,Mathlib/Analysis/SpecialFunctions/Complex/Arg.lean,Mathlib/Analysis/SpecialFunctions/Complex/Circle.lean,Mathlib/Analysis/SpecialFunctions/Gamma/Basic.lean,Mathlib/Analysis/SpecialFunctions/Gamma/Beta.lean,Mathlib/Analysis/SpecialFunctions/Gamma/BohrMollerup.lean,Mathlib/Analysis/SpecialFunctions/Gamma/Deriv.lean,Mathlib/Analysis/SpecialFunctions/Integrals/Basic.lean,Mathlib/Analysis/SpecialFunctions/Log/Basic.lean,Mathlib/Analysis/SpecialFunctions/Pow/Deriv.lean,Mathlib/Analysis/SpecialFunctions/Pow/NNReal.lean,Mathlib/Analysis/SpecialFunctions/Pow/Real.lean,Mathlib/Analysis/SpecialFunctions/Trigonometric/EulerSineProd.lean 35 4 ['Parcly-Taxel', 'github-actions', 'leanprover-community-bot-assistant', 'madvorak', 'mathlib4-merge-conflict-bot'] grunweg
assignee:grunweg
5-1448
5 days ago
12-32416
12 days ago
67-44328
67 days
28517 Vierkantor
author:Vierkantor
 chore(*): address some `@[simps]` porting notes Search for porting notes mentioning `simps` and fix the ones that are easy to fix. The search also caught some that refer to `simps` as in a `simp` set, so we fix them too. --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) tech debt 54/76 Mathlib/AlgebraicGeometry/GammaSpecAdjunction.lean,Mathlib/AlgebraicGeometry/Spec.lean,Mathlib/Analysis/RCLike/Basic.lean,Mathlib/CategoryTheory/Limits/Cones.lean,Mathlib/CategoryTheory/Limits/Shapes/BinaryBiproducts.lean,Mathlib/CategoryTheory/Limits/Shapes/Biproducts.lean,Mathlib/CategoryTheory/Limits/Shapes/Equalizers.lean,Mathlib/CategoryTheory/Limits/Shapes/Pullback/Cospan.lean,Mathlib/CategoryTheory/Localization/Predicate.lean,Mathlib/CategoryTheory/Monad/Adjunction.lean,Mathlib/CategoryTheory/Monad/Algebra.lean,Mathlib/CategoryTheory/Monad/Basic.lean,Mathlib/CategoryTheory/Monoidal/Mon_.lean,Mathlib/CategoryTheory/Preadditive/Mat.lean,Mathlib/LinearAlgebra/LinearIndependent/Defs.lean,Mathlib/Order/OmegaCompletePartialOrder.lean,Mathlib/RepresentationTheory/Rep.lean,Mathlib/RingTheory/GradedAlgebra/Basic.lean,Mathlib/Topology/Homotopy/HomotopyGroup.lean 19 1 ['github-actions'] nobody
2-32684
2 days ago
2-32684
2 days ago
2-32668
2 days
28650 Vierkantor
author:Vierkantor
 chore(Analysis): address a lot of porting notes Go through all porting notes in the Analysis folder and address those with an obvious resolution. A few won'tfixes where Lean 4 is stricter about unfolding or where `@[simp]` attributes were already wrong; otherwise most are easily resolved. --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) tech debt t-analysis 69/134 Mathlib/Analysis/Analytic/Composition.lean,Mathlib/Analysis/Analytic/Uniqueness.lean,Mathlib/Analysis/Asymptotics/Lemmas.lean,Mathlib/Analysis/BoxIntegral/Partition/Basic.lean,Mathlib/Analysis/BoxIntegral/Partition/Tagged.lean,Mathlib/Analysis/CStarAlgebra/Matrix.lean,Mathlib/Analysis/Calculus/ContDiff/Bounds.lean,Mathlib/Analysis/Calculus/FDeriv/Measurable.lean,Mathlib/Analysis/Calculus/FDeriv/Prod.lean,Mathlib/Analysis/Calculus/Implicit.lean,Mathlib/Analysis/Convex/Body.lean,Mathlib/Analysis/Convex/Gauge.lean,Mathlib/Analysis/Convex/Intrinsic.lean,Mathlib/Analysis/Convex/SimplicialComplex/Basic.lean,Mathlib/Analysis/Fourier/RiemannLebesgueLemma.lean,Mathlib/Analysis/InnerProductSpace/Adjoint.lean,Mathlib/Analysis/InnerProductSpace/Orientation.lean,Mathlib/Analysis/InnerProductSpace/PiL2.lean,Mathlib/Analysis/InnerProductSpace/Projection/Basic.lean,Mathlib/Analysis/InnerProductSpace/Projection/FiniteDimensional.lean,Mathlib/Analysis/InnerProductSpace/TwoDim.lean,Mathlib/Analysis/Matrix.lean,Mathlib/Analysis/Normed/Affine/Isometry.lean,Mathlib/Analysis/Normed/Group/AddTorsor.lean,Mathlib/Analysis/Normed/Group/Basic.lean,Mathlib/Analysis/Normed/Group/Quotient.lean,Mathlib/Analysis/Normed/Group/Rat.lean,Mathlib/Analysis/Normed/Group/SemiNormedGrp/Kernels.lean,Mathlib/Analysis/Normed/Lp/lpSpace.lean,Mathlib/Analysis/Normed/Module/Basic.lean,Mathlib/Analysis/Normed/Operator/Banach.lean,Mathlib/Analysis/Normed/Operator/BoundedLinearMaps.lean,Mathlib/Analysis/Normed/Ring/Lemmas.lean,Mathlib/Analysis/Normed/Unbundled/RingSeminorm.lean,Mathlib/Analysis/NormedSpace/Extend.lean,Mathlib/Analysis/NormedSpace/MStructure.lean,Mathlib/Analysis/NormedSpace/OperatorNorm/Completeness.lean,Mathlib/Analysis/Seminorm.lean,Mathlib/Analysis/SpecialFunctions/PolarCoord.lean,Mathlib/Analysis/SpecialFunctions/Trigonometric/Angle.lean,Mathlib/LinearAlgebra/FiniteDimensional/Defs.lean 41 11 ['Vierkantor', 'github-actions'] nobody
0-60361
16 hours ago
1-31274
1 day ago
1-31259
1 day