Why is my PR not on the queue?

This page was last updated on: September 13, 2025 at 13:04 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
14444 digama0 fix(GeneralizeProofs): unreachable! bug t-meta awaiting-author awaiting author
14345 digama0 feat: the Dialectica category is monoidal closed t-category-theory awaiting-author awaiting author
12452 JADekker feat(Cocardinal) : add some more api t-topology awaiting-CI does not pass CI
10998 hmonroe feat(Logic): Arithmetization of partial recursive functions (toward Gödel's first incompleteness theorem) t-logic awaiting-author awaiting author
10099 mcdoll feat: Integration by parts for higher dimensional spaces t-measure-probability t-analysis WIP labelled WIP
9352 chenyili0818 feat: arithmetic lemmas for `gradient` t-analysis awaiting-author awaiting author
9469 dupuisf feat: maximum modulus principle for functions vanishing at infinity t-analysis awaiting-author awaiting author
9510 eric-wieser feat(Analysis/Calculus/DualNumber): Extending differentiable functions to dual numbers t-algebra t-analysis awaiting-CI WIP labelled WIP
6859 MohanadAhmed TryLean4Bundle: Windows Bundle Creator CI WIP help-wanted looking for help
7125 eric-wieser feat: additive monoid structure via biproducts t-category-theory awaiting-CI WIP labelled WIP
5745 alexjbest feat: a tactic to consume type annotations, and make constructor nicer t-meta awaiting-author awaiting author
15224 AnthonyBordg feat(CategoryTheory/Sites): covering families and their associated Grothendieck topology new-contributor t-category-theory awaiting-author awaiting author
14563 awueth feat: if-then-else of exclusive or statement new-contributor t-algebra awaiting-author awaiting author
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
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
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
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
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
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
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
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
23929 meithecatte feat(Computability/NFA): improve bound on pumping lemma awaiting-zulip t-computability new-contributor awaiting a zulip discussion
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
24540 robertmaxton42 feat(Quiv): add the empty, vertex, point, interval, and walking quivers t-category-theory awaiting-author failing CI
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
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
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
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
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
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
20784 eric-wieser fix: prevent `exact?` recursing forever on `n = 55` t-set-theory failing CI
26449 faenuccio feat(NumberTheory/LocalFields/Basic): provide the definition of (valued) Local Field t-algebra t-number-theory WIP labelled WIP
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
27069 FrankieNC feat(Analysis/MetricSpace/HausdorffDimension): prove dimH of intervals and segments is 1 new-contributor t-topology awaiting-author awaiting author
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
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
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
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
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
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
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
27756 grunweg feat: `Weak(Pseudo)EMetricSpace`, generalises `(Pseudo)EMetricSpace` carleson t-topology WIP labelled WIP
27066 vasnesterov feat(Tactic/Order): frontend for `order` t-meta awaiting review
25989 Multramate feat(NumberTheory/EllipticDivisibilitySequence): add elliptic nets t-number-theory awaiting-author awaiting author
27813 javra feat: IMO 2025 Q1 IMO WIP labelled WIP
22366 kim-em feat: `check_equalities` tactic for diagnosing defeq problems t-meta delegated 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
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
25758 YaelDillies chore: shortcut instance `CompleteLattice α → PartialOrder α` t-order awaiting review
27050 BoltonBailey doc(Control/Monad/Cont): add docstrings t-data awaiting-author failing CI
25916 BoltonBailey feat: add `simp` lemma `coeff_eq_zero_of_not_mem_support` t-algebra awaiting-author failing CI
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
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
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
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
26158 upobir feat(NumberTheory/Divisors): add int divisors t-number-theory awaiting-author awaiting author
26154 ADedecker refactor: add refactored APIs for algebraic filter bases t-topology awaiting review
27108 pechersky chore(RingTheory/AdicValuation): golf using WithZero.log t-algebra 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
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
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
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
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
22043 YaelDillies chore: shortcut instance for `Neg ℤˣ` file-removed t-algebra 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
26679 robin-carlier feat(CategoryTheory/Limits/Shapes/Pullback/Categorical): 2-functoriality of `CatCommSqOver` t-category-theory awaiting review
28032 grunweg feat: support Partial{Homeomorph,Equiv} in differential geometry elaborators t-differential-geometry failing CI
23669 erdOne feat(FieldTheory): abelian extensions t-algebra delegated delegated
26770 Jun2M feat(Combinatorics/Graph) : subgraph relations and operations on `Graph` t-combinatorics awaiting review
28074 grunweg Isbilinearmap WIP labelled WIP
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
26765 KiringYJ feat(MeasureTheory/PiSystem): add π-λ theorem and SetLike instance new-contributor t-measure-probability awaiting review
27534 PierreQuinton feat: a typeclass for `sSup`/`sInf` to be lawful t-order awaiting review
28111 euprunin chore: remove tactic `simp_lex` and use `simp` instead t-data awaiting review
28075 tristan-f-r chore(Finsupp/Indicator): make non-classical t-data easy awaiting-author awaiting author
25779 robin-carlier feat(CategoryTheory/Bicategory/NaturalTransformations): strong and lax natural transformations of lax functors t-category-theory awaiting review
27664 pechersky feat(Topology,Analysis): discrete topology metric space and normed groups t-topology awaiting review
26667 mariainesdff feat(FieldTheory/SplittingField/IsSplittingField): add IsScalarTower.splits, IsScalarTower.isAlgebraic t-algebra awaiting-author awaiting author
23758 erdOne feat(Topology/Algebra): linearly topologized iff non-archimedean large-import t-algebra t-topology awaiting-author awaiting author
28119 JasperMS feat(Data/Set/Pairwise): prove pairwise results for Chains, move `Set.pairwise_iUnion₂` carleson t-data new-contributor 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
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
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
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
26547 robin-carlier feat(CategoryTheory/Limits/Shapes/Pullback/Categorical/CatCospanTransform): more lemmas about isomorphisms of `CatCospanTransform` t-category-theory awaiting review
27000 gasparattila feat(Analysis/Normed/Group/Quotient): isometric versions of isomorphisms large-import new-contributor t-analysis 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
25480 ocfnash feat: define a concrete model of the `𝔤₂` root system large-import t-algebra WIP labelled WIP
22300 chrisflav feat(RingTheory/GoingDown): lift `LTSeries` of primes t-ring-theory awaiting review
27552 Equilibris refactor: make universe levels visible in typevec t-data new-contributor easy 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
27934 JasperMS feat(Order): no basic lemmas and some SuccOrder `biUnion` lemmas carleson new-contributor t-order awaiting review
21031 YaelDillies chore: get rid of generic hom coercions WIP labelled WIP
25680 kim-em chore: remove some `Nat` shortcut instances failing CI
24184 YaelDillies feat: `[G : H]` notation for the index of `H : Subgroup G` t-algebra RFC awaiting review
27754 Parcly-Taxel feat: `finCycle` as iterated `finRotate` t-logic awaiting review
28057 plp127 feat(SuccOrder): simp lemma to refold `Order.succ` and `Order.pred` t-order awaiting review
27024 grunweg feat: Gram-Schmidt orthonormalisation for sections of a vector bundle t-differential-geometry awaiting-author awaiting author
27946 plp127 refactor: have `MetrizableSpace` not depend on `MetricSpace` t-topology awaiting review
26125 faenuccio first commit dependency-bump WIP labelled WIP
26489 chrisflav refactor(RingTheory/RingHom): factor out proofs for `Algebra.FinitePresentation` t-algebra awaiting review
27974 smmercuri feat: `Field`, `FiniteDimensional` and `Algebra.IsSeparable` instances for `WithAbs` large-import t-analysis awaiting-author awaiting author
28512 euprunin chore(Data/List): golf entire `getLast_append_of_right_ne_nil` and `finRange_map_getElem` t-data awaiting review
27196 YaelDillies refactor(Polynomial/Bivariate): swap `X` and `Y` for improved notation toric t-algebra WIP labelled WIP
26107 xroblot feat(NumberField/IsCM): first results about the action of `complexConjugation` on units t-number-theory awaiting review
28141 YaelDillies chore: deprecate `BialgHom.coe_toLinearMap` t-ring-theory toric easy 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
28527 grunweg feat: add ContMDiff.congr t-differential-geometry easy 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
28557 ShreckYe feat(Data/Nat/Factorization): some results on equality of powers of naturals proved from factorization t-data awaiting review
28198 Sebi-Kumar feat(Analysis/InnerProductSpace/PiL2): Add instances for EuclideanSpace rank and EuclideanSpace being infinite new-contributor t-analysis awaiting review
28580 kmill refactor: simplify implementation of `filter_upwards` t-order t-meta failing CI
27302 tristan-f-r feat(Fintype/Quotient): finLiftOn₂ t-data failing CI
5897 eric-wieser feat: add a `MonadError` instance for `ContT` t-meta awaiting-author awaiting author
23881 YaelDillies feat: `ℝ≥0`-valued Lᵖ norm t-measure-probability awaiting-author awaiting author
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
25692 Whysoserioushah feat(RingTheory/MatrixAlgebra): add a more general version of `matrixEquivTensor` t-ring-theory awaiting-author awaiting author
28631 faenuccio feat(Data\Nat\ModEq.lean): add grind attribute to ModEq t-data WIP labelled WIP
26329 Timeroot feat: Definition of `Clone` notations and typeclasses t-algebra awaiting-CI awaiting-author does not pass CI
28581 bennett-chow fix: riemmanian -> riemannian new-contributor t-differential-geometry awaiting-author awaiting author
25070 erdOne feat(EllipticCurve): rational points on singular cuspidal cubics t-algebraic-geometry awaiting-author awaiting author
27752 plp127 feat(Order): `NoBotOrder α` implies `NoMinOrder α` under `IsDirected α (· ≥ ·)` t-order awaiting-author failing CI
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
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
28680 vihdzp feat: set has cardinality one iff singleton t-set-theory easy awaiting-author awaiting author
27443 yuanyi-350 Stacks tags t-algebra WIP labelled WIP
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 labelled WIP
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
26243 DavidLedvinka feat(Topology): Add PairReduction.lean t-topology awaiting-author awaiting author
26829 pechersky feat(RingTheory/Valuation): Valuation.leAddSubgroup and ideal/submodule versions of ltAddSubgroup t-ring-theory awaiting review
28352 agjftucker feat(Analysis): add three little theorems relating argument to image t-analysis awaiting review
26777 YaelDillies chore(Data/Set/Image): move `BooleanAlgebra` material to `Order` large-import t-data WIP labelled WIP
26428 Ruben-VandeVelde feat: norm_num support for Int.fract t-data t-meta awaiting review
26396 xroblot feat(RingTheory): define the dual of a basis for the trace and prove basic properties t-ring-theory awaiting review
26975 Whysoserioushah feat: a norm_num extension for complex numbers t-meta awaiting review
26078 kckennylau feat(AlgebraicGeometry): add x, y, px, py for points on elliptic curves t-algebraic-geometry awaiting-author awaiting author
26332 Timeroot feat(ModelTheory/Definability): TermDefinable functions large-import t-logic awaiting review
28432 euprunin chore(CategoryTheory/Monoidal): golf entire `counitInv_app_comp_functor_map_η_inverse` t-category-theory awaiting review
27937 madvorak feat(Logic/Basic): `congr_heq₂` t-logic awaiting-author awaiting author
28718 imbrem Added chosen finite coproducts new-contributor t-category-theory awaiting-author failing CI
26870 grunweg feat: mdifferentiableOn_section_of_mem_baseSet₀ t-differential-geometry awaiting review
28422 euprunin chore(Data/Fin): deprecate `Fin.mul_one'` (duplicate) t-data awaiting-author awaiting author
26267 vasnesterov feat(Analysis/Calculus): Taylor series converges to function on whole ball t-analysis awaiting review
28242 robin-carlier feat(CategoryTheory/Bicategory): EqToHom for bicategories t-category-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
28378 euprunin chore(Algebra): golf entire `eq_lift_comp_mkRingHom` and `eq_liftAlgHom_comp_mkAlgHom` t-algebra awaiting review
28399 Ruben-VandeVelde feat: ring-theoretic fractions in Rat t-ring-theory awaiting review
28473 EtienneC30 feat: toLp and ofLp are analytic t-analysis awaiting review
27990 kckennylau feat(Counterexamples): a nontrivial valuation with discrete topology t-ring-theory awaiting review
24612 Paul-Lez feat(Tactic/ImportDiff): add `#import_diff` command will-close-soon t-meta awaiting-author awaiting author
28812 yury-harmonic feat(PNat/Factors): add attrs and lemmas t-data new-contributor awaiting review
27245 rirarika feat: multivariate polynomial ring properties about irreducibility new-contributor t-algebra awaiting review
27479 iu-isgood feat: Abel's Binomial Theorem t-data new-contributor awaiting-author failing CI
25907 mans0954 feat: low order roots of unity t-algebra awaiting review
25700 grunweg feat: lint upon uses of the `mono` tactic t-linter RFC please-adopt looking for help
28215 5hv5hvnk Draft PR, for Strong and Weak connectivity for Digraphs new-contributor t-combinatorics awaiting-author failing CI
28195 gasparattila feat: separating a convex compact set and its neighborhood with a polytope new-contributor t-analysis awaiting review
28439 euprunin chore(LinearAlgebra/Matrix/Determinant): golf entire `det_eq_zero_of_not_linearIndependent_rows` t-algebra awaiting review
28531 Ruben-VandeVelde chore: remove Cardinal imports from Topology.Algebra.InfiniteSum.Group awaiting review
28766 yury-harmonic feat(Nat/Factorial): add tail-recursive versions t-data new-contributor awaiting review
28837 yury-harmonic feat(ValMinAbs): add lemmas t-data awaiting review
27965 grunweg feat: verify that file names contain no forbidden characters file-removed t-linter maintainer-merge awaiting review
28604 alreadydone chore(Algebra/Ring/Defs): add two classes (minimally invasive version) t-algebra WIP labelled WIP
28868 yury-harmonic feat(Positive): add `OfNat` instance large-import t-algebra failing CI
27357 jcreedcmu feat(Algebra/Module/Submodule): add `submoduleMap` for isometries new-contributor t-algebra awaiting review
28884 kim-em chore: deprecate ShiftLeft Int instance t-data awaiting review
27944 grunweg feat: lint module names with a period t-linter awaiting review
28132 dupuisf feat: preliminary `grind` tags for `IsUnit` t-algebra awaiting review
28325 pechersky feat(WithZeroTopology): `locallyCompactSpace_iff_locallyFiniteOrder_units` large-import t-order t-topology awaiting review
27207 pechersky feat(Topology/WithVal): ValuativeRel (WithVal v) t-algebra t-topology awaiting review
26988 YaelDillies feat(Rel): more API t-data awaiting review
24333 xcloudyunx feat(Combinatorics/SimpleGraph): cycle graph implementation for generic vertex types new-contributor t-combinatorics awaiting-author awaiting author
27963 ShreckYe feat(Algebra/GCDMonoid): add some theorems related to divisibility and `lcm` for both `GCDMonoid` and `Nat` new-contributor t-algebra awaiting review
28376 euprunin chore(Analysis/Calculus/Deriv): golf entire `differentiableAt_comp_const_add` t-analysis awaiting-author awaiting author
23835 chrisflav feat(Topology): cardinality of connected components is bounded by cardinality of fiber t-topology awaiting review
27824 ChrisHughes24 feat(Calculus): exists_gt_of_deriv_pos and variants t-analysis 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
28489 joelriou feat(CategoryTheory): weaken assumptions for the stability of the left lifting property under transfinite compositions t-category-theory awaiting review
27155 Pjotr5 feat: Shearer's bound on the independence number of triangle free graphs new-contributor t-combinatorics awaiting-author failing CI
28445 mitchell-horner feat: `one_sub_one_div_cast_*` theorems t-data t-algebra t-number-theory awaiting review
24719 madvorak feat(LinearAlgebra/Matrix/NonsingularInverse): inverting `Matrix` inverts its `LinearEquiv` t-algebra awaiting-author awaiting author
28149 Equilibris feat: dcongr_heq new-contributor t-logic awaiting review
28350 themathqueen feat(Algebra/Module/LinearMap): `range (f.smulRight x) = span {x}` t-algebra awaiting review
27242 hugh-fox feat: add Gauss-like formula for sums of digit sums large-import t-data new-contributor awaiting-author awaiting author
27047 YaelDillies feat: `MonoidHom.toAdditive''` as a `MulEquiv` toric t-algebra awaiting review
26961 mariainesdff feat(RingTheory/PowerSeries/Substitution): add API t-ring-theory awaiting-author awaiting author
28925 grunweg chore: remove `linear_combination'` tactic file-removed awaiting-zulip awaiting a zulip discussion
25292 YaelDillies feat: the `ConvexCone` generated by a set t-convex-geometry toric awaiting review
28768 yury-harmonic feat(Data/Nat): define `Nat.nthRoot` t-data new-contributor awaiting review
27992 staroperator feat(Algebra): cancellation inheritance t-algebra awaiting review
26088 grunweg chore(Linter/DirectoryDependency): move forbidden directories into a JSON file t-linter failing CI
25225 xcloudyunx feat(Combinatorics/SimpleGraph): Eulerian walk in connected graph contains all vertices new-contributor t-combinatorics awaiting review
27261 Sebi-Kumar feat(Topology): add definition for subpaths new-contributor t-topology awaiting-author awaiting author
26644 kckennylau feat(SetTheory/ZFC): Define the language of sets and state the ZFC axioms t-set-theory awaiting-author awaiting author
26914 quangvdao feat(Data/PFunctor/Univariate): more definitions for univariate `PFunctor` t-data awaiting review
26648 eric-wieser chore(TensorProduct): remove more `suppress_compilation`s t-algebra blocked-by-core-PR blocked on another PR
23238 YaelDillies feat: extended floor and ceil t-algebra awaiting review
25804 erdOne feat: `∑ z ∈ L, ‖z - x‖⁻ʳ` converges for lattices `L` t-analysis awaiting-author awaiting author
28056 grunweg wip: existence of Riemannian metrics t-differential-geometry WIP labelled WIP
26885 pechersky feat(Topology/ValuativeRel): ValuativeTopology 𝒪[K] t-algebra t-topology t-number-theory awaiting review
27163 pechersky feat(Topology/ValuativeRel): of and to basis of compatible valuations t-algebra t-topology t-number-theory awaiting review
28490 euprunin chore: golf entire `epi_of_cokernel_π_eq_zero`, `bottom_row_coprime`, `congr_of_eventuallyEq` and `Invertible.congr` awaiting review
22662 plp127 feat: Localization.Away.lift (computably) t-algebra awaiting review
24373 YaelDillies refactor: golf `modularCharacter` t-measure-probability awaiting-CI does not pass CI
24383 YaelDillies feat: distributive Haar characters of `ℝ` and `ℂ` file-removed FLT t-measure-probability awaiting-CI WIP labelled WIP
29010 grunweg chore: more tests for field_simp features and edge cases failing CI
16041 vihdzp feat(SetTheory/Ordinal/Arithmetic): `Ordinal.toNat` t-set-theory t-logic awaiting-author WIP labelled WIP
29055 vihdzp feat: `Ordinal.toENat` t-set-theory awaiting review
29047 grunweg chore(1000.yaml): add Fourier's theorem delegated delegated
29033 faenuccio feat (???): a linear map is surjective iff its image contains a ball t-analysis WIP labelled WIP
28630 Antidite feat(Archive/Imo): right isosceles configuration in the complex plane IMO new-contributor awaiting review
25500 eric-wieser feat: delaborators for metadata large-import t-meta delegated awaiting-author awaiting author
27392 Paul-Lez feat(Tactic/SimpUtils): add simproc finding commands t-meta awaiting review
28441 euprunin chore(GroupTheory/Perm): golf entire `mem_of_formPerm_ne_self` t-group-theory awaiting-author awaiting author
28492 euprunin chore(Data/Finite): golf entire `card_le_of_injective`, `card_le_of_surjective` and `card_sum` t-data awaiting-author awaiting author
28488 euprunin chore(SetTheory): golf entire `cast_succ`, `mk_multiset_of_countable` and `iSup_succ` t-set-theory awaiting-author awaiting author
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
28316 eric-wieser feat(Tactic/NormNum): better trace nodes t-meta failing CI
29072 yury-harmonic feat({Nat,Int}/ModEq): add lemmas t-data awaiting-zulip awaiting a zulip discussion
28669 kckennylau chore: clean up some proofs about locally compact valuation t-ring-theory awaiting-author awaiting author
25069 erdOne feat(EllipticCurve): rational points of singular nodal cubics t-algebraic-geometry awaiting-author awaiting author
26484 peabrainiac feat(Geometry/Diffeology): basics of diffeological spaces t-differential-geometry awaiting review
26240 grunweg perf(CommandLinterLinter): use Substring more t-linter RFC awaiting review
26299 adomani perf: the `commandStart` linter only acts on modified files t-linter awaiting-author awaiting author
25743 robin-carlier feat(AlgebraicTopology/SimplexCategory/Augmented): monoidal structure on `AugmentedSimplexCategory` t-algebraic-topology t-category-theory awaiting review
28474 astrainfinita feat: add `ContinuousSMul` instances for `ℚ≥0` bench-after-CI t-algebra t-topology awaiting-author awaiting review
27516 gaetanserre feat: add rational approximation lemma for suprema in `unitInterval` t-topology awaiting review
27468 IvanRenison feat(Combinatorics/SimpleGraph): add theorem `SimpleGraph.Connected.diff_dist_adj` t-combinatorics awaiting review
27461 IvanRenison feat(Combinatorics/SimpleGraph/Paths): add lemma `SimpleGraph.Walk.IsPath.mem_support_iff_exists_append` t-combinatorics awaiting review
26913 Paul-Lez feat(NumberTheory/{*}): add a few lemmas about number field and cyclotomic extensions t-algebra t-number-theory awaiting-CI WIP labelled WIP
27433 YaelDillies refactor: make `⇑e⁻¹ = e.symm` simp awaiting review
27672 b-reinke feat(GroupTheory/FreeGroup): add definition of cyclically reduced words t-group-theory awaiting review
28560 euprunin chore(Combinatorics/Quiver): golf entire `lift_spec` using `rfl` t-combinatorics awaiting review
28574 euprunin chore(Topology/Category): golf entire `finiteCoproduct.ι_desc_apply`, `piIsoPi_hom_apply`, `prodIsoProd_hom_apply` and `pullbackIsoProdSubtype_hom_apply` using `tauto` and `rfl` t-topology awaiting review
28699 chrisflav feat(RingTheory/Cotangent): cotangent of composition with localization away from an element t-ring-theory large-import awaiting review
28772 chrisflav feat(RingTheory/IsTensorProduct): add `IsPushout.cancelBaseChange` t-ring-theory awaiting review
29089 hrmacbeth feat: field tactic t-meta 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-author awaiting author
26455 ScottCarnahan WIP - feat (LinearAlgebra/RootSystem): API for CartanMatrix t-algebra WIP labelled WIP
29014 ShreckYe feat(Data/List/Scan): some theorems that relate `scanl` with `foldl` t-data awaiting review
28891 joelriou feat(Analysis/Convex): functoriality of the standard simplex t-convex-geometry awaiting review
29145 JovanGerb chore: use `to_additive` in more places failing CI
25899 pfaffelh feat(Topology/Compactness/CompactSystem): introduce compact Systems t-topology awaiting review
25902 pfaffelh feat: The finite product of semi-rings (in terms of measure theory) is a semi-ring. large-import t-measure-probability awaiting review
28390 euprunin chore(Analysis/LocallyConvex): golf entire `polar_weak_closed` t-analysis awaiting-author awaiting author
28343 RemyDegenne feat(Probability): Fernique's theorem for distributions that are invariant by rotation t-measure-probability awaiting review
26843 vasnesterov feat(Tactic/Simproc): nested quantifiers in `existsAndEq` migrated-from-branch large-import t-meta awaiting review
26156 oliver-butterley feat(MeasureTheory.VectorMeasure) : add a definition of total variation for VectorMeasure new-contributor t-measure-probability awaiting-author failing CI
28676 sun123zxy feat(NumberTheory/ArithmeticFunction): wrap `Nat.totient` as an `ArithmeticFunction` large-import new-contributor t-number-theory awaiting review
29186 winstonyin feat: IsIntegralCurve for solutions to ODEs t-dynamics t-analysis t-differential-geometry failing CI
25856 MichaelStollBayreuth perf(Data.Real.Sqrt): make Real.sqrt irreducible migrated-from-branch t-data awaiting review
25883 pfaffelh feat: introduce Gram matrices migrated-from-branch new-contributor t-analysis awaiting review
28296 strihanje01 feat(Combinatorics/Additive/VerySmallDoubling): Hamidoune's Freiman-Kneser theorem for nonabelian groups large-import new-contributor t-combinatorics awaiting review
28555 YaelDillies feat: pullback along an epi preserved under pullbacks is faithful toric large-import t-category-theory awaiting review
28691 or4nge19 feat(Probability/Invariance):Reversibility/DetailedBalance new-contributor t-measure-probability awaiting review
25920 BoltonBailey feat(Data/Finsupp/Basic): `Finsupp.optionElim'` migrated-from-branch t-data awaiting review
26841 xroblot feat(FieldTheory/IsGalois): map induced by the restriction to a subfield t-algebra awaiting review
25969 101damnations feat(RepresentationTheory/Homological/GroupHomology/Functoriality): the degree 1 part of the corestriction-coinflation exact sequence t-algebra awaiting-author awaiting author
22231 pechersky feat(Algebra/Valued): `AdicExpansion` initial defns t-algebra t-topology awaiting-author awaiting author
29151 yuanyi-350 feat: Corollary of Hahn-Banach theorem large-import ⚠️ awaiting review
27363 101damnations feat(RepresentationTheory/Homological): add standard resolution for finite cyclic groups t-algebra delegated delegated
28452 plp127 feat: Define `ZMod.fintype` without cases t-data awaiting review
24829 urkud fix(Topology/Homotopy): fix name&args order of `comp` t-topology delegated delegated
28234 alreadydone chore(AlgebraicTopology): clean up FundamentalGroupoid t-algebraic-topology awaiting-author awaiting author
28321 kim-em chore: make OmegaCompletePartialOrder a mixin awaiting-author awaiting author
29147 ocfnash feat: miscellaneous root system lemmas t-algebra WIP labelled WIP
28702 Timeroot feat(Algebra/Group/Hom/Defs): MonoidHom switching from MulOneClass to MulOne bench-after-CI t-algebra awaiting review
26710 metakunt feat (Data/Nat/Digits/Lemmas): Add digits_getD t-data new-contributor awaiting-author failing CI
28070 grunweg style: improve indentation of multi-linear enumerations in doc-strings failing CI
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 t-algebra awaiting review
28602 gmcninch-tufts feat(Algebra/Polynomial/Module): prove equivalence of a certain tensor product with PolynomialModule new-contributor t-algebra awaiting review
23992 robertmaxton42 feat (Limits.FunctorCategory): limitIsoFlipCompLim and colimitIsoFlipCompColim are natural new-contributor t-category-theory awaiting-CI does not pass CI
28934 yury-harmonic feat(NormNum): add extensions for `Even` and `Odd` maintainer-merge t-meta awaiting-author awaiting author
29231 kim-em chore: deprecate PartENat t-data awaiting review
19860 YaelDillies refactor: review the `simps` projections of `OneHom`, `MulHom`, `MonoidHom` t-algebra WIP labelled WIP
27500 Komyyy feat: the Riemann zeta function is meromorphic large-import t-analysis WIP labelled WIP
26284 plp127 feat: faster implementation of `Nat.primeFactorsList` + `@[csimp]` lemma t-data awaiting review
25814 vlad902 feat(SimpleGraph): Weaker condition for paths in acyclic graphs t-combinatorics awaiting review
29207 YaelDillies chore(MonoidAlgebra/Defs): reorder, rename variables t-algebra awaiting-CI help-wanted looking for help
23940 YaelDillies feat: polytopes toric t-analysis awaiting-author awaiting author
26051 Komyyy feat(Mathlib/GroupTheory/SpecificGroups/Alternating): A_n is simple iff n = 3 or 5 ≤ n t-group-theory large-import WIP labelled WIP
25780 emilyriehl feat: the homotopy category functor preserves products t-algebraic-topology infinity-cosmos large-import t-category-theory failing CI
28429 euprunin chore(GroupTheory/Perm/Cycle): deprecate `Disjoint.cycleType_mul` t-group-theory awaiting-author awaiting author
26189 tb65536 feat(FieldTheory/Galois/Basic): Add simp-lemma for `FixedPoints.intermediateField` t-algebra awaiting review
27238 alreadydone feat(Algebra): IsDomain R[X] ↔ IsDomain R ∧ IsCancelAdd R t-algebra awaiting review
28564 euprunin chore(LinearAlgebra): golf entire `congr_symm`, `LinearMap.toMatrix_smulBasis_left`, `LinearMap.toMatrix_smulBasis_right` and more using `rfl` t-algebra awaiting review
28887 alreadydone feat(RingTheory): units are exactly non-zerodivisors in noncommutative Artinian rings t-ring-theory t-algebra awaiting review
28929 grunweg experiment: use `fun_prop` in Homeomorph t-topology awaiting review
28973 YaelDillies feat(TensorProduct): `lTensor` as an `AlgHom` and other lemmas t-ring-theory toric awaiting review
29281 plp127 docs: `Fin.natAdd_castLEEmb` t-data awaiting review
29162 vlad902 feat(SetTheory): generalize Schroeder-Bernstein theorem t-set-theory awaiting review
27308 xyzw12345 feat(LinearAlgebra/SymmetricAlgebra): IsSymmetricAlgebra t-algebra awaiting review
25927 jjdishere feat(RingTheory/AdicCompletion): more APIs for IsAdicComplete t-ring-theory awaiting-author failing CI
27977 smmercuri feat: predicates for extensions of complex embeddings t-number-theory WIP labelled WIP
29200 euprunin chore: remove redundant `simp_rw` invocations t-algebra awaiting-author awaiting author
26448 YaelDillies refactor: simplify `(f₁ ⊗ₘ f₂) ≫ (g₁ ⊗ₘ g₂)` to `(f₁ ≫ g₁) ⊗ₘ (f₂ ≫ g₂)` toric t-category-theory awaiting review
29232 vihdzp feat: more theorems on `SuccAddOrder` t-order t-algebra failing CI
27244 xroblot feat(RingTheory/DedekindDomain): lifting an ideal in an extension is injective t-ring-theory large-import awaiting review
27288 themathqueen chore(LinearAlgebra/TensorProduct/Basic): semi-linearize `map` and `lift` t-algebra awaiting review
26935 Paul-Lez feat(Analysis/SpecialFunction/NthRoot): definition and basic API of Real.nthRoot t-analysis failing CI
28831 qawbecrdtey feat(Logic/Equiv/List): add `decodeList_encodeList_eq_self` and removed unnecessary linter options t-logic awaiting review
28906 gasparattila feat(Topology/Algebra/Module): `prod` and `coprod` as `ContinuousLinearEquiv`s new-contributor t-topology awaiting review
29120 eric-wieser feat: add a typeclass for the indiscrete topology t-topology failing CI
29328 vlad902 feat(SimpleGraph): graph isomorphism preserves `IsAcyclic`/`IsTree` t-combinatorics awaiting review
26790 FlAmmmmING feat(Combinatorics/Enumerative/Bell.lean): define standard Bell number new-contributor t-combinatorics awaiting review
26986 WangYiran01 feat(Partition): add bijection for partitions with max part ≤ r new-contributor t-combinatorics awaiting review
29339 kim-em feat: add linter for deprecations on different dates not separated by a blank line t-linter failing CI
29307 harahu doc: hyphenate attributive compound adjectives ending in "exact" awaiting review
26155 xroblot feat(DedekindDomain/Different): add the transitivity formula t-algebra awaiting review
27254 yuanyi-350 2025 imo problem3 IMO awaiting review
26310 kckennylau Binary form t-algebra awaiting-author awaiting author
27321 kckennylau feat(CategoryTheory): Colimit can be computed fiberwise t-category-theory awaiting-CI does not pass CI
29108 JonBannon feat(MeasureTheory): add `LInfty.lean` with `Mul` and `const` related results. t-measure-probability awaiting-author awaiting author
29332 Ruben-VandeVelde feat: Set.codRestrict_range_surjective FLT t-data awaiting review
28561 euprunin chore(Data): golf entire `equivFunOnFintype_single`, `predAbove_right_zero`, `snoc_zero` and more using `rfl` t-data awaiting review
29321 FormulaRabbit81 feat(Topology): obtain new distance structures on pseudo(e)metricspaces t-topology awaiting-CI WIP labelled WIP
22954 eric-wieser feat(RingTheory/Congruence/Hom): copy from GroupTheory t-ring-theory failing CI
25843 mitchell-horner feat(Combinatorics/SimpleGraph): define `between` subgraphs t-combinatorics awaiting review
27178 artie2000 feat(Algebra/Order/Ring): make `IsOrderedRing.toStrictOrderedRing` an instance t-ring-theory RFC awaiting review
29027 grunweg feat/fix(FlexibleLinter): mark more tactics as flexible t-linter awaiting review
27995 kckennylau feat(RingTheory/Valuation): alternate constructors for Valuation t-ring-theory awaiting-CI does not pass CI
28546 Sfgangloff feat(SymbolicDynamics): basic setup of Zd, full shift, cylinders, pat… new-contributor t-dynamics awaiting review
26277 AntoineChambert-Loir feat(RingTheory/Congruence/Hom): prove basic isomorphisms theorems for ring congruences t-ring-theory awaiting review
28613 espottesmith feat(Combinatorics): define undirected hypergraphs new-contributor t-combinatorics awaiting review
29356 Paul-Lez feat(Mathlib/FieldTheory/RatFunc/Basic): add characteristic instances for `RatFunc` t-algebra failing CI
29028 themathqueen feat(Algebra/Star): define `unitary R →* StarAlgEquiv S R R` t-algebra awaiting review
28836 yury-harmonic feat: add `norm_num` extensions t-meta awaiting-author awaiting author
26339 mans0954 feat(Analysis/Normed/Module/WeakDual): Banach Dieudonné Lemma large-import t-analysis WIP labelled WIP
29355 girving feat(Trigonometric): Taylor series bounds for sin and cos t-analysis failing CI
19046 j-loreaux feat: define class `SemigroupAction` t-algebra awaiting review
28311 eric-wieser fix(Tactic/NormNum): do not hang on large powers t-meta bug awaiting review
29040 PMKielstra feat: trapezoidal rule for integration new-contributor t-measure-probability awaiting review
29042 vihdzp feat(SetTheory/Ordinal/Exponential): generalize theorems from `y = succ x` to `x < y` t-set-theory awaiting review
29058 vihdzp feat: `Colex` type synonym t-order awaiting review
29082 grunweg RFC: tag `IsInducing` and `Is{Open,Closed,}Embedding` with `fun_prop` t-topology awaiting review
29114 jeremypparker feat(MeasureTheory.Integral): Mean value theorem for integrals new-contributor t-measure-probability awaiting review
29119 JovanGerb fix(Tactic/ToAdditive/Frontend): swap `reorderForall` and `applyReplacementForall` t-meta awaiting review
27882 euprunin chore: golf using `grind [Nat.cast_*]` awaiting review
27370 euprunin chore(Tactic/CancelDenoms): golf `cancel_factors_eq` t-meta awaiting review
27252 Parcly-Taxel feat: sharp bounds for `‖exp (I * x) - 1‖` when `x` is real carleson t-analysis awaiting review
29271 euprunin chore: remove redundant `let` and `letI` invocations maintainer-merge awaiting review
28000 daefigueroa feat(Dynamics/Flow): define semiconjugacy, factor and orbit new-contributor t-dynamics awaiting review
29365 staroperator feat(SetTheory/ZFC): add `ZFSet.card` t-set-theory awaiting review
26159 upobir feat(Algebra/QuadraticDiscriminant): Adding inequalities on quadratic from inequalities on discriminant t-algebra awaiting-author awaiting author
25905 mans0954 feat(RingTheory/Polynomial/SmallDegreeVieta): polynomial versions of results in Algebra.QuadraticDiscriminant t-ring-theory awaiting-zulip awaiting a zulip discussion
28389 euprunin chore(Algebra/Group/Subgroup): golf entire `subgroupOf_sup` t-algebra awaiting-author awaiting author
28305 euprunin chore(RingTheory/MvPolynomial): deprecate `weightedHomogeneousComponent_of_isWeightedHomogeneous_same` and golf entire `weightedHomogeneousComponent_of_isWeightedHomogeneous_ne` t-ring-theory awaiting-author awaiting author
28140 YaelDillies feat: a `PointedCone`-valued version of `Submodule.span` t-convex-geometry toric awaiting review
28295 artie2000 feat(Algebra/Order/Ring/Ordering): basic results about ring (pre)orderings t-algebra awaiting-author failing CI
28970 Whysoserioushah feat(Algebra/Algebra/ReducedNorm) : Defines reduced norm and trace t-algebra awaiting review
26464 joelriou feat(LinearAlgebra): generators of pi tensor products file-removed t-algebra awaiting review
26923 oliver-butterley feat(Dynamics/BirkhoffSum): add the pointwise ergodic theorem (Birkhoff's) new-contributor t-dynamics awaiting review
28339 JovanGerb feat(gcongr): support `@[gcongr]` for `Monotone` and friends t-meta awaiting review
28876 ScottCarnahan feat (Algebra/Group/Action/Basic): add IsLeftCancelSMul ⚠️ awaiting review
28833 yury-harmonic feat(MvPolynomial/Expand): more lemmas ⚠️ awaiting review
29103 grunweg chore: tests for casting and the field_simp discharger t-meta awaiting review
29121 Ruben-VandeVelde feat: MvPolynomial.symmetricSubalgebra.{aevalMultiset,sumPolynomial} t-ring-theory awaiting review
29369 vlad902 feat(SimpleGraph): `IsSubwalk` of common Walk decompositions t-combinatorics awaiting review
29376 vlad902 feat(SimpleGraph): Helper lemmas for `Walk.IsSubwalk` t-combinatorics awaiting review
26836 mans0954 feat(Order/Lattice): conditions for an equivalence relation to be a lattice congruence t-order awaiting-author awaiting author
29306 YaelDillies chore(GroupTheory/GroupAction/Basic): don't import `Module` t-algebra awaiting review
29212 Whysoserioushah feat(Algebra/CrossProductAlgebra/Defs) : Define Cross Product Algebra t-algebra awaiting-author awaiting author
29397 vihdzp chore(Algebra/Polynomial/Basic): make some arguments implicit t-algebra awaiting review
29347 themathqueen refactor(Algebra/Star/StarAlgHom): let `StarAlgEquiv` extend `StarRingEquiv` instead of `RingEquiv` t-algebra awaiting review
28511 YaelDillies feat(Finsupp): `congr!`-compatible version of `prod_congr` t-algebra awaiting review
26544 vihdzp feat(SetTheory/ZFC/Ordinal): Lean ordinals to ZFC ordinals large-import t-set-theory awaiting review
28728 or4nge19 feat(PerronFrobenius): introduce StronglyConnected Quiver and Irreducible and Primitive Matrices and their basic properties and relations file-removed new-contributor awaiting-author ⚠️ failing CI
29362 stepanholub Periods of lists and the Periodicity Lemma t-data new-contributor awaiting review
29228 Timeroot feat(Logic/Basic): HEq iff Exists a cast t-logic awaiting review
27073 pechersky feat(Archive/Examples/Local): files showcasing properties of local fields t-number-theory awaiting review
29407 pechersky feat(RingTheory): hom from local ring to ZMod is a local hom t-ring-theory awaiting review
29410 jsm28 feat(Data/Nat/Init): `n.AtLeastTwo` implies `NeZero (n - 1)` t-data awaiting review
29404 pechersky feat(Data/Nat): p.Coprime factorial and choose t-data maintainer-merge t-algebra easy awaiting review
29225 euprunin chore: remove redundant `cases` invocations t-algebra awaiting review
28834 euprunin chore(Data/Finset): golf 10 lines from `powerset_insert` using `grind` t-data awaiting review
28835 euprunin chore(Data/List): golf 13 lines from `bidirectionalRec_cons_append` using `grind` t-data awaiting review
28841 euprunin chore(Data/List): golf entire `mem_getLast?_append_of_mem_getLast` and `mem_head?_append_of_mem_head?` using `grind` t-data awaiting review
29409 Julian feat(Mathlib/Analysis): deriv_eq_self and deriv_exp_iff t-analysis awaiting review
28219 joelriou feat(CategoryTheory): monomorphisms in Type are stable under transfinite compositions t-category-theory awaiting review
29166 YaelDillies feat: group objects form a cartesian-monoidal category toric t-category-theory awaiting review
29185 eric-wieser feat: add missing `norm_cast` on subobject coercion lemmas to set t-algebra awaiting review
24669 qawbecrdtey feat(Analysis/Normed/Operator/LinearIsometry): added definition `LinearIsometryEquiv.prodComm` maintainer-merge t-analysis awaiting-author awaiting author
27742 ChrisHughes24 feat(Nat/nth): inequalities about Nat.nth t-data awaiting review
29422 jsm28 fix(Data/Finset/Max): Use `DecidableEq` for `insert` lemmas t-data awaiting review
29352 fpvandoorn refactor: simplify dictionary in fixAbbreviation t-meta awaiting author
26757 fweth feat(CategoryTheory/Topos): define elementary topos new-contributor t-category-theory awaiting review
29427 kim-em feat: grind annotations for `Finset.sdiff` t-data awaiting review
29400 ShreckYe feat(`Algebra/BigOperators`): products of the results of insertion and removal on tuples and lists, and some needed lemmas large-import ⚠️ awaiting review
27390 alreadydone feat(FieldTheory/Galois): normal basis theorem t-algebra awaiting review
29373 staroperator doc(ModelTheory): clarify free and (in-scope) bound variables in `BoundedFormula` t-logic documentation awaiting review
28289 robin-carlier chore(CategoryTheory/Bicategory/Functor/Strict): generalize some results to op/lax functors large-import t-category-theory delegated delegated
28384 euprunin chore(Algebra/Order/Ring): golf entire `cast_natAbs` t-algebra awaiting-author awaiting author
28385 euprunin chore(Algebra/BigOperators/Finsupp): deprecate `Finsupp.sum_sum_index'` t-algebra awaiting-author awaiting author
27701 vihdzp feat: `a < b + c ↔ a < b ∨ ∃ d < c, a = b + d` t-algebra awaiting-author awaiting author
26881 emo916math feat(Analysis/Calculus/Deriv/Star) A formula for `deriv (conj ∘ f ∘ conj)` new-contributor t-analysis awaiting-author awaiting author
24533 robertmaxton42 feat (ULift): conjugation by ULift.up/down, misc cast/heq lemmas t-data awaiting-author awaiting author
25183 YaelDillies feat: convolution product on linear maps from a coalgebra to an algebra toric t-algebra awaiting review
29437 NotWearingPants feat(Data/Seq): add Seq.subsequence and prove basic theorems about it large-import t-data new-contributor awaiting review
26453 jburroni feat(Data/PNat/Basic): add order-related instances to PNat t-data new-contributor awaiting review
26330 Timeroot feat: "Junk value" test file t-data awaiting review
29439 themathqueen feat(Analysis/InnerProductSpace/Projection/Basic): `e ∘ f = 0` iff `(ker e).starProjection ∘ f = f` t-analysis awaiting review
29435 sgouezel WIP: typeclass experiment t-algebra WIP labelled WIP
28945 harahu doc: hyphenate compound adjectives ending in -dimensional maintainer-merge awaiting review
29420 llllvvuu chore: golf `LinearMap.charpoly_toMatrix` and add corollaries t-algebra awaiting review
28967 utkuokur refactor(Combinatorics/SimpleGraph/Walk): simplify proof of "support_tail_of_not_nil" new-contributor t-combinatorics awaiting review
29448 j-loreaux chore(Analysis/{NormedSpace/ConformalLinearMap → Normed/Operator/Conformal}): move file file-removed tech debt t-analysis awaiting review
26282 AntoineChambert-Loir feat: a theorem of Jordan on primitive subgroups of the permutation group t-group-theory large-import awaiting review
29351 staroperator feat(SetTheory/Cardinal): generalize and rename theorems on `Cardinal.sum` t-set-theory awaiting review
29429 kim-em feat: `grind` annotations for `Finset.card` t-data awaiting review
26462 PSchwahn feat(LinearAlgebra/Projection): add results about inverse of `Submodule.prodEquivOfIsCompl` new-contributor t-algebra awaiting-author awaiting author
29398 vihdzp feat: `Polynomial.coeffs_nonempty_iff` t-algebra easy awaiting review
29454 kim-em feat: `grind` annotations for `Nat.count` ⚠️ awaiting review
29455 kim-em chore: grind annotations in Data/Nat/Find t-data awaiting review
29133 ScottCarnahan chore (Algebra/Vertex): linearize coefficient functions t-algebra awaiting review
29154 ScottCarnahan feat (Algebra/Lie): Define low-degree cochains and differentials for coefficients with trivial action t-algebra awaiting review
29224 euprunin chore: remove redundant `rcases` invocations t-algebra awaiting review
29456 kim-em chore: basic grind annotations for Real.sqrt awaiting review
29449 mitchell-horner feat(Combinatorics/SimpleGraph): add Turán density related theorems t-combinatorics awaiting review
29458 LiamSchilling feat(MvPolynomial/WeightedHomogenous): relate `weightedTotalDegree` to `degrees`, `totalDegree`, and `degreeOf` t-ring-theory new-contributor awaiting review
28248 YaelDillies feat: expectation and (conditional) variance of a Bernoulli random variable t-measure-probability awaiting-author awaiting author
29434 ntapiam feat(NonAssoc/LieAdmissible): prove every ring/algebra is LieAdmissible new-contributor t-algebra failing CI
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 awaiting review
29459 bwangpj feat: ContMDiffAt.pow maintainer-merge t-differential-geometry awaiting review
28908 joelriou feat(CategoryTheory): Pullback functors on `Over` categories in `Type` have right adjoints t-category-theory awaiting-author failing CI
27162 themathqueen feat(Analysis/InnerProductSpace/Positive): `U.starProjection ≤ V.starProjection` iff `U ≤ V` t-analysis awaiting review
28533 kim-em feat(linarith): add `linarith?` mode which suggests a `linarith only` call codex t-meta awaiting review
28393 tristan-f-r chore(WithZero): clean t-data awaiting-author awaiting author
29470 NotWearingPants chore(Algebra/Group/Action/Faithful): fix typo in LefttCancelMonoid new-contributor t-algebra easy awaiting review
28950 Vierkantor fix(TacticAnalysis): comment out syntax range check t-meta awaiting review
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
26219 Thmoas-Guan feat(RingTheory/KrullDimension): Krull Dimension of quotient regular sequence t-ring-theory awaiting-author awaiting author
27567 themathqueen feat(LinearAlgebra/TensorProduct/Associator): add `lid` and `assoc` tensor lemmas t-algebra easy awaiting review
28097 themathqueen feat(LinearAlgebra/Matrix/PosDef): kronecker of positive (semi-)definite matrices is positive (semi-)definite t-algebra awaiting review
29383 Vierkantor chore(Topology): process porting notes tech debt t-topology awaiting review
29475 euprunin chore(RingTheory/Extension/Presentation): remove use of `erw` in `aeval_comp_val_eq` t-ring-theory awaiting review
26909 gasparattila feat(LinearAlgebra/Projectivization/Subspace): correspondence between linear and projective subspaces new-contributor t-algebra awaiting review
29474 sgouezel feat: explicit zsmul field in ring constructor to solve performance issue t-algebra awaiting review
28175 dsfxcimk feat: exterior angle theorem new-contributor t-euclidean-geometry awaiting-author awaiting author
28286 bwangpj feat(Geometry/Manifold/ContMDiff): basic lemmas for analytic (`C^ω`) functions new-contributor t-differential-geometry awaiting-author awaiting author
28871 JaafarTanoukhi feat(Combinatorics/Digraph): Tournaments new-contributor t-combinatorics failing CI
28793 grunweg feat: smooth immersions t-differential-geometry awaiting review
25736 robin-carlier feat(AlgebraicTopology/SimplexCategory/GeneratorsRelations/NormalForms): Normal forms for `P_σ`s t-algebraic-topology large-import awaiting review
26824 robin-carlier feat(CategoryTheory/Monoidal/DayConvolution): Day functors type synonym t-category-theory awaiting review
26614 Rida-Hamadani feat(SimpleGraph): add more API for `take`/`drop` t-combinatorics awaiting-author failing CI
29118 edegeltje chore(CategoryTheory): align `refl` and `rfl` declarations in CategoryTheory will-close-soon t-category-theory awaiting-author awaiting author
28719 mitchell-horner refactor: redefine `IsTuranMaximal` t-combinatorics awaiting review
28987 euprunin chore(Analysis/Distribution): remove redundant `have` in `ae_eq_zero_of_integral_smooth_smul_eq_zero` t-analysis awaiting review
29132 YaelDillies feat(AdjoinRoot): bundle operations as `AlgHom`s t-ring-theory toric awaiting review
29257 harahu doc: attach "pre", "pseudo", "semi" and "sub" as a prefixes where they are now free-standing t-meta awaiting review
29488 Timeroot feat: 'said' tactic ⚠️ awaiting review
26331 Timeroot feat(Algebra/Polynomial): Descartes' Rule of signs t-algebra awaiting review
27262 Timeroot feat(Tactic/Bound): bound? for proof scripts t-meta failing CI
29092 zhuyizheng feat(MeasureTheory): add absolutely continuous functions, FTC and integration by parts new-contributor t-measure-probability awaiting-author awaiting author
29491 bwangpj feat: closed point of scheme gives maximal ideal in affine open t-algebraic-geometry awaiting review
29464 harahu doc(AkraBazzi): corrections to docs by way of LLM t-computability awaiting-author awaiting author
28682 Thmoas-Guan feat(RingTheory): definition of regular local ring t-ring-theory awaiting-author awaiting author
29471 harahu doc: use em dash instead of hyphen in Akra-Bazzi t-computability awaiting review
29273 kim-em chore: add test for grind panic failing CI
27841 CBirkbeck feat(Topology/Algebra/InfiniteSum/NatInt): add more pnat tsum lemmas t-topology awaiting review
27702 FLDutchmann feat(NumberTheory/SelbergSieve): define Lambda-squared sieves and prove important properties t-number-theory awaiting review
28124 kckennylau feat(Tactic): Call an arbitrary Simproc t-meta failing CI
29486 kim-em chore: scope an expensive `IsDomain`->`IsAddTorsionFree` instance t-algebra awaiting review
28780 gaetanserre feat(Analysis/SpecialFunctions): add the sigmoid function t-analysis awaiting review
27304 jano-wol feat: invariant dual submodules define Lie ideals t-algebra awaiting review
28789 yury-harmonic feat(ArithmeticFunction): lemmas about positivity new-contributor t-number-theory t-meta awaiting-author awaiting author
29253 FernandoChu feat(CategoryTheory): (Co)limits in preorders new-contributor t-category-theory awaiting review
29115 CBirkbeck feat: develop some more limUnder api t-topology awaiting review
29506 Vierkantor feat(CI): `nightly-testing` regression report CI awaiting review
27306 xyzw12345 feat: `lie_ring` tactic and `LieReduce` command t-meta awaiting review
29045 grunweg chore: remove the `field_simps` simp set maintainer-merge awaiting review
29500 vihdzp feat: `WellFoundedLT (LowerSet α)` t-order awaiting review
29504 zhuyizheng feat(MeasureTheory): add absolutely continuous functions new-contributor t-measure-probability awaiting review
29113 scholzhannah chore: rename PartialHomeomorph to OpenPartialHomeomorph file-removed awaiting review
29156 harahu doc: treat "non" as a prefix where it appears as a free-standing word awaiting review
29511 luigi-massacci feat: integrating wrt a finite measure as a continuous linear map on bounded continuous functions maintainer-merge t-measure-probability awaiting review
29514 grunweg More strict mode CI WIP labelled WIP
25324 eric-wieser feat: more functorial results about DFinsupp t-data t-algebra awaiting review
29498 harahu doc: improve grammar and flow in documentation maintainer-merge t-computability awaiting review
29057 jeremypparker feat(Topology/Instances): `AddCircle.liftIoc_continuous` new-contributor t-topology awaiting review
29380 chrisflav feat(CategoryTheory/MorphismProperty): define `ind P` large-import t-category-theory awaiting review
28395 joelriou feat(AlgebraicTopology/SimplicialSet): nondegenerate simplices in the standard simplex t-algebraic-topology awaiting review
29516 kckennylau chore: Deprecate IsAdjoinRoot.subsingleton awaiting review
24050 Paul-Lez feat(Data/Finsupp/Pointwise): generalise pointwise scalar multiplication of finsupps t-data awaiting review
29405 pechersky feat(NumberTheory/Padic): characterization of norms of zmodRepr t-number-theory awaiting review
29403 pechersky feat(Data/Nat/Basic): Nat.dvd_sub_self_iff t-data easy awaiting review
29416 pechersky feat(RingTheoryy/RootsOfUnity): of_card_le t-ring-theory awaiting review
29408 pechersky feat(Analysis/Normed/Ultra): nonarch norm of sum over disjoint norms achieves max maintainer-merge t-analysis awaiting review
28349 kckennylau feat(Meta): add notation for naming stacked polynomials t-meta failing CI
29518 joelriou feat(CategoryTheory): extremal epimorphisms t-category-theory awaiting review
26031 joelriou feat(Algebra/Homology): the derived category of a linear abelian category is linear t-category-theory awaiting review
29221 euprunin chore: remove redundant `rintro` invocations (before `omega`) awaiting review
29300 Louddy feat: SkewPolynomial t-algebra awaiting review
29315 kbuzzard chore: raise priority of `IsTopologicalSemiring.toIsModuleTopology` t-topology awaiting review
29302 harahu doc: hyphenate attributive compound adjectives starting with "upper" or "lower" awaiting review
29318 FernandoChu feat(CategoryTheory): (Co)limits in skeletons new-contributor t-category-theory awaiting review
29497 xyzw12345 feat(Counterexamples): A ring such that dim A = 1 but dim A[x] = 3 t-algebra awaiting review
29527 kim-em feat: script for checking Github URLs CI WIP labelled WIP
29526 llllvvuu feat: `Multiset.map f` identifies `f` up to permutation t-data awaiting review
29532 Aaron1011 feat: add group/field versions of Filter.map_*_atTop_eq_nat new-contributor t-order awaiting review
29476 llllvvuu feat(LinearAlgebra/Matrix): `charpoly` splits into `IsHermitian.eigenvalues` t-algebra awaiting review
29248 mans0954 feature(Analysis/Convex/Basic): Convexity and the algebra map t-analysis awaiting review
29538 YaelDillies refactor(FractionalIdeal): use algebraic order theory API t-ring-theory WIP labelled WIP
29503 zhuyizheng feat(MeasureTheory): add Lebesgue differentiation theorem for intervals new-contributor t-measure-probability awaiting review
29426 kim-em feat: grind annotations for Finset.range t-data awaiting review
29539 YaelDillies feat: monoid algebras are invariant under base change t-ring-theory toric large-import awaiting review
29510 sgouezel chore: add missing fast_instance attributes t-topology awaiting review
26287 mbkybky feat(Data/ENat/Lattice): coercion to `WithBot ℕ∞` commutes with `biSup` t-data awaiting-author awaiting author
29324 tb65536 refactor(Analysis/Calculus/IteratedDeriv/Defs): tweak statement of `iteratedDerivWithin_one` t-analysis awaiting review
29247 harahu doc: hyphenize "weighted homogeneous" when used attributively t-ring-theory awaiting-author awaiting author
29326 FormulaRabbit81 feat(Analysis): constant * function tending to 0 is still 0 large-import t-analysis awaiting review
29297 harahu doc: hyphenate "first order" and "higher order" when used attributively maintainer-merge awaiting review
29256 harahu doc: attach "quasi" as a prefix where it is currently freestanding t-dynamics t-measure-probability awaiting review
29430 RemyDegenne refactor(Probability): change stopping times to take values in `WithTop` t-measure-probability WIP labelled WIP
29413 jsm28 refactor(Geometry/Euclidean/Altitude,Geometry/Euclidean/Incenter): use `Nat.AtLeastTwo` t-euclidean-geometry awaiting review
29477 izanbf1803 feat(Algebra/Ring/Invertible): add `eq_of_invOf_add_eq_invOf_add_invOf` new-contributor t-algebra awaiting review
29552 RemyDegenne feat(Probability): lemmas about composition of kernels and measures t-measure-probability awaiting review
27098 Paul-Lez feat(Algebra/Category/ModuleCat/Sheaf/VectorBundle): define vector bundles t-algebra awaiting-author awaiting author
29554 RemyDegenne feat(Probability): `CondIndepFun` lemmas t-measure-probability awaiting review
29556 joelriou feat(CategoryTheory): canonical colimits t-category-theory awaiting review
25735 robin-carlier feat(CategoryTheory/Limits/Sifted): characterization of sifted categories large-import t-category-theory awaiting review
29550 Raph-DG feat(RingTheory): Order of vanishing in a discrete valuation ring t-ring-theory file-removed awaiting review
22039 YaelDillies feat: simproc for computing `Finset.Ixx` of natural numbers large-import t-meta awaiting review
28266 euprunin chore(RingTheory): golf entire `single_one_eq_pow` using `simp` t-ring-theory awaiting-author awaiting author
29547 kim-em chore: remove defunct polyrith tactic file-removed awaiting review
29492 kim-em feat: grind golf in Mathlib.Data.List t-data awaiting review
25778 thefundamentaltheor3m feat: Monotonicity of `setIntegral` for nonnegative functions new-contributor t-measure-probability awaiting-author awaiting author
29562 ShreckYe feat(Analysis/SpecialFunctions/Trigonometric): tangent half-angle substitution t-analysis awaiting review
27847 euprunin chore(Algebra): avoid duplicating proofs by reusing existing theorems or lemmas t-algebra awaiting review
25930 loefflerd WIP towards Hecke bound for q-expansions migrated-from-branch t-number-theory WIP labelled WIP
29563 j-loreaux refactor: switch to using `Fact (0 ∈ s)` for `ContinuousMapZero.id` t-analysis awaiting review
28035 euprunin chore: replace `norm_num` with `simp` where applicable awaiting review
26640 euprunin chore(Data): golf `Data/` using `grind` bench-after-CI t-data awaiting review
28996 euprunin chore: remove redundant `have`:s in `Computability/`, `Combinatorics/`, `Condensed/`, `Data/Nat/` and `Data/PNat/` awaiting review
29564 dagurtomas feat(CategoryTheory/Monoidal): more natural constructors for monoidal functors t-category-theory awaiting review
26370 b-mehta chore(Archive): golf and generalise ascending-descending sequences t-data delegated delegated
29540 YaelDillies refactor(SimpleGraph): make `triangleRemovalBound` positive more often t-combinatorics awaiting review
26955 mariainesdff feat(LinearAlgebra/OnSup): extend linear maps to sums of modules t-algebra awaiting-author awaiting author
27864 BoltonBailey feat(Data/{Finset,Multiset}/Sort): give sort functions ≤ default argument t-data awaiting review
29530 ShreckYe feat(Dynamics/PeriodicPts): some theorems for `Pi.map` in `Dynamics/PeriodicPts` analogous to those for `Prod.map` large-import ⚠️ awaiting review
29395 YaelDillies refactor: make `PosMulMono` and alike custom classes t-order t-algebra awaiting review
19668 YaelDillies refactor: define `≤`/`<` on `WithBot`/`WithTop` by induction t-order awaiting review
26398 ChrisHughes24 feat(ModelTheory): definable functions t-logic awaiting review
26720 vlad902 feat(SimpleGraph): lemmas relating edges and darts to the support t-combinatorics awaiting review
26785 TOMILO87 feat: beta distribution new-contributor t-measure-probability awaiting review
29463 HugLycan feat(Positivity): add positivity extensions for `NNReal.rpow` and `ENNReal.rpow` new-contributor t-analysis awaiting-author awaiting author
26110 YaelDillies feat: sharp monoids toric t-algebra awaiting review
29295 YaelDillies chore: rename `mul_lt_mul_left`/`mul_lt_mul_right` to `mul_lt_mul_iff_right₀`/`mul_lt_mul_iff_left₀` t-order t-algebra failing CI
29275 wwylele feat(GroupTheory): add DivisibleHull t-group-theory awaiting review
26371 Timeroot feat(NumberTheory): Niven's theorem t-number-theory awaiting review
29551 chrisflav feat(CategoryTheory/Sites): the category of `1`-hypercovers up to homotopy large-import t-category-theory awaiting review
26039 tsuki8 feat(RingTheory/MvPolynomial/MonomialOrder): leadingTerm t-ring-theory new-contributor awaiting-author awaiting author
29227 robertmaxton42 feat (Limits.FunctorCategory): limitIsoFlipCompLim and colimitIsoFlipCompColim are natural t-category-theory awaiting review
28582 Thmoas-Guan feat(Data): some lemmas about WithBot ENat t-data awaiting-author awaiting author
19872 YaelDillies chore(GroupTheory/Index): rename `relindex` to `relIndex` FLT maintainer-merge t-algebra awaiting review
27849 robin-carlier feat(CategoryTheory/Bicategory/Functor): strictly unitary lax/pseudo functors t-category-theory ready-to-merge delegated awaiting bors
29569 chrisflav chore(RingTheory/LocalProperties): add algebra versions of exactness lemmas t-ring-theory awaiting review
29468 kim-em feat: add `cutsat` and `grobner` macro frontends to `grind` ⚠️ awaiting review
29573 kim-em chore: deprecate `Traversable` deriving handler file-removed awaiting review
26129 LessnessRandomness feat(Geometry/Euclidean/Angle/Unoriented): triangle inequality for angles new-contributor t-euclidean-geometry awaiting review
27956 bryangingechen feat: automation for removing outdated deprecations CI awaiting review
28571 euprunin chore(RingTheory): golf entire `mem_extended_iff`, `coeff_opRingEquiv` and `comp_assoc` using `rfl` t-ring-theory awaiting review
28981 euprunin chore(AlgebraicTopology/ModelCategory): remove redundant `have` in `mk'.cm3a_aux` t-algebraic-topology awaiting review
29223 dwrensha feat: norm_num extension for abs t-meta awaiting review
29270 euprunin chore: remove redundant `refine` invocations awaiting review
29250 Jlh18 chore: rename hom_to_functor, id_to_functor new-contributor t-category-theory easy awaiting review
29301 harahu doc: hyphenate attributive compound adjectives ending in "preserving" awaiting review
29316 euprunin chore: remove redundant `suffices` invocations awaiting review
29317 euprunin chore: remove redundant `generalize`, `induction`, `repeat'` and `unfold` invocations awaiting review
29344 JovanGerb feat(Geometry/Euclidean/Sphere/Power): use side condition `p ∈ line[ℝ, a, b]` t-euclidean-geometry awaiting review
29559 j-loreaux feat: add C⋆-algebra instances for elemental algebras t-analysis delegated delegated
29574 JarodUW Regular local rings are domains t-ring-theory new-contributor failing CI
28706 euprunin chore: golf entire `dite_ne_left_iff`, `exists_prime_lt_and_le_two_mul_succ`, `lt_up` and `sUnion_mem_empty_univ` using `grind` maintainer-merge awaiting review
29453 kim-em chore: grind annotations in Data/Bool t-data awaiting review
27307 xyzw12345 feat(RingTheory/GradedAlgebra): homogeneous relation t-ring-theory awaiting review
29004 euprunin WIP: experiment: bench `:= rfl` vs `:= by rfl` WIP labelled WIP
29136 YaelDillies feat(CategoryTheory/Monoidal): `mapMon` of a lax-braided functor is lax-braided toric t-category-theory awaiting review
29577 kim-em feat: alternating series error bound ⚠️ awaiting review
29548 Parcly-Taxel feat: add `induction'` to the deprecated syntax linter awaiting-zulip tech debt t-linter awaiting a zulip discussion
26096 vasnesterov feat(Topology/Instances): Cantor set is the set of ternary numbers without `1`s large-import t-topology awaiting review
29445 j-loreaux chore(Analysis/NormedSpace/Extend): split file file-removed tech debt t-analysis awaiting-author awaiting author
29432 lecopivo feat: `data_synth` tactic to prove `HasFDerivAt 𝕜 f ?f' x` and similar t-meta WIP labelled WIP
25138 chrisflav chore(RingTheory/Ideal): make `RingHom.ker` take a `RingHom` instead of `RingHomClass` t-algebra failing CI
29310 Louddy feat(SkewMonoidAlgebra): algebra instance t-algebra awaiting review
29589 grunweg feat: add mfderiv_prod and mfderiv_prodMap t-differential-geometry WIP labelled WIP
28802 grunweg feat: a tactic linter for continuity/measurability which can be `fun_prop` large-import awaiting-CI t-meta does not pass CI
29177 scholzhannah feat: a subcomplex of a classical CW complex is a CW complex t-topology delegated delegated
29590 uniwuni chore(Algebra/Group/Submonoid/Membership): fix outdated docs t-algebra easy awaiting review
29587 uniwuni feat(GroupTheory/Finiteness): define finitely generated semigroups ⚠️ awaiting review
29593 Vierkantor chore(*): replace `simp? says` with `simp only` awaiting review
29578 vlad902 feat(SimpleGraph): remove finiteness assumption from `isEmpty_of_chromaticNumber_eq_zero` t-combinatorics easy awaiting-author awaiting author
29401 eric-wieser feat: more lemmas about `Matrix.vecMulVec` t-algebra awaiting review
28693 faenuccio feat(Analysis.Normed.Module.Milman-Pettis): add Milman-Pettis theorem t-analysis WIP labelled WIP
29594 faenuccio feat(Algebra.Order.GroupWithZero.WithZero): add multiplicativity t-algebra failing CI
29087 dupuisf feat: Define strictly positive operators (i.e. positive definite) t-algebra awaiting review
28958 faenuccio feat: add Nontrivial instance for linear maps t-algebra t-analysis awaiting-author awaiting author
26259 Raph-DG feat(Topology): Connecting different notions of locally finite t-topology awaiting review
27964 smmercuri refactor(AbsoluteValue): generalise equivalence to non-real valued absolute values maintainer-merge t-algebra t-analysis awaiting review
29598 xroblot feat(NumberField): two ring-isomorphic number fields have the same discriminant t-number-theory easy awaiting review
29597 alreadydone feat(Algebra): preliminaries for ring structure on `AddLocalization` t-algebra awaiting review
26357 javra feat(CategoryTheory): linear categories as `ModuleCat R`-enriched categories large-import t-category-theory awaiting review
28493 gasparattila feat: topological affine spaces large-import new-contributor t-analysis t-topology awaiting review
29592 themathqueen feat(Analysis/SpecialFunctions/CFC/Rpow): `0 ≤ a` iff `a = star b * b` for some `b` t-analysis awaiting review
29144 ADedecker feat: some lemmas about closed maps t-topology delegated failing CI
29599 fmortimore feat(Order): bourbaki-witt theorem new-contributor ⚠️ failing CI
27429 smorel394 feat(RepresentationTheory/FinGroupCharZero): applications of Maschke's theorem t-algebra awaiting review
29319 Louddy feat(SkewMonoidAlgebra): Modifying elements of skew monoid algebra at exactly one point (erase and update) t-algebra awaiting-author awaiting author
29501 Vierkantor test(TacticAnalysis): ensure `classical`'s effects are picked up blocked-by-core-PR blocked on another PR
29182 euprunin chore: remove redundant `congr` invocations t-algebra failing CI
28100 themathqueen feat(LinearAlgebra/Matrix): algebra automorphisms on matrices are inner t-algebra awaiting-author awaiting author
29601 jt496 feat(SimpleGraph/Walk): add missing results involving `getVert` / `takeUntil` t-combinatorics awaiting review
29436 eric-wieser feat: a better version of `LinearOrder.lift` maintainer-merge t-order awaiting review
29391 eric-wieser feat: more connections between `TensorProduct` and `map₂` t-algebra awaiting review
28115 bwangpj feat(AlgebraicGeometry/EllipticCurve): reduction of elliptic curves new-contributor t-algebraic-geometry awaiting review
27216 D-Thomine feat(Cardinal/Finite): ENat powers and cardinality t-algebra awaiting review
28818 NotWearingPants feat(Data/Setoid/Basic): add theorems about lifting a function to its kernel t-data new-contributor easy awaiting review
29241 yoh-tanimoto feat(Analysis/InnerProductSpace/Orthogonal): add duplicates for `ClosedSubmodule` ⚠️ awaiting review
29235 yoh-tanimoto feat(Topology/Algebra/Module/ClosedSubmodule): add `mapEquiv`, a variation of `ClosedSubmodule.map` for CLE t-topology awaiting review
27043 wwylele feat(Algebra/Order): Hahn embedding theorem, part 1 t-algebra awaiting review
27270 EtienneC30 chore: turn WithLp into a structure large-import t-analysis failing CI
25831 ScottCarnahan feat (RingTheory/HahnSeries): Powers of a binomial t-ring-theory awaiting review
27257 JovanGerb feat(LinearAlgebra/AffineSpace/Ordered): add `lineMap_le_lineMap_iff_of_lt'` maintainer-merge t-algebra awaiting review
26035 fbarroero feat(Analysis/Polynomial/MahlerMeasure): the Mahler measure of a complex polynomial t-analysis awaiting review
29582 YaelDillies chore: rename `_root_.prop` to `finite_prop` t-data awaiting review
29517 pechersky feat(RingTheory/Torsion): torsion = union of roots of unity t-algebra failing CI
29428 llllvvuu feat: generalize `LinearMap.finrank_maxGenEigenspace` t-algebra awaiting review
29513 grunweg fix(lint-style): parse linter options and load environment extensions correctly t-meta awaiting review
26827 pechersky feat(Analysis/Normed/ValuativeRel): helper instance for NormedField t-algebra t-analysis t-number-theory failing CI
27339 pechersky chore(RingTheory/Laurent): use WithZero.exp to golf statements and proofs about valuation on K((X)) t-algebra t-number-theory failing CI
29568 dagurtomas feat(CategoryTheory/Monoidal): more natural constructors for braided categories t-category-theory awaiting review
29110 NotWearingPants feat(Counterexamples): Euler's sum of powers conjecture new-contributor ⚠️ awaiting review
29512 grunweg feat: check for PR titles which do not start with "feat" etc. ⚠️ failing CI
28874 vasnesterov feat(Data/Seq): coinductive predicates for sequences large-import t-data awaiting review
29605 alreadydone chore(Algebra): unbundle npow from Monoid t-algebra awaiting-CI does not pass CI
29411 llllvvuu feat(LinearAlgebra/Matrix/Rank): rank factorization t-algebra awaiting review
27342 staroperator feat(ModelTheory): define linear and semilinear sets t-logic awaiting review
29607 wwylele feat(RingTheory): summability lemma for (Mv)PowerSeries t-ring-theory awaiting review
27053 tb65536 (WIP) Galois group of `x^n - x - 1` large-import t-algebra WIP labelled WIP
28477 yapudpill feat(RingTheory): golf `IsPrincipalIdealRing.of_prime` t-ring-theory new-contributor awaiting review
28061 CoolRmal feat(MeasureTheory): Uniqueness of Measures in the Riesz–Markov–Kakutani Representation Theorem new-contributor t-measure-probability awaiting review
28695 chrisflav feat(RingTheory): meta properties of bijective ring homomorphisms t-ring-theory large-import awaiting review
29330 plp127 chore: define `Fin.cycleIcc` with conditions t-group-theory awaiting review
29322 xroblot feat(RingTheory/Localization/AtPrime): bijection between prime ideals t-ring-theory awaiting review
29341 joelriou feat(Topology): the topology generated by a family of spaces t-topology awaiting review
29361 FlAmmmmING feat(RingTheory/PowerSeries/Catalan.lean) t-ring-theory new-contributor awaiting review
29588 Periecle feat(Analysis/Complex/Residue): Implement residue theory for complex functions at isolated singularities new-contributor t-analysis failing CI
29208 ShreckYe feat(Algebra/GCDMonoid/Finset): change the signature of `lcm_eq_zero_iff` to its simp normal form and add `lcm_ne_zero_iff` theorems t-algebra delegated failing CI
27936 alreadydone feat(Algebra): additivize Dvd and Prime t-algebra awaiting review
29354 themathqueen refactor(Algebra/Algebra/Equiv): allow for non-unital `AlgEquiv` t-algebra awaiting review
26920 yuma-mizuno feat(Tactic.CategoryTheory): add associator inserting tactic t-category-theory t-meta WIP labelled WIP
26601 yuma-mizuno feat(CategoryTheory): make `Functor.comp` irreducible t-category-theory WIP labelled WIP
29613 RemyDegenne chore(Probability): rename IsFiniteKernel.bound to Kernel.bound t-measure-probability awaiting review
29604 mans0954 refactor(Analysis/LocallyConvex/WithSeminorms): Relax some of the hypothesis t-analysis awaiting review
28846 euprunin chore(RingTheory/HahnSeries): golf entire `C_ne_zero` using `grind` t-ring-theory awaiting-author awaiting author
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 maintainer-merge awaiting review
27107 AntoineChambert-Loir feat(GroupTheory/GroupAction/SubMulAction/Combination) : combinations and group actions t-group-theory failing CI
27400 dleijnse feat: define geometrically reduced algebras new-contributor t-algebra failing CI
27599 mitchell-horner feat(Combinatorics/SimpleGraph): define `CompleteEquipartiteSubgraph` t-combinatorics awaiting review
29615 eric-wieser chore: add a computable shortcut for `AddCommMonoid ℂ` bench-after-CI t-analysis easy failing CI
27602 mitchell-horner feat(Combinatorics/SimpleGraph): define `CompleteBipartiteSubgraph` t-combinatorics awaiting review
26783 matthewjasper feat(RingTheory/Flat): Add theorems relating Submodule.torsion and Module.Flat t-ring-theory FLT maintainer-merge new-contributor awaiting review
28767 chrisflav feat(RingTheory/Extension/Presentation): lemmas for computation of Jacobian t-ring-theory awaiting review
29600 xroblot feat(IsPrimitiveRoot): add `adjoin_pair_eq` t-ring-theory 🟤 running CI
26089 WilliamCoram feat: restricted power series form a ring new-contributor t-algebra t-number-theory awaiting-author awaiting author
27313 pechersky feat(RingTheory/ValuativeRel/Trivial): the trivial valuative relation t-algebra t-number-theory awaiting review
26192 kckennylau feat(LinearAlgebra): symmetric tensor power t-algebra awaiting review
28187 vihdzp feat: archimedean classes of rationals t-algebra ready-to-merge awaiting review
29278 Jlh18 feat: groupoid instance on quotient category large-import new-contributor t-category-theory awaiting review
26101 xroblot feat(NumberField): specialized version of Kummer Dedekind for the splitting of prime numbers t-number-theory awaiting review
26345 mans0954 feat(Analysis/LocallyConvex/Polar): Bipolar theorem large-import t-analysis awaiting-author 🟤 running CI
29122 yonggyuchoimath feat(CategoryTheory/MorphismProperty/Representable): add relative representability of diagonal map new-contributor t-category-theory awaiting review
29611 vihdzp feat: alternate characterization of `≤` on Archimedean classes t-algebra awaiting review
28329 pechersky feat(RingTheory/Valuation): generalize CommGroupWithZero on mrange to MonoidWithZeroHom maintainer-merge t-order t-algebra awaiting review
28614 kckennylau feat(CategoryTheory): The finite pretopology on a category t-category-theory delegated awaiting review
29493 kim-em chore: grind golf in Mathlib.Logic t-logic ready-to-merge awaiting review
29536 kim-em chore: minor grind golfing in Logic/Embedding t-logic ready-to-merge awaiting bors
29219 euprunin chore: remove redundant `obtain` invocations t-algebra ready-to-merge awaiting bors
29479 harahu doc: move docstring references to definitions to correct locations t-computability awaiting review
29239 harahu doc: Hyphenize compound adjectives ending in "-valued" ready-to-merge awaiting bors
29327 loefflerd feat(NumberTheory/ModularForms): Cusps of subgroups acting on upper half-plane t-number-theory awaiting review
28451 yapudpill feat(RingTheory/Noetherian): add `IsNoetherianRing.of_prime` t-ring-theory new-contributor awaiting-author 🟤 running CI
28858 themathqueen feat(LinearAlgebra/Matrix/PosDef): inner product on matrices induced by positive definite matrix t-algebra awaiting review
14426 adomani dev: `#min_imps` command merge-conflict WIP labelled WIP
14167 alreadydone feat: Group scheme structure on Weierstrass curve workshop-AIM-AG-2024 t-algebraic-geometry merge-conflict WIP labelled WIP
13847 alreadydone feat(EllipticCurve): the universal elliptic curve t-algebra t-algebraic-geometry merge-conflict awaiting-author merge conflict
13297 urkud feat(Semicontinuous): add `comp` lemma t-order t-topology merge-conflict awaiting-author merge conflict
12679 MichaelStollBayreuth perf(NumberTheory/RamificationInertia): speed up slow file merge-conflict WIP labelled WIP
12608 eric-wieser feat: allow `nsmul` / `zsmul` to be omitted again, with a warning t-algebra t-meta merge-conflict awaiting-author merge conflict
12934 grunweg chore: replace more uses of > or ≥ by < or ≤ merge-conflict awaiting-author help-wanted looking for help
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
12192 Ruben-VandeVelde feat: generalize isLittleO_const_id_atTop/atBot t-analysis merge-conflict awaiting-author merge conflict
11617 urkud refactor(Finset): redefine Finset.diag, review API t-logic merge-conflict awaiting-author merge conflict
10444 urkud doc(IsROrC): expand the docstring t-analysis merge-conflict awaiting-author documentation merge conflict
10594 lecopivo feat: `fun_trans` function transformation tactic e.g. for computing derivatives t-meta merge-conflict WIP labelled WIP
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
10024 ADedecker feat: rename `connectedComponentOfOne` to `identityComponent`, prove that it is normal and open t-topology awaiting-CI merge-conflict does not pass CI
10521 eric-wieser chore: generalize `IsBoundedLinearMap` to modules t-analysis merge-conflict awaiting-author merge conflict
9229 eric-wieser refactor(Algebra/GradedMonoid): Use `HMul` to define `GMul` t-algebra merge-conflict WIP labelled WIP
8906 jjaassoonn feat: add some missing lemmas about linear algebra t-algebra merge-conflict awaiting-author failing CI
8788 FMLJohn feat(Algebra/Module/GradeZeroModule): if `A` is a graded semiring and `M` is a graded `A`-module, then each grade of `M` is a module over the 0-th grade of `A`. t-algebra merge-conflict merge conflict
9146 laughinggas feat(Data/ZMod/Defs): Topological structure on `ZMod` t-algebra t-topology merge-conflict awaiting-author merge conflict
9356 alexjbest feat: assumption? t-meta merge-conflict awaiting-author merge conflict
9570 eric-wieser feat(Algebra/Star): Non-commutative generalization of `StarModule` t-algebra awaiting-CI merge-conflict WIP labelled WIP
9354 chenyili0818 feat: monotonicity of gradient on convex real-valued functions t-analysis 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
8961 eric-wieser refactor: use the coinduced topology on ULift awaiting-CI merge-conflict please-adopt awaiting-author looking for help
8658 eric-wieser feat: support right actions for `Con` t-algebra merge-conflict awaiting-author merge conflict
9642 eric-wieser refactor(Analysis/Normed/{Group/Field}/Basic): Let `extends` generate the repeated fields t-analysis merge-conflict awaiting-author WIP help-wanted looking for help
6630 MohanadAhmed feat: Reduced Spectral Theorem t-algebra merge-conflict WIP labelled WIP
6580 adomani chore: `move_add`-driven replacements merge-conflict awaiting-author merge conflict
7909 mcdoll fix(Tactic/Continuity): remove npowRec and add new tag for Continuous.pow t-topology t-meta 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
7467 ADedecker feat: spectrum of X →ᵇ ℂ is StoneCech X t-analysis merge-conflict WIP labelled WIP
7427 MohanadAhmed Mohanad ahmed/sort eigenvalues abs merge-conflict WIP labelled WIP
7227 kmill feat: flexible binders and integration into notation3 t-meta merge-conflict WIP labelled WIP
7962 eric-wieser feat: `DualNumber (Quaternion R)` as a `CliffordAlgebra` t-algebra merge-conflict WIP labelled WIP
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
6777 adomani chore(Co*variantClass): replace eta-expanded (· * ·), (· + ·), (· ≤ ·), (· < ·) merge-conflict merge conflict
7835 shuxuezhuyi feat(LinearAlgebra/Matrix): `lift` for projective special linear group t-algebra merge-conflict awaiting-author ??? missing CI information
7932 eric-wieser refactor(Algebra/TrivSqZeroExt): replace with a structure t-algebra awaiting-CI merge-conflict does not pass CI
6930 kmill feat: `resynth_instances` tactic for resynthesizing instances in the goal or local context t-meta merge-conflict WIP labelled WIP
7615 eric-wieser chore(LinearAlgebra/Basic): generalize compatibleMaps to semilinear maps t-algebra awaiting-CI easy merge-conflict does not pass CI
6931 urkud refactor(Analysis/Normed*): use `RingHomIsometric` for `*.norm_cast` t-analysis merge-conflict help-wanted looking for help
7601 digama0 feat: ring hom support in `ring` t-algebra t-meta merge-conflict awaiting-author merge conflict
7351 shuxuezhuyi feat(Topology/Algebra/Order): extend function on `Ioo` to `Icc` t-order merge-conflict awaiting-author merge conflict
7713 RemyDegenne feat: add_left/right_inj for measures t-measure-probability merge-conflict awaiting-author merge conflict
6002 slerpyyy feat(Analysis.SpecialFunctions.Gaussian): add `integrable_fun_mul_exp_neg_mul_sq` t-analysis 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
6195 eric-wieser chore(RingTheory/TensorProduct): golf the `mul` definition t-algebra awaiting-CI merge-conflict does not pass CI
5934 eric-wieser feat: port Data.Rat.MetaDefs t-meta merge-conflict mathlib-port help-wanted looking for help
4127 kmill refactor: create HasAdj class, define Digraph, and generalize some SimpleGraph API t-combinatorics merge-conflict awaiting-author merge conflict
6328 astrainfinita chore: make some instance about `Sub...Class` lower priority t-algebra awaiting-CI merge-conflict WIP labelled WIP
5912 ADedecker feat(Analysis.Distribution.ContDiffMapSupportedIn): space of smooth maps with support in a fixed compact t-analysis merge-conflict WIP labelled WIP
6590 mcdoll feat: composition of LinearPMaps t-algebra merge-conflict WIP labelled WIP
6210 MohanadAhmed feat(Data/IsROrC/Basic): add a `StarOrderedRing` instance t-algebra t-analysis 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
5133 kmill feat: IntermediateField adjoin syntax for sets of elements t-algebra merge-conflict WIP labelled WIP
3808 kim-em feat: #formalize, backed by a choice of LLMs t-meta merge-conflict awaiting-author merge conflict
4960 eric-wieser chore: use `open scoped` awaiting-CI merge-conflict does not pass CI
6079 eric-wieser fix: deduplicate variables awaiting-CI merge-conflict does not pass CI
6633 adomani feat(..Polynomial..): `MvPolynomial`s have no zero divisors t-algebra merge-conflict awaiting-author merge conflict
7076 grunweg feat: define measure zero subsets of a manifold t-measure-probability t-differential-geometry merge-conflict WIP labelled WIP
6330 astrainfinita chore: make some instance about `Sub...Class` higher priority than `Sub...` slow-typeclass-synthesis t-algebra merge-conflict WIP labelled WIP
6993 jjaassoonn feat : lemmas about `AddMonoidAlgebra.{divOf, modOf}` t-algebra merge-conflict merge conflict
6403 astrainfinita chore: change instance priorities of `Ordered*` hierarchy slow-typeclass-synthesis t-order t-algebra merge-conflict awaiting-author merge conflict
3757 thorimur feat: config options for `fail_if_no_progress` t-meta merge-conflict WIP labelled WIP
12353 thorimur feat: `conv%` t-meta merge-conflict WIP labelled WIP
7903 urkud feat: define `UnboundedSpace` t-topology merge-conflict help-wanted looking for help
15400 grunweg feat: "confusing variables" linter t-linter merge-conflict WIP labelled WIP
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
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
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
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
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
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
19013 quangvdao feat(Algebra/BigOperators/Fin): Add `finSigmaFinEquiv` t-algebra 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
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
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
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
16062 adomani Test/ci olean size CI merge-conflict awaiting-author WIP labelled WIP
16020 adomani feat: compare PR `olean`s size with `master` CI merge-conflict failing CI
12799 jstoobysmith feat(LinearAlgebra/UnitaryGroup): Add properties of Special Unitary Group new-contributor t-algebra merge-conflict please-adopt awaiting-author looking for help
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
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
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
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
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
23990 robertmaxton42 feat (Types.Colimits): Quot is functorial and colimitEquivQuot is natural new-contributor t-category-theory merge-conflict awaiting-author 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
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
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
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
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
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
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
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
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
26200 adomani fix: add label when landrun fails CI merge-conflict 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
27950 alreadydone feat(MonoidAlgebra): criteria for `single` to be a unit, irreducible or prime t-algebra merge-conflict WIP labelled WIP
27378 peakpoint refactor(Geometry/Euclidean/Projection): redefine projection and reflection for affine subspaces new-contributor t-euclidean-geometry merge-conflict 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
25401 digama0 feat(Util): SuppressSorry option t-meta merge-conflict merge conflict
26394 winstonyin feat: existence of local flows on manifolds t-differential-geometry merge-conflict WIP labelled WIP
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
27446 grunweg chore: more enorm lemmas carleson 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
19097 Vierkantor chore(Algebra.Polynomial): split `Polynomial/Basic.lean` into smaller files t-algebra merge-conflict merge conflict
28622 alreadydone chore(Mathlib): replace `=>` by `↦` merge-conflict merge conflict
24793 tristan-f-r feat: trace of unitarily similar matrices t-algebra merge-conflict awaiting-author merge conflict
28532 alreadydone chore(Algebra/Ring/Defs): add two classes and extend more t-algebra merge-conflict merge conflict
27872 JovanGerb chore(gcongr): clean up imports large-import merge-conflict delegated failing CI
28626 alreadydone chore(Archive, Counterexamples): replace => by ↦ merge-conflict merge conflict
26670 yu-yama feat(GroupExtension/Abelian): define `conjClassesEquivH1` t-algebra merge-conflict merge conflict
27634 agjftucker fix(Analysis/Calculus/Implicit): consistently rename {`map`, `fun`, `function`} to `fun` t-analysis merge-conflict merge conflict
7300 ah1112 feat: synthetic geometry t-euclidean-geometry merge-conflict awaiting-author help-wanted looking for help
23866 kim-em chore: remove `[AtLeastTwo n]` hypothesis from the `NatCast` to `OfNat` instance awaiting-zulip merge-conflict failing CI
13795 astrainfinita perf(Algebra/{Group, GroupWithZero, Ring}/InjSurj): reduce everything t-algebra merge-conflict merge conflict
26009 linesthatinterlace feat: Add `Vector`/`List.Vector` equivalence migrated-from-branch t-data merge-conflict merge conflict
27465 erdOne feat: the definition of nonarchimedean local fields t-number-theory merge-conflict failing CI
24095 lecopivo feat: `fun_prop` for Is(Bounded)LinearMap + notation `fun x ↦L[R] f x` large-import t-algebra merge-conflict merge conflict
25775 emilyriehl feat(AlgebraicTopology/SimplicialSet/NerveAdjunction): to Strict Segal 2 t-algebraic-topology infinity-cosmos t-category-theory merge-conflict awaiting-author merge conflict
28150 Equilibris chore: clean up proofs typevec proofs t-data new-contributor merge-conflict merge conflict
26478 JovanGerb chore(LibraryRewrite): replace `rw??` with `rw?` t-meta merge-conflict merge conflict
27868 grunweg linter indentation playground t-linter merge-conflict WIP labelled WIP
27403 MoritzBeroRoos fix: replace probably erroneous usage of ⬝ (with old \cdot) by · (with \centerdot) new-contributor merge-conflict merge conflict
28042 kckennylau feat(Topology/ValuativeRel): a topological basis indexed by pairs of elements t-ring-theory merge-conflict merge conflict
26015 linesthatinterlace feat: Add high-level generalizations from `MonoidHom` lifts migrated-from-branch t-algebra merge-conflict failing CI
27399 MoritzBeroRoos chore: replace every usage of ⬝ᵥ (with old \cdot) by ·ᵥ (with \centerdot) new-contributor merge-conflict merge conflict
27835 edegeltje feat(Tactic): ring modulo a given characteristic migrated-from-branch large-import t-meta merge-conflict ❌? infrastructure-related CI failing
25889 plp127 fix(Tactic/Widget/Conv): fix various issues t-meta merge-conflict merge conflict
23621 astrainfinita chore: deprecate `LinearOrderedComm{Monoid, Group}WithZero` t-order t-algebra 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
28933 artie2000 WIP chore(Data): correct definition for `single_apply` merge-conflict failing CI
22151 alreadydone feat(RingTheory): a semiprimary ring is Noetherian/Artinian iff its Jacobson radical is fg t-ring-theory merge-conflict merge conflict
27437 kckennylau feat(RingTheory/Valuation): some lemmas about comparing with 1 and 0 and with each other t-ring-theory merge-conflict WIP labelled WIP
28644 kckennylau don't mind me, i just want cache will-close-soon merge-conflict WIP labelled WIP
28708 sjh227 feat (Data) : edit DoublyStochastic, add Stochastic to matrix t-data new-contributor merge-conflict merge conflict
27508 chrisflav feat(RingTheory): height under ring homomorphism t-ring-theory large-import merge-conflict merge conflict
6042 MohanadAhmed feat(LinearAlgebra/Matrix/SVD): Singular Value Decomposition of R or C Matrices t-algebra merge-conflict please-adopt WIP looking for help
28826 alreadydone feat(Category): add `SemimoduleCat` t-category-theory awaiting-CI merge-conflict does not pass CI
27785 staroperator chore(Algebra/Group/Submonoid): golf `Nat.addSubmonoidClosure_one` using `simp` large-import t-algebra merge-conflict merge conflict
28148 kckennylau feat(Matrix): Simproc and Rw-proc for Matrix Transpose t-meta merge-conflict merge conflict
20850 vihdzp chore(Logic/Equiv/Basic): extend `sumCompl` API t-data t-logic merge-conflict awaiting-author merge conflict
25135 vasnesterov WIP/test PR for faster `tauto` large-import t-meta merge-conflict WIP labelled WIP
26510 alreadydone feat(Matroid): exchange lemmas involving closure t-data t-combinatorics merge-conflict merge conflict
29002 grunweg chore: move Data/Real/Irrational to RingTheory file-removed awaiting-zulip merge-conflict awaiting a zulip discussion
29012 grunweg chore: reduce `Topology` imports in `Data` file-removed merge-conflict failing CI
29020 grunweg chore: squeeze a few non-terminal simps merge-conflict awaiting-author failing CI
28224 joelriou feat(AlgebraicTopology): the type of non degenerate simplices of a simplicial set t-algebraic-topology merge-conflict WIP labelled WIP
26931 javra feat(CategoryTheory/Enriched): `V`-enriched isomorphisms infinity-cosmos t-category-theory merge-conflict awaiting-author merge conflict
26912 pechersky chore(Algebra/Ring/Subring): simp tag `Subring.smul_def` maintainer-merge t-algebra merge-conflict merge conflict
22782 alreadydone feat(Topology): étalé space associated to a predicate on sections t-topology merge-conflict merge conflict
27887 JovanGerb feat: `to_dual` attribute large-import t-meta merge-conflict merge conflict
28820 yury-harmonic feat(PeriodicPts, OrderOfElement): add `nontriviality` lemmas merge-conflict ⚠️ merge conflict
25208 erdOne feat(LinearAlgebra): `tensor_induction` macro t-algebra RFC merge-conflict WIP labelled WIP
27817 zhuyizheng feat: add IMO2025P1 IMO new-contributor merge-conflict merge conflict
28803 astrainfinita refactor: unbundle algebra from `ENormed*` awaiting-zulip slow-typeclass-synthesis t-algebra t-analysis merge-conflict awaiting a zulip discussion
23360 kim-em chore: review of `erw` in `Algebra/Homology/DerivedCategory` t-algebra merge-conflict awaiting-author merge conflict
26603 vihdzp refactor(SetTheory/Ordinal/FixedPoint): redefine `Ordinal.deriv` t-set-theory merge-conflict failing CI
25662 erdOne chore: redefine `LocalizedModule` t-algebra merge-conflict failing CI
29345 adomani test: automatically remove deprecations from before 2025-02-31 merge-conflict failing CI
26956 mariainesdff feat(RingTheory/DividedPowers/Basic): add divided power structure on pZp t-ring-theory merge-conflict merge conflict
27566 wwylele feat(Data/Real): Archimedean.embedReal is a ring hom when M is an ordered ring large-import t-data merge-conflict merge conflict
27918 kim-em wip: refactor WithBot/WithTop as structures file-removed merge-conflict failing CI
27972 smmercuri chore: make `Valuation.Completion` a `def` and refactor more of `AdicValuation.lean` t-algebra t-number-theory merge-conflict merge conflict
28151 iehality feat(Computability): r.e. sets are closed under inter/union/projection/composition t-computability merge-conflict awaiting-author merge conflict
12143 adomani feat: generic linter, absorbing `cdot` linter and `attribute [instance] in` linter t-linter merge-conflict ??? missing CI information
26908 robin-carlier feat(CategoryTheory/Monoidal/DayConvolution): alternative ext principle for unitors t-category-theory merge-conflict merge conflict
27150 robin-carlier feat(CategoryTheory/Monoidal/DayConvolution): constructors for braided and symmetric structure on day convolutions monoidal categories t-category-theory merge-conflict merge conflict
26660 strihanje01 feat(Combinatorics/Additive/VerySmallDoubling): weak non-commutative Kneser's theorem large-import new-contributor t-combinatorics merge-conflict merge conflict
27119 robin-carlier feat(CategoryTheory/Monoidal/DayConvolution): constructors for closed monoidal day convolution monoidal structures t-category-theory merge-conflict merge conflict
28411 zcyemi feat(LinearAlgebra/AffineSpace/Simplex/Centroid): define centroid and medians large-import t-algebra merge-conflict failing CI
28623 gilesgshaw feat(Logic/Basic): minor additions and simplification of proofs new-contributor t-logic merge-conflict merge conflict
24692 ScottCarnahan feat (RingTheory/HahnSeries/Basic): isomorphism of Hahn series induced by order isomorphism t-order merge-conflict WIP labelled WIP
25822 ScottCarnahan WIP: experiments with vertex algebras large-import merge-conflict WIP labelled WIP
29061 chrisflav refactor(AlgebraicGeometry): replace `Scheme.Cover` by an `abbrev` for `ZeroHypercover` large-import t-algebraic-geometry merge-conflict merge conflict
28737 astrainfinita refactor: deprecate `MulEquivClass` maintainer-merge t-algebra merge-conflict awaiting-author merge conflict
28944 linesthatinterlace refactor(Order/Hom/Basic): reorder definitions t-order merge-conflict merge conflict
27284 FernandoChu Chore(CategoryTheory/MorphismProperty/MonoFactorization): Factor out mono factorizations new-contributor t-category-theory merge-conflict awaiting-author failing CI
13036 joelriou feat(CategoryTheory/Sites): under certain conditions, cover preserving functors preserve 1-hypercovers t-category-theory merge-conflict WIP labelled WIP
27335 eric-wieser chore(Data/List): use simp-normal-form for boolean equalities t-data merge-conflict failing CI
21965 JovanGerb feat: extensible `push` and `pull` tactics maintainer-merge t-meta merge-conflict merge conflict
28241 alreadydone chore(Data): `SetLike Finset` t-data merge-conflict merge conflict
29442 Vierkantor chore(*): replace remaining `simp? says` with `simp only` merge-conflict merge conflict
29143 RemyDegenne feat(Probability/Decision): basic properties of the Bayes risk t-measure-probability merge-conflict merge conflict
26138 xroblot Development branch (2) large-import merge-conflict WIP labelled WIP
22517 j-loreaux feat: `ℕ+` powers in semigroups large-import merge-conflict WIP ⚠️ labelled WIP
26857 Thmoas-Guan feat(Algebra): define associated graded structure for abelian group t-algebra merge-conflict awaiting-author merge conflict
24794 chrisflav feat(RingTheory/Presentation): core of a presentation t-ring-theory merge-conflict merge conflict
27320 Jlh18 doc (CategoryTheory/Bicategory/Grothendieck): rename Grothendieck to coGrothendieck new-contributor t-category-theory merge-conflict merge conflict
27933 grunweg chore(OrdNode): format code example in code blocks t-data merge-conflict merge conflict
28406 YaelDillies chore: rename `Mon_Class` to `MonObj` t-category-theory merge-conflict merge conflict
29237 harahu doc: capitalize archimedean merge-conflict merge conflict
29353 Vierkantor chore(RingTheory): process porting notes, part 2 t-ring-theory tech debt merge-conflict merge conflict
29596 alreadydone chore(Algebra): extract `Submonoid.IsLocalizationMap` t-algebra merge-conflict merge conflict
13057 alreadydone feat(NumberTheory): characterize elliptic divisibility sequences t-algebra t-number-theory merge-conflict blocked-by-other-PR blocked on another PR
12879 grunweg feat: port ge_or_gt linter from mathlib3 tech debt t-linter 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
8364 thorimur feat: `refine?` t-meta merge-conflict blocked-by-other-PR 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
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
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
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
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
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
24411 joelriou feat(CategoryTheory): descent of morphisms for a pseudofunctor t-category-theory merge-conflict blocked-by-other-PR WIP blocked on another PR
26136 vasnesterov feat(Topology/Instances): Cantor set is homeomorphic to `ℕ → Bool` large-import t-topology merge-conflict blocked-by-other-PR blocked on another PR
26149 vasnesterov feat(Topology): continuous surjection from Cantor set to Hilbert cube large-import t-topology merge-conflict blocked-by-other-PR blocked on another PR
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
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
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
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
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
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
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
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
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
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
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
27228 themathqueen feat: defining the inner product on tensor products t-algebra t-analysis 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
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
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
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
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
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
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
27100 staroperator feat(ModelTheory): Presburger definability and semilinear sets t-logic merge-conflict blocked-by-other-PR blocked on another PR
28067 grunweg Docstring enumerations 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
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
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
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
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
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
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
26985 agjftucker feat(Analysis/Calculus/Implicit): define implicitFunOfBivariate large-import new-contributor t-analysis 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
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
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
27979 smmercuri feat: `RamifiedExtension` and `UnramifiedExtension` types for `InfinitePlace.Extension`s t-number-theory 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
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
23831 vasnesterov feat(Analysis): binomial series convergence t-analysis merge-conflict blocked-by-other-PR 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
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
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
25900 pfaffelh feat (Topology/Compactness/CompactSystem): Set system of finite unions of sets in a compact system is again a compact system t-topology blocked-by-other-PR blocked on another PR
25797 dagurtomas feat(Condensed): closed symmetric monoidal structure on light condensed modules t-condensed merge-conflict blocked-by-other-PR WIP blocked on another PR
19582 yu-yama feat(GroupExtension/Abelian): define `OfMulDistribMulAction.equivH2` new-contributor t-algebra merge-conflict 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
27215 kckennylau feat(AlgebraicGeometry): Define the Zariski site on `CommRingCatᵒᵖ` t-algebraic-geometry 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
26466 robin-carlier feat(AlgebraicTopology/SimplexCategory/Augmented): the canonical monoid object in the augmented simplex category t-algebraic-topology t-category-theory merge-conflict 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
25488 VTrelat feat(SetTheory/ZFC/Rationals): define rationals in ZFC t-set-theory new-contributor merge-conflict 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 WIP 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 WIP 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
27364 101damnations feat(RepresentationTheory/Homological/GroupCohomology): cohomology of finite cyclic groups t-algebra blocked-by-other-PR blocked on another PR
27365 101damnations feat(RepresentationTheory/Homological/GroupHomology): homology of finite cyclic groups t-algebra blocked-by-other-PR blocked on another PR
27366 101damnations feat(RepresentationTheory/Homological/GroupCohomology/Hilbert90): add Hilbert 90 for cyclic groups large-import t-algebra merge-conflict blocked-by-other-PR blocked on another PR
28700 Timeroot feat(ModelTheory): Set.Definable is transitive large-import t-logic blocked-by-other-PR blocked on another PR
28787 alreadydone feat(Counterexamples): a domain whose ring of differences is not a domain large-import t-algebra merge-conflict blocked-by-other-PR blocked on another PR
23920 YaelDillies feat: relation-separated sets t-data blocked-by-other-PR blocked on another PR
28475 astrainfinita chore(Analysis/SpecificLimits/Basic): generalize lemmas t-analysis 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
28685 mitchell-horner feat(Combinatorics/SimpleGraph): prove the minimal-degree version of the Erdős-Stone theorem t-combinatorics merge-conflict blocked-by-other-PR WIP blocked on another PR
28686 mitchell-horner feat(Combinatorics/SimpleGraph): prove the Erdős-Stone theorem t-combinatorics merge-conflict blocked-by-other-PR WIP blocked on another PR
28687 mitchell-horner feat(Combinatorics/SimpleGraph): prove the Erdős-Stone-Simonovits theorem t-combinatorics merge-conflict blocked-by-other-PR WIP blocked on another PR
28689 mitchell-horner feat(Combinatorics/SimpleGraph): prove well-known corollaries of the Erdős-Stone-Simonovits theorem t-combinatorics merge-conflict blocked-by-other-PR WIP blocked on another PR
23460 Timeroot feat: Definition of `Clone` t-algebra blocked-by-other-PR blocked on another PR
29076 yury-harmonic feat(BigOperators/ModEq): new file blocked-by-other-PR ⚠️ blocked on another PR
26890 robin-carlier feat(CategoryTheory/Monoidal/DayConvolution) : more API for `DayFunctor` t-category-theory merge-conflict blocked-by-other-PR blocked on another PR
26952 robin-carlier feat(CategoryTheory/DayConvolution): monoid objects internal to day convolutions t-category-theory merge-conflict 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 merge-conflict 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 merge-conflict 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 merge-conflict blocked-by-other-PR blocked on another PR
29080 vihdzp feat: `Colex` order on pi types t-order blocked-by-other-PR blocked on another PR
23181 YaelDillies refactor(Topology/UniformSpace): use `SetRel` t-topology 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
28819 ScottCarnahan feat (Data/Finsupp): define convolution smul for finsupps on formal functions blocked-by-other-PR ⚠️ blocked on another PR
28893 joelriou refactor(AlgebraicTopology): redefine the topological simplex using the convexity API t-algebraic-topology t-convex-geometry large-import blocked-by-other-PR blocked on another PR
28013 astrainfinita feat: Lindemann-Weierstrass Theorem t-algebra t-analysis merge-conflict blocked-by-other-PR WIP blocked on another PR
28962 grunweg chore: enable the flexible linter in mathlib merge-conflict blocked-by-other-PR blocked on another PR
26413 michaellee94 feat(Analysis/ODE/MaximalSolution): Existence of maximal solutions for ODE meeting Picard-Lindelöf conditions new-contributor t-analysis merge-conflict awaiting-author blocked-by-other-PR blocked on another PR
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
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
28346 joelriou feat(AlgebraicTopology/SimplicialSet): rank functions for pairings 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
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
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
26291 RemyDegenne feat(Probability): Fernique's theorem and Cameron-Martin theorem t-measure-probability blocked-by-other-PR WIP 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 merge-conflict blocked-by-other-PR 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
28786 mitchell-horner feat(Combinatorics/SimpleGraph): restate Turán's theorem in terms of `extremalNumber` t-combinatorics blocked-by-other-PR 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
27707 FLDutchmann feat(NumberTheory/SelbergSieve): define Selberg's weights and prove basic results. t-analysis t-number-theory merge-conflict blocked-by-other-PR blocked on another PR
27898 grunweg feat: check indentation of doc-strings, basic version t-linter merge-conflict blocked-by-other-PR blocked on another PR
29164 vlad902 feat(SimpleGraph): Hall's Marriage Theorem for bipartite graphs t-combinatorics blocked-by-other-PR blocked on another PR
28126 Sebi-Kumar feat(AlgebraicTopology/FundamentalGroupoid): relate equality in fundamental groupoid to homotopy t-algebraic-topology new-contributor awaiting-author 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
29283 Jlh18 feat(CategoryTheory): define forgetful-core adjunction between Cat and Grpd new-contributor blocked-by-other-PR ⚠️ blocked on another PR
29282 Jlh18 feat(CategoryTheory): HasColimits instance onGrpd new-contributor blocked-by-other-PR ⚠️ blocked on another PR
29284 Jlh18 feat(CategoryTheory): naturality lemmas for Core construction new-contributor 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 WIP blocked on another PR
27706 xroblot feat(RingTheory/Localization/AtPrime): inertia degree and ramification index are preserved by localization t-ring-theory blocked-by-other-PR WIP 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 merge-conflict blocked-by-other-PR blocked on another PR
28972 themathqueen feat(LinearAlgebra/Matrix): star-algebra automorphisms on matrices are unitarily inner t-algebra blocked-by-other-PR 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
27314 pechersky feat(TopologyValued): `Valued` based on a range topology t-topology merge-conflict blocked-by-other-PR blocked on another PR
29258 mans0954 feature(Analysis/LocallyConvex/WeakSpace): weak closed convex hull equals closed convex hull t-analysis blocked-by-other-PR blocked on another PR
29342 mans0954 refactor(Analysis/LocallyConvex/AbsConvex): Redefine AbsConvex to use a single ring of scalars t-analysis blocked-by-other-PR blocked on another PR
29343 themathqueen feat(LinearAlgebra/TensorProduct/Basic): add `range_map_mono` t-algebra blocked-by-other-PR blocked on another PR
29378 mans0954 feature(Analysis/LocallyConvex/AbsConvex): Balanced and AbsConvex sets under linear maps t-analysis blocked-by-other-PR blocked on another PR
29387 mans0954 feature(Analysis/LocallyConvex/WeakSpace): toWeakSpace_closedAbsConvexHull_eq t-analysis 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
29425 pechersky feat(NumberTheory/Padics/Torsion): `HasEnoughRootsOfUnity ℤ_[p] (p - 1)` t-ring-theory blocked-by-other-PR blocked on another PR
29424 pechersky feat(RingTheory/ZMod): `HasEnoughRootsOfUnity (ZMod p) (p - 1)` t-ring-theory blocked-by-other-PR blocked on another PR
29418 jsm28 feat(Analysis/Convex/Between): interior of a 1-simplex t-convex-geometry blocked-by-other-PR blocked on another PR
29415 jsm28 feat(Data/Finset/Max): `min'_pair`, `max'_pair` t-data 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
28796 grunweg feat: immersions are smooth t-differential-geometry merge-conflict blocked-by-other-PR WIP blocked on another PR
28853 grunweg feat: product of immersions is an immersion t-differential-geometry merge-conflict blocked-by-other-PR blocked on another PR
28865 grunweg feat: a map is smooth iff its post-composition with an immersion is t-differential-geometry merge-conflict blocked-by-other-PR WIP blocked on another PR
28905 grunweg feat: immersions are locally embeddings merge-conflict blocked-by-other-PR ⚠️ blocked on another PR
29077 grunweg feat(Manifold/Instances/Icc): golf smoothness proof using immersions merge-conflict blocked-by-other-PR ⚠️ blocked on another PR
25737 robin-carlier feat(AlgebraicTopology/SimplexCategory/GeneratorsRelations/NormalForms): Normal forms for `P_δ`s t-algebraic-topology large-import t-category-theory 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
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
26217 Thmoas-Guan feat(Algebra): Ischebeck theorem 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
29447 j-loreaux chore(Analysis/NormedSpace/HahnBanach): move and split files file-removed merge-conflict blocked-by-other-PR blocked on another PR
29472 chrisflav feat(CategoryTheory/Sites): functoriality of precoverages and `0`-hypercovers t-category-theory merge-conflict 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
28804 grunweg feat: a few more tactic linters t-meta merge-conflict 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
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
29508 zhuyizheng feat(MeasureTheory): FTC and integration by parts for absolutely continuous functions new-contributor t-measure-probability blocked-by-other-PR blocked on another PR
29507 zhuyizheng feat(MeasureTheory): derivative integrable functions new-contributor t-measure-probability blocked-by-other-PR blocked on another PR
29116 scholzhannah chore(Topology/PartialHomeomorph): add module deprecation 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
29533 Thmoas-Guan feat(Algebra): maximal Cohen Macaulay module large-import blocked-by-other-PR ⚠️ blocked on another PR
29000 JovanGerb feat(Tactic/Push): add basic tags and tests merge-conflict blocked-by-other-PR ⚠️ blocked on another PR
29519 joelriou feat(CategoryTheory): strong generators t-category-theory blocked-by-other-PR WIP blocked on another PR
29543 joelriou feat(CategoryTheory): a set S of objects is a strong generator if any object is a colimit of objects in S large-import t-category-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
29555 RemyDegenne feat(Probability): `condDistrib` lemmas t-measure-probability blocked-by-other-PR blocked on another PR
29557 Thmoas-Guan feat(Algebra): finite projective dimension of regular large-import blocked-by-other-PR ⚠️ blocked on another PR
26651 loefflerd WIP: modular forms for subgroups not contained in SL2Z t-number-theory blocked-by-other-PR WIP blocked on another PR
29204 ShreckYe feat(GroupTheory/OrderOfElement): `Pi.orderOf_eq` and its related and depended-upon theorems related to `Pi`, `minimalPeriod`, and `IsPeriodicPt` t-group-theory large-import t-dynamics merge-conflict blocked-by-other-PR blocked on another PR
29279 Jlh18 feat: free groupoid on a category, free-forgetful adjunction large-import new-contributor blocked-by-other-PR ⚠️ blocked on another PR
29274 Jlh18 feat(CategoryTheory): HasLimits instance on Grpd large-import new-contributor blocked-by-other-PR ⚠️ blocked on another PR
29561 j-loreaux feat: range of the continuous functional calculus t-analysis blocked-by-other-PR blocked on another PR
29565 joelriou feat(CategoryTheory): dense functors large-import t-category-theory blocked-by-other-PR WIP blocked on another PR
25799 dagurtomas feat(CategoryTheory): the universal property of localized monoidal categories t-category-theory blocked-by-other-PR blocked on another PR
29579 vlad902 feat(SimpleGraph): characterize graphs with chromatic number 1 or 2 t-combinatorics 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
29314 Louddy feat(SkewMonoidAlgebra): Lifts for skew monoid algebras 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 awaiting-author 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
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
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
25794 dagurtomas feat(CategoryTheory): localization preserves braided structure file-removed t-category-theory blocked-by-other-PR blocked on another PR
26588 faenuccio feat(Algebra/GroupWithZero/WithZero): add the multiplicative embedding with zero from the range t-order t-algebra blocked-by-other-PR blocked on another PR
27579 RemyDegenne feat: risk of an estimator, DeGroot statistical information, total variation distance t-measure-probability merge-conflict blocked-by-other-PR WIP blocked on another PR
29243 yoh-tanimoto feat(Analysis/InnerProductSpace/Projection/Submodule): add `sup_orthogonal` for `ClosedSubmodules` merge-conflict blocked-by-other-PR ⚠️ blocked on another PR
29251 yoh-tanimoto feat(Analysis/InnerProductSpace/): define standard subspaces of a complex Hilbert space merge-conflict blocked-by-other-PR ⚠️ blocked on another PR
26858 Thmoas-Guan feat(Algebra): Define the associated graded ring to filtered ring t-algebra merge-conflict blocked-by-other-PR blocked on another PR
26859 Thmoas-Guan feat(Algebra): Define associated graded algebra t-algebra merge-conflict blocked-by-other-PR blocked on another PR
26860 Thmoas-Guan feat(Algebra): Define associated graded module t-algebra merge-conflict blocked-by-other-PR blocked on another PR
26861 Thmoas-Guan feat(Algebra): define filtered add group hom t-algebra merge-conflict blocked-by-other-PR blocked on another PR
26862 Thmoas-Guan feat(Algebra): define filtered ring homomorphism t-algebra merge-conflict blocked-by-other-PR blocked on another PR
26863 Thmoas-Guan feat(Algebra): define filtered alghom t-algebra merge-conflict blocked-by-other-PR blocked on another PR
26867 Thmoas-Guan feat(Algebra): filtered module hom t-algebra merge-conflict blocked-by-other-PR blocked on another PR
26868 Thmoas-Guan feat(Algebra): associated graded exact of exact and strict t-algebra merge-conflict blocked-by-other-PR blocked on another PR
26869 Thmoas-Guan feat(Algebra): exact of associated graded exact t-algebra merge-conflict blocked-by-other-PR blocked on another PR
28468 alreadydone feat(Algebra): ring API for `AddLocalization` t-algebra merge-conflict awaiting-author blocked-by-other-PR blocked on another PR
28769 chrisflav feat(RingTheory/Extension/Cotangent): presentation is submersive if `I/I²` has a suitable basis t-ring-theory large-import merge-conflict blocked-by-other-PR blocked on another PR
28797 xroblot feat(DedekindDomain/Ideal): `relNorm` of a prime ideal large-import merge-conflict blocked-by-other-PR ❌? ⚠️ blocked on another PR
29560 loefflerd feat(NumberTheory/ModularForms): define boundedness / vanishing at a cusp t-number-theory blocked-by-other-PR blocked on another PR