Why is my PR not on the queue?

This page was last updated on: August 21, 2025 at 01:25 UTC

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

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

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

Number Author Title Labels CI status? not blocked? no merge conflict? ready? awaiting review? On the review queue? Missing topic label? PR's overall status
14345 digama0 feat: the Dialectica category is monoidal closed t-category-theory awaiting-author awaiting author
14444 digama0 fix(GeneralizeProofs): unreachable! bug t-meta awaiting-author awaiting author
13036 joelriou feat(CategoryTheory/Sites): under certain conditions, cover preserving functors preserve 1-hypercovers t-category-theory WIP labelled WIP
12452 JADekker feat(Cocardinal) : add some more api t-topology awaiting-CI does not pass CI
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
9510 eric-wieser feat(Analysis/Calculus/DualNumber): Extending differentiable functions to dual numbers t-algebra t-analysis awaiting-CI WIP labelled WIP
9352 chenyili0818 feat: arithmetic lemmas for `gradient` t-analysis awaiting-author awaiting author
9469 dupuisf feat: maximum modulus principle for functions vanishing at infinity t-analysis awaiting-author awaiting author
7125 eric-wieser feat: additive monoid structure via biproducts t-category-theory awaiting-CI WIP labelled WIP
6859 MohanadAhmed TryLean4Bundle: Windows Bundle Creator CI WIP help-wanted looking for help
5745 alexjbest feat: a tactic to consume type annotations, and make constructor nicer t-meta awaiting-author awaiting author
15224 AnthonyBordg feat(CategoryTheory/Sites): covering families and their associated Grothendieck topology new-contributor t-category-theory awaiting-author awaiting author
14563 awueth feat: if-then-else of exclusive or statement new-contributor t-algebra awaiting-author awaiting author
10387 adomani feat(Tactic/ComputeDegree): add `polynomial` tactic RFC t-meta WIP labelled WIP
9693 madvorak feat: Linear programming in the standard form t-algebra RFC WIP labelled WIP
7386 madvorak feat: Define linear programs t-algebra RFC WIP labelled WIP
7219 Ruben-VandeVelde feat: Equivs for AddMonoidAlgebras t-algebra awaiting-author failing CI
13163 erdOne feat(.vscode/module-docstring.code-snippet): Prevent auto-complete from firing on `do` t-meta awaiting-author awaiting author
10026 madvorak Linear programming according to Antoine Chambert-Loir's book t-algebra RFC WIP labelled WIP
10159 madvorak Linear programming according to Antoine Chambert-Loir's book — affine version t-algebra RFC WIP labelled WIP
11890 adomani feat: the terminal refine linter t-linter awaiting-author awaiting author
11207 luigi-massacci feat(Topology/MetricSpace): Add new file with type of Katetov maps new-contributor t-topology WIP ??? labelled WIP
11090 pangelinos feat: define spectral spaces and prove that a quasi-compact open of a spectral space is spectral new-contributor t-topology please-adopt good first issue looking for help
9795 sinhp feat: the type `Fib` of fibre of a function at a point t-category-theory awaiting-author awaiting author
15055 sinhp feat: the category of pointed objects of a concrete category t-category-theory awaiting-author awaiting author
16253 Shreyas4991 feat: Basics of Discrete Fair Division in Mathlib awaiting-author WIP ⚠️ labelled WIP
15121 Eloitor feat: iff theorems for IsSplitEpi and IsSplitMono in opposite category new-contributor t-category-theory awaiting-author failing CI
15895 madvorak feat(Computability/ContextFreeGrammar): mapping between two types of nonterminal symbols t-computability WIP labelled WIP
12278 Rida-Hamadani feat(Combinatorics/SimpleGraph): Provide iff statements for distance equal and greater than 2 t-combinatorics awaiting-author failing CI
16570 yuma-mizuno chore(Tactic/CategoryTheory): change `TermElabM` to `MetaM` t-meta WIP labelled WIP
10591 adri326 feat(Topology/Algebra/ConstMulAction): properties of continuous actions in Hausdorff spaces t-algebra t-topology awaiting-author awaiting author
16773 arulandu feat(Probability/Distributions): formalize Beta distribution new-contributor t-measure-probability awaiting-author failing CI
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
6042 MohanadAhmed feat(LinearAlgebra/Matrix/SVD): Singular Value Decomposition of R or C Matrices t-algebra please-adopt WIP looking for help
19329 adomani perf(CI): automatically benchmark PRs when they are opened CI WIP labelled WIP
18236 joelriou feat(Algebra/Category/ModuleCat/Presheaf): the endofunctor of presheaves of modules induced by an oplax natural transformation t-algebra t-category-theory WIP labelled WIP
20459 Ruben-VandeVelde chore: fix names of roots_C_mul_X_{add,sub}_C_of_IsUnit t-algebra awaiting-author awaiting author
10977 grunweg feat: germs of smooth functions t-analysis t-topology t-differential-geometry awaiting-author failing CI
19378 adamtopaz feat: Explanation widgets t-meta awaiting-author awaiting author
19323 madvorak feat: Function to Sum decomposition t-data WIP labelled WIP
18461 hannahfechtner feat: left and right common multiples mixins new-contributor t-algebra awaiting-author awaiting author
20797 vbeffara feat(Topology/Covering): CM version of eq_of_comp_eq new-contributor t-topology easy awaiting-author awaiting author
17589 joelriou feat(Algebra/ModuleCat/Presheaf): composition of pushforwards and pullbacks and compatibilites t-algebraic-geometry t-category-theory WIP labelled WIP
21009 vihdzp feat(Logic/Relation): more `TransGen` lemmas t-logic t-order awaiting-author awaiting author
15443 YaelDillies feat: The Marcinkiewicz-Zygmund inequality t-analysis WIP labelled WIP
20466 MohanadAhmed feat: Sherman Morrison formula for rank 1 update of the matrix inverse t-data awaiting-author awaiting author
18749 GabinKolly feat(ModelTheory): preparatory work for the existence of Fraïsse limits t-logic awaiting-author awaiting author
20649 GabinKolly feat(ModelTheory/Graph): prove characterization of the fraisse limit of finite simple graphs large-import t-logic t-combinatorics WIP labelled WIP
10660 eric-wieser feat(LinearAlgebra/CliffordAlgebra): construction from a basis t-algebra awaiting-author WIP labelled WIP
15355 adomani feat: MiM PR report WIP ⚠️ labelled WIP
21495 alreadydone experiment: reducible HasQuotient.quotient' bench-after-CI WIP labelled WIP
21447 erdOne feat(AlgebraicGeometry): the split algebraic torus t-algebraic-geometry awaiting-author awaiting author
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
19062 hannahfechtner feat(Algebra/PresentedMonoid/Basic) : facts about rel t-algebra awaiting-author awaiting author
22302 CharredLee feat: add `CategoryTheory.Topos.Power` new-contributor t-category-theory awaiting-author awaiting author
20636 eric-wieser feat: multiplication of intervals in rings t-algebra awaiting-author awaiting author
22642 grunweg WIP: add `mfderiv_prod` and `mfderiv_prodMap` t-differential-geometry WIP labelled WIP
22784 grunweg feat: add Diffeomorph.sumSumSumComm t-differential-geometry WIP labelled WIP
22159 shetzl feat: add definition of pushdown automata t-computability new-contributor awaiting-author awaiting author
23042 joneugster feat(CategoryTheory/Enriched/Limits): add HasConicalLimitsOfSize.shrink infinity-cosmos t-category-theory WIP labelled WIP
16239 Rida-Hamadani feat(Geometry/Manifold): orientable manifolds t-differential-geometry awaiting-author failing CI
23142 joneugster feat(CategoryTheory/Enriched/Limits): add API for HasConicalLimit infinity-cosmos t-category-theory awaiting-author awaiting author
23285 AntoineChambert-Loir refactor: directed systems in terms of functors large-import t-algebra t-category-theory WIP labelled WIP
21829 Whysoserioushah feat(LinearAlgebra/TensorProduct/HomTensor): Add TensorProduct of Hom-modules t-algebra awaiting-author awaiting author
22861 eric-wieser feat: add the trace of a bilinear form t-algebra awaiting-author awaiting author
22888 plp127 perf: replace `Lean.Expr.swapBVars` with a better? implementation t-meta awaiting-author awaiting author
23772 SEU-Prime Create Amice.lean t-number-theory WIP ??? labelled WIP
21903 yhtq feat: add from/toList between `FreeSemigroup` and `List` with relative theorems large-import new-contributor t-algebra awaiting-CI does not pass CI
22657 Xmask19 feat: a graph is maximally acyclic iff it is a tree new-contributor t-combinatorics failing CI
23154 vlad902 feat(Algebra/FreeMonoid): isomorphisms for the free monoid on zero/one generators t-algebra awaiting-author awaiting author
23866 kim-em chore: remove `[AtLeastTwo n]` hypothesis from the `NatCast` to `OfNat` instance awaiting-zulip failing CI
21342 YaelDillies refactor(Normed/Group/Quotient): generalise to non-abelian groups t-analysis WIP labelled WIP
24000 YaelDillies feat: correspondence between Hopf algebras and affine group schemes toric FLT t-algebraic-geometry WIP labelled WIP
21270 GabinKolly feat(ModelTheory/Bundled): first-order embeddings and equivalences from equalities large-import t-logic awaiting-author awaiting author
13038 adomani feat: Mathlib weekly reports CI t-meta awaiting-author awaiting author
19613 madvorak refactor(Combinatorics/Optimization/ValuedCSP): make only valid `FractionalOperation` possible t-combinatorics failing CI
23600 mattrobball perf(Quiver.Basic): make `IsThin` a `class` delegated delegated
24219 Paul-Lez feat: linear independence of the tensor product of two linearly independent families toric t-algebra WIP labelled WIP
13740 YaelDillies feat: More robust ae notation t-measure-probability awaiting-CI t-meta does not pass CI
20652 jjaassoonn feat: categorical description of center of a ring t-algebra t-category-theory awaiting-author failing CI
21616 peabrainiac feat(Topology): concatenating countably many paths t-topology awaiting-author awaiting author
18210 vihdzp feat(Order/Hom/Basic): `WithBot (Fin n) ≃o Fin (n + 1)` t-order awaiting-author awaiting author
23585 plp127 feat: `Filter.atMax` and `Filter.atMin` t-order WIP labelled WIP
22349 dtumad feat(Control): Laws for monads with compatible `failure` operation new-contributor t-meta WIP labelled WIP
12032 mcdoll feat: Delta distribution as a limit t-analysis WIP labelled WIP
24157 urkud feat(Convex/LinearIsometry): new file t-analysis awaiting-author awaiting author
18861 YaelDillies refactor: make `Set.mem_graphOn` defeq t-data awaiting-author failing CI
23503 apnelson1 feat(Topology/Instances/ENat): ENat and tsum large-import t-topology WIP labelled WIP
22809 b-reinke feat: Category algebras and path algebras new-contributor t-algebra t-category-theory WIP labelled WIP
24574 JovanGerb chore(Order/Notation): check for pp options in `delabSup` t-order failing CI
22488 smmercuri fix: lower priority for `UniformSpace.Completion.instSMul` FLT t-topology awaiting-author awaiting author
15649 TpmKranz feat(Computability): introduce Generalised NFA as bridge to Regular Expression awaiting-zulip t-computability new-contributor awaiting-author awaiting a zulip discussion
20648 anthonyde feat: formalize regular expression -> εNFA awaiting-zulip t-computability new-contributor awaiting a zulip discussion
23220 mattrobball refactor(Module.LinearMap.Defs): make `SemilinearMapClass` extend `AddMonoidHomClass` t-algebra awaiting-author awaiting author
24665 Komyyy feat(Mathlib/Topology/Metrizable/Uniformity): every uniform space is generated by a family of pseudometrics t-topology WIP labelled WIP
23213 mattrobball chore(RingTheory.Derivation): add a `LinearMapClass` instance t-algebra delegated delegated
23214 mattrobball perf(Module.LinearMap.Defs): deprioritize projections to parents for `SemilinearMapClass` t-algebra delegated delegated
24155 eric-wieser feat: add a "rw_proc" for fin vectors t-data RFC t-meta awaiting-author awaiting author
22314 shetzl feat: add leftmost derivations for context-free grammars t-computability new-contributor awaiting-author awaiting author
21276 GabinKolly feat(ModelTheory/Substructures): define equivalences between equal substructures t-logic awaiting-author awaiting author
23137 grunweg chore(Topology): some more fun_prop tagging t-topology delegated delegated
24532 robertmaxton42 feat(LinearAlgebra/FreeProduct): fill out the `FreeProduct.asPowers` namespace t-algebra failing CI
24008 meithecatte chore(EpsilonNFA): replace manual lemmas with @[simps] t-computability new-contributor awaiting-author awaiting author
24618 b-mehta feat(Analysis): add Schur inequality and variants t-analysis WIP labelled WIP
24957 eric-wieser feat: use ` binderNameHint` in sum_congr t-algebra failing CI
5919 MithicSpirit feat: implement orthogonality for AffineSubspace new-contributor t-analysis WIP help-wanted looking for help
10235 urkud feat: add `Decidable`, `Fintype`, `Encodable` linters awaiting-bench large-import t-linter t-meta awaiting-author failing CI
22539 joelriou feat(Algebra/Homology): construction of left resolutions t-category-theory WIP labelled WIP
21624 sinhp feat(CategoryTheory): The (closed) monoidal structure on the product category of families of (closed) monoidal categories t-category-theory awaiting-author failing CI
24333 xcloudyunx feat(Combinatorics/SimpleGraph): cycle graph implementation for generic vertex types new-contributor t-combinatorics awaiting review
25135 vasnesterov WIP/test PR for faster `tauto` large-import t-meta WIP labelled WIP
11155 smorel394 feat(LinearAlgebra/Multilinear/DirectSum, LinearAlgebra/DirectSum/{PiTensorProduct,Finsupp}): interaction between `MultilinearMap` and `DirectSum`, and between `PiTensorProduct` and `DirectSum` t-algebra please-adopt looking for help
19456 AntoineChambert-Loir feat(Data/Finsupp/MonomialOrder/DegRevLex): homogeneous reverse lexicographic order t-data t-order t-algebraic-geometry WIP labelled WIP
24050 Paul-Lez feat(Data/Finsupp/Pointwise): generalise pointwise scalar multiplication of finsupps t-data awaiting review
25208 erdOne feat(LinearAlgebra): `tensor_induction` macro t-algebra RFC WIP labelled WIP
24690 ScottCarnahan feat (Data.Prod): Reverse lexicographic order t-order WIP labelled WIP
22919 plp127 feat(Data/Fintype/Pi): Make `Fintype` instance for `RelHom`s computable t-data awaiting-author awaiting author
24065 kim-em chore: script to give topological sort of modules awaiting-author awaiting author
20238 maemre feat(Computability/DFA): Closure of regular languages under some set operations awaiting-zulip t-computability new-contributor awaiting-author awaiting a zulip discussion
25473 adomani feat(CI): check that Mathlib files have lean or md extension CI delegated delegated
18693 Ruben-VandeVelde feat: add ConjRootClass new-contributor t-algebra delegated delegated
23992 robertmaxton42 feat (Limits.FunctorCategory): limitIsoFlipCompLim and colimitIsoFlipCompColim are natural new-contributor t-category-theory awaiting-CI does not pass CI
24441 MrSumato feat(Data/List): add Lyndon-Schutzenberger theorem on list commutativity t-data new-contributor awaiting-author awaiting author
23240 urkud feat(Topology/Maps): `IsOpenMap` and `ClusterPt` t-topology delegated delegated
24612 Paul-Lez feat(Tactic/ImportDiff): add `#import_diff` command will-close-soon t-meta awaiting-author awaiting author
23929 meithecatte feat(Computability/NFA): improve bound on pumping lemma awaiting-zulip t-computability new-contributor awaiting a zulip discussion
24692 ScottCarnahan feat (RingTheory/HahnSeries/Basic): isomorphism of Hahn series induced by order isomorphism t-order WIP labelled WIP
25035 ScottCarnahan feat (Algebra/Module/Equiv/Defs): Linear equivalence between linear hom and semilinear hom. t-algebra WIP labelled WIP
25034 ScottCarnahan feat (Algebra/Module/Equiv/Basic): Restriction of scalars from a semilinear equivalence to a linear equivalence. t-algebra WIP labelled WIP
24669 qawbecrdtey feat(Analysis/Normed/Operator/LinearIsometry): added definition `LinearIsometryEquiv.prodComm` maintainer-merge t-analysis awaiting-author awaiting author
24540 robertmaxton42 feat(Quiv): add the empty, vertex, point, interval, and walking quivers t-category-theory awaiting-author failing CI
25637 Timeroot feat(Analysis/Convex): Lifting convex sets along scalar towers t-analysis awaiting-author awaiting author
22790 mhk119 feat: Extend `taylor_mean_remainder_lagrange` to `x < x_0` new-contributor t-analysis awaiting-author awaiting author
21344 kbuzzard chore: attempt to avoid diamond in OreLocalization t-algebra please-adopt looking for help
25585 Paul-Lez feat(Tactic/Linters/DeprecatedSimpLemma): lint for deprecated simp lemmas t-linter awaiting-author failing CI
25799 dagurtomas feat(CategoryTheory): the universal property of localized monoidal categories t-category-theory WIP labelled WIP
25802 dagurtomas feat(AlgebraicTopology): anodyne morphisms of simplicial sets t-topology WIP labelled WIP
25835 erdOne WIP: Weierstrass elliptic functions t-analysis WIP labelled WIP
25765 JovanGerb feat(gcongr): lemma for rewriting inside divisibility t-data delegated delegated
25700 grunweg RFC: lint upon uses of the `mono` tactic t-linter RFC failing CI
25921 BoltonBailey feat: scripts to analyze overlap between namespaces migrated-from-branch t-meta WIP labelled WIP
26085 grunweg feat: disjoint unions distribute with products of manifolds t-differential-geometry please-adopt WIP looking for help
26088 grunweg chore(Linter/DirectoryDependency): move forbidden directories into a JSON file t-linter failing CI
25971 joelriou feat(CategoryTheory): pseudofunctors to Cat t-category-theory awaiting-author awaiting author
25803 erdOne feat: taylor expansion of `1 / z ^ r` t-analysis awaiting-author awaiting author
26239 BoltonBailey feat: add sample pre-commit git hook file WIP ⚠️ labelled WIP
26231 chrisflav feat(CategoryTheory/Sites): sheaf condition and coproducts t-category-theory awaiting-author awaiting author
25603 callesonne feat(Bicategory/InducedBicategory): add induced bicategories t-category-theory awaiting-author awaiting author
24395 rudynicolop feat(Data/List): list splitting definitions and lemmas t-data new-contributor awaiting-author awaiting author
26284 plp127 feat: faster implementation of `Nat.primeFactorsList` + `@[csimp]` lemma t-data awaiting review
26292 RemyDegenne feat(MeasureTheory): tightness of the range of a sequence t-measure-probability awaiting-author failing CI
26293 RemyDegenne feat: tightness from convergence of characteristic functions t-measure-probability WIP labelled WIP
20924 tomaz1502 feat(Computability/QueryComplexity): Oracle-based computation t-computability failing CI
22089 sgouezel feat: composing a continuous multilinear map with continuous linear maps is analytic in both variables t-analysis awaiting-author awaiting author
26087 grunweg feat: a `SliceModel` typeclass for models with corners for embedded submanifolds t-differential-geometry failing CI
26389 jjdishere feat(RingTheory): Perfectoid Field t-algebra t-analysis t-topology WIP labelled WIP
26390 jjdishere feat(Topology/Algebra): Krasner's lemma t-algebra t-topology t-number-theory WIP labelled WIP
26376 maddycrim Simons2025 large-import new-contributor WIP labelled WIP
26432 AntoineChambert-Loir feat(Data.Nat.LogFueled): fueled version of `clog` t-data failing CI
25739 literandltx feat(NumberTheory/LegendreSymbol): Add sqrt‐of‐residue theorems for p=4k+3 and p=8k+5 new-contributor t-number-theory awaiting-author awaiting author
25993 Multramate feat(Algebra/Group/Units/Hom): add map lemmas t-algebra awaiting-author awaiting author
26013 tsuki8 feat(Data/Finset/Card,Data/Set/Finite/Basic) t-data new-contributor awaiting-author awaiting author
26348 mans0954 WIP: feature(Analysis/LocallyConvex/Prime): The prime map t-analysis WIP labelled WIP
26283 kckennylau (WIP) Resultant t-algebra WIP labelled WIP
22039 YaelDillies feat: simproc for computing `Finset.Ixx` of natural numbers large-import t-meta awaiting review
26710 metakunt feat (Data/Nat/Digits/Lemmas): Add digits_getD t-data new-contributor awaiting review
26743 grunweg WIP: product rule for Lie bracket on manifolds t-differential-geometry WIP labelled WIP
16303 grunweg feat(CI): check for badly formatted titles or missing/contradictory labels CI awaiting-author failing CI
24383 YaelDillies feat: distributive Haar characters of `ℝ` and `ℂ` file-removed FLT t-measure-probability awaiting-CI WIP labelled WIP
26021 vasnesterov feat(Data/Real): representation of reals from `[0, 1]` in positional system t-data awaiting review
20784 eric-wieser fix: prevent `exact?` recursing forever on `n = 55` t-set-theory failing CI
26648 eric-wieser chore(TensorProduct): remove more `suppress_compilation`s tech debt t-algebra blocked-by-core-PR blocked on another PR
26449 faenuccio feat(NumberTheory/LocalFields/Basic): provide the definition of (valued) Local Field t-algebra t-number-theory WIP labelled WIP
26920 yuma-mizuno feat(Tactic.CategoryTheory): add associator inserting tactic t-category-theory t-meta WIP labelled WIP
26935 Paul-Lez feat(Analysis/SpecialFunction/NthRoot): definition and basic API of Real.nthRoot t-analysis failing CI
26990 joelriou feat(CategoryTheory/Abelian): Noetherian objects form a Serre class t-category-theory WIP labelled WIP
26994 Paul-Lez feat(Topology/MetricSpace/Pseudo/Defs): add easy lemma about opens in topological spaces t-topology easy awaiting-author awaiting author
26838 vlad902 feat: add lemmas about `List.scanr` t-data awaiting review
27069 FrankieNC feat(Analysis/MetricSpace/HausdorffDimension): prove dimH of intervals and segments is 1 new-contributor t-topology awaiting-author awaiting author
25930 loefflerd WIP towards Hecke bound for q-expansions migrated-from-branch t-number-theory WIP labelled WIP
27155 Pjotr5 Proof of Shearers bound on the independence number of triangle free graphs new-contributor t-combinatorics failing CI
11563 YaelDillies feat: `∑ i ∈ s with hi : p i, f i hi` syntax for big operators t-algebra t-meta awaiting review
27206 grhkm21 feat(CategoryTheory/Adjunction): partial adjoints are adjoints t-category-theory failing CI
18230 digama0 feat(Tactic/ScopedNS): extend `scoped[NS]` to more commands t-meta awaiting-author awaiting author
26338 mans0954 feat(Order/ScottContinuity): Scott continuity on product spaces t-order awaiting-author awaiting author
26962 themathqueen feat(Data/Nat/Fib/Basic): some API for `Nat.fib` t-data new-contributor awaiting-author awaiting author
27233 ctchou feat: prove some properties of linearly ordered tuples of a linearly ordered typeFin ordered tuple new-contributor t-order awaiting-author awaiting author
27242 hugh-fox feat: add Gauss-like formula for sums of digit sums large-import t-data new-contributor awaiting review
27323 kckennylau chore: make the arguments of fiberInclusion explicit t-category-theory failing CI
27187 Komyyy feat: `NONote` represents ordinals < ε₀ t-set-theory WIP labelled WIP
26803 bjoernkjoshanssen feat: second partial derivatives test t-analysis awaiting-author awaiting author
27262 Timeroot feat(Tactic/Bound): bound? for proof scripts t-meta failing CI
26847 joelriou feat: multicoequalizers in the category of types t-category-theory awaiting review
12006 adomani feat: the `suffa` tactic t-meta awaiting-author ??? missing CI information
27435 callesonne feat(Normed/Algebra/Logarithm): add FormalMultilinearSeries of logarithm around `1` t-analysis WIP labelled WIP
27271 ctchou feat: prove that each (total) preorder is an extension of a (linear) partial order large-import new-contributor t-order awaiting-author awaiting author
26393 winstonyin feat: solutions to $C^n$ vector fields are $C^n$ in time t-dynamics t-analysis awaiting-author awaiting author
21915 YaelDillies feat: simproc for `Int.divisorsAntidiag` t-meta WIP labelled WIP
27507 grunweg wip(commandStart): check the indentation of declaration keywords also t-linter WIP labelled WIP
26594 metakunt feat(Algebra/Polynomial/ZMod): Add Polynomial.equiv_of_nat_of_polynomial_zmod new-contributor t-algebra awaiting-author awaiting author
27500 Komyyy feat: the Riemann zeta function is meromorphic large-import t-analysis awaiting review
27548 euprunin chore(Control/Functor/Multivariate): remove use of `erw` in `f` (`private def f`) t-data awaiting review
26031 joelriou feat(Algebra/Homology): the derived category of a linear abelian category is linear t-category-theory awaiting review
27566 wwylele feat(Data/Real): Archimedean.embedReal is a ring hom when M is an ordered ring large-import t-data awaiting review
25945 adomani feat: the empty line in commands linter large-import t-linter maintainer-merge awaiting-author awaiting author
22464 adomani feat(CI): declarations diff in Lean CI awaiting-author awaiting author
27422 vihdzp feat: relate images to pointwise negation/inverses t-data t-algebra awaiting-author awaiting author
26836 mans0954 feat(Order/Lattice): conditions for an equivalence relation to be a lattice congruence t-order awaiting-author awaiting author
27682 FernandoChu Chore: Added `vecAppend_empty` lemma t-data new-contributor awaiting review
27297 hugh-fox feat: add an equality between sums and products of cartesian products new-contributor t-algebra awaiting-author awaiting author
25864 plp127 feat(Nat/Digits): use fuel in `Nat.digits` t-data awaiting review
25875 robin-carlier feat(CategoryTheory/Monoidal/Action): actions as monoidal functors to endofunctors t-category-theory awaiting review
26945 gasparattila feat(LinearAlgebra/AffineSpace/AffineSubspace): basic properties of `sInf` and `iInf` new-contributor t-algebra awaiting review
26986 WangYiran01 feat(Partition): add bijection for partitions with max part ≤ r new-contributor t-combinatorics awaiting review
27098 Paul-Lez feat(Algebra/Category/ModuleCat/Sheaf/VectorBundle): define vector bundles t-algebra awaiting-author awaiting author
27697 BoltonBailey chore(Data/Fintype): use `univ` instead of `Fintype.elems` t-data awaiting review
27053 tb65536 (WIP) Galois group of `x^n - x - 1` large-import t-algebra WIP labelled WIP
25889 plp127 fix(Tactic/Widget/Conv): fix various issues t-meta awaiting review
27738 ChrisHughes24 feat(Rat): Decidable instance for IsSquare t-data awaiting review
26155 xroblot feat(DedekindDomain/Different): add the transitivity formula large-import t-algebra awaiting review
26453 jburroni feat(Data/PNat/Basic): add order-related instances to PNat large-import t-data new-contributor awaiting review
26790 FlAmmmmING feat(Combinatorics/Enumerative/Bell.lean): define standard Bell number new-contributor t-combinatorics awaiting review
26793 FlAmmmmING feat(Algebra/Group /ForwardDiff.lean): add five theorems for forward difference large-import new-contributor t-algebra awaiting review
27742 ChrisHughes24 feat(Nat/nth): inequalities about Nat.nth t-data awaiting review
27704 vihdzp feat: link `Minimal` and `IsLeast` together t-order awaiting-author failing CI
14237 js2357 feat: Define the localization of a fractional ideal at a prime ideal new-contributor t-algebra awaiting-author failing CI
25225 xcloudyunx feat(Combinatorics/SimpleGraph): Eulerian walk in connected graph contains all vertices new-contributor t-combinatorics awaiting review
25856 MichaelStollBayreuth perf(Data.Real.Sqrt): make Real.sqrt irreducible migrated-from-branch t-data awaiting review
26287 mbkybky feat(Data/ENat/Lattice): coercion to `WithBot ℕ∞` commutes with `biSup` t-data awaiting review
26370 b-mehta chore(Archive): golf and generalise ascending-descending sequences t-data awaiting review
26909 gasparattila feat(LinearAlgebra/Projectivization/Subspace): correspondence between linear and projective subspaces new-contributor t-algebra awaiting review
27756 grunweg feat: `Weak(Pseudo)EMetricSpace`, generalises `(Pseudo)EMetricSpace` carleson t-topology WIP labelled WIP
25500 eric-wieser feat: delaborators for metadata large-import t-meta awaiting review
26189 tb65536 feat(FieldTheory/Galois/Basic): Add simp-lemma for `FixedPoints.intermediateField` t-algebra awaiting review
26841 xroblot feat(FieldTheory/IsGalois): map induced by the restriction to a subfield t-algebra awaiting review
27066 vasnesterov feat(Tactic/Order): frontend for `order` t-meta awaiting review
27304 jano-wol feat: invariant dual submodules define Lie ideals t-algebra awaiting review
25989 Multramate feat(NumberTheory/EllipticDivisibilitySequence): add elliptic nets t-number-theory awaiting-author awaiting author
27701 vihdzp feat: `a < b + c ↔ a < b ∨ ∃ d < c, a = b + d` t-algebra awaiting-author awaiting author
26843 vasnesterov feat(Tactic/Simproc): nested quantifiers in `existsAndEq` migrated-from-branch large-import t-meta awaiting review
25069 erdOne feat(EllipticCurve): rational points of singular nodal cubics t-algebraic-geometry awaiting review
25861 robin-carlier feat(CategoryTheory/Monoidal/Action): action of opposite categories t-category-theory awaiting review
25907 mans0954 Low order roots of unity t-algebra awaiting review
27047 YaelDillies feat: `MonoidHom.toAdditive''` as a `MulEquiv` toric t-algebra awaiting review
27813 javra feat: IMO 2025 Q1 IMO WIP labelled WIP
27820 FLDutchmann chore(NumberTheory/SelbergSieve): turn `BoundingSieve` into a struct t-analysis t-number-theory awaiting review
22366 kim-em feat: `check_equalities` tactic for diagnosing defeq problems t-meta delegated failing CI
27479 iu-isgood Abel's Binomial Theorem - REU Project t-data new-contributor awaiting-author failing CI
27683 dupuisf feat: grind tags for set operations t-data failing CI
27753 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
26931 javra feat(CategoryTheory/Enriched): `V`-enriched isomorphisms infinity-cosmos t-category-theory awaiting-author awaiting author
25481 kbuzzard chore: refactor Algebra.TensorProduct.rightAlgebra t-algebra delegated delegated
27829 dupuisf feat: modify `cfc_tac` to use `grind` WIP ⚠️ labelled WIP
25974 scholzhannah feat(Topology/Compactness/CompactlyCoherentSpace): compact coherentification (k-ification) large-import t-topology awaiting review
27826 Louddy feat(Subsemiring): mk_eq_zero t-algebra WIP labelled WIP
27841 CBirkbeck feat(Topology/Algebra/InfiniteSum/NatInt): add more pnat tsum lemmas t-topology help-wanted looking for help
27257 JovanGerb feat(LinearAlgebra/AffineSpace/Ordered): add `lineMap_le_lineMap_iff_of_lt'` maintainer-merge t-algebra awaiting-author awaiting author
23460 Timeroot feat: Definition of `Clone` t-algebra awaiting review
22662 plp127 feat: Localization.Away.lift (computably) t-algebra awaiting review
25758 YaelDillies chore: shortcut instance `CompleteLattice α → PartialOrder α` t-order awaiting review
25843 mitchell-horner feat(Combinatorics/SimpleGraph): define `between` subgraphs t-combinatorics awaiting review
26398 ChrisHughes24 feat(ModelTheory): definable functions t-logic awaiting review
26462 PSchwahn feat(LinearAlgebra/Projection): add results about inverse of `Submodule.prodEquivOfIsCompl` new-contributor t-algebra awaiting review
26870 grunweg feat: mdifferentiableOn_section_of_mem_baseSet₀ t-differential-geometry awaiting review
27050 BoltonBailey doc(Control/Monad/Cont): add docstrings t-data awaiting-author failing CI
26290 BeibeiX0 feat(Combinatorics/Enumerative/Stirling.lean): define Stirling numbers of the first and second kind new-contributor t-combinatorics awaiting-author awaiting author
26955 mariainesdff feat(LinearAlgebra/OnSup): extend linear maps to sums of modules t-algebra awaiting review
27864 BoltonBailey feat(Data/{Finset,Multiset}/Sort): give sort functions ≤ default argument t-data awaiting review
25916 BoltonBailey feat: add `simp` lemma `coeff_eq_zero_of_not_mem_support` t-algebra awaiting-author failing CI
25920 BoltonBailey feat(Data/Finsupp/Basic): `Finsupp.optionElim'` migrated-from-branch t-data awaiting review
25724 bryangingechen chore: disable scheduled runs of stale issues workflow CI awaiting review
25812 vlad902 feat(data): List.Chain' helper lemmas t-data awaiting review
26130 kmill feat: make `reassoc_of%` be able to defer `Category` instance t-meta awaiting review
26240 grunweg perf(CommandLinterLinter): use Substring more t-linter RFC awaiting review
26371 Timeroot feat(NumberTheory): Niven's theorem t-number-theory awaiting review
27021 grunweg feat: custom elaborators for differential geometry t-differential-geometry t-meta awaiting review
27225 eric-wieser refactor(Tactic/Lift): deprecate the third with argument t-meta awaiting-author awaiting author
25760 robin-carlier feat(CategoryTheory/Bicategory): (2,1)-categories and `Pith` t-category-theory awaiting review
27843 JovanGerb chore(Algebra/Order/Sub/Defs): `@[gcongr low]` for `tsub_le_tsub` t-data failing CI
26914 quangvdao feat(Data/PFunctor/Univariate): more definitions for univariate `PFunctor` t-data awaiting review
25042 alreadydone feat(Topology): restriction/extension of Trivialization and composition with Homeomorph t-topology awaiting review
26061 kckennylau feat(AlgebraicGeometry): define Projective Space t-algebraic-geometry awaiting review
26299 adomani perf: the `commandStart` linter only acts on modified files t-linter awaiting review
26478 JovanGerb chore(LibraryRewrite): replace `rw??` with `rw?` t-meta awaiting review
26484 peabrainiac feat(Geometry/Diffeology): basics of diffeological spaces t-differential-geometry awaiting review
26510 alreadydone feat(Matroid): exchange lemmas involving closure t-data t-combinatorics awaiting review
26912 pechersky chore(Algebra/Ring/Subring): simp tag `Subring.smul_def` maintainer-merge t-algebra awaiting review
27703 vihdzp feat: `le_of_forall_ne` t-order easy awaiting-author awaiting author
27915 xroblot chore: example of the error `uncaught exception: dependency loop found involving Mathlib!` failing CI
27076 Komyyy refactor: don't require `DecidablePred` to state `PrimrecPred` maintainer-merge t-computability awaiting review
27868 grunweg linter indentation playground t-linter WIP labelled WIP
27306 xyzw12345 feat: `lie_ring` tactic and `LieReduce` command t-meta failing CI
26992 Paul-Lez feat(Analysis/ODE/Gronwall): add a few consequences of Grönwall's inequality t-analysis WIP labelled WIP
26956 mariainesdff feat(RingTheory/DividedPowers/Basic): add divided power structure on pZp t-ring-theory awaiting review
27252 Parcly-Taxel feat: sharp bounds for `‖exp (I * x) - 1‖` when `x` is real carleson t-analysis awaiting-author awaiting author
26347 mans0954 feature(Data/Finset/RangeDistance): abs_sub_lt_of_mem_finset_range t-data awaiting review
26341 mans0954 feat(LinearAlgebra/QuadraticForm/Basis): Free Tensor product of Quadratic Maps large-import t-algebra WIP labelled WIP
26340 mans0954 feat(Algebra/Module/NestAlgebra): Nest algebras t-algebra failing CI
25992 Multramate feat(RingTheory/Ideal/Span): add pair lemmas t-ring-theory awaiting-author awaiting author
27933 grunweg chore(OrdNode): format code example in code blocks t-data awaiting review
27926 euprunin chore(Geometry/RingedSpace): remove one porting note and one `erw` t-algebraic-geometry awaiting review
24719 madvorak feat(LinearAlgebra/Matrix/NonsingularInverse): inverting `Matrix` inverts its `LinearEquiv` t-algebra awaiting-author awaiting author
26158 upobir feat(NumberTheory/Divisors): add int divisors t-number-theory awaiting-author awaiting author
27120 YaelDillies feat: the category of commutative bialgebras toric t-algebra awaiting review
27307 xyzw12345 feat(RingTheory/GradedAlgebra): homogeneous relation t-ring-theory failing CI
27944 grunweg feat: lint module names with a period t-linter awaiting review
27245 rirarika MvPolynomial.Irreducible new-contributor t-algebra awaiting review
19668 YaelDillies refactor: define `≤`/`<` on `WithBot`/`WithTop` by induction t-order awaiting review
27918 kim-em wip: refactor WithBot/WithTop as structures failing CI
22231 pechersky feat(Algebra/Valued): `AdicExpansion` initial defns t-algebra t-topology awaiting review
26154 ADedecker refactor: add refactored APIs for algebraic filter bases t-topology awaiting review
26301 Ivan-Sergeyev feat(LinearAlgebra/Matrix/Determinant/TotallyUnimodular): new-contributor t-algebra awaiting review
27108 pechersky chore(RingTheory/AdicValuation): golf using WithZero.log t-algebra t-number-theory awaiting review
27182 eric-wieser feat: add bundled versions of `Equiv.cast` t-algebra awaiting review
27482 alreadydone chore(RingTheory/SimpleModule): golf and generalize lifting_property t-algebra awaiting review
26885 pechersky feat(Topology/ValuativeRel): ValuativeTopology 𝒪[K] t-algebra t-topology t-number-theory awaiting review
26483 metakunt feat (RingTheory/RootsOfUnity/PrimitiveRoots) : Add equiv_primitiveRoots_of_coprimePow t-ring-theory new-contributor awaiting-author awaiting author
26386 jjdishere feat(RingTheory/Perfection): lemmas for `frobeniusEquiv.symm` t-ring-theory failing CI
26368 Whysoserioushah feat(RingTheory/TwoSidedIdeal/SpanAsSum): span of set as finsum t-ring-theory awaiting-author awaiting author
26277 AntoineChambert-Loir feat(RingTheory/Congruence/Hom): prove basic isomorphisms theorems for ring congruences t-ring-theory awaiting review
26387 jjdishere feat(RingTheory/WittVector): the Teichmuller series t-ring-theory awaiting-author failing CI
26054 FMLJohn feat(RingTheory/GradedAlgebra/Homogeneous/Subsemiring): homogeneous subsemirings of a graded semiring t-ring-theory awaiting review
25927 jjdishere feat(RingTheory/AdicCompletion): more APIs for IsAdicComplete t-ring-theory awaiting-author awaiting author
25905 mans0954 feat(RingTheory/Polynomial/SmallDegreeVieta): polynomial versions of results in Algebra.QuadraticDiscriminant t-ring-theory awaiting review
25616 erdOne feat(RingTheory/Invariant): residue field extension is finite t-ring-theory awaiting-author awaiting author
24730 YaelDillies feat(RingTheory): group-like elements t-ring-theory toric awaiting review
22322 mariainesdff feat(RingTheory/DividedPowers/RatAlgebra): add definitions t-ring-theory awaiting review
22151 alreadydone feat(RingTheory): a semiprimary ring is Noetherian/Artinian iff its Jacobson radical is fg t-ring-theory awaiting review
14733 jjaassoonn feat(RingTheory/Flat/CategoryTheory): a module is flat iff tensoring preserves finite limits t-ring-theory awaiting-author awaiting author
14727 jjaassoonn feat(RingTheory/Flat/CategoryTheory): a flat module has vanishing higher Tor groups t-ring-theory awaiting-author awaiting author
27309 kckennylau feat(CategoryTheory): a presheaf on `CostructuredArrow F d` can be extended to a presheaf on `C` t-category-theory WIP labelled WIP
27976 smmercuri feat: `ramificationIdx` for `NumberField.InfinitePlace` t-number-theory WIP labelled WIP
26644 kckennylau feat(SetTheory/ZFC): Define the language of sets and state the ZFC axioms t-set-theory awaiting review
26078 kckennylau feat(AlgebraicGeometry): add x, y, px, py for points on elliptic curves t-algebraic-geometry awaiting review
25778 thefundamentaltheor3m feat: Monotonicity of `setIntegral` for nonnegative functions new-contributor t-measure-probability awaiting-author awaiting author
27417 PierreQuinton feat: add `SigmaCompleteLattice` t-order awaiting-author awaiting author
27292 gasparattila feat: asymptotic cone of a set maintainer-merge new-contributor t-analysis awaiting review
27995 kckennylau feat(RingTheory/Valuation): alternate constructors for Valuation ⚠️ awaiting review
27990 kckennylau feat(Counterexamples): a nontrivial valuation with discrete topology ⚠️ awaiting review
27392 Paul-Lez feat(Tactic/SimpUtils): add simproc finding commands t-meta awaiting review
22043 YaelDillies chore: shortcut instance for `Neg ℤˣ` file-removed t-algebra awaiting review
25814 vlad902 feat(SimpleGraph): Weaker condition for paths in acyclic graphs t-combinatorics awaiting review
26190 tb65536 feat(FieldTheory/Galois/IsGaloisGroup): Subgroups of a Galois group are Galois groups t-algebra awaiting review
26580 vasnesterov feat(Tactic/Order): translate linear orders to `Int` large-import t-meta awaiting review
26670 yu-yama feat(GroupExtension/Abelian): define `conjClassesEquivH1` t-algebra awaiting review
26766 MichaelStollBayreuth feat(Topology/MetricSpace/Bounded): add some results t-topology awaiting review
27527 peabrainiac feat(Topology): some `IsOpenMap` lemmas t-topology awaiting review
27602 mitchell-horner feat(Combinatorics/SimpleGraph): define `completeBipartiteSubgraph` t-combinatorics failing CI
26679 robin-carlier feat(CategoryTheory/Limits/Shapes/Pullback/Categorical): 2-functoriality of `CatCommSqOver` t-category-theory awaiting review
28025 kim-em feat: grind annotations in Logic/Equiv/Defs t-logic awaiting review
28032 grunweg feat: support Partial{Homeomorph,Equiv} in differential geometry elaborators t-differential-geometry failing CI
27107 AntoineChambert-Loir feat(GroupTheory/GroupAction/SubMulAction/Combination) : combinations and group actions t-group-theory failing CI
23669 erdOne feat(FieldTheory): abelian extensions t-algebra delegated delegated
27872 JovanGerb chore(gcongr): clean up imports large-import delegated failing CI
25788 Parcly-Taxel feat: number of edges in the Turán graph large-import t-combinatorics awaiting review
26225 Raph-DG feat(AlgebraicGeometry): Add some minimal API for orders on schemes t-algebraic-geometry awaiting review
26770 Jun2M feat(Combinatorics/Graph) : subgraph relations and operations on `Graph` t-combinatorics awaiting review
26798 robin-carlier feat(CategoryTheory/Monoidal/DayConvolution): `LawfulDayConvolutionMonoidalCategoryStruct` t-category-theory awaiting review
27635 Ruben-VandeVelde chore: deprecate SubsemiringClass.coe_pow awaiting review
27658 euprunin chore(Geometry/RingedSpace): remove use of `erw` in `app_inv_app'` t-algebraic-geometry awaiting review
27284 FernandoChu Chore(CategoryTheory/MorphismProperty/MonoFactorization): Factor out mono factorizations new-contributor t-category-theory awaiting-author awaiting author
28074 grunweg Isbilinearmap WIP labelled WIP
27018 Komyyy feat: Finite product of Alexandrov-discrete spaces is Alexandrov-discrete t-topology delegated delegated
27229 WilliamCoram feat(GroupTheory/DoubleCoset): multiple lemmas t-group-theory new-contributor awaiting review
27991 sinianluoye feat (Rat): add Rat.den_eq_of_add_den_eq_one and its dependent lemmas t-data new-contributor awaiting review
25969 101damnations feat(RepresentationTheory/Homological/GroupHomology/Functoriality): the degree 1 part of the corestriction-coinflation exact sequence t-algebra awaiting review
27437 kckennylau feat(RingTheory/Valuation): some lemmas about comparing with 1 and 0 and with each other t-ring-theory WIP labelled WIP
23940 YaelDillies feat: polytopes toric t-analysis awaiting review
26765 KiringYJ feat(MeasureTheory/PiSystem): add π-λ theorem and SetLike instance new-contributor t-measure-probability awaiting review
27118 Timeroot feat(Matrix/Charpoly/Eigs): Roots of Matrix.charpoly are the eigenvalues. large-import t-algebra awaiting review
27400 dleijnse feat: define geometrically reduced algebras new-contributor t-algebra awaiting review
27639 staroperator feat(Algebra/Order/Sub): `Sub` instance for linearly canonically ordered monoid t-algebra awaiting review
26777 YaelDillies chore(Data/Set/Image): move `BooleanAlgebra` material to `Order` large-import t-data WIP labelled WIP
27534 PierreQuinton feat: a typeclass for `sSup`/`sInf` to be lawful t-order awaiting review
28070 grunweg style: improve indentation of multi-linear enumerations in doc-strings failing CI
28111 euprunin chore: remove tactic `simp_lex` and use `simp` instead t-data awaiting review
26881 emo916math feat(Analysis/Calculus/Deriv/Star) A formula for `deriv (conj ∘ f ∘ conj)` new-contributor t-analysis awaiting-author awaiting author
27498 Komyyy feat: Group isomorphisms between (`Equiv.Perm`|`alternatingGroup`)s t-algebra awaiting review
28075 tristan-f-r chore(Finsupp/Indicator): make non-classical t-data easy awaiting-author awaiting author
23238 YaelDillies feat: extended floor and ceil t-algebra awaiting review
24095 lecopivo feat: `fun_prop` for Is(Bounded)LinearMap + notation `fun x ↦L[R] f x` large-import t-algebra awaiting review
25779 robin-carlier feat(CategoryTheory/Bicategory/NaturalTransformations): strong and lax natural transformations of lax functors t-category-theory awaiting review
26899 robin-carlier feat(CategoryTheory/Functor/KanExtension): transitivity of left Kan extensions t-category-theory awaiting review
27468 IvanRenison feat(Combinatorics/SimpleGraph): add theorem `SimpleGraph.Connected.diff_dist_adj` t-combinatorics awaiting review
27664 pechersky feat(Topology,Analysis): discrete topology metric space and normed groups t-topology awaiting review
25770 Parcly-Taxel chore: fix more induction/recursor branch names tech debt awaiting review
28140 YaelDillies feat: a `PointedCone`-valued version of `Submodule.span` t-convex-geometry toric awaiting review
26667 mariainesdff feat(FieldTheory/SplittingField/IsSplittingField): add IsScalarTower.splits, IsScalarTower.isAlgebraic t-algebra awaiting-author awaiting author
27265 pechersky feat(Topology/Valued): discrete topology on a valued field when trivial valuation t-topology awaiting review
27882 euprunin chore: golf using `grind [Nat.cast_*]` awaiting review
23758 erdOne feat(Topology/Algebra): linearly topologized iff non-archimedean large-import t-algebra t-topology awaiting-author awaiting author
28115 bwangpj feat(AlgebraicGeometry/EllipticCurve): reduction of elliptic curves new-contributor t-algebraic-geometry awaiting review
28164 bryangingechen fix(Cache): add put* commands to leanTarArgs easy awaiting review
27567 themathqueen feat(LinearAlgebra/TensorProduct/Tower): add `lid` and `assoc` tensor lemmas t-algebra easy awaiting review
28195 gasparattila feat: separating a convex compact set and its neighborhood with a polytope new-contributor t-analysis awaiting review
25774 Parcly-Taxel chore: deprime `induction` in `AlgebraicTopology/CategoryTheory` tech debt awaiting review
27455 pechersky chore(NumberTheory/Padics/Hensel): rephrase using `aeval` tech debt t-algebra t-number-theory awaiting review
28215 5hv5hvnk Draft PR, for Strong and Weak connectivity for Digraphs new-contributor t-combinatorics failing CI
28119 JasperMS feat(Data/Set/Pairwise): prove pairwise results for Chains, move `Set.pairwise_iUnion₂` carleson t-data new-contributor awaiting review
27712 kim-em chore: remove old irrelevant attributes in Logic/Basic t-logic awaiting review
26901 5hv5hvnk feat: a simproc version of `compute_degree` new-contributor awaiting-CI t-meta awaiting-author does not pass CI
27850 fyqing feat: 0-dimensional manifolds are discrete and countable new-contributor t-differential-geometry awaiting-author awaiting author
26981 JovanGerb chore: golf using `grw` large-import awaiting review
28077 ShreckYe feat(Data/Finset/Card): add some more Pigeonhole Principle theorems `exists_ne_map_eq_of_card_image_lt` and `not_injOn_of_card_image_lt` t-data new-contributor awaiting review
28045 ShreckYe feat(Data/Finset/Image): add `subset_univ_image_iff` t-data new-contributor awaiting review
27444 grunweg feat: generalise more lemmas to enorms carleson WIP ⚠️ labelled WIP
26351 RemyDegenne feat: covering and packing numbers of sets in a metric space t-topology awaiting-author awaiting author
27090 TerenceGitH feat(Archive): Kuratowski's closure-complement theorem (incl. sharpness) new-contributor t-topology awaiting-author awaiting author
28139 YaelDillies refactor: make the cone explicit in `ConvexCone.toPointedCone` t-convex-geometry toric maintainer-merge awaiting review
28266 euprunin chore(RingTheory): golf entire `single_one_eq_pow` using `simp` t-ring-theory awaiting-author awaiting review
27896 JovanGerb style: prefer `some`/`none` over `.some`/`.none` awaiting review
28260 euprunin chore(Analysis/Fourier): golf entire `fourier_zero` and `fourier_zero'` using `simp` t-analysis delegated delegated
27708 vihdzp feat: unions and intersections of ordinals are ordinals t-set-theory awaiting-author awaiting author
24850 pechersky feat(Topology/UniformSpace/Ultra): uniform spaces induced by pseudometrics are ultra if system is ultra t-topology awaiting review
26089 WilliamCoram feat: restricted power series form a ring new-contributor t-algebra t-number-theory awaiting review
26547 robin-carlier feat(CategoryTheory/Limits/Shapes/Pullback/Categorical/CatCospanTransform): more lemmas about isomorphisms of `CatCospanTransform` t-category-theory awaiting review
26968 vihdzp feat(Order/Concept): sets in a concept are codisjoint t-order awaiting review
27000 gasparattila feat(Analysis/Normed/Group/Quotient): isometric versions of isomorphisms large-import new-contributor t-analysis awaiting review
27049 BoltonBailey doc(Analysis/BoxIntegral/Partition/Filter): field docstrings t-analysis documentation awaiting review
27441 judithludwig feat(RingTheory/Polynomial/Quotient): Lemma on PIDs t-ring-theory awaiting review
27815 BGuillemet feat(CategoryTheory/Limits/Shapes/Products): add limMapPi and sigmaMapColim new-contributor t-category-theory awaiting review
27226 xcloudyunx feat(Combinatorics/SimpleGraph): Add Subgraph.inclusion_edge_apply_coe and inclusion_edgeSet_apply_coe new-contributor t-combinatorics awaiting-author awaiting author
19860 YaelDillies refactor: review the `simps` projections of `OneHom`, `MulHom`, `MonoidHom` t-algebra WIP labelled WIP
26110 YaelDillies feat: sharp monoids toric t-algebra awaiting review
24373 YaelDillies refactor: golf `modularCharacter` t-measure-probability awaiting-CI does not pass CI
28226 ShreckYe feat(Data/Finset): `Multiset.eq_of_le_of_card_eq` and `Finset.eq_of_subet_of_card_eq` t-data new-contributor easy awaiting review
26282 AntoineChambert-Loir feat: a theorem of Jordan on primitive subgroups of the permutation group t-group-theory large-import awaiting review
28241 alreadydone chore(Data): `SetLike Finset` t-data awaiting review
27059 Komyyy feat: Linear upper or lower sets topologies are completely normal t-topology awaiting review
25480 ocfnash feat: define a concrete model of the `𝔤₂` root system large-import t-algebra WIP labelled WIP
28242 robin-carlier feat(CategoryTheory/Bicategory): EqToHom for bicategories t-category-theory awaiting review
27261 Sebi-Kumar feat(Topology): add definition for subpaths new-contributor t-topology failing CI
27634 agjftucker fix(Analysis/Calculus/Implicit): consistently rename {`map`, `fun`, `function`} to `fun` t-analysis awaiting review
26192 kckennylau feat(LinearAlgebra): symmetric tensor power t-algebra awaiting review
27339 pechersky chore(RingTheory/Laurent): use WithZero.exp to golf statements and proofs about valuation on K((X)) tech debt t-algebra t-number-theory awaiting review
25804 erdOne feat: `∑ z ∈ L, ‖z - x‖⁻ʳ` converges for lattices `L` t-analysis awaiting review
27308 xyzw12345 feat(LinearAlgebra/SymmetricAlgebra): IsSymmetricAlgebra t-algebra awaiting review
22300 chrisflav feat(RingTheory/GoingDown): lift `LTSeries` of primes t-ring-theory awaiting review
24533 robertmaxton42 feat (ULift): conjugation by ULift.up/down, misc cast/heq lemmas t-data awaiting review
24829 urkud fix(Topology/Homotopy): fix name&args order of `comp` t-topology awaiting review
26357 javra feat(CategoryTheory): linear categories as `ModuleCat R`-enriched categories large-import t-category-theory awaiting review
27073 pechersky feat(Archive/Examples/Local): files showcasing properties of local fields t-number-theory awaiting review
27166 joelriou feat(AlgebraicTopology): the functor `II : SimplexCategory ⥤ SimplexCategoryᵒᵖ` by Gabriel and Zisman t-algebraic-topology awaiting review
27638 plp127 feat: subsingleton `ℕ` and `ℤ` modules t-algebra awaiting review
27659 euprunin chore(Geometry/RingedSpace): remove use of `erw` in `vPullbackConeIsLimit` t-algebraic-geometry awaiting review
28321 kim-em chore: make OmegaCompletePartialOrder a mixin awaiting review
28292 bwangpj feat(Geometry/Manifold/ContMDiff): add product lemmas for `ContMDiff` new-contributor ⚠️ awaiting review
27552 Equilibris refactor: make universe levels visible in typevec t-data new-contributor easy awaiting review
26339 mans0954 feat(Analysis/Normed/Module/WeakDual): Banach Dieudonné Lemma large-import t-analysis WIP labelled WIP
28150 Equilibris chore: clean up proofs typevec proofs t-data new-contributor awaiting review
22925 ggranberry feat(Mathlib/PlaceHolder/ToeplitzHausdorff): Toeplitz-Hausdorff will-close-soon new-contributor t-analysis awaiting-author WIP help-wanted looking for help
27180 ADedecker feat: quotient of a monoid with zero by a multiplicative congruence t-algebra delegated delegated
28185 Sebi-Kumar feat(Topology/Path): add theorem about casting with rfl new-contributor t-topology easy awaiting review
28325 pechersky feat(WithZeroTopology): `locallyCompactSpace_iff_locallyFiniteOrder_units` large-import t-order t-topology awaiting review
28350 themathqueen feat(Topology/Algebra/Module/LinearMap): `range (f.smulRight x) = span {x}` t-algebra t-topology awaiting review
26159 upobir feat(Algebra/QuadraticDiscriminant): Adding inequalities on quadratic from inequalities on discriminant t-algebra awaiting-author awaiting author
28337 joelriou feat(AlgebraicTopology): nondegenerate simplices in the nerve of a partially ordered type t-algebraic-topology awaiting review
28182 themathqueen feat(Data/Matrix/Basis): `center (Matrix n n α) = scalar n '' center α` t-data awaiting review
26035 fbarroero feat(Analysis/Polynomial/MahlerMeasure): the Mahler measure of a complex polynomial t-analysis awaiting review
27934 JasperMS feat(Order): no basic lemmas and some SuccOrder `biUnion` lemmas carleson new-contributor t-order awaiting review
25292 YaelDillies feat: the `ConvexCone` generated by a set t-convex-geometry toric awaiting review
21031 YaelDillies chore: get rid of generic hom coercions WIP labelled WIP
27390 alreadydone feat(FieldTheory/Galois): normal basis theorem t-algebra awaiting review
27842 alreadydone chore(MonoidLocalization): get rid of Submonoid.LocalizationWithZeroMap t-algebra awaiting review
25680 kim-em chore: remove some `Nat` shortcut instances failing CI
23360 kim-em chore: review of `erw` in `Algebra/Homology/DerivedCategory` t-algebra awaiting-author awaiting author
24184 YaelDillies feat: `[G : H]` notation for the index of `H : Subgroup G` t-algebra RFC awaiting review
25736 robin-carlier feat(AlgebraicTopology/SimplexCategory/GeneratorsRelations/NormalForms): Normal forms for `P_σ`s t-algebraic-topology large-import awaiting review
25947 qawbecrdtey feat(Data/Nat/Factors): added lemmas including `primeFactorsList_length_ne_zero` t-data awaiting review
26332 Timeroot feat(ModelTheory/Definability): TermDefinable functions large-import t-logic awaiting review
27754 Parcly-Taxel feat: `finCycle` as iterated `finRotate` t-logic awaiting review
27790 pechersky feat(Topology): `IsDenseInducing.isUniformInducing_extend` t-topology awaiting review
28374 euprunin chore(Analysis/CStarAlgebra/Module): golf entire `map_top_submodule` t-analysis awaiting review
28371 euprunin chore(Analysis/SpecialFunctions/Pow): golf entire `tendsto_rpow_atBot_of_base_gt_one` t-analysis awaiting review
28379 euprunin chore(Analysis/NormedSpace/OperatorNorm): golf entire `opNorm_subsingleton` t-analysis awaiting review
28381 euprunin chore(Analysis/Asymptotics): golf `isLittleO_pow_sub_pow_sub` t-analysis awaiting review
28384 euprunin chore(Algebra/Order/Ring): golf entire `cast_natAbs` t-algebra awaiting review
28385 euprunin chore(Algebra/BigOperators/Finsupp): golf entire `Finsupp.sum_sum_index` t-algebra awaiting review
28378 euprunin chore(Algebra): golf entire `eq_lift_comp_mkRingHom` and `eq_liftAlgHom_comp_mkAlgHom` t-algebra awaiting review
28376 euprunin chore(Analysis/Calculus/Deriv): golf entire `differentiableAt_comp_const_add` t-analysis awaiting review
28373 euprunin chore(AlgebraicGeometry/Morphisms): golf entire `isOpenImmersion_iff_stalk` t-algebraic-geometry awaiting review
28398 euprunin chore(Data/TypeVec): deprecate `subtypeVal_diagSub` (duplicate) t-data awaiting review
28000 daefigueroa feat(Dynamics/Flow): define semiconjugacy, factor and orbit new-contributor t-dynamics awaiting-author awaiting author
28399 Ruben-VandeVelde feat: ring-theoretic fractions in Rat t-ring-theory ??? missing CI information
26448 YaelDillies refactor: simplify `(f₁ ⊗ₘ f₂) ≫ (g₁ ⊗ₘ g₂)` to `(f₁ ≫ g₁) ⊗ₘ (f₂ ≫ g₂)` toric t-category-theory awaiting review
26988 YaelDillies feat(Rel): more API t-data awaiting review
28220 kim-em chore: cleanup three #adaptation_notes maintainer-merge awaiting review
27288 themathqueen chore(LinearAlgebra/TensorProduct/Basic): semi-linearize `map` and `lift` t-algebra awaiting review
28178 joelriou feat(CategoryTheory): locally presentable and accessible categories t-category-theory awaiting review
28356 JovanGerb chore(Data/Rat/Cast/CharZero): rename `Rat.cast_mk` to `Rat.cast_divInt` t-data awaiting review
28390 euprunin chore(Analysis/LocallyConvex): golf entire `polar_weak_closed` t-analysis awaiting review
28377 euprunin chore(Algebra/ContinuedFractions/Computation): golf `get?_of_eq_some_of_get?_intFractPair_stream_fr_ne_zero` t-algebra awaiting review
28057 plp127 feat(SuccOrder): simp lemma to refold `Order.succ` and `Order.pred` t-order awaiting review
27875 grunweg style(AkraBazzi): use more standard indentation t-computability awaiting review
28404 joelriou feat(AlgebraicTopology): the covariant involution of SimplexCategory t-algebraic-topology awaiting review
24015 alreadydone feat(RingTheory): lemmas on finiteness of `LinearMap` and `Module.End` t-ring-theory awaiting review
28375 euprunin chore(Analysis/SpecialFunctions/Pow): golf entire `rpow_lt_rpow_of_exponent_neg`, `rpow_le_rpow_of_exponent_nonpos`, `rpow_le_of_le_log` and `rpow_lt_of_lt_log` t-analysis awaiting review
28389 euprunin chore(Algebra/Group/Subgroup): golf entire `subgroupOf_sup` t-algebra awaiting review
27672 b-reinke feat(GroupTheory/FreeGroup): add definition of cyclically reduced words t-group-theory awaiting review
27305 eric-wieser feat: instances for `ZeroHom` and `OneHom` t-algebra delegated failing CI
28312 LLaurance feat(Combinatorics/SimpleGraph): minimum degree of nontrivial tree is one large-import new-contributor t-combinatorics awaiting review
23986 ShouxinZhang feat(FieldTheory/RatFunc): add RatFunc.toFractionRingAlgEquiv new-contributor t-algebra awaiting review
27024 grunweg feat: Gram-Schmidt orthonormalisation for sections of a vector bundle t-differential-geometry awaiting-author awaiting author
28416 Timeroot feat(Topology/Order): Add OrderIso.instContinuousMapClass t-topology awaiting review
24917 adomani feat: deprecated module automation t-meta awaiting-author awaiting author
28419 euprunin chore(Data/Matroid/Rank): deprecate `Indep.exists_insert_of_encard_lt` (duplicate) t-data awaiting review
26403 riccardobrasca feat: add `isPrincipalIdealRing_of_isPrincipal_of_lt_or_isPrincipal_of_mem_primesOver_of_mem_Icc` maintainer-merge t-number-theory awaiting review
28420 euprunin chore(Data/Nat/Digits): deprecate `coe_int_ofDigits` (duplicate) t-data awaiting review
28421 euprunin chore(Probability/Kernel): golf entire `measurable_condExpKernel` t-measure-probability awaiting review
28422 euprunin chore(Data/Fin): deprecate `Fin.mul_one'` (duplicate) t-data awaiting review
28426 euprunin chore(NumberTheory/NumberField/CanonicalEmbedding): golf entire `measurableSet_interior_paramSet` t-number-theory awaiting review
28427 euprunin chore(LinearAlgebra/Matrix/Charpoly): deprecate `det_of_card_zero` (duplicate) t-algebra awaiting review
28428 euprunin chore(Topology): deprecate `mem_iff_one_sub_mem` (duplicate) awaiting review
28429 euprunin chore(GroupTheory/Perm/Cycle): golf entire `Disjoint.cycleType_mul` t-group-theory awaiting review
28393 tristan-f-r chore(WithZero): clean t-data easy awaiting review
26534 winstonyin feat: IsIntegralCurve for solutions to ODEs t-dynamics t-analysis t-differential-geometry awaiting review
28430 euprunin chore(RingTheory/UniqueFactorizationDomain): deprecate `dvd_of_mem_normalizedFactors` (duplicate) awaiting review
28432 euprunin chore(CategoryTheory/Monoidal): golf entire `counitInv_app_comp_functor_map_η_inverse` t-category-theory awaiting review
28433 euprunin chore(Probability/Kernel): golf entire `snd_compProd_prodMkLeft` t-measure-probability awaiting review
28434 euprunin chore(FieldTheory/IntermediateField/Adjoin): golf entire `adjoin.range_algebraMap_subset` t-algebra awaiting review
28435 euprunin chore(RingTheory/Valuation): golf entire `algebraMap_injective` t-ring-theory awaiting review
28411 zcyemi feat(LinearAlgebra/AffineSpace/Simplex/Centroid): define centroid and medians large-import ⚠️ failing CI
28437 euprunin chore(Data/Finset): deprecate `exists_ne_of_one_lt_card` (duplicate) awaiting review
28439 euprunin chore(LinearAlgebra/Matrix/Determinant): golf entire `det_eq_zero_of_not_linearIndependent_rows` t-algebra awaiting review
28445 mitchell-horner feat: `one_sub_one_div_cast_*` theorems t-data awaiting review
25831 ScottCarnahan feat (RingTheory/HahnSeries): Powers of a binomial t-ring-theory awaiting review
28386 euprunin chore(Analysis/InnerProductSpace/Projection): golf entire `orthogonalProjection_mem_subspace_orthogonalComplement_eq_zero` t-analysis awaiting review
28441 euprunin chore(GroupTheory/Perm): golf entire `mem_of_formPerm_ne_self` t-group-theory awaiting review
25491 tannerduve feat(Control/Monad/Free): define free monad, prove it lawful, and implement standard effects t-data maintainer-merge awaiting review
27516 gaetanserre feat: add rational approximation lemma for suprema in `unitInterval` t-topology awaiting review
27817 zhuyizheng feat: add IMO2025P1 IMO new-contributor awaiting review
27849 robin-carlier feat(CategoryTheory/Bicategory/Functor): strictly unitary lax/pseudo functors t-category-theory awaiting review
27946 plp127 refactor: have `MetrizableSpace` not depend on `MetricSpace` t-topology awaiting review
28452 plp127 feat: Define `ZMod.fintype` without cases t-data awaiting review
27163 pechersky feat(Topology/ValuativeRel): of and to basis of compatible valuations t-algebra t-topology t-number-theory awaiting review
28458 pechersky feat(RingTheory/RootsOfUnity): trivial root of unity: `HasEnoughRootsOfUnity M 1` t-ring-theory t-algebra easy awaiting review
27283 Louddy feat(SkewMonoidAlgebra): maps on/to SkewMonoidAlgebra large-import t-algebra awaiting review
28457 euprunin chore(LinearAlgebra/AffineSpace): deprecate `coe_injective` (duplicate) maintainer-merge t-algebra awaiting review
27464 IvanRenison feat(Combinatorics/SimpleGraph/Paths): add lemma `SimpleGraph.Walk.IsPath.ne_of_mem_support_of_append` t-combinatorics awaiting review
27461 IvanRenison feat(Combinatorics/SimpleGraph/Paths): add lemma `SimpleGraph.Walk.IsPath.mem_support_iff_exists_append` t-combinatorics awaiting review
26125 faenuccio first commit dependency-bump WIP labelled WIP
27253 Louddy feat(SkewMonoidAlgebra): SkewMonoidAlgebra/Support t-algebra awaiting review
28464 robin-carlier chore(CategoryTheory/Bicategory/Basic): extra `hom_inv_id` and `inv_hom_id` lemmas t-category-theory awaiting review
28467 gasparattila chore: make `AffineSubspace.toAddTorsor` and `AffineSubspace.nonempty_map` instances new-contributor awaiting review
28470 EtienneC30 feat: ofLp and toLp are continuously differentiable t-analysis awaiting review
28471 EtienneC30 feat: toLp and ofLp are injective t-analysis awaiting review
28473 EtienneC30 feat: toLp and ofLp are analytic t-analysis awaiting review
28408 Paul-Lez feat(Data/Part): add a few easy lemmas about Part t-data easy failing CI
26075 xroblot feat(NumberField/Units): compute index of unit subgroups using regulators t-number-theory awaiting review
28474 astrainfinita feat: add `ContinuousSMul` instances for `ℚ≥0` bench-after-CI t-algebra t-topology awaiting review
26588 faenuccio feat(Algebra/GroupWithZero/WithZero): add the multiplicative embedding with zero from the range t-order t-algebra awaiting review
28487 euprunin chore(RingTheory): golf entire `smul_eq_zero_of_mem`, `hasEval`, `eq_of_prod_eq_prod` and `isIntegral_of_mem_ringOfIntegers` t-ring-theory awaiting review
28488 euprunin chore(SetTheory): golf entire `cast_succ`, `mk_multiset_of_countable` and `iSup_succ` t-set-theory awaiting review
28489 joelriou feat(CategoryTheory): weaken assumptions for the stability of the left lifting property under transfinite compositions t-category-theory awaiting review
23497 chrisflav chore(RingTheory/AdicCompletion/AsTensorProduct): golf using five lemma for modules t-algebra awaiting review
28490 euprunin chore: golf entire `epi_of_cokernel_π_eq_zero`, `bottom_row_coprime`, `congr_of_eventuallyEq` and `Invertible.congr` awaiting review
28491 euprunin chore(MeasureTheory/Measure): deprecate `injective_diracProba_of_T0` (duplicate) t-measure-probability awaiting review
28484 euprunin chore(Data): golf entire `add_one_le_exp_of_nonneg`, `toReal_eq_toReal`, `count_eq_of_nodup`, `smul_mat_cons` and `coe_inj` t-data awaiting review
28486 euprunin chore(Order): golf entire `map_covBy`, `covBy_of_apply`, `map_wcovBy`, `wcovBy_of_apply`, `ne_bot_of_ne_top'`, `insert_Icc_left_eq_Icc_pred` and `insert_Icc_right_eq_Icc_succ` t-order awaiting review
28492 euprunin chore(Data/Finite): golf entire `card_le_of_injective`, `card_le_of_surjective` and `card_sum` t-data awaiting review
26489 chrisflav refactor(RingTheory/RingHom): factor out proofs for `Algebra.FinitePresentation` t-algebra awaiting review
24794 chrisflav feat(RingTheory/Presentation): core of a presentation t-ring-theory awaiting review
28493 gasparattila feat: topological affine spaces large-import new-contributor ⚠️ awaiting review
28501 dtumad feat(Data/Set): show the `Alternative` instance on `Set` is lawful t-data new-contributor awaiting review
25776 Parcly-Taxel chore: deprime `induction` in `Analysis` tech debt t-analysis awaiting review
26961 mariainesdff feat(RingTheory/PowerSeries/Substitution): add API t-ring-theory awaiting review
27117 pechersky feat(NumberTheory): `IsDiscreteValuationRing (v.adicCompletionIntegers K)` t-algebra t-analysis t-number-theory awaiting review
27453 pechersky feat(Topology/UniformSpace/Ultra): completion is ultra uniformity iff base is t-topology awaiting review
27720 peabrainiac feat(CategoryTheory/Adjunction): lemmas on adjoint quadruples t-category-theory awaiting review
27965 grunweg feat: verify that file names contain no forbidden characters file-removed t-linter maintainer-merge awaiting review
28091 ShreckYe feat(Algebra/Order/Floor): a variant of `Nat.ceil_lt_add_one` with its condition `0 ≤ a` generalized to `-1 < a` new-contributor t-algebra awaiting review
28102 eric-wieser feat: nontriviality of `SeparationQuotient` iff the topology is nontrivial t-topology awaiting review
26358 plp127 feat(Topology): R1 spaces are quasisober t-topology awaiting review
28132 dupuisf feat: preliminary `grind` tags for `IsUnit` t-algebra awaiting review
28507 euprunin chore: remove debug output ("Unpacked in […] ms") from `lake exe cache get` output awaiting review
27974 smmercuri feat: `Field`, `FiniteDimensional` and `Algebra.IsSeparable` instances for `WithAbs` large-import t-analysis awaiting-author awaiting author
28034 joelriou feat(AlgebraicTopology): the type of simplices of a simplicial set t-algebraic-topology awaiting review
28443 mitchell-horner feat: `filter_disjiUnion` t-data awaiting review
27260 JovanGerb feat(Geometry/Euclidean/SignedDist): `signedDist` between two points t-euclidean-geometry awaiting review
26428 Ruben-VandeVelde feat: norm_num support for Int.fract t-data awaiting review
28512 euprunin chore(Data/List): golf entire `getLast_append_of_right_ne_nil` and `finRange_map_getElem` t-data awaiting review
26785 TOMILO87 feat: beta distribution new-contributor t-measure-probability awaiting review
27196 YaelDillies refactor(Polynomial/Bivariate): swap `X` and `Y` for improved notation toric t-algebra WIP labelled WIP
26857 Thmoas-Guan feat(Algebra): define associated graded structure for abelian group t-algebra awaiting-author awaiting author
28520 chrisflav chore(Data): add `Finset.exists_injOn_image_eq_of_surjOn` t-algebra awaiting review
27178 artie2000 feat(Algebra/Order/Ring): make `IsOrderedRing.toStrictOrderedRing` an instance t-ring-theory awaiting-author awaiting author
28126 Sebi-Kumar feat(AlgebraicTopology/FundamentalGroupoid): add alternative to `fromPath` t-algebraic-topology new-contributor failing CI
27094 smorel394 feat(Algebra.Category.FGModuleCat.Colimits): the category of finitely generated modules has finite colimits t-algebra awaiting review
28508 euprunin chore(Algebra/Polynomial): golf entire `homOfEq_heq` awaiting review
28271 euprunin chore(LinearAlgebra/AffineSpace): golf 11 lines from `affineIndependent_iff_indicator_eq_of_affineCombination_eq` using `simp_all` t-algebra awaiting review
27129 javra feat(CategoryTheory/Enriched): the bicategory of `V`-enriched categories infinity-cosmos t-category-theory failing CI
23594 YaelDillies chore: rename `dmaSMul_apply` to `domSMul_apply` t-algebra awaiting review
24804 Moises-Herradon-Cueto feat(CategoryTheory/Limits/Preserves/Shapes): show that if a functor preserves limits, so does `Over.post` toric new-contributor t-category-theory awaiting review
26107 xroblot feat(NumberField/IsCM): first results about the action of `complexConjugation` on units t-number-theory awaiting review
27839 CBirkbeck feat: normalised Eisenstein series t-number-theory awaiting review
28019 euprunin chore: replace `aesop_cat` with `simp` where applicable awaiting review
28122 j-loreaux refactor: change `unitary.map` to take an explicit morphism as an argument, rather than a morphism class t-algebra awaiting review
28131 plp127 feat: forgetful functor from over category preserves connected limits t-category-theory awaiting review
28141 YaelDillies chore: deprecate `BialgHom.coe_toLinearMap` t-ring-theory toric easy awaiting review
28149 Equilibris feat: dcongr_heq new-contributor t-logic awaiting review
28538 euprunin chore(Algebra/ContinuedFractions/Computation): golf entire `coe_of_h_rat_eq` using `simp_all` t-algebra awaiting review
28541 euprunin chore(Analysis/Normed/Group): golf entire `coe_inj` using `grind [DFunLike.coe_fn_eq]` t-analysis awaiting review
23999 YaelDillies feat(MonoidAlgebra): `mapDomain` and `mapRange` as ring homs toric t-algebra awaiting review
27105 xroblot feat(Ring/DedekindDomain): formula for the splitting of prime ideals in an extension large-import t-algebra t-number-theory awaiting review
26101 xroblot feat(NumberField): specialized version of Kummer Dedekind for the splitting of prime numbers t-number-theory awaiting review
26009 linesthatinterlace feat: Add `Vector`/`List.Vector` equivalence migrated-from-branch t-data awaiting review
25735 robin-carlier feat(CategoryTheory/Limits/Sifted): characterization of sifted categories large-import t-category-theory failing CI
28406 YaelDillies chore: rename `Mon_Class` to `MonObj` t-category-theory awaiting review
28286 bwangpj feat(Geometry/Manifold/ContMDiff): basic lemmas for analytic (`C^ω`) functions new-contributor t-differential-geometry awaiting review
28527 grunweg feat: add ContMDiff.congr t-differential-geometry easy failing CI
27433 YaelDillies refactor: make `⇑e⁻¹ = e.symm` simp awaiting review
28354 joelriou feat(AlgebraicTopology/ModelCategory): right homotopies t-algebraic-topology awaiting review
28179 vihdzp feat: `LinearOrderedAddCommGroupWithTop (ArchimedeanClass R)` maintainer-merge t-algebra awaiting review
28555 YaelDillies feat: pullback along an epi preserved under pullbacks is faithful toric large-import t-category-theory awaiting review
28449 wwylele feat(Algebra/Order): ArchimedeanClass ball for module t-algebra awaiting review
28570 euprunin chore(RepresentationTheory/Homological/GroupCohomology): golf entire `cochainsMap_f_1_comp_cochainsIso₁` using `tauto` t-algebra awaiting review
28571 euprunin chore(RingTheory): golf entire `mem_extended_iff`, `coeff_opRingEquiv` and `comp_assoc` using `tauto` t-ring-theory awaiting review
28573 euprunin chore(Tactic): golf entire `eval_cons` and `natPow_zero_natMod_succ_succ` using `tauto` t-meta awaiting review
27357 jcreedcmu feat(Algebra/Module/Submodule): add `submoduleMap` for isometries new-contributor t-algebra awaiting review
28560 euprunin chore(Combinatorics/Quiver): golf entire `lift_spec` using `tauto` t-combinatorics awaiting review
28562 euprunin chore(Geometry/RingedSpace): golf entire `locallyRingedSpace_toLocallyRingedSpace` using `tauto` t-algebraic-geometry awaiting review
28565 euprunin chore(Logic/Equiv): golf entire `trans_symm_eq_symm_trans_symm` using `tauto` t-logic awaiting review
28567 euprunin chore(NumberTheory): golf entire `equivHeightOneSpectrum_symm_apply` and `is_rat` using `tauto` t-number-theory awaiting review
28568 euprunin chore(Order): golf entire `IsBoundedUnder.eventually_le` and `ωSup_zip` using `tauto` t-order awaiting review
28569 euprunin chore(Probability): golf entire `comp_const` and `piFinset_eq_comap_restrict` using `tauto` t-measure-probability awaiting review
28556 euprunin chore(Algebra): golf entire `linearEquivFunOnFintype_lof`, `mem_valueMonoid`, `ofIsColimitCokernelCofork_f` and more using `tauto` t-algebra awaiting review
28558 euprunin chore(Analysis): golf entire `HasGradientAtFilter.hasDerivAtFilter`, `liftIsometry_symm_apply` and `mapL_apply` using `tauto` t-analysis awaiting review
28559 euprunin chore(CategoryTheory): golf entire `preinclusion_map₂`, `mapForget_eq`, `uSwitch_map_uSwitch_map` and more using `tauto` t-category-theory awaiting review
28561 euprunin chore(Data): golf entire `equivFunOnFintype_single`, `predAbove_right_zero`, `snoc_zero` and more using `tauto` t-data awaiting review
28563 euprunin chore(GroupTheory): golf entire `base_smul_def` and `summand_smul_def` using `tauto` t-group-theory awaiting review
28564 euprunin chore(LinearAlgebra): golf entire `congr_symm`, `LinearMap.toMatrix_smulBasis_left`, `LinearMap.toMatrix_smulBasis_right` and more using `tauto` t-algebra awaiting review
28566 euprunin chore(MeasureTheory/Constructions): golf entire `inter_cylinder{,_same}` and `union_cylinder{,_same}` using `tauto` t-measure-probability awaiting review
28574 euprunin chore(Topology/Category): golf entire `finiteCoproduct.ι_desc_apply`, `piIsoPi_hom_apply`, `prodIsoProd_hom_apply` and `pullbackIsoProdSubtype_hom_apply` using `tauto` t-topology awaiting review
26129 LessnessRandomness feat(Geometry/Euclidean/Angle/Unoriented): triangle inequality for angles new-contributor t-euclidean-geometry failing CI
26349 mans0954 feat(Analysis/SpecialFunctions/Trigonometric/Basic): sin and cos of multiples of π / 3 t-analysis help-wanted looking for help
28497 euprunin chore: golf entire `nonneg_iff_isSelfAdjoint_and_spectrumRestricts`, `tail_append_singleton_of_ne_nil` and `isLocalHom_residue` awaiting-author awaiting author
28528 euprunin chore(LinearAlgebra/AffineSpace): golf entire `univ_fin2` using `trivial` t-algebra awaiting review
28522 euprunin chore(Algebra/Ring/Subsemiring): golf entire `coe_pow` using `trivial` t-algebra awaiting review
28557 ShreckYe feat(Data/Nat/Factorization): some results on equality of powers of naturals proved from factorization t-data awaiting review
28539 euprunin chore(Algebra/Order/Interval/Set): golf entire `one_sub_mem` using `simp_all` t-algebra awaiting review
26057 YaelDillies feat: `mon_tauto`, a simp set to prove tautologies about a monoid object toric t-category-theory awaiting review
27363 101damnations feat(RepresentationTheory/Homological): add standard resolution for finite cyclic groups ⚠️ awaiting review
27743 alreadydone feat(NumberTheory): Frobenius number exists, ℕ is Noetherian semiring & Sylver coinage large-import t-algebra t-combinatorics t-number-theory awaiting review
27900 alreadydone feat(Algebra): principal ideal finite product rings t-ring-theory t-algebra awaiting review
28059 hanwenzhu refactor(MeasureTheory/RieszMarkovKakutani): Use PositiveLinearMap new-contributor t-measure-probability awaiting review
28198 Sebi-Kumar feat(Analysis/InnerProductSpace/PiL2): Add instances for EuclideanSpace rank and EuclideanSpace being infinite new-contributor t-analysis awaiting review
28572 euprunin chore(SetTheory): golf entire `congToClass_empty` using `tauto` t-set-theory awaiting review
28580 kmill refactor: simplify implementation of `filter_upwards` t-order t-meta failing CI
27370 euprunin chore(Tactic/CancelDenoms): golf `cancel_factors_eq` t-meta awaiting review
27847 euprunin chore(Algebra): avoid duplicating proofs by reusing existing theorems or lemmas t-algebra awaiting review
27856 euprunin chore(RingTheory/PowerSeries): golf entire `trunc_one` using `grind` maintainer-merge t-algebra awaiting review
27857 euprunin chore(Analysis/SpecialFunctions): golf entire `rpow_eq_top_of_nonneg` using `simp` maintainer-merge t-analysis awaiting review
27302 tristan-f-r feat(Fintype/Quotient): finLiftOn₂ t-data failing CI
28205 euprunin chore(Analysis/Calculus): golf entire `HasLineDerivWithinAt.congr_of_eventuallyEq` t-analysis awaiting review
28506 kim-em chore: clarify internal heartbeat conversion t-meta awaiting review
28204 euprunin chore(Analysis/Calculus): golf entire `HasLineDerivAt.congr_of_eventuallyEq` t-analysis awaiting-author awaiting author
28588 vihdzp feat: supremum of principal ordinals is principal t-set-theory awaiting review
28589 vihdzp feat: more lemmas on characteristic 2 rings t-algebra easy awaiting review
28590 euprunin chore(Data/List): golf entire `idxOf_eq_length_iff` using `grind` t-data awaiting review
28519 euprunin chore(LinearAlgebra/AffineSpace/AffineSubspace): deprecate `mem_mk'_iff_vsub_mem` (duplicate) t-algebra awaiting review
27109 pechersky feat(RingTheory/AdicValuation): valuation_surjective t-ring-theory t-analysis t-number-theory delegated delegated
28544 themathqueen feat(Algebra/Star/Unitary): `unitary * a * star unitary` is self-adjoint iff `a` is t-algebra easy awaiting review
28366 BoltonBailey chore(downstream_dashboard.py): Allow empty workflow list CI delegated delegated
27840 CBirkbeck feat(NumberTheory/ModularForms/EisensteinSeries): define gammaSetN t-number-theory awaiting review
27254 yuanyi-350 2025 imo problem3 IMO failing CI
5897 eric-wieser feat: add a `MonadError` instance for `ContT` t-meta awaiting-author awaiting author
28496 ntapiam feat(Algebra/LieAdmissible/Defs): define Lie-admissible rings/algebras new-contributor t-algebra failing CI
27977 smmercuri feat: predicates for extensions of complex embeddings t-number-theory WIP labelled WIP
25780 emilyriehl the homotopy category functor preserves products t-algebraic-topology infinity-cosmos large-import t-category-theory failing CI
28598 lauramonk feat(Combinatorics/Graph) add definitions of incidenceSet and loopSet new-contributor t-combinatorics easy awaiting review
28582 Thmoas-Guan feat(Data): some lemmas about withBot ENat t-data awaiting review
27958 pechersky feat(NumberTheory/Padics): norm of Int lt one iff p divides t-algebra t-analysis t-number-theory delegated failing CI
28338 themathqueen feat(Analysis/InnerProductSpace/IsPositive): `(adjoint S ∘ S).IsPositive` and `(S ∘ adjoint S).IsPositive` t-analysis easy awaiting review
28587 vihdzp feat: irreducible polynomial has positive degree t-algebra easy awaiting review
23835 chrisflav feat(Topology): cardinality of connected components is bounded by cardinality of fiber t-topology awaiting review
23881 YaelDillies feat: `ℝ≥0`-valued Lᵖ norm t-measure-probability awaiting-author awaiting author
26211 Thmoas-Guan feat(Algebra): vanishing of induced hom between ext large-import t-algebra failing CI
26210 Thmoas-Guan feat(RingTheory): associated primes of localized module t-ring-theory large-import awaiting-author awaiting author
24528 chrisflav feat(AlgebraicGeometry): directed covers t-algebraic-geometry awaiting review
28531 Ruben-VandeVelde chore: remove Cardinal imports from Topology.Algebra.InfiniteSum.Group awaiting review
28175 dsfxcimk add Exterior angle theorem new-contributor t-euclidean-geometry failing CI
28517 Vierkantor chore(*): address some `@[simps]` porting notes tech debt awaiting review
28606 euprunin chore(Data/Set): golf entire `compl_prod_eq_union` using `grind` t-data awaiting review
28602 gmcninch-tufts feat(Algebra/Polynomial/Module): prove equivalence of a certain tensor product with PolynomialModule new-contributor t-algebra awaiting review
26308 LessnessRandomness feat(Analysis.NormedSpace): add normalized vectors new-contributor t-analysis awaiting-author awaiting author
27943 dupuisf feat: `StarOrderedRing` implies `OrderedSMul` large-import t-algebra t-analysis awaiting review
28609 mans0954 feature(Analysis/LocallyConvex/Bounded): Quasi-complete spaces ⚠️ awaiting review
28612 euprunin chore(Data/List): golf entire `idxOf_append_of_mem`, `cons_sublist_cons'`, `length_eraseIdx_add_one`, `length_eraseP_add_one` and `idxOf_append_of_notMem` using `grind` t-data awaiting review
28451 yapudpill feat(RingTheory/Noetherian): add `IsNoetherianRing.of_prime` t-ring-theory new-contributor awaiting review
28477 yapudpill feat(RingTheory): golf `IsPrincipalIdealRing.of_prime` t-ring-theory new-contributor awaiting review
28035 euprunin chore: replace `norm_num` with `simp` where applicable awaiting review
28163 euprunin chore: replace `aesop` with `simp_all` where applicable awaiting review
27460 IvanRenison feat(Combinatorics/SimpleGraph/Walk): add theorems about membership on the support of `Walk.concat` t-combinatorics awaiting-author awaiting author
28339 JovanGerb feat(gcongr): support `@[gcongr]` for `Monotone` and friends ⚠️ awaiting review
28533 kim-em feat(linarith): add `linarith?` mode which suggests a `linarith only` call codex t-meta awaiting review
26259 Raph-DG feat(Topology): Connecting different notions of locally finite t-topology awaiting review
27395 joelriou feat(Algebra/Homology): the canonical t-structure on the derived category t-category-theory awaiting review
27573 jsm28 feat(LinearAlgebra/AffineSpace/Simplex/Basic): membership of interior of a face t-algebra awaiting review
28072 kckennylau feat(RingTheory/Valuation): make tactic rw_val_equiv t-ring-theory awaiting review
28191 kckennylau feat(Logic): tag Injective, Surjective, and Bijective with fun_prop t-meta awaiting review
28626 alreadydone chore(Archive, Counterexamples): replace => by ↦ awaiting review
28628 euprunin chore(Order/BooleanAlgebra): golf entire `diff_insert_of_notMem`, `insert_diff_of_mem`, `insert_diff_of_notMem` and `subset_insert_iff` using `grind` t-order awaiting review
28343 RemyDegenne feat(Probability): Fernique's theorem for distributions that are invariant by rotation t-measure-probability awaiting review
28546 Sfgangloff feat(SymbolicDynamics): basic setup of Zd, full shift, cylinders, pat… new-contributor t-dynamics awaiting review
28511 YaelDillies feat(Finsupp): `congr!`-compatible version of `prod_congr` t-algebra awaiting review
28575 YaelDillies feat: `IsOrderBornology` instances for `ℕ` and `ℤ` large-import ⚠️ awaiting review
28100 themathqueen feat(LinearAlgebra/Matrix): algebra automorphisms on matrices are inner t-algebra awaiting review
25692 Whysoserioushah feat(RingTheory/MatrixAlgebra): add a more general version of `matrixEquivTensor` t-ring-theory awaiting-author awaiting author
25832 xroblot feat(FieldTheory/LinearDisjoint): `trace` (resp. `norm`) and `algebraMap` commutes large-import maintainer-merge t-algebra awaiting review
25858 themathqueen feat(RingTheory/Coalgebra/MulOpposite): coalgebra instance for MulOpposite t-ring-theory maintainer-merge new-contributor awaiting review
28117 RemyDegenne feat(Probability): definitions of risk, Bayesian risk, Bayes risk, minimax risk t-measure-probability awaiting review
28631 faenuccio feat(Data\Nat\ModEq.lean): add grind attribute to ModEq t-data WIP labelled WIP
28526 xroblot feat(DedekindDomain): More instances t-ring-theory awaiting review
28617 kckennylau feat(AlgebraicGeometry): jointly surjective topology maintainer-merge t-algebraic-geometry awaiting review
26329 Timeroot feat: Definition of `Clone` notations and typeclasses t-algebra awaiting-CI awaiting-author does not pass CI
28349 kckennylau feat(Meta): add notation for naming stacked polynomials t-meta awaiting review
27973 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 ⚠️ awaiting review
28581 bennett-chow fix: riemmanian -> riemannian new-contributor t-differential-geometry awaiting-author awaiting author
28148 kckennylau feat(Matrix): Simproc and Rw-proc for Matrix Transpose t-meta awaiting review
28446 mitchell-horner feat(Combinatorics/SimpleGraph): `card_edgeFinset_map` t-combinatorics delegated delegated
26106 mbkybky feat(RingTheory/Regular): flat base change of weakly regular sequence t-ring-theory awaiting-author awaiting author
28615 kckennylau feat(RingTheory): Standard open immersion t-ring-theory maintainer-merge awaiting review
26960 joelriou feat(AlgebraicTopology/ModelCategory): the lemma by K. S. Brown t-algebraic-topology t-category-theory awaiting review
28627 plp127 chore: rename `Set.surjective_onto_image` t-data awaiting review
28319 kim-em chore: scope the IsSimpleOrder -> Fintype instance awaiting review
28614 kckennylau feat(CategoryTheory): The finite pretopology on a category t-category-theory awaiting review
27321 kckennylau feat(CategoryTheory): Colimit can be computed fiberwise t-category-theory awaiting review
28623 gilesgshaw feat(Logic/Basic): minor additions and simplification of proofs new-contributor t-logic failing CI
27963 ShreckYe feat(Algebra/GCDMonoid): add some theorems related to divisibility and `lcm` for both `GCDMonoid` and `Nat` new-contributor t-algebra awaiting review
28641 sun123zxy feat(RingTheory/Nakayama): add a version of Nakayama's lemma (stacks 00DV (8)) t-ring-theory new-contributor awaiting review
26614 Rida-Hamadani feat(SimpleGraph): add more API for `take`/`drop` t-combinatorics awaiting-author awaiting author
27964 smmercuri feat: two inequivalent absolute values have a `< 1` and `> 1` value ⚠️ failing CI
28180 kckennylau chore(Meta): clean up PiFin.mkLiteralQ t-data maintainer-merge t-meta awaiting review
28317 kckennylau feat(Algebra): more lemmas about units in ordered monoid t-algebra awaiting review
28305 euprunin chore(RingTheory/MvPolynomial): golf entire `weightedHomogeneousComponent_of_isWeightedHomogeneous_same` and `weightedHomogeneousComponent_of_isWeightedHomogeneous_ne` t-ring-theory failing CI
28639 ChrisHughes24 feat(Nullstellensatz); Generalize nullstellensatz to use a different field for the polynomial ring ⚠️ awaiting review
28644 kckennylau don't mind me, i just want cache will-close-soon WIP labelled WIP
25070 erdOne feat(EllipticCurve): rational points on singular cuspidal cubics t-algebraic-geometry awaiting-author awaiting author
26310 kckennylau Binary form t-algebra awaiting-author awaiting author
27696 pechersky feat(Padic/WithVal): WithVal v is isomorphic to Q_p as fields and uniform spaces t-algebra t-number-theory delegated delegated
27610 RemyDegenne feat: covariance with respect to a product measure t-measure-probability awaiting-author awaiting author
28655 YaelDillies CI: list the projects I maintain CI awaiting review
28653 strihanje01 feat(Combinatorics/Additive/Convolution): convolution map new-contributor t-combinatorics awaiting review
26640 euprunin chore(Data): golf `Data/` using `grind` t-data awaiting review
28604 alreadydone chore(Algebra/Ring/Defs): add two classes (minimally invasive version) t-algebra WIP labelled WIP
26923 oliver-butterley feat(Dynamics/BirkhoffSum): add the pointwise ergodic theorem (Birkhoff's) new-contributor t-dynamics awaiting review
27972 smmercuri chore: make `Valuation.Completion` a `def` and refactor more of `AdicValuation.lean` t-algebra t-number-theory WIP labelled WIP
25836 jt496 feat(SimpleGraph/FiveWheelLike): add the Andrásfai-Erdős-Sós theorem large-import t-combinatorics awaiting review
27752 plp127 feat(Order): `NoBotOrder α` implies `NoMinOrder α` under `IsDirected α (· ≥ ·)` t-order awaiting-author failing CI
28013 astrainfinita feat: Lindemann-Weierstrass Theorem t-algebra t-analysis WIP labelled WIP
28661 harahu doc(MeasureTheory): Miscellaneous typo fixes t-measure-probability awaiting review
28552 loefflerd feat(Compactification/OnePoint): classify GL2 elements by fixed points large-import t-algebra awaiting review
28553 themathqueen feat(Analysis/InnerProductSpace/Positive): `A.toEuclideanLin.IsPositive` iff `A.PosSemidef` t-analysis awaiting review
28549 themathqueen feat(Analysis/InnerProductSpace/Positive): `LinearIsometryEquiv ∘ T ∘ LinearIsometryEquiv.symm` is positive iff `T` is t-analysis easy awaiting review
28316 eric-wieser feat(Tactic/NormNum): better trace nodes t-meta awaiting review
28125 nonisomorphiclinearmap feat(Combinatorics): basic definition of simplicial complexes new-contributor t-combinatorics awaiting review
28153 kckennylau feat(Simproc): Simproc for explicit diagonal matrices t-meta awaiting review
28186 Sebi-Kumar feat(Topology/Homotopy/Path): Add IsEquiv instance for Path.Homotopic new-contributor t-topology awaiting review
28174 YaelDillies feat: torsion-free modules CFT t-algebra awaiting review
28234 alreadydone chore(AlgebraicTopology): clean up FundamentalGroupoid t-algebraic-topology awaiting review
28284 sgouezel feat: finite product of probability measures t-measure-probability awaiting review
28290 eric-wieser refactor(Tactic/Linarith): switch to using AtomM in natToInt t-meta awaiting review
26219 Thmoas-Guan feat(RingTheory/KrullDimension): Krull Dimension of quotient regular sequence t-ring-theory awaiting review
27039 Scarlett-le feat(Geometry/Euclidean/Sphere/Basic): add theorems for angles subtended by diameters maintainer-merge new-contributor t-euclidean-geometry awaiting-author awaiting author
28401 themathqueen chore(LinearAlgebra/Matrix/HermitianFunctionalCalculus): moving and renaming stuff t-algebra easy awaiting review
28344 themathqueen feat(Analysis/InnerProductSpace/PiL2): `(innerSL _ x).toMatrix` and `(toSpanSingleton _ x).toMatrix` t-analysis awaiting review
27162 themathqueen feat(Analysis/InnerProductSpace/Positive): `U.starProjection ≤ V.starProjection` iff `U ≤ V` t-analysis awaiting review
28630 Antidite feat(Archive/Imo): right isosceles configuration in the complex plane IMO new-contributor awaiting review
27937 madvorak feat(Logic/Basic): `congr_heq₂` t-logic awaiting review
28681 euprunin chore(Data/Finset): golf entire `diag_union_offDiag`, `erase_right_comm`, `univ_filter_mem_range` and `powersetCard_map` using `grind` t-data awaiting review
24514 b-mehta chore(Int/GCD): use fuel in xgcd t-data awaiting-author awaiting author
26645 erdOne feat(RingTheory/PowerSeries): Construction of `Q` such that `P(Q(X)) = X` t-ring-theory awaiting-author awaiting author
26783 matthewjasper feat(RingTheory/Flat): Add theorems relating Submodule.torsion and Module.Flat t-ring-theory FLT new-contributor awaiting-author awaiting author
27157 riccardobrasca feat: add relNorm_algebraMap t-algebra delegated delegated
28650 Vierkantor chore(Analysis): address a lot of porting notes tech debt t-analysis awaiting review
19872 YaelDillies chore(GroupTheory/Index): rename `relindex` to `relIndex` FLT maintainer-merge t-algebra awaiting review
27644 themathqueen chore(LinearAlgebra/Projection): deprecating `subtype ∘ linearProjOfIsCompl` in favor of `IsCompl.projection` t-algebra awaiting review
27825 yonggyuchoimath feat(RingTheory/Ideal/Height): sup of ideal heights equals Krull dimension t-ring-theory new-contributor awaiting review
28669 kckennylau chore: clean up some proofs about locally compact valuation awaiting review
28663 harahu doc(Tactic): hyphenate "right-hand" and "left-hand" where appropriate maintainer-merge t-meta awaiting review
26827 pechersky feat(Analysis/Normed/ValuativeRel): helper instance for NormedField t-algebra t-analysis t-number-theory awaiting review
28176 vihdzp chore: add `simp` attribute to `abs_mul` t-algebra easy awaiting review
27837 CBirkbeck feat(NumberTheory/Divisors): add divisorAntidiagonal equivalence. maintainer-merge t-number-theory failing CI
28691 or4nge19 feat(Probability/Invariance):Reversibility/DetailedBalance new-contributor t-measure-probability 🟤 running CI
28142 YaelDillies refactor: state hypotheses of `BialgHom.ofAlgHom` as equalities of `AlgHom`s t-ring-theory toric maintainer-merge awaiting review
28682 Thmoas-Guan feat(RingTheory): definition of regular local ring t-ring-theory 🟤 running CI
27511 Nebula691 feat(Algebra/QuadraticAlgebra) : Define Quadratic Algebra new-contributor t-algebra awaiting review
28151 iehality feat(Computability): r.e. sets are closed under inter/union/projection/composition t-computability awaiting-author awaiting author
26156 oliver-butterley feat(MeasureTheory.VectorMeasure) : add a definition of total variation for VectorMeasure new-contributor t-measure-probability awaiting-author awaiting author
27596 Paul-Lez feat(Topology/Instances/Matrix/{*}): Add `TopologicalSpace` instance for `SpecialLinearGroup`. file-removed t-algebra easy failing CI
28680 vihdzp feat: set has cardinality one iff singleton t-set-theory easy awaiting-author awaiting author
28642 chrisflav chore(RingTheory/Localization/Algebra): generalize universes and to `CommSemiring` t-ring-theory 🟤 running CI
28165 javra feat(CategoryTheory/Enriched): transport enrichment on enriched ordinary categories infinity-cosmos t-category-theory delegated awaiting review
27785 staroperator chore(Algebra/Group/Submonoid): golf `Nat.addSubmonoidClosure_one` using `simp` large-import t-algebra awaiting review
27936 alreadydone feat(Algebra): additivize Dvd and Prime t-algebra awaiting review
25183 YaelDillies feat: convolution product on linear maps from a coalgebra to an algebra toric t-algebra awaiting review
27282 artie2000 feat(Algebra/Order/Ring): define ring orderings t-ring-theory large-import delegated delegated
26330 Timeroot "Junk value" test file t-data failing CI
27889 astrainfinita chore(RingTheory/(Mv)PowerSeries): use implicit parameters in `monomial`, `coeff`, `map`, `C`, and `constantCoeff` maintainer-merge t-algebra awaiting review
28637 JovanGerb feat(to_additive): `(dont_translate := ...)` option t-meta 🟤 running CI
27443 yuanyi-350 Stacks tags t-algebra WIP 🟤 labelled WIP
28645 YaelDillies chore: rename `mul_le_mul_left`/`mul_le_mul_right` to `mul_le_mul_iff_right₀`/`mul_le_mul_iff_left₀` awaiting-CI 🟤 does not pass CI
28636 YaelDillies feat(Data/Nat): `gcongr` attributes for `sub` lemma t-data awaiting author
28676 sun123zxy feat(NumberTheory/ArithmeticFunction): wrap `Nat.totient` as an `ArithmeticFunction` large-import new-contributor t-number-theory awaiting review
26300 igorkhavkine feat(Analysis/Calculus/FDeriv): continuous differentiability from continuous partial derivatives on an open domain in a product space new-contributor t-analysis awaiting-author WIP failing CI
27715 dupuisf feat(CStarAlgebra): `a => a ^ p` is operator monotone for `p ∈ Icc 0 1` large-import t-analysis awaiting-author awaiting review
27040 Scarlett-le feat(Geometry/Euclidean/Sphere/Power): add power of a point theorems maintainer-merge new-contributor t-euclidean-geometry awaiting-author failing CI
26138 xroblot Development branch (2) large-import WIP labelled WIP
28169 xroblot feat(DedekindDomain): Monoid of ideals is torsion-free t-ring-theory awaiting review
28638 YaelDillies refactor: syntactically generalise the `Nontrivial (Fin n)` instance t-data failing CI
28547 YaelDillies feat: `measurable_from_prod_countable_right` t-measure-probability awaiting review
27216 D-Thomine feat(Cardinal/Finite): ENat powers and cardinality t-algebra merge conflict
26267 vasnesterov feat(Analysis/Calculus): Taylor series converges to function on whole ball t-analysis awaiting author
28448 ShreckYe chore(Data/Nat/Factorization/PrimePow): possibly simplify the last line of `isPrimePow_pow_iff` t-data new-contributor easy delegated awaiting review
28456 euprunin chore(Data/Nat): deprecate `exists_lt_succ` (duplicate) t-data awaiting-author awaiting review
21965 JovanGerb feat: extensible `push` and `pull` tactics t-meta awaiting-author failing CI
27824 ChrisHughes24 feat(Calculus): exists_gt_of_deriv_pos and variants t-analysis awaiting review
26331 Timeroot feat(Algebra/Polynomial): Descartes' Rule of signs t-algebra failing CI
27212 CBirkbeck Cot series iterated deriv within awaiting review
28701 grunweg feat: the maximal atlas is closed under restriction t-differential-geometry ??? missing CI information
28613 espottesmith feat(Combinatorics): define undirected hypergraphs new-contributor t-combinatorics failing CI
28469 EtienneC30 feat: basic properties of toLp and ofLp t-analysis awaiting review
28693 faenuccio feat(Analysis.Normed.Module.Milman-Pettis): add Milman-Pettis theorem t-analysis WIP labelled WIP
25970 wwylele feat(RingTheory): decompose archimedean classes of HahnSeries t-ring-theory large-import awaiting review
26975 Whysoserioushah feat: a norm_num extension for complex numbers t-meta awaiting review
25775 emilyriehl feat(AlgebraicTopology/SimplicialSet/NerveAdjunction): to Strict Segal 2 t-algebraic-topology infinity-cosmos t-category-theory awaiting-author awaiting review
28706 euprunin chore: golf entire `apply_eq_iff_eq_symm_apply`, `dite_ne_left_iff`, `exists_prime_lt_and_le_two_mul_succ`, `lt_up` and `sUnion_mem_empty_univ` using `grind` ??? missing CI information
25179 YaelDillies feat: `#print sorries`, a command to find usage of `sorry` toric maintainer-merge t-meta awaiting review
28696 or4nge19 feat(Quiver/Path/Vertices): add splitting lemmas and decomposition results new-contributor 🟤 ⚠️ running CI
28662 gasparattila feat: products of affine maps new-contributor t-euclidean-geometry t-algebra awaiting author
27301 js2357 feat: `MeasureTheory.Measure.sum_restrict_le` carleson t-measure-probability awaiting-author awaiting review
27174 ADedecker chore(OreLocalization): generalize some results from rings to monoids with zeros t-algebra delegated delegated
28708 sjh227 feat (Data) : edit DoublyStochastic, add Stochastic to matrix t-data new-contributor ??? missing CI information
28704 euprunin chore: remove unnecessary tactic invocations ??? missing CI information
25902 pfaffelh feat: The finite product of semi-rings (in terms of measure theory) is a semi-ring. large-import t-measure-probability failing CI
25883 pfaffelh feat: introduce Gram matrices migrated-from-branch new-contributor t-analysis awaiting author
25899 pfaffelh feat(Topology/Compactness/CompactSystem): introduce compact Systems t-topology failing CI
28700 Timeroot feat(ModelTheory): Set.Definable is transitive large-import ??? ⚠️ missing CI information
28697 chrisflav chore(RingTheory/Generators): make type argument in `localizationAway` and `baseChange` explicit t-ring-theory maintainer-merge awaiting review
28667 kckennylau feat(Algebra/Order): two auxiliary definitions t-algebra awaiting review
28656 euprunin chore(Data/Int): golf entire `coe_leastOfBdd_eq` and `coe_greatestOfBdd_eq` using `grind` t-data maintainer-merge awaiting review
28640 euprunin chore(Data/List): golf entire `getElem?_getD_replicate_default_eq` and `getD_append_right` using `grind` t-data maintainer-merge awaiting review
26345 mans0954 feature(Analysis/LocallyConvex/Polar): Bipolar theorem large-import t-analysis awaiting-author awaiting author
25795 dagurtomas chore(Condensed): introduce an abbrev for the equivalence of light condensed sets with a category of sheaves on a small site t-condensed awaiting review
26722 vlad902 feat(SimpleGraph): sub-walks of minimal length are also minimal t-combinatorics awaiting-author awaiting review
26201 scholzhannah feat: subcomplexes of a classical CW complex t-topology awaiting review
25794 dagurtomas feat(CategoryTheory): localization preserves braided structure file-removed t-category-theory merge conflict
26120 vasnesterov feat(Data/Seq): `update` and `set` operations for `Seq` t-data awaiting review
28702 Timeroot Experiment for swapping MulOneClass -> Mul, One in MonoidHom bench-after-CI t-algebra ??? missing CI information
28534 raja-19 feat(Data/Set/Card): add lemmas of the form `card_Union_le` t-data new-contributor awaiting review
25123 eric-wieser feat: add rfl lemmas for monoidal categories maintainer-merge t-algebra awaiting review
28400 CBirkbeck Define the Dedekind Eta function t-number-theory awaiting review
28712 euprunin chore: remove unnecessary tactic invocations ??? missing CI information
25743 robin-carlier feat(AlgebraicTopology/SimplexCategory/Augmented): monoidal structure on `AugmentedSimplexCategory` t-algebraic-topology t-category-theory awaiting review
28099 themathqueen feat(LinearAlgebra/Matrix/Spectrum): the eigenvalues of Hermitian `A` are all `0` iff `A = 0` t-algebra easy awaiting review
28678 vihdzp feat: well-founded instances for `ULift` t-order easy awaiting author
28665 staroperator feat(Algebra/Group): add theorems about `Submonoid.pi` t-algebra awaiting review
28718 imbrem Added chosen finite coproducts new-contributor t-category-theory ??? missing CI information
28658 hrmacbeth feat(Tactic/FieldSimp): rewrite for performance and robustness large-import t-meta awaiting review
28296 strihanje01 feat(Combinatorics/Additive/VerySmallDoubling): Hamidoune's Freiman-Kneser theorem for nonabelian groups large-import new-contributor t-combinatorics awaiting-author awaiting author
28705 b-mehta feat(MetricSpace/Closeds): set of nonempty compacts below a closed set is closed t-topology ??? missing CI information
26243 DavidLedvinka feat(Topology): Add PairReduction.lean t-topology awaiting-author awaiting author
28710 alreadydone chore(Algebra): make MulEquivClass an alias of MulHomClass t-algebra ??? missing CI information
28719 mitchell-horner refactor: move and refactor Turan.lean, redefine `IsTuranMaximal` large-import t-combinatorics ??? missing CI information
28674 bwangpj feat: ContMDiff.iterate new-contributor t-differential-geometry awaiting-author awaiting review
28709 yoh-tanimoto add instance `CompleteSpace` for a subtype with `IsClosed` instance t-topology ??? missing CI information
28480 euprunin chore(Combinatorics): golf entire `ofColex_inj`, `homOfEq_heq` and `mem_supp_of_adj_mem_supp`. deprecate `tail_cons_eq`. t-combinatorics awaiting bors
28720 wwylele feat(RingTheory/PowerSeries): mul and pow of monomial t-ring-theory ??? missing CI information
26738 javra feat(AlgebraicToplogy/SimplexCategory): add notation for faces and degeneracies general truncated simplex categories t-algebraic-topology infinity-cosmos awaiting review
26829 pechersky feat(RingTheory/Valuation): Valuation.leAddSubgroup and ideal/submodule versions of ltAddSubgroup t-ring-theory awaiting review
27244 xroblot feat(RingTheory/DedekindDomain): lifting an ideal in an extension is injective t-ring-theory large-import awaiting review
27657 euprunin chore(Geometry/RingedSpace): remove use of `erw` in `forget_preservesLimitsOfLeft` t-algebraic-geometry awaiting review
27992 staroperator feat(Algebra): cancellation inheritance t-algebra awaiting review
28124 kckennylau feat(Tactic): Call an arbitrary Simproc t-meta awaiting review
28248 YaelDillies feat: expectation and (conditional) variance of a Bernoulli random variable t-measure-probability awaiting review
28329 pechersky feat(RingTheory/Valuation): generalize CommGroupWithZero on mrange to MonoidWithZeroHom t-ring-theory t-order t-algebra awaiting review
28287 robin-carlier chore(CategoryTheory/Bicategory): move `map₂_eqToHom` earlier in the import graph large-import t-category-theory awaiting review
28352 agjftucker feat(Analysis): add three little theorems relating argument to image t-analysis awaiting review
14426 adomani dev: `#min_imps` command merge-conflict WIP labelled WIP
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
12936 mattrobball chore(Quiver.Opposite): make `Quiver.Hom.op/unop` `abbrev`'s merge-conflict merge conflict
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
12934 grunweg chore: replace more uses of > or ≥ by < or ≤ merge-conflict awaiting-author help-wanted looking for help
12608 eric-wieser feat: allow `nsmul` / `zsmul` to be omitted again, with a warning t-algebra t-meta merge-conflict awaiting-author merge conflict
11617 urkud refactor(Finset): redefine Finset.diag, review API t-logic merge-conflict awaiting-author merge conflict
12192 Ruben-VandeVelde feat: generalize isLittleO_const_id_atTop/atBot t-analysis merge-conflict awaiting-author 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
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
10024 ADedecker feat: rename `connectedComponentOfOne` to `identityComponent`, prove that it is normal and open t-topology awaiting-CI merge-conflict does not pass CI
10444 urkud doc(IsROrC): expand the docstring t-analysis merge-conflict awaiting-author documentation 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
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
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
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
9229 eric-wieser refactor(Algebra/GradedMonoid): Use `HMul` to define `GMul` t-algebra merge-conflict WIP labelled WIP
9354 chenyili0818 feat: monotonicity of gradient on convex real-valued functions t-analysis merge-conflict awaiting-author merge conflict
9146 laughinggas feat(Data/ZMod/Defs): Topological structure on `ZMod` t-algebra t-topology merge-conflict awaiting-author merge conflict
9487 eric-wieser feat: the exponential of dual numbers over non-commutative rings t-measure-probability t-algebra t-analysis merge-conflict WIP labelled WIP
9564 AntoineChambert-Loir weaken commutativity assumptions for AdjoinRoot.lift and AdjoinRoot.liftHom t-algebra merge-conflict WIP labelled WIP
8503 thorimur feat: meta utils for `refine?` t-meta merge-conflict awaiting-author merge conflict
8616 eric-wieser feat(Algebra/FreeAlgebra): add right action and `IsCentralScalar` t-algebra awaiting-CI merge-conflict does not pass CI
8519 eric-wieser refactor(LinearAlgebra/TensorProduct): golf using `liftAddHom` t-algebra merge-conflict awaiting-author merge conflict
7713 RemyDegenne feat: add_left/right_inj for measures t-measure-probability 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
7351 shuxuezhuyi feat(Topology/Algebra/Order): extend function on `Ioo` to `Icc` t-order merge-conflict awaiting-author merge conflict
7227 kmill feat: flexible binders and integration into notation3 t-meta merge-conflict WIP labelled WIP
6931 urkud refactor(Analysis/Normed*): use `RingHomIsometric` for `*.norm_cast` t-analysis merge-conflict help-wanted looking for help
7835 shuxuezhuyi feat(LinearAlgebra/Matrix): `lift` for projective special linear group t-algebra merge-conflict awaiting-author ??? missing CI information
7909 mcdoll fix(Tactic/Continuity): remove npowRec and add new tag for Continuous.pow t-topology t-meta merge-conflict WIP labelled WIP
7427 MohanadAhmed Mohanad ahmed/sort eigenvalues abs merge-conflict WIP labelled WIP
7467 ADedecker feat: spectrum of X →ᵇ ℂ is StoneCech X t-analysis merge-conflict WIP labelled WIP
6791 eric-wieser refactor: Use flat structures for morphisms awaiting-CI merge-conflict awaiting-author help-wanted looking for help
7875 astrainfinita chore: make `SMulCommClass A A B` and `SMulCommClass A B B` higher priority slow-typeclass-synthesis t-algebra merge-conflict ??? missing CI information
7962 eric-wieser feat: `DualNumber (Quaternion R)` as a `CliffordAlgebra` t-algebra merge-conflict WIP labelled WIP
6777 adomani chore(Co*variantClass): replace eta-expanded (· * ·), (· + ·), (· ≤ ·), (· < ·) merge-conflict merge conflict
7932 eric-wieser refactor(Algebra/TrivSqZeroExt): replace with a structure t-algebra awaiting-CI merge-conflict does not pass CI
6580 adomani chore: `move_add`-driven replacements 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
7601 digama0 feat: ring hom support in `ring` t-algebra t-meta merge-conflict awaiting-author merge conflict
6630 MohanadAhmed feat: Reduced Spectral Theorem t-algebra merge-conflict WIP labelled WIP
6079 eric-wieser fix: deduplicate variables awaiting-CI merge-conflict does not pass CI
4960 eric-wieser chore: use `open scoped` awaiting-CI merge-conflict does not pass CI
3808 kim-em feat: #formalize, backed by a choice of LLMs t-meta merge-conflict awaiting-author merge conflict
4871 j-loreaux feat: define the additive submonoid of positive elements in a star ordered ring t-algebra awaiting-CI merge-conflict ??? does not pass CI
6002 slerpyyy feat(Analysis.SpecialFunctions.Gaussian): add `integrable_fun_mul_exp_neg_mul_sq` t-analysis merge-conflict awaiting-author merge conflict
5934 eric-wieser feat: port Data.Rat.MetaDefs t-meta merge-conflict mathlib-port help-wanted looking for help
6328 astrainfinita chore: make some instance about `Sub...Class` lower priority t-algebra awaiting-CI merge-conflict WIP labelled WIP
6491 eric-wieser chore(Mathlib/Algebra/Hom/GroupAction): add `SMulHomClass.comp_smul` t-algebra merge-conflict merge conflict
6268 eric-wieser Fixups to #3838 merge-conflict WIP labelled WIP
6633 adomani feat(..Polynomial..): `MvPolynomial`s have no zero divisors t-algebra merge-conflict awaiting-author merge conflict
6993 jjaassoonn feat : lemmas about `AddMonoidAlgebra.{divOf, modOf}` t-algebra merge-conflict merge conflict
6330 astrainfinita chore: make some instance about `Sub...Class` higher priority than `Sub...` slow-typeclass-synthesis t-algebra merge-conflict WIP labelled WIP
7076 grunweg feat: define measure zero subsets of a manifold t-measure-probability t-differential-geometry merge-conflict WIP labelled WIP
6403 astrainfinita chore: change instance priorities of `Ordered*` hierarchy slow-typeclass-synthesis t-order t-algebra merge-conflict awaiting-author merge conflict
6195 eric-wieser chore(RingTheory/TensorProduct): golf the `mul` definition t-algebra awaiting-CI merge-conflict does not pass CI
4127 kmill refactor: create HasAdj class, define Digraph, and generalize some SimpleGraph API t-combinatorics merge-conflict awaiting-author merge conflict
5912 ADedecker feat(Analysis.Distribution.ContDiffMapSupportedIn): space of smooth maps with support in a fixed compact t-analysis merge-conflict WIP labelled WIP
6210 MohanadAhmed feat(Data/IsROrC/Basic): add a `StarOrderedRing` instance t-algebra t-analysis merge-conflict WIP labelled WIP
6590 mcdoll feat: composition of LinearPMaps t-algebra merge-conflict WIP labelled WIP
5133 kmill feat: IntermediateField adjoin syntax for sets of elements t-algebra merge-conflict WIP labelled WIP
3757 thorimur feat: config options for `fail_if_no_progress` t-meta merge-conflict WIP labelled WIP
12353 thorimur feat: `conv%` t-meta merge-conflict WIP labelled WIP
7903 urkud feat: define `UnboundedSpace` t-topology merge-conflict help-wanted looking for help
15400 grunweg feat: "confusing variables" linter t-linter merge-conflict WIP labelled WIP
12143 adomani feat: generic linter, absorbing `cdot` linter and `attribute [instance] in` linter t-linter merge-conflict failing CI
14654 grunweg feat(runLinter): allow only running certain linters t-linter RFC merge-conflict failing CI
15679 adomani test: refactor in CI merge-conflict WIP labelled WIP
10629 madvorak feat: List.cons_sublist_append_iff_right t-data merge-conflict merge conflict
9973 Ruben-VandeVelde feat: polynomials formed by lists t-data merge-conflict please-adopt looking for help
12926 joelriou feat(CategoryTheory): the monoidal category structure induced by a monoidal functor t-category-theory merge-conflict WIP labelled WIP
12869 adomani feat: linter and script for `theorem` vs `lemma` t-linter merge-conflict awaiting-author merge conflict
12093 ADedecker feat: tweak the definition of semicontinuity to behave better in nonlinear orders t-topology merge-conflict WIP labelled WIP
11393 mcdoll feat(Analysis/Distribution/SchwartzSpace): The Heine-Borel property t-analysis merge-conflict WIP labelled WIP
9444 erdOne feat: Various instances regarding `𝓞 K`. t-number-theory merge-conflict help-wanted looking for help
8931 hmonroe feat(Computable): define P, NP, and NP-complete t-computability merge-conflict awaiting-author failing CI
8608 eric-wieser feat: multiplicativize `AddTorsor` t-algebra merge-conflict WIP labelled WIP
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
13791 digama0 refactor: Primrec and Partrec tech debt t-computability merge-conflict merge conflict
11964 adamtopaz feat: The functor of points of a scheme t-algebraic-geometry t-category-theory merge-conflict merge conflict
12418 rosborn style: replace preimage_val with ↓∩ notation merge-conflict merge conflict
9978 astrainfinita 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
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 ??? missing CI information
13573 Shamrock-Frost feat: add multivariate polynomial modules t-algebra merge-conflict awaiting-author merge conflict
6517 MohanadAhmed feat: discrete Fourier transform of a finite sequence t-algebra merge-conflict awaiting-author merge conflict
13155 alreadydone feat(NumberTheory/EllipticDivisibilitySequence): show elliptic relations follow from even-odd recursion t-algebra t-number-theory merge-conflict awaiting-author merge conflict
15600 adomani feat: lint also `let` vs `have` t-linter merge-conflict WIP labelled WIP
14038 adomani test/decl diff in lean dev merge-conflict WIP labelled WIP
7545 shuxuezhuyi feat: APIs of `Function.extend f g e'` when `f` is injective t-logic merge-conflict awaiting-author merge conflict
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
11283 hmonroe feat(ModelTheory/Satisfiability): define theory with independent sentence t-logic merge-conflict WIP labelled WIP
16914 siddhartha-gadgil Loogle syntax with non-reserved merge-conflict WIP labelled WIP
10075 dupuisf refactor: generalize `MonoidHom.ker` and `MonoidHom.range` to `MonoidHomClass` t-algebra merge-conflict awaiting-author merge conflict
10991 thorimur feat: `tfae` block tactic t-meta merge-conflict modifies-tactic-syntax WIP labelled WIP
16464 Parcly-Taxel chore: deprecate `Nat.(case_)strong_induction_on` tech debt merge-conflict merge conflict
8118 iwilare feat(CategoryTheory): add dinatural transformations t-category-theory merge-conflict awaiting-author merge conflict
17110 astrainfinita chore: deprecate some lemmas about equality blocked-by-batt-PR merge-conflict blocked on another PR
7516 ADedecker perf: use `abbrev` to prevent unifying useless data merge-conflict WIP labelled WIP
17127 astrainfinita chore: remove global `Quotient.mk` `⟦·⟧` notation t-data merge-conflict merge conflict
14712 astrainfinita perf: change instance priority and order about `OfNat` slow-typeclass-synthesis t-algebra merge-conflict delegated merge conflict
11500 mcdoll refactor(Topology/Algebra/Module/WeakDual): Clean up t-topology merge-conflict awaiting-author merge conflict
5995 astrainfinita feat: add APIs about `Quotient.choice` t-data RFC merge-conflict awaiting-author merge conflict
8029 alreadydone refactor: Homotopy between Functions not ContinuousMaps t-topology RFC merge-conflict merge conflict
13156 erdOne refactor(Algebra/Module/LocalizedModule): Redefine `LocalizedModule` in terms of `OreLocalization`. t-algebra merge-conflict failing CI
16348 urkud refactor(Topology): require `LinearOrder` with `OrderTopology` t-order t-topology merge-conflict awaiting-author merge conflict
6034 mattrobball feat (Mathlib.Tactic.FieldSimp) : discharger uses normCast t-meta merge-conflict awaiting-author failing CI
16925 YnirPaz feat(SetTheory/Cardinal/Cofinality): aleph index of singular cardinal has infinite cofinality t-set-theory merge-conflict WIP labelled WIP
9605 davikrehalt feat(Data/Finset & List): Add Lemmas for Sorting and Filtering t-data new-contributor merge-conflict please-adopt awaiting-author looking for help
9654 urkud feat: add `@[mk_eq]` version of `@[mk_iff]` t-meta merge-conflict awaiting-author merge conflict
16704 AntoineChambert-Loir feat(Mathlib.Data.Ordering.Dickson): Dickson orders t-order merge-conflict WIP labelled WIP
16355 Ruben-VandeVelde feat: odd_{add,sub}_one t-algebra t-number-theory merge-conflict awaiting-author merge conflict
8479 alexjbest feat: use leaff in CI merge-conflict awaiting-author WIP ⚠️ labelled WIP
14598 Command-Master chore: add typeclasses to unify various `add_top`, `add_eq_top`, etc. new-contributor t-order t-algebra merge-conflict merge conflict
12778 MichaelStollBayreuth perf: decouple algebraic and order hierarchies in type class search slow-typeclass-synthesis t-order t-algebra merge-conflict merge conflict
16885 metinersin feat(ModelTheory/Complexity): define literals new-contributor t-logic merge-conflict awaiting-author merge conflict
9341 winstonyin feat: Naturality of integral curves t-differential-geometry merge-conflict awaiting-author merge conflict
13248 hcWang942 feat: basic concepts of auction theory new-contributor t-logic merge-conflict awaiting-author merge conflict
9344 erdOne feat: Add `AddGroup.FG` -> `Module.Finite ℤ` as instances t-algebra merge-conflict awaiting-author merge conflict
12133 ADedecker feat: generalize instIsLowerProd to arbitrary products t-order t-topology merge-conflict awaiting-author merge conflict
16637 astrainfinita perf: reorder `extends` of `(Add)Monoid` t-algebra merge-conflict WIP labelled WIP
14739 urkud feat(Measure): add `gcongr` lemmas t-measure-probability merge-conflict awaiting-author WIP help-wanted looking for help
8661 joelriou feat(CategoryTheory/Sites): descent of sheaves t-category-theory merge-conflict WIP labelled WIP
18806 astrainfinita 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
17623 astrainfinita feat(Algebra/Order/GroupWithZero/Unbundled): add some lemmas awaiting-zulip t-order t-algebra merge-conflict awaiting a zulip discussion
16361 vihdzp chore(SetTheory/Ordinal/FixedPointApproximants): golf + better variable management t-set-theory t-logic merge-conflict awaiting-author merge conflict
17513 astrainfinita perf: do not search algebraic hierarchies when using `map_*` lemmas awaiting-bench 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
9598 AlexKontorovich feat(Analysis/Complex): HasPrimitives on disc t-analysis merge-conflict failing CI
19420 vihdzp feat: AM-HM inequality t-algebra merge-conflict awaiting-author WIP labelled WIP
10332 adri326 feat(Topology/Sets): define regular open sets and their boolean algebra t-topology merge-conflict WIP labelled WIP
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
18756 astrainfinita 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
19125 yhtq feat: add theorems to transfer `IsGalois` between pairs of fraction rings new-contributor t-algebra merge-conflict failing CI
19046 j-loreaux feat: define class `SemigroupAction` t-algebra merge-conflict merge conflict
18841 hrmacbeth chore: change some `linarith`s to `linear_combination`s merge-conflict WIP labelled WIP
18748 astrainfinita refactor: deprecate `ContinuousLinearMapClass` t-algebra t-topology merge-conflict merge conflict
8686 j-loreaux refactor: allow non-unital `AlgEquiv` t-algebra merge-conflict WIP labelled WIP
11142 hmonroe feat(ProofTheory): Define logical symbols abstractly; opens new top-level section, drawing from lean4-logic t-logic merge-conflict awaiting-author merge conflict
11210 hmonroe Test commit merge-conflict WIP labelled WIP
19699 vihdzp chore(SetTheory/Cardinal/Basic): tweak `#α = 0`, `#α = 1`, etc. lemmas t-set-theory awaiting-CI merge-conflict does not pass CI
15773 kkytola feat: Add type class for ENat-valued floor functions t-order merge-conflict awaiting-author merge conflict
3251 kmill feat: deriving `LinearOrder` for simple enough inductive types t-meta merge-conflict awaiting-author WIP labelled WIP
3610 TimothyGu feat: derive Infinite automatically for inductive types t-meta merge-conflict awaiting-author merge conflict
16120 awainverse feat(ModelTheory/Algebra/Ring/Basic): Ring homomorphisms are a `StrongHomClass` for the language of rings t-logic t-algebra RFC merge-conflict failing CI
15045 Command-Master fix(LinearAlgebra/Alternating/Basic): fix `MultilinearMap.alternatization` t-algebra merge-conflict awaiting-author merge conflict
20527 trivial1711 refactor(Topology/UniformSpace/Completion): more descriptive names for `α → Completion α` t-topology merge-conflict merge conflict
17739 Aaron1011 feat(Topology/Order/DenselyOrdered): prove Not (IsOpen) for intervals new-contributor t-topology merge-conflict awaiting-author merge conflict
18474 astrainfinita 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
15711 znssong feat(Combinatorics/SimpleGraph): Some lemmas about walk, cycle and Hamiltonian cycle new-contributor t-combinatorics merge-conflict awaiting-author merge conflict
18629 tomaz1502 feat(Computability.Timed): Formalization of runtime complexity of List.merge t-computability new-contributor merge-conflict awaiting-author merge conflict
8362 urkud feat(Asymptotics): define `ReflectsGrowth` t-analysis merge-conflict awaiting-author failing CI
6692 prakol16 feat: disjoint indexed union of local homeomorphisms t-topology merge-conflict awaiting-author failing CI
19291 PieterCuijpers feat(Algebra/Order/Hom): add quantale homomorphism new-contributor t-algebra merge-conflict awaiting-author failing CI
19352 hrmacbeth chore: change some `nlinarith`s to `linear_combination`s merge-conflict WIP labelled WIP
20372 jvlmdr feat(MeasureTheory/Function): Add ContinuousLinearMap.bilinearCompLp(L) new-contributor t-measure-probability merge-conflict merge conflict
17176 arulandu feat: integrals and integrability with .re new-contributor t-measure-probability merge-conflict awaiting-author merge conflict
20872 grunweg feat: lint against the tactic.skipAssignedInstances option in mathlib tech debt t-linter merge-conflict awaiting-author merge conflict
2605 eric-wieser chore: better error message in linarith t-meta merge-conflict awaiting-author merge conflict
11837 trivial1711 feat: completion of a uniform multiplicative group t-algebra t-topology merge-conflict WIP help-wanted looking for help
14799 luigi-massacci feat(Analysis/MeanInequalities): Weighted QM-AM inequality new-contributor t-analysis easy merge-conflict awaiting-author merge conflict
14686 smorel394 feat (AlgebraicGeometry/Grassmannian): define the Grassmannian scheme workshop-AIM-AG-2024 t-algebraic-geometry merge-conflict please-adopt WIP looking for help
9449 hmonroe feat: Add Turing machine with the quintet definition (TMQ) and a chainable step function for each TM type t-computability merge-conflict awaiting-author failing CI
20663 EtienneC30 feat: `PFunLike` typeclass for partial homomorphisms and `LinearPMapClass` t-data t-algebra merge-conflict WIP labelled WIP
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
10678 adri326 feat(Topology/UniformSpace): prove that a uniform space is completely regular t-topology merge-conflict awaiting-author merge conflict
18785 erdOne feat(CategoryTheory): command that generates instances for `MorphismProperty` t-category-theory t-meta merge-conflict awaiting-author merge conflict
15942 grunweg chore: move style linters into their own file; document all current linters t-linter merge-conflict awaiting-author merge conflict
16311 madvorak feat(Computability): regular languages are context-free t-computability merge-conflict WIP labelled WIP
19943 AlexLoitzl feat(Computability): Add Chomsky Normal Form Grammar and translation t-computability new-contributor merge-conflict awaiting-author merge conflict
19616 adamtopaz fix: Fix the definition of the absolute Galois group of a field t-algebra t-number-theory merge-conflict awaiting-author merge conflict
17005 YnirPaz feat(SetTheory/Cardinal/Regular): define singular cardinals t-set-theory merge-conflict WIP labelled WIP
18463 vihdzp feat(SetTheory/Ordinal/Notation/FundamentalSequence): define type of fundamental sequences t-set-theory t-order merge-conflict merge conflict
12054 adomani feat: auto-bugs t-meta merge-conflict awaiting-author merge conflict
5062 adomani feat(Tactic/Prune + test/Prune): add `prune` tactic, for removing unnecessary hypotheses t-meta merge-conflict modifies-tactic-syntax awaiting-author merge conflict
21433 grunweg chore: change more lemmas to be about enorm instead of nnnorm carleson t-measure-probability merge-conflict awaiting-author merge conflict
21099 chrisflav chore(RingTheory/Generators): use unification hints for variables and relations t-algebra merge-conflict merge conflict
21269 CharredLee (WIP) feat (CategoryTheory/Topos): Add topos theory content new-contributor t-category-theory merge-conflict awaiting-author WIP labelled WIP
12394 JADekker feat : define pre-tight and tight measures t-measure-probability merge-conflict please-adopt awaiting-author looking for help
20454 urkud chore(TangentCone): review names t-analysis merge-conflict failing CI
16550 awainverse feat(ModelTheory): A typeclass for languages expanding other languages t-logic merge-conflict awaiting-author merge conflict
13686 fpvandoorn feat: some finset lemmas t-data merge-conflict awaiting-author merge conflict
14313 grhkm21 feat(RepresentationTheory/FdRep): FdRep is a full subcategory of Rep new-contributor t-algebra t-category-theory merge-conflict failing CI
18626 hannahfechtner feat : define Artin braid groups new-contributor t-algebra merge-conflict awaiting-author merge conflict
10823 alexkeizer feat: convert curried type functions into uncurried type functions t-data merge-conflict awaiting-author merge conflict
13648 urkud feat(Topology/Module): generalize `ContinuousLinearMap.compSL` t-algebra t-analysis t-topology merge-conflict awaiting-author failing CI
21339 vihdzp fix(Data/List/Lex): remove duplicate `List.LE` instance t-data merge-conflict merge conflict
16421 astrainfinita 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
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
21959 BGuillemet feat(Topology/ContinuousMap): Stone-Weierstrass theorem for MvPolynomial new-contributor t-topology merge-conflict merge conflict
20750 adomani feat: the envLinter syntax linter large-import t-linter merge-conflict failing CI
18470 astrainfinita perf: lower the priority of `Normed*.to*` instances slow-typeclass-synthesis t-algebra t-analysis merge-conflict ❌? infrastructure-related CI failing
16944 YnirPaz feat(SetTheory/Cardinal/Cofinality): lemmas about limit ordinals and cofinality t-set-theory merge-conflict WIP labelled WIP
17368 Felix-Weilacher feat(Topology/Baire/BaireMeasurable): add the Kuratowski-Ulam theorem t-topology merge-conflict failing CI
8767 eric-wieser refactor(Cache): tidy lake-manifest parsing in Cache t-meta merge-conflict failing CI
15578 znssong feat(Function): Fixed points of function `f` with `f(x) >= x` new-contributor t-analysis merge-conflict awaiting-author merge conflict
22517 j-loreaux feat: `ℕ+` powers in semigroups large-import merge-conflict WIP ⚠️ labelled WIP
22805 ScottCarnahan feat (FieldTheory/Finite): fixed points of frobenius t-algebra merge-conflict WIP labelled WIP
22660 Ruben-VandeVelde chore: follow naming convention around Group.IsNilpotent t-algebra merge-conflict merge conflict
13999 adomani feat: a linter to flag potential confusing conventions t-linter merge-conflict awaiting-author merge conflict
15991 vihdzp feat(SetTheory/Ordinal/CantorNormalForm): alternate CNF recursion principle t-set-theory t-logic merge-conflict awaiting-author merge conflict
17758 vihdzp feat(SetTheory/Ordinal/ENat): `Ordinal.toENat` t-set-theory merge-conflict failing CI
21856 vihdzp chore(SetTheory/Cardinal/Basic): generalize universes of `sum_le_iSup_lift` t-set-theory merge-conflict merge conflict
19013 quangvdao feat(Algebra/BigOperators/Fin): Add `finSigmaFinEquiv` t-algebra merge-conflict awaiting-author merge conflict
20850 vihdzp chore(Logic/Equiv/Basic): extend `sumCompl` API t-data 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
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
15774 kkytola feat: Topology on `ENat` t-order t-topology merge-conflict WIP labelled WIP
18284 chrisflav feat(AlgebraicGeometry): relative gluing of schemes t-algebraic-geometry merge-conflict WIP labelled WIP
20613 grunweg chore: golf using `List.toArrayMap` large-import merge-conflict failing CI
15989 vihdzp feat(SetTheory/Ordinal/Principal): golf theorems on additively principal ordinals t-set-theory t-logic merge-conflict awaiting-author merge conflict
22682 grunweg chore(Topology/Homeomorph): split out various constructions tech debt t-topology RFC merge-conflict failing CI
21018 markimunro feat(Data/Matrix): add file with key definitions and theorems about elementary row operations t-data new-contributor merge-conflict awaiting-author enhancement failing CI
23514 eric-wieser refactor: smooth over Lattice/LinearOrder inheritance merge-conflict failing CI
19907 kim-em chore: remove some 'nonrec' t-algebra merge-conflict failing CI
22810 pechersky feat(Counterexamples): metric space not induced by norm t-analysis t-topology merge-conflict WIP labelled WIP
13124 astrainfinita chore: remove `CovariantClass` and `ContravariantClass` merge-conflict WIP labelled WIP
20401 RemyDegenne feat: add sigmaFinite_iUnion t-measure-probability merge-conflict awaiting-author merge conflict
19275 eric-wieser fix: if nolint files change, do a full rebuild merge-conflict delegated failing CI
12251 ScottCarnahan refactor(RingTheory/HahnSeries) : several generalizations t-order t-algebra merge-conflict WIP labelled WIP
22727 grunweg feat: rewrite the isolated by and colon linters in Lean t-linter merge-conflict awaiting-author merge conflict
22027 vihdzp chore(SetTheory/Ordinal/FixedPoint); review `Ordinal.nfp` API t-set-theory merge-conflict merge conflict
15212 victorliu5296 feat: Add fundamental theorem of calculus-2 for Banach spaces new-contributor t-measure-probability t-analysis merge-conflict awaiting-author merge conflict
22701 ctchou feat(Combinatorics): the Katona circle method new-contributor t-combinatorics merge-conflict merge conflict
23786 grunweg Mr librarynote def 2b large-import merge-conflict WIP labelled WIP
23411 PatrickMassot chore: remove finiteness from Order.Filter.Lift longest-pole t-topology merge-conflict merge conflict
22579 kvanvels doc(Topology/Defs/Induced): fix comments on three functions related to RestrictGenTopology t-topology merge-conflict awaiting-author documentation merge conflict
21488 imbrem feat(CategoryTheory/Monoidal): premonoidal categories new-contributor t-category-theory merge-conflict merge conflict
21525 sinhp feat(CategoryTheory): Locally Cartesian Closed Categories (Prelim) large-import t-category-theory merge-conflict merge conflict
19425 hrmacbeth perf: gcongr forward-reasoning adjustment merge-conflict awaiting-author merge conflict
20873 vbeffara feat(Topology/Covering): path lifting and homotopy lifting new-contributor t-topology merge-conflict awaiting-author failing CI
22817 peabrainiac feat(CategoryTheory/Sites): local sites t-category-theory merge-conflict WIP labelled WIP
6252 michaellee94 feat(Geometry/Manifolds/Instances/Homeomorph): Homeomorphism maps `C^k` manifolds to `C^k` manifolds t-differential-geometry merge-conflict WIP labelled WIP
23867 kim-em chore: remove unnecessary `[AtLeastTwo n]` hypotheses bench-after-CI merge-conflict failing CI
16314 astrainfinita chore(Data/Quot): deprecate `ind*'` APIs t-data merge-conflict merge conflict
13795 astrainfinita perf(Algebra/{Group, GroupWithZero, Ring}/InjSurj): reduce everything t-algebra merge-conflict merge conflict
23509 eric-wieser refactor: Make ENNReal an abbrev t-data merge-conflict failing CI
11455 adomani fix: unsqueeze simp, re Yaël's comments on #11259 merge-conflict awaiting-author merge conflict
7325 eric-wieser chore: use preimageIso instead of defeq abuse for InducedCategory t-category-theory awaiting-CI merge-conflict does not pass CI
7874 astrainfinita chore: make `IsScalarTower A A B` and `IsScalarTower A B B` higher priority slow-typeclass-synthesis t-algebra awaiting-CI merge-conflict ??? does not pass CI
5952 eric-wieser feat: add Qq wrappers for ToExpr awaiting-CI t-meta merge-conflict does not pass CI
15483 astrainfinita chore(GroupTheory/Coset): reduce defeq abuse t-algebra merge-conflict merge conflict
16594 astrainfinita perf: reorder `extends` and remove some instances in algebra hierarchy slow-typeclass-synthesis t-algebra merge-conflict failing CI
12673 grunweg feat: add ContDiff.lipschitzOnWith t-analysis merge-conflict awaiting-author help-wanted looking for help
20567 grunweg feat(Cache): two small features t-meta merge-conflict merge conflict
20313 thefundamentaltheor3m feat(Data/Complex/Exponential): prove some useful results about the complex exponential. new-contributor t-analysis merge-conflict failing CI
22698 Kiolt feat: notation for whisker(Left/Right)Iso toric t-category-theory merge-conflict failing CI
20730 kuotsanhsu feat(LinearAlgebra/Matrix/SchurTriangulation): prove Schur decomposition/triangulation new-contributor t-algebra merge-conflict awaiting-author failing CI
19117 eric-wieser feat: derivatives of matrix operations t-analysis merge-conflict WIP labelled WIP
12605 astrainfinita chore: attribute [induction_eliminator] merge-conflict awaiting-author merge conflict
15099 joelriou feat(CategoryTheory/Sites): the Mayer-Vietoris long exact sequence in sheaf cohomology t-category-theory merge-conflict WIP labelled WIP
23859 urkud feat(Topology/../Order/Field): generalize to `Semifield` t-topology merge-conflict merge conflict
23810 b-reinke chore(Order/Interval): generalize succ/pred lemmas to partial orders t-order merge-conflict merge conflict
24285 madvorak chore(Algebra/*-{Category,Homology}): remove unnecessary universe variables t-algebra merge-conflict merge conflict
8370 eric-wieser refactor(Analysis/NormedSpace/Exponential): remove the `𝕂` argument from `exp` awaiting-zulip t-analysis merge-conflict failing CI
23621 astrainfinita chore: deprecate `LinearOrderedComm{Monoid, Group}WithZero` t-order t-algebra merge-conflict merge conflict
22583 imathwy feat: affinespace homeomorphism t-algebra merge-conflict awaiting-author failing CI
24322 mattrobball chore: merge repeated `Type*` binders merge-conflict awaiting-author failing CI
23138 grunweg feat: (unoriented) bordism groups t-differential-geometry merge-conflict WIP labelled WIP
23593 erdOne feat(AlgebraicGeometry): the tilde construction is functorial t-algebraic-geometry merge-conflict awaiting-author merge conflict
21065 eric-wieser feat: generalize `tangentConeAt.lim_zero` to TVS t-analysis merge-conflict WIP labelled WIP
22721 grunweg chore(MeasureTheory/Function/LpSeminorm/Basic): generalise more results to enorm classes carleson t-measure-probability merge-conflict WIP labelled WIP
24354 grunweg chore(HasFiniteIntegral): rename three lemmas t-measure-probability merge-conflict merge conflict
14731 adomani feat: the repeated typeclass assumption linter large-import t-linter merge-conflict WIP labelled WIP
13649 astrainfinita chore: redefine `Nat.div2` `Nat.bodd` merge-conflict merge conflict
19520 erdOne refactor(Algebra/Module): Redefine `LocalizedModule` in terms of `OreLocalization` t-algebra merge-conflict failing CI
14675 adomani dev: the repeated variable linter t-linter merge-conflict WIP labelled WIP
14330 Ruben-VandeVelde chore: split Mathlib.Algebra.Star.Basic merge-conflict awaiting-author merge conflict
14023 mattrobball perf(RingTheory.OreLocalization): make data irreducible merge-conflict ??? missing CI information
8511 eric-wieser refactor(MeasureTheory/Measure/Haar/Basic): partially generalize to the affine case t-measure-probability merge-conflict awaiting-author merge conflict
7994 ericrbg chore: generalize `LieSubalgebra.mem_map_submodule` t-algebra merge-conflict please-adopt looking for help
6317 eric-wieser refactor(Data/Finsupp/Defs): make Finsupp.single defeq to Pi.single t-data merge-conflict WIP labelled WIP
4979 mhk119 doc(Data/Nat/Bitblast): initial commit t-data merge-conflict merge conflict
11524 mcdoll refactor: Introduce type-class for SchwartzMap t-analysis merge-conflict WIP labelled WIP
22269 Thmoas-Guan chore(Algebra): replace Submodule.quotient.mk with Submodule.mkQ t-algebra merge-conflict awaiting-author merge conflict
23546 JovanGerb feat(LinearAlgebra/AffineSpace/AffineSubspace): rename `AffineSubspace.mk'` to `Submodule.shift` t-euclidean-geometry merge-conflict merge conflict
19315 quangvdao feat(Data/Finsupp/Fin): Add `Finsupp` operations on `Fin` tuple t-data merge-conflict awaiting-author merge conflict
7907 urkud feat: introduce `NthRoot` notation class t-algebra t-analysis awaiting-CI merge-conflict does not pass CI
9273 grunweg feat: extended charts are local diffeomorphisms on their source t-differential-geometry merge-conflict merge conflict
24642 grunweg WIP-feat: add layercake formula for ENNReal-valued functions carleson t-analysis merge-conflict WIP labelled WIP
21712 grunweg chore: generalise more lemmas to `ContinuousENorm` carleson t-measure-probability awaiting-CI merge-conflict does not pass CI
21375 grunweg WIP: generalise lemmas to ENorm carleson t-measure-probability awaiting-CI merge-conflict WIP labelled WIP
13685 niklasmohrin feat(Combinatorics): add definitions for network flows new-contributor t-combinatorics merge-conflict awaiting-author merge conflict
15115 kkytola feat: Generalize assumptions in liminf and limsup results in ENNReals t-order t-topology merge-conflict awaiting-author help-wanted looking for help
17129 joneugster feat(Tactic/Linter): add unicode linter for unicode variant-selectors large-import t-linter merge-conflict delegated awaiting-author failing CI
17131 joneugster feat(Tactic/Linter): add unicode linter for unwanted characters large-import t-linter merge-conflict awaiting-author merge conflict
15651 TpmKranz feat(Computability/NFA): operations for Thompson's construction awaiting-zulip t-computability new-contributor merge-conflict awaiting-author awaiting a zulip discussion
22361 rudynicolop feat(Computability/NFA): nfa closure properties awaiting-zulip t-computability new-contributor merge-conflict awaiting-author awaiting a zulip discussion
22837 joneugster feat(Data/Set/Basic): add subset_iff and not_mem_subset_iff t-set-theory t-data merge-conflict merge conflict
24100 eric-wieser feat: restore some explicit binders from Lean 3 tech debt merge-conflict awaiting-author ⚠️ failing CI
21476 grunweg feat(lint-style): enable running on downstream projects t-linter merge-conflict merge conflict
23349 BGuillemet feat: add LocallyLipschitzOn.lipschitzOnWith_of_isCompact and two small lemmas about Lipschitz functions large-import new-contributor t-topology merge-conflict merge conflict
23767 grunweg refactor: make library notes a definition large-import t-meta merge-conflict merge conflict
12438 jjaassoonn feat: some APIs for flat modules t-category-theory merge-conflict WIP labelled WIP
24409 urkud chore(*): fix `nmem` vs `not_mem` names awaiting-zulip tech debt merge-conflict delegated awaiting-author awaiting a zulip discussion
25138 chrisflav chore(RingTheory): remove unnecessary `toRingHom` coercions t-algebra merge-conflict merge conflict
24965 erdOne refactor: Make `IsLocalHom` take unbundled map maintainer-merge t-algebra merge-conflict awaiting-author merge conflict
8740 digama0 fix: improve `recall` impl / error reporting awaiting-CI t-meta merge-conflict awaiting-author does not pass CI
21182 joneugster fix(Util/CountHeartbeats): move elaboration in #count_heartbeats inside a namespace t-meta merge-conflict merge conflict
24105 urkud feat(Topology/UniformSpace/Path): new file t-topology merge-conflict awaiting-author merge conflict
23371 grunweg chore: mark `Disjoint.{eq_bot, inter_eq}` simp t-order merge-conflict awaiting-author merge conflict
16020 adomani feat: compare PR `olean`s size with `master` CI merge-conflict failing CI
16062 adomani Test/ci olean size CI merge-conflict awaiting-author WIP labelled WIP
12799 jstoobysmith feat(LinearAlgebra/UnitaryGroup): Add properties of Special Unitary Group new-contributor t-algebra merge-conflict please-adopt awaiting-author looking for help
23961 astrainfinita refactor: unbundle algebra from `ENormed*` slow-typeclass-synthesis maintainer-merge t-algebra t-analysis merge-conflict awaiting-author merge conflict
23709 plp127 feat: `Nat.findFrom` t-data merge-conflict failing CI
25340 dupuisf chore(Analysis/Convex): move files pertaining to convex/concave functions to their own folder t-convex-geometry merge-conflict merge conflict
13994 grunweg chore(Topology): replace continuity -> fun_prop t-topology merge-conflict failing CI
21734 adomani fix(PR summary): checkout GITHUB_SHA CI merge-conflict awaiting-author WIP labelled WIP
25012 urkud refactor(*): migrate from `Matrix.toLin'` to `Matrix.mulVecLin` merge-conflict merge conflict
24789 Ruben-VandeVelde chore: move Algebra.Group.Hom.End to Algebra.Ring large-import t-algebra merge-conflict awaiting-author merge conflict
13483 adomani feat: automatically replace deprecations t-meta merge-conflict delegated awaiting-author failing CI
20334 miguelmarco feat: allow polyrith to use a local Singular/Sage install new-contributor t-meta merge-conflict awaiting-author merge conflict
23953 b-reinke feat(Data/Matroid/Tutte): define the Tutte polynomial of a matroid t-data merge-conflict WIP labelled WIP
18441 ADedecker refactor(AdicTopology): use new API for algebraic filter bases, and factor some code t-algebra t-topology merge-conflict merge conflict
18439 ADedecker refactor: use new algebraic filter bases API in `FiniteAdeleRing` t-algebra t-topology merge-conflict merge conflict
18438 ADedecker refactor: adapt `KrullTopology` to the new algebraic filter bases API t-algebra t-topology merge-conflict merge conflict
23040 grunweg feat: define immersions and smooth embeddings in infinite dimensions t-differential-geometry merge-conflict WIP labelled WIP
13964 pechersky feat(Data/DigitExpansion): begin defining variant of reals without rationals t-data merge-conflict merge conflict
14752 AntoineChambert-Loir fix(Topology/Algebra/Valued): repair definition of Valued t-algebra t-topology merge-conflict WIP labelled WIP
14009 grunweg chore: replace continuity -> fun_prop in remaining directories t-analysis merge-conflict awaiting-author merge conflict
16074 Rida-Hamadani feat: combinatorial maps and planar graphs t-combinatorics merge-conflict merge conflict
16801 awainverse feat(ModelTheory/Equivalence): The quotient type of formulas modulo a theory t-logic merge-conflict awaiting-author merge conflict
17458 urkud refactor(Algebra/Group): make `IsUnit` a typeclass awaiting-zulip t-algebra merge-conflict failing CI
17627 hrmacbeth feat: universal properties of vector bundle constructions t-differential-geometry merge-conflict delegated merge conflict
19444 joelriou feat(CategoryTheory/Sites): Equivalence of categories of sheaves with a dense subsite that is 1-hypercover dense t-category-theory merge-conflict WIP labelled WIP
19796 peakpoint feat: L'Hopital's rule from within a convex set new-contributor t-analysis merge-conflict merge conflict
22928 javra feat(CategoryTheory): infrastructure for inclusion morphisms into products in categories with 0-morphisms t-category-theory merge-conflict failing CI
23763 grunweg feat(Linter.openClassical): also lint for Classical declarations as … t-linter merge-conflict failing CI
23637 kirilvino feat(Combinatorics/SimpleGraph): every circuit contains a cycle proof new-contributor t-combinatorics merge-conflict awaiting-author merge conflict
24350 erdOne feat(FieldTheory): fg extension over perfect field is separably generated t-algebra merge-conflict merge conflict
24614 JovanGerb chore: rename field `inf` to `min` in `Lattice` t-order merge-conflict awaiting-author merge conflict
24710 chrisflav chore(Data/Set): `tsum` version of `Set.encard_iUnion_of_finite` for non-finite types t-data merge-conflict failing CI
24823 eric-wieser refactor: add `hom` lemmas for the `MonoidalCategory` structure on `ModuleCat` t-algebra merge-conflict merge conflict
25071 erdOne feat(EllipticCurve): basic API for singular cubics t-algebraic-geometry merge-conflict merge conflict
25218 kckennylau feat(AlgebraicGeometry): Tate normal form of elliptic curves awaiting-zulip new-contributor t-algebraic-geometry merge-conflict awaiting a zulip discussion
25283 Brian-Nugent feat: regular local rings new-contributor t-algebra merge-conflict merge conflict
25561 callesonne feat(Category/Grpd): define the bicategory of groupoids t-category-theory merge-conflict awaiting-author merge conflict
25573 JovanGerb feat: define `∃ x > y, ...` notation to mean `∃ x, y < x ∧ ...` t-meta merge-conflict merge conflict
25622 eric-wieser refactor: overhaul instances on LocalizedModule t-algebra merge-conflict failing CI
25797 dagurtomas feat(Condensed): closed symmetric monoidal structure on light condensed modules t-condensed merge-conflict WIP labelled WIP
25816 sgouezel chore: kill coercion from EquivLike to Equiv t-logic merge-conflict WIP labelled WIP
25901 callesonne feat(Bicategory/Opposites): add 1-cell opposite bicategory t-category-theory merge-conflict awaiting-author merge conflict
25988 Multramate refactor(AlgebraicGeometry/EllipticCurve/*): replace Fin 3 with products t-algebraic-geometry merge-conflict merge conflict
26011 linesthatinterlace feat: add elementary lifts for `OneHom`, `MulHom`, `MonoidHom` and `RingHom`. migrated-from-branch t-algebra merge-conflict merge conflict
26012 linesthatinterlace feat: Low-level derivatives of lifts on `OneHom`, `MulHom` and `MonoidHom` migrated-from-branch t-algebra merge-conflict merge conflict
26015 linesthatinterlace feat: Add high-level generalizations from `MonoidHom` lifts migrated-from-branch merge-conflict ⚠️ failing CI
26071 linesthatinterlace feat: Add `id` and `comp` classes for `FunLike` and `refl`, `trans` and `symm` classes for `EquivLike` t-data RFC merge-conflict WIP labelled WIP
26090 grunweg chore: make `finiteness` a default tactic merge-conflict failing CI
26178 ppls-nd-prs feat(CategoryTheory/Limits): Fubini for products new-contributor t-category-theory merge-conflict awaiting-author merge conflict
26384 jjdishere feat(RingTheory/Perfectoid): Fontaine's theta map is surjective t-algebra t-number-theory merge-conflict WIP labelled WIP
26388 jjdishere feat(RingTheory/Perfectoid): Fontaine's theta map and the de Rham period rings t-algebra t-number-theory merge-conflict failing CI
26436 AntoineChambert-Loir feat(Mathlib/Data/Nat/Prime/Defs): fuel Nat.minFac t-data merge-conflict failing CI
26776 sgouezel refactor: make `I` an outparam, and use forgetful inheritance in products RFC merge-conflict WIP labelled WIP
26601 yuma-mizuno feat(CategoryTheory): make `Functor.comp` irreducible t-category-theory merge-conflict WIP labelled WIP
7596 alreadydone feat: covering maps from properly discontinuous actions and discrete subgroups file-removed t-topology merge-conflict merge conflict
24405 mcdoll refactor(Topology/Algebra/Module/WeakDual): Clean up large-import t-topology merge-conflict merge conflict
26647 b-mehta feat(Data/Sym/Sym2): lift commutative operations to sym2 t-data merge-conflict WIP labelled WIP
26067 mapehe feat(Topology/StoneCech): exists_continuous_surjection_from_StoneCech_to_dense_range t-topology merge-conflict merge conflict
21950 erdOne feat(NumberTheory/Padics): the completion of `ℚ` at a finite place is `ℚ_[p]` t-number-theory merge-conflict merge conflict
26913 Paul-Lez feat(NumberTheory/{*}): add a few lemmas about number field and cyclotomic extensions t-algebra t-number-theory awaiting-CI merge-conflict WIP labelled WIP
23990 robertmaxton42 feat (Types.Colimits): Quot is functorial and colimitEquivQuot is natural new-contributor t-category-theory merge-conflict awaiting-author merge conflict
23949 Louddy feat: SkewPolynomial large-import new-contributor t-algebra merge-conflict merge conflict
10541 Louddy feat(Algebra/SkewMonoidAlgebra/Basic): add SkewMonoidAlgebra new-contributor t-algebra merge-conflict WIP labelled WIP
24103 plp127 feat(Topology/UniformSpace/OfCompactT2): generalize theorem t-topology merge-conflict merge conflict
25999 bjoernkjoshanssen feat(Topology/Compactification): projective line over ℝ is homeomorphic to the one-point compactification of ℝ t-topology merge-conflict failing CI
24096 plp127 feat(Topology): Completely Regular Space iff Uniformizable t-topology merge-conflict merge conflict
25710 Paul-Lez feat(Mathlib/Analysis/PDE/Quasilinear/Characteristics): the method of characteristics for first order quasilinear PDEs t-analysis merge-conflict WIP labelled WIP
26603 vihdzp refactor(SetTheory/Ordinal/FixedPoint): redefine `Ordinal.deriv` t-set-theory merge-conflict merge conflict
26895 vihdzp feat(SetTheory/Cardinal/Aleph): `IsStrongLimit (preBeth x)` t-set-theory merge-conflict merge conflict
26911 JovanGerb chore: fix naming of `mono` and `monotone` merge-conflict delegated merge conflict
21838 joneugster feat(Cache): Allow arguments of the form `Mathlib.Data` which correspond to a folder but not a file CI t-meta merge-conflict awaiting-author merge conflict
25611 erdOne chore(RingTheory): add `Algebra (FractionRing R) (FractionRing S)` t-algebra merge-conflict failing CI
27310 ADedecker chore: semilinearize LinearAlgebra.TensorProduct.Basic t-algebra merge-conflict failing CI
27335 eric-wieser chore(Data/List): use simp-normal-form for boolean equalities t-data merge-conflict merge conflict
25284 alreadydone feat(LinearAlgebra/Contraction): bijectivity of `dualTensorHom` + generalize to CommSemiring t-algebra merge-conflict awaiting-author merge conflict
22749 joelriou feat(CategoryTheory/Abelian): the Gabriel-Popescu theorem as a localization with respect to a Serre class t-category-theory merge-conflict WIP labelled WIP
25941 erdOne feat(AlgebraicGeometry): inverse limits and schemes of finite type large-import t-algebraic-geometry merge-conflict delegated failing CI
7300 ah1112 feat: synthetic geometry t-euclidean-geometry merge-conflict awaiting-author help-wanted looking for help
26804 kckennylau (WIP) feat(SetTheory): ZFSet is a model of ZFC t-set-theory merge-conflict WIP labelled WIP
20428 madvorak feat(Data/Sign): lemmas about `∈ Set.range SignType.cast` t-data merge-conflict WIP labelled WIP
23528 Ruben-VandeVelde feat: add isOpen_setOf_affineIndependent t-analysis merge-conflict delegated merge conflict
26608 vihdzp feat(SetTheory/Cardinal/Aleph): `o.card ≤ ℵ_ o` and variants t-set-theory merge-conflict merge conflict
20029 FrederickPu Allow for Config attributes to be set directly new-contributor t-meta merge-conflict WIP labelled WIP
25662 erdOne chore: redefine `LocalizedModule` merge-conflict failing CI
26544 vihdzp feat(SetTheory/ZFC/Ordinal): Lean ordinals to ZFC ordinals large-import t-set-theory merge-conflict awaiting-author failing CI
13973 digama0 feat: lake exe refactor, initial framework t-meta merge-conflict awaiting-author merge conflict
22092 fpvandoorn perf: lower gcongr priority in group mono lemmas t-algebra merge-conflict WIP labelled WIP
27399 MoritzBeroRoos feat: replace every usage of ⬝ᵥ (with old \cdot) by ·ᵥ (with \centerdot) new-contributor merge-conflict ⚠️ merge conflict
27403 MoritzBeroRoos feat: replace probably erroneous usage of ⬝ (with old \cdot) by · (with \centerdot) new-contributor merge-conflict ⚠️ merge conflict
11021 jstoobysmith feat(AlgebraicTopology) : add join of augmented SSets t-algebraic-topology new-contributor merge-conflict WIP labelled WIP
10190 jstoobysmith feat(AlgebraicTopology): add Augmented Simplex Category t-algebraic-topology new-contributor t-category-theory merge-conflict WIP labelled WIP
26303 joelriou feat(AlgebraicTopology): the fundamental lemma of homotopical algebra t-algebraic-topology large-import t-category-theory merge-conflict WIP labelled WIP
20719 gio256 feat(AlgebraicTopology): delaborators for truncated simplicial notations t-algebraic-topology infinity-cosmos t-meta merge-conflict merge conflict
9935 jstoobysmith feat(AlgebraicTopology): add constructors for horns t-algebraic-topology new-contributor merge-conflict awaiting-author merge conflict
25914 eric-wieser feat: add an ext lemma for the opposite category t-category-theory awaiting-CI merge-conflict awaiting-author does not pass CI
20208 js2357 feat: Define the localization of a fractional ideal at a prime ideal t-algebra merge-conflict WIP labelled WIP
26474 xroblot feat(NumberTheory): `N(I 𝓞L) = N(I) ^ [L:K]` for an integral ideal `I` of `K` large-import t-number-theory 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
24260 plp127 feat(Topology): add API for Hereditarily Lindelof spaces t-topology merge-conflict awaiting-author merge conflict
27608 RemyDegenne feat(MeasureTheory): typeclasses for measures with finite moments t-measure-probability merge-conflict WIP labelled WIP
26306 j-loreaux refactor: make `IsSelfAdjoint` and `IsIdempotentElem` one-field structures. large-import merge-conflict failing CI
27238 alreadydone feat(Algebra): IsDomain R[X] ↔ IsDomain R ∧ IsCancelAdd R large-import t-algebra merge-conflict merge conflict
25726 tb65536 (WIP) Galois group of `x ^ n - x - 1` large-import t-algebra merge-conflict WIP labelled WIP
26344 mans0954 feature(Analysis/NormedSpace/MStructure): The component projections on WithLp 1 (α × β) are L-projections file-removed t-analysis merge-conflict WIP labelled WIP
27445 erdOne chore(RingTheory/LocalRing): fix problematic instance t-algebra merge-conflict failing CI
26010 linesthatinterlace feat(`Algebra/Group/Prod`): Add API for inclusion and projection maps from and to the product of units. migrated-from-branch t-algebra merge-conflict WIP labelled WIP
25991 Multramate feat(AlgebraicGeometry/EllipticCurve): generalise nonsingular condition t-algebraic-geometry merge-conflict failing CI
25985 Multramate feat(AlgebraicGeometry/EllipticCurve/Jacobian): add equivalences between points and explicit WithZero types t-algebraic-geometry merge-conflict failing CI
25984 Multramate feat(AlgebraicGeometry/EllipticCurve/Affine): add equivalences between points and explicit WithZero types t-algebraic-geometry merge-conflict failing CI
25982 Multramate feat(AlgebraicGeometry/EllipticCurve/Group): compute range of baseChange t-algebraic-geometry merge-conflict failing CI
25981 Multramate feat(GroupTheory/GroupAction/Basic): define homomorphisms of fixed subgroups induced by homomorphisms of groups t-group-theory merge-conflict failing CI
25980 Multramate feat(GroupTheory/Submonoid/Operations): define homomorphisms of subgroups induced by homomorphisms of groups t-group-theory merge-conflict failing CI
25485 VTrelat feat(SetTheory/ZFC/Naturals): define natural numbers in ZFC t-set-theory new-contributor merge-conflict failing CI
25474 adomani test for .lean/.md check file-removed t-linter merge-conflict failing CI
25238 Hagb feat(Tactic/ComputeDegree): add support for scalar multiplication with different types new-contributor t-meta merge-conflict merge conflict
11632 mattrobball chore(Group/RingTheory.Congruence): make `Quotient`'s reducible t-group-theory merge-conflict merge conflict
3171 eric-wieser refactor: make the algebra hierarchy use flat structures t-algebra merge-conflict WIP labelled WIP
26760 linesthatinterlace refactor(`InformationTheory/Hamming`): Improvements to Hamming type. file-removed t-measure-probability merge-conflict WIP labelled WIP
26385 jjdishere feat(RingTheory/Perfectoid): define integral perfectoid rings t-ring-theory merge-conflict WIP labelled WIP
22954 eric-wieser feat(RingTheory/Congruence/Hom): copy from GroupTheory t-ring-theory merge-conflict failing CI
22898 AntoineChambert-Loir feat(RingTheory/TensorProduct/DirectLimit/FG): direct limit of finitely generated submodules and tensor product t-ring-theory merge-conflict WIP labelled WIP
20431 erdOne feat(RingTheory/AdicCompletion): monotonicity of adic-completeness t-ring-theory merge-conflict awaiting-author merge conflict
20424 erdOne feat(RingTheory): evaluation of power series t-ring-theory merge-conflict failing CI
19596 Command-Master feat(RingTheory/Valuation/PrimeMultiplicity): define `WithTop ℤ`-valued prime multiplicity on a fraction field t-ring-theory large-import merge-conflict awaiting-author merge conflict
18646 jxjwan feat(RingTheory): isotypic components t-ring-theory new-contributor merge-conflict failing CI
17246 pechersky feat(RingTheory/PrimaryDecomposition): PIR of Noetherian under jacobson condition t-ring-theory merge-conflict awaiting-author failing CI
12294 AntoineChambert-Loir feat(Mathlib.RingTheory.TensorProduct.Polynomial) : tensor product of a (univariate) polynomial ring t-ring-theory merge-conflict WIP labelled WIP
21474 erdOne feat(RingTheory): replace `Ring.DimensionLEOne` with `Ring.KrullDimLE` t-ring-theory large-import merge-conflict failing CI
12292 AntoineChambert-Loir feat(Mathlib.RingTheory.TensorProduct.MonoidAlgebra) : tensor product of a monoid algebra t-ring-theory merge-conflict WIP labelled WIP
11575 ScottCarnahan feat (RingTheory/HahnSeries/Addition): Lemmas on leading terms t-ring-theory merge-conflict WIP labelled WIP
9820 jjaassoonn feat(RingTheory/GradedAlgebra/HomogeneousIdeal): generalize to homogeneous submodule t-ring-theory merge-conflict merge conflict
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-ring-theory merge-conflict merge conflict
11212 shuxuezhuyi feat(GroupTheory/GroupAction): instance `MulAction (β ⧸ H) α` t-group-theory large-import merge-conflict awaiting-author merge conflict
27886 alreadydone feat(Algebra): (Mv)Polynomial.X is irreducible assuming NoZeroDivisors t-algebra merge-conflict awaiting-author merge conflict
21847 smmercuri feat: `v.adicCompletionIntegers K` is compact large-import t-number-theory merge-conflict WIP labelled WIP
22782 alreadydone feat(Topology): étalé space associated to a predicate on sections t-topology merge-conflict merge conflict
26200 adomani fix: add label when landrun fails CI merge-conflict merge conflict
26757 fweth feat(CategoryTheory/Topos): define elementary topos new-contributor t-category-theory merge-conflict awaiting-author merge conflict
17469 joelriou feat(Algebra/ModuleCat/Differentials/Presheaf): the presheaf of relative differentials large-import t-algebraic-geometry t-category-theory merge-conflict WIP labelled WIP
18254 callesonne feat(Bicategory/Modification/Pseudo): define modifications between strong natural transformations of pseudofunctors t-category-theory merge-conflict awaiting-author merge conflict
27709 kckennylau chore: fix links merge-conflict WIP labelled WIP
27745 linesthatinterlace refactor(Order/Hom/Basic): redefine `OrderEmbedding` and `OrderIso` to be preorder embeddings and isomorphisms large-import t-order awaiting-CI merge-conflict awaiting-author does not pass CI
27950 alreadydone feat(MonoidAlgebra): criteria for `single` to be a unit, irreducible or prime t-algebra merge-conflict WIP labelled WIP
27922 Parcly-Taxel chore: deprecate `div_eq_iff_mul_eq` and `eq_div_iff_mul_eq` t-algebra merge-conflict merge conflict
27551 Paul-Lez feat(Algebra/Order/Group/Pointwise/Interval): add simple lemmas about Set.MapsTo and intervals t-algebra awaiting-CI merge-conflict ❌? does not pass CI
27378 peakpoint refactor(Geometry/Euclidean/Projection): redefine projection and reflection for affine subspaces new-contributor t-euclidean-geometry merge-conflict merge conflict
26934 mariainesdff feat(RingTheory/DedekindDomain/Ideal): add HeightOneSpectrum.ofPrime t-ring-theory merge-conflict delegated merge conflict
20671 thefundamentaltheor3m feat(Analysis/Asymptotics/SpecificAsymptotics): Proving that 𝛔ₖ(n) = O(nᵏ⁺¹) large-import new-contributor t-number-theory merge-conflict awaiting-author merge conflict
20267 joelriou feat(CategoryTheory): comma categories are accessible t-category-theory merge-conflict awaiting-author WIP labelled WIP
27451 kckennylau feat(RingTheory/Valuation): define ball, closed ball, and sphere t-ring-theory merge-conflict merge conflict
27987 kckennylau feat(RingTheory/Valuation): define ball, closed ball, and sphere t-ring-theory large-import merge-conflict merge conflict
24862 grunweg feat(LocallyIntegrable): generalise more to enorms carleson t-measure-probability merge-conflict WIP labelled WIP
25978 Bergschaf feat(Order/Sublocale): Open Sublocales t-order merge-conflict merge conflict
27003 eric-wieser chore: use `Simp.ResultQ` more often t-meta merge-conflict merge conflict
26374 joelriou feat(CategoryTheory): existence of right derived functors using derivability structures t-category-theory merge-conflict WIP labelled WIP
25483 VTrelat chore(Data/Set/Prod, SetTheory/ZFC/Basic): add theorem prod_subset_of_prod and extend ZFC model t-data new-contributor merge-conflict merge conflict
24754 urkud feat: define `pathIntegral` t-analysis merge-conflict awaiting-author merge conflict
28042 kckennylau feat(Topology/ValuativeRel): a topological basis indexed by pairs of elements merge-conflict ⚠️ merge conflict
25401 digama0 feat(Util): SuppressSorry option t-meta merge-conflict merge conflict
25822 ScottCarnahan WIP: experiments with vertex algebras large-import merge-conflict WIP labelled WIP
26394 winstonyin feat: existence of local flows on manifolds t-differential-geometry merge-conflict WIP labelled WIP
27835 edegeltje feat(Tactic): ring modulo a given characteristic migrated-from-branch large-import t-meta merge-conflict merge conflict
26446 joelriou refactor(CategoryTheory): make morphisms in full subcategories a 1-field structure t-category-theory merge-conflict WIP labelled WIP
28298 thorimur chore: dedent `to_additive` docstrings awaiting-zulip merge-conflict documentation awaiting a zulip discussion
27953 CoolRmal feat(ProbabilityTheory): Conditional Jensen's Inequality new-contributor t-measure-probability merge-conflict merge conflict
27759 plp127 chore(FreeAbelianGroup): deprecate multiplication large-import t-algebra merge-conflict failing CI
8102 miguelmarco feat(Tactic): add `unify_denoms` and `collect_signs` tactics new-contributor t-meta merge-conflict please-adopt modifies-tactic-syntax good first issue looking for help
14203 dagurtomas feat(Algebra/ModuleCat): descent data workshop-AIM-AG-2024 t-algebra t-algebraic-geometry t-category-theory merge-conflict WIP labelled WIP
26464 joelriou feat(LinearAlgebra): generators of pi tensor products file-removed t-algebra merge-conflict merge conflict
27446 grunweg chore: more enorm lemmas carleson merge-conflict WIP labelled WIP
27863 xroblot Development branch (1) merge-conflict WIP labelled WIP
14583 lecopivo fix: make concrete cycle notation local merge-conflict awaiting-author merge conflict
27819 BGuillemet feat(CategoryTheory/Yoneda): add curried version of Yoneda lemma for heterogeneous universes, and other version of homNatIso new-contributor t-category-theory merge-conflict awaiting-author merge conflict
28219 joelriou feat(CategoryTheory): monomorphisms in Type are stable under transfinite compositions file-removed t-category-theory merge-conflict WIP labelled WIP
11820 eric-wieser feat(Algebra/Star/Unitary): add unitarySubgroup t-algebra merge-conflict awaiting-author ❌? infrastructure-related CI failing
27207 pechersky feat(Topology/WithVal): ValuativeRel (WithVal v) t-algebra t-topology merge-conflict failing CI
27313 pechersky feat(RingTheory/ValuativeRel/Trivial): the trivial valuative relation t-algebra t-number-theory merge-conflict merge conflict
19097 Vierkantor chore(Algebra.Polynomial): split `Polynomial/Basic.lean` into smaller files t-algebra merge-conflict merge conflict
27465 erdOne feat: the definition of nonarchimedean local fields t-number-theory merge-conflict failing CI
27887 JovanGerb feat: `to_dual` attribute large-import t-meta merge-conflict merge conflict
26455 ScottCarnahan WIP - feat (LinearAlgebra/RootSystem): API for CartanMatrix t-algebra merge-conflict WIP labelled WIP
28622 alreadydone chore(Mathlib): replace `=>` by `↦` merge-conflict merge conflict
26396 xroblot feat(RingTheory): define the dual of a basis for the trace and prove basic properties t-ring-theory merge-conflict merge conflict
24793 tristan-f-r feat: trace of unitarily similar matrices t-algebra merge-conflict awaiting-author merge conflict
26039 tsuki8 feat(RingTheory/MvPolynomial/MonomialOrder): leadingTerm t-ring-theory new-contributor merge-conflict merge conflict
27599 mitchell-horner feat(Combinatorics/SimpleGraph): define `completeEquipartiteSubgraph` large-import t-combinatorics merge-conflict merge conflict
28311 eric-wieser fix(Tactic/NormNum): do not hang on large powers t-meta merge-conflict bug awaiting review
28532 alreadydone chore(Algebra/Ring/Defs): add two classes and extend more t-algebra merge-conflict awaiting review
28046 grunweg chore: golf the proof in #26875 t-differential-geometry merge-conflict blocked on another PR
21603 imbrem feat(CategoryTheory/ChosenFiniteProducts): add basic ChosenFiniteCoproducts class new-contributor t-category-theory merge-conflict awaiting-author merge conflict
28322 kim-em chore: remove a now-unneeded maxHeartbeats t-number-theory merge-conflict awaiting review
12879 grunweg feat: port ge_or_gt linter from mathlib3 tech debt t-linter merge-conflict blocked-by-other-PR blocked on another PR
13057 alreadydone feat(NumberTheory): characterize elliptic divisibility sequences t-algebra t-number-theory merge-conflict blocked-by-other-PR blocked on another PR
10842 mcdoll chore: simplify proofs using new positivity extensions and tests merge-conflict blocked-by-other-PR WIP blocked on another PR
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
8364 thorimur feat: `refine?` t-meta merge-conflict blocked-by-other-PR blocked on another PR
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
9154 astrainfinita 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
7861 shuxuezhuyi feat(Geometry/Hyperbolic/UpperHalfPlane): instance IsometricSMul PSL(2, ℝ) ℍ t-euclidean-geometry merge-conflict blocked-by-other-PR blocked on another PR
12087 JADekker feat : complete API for K-Lindelöf spaces t-topology merge-conflict please-adopt blocked-by-other-PR blocked on another PR
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
14242 js2357 feat: Prove equivalence of `isDedekindDomain` and `isDedekindDomainDvr` new-contributor t-algebra merge-conflict blocked-by-other-PR blocked on another PR
16215 adomasbaliuka feat(Tactic/Linter): lint unwanted unicode t-linter merge-conflict blocked-by-other-PR blocked on another PR
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
16041 vihdzp feat(SetTheory/Ordinal/Arithmetic): `Ordinal.toNat` t-set-theory t-logic awaiting-author blocked-by-other-PR WIP blocked on another PR
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
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
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
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
17593 astrainfinita chore(Algebra/Order/GroupWithZero/Unbundled): deprecate useless lemmas, use `ZeroLEOneClass` t-order t-algebra merge-conflict blocked-by-other-PR blocked on another PR
17624 astrainfinita feat(Algebra/Order/GroupWithZero/Unbundled): generalize lemmas t-order t-algebra merge-conflict blocked-by-other-PR blocked on another PR
17515 astrainfinita perf: do not need `simp low` now t-algebra merge-conflict blocked-by-other-PR blocked on another PR
19414 vihdzp feat: Nesbitt's inequality large-import t-algebra merge-conflict awaiting-author blocked-by-other-PR WIP blocked on another PR
18876 GabinKolly feat(ModelTheory/Fraisse): add proof that Fraïssé limits exist t-logic blocked-by-other-PR blocked on another PR
19281 Vierkantor chore(Algebra/{MonoidAlgebra,Polynomial}): algebra structure in `Basic.lean` t-algebra merge-conflict blocked-by-other-PR blocked on another PR
16391 vihdzp feat(SetTheory/Ordinal/NaturalOps): characterization of natural operations in base `ω` t-logic merge-conflict blocked-by-other-PR blocked on another PR
19621 Command-Master feat: Multiplicity and prime-adic valuation of derivations large-import t-algebra merge-conflict blocked-by-other-PR blocked on another PR
18262 joelriou feat(Algebra/Category/ModuleCat/Presheaf): exterior powers of presheaves of modules t-algebra t-category-theory merge-conflict blocked-by-other-PR WIP blocked on another PR
15269 kkytola feat: Add ENNReal.floor t-order t-algebra merge-conflict awaiting-author blocked-by-other-PR blocked on another PR
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
15720 znssong feat(SimpleGraph): The Bondy-Chvátal theorem new-contributor t-combinatorics merge-conflict blocked-by-other-PR blocked on another PR
12670 trivial1711 feat: completion of a nonarchimedean multiplicative group t-algebra t-topology merge-conflict blocked-by-other-PR blocked on another PR
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
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
20956 tomaz1502 feat(Computability/QueryComplexity/Sort.lean): Formalization of upper bound of queries for merge sort t-computability blocked-by-other-PR blocked on another PR
22233 pechersky feat(Algebra/Valued): `AdicExpansion.evalAt` t-topology blocked-by-other-PR blocked on another PR
22232 pechersky feat(Algebra/Valued): `AdicExpansion.apprUpto` t-topology blocked-by-other-PR blocked on another PR
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
17105 vihdzp feat(Data/List/RunLength): run-length encoding t-data merge-conflict blocked-by-other-PR blocked on another PR
16000 YaelDillies feat: Croot-Sisask Almost Periodicity t-analysis t-combinatorics blocked-by-other-PR blocked on another PR
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
20410 vihdzp refactor: redefine `Equiv.Set.sumCompl = Equiv.sumCompl` t-data awaiting-CI merge-conflict blocked-by-other-PR WIP 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
20222 eric-wieser feat: generalize lemmas about derivatives t-analysis merge-conflict blocked-by-other-PR blocked on another PR
21769 JovanGerb feat: extensible `push_neg` tactic large-import t-meta merge-conflict blocked-by-other-PR blocked on another PR
22319 sinhp feat(CategoryTheory): Locally Cartesian Closed Categories (Sections Right Adjoint) large-import t-category-theory merge-conflict blocked-by-other-PR blocked on another PR
22321 sinhp feat(CategoryTheory): Locally Cartesian Closed Categories (Definition) large-import t-category-theory merge-conflict blocked-by-other-PR blocked on another PR
19475 YaelDillies feat: group markings t-algebra blocked-by-other-PR WIP blocked on another PR
24010 grunweg feat(Counterexamples): a non-negative function, not a.e. zero, with vanishing lowe… t-measure-probability please-adopt blocked-by-other-PR WIP blocked on another PR
24016 plp127 feat: fine uniformity t-topology blocked-by-other-PR blocked on another PR
21238 joneugster feat(Cache): enable partial cache in downstream projects CI t-meta merge-conflict blocked-by-other-PR blocked on another PR
21842 joneugster refactor(Cache): use module name for file hash instead of non-resolved file path CI t-meta merge-conflict blocked-by-other-PR blocked on another PR
19467 quangvdao feat(MvPolynomial/Equiv): Add `MvPolynomial.finSuccEquivNth` t-algebra merge-conflict blocked-by-other-PR blocked on another PR
22547 joelriou feat(CategoryTheory/Abelian): construction of reduced left resolutions t-category-theory blocked-by-other-PR WIP blocked on another PR
22556 joelriou feat(Algebra/Category/ModuleCat): a functorial projective resolution t-category-theory blocked-by-other-PR blocked on another PR
24549 grunweg feat: define embedded submanifolds, attempt 1 t-differential-geometry merge-conflict blocked-by-other-PR WIP blocked on another PR
11003 thorimur chore: migrate to `tfae` block tactic t-meta merge-conflict blocked-by-other-PR WIP blocked on another PR
16186 joneugster chore: use emoji-variant-selector `\uFE0F` for emojis ✅️,❌️,💥️,🟡️ t-linter merge-conflict awaiting-author blocked-by-other-PR blocked on another PR
21853 smmercuri feat: the adele ring of a number field is locally compact large-import t-number-theory merge-conflict blocked-by-other-PR WIP blocked on another PR
15654 TpmKranz feat(Computability): language-preserving maps between NFA and RE awaiting-zulip t-computability new-contributor merge-conflict blocked-by-other-PR blocked on another PR
16553 grunweg WIP: tinkering with orientable manifolds t-differential-geometry blocked-by-other-PR WIP blocked on another PR
24550 grunweg feat: define `SliceModel` typeclass for models with corners for embedded submanifolds t-differential-geometry merge-conflict blocked-by-other-PR WIP blocked on another PR
18755 astrainfinita refactor: deprecate `LinearIsometryClass` t-algebra t-analysis merge-conflict blocked-by-other-PR blocked on another PR
5863 eric-wieser feat: add elaborators for concrete matrices t-meta blocked-by-other-PR help-wanted blocked on another PR
25737 robin-carlier feat(AlgebraicTopology/SimplexCategory/GeneratorsRelations/NormalForms): Normal forms for `P_δ`s large-import t-topology t-category-theory blocked-by-other-PR blocked on another PR
25912 BoltonBailey feat: add simp lemmas for trig functions on `π * 2⁻¹` t-analysis awaiting-author blocked-by-other-PR blocked on another PR
26108 xroblot feat(NumberField/IsCM): compute the index of the subgroup of real units large-import t-number-theory blocked-by-other-PR blocked on another PR
24434 joelriou feat(CategoryTheory): effectiveness of descent t-category-theory merge-conflict blocked-by-other-PR WIP blocked on another PR
18771 joelriou feat(LinearAlgebra/ExteriorPower): exterior powers of free modules are free t-algebra merge-conflict blocked-by-other-PR WIP blocked on another PR
25926 BoltonBailey feat: add lemma about `degreeOf_eq_degree` t-algebra blocked-by-other-PR blocked on another PR
20241 vasnesterov feat(Data/Seq): coinductive predicates for sequences t-data merge-conflict blocked-by-other-PR blocked on another PR
20051 Timeroot feat: `Clone` and some instances t-algebra awaiting-author blocked-by-other-PR blocked on another PR
18662 joelriou feat(LinearAlgebra/ExteriorPower): generators of the exterior powers t-algebra merge-conflict blocked-by-other-PR WIP blocked on another PR
18735 joelriou feat(Algebra/Module): presentation of the exterior power t-algebra merge-conflict blocked-by-other-PR WIP blocked on another PR
18551 joelriou feat(AlgebraicGeometry): the algebraic De Rham complex t-algebra t-algebraic-geometry merge-conflict blocked-by-other-PR WIP blocked on another PR
19582 yu-yama feat(GroupExtension/Abelian): define `OfMulDistribMulAction.equivH2` new-contributor t-algebra blocked-by-other-PR blocked on another PR
26720 vlad902 feat(SimpleGraph): lemmas relating edges and darts to the support t-combinatorics blocked-by-other-PR blocked on another PR
24411 joelriou feat(CategoryTheory): descent of morphisms for a pseudofunctor t-category-theory merge-conflict blocked-by-other-PR WIP blocked on another PR
25488 VTrelat feat(SetTheory/ZFC/Rationals): define rationals in ZFC new-contributor merge-conflict blocked-by-other-PR ⚠️ blocked on another PR
26096 vasnesterov feat(Topology/Instances): Cantor set is the set of ternary numbers without `1`s large-import t-topology merge-conflict blocked-by-other-PR blocked on another PR
26136 vasnesterov feat(Topology/Instances): Cantor set is homeomorphic to `ℕ → Bool` large-import t-topology merge-conflict blocked-by-other-PR blocked on another PR
26149 vasnesterov feat(Topology): continuous surjection from Cantor set to Hilbert cube large-import t-topology merge-conflict blocked-by-other-PR blocked on another PR
26184 vasnesterov feat(Topology): every compact metric space is image of Cantor set large-import t-topology merge-conflict blocked-by-other-PR blocked on another PR
26185 vasnesterov feat(Counterexamples): Peano curve large-import t-topology merge-conflict blocked-by-other-PR blocked on another PR
26395 winstonyin feat: $C^1$ vector fields on compact manifolds define global flows t-differential-geometry merge-conflict blocked-by-other-PR WIP blocked on another PR
26413 michaellee94 feat(Analysis/ODE/MaximalSolution): Existence of maximal solutions for ODE meeting Picard-Lindelöf conditions new-contributor t-analysis merge-conflict awaiting-author blocked-by-other-PR blocked on another PR
26465 joelriou feat(Algebra/Module): presentation of the `PiTensorProduct` file-removed t-algebra merge-conflict blocked-by-other-PR blocked on another PR
26467 joelriou feat(LinearAlgebra): the tensor product of a finite family of free modules is free file-removed t-algebra merge-conflict blocked-by-other-PR WIP blocked on another PR
26165 oliver-butterley feat(MeasureTheory.VectorMeasure): add lemma which shows that variation of a `ℝ≥0∞` VectorMeasure is equal to itself new-contributor t-measure-probability blocked-by-other-PR blocked on another PR
26168 oliver-butterley feat(MeasureTheory.VectorMeasure) : variation defined as a supremum is equal to variation defined using the Hahn-Jordan decomposition. new-contributor t-measure-probability blocked-by-other-PR blocked on another PR
26160 oliver-butterley feat(MeasureTheory.VectorMeasure): add several lemmas which characterize variation new-contributor t-measure-probability blocked-by-other-PR blocked on another PR
24912 YaelDillies feat: affine monoids toric t-algebra blocked-by-other-PR blocked on another PR
24627 pechersky feat(Topology/Algebra/Valued): `IsLinearTopology 𝒪[K] K` and `𝒪[K] 𝒪[K]` t-topology merge-conflict awaiting-author blocked-by-other-PR blocked on another PR
26871 grunweg feat: finite sum, difference, scalar product of differentiable sections is differentiable t-differential-geometry merge-conflict blocked-by-other-PR ❌? blocked on another PR
26908 robin-carlier feat(CategoryTheory/Monoidal/DayConvolution): alternative ext principle for unitors t-category-theory blocked-by-other-PR blocked on another PR
25900 pfaffelh feat (Topology/Compactness/CompactSystem): Set system of finite unions of sets in a compact system is again a compact system t-topology merge-conflict blocked-by-other-PR 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
27070 vasnesterov golf: use `order` large-import merge-conflict blocked-by-other-PR WIP blocked on another PR
26886 pechersky feat(NumberTheory/Padics/ValuativeRel): ValuativeRel ℚ_[p] t-algebra t-analysis t-number-theory merge-conflict blocked-by-other-PR WIP blocked on another PR
25324 eric-wieser feat: more functorial results about DFinsupp blocked-by-other-PR WIP ⚠️ blocked on another PR
26983 mans0954 feat(Order/LatticeElements): distributive, standard and neutral elements of a lattice t-order blocked-by-other-PR blocked on another PR
25834 Rida-Hamadani feat(SimpleGraph): girth-diameter inequality t-combinatorics blocked-by-other-PR WIP blocked on another PR
26973 peabrainiac feat(Geometry/Diffeology): diffeologies generated from sets of plots t-differential-geometry blocked-by-other-PR blocked on another PR
27258 JovanGerb Imo2020 q6 IMO blocked-by-other-PR blocked on another PR
27273 xroblot feat(IntermediateField/LinearDisjoint): Two fields are linearly disjoint iff they are disjoint in the Galois case t-algebra blocked-by-other-PR blocked on another PR
27274 peabrainiac feat(Geometry/Diffeology): continuous diffeologies & D-topology-lemmas t-differential-geometry blocked-by-other-PR blocked on another PR
25848 joelriou feat/refactor: redefinition of homology + derived categories large-import t-topology t-category-theory merge-conflict blocked-by-other-PR WIP blocked on another PR
27416 joelriou feat(Algebra/Homology): Ext modules t-algebra t-category-theory blocked-by-other-PR WIP blocked on another PR
19607 madvorak Block matrix totally unimodular merge-conflict blocked-by-other-PR WIP blocked on another PR
26987 joelriou chore: deprecating module LinearAlgebra.PiTensorProduct t-algebra merge-conflict blocked-by-other-PR WIP blocked on another PR
26104 xroblot feat(NumberField/IsCM): compute ratio of regulators large-import t-number-theory merge-conflict blocked-by-other-PR blocked on another PR
26872 faenuccio chore(RingTheory/Valuation/RankOne): modify the definition of Valuation.RankOne using its range rather than its codomain t-algebra merge-conflict blocked-by-other-PR WIP blocked on another PR
24668 robertmaxton42 feat(LinearAlgebra): add inductive principle for the free product of algebras t-algebra merge-conflict blocked-by-other-PR blocked on another PR
26820 robin-carlier feat(CategoryTheory/Monoidal/DayConvolution): `LawfulDayConvolutionMonoidalCategoryStruct` constructors t-category-theory blocked-by-other-PR blocked on another PR
26824 robin-carlier feat(CategoryTheory/Monoidal/DayConvolution): Day functors type synonym t-category-theory blocked-by-other-PR blocked on another PR
26890 robin-carlier feat(CategoryTheory/Monoidal/DayConvolution) : more API for `DayFunctor` t-category-theory blocked-by-other-PR blocked on another PR
26952 robin-carlier feat(CategoryTheory/DayConvolution): monoid objects internal to day convolutions t-category-theory blocked-by-other-PR blocked on another PR
27150 robin-carlier feat(CategoryTheory/Monoidal/DayConvolution): constructors for braided and symmetric structure on day convolutions monoidal categories t-category-theory blocked-by-other-PR blocked on another PR
27151 robin-carlier feat(CategoryTheory/Monoidal/DayConvolution): `C ⊛⥤ V` is braided/symmetric when `C` and `V` are braided/symmetric t-category-theory blocked-by-other-PR blocked on another PR
27175 robin-carlier feat(CategoryTheory/Monoidal/DayConvolution): `LawfulDayConvolutionMonoidalCategoryStruct.ι C V D` is monoidal when the target is `C ⊛⥤ V` t-category-theory blocked-by-other-PR blocked on another PR
27341 staroperator feat(LinearAlgebra/LinearIndependent): `linearIndependent_iffₒ` etc for canonically linearly ordered semiring t-algebra blocked-by-other-PR blocked on another PR
27025 grunweg feat: Gram-Schmidt procedure on smooth vector bundles yields smooth sections t-differential-geometry blocked-by-other-PR blocked on another PR
27694 grunweg feat: Gram-Schmidt orthonormalisation preserves continuity of sections t-differential-geometry blocked-by-other-PR blocked on another PR
26264 EtienneC30 feat: characteristic function on product space t-measure-probability merge-conflict blocked-by-other-PR blocked on another PR
26269 EtienneC30 feat: links between characteristic function and independence t-measure-probability merge-conflict blocked-by-other-PR blocked on another PR
10006 jstoobysmith feat(AlgebraicTopology): homotopy in quasicategories t-algebraic-topology new-contributor merge-conflict awaiting-author blocked-by-other-PR blocked on another PR
25740 robin-carlier feat(AlgebraicTopology/SimplexCategory/GeneratorsRelations): `SimplexCategoryGenRel.toSimplexCategory` is an equivalence t-algebraic-topology large-import blocked-by-other-PR blocked on another PR
25741 robin-carlier feat(AlgebraicTopology/SimplexCategory/SimplicialObject): definitions of simplicial objects by generators and relation t-algebraic-topology large-import t-category-theory blocked-by-other-PR blocked on another PR
26466 robin-carlier feat(AlgebraicTopology/SimplexCategory/Augmented): the canonical monoid object in the augmented simplex category t-algebraic-topology t-category-theory blocked-by-other-PR blocked on another PR
26399 ChrisHughes24 refactor(ModelTheory): tidy up proof of Ax-Grothendieck with definable functions t-logic blocked-by-other-PR blocked on another PR
27838 CBirkbeck feat(NumberTheory/LSeries/RiemannZeta): add tsum over ints lemma. t-number-theory blocked-by-other-PR blocked on another PR
27707 FLDutchmann feat(NumberTheory/SelbergSieve): define Selberg's weights and prove basic results. t-analysis t-number-theory blocked-by-other-PR blocked on another PR
27217 ctchou feat(Combinatorics/HypergraphRamsey): Ramsey's theorem for hypergraphs large-import new-contributor t-combinatorics blocked-by-other-PR blocked on another PR
27228 themathqueen feat: defining the inner product on tensor products t-algebra t-analysis blocked-by-other-PR blocked on another PR
26735 Raph-DG feat(AlgebraicGeometry): The codimension of a point of a scheme is equal to the krull dimension of the stalk t-algebraic-geometry merge-conflict blocked-by-other-PR blocked on another PR
26304 Raph-DG feat(AlgebraicGeometry): Definition of algebraic cycles t-algebraic-geometry RFC merge-conflict blocked-by-other-PR blocked on another PR
25486 VTrelat feat(SetTheory/ZFC/Integers): define integers in ZFC t-set-theory new-contributor merge-conflict blocked-by-other-PR blocked on another PR
25484 VTrelat feat(SetTheory/ZFC/Booleans): define Boolean algebra in ZFC t-set-theory new-contributor merge-conflict blocked-by-other-PR blocked on another PR
27510 chrisflav feat(RingTheory/Height): height of ideal is height of preimage plus height in quotient t-ring-theory large-import blocked-by-other-PR blocked on another PR
22059 grunweg feat: manifolds with smooth boundary t-differential-geometry merge-conflict blocked-by-other-PR WIP blocked on another PR
27119 robin-carlier feat(CategoryTheory/Monoidal/DayConvolution): constructors for closed monoidal day convolution monoidal structures t-category-theory blocked-by-other-PR blocked on another PR
27133 robin-carlier feat(CategoryTheory/Monoidal/DayConvolution): `C ⊛⥤ V` is monoidal closed when `V` is t-category-theory blocked-by-other-PR blocked on another PR
25143 chrisflav feat(RingTheory): smooth algebras have smooth Noetherian models t-ring-theory merge-conflict blocked-by-other-PR blocked on another PR
22909 AntoineChambert-Loir feat(RingTheory/Pure): pure submodules t-ring-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-ring-theory merge-conflict blocked-by-other-PR blocked on another PR
26051 Komyyy feat(Mathlib/GroupTheory/SpecificGroups/Alternating): A_n is simple iff n = 3 or 5 ≤ n t-group-theory large-import merge-conflict blocked-by-other-PR WIP blocked on another PR
27978 smmercuri feat: `InfinitePlace.Extension` API for extensions of infinite places. t-number-theory blocked-by-other-PR blocked on another PR
27971 smmercuri feat: weak approximation theorems for infinite places of a number field t-algebra t-number-theory blocked-by-other-PR blocked on another PR
27970 smmercuri feat: collections of distinct infinite places contain values that diverge around 1 large-import t-algebra t-number-theory blocked-by-other-PR blocked on another PR
26377 Whysoserioushah feat(Mathlib/RingTheory/SimpleRing/TensorProduct): Tensor product of a simple algebra and a central simple algebra is simple t-ring-theory merge-conflict blocked-by-other-PR blocked on another PR
27493 themathqueen feat(RingTheory/Coalgebra): define Frobenius algebra t-ring-theory blocked-by-other-PR ❌? blocked on another PR
23177 faenuccio feat: more lemmas about ordered groups with zero large-import t-order awaiting-CI blocked-by-other-PR WIP blocked on another PR
28001 daefigueroa feat(Dynamics): add results on topologically transitive flows new-contributor t-dynamics 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
26578 robin-carlier feat(CategoryTheory/Limits/Pullbacks/Categorical/CatCospanTransform): adjunctions of categorical cospans large-import t-category-theory blocked-by-other-PR blocked on another PR
26579 robin-carlier feat(CategoryTheory/Limits/Pullbacks/Categorical/CatCospanTransform): equivalences of categorical cospans large-import t-category-theory blocked-by-other-PR blocked on another PR
27214 robin-carlier feat(CategoryTheory/Limits/Shapes/Pullback/Categorical): Categorical pullback squares t-category-theory blocked-by-other-PR blocked on another PR
27391 robin-carlier feat(CategoryTheory/Limits/Shapes/Pullback/Categorical): pseudofunctoriality structure of categorical pullback squares t-category-theory blocked-by-other-PR blocked on another PR
27432 robin-carlier feat(CategoryTheory/Limits/Shapes/Pullback/Categorical): pseudofunctoriality of categorical pulback squares t-category-theory blocked-by-other-PR blocked on another PR
27481 robin-carlier feat(CategoryTheory/Limits/Shapes/Pullback/Categorical): adjunctions and equivalences of categorical pullback squares large-import t-category-theory blocked-by-other-PR blocked on another PR
27686 robin-carlier feat(CategoryTheory/Limits/Shapes/Pullback/Categorical/Square): more API for `CatPullbackSquare` large-import t-category-theory blocked-by-other-PR blocked on another PR
27688 robin-carlier feat(CategoryTheory/Limits/Shapes/Pullback/Categorical): coherence statement for `CatPullbackSquare.inverse` large-import t-category-theory blocked-by-other-PR blocked on another PR
27687 robin-carlier feat(CategoryTheory/Limits/Shapes/Pullback/Categorical): squares equivalent to a `CatPullbackSquare` large-import t-category-theory blocked-by-other-PR blocked on another PR
27689 robin-carlier feat(CategoryTheory/Limits/Shapes/Pullback/Categorical): horizontal pasting calculus for `CatPullbackSquare` large-import t-category-theory blocked-by-other-PR blocked on another PR
27690 robin-carlier feat(CategoryTheory/Limits/Shapes/Pullback/Categorical): vertical pasting calculus for `CatPullbackSquare` large-import t-category-theory blocked-by-other-PR blocked on another PR
27740 robin-carlier feat(CategoryTheory/Limits/Shapes/Pullback/Categorical): pasting calculus for `CategoricalPullback` large-import t-category-theory blocked-by-other-PR blocked on another PR
27982 ShreckYe chore(Data/Nat/GCD): use `Nat.Prime.dvd_or_dvd` from #27981 in `Nat.Prime.dvd_or_dvd_of_dvd_lcm` from #27963 to simplify the proof a bit large-import new-contributor blocked-by-other-PR blocked on another PR
25825 yuma-mizuno feat(CategoryTheory/Bicategory): define lax transformations between oplax functors large-import t-category-theory blocked-by-other-PR blocked on another PR
28061 CoolRmal feat(MeasureTheory): Uniqueness of Measures in the Riesz–Markov–Kakutani Representation Theorem new-contributor blocked-by-other-PR ⚠️ blocked on another PR
27969 smmercuri feat: collections of non-trivial and pairwise inequivalent absolute values contain values that diverge around 1 t-algebra t-number-theory blocked-by-other-PR blocked on another PR
26668 mariainesdff feat(Analysis/Normed/Unbundled/SpectralNorm): add API t-analysis t-number-theory merge-conflict blocked-by-other-PR blocked on another PR
28152 Sebi-Kumar feat(AlgebraicTopology): characterize simply connectedness in terms of loops t-algebraic-topology new-contributor blocked-by-other-PR blocked on another PR
27366 101damnations feat(RepresentationTheory/Homological/GroupCohomology/Hilbert90): add Hilbert 90 for cyclic groups large-import merge-conflict blocked-by-other-PR ⚠️ blocked on another PR
27314 pechersky feat(TopologyValued): `Valued` based on a range topology t-topology merge-conflict blocked-by-other-PR blocked on another PR
27364 101damnations feat(RepresentationTheory/Homological/GroupCohomology): cohomology of finite cyclic groups blocked-by-other-PR ⚠️ blocked on another PR
27365 101damnations feat(RepresentationTheory/Homological/GroupHomology): homology of finite cyclic groups blocked-by-other-PR ⚠️ blocked on another PR
28208 Sebi-Kumar feat(Topology): add the definition `foldTrans` to concatenate finite sequences of paths new-contributor t-topology blocked-by-other-PR blocked on another PR
26858 Thmoas-Guan feat(Algebra): Define the associated graded ring to filtered ring t-algebra blocked-by-other-PR blocked on another PR
26859 Thmoas-Guan feat(Algebra): Define associated graded algebra t-algebra blocked-by-other-PR blocked on another PR
26860 Thmoas-Guan feat(Algebra): Define associated graded module t-algebra blocked-by-other-PR blocked on another PR
26861 Thmoas-Guan feat(Algebra): define filtered add group hom t-algebra blocked-by-other-PR blocked on another PR
26862 Thmoas-Guan feat(Algebra): define filtered ring homomorphism t-algebra blocked-by-other-PR blocked on another PR
26867 Thmoas-Guan feat(Algebra): filtered module hom t-algebra blocked-by-other-PR blocked on another PR
26863 Thmoas-Guan feat(Algebra): define filtered alghom t-algebra blocked-by-other-PR blocked on another PR
26868 Thmoas-Guan feat(Algebra): associated graded exact of exact and strict t-algebra blocked-by-other-PR blocked on another PR
26869 Thmoas-Guan feat(Algebra): exact of associated graded exact t-algebra blocked-by-other-PR blocked on another PR
27100 staroperator feat(ModelTheory): Presburger definability and semilinear sets t-logic merge-conflict blocked-by-other-PR blocked on another PR
22771 alreadydone feat(Homotopy/Lifting): monodromy of covering maps and lifting criterion t-algebraic-topology blocked-by-other-PR blocked on another PR
28067 grunweg Docstring enumerations blocked-by-other-PR blocked on another PR
28244 robin-carlier feat(CategoryTheory/Bicategory/NaturalTransformation): Icons large-import t-category-theory awaiting-CI blocked-by-other-PR blocked on another PR
28245 robin-carlier feat(CategoryTheory/Bicategory/NaturalTransformation/Icon): strict associativity and unitality of icon composition large-import t-category-theory awaiting-CI blocked-by-other-PR blocked on another PR
28243 robin-carlier chore(CategoryTheory/Bicategory): move some `eqToHom` lemmas t-category-theory blocked-by-other-PR blocked on another PR
27626 EtienneC30 chore: turn covarianceBilin into a ContinuousBilinForm large-import t-measure-probability merge-conflict blocked-by-other-PR blocked on another PR
27675 EtienneC30 feat: introduce `covInnerBilin` large-import t-measure-probability merge-conflict blocked-by-other-PR blocked on another PR
28289 robin-carlier chore(CategoryTheory/Bicategory/Functor/Strict): generalize some results to op/lax functors large-import t-category-theory blocked-by-other-PR blocked on another PR
27645 bjornsolheim feat(Geometry/Convex/Cone): add pointed cone tensor products t-convex-geometry new-contributor blocked-by-other-PR blocked on another PR
28328 pechersky chore(Topology/Valued): golf using local finite order of WithZeroTopology large-import t-algebra t-topology t-number-theory blocked-by-other-PR blocked on another PR
23920 YaelDillies feat: relation-separated sets t-data blocked-by-other-PR blocked on another PR
23124 YaelDillies feat(MetricSpace): nets t-topology awaiting-CI blocked-by-other-PR blocked on another PR
28291 vasnesterov feat(Tactic): tactic for computing asymptotics of real functions t-analysis t-meta merge-conflict blocked-by-other-PR WIP blocked on another PR
26457 AntoineChambert-Loir feat(Mathlib/GroupTheory/Perm/MaximalSubgroups): maximal subgroups of the permutation group t-group-theory large-import blocked-by-other-PR blocked on another PR
23915 joelriou feat(CategoryTheory): deriving functors using a right derivability structure t-category-theory merge-conflict blocked-by-other-PR WIP blocked on another PR
28295 artie2000 feat(Algebra/Order/Ring/Ordering): basic results about ring (pre)orderings large-import blocked-by-other-PR ⚠️ blocked on another PR
27673 b-reinke feat(GroupTheory/FreeGroup): add cyclic reduction of words t-group-theory merge-conflict blocked-by-other-PR blocked on another PR
27678 b-reinke feat(GroupTheory/FreeGroup): reduction theorem for powers t-group-theory merge-conflict blocked-by-other-PR blocked on another PR
27679 b-reinke feat(GroupTheory/FreeGroup): add pow_left_inj t-group-theory merge-conflict blocked-by-other-PR blocked on another PR
27578 bjornsolheim feat(Geometry/Convex/Cone): add conical combinations and conical hull t-convex-geometry new-contributor blocked-by-other-PR blocked on another PR
27290 themathqueen feat: `Star`, `StarAddMonoid`, and `StarModule` instances for tensor products t-algebra blocked-by-other-PR blocked on another PR
27897 grunweg feat: check indentation of doc-strings t-linter awaiting-CI merge-conflict blocked-by-other-PR blocked on another PR
27996 grunweg feat: check indentation in doc-strings, medium version merge-conflict blocked-by-other-PR WIP ⚠️ blocked on another PR
28395 joelriou feat(AlgebraicTopology/SimplicialSet): nondegenerate simplices in the standard simplex t-algebraic-topology blocked-by-other-PR WIP blocked on another PR
23181 YaelDillies refactor(Topology/UniformSpace): use `SetRel` t-topology blocked-by-other-PR blocked on another PR
26942 pechersky feat(RingTheory/Valuation/ValueGroupIso): isomorphism of value groups when compatible t-ring-theory t-order blocked-by-other-PR blocked on another PR
27980 smmercuri feat: dimensions of completions at infinite place extensions large-import t-number-theory merge-conflict blocked-by-other-PR blocked on another PR
28392 joelriou feat(AlgebraicTopology/ModelCategory): relation between left and right homotopies t-algebraic-topology blocked-by-other-PR WIP blocked on another PR
27898 grunweg feat: check indentation of doc-strings, basic version t-linter blocked-by-other-PR blocked on another PR
7873 astrainfinita 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
28187 vihdzp feat: archimedean classes of rationals t-algebra blocked-by-other-PR blocked on another PR
27862 alreadydone chore(Algebra): generalize results on IsLocalization to Submonoid.LocalizationMap large-import t-algebra blocked-by-other-PR blocked on another PR
26985 agjftucker feat(Analysis/Calculus/Implicit): define implicitFunOfBivariate large-import new-contributor t-analysis blocked-by-other-PR blocked on another PR
25326 YaelDillies feat: `Mon_ C` is cartesian-monoidal if `C` is toric t-category-theory blocked-by-other-PR blocked on another PR
27508 chrisflav feat(RingTheory): height under ring homomorphism t-ring-theory large-import blocked-by-other-PR blocked on another PR
28246 Sebi-Kumar feat(AlgebraicTopology/FundamentalGroupoid): the n-sphere is simply connected for n > 1 t-algebraic-topology new-contributor blocked-by-other-PR blocked on another PR
27429 smorel394 feat(RepresentationTheory/FinGroupCharZero): applications of Maschke's theorem t-algebra blocked-by-other-PR blocked on another PR
27125 smorel394 feat(Algebra/Category/FGModuleCat/Abelian): `FGModuleCat k` is abelian if `k` is a noetherian ring t-algebra blocked-by-other-PR blocked on another PR
27134 smorel394 feat(RepresentationTheory/FDRep): The forgetful functor from `FDRep R G` to `Rep R G` preserves finite (co)limits t-algebra blocked-by-other-PR blocked on another PR
28530 nonisomorphiclinearmap feat(Combinatorics/SimplicialComplex/Topology): add standard simplices and geometric realisation (colimit + functoriality) new-contributor t-combinatorics blocked-by-other-PR blocked on another PR
28475 astrainfinita chore(Analysis/SpecificLimits/Basic): generalize lemmas t-analysis blocked-by-other-PR blocked on another PR
27152 xroblot feat(RingTheory/Ideal): prove transitivity for the relative norm t-ring-theory merge-conflict blocked-by-other-PR blocked on another PR
28224 joelriou feat(AlgebraicTopology): the type of non degenerate simplices of a simplicial set t-algebraic-topology merge-conflict blocked-by-other-PR WIP blocked on another PR
27668 IvanRenison feat(Analysis/InnerProductSpace): define outer product of linear maps t-analysis blocked-by-other-PR blocked on another PR
27821 BGuillemet feat(CategoryTheory/Sites/Sheaf): functorial version of Sheaf.homEquiv new-contributor t-category-theory merge-conflict blocked-by-other-PR blocked on another PR
28330 joelriou feat(AlgebraicTopology): the type of non degenerate simplices not in a given subcomplex t-algebraic-topology merge-conflict blocked-by-other-PR WIP blocked on another PR
28332 joelriou feat(AlgebraicTopology/SimplicialSet): pairings of non degenerate simplices, following Sean Moss t-algebraic-topology merge-conflict blocked-by-other-PR WIP blocked on another PR
28336 joelriou feat(AlgebraicTopology/SimplicialSet): a helper structure to construct pairings t-algebraic-topology merge-conflict blocked-by-other-PR WIP blocked on another PR
27557 chrisflav feat(RingTheory/KrullDimension): dimension of `R / (x)` for a nonzerodivisor t-ring-theory large-import merge-conflict blocked-by-other-PR blocked on another PR
27542 chrisflav feat(RingTheory/KrullDimension): dimension of polynomial ring t-ring-theory large-import merge-conflict blocked-by-other-PR blocked on another PR
28346 joelriou feat(AlgebraicTopology/SimplicialSet): rank functions for pairings t-algebraic-topology merge-conflict blocked-by-other-PR WIP blocked on another PR
28351 joelriou feat(AlgebraicTopology/SimplicialSet): the rank function with values in natural numbers of a regular pairing t-algebraic-topology merge-conflict blocked-by-other-PR WIP blocked on another PR
28462 joelriou feat(AlgebraicTopology/SimplicialSet): the relative cell complex attached to a rank function for a pairing t-algebraic-topology merge-conflict blocked-by-other-PR WIP blocked on another PR
27979 smmercuri feat: `RamifiedExtension` and `UnramifiedExtension` types for `InfinitePlace.Extension`s t-number-theory blocked-by-other-PR blocked on another PR
26218 Thmoas-Guan feat(Algebra): definition of cohen macaulay large-import t-algebra blocked-by-other-PR blocked on another PR
26245 Thmoas-Guan feat(Algebra): cohen macaulay local ring is catenary large-import t-algebra blocked-by-other-PR WIP blocked on another PR
26957 Thmoas-Guan feat(Algebra): unmixed thm of Cohen-Macaulay ring large-import t-algebra blocked-by-other-PR blocked on another PR
26212 Thmoas-Guan feat(Algebra): the Rees theorem for depth large-import t-algebra blocked-by-other-PR blocked on another PR
26213 Thmoas-Guan feat(Algebra): Ext iso quotient regular sequence large-import t-algebra blocked-by-other-PR blocked on another PR
26214 Thmoas-Guan feat(Algebra): definition of depth large-import t-algebra blocked-by-other-PR blocked on another PR
26215 Thmoas-Guan feat(Algebra): Auslander-Buchsbaum theorem large-import t-algebra blocked-by-other-PR blocked on another PR
26217 Thmoas-Guan feat(Algebra): Ischebeck theorem large-import t-algebra blocked-by-other-PR blocked on another PR
26216 Thmoas-Guan feat(Algebra): depth of QuotSMulTop large-import t-algebra blocked-by-other-PR blocked on another PR
25903 pfaffelh feat(MeasureTheory): finite unions of sets in a semi-ring (in terms of measure theory) form a ring large-import t-measure-probability blocked-by-other-PR blocked on another PR
28502 gilesgshaw feat(Logic/Basic): avoid unnecessary uses of choice new-contributor t-logic merge-conflict awaiting-author blocked-by-other-PR blocked on another PR
26831 AntoineChambert-Loir feat(GroupTheory/SpecificGroups/Alternating/MaximalSubgroups): maximal subgroups of the alternating group t-group-theory large-import blocked-by-other-PR blocked on another PR
27579 RemyDegenne feat: risk of an estimator, DeGroot statistical information, total variation distance t-measure-probability blocked-by-other-PR WIP blocked on another PR
27215 kckennylau feat(AlgebraicGeometry): Define the Zariski site on `CommRingCatᵒᵖ` t-algebraic-geometry blocked-by-other-PR blocked on another PR
26291 RemyDegenne feat(Probability): Fernique's theorem t-measure-probability blocked-by-other-PR WIP blocked on another PR
25273 YaelDillies refactor: make `MonoidAlgebra` into a one-field structure toric t-algebra blocked-by-other-PR WIP blocked on another PR
27270 EtienneC30 chore: turn WithLp into a structure large-import t-analysis blocked-by-other-PR blocked on another PR
26660 strihanje01 feat(Combinatorics/Additive/VerySmallDoubling): weak non-commutative Kneser's theorem large-import new-contributor t-combinatorics blocked-by-other-PR blocked on another PR
27706 xroblot feat(RingTheory/Localization/AtPrime): Add results about prime ideals in extension t-ring-theory file-removed merge-conflict blocked-by-other-PR WIP ❌? blocked on another PR
26651 loefflerd WIP: define cusps large-import t-number-theory blocked-by-other-PR WIP blocked on another PR
28554 themathqueen feat(Analysis/InnerProductSpace/Positive): `A.toMatrix.PosSemidef` iff `A.IsPositive` t-analysis blocked-by-other-PR blocked on another PR
28097 themathqueen feat(LinearAlgebra/Matrix/PosDef): kronecker of positive (semi-)definite matrices is positive (semi-)definite t-algebra blocked-by-other-PR blocked on another PR
27414 staroperator feat(ModelTheory): Semilinear sets in `ℕ ^ k` are closed under intersection and complement t-logic merge-conflict blocked-by-other-PR blocked on another PR
27789 staroperator feat(ModelTheory): semilinear sets are closed under intersection and set difference t-logic merge-conflict blocked-by-other-PR blocked on another PR
27353 themathqueen chore(LinearAlgebra/TensorProduct/Basic): semi-linearizing part 1 t-algebra merge-conflict blocked-by-other-PR blocked on another PR
27198 robin-carlier feat(CategoryTheory/Monoidal/DayConvolution): the Yoneda embedding is monoidal (for Day convolution) file-removed t-category-theory merge-conflict blocked-by-other-PR blocked on another PR
25841 mitchell-horner feat(Combinatorics/SimpleGraph): prove the Kővári–Sós–Turán theorem t-combinatorics blocked-by-other-PR blocked on another PR
23831 vasnesterov feat(Analysis): binomial series convergence t-analysis merge-conflict blocked-by-other-PR blocked on another PR
28689 mitchell-horner feat(Combinatorics/SimpleGraph): prove well-known corollaries of the Erdős-Stone-Simonovits theorem merge-conflict blocked-by-other-PR WIP ❌? ⚠️ blocked on another PR
28687 mitchell-horner feat(Combinatorics/SimpleGraph): prove the Erdős-Stone-Simonovits theorem merge-conflict blocked-by-other-PR WIP ⚠️ blocked on another PR
28686 mitchell-horner feat(Combinatorics/SimpleGraph): prove the Erdős-Stone theorem merge-conflict blocked-by-other-PR WIP ⚠️ blocked on another PR
26719 AntoineChambert-Loir feat(RingTheory/PolynomialLaw/Basic): extends polynomial laws to arbitrary universes t-ring-theory large-import blocked-by-other-PR blocked on another PR
28683 Thmoas-Guan feat(RingTheory) : regular local ring is domain t-ring-theory blocked-by-other-PR WIP blocked on another PR
28684 Thmoas-Guan feat(RingTheory) : definition of regular ring t-ring-theory blocked-by-other-PR WIP blocked on another PR
28499 yoh-tanimoto feat(MeasureTheory/VectorMeasure): add integral of a vector-valued function against a vector measure t-measure-probability blocked-by-other-PR blocked on another PR
28695 chrisflav feat(RingTheory): meta properties of bijective ring homomorphisms t-ring-theory large-import blocked-by-other-PR blocked on another PR
28699 chrisflav feat(RingTheory/Cotangent): cotangent of composition with localization away from an element t-ring-theory large-import blocked-by-other-PR blocked on another PR
28056 grunweg wip: existence of Riemannian metrics t-differential-geometry merge-conflict blocked-by-other-PR WIP blocked on another PR
28616 themathqueen feat(LinearAlgebra/Matrix/PosDef): positive (semi-)definite matrices commute iff their product is positive (semi-)definite t-algebra blocked-by-other-PR blocked on another PR
25906 pfaffelh feat (Topology/Compactness/CompactSystem): Closed and compact square cylinders form a compact system. t-topology blocked-by-other-PR blocked on another PR
28670 staroperator feat(GroupTheory/Finiteness): `Monoid.FG (∀ i, M i)` and `Group.FG (∀ i, M i)` blocked-by-other-PR 🟤 ⚠️ blocked on another PR
28685 mitchell-horner feat(Combinatorics/SimpleGraph): prove the minimal-degree version of the Erdős-Stone theorem blocked-by-other-PR WIP ⚠️ blocked on another PR
27342 staroperator feat(ModelTheory): define linear and semilinear sets t-logic blocked-by-other-PR blocked on another PR
27702 FLDutchmann feat(NumberTheory/SelbergSieve): define Lambda-squared sieves and prove important properties t-number-theory blocked-by-other-PR contradictory labels