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: September 13, 2025 at 13:04 UTC

Stale ready-to-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
27849 robin-carlier
author:robin-carlier
feat(CategoryTheory/Bicategory/Functor): strictly unitary lax/pseudo functors We define strictly unitary lax/pseudo functors between bicategories. A lax (resp. pseudo-)functor from `C` to `D` is strictly unitary if `F.map(𝟙 X) = 𝟙 (F.obj X)` and if the 2-cell `mapId` is the identity 2-cell induced by this equality. We provide a constructor for those that do not require the `mapId` field. Although this structure is somewhat "evil" from a purely categorical perspective (it mentions non-definitonal equality of objects in a 1-category), these class of functors are of interest: strictly unitary lax functors are part of the definition of the Duskin nerve of a bicategory (which embeds bicategories in the theory of simplicial sets), while strictly unitary pseudofunctors are part of the definition of the 2-nerve of a bicategory, which embeds bicategories into the theory of simplicial categories. This PR is part of an ongoing work that will hopefully culminate with the construction of the Duskin Nerve, as well as a proof of the fact that the Duskin nerve of a locally groupoidal bicategory is a quasicategory. --- Two designs were possible here: making `StrictlyUnitary` a class on lax/pseudo-functors to state that some functors/constructions are strictly unitary, or bundling it as a structure on its own. Since my plan for the follow-up PRs is to use the type of strictly lax unitary functors between some bicategories (e.g to define lax-composable arrows in a bicategory `C`, which will be by definition `StrictlyUnitaryLaxFunctor (LocallyDiscrete (Fin n)) C`), I chose to bundle them directly, to avoid an extra layer when working with the type of those objects. I did include strict associativity for strictly unitary lax functors but not for pseudofunctors. The reason is that the Duskin nerve mentions the 1-category of bicategories and strictly unitary lax functors (hence, this strict associativity/unitality), but the 2-nerve mentions the bicategory of bicategories, strictly unitary pseudofunctors and "icons" (identity-component oplax natural transformations): the statement for associativity for pseudofunctors will wait for icons, and will probably not be stated as an equality of pseudofunctors. [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) t-category-theory ready-to-merge delegated 356/0 Mathlib.lean,Mathlib/CategoryTheory/Bicategory/Functor/StrictlyUnitary.lean 2 8 ['adamtopaz', 'github-actions', 'mathlib-bors', 'robin-carlier'] adamtopaz
assignee:adamtopaz
1-53667
1 day ago
1-55648
1 day ago
38-25023
38 days
29493 kim-em
author:kim-em
chore: grind golf in Mathlib.Logic More golfs identified by `linter.tacticAnalysis.terminalToGrind`. t-logic ready-to-merge 8/20 Mathlib/Logic/Basic.lean,Mathlib/Logic/Function/Basic.lean,Mathlib/Logic/Relation.lean,scripts/noshake.json 4 6 ['euprunin', 'github-actions', 'grunweg', 'kim-em'] nobody
0-802
13 minutes ago
3-14989
3 days ago
3-23800
3 days

Stale maintainer-merge'd PRs

Number Author Title Description Labels +/- Modified files (first 100) 📝 💬 All users who commented or reviewed Assignee(s) Updated Last status change total time in review
25945 adomani
author:adomani
feat: the empty line in commands linter This linter flags empty lines within a command. It allows empty lines within doc-strings, module-docs and a couple of other "sensible" places. It also skips files that are likely to contain meta-code, since there the use of empty lines in definition is more widespread. This PR continues the work from #25236. large-import t-linter maintainer-merge awaiting-author 375/7 Mathlib.lean,Mathlib/Analysis/Meromorphic/FactorizedRational.lean,Mathlib/CategoryTheory/Comma/StructuredArrow/CommaMap.lean,Mathlib/Init.lean,Mathlib/RepresentationTheory/Homological/GroupHomology/LowDegree.lean,Mathlib/Tactic.lean,Mathlib/Tactic/Linter/EmptyLine.lean,MathlibTest/EmptyLine.lean 8 12 ['adomani', 'bryangingechen', 'eric-wieser', 'github-actions'] bryangingechen
assignee:bryangingechen
46-81254
1 month ago
46-81254
1 month ago
42-26074
42 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
38-69970
1 month ago
38-73255
1 month ago
53-4392
53 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 12 ['YaelDillies', 'adomani', 'euprunin', 'github-actions', 'grunweg'] joneugster
assignee:joneugster
19-71032
19 days ago
38-68719
1 month ago
39-14598
39 days
28934 yury-harmonic
author:yury-harmonic
feat(NormNum): add extensions for `Even` and `Odd` --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) maintainer-merge t-meta awaiting-author 55/0 Mathlib.lean,Mathlib/Tactic.lean,Mathlib/Tactic/NormNum/Parity.lean,scripts/noshake.json 4 10 ['JovanGerb', 'adomani', 'digama0', 'github-actions', 'mathlib4-merge-conflict-bot', 'yury-harmonic'] nobody
11-41942
11 days ago
11-59010
11 days ago
6-16639
6 days
29271 euprunin
author:euprunin
chore: remove redundant `let` and `letI` invocations --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) maintainer-merge 1/8 Mathlib/Algebra/Algebra/TransferInstance.lean,Mathlib/Algebra/Module/FinitePresentation.lean,Mathlib/CategoryTheory/Monoidal/Grp_.lean,Mathlib/ModelTheory/Algebra/Ring/FreeCommRing.lean,Mathlib/Topology/Metrizable/Uniformity.lean 5 10 ['JovanGerb', 'github-actions', 'leanprover-bot', 'leanprover-community-mathlib4-bot', 'ocfnash'] nobody
7-3079
7 days ago
7-5611
7 days ago
10-51592
10 days
29404 pechersky
author:pechersky
feat(Data/Nat): p.Coprime factorial and choose And descFactorial, for n < p --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) t-data maintainer-merge t-algebra easy
label:t-algebra$
16/0 Mathlib/Data/Nat/Choose/Dvd.lean,Mathlib/Data/Nat/Prime/Factorial.lean 2 2 ['Ruben-VandeVelde', 'github-actions'] nobody
5-54068
5 days ago
5-54068
5 days ago
5-67643
5 days
24669 qawbecrdtey
author:qawbecrdtey
feat(Analysis/Normed/Operator/LinearIsometry): added definition `LinearIsometryEquiv.prodComm` --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) This commit defines a `LinearIsometryEquiv`, and states some trivial theorems about it. ```lean def prodComm [Module R E₂] : E × E₂ ≃ₗᵢ[R] E₂ × E ``` maintainer-merge t-analysis awaiting-author 8/1 Mathlib/Analysis/Normed/Operator/LinearIsometry.lean 1 12 ['Ruben-VandeVelde', 'eric-wieser', 'faenuccio', 'github-actions', 'j-loreaux', 'jcommelin', 'qawbecrdtey'] faenuccio
assignee:faenuccio
5-41456
5 days ago
95-29288
3 months ago
32-83569
32 days
28945 harahu
author:harahu
doc: hyphenate compound adjectives ending in -dimensional Compound adjectives appearing before the noun they are modifying should be hyphenated in order to avoid ambiguity. This PR hyphenates such compound adjectives than are ending in "-dimensional". It does not cover similar compound adjectives appearing _after_ their noun, as hyphenation is then regarded as a stylistic choice, as opposed to a grammatical tool. --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) maintainer-merge 180/180 Mathlib/Algebra/Azumaya/Matrix.lean,Mathlib/Algebra/BrauerGroup/Defs.lean,Mathlib/Algebra/Category/FGModuleCat/Basic.lean,Mathlib/Algebra/Category/FGModuleCat/Limits.lean,Mathlib/Algebra/Lie/Derivation/Killing.lean,Mathlib/Algebra/Lie/Weights/RootSystem.lean,Mathlib/Algebra/Module/ZLattice/Basic.lean,Mathlib/Algebra/Module/ZLattice/Covolume.lean,Mathlib/Analysis/BoundedVariation.lean,Mathlib/Analysis/Calculus/BumpFunction/Basic.lean,Mathlib/Analysis/Calculus/BumpFunction/SmoothApprox.lean,Mathlib/Analysis/Calculus/ContDiff/FiniteDimension.lean,Mathlib/Analysis/Calculus/Deriv/AffineMap.lean,Mathlib/Analysis/Calculus/Implicit.lean,Mathlib/Analysis/Calculus/LineDeriv/QuadraticMap.lean,Mathlib/Analysis/Complex/AbsMax.lean,Mathlib/Analysis/Complex/Tietze.lean,Mathlib/Analysis/Convex/AmpleSet.lean,Mathlib/Analysis/Convex/Continuous.lean,Mathlib/Analysis/Convex/Measure.lean,Mathlib/Analysis/Convex/SimplicialComplex/Basic.lean,Mathlib/Analysis/Distribution/AEEqOfIntegralContDiff.lean,Mathlib/Analysis/FunctionalSpaces/SobolevInequality.lean,Mathlib/Analysis/InnerProductSpace/Adjoint.lean,Mathlib/Analysis/InnerProductSpace/EuclideanDist.lean,Mathlib/Analysis/InnerProductSpace/JointEigenspace.lean,Mathlib/Analysis/InnerProductSpace/PiL2.lean,Mathlib/Analysis/InnerProductSpace/Spectrum.lean,Mathlib/Analysis/Normed/Module/FiniteDimension.lean,Mathlib/Analysis/Normed/Operator/ContinuousLinearMap.lean,Mathlib/Analysis/NormedSpace/HahnBanach/Extension.lean,Mathlib/Analysis/RCLike/Lemmas.lean,Mathlib/CategoryTheory/Preadditive/Schur.lean,Mathlib/Combinatorics/Additive/AP/Three/Behrend.lean,Mathlib/FieldTheory/Differential/Liouville.lean,Mathlib/FieldTheory/IntermediateField/Algebraic.lean,Mathlib/FieldTheory/IsAlgClosed/Spectrum.lean,Mathlib/FieldTheory/PrimitiveElement.lean,Mathlib/FieldTheory/PurelyInseparable/Basic.lean,Mathlib/Geometry/Manifold/BumpFunction.lean,Mathlib/Geometry/Manifold/ChartedSpace.lean,Mathlib/Geometry/Manifold/Diffeomorph.lean,Mathlib/Geometry/Manifold/Metrizable.lean,Mathlib/Geometry/Manifold/PartitionOfUnity.lean,Mathlib/LinearAlgebra/Coevaluation.lean,Mathlib/LinearAlgebra/Complex/FiniteDimensional.lean,Mathlib/LinearAlgebra/Complex/Module.lean,Mathlib/LinearAlgebra/Dimension/Finite.lean,Mathlib/LinearAlgebra/Dimension/Finrank.lean,Mathlib/LinearAlgebra/Dimension/FreeAndStrongRankCondition.lean,Mathlib/LinearAlgebra/FiniteDimensional/Basic.lean,Mathlib/LinearAlgebra/FiniteDimensional/Defs.lean,Mathlib/LinearAlgebra/FiniteDimensional/Lemmas.lean,Mathlib/LinearAlgebra/Matrix/FiniteDimensional.lean,Mathlib/LinearAlgebra/Matrix/GeneralLinearGroup/Card.lean,Mathlib/LinearAlgebra/Multilinear/FiniteDimensional.lean,Mathlib/MeasureTheory/Integral/TorusIntegral.lean,Mathlib/MeasureTheory/Measure/Haar/InnerProductSpace.lean,Mathlib/MeasureTheory/Measure/Haar/OfBasis.lean,Mathlib/MeasureTheory/Measure/Lebesgue/EqHaar.lean,Mathlib/MeasureTheory/Measure/Lebesgue/VolumeOfBalls.lean,Mathlib/Order/RelSeries.lean,Mathlib/Probability/Process/FiniteDimensionalLaws.lean,Mathlib/RepresentationTheory/FDRep.lean,Mathlib/RepresentationTheory/Maschke.lean,Mathlib/RepresentationTheory/Tannaka.lean,Mathlib/RingTheory/Finiteness/Basic.lean,Mathlib/RingTheory/Finiteness/Lattice.lean,Mathlib/RingTheory/Grassmannian.lean,Mathlib/Tactic/FunProp/Theorems.lean,Mathlib/Topology/Algebra/InfiniteSum/Defs.lean,Mathlib/Topology/Algebra/Module/FiniteDimension.lean,Mathlib/Topology/MetricSpace/HausdorffDimension.lean,MathlibTest/fun_prop.lean,docs/overview.yaml,docs/undergrad.yaml 76 6 ['github-actions', 'mathlib4-merge-conflict-bot', 'tb65536'] tb65536
assignee:tb65536
4-60388
4 days ago
4-60407
4 days ago
17-54592
17 days
29459 bwangpj
author:bwangpj
feat: ContMDiffAt.pow Powers of `C^n` functions `M → G` into a commutative monoid `G` are `C^n`. This is upstreamed from [https://github.com/girving/ray](https://github.com/girving/ray). Co-authored-by: Geoffrey Irving --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) maintainer-merge t-differential-geometry 20/2 Mathlib/Geometry/Manifold/Algebra/Monoid.lean 1 4 ['github-actions', 'grunweg'] grunweg
assignee:grunweg
4-15492
4 days ago
4-15705
4 days ago
4-26130
4 days
29045 grunweg
author:grunweg
chore: remove the `field_simps` simp set This was used for the field_simp tactic before its recent rewrite. Its uses in mathlib were removed in #28918. --- - [x] depends on: #28918 [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) maintainer-merge 31/82 Mathlib/Algebra/CharP/MixedCharZero.lean,Mathlib/Algebra/Field/Basic.lean,Mathlib/Algebra/Group/Basic.lean,Mathlib/Algebra/Group/Defs.lean,Mathlib/Algebra/Group/Units/Basic.lean,Mathlib/Algebra/Group/Units/Defs.lean,Mathlib/Algebra/GroupWithZero/Basic.lean,Mathlib/Algebra/GroupWithZero/Units/Basic.lean,Mathlib/Algebra/NeZero.lean,Mathlib/Algebra/Order/Field/Basic.lean,Mathlib/Algebra/Ring/Basic.lean,Mathlib/Algebra/Ring/Units.lean,Mathlib/Analysis/Complex/Trigonometric.lean,Mathlib/Analysis/InnerProductSpace/Basic.lean,Mathlib/Analysis/MeanInequalitiesPow.lean,Mathlib/Analysis/Normed/Unbundled/SeminormFromBounded.lean,Mathlib/Analysis/Normed/Unbundled/SeminormFromConst.lean,Mathlib/Analysis/Normed/Unbundled/SmoothingSeminorm.lean,Mathlib/Combinatorics/SetFamily/AhlswedeZhang.lean,Mathlib/Combinatorics/SimpleGraph/Density.lean,Mathlib/MeasureTheory/Measure/Haar/Basic.lean,Mathlib/Tactic/Attr/Register.lean 22 7 ['Ruben-VandeVelde', 'bryangingechen', 'github-actions', 'grunweg', 'mathlib4-dependent-issues-bot'] nobody
2-76288
2 days ago
6-61659
6 days ago
15-60524
15 days
29511 luigi-massacci
author:luigi-massacci
feat: integrating wrt a finite measure as a continuous linear map on bounded continuous functions Add a definition `integralFiniteMeasure` of type `ContinuousLinearMap` packaging the integral of a bounded continuous function by a finite measure. --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) maintainer-merge t-measure-probability 17/0 Mathlib/MeasureTheory/Integral/BoundedContinuousFunction.lean 1 23 ['github-actions', 'grunweg', 'luigi-massacci'] nobody
2-67142
2 days ago
2-67143
2 days ago
2-69288
2 days
29498 harahu
author:harahu
doc: improve grammar and flow in documentation This PR might be deemed too stylistic in nature, but I'll propose it anyhow, with the purpose of sectioning out potential for bikeshedding from #29464. The changes are largely the work of LLM coding agents, but I have manually checked every change and have not included anything in this PR that I cannot personally stand for. In totality, my opinion is that this PR improves the legibility, clarity and conciseness of the documentation it covers, and should be merged. --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) maintainer-merge t-computability 40/39 Mathlib/Computability/AkraBazzi/AkraBazzi.lean,Mathlib/Computability/AkraBazzi/GrowsPolynomially.lean,Mathlib/Computability/AkraBazzi/SumTransform.lean 3 12 ['github-actions', 'grunweg', 'harahu', 'themathqueen'] nobody
2-65823
2 days ago
2-80752
2 days ago
3-332
3 days
29408 pechersky
author:pechersky
feat(Analysis/Normed/Ultra): nonarch norm of sum over disjoint norms achieves max --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) I thought about having a `tprod` version too, but wasn't sure the best way to phrase it maintainer-merge t-analysis 24/0 Mathlib/Analysis/Normed/Group/Ultra.lean 1 5 ['github-actions', 'loefflerd'] nobody
2-55352
2 days ago
4-84729
4 days ago
5-66072
5 days
29297 harahu
author:harahu
doc: hyphenate "first order" and "higher order" when used attributively Compound adjectives that are attributive (coming before their noun) should almost always be hyphenated in English. This PR covers "first order" and "higher order". --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) maintainer-merge 24/24 Mathlib/Analysis/Calculus/ContDiff/FTaylorSeries.lean,Mathlib/Analysis/Fourier/FourierTransformDeriv.lean,Mathlib/FieldTheory/AxGrothendieck.lean,Mathlib/Logic/Basic.lean,Mathlib/ModelTheory/Algebra/Field/Basic.lean,Mathlib/ModelTheory/Algebra/Field/CharP.lean,Mathlib/ModelTheory/Algebra/Field/IsAlgClosed.lean,Mathlib/ModelTheory/Algebra/Ring/Basic.lean,Mathlib/RingTheory/MvPolynomial/FreeCommRing.lean,Mathlib/Topology/VectorBundle/Riemannian.lean,docs/undergrad.yaml 11 3 ['github-actions', 'grunweg'] nobody
2-14817
2 days ago
2-14817
2 days ago
10-16462
10 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$
297/191 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 29 ['Ruben-VandeVelde', 'TwoFX', 'YaelDillies', 'alreadydone', 'eric-wieser', 'github-actions', 'joelriou', 'kbuzzard', 'leanprover-community-bot-assistant', 'loefflerd', 'madvorak', 'mathlib4-dependent-issues-bot', 'mathlib4-merge-conflict-bot', 'tb65536'] joelriou
assignee:joelriou
1-55661
1 day ago
10-19691
10 days ago
224-8137
224 days
28706 euprunin
author:euprunin
chore: golf entire `dite_ne_left_iff`, `exists_prime_lt_and_le_two_mul_succ`, `lt_up` and `sUnion_mem_empty_univ` using `grind` --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) maintainer-merge 4/12 Mathlib/Data/Set/Lattice.lean,Mathlib/Logic/Basic.lean,Mathlib/NumberTheory/Bertrand.lean,Mathlib/RingTheory/NoetherNormalization.lean 4 9 ['euprunin', 'github-actions', 'grunweg', 'leanprover-bot', 'leanprover-community-mathlib4-bot', 'mathlib4-merge-conflict-bot', 'tb65536'] tb65536
assignee:tb65536
1-42319
1 day ago
1-42319
1 day ago
15-19458
15 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
102-37441
3 months ago
102-37442
3 months ago
10-26015
10 days
26912 pechersky
author:pechersky
chore(Algebra/Ring/Subring): simp tag `Subring.smul_def` s-multiplying by a subtype is easiest to manipulate when both terms are in the ambient type. Many places that had to use the _def lemma for a rewrite, or to include it in a simp set, no longer have to. Ported from #25308 --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) I found this being not-simp frustrating when talking about submodules over a valuation subring. maintainer-merge t-algebra merge-conflict
label:t-algebra$
68/67 Mathlib/Algebra/Algebra/Subalgebra/Basic.lean,Mathlib/Algebra/Field/Subfield/Basic.lean,Mathlib/Algebra/Group/Subgroup/Actions.lean,Mathlib/Algebra/Group/Submonoid/MulAction.lean,Mathlib/Algebra/Module/LocalizedModule/Basic.lean,Mathlib/Algebra/Module/LocalizedModule/Exact.lean,Mathlib/Algebra/Module/LocalizedModule/IsLocalization.lean,Mathlib/Algebra/Module/LocalizedModule/Submodule.lean,Mathlib/Algebra/Ring/Periodic.lean,Mathlib/Algebra/Ring/Subring/Basic.lean,Mathlib/Algebra/Ring/Subsemiring/Basic.lean,Mathlib/Analysis/CStarAlgebra/Basic.lean,Mathlib/FieldTheory/KummerExtension.lean,Mathlib/GroupTheory/GroupAction/Defs.lean,Mathlib/GroupTheory/GroupAction/MultiplePrimitivity.lean,Mathlib/GroupTheory/GroupAction/MultipleTransitivity.lean,Mathlib/GroupTheory/GroupAction/SubMulAction/OfFixingSubgroup.lean,Mathlib/GroupTheory/GroupAction/SubMulAction/OfStabilizer.lean,Mathlib/LinearAlgebra/RootSystem/Irreducible.lean,Mathlib/LinearAlgebra/RootSystem/RootPositive.lean,Mathlib/LinearAlgebra/RootSystem/WeylGroup.lean,Mathlib/RingTheory/Etale/Kaehler.lean,Mathlib/RingTheory/LocalProperties/Projective.lean,Mathlib/RingTheory/Localization/InvSubmonoid.lean,Mathlib/RingTheory/OreLocalization/Basic.lean 25 19 ['artie2000', 'eric-wieser', 'github-actions', 'j-loreaux', 'linesthatinterlace', 'mathlib4-merge-conflict-bot', 'pechersky'] joelriou
assignee:joelriou
11-85332
11 days ago
11-85333
11 days ago
51-74059
51 days
28737 astrainfinita
author:astrainfinita
refactor: deprecate `MulEquivClass` This PR continues the work from #18806. Original PR: https://github.com/leanprover-community/mathlib4/pull/18806 maintainer-merge t-algebra merge-conflict awaiting-author
label:t-algebra$
67/77 Mathlib/Algebra/BigOperators/Finprod.lean,Mathlib/Algebra/Group/Equiv/Basic.lean,Mathlib/Algebra/Group/Equiv/Defs.lean,Mathlib/Algebra/Group/Irreducible/Lemmas.lean,Mathlib/Algebra/Group/Subgroup/Map.lean,Mathlib/Algebra/Group/Submonoid/Operations.lean,Mathlib/Algebra/Group/Units/Equiv.lean,Mathlib/Algebra/GroupWithZero/Equiv.lean,Mathlib/Algebra/GroupWithZero/NonZeroDivisors.lean,Mathlib/Algebra/Module/Equiv/Defs.lean,Mathlib/Algebra/Order/CauSeq/Basic.lean,Mathlib/Algebra/Order/Hom/Monoid.lean,Mathlib/Algebra/Prime/Lemmas.lean,Mathlib/Algebra/Ring/Divisibility/Basic.lean,Mathlib/Algebra/Ring/Equiv.lean,Mathlib/Algebra/Star/MonoidHom.lean,Mathlib/Combinatorics/Additive/FreimanHom.lean,Mathlib/GroupTheory/GroupExtension/Defs.lean,Mathlib/GroupTheory/Submonoid/Center.lean,Mathlib/LinearAlgebra/FreeModule/Finite/CardQuotient.lean,Mathlib/RingTheory/Bialgebra/Equiv.lean,Mathlib/RingTheory/Ideal/Norm/AbsNorm.lean,Mathlib/RingTheory/Multiplicity.lean,Mathlib/RingTheory/UniqueFactorizationDomain/NormalizedFactors.lean,Mathlib/Topology/Algebra/ContinuousMonoidHom.lean,Mathlib/Topology/Algebra/InfiniteSum/Basic.lean 26 20 ['Vierkantor', 'alreadydone', 'astrainfinita', 'github-actions', 'grunweg', 'leanprover-bot', 'leanprover-community-mathlib4-bot', 'mathlib4-merge-conflict-bot'] Vierkantor
assignee:Vierkantor
3-2792
3 days ago
3-2793
3 days ago
4-17723
4 days
21965 JovanGerb
author:JovanGerb
feat: extensible `push` and `pull` tactics This PR defines the `push` and `pull` tactics, and makes `push_neg` a macro for `push Not`. The tactics are also available in `conv` mode. For tagging, there is only the `@[push]` attribute, which adds the reverse rewrite for the `pull` tactic when relevant. In the future, we may also need a separate `@[pull X]` attribute for pulling `X`. Thanks to this change, we will be able to make `push_neg` into a more powerful tactic by tagging more lemmas. It also means that about 60 files now don't need to import `LinearOrder`/`PartialOrder`. This will be especially useful when we get the `@[to_dual]` attribute. This work originally started in #21769. There is now the follow up PR #29000 which adds `push` tags and tests for them. The `@[push]` attribute is defined in `Mathlib.Tactic.Push.Attr` and the main implementation of `push` and `pull` is in `Mathlib.Tactic.Push`. Some proofs need to be fixed because the new simp-based `push_neg` can see through more reducible definitions. Zulip conversation: [#mathlib4 > I made an extensible `push` tactic generalizing `push_neg`](https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/I.20made.20an.20extensible.20.60push.60.20tactic.20generalizing.20.60push_neg.60) closes #21841 --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) maintainer-merge t-meta merge-conflict 505/178 Mathlib.lean,Mathlib/Algebra/Lie/Weights/Killing.lean,Mathlib/Combinatorics/SimpleGraph/Coloring.lean,Mathlib/Combinatorics/SimpleGraph/Extremal/Basic.lean,Mathlib/Data/Nat/Basic.lean,Mathlib/Data/Set/Basic.lean,Mathlib/Order/Defs/LinearOrder.lean,Mathlib/RingTheory/AlgebraicIndependent/TranscendenceBasis.lean,Mathlib/RingTheory/HahnSeries/Lex.lean,Mathlib/RingTheory/Multiplicity.lean,Mathlib/Tactic.lean,Mathlib/Tactic/Push.lean,Mathlib/Tactic/Push/Attr.lean,Mathlib/Topology/Algebra/IsUniformGroup/Basic.lean,MathlibTest/push.lean,MathlibTest/push_neg.lean,scripts/noshake.json 17 62 ['JovanGerb', 'adomani', 'github-actions', 'grunweg', 'j-loreaux', 'leanprover-bot', 'leanprover-community-bot-assistant', 'mathlib4-merge-conflict-bot', 'plp127'] robertylewis
assignee:robertylewis
2-30190
2 days ago
2-30191
2 days ago
138-79638
138 days

All maintainer merge'd PRs

Number Author Title Description Labels +/- Modified files (first 100) 📝 💬 All users who commented or reviewed Assignee(s) Updated Last status change total time in review
25945 adomani
author:adomani
feat: the empty line in commands linter This linter flags empty lines within a command. It allows empty lines within doc-strings, module-docs and a couple of other "sensible" places. It also skips files that are likely to contain meta-code, since there the use of empty lines in definition is more widespread. This PR continues the work from #25236. large-import t-linter maintainer-merge awaiting-author 375/7 Mathlib.lean,Mathlib/Analysis/Meromorphic/FactorizedRational.lean,Mathlib/CategoryTheory/Comma/StructuredArrow/CommaMap.lean,Mathlib/Init.lean,Mathlib/RepresentationTheory/Homological/GroupHomology/LowDegree.lean,Mathlib/Tactic.lean,Mathlib/Tactic/Linter/EmptyLine.lean,MathlibTest/EmptyLine.lean 8 12 ['adomani', 'bryangingechen', 'eric-wieser', 'github-actions'] bryangingechen
assignee:bryangingechen
46-81254
1 month ago
46-81254
1 month ago
42-26074
42 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
38-69970
1 month ago
38-73255
1 month ago
53-4392
53 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 12 ['YaelDillies', 'adomani', 'euprunin', 'github-actions', 'grunweg'] joneugster
assignee:joneugster
19-71032
19 days ago
38-68719
1 month ago
39-14598
39 days
28934 yury-harmonic
author:yury-harmonic
feat(NormNum): add extensions for `Even` and `Odd` --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) maintainer-merge t-meta awaiting-author 55/0 Mathlib.lean,Mathlib/Tactic.lean,Mathlib/Tactic/NormNum/Parity.lean,scripts/noshake.json 4 10 ['JovanGerb', 'adomani', 'digama0', 'github-actions', 'mathlib4-merge-conflict-bot', 'yury-harmonic'] nobody
11-41942
11 days ago
11-59010
11 days ago
6-16639
6 days
29271 euprunin
author:euprunin
chore: remove redundant `let` and `letI` invocations --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) maintainer-merge 1/8 Mathlib/Algebra/Algebra/TransferInstance.lean,Mathlib/Algebra/Module/FinitePresentation.lean,Mathlib/CategoryTheory/Monoidal/Grp_.lean,Mathlib/ModelTheory/Algebra/Ring/FreeCommRing.lean,Mathlib/Topology/Metrizable/Uniformity.lean 5 10 ['JovanGerb', 'github-actions', 'leanprover-bot', 'leanprover-community-mathlib4-bot', 'ocfnash'] nobody
7-3079
7 days ago
7-5611
7 days ago
10-51592
10 days
29404 pechersky
author:pechersky
feat(Data/Nat): p.Coprime factorial and choose And descFactorial, for n < p --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) t-data maintainer-merge t-algebra easy
label:t-algebra$
16/0 Mathlib/Data/Nat/Choose/Dvd.lean,Mathlib/Data/Nat/Prime/Factorial.lean 2 2 ['Ruben-VandeVelde', 'github-actions'] nobody
5-54068
5 days ago
5-54068
5 days ago
5-67643
5 days
24669 qawbecrdtey
author:qawbecrdtey
feat(Analysis/Normed/Operator/LinearIsometry): added definition `LinearIsometryEquiv.prodComm` --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) This commit defines a `LinearIsometryEquiv`, and states some trivial theorems about it. ```lean def prodComm [Module R E₂] : E × E₂ ≃ₗᵢ[R] E₂ × E ``` maintainer-merge t-analysis awaiting-author 8/1 Mathlib/Analysis/Normed/Operator/LinearIsometry.lean 1 12 ['Ruben-VandeVelde', 'eric-wieser', 'faenuccio', 'github-actions', 'j-loreaux', 'jcommelin', 'qawbecrdtey'] faenuccio
assignee:faenuccio
5-41456
5 days ago
95-29288
3 months ago
32-83569
32 days
28945 harahu
author:harahu
doc: hyphenate compound adjectives ending in -dimensional Compound adjectives appearing before the noun they are modifying should be hyphenated in order to avoid ambiguity. This PR hyphenates such compound adjectives than are ending in "-dimensional". It does not cover similar compound adjectives appearing _after_ their noun, as hyphenation is then regarded as a stylistic choice, as opposed to a grammatical tool. --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) maintainer-merge 180/180 Mathlib/Algebra/Azumaya/Matrix.lean,Mathlib/Algebra/BrauerGroup/Defs.lean,Mathlib/Algebra/Category/FGModuleCat/Basic.lean,Mathlib/Algebra/Category/FGModuleCat/Limits.lean,Mathlib/Algebra/Lie/Derivation/Killing.lean,Mathlib/Algebra/Lie/Weights/RootSystem.lean,Mathlib/Algebra/Module/ZLattice/Basic.lean,Mathlib/Algebra/Module/ZLattice/Covolume.lean,Mathlib/Analysis/BoundedVariation.lean,Mathlib/Analysis/Calculus/BumpFunction/Basic.lean,Mathlib/Analysis/Calculus/BumpFunction/SmoothApprox.lean,Mathlib/Analysis/Calculus/ContDiff/FiniteDimension.lean,Mathlib/Analysis/Calculus/Deriv/AffineMap.lean,Mathlib/Analysis/Calculus/Implicit.lean,Mathlib/Analysis/Calculus/LineDeriv/QuadraticMap.lean,Mathlib/Analysis/Complex/AbsMax.lean,Mathlib/Analysis/Complex/Tietze.lean,Mathlib/Analysis/Convex/AmpleSet.lean,Mathlib/Analysis/Convex/Continuous.lean,Mathlib/Analysis/Convex/Measure.lean,Mathlib/Analysis/Convex/SimplicialComplex/Basic.lean,Mathlib/Analysis/Distribution/AEEqOfIntegralContDiff.lean,Mathlib/Analysis/FunctionalSpaces/SobolevInequality.lean,Mathlib/Analysis/InnerProductSpace/Adjoint.lean,Mathlib/Analysis/InnerProductSpace/EuclideanDist.lean,Mathlib/Analysis/InnerProductSpace/JointEigenspace.lean,Mathlib/Analysis/InnerProductSpace/PiL2.lean,Mathlib/Analysis/InnerProductSpace/Spectrum.lean,Mathlib/Analysis/Normed/Module/FiniteDimension.lean,Mathlib/Analysis/Normed/Operator/ContinuousLinearMap.lean,Mathlib/Analysis/NormedSpace/HahnBanach/Extension.lean,Mathlib/Analysis/RCLike/Lemmas.lean,Mathlib/CategoryTheory/Preadditive/Schur.lean,Mathlib/Combinatorics/Additive/AP/Three/Behrend.lean,Mathlib/FieldTheory/Differential/Liouville.lean,Mathlib/FieldTheory/IntermediateField/Algebraic.lean,Mathlib/FieldTheory/IsAlgClosed/Spectrum.lean,Mathlib/FieldTheory/PrimitiveElement.lean,Mathlib/FieldTheory/PurelyInseparable/Basic.lean,Mathlib/Geometry/Manifold/BumpFunction.lean,Mathlib/Geometry/Manifold/ChartedSpace.lean,Mathlib/Geometry/Manifold/Diffeomorph.lean,Mathlib/Geometry/Manifold/Metrizable.lean,Mathlib/Geometry/Manifold/PartitionOfUnity.lean,Mathlib/LinearAlgebra/Coevaluation.lean,Mathlib/LinearAlgebra/Complex/FiniteDimensional.lean,Mathlib/LinearAlgebra/Complex/Module.lean,Mathlib/LinearAlgebra/Dimension/Finite.lean,Mathlib/LinearAlgebra/Dimension/Finrank.lean,Mathlib/LinearAlgebra/Dimension/FreeAndStrongRankCondition.lean,Mathlib/LinearAlgebra/FiniteDimensional/Basic.lean,Mathlib/LinearAlgebra/FiniteDimensional/Defs.lean,Mathlib/LinearAlgebra/FiniteDimensional/Lemmas.lean,Mathlib/LinearAlgebra/Matrix/FiniteDimensional.lean,Mathlib/LinearAlgebra/Matrix/GeneralLinearGroup/Card.lean,Mathlib/LinearAlgebra/Multilinear/FiniteDimensional.lean,Mathlib/MeasureTheory/Integral/TorusIntegral.lean,Mathlib/MeasureTheory/Measure/Haar/InnerProductSpace.lean,Mathlib/MeasureTheory/Measure/Haar/OfBasis.lean,Mathlib/MeasureTheory/Measure/Lebesgue/EqHaar.lean,Mathlib/MeasureTheory/Measure/Lebesgue/VolumeOfBalls.lean,Mathlib/Order/RelSeries.lean,Mathlib/Probability/Process/FiniteDimensionalLaws.lean,Mathlib/RepresentationTheory/FDRep.lean,Mathlib/RepresentationTheory/Maschke.lean,Mathlib/RepresentationTheory/Tannaka.lean,Mathlib/RingTheory/Finiteness/Basic.lean,Mathlib/RingTheory/Finiteness/Lattice.lean,Mathlib/RingTheory/Grassmannian.lean,Mathlib/Tactic/FunProp/Theorems.lean,Mathlib/Topology/Algebra/InfiniteSum/Defs.lean,Mathlib/Topology/Algebra/Module/FiniteDimension.lean,Mathlib/Topology/MetricSpace/HausdorffDimension.lean,MathlibTest/fun_prop.lean,docs/overview.yaml,docs/undergrad.yaml 76 6 ['github-actions', 'mathlib4-merge-conflict-bot', 'tb65536'] tb65536
assignee:tb65536
4-60388
4 days ago
4-60407
4 days ago
17-54592
17 days
29459 bwangpj
author:bwangpj
feat: ContMDiffAt.pow Powers of `C^n` functions `M → G` into a commutative monoid `G` are `C^n`. This is upstreamed from [https://github.com/girving/ray](https://github.com/girving/ray). Co-authored-by: Geoffrey Irving --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) maintainer-merge t-differential-geometry 20/2 Mathlib/Geometry/Manifold/Algebra/Monoid.lean 1 4 ['github-actions', 'grunweg'] grunweg
assignee:grunweg
4-15492
4 days ago
4-15705
4 days ago
4-26130
4 days
29045 grunweg
author:grunweg
chore: remove the `field_simps` simp set This was used for the field_simp tactic before its recent rewrite. Its uses in mathlib were removed in #28918. --- - [x] depends on: #28918 [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) maintainer-merge 31/82 Mathlib/Algebra/CharP/MixedCharZero.lean,Mathlib/Algebra/Field/Basic.lean,Mathlib/Algebra/Group/Basic.lean,Mathlib/Algebra/Group/Defs.lean,Mathlib/Algebra/Group/Units/Basic.lean,Mathlib/Algebra/Group/Units/Defs.lean,Mathlib/Algebra/GroupWithZero/Basic.lean,Mathlib/Algebra/GroupWithZero/Units/Basic.lean,Mathlib/Algebra/NeZero.lean,Mathlib/Algebra/Order/Field/Basic.lean,Mathlib/Algebra/Ring/Basic.lean,Mathlib/Algebra/Ring/Units.lean,Mathlib/Analysis/Complex/Trigonometric.lean,Mathlib/Analysis/InnerProductSpace/Basic.lean,Mathlib/Analysis/MeanInequalitiesPow.lean,Mathlib/Analysis/Normed/Unbundled/SeminormFromBounded.lean,Mathlib/Analysis/Normed/Unbundled/SeminormFromConst.lean,Mathlib/Analysis/Normed/Unbundled/SmoothingSeminorm.lean,Mathlib/Combinatorics/SetFamily/AhlswedeZhang.lean,Mathlib/Combinatorics/SimpleGraph/Density.lean,Mathlib/MeasureTheory/Measure/Haar/Basic.lean,Mathlib/Tactic/Attr/Register.lean 22 7 ['Ruben-VandeVelde', 'bryangingechen', 'github-actions', 'grunweg', 'mathlib4-dependent-issues-bot'] nobody
2-76288
2 days ago
6-61659
6 days ago
15-60524
15 days
29511 luigi-massacci
author:luigi-massacci
feat: integrating wrt a finite measure as a continuous linear map on bounded continuous functions Add a definition `integralFiniteMeasure` of type `ContinuousLinearMap` packaging the integral of a bounded continuous function by a finite measure. --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) maintainer-merge t-measure-probability 17/0 Mathlib/MeasureTheory/Integral/BoundedContinuousFunction.lean 1 23 ['github-actions', 'grunweg', 'luigi-massacci'] nobody
2-67142
2 days ago
2-67143
2 days ago
2-69288
2 days
29498 harahu
author:harahu
doc: improve grammar and flow in documentation This PR might be deemed too stylistic in nature, but I'll propose it anyhow, with the purpose of sectioning out potential for bikeshedding from #29464. The changes are largely the work of LLM coding agents, but I have manually checked every change and have not included anything in this PR that I cannot personally stand for. In totality, my opinion is that this PR improves the legibility, clarity and conciseness of the documentation it covers, and should be merged. --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) maintainer-merge t-computability 40/39 Mathlib/Computability/AkraBazzi/AkraBazzi.lean,Mathlib/Computability/AkraBazzi/GrowsPolynomially.lean,Mathlib/Computability/AkraBazzi/SumTransform.lean 3 12 ['github-actions', 'grunweg', 'harahu', 'themathqueen'] nobody
2-65823
2 days ago
2-80752
2 days ago
3-332
3 days
29408 pechersky
author:pechersky
feat(Analysis/Normed/Ultra): nonarch norm of sum over disjoint norms achieves max --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) I thought about having a `tprod` version too, but wasn't sure the best way to phrase it maintainer-merge t-analysis 24/0 Mathlib/Analysis/Normed/Group/Ultra.lean 1 5 ['github-actions', 'loefflerd'] nobody
2-55352
2 days ago
4-84729
4 days ago
5-66072
5 days
29297 harahu
author:harahu
doc: hyphenate "first order" and "higher order" when used attributively Compound adjectives that are attributive (coming before their noun) should almost always be hyphenated in English. This PR covers "first order" and "higher order". --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) maintainer-merge 24/24 Mathlib/Analysis/Calculus/ContDiff/FTaylorSeries.lean,Mathlib/Analysis/Fourier/FourierTransformDeriv.lean,Mathlib/FieldTheory/AxGrothendieck.lean,Mathlib/Logic/Basic.lean,Mathlib/ModelTheory/Algebra/Field/Basic.lean,Mathlib/ModelTheory/Algebra/Field/CharP.lean,Mathlib/ModelTheory/Algebra/Field/IsAlgClosed.lean,Mathlib/ModelTheory/Algebra/Ring/Basic.lean,Mathlib/RingTheory/MvPolynomial/FreeCommRing.lean,Mathlib/Topology/VectorBundle/Riemannian.lean,docs/undergrad.yaml 11 3 ['github-actions', 'grunweg'] nobody
2-14817
2 days ago
2-14817
2 days ago
10-16462
10 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$
297/191 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 29 ['Ruben-VandeVelde', 'TwoFX', 'YaelDillies', 'alreadydone', 'eric-wieser', 'github-actions', 'joelriou', 'kbuzzard', 'leanprover-community-bot-assistant', 'loefflerd', 'madvorak', 'mathlib4-dependent-issues-bot', 'mathlib4-merge-conflict-bot', 'tb65536'] joelriou
assignee:joelriou
1-55661
1 day ago
10-19691
10 days ago
224-8137
224 days
28706 euprunin
author:euprunin
chore: golf entire `dite_ne_left_iff`, `exists_prime_lt_and_le_two_mul_succ`, `lt_up` and `sUnion_mem_empty_univ` using `grind` --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) maintainer-merge 4/12 Mathlib/Data/Set/Lattice.lean,Mathlib/Logic/Basic.lean,Mathlib/NumberTheory/Bertrand.lean,Mathlib/RingTheory/NoetherNormalization.lean 4 9 ['euprunin', 'github-actions', 'grunweg', 'leanprover-bot', 'leanprover-community-mathlib4-bot', 'mathlib4-merge-conflict-bot', 'tb65536'] tb65536
assignee:tb65536
1-42319
1 day ago
1-42319
1 day ago
15-19458
15 days
27964 smmercuri
author:smmercuri
refactor(AbsoluteValue): generalise equivalence to non-real valued absolute values - Abstract the definition of `AbsoluteValue.IsEquiv` to any `AbsoluteValue R S` via preservation of partial orders (previously defined only for real absolute value using the power relation `(v .)^c = w`) - Show `AbsoluteValue.IsEquiv` is equivalent to the power definition when the values are real - Two inequivalent absolute values `v` and `w` have a point `x` at which `1 < v x` and `w x < 1` --- This PR continues the work from #22100. Original PR: https://github.com/leanprover-community/mathlib4/pull/22100 maintainer-merge t-algebra t-analysis
label:t-algebra$
212/44 Mathlib/Algebra/Order/AbsoluteValue/Basic.lean,Mathlib/Analysis/AbsoluteValue/Equivalence.lean,Mathlib/NumberTheory/Ostrowski.lean 3 63 ['MichaelStollBayreuth', 'YaelDillies', 'github-actions', 'smmercuri'] YaelDillies
assignee:YaelDillies
0-78518
21 hours ago
0-83793
23 hours ago
31-28528
31 days
29436 eric-wieser
author:eric-wieser
feat: a better version of `LinearOrder.lift` This adds the following, which do not construct any new data and instead assume compatibility: * `Function.Injective.preorder` (a generalization of `PreOrder.lift`) * `Function.Injective.partialOrder` (a generalization of `PartialOrder.lift`) * `Function.Injective.linearOrder` (a generalization of `LinearOrder.liftWithOrd` and the other three variants) The following existing constructions are modified to do the same (and confusingly no longer assume injectivity): * `Function.Injective.isOrderedAddMonoid` * `Function.Injective.isOrderedRing` * `Function.Injective.isStrictOrderedRing` This fixes the instance diamond in [#mathlib4 > Instance diamond in DecidableEq Fin @ 💬](https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/Instance.20diamond.20in.20DecidableEq.20Fin/near/538119386) (which was discovered in #29418), by reusing the existing `Decidable` instance rather than constructing defeq-but-only-without-smart-unfolding instance from scratch. --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) maintainer-merge t-order 200/173 Counterexamples/MapFloor.lean,Mathlib/Algebra/Group/Subgroup/Order.lean,Mathlib/Algebra/Module/Submodule/Order.lean,Mathlib/Algebra/Order/Field/Subfield.lean,Mathlib/Algebra/Order/GroupWithZero/Canonical.lean,Mathlib/Algebra/Order/Monoid/Basic.lean,Mathlib/Algebra/Order/Monoid/Submonoid.lean,Mathlib/Algebra/Order/Monoid/Units.lean,Mathlib/Algebra/Order/Nonneg/Ring.lean,Mathlib/Algebra/Order/Ring/InjSurj.lean,Mathlib/Algebra/Ring/Subring/Order.lean,Mathlib/Algebra/Ring/Subsemiring/Order.lean,Mathlib/Analysis/Seminorm.lean,Mathlib/Order/Basic.lean,Mathlib/Order/Fin/Basic.lean,Mathlib/Order/Lattice.lean 16 15 ['YaelDillies', 'eric-wieser', 'github-actions', 'plp127'] nobody
0-69746
19 hours ago
0-69765
19 hours ago
1-51735
1 day
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
label:t-algebra$
44/0 Mathlib/LinearAlgebra/AffineSpace/Ordered.lean 1 6 ['JovanGerb', 'Ruben-VandeVelde', 'eric-wieser', 'github-actions', 'kbuzzard'] kbuzzard
assignee:kbuzzard
0-61167
16 hours ago
12-10211
12 days ago
26-27971
26 days
28612 euprunin
author:euprunin
chore(Data/List): golf entire `idxOf_append_of_mem`, `cons_sublist_cons'`, `length_eraseIdx_add_one`, `length_eraseP_add_one` and `idxOf_append_of_notMem` using `grind` --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) t-data maintainer-merge 5/26 Mathlib/Data/List/Basic.lean 1 7 ['euprunin', 'github-actions', 'grunweg', 'leanprover-bot', 'leanprover-community-mathlib4-bot'] nobody
0-17793
4 hours ago
0-17793
4 hours ago
16-76241
16 days
26783 matthewjasper
author:matthewjasper
feat(RingTheory/Flat): Add theorems relating Submodule.torsion and Module.Flat Co-authored-by: Kevin Buzzard --- This PR continues the work from #25334. [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) t-ring-theory FLT maintainer-merge new-contributor 206/0 Mathlib.lean,Mathlib/Algebra/Algebra/Bilinear.lean,Mathlib/Algebra/Module/LocalizedModule/Basic.lean,Mathlib/RingTheory/Flat/TorsionFree.lean,Mathlib/RingTheory/Ideal/IsPrincipal.lean 5 12 ['github-actions', 'kbuzzard', 'riccardobrasca'] kbuzzard
assignee:kbuzzard
0-7141
1 hour ago
0-60440
16 hours ago
57-81366
57 days
28329 pechersky
author:pechersky
feat(RingTheory/Valuation): generalize CommGroupWithZero on mrange to MonoidWithZeroHom Before, they were only for Valuation, but that is too restricted --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) maintainer-merge t-order t-algebra
label:t-algebra$
77/27 Mathlib.lean,Mathlib/Algebra/GroupWithZero/Range.lean,Mathlib/Algebra/GroupWithZero/Submonoid/Instances.lean,Mathlib/RingTheory/Valuation/Archimedean.lean,Mathlib/RingTheory/Valuation/Basic.lean 5 11 ['YaelDillies', 'eric-wieser', 'github-actions', 'pechersky', 'riccardobrasca'] YaelDillies
assignee:YaelDillies
0-875
14 minutes ago
19-27968
19 days ago
27-56322
27 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
102-37441
3 months ago
102-37442
3 months ago
10-26015
10 days
26912 pechersky
author:pechersky
chore(Algebra/Ring/Subring): simp tag `Subring.smul_def` s-multiplying by a subtype is easiest to manipulate when both terms are in the ambient type. Many places that had to use the _def lemma for a rewrite, or to include it in a simp set, no longer have to. Ported from #25308 --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) I found this being not-simp frustrating when talking about submodules over a valuation subring. maintainer-merge t-algebra merge-conflict
label:t-algebra$
68/67 Mathlib/Algebra/Algebra/Subalgebra/Basic.lean,Mathlib/Algebra/Field/Subfield/Basic.lean,Mathlib/Algebra/Group/Subgroup/Actions.lean,Mathlib/Algebra/Group/Submonoid/MulAction.lean,Mathlib/Algebra/Module/LocalizedModule/Basic.lean,Mathlib/Algebra/Module/LocalizedModule/Exact.lean,Mathlib/Algebra/Module/LocalizedModule/IsLocalization.lean,Mathlib/Algebra/Module/LocalizedModule/Submodule.lean,Mathlib/Algebra/Ring/Periodic.lean,Mathlib/Algebra/Ring/Subring/Basic.lean,Mathlib/Algebra/Ring/Subsemiring/Basic.lean,Mathlib/Analysis/CStarAlgebra/Basic.lean,Mathlib/FieldTheory/KummerExtension.lean,Mathlib/GroupTheory/GroupAction/Defs.lean,Mathlib/GroupTheory/GroupAction/MultiplePrimitivity.lean,Mathlib/GroupTheory/GroupAction/MultipleTransitivity.lean,Mathlib/GroupTheory/GroupAction/SubMulAction/OfFixingSubgroup.lean,Mathlib/GroupTheory/GroupAction/SubMulAction/OfStabilizer.lean,Mathlib/LinearAlgebra/RootSystem/Irreducible.lean,Mathlib/LinearAlgebra/RootSystem/RootPositive.lean,Mathlib/LinearAlgebra/RootSystem/WeylGroup.lean,Mathlib/RingTheory/Etale/Kaehler.lean,Mathlib/RingTheory/LocalProperties/Projective.lean,Mathlib/RingTheory/Localization/InvSubmonoid.lean,Mathlib/RingTheory/OreLocalization/Basic.lean 25 19 ['artie2000', 'eric-wieser', 'github-actions', 'j-loreaux', 'linesthatinterlace', 'mathlib4-merge-conflict-bot', 'pechersky'] joelriou
assignee:joelriou
11-85332
11 days ago
11-85333
11 days ago
51-74059
51 days
28737 astrainfinita
author:astrainfinita
refactor: deprecate `MulEquivClass` This PR continues the work from #18806. Original PR: https://github.com/leanprover-community/mathlib4/pull/18806 maintainer-merge t-algebra merge-conflict awaiting-author
label:t-algebra$
67/77 Mathlib/Algebra/BigOperators/Finprod.lean,Mathlib/Algebra/Group/Equiv/Basic.lean,Mathlib/Algebra/Group/Equiv/Defs.lean,Mathlib/Algebra/Group/Irreducible/Lemmas.lean,Mathlib/Algebra/Group/Subgroup/Map.lean,Mathlib/Algebra/Group/Submonoid/Operations.lean,Mathlib/Algebra/Group/Units/Equiv.lean,Mathlib/Algebra/GroupWithZero/Equiv.lean,Mathlib/Algebra/GroupWithZero/NonZeroDivisors.lean,Mathlib/Algebra/Module/Equiv/Defs.lean,Mathlib/Algebra/Order/CauSeq/Basic.lean,Mathlib/Algebra/Order/Hom/Monoid.lean,Mathlib/Algebra/Prime/Lemmas.lean,Mathlib/Algebra/Ring/Divisibility/Basic.lean,Mathlib/Algebra/Ring/Equiv.lean,Mathlib/Algebra/Star/MonoidHom.lean,Mathlib/Combinatorics/Additive/FreimanHom.lean,Mathlib/GroupTheory/GroupExtension/Defs.lean,Mathlib/GroupTheory/Submonoid/Center.lean,Mathlib/LinearAlgebra/FreeModule/Finite/CardQuotient.lean,Mathlib/RingTheory/Bialgebra/Equiv.lean,Mathlib/RingTheory/Ideal/Norm/AbsNorm.lean,Mathlib/RingTheory/Multiplicity.lean,Mathlib/RingTheory/UniqueFactorizationDomain/NormalizedFactors.lean,Mathlib/Topology/Algebra/ContinuousMonoidHom.lean,Mathlib/Topology/Algebra/InfiniteSum/Basic.lean 26 20 ['Vierkantor', 'alreadydone', 'astrainfinita', 'github-actions', 'grunweg', 'leanprover-bot', 'leanprover-community-mathlib4-bot', 'mathlib4-merge-conflict-bot'] Vierkantor
assignee:Vierkantor
3-2792
3 days ago
3-2793
3 days ago
4-17723
4 days
21965 JovanGerb
author:JovanGerb
feat: extensible `push` and `pull` tactics This PR defines the `push` and `pull` tactics, and makes `push_neg` a macro for `push Not`. The tactics are also available in `conv` mode. For tagging, there is only the `@[push]` attribute, which adds the reverse rewrite for the `pull` tactic when relevant. In the future, we may also need a separate `@[pull X]` attribute for pulling `X`. Thanks to this change, we will be able to make `push_neg` into a more powerful tactic by tagging more lemmas. It also means that about 60 files now don't need to import `LinearOrder`/`PartialOrder`. This will be especially useful when we get the `@[to_dual]` attribute. This work originally started in #21769. There is now the follow up PR #29000 which adds `push` tags and tests for them. The `@[push]` attribute is defined in `Mathlib.Tactic.Push.Attr` and the main implementation of `push` and `pull` is in `Mathlib.Tactic.Push`. Some proofs need to be fixed because the new simp-based `push_neg` can see through more reducible definitions. Zulip conversation: [#mathlib4 > I made an extensible `push` tactic generalizing `push_neg`](https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/I.20made.20an.20extensible.20.60push.60.20tactic.20generalizing.20.60push_neg.60) closes #21841 --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) maintainer-merge t-meta merge-conflict 505/178 Mathlib.lean,Mathlib/Algebra/Lie/Weights/Killing.lean,Mathlib/Combinatorics/SimpleGraph/Coloring.lean,Mathlib/Combinatorics/SimpleGraph/Extremal/Basic.lean,Mathlib/Data/Nat/Basic.lean,Mathlib/Data/Set/Basic.lean,Mathlib/Order/Defs/LinearOrder.lean,Mathlib/RingTheory/AlgebraicIndependent/TranscendenceBasis.lean,Mathlib/RingTheory/HahnSeries/Lex.lean,Mathlib/RingTheory/Multiplicity.lean,Mathlib/Tactic.lean,Mathlib/Tactic/Push.lean,Mathlib/Tactic/Push/Attr.lean,Mathlib/Topology/Algebra/IsUniformGroup/Basic.lean,MathlibTest/push.lean,MathlibTest/push_neg.lean,scripts/noshake.json 17 62 ['JovanGerb', 'adomani', 'github-actions', 'grunweg', 'j-loreaux', 'leanprover-bot', 'leanprover-community-bot-assistant', 'mathlib4-merge-conflict-bot', 'plp127'] robertylewis
assignee:robertylewis
2-30190
2 days ago
2-30191
2 days ago
138-79638
138 days

PRs blocked on a zulip discussion

Number Author Title Description Labels +/- Modified files (first 100) 📝 💬 All users who commented or reviewed Assignee(s) Updated Last status change total time in review
15649 TpmKranz
author:TpmKranz
feat(Computability): introduce Generalised NFA as bridge to Regular Expression Lays the groundwork for a proof of equivalence of NFA and RE, w.r.t. described language. Actual connection to NFA comes later, after the groundwork for the opposite direction has been laid. Second chunk of #12648 --- - [x] depends on: #15647 [Data.FinEnum.Option unchanged since then] [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) awaiting-zulip t-computability new-contributor awaiting-author 298/0 Mathlib.lean,Mathlib/Computability/GNFA.lean,Mathlib/Computability/Language.lean,Mathlib/Computability/RegularExpressions.lean,docs/references.bib 5 6 ['github-actions', 'mathlib4-dependent-issues-bot', 'meithecatte', 'trivial1711'] nobody
130-52580
4 months ago
130-52589
4 months ago
23-54870
23 days
20648 anthonyde
author:anthonyde
feat: formalize regular expression -> εNFA The file `Computability/RegularExpressionsToEpsilonNFA.lean` contains a formal definition of Thompson's method for constructing an `εNFA` from a `RegularExpression` and a proof of its correctness. --- - [x] depends on: #20644 - [x] depends on: #20645 [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) awaiting-zulip t-computability new-contributor 490/0 Mathlib.lean,Mathlib/Computability/RegularExpressionsToEpsilonNFA.lean,docs/references.bib 3 5 ['github-actions', 'mathlib4-dependent-issues-bot', 'meithecatte', 'qawbecrdtey'] nobody
130-51891
4 months ago
130-52526
4 months ago
75-77754
75 days
20238 maemre
author:maemre
feat(Computability/DFA): Closure of regular languages under some set operations This shows that regular languages are closed under complement and intersection by constructing DFAs for them. --- Closure under all other operations will be proved when someone adds the proof for DFA<->regular expression equivalence, so they are not part of this PR. [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) awaiting-zulip t-computability new-contributor awaiting-author 159/0 Mathlib/Computability/DFA.lean,Mathlib/Computability/Language.lean 2 59 ['EtienneC30', 'YaelDillies', 'github-actions', 'maemre', 'meithecatte', 'urkud'] EtienneC30
assignee:EtienneC30
101-18351
3 months ago
130-52490
4 months ago
48-67492
48 days
23929 meithecatte
author:meithecatte
feat(Computability/NFA): improve bound on pumping lemma --- - [x] depends on: #25321 [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) awaiting-zulip t-computability new-contributor 101/10 Mathlib/Computability/EpsilonNFA.lean,Mathlib/Computability/NFA.lean 2 41 ['YaelDillies', 'github-actions', 'leanprover-community-bot-assistant', 'mathlib4-dependent-issues-bot', 'meithecatte'] nobody
97-62142
3 months ago
97-62143
3 months ago
34-10595
34 days
28925 grunweg
author:grunweg
chore: remove `linear_combination'` tactic When `linear_combination` was refactored in #15899, the old code was kept as the `linear_combination'` tactic, for easier migration. The consensus of the zulip discussion ([#mathlib4 > Narrowing the scope of `linear_combination` @ 💬](https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/Narrowing.20the.20scope.20of.20.60linear_combination.60/near/470237816)) was to wait, and "revisit this once people have experienced the various tactics in practice". One year later, the old tactic has almost no uses: it is unused in mathlib; [searching on github](https://github.com/search?q=linear_combination%27%20path%3A*.lean&type=code) yields 37 hits --- all of which are in various forks of mathlib. Thus, removing this tactic seems appropriate. --- Do not merge before the zulip discussion has concluded! [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) file-removed awaiting-zulip 0/564 Mathlib.lean,Mathlib/Tactic.lean,Mathlib/Tactic/LinearCombination'.lean,Mathlib/Tactic/Linter/UnusedTactic.lean,MathlibTest/linear_combination'.lean 5 3 ['euprunin', 'github-actions', 'grunweg'] nobody
17-72576
17 days ago
18-56309
18 days ago
0-1
1 second
29072 yury-harmonic
author:yury-harmonic
feat({Nat,Int}/ModEq): add lemmas --- I'm not sure that I named these lemmas correctly. Suggestions about better names are welcome! [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) t-data awaiting-zulip 171/15 Mathlib/Data/Int/ModEq.lean,Mathlib/Data/Nat/ModEq.lean 2 5 ['eric-wieser', 'github-actions', 'yury-harmonic'] nobody
15-19624
15 days ago
15-19624
15 days ago
0-55232
15 hours
25905 mans0954
author:mans0954
feat(RingTheory/Polynomial/SmallDegreeVieta): polynomial versions of results in Algebra.QuadraticDiscriminant This PR continues the work from #25605. Original PR: https://github.com/leanprover-community/mathlib4/pull/25605 t-ring-theory awaiting-zulip 76/8 Mathlib/Algebra/Polynomial/Coeff.lean,Mathlib/RingTheory/Polynomial/SmallDegreeVieta.lean 2 44 ['chrisflav', 'github-actions', 'kckennylau', 'mans0954', 'ocfnash'] chrisflav
assignee:chrisflav
6-78700
6 days ago
6-78700
6 days ago
82-34290
82 days
29548 Parcly-Taxel
author:Parcly-Taxel
feat: add `induction'` to the deprecated syntax linter Exactly like `cases'`. --- * [x] depends on: #29542 awaiting-zulip tech debt t-linter 41/2 Mathlib/Init.lean,Mathlib/Tactic/Linter/DeprecatedSyntaxLinter.lean,MathlibTest/DeprecatedSyntaxLinter.lean 3 3 ['Parcly-Taxel', 'github-actions', 'grunweg'] grunweg
assignee:grunweg
1-14155
1 day ago
1-14155
1 day ago
0-83159
23 hours
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
362-29613
11 months ago
362-51588
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
297-2863
9 months ago
297-2863
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
141-44640
4 months ago
152-73270
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
116-75146
3 months ago
116-75147
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
116-74220
3 months ago
116-74222
3 months ago
39-67601
39 days
17458 urkud
author:urkud
refactor(Algebra/Group): make `IsUnit` a typeclass Also change some lemmas to assume `[IsUnit _]` instead of `[Invertible _]`. Motivated by potential non-defeq diamonds in #14986, see also [Zulip](https://leanprover.zulipchat.com/#narrow/stream/116395-maths/topic/Invertible.20and.20data) I no longer plan to merge this PR, but I'm going to cherry-pick some changes to a new PR before closing this one. --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) awaiting-zulip t-algebra merge-conflict
label:t-algebra$
82/72 Mathlib/Algebra/CharP/Invertible.lean,Mathlib/Algebra/Group/Invertible/Basic.lean,Mathlib/Algebra/Group/Units/Defs.lean,Mathlib/Algebra/GroupWithZero/Invertible.lean,Mathlib/Algebra/GroupWithZero/Units/Basic.lean,Mathlib/Algebra/Polynomial/Degree/Units.lean,Mathlib/Algebra/Polynomial/Splits.lean,Mathlib/Analysis/Convex/Segment.lean,Mathlib/Analysis/Normed/Affine/Isometry.lean,Mathlib/Analysis/Normed/Ring/Units.lean,Mathlib/CategoryTheory/Linear/Basic.lean,Mathlib/FieldTheory/Finite/Basic.lean,Mathlib/FieldTheory/Separable.lean,Mathlib/FieldTheory/SeparableDegree.lean,Mathlib/GroupTheory/Submonoid/Inverses.lean,Mathlib/LinearAlgebra/AffineSpace/AffineEquiv.lean,Mathlib/LinearAlgebra/AffineSpace/Combination.lean,Mathlib/LinearAlgebra/CliffordAlgebra/Contraction.lean,Mathlib/LinearAlgebra/CliffordAlgebra/Inversion.lean,Mathlib/LinearAlgebra/CliffordAlgebra/SpinGroup.lean,Mathlib/LinearAlgebra/Eigenspace/Minpoly.lean,Mathlib/NumberTheory/MulChar/Basic.lean,Mathlib/RingTheory/Localization/NumDen.lean,Mathlib/RingTheory/Polynomial/Content.lean,Mathlib/RingTheory/Polynomial/GaussLemma.lean,Mathlib/RingTheory/Valuation/Basic.lean 26 12 ['MichaelStollBayreuth', 'acmepjz', 'eric-wieser', 'github-actions', 'leanprover-bot', 'leanprover-community-bot-assistant', 'urkud'] nobody
70-32889
2 months ago
70-32889
2 months ago
0-66650
18 hours
25218 kckennylau
author:kckennylau
feat(AlgebraicGeometry): Tate normal form of elliptic curves --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) awaiting-zulip new-contributor t-algebraic-geometry merge-conflict 291/26 Mathlib.lean,Mathlib/AlgebraicGeometry/EllipticCurve/IsomOfJ.lean,Mathlib/AlgebraicGeometry/EllipticCurve/Modular/TateNormalForm.lean,Mathlib/AlgebraicGeometry/EllipticCurve/NormalForms.lean,Mathlib/AlgebraicGeometry/EllipticCurve/VariableChange.lean 5 31 ['MichaelStollBayreuth', 'Multramate', 'acmepjz', 'github-actions', 'grunweg', 'kckennylau', 'leanprover-community-bot-assistant'] nobody
70-31727
2 months ago
70-31728
2 months ago
6-51040
6 days
28298 thorimur
author:thorimur
chore: dedent `to_additive` docstrings This PR uses automation to dedent `to_additive` docstrings throughout Mathlib. It does not lint against indentation or in any way enforce indentation standards for future docstrings. The convention was chosen in accordance with the discussion and polls at [this Zulip thread](https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/Poll.3A.20Indentation.20style.20for.20.60to_additive.60.20docstrings/with/534285603). --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) awaiting-zulip merge-conflict documentation 949/949 Mathlib/Algebra/BigOperators/Fin.lean,Mathlib/Algebra/BigOperators/Finprod.lean,Mathlib/Algebra/BigOperators/Finsupp/Basic.lean,Mathlib/Algebra/BigOperators/Group/Finset/Lemmas.lean,Mathlib/Algebra/BigOperators/Group/List/Basic.lean,Mathlib/Algebra/BigOperators/Group/Multiset/Defs.lean,Mathlib/Algebra/BigOperators/Pi.lean,Mathlib/Algebra/Category/Grp/Basic.lean,Mathlib/Algebra/Category/Grp/FilteredColimits.lean,Mathlib/Algebra/Category/Grp/Limits.lean,Mathlib/Algebra/Category/Grp/Ulift.lean,Mathlib/Algebra/Category/MonCat/Basic.lean,Mathlib/Algebra/Category/MonCat/FilteredColimits.lean,Mathlib/Algebra/Category/MonCat/Limits.lean,Mathlib/Algebra/Category/Semigrp/Basic.lean,Mathlib/Algebra/Free.lean,Mathlib/Algebra/FreeMonoid/Basic.lean,Mathlib/Algebra/Group/Action/Defs.lean,Mathlib/Algebra/Group/Action/Pi.lean,Mathlib/Algebra/Group/Action/Pointwise/Finset.lean,Mathlib/Algebra/Group/Basic.lean,Mathlib/Algebra/Group/Defs.lean,Mathlib/Algebra/Group/Embedding.lean,Mathlib/Algebra/Group/Equiv/Basic.lean,Mathlib/Algebra/Group/Equiv/Defs.lean,Mathlib/Algebra/Group/Equiv/Opposite.lean,Mathlib/Algebra/Group/Even.lean,Mathlib/Algebra/Group/Hom/Basic.lean,Mathlib/Algebra/Group/Hom/Defs.lean,Mathlib/Algebra/Group/Hom/Instances.lean,Mathlib/Algebra/Group/Indicator.lean,Mathlib/Algebra/Group/Pi/Lemmas.lean,Mathlib/Algebra/Group/Pi/Units.lean,Mathlib/Algebra/Group/Pointwise/Finset/Basic.lean,Mathlib/Algebra/Group/Pointwise/Set/Basic.lean,Mathlib/Algebra/Group/Prod.lean,Mathlib/Algebra/Group/Subgroup/Basic.lean,Mathlib/Algebra/Group/Subgroup/Defs.lean,Mathlib/Algebra/Group/Subgroup/Ker.lean,Mathlib/Algebra/Group/Subgroup/Lattice.lean,Mathlib/Algebra/Group/Subgroup/Map.lean,Mathlib/Algebra/Group/Subgroup/Pointwise.lean,Mathlib/Algebra/Group/Submonoid/Basic.lean,Mathlib/Algebra/Group/Submonoid/BigOperators.lean,Mathlib/Algebra/Group/Submonoid/Defs.lean,Mathlib/Algebra/Group/Submonoid/Membership.lean,Mathlib/Algebra/Group/Submonoid/MulAction.lean,Mathlib/Algebra/Group/Submonoid/Operations.lean,Mathlib/Algebra/Group/Subsemigroup/Basic.lean,Mathlib/Algebra/Group/Subsemigroup/Operations.lean,Mathlib/Algebra/Group/UniqueProds/Basic.lean,Mathlib/Algebra/Group/Units/Defs.lean,Mathlib/Algebra/Group/Units/Equiv.lean,Mathlib/Algebra/Group/Units/Hom.lean,Mathlib/Algebra/Group/Units/Opposite.lean,Mathlib/Algebra/Notation/Pi/Basic.lean,Mathlib/Algebra/Opposites.lean,Mathlib/Algebra/Order/BigOperators/Group/List.lean,Mathlib/Algebra/Order/Group/Abs.lean,Mathlib/Algebra/Order/Group/Basic.lean,Mathlib/Algebra/Order/Group/Cone.lean,Mathlib/Algebra/Order/Group/OrderIso.lean,Mathlib/Algebra/Order/Group/Units.lean,Mathlib/Algebra/Order/Hom/Monoid.lean,Mathlib/Algebra/Order/Monoid/Basic.lean,Mathlib/Algebra/Order/Monoid/Canonical/Defs.lean,Mathlib/Algebra/Order/Monoid/Submonoid.lean,Mathlib/Algebra/Order/Monoid/Unbundled/Basic.lean,Mathlib/Algebra/Order/Monoid/Unbundled/WithTop.lean,Mathlib/Algebra/Order/Monoid/Units.lean,Mathlib/Algebra/Order/Pi.lean,Mathlib/Algebra/Regular/Defs.lean,Mathlib/Analysis/Normed/Group/Basic.lean,Mathlib/CategoryTheory/Monoidal/Discrete.lean,Mathlib/Data/Finset/NoncommProd.lean,Mathlib/Data/Fintype/BigOperators.lean,Mathlib/Data/Set/MulAntidiagonal.lean,Mathlib/Data/Set/SMulAntidiagonal.lean,Mathlib/Data/Vector/Basic.lean,Mathlib/Dynamics/Ergodic/Action/OfMinimal.lean,Mathlib/Dynamics/FixedPoints/Prufer.lean,Mathlib/Geometry/Manifold/Algebra/SmoothFunctions.lean,Mathlib/GroupTheory/Complement.lean,Mathlib/GroupTheory/Congruence/Basic.lean,Mathlib/GroupTheory/Congruence/Defs.lean,Mathlib/GroupTheory/Coprod/Basic.lean,Mathlib/GroupTheory/Coset/Basic.lean,Mathlib/GroupTheory/Divisible.lean,Mathlib/GroupTheory/EckmannHilton.lean,Mathlib/GroupTheory/FreeGroup/Basic.lean,Mathlib/GroupTheory/FreeGroup/Reduce.lean,Mathlib/GroupTheory/GroupAction/Basic.lean,Mathlib/GroupTheory/GroupAction/Blocks.lean,Mathlib/GroupTheory/GroupAction/Defs.lean,Mathlib/GroupTheory/GroupAction/FixedPoints.lean,Mathlib/GroupTheory/GroupAction/Hom.lean,Mathlib/GroupTheory/GroupAction/MultipleTransitivity.lean,Mathlib/GroupTheory/GroupAction/Primitive.lean,Mathlib/GroupTheory/GroupAction/Quotient.lean,Mathlib/GroupTheory/GroupAction/SubMulAction.lean 141 10 ['eric-wieser', 'github-actions', 'grunweg', 'mathlib4-merge-conflict-bot', 'thorimur'] nobody
29-60221
29 days ago
30-47593
30 days ago
0-61617
17 hours
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 merge-conflict 21/26 Mathlib/AlgebraicTopology/FundamentalGroupoid/Basic.lean,Mathlib/Data/Nat/Cast/Defs.lean,Mathlib/Data/Nat/Cast/Order/Basic.lean 3 4 ['eric-wieser', 'github-actions', 'mathlib4-merge-conflict-bot', 'urkud'] nobody
22-19415
22 days ago
22-19416
22 days ago
0-23929
6 hours
29002 grunweg
author:grunweg
chore: move Data/Real/Irrational to RingTheory It certainly has nothing to do with data (structure). --- I'm less sure where to put it instead. [zulip discussion](https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/Cleaning.20up.20.60Data.60/with/536301893) suggested this place; in the future, this could also be split. [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) file-removed awaiting-zulip merge-conflict 10/10 Counterexamples/IrrationalPowerOfIrrational.lean,Mathlib.lean,Mathlib/Analysis/Real/Pi/Irrational.lean,Mathlib/Data/Real/GoldenRatio.lean,Mathlib/NumberTheory/DiophantineApproximation/Basic.lean,Mathlib/NumberTheory/Rayleigh.lean,Mathlib/NumberTheory/Transcendental/Liouville/Basic.lean,Mathlib/RingTheory/Real/Irrational.lean,Mathlib/Tactic/NormNum/Irrational.lean,Mathlib/Topology/Instances/AddCircle/DenseSubgroup.lean,Mathlib/Topology/Instances/Irrational.lean 11 2 ['github-actions', 'mathlib4-merge-conflict-bot'] nobody
15-53888
15 days ago
15-53889
15 days ago
0-67
1 minute
28803 astrainfinita
author:astrainfinita
refactor: unbundle algebra from `ENormed*` Further speed up the search in the algebraic typeclass hierarchy by avoiding searching for `TopologicalSpace`. This PR continues the work from #23961. - Change `ESeminormed(Add)Monoid` and `ENormed(Add)Monoid` so they no longer carry algebraic data. - Deprecate `ESeminormed(Add)CommMonoid` and `ENormed(Add)CommMonoid` in favor of `ESeminormed(Add)Monoid` and `ENormed(Add)Monoid` with a commutative algebraic typeclass. |Old|New| |---|---| | `[ESeminormed(Add)(Comm)Monoid E]` | `[(Add)(Comm)Monoid E] [ESeminormed(Add)Monoid E]` | | `[ENormed(Add)(Comm)Monoid]` | `[(Add)(Comm)Monoid E] [ENormed(Add)Monoid]` | See [Zulip discussion](https://leanprover.zulipchat.com/#narrow/channel/144837-PR-reviews/topic/.2328803.20refactor.3A.20unbundle.20algebra.20from.20.60ENormed*.60/with/536024350) ------------ - [x] depends on: #28813 awaiting-zulip slow-typeclass-synthesis t-algebra t-analysis merge-conflict
label:t-algebra$
80/63 Mathlib/Analysis/CStarAlgebra/CStarMatrix.lean,Mathlib/Analysis/Normed/Group/Basic.lean,Mathlib/Analysis/Normed/Group/Continuity.lean,Mathlib/Analysis/Normed/Group/InfiniteSum.lean,Mathlib/Analysis/NormedSpace/IndicatorFunction.lean,Mathlib/MeasureTheory/Function/L1Space/AEEqFun.lean,Mathlib/MeasureTheory/Function/L1Space/HasFiniteIntegral.lean,Mathlib/MeasureTheory/Function/L1Space/Integrable.lean,Mathlib/MeasureTheory/Function/LocallyIntegrable.lean,Mathlib/MeasureTheory/Function/LpSeminorm/Basic.lean,Mathlib/MeasureTheory/Function/LpSeminorm/CompareExp.lean,Mathlib/MeasureTheory/Function/LpSeminorm/TriangleInequality.lean,Mathlib/MeasureTheory/Integral/IntegrableOn.lean,Mathlib/MeasureTheory/Integral/IntervalIntegral/Basic.lean 14 28 ['astrainfinita', 'bryangingechen', 'github-actions', 'grunweg', 'kbuzzard', 'leanprover-bot', 'leanprover-community-mathlib4-bot', 'mathlib-bors', 'mathlib4-dependent-issues-bot', 'mathlib4-merge-conflict-bot', 'sgouezel'] grunweg
assignee:grunweg
10-47372
10 days ago
10-47373
10 days ago
0-20585
5 hours
17518 grunweg
author:grunweg
feat: lint on declarations mentioning `Invertible` or `Unique` Using the same infrastructure as for #10235. Depends on that PR to land first, and also (for the first lint) a zulip discussion if that change is desired/about the best way to enact it. --- - [ ] depends on: #10235 awaiting-zulip t-linter merge-conflict blocked-by-other-PR 149/7 Mathlib.lean,Mathlib/Algebra/MvPolynomial/PDeriv.lean,Mathlib/Computability/Halting.lean,Mathlib/Computability/TuringMachine.lean,Mathlib/Data/Fintype/Card.lean,Mathlib/GroupTheory/Perm/DomMulAct.lean,Mathlib/Logic/Basic.lean,Mathlib/Logic/Encodable/Basic.lean,Mathlib/NumberTheory/JacobiSum/Basic.lean,Mathlib/Order/Heyting/Regular.lean,Mathlib/RingTheory/MvPolynomial/Symmetric/FundamentalTheorem.lean,Mathlib/Tactic.lean,Mathlib/Tactic/Linter/UnusedAssumptionInType.lean 13 3 ['github-actions', 'mathlib4-dependent-issues-bot', 'mergify'] nobody
314-69732
10 months ago
340-58254
11 months ago*
0-0
0 seconds*
15654 TpmKranz
author:TpmKranz
feat(Computability): language-preserving maps between NFA and RE Map REs to NFAs via Thompson's construction and NFAs to REs using GNFAs Last chunk of #12648 --- - [ ] depends on: #15651 - [ ] depends on: #15649 [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) awaiting-zulip t-computability new-contributor merge-conflict blocked-by-other-PR 985/2 Mathlib.lean,Mathlib/Computability/GNFA.lean,Mathlib/Computability/Language.lean,Mathlib/Computability/NFA.lean,Mathlib/Computability/RegularExpressions.lean,Mathlib/Data/FinEnum/Option.lean,docs/references.bib 7 3 ['github-actions', 'leanprover-community-mathlib4-bot', 'meithecatte'] nobody
130-52540
4 months ago
130-52545
4 months ago
0-179
2 minutes

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

Number Author Title Description Labels +/- Modified files (first 100) 📝 💬 All users who commented or reviewed Assignee(s) Updated Last status change total time in review
29448 j-loreaux
author:j-loreaux
chore(Analysis/{NormedSpace/ConformalLinearMap → Normed/Operator/Conformal}): move file This is part of #28698 to migrate the material in `Analysis/NormedSpace/` to other locations. --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) file-removed tech debt t-analysis 3/3 Mathlib.lean,Mathlib/Analysis/Calculus/Conformal/NormedSpace.lean,Mathlib/Analysis/InnerProductSpace/ConformalLinearMap.lean,Mathlib/Analysis/Normed/Operator/Conformal.lean 4 1 ['github-actions'] nobody
4-54489
4 days ago
4-54489
4 days ago
4-54533
4 days
29383 Vierkantor
author:Vierkantor
chore(Topology): process porting notes Go through the porting notes in the Topology folder and solve the ones with an obvious fix. This last batch of porting notes should bring us below 500 open porting notes in Mathlib, when the RingTheory ones get merged too! --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) tech debt t-topology 134/222 Mathlib/Topology/Algebra/Module/CharacterSpace.lean,Mathlib/Topology/Algebra/Monoid.lean,Mathlib/Topology/Algebra/MulAction.lean,Mathlib/Topology/Algebra/Ring/Ideal.lean,Mathlib/Topology/Bases.lean,Mathlib/Topology/Bornology/Basic.lean,Mathlib/Topology/Bornology/Constructions.lean,Mathlib/Topology/Category/Profinite/CofilteredLimit.lean,Mathlib/Topology/Category/TopCat/Limits/Basic.lean,Mathlib/Topology/Category/TopCat/Limits/Cofiltered.lean,Mathlib/Topology/Compactness/Compact.lean,Mathlib/Topology/Constructions/SumProd.lean,Mathlib/Topology/ContinuousMap/Periodic.lean,Mathlib/Topology/ContinuousMap/ZeroAtInfty.lean,Mathlib/Topology/DiscreteQuotient.lean,Mathlib/Topology/Gluing.lean,Mathlib/Topology/Homotopy/Basic.lean,Mathlib/Topology/Homotopy/Equiv.lean,Mathlib/Topology/Homotopy/HomotopyGroup.lean,Mathlib/Topology/LocallyConstant/Basic.lean,Mathlib/Topology/MetricSpace/Algebra.lean,Mathlib/Topology/MetricSpace/Equicontinuity.lean,Mathlib/Topology/MetricSpace/GromovHausdorff.lean,Mathlib/Topology/MetricSpace/IsometricSMul.lean,Mathlib/Topology/Order.lean,Mathlib/Topology/Order/Compact.lean,Mathlib/Topology/Separation/Basic.lean,Mathlib/Topology/Sheaves/CommRingCat.lean,Mathlib/Topology/Sheaves/SheafCondition/EqualizerProducts.lean,Mathlib/Topology/Sheaves/Sheafify.lean,Mathlib/Topology/Sheaves/Stalks.lean,Mathlib/Topology/UniformSpace/Cauchy.lean,Mathlib/Topology/UniformSpace/UniformConvergenceTopology.lean 33 1 ['github-actions'] nobody
3-74722
3 days ago
6-80193
6 days ago
6-80175
6 days