The mathlib review queue

Welcome to the mathlib review page. Everybody's help with reviewing is appreciated. Reviewing contributions is important, and everybody is welcome to review pull requests! If you're not sure how, the pull request review guide is there to help you.
This page contains tables of

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

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 (7 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 (4 days ago)
16543 CBirkbeck feat(Analysis/NormedSpace/FunctionSeries): add eventually versions t-analysis 37/0 1 25 nobody 2024-11-19 22:49 (4 days ago)
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 (1 days 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 (23 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 (22 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 (21 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 (14 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 (12 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 (11 hours ago)
19388 eric-wieser chore: make map_ofNat a simp lemma t-algebra 2/0 1 6 nobody 2024-11-23 11:55 (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)
19406 YaelDillies feat: `{a, b} * s = a • s ∪ b • s` t-algebra 34/6 1 1 nobody 2024-11-23 12:50 (10 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 (10 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 (9 hours ago)
19321 jcommelin chore: change associativity of `+ᵥ` from `infixl` to `infixr` 40/37 12 6 nobody 2024-11-23 13:56 (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)
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 (7 hours ago)
15874 vihdzp doc(Order/InitialSeg): Improve documentation t-order documentation 40/44 2 25 nobody 2024-11-23 15:55 (7 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 (7 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 (1 hours ago)
19315 quangvdao feat(Finsupp/Fin): Add `Finsupp` operations on `Fin` tuples t-data 208/22 4 7 nobody 2024-11-23 22:58 (3 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 (7 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 (21 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 (4 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 (12 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 (1 hours ago)

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

Number Author Title Labels +/- 📝 💬 Assignee(s) Updated
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)