Mathlib review and triage dashboard

Welcome to the mathlib review and triage dashboard. This is a prototype for better exposing the currently open PRs to mathlib. Feedback (including bug reports and ideas for improvements) on this dashboard is very welcome, for instance directly on the github repository.
This dashboard was last updated on: November 23, 2024 at 22:43 UTC

Quick links: PR statistics | queue | queue-new-contributors | queue-easy | queue-stale-unassigned | queue-stale-unassigned | all-ready-to-merge | stale-ready-to-merge | stale-delegated | stale-maintainer-merge | tech-debt | needs-decision | needs-merge | inessential-CI-fails | stale-new-contributor | needs-owner | other-base | from-fork | bad-title | unlabelled | contradictory-labels | approved

Overall statistics

Found 1121 open PRs overall. Among these PRs

Review queue

Number Author Title Labels +/- 📝 💬 Assignee(s) Updated
18470 FR-vdash-bot perf: lower the priority of `Normed*.to*` instances slow-typeclass-synthesis t-algebra t-analysis 28/0 2 7 nobody 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 nobody 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 nobody 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 nobody 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 nobody 2024-11-06 19:49 (17 days ago)
13786 Multramate feat(NumberTheory/EllipticDivisibilitySequence): extend even-odd recursion to integers t-number-theory 360/230 5 n/a faenuccio 2024-11-06 22:02 (17 days ago)
18713 dwrensha doc: update README.md instructions for building documentation locally 10/7 1 1 nobody 2024-11-07 01:14 (16 days ago)
18432 joelriou feat(Algebra/Module): presentation of the tensor product t-algebra 111/0 2 2 nobody 2024-11-07 15:05 (16 days ago)
18756 FR-vdash-bot refactor: deprecate `DistribMulActionSemiHomClass` `MulSemiringActionSemiHomClass` t-algebra 50/28 3 4 nobody 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 nobody 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 nobody 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 nobody 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 nobody 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 nobody 2024-11-09 19:08 (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)
17308 YaelDillies feat: Decomposing a submodule of a product t-algebra 62/0 1 9 loefflerd 2024-11-10 20:24 (13 days ago)
18315 urkud chore(Filter/Prod): drop `Filter.prod`, use `SProd` instead t-order t-topology 48/91 10 2 nobody 2024-11-11 02:21 (12 days ago)
18849 sgouezel feat: manifold derivative of operations in vector spaces t-differential-geometry 278/0 2 1 nobody 2024-11-11 09:17 (12 days ago)
17986 adomani feat: the `#find_syntax` command t-meta 167/0 4 1 nobody 2024-11-11 13:18 (12 days ago)
18818 edegeltje feat(Data/Control/Traversable/Instances): Add (Lawful)Traversable instance for Tree t-data 79/6 2 1 nobody 2024-11-11 15:29 (12 days ago)
9082 Timeroot feat: `List.destutter` on cotransitive relations. t-data 200/1 4 52 nobody 2024-11-12 10:37 (11 days ago)
18749 Vegan-Parabola feat(ModelTheory): preparation work for proving existence of fraisse limits t-logic 278/4 5 3 nobody 2024-11-12 11:51 (11 days ago)
18416 erdOne feat(RingTheory): the residue field of a prime ideal t-algebra 104/0 2 1 nobody 2024-11-12 16:03 (11 days ago)
18693 Ruben-VandeVelde feat: add ConjRootClass t-algebra 199/0 3 1 nobody 2024-11-12 18:47 (11 days ago)
17956 joelriou feat(CategoryTheory/Monoidal): composition of monoidal category adjunctions t-category-theory 62/7 2 3 nobody 2024-11-12 19:09 (11 days ago)
16656 mo271 feat(Data/Fintype/List): generalize `fintypeNodupList` (no `DecidableEq`) t-data 64/21 1 4 nobody 2024-11-12 21:57 (11 days ago)
15424 pechersky feat(Valued/LocallyCompact): `totallyBounded_iff_finite_residueField` t-algebra 156/0 3 n/a nobody 2024-11-13 02:28 (10 days ago)
16797 Command-Master feat(FieldTheory/Differential/Liouville): prove the algebraic case of Liouville's theorem large-import t-algebra 262/6 3 n/a nobody 2024-11-13 06:37 (10 days ago)
18954 Command-Master feat(Algebra/Order/AddGroupWithTop): lemmas about LinearOrderedAddCommGroupWithTop t-algebra 28/0 1 1 nobody 2024-11-13 08:07 (10 days ago)
16979 Thmoas-Guan feat(FieldTheory/Galois): Lemmas of galois theory t-algebra 94/3 4 34 nobody 2024-11-13 11:20 (10 days ago)
9651 acmepjz feat(FieldTheory/LinearDisjoint): definition and basic properties of linearly disjoint of fields t-algebra 362/0 2 n/a nobody 2024-11-13 11:52 (10 days ago)
18763 sven-manthe feat: define Descriptive.Tree t-logic 87/0 3 1 nobody 2024-11-13 15:54 (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)
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)
18893 vihdzp feat(Order/InitialSeg): `InitialSeg.exists_relIso_sum` t-order 54/9 4 2 nobody 2024-11-14 03:56 (9 days ago)
18988 TwoFX feat: ind-objects are closed under products t-category-theory 230/0 3 2 nobody 2024-11-14 05:48 (9 days ago)
18266 bjoernkjoshanssen feat: Second-derivative test from calculus t-analysis 151/0 3 2 nobody 2024-11-14 07:48 (9 days ago)
18822 YaelDillies feat: vertical line test for group/module homomorphisms t-algebra 326/1 5 7 nobody 2024-11-14 09:53 (9 days ago)
19021 joelriou feat(CategoryTheory): limits of eventually constant functors from cofiltered categories t-category-theory 285/0 3 1 nobody 2024-11-14 10:21 (9 days ago)
19024 jjaassoonn feat(Algebra/Category/ModuleCat/Products): show that arbitrary coproducts agree with direct sum large-import t-algebra 50/0 1 1 nobody 2024-11-14 11:06 (9 days ago)
17859 YaelDillies feat: family of kernels consistent with respect to a filtration t-measure-probability 24/0 2 4 RemyDegenne 2024-11-14 12:20 (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)
10668 FLDutchmann feat: Define `Nat.finMulAntidiagonal`, the `Finset` of tuples of naturals with a fixed product. t-combinatorics t-number-theory 250/1 5 33 nobody 2024-11-14 14:51 (9 days ago)
19041 Vegan-Parabola chore (ModelTheory/Fraisse): simplify IsFraisse definition t-logic easy 12/10 1 1 nobody 2024-11-14 18:02 (9 days ago)
18812 adomani feat(bench summary): report no significant changes and job_id CI 12/4 2 10 nobody 2024-11-14 22:30 (9 days ago)
19062 hannahfechtner feat (Algebra/PresentedMonoid/Basic) : facts about rel t-algebra 39/0 1 1 nobody 2024-11-15 01:20 (8 days ago)
18689 Thmoas-Guan feat(Topology): Introduce HomeomorphClass t-topology 41/0 2 21 nobody 2024-11-15 06:04 (8 days ago)
17781 robin-carlier feat(CategoryTheory/Limits/Sifted): characterization of sifted categories large-import t-category-theory 232/2 1 2 nobody 2024-11-15 06:44 (8 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)
18531 acmepjz refactor(AlgebraicGeometry/EllipticCurve/*): add `WeierstrassCurve.IsElliptic` and remove `EllipticCurve` t-algebraic-geometry 268/340 6 30 Multramate 2024-11-15 07:38 (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)
18437 ADedecker refactor: add refactored APIs for algebraic filter bases t-algebra t-topology 663/0 5 4 PatrickMassot 2024-11-15 09:49 (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)
18490 xroblot feat(Analysis/PolarCoord): add versions for Lebesgue integral t-analysis 39/17 1 10 nobody 2024-11-15 13:30 (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)
18590 joelriou feat(LinearAlgebra/ExteriorPower): the universal property of the exterior power t-algebra 256/0 3 1 nobody 2024-11-15 17:49 (8 days ago)
14501 jjaassoonn feat: module structure of filtered colimit of abelian groups over filtered colimit of rings workshop-AIM-AG-2024 t-algebra t-category-theory 439/2 2 48 joelriou 2024-11-15 19:45 (8 days ago)
19106 TwoFX feat: a fan is limit iff it is after the application of coyoneda.obj X large-import t-category-theory 50/2 1 2 nobody 2024-11-15 20:03 (8 days ago)
18711 bjoernkjoshanssen feat: One-point compactification of Euclidean space homeomorphic to sphere t-differential-geometry 92/0 2 3 nobody 2024-11-15 20:36 (8 days ago)
18501 joelriou feat(Algebra/Homology): the stupid truncation of homological complexes large-import t-algebra t-category-theory 115/1 3 2 nobody 2024-11-16 21:22 (7 days ago)
19129 adomani feat: `#trans_import` shows the imports of the current module t-meta 43/0 4 4 nobody 2024-11-16 21:24 (7 days ago)
18990 YaelDillies feat: sup-closed sets are closed under finite suprema t-order 65/1 1 6 nobody 2024-11-16 22:21 (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 (6 days ago)
18794 ScottCarnahan feat (RingTheory/HahnSeries/Summable) add pointwise product operation t-algebra 66/11 1 4 nobody 2024-11-17 00:17 (6 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)
15989 vihdzp feat(SetTheory/Ordinal/Principal): simplify characterization of additively principal ordinals t-set-theory t-logic 67/63 2 2 nobody 2024-11-17 07:22 (6 days ago)
18677 IvanRenison feat(Combinatorics/SimpleGraph): Add definitions and theorems about the coloring of sum graphs large-import t-combinatorics 79/0 2 6 nobody 2024-11-17 11:37 (6 days ago)
19154 TwoFX feat: coproducts in the category of Ind-objects large-import t-category-theory 80/3 1 1 nobody 2024-11-17 15:55 (6 days ago)
18389 joelriou feat(Algebra/Module): presentation of the restriction of scalars of a module t-algebra 68/0 2 3 nobody 2024-11-17 17:05 (6 days ago)
18414 joelriou feat(CategoryTheory/Enriched): functoriality of the enrichment of functor categories t-category-theory 125/3 1 3 nobody 2024-11-17 17:30 (6 days ago)
19133 seewoo5 feat: `isCoprime_mul_units_left`, `isCoprime_mul_units_right` t-algebra 18/6 1 5 seewoo5 2024-11-17 19:02 (6 days ago)
19170 peakpoint feat(Analysis/Convex/Topology): closure of interior and interior of closure for a convex set new-contributor t-topology 24/0 1 1 nobody 2024-11-17 21:17 (6 days ago)
18178 yoh-tanimoto feat(Analysis/Normed/Group/SeparationQuotient): add normed lifts and `mk` large-import t-analysis 218/4 6 48 nobody 2024-11-17 22:08 (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)
18985 sven-manthe feat: relate lists and infinite sequences t-data 116/0 2 4 nobody 2024-11-18 02:20 (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)
17325 b-mehta feat(Data/Nat): faster computation of Nat.log t-data 113/0 1 24 nobody 2024-11-18 02:48 (5 days ago)
19179 dwrensha feat: add Nat.digits_base_pow_mul and Nat.digits_append_zeroes_append_digits t-data 20/0 1 1 nobody 2024-11-18 03:12 (5 days ago)
19180 tb65536 feat(GroupTheory/SpecificGroups/Cyclic): Cardinality of automorphism group t-algebra 37/0 3 1 nobody 2024-11-18 05:50 (5 days ago)
18434 ChrisHughes24 chore(IsAlgClosed/Classification): Make theorems more universe polymorphic t-algebra 72/53 2 1 nobody 2024-11-18 07:14 (5 days ago)
19139 mbkybky feat(RingTheory/Ideal/Over): define the set of all prime ideals that lie over an ideal t-algebra 125/3 4 4 nobody 2024-11-18 08:20 (5 days ago)
19092 Vierkantor chore(Data/Finsupp): split off extensionality from `Defs.lean` t-data 74/45 4 3 nobody 2024-11-18 09:43 (5 days ago)
14060 YnirPaz feat(SetTheory/Ordinal/Clubs): define club sets and prove basic properties new-contributor t-logic 303/3 5 91 nobody 2024-11-18 10:52 (5 days ago)
19096 chrisflav feat(AlgebraicGeometry): covers of schemes over a base t-algebraic-geometry 251/1 6 3 nobody 2024-11-18 10:54 (5 days ago)
19201 YaelDillies feat(MvPolynomial): more lemmas about `finSuccEquiv` t-algebra 33/10 2 1 nobody 2024-11-18 12:22 (5 days ago)
19031 Vierkantor chore(Data/Set): split the `CoeSort` instance to its own file t-data 44/16 6 3 nobody 2024-11-18 12:54 (5 days ago)
19199 dagurtomas feat(CategoryTheory): split up a product into a binary product t-category-theory 70/0 2 2 nobody 2024-11-18 13:40 (5 days ago)
18563 hannahfechtner feat(Algebra/FreeMonoid): free monoids over isomorphic types are isomorphic new-contributor t-algebra 41/0 1 29 nobody 2024-11-18 13:44 (5 days ago)
17995 kex-y feat(MeasureTheory/Measure/MutuallySingular): Disjoint iff mutually singular t-measure-probability 185/5 4 4 nobody 2024-11-18 15:20 (5 days ago)
19058 chrisflav feat(Algebra/Category): API for `Under R` t-algebra t-category-theory 254/6 7 8 nobody 2024-11-18 17:24 (5 days ago)
16160 CBirkbeck feat: representatives for the `FixedDetMatrices` under SL action t-algebra 226/1 1 41 nobody 2024-11-18 19:23 (5 days ago)
19009 eric-wieser chore(Util/Superscript): use `register_parser_alias` t-meta easy 2/6 1 1 nobody 2024-11-18 21:05 (5 days ago)
19006 tb65536 feat(GroupTheory/Subgroup/Centralizer): The `N/C` theorem large-import t-algebra 20/0 1 10 nobody 2024-11-18 23:04 (4 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)
18778 vihdzp feat(SetTheory/Cardinal/Arithmetic): omega ordinals are additively/multiplicatively principal t-set-theory 34/15 2 2 nobody 2024-11-18 23:23 (4 days ago)
19232 eric-wieser refactor(Algebra/Bilinear): generalize to non-commutative base rings t-algebra 142/110 2 4 nobody 2024-11-19 01:31 (4 days ago)
19122 Command-Master feat(Algebra/Order/Monoid/Unbundled/WithTop): add lemmas about `WithTop.map` and `WithBot.map` t-algebra 66/0 2 3 nobody 2024-11-19 04:56 (4 days ago)
18510 datokrat feat(CategoryTheory/Abelian/GrothendieckAxioms): introduce grothendieck categories new-contributor t-category-theory 83/6 4 4 nobody 2024-11-19 06:12 (4 days ago)
19237 vihdzp chore(SetTheory/Ordinal/NaturalOps): address porting notes t-set-theory 45/67 1 1 nobody 2024-11-19 07:32 (4 days ago)
19066 vihdzp feat(SetTheory/Ordinal/Nimber/Field): Nimber division t-set-theory maintainer-merge 127/2 2 9 nobody 2024-11-19 08:48 (4 days ago)
19244 riccardobrasca feat: generalize `Ideal.spanNorm` to allow non free extensions t-algebra 158/59 4 2 nobody 2024-11-19 12:17 (4 days ago)
19236 vihdzp refactor(SetTheory/Ordinal/NaturalOps): redefine natural addition without `blsub` t-set-theory maintainer-merge 74/45 4 2 nobody 2024-11-19 12:31 (4 days ago)
14411 haitian-yuki feat(Data/Multiset/Order): add Dershowitz-Manna Ordering and Theorem t-data new-contributor 293/0 2 86 YaelDillies 2024-11-19 12:55 (4 days ago)
19248 YaelDillies feat: `MulLeftMono` implies `PosMulMono` t-order t-algebra 24/0 1 1 nobody 2024-11-19 14:02 (4 days ago)
18775 yoh-tanimoto feat(MeasureTheory/Integral/RieszMarkovKakutani) prove that the Riesz content is indeed a content for `NNReal` large-import t-measure-probability 205/14 2 n/a nobody 2024-11-19 14:16 (4 days ago)
18238 vihdzp refactor(Order/WellFounded): deprecate `WellFounded.succ` maintainer-merge t-order 12/4 1 2 nobody 2024-11-19 14:37 (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)
19193 YaelDillies refactor: make `LinearOrderedCommMonoidWithZero` extend `OrderBot` t-order t-algebra 51/44 3 3 nobody 2024-11-19 15:32 (4 days ago)
18102 j-loreaux refactor: add a `ContinuousSqrt` class to conclude `StarOrderedRing C(α, R)` large-import t-analysis t-topology 110/73 11 13 nobody 2024-11-19 17:27 (4 days ago)
19047 joelriou feat(CategoryTheory/SmallObject/Iteration): existence of objects (bot and succ cases) t-category-theory 260/0 3 2 nobody 2024-11-19 19:30 (4 days ago)
19221 j-loreaux feat: expand API for `CFC.posPart` t-analysis 130/11 1 2 nobody 2024-11-19 20:25 (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)
18235 vihdzp feat(SetTheory/Ordinal/Basic): notation `typeLT α = type (α := α) (· < ·)` t-set-theory maintainer-merge 13/10 2 2 nobody 2024-11-19 21:58 (4 days ago)
19266 vihdzp doc(SetTheory/ZFC/Ordinal): add docstrings to lemmas on transitive sets t-set-theory easy documentation 5/1 1 1 nobody 2024-11-19 22:48 (3 days ago)
16543 CBirkbeck feat(Analysis/NormedSpace/FunctionSeries): add eventually versions t-analysis 37/0 1 25 nobody 2024-11-19 22:49 (3 days ago)
19108 eric-wieser refactor: allow `deriv` to be used on topological vector spaces t-analysis 103/42 11 9 nobody 2024-11-19 23:38 (3 days ago)
19136 hrmacbeth feat: handle scalar multiplication in `linear_combination` large-import t-meta 135/41 7 3 nobody 2024-11-20 01:40 (3 days ago)
17142 peabrainiac feat(Geometry/Manifold): manifolds are locally path-connected large-import new-contributor t-topology t-differential-geometry 61/9 6 5 nobody 2024-11-20 05:26 (3 days ago)
19240 nomeata refactor(Nat.Prime.Defs): use `csimp` for `Nat.decidablePrime` t-number-theory 16/17 1 2 nobody 2024-11-20 08:02 (3 days ago)
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)
19252 YaelDillies feat(Pointwise): monotonicity of `pow` t-algebra 252/110 25 2 nobody 2024-11-20 12:58 (3 days ago)
19212 Julian feat(LinearAlgebra): add a variable_alias for VectorSpace t-algebra 25/0 3 10 nobody 2024-11-20 13:09 (3 days ago)
19271 chrisflav feat(CategoryTheory): pushforward pullback adjunction for `P.Over Q X` t-category-theory 289/2 5 1 nobody 2024-11-20 13:59 (3 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)
18534 joelriou feat(LinearAlgebra/PiTensorProduct): dependent version of tmulEquiv t-algebra 202/151 6 27 nobody 2024-11-20 14:42 (3 days ago)
18615 j-loreaux feat: add `NonUnital{Star}Algebra.elemental` subalgebras t-algebra t-topology 129/0 2 2 nobody 2024-11-20 14:55 (3 days ago)
18506 j-loreaux feat: approximate units in C⋆-algebras t-analysis 292/11 4 6 nobody 2024-11-20 15:34 (3 days ago)
19298 ScottCarnahan feat(Algebra/Vertex): Define vertex operators t-algebra 110/0 3 1 nobody 2024-11-20 16:34 (3 days ago)
19068 j-loreaux feat: prove Dini's theorem for uniform convergence t-topology 163/0 4 16 nobody 2024-11-20 18:16 (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)
17930 alreadydone refactor: introduce `Ideal.IsTwoSided` class for quotients of noncommutative rings t-algebra 445/273 22 61 nobody 2024-11-20 19:05 (3 days ago)
19302 fpvandoorn fix(to_additive): automatically translate all instances generated by `extends` 20/39 6 1 nobody 2024-11-20 20:01 (3 days ago)
19307 mo271 feat(LinearAlgebra/Matrix/Permanent): smul large-import t-algebra 42/2 1 1 nobody 2024-11-20 20:43 (3 days ago)
19306 joelriou feat(CategoryTheory/MorphismProperty): classes of morphisms that are stable under transfinite compositions t-order t-category-theory 120/0 2 1 nobody 2024-11-20 20:47 (3 days ago)
19115 alreadydone chore: allow Module over Semiring be Flat t-algebra 69/50 5 1 nobody 2024-11-20 21:10 (3 days ago)
19310 alreadydone chore(RingTheory/Localization): golfs and generalizations t-algebra 65/68 7 1 nobody 2024-11-20 21:59 (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)
18206 vihdzp chore(SetTheory/Ordinal/Basic): golf/clean up `Cardinal.ord` theorems t-set-theory 48/57 1 1 nobody 2024-11-20 23:43 (2 days ago)
19227 adomani fix(CI): unwrap `lake test` in problem matcher CI 9/20 5 1 nobody 2024-11-20 23:51 (2 days ago)
18933 vihdzp feat(SetTheory/Cardinal/Arithmetic): miscellaneous cardinality lemmas t-set-theory 27/0 2 4 nobody 2024-11-21 00:14 (2 days ago)
19146 ChrisHughes24 feat: Polynomial.isRoot_of_isRoot_iff_dvd_derivative_mul t-algebra 51/0 2 3 nobody 2024-11-21 06:11 (2 days ago)
17001 vihdzp feat(SetTheory/ZFC/Ordinal): Alternate characterizations of ordinals large-import t-set-theory 157/20 3 2 nobody 2024-11-21 06:31 (2 days ago)
19323 madvorak feat: Function to Sum decomposition t-data -1/-1 -1 n/a nobody 2024-11-21 08:18 (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)
19023 madvorak chore(Data/Set/Basic): remove redundant redeclarations t-data 70/69 2 9 nobody 2024-11-21 08:43 (2 days ago)
18172 mariainesdff feat(Topology/EMetricSpace/Basic): add boundedness lemmas t-analysis 49/2 3 16 nobody 2024-11-21 10:47 (2 days ago)
19330 joelriou feat(CategoryTheory): construction of sections of functors by transfinite induction t-order t-category-theory 273/0 2 1 nobody 2024-11-21 11:14 (2 days ago)
19325 madvorak style(Computability/ContextFreeGrammar/reverse): injective and surjec… t-computability easy 4/4 1 2 nobody 2024-11-21 17:56 (2 days ago)
19065 chrisflav refactor(Algebra/Category): turn homs in `AlgebraCat` into a structure t-algebra t-category-theory 195/161 7 121 nobody 2024-11-21 18:08 (2 days ago)
19164 Command-Master Add `toWithTop`, `ofWithTop` t-data RFC 58/0 1 1 nobody 2024-11-22 04:33 (1 days ago)
19149 Command-Master feat: add `ENat.map` and lemmas t-data RFC 116/16 4 1 nobody 2024-11-22 04:33 (1 days ago)
19277 jcommelin chore(Order/ConditionallyCompleteLattice): split off `Defs.lean` from `Basic.lean` t-order 255/217 4 1 nobody 2024-11-22 05:30 (1 days ago)
19357 sgouezel feat: the pullback of a vector field in a vector space t-analysis 229/1 1 1 nobody 2024-11-22 07:35 (1 days ago)
19312 chrisflav feat(CategoryTheory/Over): more API for `post` t-category-theory 181/0 1 5 nobody 2024-11-22 07:50 (1 days ago)
19222 mans0954 feat(Order/Directed): DirectedOn and products t-order 62/0 1 1 nobody 2024-11-22 07:52 (1 days ago)
19150 mans0954 feat(Order/Bounds/Lattice): Bounds over collections of sets t-order 66/0 2 1 nobody 2024-11-22 07:52 (1 days ago)
19343 ScottCarnahan feat(LinearAlgebra/RootSystem/Finite): Coxeter weights are bounded above by 4 t-algebra 127/1 3 2 nobody 2024-11-22 07:59 (1 days ago)
9013 winstonyin feat: uniform time lemma for the existence of global integral curves maintainer-merge t-differential-geometry -1/-1 -1 n/a nobody 2024-11-22 10:52 (1 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)
19364 Vierkantor chore(RingTheory/Noetherian): further split `Defs.lean` t-algebra 376/298 11 2 nobody 2024-11-22 13:19 (1 days ago)
19367 adomani test: try emoji action CI 58/11 2 2 nobody 2024-11-22 14:54 (1 days ago)
19374 sgouezel chore: avoid importing `ContDiff.Defs` in `FDeriv.Analytic` t-analysis 153/82 8 1 nobody 2024-11-22 16:25 (1 days ago)
19376 Vierkantor chore(Algebra/Polynomial): don't import `Ideal` when defining `Polynomial.roots` t-algebra 214/129 26 1 nobody 2024-11-22 17:04 (1 days ago)
17732 eric-wieser feat: notation for Euclidean space t-analysis 73/6 5 5 nobody 2024-11-22 21:32 (1 days ago)
19342 Ruben-VandeVelde chore: split out Algebra.GroupWithZero.Nat 95/32 9 3 nobody 2024-11-22 23:02 (23 hours ago)
19384 grunweg refactor(lint-style): make sure to read the nolints file outside of t… t-linter 13/6 2 2 nobody 2024-11-22 23:46 (22 hours ago)
17813 vihdzp feat(SetTheory/Cardinal/Arithmetic): cardinality of ordinal exponential t-set-theory 86/3 4 3 nobody 2024-11-23 01:00 (21 hours ago)
19296 sgouezel chore: remove the `Smooth` alias for infinitely differentiable functions between manifolds t-differential-geometry 495/742 27 10 nobody 2024-11-23 01:04 (21 hours ago)
19080 su00000 feat(RingTheory/LocalProperties): Add theorems about LocalizedModule new-contributor t-algebra 316/25 5 24 nobody 2024-11-23 01:47 (20 hours ago)
19362 winstonyin feat: locally compact manifolds are finite-dimensional t-differential-geometry 36/4 1 7 nobody 2024-11-23 02:20 (20 hours 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)
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)
18578 mans0954 feat(LinearAlgebra/QuadraticForm/Basis): basis expansion of a quadratic map t-algebra 75/0 1 6 nobody 2024-11-23 04:41 (18 hours ago)
19393 LeoDog896 feat:(SetTheory/Game/PGame): down and up games t-set-theory 51/0 1 1 nobody 2024-11-23 08:46 (13 hours ago)
19377 pimotte feat(Combinatorics/SimpleGraph): add lemmas about `spanningCoe` t-combinatorics 26/0 3 4 nobody 2024-11-23 10:19 (12 hours ago)
19397 IvanRenison feat(Algebra/Ring/Parity): Add lemma `odd_add_self_sub_one` t-algebra easy 2/0 1 1 nobody 2024-11-23 10:57 (11 hours ago)
17097 LorenzoLuccioli feat: measurability of addition and multiplication on `EReal` t-measure-probability 76/0 2 23 nobody 2024-11-23 11:09 (11 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)
19293 YaelDillies feat: more `eLpNorm` API t-measure-probability 75/27 2 1 nobody 2024-11-23 11:22 (11 hours ago)
19399 YaelDillies feat(GroupTheory): some lemmas about blocks t-algebra 35/1 1 1 nobody 2024-11-23 11:44 (10 hours ago)
19388 eric-wieser chore: make map_ofNat a simp lemma t-algebra 2/0 1 6 nobody 2024-11-23 11:55 (10 hours ago)
19403 YaelDillies chore: rename `Codisjoint_comm` to `codisjoint_comm` t-order easy 7/5 4 1 nobody 2024-11-23 12:31 (10 hours ago)
19406 YaelDillies feat: `{a, b} * s = a • s ∪ b • s` t-algebra 34/6 1 1 nobody 2024-11-23 12:50 (9 hours ago)
19407 YaelDillies feat: `(t \ s).ncard = t.ncard - s.ncard` in a ring t-data 9/2 1 1 nobody 2024-11-23 12:56 (9 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)
19410 eric-wieser doc: describe why map_ofNat can't be simp (yet) t-data 5/0 1 1 nobody 2024-11-23 13:45 (8 hours ago)
19321 jcommelin chore: change associativity of `+ᵥ` from `infixl` to `infixr` 40/37 12 6 nobody 2024-11-23 13:56 (8 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)
19401 YaelDillies chore: rename `forall_image2_iff` to `forall_mem_image2` 51/39 13 1 nobody 2024-11-23 14:35 (8 hours ago)
19371 adomani feat: trigger automated Zulip emojis via `bors x` command CI 103/51 3 2 nobody 2024-11-23 14:41 (8 hours ago)
18691 erdOne feat: the free locus of a (finitely presented) module large-import t-algebra 379/6 7 9 nobody 2024-11-23 15:04 (7 hours ago)
18836 jsm28 feat(Data/Nat/Nth): `nth_add_one` t-data 53/0 1 3 nobody 2024-11-23 15:17 (7 hours ago)
19200 dagurtomas feat(CategoryTheory): expand the API for AB axioms large-import t-category-theory 251/42 2 4 nobody 2024-11-23 15:39 (7 hours ago)
19412 YaelDillies feat: growth of a finset in the quotient and intersection with a subgroup t-combinatorics 81/0 2 1 nobody 2024-11-23 15:51 (6 hours ago)
15874 vihdzp doc(Order/InitialSeg): Improve documentation t-order documentation 40/44 2 25 nobody 2024-11-23 15:55 (6 hours ago)
19398 YaelDillies feat: `Icc a b + Icc c d = Icc (a + c) (b + d)` t-order t-algebra 86/27 7 6 nobody 2024-11-23 15:56 (6 hours ago)
19411 YaelDillies feat: `Polynomial.map f` strictly decreases the degree if `f p.leadingCoeff = 0` t-algebra 61/44 13 2 nobody 2024-11-23 16:29 (6 hours ago)
19417 vihdzp chore(SetTheory/Game/Ordinal): make `Ordinal.toGame` an order embedding t-set-theory 20/19 2 1 nobody 2024-11-23 19:03 (3 hours ago)
19378 adamtopaz feat: Explanation widgets t-meta 101/0 3 5 nobody 2024-11-23 19:21 (3 hours ago)
19413 adomani chore: remove unused variables 83/106 54 1 nobody 2024-11-23 19:32 (3 hours ago)
19303 FMLJohn feat(RingTheory/Polynomial/Hilbert): the definition of the Hilbert polynomial in terms of a natural number `d` and a polynomial `p : ℤ[X]` t-algebra t-algebraic-geometry 103/6 5 7 nobody 2024-11-23 19:35 (3 hours ago)
19420 vihdzp feat: AM-HM inequality t-algebra 36/2 2 1 nobody 2024-11-23 20:15 (2 hours ago)
19419 erdOne feat(AlgebraicGeometry): integral = universally closed + affine large-import t-algebraic-geometry 127/4 4 2 nobody 2024-11-23 20:43 (2 hours ago)
19358 urkud chore(Filter): move defs of `Filter.IsBounded` etc t-order t-topology easy 36/32 4 1 nobody 2024-11-23 21:50 (53 minutes ago)

New contributors' PRs on the queue

Number Author Title Labels +/- 📝 💬 Assignee(s) Updated
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)
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)
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)
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)
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)
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 (6 days ago)
19170 peakpoint feat(Analysis/Convex/Topology): closure of interior and interior of closure for a convex set new-contributor t-topology 24/0 1 1 nobody 2024-11-17 21:17 (6 days ago)
14060 YnirPaz feat(SetTheory/Ordinal/Clubs): define club sets and prove basic properties new-contributor t-logic 303/3 5 91 nobody 2024-11-18 10:52 (5 days ago)
18563 hannahfechtner feat(Algebra/FreeMonoid): free monoids over isomorphic types are isomorphic new-contributor t-algebra 41/0 1 29 nobody 2024-11-18 13:44 (5 days ago)
18510 datokrat feat(CategoryTheory/Abelian/GrothendieckAxioms): introduce grothendieck categories new-contributor t-category-theory 83/6 4 4 nobody 2024-11-19 06:12 (4 days ago)
14411 haitian-yuki feat(Data/Multiset/Order): add Dershowitz-Manna Ordering and Theorem t-data new-contributor 293/0 2 86 YaelDillies 2024-11-19 12:55 (4 days ago)
17142 peabrainiac feat(Geometry/Manifold): manifolds are locally path-connected large-import new-contributor t-topology t-differential-geometry 61/9 6 5 nobody 2024-11-20 05:26 (3 days ago)
19080 su00000 feat(RingTheory/LocalProperties): Add theorems about LocalizedModule new-contributor t-algebra 316/25 5 24 nobody 2024-11-23 01:47 (20 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)

PRs on the review queue labelled 'easy'

Number Author Title Labels +/- 📝 💬 Assignee(s) Updated
19041 Vegan-Parabola chore (ModelTheory/Fraisse): simplify IsFraisse definition t-logic easy 12/10 1 1 nobody 2024-11-14 18:02 (9 days ago)
19009 eric-wieser chore(Util/Superscript): use `register_parser_alias` t-meta easy 2/6 1 1 nobody 2024-11-18 21:05 (5 days ago)
19266 vihdzp doc(SetTheory/ZFC/Ordinal): add docstrings to lemmas on transitive sets t-set-theory easy documentation 5/1 1 1 nobody 2024-11-19 22:48 (3 days ago)
19325 madvorak style(Computability/ContextFreeGrammar/reverse): injective and surjec… t-computability easy 4/4 1 2 nobody 2024-11-21 17:56 (2 days ago)
19397 IvanRenison feat(Algebra/Ring/Parity): Add lemma `odd_add_self_sub_one` t-algebra easy 2/0 1 1 nobody 2024-11-23 10:57 (11 hours ago)
19403 YaelDillies chore: rename `Codisjoint_comm` to `codisjoint_comm` t-order easy 7/5 4 1 nobody 2024-11-23 12:31 (10 hours ago)
19358 urkud chore(Filter): move defs of `Filter.IsBounded` etc t-order t-topology easy 36/32 4 1 nobody 2024-11-23 21:50 (53 minutes ago)

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

Number Author Title Labels +/- 📝 💬 Assignee(s) Updated
18470 FR-vdash-bot perf: lower the priority of `Normed*.to*` instances slow-typeclass-synthesis t-algebra t-analysis 28/0 2 7 nobody 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 nobody 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 nobody 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 nobody 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 nobody 2024-11-06 19:49 (17 days ago)
18713 dwrensha doc: update README.md instructions for building documentation locally 10/7 1 1 nobody 2024-11-07 01:14 (16 days ago)
18432 joelriou feat(Algebra/Module): presentation of the tensor product t-algebra 111/0 2 2 nobody 2024-11-07 15:05 (16 days ago)
18756 FR-vdash-bot refactor: deprecate `DistribMulActionSemiHomClass` `MulSemiringActionSemiHomClass` t-algebra 50/28 3 4 nobody 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 nobody 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 nobody 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 nobody 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 nobody 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 nobody 2024-11-09 19:08 (14 days ago)

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

Number Author Title Labels +/- 📝 💬 Assignee(s) Updated
13786 Multramate feat(NumberTheory/EllipticDivisibilitySequence): extend even-odd recursion to integers t-number-theory 360/230 5 n/a faenuccio 2024-11-06 22:02 (17 days ago)

All ready-to-merge'd PRs

Number Author Title Labels +/- 📝 💬 Assignee(s) Updated
19130 erdOne chore(AlgebraicGeometry) add `Scheme.Hom.appTop` t-algebraic-geometry ready-to-merge 214/174 13 13 nobody 2024-11-23 22:16 (27 minutes ago)

Stale ready-to-merge'd PRs

There are currently no stale PRs labelled auto-merge-after-CI or ready-to-merge. Congratulations!

Stale delegated PRs

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)

Stale maintainer-merge'd PRs

Number Author Title Labels +/- 📝 💬 Assignee(s) Updated
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)
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)
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)
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)
19066 vihdzp feat(SetTheory/Ordinal/Nimber/Field): Nimber division t-set-theory maintainer-merge 127/2 2 9 nobody 2024-11-19 08:48 (4 days ago)
19236 vihdzp refactor(SetTheory/Ordinal/NaturalOps): redefine natural addition without `blsub` t-set-theory maintainer-merge 74/45 4 2 nobody 2024-11-19 12:31 (4 days ago)
18238 vihdzp refactor(Order/WellFounded): deprecate `WellFounded.succ` maintainer-merge t-order 12/4 1 2 nobody 2024-11-19 14:37 (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)
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)
18235 vihdzp feat(SetTheory/Ordinal/Basic): notation `typeLT α = type (α := α) (· < ·)` t-set-theory maintainer-merge 13/10 2 2 nobody 2024-11-19 21:58 (4 days ago)
18208 vihdzp chore(SetTheory/Ordinal/Basic): deprecate results on `WellOrder` t-set-theory maintainer-merge awaiting-author 10/13 1 4 nobody 2024-11-20 11:23 (3 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)
16020 adomani feat: compare PR `olean`s size with `master` maintainer-merge CI 120/0 5 49 nobody 2024-11-20 14:27 (3 days 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(Co*variantClass): 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 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)

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 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)

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(Co*variantClass): 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 (3 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 (21 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 delegated 36/91 18 7 nobody 2024-11-23 18:05 (4 hours ago)