Why is my PR not on the queue?

This page was last updated on: March 31, 2025 at 01:50 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 not from a fork? CI status? not blocked? no merge conflict? ready? awaiting review? On the review queue? Missing topic label? PR's overall status
14727 jjaassoonn feat(RingTheory/Flat/CategoryTheory): a flat module has vanishing higher Tor groups t-algebra awaiting-author ✅ ✅ ✅ ✅ ✅ ❌ ❌ awaiting author
14583 lecopivo fix: make concrete cycle notation local awaiting-author ✅ ✅ ✅ ✅ ✅ ❌ ❌ awaiting author
14345 digama0 feat: the Dialectica category is monoidal closed t-category-theory awaiting-author ✅ ✅ ✅ ✅ ✅ ❌ ❌ awaiting author
14386 Parcly-Taxel feat: the Rado graph t-combinatorics WIP ✅ ❌ ✅ ✅ ❌ ✅ ❌ labelled WIP
14444 digama0 fix(GeneralizeProofs): unreachable! bug t-meta awaiting-author ✅ ✅ ✅ ✅ ✅ ❌ ❌ awaiting author
13038 adomani feat: Mathlib weekly reports CI t-meta 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
12032 mcdoll feat: Delta distribution as a limit t-analysis blocked-by-other-PR WIP ✅ ❌ ❌ ✅ ❌ ✅ ❌ blocked on another PR
11496 mcdoll feat: Topology of pointwise convergence for continuous linear maps t-topology awaiting-author ✅ ✅ ✅ ✅ ✅ ❌ ❌ awaiting author
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
9320 BoltonBailey chore: Golf simp calls WIP ✅ ✅ ✅ ✅ ❌ ✅ ❌ labelled WIP
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
9352 chenyili0818 feat: arithmetic lemmas for `gradient` 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
6252 michaellee94 feat(Geometry/Manifolds/Instances/Homeomorph): Homeomorphism maps `C^k` manifolds to `C^k` manifolds t-differential-geometry WIP ✅ ✅ ✅ ✅ ❌ ✅ ❌ labelled WIP
7300 ah1112 feat: synthetic geometry t-euclidean-geometry awaiting-author help-wanted ✅ ✅ ✅ ✅ ❌ ❌ ❌ looking for help
5897 eric-wieser feat: add a `MonadError` instance for `ContT` 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
15617 vigoux perf: use foldl for implementation of Multiset.fold awaiting-author ❌ ❌? ✅ ✅ ✅ ❌ ❌ opened from a fork
14009 grunweg chore: replace continuity -> fun_prop in remaining directories t-analysis 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
12581 linesthatinterlace feat: (Probability/SubProbabilityMassFunction) t-measure-probability WIP ✅ ❌ ✅ ✅ ❌ ✅ ❌ labelled WIP
9181 linesthatinterlace feat(Data/Option/Order): Add default order structure to Option with `none` incomparable t-data RFC awaiting-CI blocked-by-other-PR WIP ✅ ❌ ❌ ✅ ❌ ❌ ❌ blocked on another PR
9040 BoltonBailey feat: `to_snoc` an attribute for generating lemmas with snoc in them t-meta please-adopt WIP help-wanted ✅ ❌ ✅ ✅ ❌ ✅ ❌ looking for help
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
5919 MithicSpirit feat: implement orthogonality for AffineSubspace t-analysis WIP help-wanted ✅ ✅ ✅ ✅ ❌ ✅ ❌ looking for help
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
7172 BoltonBailey feat: Composition of Turing machines t-computability awaiting-CI please-adopt WIP good first issue ✅ ❌ ✅ ✅ ❌ ❌ ❌ looking for help
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
11385 BoltonBailey feat: scripts to analyze overlap between namespaces t-meta WIP ✅ ✅ ✅ ✅ ❌ ✅ ❌ labelled WIP
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
16553 grunweg WIP: tinkering with orientable manifolds t-differential-geometry blocked-by-other-PR WIP ✅ ❌ ❌ ✅ ❌ ✅ ❌ blocked on another PR
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
15651 TpmKranz feat(Computability/NFA): operations for Thompson's construction t-computability new-contributor awaiting-author ✅ ✅ ✅ ✅ ✅ ❌ ❌ awaiting author
15212 victorliu5296 feat: Add fundamental theorem of calculus-2 for Banach spaces new-contributor t-measure-probability t-analysis awaiting-author ✅ ✅ ✅ ✅ ✅ ❌ ❌ awaiting author
13740 YaelDillies feat: More robust ae notation t-measure-probability awaiting-CI t-meta ✅ ❌ ✅ ✅ ✅ ❌ ❌ does not pass CI
16688 vlad902 chore(scripts/install_macos): Fix 2 PATH resolution issues ❌ ✅ ✅ ✅ ✅ ✅ ✅ opened from a fork
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
18253 callesonne feat(Bicactegory/NaturalTransformation): refactor strong natural transformations t-category-theory blocked-by-other-PR ✅ ✅ ❌ ✅ ✅ ✅ ❌ blocked on another PR
12799 jstoobysmith feat(LinearAlgebra/UnitaryGroup): Add properties of Special Unitary Group new-contributor t-algebra please-adopt awaiting-author ✅ ✅ ✅ ✅ ❌ ❌ ❌ looking for help
18252 callesonne feat(Bicategory/Oplax): Fix simp lemmas and renaming t-category-theory awaiting-author ✅ ✅ ✅ ✅ ✅ ❌ ❌ awaiting author
13611 callesonne feat(FiberedCategory/HasFibers): define HasFibers class t-category-theory awaiting-author ✅ ✅ ✅ ✅ ✅ ❌ ❌ awaiting author
16835 Parcly-Taxel feat: `Finpartition.attachEquiv` t-combinatorics awaiting-author ✅ ✅ ✅ ✅ ✅ ❌ ❌ awaiting author
18210 vihdzp feat(Order/Hom/Basic): `WithBot (Fin n) ≃o Fin (n + 1)` t-order awaiting-author ✅ ✅ ✅ ✅ ✅ ❌ ❌ awaiting author
16801 awainverse feat(ModelTheory/Equivalence): The quotient type of formulas modulo a theory t-logic awaiting-author ✅ ✅ ✅ ✅ ✅ ❌ ❌ awaiting author
18914 Vierkantor fix(Tactic/Linter): the `minImports` linter understands file edits t-linter t-meta 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
16062 adomani Test/ci olean size CI awaiting-author WIP ✅ ❌ ✅ ✅ ❌ ❌ ❌ labelled WIP
19329 adomani perf(CI): automatically benchmark PRs when they are opened CI WIP ✅ ✅ ✅ ✅ ❌ ✅ ❌ labelled WIP
13458 grunweg perf(Manifold/ContMDiff/NormedSpace): add shortcut instances t-differential-geometry awaiting-author ✅ ✅ ✅ ✅ ✅ ❌ ❌ awaiting author
19552 grunweg perf: disable the multi-goal linter t-linter WIP ✅ ❌ ✅ ✅ ❌ ✅ ❌ labelled WIP
19551 grunweg perf: TRY disabling ALL syntax style linters, see what the effect is t-linter WIP ✅ ❌ ✅ ✅ ❌ ✅ ❌ labelled WIP
19556 grunweg perf: disable the unused tactic linter awaiting-bench t-linter WIP ✅ ❌ ✅ ✅ ❌ ✅ ❌ labelled WIP
19425 hrmacbeth perf: gcongr forward-reasoning adjustment awaiting-author ✅ ✅ ✅ ✅ ✅ ❌ ❌ awaiting author
16020 adomani feat: compare PR `olean`s size with `master` CI ✅ ❌ ✅ ✅ ✅ ✅ ❌ ⚠️ failing CI
19557 grunweg perf: disable five small syntax style linters awaiting-bench t-linter 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
15649 TpmKranz feat(Computability): introduce Generalised NFA as bridge to Regular Expression t-computability new-contributor awaiting-author ✅ ✅ ✅ ✅ ✅ ❌ ❌ awaiting author
19613 madvorak make only valid `FractionalOperation` possible t-combinatorics ✅ ❌ ✅ ✅ ✅ ✅ ❌ failing CI
19633 grunweg fix(CI): build the Archive and Counterexamples with --wfail also CI awaiting-CI easy delegated ✅ ❌ ✅ ✅ ✅ ❌ ❌ does not pass CI
19972 jjdishere feat(RingTheory): Perfectoid Field t-algebra t-analysis t-topology WIP ✅ ❌ ✅ ✅ ❌ ✅ ❌ labelled WIP
20029 FrederickPu Allow for Config attributes to be set directly new-contributor t-meta WIP ✅ ✅ ✅ ✅ ❌ ✅ ❌ labelled WIP
19573 justus-springer feat(Algebra/Polynomial/Laurent): Lifting maps to ring of Laurent polynomials large-import new-contributor t-algebra delegated ✅ ❌ ✅ ✅ ✅ ✅ ❌ failing CI
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
18893 vihdzp feat(Order/InitialSeg): `InitialSeg.exists_relIso_sum` t-order awaiting-author blocked-by-other-PR ✅ ❌ ❌ ✅ ✅ ❌ ❌ blocked on another PR
20401 RemyDegenne feat: add sigmaFinite_iUnion t-measure-probability awaiting-author ✅ ✅ ✅ ✅ ✅ ❌ ❌ awaiting author
20428 madvorak feat(Data/Sign): lemmas about `∈ Set.range SignType.cast` t-data WIP ✅ ❌ ✅ ✅ ❌ ✅ ❌ labelled WIP
16303 grunweg feat(CI): check for badly formatted titles or missing/contradictory labels CI awaiting-author ✅ ✅ ✅ ✅ ✅ ❌ ❌ ⚠️ awaiting author
20409 vihdzp feat: linear order is isomorphic to lexicographic sum of two intervals t-order ✅ ❌ ✅ ✅ ✅ ✅ ❌ failing CI
18693 Ruben-VandeVelde feat: add ConjRootClass t-algebra awaiting-author ✅ ✅ ✅ ✅ ✅ ❌ ❌ awaiting author
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
19117 eric-wieser feat: derivatives of matrix operations t-analysis WIP ✅ ❌ ✅ ✅ ❌ ✅ ❌ labelled WIP
13483 adomani feat: automatically replace deprecations t-meta delegated 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
19284 adomani test: commit a change only to the "master" CI build action CI awaiting-author ✅ ✅ ✅ ✅ ✅ ❌ ❌ awaiting author
17469 joelriou feat(Algebra/ModuleCat/Differentials/Presheaf): the presheaf of relative differentials large-import t-algebraic-geometry t-category-theory WIP ✅ ❌ ✅ ✅ ❌ ✅ ❌ labelled WIP
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
18437 ADedecker refactor: add refactored APIs for algebraic filter bases t-algebra t-topology 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
20222 eric-wieser feat: generalize lemmas about derivatives t-analysis blocked-by-other-PR ✅ ❌ ❌ ✅ ✅ ✅ ❌ blocked on another PR
16547 CBirkbeck Cot mittag leffler large-import blocked-by-other-PR WIP ✅ ✅ ❌ ✅ ❌ ✅ ❌ blocked on another PR
20818 artie2000 feat(Algebra/Group/Even): Add missing lemmas large-import t-algebra awaiting-author ✅ ❌ ✅ ✅ ✅ ❌ ❌ failing CI
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
21266 ADedecker feat: restate uniformContinuous_mul in terms of convergence to uniformity t-topology easy delegated ✅ ✅ ✅ ✅ ✅ ✅ ✅ delegated
19666 FR-vdash-bot chore: redefine `Nat.bit` and `csimp` lemma for `Nat.bit` t-data awaiting-author ✅ ✅ ✅ ✅ ✅ ❌ ❌ awaiting author
18306 bjoernkjoshanssen feat(Topology/Compactification): projective line over ℝ is homeomorphic to the one-point compactification of ℝ t-topology awaiting-author ✅ ✅ ✅ ✅ ✅ ❌ ❌ awaiting author
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
20520 linesthatinterlace refactor(LinearAlgebra/Lagrange): Remove Lagrange namespace t-algebra awaiting-author ✅ ✅ ✅ ✅ ✅ ❌ ❌ awaiting author
13685 niklasmohrin feat(Combinatorics): add definitions for network flows new-contributor t-combinatorics awaiting-author ✅ ✅ ✅ ✅ ✅ ❌ ❌ awaiting author
21734 adomani fix(PR summary): checkout GITHUB_SHA CI awaiting-author WIP ✅ ✅ ✅ ✅ ❌ ❌ ❌ labelled WIP
19907 kim-em chore: remove some 'nonrec' t-algebra ✅ ❌ ✅ ✅ ✅ ✅ ❌ failing CI
21794 grunweg fix: import the flexible linter in Mathlib.Init large-import t-linter ✅ ❌ ✅ ✅ ✅ ✅ ❌ failing CI
19582 yu-yama feat(GroupExtension/Abelian): define `OfMulDistribMulAction.equivH2` new-contributor t-algebra blocked-by-other-PR ✅ ✅ ❌ ✅ ✅ ✅ ❌ blocked on another PR
21837 yu-yama feat(GroupExtension/Abelian): define `conjClassesEquivH1` t-algebra ✅ ✅ ✅ ✅ ✅ ✅ ✅ awaiting review
21860 vihdzp chore(SetTheory/Ordinal/Enum): enumerator function of closed set is normal t-set-theory ✅ ✅ ✅ ✅ ✅ ✅ ✅ awaiting review
20533 alreadydone feat(PrimeSpectrum): Clopens in spectra of CommSemirings t-algebra t-algebraic-geometry delegated ✅ ✅ ✅ ✅ ✅ ✅ ✅ delegated
15099 joelriou feat(CategoryTheory/Sites): the Mayer-Vietoris long exact sequence in sheaf cohomology t-category-theory WIP ✅ ❌ ✅ ✅ ❌ ✅ ❌ labelled WIP
21265 ADedecker feat: some lemmas about pointwise actions of units on filters and uniformities t-algebra t-topology delegated ✅ ✅ ✅ ✅ ✅ ✅ ✅ delegated
21871 YaelDillies feat: decomposition into independent atoms t-order help-wanted ✅ ❌ ✅ ✅ ❌ ✅ ❌ looking for help
21903 yhtq feat: add from/toList between `FreeSemigroup` and `List` with relative theorems large-import new-contributor t-algebra ✅ ✅ ✅ ✅ ✅ ✅ ✅ awaiting review
21960 jsm28 feat(Geometry/Euclidean/Simplex): simplex angle properties t-euclidean-geometry ✅ ✅ ✅ ✅ ✅ ✅ ✅ awaiting review
20784 eric-wieser fix: prevent `exact?` recursing forever on `n = 55` t-set-theory awaiting-author ✅ ✅ ✅ ✅ ✅ ❌ ❌ awaiting author
21616 peabrainiac feat(Topology): concatenating countably many paths t-topology ✅ ✅ ✅ ✅ ✅ ✅ ✅ awaiting review
20648 anthonyde feat: formalize regular expression -> εNFA t-computability new-contributor ✅ ✅ ✅ ✅ ✅ ✅ ✅ awaiting review
19275 eric-wieser fix: if nolint files change, do a full rebuild delegated ✅ ❌ ✅ ✅ ✅ ✅ ❌ failing CI
22031 adomani feat(zulip): add emoji reaction to first message ✅ ✅ ✅ ✅ ✅ ✅ ✅ ⚠️ awaiting review
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
21065 eric-wieser feat: generalize `tangentConeAt.lim_zero` to TVS t-analysis WIP ✅ ✅ ✅ ✅ ❌ ✅ ❌ labelled WIP
21965 JovanGerb feat: extensible `push`(_neg) tactic - part 1 large-import t-meta ✅ ✅ ✅ ✅ ✅ ✅ ✅ awaiting review
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
21260 chrisflav feat(RingTheory/Presentation): reindex presentations t-algebra ✅ ✅ ✅ ✅ ✅ ✅ ✅ merge conflict
20924 tomaz1502 feat(Computability/QueryComplexity): Oracle-based computation t-computability ✅ ❌ ✅ ✅ ✅ ✅ ❌ failing CI
22216 Rida-Hamadani chore(SimpleGraph): remove redundant import and improve style for `StronglyRegular.lean` t-combinatorics ✅ ✅ ✅ ✅ ✅ ✅ ✅ awaiting review
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
20652 jjaassoonn feat: categorical description of center of a ring t-algebra t-category-theory awaiting-author ✅ ❌ ✅ ✅ ✅ ❌ ❌ failing CI
19062 hannahfechtner feat(Algebra/PresentedMonoid/Basic) : facts about rel t-algebra awaiting-author ✅ ✅ ✅ ✅ ✅ ❌ ❌ awaiting author
21276 GabinKolly feat(ModelTheory/Substructures): define equivalences between equal substructures t-logic awaiting-author ✅ ✅ ✅ ✅ ✅ ❌ ❌ awaiting author
21829 Whysoserioushah feat(LinearAlgebra/TensorProduct/HomTensor): Add TensorProduct of Hom-modules t-algebra ✅ ✅ ✅ ✅ ✅ ✅ ✅ awaiting review
22300 chrisflav feat(RingTheory/GoingDown): lift `LTSeries` of primes blocked-by-other-PR ✅ ❌ ❌ ✅ ✅ ✅ ❌ ⚠️ blocked on another PR
22299 chrisflav chore(Order/RelSeries): induction principle for `RelSeries` t-order ✅ ✅ ✅ ✅ ✅ ✅ ✅ awaiting review
22302 CharredLee feat: add `CategoryTheory.Topos.Power` new-contributor t-category-theory awaiting-author ✅ ✅ ✅ ✅ ✅ ❌ ❌ awaiting author
21744 robin-carlier feat(AlgebraicTopology/SimplexCategory/GeneratorsRelations/NormalForms): admissible lists and simplicial insertion t-topology t-category-theory ✅ ✅ ✅ ✅ ✅ ✅ ✅ awaiting review
22314 shetzl feat: add leftmost derivations for context-free grammars t-computability new-contributor ✅ ✅ ✅ ✅ ✅ ✅ ✅ awaiting review
22330 jjdishere feat(RingTheory/Perfection): lemmas for `frobeniusEquiv.symm` t-algebra blocked-by-other-PR ✅ ✅ ❌ ✅ ✅ ✅ ❌ blocked on another PR
18444 jjdishere feat(Topology/Algebra): Krasner's lemma t-algebra t-analysis t-topology t-number-theory WIP ✅ ❌ ✅ ✅ ❌ ✅ ❌ labelled WIP
22112 tristan-f-r chore(AddCircle/Angle): norm_cast, simp ✅ ❌ ✅ ✅ ✅ ✅ ❌ failing CI
22339 chrisflav feat(RingTheory): base change commutes with finite products t-algebra ✅ ✅ ✅ ✅ ✅ ✅ ✅ awaiting review
22243 luigi-massacci feat(Topology/MetricSpace/Gluing): Inductive limits of separable spaces are separable new-contributor t-topology easy awaiting-author ✅ ✅ ✅ ✅ ✅ ❌ ❌ awaiting author
21869 Raph-DG feat(Order): Trimmed length of a RelSeries new-contributor t-order ✅ ✅ ✅ ✅ ✅ ✅ ✅ awaiting review
17404 YaelDillies chore: Merge the two series of lemmas on big operators in locally finite orders large-import t-order t-algebra WIP ✅ ❌ ✅ ✅ ❌ ✅ ❌ labelled WIP
21915 YaelDillies feat: simproc for `Int.divisorsAntidiag` t-meta WIP ✅ ❌ ✅ ✅ ❌ ✅ ❌ labelled WIP
22415 pechersky feat(Algebra/Order/Hom/Monoid): order iso versions of unitsWithZero and friends t-algebra blocked-by-other-PR ✅ ✅ ❌ ✅ ✅ ✅ ❌ blocked on another PR
22447 joelriou feat(CategoryTheory): the dual of a Guitart exact `2`-square is Guitart exact t-category-theory ✅ ✅ ✅ ✅ ✅ ✅ ✅ awaiting review
22450 joelriou feat(CategoryTheory): left derivability structures t-category-theory blocked-by-other-PR ✅ ✅ ❌ ✅ ✅ ✅ ❌ blocked on another PR
22420 pechersky feat(Order/Prod/Lex/{Hom,Monoid,GroupWithZero}): ordered inclusions and projections of prod of ordered groups t-order t-algebra blocked-by-other-PR ✅ ✅ ❌ ✅ ✅ ✅ ❌ blocked on another PR
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
19860 YaelDillies refactor: review the `simps` projections of `OneHom`, `MulHom`, `MonoidHom` t-algebra awaiting-CI ✅ ❌ ✅ ✅ ✅ ❌ ❌ does not pass CI
22474 joelriou feat(CategoryTheory/Functor): more API for pointwise Kan extensions t-category-theory ✅ ✅ ✅ ✅ ✅ ✅ ✅ awaiting review
22320 jjdishere feat(RingTheory/WittVector): the Teichmuller series t-algebra awaiting-author ✅ ✅ ✅ ✅ ✅ ❌ ❌ awaiting author
22539 joelriou feat(Algebra/Homology): construction of left resolutions t-category-theory ✅ ✅ ✅ ✅ ✅ ✅ ✅ awaiting review
22556 joelriou feat(Algebra/Category/ModuleCat): a functorial projective resolution t-category-theory blocked-by-other-PR ✅ ❌ ❌ ✅ ✅ ✅ ❌ blocked on another PR
22547 joelriou feat(CategoryTheory/Abelian): construction of reduced left resolutions t-category-theory blocked-by-other-PR WIP ✅ ❌ ❌ ✅ ❌ ✅ ❌ blocked on another PR
20504 vihdzp feat: generalize normal functions t-order awaiting-author ✅ ✅ ✅ ✅ ✅ ❌ ❌ awaiting author
22508 joelriou feat(CategoryTheory): existence of right derived functors using derivability structures t-category-theory blocked-by-other-PR WIP ✅ ✅ ❌ ✅ ❌ ✅ ❌ blocked on another PR
22565 chrisflav feat(RingTheory/Flat): descent along faithfully flat ring maps t-algebra ✅ ✅ ✅ ✅ ✅ ✅ ✅ awaiting review
20636 eric-wieser feat: multiplication of intervals in rings t-algebra awaiting-author ✅ ✅ ✅ ✅ ✅ ❌ ❌ awaiting author
22043 YaelDillies chore: shortcut instance for `Neg ℤˣ` t-algebra ✅ ✅ ✅ ✅ ✅ ✅ ✅ awaiting review
19585 joelriou feat(Algebra/Homology/DerivedCategory): the full embedding of an abelian category in its derived category t-category-theory blocked-by-other-PR WIP ✅ ✅ ❌ ✅ ❌ ✅ ❌ blocked on another PR
19591 joelriou feat(CategoryTheory/Abelian): Ext^0 and Ext-groups when there are enough projectives t-category-theory blocked-by-other-PR WIP ✅ ✅ ❌ ✅ ❌ ✅ ❌ blocked on another PR
22576 Ruben-VandeVelde feat: more lemmas about alternatingGroup t-algebra ✅ ✅ ✅ ✅ ✅ ✅ ✅ awaiting review
16000 YaelDillies feat: Croot-Sisask Almost Periodicity t-analysis t-combinatorics blocked-by-other-PR ✅ ✅ ❌ ✅ ✅ ✅ ❌ blocked on another PR
22586 joelriou feat(CategoryTheory/Localization): the right derivability structure given by functorial resolutions t-category-theory ✅ ✅ ✅ ✅ ✅ ✅ ✅ awaiting review
22392 mariainesdff feat(Algebra/Order/Antidiag/Partition): add antidiagonalTwoTwo t-algebra ✅ ✅ ✅ ✅ ✅ ✅ ✅ awaiting review
21765 101damnations feat(RepresentationTheory/GroupCohomology/LongExactSequence): specialise LES API to low degree group cohomology blocked-by-other-PR ✅ ✅ ❌ ✅ ✅ ✅ ❌ ⚠️ blocked on another PR
22611 grunweg feat: disjoint unions distribute with products of manifolds t-differential-geometry please-adopt WIP ✅ ❌ ✅ ✅ ❌ ✅ ❌ looking for help
22642 grunweg WIP: add `mfderiv_prod` and `mfderiv_prodMap` t-differential-geometry WIP ✅ ❌ ✅ ✅ ❌ ✅ ❌ labelled WIP
21603 imbrem feat(CategoryTheory/ChosenFiniteProducts): Added basic ChosenFiniteCoproducts class new-contributor t-category-theory ✅ ✅ ✅ ✅ ✅ ✅ ✅ awaiting review
21525 sinhp feat(CategoryTheory): Locally Cartesian Closed Categories (Prelim) large-import t-category-theory ✅ ✅ ✅ ✅ ✅ ✅ ✅ awaiting review
22319 sinhp feat(CategoryTheory): Locally Cartesian Closed Categories (Sections Right Adjoint) large-import t-category-theory blocked-by-other-PR ✅ ✅ ❌ ✅ ✅ ✅ ❌ blocked on another PR
22321 sinhp feat(CategoryTheory): Locally Cartesian Closed Categories (Definition) large-import t-category-theory blocked-by-other-PR ✅ ✅ ❌ ✅ ✅ ✅ ❌ blocked on another PR
22651 101damnations feat(RepresentationTheory/*): subrepresentations, quotients by subrepresentations, and representations of quotient groups t-algebra ✅ ✅ ✅ ✅ ✅ ✅ ✅ awaiting review
22652 101damnations feat(RepresentationTheory/Coinvariants): the `G ⧸ S`-representation on `A_S` for `A : Rep k G` t-algebra blocked-by-other-PR ✅ ✅ ❌ ✅ ✅ ✅ ❌ blocked on another PR
22653 101damnations feat(RepresentationTheory/GroupCohomology/Functoriality): the degree 1 part of the inflation-restriction exact sequence t-algebra blocked-by-other-PR ✅ ✅ ❌ ✅ ✅ ✅ ❌ blocked on another PR
19584 joelriou feat(Algebra/Homology/DerivedCategory): calculus of fractions t-category-theory ✅ ✅ ✅ ✅ ✅ ✅ ✅ awaiting review
20230 joelriou feat(CategoryTheory): categories of homological complexes are Grothendieck abelian t-category-theory ✅ ✅ ✅ ✅ ✅ ✅ ✅ awaiting review
21237 scholzhannah feat: a weaker definition of compactly generated spaces t-topology ✅ ✅ ✅ ✅ ✅ ✅ ✅ awaiting review
21624 sinhp feat(CategoryTheory): The (closed) monoidal structure on the product category of families of (closed) monoidal categories t-category-theory ✅ ✅ ✅ ✅ ✅ ✅ ✅ awaiting review
21018 markimunro feat(Data/Matrix): add file with key definitions and theorems about elementary row operations t-data new-contributor awaiting-author enhancement ✅ ❌ ✅ ✅ ✅ ❌ ❌ failing CI
22039 YaelDillies feat: simproc for computing `Finset.Ixx` of natural numbers large-import t-meta ✅ ✅ ✅ ✅ ✅ ✅ ✅ awaiting review
22701 ctchou feat(Combinatorics): the Katona circle method new-contributor t-combinatorics ✅ ✅ ✅ ✅ ✅ ✅ ✅ awaiting review
22724 peabrainiac feat(Geometry/Diffeology): diffeologies generated from sets of plots t-differential-geometry blocked-by-other-PR ✅ ✅ ❌ ✅ ✅ ✅ ❌ blocked on another PR
22684 vlad902 feat(Topology): add `ContinuousOn` union API lemmas new-contributor t-topology ✅ ✅ ✅ ✅ ✅ ✅ ✅ awaiting review
8167 sebzim4500 feat: Add new `grw` tactic for rewriting using inequalities. new-contributor t-meta modifies-tactic-syntax ✅ ✅ ✅ ✅ ✅ ✅ ✅ awaiting review
22745 jsm28 feat(LinearAlgebra/AffineSpace/Independent): `faceOpposite` t-algebra ✅ ✅ ✅ ✅ ✅ ✅ ✅ awaiting review
22747 jsm28 feat(LinearAlgebra/AffineSpace/Combination): affine combinations where points take only two values t-algebra ✅ ✅ ✅ ✅ ✅ ✅ ✅ awaiting review
21712 grunweg chore: generalise more lemmas to `ContinuousENorm` carleson awaiting-CI ✅ ❌ ✅ ✅ ✅ ❌ ❌ does not pass CI
22748 joelriou feat(CategoryTheory/Localization): the calculus of fractions that is deduced from an adjunction t-category-theory ✅ ✅ ✅ ✅ ✅ ✅ ✅ awaiting review
22739 joelriou feat(CategoryTheory/Abelian): isomorphisms modulo a Serre class t-category-theory ✅ ✅ ✅ ✅ ✅ ✅ ✅ awaiting review
22404 joelriou feat(Algebra/Homology): connecting a chain complex and a cochain complex t-category-theory ✅ ✅ ✅ ✅ ✅ ✅ ✅ awaiting review
21002 mans0954 feature(Analysis/LocallyConvex/Polar): Show that the polar is weak*-closed and absolutely convex t-analysis awaiting-author ✅ ✅ ✅ ✅ ✅ ❌ ❌ awaiting author
19432 mans0954 feat(LinearAlgebra/QuadraticForm/Basis): Free Tensor product of Quadratic Maps large-import t-algebra blocked-by-other-PR WIP ✅ ❌ ❌ ✅ ❌ ✅ ❌ blocked on another PR
18705 mans0954 feat(Algebra/Module/NestAlgebra): Nest algebras large-import t-order t-algebra awaiting-author ✅ ❌ ✅ ✅ ✅ ❌ ❌ failing CI
16316 mans0954 feat(Analysis/Normed/Module/WeakDual): Banach Dieudonné Lemma WIP ✅ ❌ ✅ ✅ ❌ ✅ ❌ ⚠️ labelled WIP
22751 jsm28 feat(Geometry/Euclidean/SignedDist): signed distance between affine subspace and point t-euclidean-geometry blocked-by-other-PR ✅ ✅ ❌ ✅ ✅ ✅ ❌ blocked on another PR
22741 joelriou feat(CategoryTheory/Abelian/SerreClass): left Bousfield localizations t-category-theory blocked-by-other-PR ✅ ✅ ❌ ✅ ✅ ✅ ❌ blocked on another PR
22127 Raph-DG draft(Module): Module length is additive in short exact sequences new-contributor blocked-by-other-PR WIP ✅ ❌ ❌ ✅ ❌ ✅ ❌ blocked on another PR
22628 scholzhannah feat: finiteness notions on CW complexes t-topology ✅ ✅ ✅ ✅ ✅ ✅ ✅ awaiting review
22792 madvorak Pigeonhole-like results for Fin t-data ✅ ✅ ✅ ✅ ✅ ✅ ✅ awaiting review
22721 grunweg chore(MeasureTheory/Function/LpSeminorm/Basic): generalise more results to enorm classes carleson t-measure-probability WIP ✅ ❌ ✅ ✅ ❌ ✅ ❌ labelled WIP
21476 grunweg feat(lint-style): enable running on downstream projects t-linter awaiting-author ✅ ✅ ✅ ✅ ✅ ❌ ❌ awaiting author
22784 grunweg feat: add Diffeomorph.sumSumSumComm t-differential-geometry WIP ✅ ❌ ✅ ✅ ❌ ✅ ❌ labelled WIP
20681 mitchell-horner feat(Combinatorics/SimpleGraph): define deleteIncidenceSet large-import new-contributor t-combinatorics ✅ ✅ ✅ ✅ ✅ ✅ ✅ awaiting review
18266 bjoernkjoshanssen feat: Second-derivative test from calculus t-analysis awaiting-author ✅ ✅ ✅ ✅ ✅ ❌ ❌ awaiting author
21129 chrisflav perf(RingTheory/Kaehler/JacobiZariski): reorder universe variables performance-hack t-algebra ✅ ✅ ✅ ✅ ✅ ✅ ✅ awaiting review
22809 b-reinke feat: Category algebras and path algebras new-contributor WIP ✅ ❌ ✅ ✅ ❌ ✅ ❌ ⚠️ labelled WIP
22620 ahhwuhu feat: Define shifted Legendre polynomials and prove some basic properties new-contributor t-analysis ✅ ✅ ✅ ✅ ✅ ✅ ✅ awaiting review
22662 plp127 feat: Localization.Away.lift (computably) t-algebra ✅ ✅ ✅ ✅ ✅ ✅ ✅ awaiting review
22483 jsm28 feat(Geometry/Euclidean/Sphere/Tangent): tangents to spheres t-euclidean-geometry ✅ ✅ ✅ ✅ ✅ ✅ ✅ awaiting review
22680 kebekus feat: behavior of AnalyticAt.order under addition t-analysis ✅ ✅ ✅ ✅ ✅ ✅ ✅ awaiting review
22782 alreadydone WIP: etale space associated to a presheaf t-topology WIP ✅ ❌ ✅ ✅ ❌ ✅ ❌ labelled WIP
21985 FernandoChu feat(CategoryTheory): the Grothendieck construction is prefibered large-import new-contributor t-category-theory awaiting-author ✅ ✅ ✅ ✅ ✅ ❌ ❌ awaiting author
21031 YaelDillies chore: get rid of generic hom coercions WIP ✅ ❌ ✅ ✅ ❌ ✅ ❌ labelled WIP
22089 sgouezel feat: composing a continuous multilinear map with continuous linear maps is analytic in both variables t-analysis ✅ ✅ ✅ ✅ ✅ ✅ ✅ awaiting review
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 ✅ ✅ ❌ ✅ ✅ ✅ ❌ blocked on another PR
20263 joelriou feat(CategoryTheory): locally presentable and accessible categories t-category-theory WIP ✅ ❌ ✅ ✅ ❌ ✅ ❌ labelled WIP
22890 BGuillemet feat: add versions of the Lebesgue number lemma new-contributor t-topology ✅ ✅ ✅ ✅ ✅ ✅ ✅ awaiting review
22861 eric-wieser feat: add the trace of a bilinear form t-algebra ✅ ✅ ✅ ✅ ✅ ✅ ✅ awaiting review
22531 vasnesterov feat(Analysis): radius of convergence for `FormalMultilinearSeries.compContinuousLinearMap` t-analysis ✅ ✅ ✅ ✅ ✅ ✅ ✅ awaiting review
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 blocked-by-other-PR ✅ ❌ ❌ ✅ ✅ ✅ ❌ ⚠️ blocked on another PR
22767 robin-carlier feat(AlgebraicTopology/SimplexCategory): the augmented simplex category t-category-theory ✅ ✅ ✅ ✅ ✅ ✅ ✅ awaiting review
22768 robin-carlier feat(AlgebraicTopology/SimplexCategory/Augmented): monoidal structure on `AugmentedSimplexCategory` t-category-theory blocked-by-other-PR ✅ ✅ ❌ ✅ ✅ ✅ ❌ blocked on another PR
8740 digama0 fix: improve `recall` impl / error reporting awaiting-CI t-meta awaiting-author ✅ ❌ ✅ ✅ ✅ ❌ ❌ does not pass CI
22635 Kiolt feat: submonoid of pairs with quotient in a submonoid toric new-contributor t-algebra ✅ ✅ ✅ ✅ ✅ ✅ ✅ awaiting review
19872 YaelDillies chore(GroupTheory/Index): fix names FLT t-algebra ✅ ❌ ✅ ✅ ✅ ✅ ❌ failing CI
16074 Rida-Hamadani feat: combinatorial maps and planar graphs t-combinatorics awaiting-author ✅ ✅ ✅ ✅ ✅ ❌ ❌ awaiting author
21847 smmercuri feat: `v.adicCompletionIntegers K` is compact large-import blocked-by-other-PR WIP ✅ ❌ ❌ ✅ ❌ ✅ ❌ ⚠️ blocked on another PR
22915 pimotte feat(Combinatorics/SimpleGraph): Tutte's theorem t-combinatorics blocked-by-other-PR ✅ ✅ ❌ ✅ ✅ ✅ ❌ awaiting review
22918 chrisflav feat(Algebra/Module): a finite product of finitely presented modules is finitely presented t-algebra ✅ ✅ ✅ ✅ ✅ ✅ ✅ awaiting review
22574 joelriou refactor(CategoryTheory): redefine full subcategories using `ObjectProperty` large-import t-category-theory ✅ ✅ ✅ ✅ ✅ ✅ ✅ awaiting review
22928 javra feat(CategoryTheory): infrastructure for inclusion morphisms into products in categories with 0-morphisms t-category-theory ✅ ❌ ✅ ✅ ✅ ✅ ❌ failing CI
22903 YaelDillies feat: limsups in `ℝ≥0` and `ℝ` agree t-order ✅ ✅ ✅ ✅ ✅ ✅ ✅ awaiting review
22929 b-mehta feat(Order/Cover): characterise covering in Pi types t-order ✅ ✅ ✅ ✅ ✅ ✅ ✅ awaiting review
22933 chrisflav feat(RingTheory/LocalProperties): constructor for `RingHom.OfLocalizationSpan` large-import t-algebra ✅ ✅ ✅ ✅ ✅ ✅ ✅ awaiting review
20380 mans0954 feature(Analysis/NormedSpace/MStructure): The component projections on WithLp 1 (α × β) are L-projections t-analysis awaiting-author ✅ ✅ ✅ ✅ ✅ ❌ ❌ awaiting author
22366 kim-em feat: `check_equalities` tactic for diagnosing defeq problems t-meta delegated ✅ ✅ ✅ ✅ ✅ ✅ ✅ delegated
12251 ScottCarnahan refactor(RingTheory/HahnSeries) : several generalizations t-order t-algebra WIP ✅ ✅ ✅ ✅ ❌ ✅ ❌ labelled WIP
22355 xyzw12345 feat(Algebra/RingQuot): Some lemmas about `RingQuot.mkAlgHom` and `RingQuot.mkRingHom` new-contributor t-algebra ✅ ✅ ✅ ✅ ✅ ✅ ✅ awaiting review
22948 pelicanhere feat(Algebra/DirectSum): morphism of directsum decomposition new-contributor t-algebra ✅ ✅ ✅ ✅ ✅ ✅ ✅ awaiting review
21760 101damnations feat(RepresentationTheory/GroupCohomology/LongExactSequence): specialise LES API to group cohomology t-algebra t-category-theory awaiting-author ✅ ✅ ✅ ✅ ✅ ❌ ❌ awaiting author
22196 xyzw12345 feat: `lie_ring` tactic and `LieReduce` command new-contributor t-meta ✅ ✅ ✅ ✅ ✅ ✅ ✅ awaiting review
22959 ScottCarnahan chore (RingTheory/HahnSeries/SummableFamily): refactor HahnSeries.SummableFamily.powers to take junk values t-algebra ✅ ✅ ✅ ✅ ✅ ✅ ✅ awaiting review
22932 YaelDillies feat: the product of finitely generated monoids is finitely generated toric t-algebra ✅ ✅ ✅ ✅ ✅ ✅ ✅ awaiting review
22962 YaelDillies feat: torsion-free *monoids* toric large-import t-algebra ✅ ✅ ✅ ✅ ✅ ✅ ✅ awaiting review
22970 YaelDillies feat: monoid algebras over domains are domains toric t-algebra ✅ ✅ ✅ ✅ ✅ ✅ ✅ awaiting review
22527 tristan-f-r feat(Finpartition): ofSetSetoid t-combinatorics ✅ ✅ ✅ ✅ ✅ ✅ ✅ awaiting review
22969 plp127 feat(Order/Filter/Map): add `Sum.elim` lemmas blocked-by-other-PR ✅ ✅ ❌ ✅ ✅ ✅ ❌ ⚠️ blocked on another PR
22816 peabrainiac feat(CategoryTheory/Sites): global sections functor on sheaves t-category-theory awaiting-author ✅ ✅ ✅ ✅ ✅ ❌ ❌ awaiting author
22260 ldct feat: Add SampleableExt PNat new-contributor ✅ ✅ ✅ ✅ ✅ ✅ ✅ ⚠️ awaiting review
22954 eric-wieser feat(RingTheory/Congruence/Hom): copy from GroupTheory t-algebra ✅ ❌ ✅ ✅ ✅ ✅ ❌ failing CI
22605 pechersky chore(Analysis): rename pi family from π to X t-analysis ✅ ✅ ✅ ✅ ✅ ✅ ✅ awaiting review
22027 vihdzp chore(SetTheory/Ordinal/FixedPoint); review `Ordinal.nfp` API t-set-theory ✅ ✅ ✅ ✅ ✅ ✅ ✅ awaiting review
22265 Timeroot feat(Geometry/Euclidean/Angle/Unoriented): triangle inequality large-import t-euclidean-geometry awaiting-author ✅ ✅ ✅ ✅ ✅ ❌ ❌ awaiting author
20680 joelriou feat(CategoryTheory): weak factorization systems t-category-theory ✅ ✅ ✅ ✅ ✅ ✅ ✅ awaiting review
22833 adomani feat(CI): add comment on merge-conflict to trigger an email CI ✅ ✅ ✅ ✅ ✅ ✅ ✅ ⚠️ awaiting review
22159 shetzl feat: add definition of pushdown automata t-computability new-contributor awaiting-author ✅ ✅ ✅ ✅ ✅ ❌ ❌ awaiting author
21103 joelriou feat(AlgebraicTopology/SimplicialSet): uniqueness of the decomposition involving non-degenerate simplices t-category-theory ✅ ✅ ✅ ✅ ✅ ✅ ✅ awaiting review
20210 joelriou feat(AlgebraicTopology): application of the retract argument to model categories large-import t-category-theory blocked-by-other-PR ✅ ✅ ❌ ✅ ✅ ✅ ❌ blocked on another PR
22828 joelriou feat(CategoryTheory): parametrized adjunctions t-category-theory ✅ ✅ ✅ ✅ ✅ ✅ ✅ awaiting review
22834 joelriou feat(CategoryTheory): lifting properties and adjunctions of bifunctors t-category-theory blocked-by-other-PR WIP ✅ ✅ ❌ ✅ ❌ ✅ ❌ blocked on another PR
22203 joelriou feat(CategoryTheory/Limits): multicoequalizers attached to linear orders t-category-theory ✅ ✅ ✅ ✅ ✅ ✅ ✅ awaiting review
21026 joelriou feat(CategoryTheory/Limits): certain multicoequalizers are pushouts t-category-theory blocked-by-other-PR ✅ ✅ ❌ ✅ ✅ ✅ ❌ blocked on another PR
20224 joelriou AlgebraicTopology(ModelCategory): a trick by Joyal large-import t-category-theory blocked-by-other-PR ✅ ✅ ❌ ✅ ✅ ✅ ❌ blocked on another PR
22205 joelriou feat(CategoryTheory/Limits): preservation of multicoequalizers t-category-theory ✅ ✅ ✅ ✅ ✅ ✅ ✅ awaiting review
22231 pechersky feat(Algebra/Valued): `AdicExpansion` initial defns t-algebra t-topology ✅ ✅ ✅ ✅ ✅ ✅ ✅ awaiting review
22794 vasnesterov feat(Tactic/NormNum): `norm_num` extension for `Irrational x^y` t-meta ✅ ✅ ✅ ✅ ✅ ✅ ✅ awaiting review
20238 maemre feat(Computability/DFA): Closure of regular languages under some set operations t-computability new-contributor awaiting-author ✅ ✅ ✅ ✅ ✅ ❌ ❌ awaiting author
8047 faenuccio refactor(Util/Delaborators): remove `scoped` from delabPi' awaiting-zulip t-meta ✅ ❌ ✅ ✅ ✅ ❌ ❌ failing CI
22844 grunweg chore(Topology/Constructions): tweak and move `Prod.instNeBotNhdsWithinIoi` t-topology ✅ ✅ ✅ ✅ ✅ ✅ ✅ awaiting review
15989 vihdzp feat(SetTheory/Ordinal/Principal): golf theorems on additively principal ordinals t-set-theory t-logic awaiting-author ✅ ✅ ✅ ✅ ✅ ❌ ❌ awaiting author
21488 imbrem feat(CategoryTheory/Monoidal): premonoidal categories new-contributor t-category-theory ✅ ✅ ✅ ✅ ✅ ✅ ✅ awaiting review
17131 joneugster feat(Tactic/Linter): add unicode linter for unwanted characters large-import t-linter ✅ ✅ ✅ ✅ ✅ ✅ ✅ awaiting review
17129 joneugster feat(Tactic/Linter): add unicode linter for unicode variant-selectors large-import t-linter ✅ ✅ ✅ ✅ ✅ ✅ ✅ awaiting review
22682 grunweg chore(Topology/Homeomorph): split out various constructions tech debt t-topology RFC ✅ ❌ ✅ ✅ ✅ ✅ ❌ failing CI
22579 kvanvels doc(Topology/Defs/Induced): fix comments on three functions related to RestrictGenTopology t-topology awaiting-author documentation ✅ ✅ ✅ ✅ ✅ ❌ ❌ awaiting author
22256 plp127 feat: Metric Spaces are T6 new-contributor t-topology ✅ ✅ ✅ ✅ ✅ ✅ ✅ awaiting review
21234 sven-manthe feat: Descriptive.tree basic API maintainer-merge ✅ ✅ ✅ ✅ ✅ ✅ ✅ ⚠️ awaiting review
21342 YaelDillies refactor(Normed/Group/Quotient): generalise to non-abelian groups t-analysis WIP ✅ ❌ ✅ ✅ ❌ ✅ ❌ labelled WIP
23021 101damnations feat(Data/Finsupp/Basic): add `Finsupp.(un)curry_single` and `@[simps]` to `Finsupp.finsuppProd(L)Equiv` ✅ ✅ ✅ ✅ ✅ ✅ ✅ ⚠️ awaiting review
21732 101damnations feat(RepresentationTheory/*): representations on `Finsupp` t-algebra blocked-by-other-PR ✅ ✅ ❌ ✅ ✅ ✅ ❌ blocked on another PR
22888 plp127 perf: replace `Lean.Expr.swapBVars` with a better? implementation t-meta awaiting-author ✅ ✅ ✅ ✅ ✅ ❌ ❌ awaiting author
22402 pechersky chore(Algebra/Order/Hom): initliaze simps for Order(Add)MonoidFoo t-algebra ✅ ✅ ✅ ✅ ✅ ✅ ✅ awaiting review
21493 mans0954 feat(Order): directed products and upper bounds large-import t-order awaiting-author ✅ ✅ ✅ ✅ ✅ ❌ ❌ awaiting author
22242 pimotte feat(Combinatorics/SimpleGraph): miscellaneous walk lemmas maintainer-merge t-combinatorics ✅ ✅ ✅ ✅ ✅ ✅ ✅ awaiting review
23038 Parcly-Taxel feat: IMO 2015 Q6 IMO ✅ ✅ ✅ ✅ ✅ ✅ ✅ ⚠️ awaiting review
20071 vasnesterov refactor(Data/Seq): reorganize `Seq.lean` t-data ✅ ✅ ✅ ✅ ✅ ✅ ✅ awaiting review
23042 joneugster feat(CategoryTheory/Enriched/Limits): add HasConicalLimitsOfSize.shrink infinity-cosmos t-category-theory WIP ✅ ✅ ✅ ✅ ❌ ✅ ❌ labelled WIP
23034 plp127 feat: `AddMonoidWithOne.toCharZero` t-algebra ✅ ✅ ✅ ✅ ✅ ✅ ✅ awaiting review
17802 vihdzp feat(SetTheory/Ordinal/Veblen): epsilon and gamma ordinals t-set-theory maintainer-merge awaiting-author ✅ ✅ ✅ ✅ ✅ ❌ ❌ awaiting author
23045 YaelDillies chore(LinearIndependent): rename `linearCombination` lemmas toric t-algebra ✅ ✅ ✅ ✅ ✅ ✅ ✅ awaiting review
22464 adomani feat(CI): declarations diff in Lean CI ✅ ✅ ✅ ✅ ✅ ✅ ✅ ⚠️ awaiting review
23048 scholzhannah feat: PartialEquiv on closed sets restricts to closed map t-topology ✅ ✅ ✅ ✅ ✅ ✅ ✅ awaiting review
19475 YaelDillies feat: group markings t-algebra blocked-by-other-PR WIP ✅ ❌ ❌ ✅ ❌ ✅ ❌ blocked on another PR
23057 JovanGerb doc: library note about argument order in instances maintainer-merge ✅ ✅ ✅ ✅ ✅ ✅ ✅ awaiting review
23063 xroblot feat(ZLattice): add `Real.finrank_eq_int_finrank_of_discrete` t-algebra ✅ ✅ ✅ ✅ ✅ ✅ ✅ awaiting review
22956 JovanGerb fix: tactics like `ring_nf` can get confused with bound variables t-meta blocked-by-other-PR ✅ ❌ ❌ ✅ ✅ ✅ ❌ blocked on another PR
22582 vlad902 feat: generalize theorems with linter fixes new-contributor ✅ ✅ ✅ ✅ ✅ ✅ ✅ ⚠️ awaiting review
22824 alreadydone chore: generalize universes for (pre)sheaves of types t-algebraic-geometry ✅ ✅ ✅ ✅ ✅ ✅ ✅ awaiting review
22754 Parcly-Taxel chore: clear more `docBlame` nolints large-import tech debt awaiting-author blocked-by-other-PR documentation ✅ ❌ ❌ ✅ ✅ ❌ ❌ blocked on another PR
22052 FLDutchmann feat(NumberTheory/SelbergSieve): define Lambda-squared sieves and prove important properties t-analysis t-number-theory ✅ ✅ ✅ ✅ ✅ ✅ ✅ awaiting review
23066 ybenmeur feat: more lemmas for Tannaka duality for finite groups new-contributor t-algebra ✅ ✅ ✅ ✅ ✅ ✅ ✅ awaiting review
22971 mbkybky refactor(FieldTheory/KrullTopology): clean up `KrullTopology.lean` t-algebra ✅ ✅ ✅ ✅ ✅ ✅ ✅ awaiting review
20719 gio256 feat(AlgebraicTopology): delaborators for truncated simplicial notations infinity-cosmos t-category-theory t-meta blocked-by-other-PR ✅ ✅ ❌ ✅ ✅ ✅ ❌ blocked on another PR
23102 YaelDillies chore(Set): strengthen `encard_lt_encard` t-data ✅ ✅ ✅ ✅ ✅ ✅ ✅ awaiting review
23105 YaelDillies chore: make sure that simp can prove that a finite set is relatively compact t-topology ✅ ✅ ✅ ✅ ✅ ✅ ✅ awaiting review
21585 tristan-f-r feat(Computability/CFG): lemmas about nonterminals maintainer-merge t-computability ✅ ✅ ✅ ✅ ✅ ✅ ✅ awaiting review
22790 mhk119 feat: Extend `taylor_mean_remainder_lagrange` to `x < x_0` new-contributor t-analysis ✅ ❌ ✅ ✅ ✅ ✅ ❌ failing CI
23026 Paul-Lez feat(Tactic/Simproc/Divisors): add `simproc`s to compute the divisors of a natural number. t-meta blocked-by-other-PR ✅ ❌ ❌ ✅ ✅ ✅ ❌ blocked on another PR
22771 alreadydone feat(Homotopy/Lifting): monodromy of a covering map and lifting criterion t-topology ✅ ✅ ✅ ✅ ✅ ✅ ✅ awaiting review
23132 urkud feat: the separation quotient of a finite module is a finite module t-algebra t-topology ✅ ✅ ✅ ✅ ✅ ✅ ✅ awaiting review
20733 winstonyin feat: solution to ODE is Lipschitz with respect to the initial condition t-dynamics t-analysis blocked-by-other-PR ✅ ✅ ❌ ✅ ✅ ✅ ❌ blocked on another PR
21286 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
21777 winstonyin feat: existence of local flows on manifolds t-differential-geometry blocked-by-other-PR WIP ✅ ✅ ❌ ✅ ❌ ✅ ❌ blocked on another PR
22254 winstonyin feat: $C^1$ vector fields on compact manifolds define global flows t-differential-geometry blocked-by-other-PR WIP ✅ ❌ ❌ ✅ ❌ ✅ ❌ blocked on another PR
21080 loefflerd feat(Topology/UniformSpace): uniform approximation by locally constant functions t-topology ✅ ✅ ✅ ✅ ✅ ✅ ✅ awaiting review
19920 grunweg chore(overview.yaml): mention more differential geometry items t-differential-geometry documentation ✅ ✅ ✅ ✅ ✅ ✅ ✅ awaiting review
21969 peabrainiac feat(Geometry/Diffeology): basics of diffeological spaces t-differential-geometry awaiting-author ✅ ✅ ✅ ✅ ✅ ❌ ❌ awaiting author
23122 YaelDillies feat: grading a flag t-order ✅ ✅ ✅ ✅ ✅ ✅ ✅ awaiting review
23027 ADedecker chore: fix mistake in docstring of `AdicCompletion` t-algebra easy delegated documentation ✅ ✅ ✅ ✅ ✅ ✅ ✅ delegated
23020 YaelDillies feat(Finset): extra `toLeft`/`toRight` API t-data ✅ ✅ ✅ ✅ ✅ ✅ ✅ awaiting review
22059 grunweg feat: manifolds with smooth boundary t-differential-geometry blocked-by-other-PR WIP ✅ ❌ ❌ ✅ ❌ ✅ ❌ blocked on another PR
22786 sgouezel feat: the equiv between the tangent space of the product and the product of the tangent spaces is smooth t-differential-geometry ✅ ✅ ✅ ✅ ✅ ✅ ✅ awaiting review
18091 tukamilano feat: Hoeffding's lemma large-import new-contributor t-measure-probability awaiting-author ✅ ❌ ✅ ✅ ✅ ❌ ❌ failing CI
23147 vlad902 feat: generalize Mathlib.MeasureTheory t-measure-probability ✅ ✅ ✅ ✅ ✅ ✅ ✅ awaiting review
23153 vlad902 feat: generalize Mathlib.Algebra.Order + Polynomial t-algebra ✅ ✅ ✅ ✅ ✅ ✅ ✅ awaiting review
23154 vlad902 feat(Algebra/FreeMonoid): isomorphisms for the free monoid on zero/one generators t-algebra ✅ ✅ ✅ ✅ ✅ ✅ ✅ awaiting review
23018 gio256 feat: subscript and superscript delaborators infinity-cosmos t-meta ✅ ✅ ✅ ✅ ✅ ✅ ✅ awaiting review
22837 joneugster feat(Data/Set/Basic): add subset_iff and not_mem_subset_iff t-set-theory t-data ✅ ✅ ✅ ✅ ✅ ✅ ✅ awaiting review
16239 Rida-Hamadani feat(Geometry/Manifold): orientable manifolds t-differential-geometry awaiting-author ✅ ❌ ✅ ✅ ✅ ❌ ❌ failing CI
23086 qawbecrdtey feat(Mathlib/Dynamics/PeriodicPts/Lemmas): Added lemmas about `periodicPts` on `Fintype` t-dynamics ✅ ✅ ✅ ✅ ✅ ✅ ✅ awaiting review
23074 plp127 feat: `Fact (0 < 1)` and `Fact (0 ≤ 1)` t-algebra ✅ ✅ ✅ ✅ ✅ ✅ ✅ awaiting review
22163 kebekus feat: canonical tensors in inner product spaces t-analysis ✅ ✅ ✅ ✅ ✅ ✅ ✅ awaiting review
23142 joneugster feat(CategoryTheory/Enriched/Limits): add API for HasConicalLimit infinity-cosmos t-category-theory awaiting-author ✅ ✅ ✅ ✅ ✅ ❌ ❌ awaiting author
22925 ggranberry ggranberry : WIP Toeplitz-Hausdorff new-contributor t-analysis awaiting-author help-wanted ✅ ❌ ✅ ✅ ❌ ❌ ❌ looking for help
23173 vlad902 feat: generalize half of Mathlib.RingTheory t-algebra ✅ ✅ ✅ ✅ ✅ ✅ ✅ awaiting review
23111 pechersky feat(Topology/MetricSpace): pseudometrics as bundled functions maintainer-merge t-topology ✅ ✅ ✅ ✅ ✅ ✅ ✅ awaiting review
23187 vlad902 feat: generalize Mathlib.NumberTheory t-number-theory ✅ ✅ ✅ ✅ ✅ ✅ ✅ awaiting review
23192 vlad902 feat: generalize Mathlib.GroupTheory t-algebra ✅ ✅ ✅ ✅ ✅ ✅ ✅ awaiting review
23191 vlad902 feat: generalize Mathlib.FieldTheory t-algebra ✅ ✅ ✅ ✅ ✅ ✅ ✅ awaiting review
23190 vlad902 feat: generalize Mathlib.Algebra.Algebra + Module t-algebra ✅ ✅ ✅ ✅ ✅ ✅ ✅ awaiting review
23193 vlad902 feat: generalize Mathlib.Topology t-topology ✅ ✅ ✅ ✅ ✅ ✅ ✅ awaiting review
23194 vlad902 feat: generalize rest of Mathlib.RingTheory t-algebra ✅ ✅ ✅ ✅ ✅ ✅ ✅ awaiting review
23195 vlad902 feat: generalize Mathlib.Algebra.BigOperators + CharP + Star + misc others t-algebra ✅ ✅ ✅ ✅ ✅ ✅ ✅ awaiting review
23161 mans0954 feature(Data/Finset/RangeDistance): abs_sub_lt_of_mem_finset_range t-data ✅ ✅ ✅ ✅ ✅ ✅ ✅ awaiting review
22278 robin-carlier feat(CategoryTheory/Sums/Basic): functors out of `Sum` t-category-theory ✅ ✅ ✅ ✅ ✅ ✅ ✅ awaiting review
20495 AntoineChambert-Loir feat(Combinatorics/Nullstellensatz): Alon's combinatorial Nullstellensatz t-combinatorics ✅ ✅ ✅ ✅ ✅ ✅ ✅ awaiting review
22279 xyzw12345 feat(RingTheory/GradedAlgebra): homogeneous relation new-contributor t-algebra blocked-by-other-PR ✅ ✅ ❌ ✅ ✅ ✅ ❌ blocked on another PR
23188 riccardobrasca feat: generalize coercion from polynomial to power series to semirings t-algebra ✅ ✅ ✅ ✅ ✅ ✅ ✅ awaiting review
23213 mattrobball chore(RingTheory.Derivation): add a `LinearMapClass` instance t-algebra ✅ ✅ ✅ ✅ ✅ ✅ ✅ awaiting review
23214 mattrobball perf(Module.LinearMap.Defs): deprioritize projections to parents for `SemilinearMapClass` t-algebra ✅ ✅ ✅ ✅ ✅ ✅ ✅ awaiting review
22977 Paul-Lez feat(NumberTheory/Divisors): Define `Nat.divisorsAntidiagonalList` WIP ✅ ❌ ✅ ✅ ❌ ✅ ❌ ⚠️ labelled WIP
22982 Paul-Lez feat(Algebra/MonoidAlgebra/Defs): add simple lemmas about `single` toric easy delegated ✅ ✅ ✅ ✅ ✅ ✅ ✅ ⚠️ delegated
23220 mattrobball refactor(Module.LinearMap.Defs): make `SemilinearMapClass` extend `AddMonoidHomClass` t-algebra ✅ ✅ ✅ ✅ ✅ ✅ ✅ awaiting review
22457 Komyyy feat(Mathlib/Computability/Ackermann): Ackermann function is computable t-computability ✅ ✅ ✅ ✅ ✅ ✅ ✅ awaiting review
21966 vasnesterov feat(Tactic/Order): support `⊤`, `⊥`, and lattice operations large-import t-meta ✅ ✅ ✅ ✅ ✅ ✅ ✅ awaiting review
23082 Parcly-Taxel chore: clear `docBlame` nolints in `CategoryTheory` tech debt t-category-theory documentation ✅ ✅ ✅ ✅ ✅ ✅ ✅ awaiting review
22864 urkud chore(TorusIntegral): fix porting note t-measure-probability ✅ ✅ ✅ ✅ ✅ ✅ ✅ awaiting review
23231 urkud feat(LinearPMap): more lemmas about `supSpanSingleton` t-algebra ✅ ✅ ✅ ✅ ✅ ✅ ✅ awaiting review
23232 urkud chore(Dimension/Finrank): golf, reuse `variable`s t-algebra ✅ ✅ ✅ ✅ ✅ ✅ ✅ awaiting review
23233 urkud chore(Basis): split `Submodule.exists_le_ker_of_lt_top` t-algebra blocked-by-other-PR ✅ ✅ ❌ ✅ ✅ ✅ ❌ blocked on another PR
23235 urkud feat(StrongRankCondition): linear combinations with bounded number of terms t-algebra ✅ ✅ ✅ ✅ ✅ ✅ ✅ awaiting review
22178 jsm28 feat(Analysis/Convex/BetweenList): betweenness for lists of points t-analysis ✅ ✅ ✅ ✅ ✅ ✅ ✅ awaiting review
7596 alreadydone feat: covering maps from properly discontinuous actions and discrete subgroups t-topology awaiting-author blocked-by-other-PR ✅ ✅ ❌ ✅ ✅ ❌ ❌ blocked on another PR
11563 YaelDillies feat: `∑ i ∈ s with hi : p i, f i hi` syntax for big operators t-algebra t-meta ✅ ✅ ✅ ✅ ✅ ✅ ✅ awaiting review
18861 YaelDillies refactor: make `Set.mem_graphOn` defeq t-data awaiting-author ✅ ❌ ✅ ✅ ✅ ❌ ❌ failing CI
22048 YaelDillies feat: delaborator for `∑ x ∈ s with p x, f x` notation t-meta ✅ ✅ ✅ ✅ ✅ ✅ ✅ awaiting review
23240 urkud feat(Topology/Maps): `IsOpenMap` and `ClusterPt` t-topology delegated ✅ ✅ ✅ ✅ ✅ ✅ ✅ delegated
23255 jsm28 refactor(LinearAlgebra/AffineSpace/AffineSubspace): `affineSpan` analogues of `spanPoints` lemmas t-algebra ✅ ✅ ✅ ✅ ✅ ✅ ✅ awaiting review
23265 jcommelin chore(scripts/merge-lean-testing-pr): push to github after successful merge ✅ ✅ ✅ ✅ ✅ ✅ ✅ awaiting review
23254 mariainesdff feat(Data/NNReal/Basic): add multiset_prod_le_pow_card t-analysis ✅ ✅ ✅ ✅ ✅ ✅ ✅ awaiting review
23268 mariainesdff feat(Analysis/Normed/Unbundled/RingSeminorm): add RingNorm.to_normedRing t-analysis ✅ ✅ ✅ ✅ ✅ ✅ ✅ awaiting review
19607 madvorak Block matrix totally unimodular blocked-by-other-PR WIP ✅ ❌ ❌ ✅ ❌ ✅ ❌ blocked on another PR
23261 Vierkantor chore(*): replace `@[simp, nolint simpNF]` with `@[simp high]` for specialized lemmas tech debt ✅ ✅ ✅ ✅ ✅ ✅ ✅ awaiting review
23238 YaelDillies feat: extended floor and ceil t-algebra ✅ ✅ ✅ ✅ ✅ ✅ ✅ awaiting review
23285 AntoineChambert-Loir refactor: directed systems in terms of functors large-import t-algebra t-category-theory WIP ✅ ❌ ✅ ✅ ❌ ✅ ❌ labelled WIP
22966 alreadydone feat(RingTheory): rank of rational function field extension t-algebra ✅ ✅ ✅ ✅ ✅ ✅ ✅ awaiting review
23236 alreadydone chore(Topology/Instances/AddCircle): golf and little lemmas t-algebra ✅ ✅ ✅ ✅ ✅ ✅ ✅ awaiting review
23274 jcommelin chore(ci): report dependency changes in lake update notifications CI ✅ ✅ ✅ ✅ ✅ ✅ ✅ awaiting review
23293 mans0954 refactor(Algebra/Polynomial/Roots): nthRoots as a Finset t-algebra ✅ ✅ ✅ ✅ ✅ ✅ ✅ awaiting review
23298 joelriou feat(CategoryTheory): stability properties of morphisms properties in functor categories t-category-theory ✅ ✅ ✅ ✅ ✅ ✅ ✅ awaiting review
23299 DavidLedvinka feat(Analysis): add `mlconvolution` and `lconvolution`, Convolution with the Lebesgue integral new-contributor t-analysis ✅ ✅ ✅ ✅ ✅ ✅ ✅ awaiting review
23162 mans0954 feature(Analysis/SpecialFunctions/Complex/Log): exp_mul_I_injOn t-analysis ✅ ✅ ✅ ✅ ✅ ✅ ✅ awaiting review
23266 mariainesdff feat(Algebra/Order/BigOperator): add lemmas large-import t-order t-algebra ✅ ✅ ✅ ✅ ✅ ✅ ✅ awaiting review
17627 hrmacbeth feat: universal properties of vector bundle constructions t-differential-geometry ✅ ✅ ✅ ✅ ✅ ✅ ✅ awaiting review
8738 grunweg feat: differential of a local diffeomorphism is a continuous linear equivalence t-differential-geometry ✅ ✅ ✅ ✅ ✅ ✅ ✅ awaiting review
20704 winstonyin feat: existence of local flows of vector fields t-dynamics t-analysis ✅ ✅ ✅ ✅ ✅ ✅ ✅ awaiting review
22365 euprunin feat: register more tactics for `hint` large-import awaiting-zulip t-meta ✅ ✅ ✅ ✅ ✅ ❌ ❌ awaiting a zulip discussion
23088 Vierkantor feat(Tactic/Linter): a linter for directory dependencies large-import t-linter RFC ✅ ✅ ✅ ✅ ✅ ✅ ✅ awaiting review
22069 Raph-DG feat(LinearMap): Added lemmas relating kernels of linear maps to Submodule.map new-contributor t-algebra ✅ ✅ ✅ ✅ ✅ ✅ ✅ awaiting review
23280 mattrobball chore(Ring.Defs): remove `Ring.toSemiring` t-algebra ✅ ✅ ✅ ✅ ✅ ✅ ✅ awaiting review
23270 Vierkantor refactor(MeasureTheory): fix `simp` not applying `measurableSet_inf` tech debt t-measure-probability ✅ ✅ ✅ ✅ ✅ ✅ ✅ awaiting review
23065 ybenmeur feat: lemma `eval_of_algHom` new-contributor t-algebra ✅ ✅ ✅ ✅ ✅ ✅ ✅ awaiting review
22176 ybenmeur feat: Tannaka duality for finite groups new-contributor t-algebra blocked-by-other-PR ✅ ✅ ❌ ✅ ✅ ✅ ❌ blocked on another PR
22777 xroblot feat(NumberField/CanonicalEmbedding/NormLeOne): compute the volume of `NormLeOne` t-number-theory ✅ ✅ ✅ ✅ ✅ ✅ ✅ awaiting review
22882 xroblot feat(NumberField/Units): add `regOfFamily` and refactor `regulator` t-number-theory ✅ ✅ ✅ ✅ ✅ ✅ ✅ awaiting review
13918 mans0954 feat(Topology/Order/HullKernel): Add the Hull-Kernel Topology t-order t-topology awaiting-author ✅ ✅ ✅ ✅ ✅ ❌ ❌ awaiting author
23312 xroblot feat(NumberField/Units): prove that a family of units is of max rank iff its closure has finite index t-number-theory blocked-by-other-PR ✅ ✅ ❌ ✅ ✅ ✅ ❌ blocked on another PR
23205 xroblot feat(QuotientGroup): surjectivity and kernel of `QuotientGroup.map` t-algebra ✅ ✅ ✅ ✅ ✅ ✅ ✅ awaiting review
23331 kebekus feat: define the divisor of an analytic function t-analysis ✅ ✅ ✅ ✅ ✅ ✅ ✅ awaiting review
22727 grunweg feat: rewrite the isolated by and colon linters in Lean t-linter ✅ ✅ ✅ ✅ ✅ ✅ ✅ awaiting review
23323 jsm28 feat(Geometry/Euclidean/Basic): orthogonal projection onto singleton t-euclidean-geometry ✅ ✅ ✅ ✅ ✅ ✅ ✅ awaiting review
21088 erdOne feat(RingTheory): `dim R + 1 ≤ dim R[X]` t-algebra ✅ ✅ ✅ ✅ ✅ ✅ ✅ awaiting review
21944 Thmoas-Guan feat(RingTheory/Powerseries): Weierstrass preparation for complete local ring t-algebra ✅ ✅ ✅ ✅ ✅ ✅ ✅ awaiting review
21859 Thmoas-Guan feat(RingTheory/Powerseries): Weierstrass preparation t-algebra blocked-by-other-PR ✅ ✅ ❌ ✅ ✅ ✅ ❌ blocked on another PR
23335 kim-em chore: a UniformSpace erw t-topology ✅ ✅ ✅ ✅ ✅ ✅ ✅ awaiting review
15906 grunweg feat: define singular manifolds t-differential-geometry ✅ ❌? ✅ ✅ ✅ ✅ ❌ infrastructure-related CI failing
23186 grunweg feat: split continuous linear maps t-analysis WIP ✅ ❌ ✅ ✅ ❌ ✅ ❌ labelled WIP
23338 WilliamCoram feat: Restricted powerseries form a ring new-contributor t-number-theory ✅ ❌ ✅ ✅ ✅ ✅ ❌ failing CI
21522 riccardobrasca feat: add Mathlib.RingTheory.DedekindDomain.Instances large-import t-algebra ✅ ✅ ✅ ✅ ✅ ✅ ✅ awaiting review
20887 alreadydone feat(Algebra): Transcendence degree t-algebra ✅ ✅ ✅ ✅ ✅ ✅ ✅ awaiting review
22488 smmercuri fix: lower priority for `UniformSpace.Completion.instSMul` FLT t-topology ✅ ✅ ✅ ✅ ✅ ✅ ✅ awaiting review
23346 joelriou chore(CategoryTheory/Limits): split Types.lean t-category-theory ✅ ✅ ✅ ✅ ✅ ✅ ✅ awaiting review
22884 tannerduve feat(Computability/TuringDegrees): define oracle computability and Turing degrees t-computability new-contributor ✅ ✅ ✅ ✅ ✅ ✅ ✅ awaiting review
23336 kim-em chore: `erw` in `Topology/Order/` t-topology ✅ ✅ ✅ ✅ ✅ ✅ ✅ awaiting review
23284 kbuzzard feat(Algebra/BigOperators/Finprod): add finprod_mem_eq_prod variant t-algebra awaiting-author ✅ ✅ ✅ ✅ ✅ ❌ ❌ awaiting author
23360 kim-em chore: review of `erw` in `Algebra/Homology/DerivedCategory` ✅ ✅ ✅ ✅ ✅ ✅ ✅ awaiting review
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
22705 Thmoas-Guan feat(Algebra/DirectSum): add lemma about ker and range of DirectSum.map t-algebra ✅ ✅ ✅ ✅ ✅ ✅ ✅ awaiting review
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 alghom 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
22961 xroblot feat(ZLattice/Covolume): add `covolume_div_covolume_eq_relindex` t-algebra ✅ ✅ ✅ ✅ ✅ ✅ ✅ awaiting review
23363 kebekus feat: congruence lemmas for divisors of meromorphic functions t-analysis ✅ ✅ ✅ ✅ ✅ ✅ ✅ awaiting review
18578 mans0954 feat(LinearAlgebra/QuadraticForm/Basis): basis expansion of a quadratic map maintainer-merge t-algebra ✅ ✅ ✅ ✅ ✅ ✅ ✅ awaiting review
22119 pimotte feat(Combinatorics/SimpleGraph): part of Tutte's theorem t-combinatorics awaiting-author ✅ ✅ ✅ ✅ ✅ ❌ ❌ awaiting author
23364 joelriou refactor(CategoryTheory/Limits): colimits in Type t-category-theory blocked-by-other-PR WIP ✅ ❌ ❌ ✅ ❌ ✅ ❌ blocked on another PR
22655 YaelDillies refactor: make use of `FunLike` for `Submonoid.LocalizationMap` toric t-algebra ✅ ✅ ✅ ✅ ✅ ✅ ✅ awaiting review
22904 YaelDillies feat: additivise `Irreducible` toric t-algebra ✅ ✅ ✅ ✅ ✅ ✅ ✅ awaiting review
23181 YaelDillies chore(UniformSpace/Defs): move entourages to their own file t-topology ✅ ✅ ✅ ✅ ✅ ✅ ✅ awaiting review
22639 b-reinke feat(Mathlib/GroupTheory/FreeGroup): theory of (cyclically) reduced words new-contributor t-algebra blocked-by-other-PR ✅ ✅ ❌ ✅ ✅ ✅ ❌ blocked on another PR
19668 YaelDillies refactor: define `≤`/`<` on `WithBot`/`WithTop` by induction t-order ✅ ✅ ✅ ✅ ✅ ✅ ✅ awaiting review
23370 kebekus feat: taking the divisor of a meromorphic function commutes with restriction t-analysis ✅ ✅ ✅ ✅ ✅ ✅ ✅ awaiting review
23366 b-reinke feat(GroupTheory/FreeGroup/Basic): add lemmas for invRev t-geometric-group-theory t-algebra ✅ ✅ ✅ ✅ ✅ ✅ ✅ awaiting review
23367 b-reinke feat(GroupTheory/FreeGroup/Reduce): add lemmas for toWord and reduce t-geometric-group-theory t-algebra ✅ ✅ ✅ ✅ ✅ ✅ ✅ awaiting review
23368 b-reinke feat(GroupTheory/FreeGroup/ReducedWords): add theory of reduced words t-geometric-group-theory t-algebra ✅ ✅ ✅ ✅ ✅ ✅ ✅ awaiting review
22137 grunweg feat: `IsEmbedding.sumElim_of_separatingNhds` new-contributor t-topology awaiting-author blocked-by-other-PR ✅ ❌ ❌ ✅ ✅ ❌ ❌ blocked on another PR
22898 AntoineChambert-Loir feat(RingTheory/TensorProduct/DirectLimit/FG): direct limit of finitely generated submodules and tensor product t-algebra WIP ✅ ✅ ✅ ✅ ❌ ✅ ❌ labelled WIP
23228 jhanschoo feat(Data/Int): `m/n/k=m/(n*k)` t-data awaiting-author ✅ ✅ ✅ ✅ ✅ ❌ ❌ awaiting author
23374 xroblot feat(NumberField/Units): compute index of unit subgroups using regulators blocked-by-other-PR ✅ ✅ ❌ ✅ ✅ ✅ ❌ ⚠️ blocked on another PR
23282 joelriou feat(CategoryTheory): monomorphisms in Type are stable under transfinite compositions t-category-theory ✅ ✅ ✅ ✅ ✅ ✅ ✅ awaiting review
23373 apnelson1 feat(Data/Matroid/Loop): matroid coloops t-data ✅ ✅ ✅ ✅ ✅ ✅ ✅ awaiting review
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 ✅ ✅ ✅ ✅ ✅ ✅ ✅ awaiting review
22881 Champitoad feat(CategoryTheory/Topos): add representability results for subobject classifier large-import new-contributor t-category-theory ✅ ✅ ✅ ✅ ✅ ✅ ✅ awaiting review
23252 mariainesdff feat(Algebra/Polynomial): add lemmas t-algebra ✅ ✅ ✅ ✅ ✅ ✅ ✅ awaiting review
22919 plp127 feat(Combinatorics/SimpleGraph/Coloring): Make `Fintype` instance for graph colorings computable t-combinatorics ✅ ✅ ✅ ✅ ✅ ✅ ✅ awaiting review
9820 jjaassoonn feat(RingTheory/GradedAlgebra/HomogeneousIdeal): generalize to homogeneous submodule t-algebra ✅ ❌ ✅ ✅ ✅ ✅ ❌ failing CI
23349 BGuillemet feat: add LocallyLipschitzOn.lipschitzOnWith_of_isCompact and two small lemmas about Lipschitz functions large-import new-contributor t-topology blocked-by-other-PR ✅ ✅ ❌ ✅ ✅ ✅ ❌ blocked on another PR
23198 robin-carlier feat(CategoryTheory/Equivalence): functoriality of symmetry of equivalences t-category-theory blocked-by-other-PR ✅ ✅ ❌ ✅ ✅ ✅ ❌ blocked on another PR
21344 kbuzzard chore: attempt to avoid diamond in OreLocalization t-algebra awaiting-author ✅ ❌ ✅ ✅ ✅ ❌ ❌ failing CI
23197 robin-carlier feat(CategoryTheory/Equivalences): category structure on equivalences t-category-theory ✅ ✅ ✅ ✅ ✅ ✅ ✅ awaiting review
22327 YaelDillies chore: deprecate former interaction of finite intervals and succ/pred lemmas large-import t-order WIP ✅ ❌ ✅ ✅ ❌ ✅ ❌ labelled WIP
22870 kebekus feat: behavior of MeromorphicAt.order under powers and inverses t-analysis ✅ ✅ ✅ ✅ ✅ ✅ ✅ awaiting review
23377 apnelson1 feat(Matroid/Rank): ENat-valued matroid rank t-data ✅ ✅ ✅ ✅ ✅ ✅ ✅ awaiting review
23347 loefflerd feat(Analysis/Asymptotics): generalize asymptotics results to `NormMulClass` t-analysis ✅ ✅ ✅ ✅ ✅ ✅ ✅ awaiting review
23384 feixieliz proof for multiplicative group of a finite field is cyclic ❌ ??? ✅ ✅ ✅ ✅ ❌ opened from a fork
20668 gio256 refactor(AlgebraicTopology/SimplicialSet): truncated paths infinity-cosmos t-category-theory ✅ ✅ ✅ ✅ ✅ ✅ ✅ awaiting review
23387 digama0 feat(Cache): root hash generation counter CI ✅ ✅ ✅ ✅ ✅ ✅ ✅ ⚠️ awaiting review
23388 tristan-f-r chore: proof_wanted on conway's 99 graph problem t-combinatorics easy ✅ ✅ ✅ ✅ ✅ ✅ ✅ awaiting review
23393 kebekus chore: fix minor typo t-analysis ✅ ✅ ✅ ✅ ✅ ✅ ✅ awaiting review
23381 vlad902 feat: copy Subgroup lemma for Submonoid t-algebra ✅ ✅ ✅ ✅ ✅ ✅ ✅ awaiting review
23217 acmepjz chore(AlgebraicGeometry/EllipticCurve/*): refactor VariableChange t-algebraic-geometry ✅ ✅ ✅ ✅ ✅ ✅ ✅ awaiting review
21479 jt496 feat(Combinatorics/SimpleGraph): add facts about cliques and colorings of completeMultipartiteGraph large-import t-combinatorics ✅ ✅ ✅ ✅ ✅ ✅ ✅ awaiting review
22974 YaelDillies refactor: use a junk value for the analytic order of a non-analytic function t-analysis ✅ ✅ ✅ ✅ ✅ ✅ ✅ awaiting review
23395 kim-em chore: review erw in Algebra/Homology t-algebra ✅ ✅ ✅ ✅ ✅ ✅ ✅ awaiting review
23049 YaelDillies feat: kill copies of a graph t-combinatorics ✅ ✅ ✅ ✅ ✅ ✅ ✅ awaiting review
22085 IvanRenison feat(Combinatorics/SimpleGraph): introduce `ConnectedComponent.toSimpleGraph` t-combinatorics ✅ ✅ ✅ ✅ ✅ ✅ ✅ awaiting review
22964 plp127 feat(Data/Set/Image): `Sum.elim` lemmas t-data awaiting-author blocked-by-other-PR ✅ ❌ ❌ ✅ ✅ ❌ ❌ blocked on another PR
23204 mariainesdff feat(Data/List/MinMax): add le_max_of_le' t-data ✅ ✅ ✅ ✅ ✅ ✅ ✅ awaiting review
23178 mariainesdff feat: add iSup lemmas large-import t-order ✅ ✅ ✅ ✅ ✅ ✅ ✅ awaiting review
23184 mariainesdff feat(Analysis/Normed/Unbundled/AlgNormOfGalois): add algNorm_of_galois large-import t-analysis t-number-theory blocked-by-other-PR ✅ ✅ ❌ ✅ ✅ ✅ ❌ blocked on another PR
22703 D-Thomine feat(Analysis/Asymptotics/ExpGrowth): Exponential growth and composition t-analysis delegated ✅ ✅ ✅ ✅ ✅ ✅ ✅ delegated
23396 Ruben-VandeVelde chore: split LocallyFinite results out of Compactness.Compact t-topology ✅ ✅ ✅ ✅ ✅ ✅ ✅ awaiting review
13349 CBirkbeck feat: TendstoUniformlyOn for tprod's t-analysis ✅ ✅ ✅ ✅ ✅ ✅ ✅ awaiting review
11968 JovanGerb feat: improvements to RefinedDiscrTree new-contributor t-meta ✅ ✅ ✅ ✅ ✅ ✅ ✅ awaiting review
23386 AntoineChambert-Loir feat(GroupTheory/GroupAction/MultiplePretransitivity): define multiply transitive actions t-algebra ✅ ✅ ✅ ✅ ✅ ✅ ✅ awaiting review
19783 JakobStiefel feat: definition and properties of characteristic functions large-import new-contributor t-measure-probability awaiting-author ✅ ✅ ✅ ✅ ✅ ❌ ❌ awaiting author
20671 thefundamentaltheor3m feat(Analysis/Asymptotics/SpecificAsymptotics): Proving that 𝛔ₖ(n) = O(nᵏ⁺¹) large-import new-contributor t-number-theory awaiting-author ✅ ✅ ✅ ✅ ✅ ❌ ❌ awaiting author
23179 vlad902 feat: generalize Mathlib.LinearAlgebra t-algebra ✅ ✅ ✅ ✅ ✅ ✅ ✅ awaiting review
23409 ocfnash feat: add a criterion for a set of roots to span an irreducible root system t-algebra ✅ ✅ ✅ ✅ ✅ ✅ ✅ awaiting review
23251 mariainesdff feat(FieldTheory/IntermediateField/Adjoin): add lemmas t-algebra ✅ ✅ ✅ ✅ ✅ ✅ ✅ awaiting review
23408 faenuccio feat(RingTheory/Valuation): add two lemmas about non-units in valuation subrings t-algebra t-number-theory ✅ ✅ ✅ ✅ ✅ ✅ ✅ awaiting review
23401 Ruben-VandeVelde chore: split IsTopologicalBasis results out of Compactness.Compact longest-pole t-topology ✅ ✅ ✅ ✅ ✅ ✅ ✅ awaiting review
22443 emilyriehl feat(Category Theory): unbundled quiver adjunction data infinity-cosmos t-category-theory ✅ ✅ ✅ ✅ ✅ ✅ ✅ awaiting review
11768 JovanGerb feat: Interactive Library Rewrite new-contributor t-meta blocked-by-other-PR ✅ ✅ ❌ ✅ ✅ ✅ ❌ blocked on another PR
23411 PatrickMassot chore: remove finiteness from Order.Filter.Lift longest-pole t-topology ✅ ✅ ✅ ✅ ✅ ✅ ✅ awaiting review
23412 robin-carlier feat(CategoryTheory): joins of categories t-category-theory ✅ ✅ ✅ ✅ ✅ ✅ ✅ awaiting review
23413 robin-carlier feat(CategoryTheory/Join): Pseudofunctoriality of joins of categories t-category-theory blocked-by-other-PR ✅ ✅ ❌ ✅ ✅ ✅ ❌ blocked on another PR
23324 Parcly-Taxel chore: deprime `induction'` with 5+ named variables tech debt ✅ ❌ ✅ ✅ ✅ ✅ ❌ failing CI
16596 urkud feat: orbits of an irrational rotation are dense t-dynamics t-topology ✅ ✅ ✅ ✅ ✅ ✅ ✅ awaiting review
23146 vlad902 feat: generalize Mathlib.Data t-data ✅ ✅ ✅ ✅ ✅ ✅ ✅ awaiting review
23371 grunweg chore: mark `Disjoint.{eq_bot, inter_eq}` simp bench-after-CI awaiting-CI ✅ ❌ ✅ ✅ ✅ ❌ ❌ does not pass CI
21162 smmercuri feat: add `Valued.WithZeroMulInt.tendsto_zero_pow_of_le_neg_one` and applications to `adicCompletion K v` t-algebra ✅ ✅ ✅ ✅ ✅ ✅ ✅ awaiting review
21270 GabinKolly feat(ModelTheory/Bundled): first-order embeddings and equivalences from equalities large-import t-logic awaiting-author ✅ ✅ ✅ ✅ ✅ ❌ ❌ awaiting author
19865 mitchell-horner feat(Combinatorics/SimpleGraph): define extremalNumber new-contributor t-combinatorics awaiting-author ✅ ✅ ✅ ✅ ✅ ❌ ❌ awaiting author
23167 fbarroero feat(Analysis/SpecialFunctions/Complex/Log): some basic facts about `circleMap` t-measure-probability t-analysis awaiting-author ✅ ✅ ✅ ✅ ✅ ❌ ❌ awaiting author
22361 rudynicolop feat(Computability/NFA): nfa closure properties t-computability new-contributor awaiting-author ✅ ✅ ✅ ✅ ✅ ❌ ❌ awaiting author
23419 Parcly-Taxel chore: deprime `induction'` with 5+ variables, part 1 tech debt ✅ ✅ ✅ ✅ ✅ ✅ ✅ awaiting review
23424 YaelDillies chore: move `StrictMonoOn f s → InjOn f s` earlier large-import t-order ✅ ✅ ✅ ✅ ✅ ✅ ✅ awaiting review
20315 erdOne feat(RingTheory): homogeneous localization away from an element is of finite type large-import t-algebra ✅ ✅ ✅ ✅ ✅ ✅ ✅ awaiting review
22050 IvanRenison feat(Combinatorics/SimpleGraph): Add `SimpleGraph.Preconnected.support_eq_univ` t-combinatorics ✅ ✅ ✅ ✅ ✅ ✅ ✅ awaiting review
23309 kkytola feat: left/right order-continuous functions are left/right topology-continuous t-order ✅ ✅ ✅ ✅ ✅ ✅ ✅ awaiting review
23436 robin-carlier feat(CategoryTheory/Core): functors and natural transformations induced on cores t-category-theory ✅ ✅ ✅ ✅ ✅ ✅ ✅ awaiting review
23423 jano-wol feat(RingTheory/Nilpotent): prepare exp calculations t-algebra ✅ ✅ ✅ ✅ ✅ ✅ ✅ awaiting review
23124 YaelDillies feat(MetricSpace): nets t-topology blocked-by-other-PR ✅ ✅ ❌ ✅ ✅ ✅ ❌ blocked on another PR
23206 urkud feat(EGauge): add `egauge_pi` and `egauge_prod` t-analysis ✅ ✅ ✅ ✅ ✅ ✅ ✅ awaiting review
23407 Vierkantor refactor(Data): split off material on `Set.Pairwise` from `List.Nodup` t-data longest-pole delegated ✅ ✅ ✅ ✅ ✅ ✅ ✅ delegated
23385 bsubercaseaux feat(Combinatorics/SimpleGraph/Prod): add edist lemmas about graph box product large-import new-contributor t-combinatorics awaiting-author ✅ ✅ ✅ ✅ ✅ ❌ ❌ awaiting author
23337 kebekus feat: meromorphic functions in normal form on sets maintainer-merge t-analysis ✅ ✅ ✅ ✅ ✅ ✅ ✅ awaiting review
23440 xroblot chore(NumberField/Units): make `torsionOrder` a `Nat` t-number-theory ✅ ✅ ✅ ✅ ✅ ✅ ✅ awaiting review
23055 FLDutchmann feat(Analysis/Asymptotics): `=O[atTop]` for sequences implies `=O[l]` for any filter `l` t-analysis delegated ✅ ✅ ✅ ✅ ✅ ✅ ✅ delegated
23334 Ruben-VandeVelde feat: add lemmas about Field.toEuclideanDomain t-algebra ✅ ✅ ✅ ✅ ✅ ✅ ✅ awaiting review
23414 robin-carlier feat(CategoryTheory/Join): finality/initiality of the inclusions t-category-theory blocked-by-other-PR ✅ ✅ ❌ ✅ ✅ ✅ ❌ blocked on another PR
13861 BoltonBailey feat(Data/Finsupp/Basic): `Finsupp.optionElim'` t-data ✅ ✅ ✅ ✅ ✅ ✅ ✅ awaiting review
23244 eric-wieser chore(GroupTheory/Congruence): deduplicate `ker` and `mulKer` t-algebra ✅ ✅ ✅ ✅ ✅ ✅ ✅ awaiting review
23427 eric-wieser feat(Data/Fin/Tuple/Reflection): multiplicativize t-data ✅ ✅ ✅ ✅ ✅ ✅ ✅ awaiting review
21539 Raph-DG feat(LinearAlgebra): Symmetric Algebra new-contributor t-algebra ✅ ✅ ✅ ✅ ✅ ✅ ✅ awaiting review
23209 wwylele feat(Analysis): add improper integral of complex exp new-contributor t-analysis ✅ ✅ ✅ ✅ ✅ ✅ ✅ awaiting review
22078 Louddy feat(SkewMonoidAlgebra): multiplication and algebraic instances large-import new-contributor t-algebra awaiting-author ✅ ✅ ✅ ✅ ✅ ❌ ❌ awaiting author
23446 acmepjz feat(Algebra/Exact): add `Function.Exact.[iff_]rangeFactorization` etc t-algebra ✅ ✅ ✅ ✅ ✅ ✅ ✅ awaiting review
23069 JovanGerb perf: use `singlePass := true` in main loop of `ring_nf` t-meta ✅ ✅ ✅ ✅ ✅ ✅ ✅ awaiting review
12290 yoh-tanimoto feat(MeasureTheory/Integral): the Riesz-Markov-Kakutani theorem for `Real`-linear functionals new-contributor t-measure-probability awaiting-author ✅ ❌ ✅ ✅ ✅ ❌ ❌ failing CI
23439 YaelDillies chore(SimpleGraph/Prod): correct lemma names t-combinatorics ✅ ✅ ✅ ✅ ✅ ✅ ✅ awaiting review
23447 YaelDillies chore(Order/Circular): golf large-import t-order ✅ ❌ ✅ ✅ ✅ ✅ ❌ failing CI
23425 vasnesterov feat(Algebra/BigOperators): simprocify `prod_univ_one/two/three/...` t-meta blocked-by-other-PR ✅ ✅ ❌ ✅ ✅ ✅ ❌ blocked on another PR
23444 mistarro refactor(Algebra/CharP): Frobenius map definition in `Mathlib.Algebra.CharP.Frobenius` large-import t-algebra ✅ ✅ ✅ ✅ ✅ ✅ ✅ awaiting review
23448 Parcly-Taxel chore: fix more induction branch names ✅ ✅ ✅ ✅ ✅ ✅ ✅ awaiting review
23177 faenuccio feat: add order properties to WithZero types large-import t-order awaiting-author ✅ ❌ ✅ ✅ ✅ ❌ ❌ failing CI
23450 wwylele feat(Data/List/Basic): add forall_append t-data new-contributor ✅ ✅ ✅ ✅ ✅ ✅ ✅ awaiting review
23329 ScottCarnahan feat (LinearAlgebra/RootSystem): nondegeneracy for subrings t-algebra ✅ ❌ ✅ ✅ ✅ ✅ ❌ failing CI
23452 xroblot feat(FieldTheory/Normal): A quadratic extension is normal t-algebra ✅ ✅ ✅ ✅ ✅ ✅ ✅ awaiting review
23453 xroblot feat(RootsOfUnity/Complex): the conjugate of a complex root of unity is its inverse t-algebra ✅ ✅ ✅ ✅ ✅ ✅ ✅ awaiting review
22269 Thmoas-Guan chore(Algebra):replace Submodule.quotient.mk with Submodule.mkQ ✅ ✅ ✅ ✅ ✅ ✅ ✅ awaiting review
23454 apnelson1 feat(Data/ENat): multiplication and Inf/Sup lemmas t-data ✅ ✅ ✅ ✅ ✅ ✅ ✅ awaiting review
23076 miguelmarco feat: add rewriting lemmas for euclidean domains new-contributor t-algebra enhancement ✅ ✅ ✅ ✅ ✅ ✅ ✅ awaiting review
23348 loefflerd feat(NumberTheory/Padics): Use NormMulClass for p-adic ints delegated ✅ ✅ ✅ ✅ ✅ ✅ ✅ ⚠️ delegated
21524 Timeroot feat(BigOperators/Finset): prod_comm_3 t-algebra ✅ ✅ ✅ ✅ ✅ ✅ ✅ awaiting review
23345 riccardobrasca chore: rename UniformGroup -> IsUniformGroup and UniformAddGroup -> IsUniformAddGroup t-algebra ✅ ✅ ✅ ✅ ✅ ✅ ✅ awaiting review
20051 Timeroot feat: `Clone` and some instances t-algebra awaiting-author blocked-by-other-PR ✅ ❌ ❌ ✅ ✅ ❌ ❌ blocked on another PR
23459 Timeroot feat: Definition of `Clone` notations and typeclasses t-algebra ✅ ✅ ✅ ✅ ✅ ✅ ✅ awaiting review
23460 Timeroot feat: Definition of `Clone` t-algebra blocked-by-other-PR ✅ ✅ ❌ ✅ ✅ ✅ ❌ blocked on another PR
9085 Timeroot feat: `Polynomial.coeffList` large-import t-data ✅ ✅ ✅ ✅ ✅ ✅ ✅ awaiting review
23461 xroblot feat(GroupTheory/Cyclic): formula for the card & index of kernel & range of powMonoidHom on a cyclic group t-algebra ✅ ✅ ✅ ✅ ✅ ✅ ✅ awaiting review
21336 erdOne feat(Algebra/Category): finitely presented algebras are finitely presented t-algebra t-category-theory ✅ ✅ ✅ ✅ ✅ ✅ ✅ awaiting review
22100 smmercuri feat: two inequivalent absolute values have a `< 1` and `> 1` value ✅ ✅ ✅ ✅ ✅ ✅ ✅ ⚠️ awaiting review
21283 erdOne feat: topology on Hom(R, S) in `CommRingCat` t-algebra t-topology ✅ ✅ ✅ ✅ ✅ ✅ ✅ awaiting review
21399 erdOne feat(CategoryTheory): `ChosenFiniteProducts (Over X)` t-category-theory ✅ ✅ ✅ ✅ ✅ ✅ ✅ awaiting review
22142 smmercuri feat: collections of non-trivial and pairwise inequivalent absolute values contain values that diverge around 1 blocked-by-other-PR ✅ ❌ ❌ ✅ ✅ ✅ ❌ ⚠️ blocked on another PR
23339 joelriou feat(CategoryTheory): the colimit type of a functor to types t-category-theory ✅ ✅ ✅ ✅ ✅ ✅ ✅ awaiting review
23394 BoltonBailey chore(Data/Int/WithZero): fix erw tech debt awaiting-author ✅ ✅ ✅ ✅ ✅ ❌ ❌ awaiting author
22912 AntoineChambert-Loir feat(RingTheory/PolynomialLaw/Basic): definition and elementary properties of polynomial laws large-import t-algebra ✅ ✅ ✅ ✅ ✅ ✅ ✅ awaiting review
18397 YaelDillies chore: Rename `RestrictGenTopology` to `IsRestrictGen` t-topology ✅ ✅ ✅ ✅ ✅ ✅ ✅ awaiting review
21950 erdOne feat(NumberTheory/Padics): the completion of `ℚ` at a finite place is `ℚ_[p]` t-number-theory ✅ ✅ ✅ ✅ ✅ ✅ ✅ awaiting review
23462 urkud feat(Ergodic): Radon-Nikodym derivatives of invariant measures t-dynamics t-measure-probability ✅ ✅ ✅ ✅ ✅ ✅ ✅ awaiting review
23455 urkud feat: ergodic measures as extereme points t-dynamics t-measure-probability blocked-by-other-PR ✅ ✅ ❌ ✅ ✅ ✅ ❌ blocked on another PR
21934 erdOne feat(NumberTheory): p-adic cyclotomic character large-import t-number-theory ✅ ✅ ✅ ✅ ✅ ✅ ✅ awaiting review
23310 Paul-Lez feat(Analysis/Calculus): lemmas about derivatives of constant functions maintainer-merge t-analysis delegated ✅ ✅ ✅ ✅ ✅ ✅ ✅ delegated
23025 Paul-Lez feat(Lean/ToExpr): add helper functions to create `Expr` for finsets/sets/multisets t-meta ✅ ✅ ✅ ✅ ✅ ✅ ✅ awaiting review
22503 Kevew chore(Nat): Nat factorization multiplicity large-import t-data new-contributor ✅ ✅ ✅ ✅ ✅ ✅ ✅ awaiting review
21461 erdOne feat(RingTheory): zero-dimensional rings t-algebra ✅ ✅ ✅ ✅ ✅ ✅ ✅ awaiting review
23320 Whysoserioushah feat(Mathlib/RingTheory/TwoSidedIdeal/SpanAsSum): span of set as finsum t-algebra ✅ ✅ ✅ ✅ ✅ ✅ ✅ awaiting review
22823 b-reinke feat(Algebra/Ring): associator of a non-associative ring new-contributor t-algebra awaiting-author ✅ ✅ ✅ ✅ ✅ ❌ ❌ awaiting review
21803 erdOne feat(Order): `LTSeries` can be extended to `CovBy`-`RelSeries` large-import t-order ✅ ✅ ✅ ✅ ✅ ✅ ✅ awaiting review
23275 miguelmarco feat: add rewriting lemmas for integers t-data maintainer-merge new-contributor ✅ ✅ ✅ ✅ ✅ ✅ ✅ awaiting review
23351 kim-em chore: run lean4checker on itself CI ✅ ✅ ✅ ✅ ✅ ✅ ✅ awaiting review
23294 Parcly-Taxel chore: split `Data.WSeq.Basic` t-data tech debt ✅ ✅ ✅ ✅ ✅ ✅ ✅ awaiting review
23428 Parcly-Taxel chore: split `Data.EReal.Basic` t-data tech debt ✅ 🟤 ✅ ✅ ✅ ✅ ❌ running CI
23365 vasnesterov feat(Tactic/Simproc): nested quantifiers in `existsAndEq` large-import t-meta ✅ 🟤 ✅ ✅ ✅ ✅ ❌ running CI
21800 erdOne feat(Order): more API for krull dimensions t-order ✅ 🟤 ✅ ✅ ✅ ✅ ❌ does not pass CI
23467 JovanGerb chore: remove duplicate instance `SMul Mˣ α` t-algebra ✅ 🟤 ✅ ✅ ✅ ✅ ❌ running CI
23465 JovanGerb lean pr testing 7740 ❌ ??? ✅ ✅ ✅ ✅ ❌ opened from a fork
23466 mathlib4-update-dependencies-bot chore: update Mathlib dependencies 2025-03-31 dependency-bump auto-merge-after-CI ready-to-merge ✅ 🟤 ✅ ✅ ✅ ✅ ❌ contradictory labels
23468 kim-em chore: adaptations for nightly-2025-03-30 auto-merge-after-CI ❌ ??? ✅ ✅ ✅ ✅ ❌ opened from a fork
21693 erdOne feat: taylor expansion of `1 / z ^ r` t-analysis awaiting-author ✅ ❌ ✅ ✅ ✅ ❌ ❌ failing CI
21673 erdOne feat: `∑ z ∈ L, ‖z - x‖⁻ʳ` converges for lattices `L` t-analysis ✅ ✅ ✅ ✅ ✅ ✅ ✅ merge conflict
21330 JovanGerb perf(CategoryTheory): let `aesop_cat` attempt `rfl` before `aesop` awaiting-zulip t-category-theory t-meta delegated ✅ ✅ ✅ ✅ ✅ ❌ ❌ awaiting a zulip discussion
21909 erdOne feat(RingTheory/Invariants): Generalize to profinite groups t-algebra awaiting-author ✅ ❌ ✅ ✅ ✅ ❌ ❌ failing CI
14426 adomani dev: `#min_imps` command merge-conflict WIP ✅ ✅ ✅ ❌ ❌ ✅ ❌ labelled WIP
14330 Ruben-VandeVelde chore: split Mathlib.Algebra.Star.Basic merge-conflict awaiting-author ✅ ✅ ✅ ❌ ✅ ❌ ❌ merge conflict
13847 alreadydone feat(EllipticCurve): the universal elliptic curve t-algebra t-algebraic-geometry merge-conflict awaiting-author ✅ ✅ ✅ ❌ ✅ ❌ ❌ merge conflict
14167 alreadydone feat: Group scheme structure on Weierstrass curve workshop-AIM-AG-2024 t-algebraic-geometry merge-conflict WIP ✅ ❌ ✅ ❌ ❌ ✅ ❌ labelled WIP
13297 urkud feat(Semicontinuous): add `comp` lemma t-order t-topology merge-conflict awaiting-author ✅ ✅ ✅ ❌ ✅ ❌ ❌ merge conflict
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
12773 apnelson1 feat(Combinatorics/HypergraphRamsey): Ramsey's theorem for hypergraphs t-combinatorics merge-conflict ✅ ❌ ✅ ❌ ✅ ✅ ❌ 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
12934 grunweg chore: replace more uses of > or ≥ by < or ≤ merge-conflict awaiting-author help-wanted ✅ ✅ ✅ ❌ ❌ ❌ ❌ looking for help
12933 grunweg chore: replace some use of > or ≥ by < or ≤ merge-conflict awaiting-author ✅ ❌ ✅ ❌ ✅ ❌ ❌ failing CI
12679 MichaelStollBayreuth perf(NumberTheory/RamificationInertia): speed up slow file merge-conflict WIP ✅ ✅ ✅ ❌ ❌ ✅ ❌ labelled WIP
12608 eric-wieser feat: allow `nsmul` / `zsmul` to be omitted again, with a warning t-algebra t-meta merge-conflict awaiting-author ✅ ✅ ✅ ❌ ✅ ❌ ❌ merge conflict
11524 mcdoll refactor: Introduce type-class for SchwartzMap merge-conflict WIP ✅ ❌ ✅ ❌ ❌ ✅ ❌ labelled WIP
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
11617 urkud refactor(Finset): redefine Finset.diag, review API t-logic merge-conflict awaiting-author ✅ ✅ ✅ ❌ ✅ ❌ ❌ merge conflict
11575 ScottCarnahan feat (RingTheory/HahnSeries/Addition): Lemmas on leading terms t-algebra merge-conflict WIP ✅ ✅ ✅ ❌ ❌ ✅ ❌ labelled WIP
11455 adomani fix: unsqueeze simp, re Yaël's comments on #11259 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
10594 lecopivo feat: `fun_trans` function transformation tactic e.g. for computing derivatives t-meta merge-conflict WIP ✅ ❌ ✅ ❌ ❌ ✅ ❌ labelled WIP
11021 jstoobysmith feat(AlgebraicTopology) : add join of augmented SSets new-contributor t-category-theory merge-conflict WIP ✅ ❌ ✅ ❌ ❌ ✅ ❌ labelled WIP
10842 mcdoll chore: simplify proofs using new positivity extensions and tests merge-conflict blocked-by-other-PR WIP ✅ ✅ ❌ ❌ ❌ ✅ ❌ blocked on another PR
10444 urkud doc(IsROrC): expand the docstring t-analysis merge-conflict awaiting-author documentation ✅ ✅ ✅ ❌ ✅ ❌ ❌ merge conflict
10521 eric-wieser chore: generalize `IsBoundedLinearMap` to modules t-analysis merge-conflict awaiting-author ✅ ✅ ✅ ❌ ✅ ❌ ❌ merge conflict
10721 urkud feat(Order/FunLike): define `PointwiseLE` t-logic t-order merge-conflict ✅ ✅ ✅ ❌ ✅ ✅ ❌ merge conflict
10113 Multramate feat(GroupTheory/Submonoid/Operations): define homomorphisms of subgroups induced by homomorphisms of groups t-algebra merge-conflict awaiting-author ✅ ✅ ✅ ❌ ✅ ❌ ❌ merge conflict
10126 Multramate feat(GroupTheory/GroupAction/Basic): define homomorphisms of fixed subgroups induced by homomorphisms of groups t-algebra merge-conflict blocked-by-other-PR ✅ ✅ ❌ ❌ ✅ ✅ ❌ blocked on another PR
10024 ADedecker feat: rename `connectedComponentOfOne` to `identityComponent`, prove that it is normal and open t-topology awaiting-CI merge-conflict ✅ ❌ ✅ ❌ ✅ ❌ ❌ does not pass CI
10142 Multramate feat(AlgebraicGeometry/EllipticCurve/Group): compute range of baseChange t-algebraic-geometry t-number-theory merge-conflict blocked-by-other-PR ✅ ✅ ❌ ❌ ✅ ✅ ❌ blocked on another PR
8511 eric-wieser refactor(MeasureTheory/Measure/Haar/Basic): partially generalize to the affine case merge-conflict awaiting-author ✅ ❌ ✅ ❌ ✅ ❌ ❌ failing CI
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
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
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
8658 eric-wieser feat: support right actions for `Con` t-algebra merge-conflict awaiting-author ✅ ✅ ✅ ❌ ✅ ❌ ❌ merge conflict
9356 alexjbest feat: assumption? t-meta merge-conflict awaiting-author ✅ ✅ ✅ ❌ ✅ ❌ ❌ merge conflict
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
9571 linesthatinterlace fix(Data/Fin/Tuple/Basic): Refactor snoc and cons proofs. merge-conflict awaiting-author ✅ ❌ ✅ ❌ ✅ ❌ ❌ failing CI
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
9564 AntoineChambert-Loir weaken commutativity assumptions for AdjoinRoot.lift and AdjoinRoot.liftHom t-algebra 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
8906 jjaassoonn feat: add some missing lemmas about linear algebra t-algebra merge-conflict awaiting-author ✅ ❌ ✅ ❌ ✅ ❌ ❌ failing CI
9570 eric-wieser feat(Algebra/Star): Non-commutative generalization of `StarModule` t-algebra awaiting-CI merge-conflict WIP ✅ ❌ ✅ ❌ ❌ ❌ ❌ labelled WIP
9146 laughinggas feat(Data/ZMod/Defs): Topological structure on `ZMod` t-algebra t-topology merge-conflict awaiting-author ✅ ✅ ✅ ❌ ✅ ❌ ❌ merge conflict
9229 eric-wieser refactor(Algebra/GradedMonoid): Use `HMul` to define `GMul` t-algebra merge-conflict WIP ✅ ❌ ✅ ❌ ❌ ✅ ❌ labelled WIP
9627 Ruben-VandeVelde chore: move some code out of Init.Data.Nat.Lemmas merge-conflict awaiting-author ✅ ✅ ✅ ❌ ✅ ❌ ❌ merge conflict
9354 chenyili0818 feat: monotonicity of gradient on convex real-valued functions t-analysis merge-conflict awaiting-author ✅ ✅ ✅ ❌ ✅ ❌ ❌ merge conflict
6930 kmill feat: `resynth_instances` tactic for resynthesizing instances in the goal or local context t-meta merge-conflict WIP ✅ ✅ ✅ ❌ ❌ ✅ ❌ labelled WIP
7351 shuxuezhuyi feat(Topology/Algebra/Order): extend function on `Ioo` to `Icc` t-order merge-conflict awaiting-author ✅ ✅ ✅ ❌ ✅ ❌ ❌ merge conflict
6777 adomani chore(Co*variantClass): replace eta-expanded (· * ·), (· + ·), (· ≤ ·), (· < ·) merge-conflict ✅ ✅ ✅ ❌ ✅ ✅ ❌ merge conflict
7227 kmill feat: flexible binders and integration into notation3 t-meta merge-conflict WIP ✅ ❌ ✅ ❌ ❌ ✅ ❌ labelled WIP
7427 MohanadAhmed Mohanad ahmed/sort eigenvalues abs merge-conflict WIP ✅ ✅ ✅ ❌ ❌ ✅ ❌ labelled WIP
6630 MohanadAhmed feat: Reduced Spectral Theorem t-algebra merge-conflict WIP ✅ ❌ ✅ ❌ ❌ ✅ ❌ labelled WIP
6580 adomani chore: `move_add`-driven replacements merge-conflict awaiting-author ✅ ✅ ✅ ❌ ✅ ❌ ❌ merge conflict
6791 eric-wieser refactor: Use flat structures for morphisms awaiting-CI merge-conflict awaiting-author help-wanted ✅ ✅ ✅ ❌ ❌ ❌ ❌ looking for help
7994 ericrbg chore: generalize `LieSubalgebra.mem_map_submodule` merge-conflict please-adopt ✅ ❌ ✅ ❌ ❌ ✅ ❌ looking for help
7601 digama0 feat: ring hom support in `ring` t-algebra t-meta merge-conflict awaiting-author ✅ ✅ ✅ ❌ ✅ ❌ ❌ 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
7932 eric-wieser refactor(Algebra/TrivSqZeroExt): replace with a structure t-algebra awaiting-CI merge-conflict ✅ ❌ ✅ ❌ ✅ ❌ ❌ does not pass CI
7713 RemyDegenne feat: add_left/right_inj for measures t-measure-probability merge-conflict awaiting-author ✅ ✅ ✅ ❌ ✅ ❌ ❌ merge conflict
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
7962 eric-wieser feat: `DualNumber (Quaternion R)` as a `CliffordAlgebra` t-algebra merge-conflict WIP ✅ ❌ ✅ ❌ ❌ ✅ ❌ labelled WIP
7874 FR-vdash-bot chore: make `IsScalarTower A A B` and `IsScalarTower A B B` higher priority slow-typeclass-synthesis t-algebra awaiting-CI merge-conflict ✅ ❌ ✅ ❌ ✅ ❌ ❌ 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
7649 eric-wieser wip: instead of `suppress_compilation`, use `implemented_by` merge-conflict WIP ✅ ❌ ✅ ❌ ❌ ✅ ❌ labelled WIP
7909 mcdoll fix(Tactic/Continuity): remove npowRec and add new tag for Continuous.pow t-topology t-meta merge-conflict WIP ✅ ✅ ✅ ❌ ❌ ✅ ❌ labelled WIP
7467 ADedecker feat: spectrum of X →ᵇ ℂ is StoneCech X t-analysis merge-conflict WIP ✅ ✅ ✅ ❌ ❌ ✅ ❌ labelled WIP
6931 urkud refactor(Analysis/Normed*): use `RingHomIsometric` for `*.norm_cast` t-analysis merge-conflict help-wanted ✅ ❌ ✅ ❌ ❌ ✅ ❌ looking for help
7325 eric-wieser chore: use preimageIso instead of defeq abuse for InducedCategory t-category-theory awaiting-CI merge-conflict ✅ ❌ ✅ ❌ ✅ ❌ ❌ does not pass CI
8364 thorimur feat: `refine?` t-meta merge-conflict blocked-by-other-PR ✅ ✅ ❌ ❌ ✅ ✅ ❌ blocked on another PR
8453 FR-vdash-bot chore(MeasureTheory): Golf, speed up t-measure-probability merge-conflict ✅ ❌ ✅ ❌ ✅ ✅ ❌ failing CI
6993 jjaassoonn feat : lemmas about `AddMonoidAlgebra.{divOf, modOf}` t-algebra merge-conflict ✅ ✅ ✅ ❌ ✅ ✅ ❌ merge conflict
6590 mcdoll feat: composition of LinearPMaps t-algebra merge-conflict WIP ✅ ❌ ✅ ❌ ❌ ✅ ❌ labelled WIP
6317 eric-wieser refactor(Data/Finsupp/Defs): make Finsupp.single defeq to Pi.single merge-conflict WIP ✅ ❌ ✅ ❌ ❌ ✅ ❌ labelled WIP
6633 adomani feat(..Polynomial..): `MvPolynomial`s have no zero divisors t-algebra merge-conflict awaiting-author ✅ ✅ ✅ ❌ ✅ ❌ ❌ merge conflict
3808 kim-em feat: #formalize, backed by a choice of LLMs t-meta merge-conflict awaiting-author ✅ ✅ ✅ ❌ ✅ ❌ ❌ merge conflict
6328 FR-vdash-bot chore: make some instance about `Sub...Class` lower priority t-algebra awaiting-CI merge-conflict WIP ✅ ❌ ✅ ❌ ❌ ❌ ❌ labelled WIP
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
4127 kmill refactor: create HasAdj class, define Digraph, and generalize some SimpleGraph API t-combinatorics merge-conflict awaiting-author ✅ ✅ ✅ ❌ ✅ ❌ ❌ merge conflict
6268 eric-wieser Fixups to #3838 merge-conflict WIP ✅ ❌ ✅ ❌ ❌ ✅ ❌ labelled WIP
5912 ADedecker feat(Analysis.Distribution.ContDiffMapSupportedIn): space of smooth maps with support in a fixed compact t-analysis merge-conflict WIP ✅ ✅ ✅ ❌ ❌ ✅ ❌ labelled WIP
5952 eric-wieser feat: add Qq wrappers for ToExpr awaiting-CI t-meta merge-conflict ✅ ❌ ✅ ❌ ✅ ❌ ❌ does not pass CI
4960 eric-wieser chore: use `open scoped` awaiting-CI merge-conflict ✅ ✅ ✅ ❌ ✅ ❌ ❌ does not pass CI
6079 eric-wieser fix: deduplicate variables awaiting-CI merge-conflict ✅ ❌ ✅ ❌ ✅ ❌ ❌ does not pass CI
6403 FR-vdash-bot chore: change instance priorities of `Ordered*` hierarchy slow-typeclass-synthesis t-order t-algebra merge-conflict awaiting-author ✅ ✅ ✅ ❌ ✅ ❌ ❌ merge conflict
6210 MohanadAhmed feat(Data/IsROrC/Basic): add a `StarOrderedRing` instance t-algebra t-analysis merge-conflict WIP ✅ ✅ ✅ ❌ ❌ ✅ ❌ labelled WIP
5133 kmill feat: IntermediateField adjoin syntax for sets of elements t-algebra merge-conflict WIP ✅ ✅ ✅ ❌ ❌ ✅ ❌ labelled WIP
6491 eric-wieser chore(Mathlib/Algebra/Hom/GroupAction): add `SMulHomClass.comp_smul` t-algebra merge-conflict ✅ ✅ ✅ ❌ ✅ ✅ ❌ merge conflict
7076 grunweg feat: define measure zero subsets of a manifold t-measure-probability t-differential-geometry merge-conflict WIP ✅ ✅ ✅ ❌ ❌ ✅ ❌ labelled WIP
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
5863 eric-wieser feat: add elaborators for concrete matrices t-meta merge-conflict help-wanted ✅ ✅ ✅ ❌ ❌ ✅ ❌ looking for help
5934 eric-wieser feat: port Data.Rat.MetaDefs t-meta merge-conflict mathlib-port help-wanted ✅ ✅ ✅ ❌ ❌ ✅ ❌ looking for help
6195 eric-wieser chore(RingTheory/TensorProduct): golf the `mul` definition t-algebra awaiting-CI merge-conflict ✅ ✅ ✅ ❌ ✅ ❌ ❌ does not pass CI
6002 slerpyyy feat(Analysis.SpecialFunctions.Gaussian): add `integrable_fun_mul_exp_neg_mul_sq` t-analysis merge-conflict awaiting-author ✅ ✅ ✅ ❌ ✅ ❌ ❌ merge conflict
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
14675 adomani dev: the repeated variable linter merge-conflict WIP ✅ ❌ ✅ ❌ ❌ ✅ ❌ labelled WIP
15483 FR-vdash-bot chore(GroupTheory/Coset): reduce defeq abuse t-algebra merge-conflict ✅ ✅ ✅ ❌ ✅ ✅ ❌ merge conflict
15400 grunweg feat: "confusing variables" linter t-linter merge-conflict WIP ✅ ❌ ✅ ❌ ❌ ✅ ❌ labelled WIP
10717 joelriou feat(Algebra/Homology): the total complex of a tricomplex t-category-theory 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
8435 kim-em feat: run `hint` tactics in parallel t-meta merge-conflict ✅ ❌ ✅ ❌ ✅ ✅ ❌ failing CI
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
14542 linesthatinterlace feat(GroupTheory/Perm/Support): Redefine `support` to be a `Set`, removing finiteness requirements. t-algebra 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
10283 linesthatinterlace feat(Data/Fin/OrderHom): Extend lemmas to simplex results t-data merge-conflict WIP ✅ ❌ ✅ ❌ ❌ ✅ ❌ labelled WIP
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
13026 BoltonBailey feat: add `simp` lemma `coeff_eq_zero_of_not_mem_support` t-algebra awaiting-CI merge-conflict awaiting-author ✅ ❌ ✅ ❌ ✅ ❌ ❌ does not pass CI
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
14023 mattrobball perf (RingTheory.OreLocalization): make data irreducible 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
7907 urkud feat: introduce `NthRoot` notation class t-algebra t-analysis awaiting-CI merge-conflict ✅ ❌ ✅ ❌ ✅ ❌ ❌ does not pass CI
15600 adomani feat: lint also `let` vs `have` t-linter merge-conflict WIP ✅ ✅ ✅ ❌ ❌ ✅ ❌ labelled WIP
12438 jjaassoonn feat: some APIs for flat modules t-category-theory merge-conflict WIP ✅ ✅ ✅ ❌ ❌ ✅ ❌ labelled WIP
14731 adomani feat: the repeated typeclass assumption linter t-linter merge-conflict WIP ✅ ❌ ✅ ❌ ❌ ✅ ❌ labelled WIP
14923 Multramate feat(AlgebraicGeometry/EllipticCurve/Jacobian): add equivalences between points and explicit WithZero types t-algebraic-geometry t-number-theory merge-conflict blocked-by-other-PR ✅ ❌ ❌ ❌ ✅ ✅ ❌ blocked on another PR
14266 dagurtomas feat(AlgebraicGeometry): define a pretopology from a RingHomProperty workshop-AIM-AG-2024 t-algebraic-geometry merge-conflict please-adopt WIP ✅ ❌ ✅ ❌ ❌ ✅ ❌ looking for help
14038 adomani test/decl diff in lean dev merge-conflict WIP ✅ ❌ ✅ ❌ ❌ ✅ ❌ labelled WIP
16408 Parcly-Taxel chore: remove TODO relating to #13092 tech debt merge-conflict ✅ ✅ ✅ ❌ ✅ ✅ ❌ merge conflict
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
15115 kkytola feat: Generalize assumptions in liminf and limsup results in ENNReals t-order t-topology merge-conflict awaiting-author ✅ ✅ ✅ ❌ ✅ ❌ ❌ merge conflict
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
16594 FR-vdash-bot perf: reorder `extends` and remove some instances in algebra hierarchy slow-typeclass-synthesis t-algebra merge-conflict ✅ ❌ ✅ ❌ ✅ ✅ ❌ failing CI
11003 thorimur chore: migrate to `tfae` block tactic merge-conflict blocked-by-other-PR WIP ✅ ✅ ❌ ❌ ❌ ✅ ❌ 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
14203 dagurtomas feat(Algebra/ModuleCat): descent data workshop-AIM-AG-2024 t-algebra t-algebraic-geometry t-category-theory merge-conflict please-adopt WIP ✅ ❌ ✅ ❌ ❌ ✅ ❌ looking for help
14242 js2357 feat: Prove equivalence of `isDedekindDomain` and `isDedekindDomainDvr` new-contributor t-algebra merge-conflict blocked-by-other-PR ✅ ✅ ❌ ❌ ✅ ✅ ❌ blocked on another PR
16387 adomani test: add creator check in new contributor merge-conflict WIP ✅ ✅ ✅ ❌ ❌ ✅ ❌ labelled WIP
16186 joneugster chore: use emoji-variant-selector `\uFE0F` for emojis ✅️,❌️,💥️,🟡️ merge-conflict awaiting-author 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
12617 mans0954 feat(Algebra/Ring/Defs): Add NonUnitalCommSemiring.toNonUnitalNonAssocCommSemiring instance t-algebra merge-conflict ✅ ❌ ✅ ❌ ✅ ✅ ❌ failing CI
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
9105 LukasMias feat(Algebra/Algebra/Prod): add prodUnique and uniqueProd for LinearEquiv and AlgebraEquiv t-algebra merge-conflict awaiting-author ✅ ✅ ✅ ❌ ✅ ❌ ❌ merge conflict
11500 mcdoll refactor(Topology/Algebra/Module/WeakDual): Clean up t-topology merge-conflict awaiting-author ✅ ✅ ✅ ❌ ✅ ❌ ❌ merge conflict
12994 ADedecker chore: reorganize and rename the Embedding --> Homeomorph constructions 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
14627 Multramate feat(AlgebraicGeometry/EllipticCurve/Affine): add equivalences between points and explicit WithZero types t-algebraic-geometry t-number-theory merge-conflict awaiting-author ✅ ✅ ✅ ❌ ✅ ❌ ❌ 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
14160 linesthatinterlace feat(Algebra/Group/Action/Defs): Redefine `Function.End` t-algebra merge-conflict awaiting-author WIP ✅ ❌ ✅ ❌ ❌ ❌ ❌ labelled WIP
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
17358 sgouezel feat: the tangent bundle of a product is isomorphic to the product of the tangent bundles t-differential-geometry merge-conflict WIP ✅ ✅ ✅ ❌ ❌ ✅ ❌ labelled WIP
17757 vihdzp refactor(*): generalize typeclass assumptions in morphisms t-algebra merge-conflict WIP ✅ ❌ ✅ ❌ ❌ ✅ ❌ labelled WIP
18254 callesonne feat(Bicategory/Modification/Pseudo): define modifications between strong natural transformations of pseudofunctors t-category-theory merge-conflict blocked-by-other-PR ✅ ✅ ❌ ❌ ✅ ✅ ❌ blocked on another PR
15654 TpmKranz feat(Computability): language-preserving maps between NFA and RE t-computability new-contributor merge-conflict blocked-by-other-PR ✅ ✅ ❌ ❌ ✅ ✅ ❌ blocked on another PR
14089 callesonne feat(Bicategory/Functorbicategory): define bicategory of pseudofunctors t-category-theory merge-conflict blocked-by-other-PR ✅ ✅ ❌ ❌ ✅ ✅ ❌ blocked on another PR
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
17109 grunweg feat: warn on `autoImplicit true` tech debt t-linter merge-conflict ✅ ❌ ✅ ❌ ✅ ✅ ❌ failing CI
16704 AntoineChambert-Loir feat(Mathlib.Data.Ordering.Dickson): Dickson orders t-order merge-conflict WIP ✅ ✅ ✅ ❌ ❌ ✅ ❌ labelled WIP
17746 vihdzp feat(SetTheory/Ordinal/Arithmetic): make `IsNormal` a structure t-set-theory 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
16116 jjdishere feat(Field): add theorems in Stacks Project Chapter 09FA Fields new-contributor t-algebra merge-conflict WIP ✅ ✅ ✅ ❌ ❌ ✅ ❌ labelled WIP
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
18725 joelriou feat(LinearAlgebra): generators of pi tensor products t-algebra 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
17458 urkud refactor(Algebra/Group): make `IsUnit` a typeclass awaiting-zulip t-algebra merge-conflict ✅ ❌ ✅ ❌ ✅ ❌ ❌ failing CI
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
17672 urkud refactor: turn `IsTorsionFree` into a typeclass t-algebra merge-conflict ✅ ✅ ✅ ❌ ✅ ✅ ❌ merge conflict
17623 FR-vdash-bot feat(Algebra/Order/GroupWithZero/Unbundled): add some lemmas awaiting-zulip t-order t-algebra merge-conflict ✅ ✅ ✅ ❌ ✅ ❌ ❌ awaiting a zulip discussion
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
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
16743 agjftucker feat(Analysis/Calculus/Implicit): define HasStrictDerivAt.implicitFunOfBivariate new-contributor t-analysis merge-conflict awaiting-author ✅ ✅ ✅ ❌ ✅ ❌ ❌ merge conflict
18646 jxjwan feat(RingTheory): isotypic components new-contributor t-algebra merge-conflict ✅ ❌ ✅ ❌ ✅ ✅ ❌ failing CI
12673 grunweg feat: add ContDiff.lipschitzOnWith t-analysis merge-conflict awaiting-author ✅ ✅ ✅ ❌ ✅ ❌ ❌ merge conflict
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
19299 javierlcontreras feat(Algebra/CategoryTheory): Add CommAlgebraCat new-contributor t-algebra merge-conflict WIP ✅ ❌ ✅ ❌ ❌ ✅ ❌ labelled WIP
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
16956 Parcly-Taxel refactor(Order/Interval/Finset/Nat): supersymmetrise API t-order merge-conflict awaiting-author ✅ ✅ ✅ ❌ ✅ ❌ ❌ merge conflict
19576 grunweg chore: replace many occurrences of `=>` arrows for anonymous functions awaiting-CI merge-conflict delegated ✅ ❌ ✅ ❌ ✅ ❌ ❌ does not pass CI
9598 AlexKontorovich feat(Analysis/Complex): HasPrimitives on disc t-analysis merge-conflict ✅ ❌ ✅ ❌ ✅ ✅ ❌ failing CI
19526 metakunt feat:closure properties of numbers that are introspective to polynomials new-contributor t-number-theory merge-conflict awaiting-author ✅ ✅ ✅ ❌ ✅ ❌ ❌ merge conflict
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
13124 FR-vdash-bot chore: remove `CovariantClass` and `ContravariantClass` merge-conflict 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
18662 joelriou feat(LinearAlgebra/ExteriorPower): generators of the exterior powers t-algebra merge-conflict blocked-by-other-PR WIP ✅ ✅ ❌ ❌ ❌ ✅ ❌ blocked on another PR
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
19520 erdOne refactor(Algebra/Module): Redefine `LocalizedModule` in terms of `OreLocalization` merge-conflict ✅ ❌ ✅ ❌ ✅ ✅ ❌ failing CI
4197 joelriou feat/refactor: redefinition of homology + derived categories t-topology t-category-theory merge-conflict WIP ✅ ❌ ✅ ❌ ❌ ✅ ❌ labelled WIP
16344 robertmaxton42 feat(LinearAlgebra/FreeProduct): add induction principle, further simp opts for lift new-contributor t-algebra merge-conflict blocked-by-other-PR ✅ ✅ ❌ ❌ ✅ ✅ ❌ blocked on another PR
19547 grunweg perf: merge several style syntax linters awaiting-bench t-linter merge-conflict WIP ✅ ✅ ✅ ❌ ❌ ✅ ❌ labelled WIP
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
18912 b-mehta feat(SpecialFunctions/Log): more continuity and limits for logb t-analysis merge-conflict ✅ ✅ ✅ ❌ ✅ ✅ ❌ merge conflict
12561 BoltonBailey doc: Elaborate output of `lake exe pole` merge-conflict WIP ✅ ✅ ✅ ❌ ❌ ✅ ❌ labelled WIP
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
17027 vihdzp feat(SetTheory/ZFC/Ordinal): von Neumann hierarchy of sets t-set-theory merge-conflict blocked-by-other-PR ✅ ✅ ❌ ❌ ✅ ✅ ❌ blocked on another PR
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
18508 urkud chore(OperatorNorm/Completeness): drop a duplicate instance t-analysis merge-conflict help-wanted ✅ ✅ ✅ ❌ ❌ ✅ ❌ looking for help
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
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
18527 joelriou feat(Algebra/Module): presentation of the `PiTensorProduct` t-algebra merge-conflict blocked-by-other-PR WIP ✅ ❌ ❌ ❌ ❌ ✅ ❌ 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
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
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
16314 FR-vdash-bot chore(Data/Quot): deprecate `ind*'` APIs t-data merge-conflict ✅ ✅ ✅ ❌ ✅ ✅ ❌ 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 ❌ ✅ ✅ ❌ ✅ ❌ ❌ opened from a fork
13649 FR-vdash-bot chore: redefine `Nat.div2` `Nat.bodd` merge-conflict blocked-by-other-PR ✅ ✅ ❌ ❌ ✅ ✅ ❌ blocked on another PR
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
19985 vihdzp feat(SetTheory/ZFC/Ordinal): Lean ordinals to ZFC ordinals large-import t-set-theory merge-conflict blocked-by-other-PR ✅ ✅ ❌ ❌ ✅ ✅ ❌ blocked on another PR
19882 tb65536 feat(Algebra/Module/ZMod): `ZMod`-module structures on multiplicative groups t-algebra merge-conflict ✅ ✅ ✅ ❌ ✅ ✅ ❌ merge conflict
19467 quangvdao feat(MvPolynomial/Equiv): Add `MvPolynomial.finSuccEquivNth` merge-conflict blocked-by-other-PR ✅ ✅ ❌ ❌ ✅ ✅ ❌ ⚠️ blocked on another PR
20567 grunweg feat(Cache): two small features merge-conflict ✅ ✅ ✅ ❌ ✅ ✅ ❌ ⚠️ merge conflict
20201 dagurtomas feat(AlgebraicTopology): anodyne morphisms of simplicial sets merge-conflict WIP ✅ ❌ ✅ ❌ ❌ ✅ ❌ ⚠️ labelled WIP
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
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
20527 trivial1711 refactor(Topology/UniformSpace/Completion): more descriptive names for `α → Completion α` t-topology merge-conflict ✅ ✅ ✅ ❌ ✅ ✅ ❌ merge conflict
18379 oeb25 feat(Topology/ENNReal): Add `ENNReal.tsum_biUnion` new-contributor t-topology merge-conflict ✅ ❌ ✅ ❌ ✅ ✅ ❌ failing CI
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
11155 smorel394 feat(LinearAlgebra/Multilinear/DirectSum, LinearAlgebra/DirectSum/{PiTensorProduct,Finsupp}): interaction between `MultilinearMap` and `DirectSum`, and between `PiTensorProduct` and `DirectSum` t-algebra merge-conflict please-adopt ✅ ✅ ✅ ❌ ❌ ✅ ❌ looking for help
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
18468 FR-vdash-bot perf: lower the priority of `Ordered*.to*` instances slow-typeclass-synthesis t-order t-algebra merge-conflict ✅ ✅ ✅ ❌ ✅ ✅ ❌ merge conflict
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
15720 znssong feat(SimpleGraph): The Bondy-Chvátal theorem new-contributor t-combinatorics merge-conflict blocked-by-other-PR ✅ ✅ ❌ ❌ ✅ ✅ ❌ blocked on another PR
15711 znssong feat(Combinatorics/SimpleGraph): Some lemmas about walk, cycle and Hamiltonian cycle new-contributor t-combinatorics merge-conflict awaiting-author ✅ ✅ ✅ ❌ ✅ ❌ ❌ merge conflict
20676 FR-vdash-bot chore: deprecate semibundled ordered algebraic typeclasses t-order t-algebra 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
20594 FR-vdash-bot chore: use mixin ordered algebraic typeclasses (part 1) t-order t-algebra merge-conflict blocked-by-other-PR ✅ ✅ ❌ ❌ ✅ ✅ ❌ blocked on another PR
20595 FR-vdash-bot chore: use mixin ordered algebraic typeclasses (part 2) t-order t-algebra merge-conflict blocked-by-other-PR WIP ✅ ❌ ❌ ❌ ❌ ✅ ❌ blocked on another PR
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
10129 linesthatinterlace fix(Topology/MetricSpace/InfSep): Make `infsep` consistent with `diam`, `infdist` merge-conflict awaiting-author ✅ ✅ ✅ ❌ ✅ ❌ ❌ merge conflict
13539 joelriou feat: the bicategory of adjunctions in a bicategory t-category-theory merge-conflict please-adopt WIP ✅ ❌ ✅ ❌ ❌ ✅ ❌ looking for help
18285 callesonne feat(Bicategory/Grothendieck): functoriality of the grothendieck construction t-category-theory merge-conflict blocked-by-other-PR WIP ✅ ❌ ❌ ❌ ❌ ✅ ❌ blocked on another PR
19291 PieterCuijpers feat(Algebra/Order/Hom): add quantale homomorphism new-contributor t-algebra merge-conflict awaiting-author ✅ ❌ ✅ ❌ ✅ ❌ ❌ failing CI
17781 robin-carlier feat(CategoryTheory/Limits/Sifted): characterization of sifted categories large-import t-category-theory merge-conflict awaiting-author ✅ ✅ ✅ ❌ ✅ ❌ ❌ merge conflict
20160 vasnesterov feat(Data/Seq): `modify` and `set` operations for `Seq` t-data merge-conflict blocked-by-other-PR ✅ ✅ ❌ ❌ ✅ ✅ ❌ blocked on another PR
19352 hrmacbeth chore: change some `nlinarith`s to `linear_combination`s merge-conflict WIP ✅ ✅ ✅ ❌ ❌ ✅ ❌ labelled WIP
12605 FR-vdash-bot chore: attribute [induction_eliminator] merge-conflict awaiting-author ✅ ✅ ✅ ❌ ✅ ❌ ❌ merge conflict
20781 artie2000 feat(Algebra): Add Aesop automation around `Even` / `IsSquare`. merge-conflict blocked-by-other-PR ✅ ✅ ❌ ❌ ✅ ✅ ❌ ⚠️ blocked on another PR
13795 FR-vdash-bot perf(Algebra/{Group, GroupWithZero, Ring}/InjSurj): reduce everything t-algebra merge-conflict ✅ ❌ ✅ ❌ ✅ ✅ ❌ failing CI
20477 artie2000 feat(Aesop): Improve SetLike ruleset t-algebra t-meta merge-conflict awaiting-author ✅ ✅ ✅ ❌ ✅ ❌ ❌ merge conflict
20313 thefundamentaltheor3m feat(Data/Complex/Exponential): prove some useful results about the complex exponential. new-contributor merge-conflict ✅ ❌ ✅ ❌ ✅ ✅ ❌ ⚠️ failing CI
20372 jvlmdr feat(MeasureTheory/Function): Add ContinuousLinearMap.bilinearCompLp(L) new-contributor t-measure-probability merge-conflict ✅ ✅ ✅ ❌ ✅ ✅ ❌ merge conflict
20979 sgouezel chore: deprecate the file `AnalyticManifold` t-differential-geometry merge-conflict blocked-by-other-PR WIP ✅ ✅ ❌ ❌ ❌ ✅ ❌ blocked on another PR
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
21182 joneugster fix(Util/CountHeartbeats): move elaboration in #count_heartbeats inside a namespace t-meta merge-conflict ✅ ❌ ✅ ❌ ✅ ✅ ❌ failing CI
12294 AntoineChambert-Loir feat(Mathlib.RingTheory.TensorProduct.Polynomial) : tensor product of a (univariate) polynomial ring t-algebra merge-conflict WIP ✅ ❌ ✅ ❌ ❌ ✅ ❌ labelled WIP
19456 AntoineChambert-Loir feat(Data/Finsupp/MonomialOrder/DegRevLex): homogeneous reverse lexicographic order t-data t-order t-algebraic-geometry merge-conflict WIP ✅ ❌ ✅ ❌ ❌ ✅ ❌ labelled WIP
18438 ADedecker refactor: adapt `KrullTopology` to the new algebraic filter bases API t-algebra t-topology merge-conflict blocked-by-other-PR ✅ ✅ ❌ ❌ ✅ ✅ ❌ blocked on another PR
12824 BoltonBailey refactor: `ReflTransGen` t-logic merge-conflict WIP help-wanted ✅ ❌ ✅ ❌ ❌ ✅ ❌ looking for help
19890 vihdzp chore(SetTheory/Ordinal/Arithmetic): redefine subtraction t-set-theory merge-conflict blocked-by-other-PR ✅ ✅ ❌ ❌ ✅ ✅ ❌ blocked on another PR
14686 smorel394 feat (AlgebraicGeometry/Grassmannian): define the Grassmannian scheme workshop-AIM-AG-2024 t-algebraic-geometry merge-conflict please-adopt WIP ✅ ✅ ✅ ❌ ❌ ✅ ❌ looking for help
21375 grunweg WIP: generalise lemmas to ENorm carleson awaiting-CI merge-conflict WIP ✅ ❌ ✅ ❌ ❌ ❌ ❌ labelled WIP
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
18754 FR-vdash-bot feat: `IsometryClass` t-topology merge-conflict awaiting-author ✅ ✅ ✅ ❌ ✅ ❌ ❌ merge conflict
18711 bjoernkjoshanssen feat: One-point compactification of Euclidean space homeomorphic to sphere t-topology merge-conflict awaiting-author ✅ ✅ ✅ ❌ ✅ ❌ ❌ merge conflict
18441 ADedecker refactor(AdicTopology): use new API for algebraic filter bases, and factor some code t-algebra t-topology merge-conflict blocked-by-other-PR ✅ ✅ ❌ ❌ ✅ ✅ ❌ blocked on another PR
18785 erdOne feat(CategoryTheory): command that generates instances for `MorphismProperty` t-category-theory t-meta merge-conflict awaiting-author ✅ ✅ ✅ ❌ ✅ ❌ ❌ merge conflict
20689 joelriou feat(AlgebraicTopology): cylinder objects in model categories large-import t-category-theory merge-conflict blocked-by-other-PR WIP ✅ ✅ ❌ ❌ ❌ ✅ ❌ blocked on another PR
15942 grunweg chore: move style linters into their own file; document all current linters t-linter merge-conflict awaiting-author ✅ ✅ ✅ ❌ ✅ ❌ ❌ merge conflict
21745 robin-carlier feat(AlgebraicTopology/SimplexCategory/GeneratorsRelations/NormalForms): Normal forms for `P_σ`s t-topology t-category-theory merge-conflict blocked-by-other-PR ✅ ✅ ❌ ❌ ✅ ✅ ❌ blocked on another PR
21746 robin-carlier feat(AlgebraicTopology/SimplexCategory/GeneratorsRelations/NormalForms): Normal forms for `P_δ`s t-topology t-category-theory merge-conflict blocked-by-other-PR ✅ ✅ ❌ ❌ ✅ ✅ ❌ blocked on another PR
21747 robin-carlier feat(AlgebraicTopology/SimplexCategory/GeneratorsRelations): `SimplexCategoryGenRel.toSimplexCategory` is an equivalence t-topology t-category-theory merge-conflict blocked-by-other-PR ✅ ✅ ❌ ❌ ✅ ✅ ❌ blocked on another PR
21748 robin-carlier feat(AlgebraicTopology/SimplexCategory/SimplicialObject): definitions of simplicial objects by generators and relation t-topology t-category-theory merge-conflict blocked-by-other-PR ✅ ✅ ❌ ❌ ✅ ✅ ❌ blocked on another PR
20334 miguelmarco feat: allow polyrith to use a local Singular/Sage install new-contributor t-meta 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
19802 vihdzp refactor(SetTheory/Ordinal/Arithmetic): `Ordinal.IsLimit` → `Order.IsSuccLimit` t-set-theory t-order merge-conflict awaiting-author blocked-by-other-PR ✅ ✅ ❌ ❌ ✅ ❌ ❌ blocked on another PR
18439 ADedecker refactor: use new algebraic filter bases API in `FiniteAdeleRing` t-algebra t-topology merge-conflict blocked-by-other-PR ✅ ✅ ❌ ❌ ✅ ✅ ❌ blocked on another PR
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
20180 ChrisHughes24 feat(ModelTheory): definable functions t-logic merge-conflict blocked-by-other-PR ✅ ✅ ❌ ❌ ✅ ✅ ❌ blocked on another PR
20173 ChrisHughes24 refactor(ModelTheory): tidy up proof of Ax-Grothendieck with definable functions t-logic merge-conflict blocked-by-other-PR ✅ ✅ ❌ ❌ ✅ ✅ ❌ blocked on another PR
21948 ChrisHughes24 feat(ModelTheory): Formula.iSup and iInf t-logic merge-conflict ✅ ✅ ✅ ❌ ✅ ✅ ❌ merge conflict
21769 JovanGerb feat: extensible `push_neg` tactic large-import t-meta merge-conflict ✅ ✅ ✅ ❌ ✅ ✅ ❌ merge conflict
21853 smmercuri feat: the adele ring of a number field is locally compact large-import merge-conflict blocked-by-other-PR WIP ✅ ❌ ❌ ❌ ❌ ✅ ❌ ⚠️ blocked on another PR
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
20593 FR-vdash-bot feat: mixin ordered algebraic typeclasses t-order t-algebra merge-conflict awaiting-author ✅ ✅ ✅ ❌ ✅ ❌ ❌ merge conflict
12054 adomani feat: auto-bugs t-meta merge-conflict awaiting-author ✅ ✅ ✅ ❌ ✅ ❌ ❌ merge conflict
10235 urkud feat: add `Decidable`, `Fintype`, `Encodable` linters awaiting-bench large-import t-linter t-meta merge-conflict awaiting-author ✅ ❌ ✅ ❌ ✅ ❌ ❌ failing CI
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
6718 FR-vdash-bot feat: Lindemann-Weierstrass Theorem t-algebra t-analysis merge-conflict blocked-by-other-PR WIP ✅ ❌ ❌ ❌ ❌ ✅ ❌ blocked on another PR
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
21766 101damnations feat(RepresentationTheory/Homological/GroupHomology/LongExactSequence): specialise LES API to low degree group homology merge-conflict blocked-by-other-PR ✅ ✅ ❌ ❌ ✅ ✅ ❌ ⚠️ blocked on another PR
21764 101damnations feat(RepresentationTheory/Homological/GroupHomology/LongExactSequence): specialise LES API to group homology merge-conflict blocked-by-other-PR ✅ ✅ ❌ ❌ ✅ ✅ ❌ ⚠️ blocked on another PR
21763 101damnations feat(RepresentationTheory/Homological/GroupHomology/Functoriality): low degree functoriality maps merge-conflict blocked-by-other-PR ✅ ✅ ❌ ❌ ✅ ✅ ❌ ⚠️ blocked on another PR
21762 101damnations feat(RepresentationTheory/Homological/GroupHomology/LowDegree): `H₁(G, A) ≃+ Gᵃᵇ ⊗[ℤ] A` when `A` is trivial merge-conflict blocked-by-other-PR ✅ ✅ ❌ ❌ ✅ ✅ ❌ ⚠️ blocked on another PR
21759 101damnations feat(RepresentationTheory/Homological/GroupHomology/LowDegree): Identify `groupHomology A n` with `Hn A` for `n = 0, 1, 2` merge-conflict blocked-by-other-PR ✅ ✅ ❌ ❌ ✅ ✅ ❌ ⚠️ blocked on another PR
21757 101damnations feat(RepresentationTheory/Homological/GroupHomology/LowDegree): add `IsOneCycle` predicate and friends merge-conflict blocked-by-other-PR ✅ ✅ ❌ ❌ ✅ ✅ ❌ ⚠️ blocked on another PR
21754 101damnations feat(RepresentationTheory/Homological/GroupHomology/Functoriality): add functoriality merge-conflict blocked-by-other-PR ✅ ✅ ❌ ❌ ✅ ✅ ❌ ⚠️ blocked on another PR
21755 101damnations feat(RepresentationTheory/Homological/GroupHomology/LowDegree): API for(one/two)(Cycles/Boundaries) merge-conflict blocked-by-other-PR ✅ ✅ ❌ ❌ ✅ ✅ ❌ ⚠️ blocked on another PR
21752 101damnations feat(RepresentationTheory/Homological/GroupHomology/LowDegree): simpler expressions for differentials merge-conflict blocked-by-other-PR ✅ ✅ ❌ ❌ ✅ ✅ ❌ ⚠️ blocked on another PR
21740 101damnations feat(RepresentationTheory/Homological/GroupHomology/Basic): define group homology merge-conflict blocked-by-other-PR ✅ ✅ ❌ ❌ ✅ ✅ ❌ ⚠️ blocked on another PR
21736 101damnations feat(RepresentationTheory/*): `Rep.diagonal k G (n + 1) ≅ Rep.free k G (Fin n → G) ` merge-conflict blocked-by-other-PR ✅ ✅ ❌ ❌ ✅ ✅ ❌ ⚠️ blocked on another PR
21738 101damnations feat(RepresentationTheory/*): add the bar resolution merge-conflict blocked-by-other-PR ✅ ✅ ❌ ❌ ✅ ✅ ❌ ⚠️ blocked on another PR
21735 101damnations feat(RepresentationTheory/Coinvariants): more API about the coinvariants of a representation merge-conflict blocked-by-other-PR ✅ ✅ ❌ ❌ ✅ ✅ ❌ ⚠️ blocked on another PR
21733 101damnations feat(RepresentationTheory/Coinvariants): coinvariants of a representation merge-conflict blocked-by-other-PR ✅ ✅ ❌ ❌ ✅ ✅ ❌ ⚠️ blocked on another PR
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
18534 joelriou feat(LinearAlgebra/PiTensorProduct): dependent version of tmulEquiv t-algebra merge-conflict awaiting-author ✅ ✅ ✅ ❌ ✅ ❌ ❌ merge conflict
13686 fpvandoorn feat: some finset lemmas t-data merge-conflict awaiting-author ✅ ✅ ✅ ❌ ✅ ❌ ❌ merge conflict
20897 yuma-mizuno feat(CategoryTheory/Bicategory): add lemmas about mates in bicategories t-category-theory 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
20241 vasnesterov feat(Data/Seq): coinductive predicates for sequences t-data merge-conflict blocked-by-other-PR ✅ ✅ ❌ ❌ ✅ ✅ ❌ blocked on another PR
21582 jjdishere feat(RingTheory/AdicCompletion): more APIs for IsAdicComplete t-algebra merge-conflict awaiting-author ✅ ✅ ✅ ❌ ✅ ❌ ❌ merge conflict
22331 jjdishere feat(RingTheory/Perfectoid): define integral perfectoid rings t-algebra t-number-theory merge-conflict blocked-by-other-PR WIP ✅ ❌ ❌ ❌ ❌ ✅ ❌ blocked on another PR
22332 jjdishere feat(RingTheory/Perfectoid): Fontaine's theta map is surjective t-algebra t-number-theory merge-conflict blocked-by-other-PR WIP ✅ ❌ ❌ ❌ ❌ ✅ ❌ blocked on another PR
18626 hannahfechtner feat : define Artin braid groups new-contributor t-algebra merge-conflict awaiting-author ✅ ✅ ✅ ❌ ✅ ❌ ❌ merge conflict
22289 robin-carlier feat(CategoryTheory/Sums/Associator): compatibility of products and sums associators large-import t-category-theory merge-conflict blocked-by-other-PR ✅ ✅ ❌ ❌ ✅ ✅ ❌ blocked on another PR
22295 robin-carlier feat(CategoryTheory/Sums/Basic): compatibility of `Sum.functorEquiv` and `Sum.Swap.equivalence` large-import t-category-theory merge-conflict blocked-by-other-PR ✅ ✅ ❌ ❌ ✅ ✅ ❌ blocked on another PR
4979 mhk119 doc(Data/Nat/Bitblast): initial commit merge-conflict ✅ ✅ ✅ ❌ ✅ ✅ ❌ merge conflict
10823 alexkeizer feat: convert curried type functions into uncurried type functions t-data merge-conflict awaiting-author ✅ ✅ ✅ ❌ ✅ ❌ ❌ merge conflict
18486 vasnesterov feat(Tactic): Tactic for computing asymptotics of real functions t-meta merge-conflict WIP ✅ ❌ ✅ ❌ ❌ ✅ ❌ labelled WIP
21158 smmercuri feat: the finite adele ring is locally compact if each of the ring of integers is compact FLT t-algebra merge-conflict blocked-by-other-PR ✅ ✅ ❌ ❌ ✅ ✅ ❌ blocked on another PR
22358 xyzw12345 feat(RingTheory/Artinian): proved some more lemmas about Artinian properties large-import new-contributor merge-conflict blocked-by-other-PR ✅ ❌ ❌ ❌ ✅ ✅ ❌ ⚠️ blocked on another PR
13648 urkud feat(Topology/Module): generalize `ContinuousLinearMap.compSL` t-algebra t-analysis t-topology merge-conflict awaiting-author ✅ ❌ ✅ ❌ ✅ ❌ ❌ failing CI
21714 mattrobball test t-order merge-conflict ✅ ❌ ✅ ❌ ✅ ✅ ❌ failing CI
13964 pechersky feat(Data/DigitExpansion): begin defining variant of reals without rationals t-data merge-conflict ✅ ✅ ✅ ❌ ✅ ✅ ❌ merge conflict
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
16421 FR-vdash-bot feat: `QuotLike` t-data RFC merge-conflict awaiting-author ✅ ✅ ✅ ❌ ✅ ❌ ❌ merge conflict
16837 vihdzp feat(Data/List/SplitBy): characterization of `List.splitBy` t-data 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
22490 joelriou feat(CategoryTheory/Functor): pointwise right derived functors t-category-theory merge-conflict blocked-by-other-PR ✅ ✅ ❌ ❌ ✅ ✅ ❌ blocked on another PR
22147 smmercuri feat: collections of distinct infinite places contain values that diverge around 1 large-import merge-conflict blocked-by-other-PR ✅ ✅ ❌ ❌ ✅ ✅ ❌ ⚠️ blocked on another PR
22153 smmercuri feat: weak approximation theorems for infinite places of a number field large-import merge-conflict ✅ ✅ ✅ ❌ ✅ ✅ ❌ ⚠️ merge conflict
21573 lambda-fairy feat(Computability): regular languages are closed under reversal t-computability merge-conflict ✅ ✅ ✅ ❌ ✅ ✅ ❌ merge conflict
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
22532 jcommelin chore(RingTheory/TensorProduct): cleanup t-algebra merge-conflict WIP ✅ ❌ ✅ ❌ ❌ ✅ ❌ labelled WIP
21858 vihdzp refactor(SetTheory/Ordinal/FixedPoint): redefine `Ordinal.deriv` t-set-theory merge-conflict blocked-by-other-PR ✅ ✅ ❌ ❌ ✅ ✅ ❌ blocked on another PR
22341 chrisflav feat(RingTheory): formulas for `Module.rankAtStalk` for various constructions large-import t-algebra merge-conflict blocked-by-other-PR ✅ ❌ ❌ ❌ ✅ ✅ ❌ blocked on another PR
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
8691 urkud Add `NormedSpace.Alternating` t-analysis merge-conflict awaiting-author ✅ ✅ ✅ ❌ ✅ ❌ ❌ merge conflict
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
22654 101damnations feat(RepresentationTheory/Homological/GroupHomology/Functoriality): the degree 1 part of the corestriction-coinflation exact sequence when the subgroup acts trivially large-import merge-conflict blocked-by-other-PR ✅ ✅ ❌ ❌ ✅ ✅ ❌ ⚠️ blocked on another PR
22656 101damnations feat(RepresentationTheory/Homological/GroupHomology/Functoriality): the degree 1 part of the corestriction-coinflation exact sequence large-import merge-conflict blocked-by-other-PR ✅ ✅ ❌ ❌ ✅ ✅ ❌ ⚠️ blocked on another PR
19315 quangvdao feat(Data/Finsupp/Fin): Add `Finsupp` operations on `Fin` tuple t-data maintainer-merge merge-conflict awaiting-author ✅ ✅ ✅ ❌ ✅ ❌ ❌ merge conflict
22538 vasnesterov feat(Analysis): radius of convergence for binomial series t-analysis merge-conflict blocked-by-other-PR ✅ ✅ ❌ ❌ ✅ ✅ ❌ blocked on another PR
16944 YnirPaz feat(SetTheory/Cardinal/Cofinality): lemmas about limit ordinals and cofinality t-set-theory merge-conflict WIP ✅ ✅ ✅ ❌ ❌ ✅ ❌ labelled WIP
14752 AntoineChambert-Loir fix(Topology/Algebra/Valued): repair definition of Valued t-algebra t-topology merge-conflict WIP ✅ ❌ ✅ ❌ ❌ ✅ ❌ labelled WIP
22603 pechersky chore(Topology): rename pi family from π to X tech debt t-topology merge-conflict ✅ ✅ ✅ ❌ ✅ ✅ ❌ merge conflict
17368 Felix-Weilacher feat(Topology/Baire/BaireMeasurable): add the Kuratowski-Ulam theorem t-topology merge-conflict ✅ ❌ ✅ ❌ ✅ ✅ ❌ failing CI
22779 xroblot feat(NumberField/CanonicalEmbedding/NormLeOne): prove that the frontier of `normLeOne` has zero-volume t-number-theory merge-conflict blocked-by-other-PR ✅ ✅ ❌ ❌ ✅ ✅ ❌ blocked on another PR
22349 dtumad feat(Control): Laws for monads with compatible `failure` operation new-contributor t-meta merge-conflict WIP ✅ ✅ ✅ ❌ ❌ ✅ ❌ labelled WIP
8767 eric-wieser refactor(Cache): tidy lake-manifest parsing in Cache t-meta merge-conflict ✅ ❌ ✅ ❌ ✅ ✅ ❌ failing CI
22403 xyzw12345 feat(RingTheory/Ideal/Height): Krull height theorem large-import new-contributor merge-conflict blocked-by-other-PR ✅ ❌ ❌ ❌ ✅ ✅ ❌ ⚠️ blocked on another PR
22322 mariainesdff feat(RingTheory/DividedPowers/RatAlgebra): add definitions large-import t-algebra merge-conflict WIP ✅ ✅ ✅ ❌ ❌ ✅ ❌ labelled WIP
15578 znssong feat(Function): Fixed points of function `f` with `f(x) >= x` new-contributor t-analysis merge-conflict awaiting-author ✅ ✅ ✅ ❌ ✅ ❌ ❌ merge conflict
22817 peabrainiac feat(CategoryTheory/Sites): local sites t-category-theory merge-conflict blocked-by-other-PR ✅ ✅ ❌ ❌ ✅ ✅ ❌ blocked on another PR
22698 Kiolt feat: notation for whisker(Left/Right)Iso toric merge-conflict ✅ ❌ ✅ ❌ ✅ ✅ ❌ ⚠️ failing CI
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
20171 mitchell-horner feat(Combinatorics/SimpleGraph): define turanDensity large-import new-contributor t-combinatorics merge-conflict blocked-by-other-PR WIP ✅ ✅ ❌ ❌ ❌ ✅ ❌ blocked on another PR
20240 mitchell-horner feat(Combinatorics/SimpleGraph): prove the Kővári–Sós–Turán theorem new-contributor t-combinatorics merge-conflict blocked-by-other-PR WIP ✅ ✅ ❌ ❌ ❌ ✅ ❌ blocked on another PR
22356 xyzw12345 feat(Algebra/Module/Length): proved the equivalence of `IsFiniteLength` and `Module.length ≠ ⊤` large-import new-contributor t-algebra merge-conflict blocked-by-other-PR ✅ ❌ ❌ ❌ ✅ ✅ ❌ blocked on another PR
22805 ScottCarnahan feat (FieldTheory/Finite): fixed points of frobenius t-algebra merge-conflict WIP ✅ ✅ ✅ ❌ ❌ ✅ ❌ labelled WIP
15420 eric-wieser feat: port Mathlib 3's `Nat.factors` norm_num extension to a `simproc` t-meta merge-conflict awaiting-author ✅ ✅ ✅ ❌ ✅ ❌ ❌ merge conflict
22367 joelriou feat(CategoryTheory/Abelian): Noetherian objects form a Serre class t-category-theory merge-conflict WIP ✅ ❌ ✅ ❌ ❌ ✅ ❌ labelled WIP
20873 vbeffara feat(Topology/Covering): path lifting and homotopy lifting new-contributor t-topology merge-conflict ✅ ❌ ✅ ❌ ✅ ✅ ❌ failing CI
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
21564 jjdishere feat(RingTheory/Perfectoid): Fontaine's theta map and the de Rham period rings t-algebra t-number-theory merge-conflict blocked-by-other-PR ✅ ✅ ❌ ❌ ✅ ✅ ❌ blocked on another PR
13999 adomani feat: a linter to flag potential confusing conventions t-linter merge-conflict awaiting-author ✅ ✅ ✅ ❌ ✅ ❌ ❌ merge conflict
20987 adomani feat: a linter to deprecate imported modules large-import t-linter merge-conflict awaiting-author ✅ ✅ ✅ ❌ ✅ ❌ ❌ merge conflict
22760 adomani feat: linting the start of declarations and commands large-import t-linter merge-conflict WIP ✅ ❌ ✅ ❌ ❌ ✅ ❌ labelled WIP
22810 pechersky feat(Counterexamples): metric space not induced by norm t-analysis t-topology merge-conflict ✅ ✅ ✅ ❌ ✅ ✅ ❌ 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
21032 joelriou feat(Order): bicartesian squares in lattices t-order t-category-theory merge-conflict blocked-by-other-PR WIP ✅ ✅ ❌ ❌ ❌ ✅ ❌ blocked on another PR
13578 eric-wieser feat: add a `dsimproc` for vector notation awaiting-CI t-meta merge-conflict ✅ ❌ ✅ ❌ ✅ ❌ ❌ does not pass CI
8102 miguelmarco feat (Tactic): add unify_denoms and collect_signs tactics new-contributor t-meta merge-conflict awaiting-author enhancement ✅ ✅ ✅ ❌ ✅ ❌ ❌ 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
20730 kuotsanhsu feat(LinearAlgebra/Matrix/SchurTriangulation): prove Schur decomposition/triangulation new-contributor merge-conflict awaiting-author ✅ ❌ ✅ ❌ ✅ ❌ ❌ ⚠️ failing CI
20850 vihdzp chore(Logic/Equiv/Basic): extend `sumCompl` API t-data t-logic merge-conflict awaiting-author ✅ ✅ ✅ ❌ ✅ ❌ ❌ merge conflict
13994 grunweg chore(Topology): replace continuity -> fun_prop t-topology merge-conflict ✅ ❌ ✅ ❌ ✅ ✅ ❌ failing CI
18396 sgouezel feat: the Lie algebra of a Lie group over a general field t-differential-geometry merge-conflict blocked-by-other-PR ✅ ✅ ❌ ❌ ✅ ✅ ❌ blocked on another PR
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
21751 vihdzp refactor(SetTheory/Ordinal/Arithmetic): rework `Ordinal.pred` API t-set-theory maintainer-merge merge-conflict ✅ ✅ ✅ ❌ ✅ ✅ ❌ merge conflict
22987 BoltonBailey chore(Logic/Equiv/Basic): split subtype lemmas from file tech debt t-logic merge-conflict ✅ ❌ ✅ ❌ ✅ ✅ ❌ failing CI
22920 chrisflav chore(RingTheory): various api additions t-algebra merge-conflict ✅ ✅ ✅ ❌ ✅ ✅ ❌ merge conflict
23117 pfaffelh Finite unions of sets in a semi-ring (in terms of measure theory) form a ring large-import new-contributor t-measure-probability merge-conflict blocked-by-other-PR ✅ ✅ ❌ ❌ ✅ ✅ ❌ blocked on another PR
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
23138 grunweg feat: (unoriented) bordism groups t-differential-geometry merge-conflict WIP ✅ ❌ ✅ ❌ ❌ ✅ ❌ labelled WIP
15686 robertmaxton42 refactor(LinearAlgebra/FreeProduct): move PowerAlgebra construction to its own namespace, minor simp opts new-contributor t-algebra merge-conflict awaiting-author ✅ ✅ ✅ ❌ ✅ ❌ ❌ merge conflict
21463 riccardobrasca add algEquiv_comp_algebraMap large-import t-algebra t-number-theory merge-conflict WIP ✅ ❌ ✅ ❌ ❌ ✅ ❌ labelled WIP
15158 AntoineChambert-Loir feat(MvPowerSeries/Substitution): substitution of power series inside power series t-algebra merge-conflict ✅ ✅ ✅ ❌ ✅ ✅ ❌ merge conflict
9273 grunweg feat: extended charts are local diffeomorphisms on their source t-differential-geometry merge-conflict blocked-by-other-PR ✅ ✅ ❌ ❌ ✅ ✅ ❌ blocked on another PR
22957 apnelson1 feat(Matrix): row and column functions merge-conflict WIP ✅ ✅ ✅ ❌ ❌ ✅ ❌ ⚠️ labelled WIP
12664 BoltonBailey feat: add lemma about `degreeOf_eq_degree` t-algebra merge-conflict blocked-by-other-PR WIP ✅ ❌ ❌ ❌ ❌ ✅ ❌ blocked on another PR
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 merge-conflict awaiting-author ✅ ✅ ✅ ❌ ✅ ❌ ❌ merge conflict
23040 grunweg feat: define immersions and smooth embeddings in infinite dimensions t-differential-geometry merge-conflict blocked-by-other-PR WIP ✅ ❌ ❌ ❌ ❌ ✅ ❌ blocked on another PR
22583 imathwy feat: affinespace homeomorphism t-algebra merge-conflict awaiting-author ✅ ✅ ✅ ❌ ✅ ❌ ❌ merge conflict
22866 xroblot feat(NumberField/Ideal): asymptotics for the number of integral ideals of bounded norm t-number-theory merge-conflict blocked-by-other-PR ✅ ✅ ❌ ❌ ✅ ✅ ❌ blocked on another PR
8370 eric-wieser refactor(Analysis/NormedSpace/Exponential): remove the `𝕂` argument from `exp` t-analysis RFC merge-conflict ✅ ❌ ✅ ❌ ✅ ✅ ❌ failing CI
15774 kkytola feat: Topology on `ENat` t-order t-topology merge-conflict WIP ✅ ✅ ✅ ❌ ❌ ✅ ❌ labelled WIP
19946 vihdzp feat(SetTheory/ZFC/Basic): order instances t-set-theory merge-conflict awaiting-author ✅ ✅ ✅ ❌ ✅ ❌ ❌ merge conflict
23333 mariainesdff feat(Analysis.Normed.Unbundled.SpectralNormUnique): prove unique extension theorem large-import t-analysis t-number-theory merge-conflict blocked-by-other-PR ✅ ✅ ❌ ❌ ✅ ✅ ❌ blocked on another PR
23137 grunweg chore(Topology): some more fun_prop tagging merge-conflict ✅ ✅ ✅ ❌ ✅ ✅ ❌ merge conflict
17914 xroblot feat(NumberTheory/NumberField): proof of the Analytic Class Number Formula t-number-theory merge-conflict blocked-by-other-PR ✅ ✅ ❌ ❌ ✅ ✅ ❌ blocked on another PR
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
22909 AntoineChambert-Loir feat(RingTheory/Pure): pure submodules t-algebra merge-conflict blocked-by-other-PR ✅ ✅ ❌ ❌ ✅ ✅ ❌ blocked on another PR
18284 chrisflav feat(AlgebraicGeometry): relative gluing of schemes t-algebraic-geometry merge-conflict WIP ✅ ❌ ✅ ❌ ❌ ✅ ❌ labelled WIP
22073 vasnesterov feat(Tactic/Order): frontend for `order` t-meta merge-conflict blocked-by-other-PR ✅ ✅ ❌ ❌ ✅ ✅ ❌ blocked on another PR
22657 Xmask19 feat: a graph is maximally acyclic iff it is a tree new-contributor t-combinatorics merge-conflict ✅ ✅ ✅ ❌ ✅ ✅ ❌ merge conflict
19796 peakpoint feat: Peano form of Taylor's theorem new-contributor t-analysis merge-conflict awaiting-author ✅ ✅ ✅ ❌ ✅ ❌ ❌ merge conflict
23301 mariainesdff feat(Analysis/Normed/Unbundled/SpectralNorm): add spectral norm large-import t-analysis t-number-theory merge-conflict blocked-by-other-PR ✅ ✅ ❌ ❌ ✅ ✅ ❌ blocked on another PR
16733 pechersky feat(Topology/Algebra/Valued/LocallyCompact): locally compact nonarchimedean field iff complete and DVR and finite field large-import t-algebra merge-conflict ✅ ✅ ✅ ❌ ✅ ✅ ❌ merge conflict
21356 Multramate chore(AlgebraicGeometry/EllipticCurve/Affine): split affine files t-algebraic-geometry 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 ✅ ✅ ✅ ❌ ✅ ✅ ❌ merge conflict
23211 Parcly-Taxel chore: automatically deprime common `induction'` uses tech debt merge-conflict ✅ ✅ ✅ ❌ ✅ ✅ ❌ merge conflict
23350 faenuccio chore: change UniformGroup to IsUniformGroup t-algebra t-topology merge-conflict WIP ✅ ❌ ✅ ❌ ❌ ✅ ❌ labelled WIP
19695 Timeroot feat(ModelTheory): Set.Definable is transitive large-import t-logic merge-conflict ✅ ✅ ✅ ❌ ✅ ✅ ❌ merge conflict
22930 chrisflav refactor(RingTheory/RingHom): factor out proofs for `Algebra.FinitePresentation` large-import t-algebra merge-conflict blocked-by-other-PR ✅ ✅ ❌ ❌ ✅ ✅ ❌ blocked on another PR
22931 chrisflav refactor(RingTheory/RingHom): factor out proofs for `Algebra.FiniteType` large-import t-algebra merge-conflict blocked-by-other-PR ✅ ✅ ❌ ❌ ✅ ✅ ❌ blocked on another PR
23451 loefflerd refactor: protect "map_add" lemmas merge-conflict ✅ ✅ ✅ ❌ ✅ ✅ ❌ merge conflict
20613 grunweg chore: golf using `List.toArrayMap` large-import merge-conflict ✅ ❌ ✅ ❌ ✅ ✅ ❌ failing CI