Why is my PR not on the queue?

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

To appear on the review queue, your open pull request must...

The table below contains all open PRs against the master branch which are not in draft mode. For each PR, it shows whether the checks above are satisfied. You can filter that list by entering terms into the search box, such as the PR number or your github username.

Number Author Title Labels not from a fork? CI status? not blocked? no merge conflict? ready? awaiting review? On the review queue?
14426 adomani dev: `#min_imps` command merge-conflict WIP ✅ ✅ ✅ ❌ ❌ ✅ ❌
14583 lecopivo fix: make concrete cycle notation local awaiting-author ✅ ✅ ✅ ✅ ✅ ❌ ❌
14727 jjaassoonn feat(RingTheory/Flat/CategoryTheory): a flat module has vanishing higher Tor groups t-algebra awaiting-author ✅ ✅ ✅ ✅ ✅ ❌ ❌
13847 alreadydone feat(EllipticCurve): the universal elliptic curve t-algebra t-algebraic-geometry merge-conflict awaiting-author ✅ ✅ ✅ ❌ ✅ ❌ ❌
13946 alreadydone feat(MvPolynomial/PDeriv): Euler's (weighted) homogeneous identity t-algebra awaiting-author ✅ ✅ ✅ ✅ ✅ ❌ ❌
13999 adomani feat: a linter to flag potential confusing conventions t-linter merge-conflict awaiting-author ✅ ✅ ✅ ❌ ✅ ❌ ❌
14444 digama0 fix(GeneralizeProofs): unreachable! bug t-meta awaiting-author ✅ ✅ ✅ ✅ ✅ ❌ ❌
14330 Ruben-VandeVelde chore: split Mathlib.Algebra.Star.Basic merge-conflict awaiting-author ✅ ✅ ✅ ❌ ✅ ❌ ❌
14386 Parcly-Taxel feat: the Rado graph t-combinatorics WIP ✅ ❌ ✅ ✅ ❌ ✅ ❌
14167 alreadydone feat: Group scheme structure on Weierstrass curve workshop-AIM-AG-2024 t-algebraic-geometry merge-conflict WIP ✅ ❌ ✅ ❌ ❌ ✅ ❌
14345 digama0 feat: the Dialectica category is monoidal closed t-category-theory awaiting-author ✅ ✅ ✅ ✅ ✅ ❌ ❌
13270 trivial1711 feat: power of product of two reflections t-algebra RFC merge-conflict blocked-by-other-PR ✅ ✅ ❌ ❌ ✅ ✅ ❌
13297 urkud feat(Semicontinuous): add `comp` lemma t-order t-topology merge-conflict awaiting-author ✅ ✅ ✅ ❌ ✅ ❌ ❌
13539 joelriou feat: the bicategory of adjunctions in a bicategory t-category-theory WIP ✅ ❌ ✅ ✅ ❌ ✅ ❌
13578 eric-wieser feat: add a `dsimproc` for vector notation awaiting-CI t-meta merge-conflict ✅ ❌ ✅ ❌ ✅ ❌ ❌
12561 BoltonBailey doc: Elaborate output of `lake exe pole` WIP ✅ ✅ ✅ ✅ ❌ ✅ ❌
12313 trivial1711 feat: "outer product" of functions that tend to zero on the cocompact filter t-topology awaiting-author ✅ ✅ ✅ ✅ ✅ ❌ ❌
12452 JADekker feat(Cocardinal) : add some more api t-topology awaiting-CI ✅ ❌ ✅ ✅ ✅ ❌ ❌
12608 eric-wieser feat: allow `nsmul` / `zsmul` to be omitted again, with a warning t-algebra t-meta merge-conflict awaiting-author ✅ ✅ ✅ ❌ ✅ ❌ ❌
12679 MichaelStollBayreuth perf(NumberTheory/RamificationInertia): speed up slow file merge-conflict WIP ✅ ✅ ✅ ❌ ❌ ✅ ❌
12556 fpvandoorn tests with presimps merge-conflict WIP ✅ ❌ ✅ ❌ ❌ ✅ ❌
12773 apnelson1 feat(Combinatorics/HypergraphRamsey): Ramsey's theorem for hypergraphs t-combinatorics merge-conflict ✅ ❌ ✅ ❌ ✅ ✅ ❌
12670 trivial1711 feat: completion of a nonarchimedean multiplicative group t-algebra t-topology merge-conflict blocked-by-other-PR ✅ ✅ ❌ ❌ ✅ ✅ ❌
12493 Ruben-VandeVelde chore: split Data.DFinsupp.Basic merge-conflict awaiting-author ✅ ✅ ✅ ❌ ✅ ❌ ❌
12936 mattrobball chore(Quiver.Opposite): make `Quiver.Hom.op/unop` `abbrev`'s merge-conflict ✅ ✅ ✅ ❌ ✅ ✅ ❌
13038 adomani feat: Mathlib weekly reports CI t-meta awaiting-author ✅ ✅ ✅ ✅ ✅ ❌ ❌
13057 alreadydone feat(NumberTheory): characterize elliptic divisibility sequences t-algebra t-number-theory merge-conflict blocked-by-other-PR ✅ ✅ ❌ ❌ ✅ ✅ ❌
12933 grunweg chore: replace some use of > or ≥ by < or ≤ merge-conflict awaiting-author ✅ ❌ ✅ ❌ ✅ ❌ ❌
12934 grunweg chore: replace more uses of > or ≥ by < or ≤ merge-conflict awaiting-author help-wanted ✅ ✅ ✅ ❌ ❌ ❌ ❌
12673 grunweg feat: add ContDiff.lipschitzOnWith t-analysis awaiting-author ✅ ✅ ✅ ✅ ✅ ❌ ❌
12331 mo271 chore: replace `refine ?_` and `refine' _` by `apply` awaiting-zulip merge-conflict ✅ ✅ ✅ ❌ ✅ ❌ ❌
12879 grunweg feat: port ge_or_gt linter from mathlib3 tech debt t-linter merge-conflict blocked-by-other-PR ✅ ❌ ❌ ❌ ✅ ✅ ❌
13036 joelriou feat(CategoryTheory/Sites): under certain conditions, cover preserving functors preserve 1-hypercovers t-category-theory WIP ✅ ✅ ✅ ✅ ❌ ✅ ❌
12605 FR-vdash-bot chore: attribute [induction_eliminator] merge-conflict awaiting-author ✅ ✅ ✅ ❌ ✅ ❌ ❌
12294 AntoineChambert-Loir feat(Mathlib.RingTheory.TensorProduct.Polynomial) : tensor product of a (univariate) polynomial ring t-algebra merge-conflict ✅ ❌ ✅ ❌ ✅ ✅ ❌
12292 AntoineChambert-Loir feat(Mathlib.RingTheory.TensorProduct.MonoidAlgebra) : tensor product of a monoid algebra t-algebra merge-conflict WIP ✅ ❌ ✅ ❌ ❌ ✅ ❌
12394 JADekker feat : define pre-tight and tight measures t-measure-probability awaiting-author ✅ ❌ ✅ ✅ ✅ ❌ ❌
12192 Ruben-VandeVelde feat: generalize isLittleO_const_id_atTop/atBot t-analysis merge-conflict awaiting-author ✅ ✅ ✅ ❌ ✅ ❌ ❌
12032 mcdoll feat: Delta distribution as a limit t-analysis blocked-by-other-PR WIP ✅ ❌ ❌ ✅ ❌ ✅ ❌
11617 urkud refactor(Finset): redefine Finset.diag, review API t-logic merge-conflict awaiting-author ✅ ✅ ✅ ❌ ✅ ❌ ❌
11905 grunweg chore: use @[inherit_doc] more and remove some nolints merge-conflict awaiting-author documentation ✅ ✅ ✅ ❌ ✅ ❌ ❌
12006 adomani feat: the `suffa` tactic t-meta awaiting-author ✅ ✅ ✅ ✅ ✅ ❌ ❌
11524 mcdoll refactor: Introduce type-class for SchwartzMap merge-conflict WIP ✅ ❌ ✅ ❌ ❌ ✅ ❌
11316 jcommelin chore(Polynomial/*): various cleanups awaiting-CI merge-conflict ✅ ❌ ✅ ❌ ✅ ❌ ❌
11496 mcdoll feat: Topology of pointwise convergence for continuous linear maps t-topology awaiting-author ✅ ✅ ✅ ✅ ✅ ❌ ❌
11837 trivial1711 feat: completion of a uniform multiplicative group t-algebra t-topology merge-conflict ✅ ✅ ✅ ❌ ✅ ✅ ❌
11563 YaelDillies feat: `∑ hi : i ∈ s, f i hi` syntax for big operators t-algebra t-meta WIP ✅ ✅ ✅ ✅ ❌ ✅ ❌
11577 ScottCarnahan feat (RingTheory/HahnSeries/Multiplication): lemmas about order of products t-algebra merge-conflict WIP ✅ ✅ ✅ ❌ ❌ ✅ ❌
11575 ScottCarnahan feat (RingTheory/HahnSeries/Addition): Lemmas on leading terms t-algebra merge-conflict WIP ✅ ✅ ✅ ❌ ❌ ✅ ❌
10594 lecopivo feat: `fun_trans` function transformation tactic e.g. for computing derivatives t-meta merge-conflict WIP ✅ ❌ ✅ ❌ ❌ ✅ ❌
11455 adomani fix: unsqueeze simp, re Yaël's comments on #11259 merge-conflict awaiting-author ✅ ✅ ✅ ❌ ✅ ❌ ❌
10998 hmonroe feat(Logic): Arithmetization of partial recursive functions (toward Gödel's first incompleteness theorem) t-logic awaiting-author ✅ ✅ ✅ ✅ ✅ ❌ ❌
11142 hmonroe feat(ProofTheory): Define logical symbols abstractly; opens new top-level section, drawing from lean4-logic t-logic awaiting-author ✅ ✅ ✅ ✅ ✅ ❌ ❌
10842 mcdoll chore: simplify proofs using new positivity extensions and tests merge-conflict blocked-by-other-PR WIP ✅ ✅ ❌ ❌ ❌ ✅ ❌
10024 ADedecker feat: rename `connectedComponentOfOne` to `identityComponent`, prove that it is normal and open t-topology awaiting-CI merge-conflict ✅ ❌ ✅ ❌ ✅ ❌ ❌
10058 alreadydone feat: homomorphism between fundamental groups induced by continuous maps t-topology merge-conflict WIP ✅ ❌ ✅ ❌ ❌ ✅ ❌
10099 mcdoll feat: Integration by parts for higher dimensional spaces t-measure-probability t-analysis WIP ✅ ❌ ✅ ✅ ❌ ✅ ❌
10276 ericrbg feat: norm positivity extension proves strict positivity t-meta merge-conflict awaiting-author ✅ ✅ ✅ ❌ ✅ ❌ ❌
10113 Multramate feat(GroupTheory/Submonoid/Operations): define homomorphisms of subgroups induced by homomorphisms of groups t-algebra merge-conflict awaiting-author ✅ ✅ ✅ ❌ ✅ ❌ ❌
10303 grunweg feat: three misc lemmas about Hausdorff distance t-topology merge-conflict awaiting-author help-wanted ✅ ✅ ✅ ❌ ❌ ❌ ❌
11100 eric-wieser feat(CategoryTheory/Limits): add `Functor.mapBinaryBiconeInv` t-category-theory awaiting-CI merge-conflict ✅ ❌ ✅ ❌ ✅ ❌ ❌
10126 Multramate feat(GroupTheory/GroupAction/Basic): define homomorphisms of fixed subgroups induced by homomorphisms of groups t-algebra merge-conflict blocked-by-other-PR ✅ ✅ ❌ ❌ ✅ ✅ ❌
10678 adri326 feat(Topology/UniformSpace): prove that a uniform space is completely regular t-topology awaiting-author ✅ ✅ ✅ ✅ ✅ ❌ ❌
11311 lambda-fairy feat: Myhill–Nerode theorem t-computability merge-conflict awaiting-author ✅ ✅ ✅ ❌ ✅ ❌ ❌
10660 eric-wieser feat(LinearAlgebra/CliffordAlgebra): construction from a basis t-algebra merge-conflict awaiting-author WIP ✅ ❌ ✅ ❌ ❌ ❌ ❌
10129 linesthatinterlace fix(Topology/MetricSpace/InfSep): Make `infsep` consistent with `diam`, `infdist` merge-conflict awaiting-author ✅ ✅ ✅ ❌ ✅ ❌ ❌
10521 eric-wieser chore: generalize `IsBoundedLinearMap` to modules t-analysis merge-conflict awaiting-author ✅ ✅ ✅ ❌ ✅ ❌ ❌
10444 urkud doc(IsROrC): expand the docstring t-analysis merge-conflict awaiting-author documentation ✅ ✅ ✅ ❌ ✅ ❌ ❌
10142 Multramate feat(AlgebraicGeometry/EllipticCurve/Group): compute range of baseChange t-algebraic-geometry t-number-theory merge-conflict blocked-by-other-PR ✅ ✅ ❌ ❌ ✅ ✅ ❌
10721 urkud feat(Order/FunLike): define `PointwiseLE` t-logic t-order merge-conflict ✅ ✅ ✅ ❌ ✅ ✅ ❌
11021 jstoobysmith feat(AlgebraicTopology) : add join of augmented SSets new-contributor t-category-theory merge-conflict WIP ✅ ❌ ✅ ❌ ❌ ✅ ❌
11210 hmonroe Test commit WIP ✅ ❌ ✅ ✅ ❌ ✅ ❌
8686 j-loreaux feat: refactor AlgEquiv to allow for non-unital equivalences t-algebra merge-conflict WIP ✅ ❌ ✅ ❌ ❌ ✅ ❌
9570 eric-wieser feat(Algebra/Star): Non-commutative generalization of `StarModule` t-algebra awaiting-CI merge-conflict WIP ✅ ❌ ✅ ❌ ❌ ❌ ❌
9627 Ruben-VandeVelde chore: move some code out of Init.Data.Nat.Lemmas merge-conflict awaiting-author ✅ ✅ ✅ ❌ ✅ ❌ ❌
9352 chenyili0818 feat: arithmetic lemmas for `gradient` t-analysis awaiting-author ✅ ✅ ✅ ✅ ✅ ❌ ❌
9571 linesthatinterlace fix(Data/Fin/Tuple/Basic): Refactor snoc and cons proofs. merge-conflict awaiting-author ✅ ❌ ✅ ❌ ✅ ❌ ❌
9564 AntoineChambert-Loir weaken commutativity assumptions for AdjoinRoot.lift and AdjoinRoot.liftHom t-algebra merge-conflict WIP ✅ ❌ ✅ ❌ ❌ ✅ ❌
9642 eric-wieser refactor(Analysis/Normed/{Group/Field}/Basic): Let `extends` generate the repeated fields t-analysis merge-conflict awaiting-author WIP help-wanted ✅ ✅ ✅ ❌ ❌ ❌ ❌
9229 eric-wieser refactor(Algebra/GradedMonoid): Use `HMul` to define `GMul` t-algebra merge-conflict WIP ✅ ❌ ✅ ❌ ❌ ✅ ❌
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 ✅ ✅ ✅ ❌ ✅ ✅ ❌
9146 laughinggas feat(Data/ZMod/Defs): Topological structure on `ZMod` t-algebra t-topology merge-conflict awaiting-author ✅ ✅ ✅ ❌ ✅ ❌ ❌
9469 dupuisf feat: maximum modulus principle for functions vanishing at infinity t-analysis awaiting-author ✅ ✅ ✅ ✅ ✅ ❌ ❌
9510 eric-wieser feat(Analysis/Calculus/DualNumber): Extending differentiable functions to dual numbers t-algebra t-analysis awaiting-CI WIP ✅ ❌ ✅ ✅ ❌ ❌ ❌
9755 eric-wieser chore(Analysis): rename `closedUnitBall` and `closed_unit_ball` to `unit_closedBall` t-analysis awaiting-CI merge-conflict awaiting-author ✅ ❌ ✅ ❌ ✅ ❌ ❌
9356 alexjbest feat: assumption? t-meta merge-conflict awaiting-author ✅ ✅ ✅ ❌ ✅ ❌ ❌
9320 BoltonBailey chore: Golf simp calls WIP ✅ ✅ ✅ ✅ ❌ ✅ ❌
9487 eric-wieser feat: the exponential of dual numbers over non-commutative rings t-measure-probability t-algebra t-analysis merge-conflict WIP ✅ ❌ ✅ ❌ ❌ ✅ ❌
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 ✅ ✅ ✅ ❌ ✅ ✅ ❌
9273 grunweg feat: extended charts are local diffeomorphisms on their source t-differential-geometry blocked-by-other-PR ✅ ✅ ❌ ✅ ✅ ✅ ❌
9467 eric-wieser refactor(Analysis/Calculus/FormalMultilinearSeries): generalize to additive monoids t-analysis merge-conflict ✅ ✅ ✅ ❌ ✅ ✅ ❌
8616 eric-wieser feat(Algebra/FreeAlgebra): add right action and `IsCentralScalar` t-algebra awaiting-CI merge-conflict ✅ ✅ ✅ ❌ ✅ ❌ ❌
8961 eric-wieser refactor: use the coinduced topology on ULift awaiting-CI merge-conflict please-adopt awaiting-author ✅ ❌ ✅ ❌ ❌ ❌ ❌
9354 chenyili0818 feat: monotonicity of gradient on convex real-valued functions t-analysis merge-conflict awaiting-author ✅ ✅ ✅ ❌ ✅ ❌ ❌
8906 jjaassoonn feat: add some missing lemmas about linear algebra t-algebra merge-conflict awaiting-author ✅ ❌ ✅ ❌ ✅ ❌ ❌
8658 eric-wieser feat: support right actions for `Con` t-algebra merge-conflict awaiting-author ✅ ✅ ✅ ❌ ✅ ❌ ❌
8511 eric-wieser refactor(MeasureTheory/Measure/Haar/Basic): partially generalize to the affine case merge-conflict awaiting-author ✅ ❌ ✅ ❌ ✅ ❌ ❌
8519 eric-wieser refactor(LinearAlgebra/TensorProduct): golf using `liftAddHom` t-algebra merge-conflict awaiting-author ✅ ✅ ✅ ❌ ✅ ❌ ❌
8503 thorimur feat: meta utils for `refine?` t-meta merge-conflict awaiting-author ✅ ✅ ✅ ❌ ✅ ❌ ❌
8740 digama0 fix: improve `recall` impl / error reporting awaiting-CI t-meta merge-conflict awaiting-author ✅ ❌ ✅ ❌ ✅ ❌ ❌
6930 kmill feat: `resynth_instances` tactic for resynthesizing instances in the goal or local context t-meta merge-conflict WIP ✅ ✅ ✅ ❌ ❌ ✅ ❌
6630 MohanadAhmed feat: Reduced Spectral Theorem t-algebra merge-conflict WIP ✅ ❌ ✅ ❌ ❌ ✅ ❌
6859 MohanadAhmed TryLean4Bundle: Windows Bundle Creator CI WIP help-wanted ✅ ✅ ✅ ✅ ❌ ✅ ❌
7325 eric-wieser chore: use preimageIso instead of defeq abuse for InducedCategory t-category-theory awaiting-CI merge-conflict ✅ ❌ ✅ ❌ ✅ ❌ ❌
7713 RemyDegenne feat: add_left/right_inj for measures t-measure-probability merge-conflict awaiting-author ✅ ❌ ✅ ❌ ✅ ❌ ❌
6580 adomani chore: `move_add`-driven replacements merge-conflict awaiting-author ✅ ✅ ✅ ❌ ✅ ❌ ❌
7014 kim-em chore: cleanup of `trans` tactic t-meta merge-conflict ✅ ❌ ✅ ❌ ✅ ✅ ❌
7564 shuxuezhuyi feat(Topology/Algebra/Order): extend strictly monotone function on `Ioo` to homeomorphism on `Icc` t-topology merge-conflict blocked-by-other-PR ✅ ✅ ❌ ❌ ✅ ✅ ❌
7230 kim-em chore: refactor of AtomM awaiting-CI merge-conflict ✅ ❌ ✅ ❌ ✅ ❌ ❌
7615 eric-wieser chore(LinearAlgebra/Basic): generalize compatibleMaps to semilinear maps t-algebra awaiting-CI easy merge-conflict ✅ ❌ ✅ ❌ ✅ ❌ ❌
7427 MohanadAhmed Mohanad ahmed/sort eigenvalues abs merge-conflict WIP ✅ ❌ ✅ ❌ ❌ ✅ ❌
7478 newell feat(Topology/MetricSpace/Congruence): define Congruent t-topology awaiting-author ✅ ✅ ✅ ✅ ✅ ❌ ❌
7351 shuxuezhuyi feat(Topology/Algebra/Order): extend function on `Ioo` to `Icc` t-order merge-conflict awaiting-author ✅ ✅ ✅ ❌ ✅ ❌ ❌
7227 kmill feat: flexible binders and integration into notation3 t-meta merge-conflict WIP ✅ ❌ ✅ ❌ ❌ ✅ ❌
6791 eric-wieser refactor: Use flat structures for morphisms awaiting-CI merge-conflict awaiting-author help-wanted ✅ ❌ ✅ ❌ ❌ ❌ ❌
6777 adomani chore(Co*variantClass): replace eta-expanded (· * ·), (· + ·), (· ≤ ·), (· < ·) merge-conflict ✅ ✅ ✅ ❌ ✅ ✅ ❌
7125 eric-wieser feat: additive monoid structure via biproducts t-category-theory awaiting-CI WIP ✅ ❌ ✅ ✅ ❌ ❌ ❌
7649 eric-wieser wip: instead of `suppress_compilation`, use `implemented_by` merge-conflict WIP ✅ ❌ ✅ ❌ ❌ ✅ ❌
7596 alreadydone feat: covering maps from properly discontinuous actions and discrete subgroups t-topology merge-conflict awaiting-author ✅ ✅ ✅ ❌ ✅ ❌ ❌
6931 urkud refactor(Analysis/Normed*): use `RingHomIsometric` for `*.norm_cast` t-analysis merge-conflict help-wanted ✅ ❌ ✅ ❌ ❌ ✅ ❌
7601 digama0 feat: ring hom support in `ring` t-algebra t-meta merge-conflict awaiting-author ✅ ❌ ✅ ❌ ✅ ❌ ❌
7467 ADedecker feat: spectrum of X →ᵇ ℂ is StoneCech X t-analysis merge-conflict WIP ✅ ❌ ✅ ❌ ❌ ✅ ❌
8362 urkud feat(Asymptotics): define `ReflectsGrowth` t-analysis awaiting-author ✅ ❌ ✅ ✅ ✅ ❌ ❌
8167 sebzim4500 feat: Add new `grw` tactic for rewriting using inequalities. t-meta merge-conflict modifies-tactic-syntax awaiting-author ✅ ✅ ✅ ❌ ✅ ❌ ❌
8453 FR-vdash-bot chore(MeasureTheory): Golf, speed up t-measure-probability merge-conflict ✅ ❌ ✅ ❌ ✅ ✅ ❌
7875 FR-vdash-bot chore: make `SMulCommClass A A B` and `SMulCommClass A B B` higher priority slow-typeclass-synthesis t-algebra merge-conflict ✅ ✅ ✅ ❌ ✅ ✅ ❌
8370 eric-wieser refactor(Analysis/NormedSpace/Exponential): remove the `𝕂` argument from `exp` t-analysis RFC merge-conflict ✅ ❌ ✅ ❌ ✅ ✅ ❌
7994 ericrbg chore: generalize `LieSubalgebra.mem_map_submodule` merge-conflict please-adopt ✅ ❌ ✅ ❌ ❌ ✅ ❌
7909 mcdoll fix(Tactic/Continuity): remove npowRec and add new tag for Continuous.pow t-topology t-meta merge-conflict WIP ✅ ❌ ✅ ❌ ❌ ✅ ❌
7874 FR-vdash-bot chore: make `IsScalarTower A A B` and `IsScalarTower A B B` higher priority slow-typeclass-synthesis t-algebra awaiting-CI merge-conflict ✅ ❌ ✅ ❌ ✅ ❌ ❌
7877 grunweg feat: real manifolds are locally path-connected t-topology t-differential-geometry merge-conflict awaiting-author ✅ ❌ ✅ ❌ ✅ ❌ ❌
7962 eric-wieser feat: `DualNumber (Quaternion R)` as a `CliffordAlgebra` t-algebra merge-conflict WIP ✅ ❌ ✅ ❌ ❌ ✅ ❌
7932 eric-wieser refactor(Algebra/TrivSqZeroExt): replace with a structure t-algebra awaiting-CI merge-conflict ✅ ❌ ✅ ❌ ✅ ❌ ❌
7835 shuxuezhuyi feat(LinearAlgebra/Matrix): `lift` for projective special linear group t-algebra merge-conflict awaiting-author ✅ ✅ ✅ ❌ ✅ ❌ ❌
8047 faenuccio refactor(Util/Delaborators): remove `scoped` from delabPi' t-meta ✅ ❌ ✅ ✅ ✅ ✅ ❌
8364 thorimur feat: `refine?` t-meta merge-conflict blocked-by-other-PR ✅ ✅ ❌ ❌ ✅ ✅ ❌
5133 kmill feat: IntermediateField adjoin syntax for sets of elements t-algebra merge-conflict WIP ✅ ✅ ✅ ❌ ❌ ✅ ❌
2605 eric-wieser chore: better error message in linarith t-meta merge-conflict awaiting-author ✅ ✅ ✅ ❌ ✅ ❌ ❌
3808 kim-em feat: #formalize, backed by a choice of LLMs t-meta merge-conflict awaiting-author ✅ ✅ ✅ ❌ ✅ ❌ ❌
4871 j-loreaux feat: define the additive submonoid of positive elements in a star ordered ring t-algebra awaiting-CI merge-conflict ✅ ❌ ✅ ❌ ✅ ❌ ❌
6002 slerpyyy feat(Analysis.SpecialFunctions.Gaussian): add `integrable_fun_mul_exp_neg_mul_sq` t-analysis merge-conflict awaiting-author ✅ ✅ ✅ ❌ ✅ ❌ ❌
6195 eric-wieser chore(RingTheory/TensorProduct): golf the `mul` definition t-algebra awaiting-CI merge-conflict ✅ ✅ ✅ ❌ ✅ ❌ ❌
6210 MohanadAhmed feat(Data/IsROrC/Basic): add a `StarOrderedRing` instance t-algebra t-analysis merge-conflict WIP ✅ ❌ ✅ ❌ ❌ ✅ ❌
6317 eric-wieser refactor(Data/Finsupp/Defs): make Finsupp.single defeq to Pi.single merge-conflict WIP ✅ ❌ ✅ ❌ ❌ ✅ ❌
6548 ChrisHughes24 refactor: make charP_to_charZero an instance t-algebra merge-conflict awaiting-author ✅ ✅ ✅ ❌ ✅ ❌ ❌
6328 FR-vdash-bot chore: make some instance about `Sub...Class` lower priority t-algebra awaiting-CI merge-conflict WIP ✅ ❌ ✅ ❌ ❌ ❌ ❌
6491 eric-wieser chore(Mathlib/Algebra/Hom/GroupAction): add `SMulHomClass.comp_smul` t-algebra merge-conflict ✅ ❌ ✅ ❌ ✅ ✅ ❌
5745 alexjbest feat: a tactic to consume type annotations, and make constructor nicer t-meta awaiting-author ✅ ✅ ✅ ✅ ✅ ❌ ❌
5934 eric-wieser feat: port Data.Rat.MetaDefs t-meta merge-conflict mathlib-port help-wanted ✅ ❌ ✅ ❌ ❌ ✅ ❌
6268 eric-wieser Fixups to #3838 merge-conflict WIP ✅ ❌ ✅ ❌ ❌ ✅ ❌
5912 ADedecker feat(Analysis.Distribution.ContDiffMapSupportedIn): space of smooth maps with support in a fixed compact t-analysis merge-conflict WIP ✅ ❌ ✅ ❌ ❌ ✅ ❌
5863 eric-wieser feat: add elaborators for concrete matrices t-meta merge-conflict help-wanted ✅ ✅ ✅ ❌ ❌ ✅ ❌
5897 eric-wieser feat: add a `MonadError` instance for `ContT` t-meta awaiting-author ✅ ✅ ✅ ✅ ✅ ❌ ❌
5062 adomani feat(Tactic/Prune + test/Prune): add `prune` tactic, for removing unnecessary hypotheses t-meta modifies-tactic-syntax awaiting-author ✅ ✅ ✅ ✅ ✅ ❌ ❌
6590 mcdoll feat: composition of LinearPMaps t-algebra merge-conflict WIP ✅ ❌ ✅ ❌ ❌ ✅ ❌
6252 michaellee94 feat(Geometry/Manifolds/Instances/Homeomorph): Homeomorphism maps `C^k` manifolds to `C^k` manifolds t-differential-geometry WIP ✅ ✅ ✅ ✅ ❌ ✅ ❌
4127 kmill refactor: create HasAdj class, define Digraph, and generalize some SimpleGraph API t-combinatorics merge-conflict awaiting-author ✅ ✅ ✅ ❌ ✅ ❌ ❌
6627 adomani feat(Algebra/MonoidAlgebra/NoZeroDivisors): `NoZeroDivisors` instance on `AddMonoidAlgebra`s t-algebra merge-conflict awaiting-author ✅ ✅ ✅ ❌ ✅ ❌ ❌
5952 eric-wieser feat: add Qq wrappers for ToExpr awaiting-CI t-meta merge-conflict ✅ ❌ ✅ ❌ ✅ ❌ ❌
6183 FR-vdash-bot chore: remove `normalizeScaleRoots` t-algebra merge-conflict WIP ✅ ✅ ✅ ❌ ❌ ✅ ❌
6993 jjaassoonn feat : lemmas about `AddMonoidAlgebra.{divOf, modOf}` t-algebra merge-conflict ✅ ✅ ✅ ❌ ✅ ✅ ❌
6633 adomani feat(..Polynomial..): `MvPolynomial`s have no zero divisors t-algebra merge-conflict awaiting-author ✅ ✅ ✅ ❌ ✅ ❌ ❌
7076 grunweg feat: define measure zero subsets of a manifold t-measure-probability t-differential-geometry merge-conflict WIP ✅ ✅ ✅ ❌ ❌ ✅ ❌
3171 eric-wieser refactor: make the algebra hierarchy use flat structures merge-conflict WIP ✅ ❌ ✅ ❌ ❌ ✅ ❌
6403 FR-vdash-bot chore: change instance priorities of `Ordered*` hierarchy slow-typeclass-synthesis t-order t-algebra merge-conflict awaiting-author ✅ ✅ ✅ ❌ ✅ ❌ ❌
6330 FR-vdash-bot chore: make some instance about `Sub...Class` higher priority than `Sub...` slow-typeclass-synthesis t-algebra merge-conflict WIP ✅ ✅ ✅ ❌ ❌ ✅ ❌
4960 eric-wieser chore: use `open scoped` awaiting-CI merge-conflict ✅ ✅ ✅ ❌ ✅ ❌ ❌
7300 ah1112 feat: synthetic geometry t-euclidean-geometry awaiting-author help-wanted ✅ ✅ ✅ ✅ ❌ ❌ ❌
6079 eric-wieser fix: deduplicate variables awaiting-CI merge-conflict ✅ ❌ ✅ ❌ ✅ ❌ ❌
3757 thorimur feat: config options for `fail_if_no_progress` t-meta merge-conflict WIP ✅ ✅ ✅ ❌ ❌ ✅ ❌
15355 adomani feat: MiM PR report WIP ✅ ✅ ✅ ✅ ❌ ✅ ❌
12353 thorimur feat: `conv%` t-meta merge-conflict WIP ✅ ✅ ✅ ❌ ❌ ✅ ❌
13361 Komyyy chore(Mathlib/Data/Seq/Seq): add `cases_eliminator`s to `Sequence.recOn` merge-conflict blocked-by-other-PR ✅ ✅ ❌ ❌ ✅ ✅ ❌
13509 Komyyy refactor(Mathlib/Data/Seq/Seq): make `Sequence.mem_rec_on` more useful merge-conflict blocked-by-other-PR WIP ✅ ✅ ❌ ❌ ❌ ✅ ❌
15224 AnthonyBordg feat(CategoryTheory/Sites): covering families and their associated Grothendieck topology new-contributor t-category-theory awaiting-author ✅ ✅ ✅ ✅ ✅ ❌ ❌
11521 eric-wieser feat: add `fast_instance%` elaborator t-meta ✅ ❌ ✅ ✅ ✅ ✅ ❌
7903 urkud feat: define `UnboundedSpace` t-topology merge-conflict help-wanted ✅ ❌ ✅ ❌ ❌ ✅ ❌
14675 adomani dev: the repeated variable linter merge-conflict WIP ✅ ❌ ✅ ❌ ❌ ✅ ❌
12054 adomani feat: auto-bugs t-meta awaiting-author ✅ ✅ ✅ ✅ ✅ ❌ ❌
15480 grunweg chore(NumberTheory): replace remaining occurrences of open Classical tech debt t-number-theory merge-conflict awaiting-author ✅ ✅ ✅ ❌ ✅ ❌ ❌
13458 grunweg perf(Manifold/ContMDiff/NormedSpace): add shortcut instances t-differential-geometry merge-conflict awaiting-author ✅ ✅ ✅ ❌ ✅ ❌ ❌
13795 FR-vdash-bot perf(Algebra/{Group, GroupWithZero, Ring}/InjSurj): reduce everything t-algebra merge-conflict blocked-by-other-PR ✅ ✅ ❌ ❌ ✅ ✅ ❌
15483 FR-vdash-bot chore(GroupTheory/Coset): reduce defeq abuse t-algebra merge-conflict ✅ ✅ ✅ ❌ ✅ ✅ ❌
11942 grunweg doc: add @[inherit_doc] to some local notation merge-conflict awaiting-author documentation ✅ ✅ ✅ ❌ ✅ ❌ ❌
15400 grunweg feat: "confusing variables" linter t-linter merge-conflict WIP ✅ ❌ ✅ ❌ ❌ ✅ ❌
10717 joelriou feat(Algebra/Homology): the total complex of a tricomplex t-category-theory merge-conflict WIP ✅ ✅ ✅ ❌ ❌ ✅ ❌
12143 adomani feat: generic linter, absorbing `cdot` linter and `attribute [instance] in` linter t-linter merge-conflict ✅ ❌ ✅ ❌ ✅ ✅ ❌
14654 grunweg feat(runLinter): allow only running certain linters t-linter RFC merge-conflict ✅ ❌ ✅ ❌ ✅ ✅ ❌
15679 adomani test: refactor in CI merge-conflict WIP ✅ ❌ ✅ ❌ ❌ ✅ ❌
8435 kim-em feat: run `hint` tactics in parallel t-meta merge-conflict ✅ ❌ ✅ ❌ ✅ ✅ ❌
8102 miguelmarco feat (Tactic): add unify_denoms and collect_signs tactics new-contributor t-meta merge-conflict enhancement ✅ ❌ ✅ ❌ ✅ ✅ ❌
7565 shuxuezhuyi feat(Topology/Algebra/Order): extend homeomorphism of `Ioo` to `Icc` t-order t-topology merge-conflict blocked-by-other-PR ✅ ✅ ❌ ❌ ✅ ✅ ❌
9145 linesthatinterlace feat(Data/Fin/Basic): Refactor succAbove and predAbove. t-data merge-conflict ✅ ✅ ✅ ❌ ✅ ✅ ❌
10629 madvorak feat: List.cons_sublist_append_iff_right t-data merge-conflict ✅ ✅ ✅ ❌ ✅ ✅ ❌
9085 Timeroot feat: `Polynomial.coeffList` t-data merge-conflict blocked-by-other-PR ✅ ❌ ❌ ❌ ✅ ✅ ❌
9973 Ruben-VandeVelde feat: polynomials formed by lists t-data merge-conflict please-adopt ✅ ❌ ✅ ❌ ❌ ✅ ❌
12926 joelriou feat(CategoryTheory): the monoidal category structure induced by a monoidal functor t-category-theory merge-conflict WIP ✅ ❌ ✅ ❌ ❌ ✅ ❌
13973 digama0 feat: lake exe refactor, initial framework t-meta awaiting-author ✅ ✅ ✅ ✅ ✅ ❌ ❌
12869 adomani feat: linter and script for `theorem` vs `lemma` t-linter merge-conflict awaiting-author ✅ ✅ ✅ ❌ ✅ ❌ ❌
15617 vigoux perf: use foldl for implementation of Multiset.fold awaiting-author ❌ ❌? ✅ ✅ ✅ ❌ ❌
14009 grunweg chore: replace continuity -> fun_prop in remaining directories t-analysis awaiting-author ✅ ✅ ✅ ✅ ✅ ❌ ❌
14563 awueth feat: if-then-else of exclusive or statement new-contributor t-algebra awaiting-author ✅ ✅ ✅ ✅ ✅ ❌ ❌
14733 jjaassoonn feat(RingTheory/Flat/CategoryTheory): a module is flat iff tensoring preserves finite limits t-algebra awaiting-author ✅ ✅ ✅ ✅ ✅ ❌ ❌
14542 linesthatinterlace feat(GroupTheory/Perm/Support): Redefine `support` to be a `Set`, removing finiteness requirements. t-algebra merge-conflict awaiting-author ✅ ✅ ✅ ❌ ✅ ❌ ❌
13861 BoltonBailey feat: `Finsupp.Option` t-data WIP ✅ ❌ ✅ ✅ ❌ ✅ ❌
14401 Komyyy feat: add `Stream'.pmap` & `Seq'.pmap` t-data merge-conflict WIP ✅ ✅ ✅ ❌ ❌ ✅ ❌
13511 Komyyy feat(Mathlib/Data/Seq/Seq): prove `∀ a ∈ (s : Sequence α), p a` using coinduction t-data merge-conflict blocked-by-other-PR WIP ✅ ✅ ❌ ❌ ❌ ✅ ❌
14760 FR-vdash-bot feat: define `IGame` t-logic merge-conflict blocked-by-other-PR WIP ✅ ❌ ❌ ❌ ❌ ✅ ❌
12664 BoltonBailey feat: add lemma about `degreeOf_eq_degree` t-algebra blocked-by-other-PR WIP ✅ ❌ ❌ ✅ ❌ ✅ ❌
12581 linesthatinterlace feat: (Probability/SubProbabilityMassFunction) t-measure-probability WIP ✅ ❌ ✅ ✅ ❌ ✅ ❌
12093 ADedecker feat: tweak the definition of semicontinuity to behave better in nonlinear orders t-topology merge-conflict WIP ✅ ✅ ✅ ❌ ❌ ✅ ❌
11393 mcdoll feat(Analysis/Distribution/SchwartzSpace): The Heine-Borel property t-analysis merge-conflict WIP ✅ ❌ ✅ ❌ ❌ ✅ ❌
9444 erdOne feat: Various instances regarding `𝓞 K`. t-number-theory merge-conflict help-wanted ✅ ❌ ✅ ❌ ❌ ✅ ❌
8931 hmonroe feat(Computable): define P, NP, and NP-complete t-computability merge-conflict awaiting-author ✅ ❌ ✅ ❌ ✅ ❌ ❌
9181 linesthatinterlace feat(Data/Option/Order): Add default order structure to Option with `none` incomparable t-data RFC awaiting-CI blocked-by-other-PR WIP ✅ ❌ ❌ ✅ ❌ ❌ ❌
10283 linesthatinterlace feat(Data/Fin/OrderHom): Extend lemmas to simplex results t-data merge-conflict WIP ✅ ❌ ✅ ❌ ❌ ✅ ❌
10823 alexkeizer feat: convert curried type functions into uncurried type functions t-data awaiting-author ✅ ✅ ✅ ✅ ✅ ❌ ❌
9040 BoltonBailey feat: `to_snoc` an attribute for generating lemmas with snoc in them t-meta please-adopt WIP help-wanted ✅ ❌ ✅ ✅ ❌ ✅ ❌
10387 adomani feat(Tactic/ComputeDegree): add `polynomial` tactic RFC t-meta WIP ✅ ✅ ✅ ✅ ❌ ✅ ❌
10345 newell feat(Algebra.Module.Zlattice): Add Voronoi Domain t-algebra merge-conflict WIP ✅ ❌ ✅ ❌ ❌ ✅ ❌
10332 adri326 feat(Topology/Sets): define regular open sets and their boolean algebra t-topology merge-conflict WIP ✅ ❌ ✅ ❌ ❌ ✅ ❌
9693 madvorak feat: Linear programming in the standard form t-algebra RFC WIP ✅ ✅ ✅ ✅ ❌ ✅ ❌
9449 hmonroe feat: Add Turing machine with the quintet definition (TMQ) and a chainable step function for each TM type t-computability awaiting-author ✅ ❌ ✅ ✅ ✅ ❌ ❌
8608 eric-wieser feat: multiplicativize `AddTorsor` t-algebra merge-conflict WIP ✅ ❌ ✅ ❌ ❌ ✅ ❌
9154 FR-vdash-bot feat: `npow` / `nsmul` / `Nat.cast`/ `zpow` / `zsmul` implemented using `Nat.binaryRec` t-algebra merge-conflict awaiting-author blocked-by-other-PR ✅ ✅ ❌ ❌ ✅ ❌ ❌
6603 tydeu feat: automatically try `cache get` before build CI merge-conflict WIP ✅ ✅ ✅ ❌ ❌ ✅ ❌
6058 apurvnakade feat: duality theory for cone programs t-analysis merge-conflict WIP ✅ ❌ ✅ ❌ ❌ ✅ ❌
6449 ADedecker feat: functions with finite fibers t-topology merge-conflict awaiting-author ✅ ❌ ✅ ❌ ✅ ❌ ❌
5919 MithicSpirit feat: implement orthogonality for AffineSubspace t-analysis WIP help-wanted ✅ ✅ ✅ ✅ ❌ ✅ ❌
7739 mcdoll feat(LinearAlgebra/LinearPMap): difference of inverses t-algebra merge-conflict WIP ✅ ❌ ✅ ❌ ❌ ✅ ❌
7386 madvorak feat: Define linear programs t-algebra RFC WIP ✅ ✅ ✅ ✅ ❌ ✅ ❌
7219 Ruben-VandeVelde feat: Equivs for AddMonoidAlgebras t-algebra awaiting-author ✅ ❌ ✅ ✅ ✅ ❌ ❌
7172 BoltonBailey feat: Composition of Turing machines t-computability awaiting-CI please-adopt WIP good first issue ✅ ❌ ✅ ✅ ❌ ❌ ❌
8793 101damnations feat(RepresentationTheory/GroupCohomology/Hilbert90): add Hilbert's original theorem 90 t-algebra awaiting-author ✅ ❌ ✅ ✅ ✅ ❌ ❌
13163 erdOne feat(.vscode/module-docstring.code-snippet): Prevent auto-complete from firing on `do` t-meta awaiting-author ✅ ✅ ✅ ✅ ✅ ❌ ❌
15774 kkytola feat: Topology on `ENat` t-order t-topology merge-conflict WIP ✅ ❌ ✅ ❌ ❌ ✅ ❌
10026 madvorak Linear programming according to Antoine Chambert-Loir's book t-algebra RFC WIP ✅ ✅ ✅ ✅ ❌ ✅ ❌
10159 madvorak Linear programming according to Antoine Chambert-Loir's book — affine version t-algebra RFC WIP ✅ ❌ ✅ ✅ ❌ ✅ ❌
12618 trivial1711 feat: the product of two sums in a nonarchimedean ring t-algebra t-topology merge-conflict blocked-by-other-PR ✅ ✅ ❌ ❌ ✅ ✅ ❌
13026 BoltonBailey feat: add `simp` lemma `coeff_eq_zero_of_not_mem_support` t-algebra awaiting-CI merge-conflict awaiting-author ✅ ❌ ✅ ❌ ✅ ❌ ❌
15892 grunweg feat: the real manifold [x,y] has boundary {x,y} t-differential-geometry blocked-by-other-PR ✅ ✅ ❌ ✅ ✅ ✅ ❌
13195 trivial1711 feat: the Chebyshev polynomials C and S t-algebra merge-conflict awaiting-author ✅ ✅ ✅ ❌ ✅ ❌ ❌
11632 mattrobball chore(Group/RingTheory.Congruence): make `Quotient`'s reducible merge-conflict ✅ ✅ ✅ ❌ ✅ ✅ ❌
13791 digama0 refactor: Primrec and Partrec tech debt t-computability merge-conflict ✅ ✅ ✅ ❌ ✅ ✅ ❌
14023 mattrobball perf (RingTheory.OreLocalization): make data irreducible merge-conflict ✅ ✅ ✅ ❌ ✅ ✅ ❌
11964 adamtopaz feat: The functor of points of a scheme t-algebraic-geometry t-category-theory merge-conflict ✅ ✅ ✅ ❌ ✅ ✅ ❌
12418 rosborn style: replace preimage_val with ↓∩ notation merge-conflict ✅ ✅ ✅ ❌ ✅ ✅ ❌
9978 FR-vdash-bot chore(FieldTheory/KummerExtension): move some lemmas earlier t-algebra merge-conflict awaiting-author ✅ ✅ ✅ ❌ ✅ ❌ ❌
12429 adomani feat: toND -- auto-generating natDegree t-algebra RFC t-meta merge-conflict awaiting-author ✅ ✅ ✅ ❌ ✅ ❌ ❌
14498 hwatheod feat(SetTheory/Surreal/Division): define the field structure on the Surreal numbers new-contributor t-logic awaiting-author ✅ ✅ ✅ ✅ ✅ ❌ ❌
11890 adomani feat: the terminal refine linter t-linter awaiting-author ✅ ✅ ✅ ✅ ✅ ❌ ❌
12751 Command-Master feat: add lemmas for Nat/Bits, Nat/Bitwise and Nat/Size t-data new-contributor merge-conflict ✅ ✅ ✅ ❌ ✅ ✅ ❌
9935 jstoobysmith feat(AlgebraicTopology): add constructors for horns new-contributor t-algebra t-topology merge-conflict awaiting-author ✅ ❌ ✅ ❌ ✅ ❌ ❌
11207 luigi-massacci feat(Topology/MetricSpace): Add new file with type of Katetov maps new-contributor t-topology WIP ✅ ✅ ✅ ✅ ❌ ✅ ❌
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 ✅ ✅ ✅ ✅ ❌ ✅ ❌
15448 urkud chore(*): deprecate `Option.elim'` tech debt merge-conflict awaiting-author ✅ ✅ ✅ ❌ ✅ ❌ ❌
12611 Komyyy refactor: change the format of `Repr (Equiv.Perm α)` from `{c[0, 1], c[2, 3]}` to `c[0, 1] * c[2, 3]` merge-conflict blocked-by-other-PR ✅ ✅ ❌ ❌ ✅ ✅ ❌
15941 grunweg wip: run the pedantic linter on mathlib merge-conflict WIP ✅ ❌ ✅ ❌ ❌ ✅ ❌
10349 Shamrock-Frost refactor(CategoryTheory/MorphismProperty) t-category-theory merge-conflict ✅ ❌ ✅ ❌ ✅ ✅ ❌
10350 Shamrock-Frost feat(Data/Setoid): add the operations of taking the equivalence class of an element and of saturating a set wrt an equivalence relation t-data merge-conflict ✅ ❌ ✅ ❌ ✅ ✅ ❌
13573 Shamrock-Frost feat: add multivariate polynomial modules t-algebra merge-conflict awaiting-author ✅ ✅ ✅ ❌ ✅ ❌ ❌
9795 sinhp feat: the type `Fib` of fibre of a function at a point t-category-theory awaiting-author ✅ ✅ ✅ ✅ ✅ ❌ ❌
6517 MohanadAhmed feat: discrete Fourier transform of a finite sequence t-algebra merge-conflict awaiting-author ✅ ✅ ✅ ❌ ✅ ❌ ❌
15055 sinhp feat: the category of pointed objects of a concrete category t-category-theory awaiting-author ✅ ✅ ✅ ✅ ✅ ❌ ❌
13774 grunweg chore: make expensive definitions noncomputable RFC merge-conflict ✅ ✅ ✅ ❌ ✅ ✅ ❌
13941 TucanoUrbano feat: metric entropy t-measure-probability merge-conflict awaiting-author ❌ ✅ ✅ ❌ ✅ ❌ ❌
13233 BoltonBailey feat: `abel` for multiplicative Groups/Monoids t-meta awaiting-author WIP ✅ ❌ ✅ ✅ ❌ ❌ ❌
11212 shuxuezhuyi feat(GroupTheory/GroupAction): instance `MulAction (β ⧸ H) α` t-algebra merge-conflict ✅ ✅ ✅ ❌ ✅ ✅ ❌
12610 Komyyy perf: improves the performance of the `Repr (Equiv.Perm α)` instance t-algebra merge-conflict ✅ ✅ ✅ ❌ ✅ ✅ ❌
13155 alreadydone feat(NumberTheory/EllipticDivisibilitySequence): show elliptic relations follow from even-odd recursion t-algebra t-number-theory merge-conflict awaiting-author ✅ ✅ ✅ ❌ ✅ ❌ ❌
13241 Komyyy style(Mathlib/Data/Seq/Seq): rename `Stream'.Seq` to `Sequence` merge-conflict ✅ ✅ ✅ ❌ ✅ ✅ ❌
7907 urkud feat: introduce `NthRoot` notation class t-algebra t-analysis awaiting-CI merge-conflict ✅ ❌ ✅ ❌ ✅ ❌ ❌
10977 grunweg feat: germs of smooth functions t-analysis t-topology t-differential-geometry awaiting-author ✅ ✅ ✅ ✅ ✅ ❌ ❌
14368 FMLJohn feat: morphisms from the spectrum of a field to a locally ringed space new-contributor t-algebra t-algebraic-geometry WIP ✅ ❌ ✅ ✅ ❌ ✅ ❌
15600 adomani feat: lint also `let` vs `have` t-linter merge-conflict WIP ✅ ✅ ✅ ❌ ❌ ✅ ❌
12438 jjaassoonn feat: some APIs for flat modules t-category-theory merge-conflict WIP ✅ ✅ ✅ ❌ ❌ ✅ ❌
11385 BoltonBailey feat: scripts to analyze overlap between namespaces t-meta WIP ✅ ✅ ✅ ✅ ❌ ✅ ❌
16253 Shreyas4991 feat: Basics of Discrete Fair Division in Mathlib awaiting-author WIP ✅ ❌ ✅ ✅ ❌ ❌ ❌
7162 FR-vdash-bot refactor: separate out `PGame.relabelling` t-combinatorics merge-conflict blocked-by-other-PR ✅ ✅ ❌ ❌ ✅ ✅ ❌
13590 Komyyy refactor(Mathlib/Algebra/ContinuedFractions/*): change the definition of regular continuous fractions t-algebra merge-conflict ✅ ✅ ✅ ❌ ✅ ✅ ❌
14731 adomani feat: the repeated typeclass assumption linter t-linter merge-conflict WIP ✅ ❌ ✅ ❌ ❌ ✅ ❌
14923 Multramate feat(AlgebraicGeometry/EllipticCurve/Jacobian): add equivalences between points and explicit WithZero types t-algebraic-geometry t-number-theory merge-conflict blocked-by-other-PR ✅ ❌ ❌ ❌ ✅ ✅ ❌
14943 adomani test:flag imports merge-conflict WIP ✅ ❌ ✅ ❌ ❌ ✅ ❌
15454 grunweg feat: linter for bare `open (scoped) Classical` t-linter merge-conflict blocked-by-other-PR ✅ ❌ ❌ ❌ ✅ ✅ ❌
15269 kkytola feat: Add ENNReal.floor t-order t-algebra awaiting-author blocked-by-other-PR ✅ ❌ ❌ ✅ ✅ ❌ ❌
15121 Eloitor feat: iff theorems for IsSplitEpi and IsSplitMono in opposite category new-contributor t-category-theory awaiting-author ✅ ❌ ✅ ✅ ✅ ❌ ❌
14266 dagurtomas feat(AlgebraicGeometry): define a pretopology from a RingHomProperty workshop-AIM-AG-2024 t-algebraic-geometry merge-conflict please-adopt WIP ✅ ❌ ✅ ❌ ❌ ✅ ❌
15895 madvorak feat(Computability/ContextFreeGrammar): mapping between two types of nonterminal symbols t-computability WIP ✅ ❌ ✅ ✅ ❌ ✅ ❌
12278 Rida-Hamadani feat(Combinatorics/SimpleGraph): Provide iff statements for distance equal and greater than 2 t-combinatorics awaiting-author ✅ ❌ ✅ ✅ ✅ ❌ ❌
15893 grunweg feat: boundary of a product `M \times [x,y]` t-differential-geometry merge-conflict blocked-by-other-PR ✅ ❌ ❌ ❌ ✅ ✅ ❌
14038 adomani test/decl diff in lean dev merge-conflict WIP ✅ ❌ ✅ ❌ ❌ ✅ ❌
16120 awainverse feat(ModelTheory/Algebra/Ring/Basic): Ring homomorphisms are a `StrongHomClass` for the language of rings t-logic t-algebra RFC ✅ ❌ ✅ ✅ ✅ ✅ ❌
16408 Parcly-Taxel chore: remove TODO relating to #13092 tech debt merge-conflict ✅ ✅ ✅ ❌ ✅ ✅ ❌
15942 grunweg chore: move style linters into their own file; document all current linters t-linter merge-conflict WIP ✅ ✅ ✅ ❌ ❌ ✅ ❌
13994 grunweg chore(Topology): replace continuity -> fun_prop t-topology merge-conflict ✅ ❌ ✅ ❌ ✅ ✅ ❌
8738 grunweg feat: differential of a local diffeomorphism is a continuous linear equivalence t-differential-geometry awaiting-author help-wanted ✅ ❌ ✅ ✅ ❌ ❌ ❌
16550 awainverse feat(ModelTheory): A typeclass for languages expanding other languages t-logic awaiting-author ✅ ✅ ✅ ✅ ✅ ❌ ❌
7861 shuxuezhuyi feat(Geometry/Hyperbolic/UpperHalfPlane): instance IsometricSMul PSL(2, ℝ) ℍ t-euclidean-geometry merge-conflict blocked-by-other-PR ✅ ✅ ❌ ❌ ✅ ✅ ❌
15045 Command-Master fix(LinearAlgebra/Alternating/Basic): fix `MultilinearMap.alternatization` t-algebra awaiting-author ✅ ✅ ✅ ✅ ✅ ❌ ❌
16451 Parcly-Taxel chore: `cases' ... with a a` to `rcases ... with a | a` tech debt merge-conflict blocked-by-other-PR ✅ ✅ ❌ ❌ ✅ ✅ ❌
16526 Parcly-Taxel chore: `Or 2` automated replacement of `cases'` awaiting-zulip tech debt merge-conflict ✅ ✅ ✅ ❌ ✅ ❌ ❌
16570 yuma-mizuno chore(Tactic/CategoryTheory): change `TermElabM` to `MetaM` t-meta WIP ✅ ✅ ✅ ✅ ❌ ✅ ❌
16510 grunweg chore: move style linters to `Linter/Style` t-linter merge-conflict ✅ ✅ ✅ ❌ ✅ ✅ ❌
10591 adri326 feat(Topology/Algebra/ConstMulAction): properties of continuous actions in Hausdorff spaces t-algebra t-topology awaiting-author ✅ ✅ ✅ ✅ ✅ ❌ ❌
12824 BoltonBailey refactor: `ReflTransGen` t-logic merge-conflict WIP ✅ ❌ ✅ ❌ ❌ ✅ ❌
7545 shuxuezhuyi feat: APIs of `Function.extend f g e'` when `f` is injective t-logic merge-conflict awaiting-author ✅ ✅ ✅ ❌ ✅ ❌ ❌
10765 Vierkantor feat(Tactic): `ring` modulo a given characteristic t-meta merge-conflict awaiting-author help-wanted ✅ ✅ ✅ ❌ ❌ ❌ ❌
3251 kmill feat: deriving `LinearOrder` for simple enough inductive types t-meta awaiting-author WIP ✅ ✅ ✅ ✅ ❌ ❌ ❌
16544 CBirkbeck feat(Topology/Algebra/InfiniteSum/NatInt): Add pnat lems t-analysis t-topology blocked-by-other-PR ✅ ✅ ❌ ✅ ✅ ✅ ❌
16553 grunweg WIP: tinkering with orientable manifolds t-differential-geometry blocked-by-other-PR WIP ✅ ❌ ❌ ✅ ❌ ✅ ❌
16455 adomani test: bench action merge-conflict WIP ❌ ✅ ✅ ❌ ❌ ✅ ❌
16546 CBirkbeck feat(Analysis): summable multipliable t-analysis blocked-by-other-PR ✅ ✅ ❌ ✅ ✅ ✅ ❌
8767 eric-wieser refactor(Cache): tidy lake-manifest parsing in Cache t-meta merge-conflict ✅ ❌ ✅ ❌ ✅ ✅ ❌
16391 vihdzp feat(SetTheory/Ordinal/NaturalOps): characterization of natural operations in base `ω` t-logic merge-conflict blocked-by-other-PR ✅ ❌ ❌ ❌ ✅ ✅ ❌
13480 Espio231 feat(Algebra/Lie): add Lie's theorem new-contributor t-algebra merge-conflict awaiting-author ✅ ✅ ✅ ❌ ✅ ❌ ❌
11768 JovanGerb feat: Interactive Library Rewrite new-contributor t-meta blocked-by-other-PR ✅ ✅ ❌ ✅ ✅ ✅ ❌
16382 Command-Master feat(Combinatorics/SimpleGraph/Walk): add `penultimate` and `dropLast` t-combinatorics blocked-by-other-PR ✅ ✅ ❌ ✅ ✅ ✅ ❌
14686 smorel394 feat (AlgebraicGeometry/Grassmannian): define the Grassmannian scheme workshop-AIM-AG-2024 t-algebraic-geometry please-adopt WIP ✅ ✅ ✅ ✅ ❌ ✅ ❌
14078 Ruben-VandeVelde feat(CI): continue after mk_all fails CI merge-conflict awaiting-author ✅ ❌ ✅ ❌ ✅ ❌ ❌
11800 JADekker feat : Define KappaLindelöf spaces awaiting-zulip t-topology merge-conflict please-adopt ✅ ✅ ✅ ❌ ❌ ❌ ❌
12087 JADekker feat : complete API for K-Lindelöf spaces t-topology merge-conflict please-adopt blocked-by-other-PR ✅ ✅ ❌ ❌ ❌ ✅ ❌
16633 mo271 chore(Mathlib/Algebra): minimize imports t-algebra merge-conflict ✅ ✅ ✅ ❌ ✅ ✅ ❌
15711 znssong feat(Combinatorics/SimpleGraph): Some lemmas about walk, cycle and Hamiltonian cycle new-contributor t-combinatorics awaiting-author ✅ ✅ ✅ ✅ ✅ ❌ ❌
11283 hmonroe feat(ModelTheory/Satisfiability): define theory with independent sentence t-logic merge-conflict WIP ✅ ✅ ✅ ❌ ❌ ✅ ❌
15115 kkytola feat: Generalize assumptions in liminf and limsup results in ENNReals t-order t-topology merge-conflict awaiting-author ✅ ✅ ✅ ❌ ✅ ❌ ❌
14033 pfaffelh feat(MeasureTheory): TendstoInMeasure gives ae unique limits; TendstoInMeasure equivalent to subsequences converging ae new-contributor t-measure-probability awaiting-author ✅ ✅ ✅ ✅ ✅ ❌ ❌
16914 siddhartha-gadgil Loogle syntax with non-reserved merge-conflict WIP ✅ ✅ ✅ ❌ ❌ ✅ ❌
15994 adomani feat: allow several identifiers in assert_not_exists t-meta merge-conflict ✅ ✅ ✅ ❌ ✅ ✅ ❌
10075 dupuisf refactor: generalize `MonoidHom.ker` and `MonoidHom.range` to `MonoidHomClass` t-algebra merge-conflict awaiting-author ✅ ✅ ✅ ❌ ✅ ❌ ❌
15160 joelriou refactor(CategoryTheory): making morphisms in Fullsubcategory a 1-field structure t-category-theory merge-conflict WIP ✅ ❌ ✅ ❌ ❌ ✅ ❌
10991 thorimur feat: `tfae` block tactic t-meta merge-conflict modifies-tactic-syntax WIP ✅ ✅ ✅ ❌ ❌ ✅ ❌
16773 arulandu feat(Probability/Distributions): formalize Beta distribution new-contributor t-measure-probability awaiting-author ✅ ❌ ✅ ✅ ✅ ❌ ❌
16464 Parcly-Taxel chore: deprecate `Nat.(case_)strong_induction_on` tech debt merge-conflict ✅ ✅ ✅ ❌ ✅ ✅ ❌
16944 YnirPaz feat(SetTheory/Cardinal/Cofinality): lemmas about limit ordinals and cofinality t-set-theory WIP ✅ ✅ ✅ ✅ ❌ ✅ ❌
13782 alreadydone feat(EllipticCurve): ZSMul formula in terms of division polynomials t-algebra t-algebraic-geometry t-number-theory merge-conflict blocked-by-other-PR ✅ ✅ ❌ ❌ ✅ ✅ ❌
16594 FR-vdash-bot perf: reorder `extends` and remove some instances in algebra hierarchy slow-typeclass-synthesis t-algebra merge-conflict ✅ ❌ ✅ ❌ ✅ ✅ ❌
11003 thorimur chore: migrate to `tfae` block tactic merge-conflict blocked-by-other-PR WIP ✅ ✅ ❌ ❌ ❌ ✅ ❌
8118 iwilare feat(CategoryTheory): add dinatural transformations t-category-theory merge-conflict awaiting-author ✅ ✅ ✅ ❌ ✅ ❌ ❌
10006 jstoobysmith feat(AlgebraicTopology): homotopy in quasicategories new-contributor t-category-theory merge-conflict awaiting-author blocked-by-other-PR ✅ ✅ ❌ ❌ ✅ ❌ ❌
14203 dagurtomas feat(Algebra/ModuleCat): descent data workshop-AIM-AG-2024 t-algebra t-algebraic-geometry t-category-theory merge-conflict please-adopt WIP ✅ ❌ ✅ ❌ ❌ ✅ ❌
16836 Parcly-Taxel chore: delete deprecated algebraic structure files awaiting-zulip tech debt easy merge-conflict ✅ ✅ ✅ ❌ ✅ ❌ ❌
14799 luigi-massacci feat(Analysis/MeanInequalities): Weighted QM-AM inequality new-contributor t-analysis easy awaiting-author ✅ ✅ ✅ ✅ ✅ ❌ ❌
13685 niklasmohrin feat(Combinatorics): add definitions for network flows new-contributor t-combinatorics awaiting-author ✅ ✅ ✅ ✅ ✅ ❌ ❌
14237 js2357 feat: Define the localization of a fractional ideal at a prime ideal new-contributor t-algebra awaiting-author ✅ ✅ ✅ ✅ ✅ ❌ ❌
14242 js2357 feat: Prove equivalence of `isDedekindDomain` and `isDedekindDomainDvr` new-contributor t-algebra merge-conflict blocked-by-other-PR ✅ ✅ ❌ ❌ ✅ ✅ ❌
15651 TpmKranz feat(Computability/NFA): operations for Thompson's construction t-computability new-contributor awaiting-author ✅ ✅ ✅ ✅ ✅ ❌ ❌
16387 adomani test: add creator check in new contributor merge-conflict WIP ✅ ✅ ✅ ❌ ❌ ✅ ❌
15212 victorliu5296 feat: Add fundamental theorem of calculus-2 for Banach spaces new-contributor t-measure-probability t-analysis awaiting-author ✅ ✅ ✅ ✅ ✅ ❌ ❌
16186 joneugster chore: use emoji-variant-selector `\uFE0F` for emojis ✅️,❌️,💥️,🟡️ merge-conflict awaiting-author blocked-by-other-PR ✅ ❌ ❌ ❌ ✅ ❌ ❌
16344 robertmaxton42 feat(LinearAlgebra/FreeProduct): add induction principle, further simp opts for lift new-contributor t-algebra blocked-by-other-PR ✅ ✅ ❌ ✅ ✅ ✅ ❌
17110 FR-vdash-bot chore: deprecate some lemmas about equality blocked-by-batt-PR merge-conflict ✅ ✅ ❌ ❌ ✅ ✅ ❌
13149 trivial1711 feat: multiple universe polymorphism for the equational criterion for flatness t-algebra RFC merge-conflict WIP ✅ ❌ ✅ ❌ ❌ ✅ ❌
12617 mans0954 feat(Algebra/Ring/Defs): Add NonUnitalCommSemiring.toNonUnitalNonAssocCommSemiring instance t-algebra merge-conflict ✅ ❌ ✅ ❌ ✅ ✅ ❌
7516 ADedecker perf: use `abbrev` to prevent unifying useless data merge-conflict WIP ✅ ❌ ✅ ❌ ❌ ✅ ❌
16215 adomasbaliuka feat(Tactic/Linter): lint unwanted unicode t-linter merge-conflict blocked-by-other-PR ✅ ❌ ❌ ❌ ✅ ✅ ❌
17127 FR-vdash-bot chore: remove global `Quotient.mk` `⟦·⟧` notation t-data merge-conflict ✅ ✅ ✅ ❌ ✅ ✅ ❌
17131 joneugster feat(Tactic/Linter): add unicode linter for unwanted characters t-linter merge-conflict blocked-by-other-PR ✅ ✅ ❌ ❌ ✅ ✅ ❌
13456 grunweg perf(Geometry/Manifold/Instances/Sphere): speed up t-differential-geometry merge-conflict awaiting-author ✅ ✅ ✅ ❌ ✅ ❌ ❌
13459 grunweg perf(Geometry): more small speed-ups RFC merge-conflict ✅ ❌ ✅ ❌ ✅ ✅ ❌
16887 metinersin feat(ModelTheory/Complexity): define conjunctive and disjunctive formulas new-contributor t-logic merge-conflict blocked-by-other-PR ✅ ✅ ❌ ❌ ✅ ✅ ❌
16888 metinersin feat(ModelTheory/Complexity): Define conjunctive and disjunctive normal forms new-contributor t-logic merge-conflict blocked-by-other-PR ✅ ✅ ❌ ❌ ✅ ✅ ❌
16889 metinersin feat(ModelTheory/Complexity): Normal forms new-contributor t-logic merge-conflict blocked-by-other-PR ✅ ✅ ❌ ❌ ✅ ✅ ❌
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 ✅ ✅ ✅ ❌ ✅ ❌ ❌
14752 AntoineChambert-Loir fix(Topology/Algebra/Valued): repair definition of Valued t-algebra t-topology merge-conflict WIP ✅ ❌ ✅ ❌ ❌ ✅ ❌
16956 Parcly-Taxel refactor(Order/Interval/Finset/Nat): supersymmetrise API t-order merge-conflict awaiting-author ✅ ✅ ✅ ❌ ✅ ❌ ❌
17404 YaelDillies chore: Merge the two series of lemmas on big operators in locally finite orders t-order t-algebra WIP ✅ ❌ ✅ ✅ ❌ ✅ ❌
15019 AntoineChambert-Loir feat(Mathlib.RingTheory.MvPowerSeries.Evaluation): evaluation of power series t-algebra t-topology merge-conflict blocked-by-other-PR ✅ ✅ ❌ ❌ ✅ ✅ ❌
15158 AntoineChambert-Loir feat(MvPowerSeries/Substitution): substitution of power series inside power series t-algebra merge-conflict blocked-by-other-PR ✅ ✅ ❌ ❌ ✅ ✅ ❌
14712 FR-vdash-bot perf: change instance priority and order about `OfNat` slow-typeclass-synthesis t-algebra merge-conflict delegated ✅ ✅ ✅ ❌ ✅ ✅ ❌
13740 YaelDillies feat: More robust ae notation t-measure-probability awaiting-CI t-meta ✅ ❌ ✅ ✅ ✅ ❌ ❌
9105 LukasMias feat(Algebra/Algebra/Prod): add prodUnique and uniqueProd for LinearEquiv and AlgebraEquiv t-algebra merge-conflict awaiting-author ✅ ✅ ✅ ❌ ✅ ❌ ❌
11500 mcdoll refactor(Topology/Algebra/Module/WeakDual): Clean up t-topology merge-conflict awaiting-author ✅ ✅ ✅ ❌ ✅ ❌ ❌
12994 ADedecker chore: reorganize and rename the Embedding --> Homeomorph constructions t-topology merge-conflict awaiting-author ✅ ✅ ✅ ❌ ✅ ❌ ❌
15026 grunweg fix: recognise awaiting-review comments again CI merge-conflict awaiting-author ✅ ✅ ✅ ❌ ✅ ❌ ❌
11968 JovanGerb feat: RefinedDiscrTree new-contributor t-meta merge-conflict ✅ ✅ ✅ ❌ ✅ ✅ ❌
15009 madeve-unipi feat(Analysis/Complex/Hadamard): generalize Hadamard's three lines theorem new-contributor t-analysis awaiting-author ✅ ✅ ✅ ✅ ✅ ❌ ❌
15891 grunweg feat: lemmas about the left and right boundary point under `Icc{Left,Right}Chart` t-differential-geometry merge-conflict awaiting-author ✅ ❌ ✅ ❌ ✅ ❌ ❌
14990 AntoineChambert-Loir feat: definition of linear topologies t-algebra t-topology awaiting-author ✅ ✅ ✅ ✅ ✅ ❌ ❌
5995 FR-vdash-bot feat: add APIs about `Quotient.choice` t-data RFC merge-conflict awaiting-author ✅ ✅ ✅ ❌ ✅ ❌ ❌
10190 jstoobysmith feat(AlgebraicTopology): add Augmented Simplex Category new-contributor t-algebra t-topology t-category-theory merge-conflict WIP ✅ ❌ ✅ ❌ ❌ ✅ ❌
8029 alreadydone refactor: Homotopy between Functions not ContinuousMaps t-topology RFC merge-conflict ✅ ✅ ✅ ❌ ✅ ✅ ❌
17342 Ruben-VandeVelde chore: tidy various files merge-conflict awaiting-author ✅ ✅ ✅ ❌ ✅ ❌ ❌
17624 FR-vdash-bot feat(Algebra/Order/GroupWithZero/Unbundled): generalize lemmas t-order t-algebra blocked-by-other-PR ✅ ✅ ❌ ✅ ✅ ✅ ❌
16784 digama0 feat(AlgebraicTopology/NerveAdjunction): nerve adjunction, Cat has colimits large-import t-category-theory merge-conflict blocked-by-other-PR ✅ ❌ ❌ ❌ ✅ ✅ ❌
17614 FLDutchmann feat: Count the number of pairs of `Nat`s whose `lcm` is `n` t-combinatorics t-number-theory blocked-by-other-PR ✅ ✅ ❌ ✅ ✅ ✅ ❌
14627 Multramate feat(AlgebraicGeometry/EllipticCurve/Affine): add equivalences between points and explicit WithZero types t-algebraic-geometry t-number-theory merge-conflict awaiting-author ✅ ✅ ✅ ❌ ✅ ❌ ❌
16688 vlad902 chore(scripts/install_macos): Fix 2 PATH resolution issues ❌ ✅ ✅ ✅ ✅ ✅ ✅
15916 vihdzp feat(SetTheory/Ordinal/CantorNormalForm): Coefficients of CNF as finsupp t-logic merge-conflict blocked-by-other-PR ✅ ✅ ❌ ❌ ✅ ✅ ❌
17515 FR-vdash-bot perf: do not need `simp low` now t-algebra blocked-by-other-PR ✅ ❌ ❌ ✅ ✅ ✅ ❌
17513 FR-vdash-bot perf: do not search algebraic hierarchies when using `map_*` lemmas awaiting-bench t-algebra WIP ✅ ✅ ✅ ✅ ❌ ✅ ❌
16054 vihdzp chore(SetTheory/Game/Impartial): remove `Impartial` typeclass t-combinatorics RFC merge-conflict ✅ ✅ ✅ ❌ ✅ ✅ ❌
17538 joneugster feat(scripts/autolabel): add `dependency-bump` label automatically CI merge-conflict awaiting-author ✅ ✅ ✅ ❌ ✅ ❌ ❌
13156 erdOne refactor(Algebra/Module/LocalizedModule): Redefine `LocalizedModule` in terms of `OreLocalization`. t-algebra merge-conflict ✅ ❌ ✅ ❌ ✅ ✅ ❌
14160 linesthatinterlace feat(Algebra/Group/Action/Defs): Redefine `Function.End` t-algebra merge-conflict awaiting-author WIP ✅ ❌ ✅ ❌ ❌ ❌ ❌
16348 urkud refactor(Topology): require `LinearOrder` with `OrderTopology` t-order t-topology merge-conflict awaiting-author ✅ ✅ ✅ ❌ ✅ ❌ ❌
17474 alreadydone chore: remove confounding coercions from `Submodule.(co)map` t-algebra merge-conflict please-adopt ✅ ❌ ✅ ❌ ❌ ✅ ❌
17589 joelriou feat(Algebra/ModuleCat/Presheaf): composition of pushforwards and pullbacks and compatibilites t-algebraic-geometry t-category-theory merge-conflict blocked-by-other-PR WIP ✅ ❌ ❌ ❌ ❌ ✅ ❌
6034 mattrobball feat (Mathlib.Tactic.FieldSimp) : discharger uses normCast t-meta merge-conflict awaiting-author ✅ ❌ ✅ ❌ ✅ ❌ ❌
17071 ScottCarnahan feat : (LinearAlgebra/RootSystem) : Separation, base, cartanMatrix t-algebra WIP ✅ ✅ ✅ ✅ ❌ ✅ ❌
16041 vihdzp feat(SetTheory/Ordinal/Arithmetic): `Ordinal.toNat` t-set-theory t-logic awaiting-author blocked-by-other-PR WIP ✅ ✅ ❌ ✅ ❌ ❌ ❌
17176 arulandu feat: integrals and integrability with .re new-contributor t-measure-probability awaiting-author ✅ ✅ ✅ ✅ ✅ ❌ ❌
13965 pechersky feat(Data/DigitExpansion): reals via digit expansion are complete t-data merge-conflict blocked-by-other-PR ✅ ❌ ❌ ❌ ✅ ✅ ❌
17519 grunweg feat: the `metrisableSpace` linter t-linter merge-conflict blocked-by-other-PR ✅ ✅ ❌ ❌ ✅ ✅ ❌
13159 erdOne feat(RingTheory/Smooth/LocalRing): Jacobian criterion of smoothness. t-algebra merge-conflict WIP ✅ ❌ ✅ ❌ ❌ ✅ ❌
17667 eric-wieser chore: remove lines labelled as not required porting-notes t-analysis awaiting-author ✅ ✅ ✅ ✅ ✅ ❌ ❌
17500 ahhwuhu feat: Define shifted Legendre polynomials and prove some basic properties new-contributor t-analysis awaiting-author ✅ ✅ ✅ ✅ ✅ ❌ ❌
4979 mhk119 doc(Data/Nat/Bitblast): initial commit merge-conflict ✅ ❌ ✅ ❌ ✅ ✅ ❌
15578 znssong feat(Function): Fixed points of function `f` with `f(x) >= x` new-contributor t-analysis awaiting-author ✅ ✅ ✅ ✅ ✅ ❌ ❌
15773 kkytola feat: Add type class for ENat-valued floor functions t-order awaiting-author ✅ ✅ ✅ ✅ ✅ ❌ ❌
6692 prakol16 feat: disjoint indexed union of local homeomorphisms t-topology merge-conflict ✅ ❌ ✅ ❌ ✅ ✅ ❌
7479 newell feat(Topology/MetricSpace/Similarity): define Similarity t-topology ✅ ❌ ✅ ✅ ✅ ✅ ❌
10796 mcdoll feat(Tactic/Positivity): non-negativity of functions t-meta WIP ✅ ✅ ✅ ✅ ❌ ✅ ❌
12750 Command-Master feat: define Gray code t-data new-contributor merge-conflict awaiting-author blocked-by-other-PR ✅ ❌ ❌ ❌ ✅ ❌ ❌
14603 awueth feat: degree is invariant under graph isomorphism new-contributor t-combinatorics WIP ✅ ❌ ✅ ✅ ❌ ✅ ❌
16000 YaelDillies feat: Croot-Sisask Almost Periodicity t-analysis t-combinatorics blocked-by-other-PR ✅ ✅ ❌ ✅ ✅ ✅ ❌
11633 YaelDillies refactor: Lighten finiteness dependencies large-import merge-conflict WIP ✅ ❌ ✅ ❌ ❌ ✅ ❌
16925 YnirPaz feat(SetTheory/Cardinal/Cofinality): aleph index of singular cardinal has infinite cofinality t-set-theory merge-conflict WIP ✅ ✅ ✅ ❌ ❌ ✅ ❌
13027 YaelDillies chore: Move group actions large-import t-algebra RFC awaiting-CI merge-conflict ✅ ❌ ✅ ❌ ✅ ❌ ❌
17471 joelriou feat(Algebra/ModuleCat/Differentials/Sheaf): the sheaf of relative differentials large-import t-algebraic-geometry t-category-theory merge-conflict blocked-by-other-PR WIP ✅ ❌ ❌ ❌ ❌ ✅ ❌
17514 b-mehta feat(Analysis/Convex): extreme points of doubly stochastic matrices t-analysis merge-conflict ✅ ✅ ✅ ❌ ✅ ✅ ❌
16936 Felix-Weilacher feat(Algebra/Group/Action): add definition of equidecomposition t-algebra merge-conflict ✅ ✅ ✅ ❌ ✅ ✅ ❌
17358 sgouezel feat: the tangent bundle of a product is isomorphic to the product of the tangent bundles t-differential-geometry merge-conflict WIP ✅ ✅ ✅ ❌ ❌ ✅ ❌
17757 vihdzp refactor(*): generalize typeclass assumptions in morphisms t-algebra merge-conflict WIP ✅ ❌ ✅ ❌ ❌ ✅ ❌
15720 znssong feat(SimpleGraph): The Bondy-Chvátal theorem new-contributor t-combinatorics blocked-by-other-PR ✅ ✅ ❌ ✅ ✅ ✅ ❌
17368 Felix-Weilacher feat(Topology/Baire/BaireMeasurable): add the Kuratowski-Ulam theorem t-topology merge-conflict ✅ ✅ ✅ ❌ ✅ ✅ ❌
17739 Aaron1011 feat(Topology/Order/DenselyOrdered): prove Not (IsOpen) for intervals new-contributor t-topology awaiting-author ✅ ✅ ✅ ✅ ✅ ❌ ❌
17016 vihdzp feat(SetTheory/ZFC/Basic): generalize universes of `range` t-set-theory blocked-by-other-PR ✅ ✅ ❌ ✅ ✅ ✅ ❌
18091 tukamilano feat: Hoeffding's lemma large-import new-contributor t-measure-probability awaiting-author ✅ ❌ ✅ ✅ ✅ ❌ ❌
13964 pechersky feat(Data/DigitExpansion): begin defining variant of reals without rationals t-data merge-conflict ✅ ✅ ✅ ❌ ✅ ✅ ❌
18253 callesonne feat(Bicactegory/NaturalTransformation): refactor strong natural transformations t-category-theory blocked-by-other-PR ✅ ✅ ❌ ✅ ✅ ✅ ❌
18254 callesonne feat(Bicategory/Modification/Pseudo): define modifications between strong natural transformations of pseudofunctors t-category-theory merge-conflict blocked-by-other-PR ✅ ✅ ❌ ❌ ✅ ✅ ❌
18285 callesonne feat(Bicategory/Grothendieck): functoriality of the grothendieck construction t-category-theory blocked-by-other-PR WIP ✅ ❌ ❌ ✅ ❌ ✅ ❌
12011 101damnations feat: monoidal structure on Hopf algebras t-category-theory merge-conflict blocked-by-other-PR ✅ ✅ ❌ ❌ ✅ ✅ ❌
12009 101damnations feat: tensor products of Hopf algebras t-algebra t-category-theory ✅ ❌ ✅ ✅ ✅ ✅ ❌
15654 TpmKranz feat(Computability): language-preserving maps between NFA and RE t-computability new-contributor merge-conflict blocked-by-other-PR ✅ ✅ ❌ ❌ ✅ ✅ ❌
15851 CBirkbeck feat: generators for SL(2, Z) t-algebra merge-conflict WIP ✅ ✅ ✅ ❌ ❌ ✅ ❌
18379 oeb25 feat(Topology/ENNReal): Add `ENNReal.tsum_biUnion` new-contributor t-topology ✅ ❌ ✅ ✅ ✅ ✅ ❌
18195 Whysoserioushah feat(Algebra): define `PrimitiveIdempotents` new-contributor t-algebra awaiting-author ✅ ✅ ✅ ✅ ✅ ❌ ❌
17005 YnirPaz feat(SetTheory/Cardinal/Regular): define singular cardinals t-set-theory WIP ✅ ✅ ✅ ✅ ❌ ✅ ❌
15127 goens feat(Quot): add simple lemmas on function congruence t-data new-contributor awaiting-author ✅ ✅ ✅ ✅ ✅ ❌ ❌
7850 b-mehta chore: rename `Pi.fintype` to `Pi.instFintype` easy ✅ ❌ ✅ ✅ ✅ ✅ ❌
14313 grhkm21 feat(RepresentationTheory/FdRep): FdRep is a full subcategory of Rep new-contributor t-algebra t-category-theory ✅ ❌ ✅ ✅ ✅ ✅ ❌
12799 jstoobysmith feat(LinearAlgebra/UnitaryGroup): Add properties of Special Unitary Group new-contributor t-algebra please-adopt awaiting-author ✅ ✅ ✅ ✅ ❌ ❌ ❌
12488 xroblot feat (Lattice/Covolume): Add results linking point counting in lattices and covolume t-algebra merge-conflict blocked-by-other-PR ✅ ✅ ❌ ❌ ✅ ✅ ❌
14089 callesonne feat(Bicategory/Functorbicategory): define bicategory of pseudofunctors t-category-theory merge-conflict blocked-by-other-PR ✅ ✅ ❌ ❌ ✅ ✅ ❌
9605 davikrehalt feat(Data/Finset & List): Add Lemmas for Sorting and Filtering t-data new-contributor merge-conflict please-adopt awaiting-author ✅ ❌ ✅ ❌ ❌ ❌ ❌
18252 callesonne feat(Bicategory/Oplax): Fix simp lemmas and renaming t-category-theory awaiting-author ✅ ✅ ✅ ✅ ✅ ❌ ❌
13611 callesonne feat(FiberedCategory/HasFibers): define HasFibers class t-category-theory awaiting-author ✅ ✅ ✅ ✅ ✅ ❌ ❌
7873 FR-vdash-bot perf: reorder `extends` and change instance priority in algebra hierarchy slow-typeclass-synthesis t-algebra merge-conflict blocked-by-other-PR ✅ ✅ ❌ ❌ ✅ ✅ ❌
18470 FR-vdash-bot perf: lower the priority of `Normed*.to*` instances slow-typeclass-synthesis t-algebra t-analysis ✅ ✅ ✅ ✅ ✅ ✅ ✅
18474 FR-vdash-bot perf: lower the priority of `*WithOne.to*` instances t-data slow-typeclass-synthesis t-algebra ✅ ✅ ✅ ✅ ✅ ✅ ✅
18448 jhanschoo chore(Computability/TuringMachine): split `TuringMachine.lean` t-computability new-contributor RFC merge-conflict ✅ ❌ ✅ ❌ ✅ ✅ ❌
18400 xroblot feat(Integral/Pi): a version of `polarCoord` for `pi` integrals large-import t-measure-probability blocked-by-other-PR WIP ✅ ✅ ❌ ✅ ❌ ✅ ❌
17081 jcommelin chore: add workflow for merging master into bump/v4.x.y branches CI ✅ ✅ ✅ ✅ ✅ ✅ ✅
14486 urkud feat(ENNReal/Basic): add `ofNat_ne_top` and `top_ne_ofNat` t-order t-analysis awaiting-CI awaiting-author ✅ ❌ ✅ ✅ ✅ ❌ ❌
16835 Parcly-Taxel feat: `Finpartition.attachEquiv` t-combinatorics awaiting-author ✅ ✅ ✅ ✅ ✅ ❌ ❌
17553 mo271 feat(Algebra/MvPolynomial/Degrees): degreeOf_mul_X_eq_degreeOf_add_one_iff t-algebra merge-conflict ✅ ✅ ✅ ❌ ✅ ✅ ❌
13514 madvorak feat(Computability/ContextFreeGrammar): closure under union t-computability merge-conflict blocked-by-other-PR ✅ ✅ ❌ ❌ ✅ ✅ ❌
17518 grunweg feat: lint on declarations mentioning `Invertible` or `Unique` awaiting-zulip t-linter merge-conflict blocked-by-other-PR ✅ ❌ ❌ ❌ ✅ ❌ ❌
18284 chrisflav feat(AlgebraicGeometry): relative gluing of schemes t-algebraic-geometry merge-conflict blocked-by-other-PR WIP ✅ ❌ ❌ ❌ ❌ ✅ ❌
17595 Paul-Lez feat(Order/Bounds/Basic): Add basic order lemmas new-contributor t-order awaiting-author ✅ ✅ ✅ ✅ ✅ ❌ ❌
16421 FR-vdash-bot feat: `QuotLike` t-data RFC awaiting-author ✅ ✅ ✅ ✅ ✅ ❌ ❌
10186 qawbecrdtey feat: Defining Greedoid t-data t-combinatorics awaiting-author ✅ ✅ ✅ ✅ ✅ ❌ ❌
16250 Parcly-Taxel chore: deprime `induction, cases` in `Combinatorics` tech debt t-combinatorics merge-conflict delegated ✅ ✅ ✅ ❌ ✅ ✅ ❌
13648 urkud feat(Topology/Module): generalize `ContinuousLinearMap.compSL` t-algebra t-analysis t-topology awaiting-author ✅ ❌ ✅ ✅ ✅ ❌ ❌
15373 mariainesdff feat(Analysis.Normed.Ring.Seminorm): add SmoothingSeminorm t-analysis t-number-theory merge-conflict blocked-by-other-PR ✅ ✅ ❌ ❌ ✅ ✅ ❌
8832 sebzim4500 feat: add `norm_num` extensions for factorials t-meta merge-conflict awaiting-author ✅ ✅ ✅ ❌ ✅ ❌ ❌
9654 urkud feat: add `@[mk_eq]` version of `@[mk_iff]` t-meta merge-conflict awaiting-author ✅ ✅ ✅ ❌ ✅ ❌ ❌
15129 grunweg chore: remove or tweak outdated comments about 'when X is ported' porting-notes merge-conflict awaiting-author ✅ ✅ ✅ ❌ ✅ ❌ ❌
17109 grunweg feat: warn on `autoImplicit true` tech debt t-linter merge-conflict ✅ ❌ ✅ ❌ ✅ ✅ ❌
17626 hanwenzhu chore(Tactic/Polyrith): remove polyrith dependency on Python t-meta merge-conflict ✅ ✅ ✅ ❌ ✅ ✅ ❌
16733 pechersky feat(Topology/Algebra/Valued/LocallyCompact): locally compact nonarchimedean field iff complete and DVR and finite field t-algebra blocked-by-other-PR ✅ ✅ ❌ ✅ ✅ ✅ ❌
18230 digama0 feat: `scoped[NS]` for more commands t-meta merge-conflict ✅ ❌ ✅ ❌ ✅ ✅ ❌
10654 smorel394 feat(LinearAlgebra/{ExteriorPower,LinearIndependent,TensorPower}): define the exterior powers of a module and prove some of their basic properties large-import t-algebra please-adopt blocked-by-other-PR ✅ ❌ ❌ ✅ ❌ ✅ ❌
16177 AntoineChambert-Loir feat(Mathlib/Combinatorics/Nullstellensatz) : Alon's Combinatorial Nullstellensatz t-algebra t-combinatorics merge-conflict blocked-by-other-PR ✅ ✅ ❌ ❌ ✅ ✅ ❌
16704 AntoineChambert-Loir feat(Mathlib.Data.Ordering.Dickson): Dickson orders t-order merge-conflict WIP ✅ ✅ ✅ ❌ ❌ ✅ ❌
17746 vihdzp feat(SetTheory/Ordinal/Arithmetic): make `IsNormal` a structure t-set-theory merge-conflict WIP ✅ ❌ ✅ ❌ ❌ ✅ ❌
11978 101damnations feat: monoidal category structure on bialgebras t-algebra t-category-theory awaiting-author ✅ ✅ ✅ ✅ ✅ ❌ ❌
16355 Ruben-VandeVelde feat: odd_{add,sub}_one t-algebra t-number-theory merge-conflict awaiting-author ✅ ✅ ✅ ❌ ✅ ❌ ❌
18210 vihdzp feat(Order/Hom/Basic): `WithBot (Fin n) ≃o Fin (n + 1)` t-order awaiting-author ✅ ✅ ✅ ✅ ✅ ❌ ❌
8479 alexjbest feat: use leaff in CI merge-conflict awaiting-author WIP ✅ ❌ ✅ ❌ ❌ ❌ ❌
16966 vihdzp chore(SetTheory/Ordinal/Basic): deprecate `List.Sorted.lt_ord_of_lt` t-set-theory merge-conflict awaiting-author ✅ ✅ ✅ ❌ ✅ ❌ ❌
18629 tomaz1502 feat(Computability.Timed): Formalization of runtime complexity of List.merge t-computability new-contributor ✅ ✅ ✅ ✅ ✅ ✅ ✅
15443 YaelDillies feat: The Marcinkiewicz-Zygmund inequality t-analysis awaiting-author ✅ ❌ ✅ ✅ ✅ ❌ ❌
18568 vihdzp refactor(Algebra/Order/ZeroLE): typeclass for `0` / `1` being a bottom element t-order merge-conflict WIP ✅ ❌ ✅ ❌ ❌ ✅ ❌
15779 vihdzp feat(SetTheory/Game/PGame): Improve `insertLeft` / `insertRight` API t-set-theory t-logic awaiting-author blocked-by-other-PR ✅ ❌ ❌ ✅ ✅ ❌ ❌
14598 Command-Master chore: add typeclasses to unify various `add_top`, `add_eq_top`, etc. new-contributor t-order t-algebra merge-conflict ✅ ✅ ✅ ❌ ✅ ✅ ❌
12778 MichaelStollBayreuth perf: decouple algebraic and order hierarchies in type class search slow-typeclass-synthesis t-order t-algebra merge-conflict ✅ ✅ ✅ ❌ ✅ ✅ ❌
16584 AntoineChambert-Loir feat (Mathlib/RingTheory/MvPolynomial/Groebner) : monomial orders and division t-algebra merge-conflict awaiting-author ✅ ❌ ✅ ❌ ✅ ❌ ❌
15686 robertmaxton42 refactor (LinearAlgebra/FreeProduct): move PowerAlgebra construction to its own namespace, minor simp opts new-contributor t-algebra awaiting-author ✅ ✅ ✅ ✅ ✅ ❌ ❌
15192 FR-vdash-bot feat: add some basic term elaborators large-import t-meta ✅ ✅ ✅ ✅ ✅ ✅ ✅
13786 Multramate feat(NumberTheory/EllipticDivisibilitySequence): extend even-odd recursion to integers t-number-theory ✅ ✅ ✅ ✅ ✅ ✅ ✅
18508 urkud chore(OperatorNorm/Completeness): drop a duplicate instance t-analysis help-wanted ✅ ✅ ✅ ✅ ❌ ✅ ❌
3610 TimothyGu feat: derive Infinite automatically for inductive types t-meta awaiting-author ❌ ✅ ✅ ✅ ✅ ❌ ❌
18713 dwrensha doc: update README.md instructions for building documentation locally ✅ ✅ ✅ ✅ ✅ ✅ ✅
18432 joelriou feat(Algebra/Module): presentation of the tensor product t-algebra ✅ ✅ ✅ ✅ ✅ ✅ ✅
18748 FR-vdash-bot refactor: deprecate `ContinuousLinearMapClass` t-algebra t-topology blocked-by-other-PR ✅ ✅ ❌ ✅ ✅ ✅ ❌
18756 FR-vdash-bot refactor: deprecate `DistribMulActionSemiHomClass` `MulSemiringActionSemiHomClass` t-algebra ✅ ✅ ✅ ✅ ✅ ✅ ✅
9820 jjaassoonn feat(RingTheory/GradedAlgebra/HomogeneousIdeal): generalize to homogeneous submodule t-algebra merge-conflict ✅ ✅ ✅ ❌ ✅ ✅ ❌
17908 alreadydone feat: Hopkins–Levitzki theorem t-algebra merge-conflict blocked-by-other-PR ✅ ✅ ❌ ❌ ✅ ✅ ❌
16885 metinersin feat(ModelTheory/Complexity): define literals new-contributor t-logic merge-conflict awaiting-author ✅ ✅ ✅ ❌ ✅ ❌ ❌
18716 jjaassoonn feat(Algebra/Module/GradedModule): quotient and subgrading t-algebra awaiting-CI merge-conflict blocked-by-other-PR WIP ✅ ❌ ❌ ❌ ❌ ❌ ❌
18419 alreadydone refactor: generalize `SMul (Ideal R) (Submodule R M)` to `SMul (Submodule R A) (Submodule R M)` t-algebra ✅ ✅ ✅ ✅ ✅ ✅ ✅
16619 pechersky feat(RingTheory/Valuation): valuation integers ring is a Principal Ideal ring iff the valuation range is not densely ordered t-algebra ✅ ✅ ✅ ✅ ✅ ✅ ✅
18786 Command-Master feat(RingTheory/Valuation/Basic): API for conversion `AddValuation` ↔ `Valuation` t-algebra ✅ ✅ ✅ ✅ ✅ ✅ ✅
14208 callesonne feat(AlgebraicGeometry): representability by a scheme is a local property workshop-AIM-AG-2024 t-algebraic-geometry t-category-theory merge-conflict WIP ✅ ✅ ✅ ❌ ❌ ✅ ❌
18784 erdOne feat(AlgebraicGeometry) use `addMorphismPropertyInstances` t-algebraic-geometry merge-conflict blocked-by-other-PR ✅ ❌ ❌ ❌ ✅ ✅ ❌
18780 vihdzp feat(SetTheory/Ordinal/Arithmetic): `(sInf sᶜ).card ≤ #s` t-set-theory ✅ ✅ ✅ ✅ ✅ ✅ ✅
18560 tb65536 feat(RingTheory/Invariant): Define invariant extensions of rings FLT t-algebra ✅ ✅ ✅ ✅ ✅ ✅ ✅
16801 awainverse feat(ModelTheory/Equivalence): The quotient type of formulas modulo a theory t-logic awaiting-author ✅ ✅ ✅ ✅ ✅ ❌ ❌
13124 FR-vdash-bot chore: remove `CovariantClass` and `ContravariantClass` WIP ✅ ❌ ✅ ✅ ❌ ✅ ❌
16769 Command-Master feat(Combinatorics/SimpleGraph/Walk): add `penultimate` and `snd` maintainer-merge t-combinatorics ✅ ✅ ✅ ✅ ✅ ✅ ✅
17308 YaelDillies feat: Decomposing a submodule of a product t-algebra ✅ ✅ ✅ ✅ ✅ ✅ ✅
18315 urkud chore(Filter/Prod): drop `Filter.prod`, use `SProd` instead t-order t-topology ✅ ✅ ✅ ✅ ✅ ✅ ✅
17627 hrmacbeth feat: universal properties of vector bundle constructions t-differential-geometry awaiting-author ✅ ✅ ✅ ✅ ✅ ❌ ❌
18849 sgouezel feat: manifold derivative of operations in vector spaces t-differential-geometry ✅ ✅ ✅ ✅ ✅ ✅ ✅
18790 jcommelin chore(Algebra/Lie/Weights): rename Weight to GenWeight t-algebra delegated ✅ ✅ ✅ ✅ ✅ ✅ ✅
18667 loefflerd feat(LinearAlgebra/Goursat): Goursat's lemma on submodules of products t-algebra WIP ✅ ✅ ✅ ✅ ❌ ✅ ❌
17986 adomani feat: the `#find_syntax` command t-meta ✅ ✅ ✅ ✅ ✅ ✅ ✅
13686 fpvandoorn feat: some finset lemmas large-import t-data merge-conflict awaiting-author ✅ ✅ ✅ ❌ ✅ ❌ ❌
15294 RemyDegenne feat: two Finset lemmas t-algebra merge-conflict awaiting-author ✅ ✅ ✅ ❌ ✅ ❌ ❌
18857 xroblot feat(NumberTheory/LSeries): LSeries of a counting function (part II) t-number-theory blocked-by-other-PR WIP ✅ ✅ ❌ ✅ ❌ ✅ ❌
18818 edegeltje feat(Data/Control/Traversable/Instances): Add (Lawful)Traversable instance for Tree t-data ✅ ✅ ✅ ✅ ✅ ✅ ✅
18858 xroblot feat(NumberTheory/LSeries): LSeries of a counting function (part I) t-number-theory WIP ✅ ✅ ✅ ✅ ❌ ✅ ❌
18306 bjoernkjoshanssen feat(Topology/Compactification): projective line over ℝ is homeomorphic to the one-point compactification of ℝ t-topology awaiting-author ✅ ❌ ✅ ✅ ✅ ❌ ❌
9341 winstonyin feat: Naturality of integral curves t-differential-geometry merge-conflict awaiting-author ✅ ✅ ✅ ❌ ✅ ❌ ❌
9082 Timeroot feat: `List.destutter` on cotransitive relations. t-data ✅ ✅ ✅ ✅ ✅ ✅ ✅
16014 vihdzp feat(SetTheory/Ordinal/Principal): even more lemmas on additively principal ordinals t-set-theory t-logic merge-conflict blocked-by-other-PR ✅ ❌ ❌ ❌ ✅ ✅ ❌
15099 joelriou feat(CategoryTheory/Sites): the Mayer-Vietoris long exact sequence in sheaf cohomology t-category-theory WIP ✅ ✅ ✅ ✅ ❌ ✅ ❌
18397 YaelDillies chore: Rename `RestrictGenTopology` to `Topology.IsRestrictGen` awaiting-zulip t-topology ✅ ✅ ✅ ✅ ✅ ❌ ❌
18876 Vegan-Parabola feat(ModelTheory/Fraisse): add proof that Fraïssé limits exist t-logic blocked-by-other-PR ✅ ✅ ❌ ✅ ✅ ✅ ❌
18749 Vegan-Parabola feat(ModelTheory): preparation work for proving existence of fraisse limits t-logic ✅ ✅ ✅ ✅ ✅ ✅ ✅
18438 ADedecker refactor: adapt `KrullTopology` to the new algebraic filter bases API t-algebra t-topology blocked-by-other-PR ✅ ✅ ❌ ✅ ✅ ✅ ❌
18439 ADedecker refactor: use new algebraic filter bases API in `FiniteAdeleRing` t-algebra t-topology blocked-by-other-PR ✅ ✅ ❌ ✅ ✅ ✅ ❌
18441 ADedecker refactor(AdicTopology): use new API for algebraic filter bases, and factor some code t-algebra t-topology blocked-by-other-PR ✅ ✅ ❌ ✅ ✅ ✅ ❌
18652 javierlcontreras refactor(LocalRing/Basic): generalize to non-commutative (semi)rings new-contributor t-algebra merge-conflict ✅ ✅ ✅ ❌ ✅ ✅ ❌
18914 Vierkantor fix(Tactic/Linter): the `minImports` linter understands file edits t-linter t-meta WIP ✅ ✅ ✅ ✅ ❌ ✅ ❌
18416 erdOne feat(RingTheory): the residue field of a prime ideal t-algebra ✅ ✅ ✅ ✅ ✅ ✅ ✅
17417 faenuccio feat(Counterexamples/DiscreteTopologyNonDiscreteUniformity): add a counterexample about discrete uniformity and Cauchy filters t-topology awaiting-author ✅ ❌ ✅ ✅ ✅ ❌ ❌
13349 CBirkbeck feat: some results about infinite products of the form 1+a_n t-analysis merge-conflict blocked-by-other-PR ✅ ✅ ❌ ❌ ✅ ✅ ❌
18693 Ruben-VandeVelde feat: add ConjRootClass t-algebra ✅ ✅ ✅ ✅ ✅ ✅ ✅
17956 joelriou feat(CategoryTheory/Monoidal): composition of monoidal category adjunctions t-category-theory ✅ ✅ ✅ ✅ ✅ ✅ ✅
17105 vihdzp feat(Data/List/RunLength): run-length encoding t-data blocked-by-other-PR ✅ ❌ ❌ ✅ ✅ ✅ ❌
14989 AntoineChambert-Loir feat(RingTheory.MvPowerSeries.Topology): a power series is the sum of its homogeneous components t-algebra merge-conflict blocked-by-other-PR ✅ ❌ ❌ ❌ ✅ ✅ ❌
15007 AntoineChambert-Loir feat(RingTheory.MvPowerSeries.LinearTopology): a linear topology on the ring of power series t-algebra t-topology merge-conflict blocked-by-other-PR ✅ ❌ ❌ ❌ ✅ ✅ ❌
16656 mo271 feat(Data/Fintype/List): generalize `fintypeNodupList` (no `DecidableEq`) t-data ✅ ✅ ✅ ✅ ✅ ✅ ✅
15424 pechersky feat(Valued/LocallyCompact): `totallyBounded_iff_finite_residueField` t-algebra ✅ ✅ ✅ ✅ ✅ ✅ ✅
16797 Command-Master feat(FieldTheory/Differential/Liouville): prove the algebraic case of Liouville's theorem large-import t-algebra ✅ ✅ ✅ ✅ ✅ ✅ ✅
13248 hcWang942 feat: basic concepts of auction theory new-contributor t-logic merge-conflict awaiting-author ✅ ✅ ✅ ❌ ✅ ❌ ❌
18595 pechersky chore(RingTheory/Ideal/Colon): generalize to semiring t-algebra merge-conflict ✅ ✅ ✅ ❌ ✅ ✅ ❌
18954 Command-Master feat(Algebra/Order/AddGroupWithTop): lemmas about LinearOrderedAddCommGroupWithTop t-algebra ✅ ✅ ✅ ✅ ✅ ✅ ✅
17047 AntoineChambert-Loir feat(GroupTheory/SpecificGroups/Alternating/Centralizer): compute the centralizer of a permutation in the alternating group t-algebra blocked-by-other-PR ✅ ✅ ❌ ✅ ✅ ✅ ❌
16979 Thmoas-Guan feat(FieldTheory/Galois): Lemmas of galois theory t-algebra ✅ ✅ ✅ ✅ ✅ ✅ ✅
16982 Thmoas-Guan feat(FieldTheory/Galois): Fundamental theorem of infinite galois theory t-algebra blocked-by-other-PR WIP ✅ ✅ ❌ ✅ ❌ ✅ ❌
9651 acmepjz feat(FieldTheory/LinearDisjoint): definition and basic properties of linearly disjoint of fields t-algebra ✅ ✅ ✅ ✅ ✅ ✅ ✅
12251 ScottCarnahan refactor(RingTheory/HahnSeries) : several generalizations t-order t-algebra merge-conflict WIP ✅ ✅ ✅ ❌ ❌ ✅ ❌
13483 adomani feat: automatically replace deprecations t-meta delegated ✅ ✅ ✅ ✅ ✅ ✅ ✅
18694 ooovi feat(Data/Nat/Defs): Add a commuted version of `Nat.le_div_iff_mul_le'` t-data new-contributor awaiting-author ✅ ✅ ✅ ✅ ✅ ❌ ❌
18763 sven-manthe feat: define Descriptive.Tree t-logic ✅ ✅ ✅ ✅ ✅ ✅ ✅
18608 ooovi feat(Combinatorics/SimpleGraph): add independent sets new-contributor t-combinatorics ✅ ✅ ✅ ✅ ✅ ✅ ✅
18959 YaelDillies feat: `gcongr` lemmas for `Additive`/`Multiplicative` FLT t-algebra ✅ ❌ ✅ ✅ ✅ ✅ ❌
18966 jcommelin chore(scripts/zulip_emoji_merge_delegate.py): scan more messages and channels awaiting-author ✅ ✅ ✅ ✅ ✅ ❌ ❌
18440 joelriou feat(Algebra/Module): a presentation of an algebra induces a presentation of the module of differentials t-algebra merge-conflict WIP ✅ ❌ ✅ ❌ ❌ ✅ ❌
18912 b-mehta feat(SpecialFunctions/Log): more continuity and limits for logb t-analysis awaiting-author ✅ ✅ ✅ ✅ ✅ ❌ ❌
18461 hannahfechtner feat: left and right common multiples mixins new-contributor t-algebra ✅ ✅ ✅ ✅ ✅ ✅ ✅
16239 Rida-Hamadani feat(Geometry/Manifold): orientable manifolds t-differential-geometry merge-conflict awaiting-author ✅ ❌ ✅ ❌ ✅ ❌ ❌
18728 jjaassoonn feat(RingTheory/GradedAlgebra): define homogeneous submodule t-algebra merge-conflict ✅ ✅ ✅ ❌ ✅ ✅ ❌
19000 YaelDillies feat: Kelley-Meka bound on 3AP-free sets t-combinatorics WIP ✅ ❌ ✅ ✅ ❌ ✅ ❌
18646 jxjwan feat(RingTheory): isotypic components new-contributor t-algebra ✅ ❌ ✅ ✅ ✅ ✅ ❌
18712 bryangingechen chore: add location of build.in.yml to directories checked by dependabot CI delegated ✅ ✅ ✅ ✅ ✅ ✅ ✅
18861 YaelDillies refactor: make `Set.mem_graphOn` defeq t-data awaiting-author ✅ ✅ ✅ ✅ ✅ ❌ ❌
18884 YaelDillies doc(overview): combinatorics overview awaiting-zulip documentation ✅ ✅ ✅ ✅ ✅ ❌ ❌
18627 tomaz1502 feat(Computability.Timed): Formalization of runtime complexity of insertion sort t-computability new-contributor ✅ ✅ ✅ ✅ ✅ ✅ ✅
15787 vihdzp feat(SetTheory/Game/*): `NatOrdinal →+*o Surreal` t-logic merge-conflict WIP ✅ ✅ ✅ ❌ ❌ ✅ ❌
18893 vihdzp feat(Order/InitialSeg): `InitialSeg.exists_relIso_sum` t-order ✅ ✅ ✅ ✅ ✅ ✅ ✅
18988 TwoFX feat: ind-objects are closed under products t-category-theory ✅ ✅ ✅ ✅ ✅ ✅ ✅
18266 bjoernkjoshanssen feat: Second-derivative test from calculus t-analysis ✅ ✅ ✅ ✅ ✅ ✅ ✅
18822 YaelDillies feat: vertical line test for group/module homomorphisms t-algebra ✅ ✅ ✅ ✅ ✅ ✅ ✅
19021 joelriou feat(CategoryTheory): limits of eventually constant functors from cofiltered categories t-category-theory ✅ ✅ ✅ ✅ ✅ ✅ ✅
19024 jjaassoonn feat(Algebra/Category/ModuleCat/Products): show that arbitrary coproducts agree with direct sum large-import t-algebra ✅ ✅ ✅ ✅ ✅ ✅ ✅
16216 jxjwan feat(RingTheory): isotypic components t-algebra ❌ ✅ ✅ ✅ ✅ ✅ ✅
9344 erdOne feat: Add `AddGroup.FG` -> `Module.Finite ℤ` as instances t-algebra merge-conflict awaiting-author ✅ ✅ ✅ ❌ ✅ ❌ ❌
18823 YaelDillies feat: Goursat's lemma for subgroups t-algebra blocked-by-other-PR ✅ ❌ ❌ ✅ ✅ ✅ ❌
17859 YaelDillies feat: family of kernels consistent with respect to a filtration t-measure-probability ✅ ✅ ✅ ✅ ✅ ✅ ✅
15649 TpmKranz feat(Computability): introduce Generalised NFA as bridge to Regular Expression t-computability new-contributor ✅ ✅ ✅ ✅ ✅ ✅ ✅
10668 FLDutchmann feat: Define `Nat.finMulAntidiagonal`, the `Finset` of tuples of naturals with a fixed product. t-combinatorics t-number-theory ✅ ✅ ✅ ✅ ✅ ✅ ✅
16116 jjdishere feat(Field): add theorems in Stacks Project Chapter 09FA Fields new-contributor t-algebra merge-conflict WIP ✅ ✅ ✅ ❌ ❌ ✅ ❌
19041 Vegan-Parabola chore (ModelTheory/Fraisse): simplify IsFraisse definition t-logic easy ✅ ✅ ✅ ✅ ✅ ✅ ✅
18468 FR-vdash-bot perf: lower the priority of `Ordered*.to*` instances slow-typeclass-synthesis t-order t-algebra merge-conflict ✅ ✅ ✅ ❌ ✅ ✅ ❌
18940 ocfnash feat: drop finite-dimensionality assumption from `PerfectPairing.restrictScalarsField` t-algebra merge-conflict ✅ ✅ ✅ ❌ ✅ ✅ ❌
18764 jjaassoonn feat(Algebra/Subalgebra): some lemmas about centralizers t-algebra awaiting-author ✅ ✅ ✅ ✅ ✅ ❌ ❌
18878 pimotte feat(Data/Set): add result that shows a set is even iff it splits into two sets of equal cardinality large-import t-data t-logic blocked-by-other-PR ✅ ✅ ❌ ✅ ✅ ✅ ❌
18236 joelriou feat(Algebra/Category/ModuleCat/Presheaf): the endofunctor of presheaves of modules induced by an oplax natural transformation t-algebra t-category-theory merge-conflict blocked-by-other-PR WIP ✅ ❌ ❌ ❌ ❌ ✅ ❌
18262 joelriou feat(Algebra/Category/ModuleCat/Presheaf): exterior powers of presheaves of modules t-algebra t-category-theory merge-conflict blocked-by-other-PR WIP ✅ ❌ ❌ ❌ ❌ ✅ ❌
18812 adomani feat(bench summary): report no significant changes and job_id CI ✅ ✅ ✅ ✅ ✅ ✅ ✅
16782 digama0 feat(AlgebraicTopology/Nerve): nerve is 2-coskeletal t-topology t-category-theory merge-conflict awaiting-author ✅ ✅ ✅ ❌ ✅ ❌ ❌
19062 hannahfechtner feat (Algebra/PresentedMonoid/Basic) : facts about rel t-algebra ✅ ✅ ✅ ✅ ✅ ✅ ✅
18689 Thmoas-Guan feat(Topology): Introduce HomeomorphClass t-topology ✅ ✅ ✅ ✅ ✅ ✅ ✅
16993 Thmoas-Guan feat(FieldTheory/Galois): Galois group is profinite large-import t-algebra t-topology blocked-by-other-PR WIP ✅ ✅ ❌ ✅ ❌ ✅ ❌
16991 Thmoas-Guan feat(Topology/Group): Continuous isomorphism t-algebra t-topology blocked-by-other-PR ✅ ✅ ❌ ✅ ✅ ✅ ❌
17781 robin-carlier feat(CategoryTheory/Limits/Sifted): characterization of sifted categories large-import t-category-theory ✅ ✅ ✅ ✅ ✅ ✅ ✅
19042 maddycrim feat(RingTheory/Localization/Defs): localization of a direct product injects into product of localizations new-contributor t-algebra ✅ ✅ ✅ ✅ ✅ ✅ ✅
18531 acmepjz refactor(AlgebraicGeometry/EllipticCurve/*): add `WeierstrassCurve.IsElliptic` and remove `EllipticCurve` t-algebraic-geometry ✅ ✅ ✅ ✅ ✅ ✅ ✅
8485 Multramate feat(AlgebraicGeometry/EllipticCurve/Projective): implement group law for projective coordinates t-algebraic-geometry t-number-theory merge-conflict awaiting-author ✅ ✅ ✅ ❌ ✅ ❌ ❌
12133 ADedecker feat: generalize instIsLowerProd to arbitrary products t-order t-topology merge-conflict awaiting-author ✅ ✅ ✅ ❌ ✅ ❌ ❌
16637 FR-vdash-bot perf: reorder `extends` of `(Add)Monoid` t-algebra merge-conflict WIP ✅ ❌ ✅ ❌ ❌ ✅ ❌
18527 joelriou feat(Algebra/Module): presentation of the `PiTensorProduct` t-algebra merge-conflict blocked-by-other-PR WIP ✅ ❌ ❌ ❌ ❌ ✅ ❌
18662 joelriou feat(LinearAlgebra/ExteriorPower): generators of the exterior powers t-algebra merge-conflict blocked-by-other-PR WIP ✅ ✅ ❌ ❌ ❌ ✅ ❌
18725 joelriou feat(LinearAlgebra): generators of pi tensor products t-algebra merge-conflict blocked-by-other-PR WIP ✅ ✅ ❌ ❌ ❌ ✅ ❌
18735 joelriou feat(Algebra/Module): presentation of the exterior power t-algebra merge-conflict blocked-by-other-PR WIP ✅ ❌ ❌ ❌ ❌ ✅ ❌
18754 FR-vdash-bot feat: `IsometryClass` t-topology merge-conflict blocked-by-other-PR ✅ ✅ ❌ ❌ ✅ ✅ ❌
18755 FR-vdash-bot refactor: deprecate `LinearIsometryClass` t-algebra t-analysis merge-conflict blocked-by-other-PR ✅ ✅ ❌ ❌ ✅ ✅ ❌
18771 joelriou feat(LinearAlgebra/ExteriorPower): exterior powers of free modules are free t-algebra merge-conflict blocked-by-other-PR WIP ✅ ❌ ❌ ❌ ❌ ✅ ❌
18948 Thmoas-Guan chore(Topology): move homeomorph merge-conflict blocked-by-other-PR ✅ ✅ ❌ ❌ ✅ ✅ ❌
11155 smorel394 feat(LinearAlgebra/Multilinear/DirectSum, LinearAlgebra/DirectSum/{PiTensorProduct,Finsupp}): interaction between `MultilinearMap` and `DirectSum`, and between `PiTensorProduct` and `DirectSum` t-algebra please-adopt ✅ ✅ ✅ ✅ ❌ ✅ ❌
18239 vihdzp chore(SetTheory/ZFC/Rank): clean up file t-set-theory maintainer-merge ✅ ✅ ✅ ✅ ✅ ✅ ✅
18247 su00000 feat(RingTheory/NoetherNormalization):Add noether normalization lemma new-contributor t-algebra merge-conflict WIP ✅ ✅ ✅ ❌ ❌ ✅ ❌
17638 Vierkantor feat(Tactic): `erw` tries `rw` first and warns if that succeeds t-meta WIP ✅ ✅ ✅ ✅ ❌ ✅ ❌
18437 ADedecker refactor: add refactored APIs for algebraic filter bases t-algebra t-topology ✅ ✅ ✅ ✅ ✅ ✅ ✅
16547 CBirkbeck Cot mittag leffler merge-conflict blocked-by-other-PR WIP ✅ ✅ ❌ ❌ ❌ ✅ ❌
14265 chrisflav chore(RingTheory/Generators): make algebra instance a def t-algebra merge-conflict awaiting-author ✅ ✅ ✅ ❌ ✅ ❌ ❌
17458 urkud refactor(Algebra/Group): make `IsUnit` a typeclass awaiting-zulip t-algebra merge-conflict ✅ ❌ ✅ ❌ ✅ ❌ ❌
19060 vihdzp feat(Algebra/Order/SuccPred): `IsSuccLimit` theorems for `SuccAddOrder` maintainer-merge t-order ✅ ✅ ✅ ✅ ✅ ✅ ✅
19073 javra feat(CategoryTheory): `Grothendieck.map` preserves finality merge-conflict WIP ✅ ❌ ✅ ❌ ❌ ✅ ❌
18490 xroblot feat(Analysis/PolarCoord): add versions for Lebesgue integral t-analysis ✅ ✅ ✅ ✅ ✅ ✅ ✅
19084 Louddy feat(SkewMonoidAlgebra): `coeff`, `single`, `one` and `sum` large-import new-contributor t-algebra ✅ ✅ ✅ ✅ ✅ ✅ ✅
10541 Louddy feat(Algebra/SkewMonoidAlgebra/Basic): add SkewMonoidAlgebra new-contributor t-algebra merge-conflict blocked-by-other-PR WIP ✅ ✅ ❌ ❌ ❌ ✅ ❌
18767 Happyves feat: `List.rget` and related lemmata t-data new-contributor ✅ ❌ ✅ ✅ ✅ ✅ ❌
16743 agjftucker feat(Analysis/Calculus/Implicit): define HasStrictDerivAt.implicitFunOfBivariate new-contributor t-analysis merge-conflict ✅ ✅ ✅ ❌ ✅ ✅ ❌
18596 joelriou feat(LinearAlgebra/ExteriorPower): the exterior powers, as functors t-algebra merge-conflict blocked-by-other-PR WIP ✅ ✅ ❌ ❌ ❌ ✅ ❌
18651 joelriou feat(LinearAlgebra/ExteriorPower): the pairing between the exterior power of the dual and the exterior power t-algebra merge-conflict blocked-by-other-PR WIP ✅ ✅ ❌ ❌ ❌ ✅ ❌
18624 joelriou feat(LinearAlgebra/ExteriorPower): the zeroth and first exterior powers t-algebra merge-conflict blocked-by-other-PR WIP ✅ ✅ ❌ ❌ ❌ ✅ ❌
18945 chrisflav feat(AlgebraicGeometry): the small site associated to a morphism property t-algebraic-geometry blocked-by-other-PR ✅ ❌ ❌ ✅ ✅ ✅ ❌
18590 joelriou feat(LinearAlgebra/ExteriorPower): the universal property of the exterior power t-algebra ✅ ✅ ✅ ✅ ✅ ✅ ✅
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 ✅ ✅ ✅ ✅ ✅ ✅ ✅
19106 TwoFX feat: a fan is limit iff it is after the application of coyoneda.obj X large-import t-category-theory ✅ ✅ ✅ ✅ ✅ ✅ ✅
18711 bjoernkjoshanssen feat: One-point compactification of Euclidean space homeomorphic to sphere t-differential-geometry ✅ ✅ ✅ ✅ ✅ ✅ ✅
19117 eric-wieser feat: derivatives of matrix operations t-analysis blocked-by-other-PR WIP ✅ ❌ ❌ ✅ ❌ ✅ ❌
14739 urkud feat(Measure): add `gcongr` lemmas t-measure-probability merge-conflict awaiting-author WIP help-wanted ✅ ✅ ✅ ❌ ❌ ❌ ❌
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 ✅ ❌ ✅ ❌ ❌ ✅ ❌
19030 YaelDillies feat: `f '' sᶜ = range f \ f '' s` when `f` is injective t-data easy awaiting-author ✅ ✅ ✅ ✅ ✅ ❌ ❌
18501 joelriou feat(Algebra/Homology): the stupid truncation of homological complexes large-import t-algebra t-category-theory ✅ ✅ ✅ ✅ ✅ ✅ ✅
19129 adomani feat: `#trans_import` shows the imports of the current module t-meta ✅ ✅ ✅ ✅ ✅ ✅ ✅
19127 kbuzzard doc(GroupTheory/Commensurable): clarify some docstrings t-algebra delegated documentation ✅ ✅ ✅ ✅ ✅ ✅ ✅
18990 YaelDillies feat: sup-closed sets are closed under finite suprema t-order ✅ ✅ ✅ ✅ ✅ ✅ ✅
19056 vbeffara feat(Topology/FiberBundle/Trivialization): local lifting through a Trivialization new-contributor t-topology ✅ ✅ ✅ ✅ ✅ ✅ ✅
18794 ScottCarnahan feat (RingTheory/HahnSeries/Summable) add pointwise product operation t-algebra ✅ ✅ ✅ ✅ ✅ ✅ ✅
17246 pechersky feat(RingTheory/PrimaryDecomposition): PIR of Noetherian under jacobson condition t-algebra awaiting-author ✅ ✅ ✅ ✅ ✅ ❌ ❌
18547 vihdzp feat: uncountable instances for `Ordinal` and isomorphic types t-set-theory ✅ ✅ ✅ ✅ ✅ ✅ ✅
15989 vihdzp feat(SetTheory/Ordinal/Principal): simplify characterization of additively principal ordinals t-set-theory t-logic ✅ ✅ ✅ ✅ ✅ ✅ ✅
18677 IvanRenison feat(Combinatorics/SimpleGraph): Add definitions and theorems about the coloring of sum graphs large-import t-combinatorics ✅ ✅ ✅ ✅ ✅ ✅ ✅
15277 dupuisf feat(CStarAlgebra): matrices with entries in a C⋆-algebra large-import t-analysis awaiting-author ✅ ❌ ✅ ✅ ✅ ❌ ❌
19154 TwoFX feat: coproducts in the category of Ind-objects large-import t-category-theory ✅ ✅ ✅ ✅ ✅ ✅ ✅
19158 joelriou feat(AlgebraicTopology): model categories t-category-theory blocked-by-other-PR WIP ✅ ❌ ❌ ✅ ❌ ✅ ❌
16314 FR-vdash-bot chore(Data/Quot): deprecate `ind*'` APIs t-data merge-conflict ✅ ✅ ✅ ❌ ✅ ✅ ❌
18389 joelriou feat(Algebra/Module): presentation of the restriction of scalars of a module t-algebra ✅ ✅ ✅ ✅ ✅ ✅ ✅
18414 joelriou feat(CategoryTheory/Enriched): functoriality of the enrichment of functor categories t-category-theory ✅ ✅ ✅ ✅ ✅ ✅ ✅
19133 seewoo5 feat: `isCoprime_mul_units_left`, `isCoprime_mul_units_right` t-algebra ✅ ✅ ✅ ✅ ✅ ✅ ✅
18976 joelriou feat(CategoryTheory/Enriched): enrichement of functor categories over a functor category t-category-theory blocked-by-other-PR WIP ✅ ✅ ❌ ✅ ❌ ✅ ❌
19103 joelriou feat(CategoryTheory/Closed): functor categories are monoidal closed t-category-theory blocked-by-other-PR WIP ✅ ❌ ❌ ✅ ❌ ✅ ❌
19170 peakpoint feat(Analysis/Convex/Topology): closure of interior and interior of closure for a convex set new-contributor t-topology ✅ ✅ ✅ ✅ ✅ ✅ ✅
18178 yoh-tanimoto feat(Analysis/Normed/Group/SeparationQuotient): add normed lifts and `mk` large-import t-analysis ✅ ✅ ✅ ✅ ✅ ✅ ✅
19013 quangvdao feat(Algebra/BigOperators/Fin): Add `finSigmaFinEquiv` t-algebra awaiting-author ✅ ✅ ✅ ✅ ✅ ❌ ❌
19145 vihdzp chore(SetTheory/Ordinal/Exponential): redefine ordinal exponential without `bsup` t-set-theory ✅ ✅ ✅ ✅ ✅ ✅ ✅
18985 sven-manthe feat: relate lists and infinite sequences t-data ✅ ✅ ✅ ✅ ✅ ✅ ✅
17717 tb65536 WIP: Frobenius Elements FLT t-algebra t-number-theory blocked-by-other-PR WIP ✅ ❌ ❌ ✅ ❌ ✅ ❌
18611 vihdzp feat(SetTheory/Ordinal/Veblen): the two-argument Veblen function t-set-theory ✅ ✅ ✅ ✅ ✅ ✅ ✅
17325 b-mehta feat(Data/Nat): faster computation of Nat.log t-data ✅ ✅ ✅ ✅ ✅ ✅ ✅
19179 dwrensha feat: add Nat.digits_base_pow_mul and Nat.digits_append_zeroes_append_digits t-data ✅ ✅ ✅ ✅ ✅ ✅ ✅
17758 vihdzp feat(SetTheory/Ordinal/ENat): `Ordinal.toENat` t-set-theory merge-conflict ✅ ✅ ✅ ❌ ✅ ✅ ❌
16837 vihdzp feat(Data/List/SplitBy): characterization of `List.splitBy` t-data awaiting-author ✅ ❌? ✅ ✅ ✅ ❌ ❌
19180 tb65536 feat(GroupTheory/SpecificGroups/Cyclic): Cardinality of automorphism group t-algebra ✅ ✅ ✅ ✅ ✅ ✅ ✅
18434 ChrisHughes24 chore(IsAlgClosed/Classification): Make theorems more universe polymorphic t-algebra ✅ ✅ ✅ ✅ ✅ ✅ ✅
17686 madvorak feat: Set to Function t-data WIP ✅ ✅ ✅ ✅ ❌ ✅ ❌
19139 mbkybky feat(RingTheory/Ideal/Over): define the set of all prime ideals that lie over an ideal t-algebra ✅ ✅ ✅ ✅ ✅ ✅ ✅
19092 Vierkantor chore(Data/Finsupp): split off extensionality from `Defs.lean` t-data ✅ ✅ ✅ ✅ ✅ ✅ ✅
19087 Vierkantor chore(Data/Finsupp): split off material on `single`, `update`, `erase` t-data blocked-by-other-PR ✅ ✅ ❌ ✅ ✅ ✅ ❌
14060 YnirPaz feat(SetTheory/Ordinal/Clubs): define club sets and prove basic properties new-contributor t-logic ✅ ✅ ✅ ✅ ✅ ✅ ✅
19096 chrisflav feat(AlgebraicGeometry): covers of schemes over a base t-algebraic-geometry ✅ ✅ ✅ ✅ ✅ ✅ ✅
17914 xroblot feat(NumberTheory/NumberField): proof of the Analytic Class Number Formula large-import t-number-theory merge-conflict blocked-by-other-PR WIP ✅ ✅ ❌ ❌ ❌ ✅ ❌
18502 joelriou feat(Algebra/Homology): the left homology of an extension of homological complexes t-algebra t-category-theory WIP ✅ ✅ ✅ ✅ ❌ ✅ ❌
19201 YaelDillies feat(MvPolynomial): more lemmas about `finSuccEquiv` t-algebra ✅ ✅ ✅ ✅ ✅ ✅ ✅
19198 joelriou feat(Algebra/Homology): the homology of an extension of homological complexes t-category-theory blocked-by-other-PR ✅ ✅ ❌ ✅ ✅ ✅ ❌
13442 dignissimus feat: mabel tactic for multiplicative abelian groups new-contributor t-meta merge-conflict modifies-tactic-syntax awaiting-author ✅ ❌ ✅ ❌ ✅ ❌ ❌
19031 Vierkantor chore(Data/Set): split the `CoeSort` instance to its own file t-data ✅ ✅ ✅ ✅ ✅ ✅ ✅
18085 fpvandoorn doc: factorial notation docstring t-data awaiting-zulip ✅ ❌? ✅ ✅ ✅ ❌ ❌
19199 dagurtomas feat(CategoryTheory): split up a product into a binary product t-category-theory ✅ ✅ ✅ ✅ ✅ ✅ ✅
18563 hannahfechtner feat(Algebra/FreeMonoid): free monoids over isomorphic types are isomorphic new-contributor t-algebra ✅ ✅ ✅ ✅ ✅ ✅ ✅
9598 AlexKontorovich feat(Analysis/Complex): HasPrimitives on disc t-analysis ✅ ❌ ✅ ✅ ✅ ✅ ❌
19091 Vierkantor chore(Algebra/MonoidAlgebra): split Defs.lean further t-algebra blocked-by-other-PR ✅ ✅ ❌ ✅ ✅ ✅ ❌
15906 grunweg feat: define singular `n`-manifolds t-differential-geometry awaiting-author ✅ ✅ ✅ ✅ ✅ ❌ ❌
16705 iehality feat(Computability): r.e. sets are closed under inter/union/projection/composition t-computability awaiting-author ✅ ✅ ✅ ✅ ✅ ❌ ❌
12728 joelriou feat(CategoryTheory): the localized category is monoidal t-category-theory merge-conflict WIP ✅ ❌ ✅ ❌ ❌ ✅ ❌
8661 joelriou feat(CategoryTheory/Sites): descent of sheaves t-category-theory merge-conflict WIP ✅ ✅ ✅ ❌ ❌ ✅ ❌
4197 joelriou feat/refactor: redefinition of homology + derived categories t-topology t-category-theory merge-conflict WIP ✅ ❌ ✅ ❌ ❌ ✅ ❌
17995 kex-y feat(MeasureTheory/Measure/MutuallySingular): Disjoint iff mutually singular t-measure-probability ✅ ✅ ✅ ✅ ✅ ✅ ✅
15809 archiebrowne feat(RingTheory/MvPolynomial/Ideal): introduce new lemmas about MvPolynomial Ideals new-contributor t-algebra awaiting-author ✅ ✅ ✅ ✅ ✅ ❌ ❌
13609 101damnations feat: Hopf algebra structure on monoid algebras large-import t-algebra t-category-theory delegated ✅ ✅ ✅ ✅ ✅ ✅ ✅
19058 chrisflav feat(Algebra/Category): API for `Under R` t-algebra t-category-theory ✅ ✅ ✅ ✅ ✅ ✅ ✅
19213 chrisflav feat(Algebra/Category): `Under.pushout f` is left-exact if `f` is flat. t-algebra t-category-theory blocked-by-other-PR ✅ ✅ ❌ ✅ ✅ ✅ ❌
18806 FR-vdash-bot refactor: deprecate `MulEquivClass` t-algebra merge-conflict ✅ ✅ ✅ ❌ ✅ ✅ ❌
6042 MohanadAhmed feat(LinearAlgebra/Matrix/SVD): Singular Value Decomposition of R or C Matrices t-algebra please-adopt WIP ✅ ✅ ✅ ✅ ❌ ✅ ❌
18564 kmill feat: `Encodable` deriving handler t-meta merge-conflict ✅ ✅ ✅ ❌ ✅ ✅ ❌
11820 eric-wieser feat(Algebra/Star/Unitary): add unitarySubgroup t-algebra awaiting-author ✅ ❌? ✅ ✅ ✅ ❌ ❌
16160 CBirkbeck feat: representatives for the `FixedDetMatrices` under SL action t-algebra ✅ ✅ ✅ ✅ ✅ ✅ ✅
19009 eric-wieser chore(Util/Superscript): use `register_parser_alias` t-meta easy ✅ ✅ ✅ ✅ ✅ ✅ ✅
19006 tb65536 feat(GroupTheory/Subgroup/Centralizer): The `N/C` theorem large-import t-algebra ✅ ✅ ✅ ✅ ✅ ✅ ✅
5901 FR-vdash-bot feat: more `PGame.identical` `PGame.memₗ` `PGame.memᵣ` APIs t-combinatorics merge-conflict ✅ ✅ ✅ ❌ ✅ ✅ ❌
15991 vihdzp feat(SetTheory/Ordinal/CantorNormalForm): alternate CNF recursion principle t-set-theory maintainer-merge t-logic ✅ ✅ ✅ ✅ ✅ ✅ ✅
18778 vihdzp feat(SetTheory/Cardinal/Arithmetic): omega ordinals are additively/multiplicatively principal t-set-theory ✅ ✅ ✅ ✅ ✅ ✅ ✅
18557 kmill feat: `Countable` deriving handler t-meta merge-conflict ✅ ✅ ✅ ❌ ✅ ✅ ❌
19135 mckoen feat(CategoryTheory): left and right lifting properties t-category-theory awaiting-author blocked-by-other-PR WIP ✅ ✅ ❌ ✅ ❌ ❌ ❌
19232 eric-wieser refactor(Algebra/Bilinear): generalize to non-commutative base rings t-algebra ✅ ✅ ✅ ✅ ✅ ✅ ✅
19122 Command-Master feat(Algebra/Order/Monoid/Unbundled/WithTop): add lemmas about `WithTop.map` and `WithBot.map` t-algebra ✅ ✅ ✅ ✅ ✅ ✅ ✅
18510 datokrat feat(CategoryTheory/Abelian/GrothendieckAxioms): introduce grothendieck categories new-contributor t-category-theory ✅ ✅ ✅ ✅ ✅ ✅ ✅
19237 vihdzp chore(SetTheory/Ordinal/NaturalOps): address porting notes t-set-theory ✅ ✅ ✅ ✅ ✅ ✅ ✅
10235 urkud feat: add `Decidable`, `Fintype`, `Encodable` linters awaiting-bench t-linter t-meta merge-conflict awaiting-author ✅ ✅ ✅ ❌ ✅ ❌ ❌
19066 vihdzp feat(SetTheory/Ordinal/Nimber/Field): Nimber division t-set-theory maintainer-merge ✅ ✅ ✅ ✅ ✅ ✅ ✅
17366 joelriou feat(Algebra/Category/ModuleCat): pullback of presheaves of modules t-algebra t-algebraic-geometry t-category-theory merge-conflict ✅ ✅ ✅ ❌ ✅ ✅ ❌
17469 joelriou feat(Algebra/ModuleCat/Differentials/Presheaf): the presheaf of relative differentials large-import t-algebraic-geometry t-category-theory merge-conflict blocked-by-other-PR WIP ✅ ❌ ❌ ❌ ❌ ✅ ❌
17494 joelriou feat(Algebra/Category/ModuleCat): pullback of sheaves of modules t-algebra t-algebraic-geometry t-category-theory merge-conflict blocked-by-other-PR WIP ✅ ✅ ❌ ❌ ❌ ✅ ❌
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 ✅ ✅ ✅ ❌ ✅ ❌ ❌
19244 riccardobrasca feat: generalize `Ideal.spanNorm` to allow non free extensions t-algebra ✅ ✅ ✅ ✅ ✅ ✅ ✅
19236 vihdzp refactor(SetTheory/Ordinal/NaturalOps): redefine natural addition without `blsub` t-set-theory maintainer-merge ✅ ✅ ✅ ✅ ✅ ✅ ✅
14411 haitian-yuki feat(Data/Multiset/Order): add Dershowitz-Manna Ordering and Theorem t-data new-contributor ✅ ✅ ✅ ✅ ✅ ✅ ✅
19248 YaelDillies feat: `MulLeftMono` implies `PosMulMono` t-order t-algebra ✅ ✅ ✅ ✅ ✅ ✅ ✅
18775 yoh-tanimoto feat(MeasureTheory/Integral/RieszMarkovKakutani) prove that the Riesz content is indeed a content for `NNReal` large-import t-measure-probability ✅ ✅ ✅ ✅ ✅ ✅ ✅
18238 vihdzp refactor(Order/WellFounded): deprecate `WellFounded.succ` maintainer-merge t-order ✅ ✅ ✅ ✅ ✅ ✅ ✅
18469 vihdzp chore(SetTheory/Game/PGame): deprecate primed lemmas t-set-theory maintainer-merge ✅ ✅ ✅ ✅ ✅ ✅ ✅
15915 vihdzp chore(SetTheory/Ordinal/CantorNormalForm): `CNF.exponents` and `CNF.coeffs` t-set-theory t-logic awaiting-author ✅ ✅ ✅ ✅ ✅ ❌ ❌
19193 YaelDillies refactor: make `LinearOrderedCommMonoidWithZero` extend `OrderBot` t-order t-algebra ✅ ✅ ✅ ✅ ✅ ✅ ✅
12405 xroblot feat(Analysis/BoxIntegral/UnitPartition): Prove results linking integral point counting and integrals t-analysis merge-conflict blocked-by-other-PR ✅ ✅ ❌ ❌ ✅ ✅ ❌
16303 grunweg feat(CI): check for badly formatted titles or missing/contradictory labels CI awaiting-author ✅ ✅ ✅ ✅ ✅ ❌ ❌
18580 ChrisHughes24 feat(Rat/Denumerable): Use continued fractions for denumerability large-import WIP ✅ ❌ ✅ ✅ ❌ ✅ ❌
17649 grunweg feat: add a script to check for PR title and labelling t-linter CI awaiting-author ✅ ✅ ✅ ✅ ✅ ❌ ❌
18102 j-loreaux refactor: add a `ContinuousSqrt` class to conclude `StarOrderedRing C(α, R)` large-import t-analysis t-topology ✅ ✅ ✅ ✅ ✅ ✅ ✅
19067 erdOne feat(RingTheory): Jacobi-Zariski sequence t-algebra awaiting-author ✅ ✅ ✅ ✅ ✅ ❌ ❌
10476 shuxuezhuyi feat(Topology/UniformSpace): define uniform preordered space t-topology merge-conflict awaiting-author ✅ ✅ ✅ ❌ ✅ ❌ ❌
19047 joelriou feat(CategoryTheory/SmallObject/Iteration): existence of objects (bot and succ cases) t-category-theory ✅ ✅ ✅ ✅ ✅ ✅ ✅
19221 j-loreaux feat: expand API for `CFC.posPart` t-analysis ✅ ✅ ✅ ✅ ✅ ✅ ✅
18926 LorenzoLuccioli feat: add `mul_min` and `min_mul` t-order t-algebra easy ✅ ❌ ✅ ✅ ✅ ✅ ❌
19053 vihdzp feat(Order/InitialSeg): initial segments preserve successor limits maintainer-merge t-order ✅ ✅ ✅ ✅ ✅ ✅ ✅
12052 AntoineChambert-Loir feat(GroupTheory/GroupAction/Primitive) t-algebra blocked-by-other-PR ✅ ✅ ❌ ✅ ✅ ✅ ❌
18235 vihdzp feat(SetTheory/Ordinal/Basic): notation `typeLT α = type (α := α) (· < ·)` t-set-theory maintainer-merge ✅ ✅ ✅ ✅ ✅ ✅ ✅
17027 vihdzp feat(SetTheory/ZFC/Ordinal): von Neumann hierarchy of sets large-import t-set-theory merge-conflict blocked-by-other-PR ✅ ❌ ❌ ❌ ✅ ✅ ❌
19040 kmill feat: add option `pp.mathlib.binderPredicates` large-import t-meta merge-conflict ✅ ✅ ✅ ❌ ✅ ✅ ❌
19266 vihdzp doc(SetTheory/ZFC/Ordinal): add docstrings to lemmas on transitive sets t-set-theory easy documentation ✅ ✅ ✅ ✅ ✅ ✅ ✅
16543 CBirkbeck feat(Analysis/NormedSpace/FunctionSeries): add eventually versions t-analysis ✅ ✅ ✅ ✅ ✅ ✅ ✅
19108 eric-wieser refactor: allow `deriv` to be used on topological vector spaces t-analysis ✅ ✅ ✅ ✅ ✅ ✅ ✅
19136 hrmacbeth feat: handle scalar multiplication in `linear_combination` large-import t-meta ✅ ✅ ✅ ✅ ✅ ✅ ✅
17142 peabrainiac feat(Geometry/Manifold): manifolds are locally path-connected large-import new-contributor t-topology t-differential-geometry ✅ ✅ ✅ ✅ ✅ ✅ ✅
17672 urkud refactor: turn `IsTorsionFree` into a typeclass t-algebra merge-conflict ✅ ✅ ✅ ❌ ✅ ✅ ❌
19240 nomeata refactor(Nat.Prime.Defs): use `csimp` for `Nat.decidablePrime` t-number-theory ✅ ✅ ✅ ✅ ✅ ✅ ✅
16783 digama0 feat(AlgebraicTopology/HomotopyCat): SSet.hoFunctor t-category-theory awaiting-author ✅ ✅ ✅ ✅ ✅ ❌ ❌
17087 LorenzoLuccioli feat(Data/EReal): Add results about `EReal` t-data merge-conflict ✅ ✅ ✅ ❌ ✅ ✅ ❌
18885 LorenzoLuccioli feat(EReal): add `toENNReal` t-data t-measure-probability t-topology merge-conflict blocked-by-other-PR ✅ ✅ ❌ ❌ ✅ ✅ ❌
18208 vihdzp chore(SetTheory/Ordinal/Basic): deprecate results on `WellOrder` t-set-theory maintainer-merge awaiting-author ✅ ✅ ✅ ✅ ✅ ❌ ❌
19097 Vierkantor chore(Algebra.Polynomial): split `Polynomial/Basic.lean` into smaller files t-algebra blocked-by-other-PR ✅ ✅ ❌ ✅ ✅ ✅ ❌
17593 FR-vdash-bot chore(Algebra/Order/GroupWithZero/Unbundled): deprecate useless lemmas, use `ZeroLEOneClass` t-order t-algebra merge-conflict blocked-by-other-PR ✅ ??? ❌ ❌ ✅ ✅ ❌
17623 FR-vdash-bot feat(Algebra/Order/GroupWithZero/Unbundled): add some lemmas awaiting-zulip t-order t-algebra merge-conflict ✅ ✅ ✅ ❌ ✅ ❌ ❌
19284 adomani test: commit a change only to the "master" CI build action CI ✅ ??? ✅ ✅ ✅ ✅ ❌
19282 PieterCuijpers add a variable_alias for Quantale and AddQuantale new-contributor t-algebra blocked-by-other-PR ✅ ✅ ❌ ✅ ✅ ✅ ❌
19252 YaelDillies feat(Pointwise): monotonicity of `pow` t-algebra ✅ ✅ ✅ ✅ ✅ ✅ ✅
19212 Julian feat(LinearAlgebra): add a variable_alias for VectorSpace t-algebra ✅ ✅ ✅ ✅ ✅ ✅ ✅
19271 chrisflav feat(CategoryTheory): pushforward pullback adjunction for `P.Over Q X` t-category-theory ✅ ✅ ✅ ✅ ✅ ✅ ✅
19250 pimotte feat(Combinatorics/SimpleGraph/Matching): add `IsCycles` and `IsAlternating` with basic results maintainer-merge t-combinatorics ✅ ✅ ✅ ✅ ✅ ✅ ✅
16020 adomani feat: compare PR `olean`s size with `master` maintainer-merge CI ✅ ❌ ✅ ✅ ✅ ✅ ❌
18534 joelriou feat(LinearAlgebra/PiTensorProduct): dependent version of tmulEquiv t-algebra ✅ ✅ ✅ ✅ ✅ ✅ ✅
18486 vasnesterov feat(Tactic): Tactic for computing asymptotics of real functions t-meta WIP ✅ ❌ ✅ ✅ ❌ ✅ ❌
18615 j-loreaux feat: add `NonUnital{Star}Algebra.elemental` subalgebras t-algebra t-topology ✅ ✅ ✅ ✅ ✅ ✅ ✅
18506 j-loreaux feat: approximate units in C⋆-algebras t-analysis ✅ ✅ ✅ ✅ ✅ ✅ ✅
18396 sgouezel feat: the Lie algebra of a Lie group over R or C t-differential-geometry blocked-by-other-PR ✅ ✅ ❌ ✅ ✅ ✅ ❌
19297 fpvandoorn feat(to_additive): option to not translate operations on a type ✅ ❌ ✅ ✅ ✅ ✅ ❌
19298 ScottCarnahan feat(Algebra/Vertex): Define vertex operators t-algebra ✅ ✅ ✅ ✅ ✅ ✅ ✅
19299 javierlcontreras feat(Algebra/CategoryTheory): Add CommAlgebraCat new-contributor t-algebra blocked-by-other-PR WIP ✅ ❌ ❌ ✅ ❌ ✅ ❌
19068 j-loreaux feat: prove Dini's theorem for uniform convergence t-topology ✅ ✅ ✅ ✅ ✅ ✅ ✅
18142 jjdishere feat(Topology/Algebra/Field): `ContinuousSMul` for intermediate fields t-algebra t-topology ✅ ❌ ✅ ✅ ✅ ✅ ❌
19057 emilyriehl feat(AlgebraicTopology/SimplicialSet): StrictSegal simplicial sets are 2-coskeletal t-topology t-category-theory awaiting-author ✅ ✅ ✅ ✅ ✅ ❌ ❌
19264 joelriou feat(CategoryTheory/SmallObject/Iteration): existence of objects (limit case) large-import t-category-theory blocked-by-other-PR WIP ✅ ✅ ❌ ✅ ❌ ✅ ❌
19203 joelriou feat(Algebra/Homology): API for the homology of an extension of homological complex large-import t-category-theory blocked-by-other-PR ✅ ✅ ❌ ✅ ✅ ✅ ❌
19189 YnirPaz feat(SetTheory/Ordinal/Arithmetic): order isomorphism between omega and the natural numbers t-set-theory ✅ ✅ ✅ ✅ ✅ ✅ ✅
17930 alreadydone refactor: introduce `Ideal.IsTwoSided` class for quotients of noncommutative rings t-algebra ✅ ✅ ✅ ✅ ✅ ✅ ✅
19302 fpvandoorn fix(to_additive): automatically translate all instances generated by `extends` ✅ ✅ ✅ ✅ ✅ ✅ ✅
19307 mo271 feat(LinearAlgebra/Matrix/Permanent): smul large-import t-algebra ✅ ✅ ✅ ✅ ✅ ✅ ✅
19306 joelriou feat(CategoryTheory/MorphismProperty): classes of morphisms that are stable under transfinite compositions t-order t-category-theory ✅ ✅ ✅ ✅ ✅ ✅ ✅
5297 BoltonBailey feat(Algebra/MvPolynomial): Schwartz-Zippel lemma large-import t-algebra t-combinatorics merge-conflict blocked-by-other-PR ✅ ❌ ❌ ❌ ✅ ✅ ❌
19115 alreadydone chore: allow Module over Semiring be Flat t-algebra ✅ ✅ ✅ ✅ ✅ ✅ ✅
18444 jjdishere feat(Topology/Algebra): Krasner's lemma t-algebra t-analysis t-topology t-number-theory blocked-by-other-PR WIP ✅ ❌ ❌ ✅ ❌ ✅ ❌
19310 alreadydone chore(RingTheory/Localization): golfs and generalizations t-algebra ✅ ✅ ✅ ✅ ✅ ✅ ✅
18463 vihdzp feat(SetTheory/Ordinal/Notation/FundamentalSequence): define type of fundamental sequences t-set-theory t-order ✅ ✅ ✅ ✅ ✅ ✅ ✅
18206 vihdzp chore(SetTheory/Ordinal/Basic): golf/clean up `Cardinal.ord` theorems t-set-theory ✅ ✅ ✅ ✅ ✅ ✅ ✅
19054 vihdzp refactor(SetTheory/Ordinal/Arithmetic): redefine `IsLimit` to `IsSuccLimit` t-set-theory blocked-by-other-PR ✅ ✅ ❌ ✅ ✅ ✅ ❌
19227 adomani fix(CI): unwrap `lake test` in problem matcher CI ✅ ✅ ✅ ✅ ✅ ✅ ✅
18933 vihdzp feat(SetTheory/Cardinal/Arithmetic): miscellaneous cardinality lemmas t-set-theory ✅ ✅ ✅ ✅ ✅ ✅ ✅
19146 ChrisHughes24 feat: Polynomial.isRoot_of_isRoot_iff_dvd_derivative_mul t-algebra ✅ ✅ ✅ ✅ ✅ ✅ ✅
17001 vihdzp feat(SetTheory/ZFC/Ordinal): Alternate characterizations of ordinals large-import t-set-theory ✅ ✅ ✅ ✅ ✅ ✅ ✅
19323 madvorak feat: Function to Sum decomposition t-data ✅ ??? ✅ ✅ ✅ ✅ ❌
19259 YaelDillies feat: `S ^ n = S` where `S` is a submonoid t-algebra ✅ ✅ ✅ ✅ ✅ ✅ ✅
19023 madvorak chore(Data/Set/Basic): remove redundant redeclarations t-data ✅ ✅ ✅ ✅ ✅ ✅ ✅
16992 Thmoas-Guan feat(Topology/Group/Profinite): Profinite group is limit of finite group t-algebra t-topology merge-conflict blocked-by-other-PR WIP ✅ ✅ ❌ ❌ ❌ ✅ ❌
18172 mariainesdff feat(Topology/EMetricSpace/Basic): add boundedness lemmas t-analysis ✅ ✅ ✅ ✅ ✅ ✅ ✅
19330 joelriou feat(CategoryTheory): construction of sections of functors by transfinite induction t-order t-category-theory ✅ ✅ ✅ ✅ ✅ ✅ ✅
18626 hannahfechtner feat : define Artin braid groups new-contributor t-algebra awaiting-author ✅ ✅ ✅ ✅ ✅ ❌ ❌
15466 LorenzoLuccioli feat(Probability/Kernel): `Kernel.sectL` and `sectR` t-measure-probability awaiting-author ✅ ✅ ✅ ✅ ✅ ❌ ❌
18672 TobiasLeichtfried feat: add leftmost derivation in context free grammar t-computability new-contributor merge-conflict ✅ ✅ ✅ ❌ ✅ ✅ ❌
19289 xroblot feat(NumberTheory): Abel summation t-number-theory WIP ✅ ✅ ✅ ✅ ❌ ✅ ❌
19325 madvorak style(Computability/ContextFreeGrammar/reverse): injective and surjec… t-computability easy ✅ ✅ ✅ ✅ ✅ ✅ ✅
19065 chrisflav refactor(Algebra/Category): turn homs in `AlgebraCat` into a structure t-algebra t-category-theory ✅ ✅ ✅ ✅ ✅ ✅ ✅
19233 mckoen feat(CategoryTheory): retracts of objects and morphisms t-category-theory WIP ✅ ✅ ✅ ✅ ❌ ✅ ❌
16311 madvorak feat(Computability): regular languages are context-free t-computability WIP ✅ ❌ ✅ ✅ ❌ ✅ ❌
17129 joneugster feat(Tactic/Linter): add unicode linter for unicode variant-selectors large-import t-linter merge-conflict ✅ ❌ ✅ ❌ ✅ ✅ ❌
19039 D-Thomine refactor(Probability.Martingale.BorelCantelli): move and simplify lemmas about indicators t-measure-probability t-order merge-conflict ✅ ✅ ✅ ❌ ✅ ✅ ❌
19278 RemyDegenne chore(MeasureTheory): remove the dependence of the Lebesgue decomposition on Bochner integrals t-measure-probability merge-conflict WIP ✅ ✅ ✅ ❌ ❌ ✅ ❌
19164 Command-Master Add `toWithTop`, `ofWithTop` t-data RFC ✅ ✅ ✅ ✅ ✅ ✅ ✅
19149 Command-Master feat: add `ENat.map` and lemmas t-data RFC ✅ ✅ ✅ ✅ ✅ ✅ ✅
19352 hrmacbeth chore: change some `nlinarith`s to `linear_combination`s WIP ✅ ✅ ✅ ✅ ❌ ✅ ❌
18841 hrmacbeth chore: change some `linarith`s to `linear_combination`s WIP ✅ ✅ ✅ ✅ ❌ ✅ ❌
19277 jcommelin chore(Order/ConditionallyCompleteLattice): split off `Defs.lean` from `Basic.lean` t-order ✅ ✅ ✅ ✅ ✅ ✅ ✅
19046 j-loreaux feat: define class `SemigroupAction` t-algebra merge-conflict awaiting-author ✅ ✅ ✅ ❌ ✅ ❌ ❌
19357 sgouezel feat: the pullback of a vector field in a vector space t-analysis ✅ ✅ ✅ ✅ ✅ ✅ ✅
19312 chrisflav feat(CategoryTheory/Over): more API for `post` t-category-theory ✅ ✅ ✅ ✅ ✅ ✅ ✅
18705 mans0954 feature(Algebra/Module/NestAlgebra): Nest algebras large-import t-order t-algebra awaiting-author ✅ ❌ ✅ ✅ ✅ ❌ ❌
19222 mans0954 feat(Order/Directed): DirectedOn and products t-order ✅ ✅ ✅ ✅ ✅ ✅ ✅
19150 mans0954 feat(Order/Bounds/Lattice): Bounds over collections of sets t-order ✅ ✅ ✅ ✅ ✅ ✅ ✅
19343 ScottCarnahan feat(LinearAlgebra/RootSystem/Finite): Coxeter weights are bounded above by 4 t-algebra ✅ ✅ ✅ ✅ ✅ ✅ ✅
16316 mans0954 feat(Analysis/Normed/Module/WeakDual): Banach Dieudonné Lemma WIP ✅ ❌ ✅ ✅ ❌ ✅ ❌
13918 mans0954 feat(Topology/Order/HullKernel): Add the Hull-Kernel Topology t-order t-topology awaiting-author ✅ ✅ ✅ ✅ ✅ ❌ ❌
12048 AntoineChambert-Loir feat(GroupTheory/GroupAction/Iwasawa): the Iwasawa criterion for simplicity large-import t-algebra blocked-by-other-PR ✅ ??? ❌ ✅ ✅ ✅ ❌
16062 adomani Test/ci olean size CI awaiting-author WIP ✅ ❌ ✅ ✅ ❌ ❌ ❌
19353 hrmacbeth chore: golf some term/rw proofs using `linear_combination` WIP ✅ ✅ ✅ ✅ ❌ ✅ ❌
9013 winstonyin feat: uniform time lemma for the existence of global integral curves maintainer-merge t-differential-geometry ✅ ??? ✅ ✅ ✅ ✅ ❌
16675 xroblot feat(Analysis/BoxIntegral): Add BoxPartition defined by subdivision of the integer lattice t-analysis ✅ ✅ ✅ ✅ ✅ ✅ ✅
19364 Vierkantor chore(RingTheory/Noetherian): further split `Defs.lean` t-algebra ✅ ✅ ✅ ✅ ✅ ✅ ✅
18551 joelriou feat(AlgebraicGeometry): the algebraic De Rham complex t-algebra t-algebraic-geometry merge-conflict blocked-by-other-PR WIP ✅ ❌ ❌ ❌ ❌ ✅ ❌
19205 Vierkantor chore(Data/Finsupp): split off basic scalar multiplication t-algebra delegated ✅ ✅ ✅ ✅ ✅ ✅ ✅
19367 adomani test: try emoji action CI ✅ ✅ ✅ ✅ ✅ ✅ ✅
16190 AlexBrodbelt feat(Archive/Imo): formalize IMO 1982q3 IMO new-contributor merge-conflict awaiting-author ✅ ✅ ✅ ❌ ✅ ❌ ❌
19374 sgouezel chore: avoid importing `ContDiff.Defs` in `FDeriv.Analytic` t-analysis ✅ ✅ ✅ ✅ ✅ ✅ ✅
19376 Vierkantor chore(Algebra/Polynomial): don't import `Ideal` when defining `Polynomial.roots` t-algebra ✅ ✅ ✅ ✅ ✅ ✅ ✅
19076 madvorak feat: `Matrix.fromRows_one_isTotallyUnimodular_iff` t-algebra WIP ✅ ✅ ✅ ✅ ❌ ✅ ❌
17152 sgouezel feat: update the `ContDiff` definition to integrate analytic functions in the hierarchy t-analysis blocked-by-other-PR ✅ ✅ ❌ ✅ ✅ ✅ ❌
12053 AntoineChambert-Loir feat(GroupTheory/GroupAction/Primitive): lemmas about primitive actions for finite sets large-import t-algebra blocked-by-other-PR ✅ ✅ ❌ ✅ ✅ ✅ ❌
19275 eric-wieser fix: if nolint files change, do a full rebuild delegated ✅ ✅ ✅ ✅ ✅ ✅ ✅
17732 eric-wieser feat: notation for Euclidean space t-analysis ✅ ✅ ✅ ✅ ✅ ✅ ✅
19163 erdOne feat(Polynomial): bounding the coefficients of `modByMonic`/`divByMonic` t-algebra blocked-by-other-PR ✅ ✅ ❌ ✅ ✅ ✅ ❌
13649 FR-vdash-bot chore: redefine `Nat.bit` `Nat.div2` `Nat.bodd` merge-conflict ✅ ✅ ✅ ❌ ✅ ✅ ❌
19342 Ruben-VandeVelde chore: split out Algebra.GroupWithZero.Nat ✅ ✅ ✅ ✅ ✅ ✅ ✅
19337 zeramorphic feat(Data/Finsupp): generalise `Finsupp` to any "zero" value t-data merge-conflict ✅ ✅ ✅ ❌ ✅ ✅ ❌
19384 grunweg refactor(lint-style): make sure to read the nolints file outside of t… t-linter ✅ ✅ ✅ ✅ ✅ ✅ ✅
19126 alreadydone feat(RingTheory/LocalProperties): adapt #19080 to #19118 t-algebra awaiting-author ✅ ✅ ✅ ✅ ✅ ❌ ❌
17813 vihdzp feat(SetTheory/Cardinal/Arithmetic): cardinality of ordinal exponential t-set-theory ✅ ✅ ✅ ✅ ✅ ✅ ✅
19296 sgouezel chore: remove the `Smooth` alias for infinitely differentiable functions between manifolds t-differential-geometry ✅ ✅ ✅ ✅ ✅ ✅ ✅
19281 Vierkantor Split polynomial.algebra t-algebra merge-conflict blocked-by-other-PR ✅ ✅ ❌ ❌ ✅ ✅ ❌
19080 su00000 feat(RingTheory/LocalProperties): Add theorems about LocalizedModule new-contributor t-algebra ✅ ✅ ✅ ✅ ✅ ✅ ✅
19362 winstonyin feat: locally compact manifolds are finite-dimensional t-differential-geometry ✅ ✅ ✅ ✅ ✅ ✅ ✅
19354 kim-em chore: split Order.Filter.Basic, creating Order.Filter.Finite longest-pole ✅ ✅ ✅ ✅ ✅ ✅ ✅
19350 kim-em chore: split notation typeclasses out of Algebra.Group.Defs t-algebra ✅ ✅ ✅ ✅ ✅ ✅ ✅
18578 mans0954 feat(LinearAlgebra/QuadraticForm/Basis): basis expansion of a quadratic map t-algebra ✅ ✅ ✅ ✅ ✅ ✅ ✅
19370 Vierkantor chore(RingTheory): split up `Algebraic.lean` t-algebra merge-conflict ✅ ✅ ✅ ❌ ✅ ✅ ❌
16361 vihdzp chore(SetTheory/Ordinal/FixedPointApproximants): golf + better variable management t-set-theory t-logic merge-conflict awaiting-author ✅ ✅ ✅ ❌ ✅ ❌ ❌
19329 adomani perf(CI): automatically benchmark PRs when they are opened CI WIP ✅ ✅ ✅ ✅ ❌ ✅ ❌
19291 PieterCuijpers feat: quantale homomorphisms new-contributor t-algebra ✅ ❌ ✅ ✅ ✅ ✅ ❌
19393 LeoDog896 feat:(SetTheory/Game/PGame): down and up games t-set-theory ✅ ✅ ✅ ✅ ✅ ✅ ✅
19377 pimotte feat(Combinatorics/SimpleGraph): add lemmas about `spanningCoe` t-combinatorics ✅ ✅ ✅ ✅ ✅ ✅ ✅
18406 mans0954 refactor(LinearAlgebra/SesquilinearForm): Hermitian sesquilinear maps t-algebra merge-conflict ✅ ✅ ✅ ❌ ✅ ✅ ❌
19397 IvanRenison feat(Algebra/Ring/Parity): Add lemma `odd_add_self_sub_one` t-algebra easy ✅ ✅ ✅ ✅ ✅ ✅ ✅
17097 LorenzoLuccioli feat: measurability of addition and multiplication on `EReal` t-measure-probability ✅ ✅ ✅ ✅ ✅ ✅ ✅
19245 YaelDillies feat: algebraic properties of `Finset.sup` large-import t-order t-algebra ✅ ✅ ✅ ✅ ✅ ✅ ✅
19293 YaelDillies feat: more `eLpNorm` API t-measure-probability ✅ ✅ ✅ ✅ ✅ ✅ ✅
19399 YaelDillies feat(GroupTheory): some lemmas about blocks t-algebra ✅ ✅ ✅ ✅ ✅ ✅ ✅
19388 eric-wieser chore: make map_ofNat a simp lemma t-algebra ✅ ✅ ✅ ✅ ✅ ✅ ✅
19085 su00000 feat(RingTheory/LocalProperties): flatness is a local property large-import new-contributor t-algebra blocked-by-other-PR ✅ ✅ ❌ ✅ ✅ ✅ ❌
17334 FMLJohn feat(RingTheory/Polynomial/Hilbert): the Hilbert polynomial in terms of a natural number `d` and a polynomial `p : ℤ[X]` t-algebra t-algebraic-geometry awaiting-author WIP ✅ ❌? ✅ ✅ ❌ ❌ ❌
16532 grunweg feat: rewrite the linter for spaces before semicolons in Lean t-linter merge-conflict delegated ✅ ✅ ✅ ❌ ✅ ✅ ❌
19403 YaelDillies chore: rename `Codisjoint_comm` to `codisjoint_comm` t-order easy ✅ ✅ ✅ ✅ ✅ ✅ ✅
19406 YaelDillies feat: `{a, b} * s = a • s ∪ b • s` t-algebra ✅ ✅ ✅ ✅ ✅ ✅ ✅
19407 YaelDillies feat: `(t \ s).ncard = t.ncard - s.ncard` in a ring t-data ✅ ✅ ✅ ✅ ✅ ✅ ✅
19285 YaelDillies feat: more `bound` lemmas t-algebra delegated ✅ ✅ ✅ ✅ ✅ ✅ ✅
19124 yhtq fead: Add `lift_unique`, `lift_unique'` to `IsFractionRing` new-contributor t-algebra awaiting-author ✅ ✅ ✅ ✅ ✅ ❌ ❌
19391 grhkm21 feat: prove `zmodRepr` is unique t-number-theory awaiting-author ✅ ✅ ✅ ✅ ✅ ❌ ❌
19373 pimotte feat(Combinatorics/SimpleGraph/Path): add `IsPath.getVert_injOn` maintainer-merge t-combinatorics ✅ ✅ ✅ ✅ ✅ ✅ ✅
19405 jcommelin chore(discover-lean-pr-testing): ignore stage0 PRs, more tracing CI delegated ✅ ✅ ✅ ✅ ✅ ✅ ✅
19410 eric-wieser doc: describe why map_ofNat can't be simp (yet) t-data ✅ ✅ ✅ ✅ ✅ ✅ ✅
19321 jcommelin chore: change associativity of `+ᵥ` from `infixl` to `infixr` ✅ ✅ ✅ ✅ ✅ ✅ ✅
19387 PieterCuijpers feat: introduce the missing notation for `AddHom` maintainer-merge new-contributor t-algebra ✅ ✅ ✅ ✅ ✅ ✅ ✅
14866 AntoineChambert-Loir feat(RingTheory.MvPowerSeries.Topology): define the product topology on mv power series t-algebra awaiting-author ✅ ❌ ✅ ✅ ✅ ❌ ❌
19171 AntoineChambert-Loir feat: additivize equivariance of morphisms of actions maintainer-merge t-algebra ✅ ✅ ✅ ✅ ✅ ✅ ✅
19401 YaelDillies chore: rename `forall_image2_iff` to `forall_mem_image2` ✅ ✅ ✅ ✅ ✅ ✅ ✅
19371 adomani feat: trigger automated Zulip emojis via `bors x` command CI ✅ ✅ ✅ ✅ ✅ ✅ ✅
18891 alreadydone feat: ring with discrete PrimeSpectrum t-algebra t-algebraic-geometry awaiting-author ✅ ❌ ✅ ✅ ✅ ❌ ❌
18691 erdOne feat: the free locus of a (finitely presented) module large-import t-algebra ✅ ✅ ✅ ✅ ✅ ✅ ✅
18836 jsm28 feat(Data/Nat/Nth): `nth_add_one` t-data ✅ ✅ ✅ ✅ ✅ ✅ ✅
19200 dagurtomas feat(CategoryTheory): expand the API for AB axioms large-import t-category-theory ✅ ✅ ✅ ✅ ✅ ✅ ✅
19412 YaelDillies feat: growth of a finset in the quotient and intersection with a subgroup t-combinatorics ✅ ✅ ✅ ✅ ✅ ✅ ✅
15874 vihdzp doc(Order/InitialSeg): Improve documentation t-order documentation ✅ ✅ ✅ ✅ ✅ ✅ ✅
17444 FR-vdash-bot refactor: make `CanonicallyOrdered...` mixin t-order t-algebra merge-conflict ✅ ✅ ✅ ❌ ✅ ✅ ❌
19398 YaelDillies feat: `Icc a b + Icc c d = Icc (a + c) (b + d)` t-order t-algebra ✅ ✅ ✅ ✅ ✅ ✅ ✅
19411 YaelDillies feat: `Polynomial.map f` strictly decreases the degree if `f p.leadingCoeff = 0` t-algebra ✅ ❌ ✅ ✅ ✅ ✅ ❌
19409 YaelDillies chore: rename `CompleteLattice.Independent`/`.SetIndependent` to `iSupIndep`/`sSupIndep` t-order WIP ✅ ❌ ✅ ✅ ❌ ✅ ❌
19002 YaelDillies chore: move pointwise set files to `Algebra._.Pointwise` t-algebra merge-conflict ✅ ✅ ✅ ❌ ✅ ✅ ❌
17522 AntoineChambert-Loir feat(GroupTheory/Perm/Centralizer): study the centralizer of a permutation t-algebra awaiting-author ✅ ✅ ✅ ✅ ✅ ❌ ❌
19125 yhtq feat: add theorems to transfer `IsGalois` between pairs of fraction rings new-contributor t-algebra merge-conflict blocked-by-other-PR ✅ ❌ ❌ ❌ ✅ ✅ ❌
19141 mbkybky feat(NumberTheory/RamificationInertia): `ramificationIdx` and `inertiaDeg` in Galois extensions t-number-theory merge-conflict blocked-by-other-PR WIP ✅ ✅ ❌ ❌ ❌ ✅ ❌
19414 vihdzp feat: Nesbitt's inequality large-import t-algebra awaiting-author blocked-by-other-PR WIP ✅ ❌ ❌ ✅ ❌ ❌ ❌
19417 vihdzp chore(SetTheory/Game/Ordinal): make `Ordinal.toGame` an order embedding t-set-theory ✅ ✅ ✅ ✅ ✅ ✅ ✅
19404 FMLJohn feat(RingTheory/Polynomial/Hilbert): given a natural number `d` and a polynomial `p : ℤ[X]`, proved the key property of the Hilbert polynomial in terms of `d` and `p` t-algebra t-algebraic-geometry blocked-by-other-PR ✅ ✅ ❌ ✅ ✅ ✅ ❌
19378 adamtopaz feat: Explanation widgets t-meta ✅ ✅ ✅ ✅ ✅ ✅ ✅
19413 adomani chore: remove unused variables ✅ ✅ ✅ ✅ ✅ ✅ ✅
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 ✅ ✅ ✅ ✅ ✅ ✅ ✅
19415 vihdzp chore: move results on `Σ i : Fin n, f i` earlier t-data awaiting-CI ✅ ❌ ✅ ✅ ✅ ❌ ❌
19420 vihdzp feat: AM-HM inequality t-algebra ✅ ✅ ✅ ✅ ✅ ✅ ✅
18785 erdOne feat(CategoryTheory): command that generates instances for `MorphismProperty` t-category-theory t-meta ✅ ❌? ✅ ✅ ✅ ✅ ❌
19270 gio256 feat(AlgebraicTopology): StrictSegal simplicial sets are quasicategories new-contributor t-category-theory awaiting-author ✅ ✅ ✅ ✅ ✅ ❌ ❌
19419 erdOne feat(AlgebraicGeometry): integral = universally closed + affine large-import t-algebraic-geometry ✅ ✅ ✅ ✅ ✅ ✅ ✅
19421 MichaelStollBayreuth feat(NumberTheory/LSeries/PrimesInAP): proof of Dirichlet's Theorem t-number-theory ✅ ✅ ✅ ✅ ✅ ✅ ✅
19358 urkud chore(Filter): move defs of `Filter.IsBounded` etc t-order t-topology easy ✅ ✅ ✅ ✅ ✅ ✅ ✅
18919 urkud chore(Topology/../LiminfLimsup): change assumptions of 2 instances t-order t-topology ✅ ✅ ✅ ✅ ✅ ✅ ✅
19130 erdOne chore(AlgebraicGeometry) add `Scheme.Hom.appTop` t-algebraic-geometry ready-to-merge ✅ ✅ ✅ ✅ ✅ ✅ ✅
6718 FR-vdash-bot feat: Lindemann-Weierstrass Theorem t-algebra t-analysis blocked-by-other-PR WIP ✅ ❌ ❌ ✅ ❌ ✅ ❌
19422 urkud chore(*): fix `initialize_simps_projections` commands ✅ ❌ ✅ ✅ ✅ ✅ ❌
19395 kim-em chore: more simpNF cleanup ready-to-merge delegated ✅ ✅ ✅ ✅ ✅ ✅ ✅
19315 quangvdao feat(Finsupp/Fin): Add `Finsupp` operations on `Fin` tuples t-data ✅ ✅ ✅ ✅ ✅ ✅ ✅