Helping out: short tasks

Would you like to help out at a PR, differently from reviewing? Here are some ideas:

take a look at PRs with just some mathlib-infrastructure-related CI failure: unless it's an infrastructure PR, these are spurious/not the PRs fault
take a look at PRs labelled help-wanted or please-adopt
If the author hasn't noticed, you can ask in a PR which just has a merge conflict, but would be reviewable otherwise. (Remember, that most contributors to mathlib are volunteers, contribute in their free time and often have other commitments — and that real-life events can happen!)
post a comment on a PR made from a fork, nicely asking them to re-submit it from a mathlib branch instead
check if any 'stale' PR by a new contributor benefits from support, such as help with failing CI or providing feedback on the code

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

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 looking for help

Number	Author	Title	Labels	+/-	📝	💬	Assignee(s)	Updated
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)
10303	grunweg	feat: three misc lemmas about Hausdorff distance	t-topology merge-conflict awaiting-author help-wanted	54/14	4	10	nobody	2024-07-31 08:14 (3 months ago)
9642	eric-wieser	refactor(Analysis/Normed/{Group/Field}/Basic): Let `extends` generate the repeated fields	t-analysis merge-conflict awaiting-author WIP help-wanted	122/202	17	11	nobody	2024-07-31 08:14 (3 months ago)
6859	MohanadAhmed	TryLean4Bundle: Windows Bundle Creator	CI WIP help-wanted	114/0	2	0	nobody	2024-07-31 08:14 (3 months ago)
6791	eric-wieser	refactor: Use flat structures for morphisms	awaiting-CI merge-conflict awaiting-author help-wanted	174/201	32	0	nobody	2024-07-31 08:14 (3 months ago)
6931	urkud	refactor(Analysis/Normed): use `RingHomIsometric` for `.norm_cast`	t-analysis merge-conflict help-wanted	78/68	8	0	nobody	2024-07-31 08:14 (3 months ago)
5934	eric-wieser	feat: port Data.Rat.MetaDefs	t-meta merge-conflict mathlib-port help-wanted	183/0	3	4	nobody	2024-07-31 08:14 (3 months ago)
5863	eric-wieser	feat: add elaborators for concrete matrices	t-meta merge-conflict help-wanted	299/1	5	4	nobody	2024-07-31 08:14 (3 months ago)
7300	ah1112	feat: synthetic geometry	t-euclidean-geometry awaiting-author help-wanted	2657/0	4	71	nobody	2024-07-31 08:14 (3 months ago)
7903	urkud	feat: define `UnboundedSpace`	t-topology merge-conflict help-wanted	111/59	6	1	nobody	2024-08-07 11:34 (3 months ago)
9444	erdOne	feat: Various instances regarding `𝓞 K`.	t-number-theory merge-conflict help-wanted	27/0	2	9	nobody	2024-08-15 11:04 (3 months ago)
9040	BoltonBailey	feat: `to_snoc` an attribute for generating lemmas with snoc in them	t-meta please-adopt WIP help-wanted	1292/0	1	0	nobody	2024-08-15 11:08 (3 months ago)
5919	MithicSpirit	feat: implement orthogonality for AffineSubspace	t-analysis WIP help-wanted	330/0	2	4	MithicSpirit	2024-08-15 11:13 (3 months ago)
8738	grunweg	feat: differential of a local diffeomorphism is a continuous linear equivalence	t-differential-geometry awaiting-author help-wanted	132/11	2	15	nobody	2024-09-06 22:40 (2 months ago)
10765	Vierkantor	feat(Tactic): `ring` modulo a given characteristic	t-meta merge-conflict awaiting-author help-wanted	275/108	5	7	joneugster	2024-09-11 13:16 (2 months ago)
18508	urkud	chore(OperatorNorm/Completeness): drop a duplicate instance	t-analysis help-wanted	5/21	6	13	nobody	2024-11-06 22:04 (17 days ago)
14739	urkud	feat(Measure): add `gcongr` lemmas	t-measure-probability merge-conflict awaiting-author WIP help-wanted	12/8	5	3	nobody	2024-11-16 08:45 (7 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 (3 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 (11 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 (6 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 (5 hours 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)

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)