Mathlib review and triage dashboard

Unassigned PRs on the review queue without updates in the past two weeks

Welcome to the PR triage page! This page is perfect if you intend to look for pull request which seem to have stalled.
TODO: this page is still under construction!

This dashboard was last updated on: November 23, 2024 at 23:02 UTC

Approved, not yet landed PRs

At the moment,

0 PRs are ready to merge, including no stale ones, congratulations!
17 PRs are waiting on maintainer approval (these), of which 13 have not been updated in a day (these)
9 PRs have been delegated and not updated in a day:

Number	Author	Title	Labels	+/-	📝	💬	Assignee(s)	Updated
14712	FR-vdash-bot	perf: change instance priority and order about `OfNat`	slow-typeclass-synthesis t-algebra merge-conflict delegated	49/20	9	24	nobody	2024-10-06 10:40 (1 months ago)
16250	Parcly-Taxel	chore: deprime `induction, cases` in `Combinatorics`	tech debt t-combinatorics merge-conflict delegated	323/267	39	4	nobody	2024-11-03 11:06 (20 days ago)
18790	jcommelin	chore(Algebra/Lie/Weights): rename Weight to GenWeight	t-algebra delegated	169/160	7	3	nobody	2024-11-11 09:51 (12 days ago)
13483	adomani	feat: automatically replace deprecations	t-meta delegated	304/0	7	15	nobody	2024-11-13 14:59 (10 days ago)
18712	bryangingechen	chore: add location of build.in.yml to directories checked by dependabot	CI delegated	3/1	1	4	nobody	2024-11-14 00:46 (9 days ago)
19127	kbuzzard	doc(GroupTheory/Commensurable): clarify some docstrings	t-algebra delegated documentation	15/11	2	3	nobody	2024-11-16 22:11 (7 days ago)
13609	101damnations	feat: Hopf algebra structure on monoid algebras	large-import t-algebra t-category-theory delegated	265/8	3	n/a	adamtopaz	2024-11-18 15:37 (5 days ago)
19205	Vierkantor	chore(Data/Finsupp): split off basic scalar multiplication	t-algebra delegated	105/54	3	15	nobody	2024-11-22 14:46 (1 days ago)
19275	eric-wieser	fix: if nolint files change, do a full rebuild	delegated	8/0	1	18	nobody	2024-11-22 21:22 (1 days ago)

Review status

There are currently 207 PRs awaiting review. Among these,

7 are labelled easy (these ones),
1 are addressing technical debt (namely these), and
??? appeared on the queue within the last two weeks.

On the other hand, 13 PRs are unassigned and have not been updated for two weeks, and 1 PRs are assigned, without recent review activity.

Unassigned PRs on the review queue without updates in the past two weeks

Number	Author	Title	Labels	+/-	📝	💬	Updated
18470	FR-vdash-bot	perf: lower the priority of `Normed.to` instances	slow-typeclass-synthesis t-algebra t-analysis	28/0	2	7	2024-10-31 00:42 (23 days ago)
18474	FR-vdash-bot	perf: lower the priority of `WithOne.to` instances	t-data slow-typeclass-synthesis t-algebra	13/2	3	4	2024-10-31 01:45 (23 days ago)
17081	jcommelin	chore: add workflow for merging master into bump/v4.x.y branches	CI	94/0	1	2	2024-10-31 16:47 (23 days ago)
18629	tomaz1502	feat(Computability.Timed): Formalization of runtime complexity of List.merge	t-computability new-contributor	186/0	3	1	2024-11-05 12:30 (18 days ago)
15192	FR-vdash-bot	feat: add some basic term elaborators	large-import t-meta	107/15	7	1	2024-11-06 19:49 (17 days ago)
18713	dwrensha	doc: update README.md instructions for building documentation locally		10/7	1	1	2024-11-07 01:14 (16 days ago)
18432	joelriou	feat(Algebra/Module): presentation of the tensor product	t-algebra	111/0	2	2	2024-11-07 15:05 (16 days ago)
18756	FR-vdash-bot	refactor: deprecate `DistribMulActionSemiHomClass` `MulSemiringActionSemiHomClass`	t-algebra	50/28	3	4	2024-11-08 13:57 (15 days ago)
18419	alreadydone	refactor: generalize `SMul (Ideal R) (Submodule R M)` to `SMul (Submodule R A) (Submodule R M)`	t-algebra	148/131	4	9	2024-11-08 18:19 (15 days ago)
16619	pechersky	feat(RingTheory/Valuation): valuation integers ring is a Principal Ideal ring iff the valuation range is not densely ordered	t-algebra	134/0	4	n/a	2024-11-08 21:22 (15 days ago)
18786	Command-Master	feat(RingTheory/Valuation/Basic): API for conversion `AddValuation` ↔ `Valuation`	t-algebra	35/5	1	1	2024-11-09 08:45 (14 days ago)
18780	vihdzp	feat(SetTheory/Ordinal/Arithmetic): `(sInf sᶜ).card ≤ #s`	t-set-theory	23/9	1	1	2024-11-09 12:45 (14 days ago)
18560	tb65536	feat(RingTheory/Invariant): Define invariant extensions of rings	FLT t-algebra	93/0	2	8	2024-11-09 19:08 (14 days ago)

Other lists of PRs

Some other lists of PRs which could be useful:

all PRs with just a failure of some infrastructure-related CI job (usually not this PR's fault), but are otherwise ready for review
all 'ready' PRs (not draft, not labelled WIP) labelled with 'tech debt' or 'longest-pole'
all PRs labelled 'awaiting-zulip': these are blocked on a zulip discussion or similar
all PRs which have a merge conflict, but otherwise fit the review queue
all PRs with just a failure of some infrastructure-related CI job (usually not this PR's fault), but are otherwise ready for review
all PR labelled 'new-contributor' which have not been updated in the past 7 days
all non-draft PRs, not labelled WIP, into some branch other than mathlib's master branch
all non-draft PRs, not labelled WIP, opened from a fork of mathlib
all PRs without draft status or 'WIP' label whose title does not start with an abbreviation like 'feat', 'style' or 'perf'
all PRs without draft status or 'WIP' label without a 'CI' or 't-something' label
PRs whose labels are contradictory, such as 'WIP' and 'ready-to-merge'
PRs that have at least one 'approved' review by a community member

PRs with just failing CI, but only often-spurious jobs

Number	Author	Title	Labels	+/-	📝	💬	Assignee(s)	Updated
18785	erdOne	feat(CategoryTheory): command that generates instances for `MorphismProperty`	t-category-theory t-meta	373/0	4	4	nobody	2024-11-23 20:19 (2 hours ago)

PRs addressing technical debt

Number	Author	Title	Labels	+/-	📝	💬	Assignee(s)	Updated
12879	grunweg	feat: port ge_or_gt linter from mathlib3	tech debt t-linter merge-conflict blocked-by-other-PR	736/319	109	3	nobody	2024-07-31 08:13 (3 months ago)
15480	grunweg	chore(NumberTheory): replace remaining occurrences of open Classical	tech debt t-number-theory merge-conflict awaiting-author	103/36	13	4	nobody	2024-08-08 11:34 (3 months ago)
13791	digama0	refactor: Primrec and Partrec	tech debt t-computability merge-conflict	585/778	5	2	nobody	2024-08-18 20:20 (3 months ago)
15448	urkud	chore(*): deprecate `Option.elim'`	tech debt merge-conflict awaiting-author	54/50	17	12	nobody	2024-08-19 17:34 (3 months ago)
16408	Parcly-Taxel	chore: remove TODO relating to #13092	tech debt merge-conflict	24/35	19	1	nobody	2024-09-04 19:05 (2 months ago)
16451	Parcly-Taxel	chore: `cases' ... with a a` to `rcases ... with a \| a`	tech debt merge-conflict blocked-by-other-PR	451/446	265	6	nobody	2024-09-09 10:14 (2 months ago)
16526	Parcly-Taxel	chore: `Or 2` automated replacement of `cases'`	awaiting-zulip tech debt merge-conflict	433/436	256	2	nobody	2024-09-09 10:14 (2 months ago)
16464	Parcly-Taxel	chore: deprecate `Nat.(case_)strong_induction_on`	tech debt merge-conflict	54/56	43	13	nobody	2024-09-20 17:43 (2 months ago)
16836	Parcly-Taxel	chore: delete deprecated algebraic structure files	awaiting-zulip tech debt easy merge-conflict	0/1890	7	5	nobody	2024-09-24 07:49 (1 months ago)
16250	Parcly-Taxel	chore: deprime `induction, cases` in `Combinatorics`	tech debt t-combinatorics merge-conflict delegated	323/267	39	4	nobody	2024-11-03 11:06 (20 days ago)
17109	grunweg	feat: warn on `autoImplicit true`	tech debt t-linter merge-conflict	65/26	4	12	nobody	2024-11-04 01:40 (19 days ago)
19354	kim-em	chore: split Order.Filter.Basic, creating Order.Filter.Finite	longest-pole	380/302	11	6	nobody	2024-11-23 02:38 (20 hours ago)

PRs blocked on a zulip discussion

Number	Author	Title	Labels	+/-	📝	💬	Assignee(s)	Updated
12331	mo271	chore: replace `refine ?_` and `refine' _` by `apply`	awaiting-zulip merge-conflict	200/200	136	1	nobody	2024-07-31 08:13 (3 months ago)
16526	Parcly-Taxel	chore: `Or 2` automated replacement of `cases'`	awaiting-zulip tech debt merge-conflict	433/436	256	2	nobody	2024-09-09 10:14 (2 months ago)
11800	JADekker	feat : Define KappaLindelöf spaces	awaiting-zulip t-topology merge-conflict please-adopt	301/2	3	38	nobody	2024-09-16 04:51 (2 months ago)
16836	Parcly-Taxel	chore: delete deprecated algebraic structure files	awaiting-zulip tech debt easy merge-conflict	0/1890	7	5	nobody	2024-09-24 07:49 (1 months ago)
17518	grunweg	feat: lint on declarations mentioning `Invertible` or `Unique`	awaiting-zulip t-linter merge-conflict blocked-by-other-PR	149/7	13	3	nobody	2024-11-02 17:42 (21 days ago)
18397	YaelDillies	chore: Rename `RestrictGenTopology` to `Topology.IsRestrictGen`	awaiting-zulip t-topology	33/30	7	7	nobody	2024-11-12 11:36 (11 days ago)
18884	YaelDillies	doc(overview): combinatorics overview	awaiting-zulip documentation	52/6	2	10	nobody	2024-11-14 01:10 (9 days ago)
17458	urkud	refactor(Algebra/Group): make `IsUnit` a typeclass	awaiting-zulip t-algebra merge-conflict	107/114	27	11	nobody	2024-11-15 10:57 (8 days ago)
18085	fpvandoorn	doc: factorial notation docstring	t-data awaiting-zulip	7/1	1	2	nobody	2024-11-18 13:18 (5 days ago)
17623	FR-vdash-bot	feat(Algebra/Order/GroupWithZero/Unbundled): add some lemmas	awaiting-zulip t-order t-algebra merge-conflict	146/44	2	11	nobody	2024-11-20 12:17 (3 days ago)

PRs with just a merge conflict

Number	Author	Title	Labels	+/-	📝	💬	Assignee(s)	Updated
12936	mattrobball	chore(Quiver.Opposite): make `Quiver.Hom.op/unop` `abbrev`'s	merge-conflict	39/34	10	9	nobody	2024-07-31 08:13 (3 months ago)
11837	trivial1711	feat: completion of a uniform multiplicative group	t-algebra t-topology merge-conflict	333/220	8	10	nobody	2024-07-31 08:13 (3 months ago)
10721	urkud	feat(Order/FunLike): define `PointwiseLE`	t-logic t-order merge-conflict	123/50	13	48	nobody	2024-07-31 08:14 (3 months ago)
9339	FMLJohn	feat (RingTheory/GradedAlgebra/HomogeneousIdeal): given a finitely generated homogeneous ideal of a graded semiring, construct a finite spanning set for the ideal which only contains homogeneous elements	t-algebra merge-conflict	402/4	8	11	nobody	2024-07-31 08:14 (3 months ago)
8788	FMLJohn	feat(Algebra/Module/GradeZeroModule): if `A` is a graded semiring and `M` is a graded `A`-module, then each grade of `M` is a module over the 0-th grade of `A`.	t-algebra merge-conflict	237/4	6	4	nobody	2024-07-31 08:14 (3 months ago)
9467	eric-wieser	refactor(Analysis/Calculus/FormalMultilinearSeries): generalize to additive monoids	t-analysis merge-conflict	35/22	2	2	nobody	2024-07-31 08:14 (3 months ago)
6777	adomani	chore(CovariantClass): replace eta-expanded (· ·), (· + ·), (· ≤ ·), (· < ·)	merge-conflict	703/678	81	36	nobody	2024-07-31 08:14 (3 months ago)
7875	FR-vdash-bot	chore: make `SMulCommClass A A B` and `SMulCommClass A B B` higher priority	slow-typeclass-synthesis t-algebra merge-conflict	54/48	27	15	nobody	2024-07-31 08:14 (3 months ago)
6993	jjaassoonn	feat : lemmas about `AddMonoidAlgebra.{divOf, modOf}`	t-algebra merge-conflict	147/3	5	42	nobody	2024-07-31 08:14 (3 months ago)
15483	FR-vdash-bot	chore(GroupTheory/Coset): reduce defeq abuse	t-algebra merge-conflict	114/60	6	13	nobody	2024-08-10 11:05 (3 months ago)
9145	linesthatinterlace	feat(Data/Fin/Basic): Refactor succAbove and predAbove.	t-data merge-conflict	1293/555	16	62	nobody	2024-08-14 10:01 (3 months ago)
10629	madvorak	feat: List.cons_sublist_append_iff_right	t-data merge-conflict	11/0	1	1	nobody	2024-08-14 10:01 (3 months ago)
11632	mattrobball	chore(Group/RingTheory.Congruence): make `Quotient`'s reducible	merge-conflict	16/35	2	14	nobody	2024-08-18 20:17 (3 months ago)
13791	digama0	refactor: Primrec and Partrec	tech debt t-computability merge-conflict	585/778	5	2	nobody	2024-08-18 20:20 (3 months ago)
14023	mattrobball	perf (RingTheory.OreLocalization): make data irreducible	merge-conflict	43/32	3	4	nobody	2024-08-18 20:21 (3 months ago)
11964	adamtopaz	feat: The functor of points of a scheme	t-algebraic-geometry t-category-theory merge-conflict	210/0	3	4	nobody	2024-08-18 20:23 (3 months ago)
12418	rosborn	style: replace preimage_val with ↓∩ notation	merge-conflict	56/61	18	3	nobody	2024-08-18 20:24 (3 months ago)
12751	Command-Master	feat: add lemmas for Nat/Bits, Nat/Bitwise and Nat/Size	t-data new-contributor merge-conflict	66/7	4	26	nobody	2024-08-19 14:32 (3 months ago)
13774	grunweg	chore: make expensive definitions noncomputable	RFC merge-conflict	152/135	31	15	nobody	2024-08-23 16:30 (3 months ago)
11212	shuxuezhuyi	feat(GroupTheory/GroupAction): instance `MulAction (β ⧸ H) α`	t-algebra merge-conflict	51/5	2	4	eric-wieser	2024-08-27 10:06 (2 months ago)
12610	Komyyy	perf: improves the performance of the `Repr (Equiv.Perm α)` instance	t-algebra merge-conflict	137/112	3	20	nobody	2024-08-27 10:08 (2 months ago)
13241	Komyyy	style(Mathlib/Data/Seq/Seq): rename `Stream'.Seq` to `Sequence`	merge-conflict	620/603	17	7	nobody	2024-08-27 10:11 (2 months ago)
13590	Komyyy	refactor(Mathlib/Algebra/ContinuedFractions/*): change the definition of regular continuous fractions	t-algebra merge-conflict	199/152	6	3	mattrobball	2024-08-30 12:32 (2 months ago)
16408	Parcly-Taxel	chore: remove TODO relating to #13092	tech debt merge-conflict	24/35	19	1	nobody	2024-09-04 19:05 (2 months ago)
16510	grunweg	chore: move style linters to `Linter/Style`	t-linter merge-conflict	626/607	4	1	nobody	2024-09-10 09:26 (2 months ago)
16633	mo271	chore(Mathlib/Algebra): minimize imports	t-algebra merge-conflict	157/536	329	35	nobody	2024-09-16 15:49 (2 months ago)
15994	adomani	feat: allow several identifiers in assert_not_exists	t-meta merge-conflict	377/258	97	2	nobody	2024-09-19 14:00 (2 months ago)
16464	Parcly-Taxel	chore: deprecate `Nat.(case_)strong_induction_on`	tech debt merge-conflict	54/56	43	13	nobody	2024-09-20 17:43 (2 months ago)
17127	FR-vdash-bot	chore: remove global `Quotient.mk` `⟦·⟧` notation	t-data merge-conflict	137/2	68	1	nobody	2024-09-30 04:10 (1 months ago)
11968	JovanGerb	feat: RefinedDiscrTree	new-contributor t-meta merge-conflict	2027/1366	16	24	joneugster	2024-10-08 06:48 (1 months ago)
8029	alreadydone	refactor: Homotopy between Functions not ContinuousMaps	t-topology RFC merge-conflict	246/250	8	3	nobody	2024-10-09 20:09 (1 months ago)
16054	vihdzp	chore(SetTheory/Game/Impartial): remove `Impartial` typeclass	t-combinatorics RFC merge-conflict	161/154	2	2	nobody	2024-10-14 02:49 (1 months ago)
17514	b-mehta	feat(Analysis/Convex): extreme points of doubly stochastic matrices	t-analysis merge-conflict	130/1	2	2	nobody	2024-10-24 10:59 (30 days ago)
16936	Felix-Weilacher	feat(Algebra/Group/Action): add definition of equidecomposition	t-algebra merge-conflict	243/0	3	1	nobody	2024-10-24 20:41 (30 days ago)
17368	Felix-Weilacher	feat(Topology/Baire/BaireMeasurable): add the Kuratowski-Ulam theorem	t-topology merge-conflict	187/1	5	6	nobody	2024-10-25 13:45 (29 days ago)
13964	pechersky	feat(Data/DigitExpansion): begin defining variant of reals without rationals	t-data merge-conflict	518/0	3	5	dupuisf	2024-10-27 11:05 (27 days ago)
17553	mo271	feat(Algebra/MvPolynomial/Degrees): degreeOf_mul_X_eq_degreeOf_add_one_iff	t-algebra merge-conflict	15/1	1	4	nobody	2024-11-01 14:44 (22 days ago)
17626	hanwenzhu	chore(Tactic/Polyrith): remove polyrith dependency on Python	t-meta merge-conflict	149/175	4	9	nobody	2024-11-04 01:42 (19 days ago)
14598	Command-Master	chore: add typeclasses to unify various `add_top`, `add_eq_top`, etc.	new-contributor t-order t-algebra merge-conflict	264/195	57	30	nobody	2024-11-06 05:25 (17 days ago)
12778	MichaelStollBayreuth	perf: decouple algebraic and order hierarchies in type class search	slow-typeclass-synthesis t-order t-algebra merge-conflict	306/27	135	34	nobody	2024-11-06 05:43 (17 days ago)
9820	jjaassoonn	feat(RingTheory/GradedAlgebra/HomogeneousIdeal): generalize to homogeneous submodule	t-algebra merge-conflict	623/190	8	2	nobody	2024-11-08 17:13 (15 days ago)
18652	javierlcontreras	refactor(LocalRing/Basic): generalize to non-commutative (semi)rings	new-contributor t-algebra merge-conflict	20/9	1	3	nobody	2024-11-12 13:57 (11 days ago)
18595	pechersky	chore(RingTheory/Ideal/Colon): generalize to semiring	t-algebra merge-conflict	40/10	1	1	nobody	2024-11-13 07:30 (10 days ago)
18728	jjaassoonn	feat(RingTheory/GradedAlgebra): define homogeneous submodule	t-algebra merge-conflict	171/53	10	21	nobody	2024-11-13 20:35 (10 days ago)
18468	FR-vdash-bot	perf: lower the priority of `Ordered.to` instances	slow-typeclass-synthesis t-order t-algebra merge-conflict	70/8	13	5	nobody	2024-11-14 18:54 (9 days ago)
18940	ocfnash	feat: drop finite-dimensionality assumption from `PerfectPairing.restrictScalarsField`	t-algebra merge-conflict	165/10	7	3	nobody	2024-11-14 18:58 (9 days ago)
16743	agjftucker	feat(Analysis/Calculus/Implicit): define HasStrictDerivAt.implicitFunOfBivariate	new-contributor t-analysis merge-conflict	132/8	4	1	sgouezel	2024-11-15 16:54 (8 days ago)
16314	FR-vdash-bot	chore(Data/Quot): deprecate `ind*'` APIs	t-data merge-conflict	246/286	65	2	nobody	2024-11-17 16:41 (6 days ago)
17758	vihdzp	feat(SetTheory/Ordinal/ENat): `Ordinal.toENat`	t-set-theory merge-conflict	297/0	6	2	nobody	2024-11-18 03:53 (5 days ago)
18806	FR-vdash-bot	refactor: deprecate `MulEquivClass`	t-algebra merge-conflict	84/72	15	6	nobody	2024-11-18 17:35 (5 days ago)
18564	kmill	feat: `Encodable` deriving handler	t-meta merge-conflict	450/0	4	1	adomani	2024-11-18 18:25 (5 days ago)
5901	FR-vdash-bot	feat: more `PGame.identical` `PGame.memₗ` `PGame.memᵣ` APIs	t-combinatorics merge-conflict	452/24	2	n/a	kmill	2024-11-18 23:05 (4 days ago)
18557	kmill	feat: `Countable` deriving handler	t-meta merge-conflict	380/0	4	9	adomani	2024-11-18 23:32 (4 days ago)
17366	joelriou	feat(Algebra/Category/ModuleCat): pullback of presheaves of modules	t-algebra t-algebraic-geometry t-category-theory merge-conflict	99/0	3	2	nobody	2024-11-19 09:55 (4 days ago)
19040	kmill	feat: add option `pp.mathlib.binderPredicates`	large-import t-meta merge-conflict	107/34	4	1	nobody	2024-11-19 22:44 (4 days ago)
17672	urkud	refactor: turn `IsTorsionFree` into a typeclass	t-algebra merge-conflict	256/130	21	12	nobody	2024-11-20 06:54 (3 days ago)
17087	LorenzoLuccioli	feat(Data/EReal): Add results about `EReal`	t-data merge-conflict	241/36	3	3	nobody	2024-11-20 09:30 (3 days ago)
18672	TobiasLeichtfried	feat: add leftmost derivation in context free grammar	t-computability new-contributor merge-conflict	74401/35464	2589	16	nobody	2024-11-21 16:48 (2 days ago)
19039	D-Thomine	refactor(Probability.Martingale.BorelCantelli): move and simplify lemmas about indicators	t-measure-probability t-order merge-conflict	56/84	6	1	nobody	2024-11-22 03:15 (1 days ago)
13649	FR-vdash-bot	chore: redefine `Nat.bit` `Nat.div2` `Nat.bodd`	merge-conflict	73/99	11	12	digama0	2024-11-22 22:24 (1 days ago)
19337	zeramorphic	feat(Data/Finsupp): generalise `Finsupp` to any "zero" value	t-data merge-conflict	203/83	13	5	nobody	2024-11-22 23:27 (23 hours ago)
19370	Vierkantor	chore(RingTheory): split up `Algebraic.lean`	t-algebra merge-conflict	494/316	16	1	nobody	2024-11-23 05:29 (17 hours ago)
18406	mans0954	refactor(LinearAlgebra/SesquilinearForm): Hermitian sesquilinear maps	t-algebra merge-conflict	107/43	4	5	nobody	2024-11-23 10:45 (12 hours ago)
17444	FR-vdash-bot	refactor: make `CanonicallyOrdered...` mixin	t-order t-algebra merge-conflict	641/565	102	16	nobody	2024-11-23 15:55 (7 hours ago)
19002	YaelDillies	chore: move pointwise set files to `Algebra._.Pointwise`	t-algebra merge-conflict	17/17	16	4	nobody	2024-11-23 16:49 (6 hours ago)

PRs with just failing CI, but only often-spurious jobs

Number	Author	Title	Labels	+/-	📝	💬	Assignee(s)	Updated
18785	erdOne	feat(CategoryTheory): command that generates instances for `MorphismProperty`	t-category-theory t-meta	373/0	4	4	nobody	2024-11-23 20:19 (2 hours ago)

Stale new contributor PRs

Number	Author	Title	Labels	+/-	📝	💬	Assignee(s)	Updated
11021	jstoobysmith	feat(AlgebraicTopology) : add join of augmented SSets	new-contributor t-category-theory merge-conflict WIP	2137/1	6	47	nobody	2024-07-31 08:14 (3 months ago)
15224	AnthonyBordg	feat(CategoryTheory/Sites): covering families and their associated Grothendieck topology	new-contributor t-category-theory awaiting-author	112/0	2	20	nobody	2024-08-05 15:10 (3 months ago)
8102	miguelmarco	feat (Tactic): add unify_denoms and collect_signs tactics	new-contributor t-meta merge-conflict enhancement	431/1	8	8	nobody	2024-08-14 09:57 (3 months ago)
14563	awueth	feat: if-then-else of exclusive or statement	new-contributor t-algebra awaiting-author	5/0	1	3	nobody	2024-08-15 10:20 (3 months ago)
14498	hwatheod	feat(SetTheory/Surreal/Division): define the field structure on the Surreal numbers	new-contributor t-logic awaiting-author	711/6	5	47	nobody	2024-08-19 03:48 (3 months ago)
12751	Command-Master	feat: add lemmas for Nat/Bits, Nat/Bitwise and Nat/Size	t-data new-contributor merge-conflict	66/7	4	26	nobody	2024-08-19 14:32 (3 months ago)
9935	jstoobysmith	feat(AlgebraicTopology): add constructors for horns	new-contributor t-algebra t-topology merge-conflict awaiting-author	462/2	1	15	nobody	2024-08-19 14:35 (3 months ago)
11207	luigi-massacci	feat(Topology/MetricSpace): Add new file with type of Katetov maps	new-contributor t-topology WIP	138/0	3	16	nobody	2024-08-19 14:41 (3 months ago)
11090	pangelinos	feat: define spectral spaces and prove that a quasi-compact open of a spectral space is spectral	new-contributor t-topology please-adopt good first issue	69/0	1	15	nobody	2024-08-19 14:43 (3 months ago)
14368	FMLJohn	feat: morphisms from the spectrum of a field to a locally ringed space	new-contributor t-algebra t-algebraic-geometry WIP	405/0	3	1	nobody	2024-08-28 18:57 (2 months ago)
15121	Eloitor	feat: iff theorems for IsSplitEpi and IsSplitMono in opposite category	new-contributor t-category-theory awaiting-author	40/0	1	3	nobody	2024-09-01 21:31 (2 months ago)
13480	Espio231	feat(Algebra/Lie): add Lie's theorem	new-contributor t-algebra merge-conflict awaiting-author	390/0	4	57	nobody	2024-09-12 18:38 (2 months ago)
11768	JovanGerb	feat: Interactive Library Rewrite	new-contributor t-meta blocked-by-other-PR	3102/41	17	9	nobody	2024-09-13 21:23 (2 months ago)
15711	znssong	feat(Combinatorics/SimpleGraph): Some lemmas about walk, cycle and Hamiltonian cycle	new-contributor t-combinatorics awaiting-author	407/3	4	22	nobody	2024-09-17 10:05 (2 months ago)
14033	pfaffelh	feat(MeasureTheory): TendstoInMeasure gives ae unique limits; TendstoInMeasure equivalent to subsequences converging ae	new-contributor t-measure-probability awaiting-author	208/8	5	83	kex-y	2024-09-18 09:28 (2 months ago)
16773	arulandu	feat(Probability/Distributions): formalize Beta distribution	new-contributor t-measure-probability awaiting-author	286/1	3	48	arulandu	2024-09-20 08:34 (2 months ago)
10006	jstoobysmith	feat(AlgebraicTopology): homotopy in quasicategories	new-contributor t-category-theory merge-conflict awaiting-author blocked-by-other-PR	898/1	4	3	nobody	2024-09-24 07:28 (1 months ago)
14799	luigi-massacci	feat(Analysis/MeanInequalities): Weighted QM-AM inequality	new-contributor t-analysis easy awaiting-author	26/3	1	8	nobody	2024-09-24 08:34 (1 months ago)
13685	niklasmohrin	feat(Combinatorics): add definitions for network flows	new-contributor t-combinatorics awaiting-author	241/0	3	34	nobody	2024-09-24 12:33 (1 months ago)
14237	js2357	feat: Define the localization of a fractional ideal at a prime ideal	new-contributor t-algebra awaiting-author	230/0	3	20	Vierkantor	2024-09-24 14:27 (1 months ago)
14242	js2357	feat: Prove equivalence of `isDedekindDomain` and `isDedekindDomainDvr`	new-contributor t-algebra merge-conflict blocked-by-other-PR	269/1	4	2	nobody	2024-09-24 18:27 (1 months ago)
15651	TpmKranz	feat(Computability/NFA): operations for Thompson's construction	t-computability new-contributor awaiting-author	307/5	1	13	nobody	2024-09-25 11:13 (1 months ago)
15212	victorliu5296	feat: Add fundamental theorem of calculus-2 for Banach spaces	new-contributor t-measure-probability t-analysis awaiting-author	60/1	1	3	nobody	2024-09-25 16:47 (1 months ago)
16344	robertmaxton42	feat(LinearAlgebra/FreeProduct): add induction principle, further simp opts for lift	new-contributor t-algebra blocked-by-other-PR	240/17	1	2	nobody	2024-09-27 08:57 (1 months ago)
16887	metinersin	feat(ModelTheory/Complexity): define conjunctive and disjunctive formulas	new-contributor t-logic merge-conflict blocked-by-other-PR	300/7	3	2	nobody	2024-10-02 19:34 (1 months ago)
16888	metinersin	feat(ModelTheory/Complexity): Define conjunctive and disjunctive normal forms	new-contributor t-logic merge-conflict blocked-by-other-PR	415/7	3	2	nobody	2024-10-02 19:34 (1 months ago)
16889	metinersin	feat(ModelTheory/Complexity): Normal forms	new-contributor t-logic merge-conflict blocked-by-other-PR	525/7	3	2	nobody	2024-10-02 19:34 (1 months ago)
16094	FM22	feat(Algebra/Ring): generalise and extend material about sums of squares and semireal rings	new-contributor t-order t-algebra merge-conflict awaiting-author	174/81	8	52	nobody	2024-10-02 23:12 (1 months ago)
11968	JovanGerb	feat: RefinedDiscrTree	new-contributor t-meta merge-conflict	2027/1366	16	24	joneugster	2024-10-08 06:48 (1 months ago)
15009	madeve-unipi	feat(Analysis/Complex/Hadamard): generalize Hadamard's three lines theorem	new-contributor t-analysis awaiting-author	241/18	1	34	dupuisf	2024-10-08 14:48 (1 months ago)
10190	jstoobysmith	feat(AlgebraicTopology): add Augmented Simplex Category	new-contributor t-algebra t-topology t-category-theory merge-conflict WIP	720/0	4	5	nobody	2024-10-09 16:44 (1 months ago)
17176	arulandu	feat: integrals and integrability with .re	new-contributor t-measure-probability awaiting-author	49/0	4	30	nobody	2024-10-15 06:53 (1 months ago)
17500	ahhwuhu	feat: Define shifted Legendre polynomials and prove some basic properties	new-contributor t-analysis awaiting-author	139/0	2	18	nobody	2024-10-18 02:44 (1 months ago)
15578	znssong	feat(Function): Fixed points of function `f` with `f(x) >= x`	new-contributor t-analysis awaiting-author	82/0	3	32	nobody	2024-10-18 14:16 (1 months ago)
12750	Command-Master	feat: define Gray code	t-data new-contributor merge-conflict awaiting-author blocked-by-other-PR	226/0	5	5	nobody	2024-10-20 13:16 (1 months ago)
14603	awueth	feat: degree is invariant under graph isomorphism	new-contributor t-combinatorics WIP	24/0	1	10	nobody	2024-10-22 16:15 (1 months ago)
15720	znssong	feat(SimpleGraph): The Bondy-Chvátal theorem	new-contributor t-combinatorics blocked-by-other-PR	903/3	8	3	YaelDillies	2024-10-25 01:33 (29 days ago)
17739	Aaron1011	feat(Topology/Order/DenselyOrdered): prove Not (IsOpen) for intervals	new-contributor t-topology awaiting-author	27/0	1	8	nobody	2024-10-25 17:32 (29 days ago)
18091	tukamilano	feat: Hoeffding's lemma	large-import new-contributor t-measure-probability awaiting-author	567/1	4	28	tukamilano	2024-10-26 14:02 (28 days ago)
15654	TpmKranz	feat(Computability): language-preserving maps between NFA and RE	t-computability new-contributor merge-conflict blocked-by-other-PR	985/2	7	2	nobody	2024-10-28 09:55 (26 days ago)
18379	oeb25	feat(Topology/ENNReal): Add `ENNReal.tsum_biUnion`	new-contributor t-topology	28/0	1	1	nobody	2024-10-29 09:51 (25 days ago)
18195	Whysoserioushah	feat(Algebra): define `PrimitiveIdempotents`	new-contributor t-algebra awaiting-author	125/0	2	28	erdOne	2024-10-29 11:48 (25 days ago)
15127	goens	feat(Quot): add simple lemmas on function congruence	t-data new-contributor awaiting-author	10/0	1	14	nobody	2024-10-30 10:55 (24 days ago)
14313	grhkm21	feat(RepresentationTheory/FdRep): FdRep is a full subcategory of Rep	new-contributor t-algebra t-category-theory	47/8	1	19	nobody	2024-10-30 11:59 (24 days ago)
12799	jstoobysmith	feat(LinearAlgebra/UnitaryGroup): Add properties of Special Unitary Group	new-contributor t-algebra please-adopt awaiting-author	78/0	1	7	nobody	2024-10-30 14:41 (24 days ago)
9605	davikrehalt	feat(Data/Finset & List): Add Lemmas for Sorting and Filtering	t-data new-contributor merge-conflict please-adopt awaiting-author	71/0	4	30	YaelDillies	2024-10-30 21:15 (24 days ago)
18448	jhanschoo	chore(Computability/TuringMachine): split `TuringMachine.lean`	t-computability new-contributor RFC merge-conflict	1730/1683	5	3	nobody	2024-10-31 05:08 (23 days ago)
17595	Paul-Lez	feat(Order/Bounds/Basic): Add basic order lemmas	new-contributor t-order awaiting-author	47/0	1	3	nobody	2024-11-02 21:20 (21 days ago)
18629	tomaz1502	feat(Computability.Timed): Formalization of runtime complexity of List.merge	t-computability new-contributor	186/0	3	1	nobody	2024-11-05 12:30 (18 days ago)
14598	Command-Master	chore: add typeclasses to unify various `add_top`, `add_eq_top`, etc.	new-contributor t-order t-algebra merge-conflict	264/195	57	30	nobody	2024-11-06 05:25 (17 days ago)
15686	robertmaxton42	refactor (LinearAlgebra/FreeProduct): move PowerAlgebra construction to its own namespace, minor simp opts	new-contributor t-algebra awaiting-author	143/11	1	19	kbuzzard	2024-11-06 10:51 (17 days ago)
16885	metinersin	feat(ModelTheory/Complexity): define literals	new-contributor t-logic merge-conflict awaiting-author	148/5	4	20	nobody	2024-11-08 17:36 (15 days ago)
18652	javierlcontreras	refactor(LocalRing/Basic): generalize to non-commutative (semi)rings	new-contributor t-algebra merge-conflict	20/9	1	3	nobody	2024-11-12 13:57 (11 days ago)
13248	hcWang942	feat: basic concepts of auction theory	new-contributor t-logic merge-conflict awaiting-author	204/0	3	148	hcWang942	2024-11-13 06:49 (10 days ago)
18694	ooovi	feat(Data/Nat/Defs): Add a commuted version of `Nat.le_div_iff_mul_le'`	t-data new-contributor awaiting-author	3/0	1	1	nobody	2024-11-13 15:32 (10 days ago)
18608	ooovi	feat(Combinatorics/SimpleGraph): add independent sets	new-contributor t-combinatorics	213/9	1	24	nobody	2024-11-13 16:09 (10 days ago)
18461	hannahfechtner	feat: left and right common multiples mixins	new-contributor t-algebra	68/0	1	3	nobody	2024-11-13 19:50 (10 days ago)
18646	jxjwan	feat(RingTheory): isotypic components	new-contributor t-algebra	308/0	3	1	nobody	2024-11-14 00:38 (9 days ago)
18627	tomaz1502	feat(Computability.Timed): Formalization of runtime complexity of insertion sort	t-computability new-contributor	112/0	2	7	nobody	2024-11-14 01:27 (9 days ago)
15649	TpmKranz	feat(Computability): introduce Generalised NFA as bridge to Regular Expression	t-computability new-contributor	298/0	5	2	nobody	2024-11-14 12:54 (9 days ago)
16116	jjdishere	feat(Field): add theorems in Stacks Project Chapter 09FA Fields	new-contributor t-algebra merge-conflict WIP	6/2	2	6	nobody	2024-11-14 17:29 (9 days ago)
19042	maddycrim	feat(RingTheory/Localization/Defs): localization of a direct product injects into product of localizations	new-contributor t-algebra	69/0	1	1	nobody	2024-11-15 07:07 (8 days ago)
11156	smorel394	feat(LinearAlgebra/{TensorProductBasis,Dual}): basis and dual of `PiTensorProduct`	large-import new-contributor t-algebra merge-conflict please-adopt blocked-by-other-PR	166/2	3	4	kbuzzard	2024-11-15 09:28 (8 days ago)
18247	su00000	feat(RingTheory/NoetherNormalization):Add noether normalization lemma	new-contributor t-algebra merge-conflict WIP	433/0	4	3	nobody	2024-11-15 09:33 (8 days ago)
19084	Louddy	feat(SkewMonoidAlgebra): `coeff`, `single`, `one` and `sum`	large-import new-contributor t-algebra	267/11	1	1	nobody	2024-11-15 14:09 (8 days ago)
10541	Louddy	feat(Algebra/SkewMonoidAlgebra/Basic): add SkewMonoidAlgebra	new-contributor t-algebra merge-conflict blocked-by-other-PR WIP	1624/0	4	105	AntoineChambert-Loir	2024-11-15 14:23 (8 days ago)
18767	Happyves	feat: `List.rget` and related lemmata	t-data new-contributor	108/1	3	16	nobody	2024-11-15 15:55 (8 days ago)
16743	agjftucker	feat(Analysis/Calculus/Implicit): define HasStrictDerivAt.implicitFunOfBivariate	new-contributor t-analysis merge-conflict	132/8	4	1	sgouezel	2024-11-15 16:54 (8 days ago)
12290	yoh-tanimoto	feat(MeasureTheory/Integral/linearRieszMarkovKakutani) prove that the Riesz content is indeed a content	new-contributor t-measure-probability RFC merge-conflict WIP	320/24	1	33	nobody	2024-11-16 10:05 (7 days ago)
19056	vbeffara	feat(Topology/FiberBundle/Trivialization): local lifting through a Trivialization	new-contributor t-topology	47/0	1	1	nobody	2024-11-16 22:50 (7 days ago)

PRs not into the master branch

Number	Author	Title	Labels	+/-	📝	💬	Assignee(s)	Updated
13158	erdOne	refactor(RingTheory/OreLocalization/Module): remove `LocalizedModule.mk`.	t-algebra merge-conflict blocked-by-other-PR	49/48	2	1	nobody	2024-07-09 13:36 (4 months ago)
18641	FR-vdash-bot	perf: change the priority of `*.toRing` instances	awaiting-bench slow-typeclass-synthesis t-algebra blocked-by-other-PR	7/1	4	5	nobody	2024-11-06 13:28 (17 days ago)
18472	FR-vdash-bot	perf: lower the priority of `Comm.to` instances	awaiting-bench slow-typeclass-synthesis t-algebra blocked-by-other-PR	33/10	14	5	nobody	2024-11-06 22:18 (17 days ago)
18464	FR-vdash-bot	perf: lower the priority of `toMul` and `toAdd` instances	awaiting-bench slow-typeclass-synthesis t-algebra blocked-by-other-PR	38/12	5	2	nobody	2024-11-07 02:45 (16 days ago)
18706	FR-vdash-bot	perf: change the priority of `*.toSemiring` instances	awaiting-bench slow-typeclass-synthesis t-algebra blocked-by-other-PR WIP	24/15	9	2	nobody	2024-11-07 06:07 (16 days ago)
11156	smorel394	feat(LinearAlgebra/{TensorProductBasis,Dual}): basis and dual of `PiTensorProduct`	large-import new-contributor t-algebra merge-conflict please-adopt blocked-by-other-PR	166/2	3	4	kbuzzard	2024-11-15 09:28 (8 days ago)
19257	j-loreaux	Do not merge: Performance of SemigroupAction against nightly-testing	merge-conflict WIP	33/25	11	6	nobody	2024-11-22 06:48 (1 days ago)
19423	kim-em	chore: adaptations for nightly-2024-11-23		5/5	5	1	nobody	2024-11-23 22:42 (19 minutes ago)

PRs from a fork of mathlib

Number	Author	Title	Labels	+/-	📝	💬	Assignee(s)	Updated
15617	vigoux	perf: use foldl for implementation of Multiset.fold	awaiting-author	9/0	1	1	nobody	2024-08-14 14:17 (3 months ago)
13941	TucanoUrbano	feat: metric entropy	t-measure-probability merge-conflict awaiting-author	4074/2	10	1	nobody	2024-08-23 16:48 (3 months ago)
16455	adomani	test: bench action	merge-conflict WIP	14409/7899	1181	0	nobody	2024-09-12 08:17 (2 months ago)
16688	vlad902	chore(scripts/install_macos): Fix 2 PATH resolution issues		4/0	1	1	nobody	2024-10-11 19:04 (1 months ago)
3610	TimothyGu	feat: derive Infinite automatically for inductive types	t-meta awaiting-author	517/0	3	10	kmill	2024-11-06 23:43 (16 days ago)
16216	jxjwan	feat(RingTheory): isotypic components	t-algebra	308/0	3	2	nobody	2024-11-14 11:08 (9 days ago)

PRs with non-conforming titles

Number	Author	Title	Labels	+/-	📝	💬	Assignee(s)	Updated
19284	adomani	test: commit a change only to the "master" CI build action	CI	-1/-1	-1	n/a	nobody	2024-11-20 12:46 (3 days ago)
19282	PieterCuijpers	add a variable_alias for Quantale and AddQuantale	new-contributor t-algebra blocked-by-other-PR	21/6	1	2	nobody	2024-11-20 12:48 (3 days ago)
19164	Command-Master	Add `toWithTop`, `ofWithTop`	t-data RFC	58/0	1	1	nobody	2024-11-22 04:33 (1 days ago)
19367	adomani	test: try emoji action	CI	58/11	2	2	nobody	2024-11-22 14:54 (1 days ago)
19281	Vierkantor	Split polynomial.algebra	t-algebra merge-conflict blocked-by-other-PR	3575/2865	52	2	nobody	2024-11-23 01:40 (21 hours ago)
19124	yhtq	fead: Add `lift_unique`, `lift_unique'` to `IsFractionRing`	new-contributor t-algebra awaiting-author	12/0	1	18	nobody	2024-11-23 13:18 (9 hours ago)

PRs without an area label

Number	Author	Title	Labels	+/-	📝	💬	Assignee(s)	Updated
19297	fpvandoorn	feat(to_additive): option to not translate operations on a type		172/371	4	1	nobody	2024-11-20 16:25 (3 days ago)

PRs with contradictory labels

There are currently no PRs with contradictory labels. Congratulations!

PRs with an 'approved' review

Number	Author	Title	Labels	+/-	📝	💬	Assignee(s)	Updated
12608	eric-wieser	feat: allow `nsmul` / `zsmul` to be omitted again, with a warning	t-algebra t-meta merge-conflict awaiting-author	118/2	6	12	nobody	2024-07-31 08:13 (3 months ago)
12934	grunweg	chore: replace more uses of > or ≥ by < or ≤	merge-conflict awaiting-author help-wanted	41/42	15	11	nobody	2024-07-31 08:13 (3 months ago)
12673	grunweg	feat: add ContDiff.lipschitzOnWith	t-analysis awaiting-author	30/11	1	6	nobody	2024-07-31 08:13 (3 months ago)
9352	chenyili0818	feat: arithmetic lemmas for `gradient`	t-analysis awaiting-author	404/0	2	30	nobody	2024-07-31 08:14 (3 months ago)
9146	laughinggas	feat(Data/ZMod/Defs): Topological structure on `ZMod`	t-algebra t-topology merge-conflict awaiting-author	55/3	5	61	nobody	2024-07-31 08:14 (3 months ago)
8519	eric-wieser	refactor(LinearAlgebra/TensorProduct): golf using `liftAddHom`	t-algebra merge-conflict awaiting-author	53/50	3	28	nobody	2024-07-31 08:14 (3 months ago)
6777	adomani	chore(CovariantClass): replace eta-expanded (· ·), (· + ·), (· ≤ ·), (· < ·)	merge-conflict	703/678	81	36	nobody	2024-07-31 08:14 (3 months ago)
8370	eric-wieser	refactor(Analysis/NormedSpace/Exponential): remove the `𝕂` argument from `exp`	t-analysis RFC merge-conflict	404/373	10	12	nobody	2024-07-31 08:14 (3 months ago)
2605	eric-wieser	chore: better error message in linarith	t-meta merge-conflict awaiting-author	12/1	1	2	nobody	2024-07-31 08:14 (3 months ago)
6403	FR-vdash-bot	chore: change instance priorities of `Ordered*` hierarchy	slow-typeclass-synthesis t-order t-algebra merge-conflict awaiting-author	253/79	18	39	nobody	2024-07-31 08:14 (3 months ago)
3757	thorimur	feat: config options for `fail_if_no_progress`	t-meta merge-conflict WIP	603/54	5	38	nobody	2024-07-31 08:14 (3 months ago)
11890	adomani	feat: the terminal refine linter	t-linter awaiting-author	77/0	3	14	nobody	2024-08-19 08:05 (3 months ago)
12751	Command-Master	feat: add lemmas for Nat/Bits, Nat/Bitwise and Nat/Size	t-data new-contributor merge-conflict	66/7	4	26	nobody	2024-08-19 14:32 (3 months ago)
15448	urkud	chore(*): deprecate `Option.elim'`	tech debt merge-conflict awaiting-author	54/50	17	12	nobody	2024-08-19 17:34 (3 months ago)
7907	urkud	feat: introduce `NthRoot` notation class	t-algebra t-analysis awaiting-CI merge-conflict	212/174	31	9	nobody	2024-08-27 10:38 (2 months ago)
15454	grunweg	feat: linter for bare `open (scoped) Classical`	t-linter merge-conflict blocked-by-other-PR	151/0	4	16	nobody	2024-08-30 12:49 (2 months ago)
11800	JADekker	feat : Define KappaLindelöf spaces	awaiting-zulip t-topology merge-conflict please-adopt	301/2	3	38	nobody	2024-09-16 04:51 (2 months ago)
13685	niklasmohrin	feat(Combinatorics): add definitions for network flows	new-contributor t-combinatorics awaiting-author	241/0	3	34	nobody	2024-09-24 12:33 (1 months ago)
9105	LukasMias	feat(Algebra/Algebra/Prod): add prodUnique and uniqueProd for LinearEquiv and AlgebraEquiv	t-algebra merge-conflict awaiting-author	64/4	4	8	nobody	2024-10-08 04:34 (1 months ago)
11500	mcdoll	refactor(Topology/Algebra/Module/WeakDual): Clean up	t-topology merge-conflict awaiting-author	227/179	15	14	nobody	2024-10-08 04:35 (1 months ago)
15026	grunweg	fix: recognise awaiting-review comments again	CI merge-conflict awaiting-author	4/3	1	5	nobody	2024-10-08 04:36 (1 months ago)
11968	JovanGerb	feat: RefinedDiscrTree	new-contributor t-meta merge-conflict	2027/1366	16	24	joneugster	2024-10-08 06:48 (1 months ago)
17342	Ruben-VandeVelde	chore: tidy various files	merge-conflict awaiting-author	96/108	32	12	nobody	2024-10-10 15:49 (1 months ago)
17538	joneugster	feat(scripts/autolabel): add `dependency-bump` label automatically	CI merge-conflict awaiting-author	5/3	2	3	nobody	2024-10-14 03:05 (1 months ago)
17176	arulandu	feat: integrals and integrability with .re	new-contributor t-measure-probability awaiting-author	49/0	4	30	nobody	2024-10-15 06:53 (1 months ago)
17005	YnirPaz	feat(SetTheory/Cardinal/Regular): define singular cardinals	t-set-theory WIP	94/1	3	27	nobody	2024-10-29 17:53 (25 days ago)
13514	madvorak	feat(Computability/ContextFreeGrammar): closure under union	t-computability merge-conflict blocked-by-other-PR	448/4	1	50	nobody	2024-11-02 10:08 (21 days ago)
18210	vihdzp	feat(Order/Hom/Basic): `WithBot (Fin n) ≃o Fin (n + 1)`	t-order awaiting-author	16/0	1	6	nobody	2024-11-04 23:47 (18 days ago)
18780	vihdzp	feat(SetTheory/Ordinal/Arithmetic): `(sInf sᶜ).card ≤ #s`	t-set-theory	23/9	1	1	nobody	2024-11-09 12:45 (14 days ago)
16769	Command-Master	feat(Combinatorics/SimpleGraph/Walk): add `penultimate` and `snd`	maintainer-merge t-combinatorics	68/25	4	7	nobody	2024-11-10 14:56 (13 days ago)
18790	jcommelin	chore(Algebra/Lie/Weights): rename Weight to GenWeight	t-algebra delegated	169/160	7	3	nobody	2024-11-11 09:51 (12 days ago)
15294	RemyDegenne	feat: two Finset lemmas	t-algebra merge-conflict awaiting-author	35/5	4	9	nobody	2024-11-11 14:51 (12 days ago)
18652	javierlcontreras	refactor(LocalRing/Basic): generalize to non-commutative (semi)rings	new-contributor t-algebra merge-conflict	20/9	1	3	nobody	2024-11-12 13:57 (11 days ago)
18693	Ruben-VandeVelde	feat: add ConjRootClass	t-algebra	199/0	3	1	nobody	2024-11-12 18:47 (11 days ago)
18608	ooovi	feat(Combinatorics/SimpleGraph): add independent sets	new-contributor t-combinatorics	213/9	1	24	nobody	2024-11-13 16:09 (10 days ago)
12133	ADedecker	feat: generalize instIsLowerProd to arbitrary products	t-order t-topology merge-conflict awaiting-author	34/14	2	13	nobody	2024-11-15 08:27 (8 days ago)
18239	vihdzp	chore(SetTheory/ZFC/Rank): clean up file	t-set-theory maintainer-merge	42/37	1	7	nobody	2024-11-15 09:26 (8 days ago)
17638	Vierkantor	feat(Tactic): `erw` tries `rw` first and warns if that succeeds	t-meta WIP	36/5	7	22	nobody	2024-11-15 09:39 (8 days ago)
19060	vihdzp	feat(Algebra/Order/SuccPred): `IsSuccLimit` theorems for `SuccAddOrder`	maintainer-merge t-order	47/1	2	2	nobody	2024-11-15 11:19 (8 days ago)
18547	vihdzp	feat: uncountable instances for `Ordinal` and isomorphic types	t-set-theory	25/1	5	3	nobody	2024-11-17 06:25 (6 days ago)
19145	vihdzp	chore(SetTheory/Ordinal/Exponential): redefine ordinal exponential without `bsup`	t-set-theory	36/25	2	2	nobody	2024-11-18 02:05 (5 days ago)
18611	vihdzp	feat(SetTheory/Ordinal/Veblen): the two-argument Veblen function	t-set-theory	326/0	3	17	nobody	2024-11-18 02:41 (5 days ago)
17758	vihdzp	feat(SetTheory/Ordinal/ENat): `Ordinal.toENat`	t-set-theory merge-conflict	297/0	6	2	nobody	2024-11-18 03:53 (5 days ago)
15809	archiebrowne	feat(RingTheory/MvPolynomial/Ideal): introduce new lemmas about MvPolynomial Ideals	new-contributor t-algebra awaiting-author	38/0	1	6	riccardobrasca	2024-11-18 15:28 (5 days ago)
13609	101damnations	feat: Hopf algebra structure on monoid algebras	large-import t-algebra t-category-theory delegated	265/8	3	n/a	adamtopaz	2024-11-18 15:37 (5 days ago)
15991	vihdzp	feat(SetTheory/Ordinal/CantorNormalForm): alternate CNF recursion principle	t-set-theory maintainer-merge t-logic	43/0	3	8	nobody	2024-11-18 23:17 (4 days ago)
10235	urkud	feat: add `Decidable`, `Fintype`, `Encodable` linters	awaiting-bench t-linter t-meta merge-conflict awaiting-author	151/25	16	67	nobody	2024-11-19 08:47 (4 days ago)
18197	joelriou	feat(Algebra/Category/ModuleCat): the pseudofunctors which send a ring to its category of modules	t-algebra t-category-theory merge-conflict awaiting-author	199/6	3	9	nobody	2024-11-19 09:57 (4 days ago)
18469	vihdzp	chore(SetTheory/Game/PGame): deprecate primed lemmas	t-set-theory maintainer-merge	39/27	5	2	nobody	2024-11-19 14:40 (4 days ago)
15915	vihdzp	chore(SetTheory/Ordinal/CantorNormalForm): `CNF.exponents` and `CNF.coeffs`	t-set-theory t-logic awaiting-author	117/44	1	32	nobody	2024-11-19 14:55 (4 days ago)
19053	vihdzp	feat(Order/InitialSeg): initial segments preserve successor limits	maintainer-merge t-order	92/5	4	11	nobody	2024-11-19 21:07 (4 days ago)
16543	CBirkbeck	feat(Analysis/NormedSpace/FunctionSeries): add eventually versions	t-analysis	37/0	1	25	nobody	2024-11-19 22:49 (4 days ago)
19250	pimotte	feat(Combinatorics/SimpleGraph/Matching): add `IsCycles` and `IsAlternating` with basic results	maintainer-merge t-combinatorics	83/0	1	15	nobody	2024-11-20 14:05 (3 days ago)
19189	YnirPaz	feat(SetTheory/Ordinal/Arithmetic): order isomorphism between omega and the natural numbers	t-set-theory	32/0	1	14	nobody	2024-11-20 18:47 (3 days ago)
18463	vihdzp	feat(SetTheory/Ordinal/Notation/FundamentalSequence): define type of fundamental sequences	t-set-theory t-order	188/1	3	2	nobody	2024-11-20 23:43 (2 days ago)
19259	YaelDillies	feat: `S ^ n = S` where `S` is a submonoid	t-algebra	30/5	2	5	nobody	2024-11-21 08:22 (2 days ago)
15466	LorenzoLuccioli	feat(Probability/Kernel): `Kernel.sectL` and `sectR`	t-measure-probability awaiting-author	113/0	2	15	nobody	2024-11-21 15:28 (2 days ago)
18672	TobiasLeichtfried	feat: add leftmost derivation in context free grammar	t-computability new-contributor merge-conflict	74401/35464	2589	16	nobody	2024-11-21 16:48 (2 days ago)
16675	xroblot	feat(Analysis/BoxIntegral): Add BoxPartition defined by subdivision of the integer lattice	t-analysis	294/0	3	26	MichaelStollBayreuth	2024-11-22 12:08 (1 days ago)
19205	Vierkantor	chore(Data/Finsupp): split off basic scalar multiplication	t-algebra delegated	105/54	3	15	nobody	2024-11-22 14:46 (1 days ago)
19275	eric-wieser	fix: if nolint files change, do a full rebuild	delegated	8/0	1	18	nobody	2024-11-22 21:22 (1 days ago)
17813	vihdzp	feat(SetTheory/Cardinal/Arithmetic): cardinality of ordinal exponential	t-set-theory	86/3	4	3	nobody	2024-11-23 01:00 (22 hours ago)
19350	kim-em	chore: split notation typeclasses out of Algebra.Group.Defs	t-algebra	219/191	4	3	nobody	2024-11-23 02:39 (20 hours ago)
19245	YaelDillies	feat: algebraic properties of `Finset.sup`	large-import t-order t-algebra	165/27	10	8	nobody	2024-11-23 11:16 (11 hours ago)
19373	pimotte	feat(Combinatorics/SimpleGraph/Path): add `IsPath.getVert_injOn`	maintainer-merge t-combinatorics	20/0	1	3	nobody	2024-11-23 13:35 (9 hours ago)
19387	PieterCuijpers	feat: introduce the missing notation for `AddHom`	maintainer-merge new-contributor t-algebra	6/1	1	3	nobody	2024-11-23 14:02 (8 hours ago)
19171	AntoineChambert-Loir	feat: additivize equivariance of morphisms of actions	maintainer-merge t-algebra	80/21	1	20	YaelDillies	2024-11-23 14:27 (8 hours ago)
19395	kim-em	chore: more simpNF cleanup	ready-to-merge delegated	35/93	18	10	nobody	2024-11-23 22:52 (9 minutes ago)