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.

stale PRs ready-to-merge
stale PRs labelled "maintainer merge"
all PRs labelled 'maintainer merge'
all PRs waiting on finding consensus on zulip
just the PRs addressing technical debt

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 10:48 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-45523 1 day ago	1-47504 1 day ago	38-25023 38 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-73110 1 month ago	46-73110 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-61826 1 month ago	38-65111 1 month ago	52-82649 52 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-62888 19 days ago	38-60575 1 month ago	39-6454 39 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	10	['YaelDillies', 'eric-wieser', 'github-actions', 'pechersky']	YaelDillies assignee:YaelDillies	19-2117 19 days ago	19-19824 19 days ago	27-48179 27 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-33798 11 days ago	11-50866 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	6-81335 6 days ago	6-83867 6 days ago	10-43448 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-45924 5 days ago	5-45924 5 days ago	5-59499 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-33312 5 days ago	95-21144 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-52244 4 days ago	4-52263 4 days ago	17-46448 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-7348 4 days ago	4-7561 4 days ago	4-17986 4 days
29219	euprunin author:euprunin	chore: remove redundant `obtain` invocations	--- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/)	maintainer-merge t-algebra label:t-algebra$	0/10	Mathlib/Algebra/ContinuedFractions/ConvergentsEquiv.lean,Mathlib/Algebra/Homology/HomotopyCategory/Pretriangulated.lean,Mathlib/Algebra/Lie/Weights/Cartan.lean,Mathlib/Algebra/Module/PID.lean,Mathlib/Algebra/Order/Ring/Unbundled/Basic.lean,Mathlib/Algebra/Polynomial/Monic.lean	6	6	['github-actions', 'grunweg', 'leanprover-bot', 'leanprover-community-mathlib4-bot']	nobody	2-78364 2 days ago	2-78364 2 days ago	11-56701 11 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-68144 2 days ago	6-53515 6 days ago	15-52380 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-58998 2 days ago	2-58999 2 days ago	2-61144 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-57679 2 days ago	2-72608 2 days ago	2-78588 2 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-47208 2 days ago	4-76585 4 days ago	5-57928 5 days
28614	kckennylau author:kckennylau	feat(CategoryTheory): The finite pretopology on a category	We define `CategoryTheory.Pretopology.finite`, the finite pretopology on a category, which consists of presieves that contain only finitely many arrows. --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/)	maintainer-merge t-category-theory	131/0	Mathlib.lean,Mathlib/CategoryTheory/Sites/Finite.lean,Mathlib/CategoryTheory/Sites/Sieves.lean	3	31	['chrisflav', 'github-actions', 'joelriou', 'kckennylau']	chrisflav assignee:chrisflav	2-39528 2 days ago	2-49591 2 days ago	10-84236 10 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-6673 2 days ago	2-6673 2 days ago	10-8318 10 days
29536	kim-em author:kim-em	chore: minor grind golfing in Logic/Embedding	--- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/)	maintainer-merge t-logic	18/14	Mathlib/Logic/Embedding/Basic.lean,Mathlib/Logic/Embedding/Set.lean	2	2	['euprunin', 'github-actions', 'grunweg']	nobody	1-70245 1 day ago	2-6030 2 days ago	2-25733 2 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-47517 1 day ago	10-11547 10 days ago	223-86394 223 days
29493	kim-em author:kim-em	chore: grind golf in Mathlib.Logic	More golfs identified by `linter.tacticAnalysis.terminalToGrind`.	maintainer-merge t-logic	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	1-39532 1 day ago	3-6845 3 days ago	3-15656 3 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-34175 1 day ago	1-34175 1 day ago	15-11315 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-29297 3 months ago	102-29298 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-77188 11 days ago	11-77189 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	2-81048 2 days ago	2-81049 2 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-22046 2 days ago	2-22047 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-73110 1 month ago	46-73110 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-61826 1 month ago	38-65111 1 month ago	52-82649 52 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-62888 19 days ago	38-60575 1 month ago	39-6454 39 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	10	['YaelDillies', 'eric-wieser', 'github-actions', 'pechersky']	YaelDillies assignee:YaelDillies	19-2117 19 days ago	19-19824 19 days ago	27-48179 27 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-33798 11 days ago	11-50866 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	6-81335 6 days ago	6-83867 6 days ago	10-43448 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-45924 5 days ago	5-45924 5 days ago	5-59499 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-33312 5 days ago	95-21144 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-52244 4 days ago	4-52263 4 days ago	17-46448 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-7348 4 days ago	4-7561 4 days ago	4-17986 4 days
29219	euprunin author:euprunin	chore: remove redundant `obtain` invocations	--- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/)	maintainer-merge t-algebra label:t-algebra$	0/10	Mathlib/Algebra/ContinuedFractions/ConvergentsEquiv.lean,Mathlib/Algebra/Homology/HomotopyCategory/Pretriangulated.lean,Mathlib/Algebra/Lie/Weights/Cartan.lean,Mathlib/Algebra/Module/PID.lean,Mathlib/Algebra/Order/Ring/Unbundled/Basic.lean,Mathlib/Algebra/Polynomial/Monic.lean	6	6	['github-actions', 'grunweg', 'leanprover-bot', 'leanprover-community-mathlib4-bot']	nobody	2-78364 2 days ago	2-78364 2 days ago	11-56701 11 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-68144 2 days ago	6-53515 6 days ago	15-52380 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-58998 2 days ago	2-58999 2 days ago	2-61144 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-57679 2 days ago	2-72608 2 days ago	2-78588 2 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-47208 2 days ago	4-76585 4 days ago	5-57928 5 days
28614	kckennylau author:kckennylau	feat(CategoryTheory): The finite pretopology on a category	We define `CategoryTheory.Pretopology.finite`, the finite pretopology on a category, which consists of presieves that contain only finitely many arrows. --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/)	maintainer-merge t-category-theory	131/0	Mathlib.lean,Mathlib/CategoryTheory/Sites/Finite.lean,Mathlib/CategoryTheory/Sites/Sieves.lean	3	31	['chrisflav', 'github-actions', 'joelriou', 'kckennylau']	chrisflav assignee:chrisflav	2-39528 2 days ago	2-49591 2 days ago	10-84236 10 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-6673 2 days ago	2-6673 2 days ago	10-8318 10 days
29536	kim-em author:kim-em	chore: minor grind golfing in Logic/Embedding	--- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/)	maintainer-merge t-logic	18/14	Mathlib/Logic/Embedding/Basic.lean,Mathlib/Logic/Embedding/Set.lean	2	2	['euprunin', 'github-actions', 'grunweg']	nobody	1-70245 1 day ago	2-6030 2 days ago	2-25733 2 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-47517 1 day ago	10-11547 10 days ago	223-86394 223 days
29493	kim-em author:kim-em	chore: grind golf in Mathlib.Logic	More golfs identified by `linter.tacticAnalysis.terminalToGrind`.	maintainer-merge t-logic	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	1-39532 1 day ago	3-6845 3 days ago	3-15656 3 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-34175 1 day ago	1-34175 1 day ago	15-11315 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-70374 19 hours ago	0-75649 21 hours ago	31-20384 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-61602 17 hours ago	0-61621 17 hours ago	1-43591 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-53023 14 hours ago	12-2067 12 days ago	26-19828 26 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	6	['github-actions', 'kbuzzard']	kbuzzard assignee:kbuzzard	0-52296 14 hours ago	0-52296 14 hours ago	57-73222 57 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-9649 2 hours ago	0-9649 2 hours ago	16-68098 16 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-29297 3 months ago	102-29298 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-77188 11 days ago	11-77189 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	2-81048 2 days ago	2-81049 2 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-22046 2 days ago	2-22047 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-44436 4 months ago	130-44445 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-43747 4 months ago	130-44382 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-10207 3 months ago	130-44346 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-53998 3 months ago	97-53999 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-64432 17 days ago	18-48165 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-11480 15 days ago	15-11480 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-70556 6 days ago	6-70556 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-6011 1 day ago	1-6011 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-21469 11 months ago	362-43444 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	296-81119 9 months ago	296-81119 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-36496 4 months ago	152-65126 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-67002 3 months ago	116-67003 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-66076 3 months ago	116-66078 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-24745 2 months ago	70-24745 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-23583 2 months ago	70-23584 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-52077 29 days ago	30-39449 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-11271 22 days ago	22-11272 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-45744 15 days ago	15-45745 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-39228 10 days ago	10-39229 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-61588 10 months ago	340-50110 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-44396 4 months ago	130-44401 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-46345 4 days ago	4-46345 4 days ago	4-46389 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-66578 3 days ago	6-72049 6 days ago	6-72031 6 days