Why is my PR not on the queue?

This page was last updated on: July 05, 2025 at 10:35 UTC

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

For PRs which add new code (as opposed to e.g. performance optimisation, refactoring or documentation), it is very helpful to add a corresponding area label. Otherwise, it may take longer to find a suitable reviewer.

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 CI status? not blocked? no merge conflict? ready? awaiting review? On the review queue? Missing topic label? PR's overall status
14583 lecopivo fix: make concrete cycle notation local awaiting-author ✅ ✅ ✅ ✅ ❌ ❌ awaiting author
14727 jjaassoonn feat(RingTheory/Flat/CategoryTheory): a flat module has vanishing higher Tor groups t-algebra awaiting-author ✅ ✅ ✅ ✅ ❌ ❌ awaiting author
14444 digama0 fix(GeneralizeProofs): unreachable! bug t-meta awaiting-author ✅ ✅ ✅ ✅ ❌ ❌ awaiting author
14345 digama0 feat: the Dialectica category is monoidal closed t-category-theory awaiting-author ✅ ✅ ✅ ✅ ❌ ❌ awaiting author
12452 JADekker feat(Cocardinal) : add some more api t-topology awaiting-CI ❌ ✅ ✅ ✅ ❌ ❌ does not pass CI
13036 joelriou feat(CategoryTheory/Sites): under certain conditions, cover preserving functors preserve 1-hypercovers t-category-theory WIP ✅ ✅ ✅ ❌ ✅ ❌ labelled WIP
12006 adomani feat: the `suffa` tactic t-meta awaiting-author ✅ ✅ ✅ ✅ ❌ ❌ awaiting author
10998 hmonroe feat(Logic): Arithmetization of partial recursive functions (toward Gödel's first incompleteness theorem) t-logic awaiting-author ✅ ✅ ✅ ✅ ❌ ❌ awaiting author
10099 mcdoll feat: Integration by parts for higher dimensional spaces t-measure-probability t-analysis WIP ❌ ✅ ✅ ❌ ✅ ❌ labelled WIP
9352 chenyili0818 feat: arithmetic lemmas for `gradient` t-analysis awaiting-author ✅ ✅ ✅ ✅ ❌ ❌ awaiting author
9510 eric-wieser feat(Analysis/Calculus/DualNumber): Extending differentiable functions to dual numbers t-algebra t-analysis awaiting-CI WIP ❌ ✅ ✅ ❌ ❌ ❌ labelled WIP
9469 dupuisf feat: maximum modulus principle for functions vanishing at infinity t-analysis awaiting-author ✅ ✅ ✅ ✅ ❌ ❌ awaiting author
6859 MohanadAhmed TryLean4Bundle: Windows Bundle Creator CI WIP help-wanted ✅ ✅ ✅ ❌ ✅ ❌ looking for help
7125 eric-wieser feat: additive monoid structure via biproducts t-category-theory awaiting-CI WIP ❌ ✅ ✅ ❌ ❌ ❌ labelled WIP
5745 alexjbest feat: a tactic to consume type annotations, and make constructor nicer t-meta awaiting-author ✅ ✅ ✅ ✅ ❌ ❌ awaiting author
15224 AnthonyBordg feat(CategoryTheory/Sites): covering families and their associated Grothendieck topology new-contributor t-category-theory awaiting-author ✅ ✅ ✅ ✅ ❌ ❌ awaiting author
14563 awueth feat: if-then-else of exclusive or statement new-contributor t-algebra awaiting-author ✅ ✅ ✅ ✅ ❌ ❌ awaiting author
14733 jjaassoonn feat(RingTheory/Flat/CategoryTheory): a module is flat iff tensoring preserves finite limits t-algebra awaiting-author ✅ ✅ ✅ ✅ ❌ ❌ awaiting author
10387 adomani feat(Tactic/ComputeDegree): add `polynomial` tactic RFC t-meta WIP ✅ ✅ ✅ ❌ ✅ ❌ labelled WIP
9693 madvorak feat: Linear programming in the standard form t-algebra RFC WIP ✅ ✅ ✅ ❌ ✅ ❌ labelled WIP
7386 madvorak feat: Define linear programs t-algebra RFC WIP ✅ ✅ ✅ ❌ ✅ ❌ labelled WIP
7219 Ruben-VandeVelde feat: Equivs for AddMonoidAlgebras t-algebra awaiting-author ❌ ✅ ✅ ✅ ❌ ❌ failing CI
13163 erdOne feat(.vscode/module-docstring.code-snippet): Prevent auto-complete from firing on `do` t-meta awaiting-author ✅ ✅ ✅ ✅ ❌ ❌ awaiting author
10026 madvorak Linear programming according to Antoine Chambert-Loir's book t-algebra RFC WIP ✅ ✅ ✅ ❌ ✅ ❌ labelled WIP
10159 madvorak Linear programming according to Antoine Chambert-Loir's book — affine version t-algebra RFC WIP ❌ ✅ ✅ ❌ ✅ ❌ labelled WIP
11890 adomani feat: the terminal refine linter t-linter awaiting-author ✅ ✅ ✅ ✅ ❌ ❌ awaiting author
11207 luigi-massacci feat(Topology/MetricSpace): Add new file with type of Katetov maps new-contributor t-topology WIP ✅ ✅ ✅ ❌ ✅ ❌ labelled 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 ✅ ✅ ✅ ❌ ✅ ❌ looking for help
9795 sinhp feat: the type `Fib` of fibre of a function at a point t-category-theory awaiting-author ✅ ✅ ✅ ✅ ❌ ❌ awaiting author
15055 sinhp feat: the category of pointed objects of a concrete category t-category-theory awaiting-author ✅ ✅ ✅ ✅ ❌ ❌ awaiting author
16253 Shreyas4991 feat: Basics of Discrete Fair Division in Mathlib awaiting-author WIP ❌ ✅ ✅ ❌ ❌ ❌ ⚠️ labelled WIP
15121 Eloitor feat: iff theorems for IsSplitEpi and IsSplitMono in opposite category new-contributor t-category-theory awaiting-author ❌ ✅ ✅ ✅ ❌ ❌ failing CI
15895 madvorak feat(Computability/ContextFreeGrammar): mapping between two types of nonterminal symbols t-computability WIP ❌ ✅ ✅ ❌ ✅ ❌ labelled WIP
12278 Rida-Hamadani feat(Combinatorics/SimpleGraph): Provide iff statements for distance equal and greater than 2 t-combinatorics awaiting-author ❌ ✅ ✅ ✅ ❌ ❌ failing CI
16570 yuma-mizuno chore(Tactic/CategoryTheory): change `TermElabM` to `MetaM` t-meta WIP ✅ ✅ ✅ ❌ ✅ ❌ labelled WIP
10591 adri326 feat(Topology/Algebra/ConstMulAction): properties of continuous actions in Hausdorff spaces t-algebra t-topology awaiting-author ✅ ✅ ✅ ✅ ❌ ❌ awaiting author
16773 arulandu feat(Probability/Distributions): formalize Beta distribution new-contributor t-measure-probability awaiting-author ❌ ✅ ✅ ✅ ❌ ❌ failing CI
14237 js2357 feat: Define the localization of a fractional ideal at a prime ideal new-contributor t-algebra awaiting-author ✅ ✅ ✅ ✅ ❌ ❌ awaiting author
16041 vihdzp feat(SetTheory/Ordinal/Arithmetic): `Ordinal.toNat` t-set-theory t-logic awaiting-author blocked-by-other-PR WIP ✅ ❌ ✅ ❌ ❌ ❌ blocked on another PR
10796 mcdoll feat(Tactic/Positivity): non-negativity of functions t-meta WIP ✅ ✅ ✅ ❌ ✅ ❌ labelled WIP
14603 awueth feat: degree is invariant under graph isomorphism new-contributor t-combinatorics WIP ❌ ✅ ✅ ❌ ✅ ❌ labelled WIP
15809 archiebrowne feat(RingTheory/MvPolynomial/Ideal): introduce new lemmas about MvPolynomial Ideals new-contributor t-algebra awaiting-author ✅ ✅ ✅ ✅ ❌ ❌ awaiting author
6042 MohanadAhmed feat(LinearAlgebra/Matrix/SVD): Singular Value Decomposition of R or C Matrices t-algebra please-adopt WIP ✅ ✅ ✅ ❌ ✅ ❌ looking for help
11820 eric-wieser feat(Algebra/Star/Unitary): add unitarySubgroup t-algebra awaiting-author ❌? ✅ ✅ ✅ ❌ ❌ infrastructure-related CI failing
19329 adomani perf(CI): automatically benchmark PRs when they are opened CI WIP ✅ ✅ ✅ ❌ ✅ ❌ labelled WIP
18876 GabinKolly feat(ModelTheory/Fraisse): add proof that Fraïssé limits exist t-logic blocked-by-other-PR ✅ ❌ ✅ ✅ ✅ ❌ blocked on another PR
20029 FrederickPu Allow for Config attributes to be set directly new-contributor t-meta WIP ✅ ✅ ✅ ❌ ✅ ❌ labelled WIP
18236 joelriou feat(Algebra/Category/ModuleCat/Presheaf): the endofunctor of presheaves of modules induced by an oplax natural transformation t-algebra t-category-theory WIP ✅ ✅ ✅ ❌ ✅ ❌ labelled WIP
20208 js2357 feat: Define the localization of a fractional ideal at a prime ideal t-algebra WIP ❌ ✅ ✅ ❌ ✅ ❌ labelled WIP
20428 madvorak feat(Data/Sign): lemmas about `∈ Set.range SignType.cast` t-data WIP ❌ ✅ ✅ ❌ ✅ ❌ labelled WIP
20459 Ruben-VandeVelde chore: fix names of roots_C_mul_X_{add,sub}_C_of_IsUnit t-algebra awaiting-author ✅ ✅ ✅ ✅ ❌ ❌ awaiting author
10977 grunweg feat: germs of smooth functions t-analysis t-topology t-differential-geometry awaiting-author ❌ ✅ ✅ ✅ ❌ ❌ failing CI
19378 adamtopaz feat: Explanation widgets t-meta awaiting-author ✅ ✅ ✅ ✅ ❌ ❌ awaiting author
19323 madvorak feat: Function to Sum decomposition t-data WIP ✅ ✅ ✅ ❌ ✅ ❌ labelled WIP
18461 hannahfechtner feat: left and right common multiples mixins new-contributor t-algebra awaiting-author ✅ ✅ ✅ ✅ ❌ ❌ awaiting author
20797 vbeffara feat(Topology/Covering): CM version of eq_of_comp_eq new-contributor t-topology easy awaiting-author ✅ ✅ ✅ ✅ ❌ ❌ awaiting author
13973 digama0 feat: lake exe refactor, initial framework t-meta awaiting-author ✅ ✅ ✅ ✅ ❌ ❌ awaiting author
17589 joelriou feat(Algebra/ModuleCat/Presheaf): composition of pushforwards and pullbacks and compatibilites t-algebraic-geometry t-category-theory WIP ❌ ✅ ✅ ❌ ✅ ❌ labelled WIP
21009 vihdzp feat(Logic/Relation): more `TransGen` lemmas t-logic t-order awaiting-author ✅ ✅ ✅ ✅ ❌ ❌ awaiting author
15443 YaelDillies feat: The Marcinkiewicz-Zygmund inequality t-analysis WIP ❌ ✅ ✅ ❌ ✅ ❌ labelled WIP
20466 MohanadAhmed feat: Sherman Morrison formula for rank 1 update of the matrix inverse t-data awaiting-author ✅ ✅ ✅ ✅ ❌ ❌ awaiting author
18749 GabinKolly feat(ModelTheory): preparatory work for the existence of Fraïsse limits t-logic awaiting-author ✅ ✅ ✅ ✅ ❌ ❌ awaiting author
21277 GabinKolly feat(ModelTheory/PartialEquiv): Define the mapping of a self-partialEquiv through an embedding t-logic blocked-by-other-PR ✅ ❌ ✅ ✅ ✅ ❌ blocked on another PR
20649 GabinKolly feat(ModelTheory/Graph): prove characterization of the fraisse limit of finite simple graphs large-import t-logic t-combinatorics WIP ❌ ✅ ✅ ❌ ✅ ❌ labelled WIP
10660 eric-wieser feat(LinearAlgebra/CliffordAlgebra): construction from a basis t-algebra awaiting-author WIP ❌ ✅ ✅ ❌ ❌ ❌ labelled WIP
15355 adomani feat: MiM PR report WIP ✅ ✅ ✅ ❌ ✅ ❌ ⚠️ labelled WIP
21495 alreadydone experiment: reducible HasQuotient.quotient' bench-after-CI WIP ❌ ✅ ✅ ❌ ✅ ❌ labelled WIP
21447 erdOne feat(AlgebraicGeometry): the split algebraic torus t-algebraic-geometry awaiting-author ✅ ✅ ✅ ✅ ❌ ❌ awaiting author
20784 eric-wieser fix: prevent `exact?` recursing forever on `n = 55` t-set-theory awaiting-author ✅ ✅ ✅ ✅ ❌ ❌ awaiting author
22092 fpvandoorn perf: lower gcongr priority in group mono lemmas t-algebra WIP ✅ ✅ ✅ ❌ ✅ ❌ labelled WIP
13442 dignissimus feat: mabel tactic for multiplicative abelian groups new-contributor t-meta modifies-tactic-syntax awaiting-author help-wanted ❌ ✅ ✅ ❌ ❌ ❌ looking for help
21501 sksgurdldi feat(List): add sum_zipWith_eq_finset_sum new-contributor t-algebra awaiting-author ✅ ✅ ✅ ✅ ❌ ❌ awaiting author
20956 tomaz1502 feat(Computability/QueryComplexity/Sort.lean): Formalization of upper bound of queries for merge sort t-computability blocked-by-other-PR ❌ ❌ ✅ ✅ ✅ ❌ blocked on another PR
22233 pechersky feat(Algebra/Valued): `AdicExpansion.evalAt` t-topology blocked-by-other-PR ✅ ❌ ✅ ✅ ✅ ❌ blocked on another PR
22232 pechersky feat(Algebra/Valued): `AdicExpansion.apprUpto` t-topology blocked-by-other-PR ❌ ❌ ✅ ✅ ✅ ❌ blocked on another PR
18230 digama0 feat(Tactic/ScopedNS): extend `scoped[NS]` to more commands t-meta awaiting-author ✅ ✅ ✅ ✅ ❌ ❌ awaiting author
19062 hannahfechtner feat(Algebra/PresentedMonoid/Basic) : facts about rel t-algebra awaiting-author ✅ ✅ ✅ ✅ ❌ ❌ awaiting author
22302 CharredLee feat: add `CategoryTheory.Topos.Power` new-contributor t-category-theory awaiting-author ✅ ✅ ✅ ✅ ❌ ❌ awaiting author
21915 YaelDillies feat: simproc for `Int.divisorsAntidiag` t-meta WIP ❌ ✅ ✅ ❌ ✅ ❌ labelled WIP
22390 YunkaiZhang233 feat(CategoryTheory): implemented proofs for factorisation categories being equivalent to iterated comma categories in two ways new-contributor t-category-theory awaiting-author ✅ ✅ ✅ ✅ ❌ ❌ awaiting author
20636 eric-wieser feat: multiplication of intervals in rings t-algebra awaiting-author ✅ ✅ ✅ ✅ ❌ ❌ awaiting author
16000 YaelDillies feat: Croot-Sisask Almost Periodicity t-analysis t-combinatorics blocked-by-other-PR ✅ ❌ ✅ ✅ ✅ ❌ blocked on another PR
22642 grunweg WIP: add `mfderiv_prod` and `mfderiv_prodMap` t-differential-geometry WIP ❌ ✅ ✅ ❌ ✅ ❌ labelled WIP
22784 grunweg feat: add Diffeomorph.sumSumSumComm t-differential-geometry WIP ❌ ✅ ✅ ❌ ✅ ❌ labelled WIP
22159 shetzl feat: add definition of pushdown automata t-computability new-contributor awaiting-author ✅ ✅ ✅ ✅ ❌ ❌ awaiting author
23042 joneugster feat(CategoryTheory/Enriched/Limits): add HasConicalLimitsOfSize.shrink infinity-cosmos t-category-theory WIP ✅ ✅ ✅ ❌ ✅ ❌ labelled WIP
18091 tukamilano feat: Hoeffding's lemma large-import new-contributor t-measure-probability awaiting-author ❌ ✅ ✅ ✅ ❌ ❌ failing CI
16239 Rida-Hamadani feat(Geometry/Manifold): orientable manifolds t-differential-geometry awaiting-author ❌ ✅ ✅ ✅ ❌ ❌ failing CI
23142 joneugster feat(CategoryTheory/Enriched/Limits): add API for HasConicalLimit infinity-cosmos t-category-theory awaiting-author ✅ ✅ ✅ ✅ ❌ ❌ awaiting author
19607 madvorak Block matrix totally unimodular blocked-by-other-PR WIP ❌ ❌ ✅ ❌ ✅ ❌ blocked on another PR
23285 AntoineChambert-Loir refactor: directed systems in terms of functors large-import t-algebra t-category-theory WIP ❌ ✅ ✅ ❌ ✅ ❌ labelled WIP
22355 xyzw12345 feat(Algebra/RingQuot): Some lemmas about `RingQuot.mkAlgHom` and `RingQuot.mkRingHom` new-contributor t-algebra awaiting-author ✅ ✅ ✅ ✅ ❌ ❌ awaiting author
21829 Whysoserioushah feat(LinearAlgebra/TensorProduct/HomTensor): Add TensorProduct of Hom-modules t-algebra awaiting-author ✅ ✅ ✅ ✅ ❌ ❌ awaiting author
6718 FR-vdash-bot feat: Lindemann-Weierstrass Theorem t-algebra t-analysis blocked-by-other-PR WIP ❌ ❌ ✅ ❌ ✅ ❌ blocked on another PR
22861 eric-wieser feat: add the trace of a bilinear form t-algebra awaiting-author ✅ ✅ ✅ ✅ ❌ ❌ awaiting author
22888 plp127 perf: replace `Lean.Expr.swapBVars` with a better? implementation t-meta awaiting-author ✅ ✅ ✅ ✅ ❌ ❌ awaiting author
23772 SEU-Prime Create Amice.lean t-number-theory WIP ??? ✅ ✅ ❌ ✅ ❌ labelled WIP
20671 thefundamentaltheor3m feat(Analysis/Asymptotics/SpecificAsymptotics): Proving that 𝛔ₖ(n) = O(nᵏ⁺¹) large-import new-contributor t-number-theory awaiting-author ✅ ✅ ✅ ✅ ❌ ❌ awaiting author
21903 yhtq feat: add from/toList between `FreeSemigroup` and `List` with relative theorems large-import new-contributor t-algebra awaiting-CI ❌ ✅ ✅ ✅ ❌ ❌ does not pass CI
22657 Xmask19 feat: a graph is maximally acyclic iff it is a tree new-contributor t-combinatorics ❌ ✅ ✅ ✅ ✅ ❌ failing CI
23154 vlad902 feat(Algebra/FreeMonoid): isomorphisms for the free monoid on zero/one generators t-algebra awaiting-author ✅ ✅ ✅ ✅ ❌ ❌ awaiting author
23866 kim-em chore: remove `[AtLeastTwo n]` hypothesis from the `NatCast` to `OfNat` instance awaiting-zulip ❌ ✅ ✅ ✅ ❌ ❌ failing CI
21342 YaelDillies refactor(Normed/Group/Quotient): generalise to non-abelian groups t-analysis WIP ❌ ✅ ✅ ❌ ✅ ❌ labelled WIP
19475 YaelDillies feat: group markings t-algebra blocked-by-other-PR WIP ❌ ❌ ✅ ❌ ✅ ❌ blocked on another PR
23949 Louddy feat: SkewPolynomial large-import new-contributor t-algebra blocked-by-other-PR ✅ ❌ ✅ ✅ ✅ ❌ blocked on another PR
24010 grunweg feat(Counterexamples): a non-negative function, not a.e. zero, with vanishing lowe… t-measure-probability please-adopt blocked-by-other-PR WIP ❌ ❌ ✅ ❌ ✅ ❌ blocked on another PR
24000 YaelDillies feat: correspondence between Hopf algebras and affine group schemes toric FLT t-algebraic-geometry WIP ❌ ✅ ✅ ❌ ✅ ❌ labelled WIP
21270 GabinKolly feat(ModelTheory/Bundled): first-order embeddings and equivalences from equalities large-import t-logic awaiting-author ✅ ✅ ✅ ✅ ❌ ❌ awaiting author
21031 YaelDillies chore: get rid of generic hom coercions WIP ❌ ✅ ✅ ❌ ✅ ❌ labelled WIP
20263 joelriou feat(CategoryTheory): locally presentable and accessible categories t-category-theory WIP ❌ ✅ ✅ ❌ ✅ ❌ labelled WIP
13038 adomani feat: Mathlib weekly reports CI t-meta awaiting-author ✅ ✅ ✅ ✅ ❌ ❌ awaiting author
24016 plp127 feat: fine uniformity t-topology blocked-by-other-PR ✅ ❌ ✅ ✅ ✅ ❌ blocked on another PR
19613 madvorak refactor(Combinatorics/Optimization/ValuedCSP): make only valid `FractionalOperation` possible t-combinatorics ❌ ✅ ✅ ✅ ✅ ❌ failing CI
22925 ggranberry feat(Mathlib/PlaceHolder/ToeplitzHausdorff): Toeplitz-Hausdorff new-contributor t-analysis awaiting-author WIP help-wanted ❌ ✅ ✅ ❌ ❌ ❌ looking for help
23600 mattrobball perf(Quiver.Basic): make `IsThin` a `class` delegated ✅ ✅ ✅ ✅ ✅ ✅ delegated
23990 robertmaxton42 feat (Types.Colimits): Quot is functorial and colimitEquivQuot is natural new-contributor t-category-theory awaiting-author ✅ ✅ ✅ ✅ ❌ ❌ awaiting author
24219 Paul-Lez feat: linear independence of the tensor product of two linearly independent families toric t-algebra WIP ❌ ✅ ✅ ❌ ✅ ❌ labelled WIP
13740 YaelDillies feat: More robust ae notation t-measure-probability awaiting-CI t-meta ❌ ✅ ✅ ✅ ❌ ❌ does not pass CI
20652 jjaassoonn feat: categorical description of center of a ring t-algebra t-category-theory awaiting-author ❌ ✅ ✅ ✅ ❌ ❌ failing CI
21616 peabrainiac feat(Topology): concatenating countably many paths t-topology awaiting-author ✅ ✅ ✅ ✅ ❌ ❌ awaiting author
18210 vihdzp feat(Order/Hom/Basic): `WithBot (Fin n) ≃o Fin (n + 1)` t-order awaiting-author ✅ ✅ ✅ ✅ ❌ ❌ awaiting author
23585 plp127 feat: `Filter.atMax` and `Filter.atMin` t-order WIP ✅ ✅ ✅ ❌ ✅ ❌ labelled WIP
23026 Paul-Lez feat(Tactic/Simproc/Divisors): add `simproc`s to compute the divisors of a natural number. t-meta awaiting-author ✅ ✅ ✅ ✅ ❌ ❌ awaiting author
22349 dtumad feat(Control): Laws for monads with compatible `failure` operation new-contributor t-meta WIP ❌ ✅ ✅ ❌ ✅ ❌ labelled WIP
22547 joelriou feat(CategoryTheory/Abelian): construction of reduced left resolutions t-category-theory blocked-by-other-PR WIP ✅ ❌ ✅ ❌ ✅ ❌ blocked on another PR
22556 joelriou feat(Algebra/Category/ModuleCat): a functorial projective resolution t-category-theory blocked-by-other-PR ✅ ❌ ✅ ✅ ✅ ❌ blocked on another PR
12032 mcdoll feat: Delta distribution as a limit t-analysis WIP ❌ ✅ ✅ ❌ ✅ ❌ labelled WIP
24405 mcdoll refactor(Topology/Algebra/Module/WeakDual): Clean up large-import t-topology ✅ ✅ ✅ ✅ ✅ ✅ awaiting review
24157 urkud feat(Convex/LinearIsometry): new file t-analysis awaiting-author ✅ ✅ ✅ ✅ ❌ ❌ awaiting author
20719 gio256 feat(AlgebraicTopology): delaborators for truncated simplicial notations infinity-cosmos t-category-theory t-meta ✅ ✅ ✅ ✅ ✅ ✅ awaiting review
24266 plp127 feat(Order): `NoBotOrder α` implies `NoMinOrder α` under `IsDirected α (· ≥ ·)` t-order ✅ ✅ ✅ ✅ ✅ ✅ awaiting review
18861 YaelDillies refactor: make `Set.mem_graphOn` defeq t-data awaiting-author ❌ ✅ ✅ ✅ ❌ ❌ failing CI
23498 Ruben-VandeVelde chore(Topology.MetricSpace.Lipschitz): stop depending on Topology.Algebra t-topology ✅ ✅ ✅ ✅ ✅ ✅ awaiting review
23503 apnelson1 feat(Topology/Instances/ENat): ENat and tsum large-import t-topology WIP ✅ ✅ ✅ ❌ ✅ ❌ labelled WIP
22809 b-reinke feat: Category algebras and path algebras new-contributor t-algebra t-category-theory WIP ❌ ✅ ✅ ❌ ✅ ❌ labelled WIP
24527 matthewjasper feat(Topology/Algebra/Module): Add more theorems for IsModuleTopology new-contributor t-algebra t-topology ✅ ✅ ✅ ✅ ✅ ✅ awaiting review
24574 JovanGerb chore(Order/Notation): check for pp options in `delabSup` t-order ❌ ✅ ✅ ✅ ✅ ❌ failing CI
22231 pechersky feat(Algebra/Valued): `AdicExpansion` initial defns t-algebra t-topology ✅ ✅ ✅ ✅ ✅ ✅ awaiting review
22488 smmercuri fix: lower priority for `UniformSpace.Completion.instSMul` FLT t-topology awaiting-author ✅ ✅ ✅ ✅ ❌ ❌ awaiting author
15649 TpmKranz feat(Computability): introduce Generalised NFA as bridge to Regular Expression awaiting-zulip t-computability new-contributor awaiting-author ✅ ✅ ✅ ✅ ❌ ❌ awaiting a zulip discussion
20648 anthonyde feat: formalize regular expression -> εNFA awaiting-zulip t-computability new-contributor ✅ ✅ ✅ ✅ ❌ ❌ awaiting a zulip discussion
23220 mattrobball refactor(Module.LinearMap.Defs): make `SemilinearMapClass` extend `AddMonoidHomClass` t-algebra awaiting-author ✅ ✅ ✅ ✅ ❌ ❌ awaiting author
24665 Komyyy feat(Mathlib/Topology/Metrizable/Uniformity): every uniform space is generated by a family of pseudometrics t-topology WIP ✅ ✅ ✅ ❌ ✅ ❌ labelled WIP
24667 peabrainiac feat(CategoryTheory/Adjunction): lemmas on adjoint quadruples t-category-theory blocked-by-other-PR ✅ ❌ ✅ ✅ ✅ ❌ blocked on another PR
24668 robertmaxton42 feat(LinearAlgebra): add inductive principle for the free product of algebras t-algebra blocked-by-other-PR ✅ ❌ ✅ ✅ ✅ ❌ blocked on another PR
22464 adomani feat(CI): declarations diff in Lean CI ✅ ✅ ✅ ✅ ✅ ✅ awaiting review
23758 erdOne feat(Topology/Algebra): linearly topologized iff non-archimedian large-import t-algebra t-topology ✅ ✅ ✅ ✅ ✅ ✅ awaiting review
16553 grunweg WIP: tinkering with orientable manifolds t-differential-geometry blocked-by-other-PR WIP ❌ ❌ ✅ ❌ ✅ ❌ blocked on another PR
23213 mattrobball chore(RingTheory.Derivation): add a `LinearMapClass` instance t-algebra delegated ✅ ✅ ✅ ✅ ✅ ✅ delegated
23214 mattrobball perf(Module.LinearMap.Defs): deprioritize projections to parents for `SemilinearMapClass` t-algebra delegated ✅ ✅ ✅ ✅ ✅ ✅ delegated
24155 eric-wieser feat: add a "rw_proc" for fin vectors t-data RFC t-meta awaiting-author ✅ ✅ ✅ ✅ ❌ ❌ awaiting author
22314 shetzl feat: add leftmost derivations for context-free grammars t-computability new-contributor awaiting-author ✅ ✅ ✅ ✅ ❌ ❌ awaiting author
22196 xyzw12345 feat: `lie_ring` tactic and `LieReduce` command new-contributor t-meta ✅ ✅ ✅ ✅ ✅ ✅ awaiting review
24036 Louddy feat: add `HeightOneSpectrum.ofPrime` new-contributor t-algebra ✅ ✅ ✅ ✅ ✅ ✅ awaiting review
11563 YaelDillies feat: `∑ i ∈ s with hi : p i, f i hi` syntax for big operators t-algebra t-meta ✅ ✅ ✅ ✅ ✅ ✅ awaiting review
21276 GabinKolly feat(ModelTheory/Substructures): define equivalences between equal substructures t-logic awaiting-author ✅ ✅ ✅ ✅ ❌ ❌ awaiting author
23137 grunweg chore(Topology): some more fun_prop tagging t-topology delegated ✅ ✅ ✅ ✅ ✅ ✅ delegated
24532 robertmaxton42 feat(LinearAlgebra/FreeProduct): fill out the `FreeProduct.asPowers` namespace t-algebra ❌ ✅ ✅ ✅ ✅ ❌ failing CI
24008 meithecatte chore(EpsilonNFA): replace manual lemmas with @[simps] t-computability new-contributor awaiting-author ✅ ✅ ✅ ✅ ❌ ❌ awaiting author
24602 xyzw12345 feat(LinearAlgebra/SymmetricAlgebra): IsSymmetricAlgebra t-algebra ✅ ✅ ✅ ✅ ✅ ✅ awaiting review
23238 YaelDillies feat: extended floor and ceil t-algebra ✅ ✅ ✅ ✅ ✅ ✅ awaiting review
24184 YaelDillies feat: `[G : H]` notation for the index of `H : Subgroup G` t-algebra RFC ✅ ✅ ✅ ✅ ✅ ✅ awaiting review
22948 pelicanhere feat(Algebra/DirectSum): morphism of directsum decomposition new-contributor t-algebra ❌ ✅ ✅ ✅ ✅ ❌ failing CI
24829 urkud fix(Topology/Homotopy): fix name&args order of `comp` t-topology ✅ ✅ ✅ ✅ ✅ ✅ awaiting review
24793 tristan-f-r feat: trace of unitarily similar matrices t-algebra awaiting-author ✅ ✅ ✅ ✅ ❌ ❌ awaiting author
24752 MichaelStollBayreuth perf(Data.Real.Sqrt): make Real.sqrt irreducible t-data ✅ ✅ ✅ ✅ ✅ ✅ awaiting review
24870 smmercuri feat: `Field`, `FiniteDimensional` and `Algebra.IsSeparable` instances for `WithAbs` large-import t-analysis ✅ ✅ ✅ ✅ ✅ ✅ awaiting review
24872 smmercuri feat: `apply` and `coe` results for `UniformSpace.Completion.mapRingHom` t-topology ✅ ✅ ✅ ✅ ✅ ✅ awaiting review
24883 madvorak chore(Data/Matrix): `Matrix.submatrix` naming convention t-data ✅ ✅ ✅ ✅ ✅ ✅ awaiting review
23999 YaelDillies feat: toric ideals toric t-algebraic-geometry WIP ❌ ✅ ✅ ❌ ✅ ❌ labelled WIP
24889 Kha chore: do not include cache requests in build benchmark ✅ ✅ ✅ ✅ ✅ ✅ awaiting review
22153 smmercuri feat: weak approximation theorems for infinite places of a number field t-algebra t-analysis t-number-theory ✅ ✅ ✅ ✅ ✅ ✅ awaiting review
22142 smmercuri feat: collections of non-trivial and pairwise inequivalent absolute values contain values that diverge around 1 t-algebra t-analysis blocked-by-other-PR ✅ ❌ ✅ ✅ ✅ ❌ blocked on another PR
24618 b-mehta feat(Analysis): add Schur inequality and variants t-analysis WIP ❌ ✅ ✅ ❌ ✅ ❌ labelled WIP
24311 YaelDillies chore: replace `Monoid.IsTorsionFree` with `IsMulTorsionFree` toric t-algebra ✅ ✅ ✅ ✅ ✅ ✅ awaiting review
22043 YaelDillies chore: shortcut instance for `Neg ℤˣ` file-removed t-algebra ✅ ✅ ✅ ✅ ✅ ✅ awaiting review
23920 YaelDillies feat: entourage-separated sets t-topology awaiting-author ✅ ✅ ✅ ✅ ❌ ❌ awaiting author
23881 YaelDillies feat: `ℝ≥0`-valued Lᵖ norm t-measure-probability awaiting-author ✅ ✅ ✅ ✅ ❌ ❌ awaiting author
18379 oeb25 feat(Topology/ENNReal): Add `ENNReal.tsum_biUnion` new-contributor t-topology ✅ ✅ ✅ ✅ ✅ ✅ awaiting review
24891 YaelDillies feat: `M ≃ₗ[R] (Fin (Module.finrank R M) → R)` for `M` a finite `R`-module toric t-algebra ✅ ✅ ✅ ✅ ✅ ✅ awaiting review
24957 eric-wieser feat: use ` binderNameHint` in sum_congr t-algebra ❌ ✅ ✅ ✅ ✅ ❌ failing CI
5919 MithicSpirit feat: implement orthogonality for AffineSubspace new-contributor t-analysis WIP help-wanted ✅ ✅ ✅ ❌ ✅ ❌ looking for help
10235 urkud feat: add `Decidable`, `Fintype`, `Encodable` linters awaiting-bench large-import t-linter t-meta awaiting-author ❌ ✅ ✅ ✅ ❌ ❌ failing CI
24533 robertmaxton42 feat (ULift): conjugation by ULift.up/down, misc cast/heq lemmas t-data ✅ ✅ ✅ ✅ ✅ ✅ awaiting review
17469 joelriou feat(Algebra/ModuleCat/Differentials/Presheaf): the presheaf of relative differentials large-import t-algebraic-geometry t-category-theory WIP ❌ ✅ ✅ ❌ ✅ ❌ labelled WIP
22539 joelriou feat(Algebra/Homology): construction of left resolutions t-category-theory WIP ✅ ✅ ✅ ❌ ✅ ❌ labelled WIP
22300 chrisflav feat(RingTheory/GoingDown): lift `LTSeries` of primes t-algebra ✅ ✅ ✅ ✅ ✅ ✅ awaiting review
21624 sinhp feat(CategoryTheory): The (closed) monoidal structure on the product category of families of (closed) monoidal categories t-category-theory awaiting-author ❌ ✅ ✅ ✅ ❌ ❌ failing CI
22631 Thmoas-Guan feat(Algebra): define associated graded structure for abelian group t-algebra ✅ ✅ ✅ ✅ ✅ ✅ awaiting review
20913 Thmoas-Guan feat(Algebra): Define the associated graded ring to filtered ring. new-contributor t-algebra blocked-by-other-PR ✅ ❌ ✅ ✅ ✅ ❌ blocked on another PR
21806 Thmoas-Guan feat(Algebra): associated graded algebra new-contributor t-algebra blocked-by-other-PR WIP ✅ ❌ ✅ ❌ ✅ ❌ blocked on another PR
20940 Thmoas-Guan feat(Algebra): Associated graded module new-contributor t-algebra blocked-by-other-PR WIP ✅ ❌ ✅ ❌ ✅ ❌ blocked on another PR
22632 Thmoas-Guan feat(Algebra): define filtered add group hom new-contributor t-algebra blocked-by-other-PR ✅ ❌ ✅ ✅ ✅ ❌ blocked on another PR
22208 Thmoas-Guan feat(Algebra):filtered ring hom new-contributor t-algebra blocked-by-other-PR ✅ ❌ ✅ ✅ ✅ ❌ blocked on another PR
22454 Thmoas-Guan feat(Algebra): define filtered algebra morphisms t-algebra blocked-by-other-PR WIP ✅ ❌ ✅ ❌ ✅ ❌ blocked on another PR
22893 Thmoas-Guan feat(Algebra): filtered module hom t-algebra blocked-by-other-PR ✅ ❌ ✅ ✅ ✅ ❌ blocked on another PR
22707 Thmoas-Guan feat(Algebra): associated graded exact of exact and strict new-contributor t-algebra blocked-by-other-PR ✅ ❌ ✅ ✅ ✅ ❌ blocked on another PR
22972 Thmoas-Guan feat(Algebra): exact of associated graded exact new-contributor t-algebra blocked-by-other-PR ✅ ❌ ✅ ✅ ✅ ❌ blocked on another PR
25044 alreadydone feat(Topology/Algebra): `Homeomorph` version of `unitsEquivNeZero` t-algebra t-topology ✅ ✅ ✅ ✅ ✅ ✅ awaiting review
25042 alreadydone feat(Topology): restriction/extension of Trivialization and composition with Homeomorph t-topology ✅ ✅ ✅ ✅ ✅ ✅ awaiting review
24260 plp127 feat(Topology): add API for Hereditarily Lindelof spaces t-topology awaiting-author ✅ ✅ ✅ ✅ ❌ ❌ awaiting author
24333 xcloudyunx feat(Combinatorics/SimpleGraph): cycle graph implementation for generic vertex types new-contributor t-combinatorics ✅ ✅ ✅ ✅ ✅ ✅ awaiting review
21838 joneugster feat(Cache): Allow arguments of the form `Mathlib.Data` which correspond to a folder but not a file CI t-meta awaiting-author ✅ ✅ ✅ ✅ ❌ ❌ awaiting author
22100 smmercuri feat: two inequivalent absolute values have a `< 1` and `> 1` value t-algebra t-analysis awaiting-author ✅ ✅ ✅ ✅ ❌ ❌ awaiting author
25101 erdOne feat(AlgebraicGeometry): building morphisms into Proj t-algebraic-geometry ✅ ✅ ✅ ✅ ✅ ✅ awaiting review
25123 eric-wieser feat: add rfl lemmas for monoidal categories t-algebra ✅ ✅ ✅ ✅ ✅ ✅ awaiting review
24528 chrisflav feat(AlgebraicGeometry): directed covers t-algebraic-geometry ✅ ✅ ✅ ✅ ✅ ✅ awaiting review
25069 erdOne feat(EllipticCurve): rational points of singular nodal cubics t-algebraic-geometry ✅ ✅ ✅ ✅ ✅ ✅ awaiting review
25135 vasnesterov WIP/test PR for faster `tauto` large-import t-meta WIP ✅ ✅ ✅ ❌ ✅ ❌ labelled WIP
11155 smorel394 feat(LinearAlgebra/Multilinear/DirectSum, LinearAlgebra/DirectSum/{PiTensorProduct,Finsupp}): interaction between `MultilinearMap` and `DirectSum`, and between `PiTensorProduct` and `DirectSum` t-algebra please-adopt ❌ ✅ ✅ ❌ ✅ ❌ looking for help
19456 AntoineChambert-Loir feat(Data/Finsupp/MonomialOrder/DegRevLex): homogeneous reverse lexicographic order t-data t-order t-algebraic-geometry WIP ❌ ✅ ✅ ❌ ✅ ❌ labelled WIP
5863 eric-wieser feat: add elaborators for concrete matrices t-meta blocked-by-other-PR help-wanted ❌ ❌ ✅ ❌ ✅ ❌ blocked on another PR
23547 chrisflav feat(AlgebraicGeometry): codescent implies descent t-algebraic-geometry awaiting-author ✅ ✅ ✅ ✅ ❌ ❌ awaiting author
24103 plp127 feat(Topology/UniformSpace/OfCompactT2): generalize theorem t-topology ✅ ✅ ✅ ✅ ✅ ✅ awaiting review
24862 grunweg feat(LocallyIntegrable): generalise more to enorms carleson t-measure-probability WIP ❌ ✅ ✅ ❌ ✅ ❌ labelled WIP
8102 miguelmarco feat(Tactic): add `unify_denoms` and `collect_signs` tactics new-contributor t-meta please-adopt modifies-tactic-syntax good first issue ✅ ✅ ✅ ❌ ✅ ❌ looking for help
24050 Paul-Lez feat(Data/Finsupp/Pointwise): generalise pointwise scalar multiplication of finsupps t-data ✅ ✅ ✅ ✅ ✅ ✅ awaiting review
25070 erdOne feat(EllipticCurve): rational points on singular cuspidal cubics t-algebraic-geometry ✅ ✅ ✅ ✅ ✅ ✅ awaiting review
25208 erdOne feat(LinearAlgebra): `tensor_induction` macro t-algebra RFC WIP ✅ ✅ ✅ ❌ ✅ ❌ labelled WIP
25225 xcloudyunx feat(Combinatorics/SimpleGraph): Eulerian walk in connected graph contains all vertices new-contributor t-combinatorics ✅ ✅ ✅ ✅ ✅ ✅ awaiting review
25248 xcloudyunx feat(Combinatorics/SimpleGraph): Add Subgraph.inclusion_edge_apply_coe and inclusion_edgeSet_apply_coe new-contributor t-combinatorics ✅ ✅ ✅ ✅ ✅ ✅ awaiting review
24015 alreadydone feat(RingTheory): lemmas on finiteness of `LinearMap` and `Module.End` t-algebra ❌ ✅ ✅ ✅ ✅ ❌ failing CI
24690 ScottCarnahan feat (Data.Prod): Reverse lexicographic order t-order WIP ✅ ✅ ✅ ❌ ✅ ❌ labelled WIP
25153 eric-wieser feat(Algebra/ModEq): a lemma about `[PMOD (n • p)]` t-number-theory ✅ ✅ ✅ ✅ ✅ ✅ awaiting review
24804 Moises-Herradon-Cueto feat(CategoryTheory/Limits/Preserves/Shapes): show that if a functor preserves limits, so does `Over.post` toric new-contributor t-category-theory ✅ ✅ ✅ ✅ ✅ ✅ awaiting review
25271 YaelDillies feat: promote an `AlgEquiv` preserving `counit` and `comul` to a `BialgEquiv` toric t-algebra ✅ ✅ ✅ ✅ ✅ ✅ awaiting review
24412 pechersky feat(UniformSpace/Ultra/Constructions): IsUltraUniformity.{bot,top} large-import t-topology ✅ ✅ ✅ ✅ ✅ ✅ awaiting review
22919 plp127 feat(Data/Fintype/Pi): Make `Fintype` instance for `RelHom`s computable t-data awaiting-author ✅ ✅ ✅ ✅ ❌ ❌ awaiting author
7300 ah1112 feat: synthetic geometry t-euclidean-geometry awaiting-author help-wanted ❌ ✅ ✅ ❌ ❌ ❌ looking for help
24095 lecopivo feat: `fun_prop` for Is(Bounded)LinearMap + notation `fun x ↦L[R] f x` large-import t-algebra ✅ ✅ ✅ ✅ ✅ ✅ awaiting review
25324 eric-wieser feat: more functorial results about DFinsupp WIP ✅ ✅ ✅ ❌ ✅ ❌ ⚠️ labelled WIP
21950 erdOne feat(NumberTheory/Padics): the completion of `ℚ` at a finite place is `ℚ_[p]` t-number-theory ✅ ✅ ✅ ✅ ✅ ✅ awaiting review
25322 thorimur style: use simplex notation (`⦋n⦌`) where possible t-topology ✅ ✅ ✅ ✅ ✅ ✅ awaiting review
24173 YaelDillies feat: the composition of open relations is open t-topology blocked-by-other-PR ✅ ❌ ✅ ✅ ✅ ❌ blocked on another PR
24373 YaelDillies refactor: golf `modularCharacter` t-measure-probability awaiting-CI ❌ ✅ ✅ ✅ ❌ ❌ does not pass CI
25343 plp127 docs(Topology/Perfect): Mention dense-in-itself t-topology documentation ✅ ✅ ✅ ✅ ✅ ✅ awaiting review
25337 alreadydone feat(RingTheory): invertible modules and Picard group t-algebra ✅ ✅ ✅ ✅ ✅ ✅ awaiting review
24065 kim-em chore: script to give topological sort of modules awaiting-author ✅ ✅ ✅ ✅ ❌ ❌ awaiting author
22069 Raph-DG feat(LinearMap): Added lemmas relating kernels of linear maps to Submodule.map new-contributor t-algebra ✅ ✅ ✅ ✅ ✅ ✅ awaiting review
22052 FLDutchmann feat(NumberTheory/SelbergSieve): define Lambda-squared sieves and prove important properties t-analysis t-number-theory awaiting-author ✅ ✅ ✅ ✅ ❌ ❌ awaiting author
24884 smmercuri feat: `ramificationIdx` for `NumberField.InfinitePlace` t-number-theory ✅ ✅ ✅ ✅ ✅ ✅ awaiting review
24754 urkud feat: define `pathIntegral` t-analysis awaiting-author ✅ ✅ ✅ ✅ ❌ ❌ awaiting author
20238 maemre feat(Computability/DFA): Closure of regular languages under some set operations awaiting-zulip t-computability new-contributor awaiting-author ✅ ✅ ✅ ✅ ❌ ❌ awaiting a zulip discussion
24875 smmercuri feat: injectivity of `InfinitePlace.embedding` t-number-theory ✅ ✅ ✅ ✅ ✅ ✅ awaiting review
24959 dupuisf feat: the CFC commutes with set integrals t-measure-probability t-analysis awaiting-author ✅ ✅ ✅ ✅ ❌ ❌ awaiting author
25401 digama0 feat(Util): SuppressSorry option t-meta ✅ ✅ ✅ ✅ ✅ ✅ awaiting review
25223 kckennylau feat(Algebra): Quadratic Algebra t-algebra please-adopt WIP ❌ ✅ ✅ ❌ ✅ ❌ looking for help
25453 JovanGerb perf(Algebra/Homology/HomotopyCategory): use explicit universe parameter in `Category` t-algebra ✅ ✅ ✅ ✅ ✅ ✅ awaiting review
25473 adomani feat(CI): check that Mathlib files have lean or md extension CI delegated ✅ ✅ ✅ ✅ ✅ ✅ delegated
25500 eric-wieser feat: delaborators for metadata large-import t-meta ❌ ✅ ✅ ✅ ✅ ❌ failing CI
22366 kim-em feat: `check_equalities` tactic for diagnosing defeq problems t-meta delegated ✅ ✅ ✅ ✅ ✅ ✅ delegated
18693 Ruben-VandeVelde feat: add ConjRootClass new-contributor t-algebra delegated ✅ ✅ ✅ ✅ ✅ ✅ delegated
23992 robertmaxton42 feat (Limits.FunctorCategory): limitIsoFlipCompLim and colimitIsoFlipCompColim are natural new-contributor t-category-theory awaiting-CI ❌ ✅ ✅ ✅ ❌ ❌ does not pass CI
24441 MrSumato feat(Data/List): add Lyndon-Schutzenberger theorem on list commutativity t-data new-contributor awaiting-author ✅ ✅ ✅ ✅ ❌ ❌ awaiting author
23240 urkud feat(Topology/Maps): `IsOpenMap` and `ClusterPt` t-topology delegated ✅ ✅ ✅ ✅ ✅ ✅ delegated
24612 Paul-Lez feat(Tactic/ImportDiff): add `#import_diff` command will-close-soon t-meta awaiting-author ✅ ✅ ✅ ✅ ❌ ❌ awaiting author
14089 callesonne feat(Bicategory/Functorbicategory): define bicategory of pseudofunctors t-category-theory blocked-by-other-PR ✅ ❌ ✅ ✅ ✅ ❌ blocked on another PR
23929 meithecatte feat(Computability/NFA): improve bound on pumping lemma awaiting-zulip t-computability new-contributor ✅ ✅ ✅ ✅ ❌ ❌ awaiting a zulip discussion
25089 Bergschaf feat(Order/Sublocale): definition of sublocales maintainer-merge t-order ✅ ✅ ✅ ✅ ✅ ✅ awaiting review
25481 kbuzzard chore: refactor Algebra.TensorProduct.rightAlgebra t-algebra ✅ ✅ ✅ ✅ ✅ ✅ awaiting review
25563 Komyyy chore: move `Topology.StoneCech` into `Topology.Compactification` (1/2) file-removed maintainer-merge t-topology ✅ ✅ ✅ ✅ ✅ ✅ awaiting review
25583 Komyyy style: move `Topology.StoneCech` into `Topology.Compactification` (2/2) t-topology blocked-by-other-PR ✅ ❌ ✅ ✅ ✅ ❌ blocked on another PR
25596 Komyyy feat: the Riemann zeta function is meromorphic (1/2) file-removed t-analysis blocked-by-other-PR ✅ ❌ ✅ ✅ ✅ ❌ blocked on another PR
25597 Komyyy feat: the Riemann zeta function is meromorphic (2/2) file-removed t-analysis blocked-by-other-PR ✅ ❌ ✅ ✅ ✅ ❌ blocked on another PR
24541 pfaffelh feat(Topology/Compactness/CompactSystem): introduce compact Systems new-contributor t-measure-probability ✅ ✅ ✅ ✅ ✅ ✅ awaiting review
23117 pfaffelh feat(MeasureTheory): finite unions of sets in a semi-ring (in terms of measure theory) form a ring large-import new-contributor t-measure-probability blocked-by-other-PR ✅ ❌ ✅ ✅ ✅ ❌ blocked on another PR
25600 Komyyy refactor: lemma expressing `ContinuousAt` using a punctured neighbourhood maintainer-merge t-topology ✅ ✅ ✅ ✅ ✅ ✅ awaiting review
24692 ScottCarnahan feat (RingTheory/HahnSeries/Basic): isomorphism of Hahn series induced by order isomorphism t-order WIP ✅ ✅ ✅ ❌ ✅ ❌ labelled WIP
25035 ScottCarnahan feat (Algebra/Module/Equiv/Defs): Linear equivalence between linear hom and semilinear hom. t-algebra WIP ✅ ✅ ✅ ❌ ✅ ❌ labelled WIP
25034 ScottCarnahan feat (Algebra/Module/Equiv/Basic): Restriction of scalars from a semilinear equivalence to a linear equivalence. t-algebra WIP ✅ ✅ ✅ ❌ ✅ ❌ labelled WIP
22714 pfaffelh feat: The finite product of semi-rings (in terms of measure theory) is a semi-ring. large-import new-contributor t-measure-probability ✅ ✅ ✅ ✅ ✅ ✅ awaiting review
25334 matthewjasper feat(RingTheory/Flat): Add theorems relating Submodule.torsion and Module.Flat FLT new-contributor t-algebra ✅ ✅ ✅ ✅ ✅ ✅ awaiting review
24983 alreadydone fix(Topology/Covering): switch to standard definition t-topology ❌ ✅ ✅ ✅ ✅ ❌ failing CI
23528 Ruben-VandeVelde feat: add isOpen_setOf_affineIndependent t-analysis delegated ✅ ✅ ✅ ✅ ✅ ✅ delegated
24850 pechersky feat(Topology/UniformSpace/Ultra): uniform spaces induced by pseudometrics are ultra if system is ultra t-topology ✅ ✅ ✅ ✅ ✅ ✅ awaiting review
24669 qawbecrdtey feat(Analysis/Normed/Operator/LinearIsometry): added definition `LinearIsometryEquiv.prodComm` maintainer-merge t-analysis awaiting-author ✅ ✅ ✅ ✅ ❌ ❌ awaiting author
25621 joelriou refactor(CategoryTheory/Limits): generalize universes for colimits of representables t-category-theory WIP ❌ ✅ ✅ ❌ ✅ ❌ labelled WIP
25262 Ruben-VandeVelde chore: add missing deprecations tech debt delegated ✅ ✅ ✅ ✅ ✅ ✅ delegated
24540 robertmaxton42 feat(Quiv): add the empty, vertex, point, interval, and walking quivers t-category-theory awaiting-author ❌ ✅ ✅ ✅ ❌ ❌ failing CI
25637 Timeroot feat(Analysis/Convex): Lifting convex sets along scalar towers t-analysis awaiting-author ✅ ✅ ✅ ✅ ❌ ❌ awaiting author
25574 D-Thomine feat(Cardinal/Finite): ENat powers and cardinality t-set-theory t-data ✅ ✅ ✅ ✅ ✅ ✅ awaiting review
22790 mhk119 feat: Extend `taylor_mean_remainder_lagrange` to `x < x_0` new-contributor t-analysis awaiting-author ✅ ✅ ✅ ✅ ❌ ❌ awaiting author
21344 kbuzzard chore: attempt to avoid diamond in OreLocalization t-algebra please-adopt ❌ ✅ ✅ ❌ ✅ ❌ looking for help
24321 peabrainiac feat(CategoryTheory/Adjunction): more results on adjoint triples. t-category-theory awaiting-author ✅ ✅ ✅ ✅ ❌ ❌ awaiting author
7596 alreadydone feat: covering maps from properly discontinuous actions and discrete subgroups file-removed t-topology ✅ ✅ ✅ ✅ ✅ ✅ awaiting review
23940 YaelDillies feat: polytopes toric t-analysis ✅ ✅ ✅ ✅ ✅ ✅ awaiting review
25730 xroblot feat(ZLattice/Covolume): add `covolume_div_covolume_eq_relindex` t-algebra ✅ ✅ ✅ ✅ ✅ ✅ awaiting review
25740 robin-carlier feat(AlgebraicTopology/SimplexCategory/GeneratorsRelations): `SimplexCategoryGenRel.toSimplexCategory` is an equivalence large-import t-topology t-category-theory blocked-by-other-PR ❌ ❌ ✅ ✅ ✅ ❌ blocked on another PR
25737 robin-carlier feat(AlgebraicTopology/SimplexCategory/GeneratorsRelations/NormalForms): Normal forms for `P_δ`s large-import t-topology t-category-theory blocked-by-other-PR ❌ ❌ ✅ ✅ ✅ ❌ blocked on another PR
25708 Paul-Lez feat: a few analytical results for PDEs t-analysis WIP ❌ ✅ ✅ ❌ ✅ ❌ labelled WIP
25710 Paul-Lez feat(Mathlib/Analysis/PDE/Quasilinear/Characteristics): the method of characteristics for first order quasilinear PDEs t-analysis blocked-by-other-PR WIP ❌ ❌ ✅ ❌ ✅ ❌ blocked on another PR
25760 robin-carlier feat(CategoryTheory/Bicategory): (2,1)-categories and `Pith` t-category-theory ✅ ✅ ✅ ✅ ✅ ✅ awaiting review
25585 Paul-Lez feat(Tactic/Linters/DeprecatedSimpLemma): lint for deprecated simp lemmas t-linter awaiting-author ❌ ✅ ✅ ✅ ❌ ❌ failing CI
25780 emilyriehl the homotopy category functor preserves products infinity-cosmos large-import t-category-theory WIP ❌ ✅ ✅ ❌ ✅ ❌ labelled WIP
25736 robin-carlier feat(AlgebraicTopology/SimplexCategory/GeneratorsRelations/NormalForms): Normal forms for `P_σ`s large-import t-topology t-category-theory ✅ ✅ ✅ ✅ ✅ ✅ awaiting review
25790 Parcly-Taxel chore: remove >6 month old material in `Deprecated` file-removed tech debt ✅ ✅ ✅ ✅ ✅ ✅ awaiting review
25795 dagurtomas chore(Condensed): introduce an abbrev for the equivalence of light condensed sets with a category of sheaves on a small site t-condensed ✅ ✅ ✅ ✅ ✅ ✅ awaiting review
25799 dagurtomas feat(CategoryTheory): the universal property of localized monoidal categories t-category-theory WIP ❌ ✅ ✅ ❌ ✅ ❌ labelled WIP
25802 dagurtomas feat(AlgebraicTopology): anodyne morphisms of simplicial sets t-topology WIP ❌ ✅ ✅ ❌ ✅ ❌ labelled WIP
25796 dagurtomas feat(CategoryTheory): transport symmetric monoidal structure along equivalence t-category-theory ❌ ✅ ✅ ✅ ✅ ❌ failing CI
25778 thefundamentaltheor3m feat: Monotonicity of `setIntegral` for nonnegative functions new-contributor t-measure-probability awaiting-author ✅ ✅ ✅ ✅ ❌ ❌ awaiting author
25804 erdOne feat: `∑ z ∈ L, ‖z - x‖⁻ʳ` converges for lattices `L` t-analysis ✅ ✅ ✅ ✅ ✅ ✅ awaiting review
25788 Parcly-Taxel feat: number of edges in the Turán graph large-import t-combinatorics ✅ ✅ ✅ ✅ ✅ ✅ awaiting review
25724 bryangingechen chore: disable scheduled runs of stale issues workflow CI ✅ ✅ ✅ ✅ ✅ ✅ awaiting review
25825 yuma-mizuno feat(CategoryTheory/Bicategory): define lax transformations between oplax functors large-import t-category-theory blocked-by-other-PR WIP ✅ ❌ ✅ ❌ ✅ ❌ blocked on another PR
25611 erdOne chore(RingTheory): add `Algebra (FractionRing R) (FractionRing S)` t-algebra ❌ ✅ ✅ ✅ ✅ ❌ failing CI
25829 kbuzzard feat: add mulEquivHaarChar t-measure-probability ✅ ✅ ✅ ✅ ✅ ✅ awaiting review
25835 erdOne WIP: Weierstrass elliptic functions t-analysis WIP ❌ ✅ ✅ ❌ ✅ ❌ labelled WIP
25836 jt496 feat(SimpleGraph/FiveWheelLike): add the Andrásfai-Erdős-Sós theorem large-import t-combinatorics ✅ ✅ ✅ ✅ ✅ ✅ awaiting review
25842 mitchell-horner feat(Combinatorics/SimpleGraph): define turanDensity t-combinatorics ✅ ✅ ✅ ✅ ✅ ✅ awaiting review
25680 kim-em chore: remove some `Nat` shortcut instances ✅ ✅ ✅ ✅ ✅ ✅ awaiting review
25308 pechersky chore(Algebra/Ring/Subring): simp tag `Subring.smul_def` t-algebra ✅ ✅ ✅ ✅ ✅ ✅ awaiting review
25765 JovanGerb feat(gcongr): lemma for rewriting inside divisibility t-data delegated ✅ ✅ ✅ ✅ ✅ ✅ delegated
25182 YaelDillies feat: `(M →* N₁) ≃* (M →* N₂)` if `N₁ ≃* N₂` toric t-algebra ✅ ✅ ✅ ✅ ✅ ✅ awaiting review
25856 MichaelStollBayreuth perf(Data.Real.Sqrt): make Real.sqrt irreducible migrated-from-branch t-data ✅ ✅ ✅ ✅ ✅ ✅ awaiting review
25846 mattrobball chore: deprioritize some projection instances ❌ ✅ ✅ ✅ ✅ ❌ failing CI
25700 grunweg RFC: lint upon uses of the `mono` tactic t-linter RFC ❌ ✅ ✅ ✅ ✅ ❌ failing CI
24096 plp127 feat(Topology): Completely Regular Space iff Uniformizable t-topology blocked-by-other-PR ✅ ❌ ✅ ✅ ✅ ❌ blocked on another PR
25881 eric-wieser chore: extract an auxiliary function from `congr()` awaiting-zulip maintainer-merge t-meta ✅ ✅ ✅ ✅ ❌ ❌ awaiting a zulip discussion
25851 kmill feat: improve quality of proofs generated by `congr(...)`, add caching, add support for overapplied functions t-meta ✅ ✅ ✅ ✅ ✅ ✅ awaiting review
25899 pfaffelh feat(Topology/Compactness/CompactSystem): introduce compact Systems ✅ ✅ ✅ ✅ ✅ ✅ ⚠️ awaiting review
25903 pfaffelh feat(MeasureTheory): finite unions of sets in a semi-ring (in terms of measure theory) form a ring large-import blocked-by-other-PR ✅ ❌ ✅ ✅ ✅ ❌ ⚠️ blocked on another PR
25912 BoltonBailey feat: add simp lemmas for trig functions on `π * 2⁻¹` t-analysis awaiting-author blocked-by-other-PR ✅ ❌ ✅ ✅ ❌ ❌ blocked on another PR
25916 BoltonBailey feat: add `simp` lemma `coeff_eq_zero_of_not_mem_support` t-algebra awaiting-author ❌ ✅ ✅ ✅ ❌ ❌ failing CI
25932 Garmelon chore: remove acceptSuggestionOnEnter option new-contributor ✅ ✅ ✅ ✅ ✅ ✅ awaiting review
23930 Vtec234 feat(Tactic): dependent rewriting t-meta awaiting-author ✅ ✅ ✅ ✅ ❌ ❌ awaiting author
22078 Louddy feat(SkewMonoidAlgebra): multiplication and algebraic instances large-import new-contributor t-algebra ✅ ✅ ✅ ✅ ✅ ✅ awaiting review
24254 Louddy feat: valuation on RatFunc which is trivial on constants t-algebra ✅ ✅ ✅ ✅ ✅ ✅ awaiting review
25966 b-reinke feat(GroupTheory/FreeGroup/ReducedWords): add theory of reduced words t-algebra ✅ ✅ ✅ ✅ ✅ ✅ awaiting review
25965 b-reinke feat(Algebra/BigOperators/Finprod): add powerset projection lemmas ✅ ✅ ✅ ✅ ✅ ✅ ⚠️ awaiting review
25931 joelriou refactor(CategoryTheory): redefine triangulated subcategories using ObjectProperty ✅ ✅ ✅ ✅ ✅ ✅ awaiting review
25992 Multramate feat(RingTheory/Ideal/Span): add pair lemmas ✅ ✅ ✅ ✅ ✅ ✅ ⚠️ awaiting review
25999 bjoernkjoshanssen feat(Topology/Compactification): projective line over ℝ is homeomorphic to the one-point compactification of ℝ t-topology ✅ ✅ ✅ ✅ ✅ ✅ awaiting review
25978 Bergschaf feat(Order/Sublocale): Open Sublocales t-order blocked-by-other-PR ✅ ❌ ✅ ✅ ✅ ❌ blocked on another PR
26009 linesthatinterlace feat: Add `Vector`/`List.Vector` equivalence migrated-from-branch ✅ ✅ ✅ ✅ ✅ ✅ ⚠️ awaiting review
26031 joelriou feat(Algebra/Homology): the derived category of a linear abelian category is linear blocked-by-other-PR ✅ ❌ ✅ ✅ ✅ ❌ ⚠️ blocked on another PR
25854 robin-carlier feat(CategoryTheory/Monoidal/Opposites): monoid objects internal to the monoidal opposite t-category-theory ✅ ✅ ✅ ✅ ✅ ✅ awaiting review
25767 robin-carlier feat(CategoryTheory/Monoidal/Opposite): the equivalence `Cᴹᵒᵖᴹᵒᵖ ≌ C` is monoidal t-category-theory ✅ ✅ ✅ ✅ ✅ ✅ awaiting review
26054 FMLJohn feat(RingTheory/GradedAlgebra/Homogeneous/Subsemiring): homogeneous subsemirings of a graded semiring t-algebra ✅ ✅ ✅ ✅ ✅ ✅ awaiting review
25921 BoltonBailey feat: scripts to analyze overlap between namespaces migrated-from-branch t-meta WIP ✅ ✅ ✅ ❌ ✅ ❌ labelled WIP
23360 kim-em chore: review of `erw` in `Algebra/Homology/DerivedCategory` t-algebra awaiting-author ✅ ✅ ✅ ✅ ❌ ❌ awaiting author
26067 mapehe feat(Topology/StoneCech): exists_continuous_surjection_from_StoneCech_to_dense_range t-topology ✅ ✅ ✅ ✅ ✅ ✅ awaiting review
26076 joelriou feat(AlgebraicTopology/SimplicialSet): uniqueness of the decomposition involving non-degenerate simplices t-topology ✅ ✅ ✅ ✅ ✅ ✅ awaiting review
25183 YaelDillies feat: convolution product on linear maps from a coalgebra to an algebra toric t-algebra ✅ ✅ ✅ ✅ ✅ ✅ awaiting review
25480 ocfnash feat: define a concrete model of the `𝔤₂` root system large-import t-algebra WIP ❌ ✅ ✅ ❌ ✅ ❌ labelled WIP
26085 grunweg feat: disjoint unions distribute with products of manifolds t-differential-geometry please-adopt WIP ❌ ✅ ✅ ❌ ✅ ❌ looking for help
26088 grunweg chore(Linter/DirectoryDependency): move forbidden directories into a JSON file t-linter ❌ ✅ ✅ ✅ ✅ ❌ failing CI
26089 WilliamCoram feat: restricted power series form a ring new-contributor t-algebra t-number-theory ❌ ✅ ✅ ✅ ✅ ❌ failing CI
26099 grunweg feat: add IsEmbedding.sumElim_of_separatingNhds new-contributor t-topology ✅ ✅ ✅ ✅ ✅ ✅ awaiting review
25971 joelriou feat(CategoryTheory): pseudofunctors to Cat t-category-theory awaiting-author ✅ ✅ ✅ ✅ ❌ ❌ awaiting author
26075 xroblot feat(NumberField/Units): compute index of unit subgroups using regulators t-number-theory blocked-by-other-PR ✅ ❌ ✅ ✅ ✅ ❌ blocked on another PR
26073 xroblot feat(NumberField/CMField): A totally complex abelian extension of ℚ is CM t-number-theory blocked-by-other-PR ✅ ❌ ✅ ✅ ✅ ❌ blocked on another PR
26108 xroblot feat(NumberField/IsCM): compute the index of the subgroup of real units large-import t-number-theory blocked-by-other-PR ❌ ❌ ✅ ✅ ✅ ❌ blocked on another PR
26104 xroblot feat(NumberField/IsCM): compute ratio of regulators large-import t-number-theory blocked-by-other-PR ❌ ❌ ✅ ✅ ✅ ❌ failing CI
26109 grunweg feat(workflows): automatically assign reviewers CI WIP help-wanted ✅ ✅ ✅ ❌ ✅ ❌ looking for help
24912 YaelDillies feat: affine monoids toric t-algebra blocked-by-other-PR ✅ ❌ ✅ ✅ ✅ ❌ blocked on another PR
24966 michaellee94 feat(Manifold/PartitionOfUnity): Existence of global C^n smooth section for nontrivial bundles new-contributor t-differential-geometry awaiting-author ✅ ✅ ✅ ✅ ❌ ❌ awaiting author
24873 smmercuri feat: `Subtype.map_ne` t-data awaiting-author ✅ ✅ ✅ ✅ ❌ ❌ awaiting author
26122 chrisflav refactor(CategoryTheory/CoproductDisjoint): generalize to indexed coproducts t-category-theory ✅ ✅ ✅ ✅ ✅ ✅ awaiting review
26125 faenuccio first commit dependency-bump WIP ✅ ✅ ✅ ❌ ✅ ❌ labelled WIP
25858 themathqueen feat(RingTheory/Coalgebra/MulOpposite): coalgebra instance for MulOpposite new-contributor t-algebra ✅ ✅ ✅ ✅ ✅ ✅ awaiting review
26074 oliver-butterley feat(Mathlib.Dynamics.BirkhoffSum): add 2 lemmas for birkhoffSum/birkhoffAverage concerning ae_eq observables new-contributor t-dynamics ✅ ✅ ✅ ✅ ✅ ✅ awaiting review
26154 ADedecker refactor: add refactored APIs for algebraic filter bases t-topology ✅ ✅ ✅ ✅ ✅ ✅ awaiting review
26137 xroblot feat(NumberField): specialized version of Kummer Dedekind for the splitting of prime numbers (part 1) t-number-theory ✅ ✅ ✅ ✅ ✅ ✅ awaiting review
26157 erdOne chore(RingTheory): Merge `Mathlib/RingTheory/LocalRing/ResidueField/Algebraic.lean` into `Instances.lean` file-removed ✅ ✅ ✅ ✅ ✅ ✅ awaiting review
26159 upobir feat(Algebra/QuadraticDiscriminant): Adding inequalities on quadratic from inequalities on discriminant t-algebra ✅ ✅ ✅ ✅ ✅ ✅ awaiting review
25292 YaelDillies feat: the `ConvexCone` generated by a set t-convex-geometry toric ✅ ✅ ✅ ✅ ✅ ✅ awaiting review
24149 YaelDillies refactor(Convex/Cone): streamline duality toric t-analysis ✅ ✅ ✅ ✅ ✅ ✅ awaiting review
26177 artie2000 feat(Algebra): add Aesop automation around `Even` / `IsSquare` t-algebra t-meta blocked-by-other-PR ✅ ❌ ✅ ✅ ✅ ❌ blocked on another PR
26156 oliver-butterley feat(MeasureTheory.VectorMeasure) : add a definition of total variation for VectorMeasure new-contributor t-measure-probability ✅ ✅ ✅ ✅ ✅ ✅ awaiting review
26199 Vierkantor fix(Algebra): `MulMemClass.mul_mem` should not be `aesop safe` t-algebra ✅ ✅ ✅ ✅ ✅ ✅ awaiting review
26200 adomani fix: add label when landrun fails CI ✅ ✅ ✅ ✅ ✅ ✅ awaiting review
26211 Thmoas-Guan feat(Algebra): vanishing of induced hom between ext large-import t-algebra ❌ ✅ ✅ ✅ ✅ ❌ failing CI
26212 Thmoas-Guan feat(Algebra): the Rees theorem for depth large-import t-algebra blocked-by-other-PR ❌ ❌ ✅ ✅ ✅ ❌ blocked on another PR
26213 Thmoas-Guan feat(Algebra): Ext iso quotient regular sequence large-import t-algebra blocked-by-other-PR ❌ ❌ ✅ ✅ ✅ ❌ blocked on another PR
26214 Thmoas-Guan feat(Algebra): definition of depth large-import t-algebra blocked-by-other-PR ❌ ❌ ✅ ✅ ✅ ❌ blocked on another PR
26215 Thmoas-Guan feat(Algebra): Auslander-Buchsbaum theorem large-import t-algebra blocked-by-other-PR ❌ ❌ ✅ ✅ ✅ ❌ blocked on another PR
26216 Thmoas-Guan feat(Algebra): depth of QuotSMulTop large-import t-algebra blocked-by-other-PR ❌ ❌ ✅ ✅ ✅ ❌ blocked on another PR
26217 Thmoas-Guan feat(Algebra): Ischebeck theorem large-import t-algebra blocked-by-other-PR ❌ ❌ ✅ ✅ ✅ ❌ blocked on another PR
26070 riccardobrasca feat: add Mathlib.RingTheory.DedekindDomain.Instances large-import t-algebra t-number-theory ✅ ✅ ✅ ✅ ✅ ✅ awaiting review
26225 Raph-DG feat(AlgebraicGeometry): Add some minimal API for orders on schemes t-algebraic-geometry ✅ ✅ ✅ ✅ ✅ ✅ awaiting review
26226 chrisflav chore(AlgebraicGeometry/Limits): undeprecate `sigmaOpenCover` t-algebraic-geometry ✅ ✅ ✅ ✅ ✅ ✅ awaiting review
25926 BoltonBailey feat: add lemma about `degreeOf_eq_degree` t-algebra blocked-by-other-PR ❌ ❌ ✅ ✅ ✅ ❌ blocked on another PR
25803 erdOne feat: taylor expansion of `1 / z ^ r` t-analysis awaiting-author ✅ ✅ ✅ ✅ ❌ ❌ awaiting author
26130 kmill feat: make `reassoc_of%` be able to defer `Category` instance t-meta ✅ ✅ ✅ ✅ ✅ ✅ awaiting review
26239 BoltonBailey feat: add sample pre-commit git hook file WIP ✅ ✅ ✅ ❌ ✅ ❌ ⚠️ labelled WIP
25883 pfaffelh feat: introduce Gram matrices migrated-from-branch new-contributor ✅ ✅ ✅ ✅ ✅ ✅ ⚠️ awaiting review
26240 grunweg perf(CommandLinterLinter): use Substring more t-linter RFC ✅ ✅ ✅ ✅ ✅ ✅ awaiting review
26243 DavidLedvinka feat(Topology): Add PairReduction.lean t-topology ✅ ✅ ✅ ✅ ✅ ✅ labelled WIP
26258 kckennylau feat(Topology): induction for sheafification t-topology ✅ ✅ ✅ ✅ ✅ ✅ awaiting review
26061 kckennylau feat(AlgebraicGeometry): define Projective Space t-algebraic-geometry ✅ ✅ ✅ ✅ ✅ ✅ awaiting review
26259 Raph-DG feat(Topology): Connecting different notions of locally finite t-topology ✅ ✅ ✅ ✅ ✅ ✅ awaiting review
26231 chrisflav feat(CategoryTheory/Sites): sheaf condition and coproducts t-category-theory awaiting-author ✅ ✅ ✅ ✅ ❌ ❌ awaiting author
25603 callesonne feat(Bicategory/InducedBicategory): add induced bicategories t-category-theory awaiting-author ✅ ✅ ✅ ✅ ❌ ❌ awaiting author
26120 vasnesterov feat(Data/Seq): `modify` and `set` operations for `Seq` t-data ✅ ✅ ✅ ✅ ✅ ✅ awaiting review
25837 jt496 feat(Combinatorics/SimpleGraph): add homOfConnectedComponents and related results t-combinatorics ✅ ✅ ✅ ✅ ✅ ✅ awaiting review
26271 Raph-DG feat(AlgebraicGeometry): Simple lemma about existence of affine neighbourhoods t-algebraic-geometry ✅ ✅ ✅ ✅ ✅ ✅ awaiting review
18254 callesonne feat(Bicategory/Modification/Pseudo): define modifications between strong natural transformations of pseudofunctors t-category-theory awaiting-author ✅ ✅ ✅ ✅ ❌ ❌ awaiting author
24395 rudynicolop feat(Data/List): list splitting definitions and lemmas t-data new-contributor awaiting-author ✅ ✅ ✅ ✅ ❌ ❌ awaiting author
26059 wwylele feat(GroupTheory/Divisible): Add rational SMul and Module t-algebra ✅ ✅ ✅ ✅ ✅ ✅ awaiting review
26284 plp127 feat: faster implementation of `Nat.primeFactorsList` + `@[csimp]` lemma t-data ✅ ✅ ✅ ✅ ✅ ✅ awaiting review
26292 RemyDegenne feat(MeasureTheory): tightness of the range of a sequence t-measure-probability awaiting-author ❌ ✅ ✅ ✅ ❌ ❌ failing CI
26293 RemyDegenne feat: tightness from convergence of characteristic functions t-measure-probability WIP ❌ ✅ ✅ ❌ ✅ ❌ labelled WIP
25741 robin-carlier feat(AlgebraicTopology/SimplexCategory/SimplicialObject): definitions of simplicial objects by generators and relation large-import t-topology t-category-theory blocked-by-other-PR ❌ ❌ ✅ ✅ ✅ ❌ blocked on another PR
24730 YaelDillies feat(RingTheory): group-like elements toric t-algebra ✅ ✅ ✅ ✅ ✅ ✅ awaiting review
26301 Ivan-Sergeyev feat(LinearAlgebra/Matrix/Determinant/TotallyUnimodular): new-contributor t-algebra ✅ ✅ ✅ ✅ ✅ ✅ awaiting review
25833 loefflerd feat(Counterexamples): topologists' sine curve migrated-from-branch t-topology ✅ ✅ ✅ ✅ ✅ ✅ awaiting review
26299 adomani perf: the `commandStart` linter only acts on modified files t-linter ✅ ✅ ✅ ✅ ✅ ✅ awaiting review
20924 tomaz1502 feat(Computability/QueryComplexity): Oracle-based computation t-computability ❌ ✅ ✅ ✅ ✅ ❌ failing CI
26189 tb65536 feat(FieldTheory/Galois/Basic): Add simp-lemma for `FixedPoints.intermediateField` t-algebra ✅ ✅ ✅ ✅ ✅ ✅ awaiting review
25616 erdOne feat(RingTheory/Invariant): residue field extension is finite t-algebra awaiting-author ✅ ✅ ✅ ✅ ❌ ❌ awaiting author
26304 Raph-DG feat(AlgebraicGeometry): Definition of algebraic cycles RFC blocked-by-other-PR ✅ ❌ ✅ ✅ ✅ ❌ ⚠️ blocked on another PR
26308 LessnessRandomness feat(Analysis.NormedSpace): add normalized vectors new-contributor t-analysis ✅ ✅ ✅ ✅ ✅ ✅ awaiting review
25997 tb65536 refactor(FieldTheory/Galois): Switch from `Fintype` to `Finite` t-algebra ✅ ✅ ✅ ✅ ✅ ✅ awaiting review
26190 tb65536 feat(FieldTheory/Galois/IsGaloisGroup): Subgroups of a Galois group are Galois groups t-algebra ✅ ✅ ✅ ✅ ✅ ✅ awaiting review
26315 EtienneC30 feat: continuous bilinear forms t-analysis blocked-by-other-PR ✅ ❌ ✅ ✅ ✅ ❌ blocked on another PR
26316 alreadydone feat(RingTheory): degree of rational function field extension t-algebra ✅ ✅ ✅ ✅ ✅ ✅ awaiting review
26319 Vierkantor ci: specify leanprover-community/mathlib4 when checking out master CI ✅ ✅ ✅ ✅ ✅ ✅ awaiting review
26310 kckennylau (WIP) Binary form t-algebra ❌ ✅ ✅ ✅ ✅ ❌ failing CI
26078 kckennylau feat(AlgebraicGeometry): add x, y, px, py for points on elliptic curves t-algebraic-geometry ✅ ✅ ✅ ✅ ✅ ✅ awaiting review
26330 Timeroot "Junk value" test file t-data ✅ ✅ ✅ ✅ ✅ ✅ awaiting review
26332 Timeroot feat (ModelTheory/Definability): TermDefinable functions large-import ✅ ✅ ✅ ✅ ✅ ✅ ⚠️ awaiting review
23460 Timeroot feat: Definition of `Clone` t-algebra ✅ ✅ ✅ ✅ ✅ ✅ awaiting review
20051 Timeroot feat: `Clone` and some instances t-algebra awaiting-author blocked-by-other-PR ❌ ❌ ✅ ✅ ❌ ❌ blocked on another PR
26331 Timeroot feat(Algebra/Polynomial): Descartes' Rule of signs t-algebra ✅ ✅ ✅ ✅ ✅ ✅ awaiting review
22089 sgouezel feat: composing a continuous multilinear map with continuous linear maps is analytic in both variables t-analysis awaiting-author ✅ ✅ ✅ ✅ ❌ ❌ awaiting author
26274 EtienneC30 feat: api for symmetric bilinear forms t-algebra ✅ ✅ ✅ ✅ ✅ ✅ awaiting review
26329 Timeroot feat: Definition of `Clone` notations and typeclasses t-algebra awaiting-CI ❌ ✅ ✅ ✅ ❌ ❌ does not pass CI
26030 joelriou feat(CategoryTheory): abstract argument for the stability under transfinite compositions large-import t-category-theory awaiting-author ❌ ✅ ✅ ✅ ❌ ❌ failing CI
25254 fpvandoorn fix: cleanup measurability + prod/sum lemmas + fun_prop t-measure-probability awaiting-CI ❌ ✅ ✅ ✅ ❌ ❌ does not pass CI
26087 grunweg feat: a `SliceModel` typeclass for models with corners for embedded submanifolds t-differential-geometry ❌ ✅ ✅ ✅ ✅ ❌ failing CI
26255 vasnesterov feat(Analysis): radius of convergence for `FormalMultilinearSeries.compContinuousLinearMap` t-analysis ✅ ✅ ✅ ✅ ✅ ✅ awaiting review
26374 joelriou feat(CategoryTheory): existence of right derived functors using derivability structures t-category-theory blocked-by-other-PR ❌ ❌ ✅ ✅ ✅ ❌ blocked on another PR
26387 jjdishere feat(RingTheory/WittVector): the Teichmuller series t-algebra awaiting-author ❌ ✅ ✅ ✅ ❌ ❌ failing CI
26389 jjdishere feat(RingTheory): Perfectoid Field t-algebra t-analysis t-topology WIP ❌ ✅ ✅ ❌ ✅ ❌ labelled WIP
26390 jjdishere feat(Topology/Algebra): Krasner's lemma t-algebra t-topology t-number-theory WIP ❌ ✅ ✅ ❌ ✅ ❌ labelled WIP
26398 ChrisHughes24 feat(ModelTheory): definable functions t-logic ❌ ✅ ✅ ✅ ✅ ❌ failing CI
26201 scholzhannah feat: subcomplexes of a classical CW complex t-topology ✅ ✅ ✅ ✅ ✅ ✅ awaiting review
25974 scholzhannah feat(Topology/Compactness/CompactlyCoherentSpace): compact coherentification (k-ification) large-import t-topology ✅ ✅ ✅ ✅ ✅ ✅ awaiting review
26007 linesthatinterlace feat Add an array-based implementation of finite permutations. migrated-from-branch t-data ❌ ✅ ✅ ✅ ✅ ❌ failing CI
26238 EtienneC30 feat: the linear isometry which maps an orthonormal basis to another t-analysis ❌ ✅ ✅ ✅ ✅ ❌ failing CI
26376 maddycrim Simons2025 large-import new-contributor WIP ❌ ✅ ✅ ❌ ✅ ❌ labelled WIP
22279 xyzw12345 feat(RingTheory/GradedAlgebra): homogeneous relation new-contributor t-algebra awaiting-author ✅ ✅ ✅ ✅ ❌ ❌ awaiting author
26386 jjdishere feat(RingTheory/Perfection): lemmas for `frobeniusEquiv.symm` t-algebra ❌ ✅ ✅ ✅ ✅ ❌ failing CI
26129 LessnessRandomness feat(Geometry/Euclidean/Angle/Unoriented): triangle inequality for angles new-contributor t-euclidean-geometry ❌ ✅ ✅ ✅ ✅ ❌ failing CI
26415 thorimur feat: basic translations between `X →o Y` and `X ⥤ Y` t-category-theory ✅ ✅ ✅ ✅ ✅ ✅ awaiting review
26432 AntoineChambert-Loir feat(Data.Nat.LogFueled): fueled version of `clog` t-data ❌ ✅ ✅ ✅ ✅ ❌ failing CI
25172 eric-wieser feat: restricting `Affine.Simplex` to an affine subspace that contains it maintainer-merge t-euclidean-geometry ✅ ✅ ✅ ✅ ✅ ✅ awaiting review
26268 vasnesterov feat(Analysis/Analytic): `HasFPowerSeriesOnBall.compContinuousLinearMap` t-analysis blocked-by-other-PR ❌ ❌ ✅ ✅ ✅ ❌ blocked on another PR
26428 Ruben-VandeVelde feat: norm_num support for Int.fract t-data ✅ ✅ ✅ ✅ ✅ ✅ awaiting review
5897 eric-wieser feat: add a `MonadError` instance for `ContT` t-meta awaiting-author ✅ ✅ ✅ ✅ ❌ ❌ awaiting author
26455 ScottCarnahan WIP - feat (LinearAlgebra/RootSystem): API for CartanMatrix t-algebra WIP ✅ ✅ ✅ ❌ ✅ ❌ labelled WIP
26195 yuanyi-350 add `Fin.cycleIcc` which rotates `range(i, j)` new-contributor t-algebra ✅ ✅ ✅ ✅ ✅ ✅ awaiting review
25979 joelriou feat(CategoryTheory): the derived adjunction between absolute derived functors t-category-theory ✅ ✅ ✅ ✅ ✅ ✅ awaiting review
26036 joelriou feat(CategoryTheory/Functor): pointwise right derived functors t-category-theory ✅ ✅ ✅ ✅ ✅ ✅ awaiting review
24139 yuanyi-350 feat: add `Fin.cycleIcc` which rotates `range(i, j)` new-contributor t-algebra ✅ ✅ ✅ ✅ ✅ ✅ awaiting review
26396 xroblot feat(RingTheory): define the dual of a basis for the trace and prove basic properties t-algebra ✅ ✅ ✅ ✅ ✅ ✅ awaiting review
26474 xroblot feat(NumberTheory): `N(I 𝓞L) = N(I) ^ [L:K]` for an integral ideal `I` of `K` large-import t-number-theory ✅ ✅ ✅ ✅ ✅ ✅ awaiting review
26138 xroblot Development branch (2) large-import WIP ❌ ✅ ✅ ❌ ✅ ❌ labelled WIP
26453 jburroni feat(Data/PNat/Basic): add order-related instances to PNat large-import t-data new-contributor ✅ ✅ ✅ ✅ ✅ ✅ awaiting review
24778 YaelDillies feat: `CommGrp`-valued Yoneda embedding toric t-category-theory ✅ ✅ ✅ ✅ ✅ ✅ awaiting review
26358 plp127 feat(Topology): R1 spaces are quasisober bench-after-CI t-topology ✅ ✅ ✅ ✅ ✅ ✅ awaiting review
26280 AntoineChambert-Loir feat(GroupTheory/GroupAction/Jordan) : Primitivity lemmas t-algebra ✅ ✅ ✅ ✅ ✅ ✅ awaiting review
26023 Garmelon chore: add githelper.py script new-contributor ✅ ✅ ✅ ✅ ✅ ✅ awaiting review
26371 Timeroot feat(NumberTheory): Niven's theorem t-number-theory ✅ ✅ ✅ ✅ ✅ ✅ awaiting review
26469 euprunin chore: golf using `assumption_mod_cast` ✅ ✅ ✅ ✅ ✅ ✅ awaiting review
26150 YaelDillies feat: `CanLift` instance from `ConvexCone` to `ProperCone` toric t-analysis ✅ ✅ ✅ ✅ ✅ ✅ awaiting review
26048 Vierkantor script: Add downstream project dashboard delegated ✅ ✅ ✅ ✅ ✅ ✅ delegated
26281 AntoineChambert-Loir feat(GroupTheory/GroupAction/MultiplyPretransitive) : Multiple transivity property of the permutation group t-algebra blocked-by-other-PR ✅ ❌ ✅ ✅ ✅ ❌ blocked on another PR
26287 mbkybky feat(Data/ENat/Lattice): coercion to `WithBot ℕ∞` commutes with `biSup` t-data ✅ ✅ ✅ ✅ ✅ ✅ awaiting review
26282 AntoineChambert-Loir feat: a theorem of Jordan on primitive subgroups of the permutation group large-import blocked-by-other-PR ✅ ❌ ✅ ✅ ✅ ❌ ⚠️ blocked on another PR
26492 Komyyy feat: Alexandrov discrete implies locally path-connected t-topology ✅ ✅ ✅ ✅ ✅ ✅ awaiting review
26462 PSchwahn feat(LinearAlgebra/Projection): add results about inverse of `Submodule.prodEquivOfIsCompl` new-contributor t-algebra ✅ ✅ ✅ ✅ ✅ ✅ awaiting review
24514 b-mehta chore(Int/GCD): use fuel in xgcd t-data awaiting-author ✅ ✅ ✅ ✅ ❌ ❌ awaiting author
25364 Paul-Lez feat(Analysis/SpecialFunction/NthRoot): definition and basic API of Real.nthRoot t-algebra WIP ❌ ✅ ✅ ❌ ✅ ❌ labelled WIP
26290 BeibeiX0 feat(Combinatorics/Enumerative/Stirling.lean): define Stirling numbers of the first and second kind new-contributor t-combinatorics awaiting-author ✅ ✅ ✅ ✅ ❌ ❌ awaiting author
26489 chrisflav refactor(RingTheory/RingHom): factor out proofs for `Algebra.FinitePresentation` t-algebra ✅ ✅ ✅ ✅ ✅ ✅ awaiting review
22662 plp127 feat: Localization.Away.lift (computably) t-algebra ✅ ✅ ✅ ✅ ✅ ✅ awaiting review
26478 JovanGerb chore(LibraryRewrite): replace `rw??` with `rw?` t-meta ✅ ✅ ✅ ✅ ✅ ✅ awaiting review
23669 erdOne feat(FieldTheory): abelian extensions t-algebra awaiting-author ✅ ✅ ✅ ✅ ❌ ❌ awaiting author
25782 emilyriehl feat(CategoryTheory/Category/Cat): cartesian closed instance on small categories infinity-cosmos t-category-theory ✅ ✅ ✅ ✅ ✅ ✅ awaiting review
26510 alreadydone feat(Matroid): exchange lemmas involving closure t-data t-combinatorics ✅ ✅ ✅ ✅ ✅ ✅ awaiting review
26060 kckennylau feat(RingTheory): define Grassmannians t-algebra t-algebraic-geometry ✅ ✅ ✅ ✅ ✅ ✅ awaiting review
25348 wwylele feat(LinearAlgebra): add independent iSup to LinearPMap large-import t-algebra ✅ ✅ ✅ ✅ ✅ ✅ awaiting review
26531 JovanGerb fix(RefinedDiscrTree): remove funny `transparency` handling t-meta ✅ ✅ ✅ ✅ ✅ ✅ awaiting review
26270 vasnesterov chore(Analysis/Analytic): split `Analytic.Basic` t-analysis blocked-by-other-PR ✅ ❌ ✅ ✅ ✅ ❌ blocked on another PR
25739 literandltx feat(NumberTheory/LegendreSymbol): Add sqrt‐of‐residue theorems for p=4k+3 and p=8k+5 new-contributor t-number-theory awaiting-author ✅ ✅ ✅ ✅ ❌ ❌ awaiting author
26295 DavidJWebb feat: filtering lists and bounded quantifiers are primitive recursive t-computability new-contributor ✅ ✅ ✅ ✅ ✅ ✅ awaiting review
26155 xroblot feat(DedekindDomain/Different): add the transitivity formula large-import t-algebra ✅ ✅ ✅ ✅ ✅ ✅ awaiting review
25832 xroblot feat(FieldTheory/LinearDisjoint): `trace` (resp. `norm`) and `algebraMap` commutes large-import t-algebra ✅ ✅ ✅ ✅ ✅ ✅ awaiting review
26357 javra feat(CategoryTheory): linear categories as `ModuleCat R`-enriched categories large-import ✅ ✅ ✅ ✅ ✅ ✅ ⚠️ awaiting review
26351 RemyDegenne feat: covering and packing numbers of sets in a metric space t-topology ✅ ✅ ✅ ✅ ✅ ✅ awaiting review
26210 Thmoas-Guan feat(Algebra): associated primes of localized module large-import t-algebra awaiting-author ✅ ✅ ✅ ✅ ❌ ❌ awaiting author
26041 ADedecker feat: refactor and expand lemmas about integration and continuous functional calculus t-analysis delegated ✅ ✅ ✅ ✅ ✅ ✅ delegated
26277 AntoineChambert-Loir feat(RingTheory/Congruence/Hom): prove basic isomorphisms theorems for ring congruences t-algebra ✅ ✅ ✅ ✅ ✅ ✅ awaiting review
25945 adomani feat: the empty line in commands linter large-import maintainer-merge ✅ ✅ ✅ ✅ ✅ ✅ ⚠️ awaiting review
26051 Komyyy feat(Mathlib/GroupTheory/SpecificGroups/Alternating): A_n is simple iff n = 3 or 5 ≤ n large-import t-algebra blocked-by-other-PR ✅ ❌ ✅ ✅ ✅ ❌ blocked on another PR
26035 fbarroero feat(Analysis/Polynomial/MahlerMeasure): the Mahler measure of a complex polynomial t-analysis ✅ ✅ ✅ ✅ ✅ ✅ awaiting review
26543 vihdzp feat(SetTheory/ZFC/VonNeumann): von Neumann hierarchy of sets t-set-theory maintainer-merge ✅ ✅ ✅ ✅ ✅ ✅ awaiting review
25910 themathqueen feat(Algebra/Ring/Idempotent): for idempotent `p,q`, `q-p` is idempotent iff `pq=p=qp` new-contributor t-algebra ✅ ✅ ✅ ✅ ✅ ✅ awaiting review
26404 grunweg chore: clean up and remove FunProp/Differentiable tech debt ✅ ✅ ✅ ✅ ✅ ✅ awaiting review
26264 EtienneC30 feat: characteristic function on product space t-measure-probability blocked-by-other-PR ✅ ❌ ✅ ✅ ✅ ❌ blocked on another PR
25947 qawbecrdtey feat(Data/Nat/Factors): added lemmas including `primeFactorsList_length_ne_zero` t-data ✅ ✅ ✅ ✅ ✅ ✅ awaiting review
26483 metakunt feat (RingTheory/RootsOfUnity/PrimitiveRoots) : Add equiv_primitiveRoots_of_coprimePow new-contributor t-algebra ✅ ✅ ✅ ✅ ✅ ✅ awaiting review
26552 Komyyy feat: equivalent condition for subgroups to be simple t-algebra ✅ ✅ ✅ ✅ ✅ ✅ awaiting review
26555 Komyyy feat: lemmas about betweeness on a linear space t-euclidean-geometry ✅ ✅ ✅ ✅ ✅ ✅ awaiting review
26571 dupuisf chore: Add grind tags for `Set.mem_Ixx` t-order ✅ ✅ ✅ ✅ ✅ ✅ awaiting review
26541 YaelDillies chore: rename `ZMod.natCast_zmod_eq_zero_iff_dvd` to `ZMod.natCast_eq_zero_iff` t-data ✅ ✅ ✅ ✅ ✅ ✅ awaiting review
25993 Multramate feat(Algebra/Group/Units/Hom): add map lemmas t-algebra awaiting-author ✅ ✅ ✅ ✅ ❌ ❌ awaiting author
26580 vasnesterov feat(Tactic/Order): translate linear orders to `Int` large-import t-meta blocked-by-other-PR ❌ ❌ ✅ ✅ ✅ ❌ blocked on another PR
26013 tsuki8 feat(Data/Finset/Card,Data/Set/Finite/Basic) t-data new-contributor awaiting-author ✅ ✅ ✅ ✅ ❌ ❌ awaiting author
26560 b-mehta chore(Topology/LiminfLimsup): split out non-algebraic content from Topology/Algebra file t-topology ✅ ✅ ✅ ✅ ✅ ✅ awaiting review
26587 faenuccio feat(RingTheory/Valuation/Discrete/Basic.lean): add Nontriviality instances for discrete valuations t-algebra ✅ ✅ ✅ ✅ ✅ ✅ awaiting review
26300 igorkhavkine feat(Analysis/Calculus/FDeriv): continuous differentiability from continuous partial derivatives on an open domain in a product space new-contributor t-analysis ✅ ✅ ✅ ✅ ✅ ✅ awaiting review
25919 BoltonBailey doc: suggest !bench in `lake exe pole` maintainer-merge ✅ ✅ ✅ ✅ ✅ ✅ awaiting review
26594 metakunt feat(Algebra/Polynomial/ZMod): Add Polynomial.equiv_of_nat_of_polynomial_zmod new-contributor t-algebra ✅ ✅ ✅ ✅ ✅ ✅ awaiting review
26114 wwylele feat(Data/Real): add embedding of archimedean groups into Real t-data ✅ ✅ ✅ ✅ ✅ ✅ awaiting review
24917 adomani feat: deprecated module automation t-meta ✅ ✅ ✅ ✅ ✅ ✅ awaiting review
26544 vihdzp feat(SetTheory/ZFC/Ordinal): Lean ordinals to ZFC ordinals large-import t-set-theory ✅ ✅ ✅ ✅ ✅ ✅ awaiting review
25841 mitchell-horner feat(Combinatorics/SimpleGraph): prove the Kővári–Sós–Turán theorem t-combinatorics ✅ ✅ ✅ ✅ ✅ ✅ awaiting review
25843 mitchell-horner feat(Combinatorics/SimpleGraph): define `between` subgraphs t-combinatorics ✅ ✅ ✅ ✅ ✅ ✅ awaiting review
25758 YaelDillies chore: shortcut instance `CompleteLattice α → PartialOrder α` t-order ✅ ✅ ✅ ✅ ✅ ✅ awaiting review
25715 kbuzzard feat: more RestrictedProduct API FLT t-topology ❌ ✅ ✅ ✅ ✅ ❌ failing CI
26603 vihdzp refactor(SetTheory/Ordinal/FixedPoint): redefine `Ordinal.deriv` t-set-theory ✅ ✅ ✅ ✅ ✅ ✅ awaiting review
26608 vihdzp feat(SetTheory/Cardinal/Aleph): `o.card ≤ ℵ_ o` and variants t-set-theory ✅ ✅ ✅ ✅ ✅ ✅ awaiting review
26609 artie2000 chore(Aesop): remove aesop `apply` t-algebra t-meta blocked-by-other-PR ✅ ❌ ✅ ✅ ✅ ❌ blocked on another PR
26393 winstonyin feat: solutions to $C^n$ vector fields are $C^n$ in time t-dynamics t-analysis blocked-by-other-PR ✅ ❌ ✅ ✅ ✅ ❌ blocked on another PR
26607 vihdzp feat(SetTheory/Cardinal/Aleph): characterization of initial successor ordinals t-set-theory ✅ ✅ ✅ ✅ ✅ ✅ awaiting review
26394 winstonyin feat: existence of local flows on manifolds t-differential-geometry blocked-by-other-PR WIP ✅ ❌ ✅ ❌ ✅ ❌ blocked on another PR
26617 vihdzp feat(Data/Sum/Order): `toLex` as a `RelIso` t-data t-order ✅ ✅ ✅ ✅ ✅ ✅ awaiting review
25961 artie2000 feat(Aesop): Improve SetLike ruleset maintainer-merge t-algebra t-meta ✅ ✅ ✅ ✅ ✅ ✅ awaiting review
26534 winstonyin feat: IsIntegralCurve for solutions to ODEs t-dynamics t-analysis t-differential-geometry blocked-by-other-PR ✅ ❌ ✅ ✅ ✅ ❌ blocked on another PR
26437 euprunin chore: golf using `contradiction` maintainer-merge awaiting-author ✅ ✅ ✅ ✅ ❌ ❌ awaiting author
26039 tsuki8 feat(RingTheory/MvPolynomial/MonomialOrder): leadingTerm new-contributor blocked-by-other-PR ❌ ❌ ✅ ✅ ✅ ❌ ⚠️ blocked on another PR
26269 EtienneC30 feat: links between characteristic function and independence t-measure-probability blocked-by-other-PR ✅ ❌ ✅ ✅ ✅ ❌ blocked on another PR
26484 peabrainiac feat(Geometry/Diffeology): basics of diffeological spaces t-differential-geometry ✅ ✅ ✅ ✅ ✅ ✅ awaiting review
25920 BoltonBailey feat(Data/Finsupp/Basic): `Finsupp.optionElim'` migrated-from-branch t-data ✅ ✅ ✅ ✅ ✅ ✅ awaiting review
26272 ajirving feat(NumberTheory/LucasLehmer): prove converse direction to Lucas-Lehmer large-import new-contributor t-number-theory ✅ ✅ ✅ ✅ ✅ ✅ awaiting review
25989 Multramate feat(NumberTheory/EllipticDivisibilitySequence): add elliptic nets t-number-theory ✅ ✅ ✅ ✅ ✅ ✅ awaiting review
26638 metakunt chore: Add grind to cast_zero t-data new-contributor ✅ ✅ ✅ ✅ ✅ ✅ awaiting review
24719 madvorak feat(LinearAlgebra/Matrix/NonsingularInverse): inverting `Matrix` inverts its `LinearEquiv` t-algebra ✅ ✅ ✅ ✅ ✅ ✅ awaiting review
26336 mans0954 feat(Topology/Order/HullKernel): Add the Hull-Kernel Topology maintainer-merge t-topology awaiting-author ✅ ✅ ✅ ✅ ❌ ❌ awaiting author
26350 mans0954 feature(RingTheory/RootsOfUnity/Basic) : rootsOfUnity coercions t-algebra ✅ ✅ ✅ ✅ ✅ ✅ awaiting review
26349 mans0954 feat(Analysis/SpecialFunctions/Trigonometric/Basic): sin and cos of multiples of π / 3 help-wanted ❌ ✅ ✅ ❌ ✅ ❌ ⚠️ looking for help
26348 mans0954 WIP: feature(Analysis/LocallyConvex/Prime): The prime map t-analysis WIP ❌ ✅ ✅ ❌ ✅ ❌ labelled WIP
26347 mans0954 feature(Data/Finset/RangeDistance): abs_sub_lt_of_mem_finset_range ✅ ✅ ✅ ✅ ✅ ✅ ⚠️ awaiting review
26606 vihdzp refactor(SetTheory/Cardinal/Regular): review `IsInaccessible` API t-set-theory ✅ ✅ ✅ ✅ ✅ ✅ awaiting review
26344 mans0954 feature(Analysis/NormedSpace/MStructure): The component projections on WithLp 1 (α × β) are L-projections file-removed t-analysis WIP ❌ ✅ ✅ ❌ ✅ ❌ labelled WIP
26340 mans0954 feat(Algebra/Module/NestAlgebra): Nest algebras ❌ ✅ ✅ ✅ ✅ ❌ ⚠️ failing CI
26341 mans0954 feat(LinearAlgebra/QuadraticForm/Basis): Free Tensor product of Quadratic Maps large-import WIP ❌ ✅ ✅ ❌ ✅ ❌ ⚠️ labelled WIP
26339 mans0954 feat(Analysis/Normed/Module/WeakDual): Banach Dieudonné Lemma large-import WIP ❌ ✅ ✅ ❌ ✅ ❌ ⚠️ labelled WIP
26338 mans0954 feat(Order/ScottContinuity): Scott continuity on product spaces t-order awaiting-author ❌ ✅ ✅ ✅ ❌ ❌ failing CI
26549 pechersky feat(Valued/LocallyCompact): locally compact iff complete and DVR and finite residue field t-algebra t-analysis t-number-theory blocked-by-other-PR ❌ ❌ ✅ ✅ ✅ ❌ blocked on another PR
26538 mariainesdff feat(RingTheory/Valuation/Extension): add algebra instances large-import t-algebra ✅ ✅ ✅ ✅ ✅ ✅ awaiting review
9915 eric-wieser refactor: Add norm_num machinery for NNRat t-algebra t-meta ✅ ✅ ✅ ✅ ✅ ✅ awaiting review
26563 winstonyin chore: rename `IsIntegralCurve` to `IsMIntegralCurve` t-differential-geometry ✅ ✅ ✅ ✅ ✅ ✅ awaiting review
25834 Rida-Hamadani feat(SimpleGraph): girth-diameter inequality t-combinatorics blocked-by-other-PR WIP ✅ ❌ ✅ ❌ ✅ ❌ blocked on another PR
23986 ShouxinZhang feat(FieldTheory/RatFunc): add RatFunc.toFractionRingAlgEquiv new-contributor t-algebra ✅ ✅ ✅ ✅ ✅ ✅ awaiting review
26283 kckennylau (WIP) Resultant t-algebra WIP ❌ ✅ ✅ ❌ ✅ ❌ labelled WIP
26644 kckennylau feat(SetTheory/ZFC): Define the language of sets and state the ZFC axioms t-set-theory ✅ ✅ ✅ ✅ ✅ ✅ awaiting review
26646 eric-wieser feat(TensorProduct): add a Repr t-algebra t-meta ✅ ✅ ✅ ✅ ✅ ✅ awaiting review
26370 b-mehta chore(Archive): golf and generalise ascending-descending sequences t-data ✅ ✅ ✅ ✅ ✅ ✅ awaiting review
26648 eric-wieser chore(TensorProduct): remove more `suppress_compilation`s tech debt t-algebra ✅ ✅ ✅ ✅ ✅ ✅ awaiting review
25907 mans0954 Low order roots of unity t-algebra ✅ ✅ ✅ ✅ ✅ ✅ awaiting review
25905 mans0954 feat(RingTheory/Polynomial/SmallDegreeVieta): polynomial versions of results in Algebra.QuadraticDiscriminant t-algebra ✅ ✅ ✅ ✅ ✅ ✅ awaiting review
26402 kckennylau feat(CategoryTheory): Formal products and coproducts t-category-theory awaiting-author ✅ ✅ ✅ ✅ ❌ ❌ awaiting author
26148 Hagb feat(RingTheory/Ideal/Span): some lemmas about zero and span migrated-from-branch t-algebra ✅ ✅ ✅ ✅ ✅ ✅ awaiting review
26403 riccardobrasca feat: add `isPrincipalIdealRing_of_isPrincipal_of_lt_or_isPrincipal_of_mem_primesOver_of_mem_Icc` t-number-theory ✅ ✅ ✅ ✅ ✅ ✅ awaiting review
26106 mbkybky feat(RingTheory/Regular): flat base change of weakly regular sequence t-algebra ✅ ✅ ✅ ✅ ✅ ✅ awaiting review
25996 101damnations feat(RepresentationTheory/Homological/GroupHomology): add Shapiro's lemma ✅ ✅ ✅ ✅ ✅ ✅ ⚠️ awaiting review
26645 erdOne feat(RingTheory/PowerSeries): Construction of `Q` such that `P(Q(X)) = X` t-algebra ✅ ✅ ✅ ✅ ✅ ✅ awaiting review
26378 EtienneC30 feat: inner product against funBasis t-analysis ✅ ✅ ✅ ✅ ✅ ✅ awaiting review
26663 joelriou feat(CategoryTheory/Abelian/SerreClass): left Bousfield localizations t-category-theory ✅ ✅ ✅ ✅ ✅ ✅ awaiting review
26640 euprunin chore: golf Data/ using `grind` bench-after-CI t-data ✅ ✅ ✅ ✅ ✅ ✅ awaiting review
26592 ocfnash feat: add lemma 3.5 from [Geck](https://dx.doi.org/10.1090/proc/13600) t-algebra awaiting-author ✅ ✅ ✅ ✅ ❌ ❌ awaiting author
26291 RemyDegenne feat(Probability): Fernique's theorem t-measure-probability WIP ✅ ✅ ✅ ❌ ✅ ❌ labelled WIP
26654 euprunin chore: golf using `exact` ✅ ✅ ✅ ✅ ✅ ✅ awaiting review
25882 101damnations feat(RepresentationTheory/Homological/GroupHomology/LowDegree): API for n-cycles & n-boundaries for n = 1, 2 large-import t-algebra ✅ ✅ ✅ ✅ ✅ ✅ awaiting review
26368 Whysoserioushah feat(RingTheory/TwoSidedIdeal/SpanAsSum): span of set as finsum t-algebra ✅ ✅ ✅ ✅ ✅ ✅ awaiting review
22039 YaelDillies feat: simproc for computing `Finset.Ixx` of natural numbers large-import t-meta ✅ ✅ ✅ ✅ ✅ ✅ awaiting review
26666 mariainesdff feat(Algebra/Polynomial/Lifts): add lemmas t-algebra ✅ ✅ ✅ ✅ ✅ ✅ awaiting review
25608 TOMILO87 feat: beta distribution new-contributor t-measure-probability ✅ ✅ ✅ ✅ ✅ ✅ awaiting review
26659 edegeltje feat(Tactic/Algebraize): add warning message when unable to find constant with provided name t-meta enhancement ✅ ✅ ✅ ✅ ✅ ✅ awaiting review
26658 mbkybky feat(Algebra): `a / n ≤ a` if `n : ℕ` and `0 ≤ a` t-data t-algebra ✅ ✅ ✅ ✅ ✅ ✅ awaiting review
26325 TOMILO87 feat: beta distribution new-contributor t-measure-probability ❌ ✅ ✅ ✅ ✅ ❌ failing CI
25941 erdOne feat(AlgebraicGeometry): inverse limits and schemes of finite type large-import t-algebraic-geometry delegated ❌ ✅ ✅ ✅ ✅ ❌ failing CI
26667 mariainesdff feat(FieldTheory/SplittingField/IsSplittingField): add IsScalarTower.splits, IsScalarTower.isAlgebraic t-algebra blocked-by-other-PR ✅ ❌ ✅ ✅ ✅ ❌ blocked on another PR
22749 joelriou feat(CategoryTheory/Abelian): the Gabriel-Popescu theorem as a localization with respect to a Serre class t-category-theory blocked-by-other-PR WIP ❌ ❌ ✅ ❌ ✅ ❌ blocked on another PR
26668 mariainesdff feat(Analysis/Normed/Unbundled/SpectralNorm): add API t-analysis t-number-theory blocked-by-other-PR ✅ ❌ ✅ ✅ ✅ ❌ blocked on another PR
26589 faenuccio feat(Mathlib/Algebra/GroupWithZero/Range): add withZeroUnitsHom t-order t-algebra ✅ ✅ ✅ ✅ ✅ ✅ awaiting review
19582 yu-yama feat(GroupExtension/Abelian): define `OfMulDistribMulAction.equivH2` new-contributor t-algebra blocked-by-other-PR ❌ ❌ ✅ ✅ ✅ ❌ blocked on another PR
25958 themathqueen feat(Analysis/InnerProductSpace/Projection): define Submodule.starProjection new-contributor t-analysis awaiting-author ✅ ✅ ✅ ✅ ❌ ❌ awaiting author
26556 fweth feat(CategoryTheory/Topos): subobject classifier without limits new-contributor t-category-theory ✅ ✅ ✅ ✅ ✅ ✅ awaiting review
25874 themathqueen feat(LinearAlgebra/InvariantSubmodule): invariant submodules new-contributor t-algebra awaiting-author ✅ ✅ ✅ ✅ ❌ ❌ awaiting author
25949 themathqueen feat(LinearAlgebra/Basis/MulOpposite): basis of an opposite space new-contributor t-algebra awaiting-author ✅ ✅ ✅ ✅ ❌ ❌ awaiting author
26313 kckennylau feat: 4 lemmas about Finsupp.mapDomain.linearEquiv t-algebra ✅ ✅ ✅ ✅ ✅ ✅ awaiting review
26192 kckennylau feat(LinearAlgebra): symmetric tensor power t-algebra ✅ ✅ ✅ ✅ ✅ ✅ awaiting review
26685 euprunin chore: golf LinearAlgebra/ using `grind` bench-after-CI t-algebra ✅ ✅ ✅ ✅ ✅ ✅ awaiting review
26693 euprunin chore: golf Computability/ using `grind` bench-after-CI t-computability ✅ ✅ ✅ ✅ ✅ ✅ awaiting review
26697 euprunin chore: golf Geometry/ using `grind` bench-after-CI t-euclidean-geometry ✅ ✅ ✅ ✅ ✅ ✅ awaiting review
26698 euprunin chore: golf RingTheory/ using `grind` bench-after-CI t-algebra ✅ ✅ ✅ ✅ ✅ ✅ awaiting review
26699 euprunin chore: golf AlgebraicTopology/ using `grind` bench-after-CI t-topology ✅ ✅ ✅ ✅ ✅ ✅ awaiting review
26158 upobir feat(NumberTheory/Divisors): add int divisors t-number-theory ✅ ✅ ✅ ✅ ✅ ✅ awaiting review
26639 euprunin chore: golf Analysis/ using `grind` bench-after-CI t-analysis ✅ ✅ ✅ ✅ ✅ ✅ awaiting review
26692 euprunin chore: golf Probability/ using `grind` t-measure-probability ✅ ✅ ✅ ✅ ✅ ✅ awaiting review
26691 euprunin chore: golf CategoryTheory/ using `grind` t-category-theory ✅ ✅ ✅ ✅ ✅ ✅ awaiting review
26694 BoltonBailey feat: add lemmas for modular exponentiation with the totient function t-data ✅ ✅ ✅ ✅ ✅ ✅ awaiting review
26700 grunweg feat: add version of fderiv_const_smul without differentiability hypotheses t-analysis ✅ ✅ ✅ ✅ ✅ ✅ awaiting review
26689 euprunin chore: golf Combinatorics/ using `grind` t-combinatorics ✅ ✅ ✅ ✅ ✅ ✅ awaiting review
26681 euprunin chore: golf GroupTheory/ using `grind` t-algebra ✅ ✅ ✅ ✅ ✅ ✅ awaiting review
25692 Whysoserioushah feat(RingTheory/MatrixAlgebra): add a more general version of `matrixEquivTensor` t-algebra ✅ ✅ ✅ ✅ ✅ ✅ awaiting review
26647 b-mehta feat(Data/Sym/Sym2): lift commutative operations to sym2 t-data ✅ ✅ ✅ ✅ ✅ ✅ awaiting review
26695 euprunin chore: golf AlgebraicGeometry/ using `grind` t-algebraic-geometry ✅ ✅ ✅ ✅ ✅ ✅ awaiting review
26696 euprunin chore: golf Logic/ using `grind` t-logic ✅ ✅ ✅ ✅ ✅ ✅ awaiting review
26678 grunweg feat: contMDiffOn_section_of_mem_baseSet t-differential-geometry ✅ ✅ ✅ ✅ ✅ ✅ awaiting review
26377 Whysoserioushah feat(Mathlib/RingTheory/SimpleRing/TensorProduct): Tensor product of a simple algebra and a central simple algebra is simple t-algebra blocked-by-other-PR ✅ ❌ ✅ ✅ ✅ ❌ blocked on another PR
26674 grunweg feat: finite sum, difference, `smul` of `C^k` sections is `C^k` t-differential-geometry blocked-by-other-PR ✅ ❌ ✅ ✅ ✅ ❌ blocked on another PR
26670 yu-yama feat(GroupExtension/Abelian): define `conjClassesEquivH1` t-algebra ✅ ✅ ✅ ✅ ✅ ✅ awaiting review
26710 metakunt feat (Data/Nat/Digits/Lemmas): Add digits_getD t-data new-contributor ✅ ✅ ✅ ✅ ✅ ✅ awaiting review
24064 kim-em chore: replace `norm_num` with `simp` where applicable ✅ ✅ ✅ ✅ ✅ ✅ awaiting review
25951 themathqueen feat(Analysis/InnerProductSpace/MulOpposite): defines the inner product on opposite spaces new-contributor awaiting-author ✅ ✅ ✅ ✅ ❌ ❌ ⚠️ awaiting author
26392 winstonyin feat: solution to ODE is Lipschitz with respect to the initial condition maintainer-merge t-dynamics t-analysis ✅ ✅ ✅ ✅ ✅ ✅ awaiting review
26717 AntoineChambert-Loir feat(RingTheory/TensorProduct/FG) : direct limit properties of tensor products wrt finitely generated submodules t-algebra ❌ ✅ ✅ ✅ ✅ ❌ failing CI
25814 vlad902 feat(SimpleGraph): Weaker condition for paths in acyclic graphs t-combinatorics ✅ ✅ ✅ ✅ ✅ ✅ awaiting review
25812 vlad902 feat(data): List.Chain' helper lemmas t-data ✅ ✅ ✅ ✅ ✅ ✅ awaiting review
26720 vlad902 feat(SimpleGraph): lemmas relating edges and darts to the support t-combinatorics blocked-by-other-PR ❌ ❌ ✅ ✅ ✅ ❌ blocked on another PR
26267 vasnesterov feat(Analysis/Calculus): Taylor series converges to function on whole ball large-import t-analysis ✅ ✅ ✅ ✅ ✅ ✅ awaiting review
26353 kebekus feat: restriction of scalars for iterated Fréchet derivatives t-analysis ✅ ✅ ✅ ✅ ✅ ✅ awaiting review
26716 FlAmmmmING feat(Combinatorics/Enumerative/Bell.lean): Add definitions of standrad bell number new-contributor t-combinatorics ✅ ✅ ✅ ✅ ✅ ✅ awaiting review
26597 sahanwijetunga Update Orthogonal.lean new-contributor t-algebra documentation ✅ ✅ ✅ ✅ ✅ ✅ awaiting review
26723 chrisflav feat(AlgebraicGeometry): source-local closure of a morphism property t-algebraic-geometry ✅ ✅ ✅ ✅ ✅ ✅ awaiting review
26704 euprunin chore: golf Algebra/ using `aesop` bench-after-CI t-algebra ✅ ✅ ✅ ✅ ✅ ✅ awaiting review
26577 FernandoChu feat(CategoryTheory): add dinatural transformations (continued) new-contributor t-category-theory awaiting-author ✅ ✅ ✅ ✅ ❌ ❌ awaiting author
26037 joelriou feat(Order): bicartesian squares in lattices t-order t-category-theory ✅ ✅ ✅ ✅ ✅ ✅ awaiting review
26690 euprunin chore: golf MeasureTheory/ using `grind` bench-after-CI t-measure-probability ✅ ✅ ✅ ✅ ✅ ✅ awaiting review
26726 euprunin chore: golf Algebra/ using `grind` bench-after-CI t-algebra ✅ ✅ ✅ ✅ ✅ ✅ awaiting review
26651 loefflerd WIP: define cusps large-import t-number-theory WIP ✅ ✅ ✅ ❌ ✅ ❌ labelled WIP
25179 YaelDillies feat: `#print sorries`, a command to find usage of `sorry` toric t-meta ✅ ✅ ✅ ✅ ✅ ✅ awaiting review
26675 mariainesdff feat(NumberTheory/Padics/Complex.lean): add the padic complex numbers t-number-theory ✅ ✅ ✅ ✅ ✅ ✅ awaiting review
26729 euprunin chore: golf Algebra/ using `simp` t-algebra ✅ ✅ ✅ ✅ ✅ ✅ awaiting review
26719 AntoineChambert-Loir feat(RingTheory/PolynomialLaw/Basic): extends polynomial laws to arbitrary universes large-import t-algebra blocked-by-other-PR ❌ ❌ ✅ ✅ ✅ ❌ blocked on another PR
26735 Raph-DG feat(AlgebraicGeometry): The codimension of a point of a scheme is equal to the krull dimension of the stalk blocked-by-other-PR ✅ ❌ ✅ ✅ ✅ ❌ ⚠️ blocked on another PR
26734 grunweg feat: Lie bracket with zero is zero t-analysis t-differential-geometry ✅ ✅ ✅ ✅ ✅ ✅ awaiting review
26718 adomani feat: extend the commandStart linter until after `:` t-linter maintainer-merge ✅ ✅ ✅ ✅ ✅ ✅ awaiting review
26740 edegeltje fix(Tactic/Algebraize): adapt application filter to `RingHom.toModule` t-meta bug ✅ ✅ ✅ ✅ ✅ ✅ awaiting review
26375 joelriou chore(CategoryTheory/Localization): fix morphisms in the category of resolutions t-category-theory ✅ ✅ ✅ ✅ ✅ ✅ awaiting review
26029 joelriou feat(CategoryTheory/Localization): the right derivability structure given by functorial resolutions t-category-theory ✅ ✅ ✅ ✅ ✅ ✅ awaiting review
26706 adomani fix: lint also lemmas in `commandStart` t-linter ✅ ✅ ✅ ✅ ✅ ✅ awaiting review
26265 EtienneC30 feat: random variables are independent iff their joint distribution is the product measure t-measure-probability awaiting-author ✅ ✅ ✅ ✅ ❌ ❌ awaiting author
26649 b-mehta feat(Data/Sym/Sym2): construct set of unordered pairs t-data ✅ ✅ ✅ ✅ ✅ ✅ awaiting review
26653 Hagb feat(RingTheory/Finiteness/Defs): span of a set is finitely generated iff generated by a finite subset ❌ ✅ ✅ ✅ ✅ ❌ ⚠️ failing CI
26000 Hagb feat(RingTheory/MvPolynomial/MonomialOrder): some lemmas about degree t-algebra ✅ ✅ ✅ ✅ ✅ ✅ awaiting review
26744 paulorauber feat(Probability): Hoeffding's lemma new-contributor t-measure-probability ✅ ✅ ✅ ✅ ✅ ✅ awaiting review
26601 yuma-mizuno feat(CategoryTheory): make `Functor.comp` irreducible t-category-theory WIP ❌ ✅ ✅ ❌ ✅ ❌ labelled WIP
26448 YaelDillies refactor: simplify `(f₁ ⊗ₘ f₂) ≫ (g₁ ⊗ₘ g₂)` to `(f₁ ≫ g₁) ⊗ₘ (f₂ ≫ g₂)` toric t-category-theory ✅ ✅ ✅ ✅ ✅ ✅ awaiting review
26748 yuma-mizuno fix: add `whnfR` in the code for the string diagram widget t-category-theory t-meta ✅ ✅ ✅ ✅ ✅ ✅ awaiting review
26626 PierreQuinton fix: make `CompleteLattice` extend `BoundedOrder` maintainer-merge t-order awaiting-CI ❌ ✅ ✅ ✅ ❌ ❌ does not pass CI
24794 chrisflav feat(RingTheory/Presentation): core of a presentation t-algebra ✅ ✅ ✅ ✅ ✅ ✅ awaiting review
25927 jjdishere feat(RingTheory/AdicCompletion): more APIs for IsAdicComplete t-algebra awaiting-author ❌ ✅ ✅ ✅ ❌ ❌ failing CI
26107 xroblot feat(NumberField/IsCM): first results about the action of `complexConjugation` on units large-import blocked-by-other-PR ❌ ❌ ✅ ✅ ✅ ❌ ⚠️ blocked on another PR
25757 robin-carlier feat(CategoryTheory/Monoidal/DayConvolution): left and right unitors for Day convolution large-import t-category-theory blocked-by-other-PR ❌ ❌ ✅ ✅ ✅ ❌ blocked on another PR
26733 grunweg chore: rename continuous_iff_continuousOn_univ to continuousOn_univ ✅ ✅ ✅ ✅ ✅ ✅ awaiting review
25175 zcyemi feat(Geometry/Euclidean/Congurence): add triangle congruence new-contributor t-euclidean-geometry ❌ ✅ ✅ ✅ ✅ ❌ failing CI
26759 MichaelStollBayreuth chore(Algebra/Polynomial/IsMonicOfDegree): do not import compute_degree tactic t-algebra ✅ ✅ ✅ ✅ ✅ ✅ awaiting review
26758 zcyemi feat(Geometry/Euclidean/Congurence): add triangle congruence new-contributor t-euclidean-geometry blocked-by-other-PR ✅ ❌ ✅ ✅ ✅ ❌ blocked on another PR
26736 edegeltje fix(Tactic/Algebraize): tactic is unable to see through assigned metavariables t-meta bug ✅ ✅ ✅ ✅ ✅ ✅ awaiting review
26742 agjftucker fix(Logic/Function/Basic): change precedence of uncurry prefix operator to max new-contributor t-logic ✅ ✅ ✅ ✅ ✅ ✅ awaiting review
26746 alreadydone feat(RingTheory): integral extensions of comm. rings are local homs bench-after-CI large-import ✅ ✅ ✅ ✅ ✅ ✅ ⚠️ awaiting review
26722 vlad902 feat(SimpleGraph): sub-walks of minimal length are also minimal t-combinatorics blocked-by-other-PR ❌ ❌ ✅ ✅ ✅ ❌ blocked on another PR
26765 KiringYJ feat(MeasureTheory/PiSystem): add π-λ theorem and SetLike instance new-contributor t-measure-probability ✅ ✅ ✅ ✅ ✅ ✅ awaiting review
26204 Raph-DG feat(AlgebraicGeometry): Add global preorder instance for schemes t-algebraic-geometry easy ✅ ✅ ✅ ✅ ✅ ✅ awaiting review
26721 kebekus feat: implement harmonic functions maintainer-merge t-analysis ✅ ✅ ✅ ✅ ✅ ✅ awaiting review
26766 MichaelStollBayreuth feat(Topology/MetricSpace/Bounded): add some results t-topology ✅ ✅ ✅ ✅ ✅ ✅ awaiting review
26660 strihanje01 feat(Combinatorics/Additive/VerySmallDoubling): weak non-commutative Kneser's theorem large-import new-contributor t-combinatorics awaiting-author ✅ ✅ ✅ ✅ ❌ ❌ awaiting author
26743 grunweg WIP: product rule for Lie bracket on manifolds t-differential-geometry WIP ❌ ✅ ✅ ❌ ✅ ❌ labelled WIP
26760 linesthatinterlace refactor(`InformationTheory/Hamming`): Improvements to Hamming type. large-import t-measure-probability awaiting-author ✅ ✅ ✅ ✅ ❌ ❌ awaiting author
26767 themathqueen feat(Analysis/InnerProductSpace/Adjoint): a normal idempotent operator is a star projection new-contributor ✅ ✅ ✅ ✅ ✅ ✅ ⚠️ awaiting review
25862 zcyemi feat(Geometry/Euclidean/Triangle): add law of sines migrated-from-branch new-contributor t-euclidean-geometry ✅ ✅ ✅ ✅ ✅ ✅ awaiting review
26762 YaelDillies feat: `(· ^ n)` is strictly monotone on nonnegative inputs for `n : ℤ` t-algebra ✅ ✅ ✅ ✅ ✅ ✅ awaiting review
26631 themathqueen feat(Analysis/InnerProductSpace/Positive): a star projection operator is positive new-contributor t-analysis awaiting-author ✅ ✅ ✅ ✅ ❌ ❌ awaiting author
26770 Jun2M feat(Combinatorics/Graph) : subgraph relations and operations on `Graph` t-combinatorics ✅ ✅ ✅ ✅ ✅ ✅ awaiting review
22782 alreadydone WIP: etale space associated to a presheaf t-topology WIP ❌ ✅ ✅ ❌ ✅ ❌ labelled WIP
25818 xroblot feat(NumberField/CMField): All CM-extensions come from the real maximal subfield maintainer-merge t-number-theory ✅ ✅ ✅ ✅ ✅ ✅ awaiting review
26072 xroblot feat(NumberField): Image of torsion modulo an ideal t-number-theory ✅ ✅ ✅ ✅ ✅ ✅ awaiting review
26749 qawbecrdtey feat(GroupTheory/Subgroup/Center): added lemma `center_is_normal` t-algebra easy ✅ ✅ ✅ ✅ ✅ ✅ awaiting review
26530 jsm28 feat(Geometry/Euclidean/Incenter): signs of barycentric coordinates of touchpoints t-euclidean-geometry blocked-by-other-PR ✅ ❌ ✅ ✅ ✅ ❌ blocked on another PR
26529 jsm28 feat(Geometry/Euclidean/Projection): projection onto a 0-simplex t-euclidean-geometry easy ✅ ✅ ✅ ✅ ✅ ✅ awaiting review
26354 vasnesterov feat(Tactic/Order): support `⊤`, `⊥`, and lattice operations large-import t-meta ✅ ✅ ✅ ✅ ✅ ✅ awaiting review
25889 plp127 fix(Tactic/Widget/Conv): fix various issues t-meta ✅ ✅ ✅ ✅ ✅ ✅ awaiting review
16303 grunweg feat(CI): check for badly formatted titles or missing/contradictory labels CI awaiting-author ❌ ✅ ✅ ✅ ❌ ❌ failing CI
25491 tannerduve feat(Control/Monad/Free): define free monad, prove it lawful, and implement standard effects t-data maintainer-merge ✅ ✅ ✅ ✅ ✅ ✅ awaiting review
26614 Rida-Hamadani feat(SimpleGraph): add more API for `take`/`drop` t-combinatorics ✅ ✅ ✅ ✅ ✅ ✅ awaiting review
25662 erdOne chore: redefine `LocalizedModule` ❌ ✅ ✅ ✅ ✅ ❌ failing CI
25002 YaelDillies chore(Finsupp): move order properties under `Order` large-import ❌ ✅ ✅ ✅ ✅ ❌ failing CI
25587 YaelDillies refactor: make `Rel` less see-through t-data RFC ✅ ✅ ✅ ✅ ✅ ✅ awaiting review
25267 YaelDillies feat: `counit (antipode a) = counit a` toric t-algebra ✅ ✅ ✅ ✅ ✅ ✅ awaiting review
19860 YaelDillies refactor: review the `simps` projections of `OneHom`, `MulHom`, `MonoidHom` t-algebra awaiting-CI ❌ ✅ ✅ ✅ ❌ ❌ does not pass CI
24998 YaelDillies chore(Algebra/Notation): separate very basic lemmas about `Set.indicator` and `Pi.single` file-removed ✅ ✅ ✅ ✅ ✅ ✅ awaiting review
25239 YaelDillies refactor: redefine perfect pairings as a Prop-valued typeclass toric t-algebra awaiting-CI ❌ ✅ ✅ ✅ ❌ ❌ does not pass CI
23181 YaelDillies chore(UniformSpace/Defs): move entourages to their own file t-topology awaiting-CI blocked-by-other-PR ❌ ❌ ✅ ✅ ❌ ❌ blocked on another PR
23124 YaelDillies feat(MetricSpace): nets t-topology awaiting-CI blocked-by-other-PR ❌ ❌ ✅ ✅ ❌ ❌ blocked on another PR
19872 YaelDillies chore(GroupTheory/Index): rename `relindex` to `relIndex` FLT t-algebra ✅ ✅ ✅ ✅ ✅ ✅ awaiting review
25756 robin-carlier feat(CategoryTheory/Monoidal/DayConvolution): Associators and pentagon for Day Convolution large-import t-category-theory ✅ ✅ ✅ ✅ ✅ ✅ awaiting review
25732 robin-carlier feat(CategoryTheory/Monoidal/Limits): miscellany about preservation of (co)limits by tensor products file-removed t-category-theory ✅ ✅ ✅ ✅ ✅ ✅ awaiting review
21871 YaelDillies feat: decomposition into independent atoms t-order help-wanted ❌ ✅ ✅ ❌ ✅ ❌ looking for help
25860 robin-carlier feat(CategoryTheory/Monoidal/Action): Action of monoidal opposites t-category-theory ✅ ✅ ✅ ✅ ✅ ✅ merge conflict
25861 robin-carlier feat(CategoryTheory/Monoidal/Action): action of opposite categories t-category-theory blocked-by-other-PR ✅ ❌ ✅ ✅ ✅ ❌ blocked on another PR
22655 YaelDillies refactor: make use of `FunLike` for `Submonoid.LocalizationMap` toric t-algebra ✅ ✅ ✅ ✅ ✅ ✅ awaiting review
23594 YaelDillies refactor: merge `DomMulAct` and `DomAddAct` into `DomAct` file-removed t-algebra awaiting-CI ❌ ✅ ✅ ✅ ❌ ❌ does not pass CI
25726 tb65536 (WIP) Galois group of `x ^ n - x - 1` large-import t-algebra WIP ❌ ✅ ✅ ❌ ✅ ❌ labelled WIP
26110 YaelDillies feat: sharp monoids toric t-algebra ✅ ✅ ✅ ✅ ✅ ✅ awaiting review
25875 robin-carlier feat(CategoryTheory/Monoidal/Action): actions as monoidal functors to endofunctors t-category-theory ✅ ✅ ✅ ✅ ✅ ✅ awaiting review
24383 YaelDillies feat: distributive Haar characters of `ℝ` and `ℂ` file-removed FLT t-measure-probability awaiting-CI WIP ❌ ✅ ✅ ❌ ❌ ❌ labelled WIP
25743 robin-carlier feat(AlgebraicTopology/SimplexCategory/Augmented): monoidal structure on `AugmentedSimplexCategory` t-topology t-category-theory ✅ ✅ ✅ ✅ ✅ ✅ merge conflict
26466 robin-carlier feat(AlgebraicTopology/SimplexCategory/Augmented): the canonical monoid object in the augmented simplex category t-category-theory blocked-by-other-PR ✅ ❌ ✅ ✅ ✅ ❌ blocked on another PR
26251 YaelDillies chore(Units): better follow the naming convention ✅ ✅ ✅ ✅ ✅ ✅ awaiting review
26021 vasnesterov feat(Data/Real): representation of reals from `[0, 1]` in positional system t-data ✅ ✅ ✅ ✅ ✅ ✅ awaiting review
21162 smmercuri feat: add `Valued.tendsto_zero_pow_of_le_neg_one` t-algebra delegated 🟤 ✅ ✅ ✅ ✅ ❌ running CI
26142 YaelDillies chore(GeomSum): split into ring vs field and non-ordered vs ordered parts t-algebra 🟤 ✅ ✅ ✅ ✅ ❌ running CI
26057 YaelDillies feat: `mon_tauto`, a simp set to prove tautologies about a monoid object toric t-category-theory ✅ ✅ ✅ ✅ ✅ ✅ awaiting review
25779 robin-carlier feat(CategoryTheory/Bicategory/NaturalTransformations): strong and lax natural transformations of lax functors t-category-theory ✅ ✅ ✅ ✅ ✅ ✅ awaiting review
22503 Kevew chore: deduce `Nat.multiplicity` lemmas from the `Nat.factorization` ones large-import t-data new-contributor blocked-by-other-PR ✅ ❌ ✅ ✅ ✅ ❌ blocked on another PR
26775 Komyyy style: replace `HEq x y` with `x ≍ y` ✅ ✅ ✅ ✅ ✅ ✅ awaiting review
26777 YaelDillies chore(Data/Set/Image): move `BooleanAlgebra` material to `Order` large-import ❌ ✅ ✅ ✅ ✅ ❌ failing CI
26779 zcyemi feat(LinearAlgebra/AffineSpace/Midpoint) add midpoint_vsub_midpoint_same_left new-contributor t-algebra 🟤 ✅ ✅ ✅ ✅ ❌ running CI
25273 YaelDillies refactor: make `MonoidAlgebra` into a one-field structure file-removed large-import t-algebra blocked-by-other-PR WIP ❌ ❌ ✅ ❌ ✅ ❌ blocked on another PR
26524 pechersky chore(RingTheory/Valuation): Valution.Integers implies IsFractionRing maintainer-merge t-algebra ✅ ✅ ✅ ✅ ✅ ✅ awaiting review
19668 YaelDillies refactor: define `≤`/`<` on `WithBot`/`WithTop` by induction t-order ❌ ✅ ✅ ✅ ✅ ❌ failing CI
25365 YaelDillies feat: `CommAlgCat` is cocartesian-monoidal toric t-algebra ✅ ✅ ✅ ✅ ✅ ✅ merge conflict
25326 YaelDillies feat: `Mon_ C` is cartesian-monoidal if `C` is toric t-category-theory blocked-by-other-PR ✅ ❌ ✅ ✅ ✅ ❌ blocked on another PR
26165 oliver-butterley feat(MeasureTheory.VectorMeasure): add lemma which shows that variation of a `ℝ≥0∞` VectorMeasure is equal to itself new-contributor t-measure-probability blocked-by-other-PR ✅ ❌ ✅ ✅ ✅ ❌ blocked on another PR
26168 oliver-butterley feat(MeasureTheory.VectorMeasure) : variation defined as a supremum is equal to variation defined using the Hahn-Jordan decomposition. new-contributor t-measure-probability blocked-by-other-PR ✅ ❌ ✅ ✅ ✅ ❌ awaiting review
26160 oliver-butterley feat(MeasureTheory.VectorMeasure): add several lemmas which characterize variation new-contributor t-measure-probability blocked-by-other-PR ✅ ❌ ✅ ✅ ✅ ❌ awaiting review
23177 faenuccio feat: more lemmas about ordered groups with zero large-import t-order awaiting-CI blocked-by-other-PR ❌ ❌ ✅ ✅ ❌ ❌ blocked on another PR
26447 robin-carlier feat(CategoryTheory/Limits/Shapes/Pullback/Categorical): bicategory-like lemmas for `CatCospanTransforms` t-category-theory ✅ ✅ ✅ ✅ ✅ ✅ awaiting review
26547 robin-carlier feat(CategoryTheory/Limits/Shapes/Pullback/Categorical/CatCospanTransform): more lemmas about isomorphisms of `CatCospanTransform` t-category-theory ✅ ✅ ✅ ✅ ✅ ✅ blocked on another PR
26655 Rida-Hamadani feat(SimpleGraph): sub-walks t-combinatorics ❌ ✅ ✅ ✅ ✅ ❌ failing CI
25347 sgouezel feat: define Riemannian manifolds t-differential-geometry blocked-by-other-PR WIP ✅ ❌ ✅ ❌ ✅ ❌ blocked on another PR
26578 robin-carlier feat(CategoryTheory/Limits/Pullbacks/Categorical/CatCospanTransform): adjunctions of categorical cospans large-import t-category-theory blocked-by-other-PR ✅ ❌ ✅ ✅ ✅ ❌ blocked on another PR
26731 javra feat(CategoryTheory/Enriched): category of enriched functors t-category-theory awaiting-author ✅ ✅ ✅ ✅ ❌ ❌ awaiting author
26579 robin-carlier feat(CategoryTheory/Limits/Pullbacks/Categorical/CatCospanTransform): equivalences of categorical cospans large-import t-category-theory blocked-by-other-PR ❌ ❌ ✅ ✅ ✅ ❌ blocked on another PR
26679 robin-carlier feat(CategoryTheory/Limits/Shapes/Pullback/Categorical): 2-functoriality of `CatCommSqOver` t-category-theory blocked-by-other-PR ✅ ❌ ✅ ✅ ✅ ❌ blocked on another PR
26752 robin-carlier feat(CategoryTheory/Limits/Shapes/Pullback/Categorical): pseudofunctoriality of `CategoricalPullback` t-category-theory blocked-by-other-PR 🟤 ❌ ✅ ✅ ✅ ❌ blocked on another PR
26753 robin-carlier feat(CategoryTheory/Limits/Shapes/Pullbacks/Categorical): the categorical pullback is invariant under equivalences of categories large-import t-category-theory blocked-by-other-PR 🟤 ❌ ✅ ✅ ✅ ❌ blocked on another PR
26778 sgouezel feat: length of a path in a manifold t-differential-geometry 🟤 ✅ ✅ ✅ ✅ ❌ running CI
26738 javra feat(AlgebraicToplogy/SimplexCategory): add notation for faces and degeneracies general truncated simplex categories infinity-cosmos t-topology t-category-theory ✅ ✅ ✅ ✅ ✅ ✅ awaiting review
25781 emilyriehl Feat(CategoryTheory): terminal categories with an application to hoFunctor infinity-cosmos large-import t-category-theory ✅ ✅ ✅ ✅ ✅ ✅ awaiting review
26781 zcyemi feat(Geometry/Euclidean/MongePoint) add theorems about orthocenter and circumcenter new-contributor t-euclidean-geometry ✅ ✅ ✅ ✅ ✅ ✅ awaiting review
26545 pechersky chore(RingTheory/Valuation): generalize lemmas about valuation of irreducibles in subring t-algebra t-analysis t-number-theory delegated ✅ ✅ ✅ ✅ ✅ ✅ awaiting review
25327 YaelDillies feat: `F.obj M` is a commutative monoid object if `M` is toric t-category-theory ready-to-merge ✅ ✅ ✅ ✅ ✅ ✅ awaiting bors
26757 fweth feat(CategoryTheory/Topos): define elementary topos new-contributor t-category-theory ✅ ✅ ✅ ✅ ✅ ✅ awaiting review
26318 PierreQuinton feat: add `BooleanSigmaAlgebra` new-contributor t-order awaiting-author ❌ ✅ ✅ ✅ ❌ ❌ failing CI
25784 emilyriehl feat(Bicategory/CatEnriched): 2-cat from Cat-enriched cat infinity-cosmos t-category-theory ✅ ✅ ✅ ✅ ✅ ✅ awaiting review
26772 vihdzp feat(Order/InitialSeg): `InitialSeg.exists_sum_relIso` t-order delegated 🟤 ✅ ✅ ✅ ✅ ❌ running CI
24192 alreadydone feat(RingTheory): semisimple Wedderburn–Artin existence t-algebra ✅ ✅ ✅ ✅ ✅ ✅ awaiting review
26732 YaelDillies chore(Algebra/Equiv/TransferInstance): split according to algebraic structures file-removed t-algebra awaiting-CI blocked-by-other-PR ❌ ❌ ✅ ✅ ❌ ❌ blocked on another PR
26774 YaelDillies chore(Algebra/Equiv/TransferInstance): delete duplicated `Shrink` material t-algebra ❌ ✅ ✅ ✅ ✅ ❌ failing CI
14426 adomani dev: `#min_imps` command merge-conflict WIP ✅ ✅ ❌ ❌ ✅ ❌ labelled WIP
14167 alreadydone feat: Group scheme structure on Weierstrass curve workshop-AIM-AG-2024 t-algebraic-geometry merge-conflict WIP ❌ ✅ ❌ ❌ ✅ ❌ labelled WIP
13847 alreadydone feat(EllipticCurve): the universal elliptic curve t-algebra t-algebraic-geometry merge-conflict awaiting-author ✅ ✅ ❌ ✅ ❌ ❌ merge conflict
13297 urkud feat(Semicontinuous): add `comp` lemma t-order t-topology merge-conflict awaiting-author ✅ ✅ ❌ ✅ ❌ ❌ merge conflict
12933 grunweg chore: replace some use of > or ≥ by < or ≤ merge-conflict awaiting-author ❌ ✅ ❌ ✅ ❌ ❌ failing CI
12879 grunweg feat: port ge_or_gt linter from mathlib3 tech debt t-linter merge-conflict blocked-by-other-PR ❌ ❌ ❌ ✅ ✅ ❌ blocked on another PR
12679 MichaelStollBayreuth perf(NumberTheory/RamificationInertia): speed up slow file merge-conflict WIP ✅ ✅ ❌ ❌ ✅ ❌ labelled WIP
12934 grunweg chore: replace more uses of > or ≥ by < or ≤ merge-conflict awaiting-author help-wanted ✅ ✅ ❌ ❌ ❌ ❌ looking for help
12773 apnelson1 feat(Combinatorics/HypergraphRamsey): Ramsey's theorem for hypergraphs t-combinatorics merge-conflict ❌ ✅ ❌ ✅ ✅ ❌ failing CI
13057 alreadydone feat(NumberTheory): characterize elliptic divisibility sequences t-algebra t-number-theory merge-conflict blocked-by-other-PR ✅ ❌ ❌ ✅ ✅ ❌ blocked on another PR
12936 mattrobball chore(Quiver.Opposite): make `Quiver.Hom.op/unop` `abbrev`'s merge-conflict ✅ ✅ ❌ ✅ ✅ ❌ merge conflict
12608 eric-wieser feat: allow `nsmul` / `zsmul` to be omitted again, with a warning t-algebra t-meta merge-conflict awaiting-author ✅ ✅ ❌ ✅ ❌ ❌ merge conflict
11575 ScottCarnahan feat (RingTheory/HahnSeries/Addition): Lemmas on leading terms t-algebra merge-conflict WIP ✅ ✅ ❌ ❌ ✅ ❌ labelled WIP
11617 urkud refactor(Finset): redefine Finset.diag, review API t-logic merge-conflict awaiting-author ✅ ✅ ❌ ✅ ❌ ❌ merge conflict
12292 AntoineChambert-Loir feat(Mathlib.RingTheory.TensorProduct.MonoidAlgebra) : tensor product of a monoid algebra t-algebra merge-conflict WIP ❌ ✅ ❌ ❌ ✅ ❌ labelled WIP
12192 Ruben-VandeVelde feat: generalize isLittleO_const_id_atTop/atBot t-analysis merge-conflict awaiting-author ✅ ✅ ❌ ✅ ❌ ❌ merge conflict
11100 eric-wieser feat(CategoryTheory/Limits): add `Functor.mapBinaryBiconeInv` t-category-theory awaiting-CI merge-conflict ❌ ✅ ❌ ✅ ❌ ❌ does not pass CI
11021 jstoobysmith feat(AlgebraicTopology) : add join of augmented SSets new-contributor t-category-theory merge-conflict WIP ❌ ✅ ❌ ❌ ✅ ❌ labelled WIP
10444 urkud doc(IsROrC): expand the docstring t-analysis merge-conflict awaiting-author documentation ✅ ✅ ❌ ✅ ❌ ❌ merge conflict
10842 mcdoll chore: simplify proofs using new positivity extensions and tests merge-conflict blocked-by-other-PR WIP ✅ ❌ ❌ ❌ ✅ ❌ blocked on another PR
10721 urkud feat(Order/FunLike): define `PointwiseLE` t-logic t-order merge-conflict ✅ ✅ ❌ ✅ ✅ ❌ merge conflict
10594 lecopivo feat: `fun_trans` function transformation tactic e.g. for computing derivatives t-meta merge-conflict WIP ❌ ✅ ❌ ❌ ✅ ❌ labelled WIP
10024 ADedecker feat: rename `connectedComponentOfOne` to `identityComponent`, prove that it is normal and open t-topology awaiting-CI merge-conflict ❌ ✅ ❌ ✅ ❌ ❌ does not pass CI
10521 eric-wieser chore: generalize `IsBoundedLinearMap` to modules t-analysis merge-conflict awaiting-author ✅ ✅ ❌ ✅ ❌ ❌ merge conflict
8519 eric-wieser refactor(LinearAlgebra/TensorProduct): golf using `liftAddHom` t-algebra merge-conflict awaiting-author ✅ ✅ ❌ ✅ ❌ ❌ merge conflict
8961 eric-wieser refactor: use the coinduced topology on ULift awaiting-CI merge-conflict please-adopt awaiting-author ✅ ✅ ❌ ❌ ❌ ❌ looking for help
9642 eric-wieser refactor(Analysis/Normed/{Group/Field}/Basic): Let `extends` generate the repeated fields t-analysis merge-conflict awaiting-author WIP help-wanted ✅ ✅ ❌ ❌ ❌ ❌ looking for help
8616 eric-wieser feat(Algebra/FreeAlgebra): add right action and `IsCentralScalar` t-algebra awaiting-CI merge-conflict ✅ ✅ ❌ ✅ ❌ ❌ does not pass CI
8503 thorimur feat: meta utils for `refine?` t-meta merge-conflict awaiting-author ✅ ✅ ❌ ✅ ❌ ❌ merge conflict
9146 laughinggas feat(Data/ZMod/Defs): Topological structure on `ZMod` t-algebra t-topology merge-conflict awaiting-author ✅ ✅ ❌ ✅ ❌ ❌ merge conflict
8658 eric-wieser feat: support right actions for `Con` t-algebra merge-conflict awaiting-author ✅ ✅ ❌ ✅ ❌ ❌ merge conflict
9229 eric-wieser refactor(Algebra/GradedMonoid): Use `HMul` to define `GMul` t-algebra merge-conflict WIP ❌ ✅ ❌ ❌ ✅ ❌ labelled WIP
9356 alexjbest feat: assumption? t-meta merge-conflict awaiting-author ✅ ✅ ❌ ✅ ❌ ❌ merge conflict
9487 eric-wieser feat: the exponential of dual numbers over non-commutative rings t-measure-probability t-algebra t-analysis merge-conflict WIP ❌ ✅ ❌ ❌ ✅ ❌ labelled WIP
8906 jjaassoonn feat: add some missing lemmas about linear algebra t-algebra merge-conflict awaiting-author ❌ ✅ ❌ ✅ ❌ ❌ failing CI
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 ✅ ✅ ❌ ✅ ✅ ❌ merge conflict
9564 AntoineChambert-Loir weaken commutativity assumptions for AdjoinRoot.lift and AdjoinRoot.liftHom t-algebra merge-conflict WIP ❌ ✅ ❌ ❌ ✅ ❌ labelled WIP
9354 chenyili0818 feat: monotonicity of gradient on convex real-valued functions t-analysis merge-conflict awaiting-author ✅ ✅ ❌ ✅ ❌ ❌ merge conflict
9570 eric-wieser feat(Algebra/Star): Non-commutative generalization of `StarModule` t-algebra awaiting-CI merge-conflict WIP ❌ ✅ ❌ ❌ ❌ ❌ labelled 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 ✅ ✅ ❌ ✅ ✅ ❌ 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 ✅ ❌ ❌ ✅ ✅ ❌ blocked on another PR
6630 MohanadAhmed feat: Reduced Spectral Theorem t-algebra merge-conflict WIP ❌ ✅ ❌ ❌ ✅ ❌ labelled WIP
6931 urkud refactor(Analysis/Normed*): use `RingHomIsometric` for `*.norm_cast` t-analysis merge-conflict help-wanted ❌ ✅ ❌ ❌ ✅ ❌ looking for help
6930 kmill feat: `resynth_instances` tactic for resynthesizing instances in the goal or local context t-meta merge-conflict WIP ✅ ✅ ❌ ❌ ✅ ❌ labelled WIP
7962 eric-wieser feat: `DualNumber (Quaternion R)` as a `CliffordAlgebra` t-algebra merge-conflict WIP ✅ ✅ ❌ ❌ ✅ ❌ labelled WIP
6791 eric-wieser refactor: Use flat structures for morphisms awaiting-CI merge-conflict awaiting-author help-wanted ✅ ✅ ❌ ❌ ❌ ❌ looking for help
7835 shuxuezhuyi feat(LinearAlgebra/Matrix): `lift` for projective special linear group t-algebra merge-conflict awaiting-author ✅ ✅ ❌ ✅ ❌ ❌ merge conflict
7615 eric-wieser chore(LinearAlgebra/Basic): generalize compatibleMaps to semilinear maps t-algebra awaiting-CI easy merge-conflict ✅ ✅ ❌ ✅ ❌ ❌ does not pass CI
7875 FR-vdash-bot chore: make `SMulCommClass A A B` and `SMulCommClass A B B` higher priority slow-typeclass-synthesis t-algebra merge-conflict ✅ ✅ ❌ ✅ ✅ ❌ merge conflict
6777 adomani chore(Co*variantClass): replace eta-expanded (· * ·), (· + ·), (· ≤ ·), (· < ·) merge-conflict ✅ ✅ ❌ ✅ ✅ ❌ merge conflict
7909 mcdoll fix(Tactic/Continuity): remove npowRec and add new tag for Continuous.pow t-topology t-meta merge-conflict WIP ✅ ✅ ❌ ❌ ✅ ❌ labelled WIP
7427 MohanadAhmed Mohanad ahmed/sort eigenvalues abs merge-conflict WIP ✅ ✅ ❌ ❌ ✅ ❌ labelled WIP
7932 eric-wieser refactor(Algebra/TrivSqZeroExt): replace with a structure t-algebra awaiting-CI merge-conflict ✅ ✅ ❌ ✅ ❌ ❌ does not pass CI
7649 eric-wieser wip: instead of `suppress_compilation`, use `implemented_by` merge-conflict WIP ❌ ✅ ❌ ❌ ✅ ❌ labelled WIP
7227 kmill feat: flexible binders and integration into notation3 t-meta merge-conflict WIP ❌ ✅ ❌ ❌ ✅ ❌ labelled WIP
8364 thorimur feat: `refine?` t-meta merge-conflict blocked-by-other-PR ✅ ❌ ❌ ✅ ✅ ❌ blocked on another PR
7351 shuxuezhuyi feat(Topology/Algebra/Order): extend function on `Ioo` to `Icc` t-order merge-conflict awaiting-author ✅ ✅ ❌ ✅ ❌ ❌ merge conflict
7601 digama0 feat: ring hom support in `ring` t-algebra t-meta merge-conflict awaiting-author ✅ ✅ ❌ ✅ ❌ ❌ merge conflict
7713 RemyDegenne feat: add_left/right_inj for measures t-measure-probability merge-conflict awaiting-author ✅ ✅ ❌ ✅ ❌ ❌ merge conflict
6580 adomani chore: `move_add`-driven replacements merge-conflict awaiting-author ✅ ✅ ❌ ✅ ❌ ❌ merge conflict
7467 ADedecker feat: spectrum of X →ᵇ ℂ is StoneCech X t-analysis merge-conflict WIP ✅ ✅ ❌ ❌ ✅ ❌ labelled WIP
6210 MohanadAhmed feat(Data/IsROrC/Basic): add a `StarOrderedRing` instance t-algebra t-analysis merge-conflict WIP ✅ ✅ ❌ ❌ ✅ ❌ labelled WIP
6633 adomani feat(..Polynomial..): `MvPolynomial`s have no zero divisors t-algebra merge-conflict awaiting-author ✅ ✅ ❌ ✅ ❌ ❌ merge conflict
6330 FR-vdash-bot chore: make some instance about `Sub...Class` higher priority than `Sub...` slow-typeclass-synthesis t-algebra merge-conflict WIP ✅ ✅ ❌ ❌ ✅ ❌ labelled WIP
6403 FR-vdash-bot chore: change instance priorities of `Ordered*` hierarchy slow-typeclass-synthesis t-order t-algebra merge-conflict awaiting-author ✅ ✅ ❌ ✅ ❌ ❌ merge conflict
6993 jjaassoonn feat : lemmas about `AddMonoidAlgebra.{divOf, modOf}` t-algebra merge-conflict ✅ ✅ ❌ ✅ ✅ ❌ merge conflict
5912 ADedecker feat(Analysis.Distribution.ContDiffMapSupportedIn): space of smooth maps with support in a fixed compact t-analysis merge-conflict WIP ✅ ✅ ❌ ❌ ✅ ❌ labelled WIP
5934 eric-wieser feat: port Data.Rat.MetaDefs t-meta merge-conflict mathlib-port help-wanted ✅ ✅ ❌ ❌ ✅ ❌ looking for help
6002 slerpyyy feat(Analysis.SpecialFunctions.Gaussian): add `integrable_fun_mul_exp_neg_mul_sq` t-analysis merge-conflict awaiting-author ✅ ✅ ❌ ✅ ❌ ❌ merge conflict
6268 eric-wieser Fixups to #3838 merge-conflict WIP ❌ ✅ ❌ ❌ ✅ ❌ labelled WIP
6590 mcdoll feat: composition of LinearPMaps t-algebra merge-conflict WIP ✅ ✅ ❌ ❌ ✅ ❌ labelled WIP
6195 eric-wieser chore(RingTheory/TensorProduct): golf the `mul` definition t-algebra awaiting-CI merge-conflict ✅ ✅ ❌ ✅ ❌ ❌ does not pass CI
6328 FR-vdash-bot chore: make some instance about `Sub...Class` lower priority t-algebra awaiting-CI merge-conflict WIP ✅ ✅ ❌ ❌ ❌ ❌ labelled WIP
6491 eric-wieser chore(Mathlib/Algebra/Hom/GroupAction): add `SMulHomClass.comp_smul` t-algebra merge-conflict ✅ ✅ ❌ ✅ ✅ ❌ merge conflict
5133 kmill feat: IntermediateField adjoin syntax for sets of elements t-algebra merge-conflict WIP ✅ ✅ ❌ ❌ ✅ ❌ labelled WIP
3808 kim-em feat: #formalize, backed by a choice of LLMs t-meta merge-conflict awaiting-author ✅ ✅ ❌ ✅ ❌ ❌ merge conflict
4127 kmill refactor: create HasAdj class, define Digraph, and generalize some SimpleGraph API t-combinatorics merge-conflict awaiting-author ✅ ✅ ❌ ✅ ❌ ❌ merge conflict
4871 j-loreaux feat: define the additive submonoid of positive elements in a star ordered ring t-algebra awaiting-CI merge-conflict ??? ✅ ❌ ✅ ❌ ❌ does not pass CI
6079 eric-wieser fix: deduplicate variables awaiting-CI merge-conflict ✅ ✅ ❌ ✅ ❌ ❌ does not pass CI
4960 eric-wieser chore: use `open scoped` awaiting-CI merge-conflict ✅ ✅ ❌ ✅ ❌ ❌ does not pass CI
7076 grunweg feat: define measure zero subsets of a manifold t-measure-probability t-differential-geometry merge-conflict WIP ✅ ✅ ❌ ❌ ✅ ❌ labelled WIP
3757 thorimur feat: config options for `fail_if_no_progress` t-meta merge-conflict WIP ✅ ✅ ❌ ❌ ✅ ❌ labelled WIP
12353 thorimur feat: `conv%` t-meta merge-conflict WIP ✅ ✅ ❌ ❌ ✅ ❌ labelled WIP
7903 urkud feat: define `UnboundedSpace` t-topology merge-conflict help-wanted ❌ ✅ ❌ ❌ ✅ ❌ looking for help
15400 grunweg feat: "confusing variables" linter t-linter merge-conflict WIP ❌ ✅ ❌ ❌ ✅ ❌ labelled WIP
12143 adomani feat: generic linter, absorbing `cdot` linter and `attribute [instance] in` linter t-linter merge-conflict ❌ ✅ ❌ ✅ ✅ ❌ failing CI
14654 grunweg feat(runLinter): allow only running certain linters t-linter RFC merge-conflict ❌ ✅ ❌ ✅ ✅ ❌ failing CI
15679 adomani test: refactor in CI merge-conflict WIP ❌ ✅ ❌ ❌ ✅ ❌ labelled WIP
7565 shuxuezhuyi feat(Topology/Algebra/Order): extend homeomorphism of `Ioo` to `Icc` t-order t-topology merge-conflict blocked-by-other-PR ✅ ❌ ❌ ✅ ✅ ❌ blocked on another PR
10629 madvorak feat: List.cons_sublist_append_iff_right t-data merge-conflict ✅ ✅ ❌ ✅ ✅ ❌ merge conflict
9973 Ruben-VandeVelde feat: polynomials formed by lists t-data merge-conflict please-adopt ❌ ✅ ❌ ❌ ✅ ❌ looking for help
12926 joelriou feat(CategoryTheory): the monoidal category structure induced by a monoidal functor t-category-theory merge-conflict WIP ❌ ✅ ❌ ❌ ✅ ❌ labelled WIP
12869 adomani feat: linter and script for `theorem` vs `lemma` t-linter merge-conflict awaiting-author ✅ ✅ ❌ ✅ ❌ ❌ merge conflict
12093 ADedecker feat: tweak the definition of semicontinuity to behave better in nonlinear orders t-topology merge-conflict WIP ✅ ✅ ❌ ❌ ✅ ❌ labelled WIP
11393 mcdoll feat(Analysis/Distribution/SchwartzSpace): The Heine-Borel property t-analysis merge-conflict WIP ❌ ✅ ❌ ❌ ✅ ❌ labelled WIP
9444 erdOne feat: Various instances regarding `𝓞 K`. t-number-theory merge-conflict help-wanted ❌ ✅ ❌ ❌ ✅ ❌ looking for help
8931 hmonroe feat(Computable): define P, NP, and NP-complete t-computability merge-conflict awaiting-author ❌ ✅ ❌ ✅ ❌ ❌ failing CI
10345 newell feat(Algebra.Module.Zlattice): Add Voronoi Domain t-algebra merge-conflict WIP ❌ ✅ ❌ ❌ ✅ ❌ labelled WIP
8608 eric-wieser feat: multiplicativize `AddTorsor` t-algebra merge-conflict WIP ❌ ✅ ❌ ❌ ✅ ❌ labelled 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 ✅ ❌ ❌ ✅ ❌ ❌ blocked on another PR
6603 tydeu feat: automatically try `cache get` before build CI merge-conflict WIP ✅ ✅ ❌ ❌ ✅ ❌ labelled WIP
6058 apurvnakade feat: duality theory for cone programs t-analysis merge-conflict WIP ❌ ✅ ❌ ❌ ✅ ❌ labelled WIP
6449 ADedecker feat: functions with finite fibers t-topology merge-conflict awaiting-author ❌ ✅ ❌ ✅ ❌ ❌ failing CI
7739 mcdoll feat(LinearAlgebra/LinearPMap): difference of inverses t-algebra merge-conflict WIP ❌ ✅ ❌ ❌ ✅ ❌ labelled WIP
11632 mattrobball chore(Group/RingTheory.Congruence): make `Quotient`'s reducible merge-conflict ✅ ✅ ❌ ✅ ✅ ❌ merge conflict
13791 digama0 refactor: Primrec and Partrec tech debt t-computability merge-conflict ✅ ✅ ❌ ✅ ✅ ❌ merge conflict
11964 adamtopaz feat: The functor of points of a scheme t-algebraic-geometry t-category-theory merge-conflict ✅ ✅ ❌ ✅ ✅ ❌ merge conflict
12418 rosborn style: replace preimage_val with ↓∩ notation merge-conflict ✅ ✅ ❌ ✅ ✅ ❌ merge conflict
9978 FR-vdash-bot chore(FieldTheory/KummerExtension): move some lemmas earlier t-algebra merge-conflict awaiting-author ✅ ✅ ❌ ✅ ❌ ❌ merge conflict
12429 adomani feat: toND -- auto-generating natDegree t-algebra RFC t-meta merge-conflict awaiting-author ✅ ✅ ❌ ✅ ❌ ❌ merge conflict
12751 Command-Master feat: add lemmas for Nat/Bits, Nat/Bitwise and Nat/Size t-data new-contributor merge-conflict ✅ ✅ ❌ ✅ ✅ ❌ merge conflict
9935 jstoobysmith feat(AlgebraicTopology): add constructors for horns new-contributor t-algebra t-topology merge-conflict awaiting-author ❌ ✅ ❌ ✅ ❌ ❌ failing CI
15448 urkud chore(*): deprecate `Option.elim'` tech debt merge-conflict awaiting-author ✅ ✅ ❌ ✅ ❌ ❌ merge conflict
10349 Shamrock-Frost refactor(CategoryTheory/MorphismProperty) t-category-theory merge-conflict ❌ ✅ ❌ ✅ ✅ ❌ failing CI
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 ❌ ✅ ❌ ✅ ✅ ❌ failing CI
13573 Shamrock-Frost feat: add multivariate polynomial modules t-algebra merge-conflict awaiting-author ✅ ✅ ❌ ✅ ❌ ❌ merge conflict
6517 MohanadAhmed feat: discrete Fourier transform of a finite sequence t-algebra merge-conflict awaiting-author ✅ ✅ ❌ ✅ ❌ ❌ merge conflict
13155 alreadydone feat(NumberTheory/EllipticDivisibilitySequence): show elliptic relations follow from even-odd recursion t-algebra t-number-theory merge-conflict awaiting-author ✅ ✅ ❌ ✅ ❌ ❌ merge conflict
15600 adomani feat: lint also `let` vs `have` t-linter merge-conflict WIP ✅ ✅ ❌ ❌ ✅ ❌ labelled WIP
14038 adomani test/decl diff in lean dev merge-conflict WIP ❌ ✅ ❌ ❌ ✅ ❌ labelled WIP
7861 shuxuezhuyi feat(Geometry/Hyperbolic/UpperHalfPlane): instance IsometricSMul PSL(2, ℝ) ℍ t-euclidean-geometry merge-conflict blocked-by-other-PR ✅ ❌ ❌ ✅ ✅ ❌ blocked on another PR
7545 shuxuezhuyi feat: APIs of `Function.extend f g e'` when `f` is injective t-logic merge-conflict awaiting-author ✅ ✅ ❌ ✅ ❌ ❌ merge conflict
10765 Vierkantor feat(Tactic): `ring` modulo a given characteristic t-meta merge-conflict awaiting-author help-wanted ✅ ✅ ❌ ❌ ❌ ❌ looking for help
14078 Ruben-VandeVelde feat(CI): continue after mk_all fails CI merge-conflict awaiting-author ❌ ✅ ❌ ✅ ❌ ❌ failing CI
11800 JADekker feat : Define KappaLindelöf spaces awaiting-zulip t-topology merge-conflict please-adopt ✅ ✅ ❌ ❌ ❌ ❌ looking for help
12087 JADekker feat : complete API for K-Lindelöf spaces t-topology merge-conflict please-adopt blocked-by-other-PR ✅ ❌ ❌ ❌ ✅ ❌ blocked on another PR
11283 hmonroe feat(ModelTheory/Satisfiability): define theory with independent sentence t-logic merge-conflict WIP ✅ ✅ ❌ ❌ ✅ ❌ labelled WIP
16914 siddhartha-gadgil Loogle syntax with non-reserved merge-conflict WIP ✅ ✅ ❌ ❌ ✅ ❌ labelled WIP
10075 dupuisf refactor: generalize `MonoidHom.ker` and `MonoidHom.range` to `MonoidHomClass` t-algebra merge-conflict awaiting-author ✅ ✅ ❌ ✅ ❌ ❌ merge conflict
10991 thorimur feat: `tfae` block tactic t-meta merge-conflict modifies-tactic-syntax WIP ✅ ✅ ❌ ❌ ✅ ❌ labelled WIP
16464 Parcly-Taxel chore: deprecate `Nat.(case_)strong_induction_on` tech debt merge-conflict ✅ ✅ ❌ ✅ ✅ ❌ merge conflict
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 ✅ ❌ ❌ ✅ ✅ ❌ blocked on another PR
8118 iwilare feat(CategoryTheory): add dinatural transformations t-category-theory merge-conflict awaiting-author ✅ ✅ ❌ ✅ ❌ ❌ merge conflict
10006 jstoobysmith feat(AlgebraicTopology): homotopy in quasicategories new-contributor t-category-theory merge-conflict awaiting-author blocked-by-other-PR ✅ ❌ ❌ ✅ ❌ ❌ blocked on another PR
14242 js2357 feat: Prove equivalence of `isDedekindDomain` and `isDedekindDomainDvr` new-contributor t-algebra merge-conflict blocked-by-other-PR ✅ ❌ ❌ ✅ ✅ ❌ blocked on another PR
17110 FR-vdash-bot chore: deprecate some lemmas about equality blocked-by-batt-PR merge-conflict ✅ ❌ ❌ ✅ ✅ ❌ blocked on another PR
7516 ADedecker perf: use `abbrev` to prevent unifying useless data merge-conflict WIP ❌ ✅ ❌ ❌ ✅ ❌ labelled WIP
16215 adomasbaliuka feat(Tactic/Linter): lint unwanted unicode t-linter merge-conflict blocked-by-other-PR ❌ ❌ ❌ ✅ ✅ ❌ blocked on another PR
17127 FR-vdash-bot chore: remove global `Quotient.mk` `⟦·⟧` notation t-data merge-conflict ✅ ✅ ❌ ✅ ✅ ❌ merge conflict
16888 metinersin feat(ModelTheory/Complexity): Define conjunctive and disjunctive normal forms new-contributor t-logic merge-conflict blocked-by-other-PR ✅ ❌ ❌ ✅ ✅ ❌ blocked on another PR
16887 metinersin feat(ModelTheory/Complexity): define conjunctive and disjunctive formulas new-contributor t-logic merge-conflict blocked-by-other-PR ✅ ❌ ❌ ✅ ✅ ❌ blocked on another PR
16889 metinersin feat(ModelTheory/Complexity): Normal forms new-contributor t-logic merge-conflict blocked-by-other-PR ✅ ❌ ❌ ✅ ✅ ❌ blocked on another PR
14712 FR-vdash-bot perf: change instance priority and order about `OfNat` slow-typeclass-synthesis t-algebra merge-conflict delegated ✅ ✅ ❌ ✅ ✅ ❌ merge conflict
11500 mcdoll refactor(Topology/Algebra/Module/WeakDual): Clean up t-topology merge-conflict awaiting-author ✅ ✅ ❌ ✅ ❌ ❌ merge conflict
5995 FR-vdash-bot feat: add APIs about `Quotient.choice` t-data RFC merge-conflict awaiting-author ✅ ✅ ❌ ✅ ❌ ❌ merge conflict
10190 jstoobysmith feat(AlgebraicTopology): add Augmented Simplex Category new-contributor t-algebra t-topology t-category-theory merge-conflict WIP ❌ ✅ ❌ ❌ ✅ ❌ labelled WIP
8029 alreadydone refactor: Homotopy between Functions not ContinuousMaps t-topology RFC merge-conflict ✅ ✅ ❌ ✅ ✅ ❌ merge conflict
15916 vihdzp feat(SetTheory/Ordinal/CantorNormalForm): Coefficients of CNF as finsupp t-logic merge-conflict blocked-by-other-PR ✅ ❌ ❌ ✅ ✅ ❌ blocked on another PR
13156 erdOne refactor(Algebra/Module/LocalizedModule): Redefine `LocalizedModule` in terms of `OreLocalization`. t-algebra merge-conflict ❌ ✅ ❌ ✅ ✅ ❌ failing CI
16348 urkud refactor(Topology): require `LinearOrder` with `OrderTopology` t-order t-topology merge-conflict awaiting-author ✅ ✅ ❌ ✅ ❌ ❌ merge conflict
6034 mattrobball feat (Mathlib.Tactic.FieldSimp) : discharger uses normCast t-meta merge-conflict awaiting-author ❌ ✅ ❌ ✅ ❌ ❌ failing CI
13965 pechersky feat(Data/DigitExpansion): reals via digit expansion are complete t-data merge-conflict blocked-by-other-PR ❌ ❌ ❌ ✅ ✅ ❌ blocked on another PR
17519 grunweg feat: the `metrisableSpace` linter t-linter merge-conflict blocked-by-other-PR ✅ ❌ ❌ ✅ ✅ ❌ blocked on another PR
12750 Command-Master feat: define Gray code t-data new-contributor merge-conflict awaiting-author blocked-by-other-PR ❌ ❌ ❌ ✅ ❌ ❌ blocked on another PR
16925 YnirPaz feat(SetTheory/Cardinal/Cofinality): aleph index of singular cardinal has infinite cofinality t-set-theory merge-conflict WIP ✅ ✅ ❌ ❌ ✅ ❌ labelled WIP
17757 vihdzp refactor(*): generalize typeclass assumptions in morphisms t-algebra merge-conflict WIP ❌ ✅ ❌ ❌ ✅ ❌ labelled WIP
9605 davikrehalt feat(Data/Finset & List): Add Lemmas for Sorting and Filtering t-data new-contributor merge-conflict please-adopt awaiting-author ❌ ✅ ❌ ❌ ❌ ❌ looking for help
13514 madvorak feat(Computability/ContextFreeGrammar): closure under union t-computability merge-conflict blocked-by-other-PR ✅ ❌ ❌ ✅ ✅ ❌ blocked on another PR
17518 grunweg feat: lint on declarations mentioning `Invertible` or `Unique` awaiting-zulip t-linter merge-conflict blocked-by-other-PR ❌ ❌ ❌ ✅ ❌ ❌ blocked on another PR
9654 urkud feat: add `@[mk_eq]` version of `@[mk_iff]` t-meta merge-conflict awaiting-author ✅ ✅ ❌ ✅ ❌ ❌ merge conflict
16704 AntoineChambert-Loir feat(Mathlib.Data.Ordering.Dickson): Dickson orders t-order merge-conflict WIP ✅ ✅ ❌ ❌ ✅ ❌ labelled WIP
16355 Ruben-VandeVelde feat: odd_{add,sub}_one t-algebra t-number-theory merge-conflict awaiting-author ✅ ✅ ❌ ✅ ❌ ❌ merge conflict
8479 alexjbest feat: use leaff in CI merge-conflict awaiting-author WIP ✅ ✅ ❌ ❌ ❌ ❌ ⚠️ labelled WIP
14598 Command-Master chore: add typeclasses to unify various `add_top`, `add_eq_top`, etc. new-contributor t-order t-algebra merge-conflict ✅ ✅ ❌ ✅ ✅ ❌ merge conflict
12778 MichaelStollBayreuth perf: decouple algebraic and order hierarchies in type class search slow-typeclass-synthesis t-order t-algebra merge-conflict ✅ ✅ ❌ ✅ ✅ ❌ merge conflict
16885 metinersin feat(ModelTheory/Complexity): define literals new-contributor t-logic merge-conflict awaiting-author ✅ ✅ ❌ ✅ ❌ ❌ merge conflict
18716 jjaassoonn feat(Algebra/Module/GradedModule): quotient and subgrading t-algebra awaiting-CI merge-conflict blocked-by-other-PR WIP ❌ ❌ ❌ ❌ ❌ ❌ blocked on another PR
18784 erdOne feat(AlgebraicGeometry) use `addMorphismPropertyInstances` t-algebraic-geometry merge-conflict blocked-by-other-PR ❌ ❌ ❌ ✅ ✅ ❌ blocked on another PR
9341 winstonyin feat: Naturality of integral curves t-differential-geometry merge-conflict awaiting-author ✅ ✅ ❌ ✅ ❌ ❌ merge conflict
16014 vihdzp feat(SetTheory/Ordinal/Principal): even more lemmas on additively principal ordinals t-set-theory t-logic merge-conflict blocked-by-other-PR ❌ ❌ ❌ ✅ ✅ ❌ blocked on another PR
13248 hcWang942 feat: basic concepts of auction theory new-contributor t-logic merge-conflict awaiting-author ✅ ✅ ❌ ✅ ❌ ❌ merge conflict
9344 erdOne feat: Add `AddGroup.FG` -> `Module.Finite ℤ` as instances t-algebra merge-conflict awaiting-author ✅ ✅ ❌ ✅ ❌ ❌ merge conflict
12133 ADedecker feat: generalize instIsLowerProd to arbitrary products t-order t-topology merge-conflict awaiting-author ✅ ✅ ❌ ✅ ❌ ❌ merge conflict
16637 FR-vdash-bot perf: reorder `extends` of `(Add)Monoid` t-algebra merge-conflict WIP ❌ ✅ ❌ ❌ ✅ ❌ labelled WIP
14739 urkud feat(Measure): add `gcongr` lemmas t-measure-probability merge-conflict awaiting-author WIP help-wanted ✅ ✅ ❌ ❌ ❌ ❌ looking for help
8661 joelriou feat(CategoryTheory/Sites): descent of sheaves t-category-theory merge-conflict WIP ✅ ✅ ❌ ❌ ✅ ❌ labelled WIP
18806 FR-vdash-bot refactor: deprecate `MulEquivClass` t-algebra merge-conflict ✅ ✅ ❌ ✅ ✅ ❌ merge conflict
10476 shuxuezhuyi feat(Topology/UniformSpace): define uniform preordered space t-topology merge-conflict awaiting-author ✅ ✅ ❌ ✅ ❌ ❌ merge conflict
17593 FR-vdash-bot chore(Algebra/Order/GroupWithZero/Unbundled): deprecate useless lemmas, use `ZeroLEOneClass` t-order t-algebra merge-conflict blocked-by-other-PR ✅ ❌ ❌ ✅ ✅ ❌ blocked on another PR
17623 FR-vdash-bot feat(Algebra/Order/GroupWithZero/Unbundled): add some lemmas awaiting-zulip t-order t-algebra merge-conflict ✅ ✅ ❌ ✅ ❌ ❌ awaiting a zulip discussion
16361 vihdzp chore(SetTheory/Ordinal/FixedPointApproximants): golf + better variable management t-set-theory t-logic merge-conflict awaiting-author ✅ ✅ ❌ ✅ ❌ ❌ merge conflict
17624 FR-vdash-bot feat(Algebra/Order/GroupWithZero/Unbundled): generalize lemmas t-order t-algebra merge-conflict blocked-by-other-PR ✅ ❌ ❌ ✅ ✅ ❌ blocked on another PR
18646 jxjwan feat(RingTheory): isotypic components new-contributor t-algebra merge-conflict ❌ ✅ ❌ ✅ ✅ ❌ failing CI
17513 FR-vdash-bot perf: do not search algebraic hierarchies when using `map_*` lemmas awaiting-bench t-algebra merge-conflict WIP ✅ ✅ ❌ ❌ ✅ ❌ labelled WIP
17515 FR-vdash-bot perf: do not need `simp low` now t-algebra merge-conflict blocked-by-other-PR ❌ ❌ ❌ ✅ ✅ ❌ blocked on another PR
19212 Julian feat(LinearAlgebra): add a variable_alias for VectorSpace t-algebra merge-conflict ✅ ✅ ❌ ✅ ✅ ❌ merge conflict
19337 zeramorphic feat(Data/Finsupp): generalise `Finsupp` to any "zero" value t-data merge-conflict ✅ ✅ ❌ ✅ ✅ ❌ merge conflict
9598 AlexKontorovich feat(Analysis/Complex): HasPrimitives on disc t-analysis merge-conflict ❌ ✅ ❌ ✅ ✅ ❌ failing CI
19414 vihdzp feat: Nesbitt's inequality large-import t-algebra merge-conflict awaiting-author blocked-by-other-PR WIP ❌ ❌ ❌ ❌ ❌ ❌ blocked on another PR
19420 vihdzp feat: AM-HM inequality t-algebra merge-conflict awaiting-author WIP ✅ ✅ ❌ ❌ ❌ ❌ labelled WIP
19415 vihdzp chore: move results on `Σ i : Fin n, f i` earlier t-data awaiting-CI merge-conflict ❌ ✅ ❌ ✅ ❌ ❌ does not pass CI
10332 adri326 feat(Topology/Sets): define regular open sets and their boolean algebra t-topology merge-conflict WIP ❌ ✅ ❌ ❌ ✅ ❌ labelled WIP
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 merge-conflict please-adopt blocked-by-other-PR ❌ ❌ ❌ ❌ ✅ ❌ blocked on another PR
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 merge-conflict awaiting-author ✅ ✅ ❌ ✅ ❌ ❌ merge conflict
19097 Vierkantor chore(Algebra.Polynomial): split `Polynomial/Basic.lean` into smaller files t-algebra merge-conflict blocked-by-other-PR ✅ ❌ ❌ ✅ ✅ ❌ blocked on another PR
18756 FR-vdash-bot refactor: deprecate `DistribMulActionSemiHomClass` `MulSemiringActionSemiHomClass` t-algebra merge-conflict ✅ ✅ ❌ ✅ ✅ ❌ merge conflict
17071 ScottCarnahan feat : (LinearAlgebra/RootSystem) : Separation, base, cartanMatrix t-algebra merge-conflict WIP ✅ ✅ ❌ ❌ ✅ ❌ labelled WIP
19281 Vierkantor chore(Algebra/{MonoidAlgebra,Polynomial}): algebra structure in `Basic.lean` t-algebra merge-conflict blocked-by-other-PR ✅ ❌ ❌ ✅ ✅ ❌ blocked on another PR
16391 vihdzp feat(SetTheory/Ordinal/NaturalOps): characterization of natural operations in base `ω` t-logic merge-conflict blocked-by-other-PR ❌ ❌ ❌ ✅ ✅ ❌ blocked on another PR
19125 yhtq feat: add theorems to transfer `IsGalois` between pairs of fraction rings new-contributor t-algebra merge-conflict ❌ ✅ ❌ ✅ ✅ ❌ failing CI
19046 j-loreaux feat: define class `SemigroupAction` t-algebra merge-conflict ✅ ✅ ❌ ✅ ✅ ❌ merge conflict
18841 hrmacbeth chore: change some `linarith`s to `linear_combination`s merge-conflict WIP ✅ ✅ ❌ ❌ ✅ ❌ labelled WIP
18748 FR-vdash-bot refactor: deprecate `ContinuousLinearMapClass` t-algebra t-topology merge-conflict ✅ ✅ ❌ ✅ ✅ ❌ merge conflict
8686 j-loreaux refactor: allow non-unital `AlgEquiv` t-algebra merge-conflict WIP ❌ ✅ ❌ ❌ ✅ ❌ labelled WIP
11142 hmonroe feat(ProofTheory): Define logical symbols abstractly; opens new top-level section, drawing from lean4-logic t-logic merge-conflict awaiting-author ✅ ✅ ❌ ✅ ❌ ❌ merge conflict
11210 hmonroe Test commit merge-conflict WIP ❌ ✅ ❌ ❌ ✅ ❌ labelled WIP
19621 Command-Master feat: Multiplicity and prime-adic valuation of derivations large-import t-algebra merge-conflict blocked-by-other-PR ✅ ❌ ❌ ✅ ✅ ❌ blocked on another PR
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 ❌ ❌ ❌ ❌ ✅ ❌ blocked on another PR
19699 vihdzp chore(SetTheory/Cardinal/Basic): tweak `#α = 0`, `#α = 1`, etc. lemmas t-set-theory awaiting-CI merge-conflict ❌ ✅ ❌ ✅ ❌ ❌ does not pass CI
15269 kkytola feat: Add ENNReal.floor t-order t-algebra merge-conflict awaiting-author blocked-by-other-PR ❌ ❌ ❌ ✅ ❌ ❌ blocked on another PR
15773 kkytola feat: Add type class for ENat-valued floor functions t-order merge-conflict awaiting-author ✅ ✅ ❌ ✅ ❌ ❌ merge conflict
3251 kmill feat: deriving `LinearOrder` for simple enough inductive types t-meta merge-conflict awaiting-author WIP ✅ ✅ ❌ ❌ ❌ ❌ labelled WIP
3610 TimothyGu feat: derive Infinite automatically for inductive types t-meta merge-conflict awaiting-author ✅ ✅ ❌ ✅ ❌ ❌ merge conflict
16120 awainverse feat(ModelTheory/Algebra/Ring/Basic): Ring homomorphisms are a `StrongHomClass` for the language of rings t-logic t-algebra RFC merge-conflict ❌ ✅ ❌ ✅ ✅ ❌ failing CI
15045 Command-Master fix(LinearAlgebra/Alternating/Basic): fix `MultilinearMap.alternatization` t-algebra merge-conflict awaiting-author ✅ ✅ ❌ ✅ ❌ ❌ 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 ❌ ❌ ❌ ❌ ✅ ❌ blocked on another PR
19462 joelriou feat(AlgebraicGeometry): étale sheafification t-algebraic-geometry merge-conflict blocked-by-other-PR WIP ❌ ❌ ❌ ❌ ✅ ❌ blocked on another PR
20527 trivial1711 refactor(Topology/UniformSpace/Completion): more descriptive names for `α → Completion α` t-topology merge-conflict ✅ ✅ ❌ ✅ ✅ ❌ merge conflict
17739 Aaron1011 feat(Topology/Order/DenselyOrdered): prove Not (IsOpen) for intervals new-contributor t-topology merge-conflict awaiting-author ✅ ✅ ❌ ✅ ❌ ❌ merge conflict
18474 FR-vdash-bot perf: lower the priority of `*WithOne.to*` instances t-data slow-typeclass-synthesis t-algebra merge-conflict ✅ ✅ ❌ ✅ ✅ ❌ merge conflict
20656 Komyyy feat(Mathlib/Geometry/Manifold/VectorBundle/Sphere): convert orthogonal smooth `M → 𝕊ⁿ` & `M → ℝⁿ⁺¹` to smooth `M → T𝕊ⁿ` t-differential-geometry merge-conflict please-adopt ✅ ✅ ❌ ❌ ✅ ❌ looking for help
19596 Command-Master feat(RingTheory/Valuation/PrimeMultiplicity): define `WithTop ℤ`-valued prime multiplicity on a fraction field large-import t-algebra merge-conflict awaiting-author ✅ ✅ ❌ ✅ ❌ ❌ merge conflict
19091 Vierkantor chore(Algebra/MonoidAlgebra): split Defs.lean further t-algebra merge-conflict ✅ ✅ ❌ ✅ ✅ ❌ merge conflict
15711 znssong feat(Combinatorics/SimpleGraph): Some lemmas about walk, cycle and Hamiltonian cycle new-contributor t-combinatorics merge-conflict awaiting-author ✅ ✅ ❌ ✅ ❌ ❌ merge conflict
15720 znssong feat(SimpleGraph): The Bondy-Chvátal theorem new-contributor t-combinatorics merge-conflict blocked-by-other-PR ✅ ❌ ❌ ✅ ✅ ❌ blocked on another PR
18629 tomaz1502 feat(Computability.Timed): Formalization of runtime complexity of List.merge t-computability new-contributor merge-conflict awaiting-author ✅ ✅ ❌ ✅ ❌ ❌ merge conflict
17246 pechersky feat(RingTheory/PrimaryDecomposition): PIR of Noetherian under jacobson condition t-algebra merge-conflict awaiting-author ❌ ✅ ❌ ✅ ❌ ❌ failing CI
8362 urkud feat(Asymptotics): define `ReflectsGrowth` t-analysis merge-conflict awaiting-author ❌ ✅ ❌ ✅ ❌ ❌ failing CI
6692 prakol16 feat: disjoint indexed union of local homeomorphisms t-topology merge-conflict awaiting-author ❌ ✅ ❌ ✅ ❌ ❌ failing CI
19291 PieterCuijpers feat(Algebra/Order/Hom): add quantale homomorphism new-contributor t-algebra merge-conflict awaiting-author ❌ ✅ ❌ ✅ ❌ ❌ failing CI
19352 hrmacbeth chore: change some `nlinarith`s to `linear_combination`s merge-conflict WIP ✅ ✅ ❌ ❌ ✅ ❌ labelled WIP
20372 jvlmdr feat(MeasureTheory/Function): Add ContinuousLinearMap.bilinearCompLp(L) new-contributor t-measure-probability merge-conflict ✅ ✅ ❌ ✅ ✅ ❌ merge conflict
17176 arulandu feat: integrals and integrability with .re new-contributor t-measure-probability merge-conflict awaiting-author ✅ ✅ ❌ ✅ ❌ ❌ merge conflict
20872 grunweg feat: lint against the tactic.skipAssignedInstances option in mathlib tech debt t-linter merge-conflict awaiting-author ✅ ✅ ❌ ✅ ❌ ❌ merge conflict
2605 eric-wieser chore: better error message in linarith t-meta merge-conflict awaiting-author ✅ ✅ ❌ ✅ ❌ ❌ merge conflict
3171 eric-wieser refactor: make the algebra hierarchy use flat structures merge-conflict WIP ✅ ✅ ❌ ❌ ✅ ❌ labelled WIP
11837 trivial1711 feat: completion of a uniform multiplicative group t-algebra t-topology merge-conflict WIP help-wanted ❌ ✅ ❌ ❌ ✅ ❌ looking for help
12670 trivial1711 feat: completion of a nonarchimedean multiplicative group t-algebra t-topology merge-conflict blocked-by-other-PR ❌ ❌ ❌ ✅ ✅ ❌ blocked on another PR
14799 luigi-massacci feat(Analysis/MeanInequalities): Weighted QM-AM inequality new-contributor t-analysis easy merge-conflict awaiting-author ✅ ✅ ❌ ✅ ❌ ❌ merge conflict
12294 AntoineChambert-Loir feat(Mathlib.RingTheory.TensorProduct.Polynomial) : tensor product of a (univariate) polynomial ring t-algebra merge-conflict WIP ❌ ✅ ❌ ❌ ✅ ❌ labelled WIP
14686 smorel394 feat (AlgebraicGeometry/Grassmannian): define the Grassmannian scheme workshop-AIM-AG-2024 t-algebraic-geometry merge-conflict please-adopt WIP ✅ ✅ ❌ ❌ ✅ ❌ looking for help
9449 hmonroe feat: Add Turing machine with the quintet definition (TMQ) and a chainable step function for each TM type t-computability merge-conflict awaiting-author ❌ ✅ ❌ ✅ ❌ ❌ failing CI
20663 EtienneC30 feat: `PFunLike` typeclass for partial homomorphisms and `LinearPMapClass` t-data t-algebra merge-conflict WIP ✅ ✅ ❌ ❌ ✅ ❌ labelled WIP
21474 erdOne feat(RingTheory): replace `Ring.DimensionLEOne` with `Ring.KrullDimLE` large-import t-algebra merge-conflict ❌ ✅ ❌ ✅ ✅ ❌ failing CI
19697 quangvdao feat(BigOperators/Fin): Sum/product over `Fin` intervals t-data merge-conflict awaiting-author ❌ ✅ ❌ ✅ ❌ ❌ failing CI
19353 hrmacbeth chore: golf some term/rw proofs using `linear_combination` merge-conflict WIP ✅ ✅ ❌ ❌ ✅ ❌ labelled WIP
20248 peabrainiac feat(Topology/Compactness): first-countable locally path-connected spaces are delta-generated large-import new-contributor t-topology merge-conflict awaiting-author blocked-by-other-PR ✅ ❌ ❌ ✅ ❌ ❌ blocked on another PR
10678 adri326 feat(Topology/UniformSpace): prove that a uniform space is completely regular t-topology merge-conflict awaiting-author ✅ ✅ ❌ ✅ ❌ ❌ merge conflict
20431 erdOne feat(RingTheory/AdicCompletion): monotonicity of adic-completeness t-algebra merge-conflict awaiting-author ✅ ✅ ❌ ✅ ❌ ❌ merge conflict
18785 erdOne feat(CategoryTheory): command that generates instances for `MorphismProperty` t-category-theory t-meta merge-conflict awaiting-author ✅ ✅ ❌ ✅ ❌ ❌ merge conflict
15942 grunweg chore: move style linters into their own file; document all current linters t-linter merge-conflict awaiting-author ✅ ✅ ❌ ✅ ❌ ❌ merge conflict
16311 madvorak feat(Computability): regular languages are context-free t-computability merge-conflict WIP ❌ ✅ ❌ ❌ ✅ ❌ labelled WIP
19943 AlexLoitzl feat(Computability): Add Chomsky Normal Form Grammar and translation t-computability new-contributor merge-conflict awaiting-author ✅ ✅ ❌ ✅ ❌ ❌ merge conflict
19616 adamtopaz fix: Fix the definition of the absolute Galois group of a field t-algebra t-number-theory merge-conflict awaiting-author ✅ ✅ ❌ ✅ ❌ ❌ merge conflict
21761 JovanGerb feat(Algebra): add lemmas `mul_self` and `add_self` t-algebra merge-conflict delegated ❌ ✅ ❌ ✅ ✅ ❌ failing CI
17005 YnirPaz feat(SetTheory/Cardinal/Regular): define singular cardinals t-set-theory merge-conflict WIP ✅ ✅ ❌ ❌ ✅ ❌ labelled WIP
18206 vihdzp chore(SetTheory/Ordinal/Basic): golf/clean up `Cardinal.ord` theorems t-set-theory merge-conflict awaiting-author ✅ ✅ ❌ ✅ ❌ ❌ merge conflict
18463 vihdzp feat(SetTheory/Ordinal/Notation/FundamentalSequence): define type of fundamental sequences t-set-theory t-order merge-conflict ✅ ✅ ❌ ✅ ✅ ❌ merge conflict
10541 Louddy feat(Algebra/SkewMonoidAlgebra/Basic): add SkewMonoidAlgebra new-contributor t-algebra merge-conflict blocked-by-other-PR WIP ✅ ❌ ❌ ❌ ✅ ❌ blocked on another PR
12054 adomani feat: auto-bugs t-meta merge-conflict awaiting-author ✅ ✅ ❌ ✅ ❌ ❌ merge conflict
5062 adomani feat(Tactic/Prune + test/Prune): add `prune` tactic, for removing unnecessary hypotheses t-meta merge-conflict modifies-tactic-syntax awaiting-author ✅ ✅ ❌ ✅ ❌ ❌ merge conflict
21914 vasnesterov Test PR for `order` large-import merge-conflict WIP ❌ ✅ ❌ ❌ ✅ ❌ labelled WIP
16705 iehality feat(Computability): r.e. sets are closed under inter/union/projection/composition t-computability merge-conflict awaiting-author ✅ ✅ ❌ ✅ ❌ ❌ merge conflict
21433 grunweg chore: change more lemmas to be about enorm instead of nnnorm carleson t-measure-probability merge-conflict awaiting-author ✅ ✅ ❌ ✅ ❌ ❌ merge conflict
21099 chrisflav chore(RingTheory/Generators): use unification hints for variables and relations t-algebra merge-conflict ✅ ✅ ❌ ✅ ✅ ❌ merge conflict
21269 CharredLee (WIP) feat (CategoryTheory/Topos): Add topos theory content new-contributor t-category-theory merge-conflict awaiting-author WIP ✅ ✅ ❌ ❌ ❌ ❌ labelled WIP
12394 JADekker feat : define pre-tight and tight measures t-measure-probability merge-conflict please-adopt awaiting-author ❌ ✅ ❌ ❌ ❌ ❌ looking for help
22245 Champitoad feat(CategoryTheory/Subobject): add formalization of subobject classifier new-contributor t-category-theory merge-conflict awaiting-author ✅ ✅ ❌ ✅ ❌ ❌ merge conflict
20454 urkud chore(TangentCone): review names t-analysis merge-conflict ❌ ✅ ❌ ✅ ✅ ❌ failing CI
14760 FR-vdash-bot feat: define `IGame` t-logic merge-conflict WIP ❌ ✅ ❌ ❌ ✅ ❌ labelled WIP
16550 awainverse feat(ModelTheory): A typeclass for languages expanding other languages t-logic merge-conflict awaiting-author ✅ ✅ ❌ ✅ ❌ ❌ merge conflict
13686 fpvandoorn feat: some finset lemmas t-data merge-conflict awaiting-author ✅ ✅ ❌ ✅ ❌ ❌ merge conflict
14313 grhkm21 feat(RepresentationTheory/FdRep): FdRep is a full subcategory of Rep new-contributor t-algebra t-category-theory merge-conflict ❌ ✅ ❌ ✅ ✅ ❌ failing CI
18626 hannahfechtner feat : define Artin braid groups new-contributor t-algebra merge-conflict awaiting-author ✅ ✅ ❌ ✅ ❌ ❌ merge conflict
10823 alexkeizer feat: convert curried type functions into uncurried type functions t-data merge-conflict awaiting-author ✅ ✅ ❌ ✅ ❌ ❌ merge conflict
13648 urkud feat(Topology/Module): generalize `ContinuousLinearMap.compSL` t-algebra t-analysis t-topology merge-conflict awaiting-author ❌ ✅ ❌ ✅ ❌ ❌ failing CI
21339 vihdzp fix(Data/List/Lex): remove duplicate `List.LE` instance t-data merge-conflict ✅ ✅ ❌ ✅ ✅ ❌ merge conflict
11212 shuxuezhuyi feat(GroupTheory/GroupAction): instance `MulAction (β ⧸ H) α` large-import t-algebra merge-conflict awaiting-author ✅ ✅ ❌ ✅ ❌ ❌ merge conflict
14060 YnirPaz feat(SetTheory/Ordinal/Clubs): define club sets and prove basic properties new-contributor t-logic merge-conflict blocked-by-other-PR ✅ ❌ ❌ ✅ ✅ ❌ blocked on another PR
16837 vihdzp feat(Data/List/SplitBy): characterization of `List.splitBy` t-data merge-conflict awaiting-author ✅ ✅ ❌ ✅ ❌ ❌ merge conflict
16421 FR-vdash-bot feat: `QuotLike` t-data RFC merge-conflict awaiting-author ✅ ✅ ❌ ✅ ❌ ❌ merge conflict
17105 vihdzp feat(Data/List/RunLength): run-length encoding t-data merge-conflict blocked-by-other-PR ❌ ❌ ❌ ✅ ✅ ❌ blocked on another PR
19700 vihdzp chore(SetTheory/Ordinal/Basic): tweak `type r = 0`, `type r = 1`, etc. lemmas t-set-theory awaiting-CI merge-conflict ❌ ✅ ❌ ✅ ❌ ❌ does not pass CI
22340 sinhp feat(CategoryTheory): Locally Cartesian Closed Categories (Beck-Chevalley Conditions) large-import t-category-theory merge-conflict blocked-by-other-PR WIP ✅ ❌ ❌ ❌ ✅ ❌ blocked on another PR
21959 BGuillemet feat(Topology/ContinuousMap): Stone-Weierstrass theorem for MvPolynomial new-contributor t-topology merge-conflict ✅ ✅ ❌ ✅ ✅ ❌ merge conflict
20750 adomani feat: the envLinter syntax linter large-import t-linter merge-conflict ❌ ✅ ❌ ✅ ✅ ❌ failing CI
20267 joelriou feat(CategoryTheory): comma categories are accessible t-category-theory merge-conflict awaiting-author blocked-by-other-PR WIP ❌ ❌ ❌ ❌ ❌ ❌ blocked on another PR
18470 FR-vdash-bot perf: lower the priority of `Normed*.to*` instances slow-typeclass-synthesis t-algebra t-analysis merge-conflict ❌? ✅ ❌ ✅ ✅ ❌ infrastructure-related CI failing
16944 YnirPaz feat(SetTheory/Cardinal/Cofinality): lemmas about limit ordinals and cofinality t-set-theory merge-conflict WIP ✅ ✅ ❌ ❌ ✅ ❌ labelled WIP
17368 Felix-Weilacher feat(Topology/Baire/BaireMeasurable): add the Kuratowski-Ulam theorem t-topology merge-conflict ❌ ✅ ❌ ✅ ✅ ❌ failing CI
8767 eric-wieser refactor(Cache): tidy lake-manifest parsing in Cache t-meta merge-conflict ❌ ✅ ❌ ✅ ✅ ❌ failing CI
15578 znssong feat(Function): Fixed points of function `f` with `f(x) >= x` new-contributor t-analysis merge-conflict awaiting-author ✅ ✅ ❌ ✅ ❌ ❌ merge conflict
8793 101damnations feat(RepresentationTheory/GroupCohomology/Hilbert90): add Hilbert's original theorem 90 t-algebra merge-conflict awaiting-author ❌ ✅ ❌ ✅ ❌ ❌ failing CI
22517 j-loreaux feat: `ℕ+` powers in semigroups large-import merge-conflict WIP ✅ ✅ ❌ ❌ ✅ ❌ ⚠️ labelled WIP
22805 ScottCarnahan feat (FieldTheory/Finite): fixed points of frobenius t-algebra merge-conflict WIP ✅ ✅ ❌ ❌ ✅ ❌ labelled WIP
22660 Ruben-VandeVelde chore: follow naming convention around Group.IsNilpotent t-algebra merge-conflict ✅ ✅ ❌ ✅ ✅ ❌ merge conflict
20424 erdOne feat(RingTheory): evaluation of power series t-algebra merge-conflict ❌ ✅ ❌ ✅ ✅ ❌ failing CI
13999 adomani feat: a linter to flag potential confusing conventions t-linter merge-conflict awaiting-author ✅ ✅ ❌ ✅ ❌ ❌ merge conflict
15991 vihdzp feat(SetTheory/Ordinal/CantorNormalForm): alternate CNF recursion principle t-set-theory t-logic merge-conflict awaiting-author ✅ ✅ ❌ ✅ ❌ ❌ merge conflict
17758 vihdzp feat(SetTheory/Ordinal/ENat): `Ordinal.toENat` t-set-theory merge-conflict ❌ ✅ ❌ ✅ ✅ ❌ failing CI
21856 vihdzp chore(SetTheory/Cardinal/Basic): generalize universes of `sum_le_iSup_lift` t-set-theory merge-conflict ✅ ✅ ❌ ✅ ✅ ❌ merge conflict
19013 quangvdao feat(Algebra/BigOperators/Fin): Add `finSigmaFinEquiv` t-algebra merge-conflict awaiting-author ✅ ✅ ❌ ✅ ❌ ❌ merge conflict
20410 vihdzp refactor: redefine `Equiv.Set.sumCompl = Equiv.sumCompl` t-data awaiting-CI merge-conflict blocked-by-other-PR WIP ❌ ❌ ❌ ❌ ❌ ❌ blocked on another PR
20850 vihdzp chore(Logic/Equiv/Basic): extend `sumCompl` API t-data t-logic merge-conflict awaiting-author ✅ ✅ ❌ ✅ ❌ ❌ merge conflict
15915 vihdzp chore(SetTheory/Ordinal/CantorNormalForm): `CNF.exponents` and `CNF.coeffs` t-set-theory t-logic merge-conflict awaiting-author ✅ ✅ ❌ ✅ ❌ ❌ merge conflict
19189 YnirPaz feat(SetTheory/Ordinal/Arithmetic): order isomorphism between omega and the natural numbers t-set-theory merge-conflict awaiting-author ✅ ✅ ❌ ✅ ❌ ❌ merge conflict
23145 joneugster feat(CategoryTheory/Enriched/Limits): add IsConicalLimits infinity-cosmos t-category-theory merge-conflict blocked-by-other-PR ❌ ❌ ❌ ✅ ✅ ❌ blocked on another PR
19227 adomani fix(CI): unwrap `lake test` in problem matcher CI merge-conflict awaiting-author ✅ ✅ ❌ ✅ ❌ ❌ merge conflict
20874 grunweg chore(nolint.yml): use shallow clones CI merge-conflict awaiting-author ✅ ✅ ❌ ✅ ❌ ❌ merge conflict
21463 riccardobrasca add algEquiv_comp_algebraMap large-import t-algebra t-number-theory merge-conflict WIP ❌ ✅ ❌ ❌ ✅ ❌ labelled WIP
15774 kkytola feat: Topology on `ENat` t-order t-topology merge-conflict WIP ✅ ✅ ❌ ❌ ✅ ❌ labelled WIP
18284 chrisflav feat(AlgebraicGeometry): relative gluing of schemes t-algebraic-geometry merge-conflict WIP ❌ ✅ ❌ ❌ ✅ ❌ labelled WIP
20613 grunweg chore: golf using `List.toArrayMap` large-import merge-conflict ❌ ✅ ❌ ✅ ✅ ❌ failing CI
20222 eric-wieser feat: generalize lemmas about derivatives t-analysis merge-conflict blocked-by-other-PR ❌ ❌ ❌ ✅ ✅ ❌ blocked on another PR
15989 vihdzp feat(SetTheory/Ordinal/Principal): golf theorems on additively principal ordinals t-set-theory t-logic merge-conflict awaiting-author ✅ ✅ ❌ ✅ ❌ ❌ merge conflict
22682 grunweg chore(Topology/Homeomorph): split out various constructions tech debt t-topology RFC merge-conflict ❌ ✅ ❌ ✅ ✅ ❌ failing CI
21018 markimunro feat(Data/Matrix): add file with key definitions and theorems about elementary row operations t-data new-contributor merge-conflict awaiting-author enhancement ❌ ✅ ❌ ✅ ❌ ❌ failing CI
23514 eric-wieser refactor: smooth over Lattice/LinearOrder inheritance merge-conflict ❌ ✅ ❌ ✅ ✅ ❌ failing CI
19907 kim-em chore: remove some 'nonrec' t-algebra merge-conflict ❌ ✅ ❌ ✅ ✅ ❌ failing CI
22810 pechersky feat(Counterexamples): metric space not induced by norm t-analysis t-topology merge-conflict WIP ✅ ✅ ❌ ❌ ✅ ❌ labelled WIP
13124 FR-vdash-bot chore: remove `CovariantClass` and `ContravariantClass` merge-conflict WIP ❌ ✅ ❌ ❌ ✅ ❌ labelled WIP
20401 RemyDegenne feat: add sigmaFinite_iUnion t-measure-probability merge-conflict awaiting-author ✅ ✅ ❌ ✅ ❌ ❌ merge conflict
19275 eric-wieser fix: if nolint files change, do a full rebuild merge-conflict delegated ❌ ✅ ❌ ✅ ✅ ❌ failing CI
23499 riccardobrasca feat: add `RingTheory.MvPowerSeries.rename` t-algebra merge-conflict WIP ✅ ✅ ❌ ❌ ✅ ❌ labelled WIP
12251 ScottCarnahan refactor(RingTheory/HahnSeries) : several generalizations t-order t-algebra merge-conflict WIP ✅ ✅ ❌ ❌ ✅ ❌ labelled WIP
21769 JovanGerb feat: extensible `push_neg` tactic large-import t-meta merge-conflict blocked-by-other-PR ✅ ❌ ❌ ✅ ✅ ❌ blocked on another PR
22727 grunweg feat: rewrite the isolated by and colon linters in Lean t-linter merge-conflict awaiting-author ✅ ✅ ❌ ✅ ❌ ❌ merge conflict
22027 vihdzp chore(SetTheory/Ordinal/FixedPoint); review `Ordinal.nfp` API t-set-theory merge-conflict ✅ ✅ ❌ ✅ ✅ ❌ merge conflict
15212 victorliu5296 feat: Add fundamental theorem of calculus-2 for Banach spaces new-contributor t-measure-probability t-analysis merge-conflict awaiting-author ✅ ✅ ❌ ✅ ❌ ❌ merge conflict
22701 ctchou feat(Combinatorics): the Katona circle method new-contributor t-combinatorics merge-conflict ✅ ✅ ❌ ✅ ✅ ❌ merge conflict
23786 grunweg Mr librarynote def 2b large-import merge-conflict WIP ❌ ✅ ❌ ❌ ✅ ❌ labelled WIP
23411 PatrickMassot chore: remove finiteness from Order.Filter.Lift longest-pole t-topology merge-conflict ✅ ✅ ❌ ✅ ✅ ❌ merge conflict
22579 kvanvels doc(Topology/Defs/Induced): fix comments on three functions related to RestrictGenTopology t-topology merge-conflict awaiting-author documentation ✅ ✅ ❌ ✅ ❌ ❌ merge conflict
21488 imbrem feat(CategoryTheory/Monoidal): premonoidal categories new-contributor t-category-theory merge-conflict ✅ ✅ ❌ ✅ ✅ ❌ merge conflict
21525 sinhp feat(CategoryTheory): Locally Cartesian Closed Categories (Prelim) large-import t-category-theory merge-conflict ✅ ✅ ❌ ✅ ✅ ❌ merge conflict
22321 sinhp feat(CategoryTheory): Locally Cartesian Closed Categories (Definition) large-import t-category-theory merge-conflict blocked-by-other-PR ✅ ❌ ❌ ✅ ✅ ❌ blocked on another PR
22319 sinhp feat(CategoryTheory): Locally Cartesian Closed Categories (Sections Right Adjoint) large-import t-category-theory merge-conflict blocked-by-other-PR ✅ ❌ ❌ ✅ ✅ ❌ blocked on another PR
19425 hrmacbeth perf: gcongr forward-reasoning adjustment merge-conflict awaiting-author ✅ ✅ ❌ ✅ ❌ ❌ merge conflict
20873 vbeffara feat(Topology/Covering): path lifting and homotopy lifting new-contributor t-topology merge-conflict awaiting-author ❌ ✅ ❌ ✅ ❌ ❌ failing CI
22817 peabrainiac feat(CategoryTheory/Sites): local sites t-category-theory merge-conflict WIP ✅ ✅ ❌ ❌ ✅ ❌ labelled WIP
6252 michaellee94 feat(Geometry/Manifolds/Instances/Homeomorph): Homeomorphism maps `C^k` manifolds to `C^k` manifolds t-differential-geometry merge-conflict WIP ✅ ✅ ❌ ❌ ✅ ❌ labelled WIP
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 ✅ ❌ ❌ ✅ ✅ ❌ blocked on another PR
23867 kim-em chore: remove unnecessary `[AtLeastTwo n]` hypotheses bench-after-CI merge-conflict ❌ ✅ ❌ ✅ ✅ ❌ failing CI
16314 FR-vdash-bot chore(Data/Quot): deprecate `ind*'` APIs t-data merge-conflict ✅ ✅ ❌ ✅ ✅ ❌ merge conflict
13795 FR-vdash-bot perf(Algebra/{Group, GroupWithZero, Ring}/InjSurj): reduce everything t-algebra merge-conflict ✅ ✅ ❌ ✅ ✅ ❌ merge conflict
23509 eric-wieser refactor: Make ENNReal an abbrev t-data merge-conflict ❌ ✅ ❌ ✅ ✅ ❌ failing CI
11455 adomani fix: unsqueeze simp, re Yaël's comments on #11259 merge-conflict awaiting-author ✅ ✅ ❌ ✅ ❌ ❌ merge conflict
8453 FR-vdash-bot chore(MeasureTheory): Golf, speed up t-measure-probability merge-conflict ❌ ✅ ❌ ✅ ✅ ❌ failing CI
7325 eric-wieser chore: use preimageIso instead of defeq abuse for InducedCategory t-category-theory awaiting-CI merge-conflict ✅ ✅ ❌ ✅ ❌ ❌ does not pass CI
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 ❌ ✅ ❌ ✅ ❌ ❌ does not pass CI
5952 eric-wieser feat: add Qq wrappers for ToExpr awaiting-CI t-meta merge-conflict ❌ ✅ ❌ ✅ ❌ ❌ does not pass CI
15483 FR-vdash-bot chore(GroupTheory/Coset): reduce defeq abuse t-algebra merge-conflict ✅ ✅ ❌ ✅ ✅ ❌ merge conflict
16594 FR-vdash-bot perf: reorder `extends` and remove some instances in algebra hierarchy slow-typeclass-synthesis t-algebra merge-conflict ❌ ✅ ❌ ✅ ✅ ❌ failing CI
12673 grunweg feat: add ContDiff.lipschitzOnWith t-analysis merge-conflict awaiting-author help-wanted ✅ ✅ ❌ ❌ ❌ ❌ looking for help
21238 joneugster feat(Cache): enable partial cache in downstream projects CI t-meta merge-conflict blocked-by-other-PR ✅ ❌ ❌ ✅ ✅ ❌ blocked on another PR
21842 joneugster refactor(Cache): use module name for file hash instead of non-resolved file path CI t-meta merge-conflict blocked-by-other-PR ✅ ❌ ❌ ✅ ✅ ❌ blocked on another PR
19467 quangvdao feat(MvPolynomial/Equiv): Add `MvPolynomial.finSuccEquivNth` t-algebra merge-conflict blocked-by-other-PR ✅ ❌ ❌ ✅ ✅ ❌ blocked on another PR
20567 grunweg feat(Cache): two small features t-meta merge-conflict ✅ ✅ ❌ ✅ ✅ ❌ merge conflict
20313 thefundamentaltheor3m feat(Data/Complex/Exponential): prove some useful results about the complex exponential. new-contributor t-analysis merge-conflict ❌ ✅ ❌ ✅ ✅ ❌ failing CI
22147 smmercuri feat: collections of distinct infinite places contain values that diverge around 1 large-import t-algebra t-analysis merge-conflict blocked-by-other-PR ✅ ❌ ❌ ✅ ✅ ❌ blocked on another PR
22698 Kiolt feat: notation for whisker(Left/Right)Iso toric t-category-theory merge-conflict ❌ ✅ ❌ ✅ ✅ ❌ failing CI
20730 kuotsanhsu feat(LinearAlgebra/Matrix/SchurTriangulation): prove Schur decomposition/triangulation new-contributor t-algebra merge-conflict awaiting-author ❌ ✅ ❌ ✅ ❌ ❌ failing CI
19117 eric-wieser feat: derivatives of matrix operations t-analysis merge-conflict WIP ❌ ✅ ❌ ❌ ✅ ❌ labelled WIP
12605 FR-vdash-bot chore: attribute [induction_eliminator] merge-conflict awaiting-author ✅ ✅ ❌ ✅ ❌ ❌ merge conflict
23916 Vierkantor chore: upstream shake from Mathlib to Batteries t-linter blocked-by-batt-PR merge-conflict blocked-by-other-PR ✅ ❌ ❌ ✅ ✅ ❌ blocked on another PR
15099 joelriou feat(CategoryTheory/Sites): the Mayer-Vietoris long exact sequence in sheaf cohomology t-category-theory merge-conflict WIP ❌ ✅ ❌ ❌ ✅ ❌ labelled WIP
23859 urkud feat(Topology/../Order/Field): generalize to `Semifield` t-topology merge-conflict ✅ ✅ ❌ ✅ ✅ ❌ merge conflict
22908 AntoineChambert-Loir feat(RingTheory/Finiteness/Small): tensor product of the system of small submodules t-algebra merge-conflict blocked-by-other-PR ✅ ❌ ❌ ✅ ✅ ❌ blocked on another PR
23810 b-reinke chore(Order/Interval): generalize succ/pred lemmas to partial orders t-order merge-conflict ✅ ✅ ❌ ✅ ✅ ❌ merge conflict
24285 madvorak chore(Algebra/*-{Category,Homology}): remove unnecessary universe variables t-algebra merge-conflict ✅ ✅ ❌ ✅ ✅ ❌ merge conflict
8370 eric-wieser refactor(Analysis/NormedSpace/Exponential): remove the `𝕂` argument from `exp` awaiting-zulip t-analysis merge-conflict ❌ ✅ ❌ ✅ ❌ ❌ failing CI
23621 FR-vdash-bot chore: deprecate `LinearOrderedComm{Monoid, Group}WithZero` t-order t-algebra merge-conflict ✅ ✅ ❌ ✅ ✅ ❌ merge conflict
22583 imathwy feat: affinespace homeomorphism t-algebra merge-conflict awaiting-author ❌ ✅ ❌ ✅ ❌ ❌ failing CI
24322 mattrobball chore: merge repeated `Type*` binders merge-conflict awaiting-author ❌ ✅ ❌ ✅ ❌ ❌ failing CI
23138 grunweg feat: (unoriented) bordism groups t-differential-geometry merge-conflict WIP ❌ ✅ ❌ ❌ ✅ ❌ labelled WIP
23593 erdOne feat(AlgebraicGeometry): the tilde construction is functorial t-algebraic-geometry merge-conflict awaiting-author ✅ ✅ ❌ ✅ ❌ ❌ merge conflict
21065 eric-wieser feat: generalize `tangentConeAt.lim_zero` to TVS t-analysis merge-conflict WIP ✅ ✅ ❌ ❌ ✅ ❌ labelled WIP
22721 grunweg chore(MeasureTheory/Function/LpSeminorm/Basic): generalise more results to enorm classes carleson t-measure-probability merge-conflict WIP ❌ ✅ ❌ ❌ ✅ ❌ labelled WIP
24354 grunweg chore(HasFiniteIntegral): rename three lemmas t-measure-probability merge-conflict ✅ ✅ ❌ ✅ ✅ ❌ merge conflict
14731 adomani feat: the repeated typeclass assumption linter large-import t-linter merge-conflict WIP ❌ ✅ ❌ ❌ ✅ ❌ labelled WIP
13649 FR-vdash-bot chore: redefine `Nat.div2` `Nat.bodd` merge-conflict ✅ ✅ ❌ ✅ ✅ ❌ merge conflict
23635 FLDutchmann feat(NumberTheory/SelbergSieve): define Selberg's weights and prove basic results. t-analysis t-number-theory merge-conflict blocked-by-other-PR ✅ ❌ ❌ ✅ ✅ ❌ blocked on another PR
24549 grunweg feat: define embedded submanifolds, attempt 1 t-differential-geometry merge-conflict blocked-by-other-PR WIP ❌ ❌ ❌ ❌ ✅ ❌ blocked on another PR
19520 erdOne refactor(Algebra/Module): Redefine `LocalizedModule` in terms of `OreLocalization` t-algebra merge-conflict ❌ ✅ ❌ ✅ ✅ ❌ failing CI
14675 adomani dev: the repeated variable linter t-linter merge-conflict WIP ❌ ✅ ❌ ❌ ✅ ❌ labelled WIP
14330 Ruben-VandeVelde chore: split Mathlib.Algebra.Star.Basic merge-conflict awaiting-author ✅ ✅ ❌ ✅ ❌ ❌ merge conflict
14023 mattrobball perf(RingTheory.OreLocalization): make data irreducible merge-conflict ✅ ✅ ❌ ✅ ✅ ❌ merge conflict
8511 eric-wieser refactor(MeasureTheory/Measure/Haar/Basic): partially generalize to the affine case t-measure-probability merge-conflict awaiting-author ✅ ✅ ❌ ✅ ❌ ❌ merge conflict
7994 ericrbg chore: generalize `LieSubalgebra.mem_map_submodule` t-algebra merge-conflict please-adopt ✅ ✅ ❌ ❌ ✅ ❌ looking for help
6317 eric-wieser refactor(Data/Finsupp/Defs): make Finsupp.single defeq to Pi.single t-data merge-conflict WIP ✅ ✅ ❌ ❌ ✅ ❌ labelled WIP
4979 mhk119 doc(Data/Nat/Bitblast): initial commit t-data merge-conflict ✅ ✅ ❌ ✅ ✅ ❌ merge conflict
11524 mcdoll refactor: Introduce type-class for SchwartzMap t-analysis merge-conflict WIP ❌ ✅ ❌ ❌ ✅ ❌ labelled WIP
11003 thorimur chore: migrate to `tfae` block tactic t-meta merge-conflict blocked-by-other-PR WIP ✅ ❌ ❌ ❌ ✅ ❌ blocked on another PR
16186 joneugster chore: use emoji-variant-selector `\uFE0F` for emojis ✅️,❌️,💥️,🟡️ t-linter merge-conflict awaiting-author blocked-by-other-PR ❌ ❌ ❌ ✅ ❌ ❌ blocked on another PR
22269 Thmoas-Guan chore(Algebra): replace Submodule.quotient.mk with Submodule.mkQ t-algebra merge-conflict awaiting-author ✅ ✅ ❌ ✅ ❌ ❌ merge conflict
23546 JovanGerb feat(LinearAlgebra/AffineSpace/AffineSubspace): rename `AffineSubspace.mk'` to `Submodule.shift` t-euclidean-geometry merge-conflict ✅ ✅ ❌ ✅ ✅ ❌ merge conflict
21853 smmercuri feat: the adele ring of a number field is locally compact large-import t-number-theory merge-conflict blocked-by-other-PR WIP ❌ ❌ ❌ ❌ ✅ ❌ blocked on another PR
15654 TpmKranz feat(Computability): language-preserving maps between NFA and RE awaiting-zulip t-computability new-contributor merge-conflict blocked-by-other-PR ✅ ❌ ❌ ✅ ❌ ❌ blocked on another PR
19315 quangvdao feat(Data/Finsupp/Fin): Add `Finsupp` operations on `Fin` tuple t-data merge-conflict awaiting-author ✅ ✅ ❌ ✅ ❌ ❌ merge conflict
7907 urkud feat: introduce `NthRoot` notation class t-algebra t-analysis awaiting-CI merge-conflict ❌ ✅ ❌ ✅ ❌ ❌ does not pass CI
9273 grunweg feat: extended charts are local diffeomorphisms on their source t-differential-geometry merge-conflict ✅ ✅ ❌ ✅ ✅ ❌ merge conflict
24550 grunweg feat: define `SliceModel` typeclass for models with corners for embedded submanifolds t-differential-geometry merge-conflict blocked-by-other-PR WIP ❌ ❌ ❌ ❌ ✅ ❌ blocked on another PR
18755 FR-vdash-bot refactor: deprecate `LinearIsometryClass` t-algebra t-analysis merge-conflict blocked-by-other-PR ✅ ❌ ❌ ✅ ✅ ❌ blocked on another PR
24642 grunweg WIP-feat: add layercake formula for ENNReal-valued functions carleson t-analysis merge-conflict WIP ❌ ✅ ❌ ❌ ✅ ❌ labelled WIP
21712 grunweg chore: generalise more lemmas to `ContinuousENorm` carleson t-measure-probability awaiting-CI merge-conflict ❌ ✅ ❌ ✅ ❌ ❌ does not pass CI
21375 grunweg WIP: generalise lemmas to ENorm carleson t-measure-probability awaiting-CI merge-conflict WIP ❌ ✅ ❌ ❌ ❌ ❌ labelled WIP
21847 smmercuri feat: `v.adicCompletionIntegers K` is compact large-import t-number-theory merge-conflict blocked-by-other-PR WIP ❌ ❌ ❌ ❌ ✅ ❌ blocked on another PR
24853 smmercuri feat: dimensions of completions at infinite place extensions large-import FLT merge-conflict blocked-by-other-PR ✅ ❌ ❌ ✅ ✅ ❌ ⚠️ blocked on another PR
13685 niklasmohrin feat(Combinatorics): add definitions for network flows new-contributor t-combinatorics merge-conflict awaiting-author ✅ ✅ ❌ ✅ ❌ ❌ merge conflict
24208 ADedecker chore: semilinearize LinearAlgebra.TensorProduct.Basic t-algebra merge-conflict WIP ❌ ✅ ❌ ❌ ✅ ❌ labelled WIP
15115 kkytola feat: Generalize assumptions in liminf and limsup results in ENNReals t-order t-topology merge-conflict awaiting-author help-wanted ✅ ✅ ❌ ❌ ❌ ❌ looking for help
17129 joneugster feat(Tactic/Linter): add unicode linter for unicode variant-selectors large-import t-linter merge-conflict delegated awaiting-author ❌ ✅ ❌ ✅ ❌ ❌ failing CI
17131 joneugster feat(Tactic/Linter): add unicode linter for unwanted characters large-import t-linter merge-conflict awaiting-author ✅ ✅ ❌ ✅ ❌ ❌ merge conflict
24590 smmercuri chore: make `Valuation.Completion` a `def` and refactor more of `AdicValuation.lean` FLT merge-conflict ✅ ✅ ❌ ✅ ✅ ❌ merge conflict
15651 TpmKranz feat(Computability/NFA): operations for Thompson's construction awaiting-zulip t-computability new-contributor merge-conflict awaiting-author ✅ ✅ ❌ ✅ ❌ ❌ awaiting a zulip discussion
22361 rudynicolop feat(Computability/NFA): nfa closure properties awaiting-zulip t-computability new-contributor merge-conflict awaiting-author ✅ ✅ ❌ ✅ ❌ ❌ awaiting a zulip discussion
24245 JovanGerb feat(Geometry/Euclidean/SignedDist): `signedDist` between two points t-euclidean-geometry merge-conflict ✅ ✅ ❌ ✅ ✅ ❌ merge conflict
25006 jano-wol feat: invariant dual submodules define Lie ideals t-algebra merge-conflict awaiting-author ✅ ✅ ❌ ✅ ❌ ❌ merge conflict
22837 joneugster feat(Data/Set/Basic): add subset_iff and not_mem_subset_iff t-set-theory t-data merge-conflict ✅ ✅ ❌ ✅ ✅ ❌ merge conflict
24100 eric-wieser feat: restore some explicit binders from Lean 3 tech debt merge-conflict awaiting-author ❌ ✅ ❌ ✅ ❌ ❌ ⚠️ failing CI
25143 chrisflav feat(RingTheory): smooth algebras have smooth Noetherian models t-algebra merge-conflict blocked-by-other-PR ✅ ❌ ❌ ✅ ✅ ❌ blocked on another PR
21476 grunweg feat(lint-style): enable running on downstream projects t-linter merge-conflict ✅ ✅ ❌ ✅ ✅ ❌ merge conflict
21844 smmercuri feat: the ring of integers of a `ℤₘ₀`-valued field is compact whenever it is a DVR and the residue field is finite large-import t-algebra merge-conflict blocked-by-other-PR ✅ ❌ ❌ ✅ ✅ ❌ blocked on another PR
23349 BGuillemet feat: add LocallyLipschitzOn.lipschitzOnWith_of_isCompact and two small lemmas about Lipschitz functions large-import new-contributor t-topology merge-conflict ✅ ✅ ❌ ✅ ✅ ❌ merge conflict
23767 grunweg refactor: make library notes a definition large-import t-meta merge-conflict ✅ ✅ ❌ ✅ ✅ ❌ merge conflict
12438 jjaassoonn feat: some APIs for flat modules t-category-theory merge-conflict WIP ✅ ✅ ❌ ❌ ✅ ❌ labelled WIP
24409 urkud chore(*): fix `nmem` vs `not_mem` names awaiting-zulip tech debt merge-conflict delegated awaiting-author ✅ ✅ ❌ ✅ ❌ ❌ awaiting a zulip discussion
24396 JovanGerb feat(Order/Defs): refactor in preparation of `to_dual` attribute awaiting-zulip t-order merge-conflict ✅ ✅ ❌ ✅ ❌ ❌ awaiting a zulip discussion
25138 chrisflav chore(RingTheory): remove unnecessary `toRingHom` coercions t-algebra merge-conflict ✅ ✅ ❌ ✅ ✅ ❌ merge conflict
24965 erdOne refactor: Make `IsLocalHom` take unbundled map maintainer-merge t-algebra merge-conflict awaiting-author ✅ ✅ ❌ ✅ ❌ ❌ merge conflict
8740 digama0 fix: improve `recall` impl / error reporting awaiting-CI t-meta merge-conflict awaiting-author ❌ ✅ ❌ ✅ ❌ ❌ does not pass CI
21182 joneugster fix(Util/CountHeartbeats): move elaboration in #count_heartbeats inside a namespace t-meta merge-conflict ✅ ✅ ❌ ✅ ✅ ❌ merge conflict
22909 AntoineChambert-Loir feat(RingTheory/Pure): pure submodules t-algebra merge-conflict blocked-by-other-PR ❌ ❌ ❌ ✅ ✅ ❌ blocked on another PR
24105 urkud feat(Topology/UniformSpace/Path): new file t-topology merge-conflict awaiting-author ✅ ✅ ❌ ✅ ❌ ❌ merge conflict
23371 grunweg chore: mark `Disjoint.{eq_bot, inter_eq}` simp t-order merge-conflict awaiting-author ✅ ✅ ❌ ✅ ❌ ❌ merge conflict
24877 smmercuri feat: predicates for extensions of complex embeddings t-number-theory merge-conflict ✅ ✅ ❌ ✅ ✅ ❌ merge conflict
24881 smmercuri feat: `InfinitePlace.Extension` API for extensions of infinite places. merge-conflict blocked-by-other-PR ✅ ❌ ❌ ✅ ✅ ❌ ⚠️ blocked on another PR
24882 smmercuri feat: `RamifiedExtension` and `UnramifiedExtension` types for `InfinitePlace.Extension`s t-number-theory merge-conflict blocked-by-other-PR ✅ ❌ ❌ ✅ ✅ ❌ blocked on another PR
16062 adomani Test/ci olean size CI merge-conflict awaiting-author WIP ❌ ✅ ❌ ❌ ❌ ❌ labelled WIP
16020 adomani feat: compare PR `olean`s size with `master` CI merge-conflict ❌ ✅ ❌ ✅ ✅ ❌ failing CI
12799 jstoobysmith feat(LinearAlgebra/UnitaryGroup): Add properties of Special Unitary Group new-contributor t-algebra merge-conflict please-adopt awaiting-author ✅ ✅ ❌ ❌ ❌ ❌ looking for help
23961 FR-vdash-bot refactor: unbundle algebra from `ENormed*` slow-typeclass-synthesis maintainer-merge t-algebra t-analysis merge-conflict awaiting-author ✅ ✅ ❌ ✅ ❌ ❌ merge conflict
23709 plp127 feat: `Nat.findFrom` t-data merge-conflict ❌ ✅ ❌ ✅ ✅ ❌ failing CI
25340 dupuisf chore(Analysis/Convex): move files pertaining to convex/concave functions to their own folder t-convex-geometry merge-conflict ✅ ✅ ❌ ✅ ✅ ❌ merge conflict
13994 grunweg chore(Topology): replace continuity -> fun_prop t-topology merge-conflict ❌ ✅ ❌ ✅ ✅ ❌ failing CI
21734 adomani fix(PR summary): checkout GITHUB_SHA CI merge-conflict awaiting-author WIP ✅ ✅ ❌ ❌ ❌ ❌ labelled WIP
25012 urkud refactor(*): migrate from `Matrix.toLin'` to `Matrix.mulVecLin` merge-conflict ✅ ✅ ❌ ✅ ✅ ❌ merge conflict
24789 Ruben-VandeVelde chore: move Algebra.Group.Hom.End to Algebra.Ring large-import t-algebra merge-conflict awaiting-author ✅ ✅ ❌ ✅ ❌ ❌ merge conflict
13483 adomani feat: automatically replace deprecations t-meta merge-conflict delegated awaiting-author ❌ ✅ ❌ ✅ ❌ ❌ failing CI
24628 pechersky feat(Topology/UniformSpace/Ultra): completion is ultra uniformity iff base is t-topology merge-conflict ✅ ✅ ❌ ✅ ✅ ❌ merge conflict
16743 agjftucker feat(Analysis/Calculus/Implicit): define HasStrictDerivAt.implicitFunOfBivariate new-contributor t-analysis merge-conflict awaiting-author ✅ ✅ ❌ ✅ ❌ ❌ merge conflict
20334 miguelmarco feat: allow polyrith to use a local Singular/Sage install new-contributor t-meta merge-conflict awaiting-author ✅ ✅ ❌ ✅ ❌ ❌ merge conflict
25902 pfaffelh feat: The finite product of semi-rings (in terms of measure theory) is a semi-ring. merge-conflict ❌? ✅ ❌ ✅ ✅ ❌ ⚠️ infrastructure-related CI failing
24275 joelriou feat(Algebra/Homology): the canonical t-structure on the derived category t-category-theory merge-conflict blocked-by-other-PR WIP ✅ ❌ ❌ ❌ ✅ ❌ blocked on another PR
23953 b-reinke feat(Data/Matroid/Tutte): define the Tutte polynomial of a matroid t-data merge-conflict WIP ❌ ✅ ❌ ❌ ✅ ❌ labelled WIP
22639 b-reinke feat(Mathlib/GroupTheory/FreeGroup): theory of (cyclically) reduced words new-contributor t-algebra merge-conflict ✅ ✅ ❌ ✅ ✅ ❌ merge conflict
25980 Multramate feat(GroupTheory/Submonoid/Operations): define homomorphisms of subgroups induced by homomorphisms of groups merge-conflict ❌ ✅ ❌ ✅ ✅ ❌ ⚠️ failing CI
25981 Multramate feat(GroupTheory/GroupAction/Basic): define homomorphisms of fixed subgroups induced by homomorphisms of groups merge-conflict ❌ ✅ ❌ ✅ ✅ ❌ ⚠️ failing CI
25982 Multramate feat(AlgebraicGeometry/EllipticCurve/Group): compute range of baseChange merge-conflict ❌ ✅ ❌ ✅ ✅ ❌ ⚠️ failing CI
25984 Multramate feat(AlgebraicGeometry/EllipticCurve/Affine): add equivalences between points and explicit WithZero types merge-conflict ❌? ✅ ❌ ✅ ✅ ❌ ⚠️ infrastructure-related CI failing
25985 Multramate feat(AlgebraicGeometry/EllipticCurve/Jacobian): add equivalences between points and explicit WithZero types merge-conflict ❌ ✅ ❌ ✅ ✅ ❌ ⚠️ failing CI
23282 joelriou feat(CategoryTheory): monomorphisms in Type are stable under transfinite compositions large-import t-category-theory merge-conflict WIP ❌ ✅ ❌ ❌ ✅ ❌ labelled WIP
23872 joelriou feat: multicoequalizers in the category of types t-category-theory merge-conflict blocked-by-other-PR WIP ✅ ❌ ❌ ❌ ✅ ❌ blocked on another PR
21603 imbrem feat(CategoryTheory/ChosenFiniteProducts): add basic ChosenFiniteCoproducts class new-contributor t-category-theory merge-conflict awaiting-author ✅ ✅ ❌ ✅ ❌ ❌ merge conflict
22059 grunweg feat: manifolds with smooth boundary t-differential-geometry merge-conflict blocked-by-other-PR WIP ❌ ❌ ❌ ❌ ✅ ❌ blocked on another PR
24434 joelriou feat(CategoryTheory): effectiveness of descent t-category-theory merge-conflict blocked-by-other-PR WIP ❌ ❌ ❌ ❌ ✅ ❌ blocked on another PR
18771 joelriou feat(LinearAlgebra/ExteriorPower): exterior powers of free modules are free t-algebra merge-conflict blocked-by-other-PR WIP ❌ ❌ ❌ ❌ ✅ ❌ blocked on another PR
18441 ADedecker refactor(AdicTopology): use new API for algebraic filter bases, and factor some code t-algebra t-topology merge-conflict ✅ ✅ ❌ ✅ ✅ ❌ merge conflict
18439 ADedecker refactor: use new algebraic filter bases API in `FiniteAdeleRing` t-algebra t-topology merge-conflict ✅ ✅ ❌ ✅ ✅ ❌ merge conflict
18438 ADedecker refactor: adapt `KrullTopology` to the new algebraic filter bases API t-algebra t-topology merge-conflict ✅ ✅ ❌ ✅ ✅ ❌ merge conflict
23040 grunweg feat: define immersions and smooth embeddings in infinite dimensions t-differential-geometry merge-conflict WIP ❌ ✅ ❌ ❌ ✅ ❌ labelled WIP
18486 vasnesterov feat(Tactic): tactic for computing asymptotics of real functions t-meta merge-conflict blocked-by-other-PR WIP ❌ ❌ ❌ ❌ ✅ ❌ blocked on another PR
22538 vasnesterov feat(Analysis): radius of convergence for binomial series t-analysis merge-conflict blocked-by-other-PR ✅ ❌ ❌ ✅ ✅ ❌ blocked on another PR
20241 vasnesterov feat(Data/Seq): coinductive predicates for sequences t-data merge-conflict blocked-by-other-PR ✅ ❌ ❌ ✅ ✅ ❌ blocked on another PR
13964 pechersky feat(Data/DigitExpansion): begin defining variant of reals without rationals t-data merge-conflict ✅ ✅ ❌ ✅ ✅ ❌ merge conflict
19695 Timeroot feat(ModelTheory): Set.Definable is transitive large-import t-logic merge-conflict ❌ ✅ ❌ ✅ ✅ ❌ failing CI
22073 vasnesterov feat(Tactic/Order): frontend for `order` t-meta merge-conflict blocked-by-other-PR ✅ ❌ ❌ ✅ ✅ ❌ blocked on another PR
23915 joelriou feat(CategoryTheory): deriving functors using a right derivability structure t-category-theory merge-conflict blocked-by-other-PR WIP ✅ ❌ ❌ ❌ ✅ ❌ blocked on another PR
18662 joelriou feat(LinearAlgebra/ExteriorPower): generators of the exterior powers t-algebra merge-conflict blocked-by-other-PR WIP ✅ ❌ ❌ ❌ ✅ ❌ blocked on another PR
18735 joelriou feat(Algebra/Module): presentation of the exterior power t-algebra merge-conflict blocked-by-other-PR WIP ❌ ❌ ❌ ❌ ✅ ❌ blocked on another PR
18551 joelriou feat(AlgebraicGeometry): the algebraic De Rham complex t-algebra t-algebraic-geometry merge-conflict blocked-by-other-PR WIP ❌ ❌ ❌ ❌ ✅ ❌ blocked on another PR
22724 peabrainiac feat(Geometry/Diffeology): diffeologies generated from sets of plots t-differential-geometry merge-conflict ✅ ✅ ❌ ✅ ✅ ❌ merge conflict
25848 joelriou feat/refactor: redefinition of homology + derived categories large-import t-topology t-category-theory merge-conflict blocked-by-other-PR WIP ❌? ❌ ❌ ❌ ✅ ❌ blocked on another PR
23831 vasnesterov feat(Analysis): binomial series convergence t-analysis merge-conflict blocked-by-other-PR ✅ ❌ ❌ ✅ ✅ ❌ blocked on another PR
26588 faenuccio feat(Algebra/GroupWithZero/WithZero): add the multiplicative embedding with zero from the range large-import t-order t-algebra merge-conflict blocked-by-other-PR WIP ❌ ❌ ❌ ❌ ✅ ❌ blocked on another PR
14752 AntoineChambert-Loir fix(Topology/Algebra/Valued): repair definition of Valued t-algebra t-topology merge-conflict WIP ✅ ✅ ❌ ❌ ✅ ❌ labelled WIP
19633 grunweg fix(CI): build the Archive and Counterexamples with --wfail also CI awaiting-CI easy merge-conflict delegated ❌ ✅ ❌ ✅ ❌ ❌ does not pass CI
19890 vihdzp chore(SetTheory/Ordinal/Arithmetic): redefine subtraction t-set-theory merge-conflict ✅ ✅ ❌ ✅ ✅ ❌ merge conflict
9820 jjaassoonn feat(RingTheory/GradedAlgebra/HomogeneousIdeal): generalize to homogeneous submodule t-algebra merge-conflict ✅ ✅ ❌ ✅ ✅ ❌ merge conflict
14009 grunweg chore: replace continuity -> fun_prop in remaining directories t-analysis merge-conflict awaiting-author ✅ ✅ ❌ ✅ ❌ ❌ merge conflict
14203 dagurtomas feat(Algebra/ModuleCat): descent data workshop-AIM-AG-2024 t-algebra t-algebraic-geometry t-category-theory merge-conflict blocked-by-other-PR WIP ✅ ❌ ❌ ❌ ✅ ❌ blocked on another PR
16074 Rida-Hamadani feat: combinatorial maps and planar graphs t-combinatorics merge-conflict ✅ ✅ ❌ ✅ ✅ ❌ merge conflict
16801 awainverse feat(ModelTheory/Equivalence): The quotient type of formulas modulo a theory t-logic merge-conflict awaiting-author ✅ ✅ ❌ ✅ ❌ ❌ merge conflict
17458 urkud refactor(Algebra/Group): make `IsUnit` a typeclass awaiting-zulip t-algebra merge-conflict ❌ ✅ ❌ ✅ ❌ ❌ failing CI
17627 hrmacbeth feat: universal properties of vector bundle constructions t-differential-geometry merge-conflict delegated ✅ ✅ ❌ ✅ ✅ ❌ merge conflict
19444 joelriou feat(CategoryTheory/Sites): Equivalence of categories of sheaves with a dense subsite that is 1-hypercover dense t-category-theory merge-conflict WIP ❌ ✅ ❌ ❌ ✅ ❌ labelled WIP
19796 peakpoint feat: L'Hopital's rule from within a convex set new-contributor t-analysis merge-conflict ✅ ✅ ❌ ✅ ✅ ❌ awaiting review
21965 JovanGerb feat: extensible `push`(_neg) tactic - part 1 t-meta merge-conflict awaiting-author ✅ ✅ ❌ ✅ ❌ ❌ awaiting author
22018 maddycrim feat(RingTheory/Localization/Pi): localization of a finite direct product where each semiring in product has maximal nilradical is a projection large-import new-contributor t-algebra merge-conflict WIP ✅ ✅ ❌ ❌ ✅ ❌ labelled WIP
22151 alreadydone feat(RingTheory): a semiprimary ring is Noetherian/Artinian iff its Jacobson radical is fg t-algebra merge-conflict ✅ ✅ ❌ ✅ ✅ ❌ awaiting review
22322 mariainesdff feat(RingTheory/DividedPowers/RatAlgebra): add definitions large-import t-algebra merge-conflict ✅ ✅ ❌ ✅ ✅ ❌ awaiting review
22367 joelriou feat(CategoryTheory/Abelian): Noetherian objects form a Serre class t-category-theory merge-conflict WIP ❌ ✅ ❌ ❌ ✅ ❌ labelled WIP
22603 pechersky chore(Topology): rename pi family from π to X tech debt t-topology merge-conflict ✅ ✅ ❌ ✅ ✅ ❌ awaiting review
22771 alreadydone feat(Homotopy/Lifting): monodromy of covering maps and lifting criterion t-topology merge-conflict ✅ ✅ ❌ ✅ ✅ ❌ merge conflict
22898 AntoineChambert-Loir feat(RingTheory/TensorProduct/DirectLimit/FG): direct limit of finitely generated submodules and tensor product t-algebra merge-conflict WIP ✅ ✅ ❌ ❌ ✅ ❌ labelled WIP
22928 javra feat(CategoryTheory): infrastructure for inclusion morphisms into products in categories with 0-morphisms t-category-theory merge-conflict ❌ ✅ ❌ ✅ ✅ ❌ failing CI
22954 eric-wieser feat(RingTheory/Congruence/Hom): copy from GroupTheory t-algebra merge-conflict ❌ ✅ ❌ ✅ ✅ ❌ failing CI
23365 vasnesterov feat(Tactic/Simproc): nested quantifiers in `existsAndEq` large-import t-meta merge-conflict ✅ ✅ ❌ ✅ ✅ ❌ merge conflict
23497 chrisflav chore(RingTheory/AdicCompletion/AsTensorProduct): golf using five lemma for modules t-algebra merge-conflict ✅ ✅ ❌ ✅ ✅ ❌ merge conflict
23637 kirilvino feat(Combinatorics/SimpleGraph): every circuit contains a cycle proof new-contributor t-combinatorics merge-conflict awaiting-author ✅ ✅ ❌ ✅ ❌ ❌ merge conflict
23763 grunweg feat(Linter.openClassical): also lint for Classical declarations as … t-linter merge-conflict ❌ ✅ ❌ ✅ ✅ ❌ failing CI
23835 chrisflav feat(Topology): cardinality of connected components is bounded by cardinality of fiber large-import t-topology merge-conflict ✅ ✅ ❌ ✅ ✅ ❌ merge conflict
24350 erdOne feat(FieldTheory): fg extension over perfect field is separably generated t-algebra merge-conflict ✅ ✅ ❌ ✅ ✅ ❌ awaiting review
24351 eric-wieser feat: fderiv lemmas for `pow` t-analysis merge-conflict ✅ ✅ ❌ ✅ ✅ ❌ merge conflict
24411 joelriou feat(CategoryTheory): descent of morphisms for a pseudofunctor t-category-theory merge-conflict blocked-by-other-PR WIP ✅ ❌ ❌ ❌ ✅ ❌ blocked on another PR
24435 faenuccio chore(RingTheory/Valuation/Discrete/Basic): add ordered Iso between Z_{m0} and the value group large-import t-order t-algebra merge-conflict WIP ❌ ✅ ❌ ❌ ✅ ❌ labelled WIP
24530 chrisflav feat(RingTheory): faithfully flat ring maps t-algebra merge-conflict ✅ ✅ ❌ ✅ ✅ ❌ merge conflict
24614 JovanGerb chore: rename field `inf` to `min` in `Lattice` t-order merge-conflict awaiting-author ✅ ✅ ❌ ✅ ❌ ❌ merge conflict
24627 pechersky feat(Topology/Algebra/Valued): `IsLinearTopology 𝒪[K] K` and `𝒪[K] 𝒪[K]` t-topology merge-conflict awaiting-author blocked-by-other-PR ✅ ❌ ❌ ✅ ❌ ❌ blocked on another PR
24710 chrisflav chore(Data/Set): `tsum` version of `Set.encard_iUnion_of_finite` for non-finite types t-data merge-conflict ❌ ✅ ❌ ✅ ✅ ❌ failing CI
24823 eric-wieser refactor: add `hom` lemmas for the `MonoidalCategory` structure on `ModuleCat` t-algebra merge-conflict ✅ ✅ ❌ ✅ ✅ ❌ merge conflict
25071 erdOne feat(EllipticCurve): basic API for singular cubics t-algebraic-geometry merge-conflict ✅ ✅ ❌ ✅ ✅ ❌ merge conflict
25188 vlad902 feat: add lemmas about `List.scanr` t-data merge-conflict ✅ ✅ ❌ ✅ ✅ ❌ awaiting review
25218 kckennylau feat(AlgebraicGeometry): Tate normal form of elliptic curves awaiting-zulip new-contributor t-algebraic-geometry merge-conflict ✅ ✅ ❌ ✅ ❌ ❌ awaiting a zulip discussion
25238 Hagb feat(Tactic/ComputeDegree): add support for scalar multiplication with different types new-contributor merge-conflict ✅ ✅ ❌ ✅ ✅ ❌ ⚠️ merge conflict
25283 Brian-Nugent feat: regular local rings new-contributor t-algebra merge-conflict ✅ ✅ ❌ ✅ ✅ ❌ merge conflict
25284 alreadydone feat(LinearAlgebra/Contraction): bijectivity of `dualTensorHom` + generalize to CommSemiring t-algebra merge-conflict ✅ ✅ ❌ ✅ ✅ ❌ merge conflict
25410 JovanGerb chore: remove some duplicate instances merge-conflict ✅ ✅ ❌ ✅ ✅ ❌ merge conflict
25450 pechersky feat(Valued): Valuation.leAddSubgroup and ideal/submodule versions of ltAddSubgroup t-algebra t-analysis t-number-theory merge-conflict ✅ ✅ ❌ ✅ ✅ ❌ awaiting review
25474 adomani test for .lean/.md check file-removed merge-conflict ❌ ✅ ❌ ✅ ✅ ❌ failing CI
25483 VTrelat chore(Data/Set/Prod, SetTheory/ZFC/Basic): add theorem prod_subset_of_prod and extend ZFC model t-data new-contributor merge-conflict ✅ ✅ ❌ ✅ ✅ ❌ merge conflict
25484 VTrelat feat(SetTheory/ZFC/Booleans): define Boolean algebra in ZFC new-contributor merge-conflict blocked-by-other-PR ❌ ❌ ❌ ✅ ✅ ❌ ⚠️ blocked on another PR
25485 VTrelat feat(SetTheory/ZFC/Naturals): define natural numbers in ZFC new-contributor merge-conflict ❌ ✅ ❌ ✅ ✅ ❌ ⚠️ failing CI
25486 VTrelat feat(SetTheory/ZFC/Integers): define integers in ZFC new-contributor merge-conflict blocked-by-other-PR ❌ ❌ ❌ ✅ ✅ ❌ ⚠️ blocked on another PR
25488 VTrelat feat(SetTheory/ZFC/Rationals): define rationals in ZFC new-contributor merge-conflict blocked-by-other-PR ❌ ❌ ❌ ✅ ✅ ❌ ⚠️ blocked on another PR
25561 callesonne feat(Category/Grpd): define the bicategory of groupoids t-category-theory merge-conflict awaiting-author ✅ ✅ ❌ ✅ ❌ ❌ merge conflict
25573 JovanGerb feat: define `∃ x > y, ...` notation to mean `∃ x, y < x ∧ ...` t-meta merge-conflict ✅ ✅ ❌ ✅ ✅ ❌ awaiting review
25578 peakpoint refactor(Geometry/Euclidean/Projection): redefine projection and reflection for affine subspaces new-contributor t-euclidean-geometry merge-conflict ✅ ✅ ❌ ✅ ✅ ❌ merge conflict
25586 JovanGerb chore(Order): use new ge/gt naming convention - Part 5 merge-conflict ✅ ✅ ❌ ✅ ✅ ❌ merge conflict
25622 eric-wieser refactor: overhaul instances on LocalizedModule t-algebra merge-conflict ❌ ✅ ❌ ✅ ✅ ❌ failing CI
25735 robin-carlier feat(CategoryTheory/Limits/Sifted): characterization of sifted categories file-removed large-import t-category-theory merge-conflict blocked-by-other-PR ✅ ❌ ❌ ✅ ✅ ❌ blocked on another PR
25770 Parcly-Taxel chore: fix more induction/recursor branch names tech debt merge-conflict ✅ ✅ ❌ ✅ ✅ ❌ merge conflict
25774 Parcly-Taxel chore: deprime `induction` in `AlgebraicTopology/CategoryTheory` tech debt merge-conflict ✅ ✅ ❌ ✅ ✅ ❌ merge conflict
25775 emilyriehl feat(AlgebraicTopology/SimplicialSet/NerveAdjunction): to Strict Segal 2 infinity-cosmos t-topology t-category-theory merge-conflict awaiting-author ✅ ✅ ❌ ✅ ❌ ❌ merge conflict
25776 Parcly-Taxel chore: deprime `induction` in `Analysis` tech debt t-analysis merge-conflict ✅ ✅ ❌ ✅ ✅ ❌ merge conflict
25786 Parcly-Taxel feat: IMO 2001 Q4 IMO merge-conflict ✅ ✅ ❌ ✅ ✅ ❌ merge conflict
25794 dagurtomas feat(CategoryTheory): localization preserves braided structure t-category-theory merge-conflict ✅ ✅ ❌ ✅ ✅ ❌ awaiting review
25797 dagurtomas feat(Condensed): closed symmetric monoidal structure on light condensed modules t-condensed merge-conflict WIP ❌ ✅ ❌ ❌ ✅ ❌ labelled WIP
25816 sgouezel chore: kill coercion from EquivLike to Equiv t-logic merge-conflict WIP ❌ ✅ ❌ ❌ ✅ ❌ labelled WIP
25822 ScottCarnahan WIP: experiments with vertex algebras large-import merge-conflict WIP ❌ ✅ ❌ ❌ ✅ ❌ labelled WIP
25823 joelriou refactor(CategoryTheory/Limits): colimits in Type t-category-theory merge-conflict awaiting-author ❌ ✅ ❌ ✅ ❌ ❌ failing CI
25830 ScottCarnahan refactor (RingTheory/HahnSeries/HEval): remove positive order condition from definition t-algebra merge-conflict ✅ ✅ ❌ ✅ ✅ ❌ merge conflict
25831 ScottCarnahan feat (RingTheory/HahnSeries): Powers of a binomial t-algebra merge-conflict blocked-by-other-PR ✅ ❌ ❌ ✅ ✅ ❌ blocked on another PR
25864 plp127 feat(Nat/Digits): use fuel in `Nat.digits` t-data merge-conflict ✅ ✅ ❌ ✅ ✅ ❌ merge conflict
25884 101damnations feat(RepresentationTheory/Homological/GroupHomology/LowDegree): add `IsOneCycle` predicate and friends file-removed t-algebra merge-conflict blocked-by-other-PR ✅ ❌ ❌ ✅ ✅ ❌ blocked on another PR
25888 101damnations feat(RepresentationTheory/Homological/GroupHomology/LowDegree): Identify `cycles A n` with `nCycles A` for `n = 0, 1, 2` file-removed merge-conflict blocked-by-other-PR ✅ ❌ ❌ ✅ ✅ ❌ ⚠️ blocked on another PR
25900 pfaffelh feat (Topology/Compactness/CompactSystem): Set system of finite unions of sets in a compact system is again a compact system merge-conflict blocked-by-other-PR ✅ ❌ ❌ ✅ ✅ ❌ ⚠️ blocked on another PR
25901 callesonne feat(Bicategory/Opposites): add 1-cell opposite bicategory t-category-theory merge-conflict awaiting-author ✅ ✅ ❌ ✅ ❌ ❌ merge conflict
25906 pfaffelh feat (Topology/Compactness/CompactSystem): Closed and compact square cylinders form a compact system. merge-conflict blocked-by-other-PR ✅ ❌ ❌ ✅ ✅ ❌ ⚠️ blocked on another PR
25908 101damnations feat(RepresentationTheory/Homological/GroupHomology/LowDegree): specialized API for `H0, H1, H2` file-removed t-algebra merge-conflict blocked-by-other-PR ✅ ❌ ❌ ✅ ✅ ❌ blocked on another PR
25914 eric-wieser feat: add an ext lemma for the opposite category t-category-theory awaiting-CI merge-conflict awaiting-author ❌ ✅ ❌ ✅ ❌ ❌ does not pass CI
25917 BoltonBailey docs: Add documentation to miscellaneous files migrated-from-branch merge-conflict WIP documentation ✅ ✅ ❌ ❌ ✅ ❌ labelled WIP
25928 JovanGerb feat(gcongr): let `gcongr` take a depth parameter, analogous to `congr` t-meta merge-conflict delegated awaiting-author ✅ ✅ ❌ ✅ ❌ ❌ awaiting author
25929 101damnations feat(RepresentationTheory/Homological/GroupHomology/LowDegree): `H₁(G, A) ≃+ Gᵃᵇ ⊗[ℤ] A` when `A` is trivial file-removed t-algebra merge-conflict blocked-by-other-PR ✅ ❌ ❌ ✅ ✅ ❌ blocked on another PR
25930 loefflerd WIP towards Hecke bound for q-expansions migrated-from-branch t-number-theory merge-conflict WIP ✅ ✅ ❌ ❌ ✅ ❌ labelled WIP
25933 artie2000 feat(Algebra/Order/Ring): make `IsOrderedRing.toStrictOrderedRing` an instance t-algebra merge-conflict ❌ ✅ ❌ ✅ ✅ ❌ failing CI
25939 101damnations feat(RepresentationTheory/Homological/GroupHomology/Functoriality): low degree functoriality maps file-removed t-algebra merge-conflict blocked-by-other-PR ✅ ❌ ❌ ✅ ✅ ❌ blocked on another PR
25943 101damnations feat(RepresentationTheory/Homological/GroupHomology): long exact sequences large-import t-algebra merge-conflict blocked-by-other-PR ✅ ❌ ❌ ✅ ✅ ❌ blocked on another PR
25952 101damnations feat(RepresentationTheory/Homological/GroupHomology/Functoriality): the degree 1 part of the corestriction-coinflation exact sequence when the subgroup acts trivially t-algebra merge-conflict blocked-by-other-PR ✅ ❌ ❌ ✅ ✅ ❌ blocked on another PR
25969 101damnations feat(RepresentationTheory/Homological/GroupHomology/Functoriality): the degree 1 part of the corestriction-coinflation exact sequence t-algebra merge-conflict blocked-by-other-PR ✅ ❌ ❌ ✅ ✅ ❌ blocked on another PR
25988 Multramate refactor(AlgebraicGeometry/EllipticCurve/*): replace Fin 3 with products t-algebraic-geometry merge-conflict ✅ ✅ ❌ ✅ ✅ ❌ awaiting review
25991 Multramate feat(AlgebraicGeometry/EllipticCurve): generalise nonsingular condition merge-conflict ❌ ✅ ❌ ✅ ✅ ❌ ⚠️ failing CI
26010 linesthatinterlace feat(`Algebra/Group/Prod`): Add API for inclusion and projection maps from and to the product of units. migrated-from-branch merge-conflict WIP ❌ ✅ ❌ ❌ ✅ ❌ ⚠️ labelled WIP
26011 linesthatinterlace feat: add elementary lifts for `OneHom`, `MulHom`, `MonoidHom` and `RingHom`. migrated-from-branch t-algebra merge-conflict ✅ ✅ ❌ ✅ ✅ ❌ merge conflict
26012 linesthatinterlace feat: Low-level derivatives of lifts on `OneHom`, `MulHom` and `MonoidHom` migrated-from-branch t-algebra merge-conflict ✅ ✅ ❌ ✅ ✅ ❌ merge conflict
26015 linesthatinterlace feat: Add high-level generalizations from `MonoidHom` lifts migrated-from-branch merge-conflict ❌ ✅ ❌ ✅ ✅ ❌ ⚠️ failing CI
25970 wwylele feat(RingTheory): decompose archimedean classes of HahnSeries large-import merge-conflict ✅ ✅ ❌ ✅ ✅ ❌ ⚠️ awaiting review
26071 linesthatinterlace feat: Add `id` and `comp` classes for `FunLike` and `refl`, `trans` and `symm` classes for `EquivLike` t-data RFC merge-conflict WIP ❌ ✅ ❌ ❌ ✅ ❌ labelled WIP
26090 grunweg chore: make `finiteness` a default tactic merge-conflict ❌ ✅ ❌ ✅ ✅ ❌ failing CI
26096 vasnesterov feat(Topology/Instances): Cantor set is the set of ternary numbers without `1`s large-import t-topology merge-conflict blocked-by-other-PR ✅ ❌ ❌ ✅ ✅ ❌ blocked on another PR
26101 xroblot feat(NumberField): specialized version of Kummer Dedekind for the splitting of prime numbers t-number-theory merge-conflict blocked-by-other-PR WIP ❌ ❌ ❌ ❌ ✅ ❌ blocked on another PR
26136 vasnesterov feat(Topology/Instances): Cantor set is homeomorphic to `ℕ → Bool` large-import t-topology merge-conflict blocked-by-other-PR ✅ ❌ ❌ ✅ ✅ ❌ blocked on another PR
26149 vasnesterov feat(Topology): continuous surjection from Cantor set to Hilbert cube large-import t-topology merge-conflict blocked-by-other-PR ✅ ❌ ❌ ✅ ✅ ❌ blocked on another PR
26169 joelriou feat(AlgebraicTopology/ModelCategory): a trick by Joyal large-import t-category-theory merge-conflict WIP ✅ ✅ ❌ ❌ ✅ ❌ labelled WIP
26171 joelriou feat(AlgebraicTopology): cylinder objects in model categories large-import t-topology t-category-theory merge-conflict WIP ✅ ✅ ❌ ❌ ✅ ❌ labelled WIP
26175 artie2000 feat: add new `simp` lemmas bench-after-CI awaiting-bench t-algebra t-meta merge-conflict blocked-by-other-PR ❌ ❌ ❌ ✅ ✅ ❌ blocked on another PR
26178 ppls-nd-prs feat(CategoryTheory/Limits): Fubini for products new-contributor t-category-theory merge-conflict awaiting-author ✅ ✅ ❌ ✅ ❌ ❌ merge conflict
26184 vasnesterov feat(Topology): every compact metric space is image of Cantor set large-import t-topology merge-conflict blocked-by-other-PR ✅ ❌ ❌ ✅ ✅ ❌ blocked on another PR
26185 vasnesterov feat(Counterexamples): Peano curve large-import t-topology merge-conflict blocked-by-other-PR ✅ ❌ ❌ ✅ ✅ ❌ blocked on another PR
26218 Thmoas-Guan feat(Algebra): definition of cohen macaulay large-import t-algebra merge-conflict blocked-by-other-PR ❌ ❌ ❌ ✅ ✅ ❌ blocked on another PR
26219 Thmoas-Guan feat(RingTheory/KrullDimension): Krull Dimension of quotient regular sequence t-algebra merge-conflict ✅ ✅ ❌ ✅ ✅ ❌ merge conflict
26234 BoltonBailey chore(Combinatorics/SimpleGraph/Walk): split SimpleGraph.Path file-removed tech debt t-combinatorics merge-conflict WIP ❌ ✅ ❌ ❌ ✅ ❌ labelled WIP
26241 BoltonBailey chore: add deprecations for split of SimpleGraph.Path t-combinatorics merge-conflict blocked-by-other-PR ✅ ❌ ❌ ✅ ✅ ❌ blocked on another PR
26245 Thmoas-Guan feat(Algebra): cohen macaulay local ring is catenary large-import t-algebra merge-conflict blocked-by-other-PR WIP ❌ ❌ ❌ ❌ ✅ ❌ blocked on another PR
26303 joelriou feat(AlgebraicTopology): the fundamental lemma of homotopical algebra large-import t-category-theory merge-conflict blocked-by-other-PR WIP ❌ ❌ ❌ ❌ ✅ ❌ blocked on another PR
26384 jjdishere feat(RingTheory/Perfectoid): Fontaine's theta map is surjective t-algebra t-number-theory merge-conflict WIP ❌ ✅ ❌ ❌ ✅ ❌ labelled WIP
26385 jjdishere feat(RingTheory/Perfectoid): define integral perfectoid rings t-algebra merge-conflict WIP ❌ ✅ ❌ ❌ ✅ ❌ labelled WIP
26388 jjdishere feat(RingTheory/Perfectoid): Fontaine's theta map and the de Rham period rings t-algebra t-number-theory merge-conflict ❌ ✅ ❌ ✅ ✅ ❌ failing CI
26395 winstonyin feat: $C^1$ vector fields on compact manifolds define global flows t-differential-geometry merge-conflict blocked-by-other-PR WIP ❌ ❌ ❌ ❌ ✅ ❌ blocked on another PR
26399 ChrisHughes24 refactor(ModelTheory): tidy up proof of Ax-Grothendieck with definable functions t-logic merge-conflict blocked-by-other-PR ❌ ❌ ❌ ✅ ✅ ❌ blocked on another PR
26413 michaellee94 feat(Analysis/ODE/MaximalSolution): Existence of maximal solutions for ODE meeting Picard-Lindelöf conditions new-contributor t-analysis merge-conflict awaiting-author blocked-by-other-PR ❌ ❌ ❌ ✅ ❌ ❌ blocked on another PR
26436 AntoineChambert-Loir feat(Mathlib/Data/Nat/Prime/Defs): fuel Nat.minFac t-data merge-conflict ❌ ✅ ❌ ✅ ✅ ❌ failing CI
26449 faenuccio feat(NumberTheory/LocalFields/Basic): provide the definition of (valued) Local Field large-import t-algebra t-number-theory merge-conflict WIP ✅ ✅ ❌ ❌ ✅ ❌ labelled WIP
26457 AntoineChambert-Loir feat(Mathlib/GroupTheory/Perm/MaximalSubgroups): maximal subgroups of the permutation group large-import merge-conflict blocked-by-other-PR ✅ ❌ ❌ ✅ ✅ ❌ ⚠️ blocked on another PR
26464 joelriou feat(LinearAlgebra): generators of pi tensor products file-removed t-algebra merge-conflict ✅ ✅ ❌ ✅ ✅ ❌ awaiting review
26465 joelriou feat(Algebra/Module): presentation of the `PiTensorProduct` file-removed t-algebra merge-conflict blocked-by-other-PR ❌ ❌ ❌ ✅ ✅ ❌ blocked on another PR
26467 joelriou feat(LinearAlgebra): the tensor product of a finite family of free modules is free file-removed t-algebra merge-conflict blocked-by-other-PR WIP ❌ ❌ ❌ ❌ ✅ ❌ blocked on another PR
26520 joelriou feat(Algebra/Homology): truncations of ConnectData.cochainComplex large-import t-algebra t-category-theory merge-conflict WIP ✅ ✅ ❌ ❌ ✅ ❌ labelled WIP
26526 pechersky feat(RingTheory/Valuation/IntegrallyClosed): the valuation subring is integrally closed t-algebra t-analysis t-number-theory merge-conflict blocked-by-other-PR ✅ ❌ ❌ ✅ ✅ ❌ blocked on another PR
26591 mariainesdff feat(RingTheory/Valuation/Discrete/Basic): add uniformizer API large-import t-algebra t-number-theory merge-conflict blocked-by-other-PR ❌ ❌ ❌ ✅ ✅ ❌ blocked on another PR
26596 BoltonBailey refactor(Probability/ProbabilityMassFunction): Make constructions use NNReal t-measure-probability merge-conflict ✅ ✅ ❌ ✅ ✅ ❌ awaiting review
26623 mariainesdff feat(RingTheory/Valuation/Discrete/Basic): relate DVRs and discrete valuations large-import t-algebra merge-conflict blocked-by-other-PR ❌ ❌ ❌ ✅ ✅ ❌ blocked on another PR
26625 mathlib4-update-dependencies-bot chore: update Mathlib dependencies 2025-07-02 dependency-bump auto-merge-after-CI merge-conflict ready-to-merge ✅ ✅ ❌ ✅ ✅ ❌ merge conflict
26662 ocfnash chore: use typeclass rather than implicit arguments for decidability data t-algebra easy merge-conflict ✅ ✅ ❌ ✅ ✅ ❌ awaiting review
26671 grunweg feat: `contMDiff_section_of_smul_smoothBumpFunction` t-differential-geometry merge-conflict blocked-by-other-PR WIP ❌ ❌ ❌ ❌ ✅ ❌ blocked on another PR
26713 pechersky feat(Topology/ValuativeRel): helper instance for Valued from ValuativeTopology merge-conflict ✅ ✅ ❌ ✅ ✅ ❌ ⚠️ merge conflict
26754 pechersky feat(Valuation/RankOne): equivalence with ValuativeRel.isRankLeOne large-import merge-conflict ✅ ✅ ❌ ✅ ✅ ❌ ⚠️ merge conflict
26080 grunweg feat(Tactic/Positivity): extend EReal support for numeric casts maintainer-merge t-meta merge-conflict ✅ ✅ ❌ ✅ ✅ ❌ merge conflict
24379 chrisflav feat(Algebra/AlgHom): `Unique` if target is `Subsingleton` t-algebra merge-conflict delegated ✅ ✅ ❌ ✅ ✅ ❌ merge conflict
26776 sgouezel refactor: make `I` an outparam, and use forgetful inheritance in products RFC merge-conflict WIP ❌ ✅ ❌ ❌ ✅ ❌ labelled WIP
26446 joelriou refactor(CategoryTheory): make morphisms in full subcategories a 1-field structure large-import t-category-theory merge-conflict WIP ❌ ✅ ❌ ❌ ✅ ❌ labelled WIP