Why is my PR not on the queue?

This page was last updated on: January 15, 2026 at 07:58 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 merge-conflict awaiting-author t-algebra t-algebraic-geometry ??? missing CI information
14167 alreadydone feat: Group scheme structure on Weierstrass curve merge-conflict WIP t-algebraic-geometry workshop-AIM-AG-2024 ??? labelled WIP
13297 urkud feat(Semicontinuous): add `comp` lemma merge-conflict awaiting-author t-topology t-order ??? missing CI information
12608 eric-wieser feat: allow `nsmul` / `zsmul` to be omitted again, with a warning merge-conflict awaiting-author t-algebra t-meta ??? missing CI information
12679 MichaelStollBayreuth perf(NumberTheory/RamificationInertia): speed up slow file merge-conflict WIP ??? labelled WIP
12879 grunweg feat: port ge_or_gt linter from mathlib3 merge-conflict t-linter tech debt blocked-by-other-PR ??? blocked on another PR
12933 grunweg chore: replace some use of > or ≥ by < or ≤ merge-conflict awaiting-author ??? missing CI information
13057 alreadydone feat(NumberTheory): characterize elliptic divisibility sequences merge-conflict t-algebra t-number-theory blocked-by-other-PR ??? blocked on another PR
11617 urkud refactor(Finset): redefine Finset.diag, review API merge-conflict awaiting-author t-logic ??? missing CI information
12192 Ruben-VandeVelde feat: generalize isLittleO_const_id_atTop/atBot merge-conflict awaiting-author t-analysis ??? missing CI information
10024 ADedecker feat: rename `connectedComponentOfOne` to `identityComponent`, prove that it is normal and open merge-conflict t-topology awaiting-CI ??? does not pass CI
10521 eric-wieser chore: generalize `IsBoundedLinearMap` to modules merge-conflict awaiting-author t-analysis ??? missing CI information
10594 lecopivo feat: `fun_trans` function transformation tactic e.g. for computing derivatives merge-conflict WIP 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 merge-conflict WIP blocked-by-other-PR ??? blocked on another PR
11100 eric-wieser feat(CategoryTheory/Limits): add `Functor.mapBinaryBiconeInv` merge-conflict t-category-theory awaiting-CI ??? does not pass CI
8503 thorimur feat: meta utils for `refine?` merge-conflict awaiting-author t-meta ??? missing CI information
8519 eric-wieser refactor(LinearAlgebra/TensorProduct): golf using `liftAddHom` merge-conflict awaiting-author t-algebra ??? missing CI information
8616 eric-wieser feat(Algebra/FreeAlgebra): add right action and `IsCentralScalar` merge-conflict t-algebra awaiting-CI ??? does not pass CI
8658 eric-wieser feat: support right actions for `Con` merge-conflict awaiting-author t-algebra ??? missing CI information
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 ??? missing CI information
8906 jjaassoonn feat: add some missing lemmas about linear algebra merge-conflict awaiting-author t-algebra ??? missing CI information
8961 eric-wieser refactor: use the coinduced topology on ULift please-adopt merge-conflict awaiting-author awaiting-CI ??? looking for help
9146 laughinggas feat(Data/ZMod/Defs): Topological structure on `ZMod` merge-conflict t-algebra awaiting-author t-topology ??? missing CI information
9229 eric-wieser refactor(Algebra/GradedMonoid): Use `HMul` to define `GMul` merge-conflict WIP t-algebra ??? labelled WIP
9354 chenyili0818 feat: monotonicity of gradient on convex real-valued functions merge-conflict awaiting-author t-analysis ??? missing CI information
9356 alexjbest feat: assumption? merge-conflict awaiting-author t-meta ??? missing CI information
9469 dupuisf feat: maximum modulus principle for functions vanishing at infinity awaiting-author t-analysis ??? missing CI information
9487 eric-wieser feat: the exponential of dual numbers over non-commutative rings WIP t-algebra t-measure-probability merge-conflict t-analysis ??? labelled WIP
9510 eric-wieser feat(Analysis/Calculus/DualNumber): Extending differentiable functions to dual numbers WIP t-algebra t-analysis awaiting-CI ??? labelled WIP
9570 eric-wieser feat(Algebra/Star): Non-commutative generalization of `StarModule` merge-conflict WIP t-algebra awaiting-CI ??? labelled WIP
9642 eric-wieser refactor(Analysis/Normed/{Group/Field}/Basic): Let `extends` generate the repeated fields WIP merge-conflict awaiting-author help-wanted t-analysis ??? looking for help
6580 adomani chore: `move_add`-driven replacements merge-conflict awaiting-author ??? missing CI information
6630 MohanadAhmed feat: Reduced Spectral Theorem merge-conflict WIP t-algebra ??? labelled WIP
6777 adomani chore(Co*variantClass): replace eta-expanded (· * ·), (· + ·), (· ≤ ·), (· < ·) merge-conflict ??? missing CI information
6791 eric-wieser refactor: Use flat structures for morphisms merge-conflict awaiting-author help-wanted awaiting-CI ??? looking for help
6930 kmill feat: `resynth_instances` tactic for resynthesizing instances in the goal or local context merge-conflict WIP t-meta ??? labelled WIP
6931 urkud refactor(Analysis/Normed*): use `RingHomIsometric` for `*.norm_cast` merge-conflict help-wanted t-analysis ??? looking for help
7227 kmill feat: flexible binders and integration into notation3 merge-conflict WIP t-meta ??? labelled WIP
7351 shuxuezhuyi feat(Topology/Algebra/Order): extend function on `Ioo` to `Icc` merge-conflict awaiting-author t-order ??? missing CI information
7467 ADedecker feat: spectrum of X →ᵇ ℂ is StoneCech X merge-conflict WIP t-analysis ??? labelled WIP
7564 shuxuezhuyi feat(Topology/Algebra/Order): extend strictly monotone function on `Ioo` to homeomorphism on `Icc` merge-conflict t-topology blocked-by-other-PR ??? blocked on another PR
7601 digama0 feat: ring hom support in `ring` merge-conflict awaiting-author t-algebra t-meta ??? missing CI information
7615 eric-wieser chore(LinearAlgebra/Basic): generalize compatibleMaps to semilinear maps merge-conflict t-algebra easy awaiting-CI ??? does not pass CI
7713 RemyDegenne feat: add_left/right_inj for measures merge-conflict awaiting-author t-measure-probability ??? missing CI information
7835 shuxuezhuyi feat(LinearAlgebra/Matrix): `lift` for projective special linear group merge-conflict awaiting-author t-algebra ??? missing CI information
7875 astrainfinita chore: make `SMulCommClass A A B` and `SMulCommClass A B B` higher priority merge-conflict slow-typeclass-synthesis t-algebra ??? missing CI information
7909 mcdoll fix(Tactic/Continuity): remove npowRec and add new tag for Continuous.pow merge-conflict WIP t-topology t-meta ??? labelled WIP
7932 eric-wieser refactor(Algebra/TrivSqZeroExt): replace with a structure merge-conflict t-algebra awaiting-CI ??? does not pass CI
7962 eric-wieser feat: `DualNumber (Quaternion R)` as a `CliffordAlgebra` merge-conflict WIP t-algebra ??? labelled WIP
8364 thorimur feat: `refine?` merge-conflict blocked-by-other-PR t-meta ??? blocked on another PR
4871 j-loreaux feat: define the additive submonoid of positive elements in a star ordered ring merge-conflict t-algebra awaiting-CI ??? does not pass CI
5133 kmill feat: IntermediateField adjoin syntax for sets of elements merge-conflict WIP t-algebra ??? labelled WIP
5912 ADedecker feat(Analysis.Distribution.ContDiffMapSupportedIn): space of smooth maps with support in a fixed compact merge-conflict WIP t-analysis ??? labelled WIP
6002 slerpyyy feat(Analysis.SpecialFunctions.Gaussian): add `integrable_fun_mul_exp_neg_mul_sq` merge-conflict awaiting-author t-analysis ??? missing CI information
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 t-algebra awaiting-CI ??? does not pass CI
6210 MohanadAhmed feat(Data/IsROrC/Basic): add a `StarOrderedRing` instance merge-conflict WIP t-algebra t-analysis ??? labelled WIP
6328 astrainfinita chore: make some instance about `Sub...Class` lower priority merge-conflict WIP t-algebra awaiting-CI ??? labelled WIP
6330 astrainfinita chore: make some instance about `Sub...Class` higher priority than `Sub...` merge-conflict WIP t-algebra slow-typeclass-synthesis ??? labelled WIP
6403 astrainfinita chore: change instance priorities of `Ordered*` hierarchy t-algebra t-order merge-conflict slow-typeclass-synthesis awaiting-author ??? missing CI information
6491 eric-wieser chore(Mathlib/Algebra/Hom/GroupAction): add `SMulHomClass.comp_smul` merge-conflict t-algebra ??? missing CI information
7076 grunweg feat: define measure zero subsets of a manifold merge-conflict WIP t-differential-geometry t-measure-probability ??? labelled WIP
3757 thorimur feat: config options for `fail_if_no_progress` merge-conflict WIP t-meta ??? labelled WIP
12353 thorimur feat: `conv%` merge-conflict WIP t-meta ??? labelled WIP
7903 urkud feat: define `UnboundedSpace` merge-conflict help-wanted t-topology ??? looking for help
15400 grunweg feat: "confusing variables" linter merge-conflict WIP t-linter ??? labelled WIP
15679 adomani test: refactor in CI merge-conflict WIP ??? labelled WIP
7565 shuxuezhuyi feat(Topology/Algebra/Order): extend homeomorphism of `Ioo` to `Icc` merge-conflict t-topology blocked-by-other-PR t-order ??? blocked on another PR
10629 madvorak feat: List.cons_sublist_append_iff_right merge-conflict t-data ??? missing CI information
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 merge-conflict WIP t-category-theory ??? labelled WIP
12869 adomani feat: linter and script for `theorem` vs `lemma` merge-conflict t-linter awaiting-author ??? missing CI information
14563 awueth feat: if-then-else of exclusive or statement awaiting-author t-algebra new-contributor ??? missing CI information
12093 ADedecker feat: tweak the definition of semicontinuity to behave better in nonlinear orders merge-conflict WIP t-topology ??? labelled WIP
11393 mcdoll feat(Analysis/Distribution/SchwartzSpace): The Heine-Borel property merge-conflict WIP t-analysis ??? labelled WIP
9444 erdOne feat: Various instances regarding `𝓞 K`. merge-conflict help-wanted t-number-theory ??? looking for help
8931 hmonroe feat(Computable): define P, NP, and NP-complete merge-conflict t-computability awaiting-author ??? missing CI information
10387 adomani feat(Tactic/ComputeDegree): add `polynomial` tactic WIP RFC t-meta ??? labelled WIP
8608 eric-wieser feat: multiplicativize `AddTorsor` merge-conflict WIP t-algebra ??? labelled WIP
9154 astrainfinita feat: `npow` / `nsmul` / `Nat.cast`/ `zpow` / `zsmul` implemented using `Nat.binaryRec` merge-conflict awaiting-author t-algebra blocked-by-other-PR ??? blocked on another PR
6603 tydeu feat: automatically try `cache get` before build merge-conflict WIP CI ??? labelled WIP
6058 apurvnakade feat: duality theory for cone programs merge-conflict WIP t-analysis ??? labelled WIP
6449 ADedecker feat: functions with finite fibers merge-conflict awaiting-author t-topology ??? missing CI information
13163 erdOne feat(.vscode/module-docstring.code-snippet): Prevent auto-complete from firing on `do` awaiting-author t-meta ??? missing CI information
13791 digama0 refactor: Primrec and Partrec merge-conflict t-computability tech debt ??? missing CI information
11964 adamtopaz feat: The functor of points of a scheme merge-conflict t-algebraic-geometry t-category-theory ??? missing CI information
12418 rosborn style: replace preimage_val with ↓∩ notation merge-conflict ??? missing CI information
9978 astrainfinita chore(FieldTheory/KummerExtension): move some lemmas earlier merge-conflict awaiting-author t-algebra ??? missing CI information
12429 adomani feat: toND -- auto-generating natDegree t-algebra RFC merge-conflict awaiting-author t-meta ??? missing CI information
12751 Command-Master feat: add lemmas for Nat/Bits, Nat/Bitwise and Nat/Size merge-conflict t-data new-contributor ??? missing CI information
15448 urkud chore(*): deprecate `Option.elim'` merge-conflict awaiting-author 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 merge-conflict awaiting-author t-algebra ??? missing CI information
6517 MohanadAhmed feat: discrete Fourier transform of a finite sequence merge-conflict awaiting-author t-algebra ??? missing CI information
13155 alreadydone feat(NumberTheory/EllipticDivisibilitySequence): show elliptic relations follow from even-odd recursion merge-conflict t-algebra awaiting-author t-number-theory ??? missing CI information
15600 adomani feat: lint also `let` vs `have` merge-conflict WIP 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 ??? missing CI information
15895 madvorak feat(Computability/ContextFreeGrammar): mapping between two types of nonterminal symbols t-computability WIP ??? labelled WIP
14038 adomani test/decl diff in lean dev merge-conflict WIP ??? labelled WIP
7861 shuxuezhuyi feat(Geometry/Hyperbolic/UpperHalfPlane): instance IsometricSMul PSL(2, ℝ) ℍ merge-conflict blocked-by-other-PR 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 t-topology awaiting-author t-algebra ??? missing CI information
7545 shuxuezhuyi feat: APIs of `Function.extend f g e'` when `f` is injective merge-conflict awaiting-author t-logic ??? missing CI information
14078 Ruben-VandeVelde feat(CI): continue after mk_all fails merge-conflict awaiting-author CI ??? missing CI information
11283 hmonroe feat(ModelTheory/Satisfiability): define theory with independent sentence merge-conflict WIP t-logic ??? labelled WIP
16914 siddhartha-gadgil Loogle syntax with non-reserved merge-conflict WIP ??? labelled WIP
13782 alreadydone feat(EllipticCurve): ZSMul formula in terms of division polynomials t-algebra t-number-theory blocked-by-other-PR merge-conflict t-algebraic-geometry ??? blocked on another PR
8118 iwilare feat(CategoryTheory): add dinatural transformations merge-conflict awaiting-author t-category-theory ??? missing CI information
14242 js2357 feat: Prove equivalence of `isDedekindDomain` and `isDedekindDomainDvr` merge-conflict t-algebra blocked-by-other-PR new-contributor ??? blocked on another PR
7516 ADedecker perf: use `abbrev` to prevent unifying useless data merge-conflict WIP ??? labelled WIP
16215 adomasbaliuka feat(Tactic/Linter): lint unwanted unicode merge-conflict t-linter blocked-by-other-PR ??? blocked on another PR
17127 astrainfinita chore: remove global `Quotient.mk` `⟦·⟧` notation merge-conflict t-data ??? missing CI information
16887 metinersin feat(ModelTheory/Complexity): define conjunctive and disjunctive formulas merge-conflict blocked-by-other-PR new-contributor t-logic ??? blocked on another PR
16888 metinersin feat(ModelTheory/Complexity): Define conjunctive and disjunctive normal forms merge-conflict blocked-by-other-PR new-contributor t-logic ??? blocked on another PR
16889 metinersin feat(ModelTheory/Complexity): Normal forms merge-conflict blocked-by-other-PR new-contributor t-logic ??? blocked on another PR
14712 astrainfinita perf: change instance priority and order about `OfNat` merge-conflict slow-typeclass-synthesis t-algebra delegated ??? missing CI information
11500 mcdoll refactor(Topology/Algebra/Module/WeakDual): Clean up merge-conflict awaiting-author t-topology ??? missing CI information
5995 astrainfinita feat: add APIs about `Quotient.choice` merge-conflict awaiting-author RFC t-data ??? missing CI information
8029 alreadydone refactor: Homotopy between Functions not ContinuousMaps merge-conflict t-topology RFC ??? missing CI information
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` merge-conflict awaiting-author t-topology t-order ??? missing CI information
13965 pechersky feat(Data/DigitExpansion): reals via digit expansion are complete merge-conflict blocked-by-other-PR t-data ??? blocked on another PR
17519 grunweg feat: the `metrisableSpace` linter merge-conflict t-linter blocked-by-other-PR ??? 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 t-data new-contributor merge-conflict awaiting-author ??? 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 merge-conflict WIP t-set-theory ??? labelled WIP
9605 davikrehalt feat(Data/Finset & List): Add Lemmas for Sorting and Filtering please-adopt t-data new-contributor merge-conflict awaiting-author ??? looking for help
13514 madvorak feat(Computability/ContextFreeGrammar): closure under union merge-conflict t-computability blocked-by-other-PR ??? blocked on another PR
17518 grunweg feat: lint on declarations mentioning `Invertible` or `Unique` merge-conflict t-linter blocked-by-other-PR awaiting-zulip blocked on another PR
9654 urkud feat: add `@[mk_eq]` version of `@[mk_iff]` merge-conflict awaiting-author t-meta ??? missing CI information
16704 AntoineChambert-Loir feat(Mathlib.Data.Ordering.Dickson): Dickson orders merge-conflict WIP t-order ??? labelled WIP
16355 Ruben-VandeVelde feat: odd_{add,sub}_one merge-conflict t-algebra awaiting-author t-number-theory ??? missing CI information
8479 alexjbest feat: use leaff in CI merge-conflict WIP awaiting-author ??? ⚠️ 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 ??? missing CI information
16885 metinersin feat(ModelTheory/Complexity): define literals merge-conflict awaiting-author new-contributor t-logic ??? missing CI information
18716 jjaassoonn feat(Algebra/Module/GradedModule): quotient and subgrading WIP t-algebra blocked-by-other-PR awaiting-CI merge-conflict blocked on another PR
9341 winstonyin feat: Naturality of integral curves merge-conflict awaiting-author t-differential-geometry ??? missing CI information
13248 hcWang942 feat: basic concepts of auction theory merge-conflict awaiting-author new-contributor t-logic ??? missing CI information
9344 erdOne feat: Add `AddGroup.FG` -> `Module.Finite ℤ` as instances merge-conflict awaiting-author t-algebra ??? missing CI information
12133 ADedecker feat: generalize instIsLowerProd to arbitrary products merge-conflict awaiting-author t-topology t-order ??? missing CI information
16637 astrainfinita perf: reorder `extends` of `(Add)Monoid` merge-conflict WIP t-algebra labelled WIP
14739 urkud feat(Measure): add `gcongr` lemmas WIP t-measure-probability merge-conflict awaiting-author help-wanted ??? looking for help
8661 joelriou feat(CategoryTheory/Sites): descent of sheaves merge-conflict WIP t-category-theory ??? labelled WIP
10476 shuxuezhuyi feat(Topology/UniformSpace): define uniform preordered space merge-conflict awaiting-author t-topology ??? missing CI information
17593 astrainfinita chore(Algebra/Order/GroupWithZero/Unbundled): deprecate useless lemmas, use `ZeroLEOneClass` merge-conflict t-algebra blocked-by-other-PR t-order ??? blocked on another PR
17623 astrainfinita feat(Algebra/Order/GroupWithZero/Unbundled): add some lemmas merge-conflict t-algebra awaiting-zulip t-order ??? missing CI information
17624 astrainfinita feat(Algebra/Order/GroupWithZero/Unbundled): generalize lemmas merge-conflict t-algebra blocked-by-other-PR t-order ??? blocked on another PR
17513 astrainfinita perf: do not search algebraic hierarchies when using `map_*` lemmas merge-conflict WIP t-algebra awaiting-bench ??? labelled WIP
17515 astrainfinita perf: do not need `simp low` now merge-conflict t-algebra blocked-by-other-PR blocked on another PR
19212 Julian feat(LinearAlgebra): add a variable_alias for VectorSpace merge-conflict t-algebra ??? missing CI information
19337 zeramorphic feat(Data/Finsupp): generalise `Finsupp` to any "zero" value merge-conflict t-data ??? missing CI information
10332 adri326 feat(Topology/Sets): define regular open sets and their boolean algebra merge-conflict WIP t-topology ??? labelled WIP
14501 jjaassoonn feat: module structure of filtered colimit of abelian groups over filtered colimit of rings t-algebra workshop-AIM-AG-2024 t-category-theory merge-conflict awaiting-author ??? missing CI information
18756 astrainfinita refactor: deprecate `DistribMulActionSemiHomClass` `MulSemiringActionSemiHomClass` merge-conflict t-algebra ??? missing CI information
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 merge-conflict WIP ??? labelled WIP
11142 hmonroe feat(ProofTheory): Define logical symbols abstractly; opens new top-level section, drawing from lean4-logic merge-conflict awaiting-author t-logic ??? missing CI information
11210 hmonroe Test commit merge-conflict WIP ??? labelled WIP
19621 Command-Master feat: Multiplicity and prime-adic valuation of derivations merge-conflict t-algebra blocked-by-other-PR large-import ??? blocked on another PR
18262 joelriou feat(Algebra/Category/ModuleCat/Presheaf): exterior powers of presheaves of modules WIP t-algebra blocked-by-other-PR t-category-theory merge-conflict blocked on another PR
15269 kkytola feat: Add ENNReal.floor t-algebra blocked-by-other-PR t-order merge-conflict awaiting-author ??? blocked on another PR
15773 kkytola feat: Add type class for ENat-valued floor functions merge-conflict awaiting-author t-order ??? missing CI information
3251 kmill feat: deriving `LinearOrder` for simple enough inductive types merge-conflict WIP awaiting-author t-meta ??? labelled WIP
3610 TimothyGu feat: derive Infinite automatically for inductive types merge-conflict awaiting-author t-meta ??? missing CI information
16120 awainverse feat(ModelTheory/Algebra/Ring/Basic): Ring homomorphisms are a `StrongHomClass` for the language of rings merge-conflict t-algebra RFC t-logic ??? missing CI information
20459 Ruben-VandeVelde chore: fix names of roots_C_mul_X_{add,sub}_C_of_IsUnit awaiting-author t-algebra ??? missing CI information
19462 joelriou feat(AlgebraicGeometry): étale sheafification merge-conflict WIP t-algebraic-geometry blocked-by-other-PR blocked on another PR
20527 trivial1711 refactor(Topology/UniformSpace/Completion): more descriptive names for `α → Completion α` merge-conflict t-topology ??? missing CI information
17739 Aaron1011 feat(Topology/Order/DenselyOrdered): prove Not (IsOpen) for intervals merge-conflict awaiting-author t-topology new-contributor ??? missing CI information
18474 astrainfinita perf: lower the priority of `*WithOne.to*` instances merge-conflict slow-typeclass-synthesis t-algebra t-data ??? missing CI information
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 merge-conflict awaiting-author t-combinatorics new-contributor ??? missing CI information
15720 znssong feat(SimpleGraph): The Bondy-Chvátal theorem merge-conflict blocked-by-other-PR t-combinatorics new-contributor ??? blocked on another PR
18629 tomaz1502 feat(Computability.Timed): Formalization of runtime complexity of List.merge merge-conflict t-computability awaiting-author new-contributor ??? missing CI information
8362 urkud feat(Asymptotics): define `ReflectsGrowth` merge-conflict awaiting-author t-analysis ??? missing CI information
6692 prakol16 feat: disjoint indexed union of local homeomorphisms merge-conflict awaiting-author t-topology ??? missing CI information
18461 hannahfechtner feat: left and right common multiples mixins awaiting-author t-algebra new-contributor ??? missing CI information
19291 PieterCuijpers feat(Algebra/Order/Hom): add quantale homomorphism merge-conflict awaiting-author t-algebra new-contributor failing CI
19352 hrmacbeth chore: change some `nlinarith`s to `linear_combination`s merge-conflict WIP ??? labelled WIP
20372 jvlmdr feat(MeasureTheory/Function): Add ContinuousLinearMap.bilinearCompLp(L) merge-conflict t-measure-probability new-contributor ??? missing CI information
20872 grunweg feat: lint against the tactic.skipAssignedInstances option in mathlib merge-conflict t-linter awaiting-author tech debt ??? missing CI information
2605 eric-wieser chore: better error message in linarith merge-conflict awaiting-author t-meta ??? missing CI information
11837 trivial1711 feat: completion of a uniform multiplicative group WIP t-algebra merge-conflict help-wanted t-topology looking for help
12670 trivial1711 feat: completion of a nonarchimedean multiplicative group merge-conflict t-algebra t-topology blocked-by-other-PR blocked on another PR
9449 hmonroe feat: Add Turing machine with the quintet definition (TMQ) and a chainable step function for each TM type merge-conflict t-computability awaiting-author ??? missing CI information
19697 quangvdao feat(BigOperators/Fin): Sum/product over `Fin` intervals merge-conflict awaiting-author t-data failing CI
19353 hrmacbeth chore: golf some term/rw proofs using `linear_combination` merge-conflict WIP ??? labelled WIP
20248 peabrainiac feat(Topology/Compactness): first-countable locally path-connected spaces are delta-generated blocked-by-other-PR large-import new-contributor merge-conflict awaiting-author t-topology ??? blocked on another PR
10678 adri326 feat(Topology/UniformSpace): prove that a uniform space is completely regular merge-conflict awaiting-author t-topology ??? missing CI information
18785 erdOne feat(CategoryTheory): command that generates instances for `MorphismProperty` merge-conflict awaiting-author t-category-theory t-meta ??? missing CI information
15942 grunweg chore: move style linters into their own file; document all current linters merge-conflict t-linter awaiting-author ??? missing CI information
16311 madvorak feat(Computability): regular languages are context-free merge-conflict WIP t-computability labelled WIP
19943 AlexLoitzl feat(Computability): Add Chomsky Normal Form Grammar and translation merge-conflict t-computability awaiting-author new-contributor ??? missing CI information
17005 YnirPaz feat(SetTheory/Cardinal/Regular): define singular cardinals merge-conflict WIP t-set-theory ??? labelled WIP
21501 sksgurdldi feat(List): add sum_zipWith_eq_finset_sum awaiting-author t-algebra new-contributor ??? missing CI information
12054 adomani feat: auto-bugs merge-conflict awaiting-author t-meta ??? missing CI information
5062 adomani feat(Tactic/Prune + test/Prune): add `prune` tactic, for removing unnecessary hypotheses merge-conflict modifies-tactic-syntax awaiting-author t-meta ??? missing CI information
21433 grunweg chore: change more lemmas to be about enorm instead of nnnorm merge-conflict awaiting-author carleson t-measure-probability ??? missing CI information
20454 urkud chore(TangentCone): review names merge-conflict t-analysis failing CI
16550 awainverse feat(ModelTheory): A typeclass for languages expanding other languages merge-conflict awaiting-author t-logic ??? missing CI information
13686 fpvandoorn feat: some finset lemmas merge-conflict awaiting-author t-data ??? missing CI information
14313 grhkm21 feat(RepresentationTheory/FdRep): FdRep is a full subcategory of Rep merge-conflict t-algebra t-category-theory new-contributor failing CI
10823 alexkeizer feat: convert curried type functions into uncurried type functions merge-conflict awaiting-author t-data ??? missing CI information
13648 urkud feat(Topology/Module): generalize `ContinuousLinearMap.compSL` t-algebra merge-conflict awaiting-author t-topology t-analysis failing CI
14060 YnirPaz feat(SetTheory/Ordinal/Clubs): define club sets and prove basic properties merge-conflict blocked-by-other-PR new-contributor t-logic ??? blocked on another PR
20636 eric-wieser feat: multiplication of intervals in rings awaiting-author t-algebra ??? missing CI information
16000 YaelDillies feat: Croot-Sisask Almost Periodicity t-combinatorics t-analysis blocked-by-other-PR ??? blocked on another PR
22340 sinhp feat(CategoryTheory): Locally Cartesian Closed Categories (Beck-Chevalley Conditions) WIP blocked-by-other-PR t-category-theory large-import merge-conflict ??? blocked on another PR
21959 BGuillemet feat(Topology/ContinuousMap): Stone-Weierstrass theorem for MvPolynomial merge-conflict t-topology new-contributor ??? missing CI information
18470 astrainfinita perf: lower the priority of `Normed*.to*` instances merge-conflict slow-typeclass-synthesis t-algebra t-analysis ??? missing CI information
22784 grunweg feat: add Diffeomorph.sumSumSumComm WIP t-differential-geometry labelled WIP
16944 YnirPaz feat(SetTheory/Cardinal/Cofinality): lemmas about limit ordinals and cofinality merge-conflict WIP 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 ??? missing CI information
15578 znssong feat(Function): Fixed points of function `f` with `f(x) >= x` merge-conflict awaiting-author t-analysis new-contributor ??? missing CI information
22660 Ruben-VandeVelde chore: follow naming convention around Group.IsNilpotent merge-conflict t-algebra ??? missing CI information
13999 adomani feat: a linter to flag potential confusing conventions merge-conflict t-linter awaiting-author ??? missing CI information
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` merge-conflict awaiting-author t-algebra ??? missing CI information
19189 YnirPaz feat(SetTheory/Ordinal/Arithmetic): order isomorphism between omega and the natural numbers merge-conflict awaiting-author t-set-theory ??? missing CI information
23142 joneugster feat(CategoryTheory/Enriched/Limits): add API for HasConicalLimit awaiting-author t-category-theory infinity-cosmos ??? missing CI information
23145 joneugster feat(CategoryTheory/Enriched/Limits): add IsConicalLimits merge-conflict blocked-by-other-PR t-category-theory infinity-cosmos blocked on another PR
19227 adomani fix(CI): unwrap `lake test` in problem matcher merge-conflict awaiting-author CI ??? missing CI information
20874 grunweg chore(nolint.yml): use shallow clones merge-conflict awaiting-author CI ??? missing CI information
15774 kkytola feat: Topology on `ENat` merge-conflict WIP t-topology t-order ??? labelled WIP
20613 grunweg chore: golf using `List.toArrayMap` merge-conflict large-import failing CI
20222 eric-wieser feat: generalize lemmas about derivatives merge-conflict blocked-by-other-PR t-analysis blocked on another PR
22682 grunweg chore(Topology/Homeomorph): split out various constructions merge-conflict tech debt t-topology RFC failing CI
21018 markimunro feat(Data/Matrix): add file with key definitions and theorems about elementary row operations t-data enhancement new-contributor merge-conflict awaiting-author 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 merge-conflict WIP t-topology t-analysis ??? labelled WIP
13124 astrainfinita chore: remove `CovariantClass` and `ContravariantClass` merge-conflict WIP labelled WIP
20401 RemyDegenne feat: add sigmaFinite_iUnion merge-conflict awaiting-author t-measure-probability ??? missing CI information
19275 eric-wieser fix: if nolint files change, do a full rebuild merge-conflict delegated failing CI
22727 grunweg feat: rewrite the isolated by and colon linters in Lean merge-conflict t-linter awaiting-author ??? missing CI information
15212 victorliu5296 feat: Add fundamental theorem of calculus-2 for Banach spaces t-measure-probability new-contributor merge-conflict awaiting-author t-analysis ??? missing CI information
22888 plp127 perf: replace `Lean.Expr.swapBVars` with a better? implementation awaiting-author t-meta ??? missing CI information
22579 kvanvels doc(Topology/Defs/Induced): fix comments on three functions related to RestrictGenTopology merge-conflict t-topology documentation awaiting-author ??? missing CI information
21488 imbrem feat(CategoryTheory/Monoidal): premonoidal categories merge-conflict t-category-theory new-contributor ??? missing CI information
21525 sinhp feat(CategoryTheory): Locally Cartesian Closed Categories (Prelim) merge-conflict t-category-theory large-import ??? missing CI information
22319 sinhp feat(CategoryTheory): Locally Cartesian Closed Categories (Sections Right Adjoint) merge-conflict blocked-by-other-PR t-category-theory large-import ??? blocked on another PR
22321 sinhp feat(CategoryTheory): Locally Cartesian Closed Categories (Definition) merge-conflict blocked-by-other-PR t-category-theory large-import ??? blocked on another PR
19425 hrmacbeth perf: gcongr forward-reasoning adjustment merge-conflict awaiting-author ??? missing CI information
20873 vbeffara feat(Topology/Covering): path lifting and homotopy lifting merge-conflict awaiting-author t-topology new-contributor failing CI
22817 peabrainiac feat(CategoryTheory/Sites): local sites merge-conflict WIP t-category-theory ??? labelled WIP
6252 michaellee94 feat(Geometry/Manifolds/Instances/Homeomorph): Homeomorphism maps `C^k` manifolds to `C^k` manifolds merge-conflict WIP t-differential-geometry ??? labelled WIP
16314 astrainfinita chore(Data/Quot): deprecate `ind*'` APIs merge-conflict t-data ??? missing CI information
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 merge-conflict awaiting-author ??? missing CI information
7325 eric-wieser chore: use preimageIso instead of defeq abuse for InducedCategory merge-conflict t-category-theory awaiting-CI ??? does not pass CI
7874 astrainfinita chore: make `IsScalarTower A A B` and `IsScalarTower A B B` higher priority merge-conflict slow-typeclass-synthesis t-algebra awaiting-CI ??? does not pass CI
13038 adomani feat: Mathlib weekly reports awaiting-author CI t-meta ??? missing CI information
5952 eric-wieser feat: add Qq wrappers for ToExpr merge-conflict awaiting-CI t-meta ??? does not pass CI
15483 astrainfinita chore(GroupTheory/Coset): reduce defeq abuse merge-conflict t-algebra ??? missing CI information
16594 astrainfinita perf: reorder `extends` and remove some instances in algebra hierarchy merge-conflict slow-typeclass-synthesis t-algebra ??? missing CI information
21238 joneugster feat(Cache): enable partial cache in downstream projects merge-conflict blocked-by-other-PR CI t-meta ??? blocked on another PR
21842 joneugster refactor(Cache): use module name for file hash instead of non-resolved file path merge-conflict blocked-by-other-PR CI t-meta ??? blocked on another PR
19467 quangvdao feat(MvPolynomial/Equiv): Add `MvPolynomial.finSuccEquivNth` merge-conflict t-algebra blocked-by-other-PR ??? blocked on another PR
20567 grunweg feat(Cache): two small features merge-conflict t-meta ??? missing CI information
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 merge-conflict awaiting-author t-algebra new-contributor failing CI
19117 eric-wieser feat: derivatives of matrix operations merge-conflict WIP t-analysis labelled WIP
12605 astrainfinita chore: attribute [induction_eliminator] merge-conflict awaiting-author ??? missing CI information
15099 joelriou feat(CategoryTheory/Sites): the Mayer-Vietoris long exact sequence in sheaf cohomology merge-conflict WIP t-category-theory labelled WIP
23859 urkud feat(Topology/../Order/Field): generalize to `Semifield` merge-conflict t-topology ??? missing CI information
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 ??? missing CI information
24285 madvorak chore(Algebra/*-{Category,Homology}): remove unnecessary universe variables merge-conflict t-algebra ??? missing CI information
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 merge-conflict awaiting-author t-algebra failing CI
23593 erdOne feat(AlgebraicGeometry): the tilde construction is functorial merge-conflict awaiting-author t-algebraic-geometry ??? missing CI information
21065 eric-wieser feat: generalize `tangentConeAt.lim_zero` to TVS merge-conflict WIP t-analysis ??? labelled WIP
22721 grunweg chore(MeasureTheory/Function/LpSeminorm/Basic): generalise more results to enorm classes merge-conflict WIP carleson t-measure-probability labelled WIP
24354 grunweg chore(HasFiniteIntegral): rename three lemmas merge-conflict t-measure-probability ??? missing CI information
14731 adomani feat: the repeated typeclass assumption linter merge-conflict WIP t-linter large-import labelled WIP
13649 astrainfinita chore: redefine `Nat.div2` `Nat.bodd` merge-conflict ??? missing CI information
18861 YaelDillies refactor: make `Set.mem_graphOn` defeq awaiting-author t-data failing CI
24549 grunweg feat: define embedded submanifolds, attempt 1 merge-conflict WIP t-differential-geometry blocked-by-other-PR blocked on another PR
22809 b-reinke feat: Category algebras and path algebras WIP t-algebra t-category-theory new-contributor labelled WIP
14675 adomani dev: the repeated variable linter merge-conflict WIP t-linter ??? labelled WIP
14330 Ruben-VandeVelde chore: split Mathlib.Algebra.Star.Basic merge-conflict awaiting-author ??? missing CI information
8511 eric-wieser refactor(MeasureTheory/Measure/Haar/Basic): partially generalize to the affine case merge-conflict awaiting-author t-measure-probability ??? missing CI information
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 merge-conflict WIP t-data ??? labelled WIP
11524 mcdoll refactor: Introduce type-class for SchwartzMap merge-conflict WIP t-analysis ??? labelled WIP
11003 thorimur chore: migrate to `tfae` block tactic merge-conflict WIP blocked-by-other-PR t-meta ??? blocked on another PR
16186 joneugster chore: use emoji-variant-selector `\uFE0F` for emojis ✅️,❌️,💥️,🟡️ merge-conflict t-linter awaiting-author blocked-by-other-PR ??? blocked on another PR
22488 smmercuri fix: lower priority for `UniformSpace.Completion.instSMul` awaiting-author t-topology FLT ??? missing CI information
23546 JovanGerb feat(LinearAlgebra/AffineSpace/AffineSubspace): rename `AffineSubspace.mk'` to `Submodule.shift` merge-conflict t-euclidean-geometry ??? missing CI information
15654 TpmKranz feat(Computability): language-preserving maps between NFA and RE blocked-by-other-PR new-contributor t-computability merge-conflict awaiting-zulip ??? blocked on another PR
19315 quangvdao feat(Data/Finsupp/Fin): Add `Finsupp` operations on `Fin` tuple merge-conflict awaiting-author t-data ??? missing CI information
7907 urkud feat: introduce `NthRoot` notation class merge-conflict t-algebra t-analysis awaiting-CI does not pass CI
24155 eric-wieser feat: add a "rw_proc" for fin vectors awaiting-author RFC t-data t-meta ??? missing CI information
24550 grunweg feat: define `SliceModel` typeclass for models with corners for embedded submanifolds merge-conflict WIP t-differential-geometry blocked-by-other-PR blocked on another PR
21276 GabinKolly feat(ModelTheory/Substructures): define equivalences between equal substructures awaiting-author t-logic ??? missing CI information
24008 meithecatte chore(EpsilonNFA): replace manual lemmas with @[simps] t-computability awaiting-author new-contributor ??? missing CI information
24642 grunweg WIP-feat: add layercake formula for ENNReal-valued functions merge-conflict WIP carleson t-analysis labelled WIP
21712 grunweg chore: generalise more lemmas to `ContinuousENorm` merge-conflict carleson awaiting-CI t-measure-probability does not pass CI
21375 grunweg WIP: generalise lemmas to ENorm WIP awaiting-CI t-measure-probability carleson merge-conflict 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 t-order merge-conflict help-wanted awaiting-author t-topology ??? 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 t-linter large-import merge-conflict awaiting-author delegated failing CI
17131 joneugster feat(Tactic/Linter): add unicode linter for unwanted characters merge-conflict t-linter awaiting-author large-import ??? missing CI information
22837 joneugster feat(Data/Set/Basic): add subset_iff and not_mem_subset_iff merge-conflict t-set-theory t-data ??? missing CI information
24100 eric-wieser feat: restore some explicit binders from Lean 3 merge-conflict awaiting-author tech debt ⚠️ failing CI
21476 grunweg feat(lint-style): enable running on downstream projects merge-conflict t-linter ??? missing CI information
23349 BGuillemet feat: add LocallyLipschitzOn.lipschitzOnWith_of_isCompact and two small lemmas about Lipschitz functions merge-conflict t-topology large-import new-contributor ??? missing CI information
12438 jjaassoonn feat: some APIs for flat modules merge-conflict WIP t-category-theory ??? labelled WIP
8740 digama0 fix: improve `recall` impl / error reporting merge-conflict awaiting-author awaiting-CI t-meta does not pass CI
21182 joneugster fix(Util/CountHeartbeats): move elaboration in #count_heartbeats inside a namespace merge-conflict t-meta ??? missing CI information
23371 grunweg chore: mark `Disjoint.{eq_bot, inter_eq}` simp merge-conflict awaiting-author t-order ??? missing CI information
25473 adomani feat(CI): check that Mathlib files have lean or md extension CI delegated ??? missing CI information
16020 adomani feat: compare PR `olean`s size with `master` merge-conflict CI failing CI
16062 adomani Test/ci olean size merge-conflict WIP awaiting-author CI ??? labelled WIP
12799 jstoobysmith feat(LinearAlgebra/UnitaryGroup): Add properties of Special Unitary Group please-adopt t-algebra new-contributor merge-conflict awaiting-author ??? 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 ??? missing CI information
23929 meithecatte feat(Computability/NFA): improve bound on pumping lemma t-computability awaiting-zulip new-contributor 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 merge-conflict WIP awaiting-author CI ??? labelled WIP
13483 adomani feat: automatically replace deprecations merge-conflict awaiting-author delegated t-meta failing CI
20334 miguelmarco feat: allow polyrith to use a local Singular/Sage install merge-conflict awaiting-author new-contributor t-meta ??? missing CI information
25912 BoltonBailey feat: add simp lemmas for trig functions on `π * 2⁻¹` awaiting-author blocked-by-other-PR t-analysis ??? blocked on another PR
23953 b-reinke feat(Data/Matroid/Tutte): define the Tutte polynomial of a matroid merge-conflict WIP t-data labelled WIP
25921 BoltonBailey feat: scripts to analyze overlap between namespaces WIP migrated-from-branch t-meta ??? labelled WIP
18771 joelriou feat(LinearAlgebra/ExteriorPower): exterior powers of free modules are free merge-conflict WIP t-algebra blocked-by-other-PR 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 ??? missing CI information
18439 ADedecker refactor: use new algebraic filter bases API in `FiniteAdeleRing` merge-conflict t-topology t-algebra ??? missing CI information
18438 ADedecker refactor: adapt `KrullTopology` to the new algebraic filter bases API merge-conflict t-topology t-algebra ??? missing CI information
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 ??? missing CI information
18662 joelriou feat(LinearAlgebra/ExteriorPower): generators of the exterior powers merge-conflict WIP t-algebra blocked-by-other-PR ??? blocked on another PR
18735 joelriou feat(Algebra/Module): presentation of the exterior power merge-conflict WIP t-algebra blocked-by-other-PR blocked on another PR
25993 Multramate feat(Algebra/Group/Units/Hom): add map lemmas awaiting-author t-algebra ??? missing CI information
16074 Rida-Hamadani feat: combinatorial maps and planar graphs merge-conflict t-combinatorics ??? missing CI information
16801 awainverse feat(ModelTheory/Equivalence): The quotient type of formulas modulo a theory merge-conflict awaiting-author t-logic ??? missing CI information
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 merge-conflict t-differential-geometry delegated ??? missing CI information
19444 joelriou feat(CategoryTheory/Sites): Equivalence of categories of sheaves with a dense subsite that is 1-hypercover dense merge-conflict WIP 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 ??? missing CI information
25218 kckennylau feat(AlgebraicGeometry): Tate normal form of elliptic curves merge-conflict t-algebraic-geometry awaiting-zulip new-contributor ??? missing CI information
25283 Brian-Nugent feat: regular local rings merge-conflict t-algebra new-contributor ??? missing CI information
25561 callesonne feat(Category/Grpd): define the bicategory of groupoids merge-conflict awaiting-author t-category-theory merge conflict
25988 Multramate refactor(AlgebraicGeometry/EllipticCurve/*): replace Fin 3 with products merge-conflict t-algebraic-geometry ??? missing CI information
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 merge-conflict WIP t-differential-geometry blocked-by-other-PR blocked on another PR
26465 joelriou feat(Algebra/Module): presentation of the `PiTensorProduct` merge-conflict file-removed t-algebra blocked-by-other-PR blocked on another PR
26467 joelriou feat(LinearAlgebra): the tensor product of a finite family of free modules is free WIP t-algebra blocked-by-other-PR merge-conflict 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 ??? missing CI information
26647 b-mehta feat(Data/Sym/Sym2): lift commutative operations to sym2 merge-conflict WIP t-data labelled WIP
26067 mapehe feat(Topology/StoneCech): exists_continuous_surjection_from_StoneCech_to_dense_range merge-conflict t-topology merge conflict
10541 xgenereux feat(Algebra/SkewMonoidAlgebra/Basic): add SkewMonoidAlgebra merge-conflict WIP 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 t-topology easy awaiting author
25710 Paul-Lez feat(Mathlib/Analysis/PDE/Quasilinear/Characteristics): the method of characteristics for first order quasilinear PDEs merge-conflict WIP t-analysis labelled WIP
26911 JovanGerb chore: fix naming of `mono` and `monotone` merge-conflict delegated merge conflict
21838 joneugster feat(Cache): Allow arguments of the form `Mathlib.Data` which correspond to a folder but not a file merge-conflict awaiting-author CI t-meta ??? missing CI information
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 merge-conflict awaiting-author t-algebra merge conflict
22749 joelriou feat(CategoryTheory/Abelian): the Gabriel-Popescu theorem as a localization with respect to a Serre class merge-conflict WIP t-category-theory labelled WIP
20428 madvorak feat(Data/Sign): lemmas about `∈ Set.range SignType.cast` merge-conflict WIP t-data labelled WIP
26987 joelriou chore: deprecating module LinearAlgebra.PiTensorProduct merge-conflict WIP t-algebra blocked-by-other-PR 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 merge-conflict t-algebra blocked-by-other-PR ??? blocked on another PR
13973 digama0 feat: lake exe refactor, initial framework merge-conflict awaiting-author t-meta ??? missing CI information
10190 jstoobysmith feat(AlgebraicTopology): add Augmented Simplex Category t-algebraic-topology WIP t-category-theory new-contributor merge-conflict ??? labelled WIP
20719 gio256 feat(AlgebraicTopology): delaborators for truncated simplicial notations merge-conflict t-algebraic-topology infinity-cosmos t-meta ??? missing CI information
25914 eric-wieser feat: add an ext lemma for the opposite category merge-conflict awaiting-author t-category-theory awaiting-CI 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 merge-conflict WIP t-algebra labelled WIP
24260 plp127 feat(Topology): add API for Hereditarily Lindelof spaces merge-conflict awaiting-author t-topology ??? missing CI information
27813 javra feat: IMO 2025 Q1 IMO WIP labelled WIP
27608 RemyDegenne feat(MeasureTheory): typeclasses for measures with finite moments merge-conflict WIP t-measure-probability labelled WIP
27826 xgenereux 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 ??? missing CI information
25985 Multramate feat(AlgebraicGeometry/EllipticCurve/Jacobian): add equivalences between points and explicit WithZero types merge-conflict t-algebraic-geometry ??? missing CI information
25984 Multramate feat(AlgebraicGeometry/EllipticCurve/Affine): add equivalences between points and explicit WithZero types merge-conflict t-algebraic-geometry ??? missing CI information
25982 Multramate feat(AlgebraicGeometry/EllipticCurve/Group): compute range of baseChange merge-conflict t-algebraic-geometry ??? missing CI information
25981 Multramate feat(GroupTheory/GroupAction/Basic): define homomorphisms of fixed subgroups induced by homomorphisms of groups merge-conflict t-group-theory ??? missing CI information
25980 Multramate feat(GroupTheory/Submonoid/Operations): define homomorphisms of subgroups induced by homomorphisms of groups merge-conflict t-group-theory ??? missing CI information
25486 VTrelat feat(SetTheory/ZFC/Integers): define integers in ZFC merge-conflict t-set-theory blocked-by-other-PR new-contributor blocked on another PR
25485 VTrelat feat(SetTheory/ZFC/Naturals): define natural numbers in ZFC merge-conflict t-set-theory new-contributor failing CI
25484 VTrelat feat(SetTheory/ZFC/Booleans): define Boolean algebra in ZFC merge-conflict t-set-theory blocked-by-other-PR new-contributor ??? blocked on another PR
25474 adomani test for .lean/.md check merge-conflict t-linter file-removed ??? missing CI information
25238 Hagb feat(Tactic/ComputeDegree): add support for scalar multiplication with different types merge-conflict t-meta new-contributor ??? missing CI information
26385 jjdishere feat(RingTheory/Perfectoid): define integral perfectoid rings merge-conflict WIP t-ring-theory labelled WIP
22909 AntoineChambert-Loir feat(RingTheory/Pure): pure submodules merge-conflict t-ring-theory blocked-by-other-PR blocked on another PR
22908 AntoineChambert-Loir feat(RingTheory/Finiteness/Small): tensor product of the system of small submodules merge-conflict t-ring-theory blocked-by-other-PR ??? blocked on another PR
22898 AntoineChambert-Loir feat(RingTheory/TensorProduct/DirectLimit/FG): direct limit of finitely generated submodules and tensor product merge-conflict WIP t-ring-theory ??? labelled WIP
20431 erdOne feat(RingTheory/AdicCompletion): monotonicity of adic-completeness merge-conflict awaiting-author t-ring-theory ??? missing CI information
19596 Command-Master feat(RingTheory/Valuation/PrimeMultiplicity): define `WithTop ℤ`-valued prime multiplicity on a fraction field merge-conflict awaiting-author t-ring-theory large-import ??? missing CI information
18646 jxjwan feat(RingTheory): isotypic components merge-conflict t-ring-theory new-contributor failing CI
17246 pechersky feat(RingTheory/PrimaryDecomposition): PIR of Noetherian under jacobson condition merge-conflict awaiting-author t-ring-theory failing CI
21474 erdOne feat(RingTheory): replace `Ring.DimensionLEOne` with `Ring.KrullDimLE` merge-conflict t-ring-theory large-import 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) α` merge-conflict awaiting-author t-group-theory large-import ??? missing CI information
27886 alreadydone feat(Algebra): (Mv)Polynomial.X is irreducible assuming NoZeroDivisors merge-conflict awaiting-author 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 t-category-theory large-import merge-conflict t-algebraic-geometry labelled WIP
27709 kckennylau chore: fix links merge-conflict WIP labelled WIP
28075 tristan-f-r chore(Finsupp/Indicator): make non-classical awaiting-author t-data easy awaiting author
20671 thefundamentaltheor3m feat(Analysis/Asymptotics/SpecificAsymptotics): Proving that 𝛔ₖ(n) = O(nᵏ⁺¹) t-number-theory new-contributor large-import merge-conflict awaiting-author ??? missing CI information
20267 joelriou feat(CategoryTheory): comma categories are accessible merge-conflict WIP awaiting-author 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 t-ring-theory large-import merge conflict
27444 grunweg feat: generalise more lemmas to enorms carleson WIP ⚠️ labelled WIP
24862 grunweg feat(LocallyIntegrable): generalise more to enorms merge-conflict WIP carleson t-measure-probability 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 WIP new-contributor will-close-soon awaiting-author help-wanted t-analysis looking for help
25483 VTrelat chore(Data/Set/Prod, SetTheory/ZFC/Basic): add theorem prod_subset_of_prod and extend ZFC model merge-conflict t-data new-contributor ??? missing CI information
25401 digama0 feat(Util): SuppressSorry option merge-conflict t-meta ??? missing CI information
26394 winstonyin feat: existence of local flows on manifolds merge-conflict WIP t-differential-geometry labelled WIP
27897 grunweg feat: check indentation of doc-strings merge-conflict t-linter blocked-by-other-PR awaiting-CI blocked on another PR
27996 grunweg feat: check indentation in doc-strings, medium version merge-conflict WIP blocked-by-other-PR ⚠️ 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 please-adopt new-contributor merge-conflict modifies-tactic-syntax good first issue t-meta ??? looking for help
7873 astrainfinita perf: reorder `extends` and change instance priority in algebra hierarchy merge-conflict slow-typeclass-synthesis t-algebra blocked-by-other-PR ??? blocked on another PR
27446 grunweg chore: more enorm lemmas merge-conflict WIP carleson labelled WIP
14583 lecopivo fix: make concrete cycle notation local merge-conflict awaiting-author ??? missing CI information
5897 eric-wieser feat: add a `MonadError` instance for `ContT` awaiting-author t-meta ??? missing CI information
28502 gilesgshaw feat(Logic/Basic): avoid unnecessary uses of choice blocked-by-other-PR new-contributor merge-conflict awaiting-author t-logic 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 merge-conflict awaiting-author t-algebra ??? missing CI information
27198 robin-carlier feat(CategoryTheory/Monoidal/DayConvolution): the Yoneda embedding is monoidal (for Day convolution) merge-conflict file-removed blocked-by-other-PR t-category-theory 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 t-set-theory easy awaiting author
27872 JovanGerb chore(gcongr): clean up imports merge-conflict delegated 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` merge-conflict t-algebra blocked-by-other-PR new-contributor blocked on another PR
7300 ah1112 feat: synthetic geometry merge-conflict awaiting-author help-wanted t-euclidean-geometry looking for help
13795 astrainfinita perf(Algebra/{Group, GroupWithZero, Ring}/InjSurj): reduce everything merge-conflict t-algebra ??? missing CI information
28150 Equilibris chore: clean up proofs typevec proofs merge-conflict t-data new-contributor merge conflict
27868 grunweg linter indentation playground merge-conflict WIP t-linter labelled WIP
25488 VTrelat feat(SetTheory/ZFC/Rationals): define rationals in ZFC merge-conflict t-set-theory blocked-by-other-PR new-contributor 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 t-data new-contributor failing CI
25700 grunweg feat: lint upon uses of the `mono` tactic please-adopt t-linter RFC looking for help
27835 edegeltje feat(Tactic): ring modulo a given characteristic merge-conflict large-import migrated-from-branch t-meta failing CI
28787 alreadydone feat(Counterexamples): a domain whose ring of differences is not a domain merge-conflict t-algebra blocked-by-other-PR large-import blocked on another PR
24719 madvorak feat(LinearAlgebra/Matrix/NonsingularInverse): inverting `Matrix` inverts its `LinearEquiv` awaiting-author t-algebra ??? missing CI information
27437 kckennylau feat(RingTheory/Valuation): some lemmas about comparing with 1 and 0 and with each other merge-conflict WIP 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 merge-conflict WIP blocked-by-other-PR t-combinatorics blocked on another PR
28687 mitchell-horner feat(Combinatorics/SimpleGraph): prove the Erdős-Stone-Simonovits theorem merge-conflict WIP blocked-by-other-PR t-combinatorics blocked on another PR
28689 mitchell-horner feat(Combinatorics/SimpleGraph): prove well-known corollaries of the Erdős-Stone-Simonovits theorem merge-conflict WIP blocked-by-other-PR t-combinatorics blocked on another PR
26952 robin-carlier feat(CategoryTheory/DayConvolution): monoid objects internal to day convolutions merge-conflict blocked-by-other-PR t-category-theory blocked on another PR
27133 robin-carlier feat(CategoryTheory/Monoidal/DayConvolution): `C ⊛⥤ V` is monoidal closed when `V` is merge-conflict blocked-by-other-PR 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 merge-conflict blocked-by-other-PR 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` merge-conflict blocked-by-other-PR 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 new-contributor merge-conflict awaiting-author t-analysis blocked on another PR
25741 robin-carlier feat(AlgebraicTopology/SimplexCategory/SimplicialObject): definitions of simplicial objects by generators and relation t-algebraic-topology blocked-by-other-PR t-category-theory large-import merge-conflict blocked on another PR
26931 javra feat(CategoryTheory/Enriched): `V`-enriched isomorphisms merge-conflict awaiting-author t-category-theory infinity-cosmos merge conflict
27707 FLDutchmann feat(NumberTheory/SelbergSieve): define Selberg's weights and prove basic results. merge-conflict t-number-theory blocked-by-other-PR t-analysis blocked on another PR
27898 grunweg feat: check indentation of doc-strings, basic version merge-conflict t-linter blocked-by-other-PR blocked on another PR
25208 erdOne feat(LinearAlgebra): `tensor_induction` macro merge-conflict WIP t-algebra RFC ??? labelled WIP
28803 astrainfinita refactor: unbundle algebra from `ENormed*` t-algebra merge-conflict slow-typeclass-synthesis awaiting-zulip t-analysis ❌? infrastructure-related CI failing
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 t-ring-theory awaiting-CI 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 merge-conflict t-computability awaiting-author 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 ??? missing CI information
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 ??? missing CI information
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 merge-conflict blocked-by-other-PR t-meta blocked on another PR
13036 joelriou feat(CategoryTheory/Sites): under certain conditions, cover preserving functors preserve 1-hypercovers merge-conflict WIP 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 merge-conflict WIP 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 ℂ` t-analysis easy bench-after-CI failing CI
28802 grunweg feat: a tactic linter for continuity/measurability which can be `fun_prop` merge-conflict large-import awaiting-CI t-meta does not pass CI
25069 erdOne feat(EllipticCurve): rational points of singular nodal cubics merge-conflict awaiting-author t-algebraic-geometry ??? missing CI information
25070 erdOne feat(EllipticCurve): rational points on singular cuspidal cubics merge-conflict awaiting-author t-algebraic-geometry ??? missing CI information
26670 yu-yama feat(GroupExtension/Abelian): define `conjClassesEquivH1` merge-conflict awaiting-author 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 merge-conflict awaiting-author t-differential-geometry merge conflict
28580 kmill refactor: simplify implementation of `filter_upwards` merge-conflict t-order t-meta failing CI
29605 alreadydone experiment(Algebra): unbundle npow/zpow from Monoid/InvDivMonoid merge-conflict t-algebra awaiting-CI 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 merge-conflict WIP t-category-theory awaiting-CI ??? labelled WIP
27950 alreadydone feat(MonoidAlgebra): criteria for `single` to be a unit, irreducible or prime merge-conflict WIP t-algebra blocked-by-other-PR blocked on another PR
28067 grunweg Docstring enumerations merge-conflict blocked-by-other-PR 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 merge-conflict awaiting-author t-category-theory failing CI
25480 ocfnash feat: define a concrete model of the `𝔤₂` root system merge-conflict WIP 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 merge-conflict t-algebraic-geometry blocked-by-other-PR RFC blocked on another PR
27829 dupuisf feat: modify `cfc_tac` to use `grind` merge-conflict WIP ⚠️ labelled WIP
21950 erdOne feat(NumberTheory/Padics): the completion of `ℚ` at a finite place is `ℚ_[p]` merge-conflict t-number-theory ??? missing CI information
12278 Rida-Hamadani feat(Combinatorics/SimpleGraph): Provide iff statements for distance equal and greater than 2 merge-conflict awaiting-author t-combinatorics ??? missing CI information
29092 zhuyizheng feat(MeasureTheory): add absolutely continuous functions, FTC and integration by parts merge-conflict awaiting-author new-contributor t-measure-probability merge conflict
26178 ppls-nd-prs feat(CategoryTheory/Limits): Fubini for products merge-conflict awaiting-author 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 merge-conflict blocked-by-other-PR t-category-theory blocked on another PR
27432 robin-carlier feat(CategoryTheory/Limits/Shapes/Pullback/Categorical): pseudofunctoriality of categorical pulback squares merge-conflict blocked-by-other-PR t-category-theory blocked on another PR
27481 robin-carlier feat(CategoryTheory/Limits/Shapes/Pullback/Categorical): adjunctions and equivalences of categorical pullback squares merge-conflict blocked-by-other-PR t-category-theory large-import blocked on another PR
27686 robin-carlier feat(CategoryTheory/Limits/Shapes/Pullback/Categorical/Square): more API for `CatPullbackSquare` merge-conflict blocked-by-other-PR t-category-theory large-import blocked on another PR
27687 robin-carlier feat(CategoryTheory/Limits/Shapes/Pullback/Categorical): squares equivalent to a `CatPullbackSquare` merge-conflict blocked-by-other-PR t-category-theory large-import blocked on another PR
27688 robin-carlier feat(CategoryTheory/Limits/Shapes/Pullback/Categorical): coherence statement for `CatPullbackSquare.inverse` merge-conflict blocked-by-other-PR t-category-theory large-import blocked on another PR
27689 robin-carlier feat(CategoryTheory/Limits/Shapes/Pullback/Categorical): horizontal pasting calculus for `CatPullbackSquare` merge-conflict blocked-by-other-PR t-category-theory large-import blocked on another PR
27690 robin-carlier feat(CategoryTheory/Limits/Shapes/Pullback/Categorical): vertical pasting calculus for `CatPullbackSquare` merge-conflict blocked-by-other-PR t-category-theory large-import blocked on another PR
27740 robin-carlier feat(CategoryTheory/Limits/Shapes/Pullback/Categorical): pasting calculus for `CategoricalPullback` merge-conflict blocked-by-other-PR 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-algebraic-topology t-category-theory merge conflict
28074 grunweg Isbilinearmap merge-conflict WIP labelled WIP
26579 robin-carlier feat(CategoryTheory/Limits/Pullbacks/Categorical/CatCospanTransform): equivalences of categorical cospans merge-conflict blocked-by-other-PR 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 ??? missing CI information
27634 agjftucker fix(Analysis/Calculus/Implicit): consistently rename {`map`, `fun`, `function`} to `fun` merge-conflict blocked-by-other-PR 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 t-category-theory awaiting-CI large-import merge-conflict 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 merge-conflict WIP 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 merge-conflict t-algebraic-topology blocked-by-other-PR large-import ??? blocked on another PR
23621 astrainfinita chore: deprecate `LinearOrderedComm{Monoid, Group}WithZero` merge-conflict t-algebra t-order ??? missing CI information
28630 Antidite feat(Archive/Imo): right isosceles configuration in the complex plane IMO awaiting-author new-contributor awaiting author
30192 erdOne feat(RingTheory): valuative topology = adic topology for discrete rank 1 valuations merge-conflict WIP t-ring-theory t-topology labelled WIP
26886 pechersky feat(NumberTheory/Padics/ValuativeRel): ValuativeRel ℚ_[p] WIP t-number-theory blocked-by-other-PR t-algebra merge-conflict t-analysis 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 merge-conflict t-topology blocked-by-other-PR 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 merge-conflict awaiting-author t-ring-theory ??? missing CI information
29587 uniwuni feat(GroupTheory/Finiteness): define finitely generated semigroups merge-conflict ⚠️ merge conflict
16239 Rida-Hamadani feat(Geometry/Manifold): orientable manifolds merge-conflict awaiting-author t-differential-geometry failing CI
16553 grunweg WIP: tinkering with orientable manifolds merge-conflict WIP t-differential-geometry blocked-by-other-PR ??? blocked on another PR
28328 pechersky chore(Topology/Valued): golf using local finite order of WithZeroTopology t-number-theory blocked-by-other-PR t-algebra large-import merge-conflict t-topology blocked on another PR
29282 Jlh18 feat(CategoryTheory): HasColimits instance on Grpd merge-conflict blocked-by-other-PR new-contributor ⚠️ blocked on another PR
16773 arulandu feat(Probability/Distributions): formalize Beta distribution merge-conflict awaiting-author new-contributor t-measure-probability ??? missing CI information
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 merge-conflict awaiting-author t-category-theory ??? missing CI information
9273 grunweg feat: extended charts are local diffeomorphisms on their source merge-conflict awaiting-author t-differential-geometry ??? missing CI information
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 merge-conflict WIP t-number-theory large-import ??? labelled WIP
26913 Paul-Lez feat(NumberTheory/{*}): add a few lemmas about number field and cyclotomic extensions WIP t-number-theory t-algebra awaiting-CI merge-conflict 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 file-removed awaiting-zulip 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 _` t-data t-order delegated easy failing CI
19616 adamtopaz fix: fix the definition of the absolute Galois group of a field merge-conflict t-algebra awaiting-author t-number-theory ??? missing CI information
28826 alreadydone feat(CategoryTheory): Additive and Linear when Hom types are only monoids merge-conflict WIP t-category-theory awaiting-CI labelled WIP
28152 Sebi-Kumar feat(AlgebraicTopology): characterize simply connectedness in terms of loops merge-conflict t-algebraic-topology blocked-by-other-PR new-contributor blocked on another PR
30460 janithamalith feat(Nat): add lemma nat_card_orbit_mul_card_stabilizer_eq_card_group awaiting-author t-group-theory new-contributor awaiting author
25737 robin-carlier feat(AlgebraicTopology/SimplexCategory/GeneratorsRelations/NormalForms): Normal forms for `P_δ`s t-algebraic-topology delegated t-category-theory failing CI
30209 Ruben-VandeVelde feat: some TwoSidedIdeal.span lemmas awaiting-author t-ring-theory FLT awaiting author
25225 xcloudyunx feat(Combinatorics/SimpleGraph): Eulerian walk in connected graph contains all vertices awaiting-author t-combinatorics new-contributor ??? missing CI information
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` t-data new-contributor 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 merge-conflict documentation awaiting-author merge conflict
28737 astrainfinita refactor: deprecate `MulEquivClass` merge-conflict awaiting-author t-algebra merge conflict
28676 sun123zxy feat(NumberTheory/ArithmeticFunction): wrap `Nat.totient` as an `ArithmeticFunction` t-number-theory new-contributor large-import merge-conflict awaiting-author merge conflict
30421 grunweg WIP: support products in the differential geometry elaborators merge-conflict failing CI
30299 franv314 feat(Topology/Instances): Cantor set new-contributor merge-conflict file-removed awaiting-author t-topology merge conflict
30303 franv314 chore(Topology/Instances): add deprecated module merge-conflict blocked-by-other-PR new-contributor blocked on another PR
30900 vihdzp feat: run-length encoding merge-conflict blocked-by-other-PR 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` merge-conflict WIP 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 merge-conflict awaiting-author t-category-theory large-import merge conflict
26085 grunweg feat: disjoint unions distribute with products of manifolds please-adopt WIP t-differential-geometry merge-conflict looking for help
27180 ADedecker feat: quotient of a monoid with zero by a multiplicative congruence merge-conflict t-algebra delegated ??? missing CI information
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 merge-conflict awaiting-author 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` merge-conflict awaiting-author t-ring-theory merge conflict
29774 Raph-DG feat(AlgebraicGeometry): Order of vanishing of elements of the function field of locally noetherian, integral schemes merge-conflict file-removed blocked-by-other-PR ⚠️ 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 merge-conflict WIP t-category-theory labelled WIP
22361 rudynicolop feat(Computability/NFA): nfa closure properties new-contributor t-computability merge-conflict awaiting-author awaiting-zulip ??? missing CI information
30158 nicolaviolette feat: combinatorics simplegraph basic awaiting-author t-combinatorics new-contributor awaiting author
27708 vihdzp feat: unions and intersections of ordinals are ordinals merge-conflict awaiting-author 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 FLT t-group-theory new-contributor 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 merge-conflict file-removed awaiting-author 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 merge-conflict blocked-by-other-PR large-import t-measure-probability 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 merge-conflict awaiting-author t-algebraic-geometry large-import failing CI
29992 vlad902 feat(Order): finite (Max)Chains always contains a top/max element merge-conflict WIP t-order large-import labelled WIP
26901 5hv5hvnk feat: a simproc version of `compute_degree` awaiting-CI new-contributor merge-conflict awaiting-author t-meta does not pass CI
31020 grunweg feat: mfderiv of Sum.inl and Sum.inr merge-conflict WIP ⚠️ labelled WIP
31348 PatrickMassot chore: fix a docstring typo documentation awaiting-author t-analysis easy awaiting author
28685 mitchell-horner feat(Combinatorics/SimpleGraph): prove the minimal-degree version of the Erdős-Stone theorem merge-conflict WIP blocked-by-other-PR t-combinatorics ??? blocked on another PR
25775 emilyriehl feat(AlgebraicTopology/SimplicialSet/NerveAdjunction): to Strict Segal 2 t-algebraic-topology t-category-theory merge-conflict awaiting-author infinity-cosmos failing CI
14752 AntoineChambert-Loir fix(Topology/Algebra/Valued): repair definition of Valued merge-conflict WIP t-topology t-algebra ??? labelled WIP
29145 JovanGerb chore: use `to_additive` in more places awaiting-CI t-meta does not pass CI
26827 pechersky feat(Analysis/Normed/ValuativeRel): helper instance for NormedField merge-conflict t-algebra t-number-theory t-analysis merge conflict
29458 LiamSchilling feat(MvPolynomial/WeightedHomogenous): relate `weightedTotalDegree` to `degrees` and `degreeOf` awaiting-author t-ring-theory new-contributor 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 t-category-theory large-import new-contributor merge-conflict awaiting-zulip t-meta awaiting a zulip discussion
30258 imbrem feat(CategoryTheory/Monoidal): to_additive for proofs using `monoidal` merge-conflict blocked-by-other-PR large-import new-contributor ⚠️ blocked on another PR
30260 imbrem feat(CategoryTheory/Monoidal): added CocartesianMonoidalCategory merge-conflict blocked-by-other-PR large-import new-contributor ??? ⚠️ blocked on another PR
26973 peabrainiac feat(Geometry/Diffeology): diffeologies generated from sets of plots merge-conflict t-differential-geometry blocked-by-other-PR blocked on another PR
27274 peabrainiac feat(Geometry/Diffeology): continuous diffeologies & D-topology-lemmas merge-conflict t-differential-geometry blocked-by-other-PR 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 merge-conflict awaiting-author tech debt t-analysis merge conflict
27953 CoolRmal feat(ProbabilityTheory): Conditional Jensen's Inequality merge-conflict blocked-by-other-PR new-contributor t-measure-probability ??? blocked on another PR
30824 grunweg wip: another smoothness lemma for local frames merge-conflict WIP t-differential-geometry labelled WIP
30322 kckennylau feat(RingTheory): base change of graded algebra merge-conflict awaiting-author t-ring-theory merge conflict
30399 kckennylau feat(RingTheory): make HomogeneousLocalization.map take a graded ring hom merge-conflict blocked-by-other-PR ⚠️ blocked on another PR
10235 urkud feat: add `Decidable`, `Fintype`, `Encodable` linters awaiting-bench t-linter large-import merge-conflict awaiting-author t-meta failing CI
31593 Ruben-VandeVelde feat: some lemmas about MonoidAlgebra merge-conflict awaiting-author t-algebra merge conflict
31596 grunweg chore: remove extraneous uses of push_neg merge-conflict WIP labelled WIP
30357 grunweg chore: golf using custom elaborators merge-conflict awaiting-bench t-differential-geometry blocked-by-other-PR blocked on another PR
26885 pechersky feat(Topology/ValuativeRel): ValuativeTopology 𝒪[K] t-algebra t-number-theory t-topology 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 new-contributor t-computability merge-conflict awaiting-author awaiting-zulip ??? missing CI information
12032 mcdoll feat: delta distribution as a limit WIP t-analysis labelled WIP
26240 grunweg perf(CommandLinterLinter): use Substring more merge-conflict t-linter RFC merge conflict
9693 madvorak feat: Linear programming in the standard form merge-conflict WIP t-algebra RFC ??? labelled WIP
22464 adomani feat(CI): declarations diff in Lean awaiting-author CI ??? missing CI information
27392 Paul-Lez feat(Tactic/SimpUtils): add simproc finding commands large-import merge-conflict file-removed awaiting-author t-meta 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 new-contributor t-computability merge-conflict awaiting-author awaiting-zulip ??? missing CI information
20238 maemre feat(Computability/DFA): Closure of regular languages under some set operations new-contributor t-computability merge-conflict awaiting-author awaiting-zulip ??? missing CI information
5745 alexjbest feat: a tactic to consume type annotations, and make constructor nicer merge-conflict awaiting-author t-meta ??? missing CI information
5863 eric-wieser feat: add elaborators for concrete matrices merge-conflict help-wanted blocked-by-other-PR t-meta blocked on another PR
5919 MithicSpirit feat: implement orthogonality for AffineSubspace WIP new-contributor merge-conflict help-wanted t-analysis ??? looking for help
7386 madvorak feat: Define linear programs merge-conflict WIP t-algebra RFC ??? labelled WIP
9352 chenyili0818 feat: arithmetic lemmas for `gradient` merge-conflict awaiting-author t-analysis ??? missing CI information
9795 sinhp feat: the type `Fib` of fibre of a function at a point merge-conflict awaiting-author t-category-theory ??? missing CI information
10660 eric-wieser feat(LinearAlgebra/CliffordAlgebra): construction from a basis merge-conflict WIP awaiting-author t-algebra labelled WIP
10977 grunweg feat: germs of smooth functions t-differential-geometry merge-conflict awaiting-author t-topology t-analysis failing CI
10998 hmonroe feat(Logic): Arithmetization of partial recursive functions (toward Gödel's first incompleteness theorem) merge-conflict awaiting-author t-logic ??? missing CI information
11890 adomani feat: the terminal refine linter merge-conflict t-linter awaiting-author ??? missing CI information
12006 adomani feat: the `suffa` tactic merge-conflict awaiting-author t-meta ??? missing CI information
13442 dignissimus feat: mabel tactic for multiplicative abelian groups new-contributor merge-conflict modifies-tactic-syntax awaiting-author help-wanted t-meta looking for help
14237 js2357 feat: Define the localization of a fractional ideal at a prime ideal merge-conflict awaiting-author t-algebra new-contributor failing CI
14345 digama0 feat: the Dialectica category is monoidal closed merge-conflict awaiting-author t-category-theory ??? missing CI information
14727 jjaassoonn feat(RingTheory/Flat/CategoryTheory): a flat module has vanishing higher Tor groups merge-conflict awaiting-author t-ring-theory ??? missing CI information
14733 jjaassoonn feat(RingTheory/Flat/CategoryTheory): a module is flat iff tensoring preserves finite limits merge-conflict awaiting-author t-ring-theory ??? missing CI information
15055 sinhp feat: the category of pointed objects of a concrete category merge-conflict awaiting-author t-category-theory ??? missing CI information
15224 AnthonyBordg feat(CategoryTheory/Sites): covering families and their associated Grothendieck topology merge-conflict awaiting-author t-category-theory new-contributor ??? missing CI information
16303 grunweg feat(CI): check for badly formatted titles or missing/contradictory labels merge-conflict awaiting-author CI failing CI
18236 joelriou feat(Algebra/Category/ModuleCat/Presheaf): the endofunctor of presheaves of modules induced by an oplax natural transformation WIP t-algebra t-category-theory awaiting-CI merge-conflict awaiting-author labelled WIP
18749 GabinKolly feat(ModelTheory): preparatory work for the existence of Fraïsse limits merge-conflict awaiting-author t-logic ??? missing CI information
18876 GabinKolly feat(ModelTheory/Fraisse): add proof that Fraïssé limits exist merge-conflict blocked-by-other-PR t-logic ??? blocked on another PR
19323 madvorak feat: Function to Sum decomposition merge-conflict WIP t-data ??? labelled WIP
19378 adamtopaz feat: Explanation widgets merge-conflict awaiting-author t-meta ??? missing CI information
19456 AntoineChambert-Loir feat(Data/Finsupp/MonomialOrder/DegRevLex): homogeneous reverse lexicographic order WIP t-order t-data merge-conflict t-algebraic-geometry labelled WIP
20051 Timeroot feat: `Clone` and some instances merge-conflict awaiting-author t-algebra blocked-by-other-PR blocked on another PR
20466 MohanadAhmed feat: Sherman Morrison formula for rank 1 update of the matrix inverse merge-conflict awaiting-author t-data ??? missing CI information
20648 anthonyde feat: formalize regular expression -> εNFA merge-conflict t-computability awaiting-zulip new-contributor ??? missing CI information
20649 GabinKolly feat(ModelTheory/Graph): prove characterization of the fraisse limit of finite simple graphs WIP large-import merge-conflict t-combinatorics t-logic labelled WIP
20652 jjaassoonn feat: categorical description of center of a ring merge-conflict awaiting-author t-algebra t-category-theory 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 merge-conflict t-computability blocked-by-other-PR blocked on another PR
21270 GabinKolly feat(ModelTheory/Bundled): first-order embeddings and equivalences from equalities merge-conflict awaiting-author large-import t-logic ??? missing CI information
21277 GabinKolly feat(ModelTheory/PartialEquiv): Define the mapping of a self-partialEquiv through an embedding merge-conflict blocked-by-other-PR t-logic ??? blocked on another PR
21616 peabrainiac feat(Topology): concatenating countably many paths merge-conflict awaiting-author t-topology ??? missing CI information
21624 sinhp feat(CategoryTheory): The (closed) monoidal structure on the product category of families of (closed) monoidal categories merge-conflict awaiting-author t-category-theory failing CI
21829 Whysoserioushah feat(LinearAlgebra/TensorProduct/HomTensor): Add TensorProduct of Hom-modules merge-conflict awaiting-author t-algebra ??? missing CI information
21903 yhtq feat: add from/toList between `FreeSemigroup` and `List` with relative theorems t-algebra new-contributor awaiting-CI large-import merge-conflict does not pass CI
22159 shetzl feat: add definition of pushdown automata merge-conflict t-computability awaiting-author new-contributor ??? missing CI information
22231 pechersky feat(Algebra/Valued): `AdicExpansion` initial defns merge-conflict t-algebra awaiting-author t-topology ??? missing CI information
22232 pechersky feat(Algebra/Valued): `AdicExpansion.apprUpto` merge-conflict t-topology blocked-by-other-PR blocked on another PR
22233 pechersky feat(Algebra/Valued): `AdicExpansion.evalAt` merge-conflict t-topology blocked-by-other-PR ??? blocked on another PR
22302 658060 feat: add `CategoryTheory.Topos.Power` merge-conflict awaiting-author t-category-theory new-contributor ??? missing CI information
22314 shetzl feat: add leftmost derivations for context-free grammars merge-conflict t-computability awaiting-author new-contributor ??? missing CI information
22662 plp127 feat: Localization.Away.lift (computably) merge-conflict t-algebra ??? missing CI information
22790 mhk119 feat: Extend `taylor_mean_remainder_lagrange` to `x < x_0` merge-conflict awaiting-author t-analysis new-contributor merge conflict
22861 eric-wieser feat: add the trace of a bilinear form merge-conflict awaiting-author t-algebra ??? missing CI information
22919 plp127 feat(Data/Fintype/Pi): Make `Fintype` instance for `RelHom`s computable merge-conflict awaiting-author t-data ??? missing CI information
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 t-algebra t-category-theory large-import merge-conflict labelled WIP
23460 Timeroot feat: Definition of `Clone` merge-conflict t-algebra blocked-by-other-PR ??? blocked on another PR
23503 apnelson1 feat(Topology/Instances/ENat): ENat and tsum merge-conflict WIP t-topology large-import ??? labelled WIP
23585 plp127 feat: `Filter.atMax` and `Filter.atMin` merge-conflict WIP t-order ??? labelled WIP
23758 erdOne feat(Topology/Algebra): linearly topologized iff non-archimedean t-algebra large-import merge-conflict awaiting-author t-topology ??? missing CI information
23835 chrisflav feat(Topology): cardinality of connected components is bounded by cardinality of fiber merge-conflict awaiting-author t-topology failing CI
24333 xcloudyunx feat(Combinatorics/SimpleGraph): cycle graph implementation for generic vertex types merge-conflict awaiting-author t-combinatorics new-contributor ??? missing CI information
24540 robertmaxton42 feat(Quiv): add the empty, vertex, point, interval, and walking quivers merge-conflict awaiting-author t-category-theory failing CI
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 merge-conflict awaiting-author t-algebra t-data merge conflict
25585 Paul-Lez feat(Tactic/Linters/DeprecatedSimpLemma): lint for deprecated simp lemmas merge-conflict t-linter awaiting-author failing CI
25739 literandltx feat(NumberTheory/LegendreSymbol): Add sqrt‐of‐residue theorems for p=4k+3 and p=8k+5 merge-conflict awaiting-author 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 merge-conflict awaiting-author t-number-theory ??? missing CI information
26051 Komyyy feat(Mathlib/GroupTheory/SpecificGroups/Alternating): A_n is simple iff n = 3 or 5 ≤ n merge-conflict WIP t-group-theory large-import labelled WIP
26061 kckennylau (WIP) feat(AlgebraicGeometry): define Projective Space merge-conflict WIP t-algebraic-geometry blocked-by-other-PR blocked on another PR
26158 upobir feat(NumberTheory/Divisors): add int divisors merge-conflict awaiting-author t-number-theory merge conflict
26160 oliver-butterley feat(MeasureTheory.VectorMeasure): add several lemmas which characterize variation merge-conflict blocked-by-other-PR new-contributor t-measure-probability ??? blocked on another PR
26165 oliver-butterley feat(MeasureTheory.VectorMeasure): add lemma which shows that variation of a `ℝ≥0∞` VectorMeasure is equal to itself merge-conflict blocked-by-other-PR new-contributor t-measure-probability blocked on another PR
26292 RemyDegenne feat(MeasureTheory): tightness of the range of a sequence merge-conflict awaiting-author t-measure-probability failing CI
26293 RemyDegenne feat: tightness from convergence of characteristic functions merge-conflict WIP 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 new-contributor merge-conflict awaiting-author t-analysis labelled WIP
26329 Timeroot feat: Definition of `Clone` notations and typeclasses merge-conflict awaiting-author t-algebra awaiting-CI 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 merge-conflict blocked-by-other-PR 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 merge-conflict awaiting-author t-algebra new-contributor merge conflict
26644 kckennylau feat(SetTheory/ZFC): Define the language of sets and state the ZFC axioms merge-conflict awaiting-author t-set-theory merge conflict
26648 eric-wieser chore(TensorProduct): remove more `suppress_compilation`s merge-conflict blocked-by-core-PR t-algebra blocked on another PR
26757 fweth feat(CategoryTheory/Topos): define elementary topos merge-conflict awaiting-author t-category-theory new-contributor failing CI
26803 bjoernkjoshanssen feat: second partial derivatives test merge-conflict awaiting-author t-analysis failing CI
26872 faenuccio chore(RingTheory/Valuation/RankOne): modify the definition of Valuation.RankOne using its range rather than its codomain merge-conflict awaiting-author t-algebra blocked-by-other-PR 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 merge-conflict WIP t-category-theory t-meta labelled WIP
26942 pechersky feat(RingTheory/Valuation/ValueGroupIso): isomorphism of value groups when compatible merge-conflict t-ring-theory blocked-by-other-PR t-order blocked on another PR
26990 joelriou feat(CategoryTheory/Abelian): Noetherian objects form a Serre class merge-conflict WIP t-category-theory labelled WIP
27098 Paul-Lez feat(Algebra/Category/ModuleCat/Sheaf/VectorBundle): define vector bundles merge-conflict awaiting-author t-algebra merge conflict
27155 Pjotr5 feat: Shearer's bound on the independence number of triangle free graphs merge-conflict awaiting-author t-combinatorics new-contributor failing CI
27163 pechersky feat(Topology/ValuativeRel): of and to basis of compatible valuations t-number-theory t-algebra merge-conflict awaiting-author t-topology merge conflict
27187 Komyyy feat: `NONote` represents ordinals < ε₀ merge-conflict WIP t-set-theory labelled WIP
27215 kckennylau feat(AlgebraicGeometry): Define the Zariski site on `CommRingCatᵒᵖ` merge-conflict awaiting-author t-algebraic-geometry merge conflict
27307 xyzw12345 feat(RingTheory/GradedAlgebra): homogeneous relation merge-conflict awaiting-author t-ring-theory merge conflict
27309 kckennylau feat(CategoryTheory): a presheaf on `CostructuredArrow F d` can be extended to a presheaf on `C` merge-conflict WIP t-category-theory labelled WIP
27321 kckennylau feat(CategoryTheory): Colimit can be computed fiberwise merge-conflict t-category-theory awaiting-CI does not pass CI
27417 PierreQuinton feat: add `SigmaCompleteLattice` merge-conflict awaiting-author t-order merge conflict
27500 Komyyy feat: the Riemann zeta function is meromorphic merge-conflict WIP 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 merge-conflict awaiting-author t-category-theory new-contributor merge conflict
27824 ChrisHughes24 feat(Calculus): exists_gt_of_deriv_pos and variants merge-conflict awaiting-author t-analysis merge conflict
27850 fyqing feat: 0-dimensional manifolds are discrete and countable merge-conflict awaiting-author 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 merge-conflict awaiting-author t-algebra large-import merge conflict
28056 grunweg wip: existence of Riemannian metrics merge-conflict WIP t-differential-geometry labelled WIP
28072 kckennylau feat(RingTheory/Valuation): make tactic rw_val_equiv merge-conflict awaiting-author 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 merge-conflict awaiting-author t-meta merge conflict
28530 nonisomorphiclinearmap feat(Combinatorics/SimplicialComplex/Topology): add standard simplices and geometric realisation (colimit + functoriality) merge-conflict blocked-by-other-PR 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` merge-conflict awaiting-author t-set-theory merge conflict
29108 JonBannon feat(MeasureTheory): add `LInfty.lean` with `Mul` and `const` related results. merge-conflict awaiting-author t-measure-probability merge conflict
29411 llllvvuu feat(LinearAlgebra/Matrix/Rank): rank factorization merge-conflict awaiting-author ⚠️ merge conflict
29425 pechersky feat(NumberTheory/Padics/Torsion): `HasEnoughRootsOfUnity ℤ_[p] (p - 1)` merge-conflict awaiting-author t-ring-theory blocked-by-other-PR blocked on another PR
29500 vihdzp feat: `WellFoundedLT (LowerSet α)` merge-conflict awaiting-author t-order merge conflict
29526 llllvvuu feat: `Multiset.map f` identifies `f` up to permutation merge-conflict t-data merge conflict
29675 yury-harmonic feat(Wolstenholme): new file merge-conflict awaiting-author help-wanted t-data looking for help
29720 javra feat(CategoryTheory): `TransportEnrichment` and `ForgetEnrichment` as 2-functors merge-conflict WIP 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 merge-conflict WIP t-measure-probability labelled WIP
30001 vihdzp feat: concept generated by set of objects/attributes merge-conflict blocked-by-other-PR 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 merge-conflict awaiting-author t-analysis t-measure-probability merge conflict
30042 JovanGerb feat(push): `@[push]` attributes for `∈` in `Set`, `Finset` and `Multiset` merge-conflict awaiting-author t-meta merge conflict
30077 agjftucker feat(Analysis/Calculus/ImplicitFunOfBivariate): define implicitFunOfBivariate merge-conflict blocked-by-other-PR t-analysis blocked on another PR
30121 idontgetoutmuch Principal fiber bundle core merge-conflict awaiting-author t-differential-geometry new-contributor merge conflict
30312 kckennylau feat(RingTheory): define graded ring homomorphisms merge-conflict t-ring-theory blocked-by-other-PR ??? blocked on another PR
30334 kckennylau feat(RingTheory): define maps of homogeneous ideals merge-conflict t-ring-theory blocked-by-other-PR 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 merge-conflict blocked-by-other-PR ⚠️ blocked on another PR
30367 kckennylau feat(Data): define grading-preserving isomorphisms merge-conflict blocked-by-other-PR t-data blocked on another PR
30379 kckennylau feat(RingTheory): isomorphism of graded rings merge-conflict blocked-by-other-PR ⚠️ 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 merge-conflict awaiting-author t-category-theory merge conflict
31008 RemyDegenne refactor: generalize the index of the process in the Doob decomposition merge-conflict WIP 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 merge-conflict awaiting-author t-meta merge conflict
31351 grunweg feat: manifolds with smooth boundary merge-conflict WIP 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 t-differential-geometry blocked-by-other-PR merge-conflict t-meta blocked on another PR
31604 maksym-radziwill feat: analyticity of dslope merge-conflict awaiting-author t-analysis merge conflict
31738 robertmaxton42 feat: quivers can be represented as functors from the walking quiver merge-conflict awaiting-author t-category-theory failing CI
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 t-algebra blocked-by-other-PR blocked on another PR
15443 YaelDillies feat: Marcinkiewicz-Zygmund inequality WIP t-analysis labelled WIP
30083 grunweg feat: local frames in a vector bundle merge-conflict awaiting-author t-differential-geometry failing CI
30339 grunweg feat: extend a tangent vector for a locally smooth vector field merge-conflict t-differential-geometry blocked-by-other-PR blocked on another PR
31338 grunweg chore: move Pretrivialization, Trivialization to the Bundle namespace merge-conflict t-differential-geometry blocked-by-other-PR blocked on another PR
31339 grunweg Movelemma merge-conflict blocked-by-other-PR 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 merge-conflict WIP labelled WIP
25802 dagurtomas feat(AlgebraicTopology): anodyne morphisms of simplicial sets WIP t-topology labelled WIP
6268 eric-wieser fix: fixups to #3838 merge-conflict WIP ??? labelled WIP
6859 MohanadAhmed feat: TryLean4Bundle: Windows Bundle Creator WIP help-wanted CI ??? looking for help
6993 jjaassoonn feat: lemmas about `AddMonoidAlgebra.{divOf, modOf}` merge-conflict t-algebra ??? missing CI information
7427 MohanadAhmed feat: eigenvalues sorted in ascending/descending order merge-conflict WIP ??? ⚠️ labelled WIP
9339 FMLJohn feat(RingTheory/GradedAlgebra/HomogeneousIdeal): given a finitely generated homogeneous ideal of a graded semiring, construct a finite spanning set for the ideal which only contains homogeneous elements merge-conflict t-ring-theory ??? missing CI information
9564 AntoineChambert-Loir chore: weaken commutativity assumptions for AdjoinRoot.lift and AdjoinRoot.liftHom merge-conflict WIP t-algebra ??? labelled WIP
10026 madvorak feat: linear programming according to Antoine Chambert-Loir's book merge-conflict WIP t-algebra RFC ??? labelled WIP
10159 madvorak feat: linear programming according to Antoine Chambert-Loir's book — affine version merge-conflict WIP t-algebra RFC ??? 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 merge-conflict WIP t-algebraic-topology new-contributor ??? 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 please-adopt merge-conflict t-topology blocked-by-other-PR ??? blocked on another PR
12251 ScottCarnahan refactor(RingTheory/HahnSeries): several generalizations merge-conflict WIP t-algebra t-order ??? labelled WIP
12394 JADekker feat: define pre-tight and tight measures please-adopt merge-conflict awaiting-author t-measure-probability looking for help
12452 JADekker feat(Cocardinal): add some more api t-topology awaiting-CI ??? does not pass CI
14426 adomani feat: `#min_imps` command (development branch) merge-conflict WIP ??? ⚠️ labelled WIP
14686 smorel394 feat(AlgebraicGeometry/Grassmannian): define the Grassmannian scheme please-adopt WIP workshop-AIM-AG-2024 merge-conflict t-algebraic-geometry ??? looking for help
17071 ScottCarnahan feat(LinearAlgebra/RootSystem): separation, base, cartanMatrix merge-conflict WIP t-algebra ??? labelled WIP
17471 joelriou feat(Algebra/ModuleCat/Differentials/Sheaf): the sheaf of relative differentials WIP blocked-by-other-PR t-category-theory large-import merge-conflict t-algebraic-geometry blocked on another PR
18626 hannahfechtner feat: define Artin braid groups merge-conflict awaiting-author t-algebra new-contributor ??? missing CI information
18784 erdOne feat(AlgebraicGeometry): use `addMorphismPropertyInstances` merge-conflict t-algebraic-geometry blocked-by-other-PR blocked on another PR
19062 hannahfechtner feat(Algebra/PresentedMonoid/Basic): facts about rel awaiting-author t-algebra ??? missing CI information
19607 madvorak feat: block matrices are totally unimodular merge-conflict WIP blocked-by-other-PR ⚠️ blocked on another PR
20029 FrederickPu feat(Tactic/simps): allow for Config attributes to be set directly merge-conflict WIP new-contributor t-meta ??? labelled WIP
21269 658060 feat(CategoryTheory/Topos): basic definitions and results in topos theory WIP t-category-theory new-contributor merge-conflict awaiting-author ??? labelled WIP
22805 ScottCarnahan feat(FieldTheory/Finite): fixed points of Frobenius automorphism merge-conflict WIP 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 merge-conflict awaiting-author t-category-theory new-contributor ??? missing CI information
24533 robertmaxton42 feat(ULift): conjugation by ULift.up/down, misc cast/heq lemmas awaiting-author t-data ??? missing CI information
24690 ScottCarnahan feat(Data.Prod): reverse lexicographic order merge-conflict WIP t-order ??? labelled WIP
24692 ScottCarnahan feat(RingTheory/HahnSeries/Basic): isomorphism of Hahn series induced by order isomorphism merge-conflict WIP 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 merge-conflict WIP t-ring-theory labelled WIP
25906 pfaffelh feat(Topology/Compactness/CompactSystem): closed and compact square cylinders form a compact system merge-conflict t-topology blocked-by-other-PR blocked on another PR
26013 tsuki8 feat(Data/Finset/Card,Data/Set/Finite/Basic): TODO needs a better title awaiting-author t-data new-contributor awaiting author
25900 pfaffelh feat(Topology/Compactness/CompactSystem): set system of finite unions of sets in a compact system is again a compact system merge-conflict t-topology blocked-by-other-PR blocked on another PR
26455 ScottCarnahan feat(LinearAlgebra/RootSystem): API for CartanMatrix merge-conflict WIP 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 merge-conflict WIP 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 ??? missing CI information
26310 kckennylau feat: binary forms merge-conflict awaiting-author t-algebra merge conflict
26283 kckennylau feat: resultant of polynomials merge-conflict WIP t-algebra labelled WIP
27991 sinianluoye feat(Rat): add Rat.den_eq_of_add_den_eq_one and its dependent lemmas awaiting-author t-data new-contributor failing CI
28215 5hv5hvnk feat: strong and Weak connectivity for Digraphs WIP new-contributor merge-conflict awaiting-author t-combinatorics labelled WIP
28970 Whysoserioushah feat(Algebra/Algebra/ReducedNorm): defines reduced norm and trace merge-conflict awaiting-author t-algebra merge conflict
29212 Whysoserioushah feat(Algebra/CrossProductAlgebra/Defs): define Cross Product Algebra merge-conflict awaiting-author t-algebra merge conflict
29281 plp127 doc: `Fin.natAdd_castLEEmb` merge-conflict t-data merge conflict
29514 grunweg feat(CI): use more strict mode merge-conflict WIP CI ❌? labelled WIP
29574 JarodAlper feat: regular local rings are domains merge-conflict t-ring-theory new-contributor failing CI
29792 robertmaxton42 feat(RelCWComplex): a (relative, concrete) CW complex is the colimit of its skeleta merge-conflict blocked-by-other-PR large-import ⚠️ blocked on another PR
28718 imbrem feat: class for chosen finite coproducts blocked-by-other-PR t-category-theory new-contributor merge-conflict awaiting-author blocked on another PR
30352 kckennylau feat(RingTheory): Homogeneous localization of tensor product merge-conflict WIP blocked-by-other-PR ⚠️ blocked on another PR
30366 sinhp feat(CategoryTheory): The Preliminaries for Locally Cartesian Closed Categories merge-conflict awaiting-author 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 merge-conflict blocked-by-other-PR 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 merge-conflict blocked-by-other-PR 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 merge-conflict t-differential-geometry blocked-by-other-PR blocked on another PR
27025 grunweg feat: Gram-Schmidt procedure on smooth vector bundles yields smooth sections merge-conflict t-differential-geometry blocked-by-other-PR blocked on another PR
29777 yuanyi-350 feat(Functional Analysis): closed Range Theorem WIP blocked-by-other-PR new-contributor awaiting-author t-analysis blocked on another PR
28141 YaelDillies chore: deprecate `BialgHom.coe_toLinearMap` t-ring-theory awaiting-zulip toric 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` t-algebra awaiting-author awaiting author
25902 pfaffelh feat: The finite product of semi-rings (in terms of measure theory) is a semi-ring. t-measure-probability brownian large-import merge-conflict awaiting-author 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 merge-conflict awaiting-author t-algebra failing CI
31176 mcdoll feat(Analysis): Taylor's theorem with the integral remainder t-analysis awaiting-author awaiting author
30831 chrisflav feat(AlgebraicGeometry): the fpqc topology t-algebraic-geometry blocked-by-other-PR ??? blocked on another PR
28933 artie2000 chore(Data): correct definition for `single_apply` merge-conflict WIP labelled WIP
24627 pechersky feat(Topology/Algebra/Valued): `IsLinearTopology 𝒪[K] K` and `𝒪[K] 𝒪[K]` merge-conflict awaiting-author t-topology merge conflict
27756 grunweg feat: `Weak(Pseudo)EMetricSpace`, generalises `(Pseudo)EMetricSpace` merge-conflict WIP t-topology carleson 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 t-algebra t-ring-theory awaiting-author failing CI
24016 plp127 feat: fine uniformity merge-conflict t-topology ??? missing CI information
30995 kckennylau feat(RingTheory): replace ofLinearEquiv with limit t-ring-theory awaiting-author awaiting author
32094 grunweg feat(runLinter): allow only running certain linters t-linter CI failing CI
32095 grunweg chore: fix some explicitVarOfIff linter errors please-adopt WIP merge-conflict looking for help
31366 FaffyWaffles feat(Analysis/SpecialFunctions/StirlingRobbins): Robbins' sharp stepwise bound for stirlingSeq t-analysis new-contributor awaiting-author awaiting author
29982 hrmacbeth feat: new `isolate` tactic merge-conflict awaiting-author large-import t-meta failing CI
31796 dobronx1325 feat(Data/Real/EReal): add mul_lt_mul_of_pos_left theorem t-data new-contributor 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 merge-conflict t-differential-geometry blocked-by-other-PR t-meta blocked on another PR
29449 mitchell-horner feat(Combinatorics/SimpleGraph): add Turán density related theorems t-combinatorics blocked-by-other-PR blocked on another PR
27258 JovanGerb feat: Imo2020 q6 IMO awaiting-author 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 merge-conflict blocked-by-other-PR large-import blocked on another PR
32157 peabrainiac feat(Analysis/Calculus): Hadamard's lemma t-analysis blocked-by-other-PR blocked on another PR
26966 vihdzp feat: the Dedekind–MacNeille completion merge-conflict awaiting-author blocked-by-other-PR t-order blocked on another PR
30750 SnirBroshi feat(Data/Quot): `toSet` and `equivClassOf` t-data awaiting-author awaiting-zulip 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 merge-conflict t-data awaiting-author failing CI
24514 b-mehta chore(Int/GCD): use fuel in xgcd awaiting-author t-data merge-conflict ??? missing CI information
32169 saodimao20 feat: add convolution_comp_add_right t-analysis new-contributor awaiting-author 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 t-category-theory awaiting-CI large-import merge-conflict ??? blocked on another PR
31135 kckennylau feat(RingTheory): is localization iff is localization on saturation merge-conflict blocked-by-other-PR ⚠️ blocked on another PR
29934 smmercuri feat(Field/WithAbs): the lift of a ring homomorphism from `WithAbs v` to `WithAbs w` to their completions merge-conflict WIP 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` t-analysis t-measure-probability awaiting-author awaiting author
27980 smmercuri feat: dimensions of completions at infinite place extensions t-number-theory blocked-by-other-PR large-import merge-conflict FLT blocked on another PR
31350 grunweg feat: (unoriented) bordism groups merge-conflict WIP t-differential-geometry blocked-by-other-PR blocked on another PR
26389 jjdishere feat(RingTheory): Perfectoid Field t-algebra WIP t-topology t-analysis labelled WIP
26390 jjdishere feat(Topology/Algebra): Krasner's lemma WIP t-number-theory t-algebra t-topology labelled WIP
26961 mariainesdff feat(RingTheory/PowerSeries/Substitution): add API awaiting-author t-ring-theory failing CI
32285 awainverse chore(ModelTheory/Bundled): Replace CategoryTheory.Bundled t-logic awaiting-author awaiting author
31663 xroblot feat(Algebra): more instances about `min`, `max`, `iSup` and `iInf` of sub-algebras t-algebra WIP 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 t-category-theory merge-conflict labelled WIP
26464 joelriou feat(LinearAlgebra): generators of pi tensor products file-removed awaiting-author t-algebra merge-conflict failing CI
29393 staroperator feat(SetTheory/ZFC): `card (V_ o) = preBeth o` large-import t-set-theory awaiting review
30582 RemyDegenne feat: extension of a function to the closure of a submodule t-topology WIP labelled WIP
27579 RemyDegenne feat: risk of an estimator, DeGroot statistical information, total variation distance WIP large-import t-measure-probability labelled WIP
32269 EtienneC30 feat: introduce Gaussian processes brownian t-measure-probability blocked-by-other-PR 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 t-algebra RFC merge-conflict 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 t-order awaiting-author merge-conflict merge conflict
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 new-contributor t-ring-theory awaiting-author failing CI
31597 grunweg chore(AtLocation): allow throwing a warning when no progress is being made awaiting-author t-meta merge-conflict merge conflict
30439 plp127 feat: `norm_num` extension for `IsSquare` on `Nat`, `Int`, `Rat` merge-conflict awaiting-author t-meta merge conflict
30525 515801431 feat(Mathlib/Combinatorics/Enumerative/Polya): Add Polya Counting t-combinatorics new-contributor awaiting-author merge-conflict merge conflict
31113 515801431 feat(Mathlib/Combinatorics/Enumerative/Polya.lean): Add additional theorem in `Polya.lean` t-combinatorics new-contributor blocked-by-other-PR merge-conflict blocked on another PR
29000 JovanGerb feat(Tactic/Push): add basic tags and tests merge-conflict blocked-by-other-PR ⚠️ blocked on another PR
24441 MrSumato feat(Data/List): add Lyndon-Schutzenberger theorem on list commutativity merge-conflict awaiting-author t-data new-contributor ??? missing CI information
32125 SnirBroshi feat(SimpleGraph/Walks/Subwalks): `p₁.IsSubwalk p₂ ↔ p₁.darts <:+: p₂.darts` and similar theorems t-combinatorics blocked-by-other-PR blocked on another PR
28468 alreadydone feat(Algebra): ring API for `AddLocalization` t-algebra awaiting-author large-import awaiting author
28057 plp127 feat(SuccOrder): simp lemma to refold `Order.succ` and `Order.pred` awaiting-author t-order merge-conflict merge conflict
31901 callesonne feat(Bicategory/Subbicategory): add full subbicategories using `ObjectProperty` t-category-theory awaiting-author awaiting author
32326 chrisflav feat(Algebra/ModuleCat): extension of scalars is comonadic for a faithfully flat algebra t-ring-theory awaiting-author awaiting author
32473 mattrobball chore(Kaehler.JacobiZariski): remove egregious local instance hack t-ring-theory awaiting-author awaiting author
18551 joelriou feat(AlgebraicGeometry): the algebraic De Rham complex WIP t-algebra blocked-by-other-PR merge-conflict t-algebraic-geometry blocked on another PR
24434 joelriou feat(CategoryTheory): effectiveness of descent merge-conflict WIP t-category-theory labelled WIP
32374 adamtopaz feat(Tactic/WildcardUniverse): Foo.{*, _, v*, max u v} t-meta 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 t-dynamics new-contributor awaiting-author awaiting author
29354 themathqueen refactor(Algebra/Algebra/Equiv): allow for non-unital `AlgEquiv` t-algebra awaiting-author merge-conflict 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 file-removed merge-conflict failing CI
30119 Ruben-VandeVelde feat: WithTop/Bot.mapD awaiting-author t-order merge-conflict merge conflict
32458 vihdzp feat: order isomorphisms preserve successor/predecessor limits t-order awaiting-author awaiting author
28613 espottesmith feat(Combinatorics): define undirected hypergraphs t-combinatorics new-contributor merge-conflict failing CI
24000 YaelDillies feat: correspondence between affine group schemes and Hopf algebras WIP t-algebraic-geometry toric FLT labelled WIP
23040 grunweg feat: define immersions and smooth embeddings in infinite dimensions merge-conflict WIP t-differential-geometry blocked-by-other-PR ??? blocked on another PR
26231 chrisflav feat(CategoryTheory/Sites): sheaf condition and coproducts awaiting-author t-category-theory WIP labelled WIP
10991 thorimur feat: `tfae` block tactic merge-conflict WIP modifies-tactic-syntax t-meta ??? labelled WIP
30668 astrainfinita feat: `QuotType` RFC t-data awaiting-zulip awaiting a zulip discussion
32278 jsm28 feat(Geometry/Euclidean/Incenter): excenters on sides of faces t-euclidean-geometry blocked-by-other-PR blocked on another PR
32556 vihdzp doc: fix URL in docs documentation awaiting-author awaiting author
30847 joelriou feat(CategoryTheory/Presentable): the representation theorem WIP blocked-by-other-PR t-category-theory merge-conflict blocked on another PR
30620 plp127 feat: copy LE and LT on preorder and partial order t-order awaiting-author merge-conflict merge conflict
30853 JovanGerb feat(LinearAlgebra/AffineSpace/Simplex): `CoeFun` instance for `Simplex` awaiting-author t-euclidean-geometry merge-conflict merge conflict
30817 joelriou feat(CategoryTheory): `κ`-continuous presheaves WIP t-category-theory blocked-by-other-PR blocked on another PR
30185 alreadydone feat(MathlibTest): kernel reduction of nsmul on elliptic curve over ZMod t-algebra t-number-theory blocked-by-other-PR t-algebraic-geometry merge-conflict blocked on another PR
6633 adomani feat(..Polynomial..): `MvPolynomial`s have no zero divisors merge-conflict awaiting-author t-algebra ??? missing CI information
31508 FLDutchmann feat(Tactic): `algebra` tactic. t-meta awaiting-author awaiting author
28865 grunweg feat: a map is smooth iff its post-composition with an immersion is merge-conflict WIP t-differential-geometry blocked-by-other-PR ??? blocked on another PR
32609 PrParadoxy feat(LinearAlgebra/PiTensorProduct): Relation between nested tensor products and tensor products indexed by dependent sums new-contributor blocked-by-other-PR ⚠️ blocked on another PR
29508 zhuyizheng feat(MeasureTheory): FTC and integration by parts for absolutely continuous functions t-measure-probability new-contributor awaiting-author merge-conflict merge conflict
30666 erdOne feat(NumberTheory): every number field has a ramified prime t-number-theory awaiting-author t-algebra merge-conflict failing CI
30811 yonggyuchoimath feat(AlgebraicGeometry.EffectiveEpi): effective epimorphisms in schemes blocked-by-other-PR merge-conflict ⚠️ blocked on another PR
30329 luigi-massacci feat(Analysis/Distribution/TestFunction): integrating against a measure as a continuous linear map on test functions merge-conflict blocked-by-other-PR ⚠️ blocked on another PR
30327 luigi-massacci feat(Analysis/Distribution/TestFunction): add characterizations of continuity for linear maps on test functions merge-conflict blocked-by-other-PR ??? ⚠️ blocked on another PR
30255 luigi-massacci feat(Analysis/Distribution/ContDiffMapSupportedIn): specialize singleton seminorm family for D_K^n when n finite merge-conflict blocked-by-other-PR ??? ⚠️ 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
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 t-set-theory new-contributor awaiting review
32334 EtienneC30 feat: independence of Gaussian processes brownian t-measure-probability blocked-by-other-PR merge-conflict blocked on another PR
32704 euprunin chore: remove use of `erw` awaiting-author t-topology t-category-theory t-measure-probability awaiting author
31987 saodimao20 feat: add monotonicity and relation lemmas for mgf and cgf t-measure-probability new-contributor awaiting-author awaiting author
32600 PrParadoxy feat(LinearAlgebra/Multilinear): composition of multilinear maps new-contributor ??? ⚠️ missing CI information
29764 ScottCarnahan feat(Algebra/Vertex): API up to residue products (WIP) t-algebra blocked-by-other-PR large-import blocked on another PR
32147 EtienneC30 feat: independence of Gaussian random variables brownian t-measure-probability blocked-by-other-PR merge-conflict blocked on another PR
31766 SuccessMoses feat(Topology/EMetricSpace): continuity of arc length new-contributor t-topology awaiting-author awaiting author
30505 mariainesdff feat(NumberTheory/RatFunc/Ostrowski): prove Ostrowski's theorem for K(X) t-algebra awaiting-author t-number-theory merge-conflict failing CI
31965 bwangpj feat: fiber of RingHom.specComap t-ring-theory awaiting-author merge-conflict 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 t-analysis blocked-by-other-PR merge-conflict 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 ??? missing CI information
28291 vasnesterov feat(Tactic): tactic for computing asymptotics of real functions WIP t-analysis t-meta large-import labelled WIP
30240 luigi-massacci feat(Analysis/Distribution/ContDiffMapSupportedIn): Add a wrapper for fderiv on D_K^n t-analysis awaiting-author ??? missing CI information
32828 Hagb feat(Algebra/Order/Group/Defs): add `IsOrderedAddMonoid.toIsOrderedCancelAddMonoid'` t-algebra ??? missing CI information
29274 Jlh18 feat(CategoryTheory): HasLimits instance on Grpd file-removed blocked-by-other-PR t-category-theory merge-conflict blocked on another PR
29283 Jlh18 feat(CategoryTheory): define forgetful-core adjunction between Cat and Grpd file-removed t-category-theory awaiting-author merge-conflict ??? missing CI information
28248 YaelDillies feat: binomial random variables t-measure-probability failing CI
30920 callesonne feat(Category/Grpd): define the bicategory of groupoids t-category-theory large-import merge-conflict 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 t-topology large-import merge-conflict merge conflict
21447 erdOne feat(AlgebraicGeometry): the split algebraic torus merge-conflict awaiting-author t-algebraic-geometry ??? missing CI information
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 t-convex-geometry awaiting-author merge-conflict merge conflict
25963 artie2000 refactor(Algebra): uniform API for substructures merge-conflict WIP t-algebra labelled WIP
32845 jonasvanderschaaf feat(CategoryTheory): `GrothendieckTopology.yoneda` preserves certain (co)limits new-contributor WIP ⚠️ labelled WIP
31662 edwin1729 feat(Topology/Order): topological basis of scott topology on Complete… t-topology new-contributor awaiting-author blocked-by-other-PR blocked on another PR
32679 YaelDillies chore(Data/Sym2): improve defeq of `diagSet` t-data awaiting review
32938 0xTerencePrime feat(Order/LocallyFinite): prove DenselyOrdered and LocallyFiniteOrder are incompatible t-order new-contributor awaiting-author awaiting author
33077 YaelDillies feat(Data/Rel): balls WIP t-data labelled WIP
31226 erdOne chore(RingTheory): add `@[ext]` to `Ideal.Quotient.algHom_ext` awaiting-author t-ring-theory easy merge-conflict merge conflict
28246 Sebi-Kumar feat(AlgebraicTopology/FundamentalGroupoid): the n-sphere is simply connected for n > 1 merge-conflict t-algebraic-topology blocked-by-other-PR new-contributor blocked on another PR
21495 alreadydone experiment: reducible HasQuotient.quotient' WIP bench-after-CI merge-conflict 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 t-computability new-contributor maintainer-merge awaiting review
32698 farruhx feat(List): add aesop / simp annotations to selected lemmas for improved automation t-data new-contributor awaiting-author 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 t-data new-contributor awaiting review
32127 CoolRmal feat: use IndexedPartition.piecewise to create simple/measurable/strongly measurable functions brownian t-measure-probability large-import awaiting review
27817 zhuyizheng feat: add IMO2025P1 IMO awaiting-author new-contributor merge-conflict merge conflict
24383 YaelDillies feat: distributive Haar characters of `ℝ` and `ℂ` WIP awaiting-CI t-measure-probability file-removed FLT 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 t-algebra large-import merge-conflict looking for help
32983 JovanGerb feat: use `LE.le` for subset relation in `Set`, `Finset`, `PSet`, `ZFSet` merge-conflict ⚠️ failing CI
31377 CoolRmal feat: a series of smooth functions that converges (locally) uniformly is smooth t-topology new-contributor awaiting-author failing CI
26923 oliver-butterley feat(Dynamics/BirkhoffSum): add the pointwise ergodic theorem (Birkhoff's) t-dynamics new-contributor awaiting-author 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
33082 AntoineChambert-Loir feat(GroupTheory/SpecificGroups/Alternating/Simple): the alternating group on at least 5 letters is simple. t-group-theory large-import 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 t-algebraic-topology WIP t-topology merge-conflict labelled WIP
33218 Blackfeather007 feat(Algebra): Define the associated graded ring to filtered ring t-ring-theory new-contributor blocked-by-other-PR blocked on another PR
33219 Blackfeather007 feat(Algebra): Define associated graded algebra t-ring-theory new-contributor blocked-by-other-PR blocked on another PR
33220 Blackfeather007 feat(Algebra): Define associated graded module t-ring-theory new-contributor blocked-by-other-PR blocked on another PR
33227 Blackfeather007 feat(Algebra): exact of associated graded exact t-ring-theory new-contributor blocked-by-other-PR blocked on another PR
33226 Blackfeather007 feat(Algebra): associated graded exact of exact and strict t-ring-theory new-contributor blocked-by-other-PR blocked on another PR
33225 Blackfeather007 feat(Algebra): filtered module hom t-ring-theory new-contributor blocked-by-other-PR blocked on another PR
33224 Blackfeather007 feat(Algebra): define filtered alghom t-ring-theory new-contributor blocked-by-other-PR blocked on another PR
33223 Blackfeather007 feat(Algebra): define filtered ring homomorphism t-ring-theory new-contributor blocked-by-other-PR blocked on another PR
33222 Blackfeather007 feat(Algebra): define filtered add group hom new-contributor t-ring-theory blocked-by-other-PR blocked on another PR
30880 themathqueen feat(Analysis/InnerProductSpace): finite-dimensional inner product space with an algebra implies a coalgebra t-analysis delegated 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 new-contributor t-analysis awaiting-author awaiting author
33126 CoolRmal feat: function composition preserves boundedness t-order awaiting review
25834 Rida-Hamadani feat(SimpleGraph): girth-diameter inequality merge-conflict WIP blocked-by-other-PR t-combinatorics blocked on another PR
28462 joelriou feat(AlgebraicTopology/SimplicialSet): the relative cell complex attached to a rank function for a pairing t-algebraic-topology WIP labelled WIP
33249 Rida-Hamadani feat(SimpleGraph): `take` is path if original walk is path blocked-by-other-PR t-combinatorics ??? blocked on another PR
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` t-measure-probability tech debt awaiting-author 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
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 t-order awaiting-CI merge-conflict blocked on another PR
33313 SnirBroshi feat(Combinatorics/SimpleGraph/EdgeColoring): create a basic edge-coloring API large-import t-combinatorics blocked-by-other-PR blocked on another PR
5934 eric-wieser feat: port Data.Rat.MetaDefs merge-conflict help-wanted mathlib-port 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 please-adopt WIP t-algebra merge-conflict ??? looking for help
32270 jsm28 feat(Geometry/Euclidean/Incenter): `map` and `restrict` lemmas t-euclidean-geometry blocked-by-other-PR ??? blocked on another PR
4127 kmill refactor: create HasAdj class, define Digraph, and generalize some SimpleGraph API merge-conflict awaiting-author t-combinatorics ??? missing CI information
27752 plp127 feat(Order): `NoBotOrder α` implies `NoMinOrder α` under `IsDirected α (· ≥ ·)` awaiting-author t-order merge-conflict failing CI
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 t-logic new-contributor blocked-by-other-PR ??? blocked on another PR
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 t-algebra merge-conflict labelled WIP
33189 peabrainiac feat(Geometry/Manifold): the interior of a manifold is open t-differential-geometry awaiting-author awaiting author
32889 artie2000 feat(Algebra): forgetful lemmas for `map` and `comap` on substructures t-algebra awaiting-author blocked-by-other-PR merge-conflict blocked on another PR
32960 dleijnse feat(FieldTheory): adjoin pth roots t-algebra new-contributor awaiting-author awaiting author
33163 Aaron1011 feat: prove subgroup of (M -> Z) is finitely generated t-ring-theory new-contributor awaiting-author awaiting author
33217 Blackfeather007 feat(Algebra): define associated graded structure for abelian group new-contributor t-ring-theory awaiting-author awaiting author
32987 kim-em feat: pipeline downloads and decompression in `cache get` ⚠️ awaiting review
25481 kbuzzard chore: refactor Algebra.TensorProduct.rightAlgebra t-algebra failing CI
28972 themathqueen feat(LinearAlgebra/Matrix): star-algebra automorphisms on matrices are unitarily inner t-algebra t-analysis awaiting-author awaiting author
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 merge-conflict awaiting-author t-meta ??? missing CI information
30391 rudynicolop feat(Data/List): list splitting definitions and lemmas t-data new-contributor awaiting review
25138 chrisflav chore(RingTheory/Ideal): make `RingHom.ker` take a `RingHom` instead of `RingHomClass` t-algebra awaiting-author merge-conflict 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 t-algebraic-topology WIP RFC 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
33021 farmanb feat(RingTheory/IdealFilter): add ideal filters and Gabriel filters t-ring-theory new-contributor blocked-by-other-PR ??? blocked on another PR
24665 Komyyy feat(Mathlib/Topology/Metrizable/Uniformity): every uniform space is generated by a family of pseudometrics WIP t-topology merge-conflict ??? labelled WIP
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 t-analysis blocked-by-other-PR merge-conflict blocked on another PR
33080 sinhp feat(Category Theory): Cartesian Natural Transformation t-category-theory awaiting-author awaiting author
33394 dupuisf feat: add lemmas about doubly stochastic matrices t-analysis awaiting-author ??? missing CI information
33448 astrainfinita refactor: deprecate `ContinuousLinearMapClass` t-topology t-algebra awaiting-author awaiting author
21031 YaelDillies chore: get rid of generic hom coercions WIP labelled WIP
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 t-category-theory awaiting-author awaiting author
32840 joelriou chore(CategoryTheory): remove the old Ext API file-removed t-category-theory large-import merge-conflict WIP labelled WIP
33133 0xTerencePrime feat(Algebra/Group/Center): add Decidable (IsMulCentral a) instance t-algebra new-contributor awaiting-author awaiting author
33276 NicolaBernini feat: Rename List.reverse_perm to List.reverse_perm_self and List.reverse_perm' to List.reverse_perm_iff new-contributor awaiting-author ⚠️ awaiting author
33351 themathqueen chore(Analysis/LocallyConvex/SeparatingDual): generalize `Algebra.IsCentral.instContinuousLinearMap` t-analysis awaiting-author awaiting author
33191 sinhp feat(CategoryTheory): Locally cartesian closed structure on presheaf categories WIP t-category-theory blocked-by-other-PR merge-conflict blocked on another PR
33495 vihdzp chore(RingTheory/HahnSeries/Basic): redefine `order` using `unbotD` t-ring-theory blocked-by-other-PR blocked on another PR
28153 kckennylau feat(Simproc): Simproc for explicit diagonal matrices merge-conflict awaiting-author t-meta merge conflict
25500 eric-wieser feat: delaborators for metadata large-import merge-conflict awaiting-author delegated t-meta merge conflict
28191 kckennylau feat(Logic): tag Injective, Surjective, and Bijective with fun_prop merge-conflict awaiting-author 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 t-meta awaiting-author 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 failing CI
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-algebra t-category-theory awaiting review
33256 joelriou feat(CategoryTheory/Sites): characterization of (pre)stacks for a precoverage WIP t-category-theory blocked-by-other-PR blocked on another PR
32389 LLaurance feat(Analysis): Trigonometric identities t-analysis awaiting-author 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 t-analysis awaiting-author awaiting author
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 new-contributor t-meta WIP labelled WIP
22657 Xmask19 feat: a graph is maximally acyclic iff it is a tree merge-conflict t-combinatorics new-contributor failing CI
33416 vihdzp chore(Order/GameAdd): add `elab_as_elim` attributes t-order awaiting review
33475 BoltonBailey feat(Logic/IsEmpty): add theorems relating surjectivity and emptiness t-logic awaiting review
33247 sun123zxy feat(Mathlib/RingTheory/Ideal/Cotangent): dimension of cotangent spaces file-removed new-contributor t-ring-theory blocked-by-other-PR WIP merge-conflict blocked on another PR
26368 Whysoserioushah feat(RingTheory/TwoSidedIdeal/SpanAsSum): span of set as finsum merge-conflict awaiting-author 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 t-euclidean-geometry awaiting-author awaiting author
33375 kex-y feat(Probability): Local and stable properties brownian t-measure-probability blocked-by-other-PR blocked on another PR
31719 maksym-radziwill feat: Borel-Caratheodory (2nd revision) awaiting-author t-analysis failing CI
28013 astrainfinita feat: Lindemann-Weierstrass Theorem t-algebra t-analysis awaiting-author merge-conflict failing CI
32886 alreadydone refactor(Algebra/Order): change `MulArchimedeanClass.subgroup` to `FiniteArchimedeanClass.subgroup` t-algebra t-order awaiting review
31361 alreadydone feat(Algebra/Order): convex subgroups t-algebra t-order blocked-by-other-PR merge-conflict 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ᵐᵒᵖ` t-algebra t-group-theory awaiting-author 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 t-euclidean-geometry blocked-by-other-PR ??? blocked on another PR
32294 jsm28 feat(Geometry/Euclidean/Angle/Incenter): distance from second intersection with circumcircle t-euclidean-geometry blocked-by-other-PR ??? blocked on another PR
30981 jsm28 feat(Geometry/Euclidean/Angle/Bisector): oriented angle bisection mod π t-euclidean-geometry ??? missing CI information
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 t-analysis WIP t-algebraic-topology awaiting-author labelled WIP
33039 euprunin chore(Data/List): deprecate `ext_get_iff` t-data awaiting review
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 new-contributor t-number-theory awaiting-author awaiting author
33601 nielstron feat(Computability/ContextFreeGrammar): Concatenation of CFGs is CFG t-computability new-contributor blocked-by-other-PR blocked on another PR
29624 mcdoll feat(LinearAlgebra/LinearPMap): add definition of resolvent and first resolvent identity t-algebra t-analysis awaiting-author failing CI
33599 nielstron feat(Computability/ContextFreeGrammar): closure under union t-computability new-contributor awaiting review
30375 sinhp feat(CategoryTheory): Basics of Locally Cartesian Closed Categories t-category-theory merge-conflict ??? missing CI information
32991 artie2000 chore(Algebra/Algebra): remove `Algebra.cast` coercion t-algebra merge-conflict failing CI
27972 smmercuri refactor: make `Valuation.Completion` a `def` and refactor more of `AdicValuation.lean` WIP t-number-theory t-algebra merge-conflict labelled WIP
32585 CBirkbeck feat(NumberTheory/ModularForms/EisensteinSeries/E2/Transform): E2 under the action of SL2 ⚠️ awaiting review
33490 YaelDillies refactor(Data/Finsupp): remove `DecidableEq` argument from `curry` CFT t-data awaiting review
17176 arulandu feat: integrals and integrability with .re merge-conflict awaiting-author new-contributor t-measure-probability please-adopt ??? looking for help
32918 michelsol feat: define `supEdist` and `supDist` t-topology new-contributor merge-conflict 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 t-order awaiting-CI 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 t-ring-theory large-import awaiting-author WIP blocked-by-other-PR 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. new-contributor blocked-by-other-PR merge-conflict ⚠️ 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` t-analysis large-import blocked-by-other-PR blocked on another PR
31219 Thmoas-Guan feat(Algebra): lemma about `IsBaseChange` under exact sequence t-ring-theory awaiting-author 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 t-algebra blocked-by-other-PR large-import blocked on another PR
26216 Thmoas-Guan feat(Algebra): depth of QuotSMulTop t-algebra blocked-by-other-PR large-import blocked on another PR
32000 Thmoas-Guan feat(Algebra): projective dimension equal supremum of localized module ⚠️ failing CI
31697 Thmoas-Guan feat(Homology): bijection between `Ext` t-algebra blocked-by-other-PR t-category-theory blocked on another PR
31768 Thmoas-Guan feat(Homology): `Ext` commute with ulift functor t-algebra blocked-by-other-PR t-category-theory blocked on another PR
33061 edwin1729 refactor: generalise compact from CompleteLattice to PartialOrder new-contributor awaiting-author awaiting author
32081 Thmoas-Guan feat(RingTheory/Homology): `Ext` over Noetherian ring finitely generated t-algebra blocked-by-other-PR t-category-theory blocked on another PR
31879 Thmoas-Guan feat(Algebra/Homology): Projective dimension in linear equiv t-algebra blocked-by-other-PR blocked on another PR
32058 Thmoas-Guan feat(Algebra): category version Baer criterion t-algebra t-category-theory awaiting-author blocked-by-other-PR blocked on another PR
26215 Thmoas-Guan feat(Algebra): Auslander–Buchsbaum theorem t-algebra blocked-by-other-PR large-import blocked on another PR
26217 Thmoas-Guan feat(Algebra): Ischebeck theorem t-algebra blocked-by-other-PR large-import blocked on another PR
26212 Thmoas-Guan feat(Algebra): the Rees theorem for depth large-import awaiting-author t-ring-theory ??? missing CI information
26218 Thmoas-Guan feat(Algebra): definition of cohen macaulay t-algebra blocked-by-other-PR large-import blocked on another PR
28599 Thmoas-Guan feat(RingTheory): polynomial over CM ring is CM WIP t-ring-theory large-import labelled WIP
26245 Thmoas-Guan feat(Algebra): cohen macaulay local ring is catenary WIP t-algebra blocked-by-other-PR large-import blocked on another PR
26957 Thmoas-Guan feat(Algebra): unmixed thm of Cohen-Macaulay ring t-algebra blocked-by-other-PR large-import blocked on another PR
31851 Thmoas-Guan feat(Algebra/Homology): Injective dimension in linear equiv t-algebra blocked-by-other-PR blocked on another PR
31644 Thmoas-Guan feat(Algebra): projective dimension of quotient regular sequence awaiting-author t-ring-theory blocked-by-other-PR 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 t-ring-theory awaiting-author 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 large-import blocked-by-other-PR ⚠️ blocked on another PR
33377 Thmoas-Guan feat(RingTheory): polynomial over Gorenstein ring is Gorenstein large-import blocked-by-other-PR ⚠️ blocked on another PR
33379 Thmoas-Guan feat(RingTheory): Gorenstein local ring is Cohen Macaulay large-import blocked-by-other-PR ⚠️ blocked on another PR
33380 Thmoas-Guan feat(RingTheory): Gorenstein local ring is Cohen--Macaulay local ring of type one large-import blocked-by-other-PR ⚠️ blocked on another PR
28684 Thmoas-Guan feat(RingTheory): definition of regular ring t-ring-theory blocked-by-other-PR blocked on another PR
28683 Thmoas-Guan feat(RingTheory): regular local ring is domain t-ring-theory blocked-by-other-PR blocked on another PR
28582 Thmoas-Guan feat(Data): some lemmas about WithBot ENat t-data awaiting-author ??? missing CI information
33257 NickAdfor feat(Combinatorics/SimpleGraph/Bipartite): Odd Cycle Theorem (A Solution to TODO) t-combinatorics new-contributor awaiting-author awaiting author
29533 Thmoas-Guan feat(Algebra): maximal Cohen Macaulay module blocked-by-other-PR 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 t-ring-theory blocked-by-other-PR WIP blocked on another PR
33032 ksenono feat(Combinatorics/SimpleGraph): Konig’s theorem on bipartite graphs t-combinatorics new-contributor blocked-by-other-PR merge-conflict blocked on another PR
29558 Thmoas-Guan feat(Algebra): definition of global dimension t-ring-theory blocked-by-other-PR blocked on another PR
31999 Thmoas-Guan feat(RingTheory): global dimension equals the supremum over localizations awaiting-author blocked-by-other-PR ⚠️ 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) blocked-by-other-PR large-import WIP ⚠️ blocked on another PR
33592 nielstron feat(Computability/ContextFreeGrammar): mapping between two types of nonterminal symbols t-computability new-contributor ??? missing CI information
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
33286 euprunin chore: golf using `grind` awaiting review
33464 Paul-Lez feat(Analysis/ODE/Gronwall): Add two easy lemmas t-analysis awaiting-author awaiting author
33454 astrainfinita feat: lemmas about `IsometryClass` t-topology t-analysis awaiting-author awaiting author
13740 YaelDillies feat: more robust ae notation t-meta t-measure-probability awaiting-author awaiting author
32165 yuanyi-350 feat(Real/Trigonometric): Add `sum_cos_arith_progression` and prepare for Dirichlet kernel t-analysis awaiting-author merge-conflict merge conflict
33050 mkaratarakis feat: lemmas for the analytic part of the proof of the Gelfond–Schneider theorem t-number-theory new-contributor awaiting-author awaiting author
33691 kim-em feat(scripts): add find-ci-errors.sh to diagnose widespread CI failures CI delegated delegated
33389 khwilson feat(Mathlib/Analysis/SpecialFunctions/Log/Base): More log asymptotics t-analysis new-contributor awaiting-author awaiting author
33368 urkud feat: define `Complex.UnitDisc.shift` t-analysis awaiting-zulip merge-conflict ??? missing CI information
33450 astrainfinita refactor: deprecate `LinearIsometryClass` t-algebra t-analysis blocked-by-other-PR t-topology merge-conflict blocked on another PR
33295 AntoineChambert-Loir feat(Algebra/Central/End): center of the group of automorphisms of a free module t-algebra WIP labelled WIP
33702 JovanGerb doc(Algebra/Quotient): update `HasQuotient.Quotient` doc-string t-algebra delegated delegated
32583 MJ141592 refactor(SimpleGraph): change bridges not to require the edge to be present t-combinatorics new-contributor awaiting-author 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 t-ring-theory awaiting-author awaiting author
33192 linesthatinterlace refactor(Data/List/Induction): improve definition of `reverseRecOn` t-data awaiting review
31607 grunweg chore: rename `continuous{,On,At,Within}_const to `ContinuousFoo.const` delegated awaiting-CI merge-conflict does not pass CI
33554 themathqueen chore(Analysis/Normed/Module/Normalize): allow for `RCLike` instead of just the reals t-analysis awaiting-author merge-conflict merge conflict
31754 dagurtomas feat(Topology/Category): light profinite sets are injective objects t-topology t-category-theory merge-conflict merge conflict
33561 kbuzzard chore: cont -> continuous_toFun merge-conflict merge conflict
26299 adomani perf: the `commandStart` linter only acts on modified files t-linter awaiting-author merge-conflict merge conflict
27507 grunweg wip(commandStart): check the indentation of declaration keywords also WIP t-linter merge-conflict labelled WIP
26088 grunweg chore(Linter/DirectoryDependency): move forbidden directories into a JSON file please-adopt t-linter merge-conflict looking for help
28708 sjh227 feat(LinearAlgebra): define row- and column-stochastic matrices t-data new-contributor 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 ??? missing CI information
33436 astrainfinita feat: lemmas about `(Add)MonoidAlgebra.mapRangeRingHom` t-algebra awaiting review
33330 michael-novak-math feat: add arc-length reparametrization of parametrized curves t-analysis new-contributor merge-conflict merge conflict
33707 jcommelin ci: add commit verification for transient and automated commits CI merge-conflict ??? missing CI information
32617 erdOne feat(RingTheory): field extension over perfect fields are smooth t-ring-theory awaiting review
33033 kim-em feat(Tactic/Choose): add type annotation support t-meta awaiting review
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
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… merge-conflict please-adopt WIP blocked-by-other-PR t-measure-probability blocked on another PR
30855 Ruben-VandeVelde fix: deprecate IsTotal in favour of Std.Total t-order merge-conflict RFC merge conflict
24065 kim-em chore: script to give topological sort of modules awaiting-author ??? missing CI information
28700 Timeroot feat(ModelTheory): Set.Definable is transitive merge-conflict large-import t-logic merge conflict
30608 grunweg feat: another lemma about derivatives of parametric integrals merge-conflict awaiting-author t-analysis ??? missing CI information
30610 grunweg feat: yet another lemma about differentiability of parametric integrals merge-conflict blocked-by-other-PR t-analysis blocked on another PR
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 new-contributor t-order awaiting author
33359 sun123zxy feat(Algebra/Module/SpanRank): add comparing lemmas for span rank t-algebra new-contributor 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
32190 vihdzp chore(Algebra/Order/Ring/Archimedean): generalize theorems to `OrderHomClass` + `RingHomClass` t-algebra failing CI
32672 tb65536 feat: haar measures on short exact sequences t-measure-probability t-topology FLT awaiting review
31141 peabrainiac feat(Analysis/Calculus): parametric integrals over smooth functions are smooth t-analysis awaiting-author merge-conflict merge conflict
33749 plp127 feat: `NNRat` is countable t-data large-import awaiting review
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 t-data new-contributor awaiting review
33635 plp127 feat(Tactic/Set): use `binderIdent` instead of `ident` t-meta awaiting review
30204 yonggyuchoimath feat(Algebra/Category/Ring/EqualizerPushout): add effectiveEpi_of_faithfullyFlat in CommRingCatᵒᵖ blocked-by-other-PR ⚠️ blocked on another PR
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 t-ring-theory large-import awaiting-author WIP labelled WIP
32744 NoneMore feat(ModelTheory/Definablity): add `DefinableFun` definition and lemmas new-contributor t-logic awaiting review
33555 erdOne feat(RingTheory): standard smooth = etale over mvpolynomial large-import ⚠️ awaiting review
32215 jonasvanderschaaf feat(ModelTheory/Types): Construct a topology on CompleteType and prove the space is TotallySeparated new-contributor t-topology t-logic failing CI
33403 xroblot feat(GroupTheory/FiniteAbelian): prove that the restriction map is surjective t-group-theory ??? missing CI information
30142 shalliso feat(Topology/Baire): define IsNonMeagre t-topology new-contributor merge-conflict failing CI
33792 xroblot feat(GroupTheory/FiniteAbelian): construct bijection between subgroups and subgroups of the dual t-group-theory blocked-by-other-PR ??? blocked on another PR
31925 alreadydone feat(Topology): étalé space associated to a predicate on sections t-topology blocked-by-other-PR ??? 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
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 new-contributor t-algebraic-topology awaiting-author awaiting author
32856 stepan2698-cpu feat: definition of an irreducible representation t-algebra new-contributor awaiting review
33518 joelriou feat(CategoryTheory/Sites): fullness of `DescentData.pullFunctor` awaiting-author t-category-theory awaiting author
30640 SnirBroshi feat(Combinatorics/SimpleGraph/Acyclic): acyclic and bridge theorems t-combinatorics awaiting review
22366 kim-em feat: `check_equalities` tactic for diagnosing defeq problems delegated t-meta merge-conflict failing CI
30579 smmercuri feat : `v.adicCompletionIntegers K` is compact when `K` is a number field WIP merge-conflict blocked-by-other-PR large-import ⚠️ blocked on another PR
31755 kaantahti feat(Combinatorics): Add Sperner's Lemma formalization t-combinatorics new-contributor WIP merge-conflict labelled WIP
31809 ADedecker feat: differentiation of test function as a CLM blocked-by-other-PR t-analysis merge-conflict blocked on another PR
32210 ADedecker feat: iteratedFDeriv as a linear map on test functions merge-conflict t-analysis awaiting-author merge conflict
32305 faenuccio feat: define Sobolev Spaces merge-conflict WIP t-analysis large-import blocked-by-other-PR blocked on another PR
32401 ADedecker feat: monotonicity of D^n(U) in n and in U as CLMs merge-conflict t-analysis delegated merge conflict
32410 callesonne feat(Bicategory/FunctorCategory/Pseudo): Add evaluation pseudofunctor merge-conflict WIP t-category-theory blocked-by-other-PR blocked on another PR
33240 khwilson feat(Mathlib/Analysis/Polynomial/Norm): Introduce Polynomial.supNorm merge-conflict t-analysis new-contributor awaiting-author merge conflict
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 merge-conflict t-algebra file-removed blocked-by-other-PR ??? blocked on another PR
33715 AntoineChambert-Loir feat(LinearAlgebra/Projectivization/Action): prove that the action is 2-transitive and primitive merge-conflict file-removed blocked-by-other-PR t-algebra large-import ??? 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 new-contributor t-measure-probability blocked on another PR
30562 dwrensha fix(Data/Fintype/Perm): make the main logic of Equiv.instFintype irreducible awaiting-author t-data failing CI
33594 smmercuri feat: `HeightOneSpectrum.valuation` is rank one for number fields large-import ⚠️ 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
33688 Citronhat feat(PMF): add expectation lemmas for Poisson PMF new-contributor t-measure-probability awaiting review
31180 CoolRmal feat(Analysis): a closed convex set is the intersection of countably many half-spaces in a separable Banach space t-analysis new-contributor awaiting-author failing CI
33669 eric-wieser chore(Data/Nat/Digits): refactor to use List.rightpad large-import merge-conflict failing CI
32541 YaelDillies chore: import Tactic.Attr.Register privately large-import failing CI
33348 AntoineChambert-Loir feat(LinearAlgebra/Transvection): characterization of transvections among dilatransvections t-algebra blocked-by-other-PR ??? blocked on another PR
33493 michelsol feat(RingTheory/Polynomial): An explicit formula for the Chebyshev polynomials of the first kind t-ring-theory new-contributor awaiting review
29960 yonggyuchoimath feat(Algebra/Category/Ring): equalizers of pushout maps of tensor product inclusions new-contributor awaiting-author t-ring-theory awaiting author
33604 xgenereux feat(ValuationSubring): eq_top_iff + qol changes t-ring-theory ??? missing CI information
33612 xgenereux feat(ValuationSubring): fieldTop t-ring-theory awaiting review
31795 thorimur feat: turn on `unusedFintypeInType` linter blocked-by-other-PR merge-conflict file-removed ⚠️ blocked on another PR
33049 xgenereux feat: Valuation.IsTrivialOn t-ring-theory failing CI
33658 vihdzp refactor(RingTheory/Valuation/ValuativeRel/Basic): fix theorem names for multiplication t-ring-theory awaiting review
25905 mans0954 feat(RingTheory/Polynomial/SmallDegreeVieta): polynomial versions of results in Algebra.QuadraticDiscriminant merge-conflict t-ring-theory please-adopt looking for help
25907 mans0954 feat: low order roots of unity t-algebra please-adopt looking for help
26339 mans0954 feat(Analysis/Normed/Module/WeakDual): Banach Dieudonné Lemma merge-conflict WIP t-analysis large-import please-adopt looking for help
26340 mans0954 feat(Algebra/Module/NestAlgebra): Nest algebras merge-conflict t-algebra please-adopt looking for help
26341 mans0954 feat(LinearAlgebra/QuadraticForm/Basis): Free Tensor product of Quadratic Maps merge-conflict WIP t-algebra large-import please-adopt looking for help
33808 seewoo5 feat(Manifold/MFDeriv): add fun_prop to `MDifferentiable` awaiting-author t-differential-geometry ??? missing CI information
26344 mans0954 feat(Analysis/NormedSpace/MStructure): The component projections on WithLp 1 (α × β) are L-projections merge-conflict WIP t-analysis file-removed please-adopt looking for help
26345 mans0954 feat(Analysis/LocallyConvex/Polar): Bipolar theorem merge-conflict awaiting-author t-analysis large-import please-adopt looking for help
26347 mans0954 feat(Data/Finset/RangeDistance): abs_sub_lt_of_mem_finset_range merge-conflict t-data please-adopt looking for help
26349 mans0954 feat(Analysis/SpecialFunctions/Trigonometric/Basic): sin and cos of multiples of π / 3 help-wanted t-analysis please-adopt looking for help
26348 mans0954 feat(Analysis/LocallyConvex/Prime): the prime map merge-conflict WIP t-analysis please-adopt looking for help
26983 mans0954 feat(Order/LatticeElements): distributive, standard and neutral elements of a lattice merge-conflict WIP t-order please-adopt looking for help
29980 mans0954 refactor(RingTheory/Polynomial/Resultant/Quadratic): Re-implement QuadraticDiscriminant for R[X] merge-conflict please-adopt looking for help
29387 mans0954 feat(Analysis/LocallyConvex/WeakSpace): toWeakSpace_closedAbsConvexHull_eq merge-conflict blocked-by-other-PR t-analysis please-adopt blocked on another PR
29378 mans0954 feat(Analysis/LocallyConvex/AbsConvex): Balanced and AbsConvex sets under linear maps merge-conflict t-analysis please-adopt ??? looking for help
29856 mans0954 feat(Analysis/Normed/Ring/Basic): Add NonUnitalNonAssocSeminormedRing and NonUnitalNonAssocNormedRing t-analysis please-adopt looking for help
26614 Rida-Hamadani feat(SimpleGraph): add more API for `take`/`drop` t-combinatorics awaiting review
33611 urkud feat(ImplicitFunction): add a parametric version t-analysis awaiting review
33649 vihdzp feat(Analysis/Real/Hyperreal): more lemmas on `ω` and `ε` large-import t-algebra awaiting review
33700 vihdzp feat: dense orders have elements lying between two finite sets t-order large-import awaiting review
33724 alreadydone chore(Algebra): deprecate `DistribMulAction.toAddMonoidHom` t-algebra awaiting review
33501 SnirBroshi feat(Combinatorics/SimpleGraph/Finite): degrees for infinite graphs large-import t-combinatorics awaiting review
33665 JovanGerb fix(addRelatedDecl): support imported theorems in module t-meta awaiting review
30526 SnirBroshi chore(Logic/Relation): use `Subrelation` to state theorems awaiting-zulip t-logic awaiting a zulip discussion
33209 JovanGerb feat(infoview_search): move to new frontend large-import file-removed t-meta blocked-by-other-PR blocked on another PR
33052 JovanGerb feat: replace `rw??` tactic with `#infoview_search` command large-import t-meta file-removed failing CI
33025 JovanGerb feat(gcongr): beef up `@[gcongr]` tag to accept `↔` & any argument order t-meta awaiting review
33507 khwilson feat(Mathlib/Analysis/Polynomial/Fourier): Add Parseval's Identity specialized to Polynomials t-analysis new-contributor awaiting-author awaiting author
33815 grunweg style: fix whitespace around conditional variance t-measure-probability awaiting-author awaiting author
33417 themathqueen feat: `{Continuous}Linear{Isometry}Equiv.conj{Continuous, Star}AlgEquiv` are "almost" injective t-analysis t-algebra awaiting review
32144 EtienneC30 feat: add a predicate HasGaussianLaw brownian t-measure-probability awaiting review
25848 joelriou feat/refactor: redefinition of homology + derived categories WIP t-category-theory large-import t-topology labelled WIP
33690 Ljon4ik4 feat: Defining Lie Rinehart algebras t-algebra new-contributor awaiting-author awaiting author
33709 wangying11123 feat(Analysis/Convex/Between): Add wbtw_of_sameRay_vsub_left new-contributor t-convex-geometry awaiting review
33254 SnirBroshi feat(Data/Nat/Lattice): `¬BddAbove s → sSup s = 0` t-data awaiting review
32971 Paul-Lez feat(Data/Finsupp/Pointwise): generalise pointwise scalar multiplication of finsupps t-data awaiting review
32984 artie2000 refactor: remove order instances from `SetLike` blocked-by-other-PR t-data t-meta blocked on another PR
32888 staroperator feat(Tactic/FunProp): make `fun_prop` able to tag `→` and `∀` t-meta awaiting review
33336 fbarroero feat(NumberTheory/MahlerMeasure): Kronecker's Theorem for the Mahler Measure awaiting-author t-number-theory awaiting author
31891 jsm28 feat(Geometry/Euclidean/Sphere/OrthRadius): lemmas for setting up and using polars t-euclidean-geometry ??? missing CI information
33845 bjornsolheim feat(Analysis/Convex): barycenter of a standard simplex t-analysis awaiting review
33840 vihdzp feat(SetTheory/Ordinal/CantorNormalForm): Evaluate a Finsupp as a CNF t-set-theory awaiting review
33312 YuvalFilmus feat(Polynomial/Chebyshev): formulas for iterated derivatives of T and U at 1 ⚠️ awaiting review
33714 idontgetoutmuch Riemannian metrics exist II t-differential-geometry new-contributor awaiting review
33740 SnirBroshi chore(Order/CompleteLattice/Basic): generalize many theorems to `CompleteSemilattice{Sup/Inf}` t-order awaiting review
33753 SnO2WMaN doc(1000.yaml): Mention Tarski's Undefinability Theorem in FFL new-contributor awaiting review
33760 JovanGerb feat(Order/Bounds/Basic): use `to_dual` - part 1 large-import t-order awaiting review
33774 SnO2WMaN doc(100.yaml, 1000.yaml): Update about Gödel's Incompleteness Theorem new-contributor awaiting review
33860 DavidLedvinka feat(Probability): Add Cauchy distribution t-measure-probability awaiting review
33791 PhoenixIra feat: Generalization of FixedPointApproximants to CompletePartialOrder new-contributor ⚠️ failing CI
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
33852 zcyemi feat(LinearAlgebra/AffineSpace/Independent): Add affineCombination_eq_lineMap_iff_weight_lineMap t-algebra awaiting review
31981 jsm28 feat(Geometry/Euclidean/Incenter): `tangentSet` and `tangentsFrom` lemmas t-euclidean-geometry blocked-by-other-PR ??? blocked on another PR
32295 jsm28 feat(Archive/Imo/Imo2024Q4): IMO 2024 Q4 IMO blocked-by-other-PR blocked on another PR
27702 FLDutchmann feat(NumberTheory/SelbergSieve): define Lambda-squared sieves and prove important properties t-number-theory delegated failing CI
33697 artie2000 feat(FieldTheory): real closed field t-algebra 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
12934 grunweg chore: replace more uses of > or ≥ by < or ≤ merge-conflict awaiting-author help-wanted ??? looking for help
28070 grunweg style: improve indentation of multi-linear enumerations in doc-strings merge-conflict failing CI
31110 bryangingechen ci: don't delete merged branches awaiting-author CI merge-conflict merge conflict
33863 urkud feat: generalize some lemmas about LTOs ⚠️ awaiting review
32030 newell feat(Analysis/AperiodicOrder/Delone): Delone Sets t-analysis awaiting-author awaiting author
33105 Timeroot feat(BoundedOrder): add `finiteness` rule for ite and dite t-order awaiting-author t-meta ??? missing CI information
32440 thorimur feat: make the `unusedDecidableInType` linter fire when `Decidable*` instances are used only inside of proofs in the type t-linter failing CI
32892 Parcly-Taxel feat(Analysis/SpecialFunctions): arithmetic-geometric mean t-analysis failing CI
33832 alreadydone feat(Algebra): localization preserves unique factorization blocked-by-other-PR t-algebra bench-after-CI blocked on another PR
31706 Thmoas-Guan feat(Algebra/ModuleCat): `ModuleCat.uliftFunctor` t-algebra awaiting-author maintainer-merge awaiting author
31059 gasparattila feat(Topology/Sets): define the Vietoris topology on `(Nonempty)Compacts` t-topology awaiting review
33872 WenrongZou feat(RingTheory/MvPowerSeries): some inequalities related to order t-ring-theory awaiting review
33764 IvanRenison feat(Combinatorics/SimpleGraph/Diam): drop `Finite α` from `ediam_le_two_mul_radius` t-combinatorics awaiting review
31595 astrainfinita chore: redefine `Ideal.IsPrime` t-algebra merge-conflict merge conflict
32974 jano-wol feat: golf eq_top_of_invtSubmodule_ne_bot delegated t-algebra delegated
33478 anishrajeev feat(ModelTheory): define a subset of the topology over complete types t-logic blocked-by-other-PR new-contributor blocked on another PR
33874 joelriou feat(Algebra/Homology/ShortComplex): cycles can be computed with a limit kernel fork t-algebra t-category-theory ??? missing CI information
33595 JovanGerb chore: remove some `backward.proofsInPublic` failing CI
33879 joelriou feat(CategoryTheory/ComposableArrows): isIso_iff t-category-theory ??? missing CI information
33437 joelriou feat(Algebra/Homology): short exact sequences with four terms t-algebra t-category-theory failing CI
33881 joelriou feat(CategoryTheory/ComposableArrows): API for the composition of four arrows t-category-theory WIP blocked-by-other-PR ??? blocked on another PR
33880 joelriou feat(CategoryTheory/ComposableArrows): API for the composition of three arrows t-category-theory WIP blocked-by-other-PR ??? blocked on another PR
33875 joelriou feat(Algebra/Homology): an homology data from an epi-mono factorization large-import WIP blocked-by-other-PR ⚠️ blocked on another PR
33883 joelriou feat(CategoryTheory/ObjectProperty): various additions t-category-theory awaiting review
32039 HugLycan feat(Tactic/Positivity): handle non-zeroness in non-orders WIP new-contributor t-meta merge-conflict labelled WIP
30122 xroblot Development branch (1) WIP large-import ??? labelled WIP
27557 chrisflav feat(RingTheory/KrullDimension): generalize some results about local rings t-ring-theory ??? missing CI information
33088 joelriou feat(AlgebraicTopology/ModelCategory): the left derivability structure t-algebraic-topology t-category-theory WIP blocked-by-other-PR ??? blocked on another PR
33822 robin-carlier feat(Meta/CategoryTheory): `cancelIso` simproc WIP t-category-theory t-meta merge-conflict labelled WIP
33387 AntoineChambert-Loir chore(LinearAlgebra/Transvection/Basic): mv Transvection.lean file to Transvection.Basic.lean file-removed t-algebra blocked-by-other-PR ??? blocked on another PR
33392 AntoineChambert-Loir feat(LinearAlgebra/Transvection/Generation): non-exceptional case in Dieudonné's theorem t-algebra blocked-by-other-PR file-removed ??? blocked on another PR
29077 grunweg feat(Manifold/Instances/Icc): golf smoothness proof using immersions merge-conflict blocked-by-other-PR t-differential-geometry blocked on another PR
28905 grunweg feat: immersions are locally embeddings blocked-by-other-PR t-differential-geometry blocked on another PR
25822 ScottCarnahan WIP: experiments with vertex algebras WIP large-import merge-conflict labelled WIP
33303 sinhp feat(CategoryTheory): The monads and comonads of locally cartesian closed categories WIP t-category-theory labelled WIP
33877 joelriou feat(CategoryTheory/Category/Preorder): isIso_homOfLE t-category-theory awaiting review
33886 joelriou feat(CategoryTheory/Triangulated): functors to `Triangle` t-category-theory awaiting review
33887 joelriou feat(CategoryTheory/Triangulated): fully faithful triangulated functors t-category-theory awaiting review
33866 robin-carlier fix(AlgebraicTopology/SimplicialNerve): make `SimplicialThickening` a one field structure t-algebraic-topology t-category-theory awaiting review
33888 joelriou feat(CategoryTheory/Shift): more API for NatTrans.CommShift t-category-theory awaiting review
33803 erdOne feat(RingTheory): integral closure commutes with standard etale basechange t-ring-theory large-import awaiting review
30985 erdOne feat(AlgbraicGeometry), `Hom(-, X)` commutes with inverse limits for schemes of finite presentation t-algebraic-geometry awaiting review
24965 erdOne refactor: Make `IsLocalHom` take unbundled map t-algebra delegated failing CI
33532 vihdzp feat(RingTheory/Valuation/ValuativeRel): introduce `=ᵥ` relation t-ring-theory awaiting review
33810 dupuisf feat: add instances of `LawfulInv` WIP blocked-by-other-PR ⚠️ blocked on another PR
32880 0xTerencePrime feat(Analysis/Asymptotics): define subpolynomial growth awaiting-author t-analysis new-contributor failing CI
33891 Komyyy refactor: make `Nat.Partrec` protected t-computability awaiting review
33850 YuvalFilmus feat(Chebyshev/ChebyshevGauss): Chebyshev–Gauss formula t-analysis blocked-by-other-PR ??? blocked on another PR
33843 euprunin chore: golf using `grind` and `simp` awaiting review
33826 euprunin chore: golf using `grind` awaiting review
33897 ADedecker feat(HereditarilyLindelof): review and expand API t-topology ??? missing CI information
33864 Timeroot feat(Computability/Primrec): Proving several Nat arithmetic functions are primrec large-import ⚠️ awaiting review
33778 ADedecker feat: on a Hereditarily Lindelöf space, any family of lower semicontinuous function admits a countable subfamily with same supremum t-topology blocked-by-other-PR blocked on another PR
31449 kim-em feat(SemilocallySimplyConnected): definition and alternative formulation awaiting-author t-topology awaiting author
33896 loefflerd refactor(Geometry/Manifold): split long file ChartedSpace.lean t-differential-geometry tech debt awaiting review
31046 Thmoas-Guan feat(Homology) : compatibility of map between `Ext` awaiting-author t-category-theory awaiting author
33838 chainstart feat(NumberTheory): add unitary divisor sum function new-contributor t-number-theory awaiting review
33905 plp127 chore(Order/RelClasses): name arguments of recursors t-order ??? missing CI information
33613 DavidLedvinka feat(Probability): `UniformOn_univ_instIsProbabilityMeasure` t-measure-probability awaiting review
33736 fbarroero feat(RingTheory/Polynomial/GaussNorm): The `gaussNorm` is an absolute value if `v` is a nonarchimedean absolute value ⚠️ awaiting review
33743 jcommelin ci: add automated commit verification CI awaiting review
33782 tb65536 refactor(RingTheory/Lasker): create structure for primary decomposition t-ring-theory t-algebra awaiting review
33784 tb65536 refactor(Topology/Irreducible): weaken assumptions of `preimage_mem_irreducibleComponents_of_isPreirreducible_fiber` t-topology awaiting review
33786 hdmkindom feat(Analysis/Matrix): add Jacobian matrix for matrix-valued functions t-analysis new-contributor awaiting review
33795 alreadydone feat(Topology/Sheaves): LocalPredicate prerequisite for étalé spaces t-topology awaiting review
33862 dupuisf chore(AkraBazzi): golf the main proof WIP t-analysis blocked-by-other-PR blocked on another PR
33504 ldct feat: Add lemmas for DihedralGroup.fintypeHelper t-group-theory awaiting review
33718 erdOne feat(RingTheory): predicate for `QuasiFiniteAt` large-import t-ring-theory awaiting review
33895 jessealama feat(Computability/Primrec): add list_take, list_drop, list_modify, and list_set new-contributor t-computability failing CI
33757 fpvandoorn feat: remove decidability instances on sets or ideals ⚠️ awaiting review
33780 ooovi feat(Geometry/Convex/Cone): lineality space of pointed cones t-convex-geometry ??? missing CI information
33664 ooovi feat(Geometry/Convex/Cone/Pointed): face lattice of pointed cones file-removed awaiting-author t-convex-geometry awaiting author
33878 xroblot feat(MulChar): generalize duality results on finite abelian groups to multiplicative characters large-import t-number-theory awaiting review
33893 MichaelStollBayreuth feat(NumberTheory/Height): heights of tuples and finsupps t-number-theory awaiting review
33355 0xTerencePrime feat(Combinatorics/SimpleGraph/Connectivity): define vertex connectivity new-contributor t-combinatorics awaiting review
33802 stepan2698-cpu feat: Schur's lemma for monoid representations new-contributor t-algebra blocked-by-other-PR blocked on another PR
24789 Ruben-VandeVelde chore: move Algebra.Group.Hom.End to Algebra.Ring merge-conflict file-removed awaiting-author t-algebra merge conflict
29186 winstonyin feat: IsIntegralCurve for solutions to ODEs t-dynamics t-differential-geometry t-analysis awaiting-author awaiting author
27936 alreadydone feat(Algebra): additivize Dvd and Prime t-algebra awaiting review
33842 joelriou feat(Algebra/Homology): spectral sequences blocked-by-other-PR WIP t-category-theory large-import blocked on another PR
33675 euprunin feat(RingTheory/RingHom): remove unnecessary assumptions in `locally_StableUnderCompositionWithLocalizationAwayTarget` (WIP) WIP t-ring-theory labelled WIP
33901 martinwintermath feat(LinearAlgebra/Span): add inter/union/sInf/sSup lemmas for Submodule.span new-contributor t-algebra awaiting review
32757 AntoineChambert-Loir feat(LinearAlgebra/Transvection): the determinant of a transvection is equal to 1. ⚠️ awaiting review
33911 YaelDillies feat(Data/Set/Finite): make simp more powerful t-data awaiting review
33903 erdOne feat(RingTheory): local structure of monogenic unramified algebras t-ring-theory large-import awaiting review
33323 harahu doc(Algebra): fix file refs t-algebra awaiting review
33797 SnirBroshi chore(Order/Defs/Unbundled): deprecate `IsTotal` in favor of core's `Std.Total` t-order awaiting review
33028 bjornsolheim feat(Geometry/Convex/Cone): minimal and maximal cone tensor products are commutative t-convex-geometry awaiting review
27053 tb65536 feat: Galois group of `x^n - x - 1` WIP t-algebra large-import labelled WIP
30504 grunweg feat: add custom elaborators for immersions blocked-by-other-PR t-meta t-differential-geometry blocked on another PR
33885 WenrongZou feat(RingTheory/MvPowerSeries): some theorems about expand t-ring-theory awaiting review
33793 LTolDe feat(MeasureTheory/Constructions/Polish/Basic): add lemma AnalyticSet.inter_nonempty_of_nowhereMeagre t-measure-probability new-contributor awaiting review
33890 joelriou feat(CategoryTheory/Triangulated): distinguished_iff_of_isZero t-category-theory awaiting review
33908 erdOne perf: set `IsScalarTower.right` to high priority t-algebra awaiting review
33746 ster99 feat(Algebra/Module/ZLattice): add lemma `floor b (m + x) = m + floor b x` and similar t-algebra new-contributor awaiting review
33917 tb65536 feat(Algebra/Module/LocalizedModule/Submodule): add `inf` and `sup` API t-ring-theory t-algebra awaiting review
33924 martinwintermath feat(Order/ModularLattice): add some dual codisjoint lemma for modular lattices t-order new-contributor awaiting review
30744 grunweg feat: more extensions for differential geometry elaborators t-differential-geometry t-meta blocked-by-other-PR blocked on another PR
28796 grunweg feat: immersions are smooth t-differential-geometry maintainer-merge failing CI
33844 michelsol feat: lemmas to change variables in iSup / iInf / iUnion / iInter over a set new-contributor t-order awaiting review
31364 YaelDillies feat: binomial random graphs t-combinatorics t-measure-probability awaiting review
33676 YuvalFilmus feat(Chebyshev/Orthogonality): Chebyshev T polynomials are orthogonal t-analysis awaiting review
33435 astrainfinita feat: algebra automorphisms of monoid algebras merge-conflict t-algebra merge conflict
33925 harahu doc(Topology): fix typos t-topology awaiting review
32481 ADedecker feat: add `PolynormableSpace.banach_steinhaus` t-analysis delegated delegated
32882 DavidLedvinka feat(Probability): add `Adapted ` t-measure-probability awaiting review
33634 xgenereux feat(ValuationSubring): eq_self_or_eq_top_of_le merge-conflict blocked-by-other-PR large-import ⚠️ blocked on another PR
33814 seewoo5 feat(Manifold/MFDeriv): add `MDifferentiable.pow` with FunProp t-differential-geometry blocked-by-other-PR merge-conflict blocked on another PR
33857 euprunin chore: golf and reduce compilation time awaiting review
33935 mckoen feat(CategoryTheory/Arrow): define monoidal structure on the arrow category merge-conflict WIP t-category-theory labelled WIP
33441 dupuisf feat: add `LawfulInv` class for types with an inverse that behaves like `Ring.inverse` awaiting-author t-algebra awaiting author
33491 themathqueen feat(Analysis/InnerProductSpace): linear map is positive iff it equals the sum of rank-one operators t-analysis awaiting review
33882 AntoineChambert-Loir feat(LinearAlgebra/Transvection/SpecialLinearGroup): commutators in the special linear group blocked-by-other-PR file-removed ??? ⚠️ blocked on another PR
33870 jcommelin feat(Data/Matrix/Cartan): add IsSymm lemmas and simplify IsSimplyLaced proofs t-data merge-conflict merge conflict
33631 xgenereux feat(ValuationSubring): simp lemmas for idealOfLE/ofPrime in relation to top/bot blocked-by-other-PR ⚠️ blocked on another PR
31425 robertmaxton42 feat(Topology): implement delaborators for non-standard topology notation t-topology awaiting review
33851 alreadydone chore(Algebra): deprecate `CancelMonoidWithZero` t-algebra ??? missing CI information
33929 tb65536 feat(RingTheory/IsPrimary): add lemma connecting `Submodule.IsPrimary` and `Submodule.colon` t-ring-theory t-algebra awaiting review
33766 alreadydone feat(Analysis, Topology): more examples of covering maps involving the complex plane merge-conflict t-topology t-analysis blocked-by-other-PR large-import ❌? blocked on another PR
32134 mitchell-horner feat(Topology/Real): theorems linking `IsGLB` with `BddBelow`, `Antitone`, `Tendsto _ atTop` blocked-by-other-PR t-topology large-import 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
32777 madvorak doc: Contributing moved to Contributing ❌? infrastructure-related CI failing
33118 thomaskwaring feat(Combinatorics/SimpleGraph/Acyclic): every graph has a spanning forest. new-contributor t-combinatorics awaiting review
33253 SnirBroshi feat(Combinatorics/SimpleGraph/Clique): avoid `Fintype`/`Finite` assumptions where possible t-combinatorics awaiting review
33288 vihdzp chore(Combinatorics/SimpleGraph/Paths): review API t-combinatorics awaiting review
33292 SnirBroshi feat(Combinatorics/SimpleGraph/LineGraph): lift copies/isomorphisms to line-graph large-import t-combinatorics awaiting review
33335 YaelDillies feat(Combinatorics/SimpleGraph): more about two-reachability t-combinatorics awaiting review
33347 AntoineChambert-Loir feat(LinearAlgebra/Transvection/Basic): define dilatransvections t-algebra awaiting review
33360 joelriou feat(Algebra/Homology): functoriality of `extMk` with respect to the injective resolution t-category-theory awaiting review
33431 gululu996-ui feat(Combinatorics/SimpleGraph/Bipartite): characterize bipartite simplegraphs by even cycles new-contributor t-combinatorics awaiting review
33527 SnirBroshi feat(Combinatorics/SimpleGraph/Connectivity/Subgraph): `w.toSubgraph ≤ G' ↔ w.edgeSet ⊆ G'.edgeSet` t-combinatorics awaiting review
33804 tb65536 feat(RingTheory/Localization/Ideal): `map` distributes over `inf` t-ring-theory t-algebra awaiting review
33818 JohnnyTeutonic feat(Algebra/Lie/Classical): finrank of sl(n) equals n² - 1 t-algebra awaiting review
33825 euprunin chore: golf using `grind` awaiting review
33132 BoltonBailey feat(Computability): Single-tape TM complexity t-computability WIP blocked-by-other-PR blocked on another PR
33934 tb65536 chore(Algebra/Polynomial/Splits): deprecate `Splits.splits` and `splits_iff_splits` t-algebra awaiting review
33542 yuanyi-350 feat(integral): Error Estimation for the Rectangle Rule in Numerical Integration awaiting-author t-analysis awaiting author
33943 urkud feat(Asymptotics/TVS): add more lemmas t-analysis awaiting review
33582 urkud feat(ContDiffHolder/Moreira): define $C^{k+(α)}$ maps t-analysis awaiting review
33206 lua-vr feat(Integral.Bochner.Set): add `tendsto_setIntegral_of_monotone₀` awaiting-author t-measure-probability awaiting author
33876 joelriou feat(Order): `WithBotTop` and the extended integers t-algebra t-data awaiting review
33884 vihdzp chore(Order/Hom/BoundedLattice): remove `initialize_simps_projections` t-order awaiting review
33909 YaelDillies feat(SetTheory/Cardinal): more lemmas about `ENat` ⚠️ failing CI
33948 anivegesana feat(Analysis/Normed/Algebra): matrix exponential of nilpotent matrix new-contributor t-analysis failing CI
33270 vihdzp chore(Order/Disjoint): use `to_dual` t-order awaiting-author failing CI
15355 adomani feat: MiM PR report WIP ??? ⚠️ labelled WIP
33119 euprunin chore: golf using `grind` awaiting-author awaiting author
26986 WangYiran01 feat(Partition): add bijection for partitions with max part ≤ r awaiting-author t-combinatorics new-contributor failing CI
33894 vihdzp chore: move `Archimedean` to a new `Defs` file t-algebra awaiting review
33788 harahu chore(Algebra): move `LinearMap.ker_restrictScalars` t-algebra awaiting review
33726 alreadydone feat(Analysis): (complex) polynomials as branched coverings large-import t-topology t-analysis awaiting review
26291 RemyDegenne feat(Probability): Cameron-Martin theorem WIP blocked-by-other-PR t-measure-probability merge-conflict blocked on another PR
33388 plby doc(docs/100.yaml): add recently-proven theorems merge-conflict new-contributor awaiting-author merge conflict
33765 JovanGerb feat(Order/CompleteLattice/Defs): `to_dual` for `CompleteSemilattice`s blocked-by-other-PR large-import t-order ❌? blocked on another PR
33506 Rida-Hamadani feat(SimpleGraph): construct a cycle of two distinct paths with same start and end blocked-by-other-PR t-combinatorics blocked on another PR
32891 felixpernegger feat(Topology/EMetricSpace): Introduction of ```Weak(Pseudo)EMetricSpace``` new-contributor t-topology awaiting review
33767 Whysoserioushah chore(RingTheory/Morita/Matrix): Finish the morita equivalence between matrix ring and the ring itself t-ring-theory large-import awaiting review
33636 mcdoll feat(Analysis/Distribution): the Laplacian on Schwartz functions awaiting-author t-analysis awaiting author
33087 joelriou feat(AlgebraicTopology): the cofibrant resolution functor (up to homotopy) t-algebraic-topology awaiting review
33606 ScottCarnahan feat(Algebra/Lie): basics of loop algebras t-algebra awaiting review
33939 mitchell-horner chore(Analysis/Normed): redefine `seminormFromConst'` without `choose` awaiting review
33954 or4nge19 feat(CategoryTheory/Abelian): add Filtration API awaiting-author t-category-theory awaiting author
33952 vihdzp chore(Order/FixedPoints): use `where` notation t-order awaiting review
32403 FLDutchmann fix(FieldSimp): `declaration has free variables` kernel errors delegated t-meta ❌? infrastructure-related CI failing
33329 mcdoll feat(Analysis): Fourier-based Sobolev spaces WIP t-analysis blocked-by-other-PR blocked on another PR
33958 chrisflav feat(AlgebraicGeometry): the small affine étale site WIP t-algebraic-geometry labelled WIP
32745 LTolDe feat(Topology/Algebra): add MulActionConst.lean awaiting-author new-contributor t-topology awaiting author
32692 WilliamCoram feat: define multivariate restricted power series t-ring-theory t-number-theory new-contributor awaiting review
32807 WilliamCoram feat: Define the Gauss norm for MvPowerSeries t-ring-theory new-contributor failing CI
33955 joelriou feat(AlgebraicTopology): the fibrant resolution functor up to homotopy t-algebraic-topology WIP blocked-by-other-PR blocked on another PR
33790 eliasjudin feat(CategoryTheory/Preadditive/Mat): add natural transformation and isomorphism extension theorems t-category-theory new-contributor awaiting-author awaiting author
32316 Thmoas-Guan feat(Homology/ModuleCat): Dimension Shifting tools in ModuleCat awaiting-author t-algebra t-category-theory awaiting author
33921 SnirBroshi chore(Data/Nat/Factorial): replace `n !` with `(n)!` everywhere tech debt t-data awaiting review
33960 justus-springer feat(FieldTheory/RatFunc): Generalize lifts/maps to FunLike new-contributor t-algebra failing CI
29996 vihdzp chore(Order/Concept): `IsIntent` and `IsExtent` blocked-by-other-PR t-order merge-conflict blocked on another PR
32159 zhuyizheng feat(Order): gaps of disjoint intervals awaiting-author new-contributor t-order ❌? infrastructure-related CI failing
25622 eric-wieser refactor: overhaul instances on LocalizedModule t-algebra failing CI
31613 xyzw12345 feat(RepresentationTheory/GroupCohomology): Non-abelian Group Cohomology t-algebra large-import awaiting review
33963 gasparattila feat(Topology/UniformSpace/Closeds): completeness of `(Nonempty)Compacts` t-topology awaiting review
33044 bryangingechen ci: also get cache for parent commit CI failing CI
33801 artie2000 chore: add missing mem lemmas t-meta failing CI
30112 gaetanserre feat(Probability.Kernel): add representation of kernel as a map of a uniform measure t-measure-probability awaiting review
33965 gasparattila feat(Topology/MetricSpace/Closeds): define a metric on `Compacts` t-topology awaiting review
33854 loefflerd feat(Analysis): generalize normed spaces to normed modules WIP blocked-by-other-PR ??? ⚠️ blocked on another PR
33712 wangying11123 feat(Geometry/Euclidean/Angle/Unoriented/Projection): Add sameray_orthogonalProjection_vsub_of_angle_lt new-contributor t-euclidean-geometry awaiting review
33907 dupuisf feat(Asymptotics): Show that `f =O[atTop] g` from a recurrence relation t-analysis awaiting review
30030 JonBannon feat(MeasureTheory): add `MemLp.Const` class and instances to unify `p = ∞` and `μ.IsFiniteMeasure` cases awaiting-author t-measure-probability merge-conflict failing CI
33966 gasparattila feat(Topology): characterization of `LocallyConnectedSpace` in terms of `IsTopologicalBasis` t-topology awaiting review
33807 adamtopaz feat: TypeCat refactor WIP t-category-theory merge-conflict labelled WIP
33969 goliath-klein refactor(PiTensorProduct/{InjectiveNorm, ProjectiveNorm}): Currently, injectiveSeminorm = projectiveSeminorm WIP t-analysis new-contributor labelled WIP
32438 JovanGerb feat: unfold-boundaries in `to_dual` t-meta awaiting review
33964 JovanGerb feat(Order/Interval/Set): `to_dual` for `Iio`/`Iic` ⚠️ failing CI
32355 bjornsolheim feat(Geometry/Convex/Cone): define and characterize simplicial pointed cones t-convex-geometry new-contributor awaiting review
33936 cameronfreer feat(NumberTheory/LSeries): add positivity and real-valuedness lemmas for Riemann zeta new-contributor t-number-theory sphere-packing awaiting review
33956 joelriou feat(AlgebraicTopology/ModelCategory): the right derivability structure t-algebraic-topology WIP blocked-by-other-PR ??? blocked on another PR
31794 thorimur feat: `unusedFintypeInType` linter maintainer-merge file-removed ⚠️ awaiting review
33962 loefflerd feat(Analysis/Normed): generalize `smul` on cts [multi-]linear maps t-analysis awaiting review
33947 urkud chore: move `Complex.expPartialHomeomorph` t-analysis awaiting review
33971 seewoo5 feat(DihedralGroup): center of D_n for odd n \ge 3 trivial t-group-theory awaiting review
29610 llllvvuu feat(LinearAlgebra): define LinearMap.Eigenbasis merge-conflict t-algebra awaiting-author merge conflict
33919 tb65536 feat(Algebra/Polynomial/Roots): Action of group on `rootSet` t-ring-theory t-algebra delegated failing CI
33961 JovanGerb feat(to_dual): don't translate the order on `Prop` t-meta awaiting review
33930 chrisflav feat(AlgebraicGeometry): gluing colimits in `P.Over ⊤ S` merge-conflict t-algebraic-geometry merge conflict
33915 tb65536 feat: irreducible components of schemes WIP t-ring-theory t-algebra t-algebraic-geometry large-import awaiting-author labelled WIP
31610 rudynicolop feat(Computability/NFA): Kleene star closure for Regular Languages via NFA t-computability new-contributor awaiting-author awaiting-CI does not pass CI
33928 jsm28 feat(Combinatorics/Tiling/TileSet): indexed families of tiles t-combinatorics awaiting review
33744 bilichboris feat(RingTheory): Class Group of a Unique Factorization Domain is trivial t-ring-theory new-contributor failing CI
33397 themathqueen feat(Topology/Algebra/Star/LinearMap): intrinsic star for continuous linear maps t-algebra t-topology awaiting review
29942 smmercuri feat(InfinitePlace/Completion): embeddings of `w.Completion` factor through embeddings of `v.Completion` when `w` extends `v` FLT ⚠️ awaiting review
25899 pfaffelh feat(Topology/Compactness/CompactSystem): introduce compact Systems merge-conflict awaiting-author t-topology brownian failing CI
26303 joelriou feat(AlgebraicTopology): the fundamental lemma of homotopical algebra t-algebraic-topology WIP t-category-theory blocked-by-other-PR blocked on another PR
33282 AntoineChambert-Loir feat(LinearAlgebra/Center): description of the center of the algebra of endomorphisms t-algebra awaiting review
33259 YuvalFilmus feat(Trigonometric/Chebyshev/Extremal): Chebyshev polynomials are extremal in terms of leading coefficient t-analysis blocked-by-other-PR blocked on another PR
33914 Vierkantor fix(Tactic/Linter): support Verso docstrings in header style linter t-linter delegated delegated
33833 JovanGerb feat(reassoc): tag the generated declaration with `to_dual none` t-meta awaiting review
33683 joelriou feat(AlgebraicTopology/SimplicialSet): the simplicial homotopy induced by an homotopy blocked-by-other-PR t-algebraic-topology WIP blocked on another PR
33834 JovanGerb feat(CategoryTheory/NatTrans): use to_dual ⚠️ awaiting review
33974 mckoen feat(CategoryTheory/Functor): pushout-products and pullback-powers WIP t-category-theory labelled WIP
25273 YaelDillies refactor: make `MonoidAlgebra` into a one-field structure WIP t-algebra large-import labelled WIP
33846 ocfnash feat: the rank of the ℤ-span of the roots of a root system is the dimension t-algebra large-import failing CI
33979 adomani ci: add `splice-bot` action CI failing CI
27493 themathqueen feat(RingTheory/Coalgebra): define Frobenius algebra t-ring-theory awaiting-author blocked-by-other-PR blocked on another PR
33916 AntoineChambert-Loir feat(LinearAlgebra/SpecialLinearGroup/Simple): simplicity of the projective special linear group. file-removed large-import blocked-by-other-PR ⚠️ blocked on another PR
33129 Paul-Lez feat(Tactic/Simproc/VecPerm): Add simproc for permuting entries of a vector t-meta failing CI
33221 stepan2698-cpu feat: definition of an intertwining map t-algebra new-contributor awaiting review
33466 Shreyas4991 refactor(Combinatorics/Digraph): add vertex sets t-combinatorics awaiting review
33953 vihdzp feat: IncompRel.ne t-order easy awaiting review
32186 urkud feat(Integral): estimate displacement by the integral of the speed t-measure-probability awaiting review
33950 vihdzp feat(Order/UpperLower/Basic): use `to_dual` - part 1 blocked-by-other-PR t-order blocked on another PR
33402 AntoineChambert-Loir feat(LinearAlgebra/Transvection/Generation): prove exceptional case in Dieudonné's theorem file-removed t-algebra blocked-by-other-PR blocked on another PR
33485 AntoineChambert-Loir feat(LinearAlgebra/Transvection/Generation): prove the third part of Dieudonné's theorem file-removed t-algebra blocked-by-other-PR blocked on another PR
33560 AntoineChambert-Loir feat(LinearAlgebra/Transvection/Generation): a linear equivalence is the product of dilatransvections file-removed t-algebra blocked-by-other-PR blocked on another PR
33923 grunweg fix: example of GL(V) being a Lie group t-differential-geometry easy awaiting review
33693 yoh-tanimoto feat(Mathlib/Analysis/Normed/Module): add instances of `CompleteSpace` for `Submodules` and `ClosedSubmodule` ⚠️ awaiting review
33980 martinwintermath feat(RingTheory/Finiteness/Basic): add lemmas for restricting scalars t-ring-theory new-contributor awaiting review
33194 YuvalFilmus feat(LinearAlgebra/Lagrange): refactored proof of leadingCoeff_eq_sum t-algebra awaiting review
33236 JovanGerb refactor(translate): merge `expand` into `applyReplacementFun` t-meta awaiting review
33973 tb65536 feat(RingTheory/Ideal/Ann): define the annihilator ideal `Ann(m)` t-ring-theory t-algebra awaiting review
33981 eric-wieser fix: use the tracing API to detect trace options easy t-meta awaiting review
33975 pfaffelh feat(Data/Set/Dissipate): Introduce dissipate s x := ⋂ y ≤ x, s y t-data new-contributor awaiting review
33821 JohnnyTeutonic feat(LinearAlgebra/Matrix/Hermitian): add IsSkewHermitian predicate t-algebra failing CI
33967 wangying11123 feat(Analysis/Convex/Between): Add Sbtw_expand and Wbtw_expand t-analysis new-contributor failing CI
33920 Citronhat feat(topology): generalize tendsto_inv_iff from ℝ≥0∞ to topological groups t-topology new-contributor awaiting review
29241 yoh-tanimoto feat(Analysis/InnerProductSpace/Orthogonal): add duplicates for `ClosedSubmodule` ⚠️ awaiting review
28208 Sebi-Kumar feat(Topology): add the definition `foldTrans` to concatenate finite sequences of paths t-topology new-contributor awaiting review
33983 erdOne feat(AlgebraicGeometry): union of disjoint affine opens is affine t-algebraic-geometry awaiting review
33443 sahanwijetunga feat: Define Isometries of Bilinear Spaces t-algebra new-contributor awaiting review
30658 grunweg feat: extend the `whitespace` linter to proof bodies blocked-by-other-PR large-import awaiting-CI t-linter blocked on another PR
33607 xgenereux feat: primeSpectrum_eq_of_KrullDimLEOne awaiting-author t-ring-theory awaiting author
32825 erdOne perf(RingTheory): `attribute [irreducible] KaehlerDifferential` t-ring-theory awaiting review
33982 erdOne feat(AlgebraicGeometry): being locally artinian is local t-algebraic-geometry large-import awaiting review
33941 YellPika feat(Order/OmegaCompletePartialOrder): teach fun_prop about ωScottContinuous functions new-contributor t-order ??? missing CI information
33986 martinwintermath feat(Order/ModularLattice): add lemmas to construct IsCompl from Disjoint/Codisjoint on complemented modular lattices new-contributor t-order awaiting review
33188 BryceT233 feat: MvPowerSeries.rename new-contributor t-ring-theory awaiting-author awaiting author
33768 vihdzp chore(Order/RelClasses): remove redundant instances t-order failing CI
32534 erdOne feat(AlgebraicGeometry): Zariski's main theorem WIP t-ring-theory blocked-by-other-PR blocked on another PR
33984 erdOne feat(AlgebraicGeometry): quasi-finite morphisms t-algebraic-geometry awaiting review
32027 alreadydone feat(Counterexamples): invertible module not isomorphic to any ideal t-ring-theory awaiting review
33291 BoltonBailey refactor(Computability): File for state transition systems t-computability awaiting review
33831 vihdzp refactor(RingTheory/Polynomial/SmallDegreeVieta): convert to {p : R[X]} (hp : p.natDegree = 2) t-ring-theory awaiting review
28126 Sebi-Kumar feat(AlgebraicTopology/FundamentalGroupoid): relate equality in fundamental groupoid to homotopy t-algebraic-topology new-contributor awaiting-author please-merge-master failing CI
33968 edegeltje chore(CategoryTheory/Limits/Shapes/Pullback): Split `CommSq` awaiting-CI t-category-theory does not pass CI
33985 YellPika feat(Order/OmegaCompletePartialOrder): `OmegaCompletePartialOrder` instance for `Sum` with basic `ωScottContinuous` lemmas new-contributor large-import blocked-by-other-PR ⚠️ blocked on another PR
26156 oliver-butterley feat(MeasureTheory.VectorMeasure): add a definition of total variation for VectorMeasure awaiting-author new-contributor t-measure-probability awaiting author
33819 bjornsolheim feat(Analysis/Convex): diameter of a standard simplex t-analysis awaiting review
32924 chrisflav feat(RingTheory/Smooth): smooth is equivalent to locally standard smooth awaiting-author t-ring-theory large-import awaiting author
32042 chrisflav feat(AlgebraicGeometry): quasi compact covers t-algebraic-geometry awaiting review
33987 MrQubo doc(Tactic/Lift): Mention `norm_cast` in documentation of `lift` t-meta new-contributor awaiting review
30484 vihdzp refactor: override `≤` and `<` in `Function.Injective.semilatticeSup`, etc. t-order failing CI
33393 grunweg chore: extend the whitespace linter to structure and instance fields please-adopt merge-conflict large-import blocked-by-other-PR blocked on another PR
33904 alreadydone refactor(Algebra): weaken NormalizationMonoid t-ring-theory t-algebra blocked-by-other-PR WIP merge-conflict blocked on another PR
33539 BryceT233 feat(RingTheory/MvPolynomial): powers of ideal of variables awaiting-author large-import t-ring-theory new-contributor awaiting author
33390 farmanb feat(RingTheory/Ideal): generalize Submodule.colon to sets t-ring-theory new-contributor awaiting review
33680 BoltonBailey feat(Probability/ProbabilityMassFunction): add Total Variation distance t-measure-probability failing CI
33942 artie2000 refactor: unbundle `GroupCone` large-import t-algebra failing CI
33944 artie2000 feat: formally real rings t-algebra awaiting-author failing CI
33817 FlAmmmmING fix(Combinatorics/Enumerative/Schroder.lean): Fix the definition and theorem of smallSchroder. new-contributor t-combinatorics large-import awaiting review
33752 mcdoll feat(Analysis/FourierSchwartz): the derivative of the Fourier transform t-analysis awaiting review
32367 BoltonBailey feat(Computability): add finEncodings for List Bool and pairs of types t-computability awaiting review
33411 IlPreteRosso feat(Analysis/DiscreteConvolution): Discrete convolution API basics t-analysis new-contributor awaiting review
33988 leanprover-community-bot-assistant chore: remove declarations deprecated between 2021-01-15 and 2025-07-15 failing CI
32851 tdwag123 feat(MeasureTheory/Measure/TypeClass/NoAtoms) add `exists_accPt_of_noAtoms` new-contributor t-measure-probability awaiting-author awaiting author
33926 tb65536 feat(RingTheory/Ideal/Colon): add more API for `sup` and `inf` t-ring-theory t-algebra awaiting review
33972 YuvalFilmus feat(Analysis/Polynomial/Order): polynomial has fixed sign beyond largest root ⚠️ failing CI
33461 loefflerd feat(NumberTheory/Modular): stabilizers for action on upper halfplane WIP ⚠️ labelled WIP
33873 YaelDillies chore(Algebra): replace `NoZeroSMulDivisors` with `Module.IsTorsionFree`, losing generality t-algebra large-import failing CI
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
26777 YaelDillies chore(Data/Set/Image): move `BooleanAlgebra` material to `Order` WIP t-data large-import labelled WIP
33643 vihdzp feat: `r < stdPart x → r < x` t-algebra failing CI