Why is my PR not on the queue?

This page was last updated on: January 11, 2026 at 17:05 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
13847 alreadydone feat(EllipticCurve): the universal elliptic curve awaiting-author merge-conflict t-algebraic-geometry t-algebra merge conflict
14167 alreadydone feat: Group scheme structure on Weierstrass curve WIP merge-conflict t-algebraic-geometry workshop-AIM-AG-2024 labelled WIP
13297 urkud feat(Semicontinuous): add `comp` lemma awaiting-author merge-conflict t-topology t-order merge conflict
12608 eric-wieser feat: allow `nsmul` / `zsmul` to be omitted again, with a warning awaiting-author merge-conflict t-meta t-algebra merge conflict
12679 MichaelStollBayreuth perf(NumberTheory/RamificationInertia): speed up slow file WIP merge-conflict labelled WIP
12879 grunweg feat: port ge_or_gt linter from mathlib3 blocked-by-other-PR merge-conflict t-linter tech debt blocked on another PR
12933 grunweg chore: replace some use of > or ≥ by < or ≤ awaiting-author merge-conflict failing CI
12934 grunweg chore: replace more uses of > or ≥ by < or ≤ help-wanted awaiting-author merge-conflict looking for help
13057 alreadydone feat(NumberTheory): characterize elliptic divisibility sequences blocked-by-other-PR merge-conflict t-number-theory t-algebra blocked on another PR
11617 urkud refactor(Finset): redefine Finset.diag, review API awaiting-author merge-conflict t-logic merge conflict
12192 Ruben-VandeVelde feat: generalize isLittleO_const_id_atTop/atBot awaiting-author merge-conflict t-analysis merge conflict
10024 ADedecker feat: rename `connectedComponentOfOne` to `identityComponent`, prove that it is normal and open merge-conflict awaiting-CI t-topology does not pass CI
10521 eric-wieser chore: generalize `IsBoundedLinearMap` to modules awaiting-author merge-conflict t-analysis merge conflict
10594 lecopivo feat: `fun_trans` function transformation tactic e.g. for computing derivatives WIP merge-conflict t-meta labelled WIP
10721 urkud feat(Order/FunLike): define `PointwiseLE` merge-conflict t-order t-logic ??? missing CI information
10842 mcdoll chore: simplify proofs using new positivity extensions and tests WIP blocked-by-other-PR merge-conflict blocked on another PR
11100 eric-wieser feat(CategoryTheory/Limits): add `Functor.mapBinaryBiconeInv` merge-conflict awaiting-CI t-category-theory does not pass CI
8503 thorimur feat: meta utils for `refine?` awaiting-author merge-conflict t-meta merge conflict
8519 eric-wieser refactor(LinearAlgebra/TensorProduct): golf using `liftAddHom` awaiting-author merge-conflict t-algebra merge conflict
8616 eric-wieser feat(Algebra/FreeAlgebra): add right action and `IsCentralScalar` merge-conflict awaiting-CI t-algebra does not pass CI
8658 eric-wieser feat: support right actions for `Con` awaiting-author merge-conflict t-algebra merge conflict
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`. merge-conflict t-algebra merge conflict
8906 jjaassoonn feat: add some missing lemmas about linear algebra awaiting-author merge-conflict t-algebra failing CI
8961 eric-wieser refactor: use the coinduced topology on ULift awaiting-author please-adopt merge-conflict awaiting-CI looking for help
9146 laughinggas feat(Data/ZMod/Defs): Topological structure on `ZMod` awaiting-author merge-conflict t-topology t-algebra merge conflict
9229 eric-wieser refactor(Algebra/GradedMonoid): Use `HMul` to define `GMul` WIP merge-conflict t-algebra labelled WIP
9354 chenyili0818 feat: monotonicity of gradient on convex real-valued functions awaiting-author merge-conflict t-analysis merge conflict
9356 alexjbest feat: assumption? awaiting-author merge-conflict t-meta merge conflict
9469 dupuisf feat: maximum modulus principle for functions vanishing at infinity awaiting-author t-analysis awaiting author
9487 eric-wieser feat: the exponential of dual numbers over non-commutative rings WIP merge-conflict t-analysis t-algebra t-measure-probability labelled WIP
9510 eric-wieser feat(Analysis/Calculus/DualNumber): Extending differentiable functions to dual numbers WIP awaiting-CI t-analysis t-algebra labelled WIP
9570 eric-wieser feat(Algebra/Star): Non-commutative generalization of `StarModule` WIP merge-conflict awaiting-CI t-algebra labelled WIP
9642 eric-wieser refactor(Analysis/Normed/{Group/Field}/Basic): Let `extends` generate the repeated fields help-wanted WIP awaiting-author merge-conflict t-analysis looking for help
6580 adomani chore: `move_add`-driven replacements awaiting-author merge-conflict merge conflict
6630 MohanadAhmed feat: Reduced Spectral Theorem WIP merge-conflict t-algebra labelled WIP
6777 adomani chore(Co*variantClass): replace eta-expanded (· * ·), (· + ·), (· ≤ ·), (· < ·) merge-conflict merge conflict
6791 eric-wieser refactor: Use flat structures for morphisms help-wanted awaiting-author merge-conflict awaiting-CI looking for help
6930 kmill feat: `resynth_instances` tactic for resynthesizing instances in the goal or local context WIP merge-conflict t-meta labelled WIP
6931 urkud refactor(Analysis/Normed*): use `RingHomIsometric` for `*.norm_cast` help-wanted merge-conflict t-analysis ??? looking for help
7227 kmill feat: flexible binders and integration into notation3 WIP merge-conflict t-meta labelled WIP
7351 shuxuezhuyi feat(Topology/Algebra/Order): extend function on `Ioo` to `Icc` awaiting-author merge-conflict t-order merge conflict
7467 ADedecker feat: spectrum of X →ᵇ ℂ is StoneCech X WIP merge-conflict t-analysis labelled WIP
7564 shuxuezhuyi feat(Topology/Algebra/Order): extend strictly monotone function on `Ioo` to homeomorphism on `Icc` blocked-by-other-PR merge-conflict t-topology blocked on another PR
7601 digama0 feat: ring hom support in `ring` awaiting-author merge-conflict t-meta t-algebra merge conflict
7615 eric-wieser chore(LinearAlgebra/Basic): generalize compatibleMaps to semilinear maps merge-conflict easy awaiting-CI t-algebra does not pass CI
7713 RemyDegenne feat: add_left/right_inj for measures awaiting-author merge-conflict t-measure-probability merge conflict
7835 shuxuezhuyi feat(LinearAlgebra/Matrix): `lift` for projective special linear group awaiting-author merge-conflict t-algebra ??? missing CI information
7875 astrainfinita chore: make `SMulCommClass A A B` and `SMulCommClass A B B` higher priority merge-conflict t-algebra slow-typeclass-synthesis ??? missing CI information
7909 mcdoll fix(Tactic/Continuity): remove npowRec and add new tag for Continuous.pow WIP merge-conflict t-meta t-topology labelled WIP
7932 eric-wieser refactor(Algebra/TrivSqZeroExt): replace with a structure merge-conflict awaiting-CI t-algebra does not pass CI
7962 eric-wieser feat: `DualNumber (Quaternion R)` as a `CliffordAlgebra` WIP merge-conflict t-algebra labelled WIP
8364 thorimur feat: `refine?` blocked-by-other-PR merge-conflict t-meta blocked on another PR
4871 j-loreaux feat: define the additive submonoid of positive elements in a star ordered ring merge-conflict awaiting-CI t-algebra ??? does not pass CI
5133 kmill feat: IntermediateField adjoin syntax for sets of elements WIP merge-conflict t-algebra labelled WIP
5912 ADedecker feat(Analysis.Distribution.ContDiffMapSupportedIn): space of smooth maps with support in a fixed compact WIP merge-conflict t-analysis labelled WIP
6002 slerpyyy feat(Analysis.SpecialFunctions.Gaussian): add `integrable_fun_mul_exp_neg_mul_sq` awaiting-author merge-conflict t-analysis merge conflict
6079 eric-wieser fix: deduplicate variables merge-conflict awaiting-CI does not pass CI
6195 eric-wieser chore(RingTheory/TensorProduct): golf the `mul` definition merge-conflict awaiting-CI t-algebra does not pass CI
6210 MohanadAhmed feat(Data/IsROrC/Basic): add a `StarOrderedRing` instance WIP merge-conflict t-analysis t-algebra labelled WIP
6328 FR-vdash-bot chore: make some instance about `Sub...Class` lower priority WIP merge-conflict awaiting-CI t-algebra labelled WIP
6330 astrainfinita chore: make some instance about `Sub...Class` higher priority than `Sub...` WIP merge-conflict t-algebra slow-typeclass-synthesis labelled WIP
6403 astrainfinita chore: change instance priorities of `Ordered*` hierarchy awaiting-author merge-conflict t-algebra t-order slow-typeclass-synthesis merge conflict
6491 eric-wieser chore(Mathlib/Algebra/Hom/GroupAction): add `SMulHomClass.comp_smul` merge-conflict t-algebra merge conflict
7076 grunweg feat: define measure zero subsets of a manifold WIP merge-conflict t-differential-geometry t-measure-probability labelled WIP
3757 thorimur feat: config options for `fail_if_no_progress` WIP merge-conflict t-meta labelled WIP
12353 thorimur feat: `conv%` WIP merge-conflict t-meta labelled WIP
7903 urkud feat: define `UnboundedSpace` help-wanted merge-conflict t-topology looking for help
15400 grunweg feat: "confusing variables" linter WIP merge-conflict t-linter labelled WIP
15679 adomani test: refactor in CI WIP merge-conflict labelled WIP
7565 shuxuezhuyi feat(Topology/Algebra/Order): extend homeomorphism of `Ioo` to `Icc` blocked-by-other-PR merge-conflict t-topology t-order blocked on another PR
10629 madvorak feat: List.cons_sublist_append_iff_right merge-conflict t-data merge conflict
9973 Ruben-VandeVelde feat: polynomials formed by lists please-adopt merge-conflict t-data looking for help
12926 joelriou feat(CategoryTheory): the monoidal category structure induced by a monoidal functor WIP merge-conflict t-category-theory labelled WIP
12869 adomani feat: linter and script for `theorem` vs `lemma` awaiting-author merge-conflict t-linter merge conflict
14563 awueth feat: if-then-else of exclusive or statement awaiting-author t-algebra new-contributor awaiting author
12093 ADedecker feat: tweak the definition of semicontinuity to behave better in nonlinear orders WIP merge-conflict t-topology labelled WIP
11393 mcdoll feat(Analysis/Distribution/SchwartzSpace): The Heine-Borel property WIP merge-conflict t-analysis labelled WIP
9444 erdOne feat: Various instances regarding `𝓞 K`. help-wanted merge-conflict t-number-theory looking for help
8931 hmonroe feat(Computable): define P, NP, and NP-complete awaiting-author merge-conflict t-computability failing CI
10387 adomani feat(Tactic/ComputeDegree): add `polynomial` tactic WIP t-meta RFC labelled WIP
8608 eric-wieser feat: multiplicativize `AddTorsor` WIP merge-conflict t-algebra labelled WIP
9154 FR-vdash-bot feat: `npow` / `nsmul` / `Nat.cast`/ `zpow` / `zsmul` implemented using `Nat.binaryRec` blocked-by-other-PR awaiting-author merge-conflict t-algebra blocked on another PR
6603 tydeu feat: automatically try `cache get` before build WIP merge-conflict CI labelled WIP
6058 apurvnakade feat: duality theory for cone programs WIP merge-conflict t-analysis labelled WIP
6449 ADedecker feat: functions with finite fibers awaiting-author merge-conflict t-topology failing CI
13163 erdOne feat(.vscode/module-docstring.code-snippet): Prevent auto-complete from firing on `do` awaiting-author t-meta awaiting author
13791 digama0 refactor: Primrec and Partrec merge-conflict t-computability tech debt merge conflict
11964 adamtopaz feat: The functor of points of a scheme merge-conflict t-category-theory t-algebraic-geometry merge conflict
12418 rosborn style: replace preimage_val with ↓∩ notation merge-conflict merge conflict
9978 FR-vdash-bot chore(FieldTheory/KummerExtension): move some lemmas earlier awaiting-author merge-conflict t-algebra merge conflict
12429 adomani feat: toND -- auto-generating natDegree awaiting-author merge-conflict t-meta RFC t-algebra merge conflict
12751 Command-Master feat: add lemmas for Nat/Bits, Nat/Bitwise and Nat/Size merge-conflict new-contributor t-data merge conflict
15448 urkud chore(*): deprecate `Option.elim'` awaiting-author merge-conflict tech debt ??? missing CI information
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 merge-conflict t-data ??? missing CI information
13573 Shamrock-Frost feat: add multivariate polynomial modules awaiting-author merge-conflict t-algebra merge conflict
6517 MohanadAhmed feat: discrete Fourier transform of a finite sequence awaiting-author merge-conflict t-algebra merge conflict
13155 alreadydone feat(NumberTheory/EllipticDivisibilitySequence): show elliptic relations follow from even-odd recursion awaiting-author merge-conflict t-number-theory t-algebra merge conflict
15600 adomani feat: lint also `let` vs `have` WIP merge-conflict t-linter labelled WIP
16253 Shreyas4991 feat: Basics of Discrete Fair Division in Mathlib WIP awaiting-author ⚠️ labelled WIP
15121 Eloitor feat: iff theorems for IsSplitEpi and IsSplitMono in opposite category awaiting-author t-category-theory new-contributor failing CI
15895 madvorak feat(Computability/ContextFreeGrammar): mapping between two types of nonterminal symbols WIP t-computability labelled WIP
14038 adomani test/decl diff in lean dev WIP merge-conflict labelled WIP
7861 shuxuezhuyi feat(Geometry/Hyperbolic/UpperHalfPlane): instance IsometricSMul PSL(2, ℝ) ℍ blocked-by-other-PR merge-conflict t-euclidean-geometry blocked on another PR
16570 yuma-mizuno chore(Tactic/CategoryTheory): change `TermElabM` to `MetaM` WIP t-meta labelled WIP
10591 adri326 feat(Topology/Algebra/ConstMulAction): properties of continuous actions in Hausdorff spaces awaiting-author t-topology t-algebra awaiting author
7545 shuxuezhuyi feat: APIs of `Function.extend f g e'` when `f` is injective awaiting-author merge-conflict t-logic merge conflict
14078 Ruben-VandeVelde feat(CI): continue after mk_all fails awaiting-author merge-conflict CI failing CI
11283 hmonroe feat(ModelTheory/Satisfiability): define theory with independent sentence WIP merge-conflict t-logic labelled WIP
16914 siddhartha-gadgil Loogle syntax with non-reserved WIP merge-conflict labelled WIP
13782 alreadydone feat(EllipticCurve): ZSMul formula in terms of division polynomials blocked-by-other-PR merge-conflict t-number-theory t-algebraic-geometry t-algebra blocked on another PR
8118 iwilare feat(CategoryTheory): add dinatural transformations awaiting-author merge-conflict t-category-theory merge conflict
14242 js2357 feat: Prove equivalence of `isDedekindDomain` and `isDedekindDomainDvr` blocked-by-other-PR merge-conflict t-algebra new-contributor blocked on another PR
7516 ADedecker perf: use `abbrev` to prevent unifying useless data WIP merge-conflict labelled WIP
16215 adomasbaliuka feat(Tactic/Linter): lint unwanted unicode blocked-by-other-PR merge-conflict t-linter blocked on another PR
17127 FR-vdash-bot chore: remove global `Quotient.mk` `⟦·⟧` notation merge-conflict t-data merge conflict
16887 metinersin feat(ModelTheory/Complexity): define conjunctive and disjunctive formulas blocked-by-other-PR merge-conflict t-logic new-contributor blocked on another PR
16888 metinersin feat(ModelTheory/Complexity): Define conjunctive and disjunctive normal forms blocked-by-other-PR merge-conflict t-logic new-contributor blocked on another PR
16889 metinersin feat(ModelTheory/Complexity): Normal forms blocked-by-other-PR merge-conflict t-logic new-contributor blocked on another PR
14712 FR-vdash-bot perf: change instance priority and order about `OfNat` delegated merge-conflict t-algebra slow-typeclass-synthesis merge conflict
11500 mcdoll refactor(Topology/Algebra/Module/WeakDual): Clean up awaiting-author merge-conflict t-topology merge conflict
5995 FR-vdash-bot feat: add APIs about `Quotient.choice` awaiting-author merge-conflict RFC t-data merge conflict
8029 alreadydone refactor: Homotopy between Functions not ContinuousMaps merge-conflict RFC t-topology merge conflict
13156 erdOne refactor(Algebra/Module/LocalizedModule): Redefine `LocalizedModule` in terms of `OreLocalization`. merge-conflict t-algebra failing CI
16348 urkud refactor(Topology): require `LinearOrder` with `OrderTopology` awaiting-author merge-conflict t-topology t-order merge conflict
13965 pechersky feat(Data/DigitExpansion): reals via digit expansion are complete blocked-by-other-PR merge-conflict t-data blocked on another PR
17519 grunweg feat: the `metrisableSpace` linter blocked-by-other-PR merge-conflict t-linter blocked on another PR*
10796 mcdoll feat(Tactic/Positivity): non-negativity of functions WIP t-meta labelled WIP
12750 Command-Master feat: define Gray code blocked-by-other-PR awaiting-author merge-conflict new-contributor t-data blocked on another PR
14603 awueth feat: degree is invariant under graph isomorphism WIP t-combinatorics new-contributor labelled WIP
16925 YnirPaz feat(SetTheory/Cardinal/Cofinality): aleph index of singular cardinal has infinite cofinality WIP merge-conflict t-set-theory labelled WIP
9605 davikrehalt feat(Data/Finset & List): Add Lemmas for Sorting and Filtering awaiting-author please-adopt merge-conflict new-contributor t-data looking for help
13514 madvorak feat(Computability/ContextFreeGrammar): closure under union blocked-by-other-PR merge-conflict t-computability blocked on another PR
17518 grunweg feat: lint on declarations mentioning `Invertible` or `Unique` blocked-by-other-PR merge-conflict t-linter awaiting-zulip blocked on another PR*
9654 urkud feat: add `@[mk_eq]` version of `@[mk_iff]` awaiting-author merge-conflict t-meta merge conflict
16704 AntoineChambert-Loir feat(Mathlib.Data.Ordering.Dickson): Dickson orders WIP merge-conflict t-order labelled WIP
16355 Ruben-VandeVelde feat: odd_{add,sub}_one awaiting-author merge-conflict t-number-theory t-algebra merge conflict
8479 alexjbest feat: use leaff in CI WIP awaiting-author merge-conflict ⚠️ labelled WIP
14598 Command-Master chore: add typeclasses to unify various `add_top`, `add_eq_top`, etc. merge-conflict t-algebra t-order new-contributor merge conflict
16885 metinersin feat(ModelTheory/Complexity): define literals awaiting-author merge-conflict t-logic new-contributor merge conflict
18716 jjaassoonn feat(Algebra/Module/GradedModule): quotient and subgrading WIP blocked-by-other-PR merge-conflict awaiting-CI t-algebra blocked on another PR
9341 winstonyin feat: Naturality of integral curves awaiting-author merge-conflict t-differential-geometry merge conflict
13248 hcWang942 feat: basic concepts of auction theory awaiting-author merge-conflict t-logic new-contributor merge conflict
9344 erdOne feat: Add `AddGroup.FG` -> `Module.Finite ℤ` as instances awaiting-author merge-conflict t-algebra merge conflict
12133 ADedecker feat: generalize instIsLowerProd to arbitrary products awaiting-author merge-conflict t-topology t-order merge conflict
16637 FR-vdash-bot perf: reorder `extends` of `(Add)Monoid` WIP merge-conflict t-algebra labelled WIP
14739 urkud feat(Measure): add `gcongr` lemmas help-wanted WIP awaiting-author merge-conflict t-measure-probability looking for help
8661 joelriou feat(CategoryTheory/Sites): descent of sheaves WIP merge-conflict t-category-theory labelled WIP
10476 shuxuezhuyi feat(Topology/UniformSpace): define uniform preordered space awaiting-author merge-conflict t-topology merge conflict
17593 FR-vdash-bot chore(Algebra/Order/GroupWithZero/Unbundled): deprecate useless lemmas, use `ZeroLEOneClass` blocked-by-other-PR merge-conflict t-algebra t-order blocked on another PR
17623 FR-vdash-bot feat(Algebra/Order/GroupWithZero/Unbundled): add some lemmas merge-conflict t-algebra t-order awaiting-zulip awaiting a zulip discussion
17624 FR-vdash-bot feat(Algebra/Order/GroupWithZero/Unbundled): generalize lemmas blocked-by-other-PR merge-conflict t-algebra t-order blocked on another PR
17513 FR-vdash-bot perf: do not search algebraic hierarchies when using `map_*` lemmas WIP merge-conflict t-algebra awaiting-bench labelled WIP
17515 FR-vdash-bot perf: do not need `simp low` now blocked-by-other-PR merge-conflict t-algebra blocked on another PR
19212 Julian feat(LinearAlgebra): add a variable_alias for VectorSpace merge-conflict t-algebra merge conflict
19337 zeramorphic feat(Data/Finsupp): generalise `Finsupp` to any "zero" value merge-conflict t-data merge conflict
10332 adri326 feat(Topology/Sets): define regular open sets and their boolean algebra WIP merge-conflict t-topology labelled WIP
14501 jjaassoonn feat: module structure of filtered colimit of abelian groups over filtered colimit of rings awaiting-author merge-conflict t-category-theory t-algebra workshop-AIM-AG-2024 merge conflict
18756 astrainfinita refactor: deprecate `DistribMulActionSemiHomClass` `MulSemiringActionSemiHomClass` merge-conflict t-algebra merge conflict
19125 yhtq feat: add theorems to transfer `IsGalois` between pairs of fraction rings merge-conflict t-algebra new-contributor failing CI
18841 hrmacbeth chore: change some `linarith`s to `linear_combination`s WIP merge-conflict labelled WIP
11142 hmonroe feat(ProofTheory): Define logical symbols abstractly; opens new top-level section, drawing from lean4-logic awaiting-author merge-conflict t-logic merge conflict
11210 hmonroe Test commit WIP merge-conflict labelled WIP
19621 Command-Master feat: Multiplicity and prime-adic valuation of derivations blocked-by-other-PR merge-conflict t-algebra large-import blocked on another PR
18262 joelriou feat(Algebra/Category/ModuleCat/Presheaf): exterior powers of presheaves of modules WIP blocked-by-other-PR merge-conflict t-category-theory t-algebra blocked on another PR
15269 kkytola feat: Add ENNReal.floor blocked-by-other-PR awaiting-author merge-conflict t-algebra t-order blocked on another PR
15773 kkytola feat: Add type class for ENat-valued floor functions awaiting-author merge-conflict t-order merge conflict
3251 kmill feat: deriving `LinearOrder` for simple enough inductive types WIP awaiting-author merge-conflict t-meta labelled WIP
3610 TimothyGu feat: derive Infinite automatically for inductive types awaiting-author merge-conflict t-meta merge conflict
16120 awainverse feat(ModelTheory/Algebra/Ring/Basic): Ring homomorphisms are a `StrongHomClass` for the language of rings merge-conflict RFC t-algebra t-logic failing CI
20459 Ruben-VandeVelde chore: fix names of roots_C_mul_X_{add,sub}_C_of_IsUnit awaiting-author t-algebra awaiting author
19462 joelriou feat(AlgebraicGeometry): étale sheafification WIP blocked-by-other-PR merge-conflict t-algebraic-geometry blocked on another PR
20527 trivial1711 refactor(Topology/UniformSpace/Completion): more descriptive names for `α → Completion α` merge-conflict t-topology merge conflict
17739 Aaron1011 feat(Topology/Order/DenselyOrdered): prove Not (IsOpen) for intervals awaiting-author merge-conflict t-topology new-contributor merge conflict
18474 FR-vdash-bot perf: lower the priority of `*WithOne.to*` instances merge-conflict t-algebra slow-typeclass-synthesis t-data merge conflict
20656 Komyyy feat(Mathlib/Geometry/Manifold/VectorBundle/Sphere): convert orthogonal smooth `M → 𝕊ⁿ` & `M → ℝⁿ⁺¹` to smooth `M → T𝕊ⁿ` please-adopt merge-conflict t-differential-geometry looking for help
15711 znssong feat(Combinatorics/SimpleGraph): Some lemmas about walk, cycle and Hamiltonian cycle awaiting-author merge-conflict t-combinatorics new-contributor merge conflict
15720 znssong feat(SimpleGraph): The Bondy-Chvátal theorem blocked-by-other-PR merge-conflict t-combinatorics new-contributor blocked on another PR
18629 tomaz1502 feat(Computability.Timed): Formalization of runtime complexity of List.merge awaiting-author merge-conflict new-contributor t-computability merge conflict
8362 urkud feat(Asymptotics): define `ReflectsGrowth` awaiting-author merge-conflict t-analysis failing CI
6692 prakol16 feat: disjoint indexed union of local homeomorphisms awaiting-author merge-conflict t-topology failing CI
18461 hannahfechtner feat: left and right common multiples mixins awaiting-author t-algebra new-contributor awaiting author
19291 PieterCuijpers feat(Algebra/Order/Hom): add quantale homomorphism awaiting-author merge-conflict t-algebra new-contributor failing CI
19352 hrmacbeth chore: change some `nlinarith`s to `linear_combination`s WIP merge-conflict labelled WIP
20372 jvlmdr feat(MeasureTheory/Function): Add ContinuousLinearMap.bilinearCompLp(L) merge-conflict t-measure-probability new-contributor merge conflict
20872 grunweg feat: lint against the tactic.skipAssignedInstances option in mathlib awaiting-author merge-conflict t-linter tech debt merge conflict
2605 eric-wieser chore: better error message in linarith awaiting-author merge-conflict t-meta merge conflict
11837 trivial1711 feat: completion of a uniform multiplicative group help-wanted WIP merge-conflict t-topology t-algebra looking for help
12670 trivial1711 feat: completion of a nonarchimedean multiplicative group blocked-by-other-PR merge-conflict t-topology t-algebra blocked on another PR
9449 hmonroe feat: Add Turing machine with the quintet definition (TMQ) and a chainable step function for each TM type awaiting-author merge-conflict t-computability failing CI
15355 adomani feat: MiM PR report WIP ⚠️ labelled WIP
19697 quangvdao feat(BigOperators/Fin): Sum/product over `Fin` intervals awaiting-author merge-conflict t-data failing CI
19353 hrmacbeth chore: golf some term/rw proofs using `linear_combination` WIP merge-conflict labelled WIP
20248 peabrainiac feat(Topology/Compactness): first-countable locally path-connected spaces are delta-generated blocked-by-other-PR awaiting-author merge-conflict t-topology new-contributor large-import blocked on another PR
10678 adri326 feat(Topology/UniformSpace): prove that a uniform space is completely regular awaiting-author merge-conflict t-topology merge conflict
18785 erdOne feat(CategoryTheory): command that generates instances for `MorphismProperty` awaiting-author merge-conflict t-meta t-category-theory merge conflict
15942 grunweg chore: move style linters into their own file; document all current linters awaiting-author merge-conflict t-linter merge conflict
16311 madvorak feat(Computability): regular languages are context-free WIP merge-conflict t-computability labelled WIP
19943 AlexLoitzl feat(Computability): Add Chomsky Normal Form Grammar and translation awaiting-author merge-conflict new-contributor t-computability merge conflict
17005 YnirPaz feat(SetTheory/Cardinal/Regular): define singular cardinals WIP merge-conflict t-set-theory labelled WIP
21501 sksgurdldi feat(List): add sum_zipWith_eq_finset_sum awaiting-author t-algebra new-contributor awaiting author
12054 adomani feat: auto-bugs awaiting-author merge-conflict t-meta merge conflict
5062 adomani feat(Tactic/Prune + test/Prune): add `prune` tactic, for removing unnecessary hypotheses awaiting-author modifies-tactic-syntax merge-conflict t-meta merge conflict
21433 grunweg chore: change more lemmas to be about enorm instead of nnnorm awaiting-author merge-conflict t-measure-probability carleson merge conflict
20454 urkud chore(TangentCone): review names merge-conflict t-analysis failing CI
16550 awainverse feat(ModelTheory): A typeclass for languages expanding other languages awaiting-author merge-conflict t-logic merge conflict
13686 fpvandoorn feat: some finset lemmas awaiting-author merge-conflict t-data merge conflict
14313 grhkm21 feat(RepresentationTheory/FdRep): FdRep is a full subcategory of Rep merge-conflict t-category-theory t-algebra new-contributor failing CI
10823 alexkeizer feat: convert curried type functions into uncurried type functions awaiting-author merge-conflict t-data merge conflict
13648 urkud feat(Topology/Module): generalize `ContinuousLinearMap.compSL` awaiting-author merge-conflict t-topology t-analysis t-algebra failing CI
14060 YnirPaz feat(SetTheory/Ordinal/Clubs): define club sets and prove basic properties blocked-by-other-PR merge-conflict t-logic new-contributor blocked on another PR
20636 eric-wieser feat: multiplication of intervals in rings awaiting-author t-algebra awaiting author
16000 YaelDillies feat: Croot-Sisask Almost Periodicity blocked-by-other-PR t-combinatorics t-analysis blocked on another PR
22340 sinhp feat(CategoryTheory): Locally Cartesian Closed Categories (Beck-Chevalley Conditions) WIP blocked-by-other-PR merge-conflict t-category-theory large-import blocked on another PR
21959 BGuillemet feat(Topology/ContinuousMap): Stone-Weierstrass theorem for MvPolynomial merge-conflict t-topology new-contributor merge conflict
18470 FR-vdash-bot perf: lower the priority of `Normed*.to*` instances merge-conflict t-analysis t-algebra slow-typeclass-synthesis ❌? infrastructure-related CI failing
22784 grunweg feat: add Diffeomorph.sumSumSumComm WIP t-differential-geometry labelled WIP
16944 YnirPaz feat(SetTheory/Cardinal/Cofinality): lemmas about limit ordinals and cofinality WIP merge-conflict t-set-theory labelled WIP
17368 Felix-Weilacher feat(Topology/Baire/BaireMeasurable): add the Kuratowski-Ulam theorem merge-conflict t-topology failing CI
8767 eric-wieser refactor(Cache): tidy lake-manifest parsing in Cache merge-conflict t-meta failing CI
15578 znssong feat(Function): Fixed points of function `f` with `f(x) >= x` awaiting-author merge-conflict t-analysis new-contributor merge conflict
22660 Ruben-VandeVelde chore: follow naming convention around Group.IsNilpotent merge-conflict t-algebra merge conflict
13999 adomani feat: a linter to flag potential confusing conventions awaiting-author merge-conflict t-linter merge conflict
23042 joneugster feat(CategoryTheory/Enriched/Limits): add HasConicalLimitsOfSize.shrink WIP t-category-theory infinity-cosmos labelled WIP
19013 quangvdao feat(Algebra/BigOperators/Fin): Add `finSigmaFinEquiv` awaiting-author merge-conflict t-algebra merge conflict
19189 YnirPaz feat(SetTheory/Ordinal/Arithmetic): order isomorphism between omega and the natural numbers awaiting-author merge-conflict t-set-theory merge conflict
23142 joneugster feat(CategoryTheory/Enriched/Limits): add API for HasConicalLimit awaiting-author t-category-theory infinity-cosmos awaiting author
23145 joneugster feat(CategoryTheory/Enriched/Limits): add IsConicalLimits blocked-by-other-PR merge-conflict t-category-theory infinity-cosmos blocked on another PR
19227 adomani fix(CI): unwrap `lake test` in problem matcher awaiting-author merge-conflict CI merge conflict
20874 grunweg chore(nolint.yml): use shallow clones awaiting-author merge-conflict CI merge conflict
15774 kkytola feat: Topology on `ENat` WIP merge-conflict t-topology t-order labelled WIP
18284 chrisflav feat(AlgebraicGeometry): relative gluing of schemes WIP merge-conflict t-algebraic-geometry labelled WIP
20613 grunweg chore: golf using `List.toArrayMap` merge-conflict large-import failing CI
20222 eric-wieser feat: generalize lemmas about derivatives blocked-by-other-PR merge-conflict t-analysis blocked on another PR
22682 grunweg chore(Topology/Homeomorph): split out various constructions merge-conflict RFC t-topology tech debt failing CI
21018 markimunro feat(Data/Matrix): add file with key definitions and theorems about elementary row operations enhancement awaiting-author merge-conflict new-contributor t-data failing CI
23514 eric-wieser refactor: smooth over Lattice/LinearOrder inheritance merge-conflict failing CI
22810 pechersky feat(Counterexamples): metric space not induced by norm WIP merge-conflict t-topology t-analysis labelled WIP
13124 FR-vdash-bot chore: remove `CovariantClass` and `ContravariantClass` WIP merge-conflict labelled WIP
20401 RemyDegenne feat: add sigmaFinite_iUnion awaiting-author merge-conflict t-measure-probability merge conflict
19275 eric-wieser fix: if nolint files change, do a full rebuild delegated merge-conflict failing CI
22727 grunweg feat: rewrite the isolated by and colon linters in Lean awaiting-author merge-conflict t-linter merge conflict
15212 victorliu5296 feat: Add fundamental theorem of calculus-2 for Banach spaces awaiting-author merge-conflict t-analysis t-measure-probability new-contributor merge conflict
22888 plp127 perf: replace `Lean.Expr.swapBVars` with a better? implementation awaiting-author t-meta awaiting author
22579 kvanvels doc(Topology/Defs/Induced): fix comments on three functions related to RestrictGenTopology documentation awaiting-author merge-conflict t-topology merge conflict
21488 imbrem feat(CategoryTheory/Monoidal): premonoidal categories merge-conflict t-category-theory new-contributor merge conflict
21525 sinhp feat(CategoryTheory): Locally Cartesian Closed Categories (Prelim) merge-conflict t-category-theory large-import merge conflict
22319 sinhp feat(CategoryTheory): Locally Cartesian Closed Categories (Sections Right Adjoint) blocked-by-other-PR merge-conflict t-category-theory large-import blocked on another PR
22321 sinhp feat(CategoryTheory): Locally Cartesian Closed Categories (Definition) blocked-by-other-PR merge-conflict t-category-theory large-import blocked on another PR
19425 hrmacbeth perf: gcongr forward-reasoning adjustment awaiting-author merge-conflict merge conflict
20873 vbeffara feat(Topology/Covering): path lifting and homotopy lifting awaiting-author merge-conflict t-topology new-contributor failing CI
22817 peabrainiac feat(CategoryTheory/Sites): local sites WIP merge-conflict t-category-theory labelled WIP
6252 michaellee94 feat(Geometry/Manifolds/Instances/Homeomorph): Homeomorphism maps `C^k` manifolds to `C^k` manifolds WIP merge-conflict t-differential-geometry labelled WIP
16314 FR-vdash-bot chore(Data/Quot): deprecate `ind*'` APIs merge-conflict t-data merge conflict
23509 eric-wieser refactor: Make ENNReal an abbrev merge-conflict t-data failing CI
11455 adomani fix: unsqueeze simp, re Yaël's comments on #11259 awaiting-author merge-conflict merge conflict
7325 eric-wieser chore: use preimageIso instead of defeq abuse for InducedCategory merge-conflict awaiting-CI t-category-theory does not pass CI
7874 astrainfinita chore: make `IsScalarTower A A B` and `IsScalarTower A B B` higher priority merge-conflict awaiting-CI t-algebra slow-typeclass-synthesis ??? does not pass CI
13038 adomani feat: Mathlib weekly reports awaiting-author t-meta CI awaiting author
5952 eric-wieser feat: add Qq wrappers for ToExpr merge-conflict t-meta awaiting-CI does not pass CI
15483 FR-vdash-bot chore(GroupTheory/Coset): reduce defeq abuse merge-conflict t-algebra merge conflict
16594 FR-vdash-bot perf: reorder `extends` and remove some instances in algebra hierarchy merge-conflict t-algebra slow-typeclass-synthesis failing CI
21238 joneugster feat(Cache): enable partial cache in downstream projects blocked-by-other-PR merge-conflict t-meta CI blocked on another PR
21842 joneugster refactor(Cache): use module name for file hash instead of non-resolved file path blocked-by-other-PR merge-conflict t-meta CI blocked on another PR*
19467 quangvdao feat(MvPolynomial/Equiv): Add `MvPolynomial.finSuccEquivNth` blocked-by-other-PR merge-conflict t-algebra blocked on another PR
20567 grunweg feat(Cache): two small features merge-conflict t-meta merge conflict
20313 thefundamentaltheor3m feat(Data/Complex/Exponential): prove some useful results about the complex exponential. merge-conflict t-analysis new-contributor failing CI
22698 Kiolt feat: notation for whisker(Left/Right)Iso merge-conflict t-category-theory toric failing CI
19613 madvorak refactor(Combinatorics/Optimization/ValuedCSP): make only valid `FractionalOperation` possible t-combinatorics failing CI
20730 kuotsanhsu feat(LinearAlgebra/Matrix/SchurTriangulation): prove Schur decomposition/triangulation awaiting-author merge-conflict t-algebra new-contributor failing CI
19117 eric-wieser feat: derivatives of matrix operations WIP merge-conflict t-analysis labelled WIP
12605 FR-vdash-bot chore: attribute [induction_eliminator] awaiting-author merge-conflict merge conflict
15099 joelriou feat(CategoryTheory/Sites): the Mayer-Vietoris long exact sequence in sheaf cohomology WIP merge-conflict t-category-theory labelled WIP
23859 urkud feat(Topology/../Order/Field): generalize to `Semifield` merge-conflict t-topology merge conflict
24219 Paul-Lez feat: linear independence of the tensor product of two linearly independent families WIP t-algebra toric labelled WIP
23810 b-reinke chore(Order/Interval): generalize succ/pred lemmas to partial orders merge-conflict t-order merge conflict
24285 madvorak chore(Algebra/*-{Category,Homology}): remove unnecessary universe variables merge-conflict t-algebra merge conflict
8370 eric-wieser refactor(Analysis/NormedSpace/Exponential): remove the `𝕂` argument from `exp` merge-conflict t-analysis awaiting-zulip failing CI
22583 imathwy feat: affinespace homeomorphism awaiting-author merge-conflict t-algebra failing CI
23593 erdOne feat(AlgebraicGeometry): the tilde construction is functorial awaiting-author merge-conflict t-algebraic-geometry merge conflict
21065 eric-wieser feat: generalize `tangentConeAt.lim_zero` to TVS WIP merge-conflict t-analysis labelled WIP
22721 grunweg chore(MeasureTheory/Function/LpSeminorm/Basic): generalise more results to enorm classes WIP merge-conflict t-measure-probability carleson labelled WIP
24354 grunweg chore(HasFiniteIntegral): rename three lemmas merge-conflict t-measure-probability merge conflict
14731 adomani feat: the repeated typeclass assumption linter WIP merge-conflict t-linter large-import labelled WIP
13649 FR-vdash-bot chore: redefine `Nat.div2` `Nat.bodd` merge-conflict merge conflict
18861 YaelDillies refactor: make `Set.mem_graphOn` defeq awaiting-author t-data failing CI
24549 grunweg feat: define embedded submanifolds, attempt 1 WIP blocked-by-other-PR merge-conflict t-differential-geometry blocked on another PR
22809 b-reinke feat: Category algebras and path algebras WIP t-category-theory t-algebra new-contributor labelled WIP
14675 adomani dev: the repeated variable linter WIP merge-conflict t-linter labelled WIP
14330 Ruben-VandeVelde chore: split Mathlib.Algebra.Star.Basic awaiting-author merge-conflict merge conflict
8511 eric-wieser refactor(MeasureTheory/Measure/Haar/Basic): partially generalize to the affine case awaiting-author merge-conflict t-measure-probability merge conflict
7994 ericrbg chore: generalize `LieSubalgebra.mem_map_submodule` please-adopt merge-conflict t-algebra looking for help
6317 eric-wieser refactor(Data/Finsupp/Defs): make Finsupp.single defeq to Pi.single WIP merge-conflict t-data labelled WIP
11524 mcdoll refactor: Introduce type-class for SchwartzMap WIP merge-conflict t-analysis labelled WIP
11003 thorimur chore: migrate to `tfae` block tactic WIP blocked-by-other-PR merge-conflict t-meta blocked on another PR
16186 joneugster chore: use emoji-variant-selector `\uFE0F` for emojis ✅️,❌️,💥️,🟡️ blocked-by-other-PR awaiting-author merge-conflict t-linter blocked on another PR
22488 smmercuri fix: lower priority for `UniformSpace.Completion.instSMul` awaiting-author t-topology FLT awaiting author
23546 JovanGerb feat(LinearAlgebra/AffineSpace/AffineSubspace): rename `AffineSubspace.mk'` to `Submodule.shift` merge-conflict t-euclidean-geometry merge conflict
15654 TpmKranz feat(Computability): language-preserving maps between NFA and RE blocked-by-other-PR merge-conflict new-contributor t-computability awaiting-zulip blocked on another PR
19315 quangvdao feat(Data/Finsupp/Fin): Add `Finsupp` operations on `Fin` tuple awaiting-author merge-conflict t-data merge conflict
7907 urkud feat: introduce `NthRoot` notation class merge-conflict awaiting-CI t-analysis t-algebra does not pass CI
24155 eric-wieser feat: add a "rw_proc" for fin vectors awaiting-author t-meta RFC t-data awaiting author
24550 grunweg feat: define `SliceModel` typeclass for models with corners for embedded submanifolds WIP blocked-by-other-PR merge-conflict t-differential-geometry blocked on another PR
21276 GabinKolly feat(ModelTheory/Substructures): define equivalences between equal substructures awaiting-author t-logic awaiting author
24008 meithecatte chore(EpsilonNFA): replace manual lemmas with @[simps] awaiting-author new-contributor t-computability awaiting author
24642 grunweg WIP-feat: add layercake formula for ENNReal-valued functions WIP merge-conflict t-analysis carleson labelled WIP
21712 grunweg chore: generalise more lemmas to `ContinuousENorm` merge-conflict awaiting-CI t-measure-probability carleson does not pass CI
21375 grunweg WIP: generalise lemmas to ENorm WIP merge-conflict awaiting-CI t-measure-probability carleson labelled WIP
24618 b-mehta feat(Analysis): add Schur inequality and variants WIP t-analysis labelled WIP
15115 kkytola feat: Generalize assumptions in liminf and limsup results in ENNReals help-wanted awaiting-author merge-conflict t-topology t-order looking for help
24957 eric-wieser feat: use ` binderNameHint` in sum_congr t-algebra failing CI
17129 joneugster feat(Tactic/Linter): add unicode linter for unicode variant-selectors awaiting-author delegated merge-conflict t-linter large-import failing CI
17131 joneugster feat(Tactic/Linter): add unicode linter for unwanted characters awaiting-author merge-conflict t-linter large-import merge conflict
22837 joneugster feat(Data/Set/Basic): add subset_iff and not_mem_subset_iff merge-conflict t-data t-set-theory merge conflict
24100 eric-wieser feat: restore some explicit binders from Lean 3 awaiting-author merge-conflict tech debt ⚠️ failing CI
21476 grunweg feat(lint-style): enable running on downstream projects merge-conflict t-linter merge conflict
23349 BGuillemet feat: add LocallyLipschitzOn.lipschitzOnWith_of_isCompact and two small lemmas about Lipschitz functions merge-conflict t-topology new-contributor large-import merge conflict
12438 jjaassoonn feat: some APIs for flat modules WIP merge-conflict t-category-theory labelled WIP
8740 digama0 fix: improve `recall` impl / error reporting awaiting-author merge-conflict t-meta awaiting-CI does not pass CI
21182 joneugster fix(Util/CountHeartbeats): move elaboration in #count_heartbeats inside a namespace merge-conflict t-meta merge conflict
23371 grunweg chore: mark `Disjoint.{eq_bot, inter_eq}` simp awaiting-author merge-conflict t-order merge conflict
25473 adomani feat(CI): check that Mathlib files have lean or md extension delegated CI delegated
16020 adomani feat: compare PR `olean`s size with `master` merge-conflict CI failing CI
16062 adomani Test/ci olean size WIP awaiting-author merge-conflict CI labelled WIP
12799 jstoobysmith feat(LinearAlgebra/UnitaryGroup): Add properties of Special Unitary Group awaiting-author please-adopt merge-conflict t-algebra new-contributor looking for help
23709 plp127 feat: `Nat.findFrom` merge-conflict t-data failing CI
25340 dupuisf chore(Analysis/Convex): move files pertaining to convex/concave functions to their own folder merge-conflict t-convex-geometry merge conflict
23929 meithecatte feat(Computability/NFA): improve bound on pumping lemma new-contributor t-computability awaiting-zulip awaiting a zulip discussion
13994 grunweg chore(Topology): replace continuity -> fun_prop merge-conflict t-topology failing CI
21734 adomani fix(PR summary): checkout GITHUB_SHA WIP awaiting-author merge-conflict CI labelled WIP
13483 adomani feat: automatically replace deprecations awaiting-author delegated merge-conflict t-meta failing CI
20334 miguelmarco feat: allow polyrith to use a local Singular/Sage install awaiting-author merge-conflict t-meta new-contributor merge conflict
25912 BoltonBailey feat: add simp lemmas for trig functions on `π * 2⁻¹` blocked-by-other-PR awaiting-author t-analysis blocked on another PR
23953 b-reinke feat(Data/Matroid/Tutte): define the Tutte polynomial of a matroid WIP merge-conflict t-data labelled WIP
25921 BoltonBailey feat: scripts to analyze overlap between namespaces WIP t-meta migrated-from-branch labelled WIP
18771 joelriou feat(LinearAlgebra/ExteriorPower): exterior powers of free modules are free WIP blocked-by-other-PR merge-conflict t-algebra blocked on another PR
18441 ADedecker refactor(AdicTopology): use new API for algebraic filter bases, and factor some code merge-conflict t-topology t-algebra merge conflict
18439 ADedecker refactor: use new algebraic filter bases API in `FiniteAdeleRing` merge-conflict t-topology t-algebra merge conflict
18438 ADedecker refactor: adapt `KrullTopology` to the new algebraic filter bases API merge-conflict t-topology t-algebra merge conflict
26239 BoltonBailey feat: add sample pre-commit git hook file WIP ⚠️ labelled WIP
13964 pechersky feat(Data/DigitExpansion): begin defining variant of reals without rationals merge-conflict t-data merge conflict
18662 joelriou feat(LinearAlgebra/ExteriorPower): generators of the exterior powers WIP blocked-by-other-PR merge-conflict t-algebra blocked on another PR
18735 joelriou feat(Algebra/Module): presentation of the exterior power WIP blocked-by-other-PR merge-conflict t-algebra blocked on another PR
25993 Multramate feat(Algebra/Group/Units/Hom): add map lemmas awaiting-author t-algebra awaiting author
16074 Rida-Hamadani feat: combinatorial maps and planar graphs merge-conflict t-combinatorics merge conflict
16801 awainverse feat(ModelTheory/Equivalence): The quotient type of formulas modulo a theory awaiting-author merge-conflict t-logic merge conflict
17458 urkud refactor(Algebra/Group): make `IsUnit` a typeclass merge-conflict t-algebra awaiting-zulip failing CI
17627 hrmacbeth feat: universal properties of vector bundle constructions delegated merge-conflict t-differential-geometry merge conflict
19444 joelriou feat(CategoryTheory/Sites): Equivalence of categories of sheaves with a dense subsite that is 1-hypercover dense WIP merge-conflict t-category-theory labelled WIP
22928 javra feat(CategoryTheory): infrastructure for inclusion morphisms into products in categories with 0-morphisms merge-conflict t-category-theory failing CI
23763 grunweg feat(Linter.openClassical): also lint for Classical declarations as … merge-conflict t-linter failing CI
24710 chrisflav chore(Data/Set): `tsum` version of `Set.encard_iUnion_of_finite` for non-finite types merge-conflict t-data failing CI
24823 eric-wieser refactor: add `hom` lemmas for the `MonoidalCategory` structure on `ModuleCat` merge-conflict t-algebra merge conflict
25071 erdOne feat(EllipticCurve): basic API for singular cubics merge-conflict t-algebraic-geometry merge conflict
25218 kckennylau feat(AlgebraicGeometry): Tate normal form of elliptic curves merge-conflict t-algebraic-geometry new-contributor awaiting-zulip awaiting a zulip discussion
25283 Brian-Nugent feat: regular local rings merge-conflict t-algebra new-contributor merge conflict
25561 callesonne feat(Category/Grpd): define the bicategory of groupoids awaiting-author merge-conflict t-category-theory merge conflict
25622 eric-wieser refactor: overhaul instances on LocalizedModule merge-conflict t-algebra failing CI
25988 Multramate refactor(AlgebraicGeometry/EllipticCurve/*): replace Fin 3 with products merge-conflict t-algebraic-geometry merge conflict
26090 grunweg chore: make `finiteness` a default tactic merge-conflict failing CI
26395 winstonyin feat: $C^1$ vector fields on compact manifolds define global flows WIP blocked-by-other-PR merge-conflict t-differential-geometry blocked on another PR
26465 joelriou feat(Algebra/Module): presentation of the `PiTensorProduct` blocked-by-other-PR merge-conflict t-algebra file-removed blocked on another PR
26467 joelriou feat(LinearAlgebra): the tensor product of a finite family of free modules is free WIP blocked-by-other-PR merge-conflict t-algebra file-removed blocked on another PR
20784 eric-wieser fix: prevent `exact?` recursing forever on `n = 55` t-set-theory failing CI
24405 mcdoll refactor(Topology/Algebra/Module/WeakDual): Clean up merge-conflict t-topology large-import merge conflict
26647 b-mehta feat(Data/Sym/Sym2): lift commutative operations to sym2 WIP merge-conflict t-data labelled WIP
26067 mapehe feat(Topology/StoneCech): exists_continuous_surjection_from_StoneCech_to_dense_range merge-conflict t-topology merge conflict
10541 Louddy feat(Algebra/SkewMonoidAlgebra/Basic): add SkewMonoidAlgebra WIP merge-conflict t-algebra new-contributor labelled WIP
25999 bjoernkjoshanssen feat(Topology/Compactification): projective line over ℝ is homeomorphic to the one-point compactification of ℝ merge-conflict t-topology failing CI
26994 Paul-Lez feat(Topology/MetricSpace/Pseudo/Defs): add easy lemma about opens in topological spaces awaiting-author easy t-topology awaiting author
25710 Paul-Lez feat(Mathlib/Analysis/PDE/Quasilinear/Characteristics): the method of characteristics for first order quasilinear PDEs WIP merge-conflict t-analysis labelled WIP
26911 JovanGerb chore: fix naming of `mono` and `monotone` delegated merge-conflict merge conflict
21838 joneugster feat(Cache): Allow arguments of the form `Mathlib.Data` which correspond to a folder but not a file awaiting-author merge-conflict t-meta CI merge conflict
27069 FrankieNC feat(Analysis/MetricSpace/HausdorffDimension): prove dimH of intervals and segments is 1 awaiting-author t-topology new-contributor awaiting author
25611 erdOne chore(RingTheory): add `Algebra (FractionRing R) (FractionRing S)` merge-conflict t-algebra failing CI
18230 digama0 feat(Tactic/ScopedNS): extend `scoped[NS]` to more commands awaiting-author t-meta awaiting author
25284 alreadydone feat(LinearAlgebra/Contraction): bijectivity of `dualTensorHom` + generalize to CommSemiring awaiting-author merge-conflict t-algebra merge conflict
22749 joelriou feat(CategoryTheory/Abelian): the Gabriel-Popescu theorem as a localization with respect to a Serre class WIP merge-conflict t-category-theory labelled WIP
20428 madvorak feat(Data/Sign): lemmas about `∈ Set.range SignType.cast` WIP merge-conflict t-data labelled WIP
26987 joelriou chore: deprecating module LinearAlgebra.PiTensorProduct WIP blocked-by-other-PR merge-conflict t-algebra blocked on another PR
27435 callesonne feat(Normed/Algebra/Logarithm): add FormalMultilinearSeries of logarithm around `1` WIP t-analysis labelled WIP
24668 robertmaxton42 feat(LinearAlgebra): add inductive principle for the free product of algebras blocked-by-other-PR merge-conflict t-algebra blocked on another PR
13973 digama0 feat: lake exe refactor, initial framework awaiting-author merge-conflict t-meta merge conflict
10190 jstoobysmith feat(AlgebraicTopology): add Augmented Simplex Category WIP merge-conflict t-category-theory new-contributor t-algebraic-topology labelled WIP
20719 gio256 feat(AlgebraicTopology): delaborators for truncated simplicial notations merge-conflict t-meta infinity-cosmos t-algebraic-topology merge conflict
25914 eric-wieser feat: add an ext lemma for the opposite category awaiting-author merge-conflict awaiting-CI t-category-theory does not pass CI
27704 vihdzp feat: link `Minimal` and `IsLeast` together awaiting-author t-order failing CI
20208 js2357 feat: Define the localization of a fractional ideal at a prime ideal WIP merge-conflict t-algebra labelled WIP
24260 plp127 feat(Topology): add API for Hereditarily Lindelof spaces awaiting-author merge-conflict t-topology merge conflict
27813 javra feat: IMO 2025 Q1 WIP IMO labelled WIP
27608 RemyDegenne feat(MeasureTheory): typeclasses for measures with finite moments WIP merge-conflict t-measure-probability labelled WIP
27826 Louddy feat(Subsemiring): mk_eq_zero WIP t-algebra labelled WIP
27050 BoltonBailey doc(Control/Monad/Cont): add docstrings awaiting-author t-data failing CI
27225 eric-wieser refactor(Tactic/Lift): deprecate the third with argument awaiting-author t-meta awaiting author
25991 Multramate feat(AlgebraicGeometry/EllipticCurve): generalise nonsingular condition merge-conflict t-algebraic-geometry failing CI
25985 Multramate feat(AlgebraicGeometry/EllipticCurve/Jacobian): add equivalences between points and explicit WithZero types merge-conflict t-algebraic-geometry failing CI
25984 Multramate feat(AlgebraicGeometry/EllipticCurve/Affine): add equivalences between points and explicit WithZero types merge-conflict t-algebraic-geometry failing CI
25982 Multramate feat(AlgebraicGeometry/EllipticCurve/Group): compute range of baseChange merge-conflict t-algebraic-geometry failing CI
25981 Multramate feat(GroupTheory/GroupAction/Basic): define homomorphisms of fixed subgroups induced by homomorphisms of groups merge-conflict t-group-theory failing CI
25980 Multramate feat(GroupTheory/Submonoid/Operations): define homomorphisms of subgroups induced by homomorphisms of groups merge-conflict t-group-theory failing CI
25486 VTrelat feat(SetTheory/ZFC/Integers): define integers in ZFC blocked-by-other-PR merge-conflict new-contributor t-set-theory blocked on another PR
25485 VTrelat feat(SetTheory/ZFC/Naturals): define natural numbers in ZFC merge-conflict new-contributor t-set-theory failing CI
25484 VTrelat feat(SetTheory/ZFC/Booleans): define Boolean algebra in ZFC blocked-by-other-PR merge-conflict new-contributor t-set-theory blocked on another PR
25474 adomani test for .lean/.md check merge-conflict t-linter file-removed failing CI
25238 Hagb feat(Tactic/ComputeDegree): add support for scalar multiplication with different types merge-conflict t-meta new-contributor merge conflict
26385 jjdishere feat(RingTheory/Perfectoid): define integral perfectoid rings WIP merge-conflict t-ring-theory labelled WIP
22909 AntoineChambert-Loir feat(RingTheory/Pure): pure submodules blocked-by-other-PR merge-conflict t-ring-theory blocked on another PR
22908 AntoineChambert-Loir feat(RingTheory/Finiteness/Small): tensor product of the system of small submodules blocked-by-other-PR merge-conflict t-ring-theory blocked on another PR
22898 AntoineChambert-Loir feat(RingTheory/TensorProduct/DirectLimit/FG): direct limit of finitely generated submodules and tensor product WIP merge-conflict t-ring-theory labelled WIP
20431 erdOne feat(RingTheory/AdicCompletion): monotonicity of adic-completeness awaiting-author merge-conflict t-ring-theory merge conflict
19596 Command-Master feat(RingTheory/Valuation/PrimeMultiplicity): define `WithTop ℤ`-valued prime multiplicity on a fraction field awaiting-author merge-conflict large-import t-ring-theory merge conflict
18646 jxjwan feat(RingTheory): isotypic components merge-conflict new-contributor t-ring-theory failing CI
17246 pechersky feat(RingTheory/PrimaryDecomposition): PIR of Noetherian under jacobson condition awaiting-author merge-conflict t-ring-theory failing CI
21474 erdOne feat(RingTheory): replace `Ring.DimensionLEOne` with `Ring.KrullDimLE` merge-conflict large-import t-ring-theory failing CI
9820 jjaassoonn feat(RingTheory/GradedAlgebra/HomogeneousIdeal): generalize to homogeneous submodule merge-conflict t-ring-theory merge conflict
11212 shuxuezhuyi feat(GroupTheory/GroupAction): instance `MulAction (β ⧸ H) α` awaiting-author merge-conflict large-import t-group-theory merge conflict
27886 alreadydone feat(Algebra): (Mv)Polynomial.X is irreducible assuming NoZeroDivisors awaiting-author merge-conflict t-algebra merge conflict
26200 adomani fix: add label when landrun fails merge-conflict CI merge conflict
17469 joelriou feat(Algebra/ModuleCat/Differentials/Presheaf): the presheaf of relative differentials WIP merge-conflict t-category-theory t-algebraic-geometry large-import labelled WIP
27709 kckennylau chore: fix links WIP merge-conflict labelled WIP
28075 tristan-f-r chore(Finsupp/Indicator): make non-classical awaiting-author easy t-data awaiting author
20671 thefundamentaltheor3m feat(Analysis/Asymptotics/SpecificAsymptotics): Proving that 𝛔ₖ(n) = O(nᵏ⁺¹) awaiting-author merge-conflict t-number-theory new-contributor large-import merge conflict
20267 joelriou feat(CategoryTheory): comma categories are accessible WIP awaiting-author merge-conflict t-category-theory labelled WIP
27451 kckennylau feat(RingTheory/Valuation): define ball, closed ball, and sphere merge-conflict t-ring-theory merge conflict
27987 kckennylau feat(RingTheory/Valuation): define ball, closed ball, and sphere merge-conflict large-import t-ring-theory merge conflict
27444 grunweg feat: generalise more lemmas to enorms WIP carleson ⚠️ labelled WIP
24862 grunweg feat(LocallyIntegrable): generalise more to enorms WIP merge-conflict t-measure-probability carleson labelled WIP
27226 xcloudyunx feat(Combinatorics/SimpleGraph): Add Subgraph.inclusion_edge_apply_coe and inclusion_edgeSet_apply_coe awaiting-author t-combinatorics new-contributor awaiting author
27003 eric-wieser chore: use `Simp.ResultQ` more often merge-conflict t-meta merge conflict
22925 ggranberry feat(Mathlib/PlaceHolder/ToeplitzHausdorff): Toeplitz-Hausdorff help-wanted WIP awaiting-author t-analysis new-contributor will-close-soon looking for help
25483 VTrelat chore(Data/Set/Prod, SetTheory/ZFC/Basic): add theorem prod_subset_of_prod and extend ZFC model merge-conflict new-contributor t-data merge conflict
25401 digama0 feat(Util): SuppressSorry option merge-conflict t-meta merge conflict
26394 winstonyin feat: existence of local flows on manifolds WIP merge-conflict t-differential-geometry labelled WIP
27897 grunweg feat: check indentation of doc-strings blocked-by-other-PR merge-conflict awaiting-CI t-linter blocked on another PR
27996 grunweg feat: check indentation in doc-strings, medium version WIP blocked-by-other-PR merge-conflict ⚠️ blocked on another PR
27759 plp127 chore(FreeAbelianGroup): deprecate multiplication merge-conflict t-algebra large-import failing CI
8102 miguelmarco feat(Tactic): add `unify_denoms` and `collect_signs` tactics good first issue modifies-tactic-syntax please-adopt merge-conflict t-meta new-contributor looking for help
7873 astrainfinita perf: reorder `extends` and change instance priority in algebra hierarchy blocked-by-other-PR merge-conflict t-algebra slow-typeclass-synthesis blocked on another PR
27446 grunweg chore: more enorm lemmas WIP merge-conflict carleson labelled WIP
14583 lecopivo fix: make concrete cycle notation local awaiting-author merge-conflict merge conflict
5897 eric-wieser feat: add a `MonadError` instance for `ContT` awaiting-author t-meta awaiting author
28502 gilesgshaw feat(Logic/Basic): avoid unnecessary uses of choice blocked-by-other-PR awaiting-author merge-conflict t-logic new-contributor blocked on another PR
28631 faenuccio feat(Data\Nat\ModEq.lean): add grind attribute to ModEq WIP t-data labelled WIP
28622 alreadydone chore(Mathlib): replace `=>` by `↦` merge-conflict merge conflict
24793 tristan-f-r feat: trace of unitarily similar matrices awaiting-author merge-conflict t-algebra merge conflict
27198 robin-carlier feat(CategoryTheory/Monoidal/DayConvolution): the Yoneda embedding is monoidal (for Day convolution) blocked-by-other-PR merge-conflict t-category-theory file-removed blocked on another PR
26645 erdOne feat(RingTheory/PowerSeries): Construction of `Q` such that `P(Q(X)) = X` awaiting-author t-ring-theory awaiting author
28680 vihdzp feat: set has cardinality one iff singleton awaiting-author easy t-set-theory awaiting author
27872 JovanGerb chore(gcongr): clean up imports delegated merge-conflict large-import failing CI
28626 alreadydone chore(Archive, Counterexamples): replace => by ↦ merge-conflict merge conflict
26078 kckennylau feat(AlgebraicGeometry): add x, y, px, py for points on elliptic curves awaiting-author t-algebraic-geometry awaiting author
19582 yu-yama feat(GroupExtension/Abelian): define `OfMulDistribMulAction.equivH2` blocked-by-other-PR merge-conflict t-algebra new-contributor blocked on another PR
7300 ah1112 feat: synthetic geometry help-wanted awaiting-author merge-conflict t-euclidean-geometry looking for help
13795 astrainfinita perf(Algebra/{Group, GroupWithZero, Ring}/InjSurj): reduce everything merge-conflict t-algebra merge conflict
28150 Equilibris chore: clean up proofs typevec proofs merge-conflict new-contributor t-data merge conflict
27868 grunweg linter indentation playground WIP merge-conflict t-linter labelled WIP
25488 VTrelat feat(SetTheory/ZFC/Rationals): define rationals in ZFC blocked-by-other-PR merge-conflict new-contributor t-set-theory blocked on another PR
27403 MoritzBeroRoos fix: replace probably erroneous usage of ⬝ (with old \cdot) by · (with \centerdot) merge-conflict new-contributor merge conflict
28042 kckennylau feat(Topology/ValuativeRel): a topological basis indexed by pairs of elements merge-conflict t-ring-theory merge conflict
27399 MoritzBeroRoos chore: replace every usage of ⬝ᵥ (with old \cdot) by ·ᵥ (with \centerdot) merge-conflict new-contributor merge conflict
27479 iu-isgood feat: Abel's Binomial Theorem awaiting-author new-contributor t-data failing CI
25700 grunweg feat: lint upon uses of the `mono` tactic please-adopt RFC t-linter looking for help
27835 edegeltje feat(Tactic): ring modulo a given characteristic merge-conflict t-meta large-import migrated-from-branch ❌? infrastructure-related CI failing
28787 alreadydone feat(Counterexamples): a domain whose ring of differences is not a domain blocked-by-other-PR merge-conflict t-algebra large-import blocked on another PR
24719 madvorak feat(LinearAlgebra/Matrix/NonsingularInverse): inverting `Matrix` inverts its `LinearEquiv` awaiting-author t-algebra awaiting author
27437 kckennylau feat(RingTheory/Valuation): some lemmas about comparing with 1 and 0 and with each other WIP merge-conflict t-ring-theory labelled WIP
27785 staroperator chore(Algebra/Group/Submonoid): golf `Nat.addSubmonoidClosure_one` using `simp` merge-conflict t-algebra large-import merge conflict
28148 kckennylau feat(Matrix): Simproc and Rw-proc for Matrix Transpose merge-conflict t-meta merge conflict
24373 YaelDillies refactor: golf `modularCharacter` awaiting-CI t-measure-probability does not pass CI
28686 mitchell-horner feat(Combinatorics/SimpleGraph): prove the Erdős-Stone theorem WIP blocked-by-other-PR merge-conflict t-combinatorics blocked on another PR
28687 mitchell-horner feat(Combinatorics/SimpleGraph): prove the Erdős-Stone-Simonovits theorem WIP blocked-by-other-PR merge-conflict t-combinatorics blocked on another PR
28689 mitchell-horner feat(Combinatorics/SimpleGraph): prove well-known corollaries of the Erdős-Stone-Simonovits theorem WIP blocked-by-other-PR merge-conflict t-combinatorics blocked on another PR
26952 robin-carlier feat(CategoryTheory/DayConvolution): monoid objects internal to day convolutions blocked-by-other-PR merge-conflict t-category-theory blocked on another PR
27133 robin-carlier feat(CategoryTheory/Monoidal/DayConvolution): `C ⊛⥤ V` is monoidal closed when `V` is blocked-by-other-PR merge-conflict t-category-theory blocked on another PR
27151 robin-carlier feat(CategoryTheory/Monoidal/DayConvolution): `C ⊛⥤ V` is braided/symmetric when `C` and `V` are braided/symmetric blocked-by-other-PR merge-conflict t-category-theory blocked on another PR
27175 robin-carlier feat(CategoryTheory/Monoidal/DayConvolution): `LawfulDayConvolutionMonoidalCategoryStruct.ι C V D` is monoidal when the target is `C ⊛⥤ V` blocked-by-other-PR merge-conflict t-category-theory blocked on another PR
26413 michaellee94 feat(Analysis/ODE/MaximalSolution): Existence of maximal solutions for ODE meeting Picard-Lindelöf conditions blocked-by-other-PR awaiting-author merge-conflict t-analysis new-contributor blocked on another PR
25741 robin-carlier feat(AlgebraicTopology/SimplexCategory/SimplicialObject): definitions of simplicial objects by generators and relation blocked-by-other-PR merge-conflict t-category-theory large-import t-algebraic-topology blocked on another PR
26931 javra feat(CategoryTheory/Enriched): `V`-enriched isomorphisms awaiting-author merge-conflict t-category-theory infinity-cosmos merge conflict
27707 FLDutchmann feat(NumberTheory/SelbergSieve): define Selberg's weights and prove basic results. blocked-by-other-PR merge-conflict t-number-theory t-analysis blocked on another PR
27898 grunweg feat: check indentation of doc-strings, basic version blocked-by-other-PR merge-conflict t-linter blocked on another PR
25208 erdOne feat(LinearAlgebra): `tensor_induction` macro WIP merge-conflict RFC t-algebra labelled WIP
28803 astrainfinita refactor: unbundle algebra from `ENormed*` merge-conflict t-analysis t-algebra slow-typeclass-synthesis awaiting-zulip awaiting a zulip discussion
26603 vihdzp refactor(SetTheory/Ordinal/FixedPoint): redefine `Ordinal.deriv` merge-conflict t-set-theory failing CI
29232 vihdzp feat: more theorems on `SuccAddOrder` t-algebra t-order failing CI
26935 Paul-Lez feat(Analysis/SpecialFunction/NthRoot): definition and basic API of Real.nthRoot t-analysis failing CI
27995 kckennylau feat(RingTheory/Valuation): alternate constructors for Valuation awaiting-CI t-ring-theory does not pass CI
27566 wwylele feat(Data/Real): Archimedean.embedReal is a ring hom when M is an ordered ring merge-conflict t-data large-import merge conflict
26159 upobir feat(Algebra/QuadraticDiscriminant): Adding inequalities on quadratic from inequalities on discriminant awaiting-author t-algebra awaiting author
28151 iehality feat(Computability): r.e. sets are closed under inter/union/projection/composition awaiting-author merge-conflict t-computability merge conflict
27701 vihdzp feat: `a < b + c ↔ a < b ∨ ∃ d < c, a = b + d` awaiting-author t-algebra awaiting author
26908 robin-carlier feat(CategoryTheory/Monoidal/DayConvolution): alternative ext principle for unitors merge-conflict t-category-theory merge conflict
27150 robin-carlier feat(CategoryTheory/Monoidal/DayConvolution): constructors for braided and symmetric structure on day convolutions monoidal categories merge-conflict t-category-theory merge conflict
29077 grunweg feat(Manifold/Instances/Icc): golf smoothness proof using immersions blocked-by-other-PR merge-conflict ⚠️ blocked on another PR
26462 PSchwahn feat(LinearAlgebra/Projection): add results about inverse of `Submodule.prodEquivOfIsCompl` awaiting-author t-algebra new-contributor awaiting author
27119 robin-carlier feat(CategoryTheory/Monoidal/DayConvolution): constructors for closed monoidal day convolution monoidal structures merge-conflict t-category-theory merge conflict
28623 gilesgshaw feat(Logic/Basic): minor additions and simplification of proofs merge-conflict t-logic new-contributor merge conflict
28286 bwangpj feat(Geometry/Manifold/ContMDiff): basic lemmas for analytic (`C^ω`) functions awaiting-author t-differential-geometry new-contributor awaiting author
28804 grunweg feat: a few more tactic linters blocked-by-other-PR merge-conflict t-meta blocked on another PR
13036 joelriou feat(CategoryTheory/Sites): under certain conditions, cover preserving functors preserve 1-hypercovers WIP merge-conflict t-category-theory labelled WIP
29527 kim-em feat: script for checking Github URLs WIP CI labelled WIP
27335 eric-wieser chore(Data/List): use simp-normal-form for boolean equalities merge-conflict t-data failing CI
25778 thefundamentaltheor3m feat: Monotonicity of `setIntegral` for nonnegative functions awaiting-author t-measure-probability new-contributor awaiting author
22517 j-loreaux feat: `ℕ+` powers in semigroups WIP merge-conflict large-import ⚠️ labelled WIP
27933 grunweg chore(OrdNode): format code example in code blocks merge-conflict t-data merge conflict
29615 eric-wieser chore: add a computable shortcut for `AddCommMonoid ℂ` easy t-analysis bench-after-CI failing CI
28802 grunweg feat: a tactic linter for continuity/measurability which can be `fun_prop` merge-conflict t-meta awaiting-CI large-import does not pass CI
25069 erdOne feat(EllipticCurve): rational points of singular nodal cubics awaiting-author merge-conflict t-algebraic-geometry merge conflict
25070 erdOne feat(EllipticCurve): rational points on singular cuspidal cubics awaiting-author merge-conflict t-algebraic-geometry merge conflict
26670 yu-yama feat(GroupExtension/Abelian): define `conjClassesEquivH1` awaiting-author merge-conflict t-algebra merge conflict
26154 ADedecker refactor: add refactored APIs for algebraic filter bases merge-conflict t-topology merge conflict
27024 grunweg feat: Gram-Schmidt orthonormalisation for sections of a vector bundle awaiting-author merge-conflict t-differential-geometry merge conflict
28580 kmill refactor: simplify implementation of `filter_upwards` merge-conflict t-meta t-order failing CI
29605 alreadydone experiment(Algebra): unbundle npow/zpow from Monoid/InvDivMonoid merge-conflict awaiting-CI t-algebra does not pass CI
29010 grunweg chore: more tests for field_simp features and edge cases failing CI
27937 madvorak feat(Logic/Basic): `congr_heq₂` awaiting-author t-logic awaiting author
7125 eric-wieser feat: additive monoid structure via biproducts WIP merge-conflict awaiting-CI t-category-theory labelled WIP
27950 alreadydone feat(MonoidAlgebra): criteria for `single` to be a unit, irreducible or prime WIP merge-conflict t-algebra labelled WIP
28067 grunweg Docstring enumerations blocked-by-other-PR merge-conflict blocked on another PR
29870 mckoen feat(CategoryTheory/Adhesive): subobjects in adhesive categories have binary coproducts WIP t-category-theory labelled WIP
28908 joelriou feat(CategoryTheory): Pullback functors on `Over` categories in `Type` have right adjoints awaiting-author merge-conflict t-category-theory failing CI
25480 ocfnash feat: define a concrete model of the `𝔤₂` root system WIP merge-conflict t-algebra large-import labelled WIP
29330 plp127 chore: define `Fin.cycleIcc` with conditions merge-conflict t-group-theory merge conflict
29588 Periecle feat(Analysis/Complex/Residue): Implement residue theory for complex functions at isolated singularities awaiting-author t-analysis new-contributor failing CI
26304 Raph-DG feat(AlgebraicGeometry): Definition of algebraic cycles blocked-by-other-PR merge-conflict RFC t-algebraic-geometry blocked on another PR
27829 dupuisf feat: modify `cfc_tac` to use `grind` WIP merge-conflict ⚠️ labelled WIP
21950 erdOne feat(NumberTheory/Padics): the completion of `ℚ` at a finite place is `ℚ_[p]` merge-conflict t-number-theory merge conflict
12278 Rida-Hamadani feat(Combinatorics/SimpleGraph): Provide iff statements for distance equal and greater than 2 awaiting-author merge-conflict t-combinatorics failing CI
29092 zhuyizheng feat(MeasureTheory): add absolutely continuous functions, FTC and integration by parts awaiting-author merge-conflict t-measure-probability new-contributor merge conflict
26178 ppls-nd-prs feat(CategoryTheory/Limits): Fubini for products awaiting-author merge-conflict t-category-theory new-contributor merge conflict
27214 robin-carlier feat(CategoryTheory/Limits/Shapes/Pullback/Categorical): Categorical pullback squares merge-conflict t-category-theory merge conflict
27391 robin-carlier feat(CategoryTheory/Limits/Shapes/Pullback/Categorical): pseudofunctoriality structure of categorical pullback squares blocked-by-other-PR merge-conflict t-category-theory blocked on another PR
27432 robin-carlier feat(CategoryTheory/Limits/Shapes/Pullback/Categorical): pseudofunctoriality of categorical pulback squares blocked-by-other-PR merge-conflict t-category-theory blocked on another PR
27481 robin-carlier feat(CategoryTheory/Limits/Shapes/Pullback/Categorical): adjunctions and equivalences of categorical pullback squares blocked-by-other-PR merge-conflict t-category-theory large-import blocked on another PR
27686 robin-carlier feat(CategoryTheory/Limits/Shapes/Pullback/Categorical/Square): more API for `CatPullbackSquare` blocked-by-other-PR merge-conflict t-category-theory large-import blocked on another PR
27687 robin-carlier feat(CategoryTheory/Limits/Shapes/Pullback/Categorical): squares equivalent to a `CatPullbackSquare` blocked-by-other-PR merge-conflict t-category-theory large-import blocked on another PR
27688 robin-carlier feat(CategoryTheory/Limits/Shapes/Pullback/Categorical): coherence statement for `CatPullbackSquare.inverse` blocked-by-other-PR merge-conflict t-category-theory large-import blocked on another PR
27689 robin-carlier feat(CategoryTheory/Limits/Shapes/Pullback/Categorical): horizontal pasting calculus for `CatPullbackSquare` blocked-by-other-PR merge-conflict t-category-theory large-import blocked on another PR
27690 robin-carlier feat(CategoryTheory/Limits/Shapes/Pullback/Categorical): vertical pasting calculus for `CatPullbackSquare` blocked-by-other-PR merge-conflict t-category-theory large-import blocked on another PR
27740 robin-carlier feat(CategoryTheory/Limits/Shapes/Pullback/Categorical): pasting calculus for `CategoricalPullback` blocked-by-other-PR merge-conflict t-category-theory large-import blocked on another PR
26330 Timeroot feat: "Junk value" test file awaiting-author t-data awaiting author
28452 plp127 feat: Define `ZMod.fintype` without cases awaiting-author t-data awaiting author
26466 robin-carlier feat(AlgebraicTopology/SimplexCategory/Augmented): the canonical monoid object in the augmented simplex category merge-conflict t-category-theory t-algebraic-topology merge conflict
28074 grunweg Isbilinearmap WIP merge-conflict labelled WIP
26579 robin-carlier feat(CategoryTheory/Limits/Pullbacks/Categorical/CatCospanTransform): equivalences of categorical cospans blocked-by-other-PR merge-conflict t-category-theory large-import blocked on another PR
26578 robin-carlier feat(CategoryTheory/Limits/Pullbacks/Categorical/CatCospanTransform): adjunctions of categorical cospans merge-conflict t-category-theory large-import merge conflict
27634 agjftucker fix(Analysis/Calculus/Implicit): consistently rename {`map`, `fun`, `function`} to `fun` blocked-by-other-PR merge-conflict t-analysis blocked on another PR
28245 robin-carlier feat(CategoryTheory/Bicategory/NaturalTransformation/Icon): strict associativity and unitality of icon composition WIP blocked-by-other-PR merge-conflict awaiting-CI t-category-theory large-import blocked on another PR
30079 dagurtomas feat(CategoryTheory): IsSheafFor as a multiequalizer condition WIP t-category-theory labelled WIP
29012 grunweg chore: reduce `Topology` imports in `Data` merge-conflict file-removed failing CI
26601 yuma-mizuno feat(CategoryTheory): make `Functor.comp` irreducible WIP merge-conflict t-category-theory labelled WIP
19860 YaelDillies refactor: review the `simps` projections of `OneHom`, `MulHom`, `MonoidHom` WIP t-algebra labelled WIP
25740 robin-carlier feat(AlgebraicTopology/SimplexCategory/GeneratorsRelations): `SimplexCategoryGenRel.toSimplexCategory` is an equivalence blocked-by-other-PR merge-conflict large-import t-algebraic-topology blocked on another PR
23621 astrainfinita chore: deprecate `LinearOrderedComm{Monoid, Group}WithZero` merge-conflict t-algebra t-order merge conflict
28630 Antidite feat(Archive/Imo): right isosceles configuration in the complex plane awaiting-author new-contributor IMO awaiting author
30192 erdOne feat(RingTheory): valuative topology = adic topology for discrete rank 1 valuations WIP merge-conflict t-topology t-ring-theory labelled WIP
26886 pechersky feat(NumberTheory/Padics/ValuativeRel): ValuativeRel ℚ_[p] WIP blocked-by-other-PR merge-conflict t-number-theory t-analysis t-algebra blocked on another PR
27073 pechersky feat(Archive/Examples/Local): files showcasing properties of local fields awaiting-author t-number-theory awaiting author
27314 pechersky feat(TopologyValued): `Valued` based on a range topology blocked-by-other-PR merge-conflict t-topology blocked on another PR
30135 erdOne feat(RingTheory): `ValuativeRel` on subrings awaiting-author t-ring-theory awaiting author
25992 Multramate feat(RingTheory/Ideal/Span): add pair lemmas awaiting-author merge-conflict t-ring-theory merge conflict
29587 uniwuni feat(GroupTheory/Finiteness): define finitely generated semigroups merge-conflict ⚠️ merge conflict
16239 Rida-Hamadani feat(Geometry/Manifold): orientable manifolds awaiting-author merge-conflict t-differential-geometry failing CI
16553 grunweg WIP: tinkering with orientable manifolds WIP blocked-by-other-PR merge-conflict t-differential-geometry blocked on another PR
28328 pechersky chore(Topology/Valued): golf using local finite order of WithZeroTopology blocked-by-other-PR merge-conflict t-number-theory t-topology t-algebra large-import blocked on another PR
29282 Jlh18 feat(CategoryTheory): HasColimits instance on Grpd blocked-by-other-PR merge-conflict new-contributor ⚠️ blocked on another PR
16773 arulandu feat(Probability/Distributions): formalize Beta distribution awaiting-author merge-conflict t-measure-probability new-contributor failing CI
26284 plp127 feat: faster implementation of `Nat.primeFactorsList` + `@[csimp]` lemma awaiting-author t-data awaiting author
27990 kckennylau feat(Counterexamples): a nontrivial valuation with discrete topology merge-conflict t-ring-theory merge conflict
28243 robin-carlier chore(CategoryTheory/Bicategory): move some `eqToHom` lemmas awaiting-author merge-conflict t-category-theory merge conflict
9273 grunweg feat: extended charts are local diffeomorphisms on their source awaiting-author merge-conflict t-differential-geometry merge conflict
29120 eric-wieser feat: add a typeclass for the indiscrete topology merge-conflict t-topology failing CI
21853 smmercuri feat: the adele ring of a number field is locally compact WIP merge-conflict t-number-theory large-import labelled WIP
26913 Paul-Lez feat(NumberTheory/{*}): add a few lemmas about number field and cyclotomic extensions WIP merge-conflict awaiting-CI t-number-theory t-algebra labelled WIP
27302 tristan-f-r feat(Fintype/Quotient): finLiftOn₂ awaiting-author t-data awaiting author
28925 grunweg chore: remove `linear_combination'` tactic merge-conflict awaiting-zulip file-removed awaiting a zulip discussion
29432 lecopivo feat: `data_synth` tactic to prove `HasFDerivAt 𝕜 f ?f' x` and similar WIP t-meta labelled WIP
29855 eric-wieser chore(Data/Finset/Sort): lemmas about `0 : Fin _` and `Fin.last _` delegated easy t-order t-data failing CI
19616 adamtopaz fix: fix the definition of the absolute Galois group of a field awaiting-author merge-conflict t-number-theory t-algebra merge conflict
28826 alreadydone feat(CategoryTheory): Additive and Linear when Hom types are only monoids WIP merge-conflict awaiting-CI t-category-theory labelled WIP
28152 Sebi-Kumar feat(AlgebraicTopology): characterize simply connectedness in terms of loops blocked-by-other-PR merge-conflict new-contributor t-algebraic-topology blocked on another PR
30460 janithamalith feat(Nat): add lemma nat_card_orbit_mul_card_stabilizer_eq_card_group awaiting-author new-contributor t-group-theory awaiting author
25737 robin-carlier feat(AlgebraicTopology/SimplexCategory/GeneratorsRelations/NormalForms): Normal forms for `P_δ`s delegated t-category-theory t-algebraic-topology failing CI
30209 Ruben-VandeVelde feat: some TwoSidedIdeal.span lemmas awaiting-author FLT t-ring-theory awaiting author
25225 xcloudyunx feat(Combinatorics/SimpleGraph): Eulerian walk in connected graph contains all vertices awaiting-author t-combinatorics new-contributor awaiting author
27206 grhkm21 feat(CategoryTheory/Adjunction): partial adjoints are adjoints awaiting-author t-category-theory failing CI
27196 YaelDillies refactor(Polynomial/Bivariate): swap `X` and `Y` for improved notation WIP t-algebra toric labelled WIP
24532 robertmaxton42 feat(LinearAlgebra/FreeProduct): fill out the `FreeProduct.asPowers` namespace merge-conflict t-algebra failing CI
27683 dupuisf feat: grind tags for set operations merge-conflict t-data failing CI
30828 DeVilhena-Paulo feat: implementation of `Finmap.merge` new-contributor t-data failing CI
25978 Bergschaf feat(Order/Sublocale): Open Sublocales merge-conflict t-order merge conflict
29355 girving feat(Trigonometric): Taylor series bounds for sin and cos merge-conflict t-analysis failing CI
30902 adomani chore: longLine warnings happen starting at the 101st character t-linter awaiting-zulip awaiting a zulip discussion
28298 thorimur chore: dedent `to_additive` docstrings documentation awaiting-author merge-conflict merge conflict
28737 astrainfinita refactor: deprecate `MulEquivClass` awaiting-author merge-conflict t-algebra merge conflict
28676 sun123zxy feat(NumberTheory/ArithmeticFunction): wrap `Nat.totient` as an `ArithmeticFunction` awaiting-author merge-conflict t-number-theory new-contributor large-import merge conflict
30462 grunweg Everything I wanted about immersions blocked-by-other-PR merge-conflict blocked on another PR
30421 grunweg WIP: support products in the differential geometry elaborators merge-conflict failing CI
30299 franv314 feat(Topology/Instances): Cantor set awaiting-author merge-conflict t-topology new-contributor file-removed merge conflict
30303 franv314 chore(Topology/Instances): add deprecated module blocked-by-other-PR merge-conflict new-contributor blocked on another PR
30900 vihdzp feat: run-length encoding blocked-by-other-PR merge-conflict t-data large-import blocked on another PR
30667 FrederickPu Subgroup mul awaiting-author t-algebra new-contributor awaiting author
27976 smmercuri feat: `ramificationIdx` for `NumberField.InfinitePlace` WIP merge-conflict t-number-theory labelled WIP
30975 mariainesdff feat(Data/Finsupp/Defs): add Finsupp.restrict awaiting-author t-data awaiting author
26357 javra feat(CategoryTheory): linear categories as `ModuleCat R`-enriched categories awaiting-author merge-conflict t-category-theory large-import merge conflict
26085 grunweg feat: disjoint unions distribute with products of manifolds WIP please-adopt merge-conflict t-differential-geometry looking for help
27180 ADedecker feat: quotient of a monoid with zero by a multiplicative congruence delegated merge-conflict t-algebra merge conflict
30790 urkud chore: partially migrate from `ContinuousMap.continuous` merge-conflict failing CI
30408 kckennylau feat(RingTheory): more algebra instances for HomogeneousLocalization and linear constructors t-ring-theory failing CI
29871 zach1502 feat(Matrix/Transvection): Gauss pivot determinant identity and pivot preservation awaiting-author t-algebra new-contributor awaiting author
26259 Raph-DG feat(Topology): Connecting different notions of locally finite awaiting-author merge-conflict t-topology merge conflict
30109 scholzhannah feat: the subcomplexes of a (relative classical) CW complex form a completely distributive lattice awaiting-author t-topology awaiting author
25692 Whysoserioushah feat(RingTheory/MatrixAlgebra): add a more general version of `matrixEquivTensor` awaiting-author merge-conflict t-ring-theory merge conflict
29774 Raph-DG feat(AlgebraicGeometry): Order of vanishing of elements of the function field of locally noetherian, integral schemes blocked-by-other-PR merge-conflict file-removed ⚠️ blocked on another PR
25012 urkud refactor(*): migrate from `Matrix.toLin'` to `Matrix.mulVecLin` merge-conflict failing CI
29638 yuma-mizuno feat(CategoryTheory): define descent data by presieves WIP merge-conflict t-category-theory labelled WIP
22361 rudynicolop feat(Computability/NFA): nfa closure properties awaiting-author merge-conflict new-contributor t-computability awaiting-zulip awaiting a zulip discussion
30158 nicolaviolette feat: combinatorics simplegraph basic awaiting-author t-combinatorics new-contributor awaiting author
27708 vihdzp feat: unions and intersections of ordinals are ordinals awaiting-author merge-conflict t-set-theory merge conflict
30431 kckennylau feat(RingTheory): a homogeneous submodule is the span of its homogeneous elements t-ring-theory failing CI
27229 WilliamCoram feat(GroupTheory/DoubleCoset): multiple lemmas new-contributor FLT t-group-theory failing CI
27516 gaetanserre feat: add rational approximation lemma for suprema in `unitInterval` awaiting-author t-topology awaiting author
29550 Raph-DG feat(RingTheory): Order of vanishing in a discrete valuation ring awaiting-author merge-conflict file-removed t-ring-theory failing CI
28132 dupuisf feat: preliminary `grind` tags for `IsUnit` merge-conflict t-algebra merge conflict
25903 pfaffelh feat(MeasureTheory): finite unions of sets in a semi-ring (in terms of measure theory) form a ring blocked-by-other-PR merge-conflict t-measure-probability large-import blocked on another PR
26735 Raph-DG feat(AlgebraicGeometry): The codimension of a point of a scheme is equal to the krull dimension of the stalk awaiting-author merge-conflict t-algebraic-geometry large-import failing CI
29992 vlad902 feat(Order): finite (Max)Chains always contains a top/max element WIP merge-conflict t-order large-import labelled WIP
26901 5hv5hvnk feat: a simproc version of `compute_degree` awaiting-author merge-conflict t-meta awaiting-CI new-contributor does not pass CI
31020 grunweg feat: mfderiv of Sum.inl and Sum.inr WIP merge-conflict ⚠️ labelled WIP
31348 PatrickMassot chore: fix a docstring typo documentation awaiting-author easy t-analysis awaiting author
28685 mitchell-horner feat(Combinatorics/SimpleGraph): prove the minimal-degree version of the Erdős-Stone theorem WIP blocked-by-other-PR merge-conflict t-combinatorics blocked on another PR
25775 emilyriehl feat(AlgebraicTopology/SimplicialSet/NerveAdjunction): to Strict Segal 2 awaiting-author merge-conflict t-category-theory infinity-cosmos t-algebraic-topology ❌? infrastructure-related CI failing
14752 AntoineChambert-Loir fix(Topology/Algebra/Valued): repair definition of Valued WIP merge-conflict t-topology t-algebra labelled WIP
29145 JovanGerb chore: use `to_additive` in more places t-meta awaiting-CI does not pass CI
26827 pechersky feat(Analysis/Normed/ValuativeRel): helper instance for NormedField merge-conflict t-number-theory t-analysis t-algebra merge conflict
29458 LiamSchilling feat(MvPolynomial/WeightedHomogenous): relate `weightedTotalDegree` to `degrees` and `degreeOf` awaiting-author new-contributor t-ring-theory awaiting author
29014 ShreckYe feat(Data/List/Scan): some theorems that relate `scanl` with `foldl` merge-conflict t-data merge conflict
30150 imbrem feat(CategoryTheory/Monoidal): to_additive for MonoidalCategory merge-conflict t-meta t-category-theory new-contributor awaiting-zulip large-import awaiting a zulip discussion
30258 imbrem feat(CategoryTheory/Monoidal): to_additive for proofs using `monoidal` blocked-by-other-PR merge-conflict new-contributor large-import ⚠️ blocked on another PR
30260 imbrem feat(CategoryTheory/Monoidal): added CocartesianMonoidalCategory blocked-by-other-PR merge-conflict new-contributor large-import ⚠️ blocked on another PR
26973 peabrainiac feat(Geometry/Diffeology): diffeologies generated from sets of plots blocked-by-other-PR merge-conflict t-differential-geometry blocked on another PR
27274 peabrainiac feat(Geometry/Diffeology): continuous diffeologies & D-topology-lemmas blocked-by-other-PR merge-conflict t-differential-geometry blocked on another PR
25765 JovanGerb feat(gcongr): lemma for rewriting inside divisibility delegated t-data delegated
31388 b-mehta feat(Topology/Order): add unordered versions of topological Rolle's theorem awaiting-author merge-conflict t-analysis tech debt merge conflict
27953 CoolRmal feat(ProbabilityTheory): Conditional Jensen's Inequality blocked-by-other-PR merge-conflict t-measure-probability new-contributor blocked on another PR
30824 grunweg wip: another smoothness lemma for local frames WIP merge-conflict t-differential-geometry labelled WIP
30322 kckennylau feat(RingTheory): base change of graded algebra awaiting-author merge-conflict t-ring-theory merge conflict
30399 kckennylau feat(RingTheory): make HomogeneousLocalization.map take a graded ring hom blocked-by-other-PR merge-conflict ⚠️ blocked on another PR
10235 urkud feat: add `Decidable`, `Fintype`, `Encodable` linters awaiting-author merge-conflict t-meta t-linter large-import awaiting-bench failing CI
31593 Ruben-VandeVelde feat: some lemmas about MonoidAlgebra awaiting-author merge-conflict t-algebra merge conflict
31596 grunweg chore: remove extraneous uses of push_neg WIP merge-conflict labelled WIP
30357 grunweg chore: golf using custom elaborators blocked-by-other-PR merge-conflict t-differential-geometry awaiting-bench blocked on another PR
26885 pechersky feat(Topology/ValuativeRel): ValuativeTopology 𝒪[K] t-number-theory t-topology t-algebra failing CI
26087 grunweg feat: a `SliceModel` typeclass for models with corners for embedded submanifolds merge-conflict t-differential-geometry failing CI
15651 TpmKranz feat(Computability/NFA): operations for Thompson's construction awaiting-author merge-conflict new-contributor t-computability awaiting-zulip awaiting a zulip discussion
12032 mcdoll feat: delta distribution as a limit WIP t-analysis labelled WIP
26240 grunweg perf(CommandLinterLinter): use Substring more merge-conflict RFC t-linter merge conflict
9693 madvorak feat: Linear programming in the standard form WIP merge-conflict RFC t-algebra labelled WIP
22464 adomani feat(CI): declarations diff in Lean awaiting-author CI awaiting author
27392 Paul-Lez feat(Tactic/SimpUtils): add simproc finding commands awaiting-author merge-conflict t-meta large-import file-removed failing CI*
29909 Vierkantor feat(CI): add build output to CI workflows merge-conflict CI merge conflict
15649 TpmKranz feat(Computability): introduce Generalised NFA as bridge to Regular Expression awaiting-author merge-conflict new-contributor t-computability awaiting-zulip awaiting a zulip discussion
28070 grunweg style: improve indentation of multi-linear enumerations in doc-strings merge-conflict failing CI
20238 maemre feat(Computability/DFA): Closure of regular languages under some set operations awaiting-author merge-conflict new-contributor t-computability awaiting-zulip awaiting a zulip discussion
5745 alexjbest feat: a tactic to consume type annotations, and make constructor nicer awaiting-author merge-conflict t-meta merge conflict
5863 eric-wieser feat: add elaborators for concrete matrices help-wanted blocked-by-other-PR merge-conflict t-meta blocked on another PR
5919 MithicSpirit feat: implement orthogonality for AffineSubspace help-wanted WIP merge-conflict t-analysis new-contributor looking for help
7386 madvorak feat: Define linear programs WIP merge-conflict RFC t-algebra labelled WIP
9352 chenyili0818 feat: arithmetic lemmas for `gradient` awaiting-author merge-conflict t-analysis merge conflict
9795 sinhp feat: the type `Fib` of fibre of a function at a point awaiting-author merge-conflict t-category-theory merge conflict
10660 eric-wieser feat(LinearAlgebra/CliffordAlgebra): construction from a basis WIP awaiting-author merge-conflict t-algebra labelled WIP
10977 grunweg feat: germs of smooth functions awaiting-author merge-conflict t-differential-geometry t-topology t-analysis failing CI
10998 hmonroe feat(Logic): Arithmetization of partial recursive functions (toward Gödel's first incompleteness theorem) awaiting-author merge-conflict t-logic merge conflict
11890 adomani feat: the terminal refine linter awaiting-author merge-conflict t-linter merge conflict
12006 adomani feat: the `suffa` tactic awaiting-author merge-conflict t-meta merge conflict
13442 dignissimus feat: mabel tactic for multiplicative abelian groups help-wanted awaiting-author modifies-tactic-syntax merge-conflict t-meta new-contributor looking for help
14237 js2357 feat: Define the localization of a fractional ideal at a prime ideal awaiting-author merge-conflict t-algebra new-contributor failing CI
14345 digama0 feat: the Dialectica category is monoidal closed awaiting-author merge-conflict t-category-theory merge conflict
14727 jjaassoonn feat(RingTheory/Flat/CategoryTheory): a flat module has vanishing higher Tor groups awaiting-author merge-conflict t-ring-theory merge conflict
14733 jjaassoonn feat(RingTheory/Flat/CategoryTheory): a module is flat iff tensoring preserves finite limits awaiting-author merge-conflict t-ring-theory merge conflict
15055 sinhp feat: the category of pointed objects of a concrete category awaiting-author merge-conflict t-category-theory merge conflict
15224 AnthonyBordg feat(CategoryTheory/Sites): covering families and their associated Grothendieck topology awaiting-author merge-conflict t-category-theory new-contributor merge conflict
16303 grunweg feat(CI): check for badly formatted titles or missing/contradictory labels awaiting-author merge-conflict CI failing CI
18236 joelriou feat(Algebra/Category/ModuleCat/Presheaf): the endofunctor of presheaves of modules induced by an oplax natural transformation WIP awaiting-author merge-conflict awaiting-CI t-category-theory t-algebra labelled WIP
18749 GabinKolly feat(ModelTheory): preparatory work for the existence of Fraïsse limits awaiting-author merge-conflict t-logic merge conflict
18876 GabinKolly feat(ModelTheory/Fraisse): add proof that Fraïssé limits exist blocked-by-other-PR merge-conflict t-logic blocked on another PR
19323 madvorak feat: Function to Sum decomposition WIP merge-conflict t-data labelled WIP
19378 adamtopaz feat: Explanation widgets awaiting-author merge-conflict t-meta merge conflict
19456 AntoineChambert-Loir feat(Data/Finsupp/MonomialOrder/DegRevLex): homogeneous reverse lexicographic order WIP merge-conflict t-algebraic-geometry t-order t-data labelled WIP
20051 Timeroot feat: `Clone` and some instances blocked-by-other-PR awaiting-author merge-conflict t-algebra blocked on another PR
20466 MohanadAhmed feat: Sherman Morrison formula for rank 1 update of the matrix inverse awaiting-author merge-conflict t-data merge conflict
20648 anthonyde feat: formalize regular expression -> εNFA merge-conflict new-contributor t-computability awaiting-zulip awaiting a zulip discussion
20649 GabinKolly feat(ModelTheory/Graph): prove characterization of the fraisse limit of finite simple graphs WIP merge-conflict t-combinatorics t-logic large-import labelled WIP
20652 jjaassoonn feat: categorical description of center of a ring awaiting-author merge-conflict t-category-theory t-algebra failing CI
20924 tomaz1502 feat(Computability/QueryComplexity): Oracle-based computation merge-conflict t-computability failing CI
20956 tomaz1502 feat(Computability/QueryComplexity/Sort.lean): Formalization of upper bound of queries for merge sort blocked-by-other-PR merge-conflict t-computability blocked on another PR
21270 GabinKolly feat(ModelTheory/Bundled): first-order embeddings and equivalences from equalities awaiting-author merge-conflict t-logic large-import merge conflict
21277 GabinKolly feat(ModelTheory/PartialEquiv): Define the mapping of a self-partialEquiv through an embedding blocked-by-other-PR merge-conflict t-logic blocked on another PR
21616 peabrainiac feat(Topology): concatenating countably many paths awaiting-author merge-conflict t-topology merge conflict
21624 sinhp feat(CategoryTheory): The (closed) monoidal structure on the product category of families of (closed) monoidal categories awaiting-author merge-conflict t-category-theory failing CI
21829 Whysoserioushah feat(LinearAlgebra/TensorProduct/HomTensor): Add TensorProduct of Hom-modules awaiting-author merge-conflict t-algebra merge conflict
21903 yhtq feat: add from/toList between `FreeSemigroup` and `List` with relative theorems merge-conflict awaiting-CI t-algebra new-contributor large-import does not pass CI
22159 shetzl feat: add definition of pushdown automata awaiting-author merge-conflict new-contributor t-computability merge conflict
22231 pechersky feat(Algebra/Valued): `AdicExpansion` initial defns awaiting-author merge-conflict t-topology t-algebra merge conflict
22232 pechersky feat(Algebra/Valued): `AdicExpansion.apprUpto` blocked-by-other-PR merge-conflict t-topology blocked on another PR
22233 pechersky feat(Algebra/Valued): `AdicExpansion.evalAt` blocked-by-other-PR merge-conflict t-topology blocked on another PR
22302 658060 feat: add `CategoryTheory.Topos.Power` awaiting-author merge-conflict t-category-theory new-contributor merge conflict
22314 shetzl feat: add leftmost derivations for context-free grammars awaiting-author merge-conflict new-contributor t-computability merge conflict
22662 plp127 feat: Localization.Away.lift (computably) merge-conflict t-algebra merge conflict
22790 mhk119 feat: Extend `taylor_mean_remainder_lagrange` to `x < x_0` awaiting-author merge-conflict t-analysis new-contributor merge conflict
22861 eric-wieser feat: add the trace of a bilinear form awaiting-author merge-conflict t-algebra merge conflict
22919 plp127 feat(Data/Fintype/Pi): Make `Fintype` instance for `RelHom`s computable awaiting-author merge-conflict t-data merge conflict
22954 eric-wieser feat(RingTheory/Congruence/Hom): copy from GroupTheory merge-conflict t-ring-theory failing CI
23285 AntoineChambert-Loir refactor: directed systems in terms of functors WIP merge-conflict t-category-theory t-algebra large-import labelled WIP
23460 Timeroot feat: Definition of `Clone` blocked-by-other-PR merge-conflict t-algebra blocked on another PR
23503 apnelson1 feat(Topology/Instances/ENat): ENat and tsum WIP merge-conflict t-topology large-import labelled WIP
23585 plp127 feat: `Filter.atMax` and `Filter.atMin` WIP merge-conflict t-order labelled WIP
23758 erdOne feat(Topology/Algebra): linearly topologized iff non-archimedean awaiting-author merge-conflict t-topology t-algebra large-import merge conflict
23835 chrisflav feat(Topology): cardinality of connected components is bounded by cardinality of fiber awaiting-author merge-conflict t-topology failing CI
24333 xcloudyunx feat(Combinatorics/SimpleGraph): cycle graph implementation for generic vertex types awaiting-author merge-conflict t-combinatorics new-contributor merge conflict
24540 robertmaxton42 feat(Quiv): add the empty, vertex, point, interval, and walking quivers awaiting-author merge-conflict t-category-theory failing CI
24789 Ruben-VandeVelde chore: move Algebra.Group.Hom.End to Algebra.Ring awaiting-author merge-conflict t-algebra file-removed merge conflict
24850 pechersky feat(Topology/UniformSpace/Ultra): uniform spaces induced by pseudometrics are ultra if system is ultra merge-conflict t-topology merge conflict
25324 eric-wieser feat: more functorial results about DFinsupp awaiting-author merge-conflict t-algebra t-data merge conflict
25585 Paul-Lez feat(Tactic/Linters/DeprecatedSimpLemma): lint for deprecated simp lemmas awaiting-author merge-conflict t-linter failing CI
25739 literandltx feat(NumberTheory/LegendreSymbol): Add sqrt‐of‐residue theorems for p=4k+3 and p=8k+5 awaiting-author merge-conflict t-number-theory new-contributor merge conflict
25974 scholzhannah feat(Topology/Compactness/CompactlyCoherentSpace): compact coherentification (k-ification) merge-conflict t-topology large-import merge conflict
25989 Multramate feat(NumberTheory/EllipticDivisibilitySequence): add elliptic nets awaiting-author merge-conflict t-number-theory merge conflict
26051 Komyyy feat(Mathlib/GroupTheory/SpecificGroups/Alternating): A_n is simple iff n = 3 or 5 ≤ n WIP merge-conflict large-import t-group-theory labelled WIP
26061 kckennylau (WIP) feat(AlgebraicGeometry): define Projective Space WIP blocked-by-other-PR merge-conflict t-algebraic-geometry blocked on another PR
26158 upobir feat(NumberTheory/Divisors): add int divisors awaiting-author merge-conflict t-number-theory merge conflict
26160 oliver-butterley feat(MeasureTheory.VectorMeasure): add several lemmas which characterize variation blocked-by-other-PR merge-conflict t-measure-probability new-contributor blocked on another PR
26165 oliver-butterley feat(MeasureTheory.VectorMeasure): add lemma which shows that variation of a `ℝ≥0∞` VectorMeasure is equal to itself blocked-by-other-PR merge-conflict t-measure-probability new-contributor blocked on another PR
26292 RemyDegenne feat(MeasureTheory): tightness of the range of a sequence awaiting-author merge-conflict t-measure-probability failing CI
26293 RemyDegenne feat: tightness from convergence of characteristic functions WIP merge-conflict t-measure-probability labelled WIP
26300 igorkhavkine feat(Analysis/Calculus/FDeriv): continuous differentiability from continuous partial derivatives on an open domain in a product space WIP awaiting-author merge-conflict t-analysis new-contributor labelled WIP
26329 Timeroot feat: Definition of `Clone` notations and typeclasses awaiting-author merge-conflict awaiting-CI t-algebra does not pass CI
26398 ChrisHughes24 feat(ModelTheory): definable functions please-adopt merge-conflict t-logic looking for help
26399 ChrisHughes24 refactor(ModelTheory): tidy up proof of Ax-Grothendieck with definable functions blocked-by-other-PR merge-conflict t-logic blocked on another PR
26432 AntoineChambert-Loir feat(Data.Nat.LogFueled): fueled version of `clog` merge-conflict t-data failing CI
26594 metakunt feat(Algebra/Polynomial/ZMod): Add Polynomial.equiv_of_nat_of_polynomial_zmod awaiting-author merge-conflict t-algebra new-contributor merge conflict
26644 kckennylau feat(SetTheory/ZFC): Define the language of sets and state the ZFC axioms awaiting-author merge-conflict t-set-theory merge conflict
26648 eric-wieser chore(TensorProduct): remove more `suppress_compilation`s blocked-by-core-PR merge-conflict t-algebra blocked on another PR
26757 fweth feat(CategoryTheory/Topos): define elementary topos awaiting-author merge-conflict t-category-theory new-contributor failing CI
26803 bjoernkjoshanssen feat: second partial derivatives test awaiting-author merge-conflict t-analysis failing CI
26872 faenuccio chore(RingTheory/Valuation/RankOne): modify the definition of Valuation.RankOne using its range rather than its codomain blocked-by-other-PR awaiting-author merge-conflict t-algebra blocked on another PR
26914 quangvdao feat(Data/PFunctor/Univariate): more definitions for univariate `PFunctor` merge-conflict t-data merge conflict
26920 yuma-mizuno feat(Tactic.CategoryTheory): add associator inserting tactic WIP merge-conflict t-meta t-category-theory labelled WIP
26942 pechersky feat(RingTheory/Valuation/ValueGroupIso): isomorphism of value groups when compatible blocked-by-other-PR merge-conflict t-order t-ring-theory blocked on another PR
26990 joelriou feat(CategoryTheory/Abelian): Noetherian objects form a Serre class WIP merge-conflict t-category-theory labelled WIP
27098 Paul-Lez feat(Algebra/Category/ModuleCat/Sheaf/VectorBundle): define vector bundles awaiting-author merge-conflict t-algebra merge conflict
27155 Pjotr5 feat: Shearer's bound on the independence number of triangle free graphs awaiting-author merge-conflict t-combinatorics new-contributor failing CI
27163 pechersky feat(Topology/ValuativeRel): of and to basis of compatible valuations awaiting-author merge-conflict t-number-theory t-topology t-algebra merge conflict
27187 Komyyy feat: `NONote` represents ordinals < ε₀ WIP merge-conflict t-set-theory labelled WIP
27215 kckennylau feat(AlgebraicGeometry): Define the Zariski site on `CommRingCatᵒᵖ` awaiting-author merge-conflict t-algebraic-geometry merge conflict
27307 xyzw12345 feat(RingTheory/GradedAlgebra): homogeneous relation awaiting-author merge-conflict t-ring-theory merge conflict
27309 kckennylau feat(CategoryTheory): a presheaf on `CostructuredArrow F d` can be extended to a presheaf on `C` WIP merge-conflict t-category-theory labelled WIP
27321 kckennylau feat(CategoryTheory): Colimit can be computed fiberwise merge-conflict awaiting-CI t-category-theory does not pass CI
27417 PierreQuinton feat: add `SigmaCompleteLattice` awaiting-author merge-conflict t-order merge conflict
27500 Komyyy feat: the Riemann zeta function is meromorphic WIP merge-conflict t-analysis large-import labelled WIP
27534 PierreQuinton feat: a typeclass for `sSup`/`sInf` to be lawful merge-conflict t-order merge conflict
27753 YunkaiZhang233 feat(CategoryTheory): implemented proofs for factorisation categories being equivalent to iterated comma categories in two ways awaiting-author merge-conflict t-category-theory new-contributor merge conflict
27824 ChrisHughes24 feat(Calculus): exists_gt_of_deriv_pos and variants awaiting-author merge-conflict t-analysis merge conflict
27850 fyqing feat: 0-dimensional manifolds are discrete and countable awaiting-author merge-conflict t-differential-geometry new-contributor merge conflict
27973 smmercuri feat: the ring of integers of a `ℤₘ₀`-valued field is compact whenever it is a DVR and the residue field is finite awaiting-author merge-conflict t-algebra large-import merge conflict
28056 grunweg wip: existence of Riemannian metrics WIP merge-conflict t-differential-geometry labelled WIP
28072 kckennylau feat(RingTheory/Valuation): make tactic rw_val_equiv awaiting-author merge-conflict t-ring-theory merge conflict
28124 kckennylau feat(Tactic): Call an arbitrary Simproc merge-conflict t-meta failing CI
28125 nonisomorphiclinearmap feat(Combinatorics): basic definition of simplicial complexes merge-conflict t-combinatorics new-contributor merge conflict
28316 eric-wieser feat(Tactic/NormNum): better trace nodes merge-conflict t-meta failing CI
28325 pechersky feat(WithZeroTopology): `locallyCompactSpace_iff_locallyFiniteOrder_units` merge-conflict t-topology t-order large-import failing CI
28349 kckennylau feat(Meta): add notation for naming stacked polynomials awaiting-author merge-conflict t-meta merge conflict
28530 nonisomorphiclinearmap feat(Combinatorics/SimplicialComplex/Topology): add standard simplices and geometric realisation (colimit + functoriality) blocked-by-other-PR merge-conflict t-combinatorics new-contributor blocked on another PR
28868 yury-harmonic feat(Positive): add `OfNat` instance merge-conflict t-algebra large-import failing CI
28871 JaafarTanoukhi feat(Combinatorics/Digraph): Tournaments merge-conflict t-combinatorics new-contributor merge conflict
29055 vihdzp feat: `Ordinal.toENat` awaiting-author merge-conflict t-set-theory merge conflict
29108 JonBannon feat(MeasureTheory): add `LInfty.lean` with `Mul` and `const` related results. awaiting-author merge-conflict t-measure-probability merge conflict
29411 llllvvuu feat(LinearAlgebra/Matrix/Rank): rank factorization awaiting-author merge-conflict ⚠️ merge conflict
29425 pechersky feat(NumberTheory/Padics/Torsion): `HasEnoughRootsOfUnity ℤ_[p] (p - 1)` blocked-by-other-PR awaiting-author merge-conflict t-ring-theory blocked on another PR
29500 vihdzp feat: `WellFoundedLT (LowerSet α)` awaiting-author merge-conflict t-order merge conflict
29526 llllvvuu feat: `Multiset.map f` identifies `f` up to permutation merge-conflict t-data merge conflict
29610 llllvvuu feat(LinearAlgebra): define LinearMap.Eigenbasis merge-conflict t-algebra merge conflict
29675 yury-harmonic feat(Wolstenholme): new file help-wanted awaiting-author merge-conflict t-data looking for help
29720 javra feat(CategoryTheory): `TransportEnrichment` and `ForgetEnrichment` as 2-functors WIP merge-conflict t-category-theory labelled WIP
29827 js2357 feat: define two (trivial) ContinuousMulEquivs merge-conflict t-topology FLT large-import failing CI
29947 JaafarTanoukhi feat(Combinatorics/Digraph): Maps merge-conflict t-combinatorics new-contributor merge conflict
29965 RemyDegenne feat(probability): define subtraction of kernels WIP merge-conflict t-measure-probability labelled WIP
30001 vihdzp feat: concept generated by set of objects/attributes blocked-by-other-PR merge-conflict t-order blocked on another PR
30004 luigi-massacci feat(MeasureTheory/Integral/TestAgainst): integrating BCFs against a finite measure or an L1Loc map as CLMs awaiting-author merge-conflict t-analysis t-measure-probability merge conflict
30042 JovanGerb feat(push): `@[push]` attributes for `∈` in `Set`, `Finset` and `Multiset` awaiting-author merge-conflict t-meta merge conflict
30077 agjftucker feat(Analysis/Calculus/ImplicitFunOfBivariate): define implicitFunOfBivariate blocked-by-other-PR merge-conflict t-analysis blocked on another PR
30121 idontgetoutmuch Principal fiber bundle core awaiting-author merge-conflict t-differential-geometry new-contributor merge conflict
30312 kckennylau feat(RingTheory): define graded ring homomorphisms blocked-by-other-PR merge-conflict t-ring-theory blocked on another PR
30334 kckennylau feat(RingTheory): define maps of homogeneous ideals blocked-by-other-PR merge-conflict t-ring-theory blocked on another PR
30355 kckennylau feat(Logic): graded functions merge-conflict t-data merge conflict
30365 kckennylau feat(RingTheory): define R-linear graded algebra homomorphism blocked-by-other-PR merge-conflict ⚠️ blocked on another PR
30367 kckennylau feat(Data): define grading-preserving isomorphisms blocked-by-other-PR merge-conflict t-data blocked on another PR
30379 kckennylau feat(RingTheory): isomorphism of graded rings blocked-by-other-PR merge-conflict ⚠️ blocked on another PR
30451 kckennylau feat(HomogeneousIdeal): generalize to homogeneous submodule merge-conflict t-ring-theory failing CI
30933 joelriou feat(CategoryTheory): the linearization of a category awaiting-author merge-conflict t-category-theory merge conflict
31008 RemyDegenne refactor: generalize the index of the process in the Doob decomposition WIP merge-conflict t-measure-probability labelled WIP
31102 JOSHCLUNE Require LeanHammer merge-conflict new-contributor failing CI
31194 grunweg feat: add `#check'` command and tactic, which only show explicit arguments awaiting-author merge-conflict t-meta merge conflict
31351 grunweg feat: manifolds with smooth boundary WIP merge-conflict t-differential-geometry labelled WIP
31356 adomani feat: add inspect-like functions merge-conflict t-meta merge conflict
31580 grunweg feat: towards `ContMDiff` support in fun_prop WIP blocked-by-other-PR merge-conflict t-meta t-differential-geometry blocked on another PR
31604 maksym-radziwill feat: analyticity of dslope awaiting-author merge-conflict t-analysis merge conflict
31613 xyzw12345 feat(RepresentationTheory/GroupCohomology): Non-abelian Group Cohomology WIP merge-conflict t-algebra large-import labelled WIP
31738 robertmaxton42 feat: quivers can be represented as functors from the walking quiver awaiting-author merge-conflict t-category-theory failing CI
26777 YaelDillies chore(Data/Set/Image): move `BooleanAlgebra` material to `Order` WIP t-data labelled WIP
23881 YaelDillies feat: `ℝ≥0`-valued Lᵖ norm awaiting-author t-measure-probability awaiting author
21915 YaelDillies feat: simproc for `Int.divisorsAntidiag` WIP t-meta labelled WIP
21342 YaelDillies refactor(Normed/Group/Quotient): generalise to non-abelian groups WIP t-analysis labelled WIP
19475 YaelDillies feat: group markings WIP blocked-by-other-PR t-algebra blocked on another PR
15443 YaelDillies feat: Marcinkiewicz-Zygmund inequality WIP t-analysis labelled WIP
30083 grunweg feat: local frames in a vector bundle awaiting-author merge-conflict t-differential-geometry failing CI
30339 grunweg feat: extend a tangent vector for a locally smooth vector field blocked-by-other-PR merge-conflict t-differential-geometry blocked on another PR
31338 grunweg chore: move Pretrivialization, Trivialization to the Bundle namespace blocked-by-other-PR merge-conflict t-differential-geometry blocked on another PR
31339 grunweg Movelemma blocked-by-other-PR merge-conflict blocked on another PR
31590 SuccessMoses chore: tag `commutatorElement_def` with `simp` awaiting-author t-algebra new-contributor failing CI
31587 JovanGerb Lean pr testing 11156 WIP merge-conflict labelled WIP*
25802 dagurtomas feat(AlgebraicTopology): anodyne morphisms of simplicial sets WIP t-topology labelled WIP
6268 eric-wieser fix: fixups to #3838 WIP merge-conflict labelled WIP
6859 MohanadAhmed feat: TryLean4Bundle: Windows Bundle Creator help-wanted WIP CI looking for help
6993 jjaassoonn feat: lemmas about `AddMonoidAlgebra.{divOf, modOf}` merge-conflict t-algebra merge conflict
7427 MohanadAhmed feat: eigenvalues sorted in ascending/descending order WIP merge-conflict ⚠️ labelled WIP
9339 FMLJohn feat(RingTheory/GradedAlgebra/HomogeneousIdeal): given a finitely generated homogeneous ideal of a graded semiring, construct a finite spanning set for the ideal which only contains homogeneous elements merge-conflict t-ring-theory merge conflict
9564 AntoineChambert-Loir chore: weaken commutativity assumptions for AdjoinRoot.lift and AdjoinRoot.liftHom WIP merge-conflict t-algebra ??? labelled WIP
10026 madvorak feat: linear programming according to Antoine Chambert-Loir's book WIP merge-conflict RFC t-algebra labelled WIP
10159 madvorak feat: linear programming according to Antoine Chambert-Loir's book — affine version WIP merge-conflict RFC t-algebra labelled WIP
10349 Shamrock-Frost refactor(CategoryTheory/MorphismProperty): some clean-ups merge-conflict t-category-theory ??? missing CI information
11021 jstoobysmith feat(AlgebraicTopology): add join of augmented SSets WIP merge-conflict new-contributor t-algebraic-topology labelled WIP
11800 JADekker feat: KappaLindelöf spaces please-adopt merge-conflict t-topology awaiting-zulip ??? looking for help
12087 JADekker feat: complete API for K-Lindelöf spaces blocked-by-other-PR please-adopt merge-conflict t-topology ??? blocked on another PR
12251 ScottCarnahan refactor(RingTheory/HahnSeries): several generalizations WIP merge-conflict t-algebra t-order labelled WIP
12394 JADekker feat: define pre-tight and tight measures awaiting-author please-adopt merge-conflict t-measure-probability looking for help
12452 JADekker feat(Cocardinal): add some more api awaiting-CI t-topology ??? does not pass CI
14426 adomani feat: `#min_imps` command (development branch) WIP merge-conflict ??? ⚠️ labelled WIP
14686 smorel394 feat(AlgebraicGeometry/Grassmannian): define the Grassmannian scheme WIP please-adopt merge-conflict t-algebraic-geometry workshop-AIM-AG-2024 ??? looking for help
17071 ScottCarnahan feat(LinearAlgebra/RootSystem): separation, base, cartanMatrix WIP merge-conflict t-algebra ??? labelled WIP
17471 joelriou feat(Algebra/ModuleCat/Differentials/Sheaf): the sheaf of relative differentials WIP blocked-by-other-PR merge-conflict t-category-theory t-algebraic-geometry large-import blocked on another PR
18626 hannahfechtner feat: define Artin braid groups awaiting-author merge-conflict t-algebra new-contributor merge conflict
18784 erdOne feat(AlgebraicGeometry): use `addMorphismPropertyInstances` blocked-by-other-PR merge-conflict t-algebraic-geometry blocked on another PR
19062 hannahfechtner feat(Algebra/PresentedMonoid/Basic): facts about rel awaiting-author t-algebra awaiting author
19607 madvorak feat: block matrices are totally unimodular WIP blocked-by-other-PR merge-conflict ⚠️ blocked on another PR
20029 FrederickPu feat(Tactic/simps): allow for Config attributes to be set directly WIP merge-conflict t-meta new-contributor labelled WIP
21269 658060 feat(CategoryTheory/Topos): basic definitions and results in topos theory WIP awaiting-author merge-conflict t-category-theory new-contributor labelled WIP
22805 ScottCarnahan feat(FieldTheory/Finite): fixed points of Frobenius automorphism WIP merge-conflict t-algebra labelled WIP
23772 SEU-Prime feat: Amice equivalence WIP t-number-theory ??? labelled WIP
23990 robertmaxton42 feat(Types.Colimits): Quot is functorial and colimitEquivQuot is natural awaiting-author merge-conflict t-category-theory new-contributor merge conflict
24533 robertmaxton42 feat(ULift): conjugation by ULift.up/down, misc cast/heq lemmas awaiting-author t-data awaiting author
24690 ScottCarnahan feat(Data.Prod): reverse lexicographic order WIP merge-conflict t-order labelled WIP
24692 ScottCarnahan feat(RingTheory/HahnSeries/Basic): isomorphism of Hahn series induced by order isomorphism WIP merge-conflict t-order labelled WIP
25034 ScottCarnahan feat(Algebra/Module/Equiv/Basic): Restriction of scalars from a semilinear equivalence to a linear equivalence WIP t-algebra labelled WIP
25035 ScottCarnahan feat(Algebra/Module/Equiv/Defs): linear equivalence between linear hom and semilinear hom WIP t-algebra labelled WIP
25831 ScottCarnahan feat(RingTheory/HahnSeries): Powers of a binomial WIP merge-conflict t-ring-theory labelled WIP
25906 pfaffelh feat(Topology/Compactness/CompactSystem): closed and compact square cylinders form a compact system blocked-by-other-PR merge-conflict t-topology blocked on another PR
26013 tsuki8 feat(Data/Finset/Card,Data/Set/Finite/Basic): TODO needs a better title awaiting-author new-contributor t-data awaiting author
25900 pfaffelh feat(Topology/Compactness/CompactSystem): set system of finite unions of sets in a compact system is again a compact system blocked-by-other-PR merge-conflict t-topology blocked on another PR
26455 ScottCarnahan feat(LinearAlgebra/RootSystem): API for CartanMatrix WIP merge-conflict t-algebra labelled WIP
26770 Jun2M feat(Combinatorics/Graph): subgraph relations on `Graph` merge-conflict t-combinatorics merge conflict
26804 kckennylau feat(SetTheory): ZFSet is a model of ZFC WIP merge-conflict t-set-theory labelled WIP
26881 emo916math feat(Analysis/Calculus/Deriv/Star): a formula for `deriv (conj ∘ f ∘ conj)` awaiting-author t-analysis new-contributor awaiting author
26890 robin-carlier feat(CategoryTheory/Monoidal/DayConvolution): more API for `DayFunctor` merge-conflict t-category-theory merge conflict
26310 kckennylau feat: binary forms awaiting-author merge-conflict t-algebra merge conflict
26283 kckennylau feat: resultant of polynomials WIP merge-conflict t-algebra labelled WIP
27991 sinianluoye feat(Rat): add Rat.den_eq_of_add_den_eq_one and its dependent lemmas awaiting-author new-contributor t-data failing CI
28215 5hv5hvnk feat: strong and Weak connectivity for Digraphs WIP awaiting-author merge-conflict t-combinatorics new-contributor labelled WIP
28970 Whysoserioushah feat(Algebra/Algebra/ReducedNorm): defines reduced norm and trace awaiting-author merge-conflict t-algebra merge conflict
29212 Whysoserioushah feat(Algebra/CrossProductAlgebra/Defs): define Cross Product Algebra awaiting-author merge-conflict t-algebra merge conflict
29281 plp127 doc: `Fin.natAdd_castLEEmb` merge-conflict t-data merge conflict
29514 grunweg feat(CI): use more strict mode WIP merge-conflict CI labelled WIP
29574 JarodAlper feat: regular local rings are domains merge-conflict new-contributor t-ring-theory failing CI
29792 robertmaxton42 feat(RelCWComplex): a (relative, concrete) CW complex is the colimit of its skeleta blocked-by-other-PR merge-conflict large-import ⚠️ blocked on another PR
28718 imbrem feat: class for chosen finite coproducts blocked-by-other-PR awaiting-author merge-conflict t-category-theory new-contributor blocked on another PR
30352 kckennylau feat(RingTheory): Homogeneous localization of tensor product WIP blocked-by-other-PR merge-conflict ⚠️ blocked on another PR
30366 sinhp feat(CategoryTheory): The Preliminaries for Locally Cartesian Closed Categories awaiting-author merge-conflict t-category-theory merge conflict
31411 CoolRmal feat: a convex lower-semicontinuous function is the supremum of a sequence of affine functions in a separable space blocked-by-other-PR merge-conflict t-analysis new-contributor blocked on another PR
26765 KiringYJ feat(MeasureTheory/PiSystem): add π-λ theorem and SetLike instance awaiting-author t-measure-probability new-contributor awaiting author
29409 Julian feat(Mathlib/Analysis): deriv_eq_self and deriv_exp_iff awaiting-author t-analysis awaiting author
31513 FLDutchmann feat(Tactic): `polynomial` tactic blocked-by-other-PR merge-conflict t-meta blocked on another PR
27306 xyzw12345 feat: `lie_ring` tactic and `LieReduce` command t-meta failing CI
29434 ntapiam feat(NonAssoc/LieAdmissible): prove every ring/algebra is LieAdmissible t-algebra new-contributor failing CI
27694 grunweg feat: Gram-Schmidt orthonormalisation preserves continuity of sections blocked-by-other-PR merge-conflict t-differential-geometry blocked on another PR
27025 grunweg feat: Gram-Schmidt procedure on smooth vector bundles yields smooth sections blocked-by-other-PR merge-conflict t-differential-geometry blocked on another PR
29777 yuanyi-350 feat(Functional Analysis): closed Range Theorem WIP blocked-by-other-PR awaiting-author t-analysis new-contributor blocked on another PR
28141 YaelDillies chore: deprecate `BialgHom.coe_toLinearMap` awaiting-zulip toric t-ring-theory awaiting a zulip discussion
30637 strihanje01 feat(Combinatorics/SetFamily/Lindstrom): Lindstrom's theorem for subfamilies with equal unions t-combinatorics new-contributor failing CI
31949 ADedecker chore: prefer `Pi.single i 1 j` over `fun j => if i = j then 1 else 0` awaiting-author t-algebra awaiting author
25902 pfaffelh feat: The finite product of semi-rings (in terms of measure theory) is a semi-ring. awaiting-author merge-conflict t-measure-probability large-import brownian merge conflict
31571 erdOne feat(RingTheory): existence of local algebra with given residue field awaiting-author t-ring-theory awaiting author
29517 pechersky feat(RingTheory/Torsion): torsion = union of roots of unity awaiting-author merge-conflict t-algebra failing CI
31176 mcdoll feat(Analysis): Taylor's theorem with the integral remainder awaiting-author t-analysis awaiting author
30831 chrisflav feat(AlgebraicGeometry): the fpqc topology blocked-by-other-PR t-algebraic-geometry blocked on another PR
28933 artie2000 chore(Data): correct definition for `single_apply` WIP merge-conflict labelled WIP
24627 pechersky feat(Topology/Algebra/Valued): `IsLinearTopology 𝒪[K] K` and `𝒪[K] 𝒪[K]` awaiting-author merge-conflict t-topology merge conflict
27756 grunweg feat: `Weak(Pseudo)EMetricSpace`, generalises `(Pseudo)EMetricSpace` WIP merge-conflict t-topology carleson labelled WIP
25835 erdOne WIP: Weierstrass elliptic functions WIP t-analysis labelled WIP
26975 Whysoserioushah feat: a norm_num extension for complex numbers t-meta failing CI
31817 kckennylau chore: remove extra monic hypotheses from divByMonic and modByMonic lemmas awaiting-author t-algebra t-ring-theory failing CI
24016 plp127 feat: fine uniformity merge-conflict t-topology merge conflict
30995 kckennylau feat(RingTheory): replace ofLinearEquiv with limit awaiting-author t-ring-theory awaiting author
32094 grunweg feat(runLinter): allow only running certain linters CI t-linter failing CI
32095 grunweg chore: fix some explicitVarOfIff linter errors WIP please-adopt merge-conflict looking for help
31366 FaffyWaffles feat(Analysis/SpecialFunctions/StirlingRobbins): Robbins' sharp stepwise bound for stirlingSeq awaiting-author t-analysis new-contributor awaiting author
29982 hrmacbeth feat: new `isolate` tactic awaiting-author merge-conflict t-meta large-import failing CI
31796 dobronx1325 feat(Data/Real/EReal): add mul_lt_mul_of_pos_left theorem new-contributor t-data failing CI
31007 kckennylau feat(RingTheory): generalise perfection to monoids merge-conflict ⚠️ failing CI
30463 grunweg feat: support products and disjoint unions in the differential geometry elaborators blocked-by-other-PR merge-conflict t-meta t-differential-geometry blocked on another PR
29449 mitchell-horner feat(Combinatorics/SimpleGraph): add Turán density related theorems blocked-by-other-PR t-combinatorics blocked on another PR
27258 JovanGerb feat: Imo2020 q6 awaiting-author IMO awaiting author
26138 xroblot Development branch (2) WIP merge-conflict labelled WIP
31729 thorimur chore: log on theorem type signature in unused instances in type linters blocked-by-other-PR merge-conflict large-import blocked on another PR
32157 peabrainiac feat(Analysis/Calculus): Hadamard's lemma blocked-by-other-PR t-analysis blocked on another PR
30744 grunweg feat: more extensions for differential geometry elaborators t-meta t-differential-geometry failing CI
26966 vihdzp feat: the Dedekind–MacNeille completion blocked-by-other-PR awaiting-author merge-conflict t-order blocked on another PR
30750 SnirBroshi feat(Data/Quot): `toSet` and `equivClassOf` awaiting-author awaiting-zulip t-data awaiting a zulip discussion
26588 faenuccio feat(Algebra/GroupWithZero/WithZero): add the multiplicative embedding with zero from the range t-algebra t-order failing CI
26436 AntoineChambert-Loir feat(Mathlib/Data/Nat/Prime/Defs): fuel Nat.minFac awaiting-author merge-conflict t-data failing CI
24514 b-mehta chore(Int/GCD): use fuel in xgcd awaiting-author merge-conflict t-data merge conflict
32169 saodimao20 feat: add convolution_comp_add_right awaiting-author t-analysis new-contributor awaiting author
31132 kckennylau feat(Algebra): saturation of a submonoid t-algebra failing CI
28244 robin-carlier feat(CategoryTheory/Bicategory/NaturalTransformation): Icons WIP blocked-by-other-PR merge-conflict awaiting-CI t-category-theory large-import blocked on another PR
31135 kckennylau feat(RingTheory): is localization iff is localization on saturation blocked-by-other-PR merge-conflict ⚠️ blocked on another PR
29934 smmercuri feat(Field/WithAbs): the lift of a ring homomorphism from `WithAbs v` to `WithAbs w` to their completions WIP merge-conflict FLT ⚠️ labelled WIP
29933 smmercuri chore: fix `def` naming isses in `Normed/Field/WithAbs.lean` WIP merge-conflict labelled WIP
31836 hanwenzhu chore(MeasureTheory/IntervalIntegral): generalize fundamental theorem of calculus to `HasDerivWithinAt` instead of `HasDerivAt` awaiting-author t-analysis t-measure-probability awaiting author
27980 smmercuri feat: dimensions of completions at infinite place extensions blocked-by-other-PR merge-conflict t-number-theory FLT large-import blocked on another PR
31350 grunweg feat: (unoriented) bordism groups WIP blocked-by-other-PR merge-conflict t-differential-geometry blocked on another PR
26389 jjdishere feat(RingTheory): Perfectoid Field WIP t-topology t-analysis t-algebra labelled WIP
26390 jjdishere feat(Topology/Algebra): Krasner's lemma WIP t-number-theory t-topology t-algebra labelled WIP
27493 themathqueen feat(RingTheory/Coalgebra): define Frobenius algebra blocked-by-other-PR awaiting-author t-ring-theory blocked on another PR
30504 grunweg feat: add custom elaborators for immersions merge-conflict t-differential-geometry failing CI
26961 mariainesdff feat(RingTheory/PowerSeries/Substitution): add API t-ring-theory awaiting review
32285 awainverse chore(ModelTheory/Bundled): Replace CategoryTheory.Bundled awaiting-author t-logic awaiting author
31663 xroblot feat(Algebra): more instances about `min`, `max`, `iSup` and `iInf` of sub-algebras WIP t-algebra labelled WIP
30989 kckennylau feat(RingTheory): Teichmuller map awaiting-author merge-conflict ⚠️ merge conflict
27100 staroperator feat(ModelTheory): Presburger definability and semilinear sets t-logic awaiting review
32124 SnirBroshi feat(SimpleGraph/Walks/Operations): expand basic drop/take/reverse API t-combinatorics awaiting review
31950 callesonne feat(CategoryTheory/Product/Basic): make `Hom` into a 1-field structure WIP merge-conflict t-category-theory labelled WIP
26464 joelriou feat(LinearAlgebra): generators of pi tensor products awaiting-author merge-conflict t-algebra file-removed failing CI
31110 bryangingechen ci: don't delete merged branches awaiting-author merge-conflict CI merge conflict
29393 staroperator feat(SetTheory/ZFC): `card (V_ o) = preBeth o` t-set-theory large-import awaiting review
30582 RemyDegenne feat: extension of a function to the closure of a submodule WIP t-topology labelled WIP
27579 RemyDegenne feat: risk of an estimator, DeGroot statistical information, total variation distance WIP t-measure-probability large-import labelled WIP
32269 EtienneC30 feat: introduce Gaussian processes blocked-by-other-PR t-measure-probability brownian blocked on another PR
29315 kbuzzard chore: raise priority of `IsTopologicalSemiring.toIsModuleTopology` awaiting-author t-topology failing CI
30551 smmercuri feat: dimension formulae for infinite places above WIP blocked-by-other-PR merge-conflict ⚠️ blocked on another PR
31603 alreadydone chore(Algebra): make `RatFunc` an abbrev awaiting-author merge-conflict RFC t-algebra merge conflict
31730 thorimur feat(Meta): declaration manipulation meta API: allow logging on type signature of theorems t-meta failing CI
31242 plp127 feat: express filter as supremum of principal filter and free filter awaiting-author merge-conflict t-order merge conflict
32159 zhuyizheng feat(Order): gaps of disjoint intervals t-order new-contributor failing CI
32474 mattrobball perf(Module.LinearMap.Defs): deprioritize projections to parents for SemilinearMapClass t-algebra failing CI
31898 ntapiam feat(LinearAlgebra/TensorAlgebra): implement HopfAlgebra for TensorAlgebra awaiting-author new-contributor t-ring-theory failing CI
31597 grunweg chore(AtLocation): allow throwing a warning when no progress is being made awaiting-author merge-conflict t-meta merge conflict
30439 plp127 feat: `norm_num` extension for `IsSquare` on `Nat`, `Int`, `Rat` awaiting-author merge-conflict t-meta merge conflict
30525 515801431 feat(Mathlib/Combinatorics/Enumerative/Polya): Add Polya Counting awaiting-author merge-conflict t-combinatorics new-contributor merge conflict
31113 515801431 feat(Mathlib/Combinatorics/Enumerative/Polya.lean): Add additional theorem in `Polya.lean` blocked-by-other-PR merge-conflict t-combinatorics new-contributor blocked on another PR
29000 JovanGerb feat(Tactic/Push): add basic tags and tests blocked-by-other-PR merge-conflict ⚠️ blocked on another PR
24441 MrSumato feat(Data/List): add Lyndon-Schutzenberger theorem on list commutativity awaiting-author merge-conflict new-contributor t-data merge conflict
32125 SnirBroshi feat(SimpleGraph/Walks/Subwalks): `p₁.IsSubwalk p₂ ↔ p₁.darts <:+: p₂.darts` and similar theorems blocked-by-other-PR t-combinatorics blocked on another PR
28468 alreadydone feat(Algebra): ring API for `AddLocalization` awaiting-author t-algebra large-import awaiting author
28057 plp127 feat(SuccOrder): simp lemma to refold `Order.succ` and `Order.pred` awaiting-author merge-conflict t-order merge conflict
31901 callesonne feat(Bicategory/Subbicategory): add full subbicategories using `ObjectProperty` awaiting-author t-category-theory awaiting author
32326 chrisflav feat(Algebra/ModuleCat): extension of scalars is comonadic for a faithfully flat algebra awaiting-author t-ring-theory awaiting author
32473 mattrobball chore(Kaehler.JacobiZariski): remove egregious local instance hack awaiting-author t-ring-theory awaiting author
18551 joelriou feat(AlgebraicGeometry): the algebraic De Rham complex WIP blocked-by-other-PR merge-conflict t-algebraic-geometry t-algebra blocked on another PR
24434 joelriou feat(CategoryTheory): effectiveness of descent WIP merge-conflict t-category-theory labelled WIP
32367 BoltonBailey feat(Computability): add finEncodings for List Bool and pairs of types t-computability awaiting review
31610 rudynicolop feat(Computability/NFA): Kleene star closure for Regular Languages via NFA new-contributor t-computability awaiting review
32374 adamtopaz feat(Tactic/WildcardUniverse): Foo.{*, _, v*, max u v} t-meta awaiting review
32273 jsm28 feat(Analysis/Convex/Side): affine combinations on same / opposite side of face of a simplex as a vertex t-analysis t-convex-geometry awaiting review
29744 espottesmith feat(Combinatorics): define directed hypergraphs t-combinatorics new-contributor failing CI
31147 daefigueroa feat(Dynamics): point transitive monoid actions and transitive points awaiting-author t-dynamics new-contributor awaiting author
29354 themathqueen refactor(Algebra/Algebra/Equiv): allow for non-unital `AlgEquiv` awaiting-author merge-conflict t-algebra merge conflict
32455 vihdzp feat: order topologies of successor orders t-topology t-order awaiting review
27918 kim-em wip: refactor WithBot/WithTop as structures merge-conflict file-removed failing CI
30119 Ruben-VandeVelde feat: WithTop/Bot.mapD awaiting-author merge-conflict t-order merge conflict
32458 vihdzp feat: order isomorphisms preserve successor/predecessor limits awaiting-author t-order awaiting author
28613 espottesmith feat(Combinatorics): define undirected hypergraphs merge-conflict t-combinatorics new-contributor failing CI
32676 Scarlett-le doc(Sphere.Power): add theorem to 1000.yaml and author credit t-euclidean-geometry new-contributor failing CI
24000 YaelDillies feat: correspondence between affine group schemes and Hopf algebras WIP t-algebraic-geometry FLT toric labelled WIP
23040 grunweg feat: define immersions and smooth embeddings in infinite dimensions WIP blocked-by-other-PR merge-conflict t-differential-geometry blocked on another PR
26231 chrisflav feat(CategoryTheory/Sites): sheaf condition and coproducts WIP awaiting-author t-category-theory labelled WIP
10991 thorimur feat: `tfae` block tactic WIP modifies-tactic-syntax merge-conflict t-meta labelled WIP
30668 astrainfinita feat: `QuotType` RFC awaiting-zulip t-data awaiting a zulip discussion
32278 jsm28 feat(Geometry/Euclidean/Incenter): excenters on sides of faces blocked-by-other-PR t-euclidean-geometry blocked on another PR
32556 vihdzp doc: fix URL in docs documentation awaiting-author awaiting author
27702 FLDutchmann feat(NumberTheory/SelbergSieve): define Lambda-squared sieves and prove important properties delegated t-number-theory delegated
30847 joelriou feat(CategoryTheory/Presentable): the representation theorem WIP blocked-by-other-PR merge-conflict t-category-theory blocked on another PR
30620 plp127 feat: copy LE and LT on preorder and partial order awaiting-author merge-conflict t-order merge conflict
30853 JovanGerb feat(LinearAlgebra/AffineSpace/Simplex): `CoeFun` instance for `Simplex` awaiting-author merge-conflict t-euclidean-geometry merge conflict
30817 joelriou feat(CategoryTheory): `κ`-continuous presheaves WIP blocked-by-other-PR t-category-theory blocked on another PR
30185 alreadydone feat(MathlibTest): kernel reduction of nsmul on elliptic curve over ZMod blocked-by-other-PR merge-conflict t-number-theory t-algebraic-geometry t-algebra blocked on another PR
6633 adomani feat(..Polynomial..): `MvPolynomial`s have no zero divisors awaiting-author merge-conflict t-algebra merge conflict
31508 FLDutchmann feat(Tactic): `algebra` tactic. awaiting-author t-meta awaiting author
31059 gasparattila feat(Topology/Sets): define the Vietoris topology on `(Nonempty)Compacts` t-topology awaiting review
28865 grunweg feat: a map is smooth iff its post-composition with an immersion is WIP blocked-by-other-PR merge-conflict t-differential-geometry blocked on another PR
32609 PrParadoxy feat(LinearAlgebra/PiTensorProduct): Relation between nested tensor products and tensor products indexed by dependent sums blocked-by-other-PR new-contributor ⚠️ blocked on another PR
29508 zhuyizheng feat(MeasureTheory): FTC and integration by parts for absolutely continuous functions awaiting-author merge-conflict t-measure-probability new-contributor merge conflict
30666 erdOne feat(NumberTheory): every number field has a ramified prime awaiting-author merge-conflict t-number-theory t-algebra failing CI
30811 yonggyuchoimath feat(AlgebraicGeometry.EffectiveEpi): effective epimorphisms in schemes blocked-by-other-PR merge-conflict ⚠️ blocked on another PR
32777 madvorak doc: Contributing moved to Contributing failing CI
30329 luigi-massacci feat(Analysis/Distribution/TestFunction): integrating against a measure as a continuous linear map on test functions blocked-by-other-PR merge-conflict ⚠️ blocked on another PR*
30327 luigi-massacci feat(Analysis/Distribution/TestFunction): add characterizations of continuity for linear maps on test functions blocked-by-other-PR merge-conflict ⚠️ blocked on another PR
30255 luigi-massacci feat(Analysis/Distribution/ContDiffMapSupportedIn): specialize singleton seminorm family for D_K^n when n finite blocked-by-other-PR merge-conflict ⚠️ blocked on another PR
30253 luigi-massacci feat(Analysis/Distribution/ContDiffMapSupportedIn): Add a wrapper for iteratedFDeriv on the type of bundled smooth compactly supported maps blocked-by-other-PR merge-conflict ⚠️ blocked on another PR
30112 gaetanserre feat(Probability.Kernel): add representation of kernel as a map of a uniform measure t-measure-probability awaiting review
32692 WilliamCoram feat: define multivariate restricted power series awaiting-author t-number-theory new-contributor t-ring-theory awaiting author
27664 pechersky feat(Topology,Analysis): discrete topology metric space and normed groups awaiting-author t-topology failing CI
32552 ksenono feat(SetTheory/Cardinal): helpers for Konig's theorem new-contributor t-set-theory awaiting review
32334 EtienneC30 feat: independence of Gaussian processes blocked-by-other-PR merge-conflict t-measure-probability brownian blocked on another PR
32704 euprunin chore: remove use of `erw` awaiting-author t-category-theory t-topology t-measure-probability awaiting author
31987 saodimao20 feat: add monotonicity and relation lemmas for mgf and cgf awaiting-author t-measure-probability new-contributor awaiting author
32600 PrParadoxy feat(LinearAlgebra/Multilinear): composition of multilinear maps new-contributor ⚠️ awaiting review
29764 ScottCarnahan feat(Algebra/Vertex): API up to residue products (WIP) blocked-by-other-PR t-algebra large-import blocked on another PR
32147 EtienneC30 feat: independence of Gaussian random variables blocked-by-other-PR merge-conflict t-measure-probability brownian blocked on another PR
31766 SuccessMoses feat(Topology/EMetricSpace): continuity of arc length awaiting-author t-topology new-contributor awaiting author
30505 mariainesdff feat(NumberTheory/RatFunc/Ostrowski): prove Ostrowski's theorem for K(X) awaiting-author merge-conflict t-number-theory t-algebra failing CI
31965 bwangpj feat: fiber of RingHom.specComap awaiting-author merge-conflict t-ring-theory merge conflict
32829 Hagb feat(Data/Finsupp/MonomialOrder): weaken `IsOrderedCancelAddMonoid` to `IsOrderedAddMonoid` blocked-by-other-PR ⚠️ blocked on another PR
32211 ADedecker feat: inclusion from `ContDiffMapSupportedIn` to `TestFunction` is a topological embedding blocked-by-other-PR t-analysis blocked on another PR
32602 adamtopaz feat: Refactor graph WIP ⚠️ labelled WIP
26912 pechersky chore(Algebra/Ring/Subring): simp tag `Subring.smul_def` merge-conflict t-algebra merge conflict
32737 j-loreaux refactor: rename `MulAction` to `MonoidAction` merge-conflict failing CI
26608 vihdzp feat(SetTheory/Cardinal/Aleph): `o.card ≤ ℵ_ o` and variants t-set-theory awaiting review
24050 Paul-Lez feat(Data/Finsupp/Pointwise): generalise pointwise scalar multiplication of finsupps awaiting-author t-data awaiting author
28291 vasnesterov feat(Tactic): tactic for computing asymptotics of real functions WIP t-meta t-analysis large-import labelled WIP
30240 luigi-massacci feat(Analysis/Distribution/ContDiffMapSupportedIn): Add a wrapper for fderiv on D_K^n blocked-by-other-PR t-analysis blocked on another PR
32828 Hagb feat(Algebra/Order/Group/Defs): add `IsOrderedAddMonoid.toIsOrderedCancelAddMonoid'` t-algebra awaiting review
30030 JonBannon feat(MeasureTheory): add `MemLp.Const` class and instances to unify `p = ∞` and `μ.IsFiniteMeasure` cases awaiting-author merge-conflict t-measure-probability failing CI
31364 YaelDillies feat: binomial random graphs t-combinatorics t-measure-probability awaiting review
29274 Jlh18 feat(CategoryTheory): HasLimits instance on Grpd blocked-by-other-PR merge-conflict t-category-theory file-removed blocked on another PR
29283 Jlh18 feat(CategoryTheory): define forgetful-core adjunction between Cat and Grpd awaiting-author merge-conflict t-category-theory file-removed merge conflict
28248 YaelDillies feat: binomial random variables t-measure-probability failing CI
30920 callesonne feat(Category/Grpd): define the bicategory of groupoids merge-conflict t-category-theory large-import failing CI
32772 tb65536 feat(Data/Set/Card): criterion for `s.ncard ≤ (f '' s).ncard + 1` t-data awaiting review
32555 ksenono feat(Combinatorics/SimpleGraph/Matching): maximum and maximal matchings for Konig's theorem t-combinatorics new-contributor awaiting review
32570 ksenono feat(Combinatorics/SimpleGraph): bipartite subgraphs and vertex-disjoint graphs for Konig's theorem t-combinatorics new-contributor awaiting review
33020 FormulaRabbit81 chore(Topology): Deprecate file merge-conflict t-topology large-import merge conflict
21447 erdOne feat(AlgebraicGeometry): the split algebraic torus awaiting-author merge-conflict t-algebraic-geometry merge conflict
28693 faenuccio feat(Analysis.Normed.Module.Milman-Pettis): add Milman-Pettis theorem WIP t-analysis labelled WIP
31500 zcyemi feat(Analysis/Convex/Between): add lemmas on affine independence under strict betweenness awaiting-author merge-conflict t-convex-geometry merge conflict
32807 WilliamCoram feat: Define the Gauss norm for MvPowerSeries merge-conflict new-contributor t-ring-theory failing CI
25963 artie2000 refactor(Algebra): uniform API for substructures WIP merge-conflict t-algebra labelled WIP
32039 HugLycan feat(Tactic/Positivity): handle non-zeroness in non-orders WIP t-meta new-contributor labelled WIP
32845 jonasvanderschaaf feat(CategoryTheory): `GrothendieckTopology.yoneda` preserves certain (co)limits WIP new-contributor ⚠️ labelled WIP
32882 DavidLedvinka feat(Probability): add `Adapted ` blocked-by-other-PR t-measure-probability blocked on another PR
31662 edwin1729 feat(Topology/Order): topological basis of scott topology on Complete… blocked-by-other-PR awaiting-author t-topology new-contributor blocked on another PR
32679 YaelDillies chore(Data/Sym2): improve defeq of `diagSet` t-data awaiting review
32355 bjornsolheim feat(Geometry/Convex/Cone): define and characterize simplicial pointed cones new-contributor t-convex-geometry awaiting review
28905 grunweg feat: immersions are locally embeddings blocked-by-other-PR ⚠️ blocked on another PR
32938 0xTerencePrime feat(Order/LocallyFinite): prove DenselyOrdered and LocallyFiniteOrder are incompatible awaiting-author t-order new-contributor awaiting author
33028 bjornsolheim feat(Geometry/Convex/Cone): minimal and maximal cone tensor products are commutative t-convex-geometry awaiting review
33077 YaelDillies feat(Data/Rel): balls WIP t-data labelled WIP
26291 RemyDegenne feat(Probability): Cameron-Martin theorem WIP blocked-by-other-PR merge-conflict t-measure-probability blocked on another PR*
31226 erdOne chore(RingTheory): add `@[ext]` to `Ideal.Quotient.algHom_ext` awaiting-author merge-conflict easy t-ring-theory merge conflict
31425 robertmaxton42 feat(Topology): implement delaborators for non-standard topology notation t-topology awaiting review
28246 Sebi-Kumar feat(AlgebraicTopology/FundamentalGroupoid): the n-sphere is simply connected for n > 1 blocked-by-other-PR merge-conflict new-contributor t-algebraic-topology blocked on another PR
21495 alreadydone experiment: reducible HasQuotient.quotient' WIP merge-conflict bench-after-CI labelled WIP
32532 SnirBroshi feat(Combinatorics/SimpleGraph/Connectivity): connected components are maximally connected subsets/subgraphs t-combinatorics awaiting review
30872 rudynicolop feat(Computability/NFA): NFA closure under concatenation new-contributor t-computability maintainer-merge awaiting review
32698 farruhx feat(List): add aesop / simp annotations to selected lemmas for improved automation awaiting-author new-contributor t-data awaiting author
32872 JovanGerb feat(Data/Real/Basic): don't expose the definition of `Real` t-data failing CI
32260 jsm28 feat(Geometry/Euclidean/Angle/Oriented/Affine): oriented angle bisection and halving unoriented angles t-euclidean-geometry awaiting review
32826 felixpernegger feat(Data/Tuple/Sort): Permutation is monotone iff its the identity new-contributor t-data awaiting review
32127 CoolRmal feat: use IndexedPartition.piecewise to create simple/measurable/strongly measurable functions t-measure-probability large-import brownian awaiting review
27817 zhuyizheng feat: add IMO2025P1 awaiting-author merge-conflict new-contributor IMO merge conflict
24383 YaelDillies feat: distributive Haar characters of `ℝ` and `ℂ` WIP awaiting-CI t-measure-probability FLT file-removed labelled WIP
32739 Rida-Hamadani chore(SimpleGraph): golf and improve style of `Subwalks.lean` t-combinatorics awaiting review
32910 felixpernegger feat(Data/Nat/Choose): two binomial coefficient sum identities new-contributor t-data awaiting review
32989 kim-em fix(Tactic/Simps): skip @[defeq] inference for non-exposed definitions t-meta awaiting review
33016 xgenereux feat: RingHom.adjoinAlgebraMap ⚠️ awaiting review
29151 yuanyi-350 feat: Corollary of Hahn–Banach theorem awaiting-author new-contributor large-import ⚠️ awaiting author
30898 vihdzp feat: characterization of `List.splitBy` t-data awaiting review
10654 smorel394 feat(LinearAlgebra/{ExteriorPower,LinearIndependent,TensorPower}): define the exterior powers of a module and prove some of their basic properties please-adopt merge-conflict t-algebra large-import looking for help
32983 JovanGerb feat: use `LE.le` for subset relation in `Set`, `Finset`, `PSet`, `ZFSet` merge-conflict ⚠️ failing CI
28796 grunweg feat: immersions are smooth t-differential-geometry awaiting review
31377 CoolRmal feat: a series of smooth functions that converges (locally) uniformly is smooth awaiting-author t-topology new-contributor failing CI
26923 oliver-butterley feat(Dynamics/BirkhoffSum): add the pointwise ergodic theorem (Birkhoff's) awaiting-author t-dynamics new-contributor failing CI
26484 peabrainiac feat(Geometry/Diffeology): basics of diffeological spaces t-differential-geometry awaiting review
26743 grunweg feat: product rule for Lie bracket on manifolds WIP t-differential-geometry labelled WIP
33110 dagurtomas feat(CategoryTheory): adjoint functor theorems for presentable categories WIP t-category-theory labelled WIP
32021 jsm28 feat(Geometry/Euclidean/Altitude): `map` and `restrict` lemmas t-euclidean-geometry awaiting review
33031 chiyunhsu feat(Combinatorics/Enumerative/Partition): add combinatorial proof of Euler's partition theorem t-combinatorics new-contributor awaiting review
33044 bryangingechen ci: also get cache for parent commit CI awaiting review
33063 DavidLedvinka chore(Probability): Rename Adapted to StronglyAdapted t-measure-probability awaiting review
33082 AntoineChambert-Loir feat(GroupTheory/SpecificGroups/Alternating/Simple): the alternating group on at least 5 letters is simple. large-import t-group-theory awaiting review
33109 felixpernegger feat(Data/Nat/Choose): Binomial inversion new-contributor ⚠️ awaiting review
33108 alreadydone feat(Topology): `π₁(E⧸G)⧸π₁(E) ≃* G` for `E` path connected WIP merge-conflict t-topology t-algebraic-topology labelled WIP
33218 Blackfeather007 feat(Algebra): Define the associated graded ring to filtered ring blocked-by-other-PR new-contributor t-ring-theory blocked on another PR
33219 Blackfeather007 feat(Algebra): Define associated graded algebra blocked-by-other-PR new-contributor t-ring-theory blocked on another PR
33220 Blackfeather007 feat(Algebra): Define associated graded module blocked-by-other-PR new-contributor t-ring-theory blocked on another PR
33227 Blackfeather007 feat(Algebra): exact of associated graded exact blocked-by-other-PR new-contributor t-ring-theory blocked on another PR
33226 unknown unknown title ??? missing CI information
33225 Blackfeather007 feat(Algebra): filtered module hom blocked-by-other-PR new-contributor t-ring-theory blocked on another PR
33224 Blackfeather007 feat(Algebra): define filtered alghom blocked-by-other-PR new-contributor t-ring-theory blocked on another PR
33223 unknown unknown title ??? missing CI information
33222 Blackfeather007 feat(Algebra): define filtered add group hom blocked-by-other-PR new-contributor t-ring-theory blocked on another PR
32888 staroperator feat(Tactic/FunProp): make `fun_prop` able to tag `→` and `∀` t-meta failing CI
30880 themathqueen feat(Analysis/InnerProductSpace): finite-dimensional inner product space with an algebra implies a coalgebra delegated t-analysis delegated
33134 faenuccio feat(Normed/Module/WeakDual): add Goldstine lemma WIP t-analysis labelled WIP
33178 gw90 feat(Analysis/CStarAlgebra/Spectrum): Adding lemmas that the CStarAlgebra norm equals the square root of the spectral radius of star a * a awaiting-author t-analysis new-contributor awaiting author
33126 CoolRmal feat: function composition preserves boundedness t-order awaiting review
33128 gasparattila feat(Topology/UniformSpace): generalize `TotallyBounded` to filters t-topology awaiting review
25834 Rida-Hamadani feat(SimpleGraph): girth-diameter inequality WIP blocked-by-other-PR merge-conflict t-combinatorics blocked on another PR
33253 SnirBroshi feat(Combinatorics/SimpleGraph/Clique): avoid `Fintype`/`Finite` assumptions where possible t-combinatorics awaiting review
28462 joelriou feat(AlgebraicTopology/SimplicialSet): the relative cell complex attached to a rank function for a pairing WIP blocked-by-other-PR merge-conflict t-algebraic-topology blocked on another PR
29996 vihdzp chore(Order/Concept): `IsIntent` and `IsExtent` blocked-by-other-PR t-order blocked on another PR
33249 Rida-Hamadani feat(SimpleGraph): `take` is path if original walk is path blocked-by-other-PR t-combinatorics blocked on another PR
33254 SnirBroshi feat(Data/Nat/Lattice): `¬BddAbove s → sSup s = 0` t-data awaiting review
32160 SnirBroshi feat(Combinatorics/SimpleGraph/Walks): helper theorems about `darts` and `support` t-combinatorics awaiting review
33147 SnirBroshi feat(Combinatorics/SimpleGraph/Coloring): add a few missing instances (`IsEmpty`/`Nontrivial`/`Infinite`) t-combinatorics awaiting review
31092 FlAmmmmING feat(Algebra/Group/ForwardDiff.lean): Add theorem `sum_shift_eq_fwdDiff_iter`. t-algebra new-contributor awaiting review
33121 SnirBroshi feat(Combinatorics/SimpleGraph/Hasse): paths in a graph are isomorphic to path graphs t-combinatorics large-import awaiting review
33138 gasparattila chore(MeasureTheory/Measure/Stieltjes): remove `backward.privateInPublic` awaiting-author t-measure-probability tech debt awaiting author
33211 Komyyy doc(Order/Filter/*): outdated documents documentation t-order awaiting review
33043 euprunin chore: golf using `grind` and `simp` awaiting-author awaiting author
33119 euprunin chore: golf using `grind` awaiting-author awaiting author
32627 dagurtomas feat(Condensed): the functor from light profinite sets preserves effective epimorphisms awaiting-author t-condensed awaiting author
33307 grunweg Orientable manifolds updated WIP t-differential-geometry labelled WIP
23177 faenuccio feat: more lemmas about ordered groups with zero WIP blocked-by-other-PR merge-conflict awaiting-CI t-order blocked on another PR
33313 SnirBroshi feat(Combinatorics/SimpleGraph/EdgeColoring): create a basic edge-coloring API blocked-by-other-PR t-combinatorics large-import blocked on another PR
5934 eric-wieser feat: port Data.Rat.MetaDefs help-wanted mathlib-port merge-conflict t-meta looking for help
4960 eric-wieser chore: use `open scoped` merge-conflict awaiting-CI does not pass CI
6042 MohanadAhmed feat(LinearAlgebra/Matrix/SVD): Singular Value Decomposition of R or C Matrices WIP please-adopt merge-conflict t-algebra looking for help
32270 jsm28 feat(Geometry/Euclidean/Incenter): `map` and `restrict` lemmas blocked-by-other-PR t-euclidean-geometry blocked on another PR
26303 joelriou feat(AlgebraicTopology): the fundamental lemma of homotopical algebra WIP blocked-by-other-PR merge-conflict t-category-theory t-algebraic-topology blocked on another PR
4127 kmill refactor: create HasAdj class, define Digraph, and generalize some SimpleGraph API awaiting-author merge-conflict t-combinatorics merge conflict
33087 joelriou feat(AlgebraicTopology): the cofibrant resolution functor (up to homotopy) WIP blocked-by-other-PR merge-conflict t-algebraic-topology blocked on another PR
33088 joelriou feat(AlgebraicTopology/ModelCategory): the left derivability structure WIP blocked-by-other-PR merge-conflict t-category-theory t-algebraic-topology blocked on another PR
27752 plp127 feat(Order): `NoBotOrder α` implies `NoMinOrder α` under `IsDirected α (· ≥ ·)` awaiting-author merge-conflict t-order failing CI
32971 Paul-Lez feat(Data/Finsupp/Pointwise): generalise pointwise scalar multiplication of finsupps t-data awaiting review
33248 vihdzp refactor(MeasureTheory/Measure/Stieltjes): simpler definition of `botSet` t-measure-probability awaiting review
32546 anishrajeev feat(ModelTheory): Prove compactness of the type space blocked-by-other-PR t-logic new-contributor blocked on another PR
33292 SnirBroshi feat(Combinatorics/SimpleGraph/LineGraph): lift copies/isomorphisms to line-graph t-combinatorics large-import awaiting review
29776 yuanyi-350 chore: refactor `ContinuousLinearMap.isOpenMap` by separating it into sublemmas WIP t-analysis labelled WIP
32921 faenuccio refactor Submodule.map WIP awaiting-author merge-conflict t-algebra labelled WIP
33189 peabrainiac feat(Geometry/Manifold): the interior of a manifold is open awaiting-author t-differential-geometry awaiting author
32889 artie2000 feat(Algebra): forgetful lemmas for `map` and `comap` on substructures blocked-by-other-PR awaiting-author merge-conflict t-algebra blocked on another PR
32960 dleijnse feat(FieldTheory): adjoin pth roots awaiting-author t-algebra new-contributor awaiting author
33163 Aaron1011 feat: prove subgroup of (M -> Z) is finitely generated awaiting-author new-contributor t-ring-theory awaiting author
33217 Blackfeather007 feat(Algebra): define associated graded structure for abelian group awaiting-author new-contributor t-ring-theory awaiting author
32987 kim-em feat: pipeline downloads and decompression in `cache get` ⚠️ awaiting review
24965 erdOne refactor: Make `IsLocalHom` take unbundled map delegated t-algebra failing CI
25481 kbuzzard chore: refactor Algebra.TensorProduct.rightAlgebra t-algebra failing CI
33206 lua-vr feat(Integral.Bochner.Set): add `tendsto_setIntegral_of_monotone₀` t-measure-probability awaiting review
28972 themathqueen feat(LinearAlgebra/Matrix): star-algebra automorphisms on matrices are unitarily inner awaiting-author t-analysis t-algebra awaiting author
33270 vihdzp chore(Order/Disjoint): use `to_dual` awaiting-author t-order failing CI
33363 BoltonBailey feat: add `empty_eq_image` simp lemmas t-data awaiting review
29790 robertmaxton42 feat(IsCoherentWith) : families of maps from a coherent collection of subspaces lift uniquely to maps from the total space blocked-by-other-PR large-import ⚠️ blocked on another PR
29788 robertmaxton42 feat(Topology): adds bundled continuous maps for sum, sigma, subtype, mapsto, inclusion large-import ⚠️ awaiting review
33280 michelsol feat(MeasureTheory/Integral/IntervalIntegral): add variant `integral_deriv_eq_sub_uIoo` of 2nd theorem of calculus. t-measure-probability new-contributor awaiting review
14444 digama0 fix(GeneralizeProofs): unreachable! bug awaiting-author merge-conflict t-meta merge conflict
30391 rudynicolop feat(Data/List): list splitting definitions and lemmas new-contributor t-data awaiting review
25138 chrisflav chore(RingTheory/Ideal): make `RingHom.ker` take a `RingHom` instead of `RingHomClass` awaiting-author merge-conflict t-algebra failing CI
30962 WangYiran01 feat(Combinatorics/Enumerative): add lattice path lemmas and counts t-combinatorics new-contributor awaiting review
31018 joelriou feat(CategoryTheory): the κ-accessible category of κ-directed posets WIP t-category-theory labelled WIP
33386 joelriou feat(AlgebraicTopology/SimplicialSet): decidable instances WIP RFC t-algebraic-topology labelled WIP
27053 tb65536 feat: Galois group of `x^n - x - 1` WIP t-algebra large-import labelled WIP
32688 grunweg chore: update complex analysis library overview t-analysis failing CI
33064 DavidLedvinka feat(Probability): Add `condLExp`, conditional expectation with the Lebesgue integral t-measure-probability awaiting review
33143 wwylele feat(PowerSeries): pentagonal number theorem ⚠️ awaiting review
33297 tb65536 feat(Algebra/Polynomial/Roots): add `card_rootSet_le` t-algebra large-import awaiting review
33335 YaelDillies feat(Combinatorics/SimpleGraph): more about two-reachability t-combinatorics awaiting review
33021 farmanb feat(RingTheory/IdealFilter): add ideal filters and Gabriel filters blocked-by-other-PR new-contributor t-ring-theory blocked on another PR
24665 Komyyy feat(Mathlib/Topology/Metrizable/Uniformity): every uniform space is generated by a family of pseudometrics WIP merge-conflict t-topology labelled WIP
33084 joelriou feat(CategoryTheory): MorphismProperty induced on a quotient category t-category-theory maintainer-merge awaiting review
33406 dupuisf feat: add basics of majorization blocked-by-other-PR ⚠️ blocked on another PR
33381 urkud feat: add a version of the Schwarz lemma blocked-by-other-PR merge-conflict t-analysis blocked on another PR
33437 joelriou feat(Algebra/Homology): short exact sequences with four terms WIP t-category-theory t-algebra labelled WIP
33080 sinhp feat(Category Theory): Cartesian Natural Transformation awaiting-author t-category-theory awaiting author
33394 dupuisf feat: add lemmas about doubly stochastic matrices awaiting-author t-analysis awaiting author
33448 astrainfinita refactor: deprecate `ContinuousLinearMapClass` awaiting-author t-topology t-algebra awaiting author
33461 loefflerd feat(NumberTheory/Modular): stabilizers for action on upper halfplane WIP ⚠️ labelled WIP
21031 YaelDillies chore: get rid of generic hom coercions WIP labelled WIP
33465 SnirBroshi chore(Data/Finset/Insert): golf `eq_singleton_iff_nonempty_unique_mem` using grind t-data awaiting review
33462 eric-wieser feat: teach `fun_prop` about `ContinousMultilinearMap.compContinuousLinearMap` t-analysis failing CI
32803 erdOne feat(RIngTheory): more-linear version of `tensorKaehlerEquiv` t-ring-theory awaiting review
32725 joelriou feat(CategoryTheory): presheaves of types which preserve a limit awaiting-author t-category-theory awaiting author
32840 joelriou chore(CategoryTheory): remove the old Ext API WIP merge-conflict t-category-theory large-import file-removed labelled WIP
33133 0xTerencePrime feat(Algebra/Group/Center): add Decidable (IsMulCentral a) instance awaiting-author t-algebra new-contributor awaiting author
33276 NicolaBernini feat: Rename List.reverse_perm to List.reverse_perm_self and List.reverse_perm' to List.reverse_perm_iff awaiting-author new-contributor ⚠️ awaiting author
33351 themathqueen chore(Analysis/LocallyConvex/SeparatingDual): generalize `Algebra.IsCentral.instContinuousLinearMap` awaiting-author t-analysis awaiting author
33291 BoltonBailey refactor(Computability): File for state transition systems t-computability awaiting review
33191 sinhp feat(CategoryTheory): Locally cartesian closed structure on presheaf categories WIP blocked-by-other-PR merge-conflict t-category-theory blocked on another PR
33495 vihdzp chore(RingTheory/HahnSeries/Basic): redefine `order` using `unbotD` blocked-by-other-PR t-ring-theory blocked on another PR
28153 kckennylau feat(Simproc): Simproc for explicit diagonal matrices awaiting-author merge-conflict t-meta merge conflict
25500 eric-wieser feat: delaborators for metadata awaiting-author delegated merge-conflict t-meta large-import merge conflict
28191 kckennylau feat(Logic): tag Injective, Surjective, and Bijective with fun_prop awaiting-author merge-conflict t-meta merge conflict
30432 kckennylau feat(AlgebraicGeometry): define the non-vanishing locus of a set in Proj awaiting-author t-algebraic-geometry awaiting author
31611 thorimur feat(Meta): `withPlural` wrapper for more readable messages in source awaiting-author t-meta awaiting author
27262 Timeroot feat(Tactic/Bound): bound? for proof scripts awaiting-author t-meta failing CI
30758 Timeroot chore: tag abs_inv and abs_div with grind= t-algebra awaiting review
33105 Timeroot feat(BoundedOrder): add `finiteness` rule for ite and dite awaiting-author t-meta t-order awaiting author
33481 NoneMore feat(ModelTheory/Encoding): add `Countable` instances for (bounded) formulas in countable languages t-logic new-contributor awaiting review
31121 jessealama feat: add ComplexShape.EulerCharSigns for generalized Euler characteristic t-category-theory t-algebra awaiting review
33256 joelriou feat(CategoryTheory/Sites): characterization of (pre)stacks for a precoverage WIP blocked-by-other-PR t-category-theory blocked on another PR
32389 LLaurance feat(Analysis): Trigonometric identities awaiting-author t-analysis awaiting author
32654 YaelDillies feat(Combinatorics): a clique has size at most the chromatic number t-combinatorics awaiting review
33520 NoneMore feat(ModelTheory/ElementarySubstructures): add a variant of Tarski-Vaught test taking sets as input t-logic new-contributor awaiting review
33463 khwilson feat(Mathlib/Analysis/Polynomial/MahlerMeasure): Mahler Measure for other rings new-contributor ⚠️ failing CI
33514 urkud feat(Analysis/../Connected): balls are preconnected awaiting-author t-analysis awaiting author
33523 jsm28 feat(Combinatorics/Tiling/Tile): tiles and protosets for tilings t-combinatorics awaiting review
32608 PrParadoxy feat(LinearAlgebra/PiTensorProduct): API for PiTensorProducts indexed by sets new-contributor awaiting-zulip ⚠️ awaiting a zulip discussion
33502 MrQubo fix(Tactic/ProxyType): Pass params explicitly in proxy_equiv% implementation WIP t-meta new-contributor labelled WIP
22657 Xmask19 feat: a graph is maximally acyclic iff it is a tree merge-conflict t-combinatorics new-contributor failing CI
33397 themathqueen feat(Topology/Algebra/Star/LinearMap): intrinsic star for continuous linear maps t-topology t-algebra awaiting review
33416 vihdzp chore(Order/GameAdd): add `elab_as_elim` attributes t-order awaiting review
33443 sahanwijetunga feat: Define Isometries of Bilinear Spaces t-algebra new-contributor awaiting review
33118 thomaskwaring feat(Combinatorics/SimpleGraph/Acyclic): every graph has a spanning forest. t-combinatorics new-contributor awaiting review
33475 BoltonBailey feat(Logic/IsEmpty): add theorems relating surjectivity and emptiness t-logic awaiting review
33545 JovanGerb feat: rename `HasCompl` to `Compl` ⚠️ failing CI
33247 sun123zxy feat(Mathlib/RingTheory/Ideal/Cotangent): dimension of cotangent spaces WIP blocked-by-other-PR merge-conflict new-contributor file-removed t-ring-theory blocked on another PR
31444 harahu doc(Probability/Martingale/BorelCantelli): fix LaTeX typo delegated t-measure-probability delegated
26368 Whysoserioushah feat(RingTheory/TwoSidedIdeal/SpanAsSum): span of set as finsum awaiting-author merge-conflict t-ring-theory merge conflict
30927 callesonne feat(Bicategory/Yoneda): add the yoneda pseudofunctor ⚠️ failing CI
33479 zcyemi feat(Geometry/Euclidean/Angle/Sphere): Add theorem about cospherical points on two intersecting lines awaiting-author t-euclidean-geometry awaiting author
33375 kex-y feat(Probability): Local and stable properties blocked-by-other-PR t-measure-probability brownian blocked on another PR
31719 maksym-radziwill feat: Borel-Caratheodory (2nd revision) awaiting-author t-analysis failing CI
28013 astrainfinita feat: Lindemann-Weierstrass Theorem awaiting-author merge-conflict t-analysis t-algebra failing CI
33435 astrainfinita feat: algebra automorphisms of monoid algebras t-algebra awaiting review
32886 alreadydone refactor(Algebra/Order): change `MulArchimedeanClass.subgroup` to `FiniteArchimedeanClass.subgroup` t-algebra t-order awaiting review
31361 alreadydone feat(Algebra/Order): convex subgroups blocked-by-other-PR merge-conflict t-algebra t-order blocked on another PR
21344 kbuzzard chore: attempt to avoid diamond in OreLocalization please-adopt t-algebra looking for help
33112 alreadydone feat(GroupAction): `(M →[M] M) ≃* Mᵐᵒᵖ` awaiting-author t-algebra t-group-theory awaiting author
30982 jsm28 feat(Geometry/Euclidean/Angle/Incenter): angle bisection and the incenter blocked-by-other-PR t-euclidean-geometry blocked on another PR
32282 jsm28 feat(Geometry/Euclidean/Angle/Incenter): unoriented angle bisection blocked-by-other-PR t-euclidean-geometry blocked on another PR
32294 jsm28 feat(Geometry/Euclidean/Angle/Incenter): distance from second intersection with circumcircle blocked-by-other-PR t-euclidean-geometry blocked on another PR
30981 jsm28 feat(Geometry/Euclidean/Angle/Bisector): oriented angle bisection mod π t-euclidean-geometry awaiting review
33467 euprunin chore: golf using `grind`. add `grind` annotations. awaiting review
33469 erdOne feat(LinearAlgebra): make TensorProduct.finsuppLeft and friends heterobasic ⚠️ awaiting review
33470 erdOne feat: generalize `Polynomial.freeMonic` ⚠️ awaiting review
33364 BoltonBailey feat(Analysis/Convex/SimplicialComplex): add AbstractSimplicialComplex + constructions WIP awaiting-author t-analysis t-algebraic-topology labelled WIP
33423 urkud feat: add an explicit trivialization for `Complex.exp` blocked-by-other-PR t-analysis blocked on another PR
29235 yoh-tanimoto feat(Topology/Algebra/Module/ClosedSubmodule): add `mapEquiv`, a variation of `ClosedSubmodule.map` for CLE t-topology awaiting review
33039 euprunin chore(Data/List): deprecate `ext_get_iff` t-data awaiting review
33595 JovanGerb chore: remove some `backward.proofsInPublic` failing CI
31187 loefflerd feat(NumberTheory/LSeries): Define the L-series of a modular form WIP t-number-theory labelled WIP
32978 archiebrowne feat(NumberTheory/ModularForms/Basic): Provide definition of the products of finitely many modular forms awaiting-author t-number-theory new-contributor awaiting author
33601 nielstron feat(Computability/ContextFreeGrammar): Concatenation of CFGs is CFG blocked-by-other-PR new-contributor t-computability blocked on another PR
29624 mcdoll feat(LinearAlgebra/LinearPMap): add definition of resolvent and first resolvent identity awaiting-author t-analysis t-algebra failing CI
33599 nielstron feat(Computability/ContextFreeGrammar): closure under union new-contributor t-computability awaiting review
30375 sinhp feat(CategoryTheory): Basics of Locally Cartesian Closed Categories WIP blocked-by-other-PR t-category-theory blocked on another PR
32991 artie2000 chore(Algebra/Algebra): remove `Algebra.cast` coercion merge-conflict t-algebra failing CI
27972 smmercuri refactor: make `Valuation.Completion` a `def` and refactor more of `AdicValuation.lean` WIP merge-conflict t-number-theory t-algebra labelled WIP
33490 YaelDillies refactor(Data/Finsupp): remove `DecidableEq` argument from `curry` t-data CFT awaiting review
17176 arulandu feat: integrals and integrability with .re awaiting-author please-adopt merge-conflict t-measure-probability new-contributor looking for help
32918 michelsol feat: define `supEdist` and `supDist` merge-conflict t-topology new-contributor merge conflict
33100 themathqueen refactor(Algebra/Order/Field/Basic): generalize file from `LinearOrder` to `PartialOrder` and `PosMulReflectLT` t-algebra awaiting review
33608 riccardobrasca feat: generalize universes in representation theory (#33598) WIP t-algebra labelled WIP
29243 yoh-tanimoto feat(Analysis/InnerProductSpace/Projection/Submodule): add `sup_orthogonal` for `ClosedSubmodules` blocked-by-other-PR ⚠️ blocked on another PR
33619 vihdzp refactor: flip `Ixx_def` theorems awaiting-CI t-order does not pass CI
28499 yoh-tanimoto feat(MeasureTheory/VectorMeasure): add integral of a vector-valued function against a vector measure blocked-by-other-PR t-measure-probability blocked on another PR
33010 xgenereux feat: localizations of primes in Dedekind domains are valuation subrings WIP blocked-by-other-PR awaiting-author large-import t-ring-theory blocked on another PR
33557 ocfnash feat: existence of bases for root pairings WIP t-algebra labelled WIP
33281 michelsol feat(Analysis/SpecialFunctions/Integrals): integral of 1/sqrt(1-x^2) and its integrability. blocked-by-other-PR merge-conflict new-contributor ⚠️ blocked on another PR
30144 alreadydone feat(Data/Nat): kernel reducible binaryRec t-algebra t-data awaiting review
33458 NoneMore feat(ModelTheory): add lifting for embeddings to languages with constants t-logic new-contributor awaiting review
33487 gasparattila feat(Topology/UniformSpace): `SetRel.{inv,image,preimage}` of `entourageProd` t-topology awaiting review
33494 vihdzp feat(RingTheory/HahnSeries/Basic): more theorems on `order`/`orderTop` t-ring-theory awaiting review
33644 vihdzp feat(Analysis/Real/Hyperreal): more lemmas on `Tendsto` blocked-by-other-PR t-analysis large-import blocked on another PR
31219 Thmoas-Guan feat(Algebra): lemma about `IsBaseChange` under exact sequence awaiting-author t-ring-theory awaiting author
31222 Thmoas-Guan feat(Algebra): `Hom` commute with flat base change blocked-by-other-PR large-import ⚠️ blocked on another PR
26214 Thmoas-Guan feat(Algebra): definition of depth blocked-by-other-PR t-algebra large-import blocked on another PR
26216 Thmoas-Guan feat(Algebra): depth of QuotSMulTop blocked-by-other-PR t-algebra large-import blocked on another PR
32000 Thmoas-Guan feat(Algebra): projective dimension equal supremum of localized module ⚠️ failing CI
31046 Thmoas-Guan feat(Homology) : compatibility of map between `Ext` t-category-theory awaiting review
31697 Thmoas-Guan feat(Homology): bijection between `Ext` blocked-by-other-PR merge-conflict t-category-theory t-algebra blocked on another PR
31768 Thmoas-Guan feat(Homology): `Ext` commute with ulift functor blocked-by-other-PR t-category-theory t-algebra blocked on another PR
33061 edwin1729 refactor: generalise compact from CompleteLattice to PartialOrder awaiting-author new-contributor awaiting author
31891 jsm28 feat(Geometry/Euclidean/Sphere/OrthRadius): lemmas for setting up and using polars t-euclidean-geometry awaiting review
32081 Thmoas-Guan feat(RingTheory/Homology): `Ext` over Noetherian ring finitely generated blocked-by-other-PR t-category-theory t-algebra blocked on another PR
31879 Thmoas-Guan feat(Algebra/Homology): Projective dimension in linear equiv blocked-by-other-PR t-algebra blocked on another PR
32058 Thmoas-Guan feat(Algebra): category version Baer criterion blocked-by-other-PR awaiting-author t-category-theory t-algebra blocked on another PR
26215 Thmoas-Guan feat(Algebra): Auslander–Buchsbaum theorem blocked-by-other-PR t-algebra large-import blocked on another PR
26217 Thmoas-Guan feat(Algebra): Ischebeck theorem blocked-by-other-PR t-algebra large-import blocked on another PR
26212 Thmoas-Guan feat(Algebra): the Rees theorem for depth awaiting-author large-import t-ring-theory failing CI
26218 Thmoas-Guan feat(Algebra): definition of cohen macaulay blocked-by-other-PR t-algebra large-import blocked on another PR
32316 Thmoas-Guan feat(Homology/ModuleCat): Dimension Shifting tools in ModuleCat t-category-theory t-algebra awaiting review
28599 Thmoas-Guan feat(RingTheory): polynomial over CM ring is CM WIP large-import t-ring-theory labelled WIP
26245 Thmoas-Guan feat(Algebra): cohen macaulay local ring is catenary WIP blocked-by-other-PR t-algebra large-import blocked on another PR
26957 Thmoas-Guan feat(Algebra): unmixed thm of Cohen-Macaulay ring blocked-by-other-PR t-algebra large-import blocked on another PR
31851 Thmoas-Guan feat(Algebra/Homology): Injective dimension in linear equiv blocked-by-other-PR t-algebra blocked on another PR
31644 Thmoas-Guan feat(Algebra): projective dimension of quotient regular sequence blocked-by-other-PR awaiting-author t-ring-theory blocked on another PR
32098 Thmoas-Guan feat(RingTheory): injective dimension of quotSMulTop blocked-by-other-PR ⚠️ blocked on another PR
31884 Thmoas-Guan feat(RingTheory): definition of Gorenstein local ring blocked-by-other-PR ⚠️ blocked on another PR
31995 Thmoas-Guan feat(RingTheory): Module being injective is local property awaiting-author t-ring-theory awaiting author
32033 Thmoas-Guan feat(Algebra): injective dimension equal supremum of localized module blocked-by-other-PR ⚠️ blocked on another PR
32035 Thmoas-Guan feat(RingTheory): localization of Gorenstein local ring blocked-by-other-PR ⚠️ blocked on another PR
32959 CBirkbeck feat(NumberTheory/ModularForms/QExpansion): define qExpansion ring hom and some more API t-number-theory awaiting review
33369 Thmoas-Guan feat(Homology): `Ext` commute with flat base change blocked-by-other-PR large-import ⚠️ blocked on another PR
33377 Thmoas-Guan feat(RingTheory): polynomial over Gorenstein ring is Gorenstein blocked-by-other-PR large-import ⚠️ blocked on another PR
33379 Thmoas-Guan feat(RingTheory): Gorenstein local ring is Cohen Macaulay blocked-by-other-PR large-import ⚠️ blocked on another PR
33380 Thmoas-Guan feat(RingTheory): Gorenstein local ring is Cohen--Macaulay local ring of type one blocked-by-other-PR large-import ⚠️ blocked on another PR
28684 Thmoas-Guan feat(RingTheory): definition of regular ring blocked-by-other-PR t-ring-theory blocked on another PR
28683 Thmoas-Guan feat(RingTheory): regular local ring is domain WIP blocked-by-other-PR t-ring-theory blocked on another PR
33303 sinhp feat(CategoryTheory): The monads and comonads of locally cartesian closed categories WIP t-category-theory labelled WIP
33431 gululu996-ui feat(Combinatorics/SimpleGraph/Bipartite): characterize bipartite simplegraphs by even cycles t-combinatorics new-contributor awaiting review
28582 Thmoas-Guan feat(Data): some lemmas about WithBot ENat awaiting-author t-data awaiting author
33257 NickAdfor feat(Combinatorics/SimpleGraph/Bipartite): Odd Cycle Theorem (A Solution to TODO) awaiting-author t-combinatorics new-contributor awaiting author
29533 Thmoas-Guan feat(Algebra): maximal Cohen Macaulay module blocked-by-other-PR merge-conflict large-import ⚠️ blocked on another PR*
29557 Thmoas-Guan feat(Algebra): finite projective dimension of regular blocked-by-other-PR large-import ⚠️ blocked on another PR
29701 Thmoas-Guan feat(Algebra/RingTheory): polynomial over regular ring blocked-by-other-PR t-ring-theory blocked on another PR
33032 ksenono feat(Combinatorics/SimpleGraph): Konig’s theorem on bipartite graphs blocked-by-other-PR merge-conflict t-combinatorics new-contributor blocked on another PR
29558 Thmoas-Guan feat(Algebra): definition of global dimension awaiting-author t-ring-theory awaiting author
31999 Thmoas-Guan feat(RingTheory): global dimension equals the supremum over localizations blocked-by-other-PR awaiting-author ⚠️ blocked on another PR
29534 Thmoas-Guan feat(Algebra): global dimension of regular local ring blocked-by-other-PR large-import ⚠️ blocked on another PR
29699 Thmoas-Guan feat(Algebra/RingTheory): global dimension of regular ring blocked-by-other-PR large-import ⚠️ blocked on another PR
29796 Thmoas-Guan feat(RingTheory): regular of finite global dimension blocked-by-other-PR large-import ⚠️ blocked on another PR
29802 Thmoas-Guan feat(Algebra/RingTheory): Auslander–Buchsbaum–Serre criterion and its corollaries blocked-by-other-PR large-import ⚠️ blocked on another PR
29703 Thmoas-Guan feat(Algebra/RingTheory): Hilbert's Syzygy theorem (projective version) WIP blocked-by-other-PR large-import ⚠️ blocked on another PR
33592 nielstron feat(Computability/ContextFreeGrammar): mapping between two types of nonterminal symbols new-contributor t-computability awaiting review
32742 LTolDe feat(MeasureTheory/Constructions/Polish/Basic): add class SuslinSpace new-contributor awaiting-zulip ⚠️ awaiting a zulip discussion
29251 yoh-tanimoto feat(Analysis/InnerProductSpace/): define standard subspaces of a complex Hilbert space blocked-by-other-PR ⚠️ blocked on another PR
31560 AntoineChambert-Loir feat(Topology/Sion): the minimax theorem of von Neumann - Sion t-topology awaiting review
33675 euprunin feat(RingTheory/RingHom): remove unnecessary assumptions in `locally_StableUnderCompositionWithLocalizationAwayTarget` (WIP) WIP t-ring-theory labelled WIP
33286 euprunin chore: golf using `grind` awaiting review
33464 Paul-Lez feat(Analysis/ODE/Gronwall): Add two easy lemmas awaiting-author t-analysis awaiting author
33454 astrainfinita feat: lemmas about `IsometryClass` awaiting-author t-topology t-analysis awaiting author
13740 YaelDillies feat: more robust ae notation awaiting-author t-meta t-measure-probability awaiting author
32165 yuanyi-350 feat(Real/Trigonometric): Add `sum_cos_arith_progression` and prepare for Dirichlet kernel awaiting-author merge-conflict t-analysis merge conflict
33050 mkaratarakis feat: lemmas for the analytic part of the proof of the Gelfond–Schneider theorem awaiting-author t-number-theory new-contributor awaiting author
30985 erdOne feat(AlgbraicGeometry), `Hom(-, X)` commutes with inverse limits for schemes of finite presentation t-algebraic-geometry failing CI
33691 kim-em feat(scripts): add find-ci-errors.sh to diagnose widespread CI failures delegated CI delegated
33492 YaelDillies feat(Algebra/MonoidAlgebra): `R[M][N] ≃+* R[N][M]` t-algebra awaiting review
31892 jsm28 feat(Geometry/Euclidean/Sphere/PolePolar): poles and polars blocked-by-other-PR t-euclidean-geometry blocked on another PR
31893 jsm28 feat(Geometry/Euclidean/Sphere/Tangent): characterize `tangentsFrom` blocked-by-other-PR t-euclidean-geometry blocked on another PR
31981 jsm28 feat(Geometry/Euclidean/Incenter): `tangentSet` and `tangentsFrom` lemmas blocked-by-other-PR t-euclidean-geometry blocked on another PR
32295 jsm28 feat(Archive/Imo/Imo2024Q4): IMO 2024 Q4 blocked-by-other-PR IMO blocked on another PR
33389 khwilson feat(Mathlib/Analysis/SpecialFunctions/Log/Base): More log asymptotics awaiting-author t-analysis new-contributor awaiting author
33368 urkud feat: define `Complex.UnitDisc.shift` merge-conflict t-analysis awaiting-zulip awaiting a zulip discussion
33450 astrainfinita refactor: deprecate `LinearIsometryClass` blocked-by-other-PR merge-conflict t-topology t-analysis t-algebra blocked on another PR
33295 AntoineChambert-Loir feat(Algebra/Central/End): center of the group of automorphisms of a free module WIP t-algebra labelled WIP
33702 JovanGerb doc(Algebra/Quotient): update `HasQuotient.Quotient` doc-string delegated t-algebra delegated
33683 joelriou feat(AlgebraicTopology/SimplicialSet): the simplicial homotopy induced by an homotopy WIP t-algebraic-topology labelled WIP
32134 mitchell-horner feat(Topology/Real): theorems linking `IsGLB` with `BddBelow`, `Antitone`, `Tendsto _ atTop` t-topology maintainer-merge large-import awaiting review
32583 MJ141592 refactor(SimpleGraph): change bridges not to require the edge to be present awaiting-author t-combinatorics new-contributor failing CI
33434 astrainfinita chore: redefine `Finsupp.indicator` using `Finsupp.onFinset` t-data failing CI
28682 Thmoas-Guan feat(RingTheory): definition of regular local ring awaiting-author t-ring-theory awaiting author
33192 linesthatinterlace refactor(Data/List/Induction): improve definition of `reverseRecOn` t-data awaiting review
33388 plby doc(docs/100.yaml): add recently-proven theorems awaiting-author new-contributor awaiting author
31607 grunweg chore: rename `continuous{,On,At,Within}_const to `ContinuousFoo.const` delegated merge-conflict awaiting-CI does not pass CI
33554 themathqueen chore(Analysis/Normed/Module/Normalize): allow for `RCLike` instead of just the reals awaiting-author merge-conflict t-analysis merge conflict
32811 erdOne feat(RingTheory): predicate on satisfying Zariski's main theorem t-ring-theory awaiting review
33680 BoltonBailey feat(Probability/ProbabilityMassFunction): add Total Variation distance t-measure-probability failing CI
31754 dagurtomas feat(Topology/Category): light profinite sets are injective objects merge-conflict t-category-theory t-topology merge conflict
33194 YuvalFilmus feat(LinearAlgebra/Lagrange): refactored proof of leadingCoeff_eq_sum t-algebra awaiting review
33259 YuvalFilmus feat(Trigonometric/Chebyshev/Extremal): Chebyshev polynomials are extremal in terms of leading coefficient blocked-by-other-PR t-analysis blocked on another PR
32939 JovanGerb fix(to_additive): don't translate into non-existent names delegated t-meta delegated
33561 kbuzzard chore: cont -> continuous_toFun merge-conflict merge conflict
33288 vihdzp chore(Combinatorics/SimpleGraph/Paths): review API t-combinatorics awaiting review
26299 adomani perf: the `commandStart` linter only acts on modified files awaiting-author merge-conflict t-linter merge conflict
27507 grunweg wip(commandStart): check the indentation of declaration keywords also WIP merge-conflict t-linter labelled WIP
26088 grunweg chore(Linter/DirectoryDependency): move forbidden directories into a JSON file please-adopt merge-conflict t-linter looking for help
33336 fbarroero feat(NumberTheory/MahlerMeasure): Kronecker's Theorem for the Mahler Measure ⚠️ awaiting review
33633 mcdoll chore(Analysis/Fourier): split type class, add continuity one t-analysis large-import awaiting review
28708 sjh227 feat(LinearAlgebra): define row- and column-stochastic matrices new-contributor t-data awaiting review
31854 erdOne chore(AlgebraicGeometry): API for `𝒪ₓ`-modules t-algebraic-geometry awaiting review
33372 kex-y feat(Probability): Countable infimum of stopping times is a stopping time t-measure-probability brownian awaiting review
33436 astrainfinita feat: lemmas about `(Add)MonoidAlgebra.mapRangeRingHom` t-algebra awaiting review
33544 YaelDillies chore(LinearAlgebra): make one more argument implicit in `ker_toSpanSingleton` t-algebra awaiting review
33330 michael-novak-math feat: add arc-length reparametrization of parametrized curves merge-conflict t-analysis new-contributor merge conflict
33707 jcommelin ci: add commit verification for transient and automated commits merge-conflict CI failing CI
32617 erdOne feat(RingTheory): field extension over perfect fields are smooth t-ring-theory awaiting review
33741 mcdoll feat(Analysis/SchwartzSpace): additional lemmas for `smulLeftCLM` t-analysis awaiting review
33712 wangying11123 abbrev(Geometry/Euclidean/Angle/Unoriented/Projection):Add sameray_orthogonalProjection_vsub_of_angle_lt t-euclidean-geometry new-contributor failing CI
33033 kim-em feat(Tactic/Choose): add type annotation support t-meta awaiting review
32851 tdwag123 feat(MeasureTheory/Measure/TypeClass/NoAtoms) add `exists_accPt_of_noAtoms` awaiting-author t-measure-probability new-contributor awaiting author
31449 kim-em feat(SemilocallySimplyConnected): definition and alternative formulation awaiting-author t-topology awaiting author
33745 euprunin chore: golf proofs awaiting review
26986 WangYiran01 feat(Partition): add bijection for partitions with max part ≤ r awaiting-author t-combinatorics new-contributor awaiting author
33314 YuvalFilmus feat(Trigonometric/Chebyshev/Basic): calculate iterated derivatives of T and U at 1 blocked-by-other-PR ⚠️ blocked on another PR
27599 mitchell-horner feat(Combinatorics/SimpleGraph): define `CompleteEquipartiteSubgraph` t-combinatorics awaiting review
33751 mcdoll feat(Analysis/FourierSchwartz): self-adjointness for the inverse Fourier transform t-analysis awaiting review
33752 mcdoll feat(Analysis/FourierSchwartz): the derivative of the Fourier transform t-analysis awaiting review
33743 jcommelin ci: add automated commit verification CI awaiting review
33449 yuanyi-350 feat(ProbabilityTheory): Add Poisson limit theorem t-measure-probability awaiting review
24010 grunweg feat(Counterexamples): a non-negative function, not a.e. zero, with vanishing lowe… WIP blocked-by-other-PR please-adopt merge-conflict t-measure-probability blocked on another PR
33754 euprunin chore: golf proofs awaiting review
30855 Ruben-VandeVelde fix: deprecate IsTotal in favour of Std.Total merge-conflict RFC t-order merge conflict
24065 kim-em chore: script to give topological sort of modules awaiting-author awaiting author
28700 Timeroot feat(ModelTheory): Set.Definable is transitive merge-conflict t-logic large-import merge conflict
33746 ster99 feat(Algebra/Module/ZLattice): add lemma `floor b (m + x) = m + floor b x` and similar t-algebra new-contributor failing CI
33763 smmercuri doc: add note in `Asymptotics` docstring about the existential pattern t-analysis awaiting review
30608 grunweg feat: another lemma about derivatives of parametric integrals awaiting-author merge-conflict t-analysis merge conflict
30610 grunweg feat: yet another lemma about differentiability of parametric integrals blocked-by-other-PR merge-conflict t-analysis blocked on another PR
29942 smmercuri feat(InfinitePlace/Completion): embeddings of `w.Completion` factor through embeddings of `v.Completion` when `w` extends `v` FLT ⚠️ awaiting review
33275 YuvalFilmus feat(Trigonometric/Chebyshev/Extremal): Chebyshev polynomials maximize iterated derivatives blocked-by-other-PR ⚠️ blocked on another PR
33299 kingiler feat: Add decidable membership for Interval awaiting-author t-order new-contributor awaiting author
30484 vihdzp refactor: override `≤` and `<` in `Function.Injective.semilatticeSup`, etc. t-order awaiting review
33359 sun123zxy feat(Algebra/Module/SpanRank): add comparing lemmas for span rank t-algebra new-contributor awaiting review
29186 winstonyin feat: IsIntegralCurve for solutions to ODEs t-differential-geometry t-analysis t-dynamics awaiting review
33274 YuvalFilmus feat(LinearAlgebra/Lagrange): Formula for iterated derivative of a polynomial using Lagrange interpolation blocked-by-other-PR ⚠️ blocked on another PR
33045 chrisflav feat(CategoryTheory/MorphismProperty): `ind P` is stable under composition if `P` is awaiting-author t-category-theory awaiting author
32190 vihdzp chore(Algebra/Order/Ring/Archimedean): generalize theorems to `OrderHomClass` + `RingHomClass` t-algebra failing CI
33654 vihdzp chore: `LinearOrderedCommMonoidWithZero` extends `ZeroLEOneClass` t-algebra failing CI
33740 SnirBroshi chore(Order/CompleteLattice/Basic): generalize many theorems to `CompleteSemilattice{Sup/Inf}` t-order awaiting review
33768 vihdzp chore(Order/RelClasses): remove redundant instances t-order awaiting review
32672 tb65536 feat: haar measures on short exact sequences t-topology t-measure-probability FLT awaiting review
31141 peabrainiac feat(Analysis/Calculus): parametric integrals over smooth functions are smooth awaiting-author merge-conflict t-analysis merge conflict
32042 chrisflav feat(AlgebraicGeometry): quasi compact covers t-algebraic-geometry awaiting review
33749 plp127 feat: `NNRat` is countable t-data large-import awaiting review
33769 alreadydone feat(LinearAlgebra): add `Module.IsPrincipal` t-algebra awaiting review
33527 SnirBroshi feat(Combinatorics/SimpleGraph/Connectivity/Subgraph): `w.toSubgraph ≤ G' ↔ w.edgeSet ⊆ G'.edgeSet` t-combinatorics awaiting review
33776 mcdoll feat(MeasureTheory): every bounded continuous function is in `L∞` t-measure-probability awaiting review
33780 ooovi feat(Geometry/Convex/Cone): lineality space of pointed cones t-convex-geometry awaiting review
33329 mcdoll feat(Analysis): Fourier-based Sobolev spaces WIP blocked-by-other-PR merge-conflict t-analysis large-import blocked on another PR
25841 mitchell-horner feat(Combinatorics/SimpleGraph): prove the Kővári–Sós–Turán theorem t-combinatorics awaiting review
33214 JJYYY-JJY chore(Data/List/Rotate): add simp attributes new-contributor t-data awaiting review
33582 urkud feat(ContDiffHolder/Moreira): define $C^{k+(α)}$ maps t-analysis awaiting review
33635 plp127 feat(Tactic/Set): use `binderIdent` instead of `ident` t-meta awaiting review
33636 mcdoll feat(Analysis/Distribution): the Laplacian on Schwartz functions t-analysis awaiting review
33757 fpvandoorn feat: remove decidability instances on sets or ideals ⚠️ awaiting review
30204 yonggyuchoimath feat(Algebra/Category/Ring/EqualizerPushout): add effectiveEpi_of_faithfullyFlat in CommRingCatᵒᵖ blocked-by-other-PR ⚠️ blocked on another PR
33771 plp127 feat: prove `Prod.wellFoundedLT` directly t-order awaiting review
33784 tb65536 refactor(Topology/Irreducible): weaken assumptions of `preimage_mem_irreducibleComponents_of_isPreirreducible_fiber` t-topology awaiting review
33542 yuanyi-350 feat(integral): Error Estimation for the Rectangle Rule in Numerical Integration t-analysis awaiting review
28546 Sfgangloff feat(SymbolicDynamics): basic setup of Zd, full shift, cylinders, pat… t-dynamics new-contributor awaiting review
29203 Hagb feat(RingTheory/MvPolynomial/Groebner): add Gröbner basis awaiting-author large-import t-ring-theory awaiting author
32744 NoneMore feat(ModelTheory/Definablity): add `DefinableFun` definition and lemmas t-logic new-contributor awaiting review
31325 joelriou feat(AlgebraicTopology): a computable monoidal functor instance for `hoFunctor` maintainer-merge t-algebraic-topology awaiting review
33787 LTolDe doc(Topology/Baire/BaireMeasurable): add naming convention for notation `residualEq` easy t-topology new-contributor awaiting review
33714 idontgetoutmuch Riemannian metrics exist II t-differential-geometry new-contributor awaiting review
33555 erdOne feat(RingTheory): standard smooth = etale over mvpolynomial large-import ⚠️ awaiting review
32438 JovanGerb feat: unfold-boundaries in `to_dual` merge-conflict t-meta merge conflict
33788 harahu chore(Algebra): move `LinearMap.ker_restrictScalars` t-algebra awaiting review
25822 ScottCarnahan WIP: experiments with vertex algebras WIP large-import labelled WIP
33129 Paul-Lez feat(Tactic/Simproc/VecPerm): Add simproc for permuting entries of a vector t-meta awaiting review
32481 ADedecker feat: add `PolynormableSpace.banach_steinhaus` t-analysis awaiting review
33339 Ruben-VandeVelde feat: small lemmas about LeftInverse and image/preimage maintainer-merge t-data awaiting review
32215 jonasvanderschaaf feat(ModelTheory/Types): Construct a topology on CompleteType and prove the space is TotallySeparated t-topology t-logic new-contributor failing CI
33664 ooovi feat(Geometry/Convex/Cone/Pointed): face lattice of pointed cones awaiting-author file-removed t-convex-geometry awaiting author
33767 Whysoserioushah chore(RingTheory/Morita/Matrix): Finish the morita equivalence between matrix ring and the ring itself large-import t-ring-theory awaiting review
33761 ooovi feat(Algebra/Module/Submodule): behaviour of `restrictScalars` under lattice operations t-algebra awaiting review
33613 DavidLedvinka feat(Probability): `UniformOn_univ_instIsProbabilityMeasure` t-measure-probability awaiting review
31706 Thmoas-Guan feat(Algebra/ModuleCat): `ModuleCat.uliftFunctor` t-algebra maintainer-merge awaiting review
33793 LTolDe feat(MeasureTheory/Constructions/Polish/Basic): add lemma AnalyticSet.inter_nonempty_of_nowhereMeagre new-contributor ⚠️ awaiting review
33403 xroblot feat(GroupTheory/FiniteAbelian): prove that the restriction map is surjective t-group-theory awaiting review
30142 shalliso feat(Topology/Baire): define IsNonMeagre merge-conflict t-topology new-contributor failing CI
33531 harahu doc(CategoryTheory): fix typos t-category-theory maintainer-merge awaiting review
33786 hdmkindom feat(Analysis/Matrix): add Jacobian matrix for matrix-valued functions t-analysis new-contributor awaiting review
33792 xroblot feat(GroupTheory/FiniteAbelian): construct bijection between subgroups and subgroups of the dual blocked-by-other-PR t-group-theory 🟤 blocked on another PR
33113 sinhp feat(Category Theory): A natural isomorphism connecting Over.iteratedSlice and Over.map t-category-theory maintainer-merge awaiting review
33736 fbarroero feat(RingTheory/Polynomial/GaussNorm): The `gaussNorm` is an absolute value if `v` is a nonarchimedean absolute value ⚠️ awaiting review
31925 alreadydone feat(Topology): étalé space associated to a predicate on sections blocked-by-other-PR t-topology blocked on another PR
33656 metakunt feat(Data/Nat/Choose): Add sum_range_multichoose t-data awaiting review
33551 metakunt feat(Data/Nat/Factorization/PrimePow): Add Nat.nontrivial_primeFactors_of_two_le_of_not_isPrimePow t-data awaiting review
33538 JohnnyTeutonic feat(Data/Matrix/Cartan): non-simply-laced theorems for F and G maintainer-merge t-data awaiting review
33221 stepan2698-cpu feat: definition of an intertwining map t-algebra new-contributor awaiting review
33447 urkud feat(FundamentalGroupoid): define simply connected sets maintainer-merge t-algebraic-topology awaiting review
33800 bryangingechen ci(lint_and_suggest.yml): rename job easy CI awaiting review
33795 alreadydone feat(Topology/Sheaves): LocalPredicate prerequisite for étalé spaces t-topology awaiting review
29241 yoh-tanimoto feat(Analysis/InnerProductSpace/Orthogonal): add duplicates for `ClosedSubmodule` ⚠️ awaiting review
33723 erdOne feat(Analytic): `℘'(z)² = 4 ℘(z)³ - g₂ ℘(z) - g₃` t-analysis awaiting review
33535 erdOne feat(Algebra/Category): `Under.pushout` preserves finite limits for flat homomorphisms t-algebra awaiting review
32881 foderm feat(AlgebraicTopology/SimplicialObject): define simplicial homotopy awaiting-author new-contributor t-algebraic-topology awaiting author
32856 stepan2698-cpu feat: definition of an irreducible representation t-algebra new-contributor awaiting review
33803 erdOne feat(RingTheory): integral closure commutes with standard etale basechange large-import t-ring-theory failing CI
33518 joelriou feat(CategoryTheory/Sites): fullness of `DescentData.pullFunctor` awaiting-author t-category-theory awaiting author
33805 erdOne feat(AlgebraicGeometry): relative normalization in coproduct t-algebraic-geometry failing CI
33718 erdOne feat(RingTheory): predicate for `QuasiFiniteAt` large-import t-ring-theory failing CI
33807 adamtopaz feat: TypeCat refactor WIP t-category-theory labelled WIP
32534 erdOne feat(AlgebraicGeometry): Zariski's main theorem WIP blocked-by-other-PR t-ring-theory blocked on another PR
30640 SnirBroshi feat(Combinatorics/SimpleGraph/Acyclic): acyclic and bridge theorems t-combinatorics awaiting review
28208 Sebi-Kumar feat(Topology): add the definition `foldTrans` to concatenate finite sequences of paths t-topology new-contributor failing CI
22366 kim-em feat: `check_equalities` tactic for diagnosing defeq problems delegated merge-conflict t-meta failing CI
25899 pfaffelh feat(Topology/Compactness/CompactSystem): introduce compact Systems awaiting-author merge-conflict t-topology brownian ❌? infrastructure-related CI failing*
30579 smmercuri feat : `v.adicCompletionIntegers K` is compact when `K` is a number field WIP blocked-by-other-PR merge-conflict large-import ⚠️ blocked on another PR
31755 kaantahti feat(Combinatorics): Add Sperner's Lemma formalization WIP merge-conflict t-combinatorics new-contributor labelled WIP
31809 ADedecker feat: differentiation of test function as a CLM blocked-by-other-PR merge-conflict t-analysis blocked on another PR
32210 ADedecker feat: iteratedFDeriv as a linear map on test functions t-analysis awaiting review
32305 faenuccio feat: define Sobolev Spaces WIP blocked-by-other-PR merge-conflict t-analysis large-import blocked on another PR
32401 ADedecker feat: monotonicity of D^n(U) in n and in U as CLMs delegated merge-conflict t-analysis merge conflict
32410 callesonne feat(Bicategory/FunctorCategory/Pseudo): Add evaluation pseudofunctor WIP blocked-by-other-PR merge-conflict t-category-theory blocked on another PR
33606 ScottCarnahan feat(Algebra/Lie): basics of loop algebras t-algebra failing CI
33240 khwilson feat(Mathlib/Analysis/Polynomial/Norm): Introduce Polynomial.supNorm awaiting-author merge-conflict t-analysis new-contributor merge conflict
33387 AntoineChambert-Loir chore(LinearAlgebra/Transvection/Basic): mv Transvection.lean file to Transvection.Basic.lean blocked-by-other-PR merge-conflict t-algebra file-removed blocked on another PR
33392 AntoineChambert-Loir feat(LinearAlgebra/Transvection/Generation): non-exceptional case in Dieudonné's theorem blocked-by-other-PR merge-conflict t-algebra file-removed blocked on another PR
33402 AntoineChambert-Loir feat(LinearAlgebra/Transvection/Generation): prove exceptional case in Dieudonné's theorem blocked-by-other-PR t-algebra file-removed blocked on another PR
33485 AntoineChambert-Loir feat(LinearAlgebra/Transvection/Generation): prove the third part of Dieudonné's theorem blocked-by-other-PR merge-conflict t-algebra file-removed blocked on another PR
33560 AntoineChambert-Loir feat(LinearAlgebra/Transvection/Generation): a linear equivalence is the product of dilatransvections blocked-by-other-PR merge-conflict t-algebra file-removed blocked on another PR
33645 kim-em feat(TacticAnalysis): verify grind? suggestions work merge-conflict t-meta failing CI
33692 AntoineChambert-Loir feat(LinearAlgebra/Transvection/SpecialLinearGroup): generation of the special linear group by transvections blocked-by-other-PR merge-conflict t-algebra file-removed blocked on another PR
33715 AntoineChambert-Loir feat(LinearAlgebra/Projectivization/Action): prove that the action is 2-transitive and primitive blocked-by-other-PR merge-conflict t-algebra large-import file-removed blocked on another PR
33766 alreadydone feat(Analysis, Topology): more examples of covering maps involving the complex plane blocked-by-other-PR merge-conflict t-topology t-analysis large-import blocked on another PR
33810 dupuisf feat: add instances of `LawfulInv` WIP blocked-by-other-PR ⚠️ blocked on another PR
26168 oliver-butterley feat(MeasureTheory.VectorMeasure): variation defined as a supremum is equal to variation defined using the Hahn-Jordan decomposition blocked-by-other-PR t-measure-probability new-contributor blocked on another PR
30562 dwrensha fix(Data/Fintype/Perm): make the main logic of Equiv.instFintype irreducible awaiting-author t-data failing CI
33726 alreadydone feat(Analysis): (complex) polynomials as branched coverings t-topology t-analysis large-import awaiting review
33409 jsm28 feat(LinearAlgebra/AffineSpace/Ceva): Ceva's theorem t-algebra t-euclidean-geometry awaiting review
33588 JovanGerb chore(Geometry/Euclidean/SignedDist): remove `privateInPublic` t-euclidean-geometry maintainer-merge awaiting review
33802 stepan2698-cpu feat: Schur's lemma for monoid representations t-algebra new-contributor awaiting review
33188 BryceT233 feat: MvPowerSeries.rename awaiting-author new-contributor t-ring-theory awaiting author
28126 Sebi-Kumar feat(AlgebraicTopology/FundamentalGroupoid): relate equality in fundamental groupoid to homotopy awaiting-author new-contributor t-algebraic-topology please-merge-master failing CI
33491 themathqueen feat(Analysis/InnerProductSpace): linear map is positive iff it equals the sum of rank-one operators t-analysis awaiting review
33594 smmercuri feat: `HeightOneSpectrum.valuation` is rank one for number fields large-import ⚠️ awaiting review
33643 vihdzp feat: `r < stdPart x → r < x` t-algebra awaiting review
33657 vihdzp chore(SetTheory/Cardinal/Arithmetic): switch `lift.{max u w} x = lift.{max v w} y` to `lift.{u} x = lift.{v} y` t-set-theory awaiting review
33662 Pjotr5 feat(Algebra/Order/BigOperators/Expect): add lemmas and strict variants new-contributor ⚠️ awaiting review
33668 Citronhat feat(PMF): add lintegral formulas for PMF t-measure-probability new-contributor awaiting review
33672 euprunin chore: golf using `grind`. add `grind` annotations. awaiting review
33676 YuvalFilmus feat(Chebyshev/Orthogonality): Chebyshev T polynomials are orthogonal t-analysis awaiting review
33679 DavidLedvinka feat(MeasureTheory): add formulas for the measures formed by a density with respect to counting or dirac measures. t-measure-probability awaiting review
33688 Citronhat feat(PMF): add expectation lemmas for Poisson PMF t-measure-probability new-contributor awaiting review
27936 alreadydone feat(Algebra): additivize Dvd and Prime t-algebra failing CI
33801 artie2000 chore: add missing mem lemmas t-meta awaiting review
32892 Parcly-Taxel feat(Analysis/SpecialFunctions): arithmetic-geometric mean t-analysis failing CI
31180 CoolRmal feat(Analysis): a closed convex set is the intersection of countably many half-spaces in a separable Banach space awaiting-author t-analysis new-contributor failing CI
32186 urkud feat(Integral): estimate displacement by the integral of the speed t-measure-probability awaiting review
33441 dupuisf feat: add `LawfulInv` class for types with an inverse that behaves like `Ring.inverse` t-algebra awaiting review
33669 eric-wieser chore(Data/Nat/Digits): refactor to use List.rightpad merge-conflict large-import failing CI
33814 seewoo5 feat(Manifold/MFDeriv): add `MDifferentiable.pow` with FunProp blocked-by-other-PR t-differential-geometry blocked on another PR
32541 YaelDillies chore: import Tactic.Attr.Register privately large-import awaiting review
33774 SnO2WMaN doc(100.yaml, 1000.yaml): Update about Gödel's Incompleteness Theorem new-contributor awaiting review
33753 SnO2WMaN doc(1000.yaml): Mention Tarski's Undefinability Theorem in FFL new-contributor awaiting review
32745 LTolDe feat(Topology/Algebra): add MulActionConst.lean t-topology new-contributor awaiting review
31653 ster99 feat(MeasureTheory): Foelner filters new-contributor ⚠️ awaiting review
33237 JovanGerb feat(CategoryTheory/Functor): use `@[to_dual]` ready-to-merge t-category-theory awaiting bors
33770 eric-wieser chore(RingTheory/Morita/Matrix): remove uses of `default` t-ring-theory awaiting review
33282 AntoineChambert-Loir feat(LinearAlgebra/Center): description of the center of the algebra of endomorphisms t-algebra failing CI
32757 AntoineChambert-Loir feat(LinearAlgebra/Transvection): the determinant of a transvection is equal to 1. ⚠️ awaiting review
33348 AntoineChambert-Loir feat(LinearAlgebra/Transvection): characterization of transvections among dilatransvections blocked-by-other-PR t-algebra blocked on another PR
33347 AntoineChambert-Loir feat(LinearAlgebra/Transvection/Basic): define dilatransvections t-algebra awaiting review
33812 urkud feat: define `List.offDiag` t-data awaiting review
33772 urkud chore(*): rename `EMetric.infEdist` -> `Metric.infEDist` etc awaiting review
33552 YaelDillies feat: a non-domain cannot act faithfully on a domain t-algebra maintainer-merge awaiting review
33312 YuvalFilmus feat(Polynomial/Chebyshev): formulas for iterated derivatives of T and U at 1 ⚠️ awaiting review
33493 michelsol feat(RingTheory/Polynomial): An explicit formula for the Chebyshev polynomials of the first kind new-contributor t-ring-theory awaiting review
29960 yonggyuchoimath feat(Algebra/Category/Ring): equalizers of pushout maps of tensor product inclusions awaiting-author new-contributor t-ring-theory awaiting author
33411 IlPreteRosso feat(Analysis/DiscreteConvolution): Discrete convolution API basics t-analysis new-contributor awaiting review
32924 chrisflav feat(RingTheory/Smooth): smooth is equivalent to locally standard smooth awaiting-author large-import t-ring-theory awaiting author
33818 JohnnyTeutonic feat(Algebra/Lie/Classical): finrank of sl(n) equals n² - 1 t-algebra awaiting review
33782 tb65536 refactor(RingTheory/Lasker): create structure for primary decomposition t-algebra t-ring-theory awaiting review
33525 urkud feat(AddCircle/Defs): prove continuity of `toIocDiv` etc awaiting-author t-topology awaiting author
33390 farmanb feat(RingTheory/Ideal): generalize Submodule.colon to sets awaiting-author new-contributor t-ring-theory awaiting author
27557 chrisflav feat(RingTheory/KrullDimension): dimension of `R / (x)` for a nonzerodivisor merge-conflict t-ring-theory failing CI
33798 Paul-Lez feat(Combinatorics/SimpleGraph/Basic): decidability instance for `fromRel.Adj` t-combinatorics maintainer-merge awaiting review
33604 xgenereux feat(ValuationSubring): eq_top_iff + qol changes t-ring-theory failing CI
33612 xgenereux feat(ValuationSubring): fieldTop t-ring-theory awaiting review
33823 SnirBroshi chore(GroupTheory/GroupAction/Defs): golf `orbitRel.iseqv` t-group-theory awaiting review
32984 artie2000 refactor: remove order instances from `SetLike` t-meta t-data awaiting review
31794 thorimur feat: `unusedFintypeInType` linter merge-conflict file-removed ⚠️ merge conflict
31795 thorimur feat: turn on `unusedFintypeInType` linter blocked-by-other-PR merge-conflict file-removed ⚠️ blocked on another PR
32440 thorimur feat: make the `unusedDecidableInType` linter fire when `Decidable*` instances are used only inside of proofs in the type merge-conflict t-linter merge conflict
33393 grunweg chore: extend the whitespace linter to structure and instance fields blocked-by-other-PR please-adopt merge-conflict large-import blocked on another PR
33790 eliasjudin feat(CategoryTheory/Preadditive/Mat): add natural transformation and isomorphism extension theorems awaiting-author t-category-theory new-contributor awaiting author
33634 xgenereux feat(ValuationSubring): eq_self_or_eq_top_of_le blocked-by-other-PR large-import ⚠️ blocked on another PR
33631 xgenereux feat(ValuationSubring): simp lemmas for idealOfLE/ofPrime in relation to top/bot blocked-by-other-PR ⚠️ blocked on another PR
33360 joelriou feat(Algebra/Homology): functoriality of `extMk` with respect to the injective resolution t-category-theory awaiting review
26156 oliver-butterley feat(MeasureTheory.VectorMeasure): add a definition of total variation for VectorMeasure awaiting-author t-measure-probability new-contributor awaiting author
31595 astrainfinita chore: redefine `Ideal.IsPrime` merge-conflict t-algebra merge conflict
33825 euprunin chore: golf using `grind` awaiting review
33826 euprunin chore: golf using `grind` awaiting review
33804 tb65536 feat(RingTheory/Localization/Ideal): `map` distributes over `inf` t-algebra t-ring-theory awaiting review
33049 xgenereux feat: Valuation.IsTrivialOn t-ring-theory 🟤 running CI
25889 plp127 fix(Tactic/Widget/Conv): fix various issues t-meta awaiting review
33236 JovanGerb refactor(translate): merge `expand` into `applyReplacementFun` t-meta awaiting review
33658 vihdzp refactor(RingTheory/Valuation/ValuativeRel/Basic): fix theorem names for multiplication t-ring-theory awaiting review
33819 bjornsolheim feat(Analysis/Convex): diameter of a standard simplex t-analysis awaiting review
25905 mans0954 feat(RingTheory/Polynomial/SmallDegreeVieta): polynomial versions of results in Algebra.QuadraticDiscriminant please-adopt merge-conflict t-ring-theory looking for help
25907 mans0954 feat: low order roots of unity please-adopt t-algebra looking for help
26339 mans0954 feat(Analysis/Normed/Module/WeakDual): Banach Dieudonné Lemma WIP please-adopt merge-conflict t-analysis large-import looking for help
26340 mans0954 feat(Algebra/Module/NestAlgebra): Nest algebras please-adopt merge-conflict t-algebra looking for help
26341 mans0954 feat(LinearAlgebra/QuadraticForm/Basis): Free Tensor product of Quadratic Maps WIP please-adopt merge-conflict t-algebra large-import looking for help
33607 xgenereux feat: primeSpectrum_eq_of_KrullDimLEOne WIP awaiting-author t-ring-theory labelled WIP
33830 seewoo5 feat(Manifold/MFDeriv): `MDifferentiable.pow` and variants t-differential-geometry awaiting review
33808 seewoo5 feat(Manifold/MFDeriv): add fun_prop to `MDifferentiable` awaiting-author t-differential-geometry awaiting author
26344 mans0954 feat(Analysis/NormedSpace/MStructure): The component projections on WithLp 1 (α × β) are L-projections WIP please-adopt merge-conflict t-analysis file-removed looking for help
26345 mans0954 feat(Analysis/LocallyConvex/Polar): Bipolar theorem awaiting-author please-adopt merge-conflict t-analysis large-import looking for help
26347 mans0954 feat(Data/Finset/RangeDistance): abs_sub_lt_of_mem_finset_range please-adopt merge-conflict t-data looking for help
26349 mans0954 feat(Analysis/SpecialFunctions/Trigonometric/Basic): sin and cos of multiples of π / 3 help-wanted please-adopt t-analysis looking for help
26348 mans0954 feat(Analysis/LocallyConvex/Prime): the prime map WIP please-adopt merge-conflict t-analysis looking for help
26983 mans0954 feat(Order/LatticeElements): distributive, standard and neutral elements of a lattice WIP please-adopt merge-conflict t-order looking for help
29980 mans0954 refactor(RingTheory/Polynomial/Resultant/Quadratic): Re-implement QuadraticDiscriminant for R[X] please-adopt merge-conflict looking for help
29387 mans0954 feat(Analysis/LocallyConvex/WeakSpace): toWeakSpace_closedAbsConvexHull_eq blocked-by-other-PR please-adopt merge-conflict t-analysis blocked on another PR
30378 mans0954 refactor(Order/Hom/Lattice): Use default `initialize_simps_projections` configuration for `LatticeHom`. t-order awaiting review
29378 mans0954 feat(Analysis/LocallyConvex/AbsConvex): Balanced and AbsConvex sets under linear maps merge-conflict t-analysis merge conflict
29856 mans0954 feat(Analysis/Normed/Ring/Basic): Add NonUnitalNonAssocSeminormedRing and NonUnitalNonAssocNormedRing please-adopt t-analysis looking for help
26614 Rida-Hamadani feat(SimpleGraph): add more API for `take`/`drop` t-combinatorics awaiting review
32734 Vierkantor chore(Tactic): document remaining undocumented tactics documentation t-meta awaiting review
32735 Jlh18 refactor: move `CategoryTheory.Category.Grpd` to `CategoryTheory.Groupoid.Grpd.Basic` file-removed awaiting review
33185 alreadydone feat(Algebra): MulAction/SMulWithZero by Nat/Int t-algebra awaiting review
33504 ldct feat: Add lemmas for DihedralGroup.fintypeHelper t-group-theory awaiting review
33611 urkud feat(ImplicitFunction): add a parametric version t-analysis awaiting review
33642 themathqueen feat(Analysis/Matrix/Order): polar decomposition for {invertible, Hermitian} matrices t-analysis awaiting review
33649 vihdzp feat(Analysis/Real/Hyperreal): more lemmas on `ω` and `ε` t-algebra large-import awaiting review
33693 yoh-tanimoto feat(Mathlib/Analysis/Normed/Module): add instances of `CompleteSpace` for `Submodules` and `ClosedSubmodule` ⚠️ awaiting review
33698 artie2000 feat(Algebra/Ring): characteristic of semireal ring t-algebra awaiting review
33699 artie2000 chore(Algebra/Ring): semireal definition lemmas t-algebra awaiting review
33700 vihdzp feat: dense orders have elements lying between two finite sets t-order large-import awaiting review
33709 wangying11123 feat(Analysis/Convex/Between):Add wbtw_of_sameRay_vsub_left new-contributor ⚠️ awaiting review
33722 erdOne feat(RingTheory): Add `RingHom.QuasiFinite` t-ring-theory awaiting review
33724 alreadydone chore(Algebra): deprecate `DistribMulAction.toAddMonoidHom` t-algebra awaiting review
33501 SnirBroshi feat(Combinatorics/SimpleGraph/Finite): degrees for infinite graphs t-combinatorics large-import awaiting review
33828 themathqueen chore(Algebra/Group/Center): golf some stuff t-algebra awaiting review
33665 JovanGerb fix(addRelatedDecl): support imported theorems in module t-meta awaiting review
33532 vihdzp feat(RingTheory/Valuation/ValuativeRel): introduce `=ᵥ` relation awaiting-author t-ring-theory awaiting author
33797 SnirBroshi chore(Order/Defs/Unbundled): deprecate `IsTotal` in favor of core's `Std.Total` awaiting review
33821 JohnnyTeutonic feat(LinearAlgebra/Matrix/Hermitian): add IsSkewHermitian predicate t-algebra 🟤 running CI
33239 JovanGerb feat(to_dual): linter for redundant uses of `to_dual`/`to_additive` ⚠️ awaiting review
33478 anishrajeev feat(ModelTheory): define a subset of the topology over complete types new-contributor ⚠️ awaiting review
30526 SnirBroshi chore(Logic/Relation): use `Subrelation` to state theorems t-logic awaiting-zulip awaiting a zulip discussion
33833 JovanGerb feat(reassoc): tag the generated declaration with `to_dual none` t-meta awaiting review
33209 JovanGerb feat(infoview_search): move to new frontend blocked-by-other-PR t-meta large-import file-removed blocked on another PR
33834 JovanGerb feat(CategoryTheory/NatTrans): use to_dual blocked-by-other-PR ⚠️ blocked on another PR
33052 JovanGerb feat: replace `rw??` tactic with `#infoview_search` command t-meta large-import file-removed 🟤 running CI
33025 JovanGerb feat(gcongr): beef up `@[gcongr]` tag to accept `↔` & any argument order t-meta awaiting review
33831 vihdzp refactor(RingTheory/Polynomial/SmallDegreeVieta): convert to {p : R[X]} (hp : p.natDegree = 2) t-ring-theory awaiting review
33507 khwilson feat(Mathlib/Analysis/Polynomial/Fourier): Add Parseval's Identity specialized to Polynomials awaiting-author t-analysis new-contributor awaiting author
33824 Komyyy doc: update the doc of Bolzano-Weierstrass documentation t-topology awaiting review
33132 BoltonBailey feat(Computability): Single-tape TM complexity WIP blocked-by-other-PR t-computability blocked on another PR
33539 BryceT233 feat(RingTheory/MvPolynomial): powers of ideal of variables awaiting-author new-contributor large-import t-ring-theory failing CI
33835 BoltonBailey chore(Computability/Primrec): split file t-computability tech debt awaiting review
26377 Whysoserioushah feat(RingTheory/SimpleRing/TensorProduct): tensor product of a simple algebra and a central simple algebra is simple t-ring-theory awaiting review
33815 grunweg style: fix whitespace around conditional variance awaiting-author t-measure-probability awaiting author
30658 grunweg feat: extend the `whitespace` linter to proof bodies blocked-by-other-PR awaiting-CI t-linter large-import blocked on another PR*
33417 themathqueen feat: `{Continuous}Linear{Isometry}Equiv.conj{Continuous, Star}AlgEquiv` are "almost" injective t-analysis t-algebra awaiting review
33806 tb65536 feat(RingTheory/Localization/Ideal): generalize `comap_map_of_isPrime_disjoint` to primary ideals delegated merge-conflict t-algebra t-ring-theory ❌? infrastructure-related CI failing
32974 jano-wol feat: golf eq_top_of_invtSubmodule_ne_bot t-algebra awaiting review
33617 j-loreaux feat: continuity of common functions involving the continuous functional calculus merge-conflict t-analysis large-import merge conflict
33777 JovanGerb feat(translate): linter for overwriting existing translations 🟤 ⚠️ running CI
32812 harahu doc(Geometry): fix typos awaiting review
33817 FlAmmmmING fix(Combinatorics/Enumerative/Schroder.lean): Fix the definition and theorem of smallSchroder. t-combinatorics new-contributor large-import awaiting review
33836 VagelisKitsios feat: add lemma `le_abs_of_dvd` easy t-algebra new-contributor awaiting review
32030 newell feat(Analysis/AperiodicOrder/Delone): Delone Sets awaiting-author t-analysis awaiting author
32403 FLDutchmann fix(FieldSimp): `declaration has free variables` kernel errors t-meta awaiting review
32795 fpvandoorn fix: restrict abv positivity extension to variable functions t-meta t-algebra maintainer-merge awaiting review
33791 PhoenixIra feat: Generalization of FixedPointApproximants to CompletePartialOrder new-contributor ⚠️ failing CI
33697 artie2000 feat(FieldTheory): real closed field t-algebra awaiting review
32027 alreadydone feat(Counterexamples): invertible module not isomorphic to any ideal blocked-by-other-PR merge-conflict t-ring-theory ❌? blocked on another PR
33760 JovanGerb feat(Order/Bounds/Basic): use `to_dual` - part 1 t-order large-import awaiting review
33765 JovanGerb feat(Order/CompleteLattice/Defs): `to_dual` for `CompleteSemilattice`s blocked-by-other-PR large-import ⚠️ blocked on another PR
33838 chainstart feat(NumberTheory): add unitary divisor sum function t-number-theory new-contributor awaiting review
33839 qawbecrdtey chore(ModelTheory/Basic): fix comments easy t-logic 🟤 running CI
32144 EtienneC30 feat: add a predicate HasGaussianLaw t-measure-probability brownian awaiting review
25848 joelriou feat/refactor: redefinition of homology + derived categories WIP t-category-theory t-topology large-import labelled WIP
33637 themathqueen feat(Analysis/Matrix/Order): `det (abs A) = |det A|` and `det (sqrt A) = √(det A)` t-analysis awaiting review
30122 xroblot Development branch (1) WIP merge-conflict labelled WIP
33764 IvanRenison feat(Combinatorics/SimpleGraph/Diam): drop `Finite α` from `ediam_le_two_mul_radius` t-combinatorics awaiting review
25273 YaelDillies refactor: make `MonoidAlgebra` into a one-field structure WIP blocked-by-other-PR t-algebra large-import blocked on another PR
32702 SnirBroshi chore(Combinatorics/SimpleGraph/Connectivity): move `Finite ConnectedComponent` instance from `WalkCounting.lean` to `Connected.lean` t-combinatorics awaiting review
33841 unknown unknown title ??? missing CI information
33775 alreadydone chore(Algebra): deduplicate `IsReduced` lemmas t-algebra 🟤 running CI
30563 YaelDillies chore(Algebra): replace `NoZeroSMulDivisors` with `Module.IsTorsionFree` blocked-by-other-PR t-algebra large-import 🟤 blocked on another PR
33837 Komyyy feat: `Tendsto (√·) atTop atTop` t-topology t-order awaiting review
33843 euprunin chore: golf using `grind` and `simp` 🟤 running CI
33690 Ljon4ik4 feat: Defining Lie Rinehart algebras awaiting-author t-algebra new-contributor awaiting author
33832 alreadydone feat(Algebra): localization preserves unique factorization t-algebra bench-after-CI 🟤 running CI
33822 robin-carlier feat(Meta/CategoryTheory): `cancelIso` simproc t-meta t-category-theory awaiting review
33842 joelriou feat(Algebra/Homology): spectral sequences WIP t-category-theory large-import 🟤 labelled WIP
33355 0xTerencePrime feat(Combinatorics/SimpleGraph/Connectivity): define vertex connectivity t-combinatorics new-contributor awaiting review
32764 plp127 feat(Topology/Separation): completely normal iff hereditarily normal delegated t-topology delegated
33785 vihdzp feat: small lemmas on `ArchimedeanClass` t-algebra awaiting review
33844 michelsol feat: lemmas to change variables in iSup / iInf over a set t-order new-contributor 🟤 running CI
33845 bjornsolheim feat(Analysis/Convex): barycenter of a standard simplex t-analysis 🟤 running CI
33840 vihdzp feat(SetTheory/Ordinal/CantorNormalForm): Evaluate a Finsupp as a CNF t-set-theory 🟤 running CI
32880 0xTerencePrime feat(Analysis/Asymptotics): define subpolynomial growth awaiting-author t-analysis new-contributor awaiting author
33744 bilichboris feat(RingTheory): Class Group of a Unique Factorization Domain is trivial new-contributor t-ring-theory 🟤 running CI