Why is my PR not on the queue?

This page was last updated on: March 04, 2026 at 14:55 UTC

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

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

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

Number Author Title Labels CI status? not blocked? no merge conflict? ready? awaiting review? On the review queue? Missing topic label? PR's overall status
13847 alreadydone feat(EllipticCurve): the universal elliptic curve awaiting-author merge-conflict t-algebraic-geometry t-algebra opened from a branch in the main mathlib repo (not a fork)
14167 alreadydone feat: Group scheme structure on Weierstrass curve WIP merge-conflict t-algebraic-geometry workshop-AIM-AG-2024 opened from a branch in the main mathlib repo (not a fork)
13297 urkud feat(Semicontinuous): add `comp` lemma awaiting-author merge-conflict t-topology t-order opened from a branch in the main mathlib repo (not a fork)
12608 eric-wieser feat: allow `nsmul` / `zsmul` to be omitted again, with a warning awaiting-author merge-conflict t-meta t-algebra opened from a branch in the main mathlib repo (not a fork)
12679 MichaelStollBayreuth perf(NumberTheory/RamificationInertia): speed up slow file WIP merge-conflict opened from a branch in the main mathlib repo (not a fork)
13057 alreadydone feat(NumberTheory): characterize elliptic divisibility sequences blocked-by-other-PR merge-conflict t-number-theory t-algebra opened from a branch in the main mathlib repo (not a fork)
12192 Ruben-VandeVelde feat: generalize isLittleO_const_id_atTop/atBot awaiting-author merge-conflict t-analysis opened from a branch in the main mathlib repo (not a fork)
10024 ADedecker feat: rename `connectedComponentOfOne` to `identityComponent`, prove that it is normal and open merge-conflict awaiting-CI t-topology opened from a branch in the main mathlib repo (not a fork)
10521 eric-wieser chore: generalize `IsBoundedLinearMap` to modules awaiting-author merge-conflict t-analysis opened from a branch in the main mathlib repo (not a fork)
10594 lecopivo feat: `fun_trans` function transformation tactic e.g. for computing derivatives WIP merge-conflict t-meta opened from a branch in the main mathlib repo (not a fork)
10721 urkud feat(Order/FunLike): define `PointwiseLE` merge-conflict t-order t-logic ??? opened from a branch in the main mathlib repo (not a fork)
10842 mcdoll chore: simplify proofs using new positivity extensions and tests WIP blocked-by-other-PR merge-conflict opened from a branch in the main mathlib repo (not a fork)
11100 eric-wieser feat(CategoryTheory/Limits): add `Functor.mapBinaryBiconeInv` merge-conflict awaiting-CI t-category-theory opened from a branch in the main mathlib repo (not a fork)
8503 thorimur feat: meta utils for `refine?` awaiting-author merge-conflict t-meta opened from a branch in the main mathlib repo (not a fork)
8519 eric-wieser refactor(LinearAlgebra/TensorProduct): golf using `liftAddHom` awaiting-author merge-conflict t-algebra opened from a branch in the main mathlib repo (not a fork)
8616 eric-wieser feat(Algebra/FreeAlgebra): add right action and `IsCentralScalar` merge-conflict awaiting-CI t-algebra opened from a branch in the main mathlib repo (not a fork)
8658 eric-wieser feat: support right actions for `Con` awaiting-author merge-conflict t-algebra opened from a branch in the main mathlib repo (not a fork)
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 opened from a branch in the main mathlib repo (not a fork)
8906 jjaassoonn feat: add some missing lemmas about linear algebra awaiting-author merge-conflict t-algebra opened from a branch in the main mathlib repo (not a fork)
8961 eric-wieser refactor: use the coinduced topology on ULift awaiting-author please-adopt merge-conflict awaiting-CI opened from a branch in the main mathlib repo (not a fork)
9146 laughinggas feat(Data/ZMod/Defs): Topological structure on `ZMod` awaiting-author merge-conflict t-topology t-algebra opened from a branch in the main mathlib repo (not a fork)
9229 eric-wieser refactor(Algebra/GradedMonoid): Use `HMul` to define `GMul` WIP merge-conflict t-algebra opened from a branch in the main mathlib repo (not a fork)
9354 chenyili0818 feat: monotonicity of gradient on convex real-valued functions awaiting-author merge-conflict t-analysis opened from a branch in the main mathlib repo (not a fork)
9356 alexjbest feat: assumption? awaiting-author merge-conflict t-meta opened from a branch in the main mathlib repo (not a fork)
9469 dupuisf feat: maximum modulus principle for functions vanishing at infinity awaiting-author t-analysis opened from a branch in the main mathlib repo (not a fork)
9487 eric-wieser feat: the exponential of dual numbers over non-commutative rings WIP merge-conflict t-analysis t-algebra t-measure-probability opened from a branch in the main mathlib repo (not a fork)
9510 eric-wieser feat(Analysis/Calculus/DualNumber): Extending differentiable functions to dual numbers WIP awaiting-CI t-analysis t-algebra opened from a branch in the main mathlib repo (not a fork)
9570 eric-wieser feat(Algebra/Star): Non-commutative generalization of `StarModule` WIP merge-conflict awaiting-CI t-algebra opened from a branch in the main mathlib repo (not a fork)
9642 eric-wieser refactor(Analysis/Normed/{Group/Field}/Basic): Let `extends` generate the repeated fields help-wanted WIP awaiting-author merge-conflict t-analysis opened from a branch in the main mathlib repo (not a fork)
6580 adomani chore: `move_add`-driven replacements awaiting-author merge-conflict opened from a branch in the main mathlib repo (not a fork)
6630 MohanadAhmed feat: Reduced Spectral Theorem WIP merge-conflict t-algebra opened from a branch in the main mathlib repo (not a fork)
6777 adomani chore(Co*variantClass): replace eta-expanded (· * ·), (· + ·), (· ≤ ·), (· < ·) merge-conflict opened from a branch in the main mathlib repo (not a fork)
6791 eric-wieser refactor: Use flat structures for morphisms help-wanted awaiting-author merge-conflict awaiting-CI opened from a branch in the main mathlib repo (not a fork)
6930 kmill feat: `resynth_instances` tactic for resynthesizing instances in the goal or local context WIP merge-conflict t-meta opened from a branch in the main mathlib repo (not a fork)
6931 urkud refactor(Analysis/Normed*): use `RingHomIsometric` for `*.norm_cast` help-wanted merge-conflict t-analysis ??? opened from a branch in the main mathlib repo (not a fork)
7227 kmill feat: flexible binders and integration into notation3 WIP merge-conflict t-meta opened from a branch in the main mathlib repo (not a fork)
7351 shuxuezhuyi feat(Topology/Algebra/Order): extend function on `Ioo` to `Icc` awaiting-author merge-conflict t-order opened from a branch in the main mathlib repo (not a fork)
7467 ADedecker feat: spectrum of X →ᵇ ℂ is StoneCech X WIP merge-conflict t-analysis opened from a branch in the main mathlib repo (not a fork)
7564 shuxuezhuyi feat(Topology/Algebra/Order): extend strictly monotone function on `Ioo` to homeomorphism on `Icc` blocked-by-other-PR merge-conflict t-topology opened from a branch in the main mathlib repo (not a fork)
7601 digama0 feat: ring hom support in `ring` awaiting-author merge-conflict t-meta t-algebra opened from a branch in the main mathlib repo (not a fork)
7615 eric-wieser chore(LinearAlgebra/Basic): generalize compatibleMaps to semilinear maps merge-conflict easy awaiting-CI t-algebra opened from a branch in the main mathlib repo (not a fork)
7713 RemyDegenne feat: add_left/right_inj for measures awaiting-author merge-conflict t-measure-probability opened from a branch in the main mathlib repo (not a fork)
7835 shuxuezhuyi feat(LinearAlgebra/Matrix): `lift` for projective special linear group awaiting-author merge-conflict t-algebra ??? opened from a branch in the main mathlib repo (not a fork)
7875 astrainfinita chore: make `SMulCommClass A A B` and `SMulCommClass A B B` higher priority merge-conflict t-algebra slow-typeclass-synthesis ??? opened from a branch in the main mathlib repo (not a fork)
7909 mcdoll fix(Tactic/Continuity): remove npowRec and add new tag for Continuous.pow WIP merge-conflict t-meta t-topology opened from a branch in the main mathlib repo (not a fork)
7932 eric-wieser refactor(Algebra/TrivSqZeroExt): replace with a structure merge-conflict awaiting-CI t-algebra opened from a branch in the main mathlib repo (not a fork)
7962 eric-wieser feat: `DualNumber (Quaternion R)` as a `CliffordAlgebra` WIP merge-conflict t-algebra opened from a branch in the main mathlib repo (not a fork)
8364 thorimur feat: `refine?` blocked-by-other-PR merge-conflict t-meta opened from a branch in the main mathlib repo (not a fork)
4871 j-loreaux feat: define the additive submonoid of positive elements in a star ordered ring merge-conflict awaiting-CI t-algebra ??? opened from a branch in the main mathlib repo (not a fork)
5133 kmill feat: IntermediateField adjoin syntax for sets of elements WIP merge-conflict t-algebra opened from a branch in the main mathlib repo (not a fork)
5912 ADedecker feat(Analysis.Distribution.ContDiffMapSupportedIn): space of smooth maps with support in a fixed compact WIP merge-conflict t-analysis opened from a branch in the main mathlib repo (not a fork)
6002 slerpyyy feat(Analysis.SpecialFunctions.Gaussian): add `integrable_fun_mul_exp_neg_mul_sq` awaiting-author merge-conflict t-analysis opened from a branch in the main mathlib repo (not a fork)
6079 eric-wieser fix: deduplicate variables merge-conflict awaiting-CI opened from a branch in the main mathlib repo (not a fork)
6195 eric-wieser chore(RingTheory/TensorProduct): golf the `mul` definition merge-conflict awaiting-CI t-algebra opened from a branch in the main mathlib repo (not a fork)
6210 MohanadAhmed feat(Data/IsROrC/Basic): add a `StarOrderedRing` instance WIP merge-conflict t-analysis t-algebra opened from a branch in the main mathlib repo (not a fork)
6328 FR-vdash-bot chore: make some instance about `Sub...Class` lower priority WIP merge-conflict awaiting-CI t-algebra opened from a branch in the main mathlib repo (not a fork)
6330 astrainfinita chore: make some instance about `Sub...Class` higher priority than `Sub...` WIP merge-conflict t-algebra slow-typeclass-synthesis opened from a branch in the main mathlib repo (not a fork)
6403 astrainfinita chore: change instance priorities of `Ordered*` hierarchy awaiting-author merge-conflict t-algebra t-order slow-typeclass-synthesis opened from a branch in the main mathlib repo (not a fork)
6491 eric-wieser chore(Mathlib/Algebra/Hom/GroupAction): add `SMulHomClass.comp_smul` merge-conflict t-algebra opened from a branch in the main mathlib repo (not a fork)
7076 grunweg feat: define measure zero subsets of a manifold WIP merge-conflict t-differential-geometry t-measure-probability opened from a branch in the main mathlib repo (not a fork)
3757 thorimur feat: config options for `fail_if_no_progress` WIP merge-conflict t-meta opened from a branch in the main mathlib repo (not a fork)
12353 thorimur feat: `conv%` WIP merge-conflict t-meta opened from a branch in the main mathlib repo (not a fork)
7903 urkud feat: define `UnboundedSpace` help-wanted merge-conflict t-topology opened from a branch in the main mathlib repo (not a fork)
15679 adomani test: refactor in CI WIP merge-conflict opened from a branch in the main mathlib repo (not a fork)
7565 shuxuezhuyi feat(Topology/Algebra/Order): extend homeomorphism of `Ioo` to `Icc` blocked-by-other-PR merge-conflict t-topology t-order opened from a branch in the main mathlib repo (not a fork)
10629 madvorak feat: List.cons_sublist_append_iff_right merge-conflict t-data opened from a branch in the main mathlib repo (not a fork)
9973 Ruben-VandeVelde feat: polynomials formed by lists please-adopt merge-conflict t-data opened from a branch in the main mathlib repo (not a fork)
12926 joelriou feat(CategoryTheory): the monoidal category structure induced by a monoidal functor WIP merge-conflict t-category-theory opened from a branch in the main mathlib repo (not a fork)
12869 adomani feat: linter and script for `theorem` vs `lemma` awaiting-author merge-conflict t-linter opened from a branch in the main mathlib repo (not a fork)
14563 awueth feat: if-then-else of exclusive or statement awaiting-author t-algebra new-contributor opened from a branch in the main mathlib repo (not a fork)
12093 ADedecker feat: tweak the definition of semicontinuity to behave better in nonlinear orders WIP merge-conflict t-topology opened from a branch in the main mathlib repo (not a fork)
11393 mcdoll feat(Analysis/Distribution/SchwartzSpace): The Heine-Borel property WIP merge-conflict t-analysis opened from a branch in the main mathlib repo (not a fork)
9444 erdOne feat: Various instances regarding `𝓞 K`. help-wanted merge-conflict t-number-theory opened from a branch in the main mathlib repo (not a fork)
8931 hmonroe feat(Computable): define P, NP, and NP-complete awaiting-author merge-conflict t-computability opened from a branch in the main mathlib repo (not a fork)
10387 adomani feat(Tactic/ComputeDegree): add `polynomial` tactic WIP t-meta RFC opened from a branch in the main mathlib repo (not a fork)
9154 FR-vdash-bot feat: `npow` / `nsmul` / `Nat.cast`/ `zpow` / `zsmul` implemented using `Nat.binaryRec` blocked-by-other-PR awaiting-author merge-conflict t-algebra opened from a branch in the main mathlib repo (not a fork)
6603 tydeu feat: automatically try `cache get` before build WIP merge-conflict CI opened from a branch in the main mathlib repo (not a fork)
6058 apurvnakade feat: duality theory for cone programs WIP merge-conflict t-analysis opened from a branch in the main mathlib repo (not a fork)
6449 ADedecker feat: functions with finite fibers awaiting-author merge-conflict t-topology opened from a branch in the main mathlib repo (not a fork)
13163 erdOne feat(.vscode/module-docstring.code-snippet): Prevent auto-complete from firing on `do` awaiting-author t-meta opened from a branch in the main mathlib repo (not a fork)
13791 digama0 refactor: Primrec and Partrec merge-conflict t-computability tech debt opened from a branch in the main mathlib repo (not a fork)
11964 adamtopaz feat: The functor of points of a scheme merge-conflict t-category-theory t-algebraic-geometry opened from a branch in the main mathlib repo (not a fork)
12418 rosborn style: replace preimage_val with ↓∩ notation merge-conflict opened from a branch in the main mathlib repo (not a fork)
9978 FR-vdash-bot chore(FieldTheory/KummerExtension): move some lemmas earlier awaiting-author merge-conflict t-algebra opened from a branch in the main mathlib repo (not a fork)
12429 adomani feat: toND -- auto-generating natDegree awaiting-author merge-conflict t-meta RFC t-algebra opened from a branch in the main mathlib repo (not a fork)
12751 Command-Master feat: add lemmas for Nat/Bits, Nat/Bitwise and Nat/Size merge-conflict new-contributor t-data opened from a branch in the main mathlib repo (not a fork)
15448 urkud chore(*): deprecate `Option.elim'` awaiting-author merge-conflict tech debt ??? opened from a branch in the main mathlib repo (not a fork)
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 ??? opened from a branch in the main mathlib repo (not a fork)
13573 Shamrock-Frost feat: add multivariate polynomial modules awaiting-author merge-conflict t-algebra opened from a branch in the main mathlib repo (not a fork)
6517 MohanadAhmed feat: discrete Fourier transform of a finite sequence awaiting-author merge-conflict t-algebra opened from a branch in the main mathlib repo (not a fork)
13155 alreadydone feat(NumberTheory/EllipticDivisibilitySequence): show elliptic relations follow from even-odd recursion awaiting-author merge-conflict t-number-theory t-algebra opened from a branch in the main mathlib repo (not a fork)
15600 adomani feat: lint also `let` vs `have` WIP merge-conflict t-linter opened from a branch in the main mathlib repo (not a fork)
16253 Shreyas4991 feat: Basics of Discrete Fair Division in Mathlib WIP awaiting-author ⚠️ opened from a branch in the main mathlib repo (not a fork)
15121 Eloitor feat: iff theorems for IsSplitEpi and IsSplitMono in opposite category awaiting-author t-category-theory new-contributor opened from a branch in the main mathlib repo (not a fork)
15895 madvorak feat(Computability/ContextFreeGrammar): mapping between two types of nonterminal symbols WIP t-computability opened from a branch in the main mathlib repo (not a fork)
14038 adomani test/decl diff in lean dev WIP merge-conflict opened from a branch in the main mathlib repo (not a fork)
7861 shuxuezhuyi feat(Geometry/Hyperbolic/UpperHalfPlane): instance IsometricSMul PSL(2, ℝ) ℍ blocked-by-other-PR merge-conflict t-euclidean-geometry opened from a branch in the main mathlib repo (not a fork)
16570 yuma-mizuno chore(Tactic/CategoryTheory): change `TermElabM` to `MetaM` WIP t-meta opened from a branch in the main mathlib repo (not a fork)
10591 adri326 feat(Topology/Algebra/ConstMulAction): properties of continuous actions in Hausdorff spaces awaiting-author t-topology t-algebra opened from a branch in the main mathlib repo (not a fork)
7545 shuxuezhuyi feat: APIs of `Function.extend f g e'` when `f` is injective awaiting-author merge-conflict t-logic opened from a branch in the main mathlib repo (not a fork)
14078 Ruben-VandeVelde feat(CI): continue after mk_all fails awaiting-author merge-conflict CI opened from a branch in the main mathlib repo (not a fork)
11283 hmonroe feat(ModelTheory/Satisfiability): define theory with independent sentence WIP merge-conflict t-logic opened from a branch in the main mathlib repo (not a fork)
16914 siddhartha-gadgil Loogle syntax with non-reserved WIP merge-conflict opened from a branch in the main mathlib repo (not a fork)
13782 alreadydone feat(EllipticCurve): ZSMul formula in terms of division polynomials blocked-by-other-PR merge-conflict t-number-theory t-algebraic-geometry t-algebra opened from a branch in the main mathlib repo (not a fork)
8118 iwilare feat(CategoryTheory): add dinatural transformations awaiting-author merge-conflict t-category-theory opened from a branch in the main mathlib repo (not a fork)
14242 js2357 feat: Prove equivalence of `isDedekindDomain` and `isDedekindDomainDvr` blocked-by-other-PR merge-conflict t-algebra new-contributor opened from a branch in the main mathlib repo (not a fork)
7516 ADedecker perf: use `abbrev` to prevent unifying useless data WIP merge-conflict opened from a branch in the main mathlib repo (not a fork)
17127 FR-vdash-bot chore: remove global `Quotient.mk` `⟦·⟧` notation merge-conflict t-data opened from a branch in the main mathlib repo (not a fork)
16887 metinersin feat(ModelTheory/Complexity): define conjunctive and disjunctive formulas blocked-by-other-PR merge-conflict t-logic new-contributor opened from a branch in the main mathlib repo (not a fork)
16888 metinersin feat(ModelTheory/Complexity): Define conjunctive and disjunctive normal forms blocked-by-other-PR merge-conflict t-logic new-contributor opened from a branch in the main mathlib repo (not a fork)
16889 metinersin feat(ModelTheory/Complexity): Normal forms blocked-by-other-PR merge-conflict t-logic new-contributor opened from a branch in the main mathlib repo (not a fork)
14712 FR-vdash-bot perf: change instance priority and order about `OfNat` delegated merge-conflict t-algebra slow-typeclass-synthesis opened from a branch in the main mathlib repo (not a fork)
5995 FR-vdash-bot feat: add APIs about `Quotient.choice` awaiting-author merge-conflict RFC t-data opened from a branch in the main mathlib repo (not a fork)
13156 erdOne refactor(Algebra/Module/LocalizedModule): Redefine `LocalizedModule` in terms of `OreLocalization`. merge-conflict t-algebra opened from a branch in the main mathlib repo (not a fork)
16348 urkud refactor(Topology): require `LinearOrder` with `OrderTopology` awaiting-author merge-conflict t-topology t-order opened from a branch in the main mathlib repo (not a fork)
13965 pechersky feat(Data/DigitExpansion): reals via digit expansion are complete blocked-by-other-PR merge-conflict t-data opened from a branch in the main mathlib repo (not a fork)
10796 mcdoll feat(Tactic/Positivity): non-negativity of functions WIP t-meta opened from a branch in the main mathlib repo (not a fork)
12750 Command-Master feat: define Gray code blocked-by-other-PR awaiting-author merge-conflict new-contributor t-data opened from a branch in the main mathlib repo (not a fork)
14603 awueth feat: degree is invariant under graph isomorphism WIP t-combinatorics new-contributor opened from a branch in the main mathlib repo (not a fork)
16925 YnirPaz feat(SetTheory/Cardinal/Cofinality): aleph index of singular cardinal has infinite cofinality WIP merge-conflict t-set-theory opened from a branch in the main mathlib repo (not a fork)
9605 davikrehalt feat(Data/Finset & List): Add Lemmas for Sorting and Filtering awaiting-author please-adopt merge-conflict new-contributor t-data opened from a branch in the main mathlib repo (not a fork)
13514 madvorak feat(Computability/ContextFreeGrammar): closure under union blocked-by-other-PR merge-conflict t-computability opened from a branch in the main mathlib repo (not a fork)
9654 urkud feat: add `@[mk_eq]` version of `@[mk_iff]` awaiting-author merge-conflict t-meta opened from a branch in the main mathlib repo (not a fork)
16704 AntoineChambert-Loir feat(Mathlib.Data.Ordering.Dickson): Dickson orders WIP merge-conflict t-order opened from a branch in the main mathlib repo (not a fork)
16355 Ruben-VandeVelde feat: odd_{add,sub}_one awaiting-author merge-conflict t-number-theory t-algebra opened from a branch in the main mathlib repo (not a fork)
8479 alexjbest feat: use leaff in CI WIP awaiting-author merge-conflict ⚠️ opened from a branch in the main mathlib repo (not a fork)
14598 Command-Master chore: add typeclasses to unify various `add_top`, `add_eq_top`, etc. merge-conflict t-algebra t-order new-contributor opened from a branch in the main mathlib repo (not a fork)
16885 metinersin feat(ModelTheory/Complexity): define literals awaiting-author merge-conflict t-logic new-contributor opened from a branch in the main mathlib repo (not a fork)
18716 jjaassoonn feat(Algebra/Module/GradedModule): quotient and subgrading WIP blocked-by-other-PR merge-conflict awaiting-CI t-algebra opened from a branch in the main mathlib repo (not a fork)
9341 winstonyin feat: Naturality of integral curves awaiting-author merge-conflict t-differential-geometry opened from a branch in the main mathlib repo (not a fork)
13248 hcWang942 feat: basic concepts of auction theory awaiting-author merge-conflict t-logic new-contributor opened from a branch in the main mathlib repo (not a fork)
9344 erdOne feat: Add `AddGroup.FG` -> `Module.Finite ℤ` as instances awaiting-author merge-conflict t-algebra opened from a branch in the main mathlib repo (not a fork)
12133 ADedecker feat: generalize instIsLowerProd to arbitrary products awaiting-author merge-conflict t-topology t-order opened from a branch in the main mathlib repo (not a fork)
16637 FR-vdash-bot perf: reorder `extends` of `(Add)Monoid` WIP merge-conflict t-algebra opened from a branch in the main mathlib repo (not a fork)
8661 joelriou feat(CategoryTheory/Sites): descent of sheaves WIP merge-conflict t-category-theory opened from a branch in the main mathlib repo (not a fork)
10476 shuxuezhuyi feat(Topology/UniformSpace): define uniform preordered space awaiting-author merge-conflict t-topology opened from a branch in the main mathlib repo (not a fork)
17593 FR-vdash-bot chore(Algebra/Order/GroupWithZero/Unbundled): deprecate useless lemmas, use `ZeroLEOneClass` blocked-by-other-PR merge-conflict t-algebra t-order opened from a branch in the main mathlib repo (not a fork)
17623 FR-vdash-bot feat(Algebra/Order/GroupWithZero/Unbundled): add some lemmas merge-conflict t-algebra t-order awaiting-zulip opened from a branch in the main mathlib repo (not a fork)
17624 FR-vdash-bot feat(Algebra/Order/GroupWithZero/Unbundled): generalize lemmas blocked-by-other-PR merge-conflict t-algebra t-order opened from a branch in the main mathlib repo (not a fork)
17513 FR-vdash-bot perf: do not search algebraic hierarchies when using `map_*` lemmas WIP merge-conflict t-algebra awaiting-bench opened from a branch in the main mathlib repo (not a fork)
17515 FR-vdash-bot perf: do not need `simp low` now blocked-by-other-PR merge-conflict t-algebra opened from a branch in the main mathlib repo (not a fork)
19212 Julian feat(LinearAlgebra): add a variable_alias for VectorSpace merge-conflict t-algebra opened from a branch in the main mathlib repo (not a fork)
19337 zeramorphic feat(Data/Finsupp): generalise `Finsupp` to any "zero" value merge-conflict t-data opened from a branch in the main mathlib repo (not a fork)
10332 adri326 feat(Topology/Sets): define regular open sets and their boolean algebra WIP merge-conflict t-topology opened from a branch in the main mathlib repo (not a fork)
18756 astrainfinita refactor: deprecate `DistribMulActionSemiHomClass` `MulSemiringActionSemiHomClass` merge-conflict t-algebra opened from a branch in the main mathlib repo (not a fork)
19125 yhtq feat: add theorems to transfer `IsGalois` between pairs of fraction rings merge-conflict t-algebra new-contributor opened from a branch in the main mathlib repo (not a fork)
18841 hrmacbeth chore: change some `linarith`s to `linear_combination`s WIP merge-conflict opened from a branch in the main mathlib repo (not a fork)
11142 hmonroe feat(ProofTheory): Define logical symbols abstractly; opens new top-level section, drawing from lean4-logic awaiting-author merge-conflict t-logic opened from a branch in the main mathlib repo (not a fork)
11210 hmonroe Test commit WIP merge-conflict opened from a branch in the main mathlib repo (not a fork)
19621 Command-Master feat: Multiplicity and prime-adic valuation of derivations blocked-by-other-PR merge-conflict t-algebra large-import opened from a branch in the main mathlib repo (not a fork)
18262 joelriou feat(Algebra/Category/ModuleCat/Presheaf): exterior powers of presheaves of modules WIP blocked-by-other-PR merge-conflict t-category-theory t-algebra opened from a branch in the main mathlib repo (not a fork)
15269 kkytola feat: Add ENNReal.floor blocked-by-other-PR awaiting-author merge-conflict t-algebra t-order opened from a branch in the main mathlib repo (not a fork)
15773 kkytola feat: Add type class for ENat-valued floor functions awaiting-author merge-conflict t-order opened from a branch in the main mathlib repo (not a fork)
3251 kmill feat: deriving `LinearOrder` for simple enough inductive types WIP awaiting-author merge-conflict t-meta opened from a branch in the main mathlib repo (not a fork)
3610 TimothyGu feat: derive Infinite automatically for inductive types awaiting-author merge-conflict t-meta merge conflict
16120 awainverse feat(ModelTheory/Algebra/Ring/Basic): Ring homomorphisms are a `StrongHomClass` for the language of rings merge-conflict RFC t-algebra t-logic opened from a branch in the main mathlib repo (not a fork)
20459 Ruben-VandeVelde chore: fix names of roots_C_mul_X_{add,sub}_C_of_IsUnit awaiting-author t-algebra opened from a branch in the main mathlib repo (not a fork)
20527 trivial1711 refactor(Topology/UniformSpace/Completion): more descriptive names for `α → Completion α` merge-conflict t-topology opened from a branch in the main mathlib repo (not a fork)
17739 Aaron1011 feat(Topology/Order/DenselyOrdered): prove Not (IsOpen) for intervals awaiting-author merge-conflict t-topology new-contributor opened from a branch in the main mathlib repo (not a fork)
18474 FR-vdash-bot perf: lower the priority of `*WithOne.to*` instances merge-conflict t-algebra slow-typeclass-synthesis t-data opened from a branch in the main mathlib repo (not a fork)
20656 Komyyy feat(Mathlib/Geometry/Manifold/VectorBundle/Sphere): convert orthogonal smooth `M → 𝕊ⁿ` & `M → ℝⁿ⁺¹` to smooth `M → T𝕊ⁿ` please-adopt merge-conflict t-differential-geometry opened from a branch in the main mathlib repo (not a fork)
15711 znssong feat(Combinatorics/SimpleGraph): Some lemmas about walk, cycle and Hamiltonian cycle awaiting-author merge-conflict t-combinatorics new-contributor opened from a branch in the main mathlib repo (not a fork)
15720 znssong feat(SimpleGraph): The Bondy-Chvátal theorem blocked-by-other-PR merge-conflict t-combinatorics new-contributor opened from a branch in the main mathlib repo (not a fork)
18629 tomaz1502 feat(Computability.Timed): Formalization of runtime complexity of List.merge awaiting-author merge-conflict new-contributor t-computability opened from a branch in the main mathlib repo (not a fork)
8362 urkud feat(Asymptotics): define `ReflectsGrowth` awaiting-author merge-conflict t-analysis opened from a branch in the main mathlib repo (not a fork)
6692 prakol16 feat: disjoint indexed union of local homeomorphisms awaiting-author merge-conflict t-topology opened from a branch in the main mathlib repo (not a fork)
18461 hannahfechtner feat: left and right common multiples mixins awaiting-author t-algebra new-contributor opened from a branch in the main mathlib repo (not a fork)
19291 PieterCuijpers feat(Algebra/Order/Hom): add quantale homomorphism awaiting-author merge-conflict t-algebra new-contributor opened from a branch in the main mathlib repo (not a fork)
19352 hrmacbeth chore: change some `nlinarith`s to `linear_combination`s WIP merge-conflict opened from a branch in the main mathlib repo (not a fork)
20372 jvlmdr feat(MeasureTheory/Function): Add ContinuousLinearMap.bilinearCompLp(L) merge-conflict t-measure-probability new-contributor opened from a branch in the main mathlib repo (not a fork)
2605 eric-wieser chore: better error message in linarith awaiting-author merge-conflict t-meta opened from a branch in the main mathlib repo (not a fork)
11837 trivial1711 feat: completion of a uniform multiplicative group help-wanted WIP merge-conflict t-topology t-algebra opened from a branch in the main mathlib repo (not a fork)
12670 trivial1711 feat: completion of a nonarchimedean multiplicative group blocked-by-other-PR merge-conflict t-topology t-algebra opened from a branch in the main mathlib repo (not a fork)
9449 hmonroe feat: Add Turing machine with the quintet definition (TMQ) and a chainable step function for each TM type awaiting-author merge-conflict t-computability opened from a branch in the main mathlib repo (not a fork)
19697 quangvdao feat(BigOperators/Fin): Sum/product over `Fin` intervals awaiting-author merge-conflict t-data opened from a branch in the main mathlib repo (not a fork)
19353 hrmacbeth chore: golf some term/rw proofs using `linear_combination` WIP merge-conflict opened from a branch in the main mathlib repo (not a fork)
20248 peabrainiac feat(Topology/Compactness): first-countable locally path-connected spaces are delta-generated blocked-by-other-PR awaiting-author merge-conflict t-topology new-contributor large-import opened from a branch in the main mathlib repo (not a fork)
10678 adri326 feat(Topology/UniformSpace): prove that a uniform space is completely regular awaiting-author merge-conflict t-topology opened from a branch in the main mathlib repo (not a fork)
18785 erdOne feat(CategoryTheory): command that generates instances for `MorphismProperty` awaiting-author merge-conflict t-meta t-category-theory opened from a branch in the main mathlib repo (not a fork)
16311 madvorak feat(Computability): regular languages are context-free WIP merge-conflict t-computability opened from a branch in the main mathlib repo (not a fork)
19943 AlexLoitzl feat(Computability): Add Chomsky Normal Form Grammar and translation awaiting-author merge-conflict new-contributor t-computability opened from a branch in the main mathlib repo (not a fork)
17005 YnirPaz feat(SetTheory/Cardinal/Regular): define singular cardinals WIP merge-conflict t-set-theory opened from a branch in the main mathlib repo (not a fork)
21501 sksgurdldi feat(List): add sum_zipWith_eq_finset_sum awaiting-author t-algebra new-contributor opened from a branch in the main mathlib repo (not a fork)
12054 adomani feat: auto-bugs awaiting-author merge-conflict t-meta opened from a branch in the main mathlib repo (not a fork)
5062 adomani feat(Tactic/Prune + test/Prune): add `prune` tactic, for removing unnecessary hypotheses awaiting-author modifies-tactic-syntax merge-conflict t-meta opened from a branch in the main mathlib repo (not a fork)
21433 grunweg chore: change more lemmas to be about enorm instead of nnnorm awaiting-author merge-conflict t-measure-probability carleson opened from a branch in the main mathlib repo (not a fork)
20454 urkud chore(TangentCone): review names merge-conflict t-analysis opened from a branch in the main mathlib repo (not a fork)
16550 awainverse feat(ModelTheory): A typeclass for languages expanding other languages awaiting-author merge-conflict t-logic opened from a branch in the main mathlib repo (not a fork)
14313 grhkm21 feat(RepresentationTheory/FdRep): FdRep is a full subcategory of Rep merge-conflict t-category-theory t-algebra new-contributor opened from a branch in the main mathlib repo (not a fork)
10823 alexkeizer feat: convert curried type functions into uncurried type functions awaiting-author merge-conflict t-data opened from a branch in the main mathlib repo (not a fork)
13648 urkud feat(Topology/Module): generalize `ContinuousLinearMap.compSL` awaiting-author merge-conflict t-topology t-analysis t-algebra opened from a branch in the main mathlib repo (not a fork)
14060 YnirPaz feat(SetTheory/Ordinal/Clubs): define club sets and prove basic properties blocked-by-other-PR merge-conflict t-logic new-contributor opened from a branch in the main mathlib repo (not a fork)
20636 eric-wieser feat: multiplication of intervals in rings awaiting-author t-algebra opened from a branch in the main mathlib repo (not a fork)
16000 YaelDillies feat: Croot-Sisask Almost Periodicity blocked-by-other-PR t-combinatorics t-analysis opened from a branch in the main mathlib repo (not a fork)
22340 sinhp feat(CategoryTheory): Locally Cartesian Closed Categories (Beck-Chevalley Conditions) WIP blocked-by-other-PR merge-conflict t-category-theory large-import opened from a branch in the main mathlib repo (not a fork)
21959 BGuillemet feat(Topology/ContinuousMap): Stone-Weierstrass theorem for MvPolynomial merge-conflict t-topology new-contributor opened from a branch in the main mathlib repo (not a fork)
18470 FR-vdash-bot perf: lower the priority of `Normed*.to*` instances merge-conflict t-analysis t-algebra slow-typeclass-synthesis ❌? opened from a branch in the main mathlib repo (not a fork)
16944 YnirPaz feat(SetTheory/Cardinal/Cofinality): lemmas about limit ordinals and cofinality WIP merge-conflict t-set-theory opened from a branch in the main mathlib repo (not a fork)
17368 Felix-Weilacher feat(Topology/Baire/BaireMeasurable): add the Kuratowski-Ulam theorem merge-conflict t-topology opened from a branch in the main mathlib repo (not a fork)
8767 eric-wieser refactor(Cache): tidy lake-manifest parsing in Cache merge-conflict t-meta opened from a branch in the main mathlib repo (not a fork)
15578 znssong feat(Function): Fixed points of function `f` with `f(x) >= x` awaiting-author merge-conflict t-analysis new-contributor opened from a branch in the main mathlib repo (not a fork)
22660 Ruben-VandeVelde chore: follow naming convention around Group.IsNilpotent merge-conflict t-algebra opened from a branch in the main mathlib repo (not a fork)
13999 adomani feat: a linter to flag potential confusing conventions awaiting-author merge-conflict t-linter opened from a branch in the main mathlib repo (not a fork)
19013 quangvdao feat(Algebra/BigOperators/Fin): Add `finSigmaFinEquiv` awaiting-author merge-conflict t-algebra opened from a branch in the main mathlib repo (not a fork)
19189 YnirPaz feat(SetTheory/Ordinal/Arithmetic): order isomorphism between omega and the natural numbers awaiting-author merge-conflict t-set-theory opened from a branch in the main mathlib repo (not a fork)
19227 adomani fix(CI): unwrap `lake test` in problem matcher awaiting-author merge-conflict CI opened from a branch in the main mathlib repo (not a fork)
15774 kkytola feat: Topology on `ENat` WIP merge-conflict t-topology t-order opened from a branch in the main mathlib repo (not a fork)
20222 eric-wieser feat: generalize lemmas about derivatives blocked-by-other-PR merge-conflict t-analysis opened from a branch in the main mathlib repo (not a fork)
21018 markimunro feat(Data/Matrix): add file with key definitions and theorems about elementary row operations enhancement awaiting-author merge-conflict new-contributor t-data opened from a branch in the main mathlib repo (not a fork)
23514 eric-wieser refactor: smooth over Lattice/LinearOrder inheritance merge-conflict opened from a branch in the main mathlib repo (not a fork)
22810 pechersky feat(Counterexamples): metric space not induced by norm WIP merge-conflict t-topology t-analysis opened from a branch in the main mathlib repo (not a fork)
13124 FR-vdash-bot chore: remove `CovariantClass` and `ContravariantClass` WIP merge-conflict opened from a branch in the main mathlib repo (not a fork)
19275 eric-wieser fix: if nolint files change, do a full rebuild delegated merge-conflict opened from a branch in the main mathlib repo (not a fork)
15212 victorliu5296 feat: Add fundamental theorem of calculus-2 for Banach spaces awaiting-author merge-conflict t-analysis t-measure-probability new-contributor opened from a branch in the main mathlib repo (not a fork)
22888 plp127 perf: replace `Lean.Expr.swapBVars` with a better? implementation awaiting-author t-meta opened from a branch in the main mathlib repo (not a fork)
22579 kvanvels doc(Topology/Defs/Induced): fix comments on three functions related to RestrictGenTopology documentation awaiting-author merge-conflict t-topology opened from a branch in the main mathlib repo (not a fork)
21488 imbrem feat(CategoryTheory/Monoidal): premonoidal categories merge-conflict t-category-theory new-contributor opened from a branch in the main mathlib repo (not a fork)
21525 sinhp feat(CategoryTheory): Locally Cartesian Closed Categories (Prelim) merge-conflict t-category-theory large-import opened from a branch in the main mathlib repo (not a fork)
22319 sinhp feat(CategoryTheory): Locally Cartesian Closed Categories (Sections Right Adjoint) blocked-by-other-PR merge-conflict t-category-theory large-import opened from a branch in the main mathlib repo (not a fork)
22321 sinhp feat(CategoryTheory): Locally Cartesian Closed Categories (Definition) blocked-by-other-PR merge-conflict t-category-theory large-import opened from a branch in the main mathlib repo (not a fork)
19425 hrmacbeth perf: gcongr forward-reasoning adjustment awaiting-author merge-conflict opened from a branch in the main mathlib repo (not a fork)
20873 vbeffara feat(Topology/Covering): path lifting and homotopy lifting awaiting-author merge-conflict t-topology new-contributor opened from a branch in the main mathlib repo (not a fork)
22817 peabrainiac feat(CategoryTheory/Sites): local sites WIP merge-conflict t-category-theory opened from a branch in the main mathlib repo (not a fork)
16314 FR-vdash-bot chore(Data/Quot): deprecate `ind*'` APIs merge-conflict t-data opened from a branch in the main mathlib repo (not a fork)
23509 eric-wieser refactor: Make ENNReal an abbrev merge-conflict t-data opened from a branch in the main mathlib repo (not a fork)
11455 adomani fix: unsqueeze simp, re Yaël's comments on #11259 awaiting-author merge-conflict opened from a branch in the main mathlib repo (not a fork)
7325 eric-wieser chore: use preimageIso instead of defeq abuse for InducedCategory merge-conflict awaiting-CI t-category-theory opened from a branch in the main mathlib repo (not a fork)
7874 astrainfinita chore: make `IsScalarTower A A B` and `IsScalarTower A B B` higher priority merge-conflict awaiting-CI t-algebra slow-typeclass-synthesis ??? opened from a branch in the main mathlib repo (not a fork)
13038 adomani feat: Mathlib weekly reports awaiting-author t-meta CI opened from a branch in the main mathlib repo (not a fork)
5952 eric-wieser feat: add Qq wrappers for ToExpr merge-conflict t-meta awaiting-CI opened from a branch in the main mathlib repo (not a fork)
15483 FR-vdash-bot chore(GroupTheory/Coset): reduce defeq abuse merge-conflict t-algebra opened from a branch in the main mathlib repo (not a fork)
16594 FR-vdash-bot perf: reorder `extends` and remove some instances in algebra hierarchy merge-conflict t-algebra slow-typeclass-synthesis opened from a branch in the main mathlib repo (not a fork)
19467 quangvdao feat(MvPolynomial/Equiv): Add `MvPolynomial.finSuccEquivNth` blocked-by-other-PR merge-conflict t-algebra opened from a branch in the main mathlib repo (not a fork)
20313 thefundamentaltheor3m feat(Data/Complex/Exponential): prove some useful results about the complex exponential. merge-conflict t-analysis new-contributor opened from a branch in the main mathlib repo (not a fork)
22698 Kiolt feat: notation for whisker(Left/Right)Iso merge-conflict t-category-theory toric opened from a branch in the main mathlib repo (not a fork)
19613 madvorak refactor(Combinatorics/Optimization/ValuedCSP): make only valid `FractionalOperation` possible t-combinatorics opened from a branch in the main mathlib repo (not a fork)
20730 kuotsanhsu feat(LinearAlgebra/Matrix/SchurTriangulation): prove Schur decomposition/triangulation awaiting-author merge-conflict t-algebra new-contributor opened from a branch in the main mathlib repo (not a fork)
19117 eric-wieser feat: derivatives of matrix operations WIP merge-conflict t-analysis opened from a branch in the main mathlib repo (not a fork)
12605 FR-vdash-bot chore: attribute [induction_eliminator] awaiting-author merge-conflict opened from a branch in the main mathlib repo (not a fork)
23859 urkud feat(Topology/../Order/Field): generalize to `Semifield` merge-conflict t-topology opened from a branch in the main mathlib repo (not a fork)
24219 Paul-Lez feat: linear independence of the tensor product of two linearly independent families WIP t-algebra toric opened from a branch in the main mathlib repo (not a fork)
23810 b-reinke chore(Order/Interval): generalize succ/pred lemmas to partial orders merge-conflict t-order opened from a branch in the main mathlib repo (not a fork)
24285 madvorak chore(Algebra/*-{Category,Homology}): remove unnecessary universe variables merge-conflict t-algebra opened from a branch in the main mathlib repo (not a fork)
8370 eric-wieser refactor(Analysis/NormedSpace/Exponential): remove the `𝕂` argument from `exp` merge-conflict t-analysis awaiting-zulip opened from a branch in the main mathlib repo (not a fork)
22583 imathwy feat: affinespace homeomorphism awaiting-author merge-conflict t-algebra opened from a branch in the main mathlib repo (not a fork)
23593 erdOne feat(AlgebraicGeometry): the tilde construction is functorial awaiting-author merge-conflict t-algebraic-geometry opened from a branch in the main mathlib repo (not a fork)
21065 eric-wieser feat: generalize `tangentConeAt.lim_zero` to TVS WIP merge-conflict t-analysis opened from a branch in the main mathlib repo (not a fork)
22721 grunweg chore(MeasureTheory/Function/LpSeminorm/Basic): generalise more results to enorm classes WIP merge-conflict t-measure-probability carleson opened from a branch in the main mathlib repo (not a fork)
14731 adomani feat: the repeated typeclass assumption linter WIP merge-conflict t-linter large-import opened from a branch in the main mathlib repo (not a fork)
13649 FR-vdash-bot chore: redefine `Nat.div2` `Nat.bodd` merge-conflict opened from a branch in the main mathlib repo (not a fork)
24549 grunweg feat: define embedded submanifolds, attempt 1 WIP blocked-by-other-PR merge-conflict t-differential-geometry opened from a branch in the main mathlib repo (not a fork)
22809 b-reinke feat: Category algebras and path algebras WIP t-category-theory t-algebra new-contributor opened from a branch in the main mathlib repo (not a fork)
14675 adomani dev: the repeated variable linter WIP merge-conflict t-linter opened from a branch in the main mathlib repo (not a fork)
14330 Ruben-VandeVelde chore: split Mathlib.Algebra.Star.Basic awaiting-author merge-conflict opened from a branch in the main mathlib repo (not a fork)
8511 eric-wieser refactor(MeasureTheory/Measure/Haar/Basic): partially generalize to the affine case awaiting-author merge-conflict t-measure-probability opened from a branch in the main mathlib repo (not a fork)
7994 ericrbg chore: generalize `LieSubalgebra.mem_map_submodule` please-adopt merge-conflict t-algebra opened from a branch in the main mathlib repo (not a fork)
6317 eric-wieser refactor(Data/Finsupp/Defs): make Finsupp.single defeq to Pi.single WIP merge-conflict t-data opened from a branch in the main mathlib repo (not a fork)
11524 mcdoll refactor: Introduce type-class for SchwartzMap WIP merge-conflict t-analysis opened from a branch in the main mathlib repo (not a fork)
11003 thorimur chore: migrate to `tfae` block tactic WIP blocked-by-other-PR merge-conflict t-meta opened from a branch in the main mathlib repo (not a fork)
22488 smmercuri fix: lower priority for `UniformSpace.Completion.instSMul` awaiting-author t-topology FLT opened from a branch in the main mathlib repo (not a fork)
23546 JovanGerb feat(LinearAlgebra/AffineSpace/AffineSubspace): rename `AffineSubspace.mk'` to `Submodule.shift` merge-conflict t-euclidean-geometry opened from a branch in the main mathlib repo (not a fork)
15654 TpmKranz feat(Computability): language-preserving maps between NFA and RE blocked-by-other-PR merge-conflict new-contributor t-computability awaiting-zulip opened from a branch in the main mathlib repo (not a fork)
19315 quangvdao feat(Data/Finsupp/Fin): Add `Finsupp` operations on `Fin` tuple awaiting-author merge-conflict t-data opened from a branch in the main mathlib repo (not a fork)
24155 eric-wieser feat: add a "rw_proc" for fin vectors awaiting-author t-meta RFC t-data opened from a branch in the main mathlib repo (not a fork)
21276 GabinKolly feat(ModelTheory/Substructures): define equivalences between equal substructures awaiting-author t-logic opened from a branch in the main mathlib repo (not a fork)
24008 meithecatte chore(EpsilonNFA): replace manual lemmas with @[simps] awaiting-author new-contributor t-computability opened from a branch in the main mathlib repo (not a fork)
24642 grunweg WIP-feat: add layercake formula for ENNReal-valued functions WIP merge-conflict t-analysis carleson opened from a branch in the main mathlib repo (not a fork)
21712 grunweg chore: generalise more lemmas to `ContinuousENorm` merge-conflict awaiting-CI t-measure-probability carleson opened from a branch in the main mathlib repo (not a fork)
21375 grunweg WIP: generalise lemmas to ENorm WIP merge-conflict awaiting-CI t-measure-probability carleson opened from a branch in the main mathlib repo (not a fork)
24618 b-mehta feat(Analysis): add Schur inequality and variants WIP t-analysis opened from a branch in the main mathlib repo (not a fork)
15115 kkytola feat: Generalize assumptions in liminf and limsup results in ENNReals help-wanted awaiting-author merge-conflict t-topology t-order opened from a branch in the main mathlib repo (not a fork)
24957 eric-wieser feat: use ` binderNameHint` in sum_congr t-algebra opened from a branch in the main mathlib repo (not a fork)
23349 BGuillemet feat: add LocallyLipschitzOn.lipschitzOnWith_of_isCompact and two small lemmas about Lipschitz functions merge-conflict t-topology new-contributor large-import opened from a branch in the main mathlib repo (not a fork)
12438 jjaassoonn feat: some APIs for flat modules WIP merge-conflict t-category-theory opened from a branch in the main mathlib repo (not a fork)
8740 digama0 fix: improve `recall` impl / error reporting awaiting-author merge-conflict t-meta awaiting-CI opened from a branch in the main mathlib repo (not a fork)
25473 adomani feat(CI): check that Mathlib files have lean or md extension delegated CI opened from a branch in the main mathlib repo (not a fork)
16020 adomani feat: compare PR `olean`s size with `master` merge-conflict CI opened from a branch in the main mathlib repo (not a fork)
16062 adomani Test/ci olean size WIP awaiting-author merge-conflict CI opened from a branch in the main mathlib repo (not a fork)
12799 jstoobysmith feat(LinearAlgebra/UnitaryGroup): Add properties of Special Unitary Group awaiting-author please-adopt merge-conflict t-algebra new-contributor opened from a branch in the main mathlib repo (not a fork)
23709 plp127 feat: `Nat.findFrom` merge-conflict t-data opened from a branch in the main mathlib repo (not a fork)
25340 dupuisf chore(Analysis/Convex): move files pertaining to convex/concave functions to their own folder merge-conflict t-convex-geometry opened from a branch in the main mathlib repo (not a fork)
21734 adomani fix(PR summary): checkout GITHUB_SHA WIP awaiting-author merge-conflict CI opened from a branch in the main mathlib repo (not a fork)
13483 adomani feat: automatically replace deprecations awaiting-author delegated merge-conflict t-meta opened from a branch in the main mathlib repo (not a fork)
20334 miguelmarco feat: allow polyrith to use a local Singular/Sage install awaiting-author merge-conflict t-meta new-contributor opened from a branch in the main mathlib repo (not a fork)
25912 BoltonBailey feat: add simp lemmas for trig functions on `π * 2⁻¹` blocked-by-other-PR awaiting-author t-analysis blocked on another PR
23953 b-reinke feat(Data/Matroid/Tutte): define the Tutte polynomial of a matroid WIP merge-conflict t-data opened from a branch in the main mathlib repo (not a fork)
25921 BoltonBailey feat: scripts to analyze overlap between namespaces WIP t-meta migrated-from-branch labelled WIP
18771 joelriou feat(LinearAlgebra/ExteriorPower): exterior powers of free modules are free WIP blocked-by-other-PR merge-conflict t-algebra opened from a branch in the main mathlib repo (not a fork)
18441 ADedecker refactor(AdicTopology): use new API for algebraic filter bases, and factor some code merge-conflict t-topology t-algebra opened from a branch in the main mathlib repo (not a fork)
18439 ADedecker refactor: use new algebraic filter bases API in `FiniteAdeleRing` merge-conflict t-topology t-algebra opened from a branch in the main mathlib repo (not a fork)
18438 ADedecker refactor: adapt `KrullTopology` to the new algebraic filter bases API merge-conflict t-topology t-algebra opened from a branch in the main mathlib repo (not a fork)
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 opened from a branch in the main mathlib repo (not a fork)
18662 joelriou feat(LinearAlgebra/ExteriorPower): generators of the exterior powers WIP blocked-by-other-PR merge-conflict t-algebra opened from a branch in the main mathlib repo (not a fork)
18735 joelriou feat(Algebra/Module): presentation of the exterior power WIP blocked-by-other-PR merge-conflict t-algebra opened from a branch in the main mathlib repo (not a fork)
16801 awainverse feat(ModelTheory/Equivalence): The quotient type of formulas modulo a theory awaiting-author merge-conflict t-logic opened from a branch in the main mathlib repo (not a fork)
17458 urkud refactor(Algebra/Group): make `IsUnit` a typeclass merge-conflict t-algebra awaiting-zulip opened from a branch in the main mathlib repo (not a fork)
17627 hrmacbeth feat: universal properties of vector bundle constructions delegated merge-conflict t-differential-geometry opened from a branch in the main mathlib repo (not a fork)
22928 javra feat(CategoryTheory): infrastructure for inclusion morphisms into products in categories with 0-morphisms merge-conflict t-category-theory opened from a branch in the main mathlib repo (not a fork)
24710 chrisflav chore(Data/Set): `tsum` version of `Set.encard_iUnion_of_finite` for non-finite types merge-conflict t-data opened from a branch in the main mathlib repo (not a fork)
24823 eric-wieser refactor: add `hom` lemmas for the `MonoidalCategory` structure on `ModuleCat` merge-conflict t-algebra opened from a branch in the main mathlib repo (not a fork)
25071 erdOne feat(EllipticCurve): basic API for singular cubics merge-conflict t-algebraic-geometry opened from a branch in the main mathlib repo (not a fork)
25218 kckennylau feat(AlgebraicGeometry): Tate normal form of elliptic curves merge-conflict t-algebraic-geometry new-contributor awaiting-zulip opened from a branch in the main mathlib repo (not a fork)
25561 callesonne feat(Category/Grpd): define the bicategory of groupoids awaiting-author merge-conflict t-category-theory opened from a branch in the main mathlib repo (not a fork)
25988 Multramate refactor(AlgebraicGeometry/EllipticCurve/*): replace Fin 3 with products merge-conflict t-algebraic-geometry merge conflict
26090 grunweg chore: make `finiteness` a default tactic merge-conflict failing CI
26465 joelriou feat(Algebra/Module): presentation of the `PiTensorProduct` blocked-by-other-PR merge-conflict t-algebra file-removed blocked on another PR
26467 joelriou feat(LinearAlgebra): the tensor product of a finite family of free modules is free WIP blocked-by-other-PR merge-conflict t-algebra file-removed blocked on another PR
20784 eric-wieser fix: prevent `exact?` recursing forever on `n = 55` t-set-theory opened from a branch in the main mathlib repo (not a fork)
24405 mcdoll refactor(Topology/Algebra/Module/WeakDual): Clean up merge-conflict t-topology large-import opened from a branch in the main mathlib repo (not a fork)
26647 b-mehta feat(Data/Sym/Sym2): lift commutative operations to sym2 WIP merge-conflict t-data opened from a branch in the main mathlib repo (not a fork)
26067 mapehe feat(Topology/StoneCech): exists_continuous_surjection_from_StoneCech_to_dense_range merge-conflict t-topology merge conflict
10541 Louddy feat(Algebra/SkewMonoidAlgebra/Basic): add SkewMonoidAlgebra WIP merge-conflict t-algebra new-contributor opened from a branch in the main mathlib repo (not a fork)
25999 bjoernkjoshanssen feat(Topology/Compactification): projective line over ℝ is homeomorphic to the one-point compactification of ℝ merge-conflict t-topology failing CI
26994 Paul-Lez feat(Topology/MetricSpace/Pseudo/Defs): add easy lemma about opens in topological spaces awaiting-author easy t-topology awaiting author
26911 JovanGerb chore: fix naming of `mono` and `monotone` delegated merge-conflict merge conflict
25611 erdOne chore(RingTheory): add `Algebra (FractionRing R) (FractionRing S)` merge-conflict t-algebra opened from a branch in the main mathlib repo (not a fork)
18230 digama0 feat(Tactic/ScopedNS): extend `scoped[NS]` to more commands awaiting-author t-meta opened from a branch in the main mathlib repo (not a fork)
25284 alreadydone feat(LinearAlgebra/Contraction): bijectivity of `dualTensorHom` + generalize to CommSemiring awaiting-author merge-conflict t-algebra opened from a branch in the main mathlib repo (not a fork)
22749 joelriou feat(CategoryTheory/Abelian): the Gabriel-Popescu theorem as a localization with respect to a Serre class WIP merge-conflict t-category-theory opened from a branch in the main mathlib repo (not a fork)
26987 joelriou chore: deprecating module LinearAlgebra.PiTensorProduct WIP blocked-by-other-PR merge-conflict t-algebra blocked on another PR
27435 callesonne feat(Normed/Algebra/Logarithm): add FormalMultilinearSeries of logarithm around `1` WIP t-analysis labelled WIP
24668 robertmaxton42 feat(LinearAlgebra): add inductive principle for the free product of algebras blocked-by-other-PR merge-conflict t-algebra opened from a branch in the main mathlib repo (not a fork)
13973 digama0 feat: lake exe refactor, initial framework awaiting-author merge-conflict t-meta opened from a branch in the main mathlib repo (not a fork)
10190 jstoobysmith feat(AlgebraicTopology): add Augmented Simplex Category WIP merge-conflict t-category-theory new-contributor t-algebraic-topology opened from a branch in the main mathlib repo (not a fork)
25914 eric-wieser feat: add an ext lemma for the opposite category awaiting-author merge-conflict awaiting-CI t-category-theory opened from a branch in the main mathlib repo (not a fork)
20208 js2357 feat: Define the localization of a fractional ideal at a prime ideal WIP merge-conflict t-algebra opened from a branch in the main mathlib repo (not a fork)
24260 plp127 feat(Topology): add API for Hereditarily Lindelof spaces awaiting-author merge-conflict t-topology opened from a branch in the main mathlib repo (not a fork)
27813 javra feat: IMO 2025 Q1 WIP IMO labelled WIP
27608 RemyDegenne feat(MeasureTheory): typeclasses for measures with finite moments WIP merge-conflict t-measure-probability labelled WIP
27826 Louddy feat(Subsemiring): mk_eq_zero WIP t-algebra labelled WIP
27050 BoltonBailey doc(Control/Monad/Cont): add docstrings awaiting-author t-data failing CI
27225 eric-wieser refactor(Tactic/Lift): deprecate the third with argument awaiting-author t-meta opened from a branch in the main mathlib repo (not a fork)
25991 Multramate feat(AlgebraicGeometry/EllipticCurve): generalise nonsingular condition merge-conflict t-algebraic-geometry failing CI
25985 Multramate feat(AlgebraicGeometry/EllipticCurve/Jacobian): add equivalences between points and explicit WithZero types merge-conflict t-algebraic-geometry failing CI
25982 Multramate feat(AlgebraicGeometry/EllipticCurve/Group): compute range of baseChange merge-conflict t-algebraic-geometry failing CI
25486 VTrelat feat(SetTheory/ZFC/Integers): define integers in ZFC blocked-by-other-PR merge-conflict new-contributor t-set-theory opened from a branch in the main mathlib repo (not a fork)
25485 VTrelat feat(SetTheory/ZFC/Naturals): define natural numbers in ZFC merge-conflict new-contributor t-set-theory opened from a branch in the main mathlib repo (not a fork)
25484 VTrelat feat(SetTheory/ZFC/Booleans): define Boolean algebra in ZFC blocked-by-other-PR merge-conflict new-contributor t-set-theory opened from a branch in the main mathlib repo (not a fork)
25238 Hagb feat(Tactic/ComputeDegree): add support for scalar multiplication with different types merge-conflict t-meta new-contributor opened from a branch in the main mathlib repo (not a fork)
26385 jjdishere feat(RingTheory/Perfectoid): define integral perfectoid rings WIP merge-conflict t-ring-theory labelled WIP
22909 AntoineChambert-Loir feat(RingTheory/Pure): pure submodules blocked-by-other-PR merge-conflict t-ring-theory opened from a branch in the main mathlib repo (not a fork)
22908 AntoineChambert-Loir feat(RingTheory/Finiteness/Small): tensor product of the system of small submodules blocked-by-other-PR merge-conflict t-ring-theory opened from a branch in the main mathlib repo (not a fork)
22898 AntoineChambert-Loir feat(RingTheory/TensorProduct/DirectLimit/FG): direct limit of finitely generated submodules and tensor product WIP merge-conflict t-ring-theory opened from a branch in the main mathlib repo (not a fork)
20431 erdOne feat(RingTheory/AdicCompletion): monotonicity of adic-completeness awaiting-author merge-conflict t-ring-theory opened from a branch in the main mathlib repo (not a fork)
19596 Command-Master feat(RingTheory/Valuation/PrimeMultiplicity): define `WithTop ℤ`-valued prime multiplicity on a fraction field awaiting-author merge-conflict large-import t-ring-theory opened from a branch in the main mathlib repo (not a fork)
18646 jxjwan feat(RingTheory): isotypic components merge-conflict new-contributor t-ring-theory opened from a branch in the main mathlib repo (not a fork)
17246 pechersky feat(RingTheory/PrimaryDecomposition): PIR of Noetherian under jacobson condition awaiting-author merge-conflict t-ring-theory opened from a branch in the main mathlib repo (not a fork)
21474 erdOne feat(RingTheory): replace `Ring.DimensionLEOne` with `Ring.KrullDimLE` merge-conflict large-import t-ring-theory opened from a branch in the main mathlib repo (not a fork)
11212 shuxuezhuyi feat(GroupTheory/GroupAction): instance `MulAction (β ⧸ H) α` awaiting-author merge-conflict large-import t-group-theory opened from a branch in the main mathlib repo (not a fork)
27886 alreadydone feat(Algebra): (Mv)Polynomial.X is irreducible assuming NoZeroDivisors awaiting-author merge-conflict t-algebra merge conflict
26200 adomani fix: add label when landrun fails merge-conflict CI merge conflict
17469 joelriou feat(Algebra/ModuleCat/Differentials/Presheaf): the presheaf of relative differentials WIP merge-conflict t-category-theory t-algebraic-geometry large-import opened from a branch in the main mathlib repo (not a fork)
27709 kckennylau chore: fix links WIP merge-conflict labelled WIP
28075 tristan-f-r chore(Finsupp/Indicator): make non-classical awaiting-author easy t-data awaiting author
20671 thefundamentaltheor3m feat(Analysis/Asymptotics/SpecificAsymptotics): Proving that 𝛔ₖ(n) = O(nᵏ⁺¹) awaiting-author merge-conflict t-number-theory new-contributor large-import opened from a branch in the main mathlib repo (not a fork)
20267 joelriou feat(CategoryTheory): comma categories are accessible WIP awaiting-author merge-conflict t-category-theory opened from a branch in the main mathlib repo (not a fork)
27451 kckennylau feat(RingTheory/Valuation): define ball, closed ball, and sphere merge-conflict t-ring-theory merge conflict
27987 kckennylau feat(RingTheory/Valuation): define ball, closed ball, and sphere merge-conflict large-import t-ring-theory merge conflict
27444 grunweg feat: generalise more lemmas to enorms WIP carleson ⚠️ labelled WIP
24862 grunweg feat(LocallyIntegrable): generalise more to enorms WIP merge-conflict t-measure-probability carleson opened from a branch in the main mathlib repo (not a fork)
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 opened from a branch in the main mathlib repo (not a fork)
22925 ggranberry feat(Mathlib/PlaceHolder/ToeplitzHausdorff): Toeplitz-Hausdorff help-wanted WIP awaiting-author t-analysis new-contributor will-close-soon opened from a branch in the main mathlib repo (not a fork)
25483 VTrelat chore(Data/Set/Prod, SetTheory/ZFC/Basic): add theorem prod_subset_of_prod and extend ZFC model merge-conflict new-contributor t-data opened from a branch in the main mathlib repo (not a fork)
25401 digama0 feat(Util): SuppressSorry option merge-conflict t-meta opened from a branch in the main mathlib repo (not a fork)
27759 plp127 chore(FreeAbelianGroup): deprecate multiplication merge-conflict t-algebra large-import failing CI
7873 astrainfinita perf: reorder `extends` and change instance priority in algebra hierarchy blocked-by-other-PR merge-conflict t-algebra slow-typeclass-synthesis opened from a branch in the main mathlib repo (not a fork)
27446 grunweg chore: more enorm lemmas WIP merge-conflict carleson labelled WIP
14583 lecopivo fix: make concrete cycle notation local awaiting-author merge-conflict opened from a branch in the main mathlib repo (not a fork)
5897 eric-wieser feat: add a `MonadError` instance for `ContT` awaiting-author t-meta opened from a branch in the main mathlib repo (not a fork)
28502 gilesgshaw feat(Logic/Basic): avoid unnecessary uses of choice blocked-by-other-PR awaiting-author merge-conflict t-logic new-contributor blocked on another PR
28622 alreadydone chore(Mathlib): replace `=>` by `↦` merge-conflict merge conflict
24793 tristan-f-r feat: trace of unitarily similar matrices awaiting-author merge-conflict t-algebra opened from a branch in the main mathlib repo (not a fork)
26645 erdOne feat(RingTheory/PowerSeries): Construction of `Q` such that `P(Q(X)) = X` awaiting-author t-ring-theory awaiting author
28626 alreadydone chore(Archive, Counterexamples): replace => by ↦ merge-conflict merge conflict
26078 kckennylau feat(AlgebraicGeometry): add x, y, px, py for points on elliptic curves awaiting-author t-algebraic-geometry awaiting author
19582 yu-yama feat(GroupExtension/Abelian): define `OfMulDistribMulAction.equivH2` blocked-by-other-PR merge-conflict t-algebra new-contributor opened from a branch in the main mathlib repo (not a fork)
7300 ah1112 feat: synthetic geometry help-wanted awaiting-author merge-conflict t-euclidean-geometry opened from a branch in the main mathlib repo (not a fork)
13795 astrainfinita perf(Algebra/{Group, GroupWithZero, Ring}/InjSurj): reduce everything merge-conflict t-algebra opened from a branch in the main mathlib repo (not a fork)
28150 Equilibris chore: clean up proofs typevec proofs merge-conflict new-contributor t-data merge conflict
25488 VTrelat feat(SetTheory/ZFC/Rationals): define rationals in ZFC blocked-by-other-PR merge-conflict new-contributor t-set-theory opened from a branch in the main mathlib repo (not a fork)
27403 MoritzBeroRoos fix: replace probably erroneous usage of ⬝ (with old \cdot) by · (with \centerdot) merge-conflict new-contributor merge conflict
28042 kckennylau feat(Topology/ValuativeRel): a topological basis indexed by pairs of elements merge-conflict t-ring-theory merge conflict
27399 MoritzBeroRoos chore: replace every usage of ⬝ᵥ (with old \cdot) by ·ᵥ (with \centerdot) merge-conflict new-contributor merge conflict
27479 iu-isgood feat: Abel's Binomial Theorem awaiting-author new-contributor t-data failing CI
28787 alreadydone feat(Counterexamples): a domain whose ring of differences is not a domain blocked-by-other-PR merge-conflict t-algebra large-import blocked on another PR
24719 madvorak feat(LinearAlgebra/Matrix/NonsingularInverse): inverting `Matrix` inverts its `LinearEquiv` awaiting-author t-algebra opened from a branch in the main mathlib repo (not a fork)
27437 kckennylau feat(RingTheory/Valuation): some lemmas about comparing with 1 and 0 and with each other WIP merge-conflict t-ring-theory labelled WIP
28148 kckennylau feat(Matrix): Simproc and Rw-proc for Matrix Transpose merge-conflict t-meta merge conflict
28686 mitchell-horner feat(Combinatorics/SimpleGraph): prove the Erdős-Stone theorem WIP blocked-by-other-PR merge-conflict t-combinatorics blocked on another PR
28687 mitchell-horner feat(Combinatorics/SimpleGraph): prove the Erdős-Stone-Simonovits theorem WIP blocked-by-other-PR merge-conflict t-combinatorics blocked on another PR
28689 mitchell-horner feat(Combinatorics/SimpleGraph): prove well-known corollaries of the Erdős-Stone-Simonovits theorem WIP blocked-by-other-PR merge-conflict t-combinatorics blocked on another PR
26952 robin-carlier feat(CategoryTheory/DayConvolution): monoid objects internal to day convolutions blocked-by-other-PR merge-conflict t-category-theory blocked on another PR
27133 robin-carlier feat(CategoryTheory/Monoidal/DayConvolution): `C ⊛⥤ V` is monoidal closed when `V` is blocked-by-other-PR merge-conflict t-category-theory blocked on another PR
27151 robin-carlier feat(CategoryTheory/Monoidal/DayConvolution): `C ⊛⥤ V` is braided/symmetric when `C` and `V` are braided/symmetric blocked-by-other-PR merge-conflict t-category-theory blocked on another PR
27175 robin-carlier feat(CategoryTheory/Monoidal/DayConvolution): `LawfulDayConvolutionMonoidalCategoryStruct.ι C V D` is monoidal when the target is `C ⊛⥤ V` blocked-by-other-PR merge-conflict t-category-theory blocked on another PR
25741 robin-carlier feat(AlgebraicTopology/SimplexCategory/SimplicialObject): definitions of simplicial objects by generators and relation blocked-by-other-PR merge-conflict t-category-theory large-import t-algebraic-topology blocked on another PR
26931 javra feat(CategoryTheory/Enriched): `V`-enriched isomorphisms awaiting-author merge-conflict t-category-theory infinity-cosmos merge conflict
27707 FLDutchmann feat(NumberTheory/SelbergSieve): define Selberg's weights and prove basic results. blocked-by-other-PR merge-conflict t-number-theory t-analysis blocked on another PR
25208 erdOne feat(LinearAlgebra): `tensor_induction` macro WIP merge-conflict RFC t-algebra opened from a branch in the main mathlib repo (not a fork)
28803 astrainfinita refactor: unbundle algebra from `ENormed*` merge-conflict t-analysis t-algebra slow-typeclass-synthesis awaiting-zulip awaiting a zulip discussion
26935 Paul-Lez feat(Analysis/SpecialFunction/NthRoot): definition and basic API of Real.nthRoot t-analysis failing CI
27995 kckennylau feat(RingTheory/Valuation): alternate constructors for Valuation awaiting-CI t-ring-theory does not pass CI
26159 upobir feat(Algebra/QuadraticDiscriminant): Adding inequalities on quadratic from inequalities on discriminant awaiting-author t-algebra awaiting author
28151 iehality feat(Computability): r.e. sets are closed under inter/union/projection/composition awaiting-author merge-conflict t-computability merge conflict
26908 robin-carlier feat(CategoryTheory/Monoidal/DayConvolution): alternative ext principle for unitors merge-conflict t-category-theory merge conflict
27150 robin-carlier feat(CategoryTheory/Monoidal/DayConvolution): constructors for braided and symmetric structure on day convolutions monoidal categories merge-conflict t-category-theory merge conflict
26462 PSchwahn feat(LinearAlgebra/Projection): add results about inverse of `Submodule.prodEquivOfIsCompl` awaiting-author t-algebra new-contributor awaiting author
27119 robin-carlier feat(CategoryTheory/Monoidal/DayConvolution): constructors for closed monoidal day convolution monoidal structures merge-conflict t-category-theory merge conflict
28623 gilesgshaw feat(Logic/Basic): minor additions and simplification of proofs merge-conflict t-logic new-contributor merge conflict
28804 grunweg feat: a few more tactic linters blocked-by-other-PR merge-conflict t-meta blocked on another PR
13036 joelriou feat(CategoryTheory/Sites): under certain conditions, cover preserving functors preserve 1-hypercovers WIP merge-conflict t-category-theory opened from a branch in the main mathlib repo (not a fork)
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 opened from a branch in the main mathlib repo (not a fork)
25778 thefundamentaltheor3m feat: Monotonicity of `setIntegral` for nonnegative functions awaiting-author t-measure-probability new-contributor awaiting author
22517 j-loreaux feat: `ℕ+` powers in semigroups WIP merge-conflict large-import ⚠️ opened from a branch in the main mathlib repo (not a fork)
27933 grunweg chore(OrdNode): format code example in code blocks merge-conflict t-data merge conflict
29615 eric-wieser chore: add a computable shortcut for `AddCommMonoid ℂ` easy t-analysis bench-after-CI opened from a branch in the main mathlib repo (not a fork)
28802 grunweg feat: a tactic linter for continuity/measurability which can be `fun_prop` merge-conflict t-meta awaiting-CI large-import does not pass CI
25069 erdOne feat(EllipticCurve): rational points of singular nodal cubics awaiting-author merge-conflict t-algebraic-geometry opened from a branch in the main mathlib repo (not a fork)
25070 erdOne feat(EllipticCurve): rational points on singular cuspidal cubics awaiting-author merge-conflict t-algebraic-geometry opened from a branch in the main mathlib repo (not a fork)
26670 yu-yama feat(GroupExtension/Abelian): define `conjClassesEquivH1` awaiting-author merge-conflict t-algebra merge conflict
26154 ADedecker refactor: add refactored APIs for algebraic filter bases merge-conflict t-topology merge conflict
27024 grunweg feat: Gram-Schmidt orthonormalisation for sections of a vector bundle awaiting-author merge-conflict t-differential-geometry merge conflict
28580 kmill refactor: simplify implementation of `filter_upwards` merge-conflict t-meta t-order opened from a branch in the main mathlib repo (not a fork)
29010 grunweg chore: more tests for field_simp features and edge cases failing CI
27937 madvorak feat(Logic/Basic): `congr_heq₂` awaiting-author t-logic awaiting author
7125 eric-wieser feat: additive monoid structure via biproducts WIP merge-conflict awaiting-CI t-category-theory opened from a branch in the main mathlib repo (not a fork)
27950 alreadydone feat(MonoidAlgebra): criteria for `single` to be a unit, irreducible or prime WIP merge-conflict t-algebra labelled WIP
28067 grunweg Docstring enumerations blocked-by-other-PR merge-conflict blocked on another PR
28908 joelriou feat(CategoryTheory): Pullback functors on `Over` categories in `Type` have right adjoints awaiting-author merge-conflict t-category-theory failing CI
25480 ocfnash feat: define a concrete model of the `𝔤₂` root system WIP merge-conflict t-algebra large-import opened from a branch in the main mathlib repo (not a fork)
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
27829 dupuisf feat: modify `cfc_tac` to use `grind` WIP merge-conflict ⚠️ labelled WIP
21950 erdOne feat(NumberTheory/Padics): the completion of `ℚ` at a finite place is `ℚ_[p]` merge-conflict t-number-theory opened from a branch in the main mathlib repo (not a fork)
26178 ppls-nd-prs feat(CategoryTheory/Limits): Fubini for products awaiting-author merge-conflict t-category-theory new-contributor merge conflict
27214 robin-carlier feat(CategoryTheory/Limits/Shapes/Pullback/Categorical): Categorical pullback squares merge-conflict t-category-theory merge conflict
27391 robin-carlier feat(CategoryTheory/Limits/Shapes/Pullback/Categorical): pseudofunctoriality structure of categorical pullback squares blocked-by-other-PR merge-conflict t-category-theory blocked on another PR
27432 robin-carlier feat(CategoryTheory/Limits/Shapes/Pullback/Categorical): pseudofunctoriality of categorical pulback squares blocked-by-other-PR merge-conflict t-category-theory blocked on another PR
27481 robin-carlier feat(CategoryTheory/Limits/Shapes/Pullback/Categorical): adjunctions and equivalences of categorical pullback squares blocked-by-other-PR merge-conflict t-category-theory large-import blocked on another PR
27686 robin-carlier feat(CategoryTheory/Limits/Shapes/Pullback/Categorical/Square): more API for `CatPullbackSquare` blocked-by-other-PR merge-conflict t-category-theory large-import blocked on another PR
27687 robin-carlier feat(CategoryTheory/Limits/Shapes/Pullback/Categorical): squares equivalent to a `CatPullbackSquare` blocked-by-other-PR merge-conflict t-category-theory large-import blocked on another PR
27688 robin-carlier feat(CategoryTheory/Limits/Shapes/Pullback/Categorical): coherence statement for `CatPullbackSquare.inverse` blocked-by-other-PR merge-conflict t-category-theory large-import blocked on another PR
27689 robin-carlier feat(CategoryTheory/Limits/Shapes/Pullback/Categorical): horizontal pasting calculus for `CatPullbackSquare` blocked-by-other-PR merge-conflict t-category-theory large-import blocked on another PR
27690 robin-carlier feat(CategoryTheory/Limits/Shapes/Pullback/Categorical): vertical pasting calculus for `CatPullbackSquare` blocked-by-other-PR merge-conflict t-category-theory large-import blocked on another PR
27740 robin-carlier feat(CategoryTheory/Limits/Shapes/Pullback/Categorical): pasting calculus for `CategoricalPullback` blocked-by-other-PR merge-conflict t-category-theory large-import blocked on another PR
26330 Timeroot feat: "Junk value" test file awaiting-author t-data awaiting author
28452 plp127 feat: Define `ZMod.fintype` without cases awaiting-author t-data awaiting author
26466 robin-carlier feat(AlgebraicTopology/SimplexCategory/Augmented): the canonical monoid object in the augmented simplex category merge-conflict t-category-theory t-algebraic-topology merge conflict
28074 grunweg Isbilinearmap WIP merge-conflict labelled WIP
26579 robin-carlier feat(CategoryTheory/Limits/Pullbacks/Categorical/CatCospanTransform): equivalences of categorical cospans blocked-by-other-PR merge-conflict t-category-theory large-import blocked on another PR
26578 robin-carlier feat(CategoryTheory/Limits/Pullbacks/Categorical/CatCospanTransform): adjunctions of categorical cospans merge-conflict t-category-theory large-import merge conflict
27634 agjftucker fix(Analysis/Calculus/Implicit): consistently rename {`map`, `fun`, `function`} to `fun` blocked-by-other-PR merge-conflict t-analysis blocked on another PR
28245 robin-carlier feat(CategoryTheory/Bicategory/NaturalTransformation/Icon): strict associativity and unitality of icon composition WIP blocked-by-other-PR merge-conflict awaiting-CI t-category-theory large-import blocked on another PR
30079 dagurtomas feat(CategoryTheory): IsSheafFor as a multiequalizer condition WIP t-category-theory labelled WIP
29012 grunweg chore: reduce `Topology` imports in `Data` merge-conflict file-removed failing CI
26601 yuma-mizuno feat(CategoryTheory): make `Functor.comp` irreducible WIP merge-conflict t-category-theory labelled WIP
23621 astrainfinita chore: deprecate `LinearOrderedComm{Monoid, Group}WithZero` merge-conflict t-algebra t-order opened from a branch in the main mathlib repo (not a fork)
28630 Antidite feat(Archive/Imo): right isosceles configuration in the complex plane awaiting-author new-contributor IMO awaiting author
30192 erdOne feat(RingTheory): valuative topology = adic topology for discrete rank 1 valuations WIP merge-conflict t-topology t-ring-theory labelled WIP
26886 pechersky feat(NumberTheory/Padics/ValuativeRel): ValuativeRel ℚ_[p] WIP blocked-by-other-PR merge-conflict t-number-theory t-analysis t-algebra blocked on another PR
27314 pechersky feat(TopologyValued): `Valued` based on a range topology blocked-by-other-PR merge-conflict t-topology blocked on another PR
30135 erdOne feat(RingTheory): `ValuativeRel` on subrings awaiting-author t-ring-theory awaiting author
28328 pechersky chore(Topology/Valued): golf using local finite order of WithZeroTopology blocked-by-other-PR merge-conflict t-number-theory t-topology t-algebra large-import blocked on another PR
16773 arulandu feat(Probability/Distributions): formalize Beta distribution awaiting-author merge-conflict t-measure-probability new-contributor opened from a branch in the main mathlib repo (not a fork)
26284 plp127 feat: faster implementation of `Nat.primeFactorsList` + `@[csimp]` lemma awaiting-author t-data awaiting author
27990 kckennylau feat(Counterexamples): a nontrivial valuation with discrete topology merge-conflict t-ring-theory merge conflict
28243 robin-carlier chore(CategoryTheory/Bicategory): move some `eqToHom` lemmas awaiting-author merge-conflict t-category-theory merge conflict
21853 smmercuri feat: the adele ring of a number field is locally compact WIP merge-conflict t-number-theory large-import opened from a branch in the main mathlib repo (not a fork)
26913 Paul-Lez feat(NumberTheory/{*}): add a few lemmas about number field and cyclotomic extensions WIP merge-conflict awaiting-CI t-number-theory t-algebra labelled WIP
27302 tristan-f-r feat(Fintype/Quotient): finLiftOn₂ awaiting-author t-data awaiting author
28925 grunweg chore: remove `linear_combination'` tactic merge-conflict awaiting-zulip file-removed awaiting a zulip discussion
29432 lecopivo feat: `data_synth` tactic to prove `HasFDerivAt 𝕜 f ?f' x` and similar WIP t-meta labelled WIP
29855 eric-wieser chore(Data/Finset/Sort): lemmas about `0 : Fin _` and `Fin.last _` delegated easy t-order t-data opened from a branch in the main mathlib repo (not a fork)
19616 adamtopaz fix: fix the definition of the absolute Galois group of a field awaiting-author merge-conflict t-number-theory t-algebra opened from a branch in the main mathlib repo (not a fork)
28826 alreadydone feat(CategoryTheory): Additive and Linear when Hom types are only monoids WIP merge-conflict awaiting-CI t-category-theory labelled WIP
30460 janithamalith feat(Nat): add lemma nat_card_orbit_mul_card_stabilizer_eq_card_group awaiting-author new-contributor t-group-theory awaiting author
30209 Ruben-VandeVelde feat: some TwoSidedIdeal.span lemmas awaiting-author FLT t-ring-theory awaiting author
25225 xcloudyunx feat(Combinatorics/SimpleGraph): Eulerian walk in connected graph contains all vertices awaiting-author t-combinatorics new-contributor opened from a branch in the main mathlib repo (not a fork)
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 opened from a branch in the main mathlib repo (not a fork)
27683 dupuisf feat: grind tags for set operations merge-conflict t-data failing CI
30828 DeVilhena-Paulo feat: implementation of `Finmap.merge` new-contributor t-data failing CI
29355 girving feat(Trigonometric): Taylor series bounds for sin and cos merge-conflict t-analysis failing CI
28298 thorimur chore: dedent `to_additive` docstrings documentation awaiting-author merge-conflict merge conflict
28737 astrainfinita refactor: deprecate `MulEquivClass` awaiting-author merge-conflict t-algebra merge conflict
28676 sun123zxy feat(NumberTheory/ArithmeticFunction): wrap `Nat.totient` as an `ArithmeticFunction` awaiting-author merge-conflict t-number-theory new-contributor large-import merge conflict
30299 franv314 feat(Topology/Instances): Cantor set awaiting-author merge-conflict t-topology new-contributor file-removed merge conflict
30303 franv314 chore(Topology/Instances): add deprecated module blocked-by-other-PR merge-conflict new-contributor blocked on another PR
27976 smmercuri feat: `ramificationIdx` for `NumberField.InfinitePlace` WIP merge-conflict t-number-theory labelled WIP
26357 javra feat(CategoryTheory): linear categories as `ModuleCat R`-enriched categories awaiting-author merge-conflict t-category-theory large-import merge conflict
26085 grunweg feat: disjoint unions distribute with products of manifolds WIP please-adopt merge-conflict t-differential-geometry looking for help
27180 ADedecker feat: quotient of a monoid with zero by a multiplicative congruence delegated merge-conflict t-algebra merge conflict
30790 urkud chore: partially migrate from `ContinuousMap.continuous` merge-conflict failing CI
30408 kckennylau feat(RingTheory): more algebra instances for HomogeneousLocalization and linear constructors t-ring-theory failing CI
29871 zach1502 feat(Matrix/Transvection): Gauss pivot determinant identity and pivot preservation awaiting-author t-algebra new-contributor awaiting author
30109 scholzhannah feat: the subcomplexes of a (relative classical) CW complex form a completely distributive lattice awaiting-author t-topology awaiting author
25692 Whysoserioushah feat(RingTheory/MatrixAlgebra): add a more general version of `matrixEquivTensor` awaiting-author merge-conflict t-ring-theory opened from a branch in the main mathlib repo (not a fork)
25012 urkud refactor(*): migrate from `Matrix.toLin'` to `Matrix.mulVecLin` merge-conflict opened from a branch in the main mathlib repo (not a fork)
29638 yuma-mizuno feat(CategoryTheory): define descent data by presieves WIP merge-conflict t-category-theory labelled WIP
30158 nicolaviolette feat: combinatorics simplegraph basic awaiting-author t-combinatorics new-contributor awaiting author
27708 vihdzp feat: unions and intersections of ordinals are ordinals awaiting-author merge-conflict t-set-theory merge conflict
27516 gaetanserre feat: add rational approximation lemma for suprema in `unitInterval` awaiting-author t-topology awaiting author
28132 dupuisf feat: preliminary `grind` tags for `IsUnit` merge-conflict t-algebra merge conflict
25903 pfaffelh feat(MeasureTheory): finite unions of sets in a semi-ring (in terms of measure theory) form a ring blocked-by-other-PR merge-conflict t-measure-probability large-import blocked on another PR
29992 vlad902 feat(Order): finite (Max)Chains always contains a top/max element WIP merge-conflict t-order large-import labelled WIP
26901 5hv5hvnk feat: a simproc version of `compute_degree` awaiting-author merge-conflict t-meta awaiting-CI new-contributor does not pass CI
31020 grunweg feat: mfderiv of Sum.inl and Sum.inr WIP merge-conflict ⚠️ labelled WIP
25775 emilyriehl feat(AlgebraicTopology/SimplicialSet/NerveAdjunction): to Strict Segal 2 awaiting-author merge-conflict t-category-theory infinity-cosmos t-algebraic-topology ❌? infrastructure-related CI failing
14752 AntoineChambert-Loir fix(Topology/Algebra/Valued): repair definition of Valued WIP merge-conflict t-topology t-algebra opened from a branch in the main mathlib repo (not a fork)
26827 pechersky feat(Analysis/Normed/ValuativeRel): helper instance for NormedField merge-conflict t-number-theory t-analysis t-algebra merge conflict
30150 imbrem feat(CategoryTheory/Monoidal): to_additive for MonoidalCategory merge-conflict t-meta t-category-theory new-contributor awaiting-zulip large-import awaiting a zulip discussion
25765 JovanGerb feat(gcongr): lemma for rewriting inside divisibility delegated t-data delegated
30824 grunweg wip: another smoothness lemma for local frames WIP merge-conflict t-differential-geometry labelled WIP
31593 Ruben-VandeVelde feat: some lemmas about MonoidAlgebra awaiting-author merge-conflict t-algebra merge conflict
31596 grunweg chore: remove extraneous uses of push_neg WIP merge-conflict labelled WIP
26885 pechersky feat(Topology/ValuativeRel): ValuativeTopology 𝒪[K] t-number-theory t-topology t-algebra failing CI
15651 TpmKranz feat(Computability/NFA): operations for Thompson's construction awaiting-author merge-conflict new-contributor t-computability awaiting-zulip opened from a branch in the main mathlib repo (not a fork)
12032 mcdoll feat: delta distribution as a limit WIP t-analysis opened from a branch in the main mathlib repo (not a fork)
9693 madvorak feat: Linear programming in the standard form WIP merge-conflict RFC t-algebra opened from a branch in the main mathlib repo (not a fork)
27392 Paul-Lez feat(Tactic/SimpUtils): add simproc finding commands awaiting-author merge-conflict t-meta large-import file-removed failing CI*
15649 TpmKranz feat(Computability): introduce Generalised NFA as bridge to Regular Expression awaiting-author merge-conflict new-contributor t-computability awaiting-zulip opened from a branch in the main mathlib repo (not a fork)
5745 alexjbest feat: a tactic to consume type annotations, and make constructor nicer awaiting-author merge-conflict t-meta opened from a branch in the main mathlib repo (not a fork)
5863 eric-wieser feat: add elaborators for concrete matrices help-wanted blocked-by-other-PR merge-conflict t-meta opened from a branch in the main mathlib repo (not a fork)
5919 MithicSpirit feat: implement orthogonality for AffineSubspace help-wanted WIP merge-conflict t-analysis new-contributor opened from a branch in the main mathlib repo (not a fork)
7386 madvorak feat: Define linear programs WIP merge-conflict RFC t-algebra opened from a branch in the main mathlib repo (not a fork)
9352 chenyili0818 feat: arithmetic lemmas for `gradient` awaiting-author merge-conflict t-analysis opened from a branch in the main mathlib repo (not a fork)
9795 sinhp feat: the type `Fib` of fibre of a function at a point awaiting-author merge-conflict t-category-theory opened from a branch in the main mathlib repo (not a fork)
10660 eric-wieser feat(LinearAlgebra/CliffordAlgebra): construction from a basis WIP awaiting-author merge-conflict t-algebra opened from a branch in the main mathlib repo (not a fork)
10977 grunweg feat: germs of smooth functions awaiting-author merge-conflict t-differential-geometry t-topology t-analysis opened from a branch in the main mathlib repo (not a fork)
10998 hmonroe feat(Logic): Arithmetization of partial recursive functions (toward Gödel's first incompleteness theorem) awaiting-author merge-conflict t-logic opened from a branch in the main mathlib repo (not a fork)
11890 adomani feat: the terminal refine linter awaiting-author merge-conflict t-linter opened from a branch in the main mathlib repo (not a fork)
12006 adomani feat: the `suffa` tactic awaiting-author merge-conflict t-meta opened from a branch in the main mathlib repo (not a fork)
13442 dignissimus feat: mabel tactic for multiplicative abelian groups help-wanted awaiting-author modifies-tactic-syntax merge-conflict t-meta new-contributor opened from a branch in the main mathlib repo (not a fork)
14237 js2357 feat: Define the localization of a fractional ideal at a prime ideal awaiting-author merge-conflict t-algebra new-contributor opened from a branch in the main mathlib repo (not a fork)
14345 digama0 feat: the Dialectica category is monoidal closed awaiting-author merge-conflict t-category-theory opened from a branch in the main mathlib repo (not a fork)
14727 jjaassoonn feat(RingTheory/Flat/CategoryTheory): a flat module has vanishing higher Tor groups awaiting-author merge-conflict t-ring-theory opened from a branch in the main mathlib repo (not a fork)
14733 jjaassoonn feat(RingTheory/Flat/CategoryTheory): a module is flat iff tensoring preserves finite limits awaiting-author merge-conflict t-ring-theory opened from a branch in the main mathlib repo (not a fork)
15055 sinhp feat: the category of pointed objects of a concrete category awaiting-author merge-conflict t-category-theory opened from a branch in the main mathlib repo (not a fork)
15224 AnthonyBordg feat(CategoryTheory/Sites): covering families and their associated Grothendieck topology awaiting-author merge-conflict t-category-theory new-contributor opened from a branch in the main mathlib repo (not a fork)
16303 grunweg feat(CI): check for badly formatted titles or missing/contradictory labels awaiting-author merge-conflict CI opened from a branch in the main mathlib repo (not a fork)
18236 joelriou feat(Algebra/Category/ModuleCat/Presheaf): the endofunctor of presheaves of modules induced by an oplax natural transformation WIP awaiting-author merge-conflict awaiting-CI t-category-theory t-algebra opened from a branch in the main mathlib repo (not a fork)
18749 GabinKolly feat(ModelTheory): preparatory work for the existence of Fraïsse limits awaiting-author merge-conflict t-logic opened from a branch in the main mathlib repo (not a fork)
18876 GabinKolly feat(ModelTheory/Fraisse): add proof that Fraïssé limits exist blocked-by-other-PR merge-conflict t-logic opened from a branch in the main mathlib repo (not a fork)
19323 madvorak feat: Function to Sum decomposition WIP merge-conflict t-data opened from a branch in the main mathlib repo (not a fork)
19378 adamtopaz feat: Explanation widgets awaiting-author merge-conflict t-meta opened from a branch in the main mathlib repo (not a fork)
19456 AntoineChambert-Loir feat(Data/Finsupp/MonomialOrder/DegRevLex): homogeneous reverse lexicographic order WIP merge-conflict t-algebraic-geometry t-order t-data opened from a branch in the main mathlib repo (not a fork)
20051 Timeroot feat: `Clone` and some instances blocked-by-other-PR awaiting-author merge-conflict t-algebra opened from a branch in the main mathlib repo (not a fork)
20466 MohanadAhmed feat: Sherman Morrison formula for rank 1 update of the matrix inverse awaiting-author merge-conflict t-data opened from a branch in the main mathlib repo (not a fork)
20648 anthonyde feat: formalize regular expression -> εNFA merge-conflict new-contributor t-computability awaiting-zulip opened from a branch in the main mathlib repo (not a fork)
20649 GabinKolly feat(ModelTheory/Graph): prove characterization of the fraisse limit of finite simple graphs WIP merge-conflict t-combinatorics t-logic large-import opened from a branch in the main mathlib repo (not a fork)
20652 jjaassoonn feat: categorical description of center of a ring awaiting-author merge-conflict t-category-theory t-algebra opened from a branch in the main mathlib repo (not a fork)
20924 tomaz1502 feat(Computability/QueryComplexity): Oracle-based computation merge-conflict t-computability opened from a branch in the main mathlib repo (not a fork)
20956 tomaz1502 feat(Computability/QueryComplexity/Sort.lean): Formalization of upper bound of queries for merge sort blocked-by-other-PR merge-conflict t-computability opened from a branch in the main mathlib repo (not a fork)
21270 GabinKolly feat(ModelTheory/Bundled): first-order embeddings and equivalences from equalities awaiting-author merge-conflict t-logic large-import opened from a branch in the main mathlib repo (not a fork)
21277 GabinKolly feat(ModelTheory/PartialEquiv): Define the mapping of a self-partialEquiv through an embedding blocked-by-other-PR merge-conflict t-logic opened from a branch in the main mathlib repo (not a fork)
21616 peabrainiac feat(Topology): concatenating countably many paths awaiting-author merge-conflict t-topology opened from a branch in the main mathlib repo (not a fork)
21624 sinhp feat(CategoryTheory): The (closed) monoidal structure on the product category of families of (closed) monoidal categories awaiting-author merge-conflict t-category-theory opened from a branch in the main mathlib repo (not a fork)
21829 Whysoserioushah feat(LinearAlgebra/TensorProduct/HomTensor): Add TensorProduct of Hom-modules awaiting-author merge-conflict t-algebra opened from a branch in the main mathlib repo (not a fork)
21903 yhtq feat: add from/toList between `FreeSemigroup` and `List` with relative theorems merge-conflict awaiting-CI t-algebra new-contributor large-import opened from a branch in the main mathlib repo (not a fork)
22159 shetzl feat: add definition of pushdown automata awaiting-author merge-conflict new-contributor t-computability opened from a branch in the main mathlib repo (not a fork)
22231 pechersky feat(Algebra/Valued): `AdicExpansion` initial defns awaiting-author merge-conflict t-topology t-algebra opened from a branch in the main mathlib repo (not a fork)
22232 pechersky feat(Algebra/Valued): `AdicExpansion.apprUpto` blocked-by-other-PR merge-conflict t-topology opened from a branch in the main mathlib repo (not a fork)
22233 pechersky feat(Algebra/Valued): `AdicExpansion.evalAt` blocked-by-other-PR merge-conflict t-topology opened from a branch in the main mathlib repo (not a fork)
22302 658060 feat: add `CategoryTheory.Topos.Power` awaiting-author merge-conflict t-category-theory new-contributor opened from a branch in the main mathlib repo (not a fork)
22314 shetzl feat: add leftmost derivations for context-free grammars awaiting-author merge-conflict new-contributor t-computability opened from a branch in the main mathlib repo (not a fork)
22662 plp127 feat: Localization.Away.lift (computably) merge-conflict t-algebra opened from a branch in the main mathlib repo (not a fork)
22790 mhk119 feat: Extend `taylor_mean_remainder_lagrange` to `x < x_0` awaiting-author merge-conflict t-analysis new-contributor opened from a branch in the main mathlib repo (not a fork)
22861 eric-wieser feat: add the trace of a bilinear form awaiting-author merge-conflict t-algebra opened from a branch in the main mathlib repo (not a fork)
22919 plp127 feat(Data/Fintype/Pi): Make `Fintype` instance for `RelHom`s computable awaiting-author merge-conflict t-data opened from a branch in the main mathlib repo (not a fork)
22954 eric-wieser feat(RingTheory/Congruence/Hom): copy from GroupTheory merge-conflict t-ring-theory opened from a branch in the main mathlib repo (not a fork)
23285 AntoineChambert-Loir refactor: directed systems in terms of functors WIP merge-conflict t-category-theory t-algebra large-import opened from a branch in the main mathlib repo (not a fork)
23460 Timeroot feat: Definition of `Clone` blocked-by-other-PR merge-conflict t-algebra opened from a branch in the main mathlib repo (not a fork)
23503 apnelson1 feat(Topology/Instances/ENat): ENat and tsum WIP merge-conflict t-topology large-import opened from a branch in the main mathlib repo (not a fork)
23585 plp127 feat: `Filter.atMax` and `Filter.atMin` WIP merge-conflict t-order opened from a branch in the main mathlib repo (not a fork)
23758 erdOne feat(Topology/Algebra): linearly topologized iff non-archimedean awaiting-author merge-conflict t-topology t-algebra large-import opened from a branch in the main mathlib repo (not a fork)
23835 chrisflav feat(Topology): cardinality of connected components is bounded by cardinality of fiber awaiting-author merge-conflict t-topology opened from a branch in the main mathlib repo (not a fork)
24333 xcloudyunx feat(Combinatorics/SimpleGraph): cycle graph implementation for generic vertex types awaiting-author merge-conflict t-combinatorics new-contributor opened from a branch in the main mathlib repo (not a fork)
24540 robertmaxton42 feat(Quiv): add the empty, vertex, point, interval, and walking quivers awaiting-author merge-conflict t-category-theory opened from a branch in the main mathlib repo (not a fork)
24850 pechersky feat(Topology/UniformSpace/Ultra): uniform spaces induced by pseudometrics are ultra if system is ultra merge-conflict t-topology opened from a branch in the main mathlib repo (not a fork)
25324 eric-wieser feat: more functorial results about DFinsupp awaiting-author merge-conflict t-algebra t-data opened from a branch in the main mathlib repo (not a fork)
25585 Paul-Lez feat(Tactic/Linters/DeprecatedSimpLemma): lint for deprecated simp lemmas awaiting-author merge-conflict t-linter opened from a branch in the main mathlib repo (not a fork)
25739 literandltx feat(NumberTheory/LegendreSymbol): Add sqrt‐of‐residue theorems for p=4k+3 and p=8k+5 awaiting-author merge-conflict t-number-theory new-contributor merge conflict
25974 scholzhannah feat(Topology/Compactness/CompactlyCoherentSpace): compact coherentification (k-ification) merge-conflict t-topology large-import merge conflict
26051 Komyyy feat(Mathlib/GroupTheory/SpecificGroups/Alternating): A_n is simple iff n = 3 or 5 ≤ n WIP merge-conflict large-import t-group-theory labelled WIP
26165 oliver-butterley feat(MeasureTheory.VectorMeasure): add lemma which shows that variation of a `ℝ≥0∞` VectorMeasure is equal to itself blocked-by-other-PR merge-conflict t-measure-probability new-contributor blocked on another PR
26300 igorkhavkine feat(Analysis/Calculus/FDeriv): continuous differentiability from continuous partial derivatives on an open domain in a product space WIP awaiting-author merge-conflict t-analysis new-contributor labelled WIP
26329 Timeroot feat: Definition of `Clone` notations and typeclasses awaiting-author merge-conflict awaiting-CI t-algebra does not pass CI
26398 ChrisHughes24 feat(ModelTheory): definable functions please-adopt merge-conflict t-logic looking for help
26399 ChrisHughes24 refactor(ModelTheory): tidy up proof of Ax-Grothendieck with definable functions blocked-by-other-PR merge-conflict t-logic blocked on another PR
26432 AntoineChambert-Loir feat(Data.Nat.LogFueled): fueled version of `clog` merge-conflict t-data failing CI
26594 metakunt feat(Algebra/Polynomial/ZMod): Add Polynomial.equiv_of_nat_of_polynomial_zmod awaiting-author merge-conflict t-algebra new-contributor merge conflict
26644 kckennylau feat(SetTheory/ZFC): Define the language of sets and state the ZFC axioms awaiting-author merge-conflict t-set-theory merge conflict
26648 eric-wieser chore(TensorProduct): remove more `suppress_compilation`s blocked-by-core-PR merge-conflict t-algebra opened from a branch in the main mathlib repo (not a fork)
26757 fweth feat(CategoryTheory/Topos): define elementary topos awaiting-author merge-conflict t-category-theory new-contributor failing CI
26914 quangvdao feat(Data/PFunctor/Univariate): more definitions for univariate `PFunctor` merge-conflict t-data merge conflict
26920 yuma-mizuno feat(Tactic.CategoryTheory): add associator inserting tactic WIP merge-conflict t-meta t-category-theory labelled WIP
26990 joelriou feat(CategoryTheory/Abelian): Noetherian objects form a Serre class WIP merge-conflict t-category-theory labelled WIP
27098 Paul-Lez feat(Algebra/Category/ModuleCat/Sheaf/VectorBundle): define vector bundles awaiting-author merge-conflict t-algebra merge conflict
27155 Pjotr5 feat: Shearer's bound on the independence number of triangle free graphs awaiting-author merge-conflict t-combinatorics new-contributor failing CI
27163 pechersky feat(Topology/ValuativeRel): of and to basis of compatible valuations awaiting-author merge-conflict t-number-theory t-topology t-algebra merge conflict
27187 Komyyy feat: `NONote` represents ordinals < ε₀ WIP merge-conflict t-set-theory labelled WIP
27215 kckennylau feat(AlgebraicGeometry): Define the Zariski site on `CommRingCatᵒᵖ` awaiting-author merge-conflict t-algebraic-geometry merge conflict
27309 kckennylau feat(CategoryTheory): a presheaf on `CostructuredArrow F d` can be extended to a presheaf on `C` WIP merge-conflict t-category-theory labelled WIP
27321 kckennylau feat(CategoryTheory): Colimit can be computed fiberwise merge-conflict awaiting-CI t-category-theory does not pass CI
27417 PierreQuinton feat: add `SigmaCompleteLattice` awaiting-author merge-conflict t-order merge conflict
27534 PierreQuinton feat: a typeclass for `sSup`/`sInf` to be lawful merge-conflict t-order merge conflict
27753 YunkaiZhang233 feat(CategoryTheory): implemented proofs for factorisation categories being equivalent to iterated comma categories in two ways awaiting-author merge-conflict t-category-theory new-contributor merge conflict
27824 ChrisHughes24 feat(Calculus): exists_gt_of_deriv_pos and variants awaiting-author merge-conflict t-analysis merge conflict
27850 fyqing feat: 0-dimensional manifolds are discrete and countable awaiting-author merge-conflict t-differential-geometry new-contributor merge conflict
27973 smmercuri feat: the ring of integers of a `ℤₘ₀`-valued field is compact whenever it is a DVR and the residue field is finite awaiting-author merge-conflict t-algebra large-import merge conflict
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 opened from a branch in the main mathlib repo (not a fork)
28325 pechersky feat(WithZeroTopology): `locallyCompactSpace_iff_locallyFiniteOrder_units` merge-conflict t-topology t-order large-import failing CI
28349 kckennylau feat(Meta): add notation for naming stacked polynomials awaiting-author merge-conflict t-meta merge conflict
28530 nonisomorphiclinearmap feat(Combinatorics/SimplicialComplex/Topology): add standard simplices and geometric realisation (colimit + functoriality) blocked-by-other-PR merge-conflict t-combinatorics new-contributor blocked on another PR
28868 yury-harmonic feat(Positive): add `OfNat` instance merge-conflict t-algebra large-import failing CI
28871 JaafarTanoukhi feat(Combinatorics/Digraph): Tournaments merge-conflict t-combinatorics new-contributor merge conflict
29055 vihdzp feat: `Ordinal.toENat` awaiting-author merge-conflict t-set-theory merge conflict
29108 JonBannon feat(MeasureTheory): add `LInfty.lean` with `Mul` and `const` related results. awaiting-author merge-conflict t-measure-probability merge conflict
29500 vihdzp feat: `WellFoundedLT (LowerSet α)` awaiting-author merge-conflict t-order merge conflict
29526 llllvvuu feat: `Multiset.map f` identifies `f` up to permutation merge-conflict t-data merge conflict
29675 yury-harmonic feat(Wolstenholme): new file help-wanted awaiting-author merge-conflict t-data looking for help
29720 javra feat(CategoryTheory): `TransportEnrichment` and `ForgetEnrichment` as 2-functors WIP merge-conflict t-category-theory labelled WIP
29827 js2357 feat: define two (trivial) ContinuousMulEquivs merge-conflict t-topology FLT large-import failing CI
29947 JaafarTanoukhi feat(Combinatorics/Digraph): Maps merge-conflict t-combinatorics new-contributor merge conflict
30004 luigi-massacci feat(MeasureTheory/Integral/TestAgainst): integrating BCFs against a finite measure or an L1Loc map as CLMs awaiting-author merge-conflict t-analysis t-measure-probability merge conflict
30042 JovanGerb feat(push): `@[push]` attributes for `∈` in `Set`, `Finset` and `Multiset` awaiting-author merge-conflict t-meta merge conflict
30451 kckennylau feat(HomogeneousIdeal): generalize to homogeneous submodule merge-conflict t-ring-theory failing CI
30933 joelriou feat(CategoryTheory): the linearization of a category awaiting-author merge-conflict t-category-theory merge conflict
31194 grunweg feat: add `#check'` command and tactic, which only show explicit arguments awaiting-author merge-conflict t-meta merge conflict
31351 grunweg feat: manifolds with smooth boundary WIP merge-conflict t-differential-geometry labelled WIP
31356 adomani feat: add inspect-like functions merge-conflict t-meta merge conflict
31604 maksym-radziwill feat: analyticity of dslope awaiting-author merge-conflict t-analysis merge conflict
31738 robertmaxton42 feat: quivers can be represented as functors from the walking quiver awaiting-author merge-conflict t-category-theory failing CI
21915 YaelDillies feat: simproc for `Int.divisorsAntidiag` WIP t-meta opened from a branch in the main mathlib repo (not a fork)
19475 YaelDillies feat: group markings WIP blocked-by-other-PR t-algebra opened from a branch in the main mathlib repo (not a fork)
15443 YaelDillies feat: Marcinkiewicz-Zygmund inequality WIP t-analysis opened from a branch in the main mathlib repo (not a fork)
31590 SuccessMoses chore: tag `commutatorElement_def` with `simp` awaiting-author t-algebra new-contributor failing CI
31587 JovanGerb Lean pr testing 11156 WIP merge-conflict opened from a branch in the main mathlib repo (not a fork)*
25802 dagurtomas feat(AlgebraicTopology): anodyne morphisms of simplicial sets WIP t-topology labelled WIP
6268 eric-wieser fix: fixups to #3838 WIP merge-conflict opened from a branch in the main mathlib repo (not a fork)
6859 MohanadAhmed feat: TryLean4Bundle: Windows Bundle Creator help-wanted WIP CI opened from a branch in the main mathlib repo (not a fork)
6993 jjaassoonn feat: lemmas about `AddMonoidAlgebra.{divOf, modOf}` merge-conflict t-algebra opened from a branch in the main mathlib repo (not a fork)
7427 MohanadAhmed feat: eigenvalues sorted in ascending/descending order WIP merge-conflict ⚠️ opened from a branch in the main mathlib repo (not a fork)
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 opened from a branch in the main mathlib repo (not a fork)
9564 AntoineChambert-Loir chore: weaken commutativity assumptions for AdjoinRoot.lift and AdjoinRoot.liftHom WIP merge-conflict t-algebra ??? opened from a branch in the main mathlib repo (not a fork)
10026 madvorak feat: linear programming according to Antoine Chambert-Loir's book WIP merge-conflict RFC t-algebra opened from a branch in the main mathlib repo (not a fork)
10159 madvorak feat: linear programming according to Antoine Chambert-Loir's book — affine version WIP merge-conflict RFC t-algebra opened from a branch in the main mathlib repo (not a fork)
10349 Shamrock-Frost refactor(CategoryTheory/MorphismProperty): some clean-ups merge-conflict t-category-theory ??? opened from a branch in the main mathlib repo (not a fork)
11021 jstoobysmith feat(AlgebraicTopology): add join of augmented SSets WIP merge-conflict new-contributor t-algebraic-topology opened from a branch in the main mathlib repo (not a fork)
11800 JADekker feat: KappaLindelöf spaces please-adopt merge-conflict t-topology awaiting-zulip ??? opened from a branch in the main mathlib repo (not a fork)
12087 JADekker feat: complete API for K-Lindelöf spaces blocked-by-other-PR please-adopt merge-conflict t-topology ??? opened from a branch in the main mathlib repo (not a fork)
12251 ScottCarnahan refactor(RingTheory/HahnSeries): several generalizations WIP merge-conflict t-algebra t-order opened from a branch in the main mathlib repo (not a fork)
12394 JADekker feat: define pre-tight and tight measures awaiting-author please-adopt merge-conflict t-measure-probability opened from a branch in the main mathlib repo (not a fork)
12452 JADekker feat(Cocardinal): add some more api awaiting-CI t-topology ??? opened from a branch in the main mathlib repo (not a fork)
14426 adomani feat: `#min_imps` command (development branch) WIP merge-conflict ??? ⚠️ opened from a branch in the main mathlib repo (not a fork)
14686 smorel394 feat(AlgebraicGeometry/Grassmannian): define the Grassmannian scheme WIP please-adopt merge-conflict t-algebraic-geometry workshop-AIM-AG-2024 ??? opened from a branch in the main mathlib repo (not a fork)
17071 ScottCarnahan feat(LinearAlgebra/RootSystem): separation, base, cartanMatrix WIP merge-conflict t-algebra ??? opened from a branch in the main mathlib repo (not a fork)
17471 joelriou feat(Algebra/ModuleCat/Differentials/Sheaf): the sheaf of relative differentials WIP blocked-by-other-PR merge-conflict t-category-theory t-algebraic-geometry large-import opened from a branch in the main mathlib repo (not a fork)
18626 hannahfechtner feat: define Artin braid groups awaiting-author merge-conflict t-algebra new-contributor opened from a branch in the main mathlib repo (not a fork)
18784 erdOne feat(AlgebraicGeometry): use `addMorphismPropertyInstances` blocked-by-other-PR merge-conflict t-algebraic-geometry opened from a branch in the main mathlib repo (not a fork)
19062 hannahfechtner feat(Algebra/PresentedMonoid/Basic): facts about rel awaiting-author t-algebra opened from a branch in the main mathlib repo (not a fork)
19607 madvorak feat: block matrices are totally unimodular WIP blocked-by-other-PR merge-conflict ⚠️ opened from a branch in the main mathlib repo (not a fork)
20029 FrederickPu feat(Tactic/simps): allow for Config attributes to be set directly WIP merge-conflict t-meta new-contributor opened from a branch in the main mathlib repo (not a fork)
21269 658060 feat(CategoryTheory/Topos): basic definitions and results in topos theory WIP awaiting-author merge-conflict t-category-theory new-contributor opened from a branch in the main mathlib repo (not a fork)
22805 ScottCarnahan feat(FieldTheory/Finite): fixed points of Frobenius automorphism WIP merge-conflict t-algebra opened from a branch in the main mathlib repo (not a fork)
23772 SEU-Prime feat: Amice equivalence WIP t-number-theory ??? labelled WIP
23990 robertmaxton42 feat(Types.Colimits): Quot is functorial and colimitEquivQuot is natural awaiting-author merge-conflict t-category-theory new-contributor opened from a branch in the main mathlib repo (not a fork)
24533 robertmaxton42 feat(ULift): conjugation by ULift.up/down, misc cast/heq lemmas awaiting-author t-data opened from a branch in the main mathlib repo (not a fork)
24690 ScottCarnahan feat(Data.Prod): reverse lexicographic order WIP merge-conflict t-order opened from a branch in the main mathlib repo (not a fork)
24692 ScottCarnahan feat(RingTheory/HahnSeries/Basic): isomorphism of Hahn series induced by order isomorphism WIP merge-conflict t-order opened from a branch in the main mathlib repo (not a fork)
25034 ScottCarnahan feat(Algebra/Module/Equiv/Basic): Restriction of scalars from a semilinear equivalence to a linear equivalence WIP t-algebra opened from a branch in the main mathlib repo (not a fork)
25831 ScottCarnahan feat(RingTheory/HahnSeries): Powers of a binomial WIP merge-conflict t-ring-theory labelled WIP
26455 ScottCarnahan feat(LinearAlgebra/RootSystem): API for CartanMatrix WIP merge-conflict t-algebra labelled WIP
26804 kckennylau feat(SetTheory): ZFSet is a model of ZFC WIP merge-conflict t-set-theory labelled WIP
26881 emo916math feat(Analysis/Calculus/Deriv/Star): a formula for `deriv (conj ∘ f ∘ conj)` awaiting-author t-analysis new-contributor awaiting author
26890 robin-carlier feat(CategoryTheory/Monoidal/DayConvolution): more API for `DayFunctor` merge-conflict t-category-theory merge conflict
26310 kckennylau feat: binary forms awaiting-author merge-conflict t-algebra merge conflict
26283 kckennylau feat: resultant of polynomials WIP merge-conflict t-algebra labelled WIP
27991 sinianluoye feat(Rat): add Rat.den_eq_of_add_den_eq_one and its dependent lemmas awaiting-author new-contributor t-data failing CI
28215 5hv5hvnk feat: strong and Weak connectivity for Digraphs WIP awaiting-author merge-conflict t-combinatorics new-contributor labelled WIP
28970 Whysoserioushah feat(Algebra/Algebra/ReducedNorm): defines reduced norm and trace awaiting-author merge-conflict t-algebra merge conflict
29212 Whysoserioushah feat(Algebra/CrossProductAlgebra/Defs): define Cross Product Algebra awaiting-author merge-conflict t-algebra merge conflict
29514 grunweg feat(CI): use more strict mode WIP merge-conflict CI labelled WIP
29574 JarodAlper feat: regular local rings are domains merge-conflict new-contributor t-ring-theory failing CI
28718 imbrem feat: class for chosen finite coproducts blocked-by-other-PR awaiting-author merge-conflict t-category-theory new-contributor blocked on another PR
30352 kckennylau feat(RingTheory): Homogeneous localization of tensor product WIP blocked-by-other-PR merge-conflict ⚠️ blocked on another PR
30366 sinhp feat(CategoryTheory): The Preliminaries for Locally Cartesian Closed Categories awaiting-author merge-conflict t-category-theory merge conflict
26765 KiringYJ feat(MeasureTheory/PiSystem): add π-λ theorem and SetLike instance awaiting-author t-measure-probability new-contributor awaiting author
29409 Julian feat(Mathlib/Analysis): deriv_eq_self and deriv_exp_iff awaiting-author t-analysis awaiting author
31513 FLDutchmann feat(Tactic): `polynomial` tactic blocked-by-other-PR merge-conflict t-meta blocked on another PR
27306 xyzw12345 feat: `lie_ring` tactic and `LieReduce` command t-meta failing CI
29434 ntapiam feat(NonAssoc/LieAdmissible): prove every ring/algebra is LieAdmissible t-algebra new-contributor failing CI
27694 grunweg feat: Gram-Schmidt orthonormalisation preserves continuity of sections blocked-by-other-PR merge-conflict t-differential-geometry blocked on another PR
27025 grunweg feat: Gram-Schmidt procedure on smooth vector bundles yields smooth sections blocked-by-other-PR merge-conflict t-differential-geometry blocked on another PR
30637 strihanje01 feat(Combinatorics/SetFamily/Lindstrom): Lindstrom's theorem for subfamilies with equal unions t-combinatorics new-contributor failing CI
31949 ADedecker chore: prefer `Pi.single i 1 j` over `fun j => if i = j then 1 else 0` awaiting-author t-algebra awaiting author
25902 pfaffelh feat: The finite product of semi-rings (in terms of measure theory) is a semi-ring. awaiting-author merge-conflict t-measure-probability large-import brownian merge conflict
31571 erdOne feat(RingTheory): existence of local algebra with given residue field awaiting-author t-ring-theory awaiting author
29517 pechersky feat(RingTheory/Torsion): torsion = union of roots of unity awaiting-author merge-conflict t-algebra failing CI
31176 mcdoll feat(Analysis): Taylor's theorem with the integral remainder awaiting-author t-analysis awaiting author
28933 artie2000 chore(Data): correct definition for `single_apply` WIP merge-conflict labelled WIP
24627 pechersky feat(Topology/Algebra/Valued): `IsLinearTopology 𝒪[K] K` and `𝒪[K] 𝒪[K]` awaiting-author merge-conflict t-topology opened from a branch in the main mathlib repo (not a fork)
27756 grunweg feat: `Weak(Pseudo)EMetricSpace`, generalises `(Pseudo)EMetricSpace` WIP merge-conflict t-topology carleson labelled WIP
24016 plp127 feat: fine uniformity merge-conflict t-topology opened from a branch in the main mathlib repo (not a fork)
30995 kckennylau feat(RingTheory): replace ofLinearEquiv with limit awaiting-author t-ring-theory awaiting author
32094 grunweg feat(runLinter): allow only running certain linters CI t-linter failing CI
32095 grunweg chore: fix some explicitVarOfIff linter errors WIP please-adopt merge-conflict looking for help
31796 dobronx1325 feat(Data/Real/EReal): add mul_lt_mul_of_pos_left theorem new-contributor t-data failing CI
27258 JovanGerb feat: Imo2020 q6 awaiting-author IMO awaiting author
26138 xroblot Development branch (2) WIP merge-conflict labelled WIP
31729 thorimur chore: log on theorem type signature in unused instances in type linters blocked-by-other-PR merge-conflict large-import blocked on another PR
32157 peabrainiac feat(Analysis/Calculus): Hadamard's lemma blocked-by-other-PR t-analysis blocked on another PR
26436 AntoineChambert-Loir feat(Mathlib/Data/Nat/Prime/Defs): fuel Nat.minFac awaiting-author merge-conflict t-data failing CI
24514 b-mehta chore(Int/GCD): use fuel in xgcd awaiting-author merge-conflict t-data opened from a branch in the main mathlib repo (not a fork)
32169 saodimao20 feat: add convolution_comp_add_right awaiting-author t-analysis new-contributor awaiting author
28244 robin-carlier feat(CategoryTheory/Bicategory/NaturalTransformation): Icons WIP blocked-by-other-PR merge-conflict awaiting-CI t-category-theory large-import blocked on another PR
29933 smmercuri chore: fix `def` naming isses in `Normed/Field/WithAbs.lean` WIP merge-conflict labelled WIP
31350 grunweg feat: (unoriented) bordism groups WIP blocked-by-other-PR merge-conflict t-differential-geometry blocked on another PR
26389 jjdishere feat(RingTheory): Perfectoid Field WIP t-topology t-analysis t-algebra labelled WIP
32285 awainverse chore(ModelTheory/Bundled): Replace CategoryTheory.Bundled awaiting-author t-logic awaiting author
31663 xroblot feat(Algebra): more instances about `min`, `max`, `iSup` and `iInf` of sub-algebras WIP t-algebra labelled WIP
31950 callesonne feat(CategoryTheory/Product/Basic): make `Hom` into a 1-field structure WIP merge-conflict t-category-theory labelled WIP
27579 RemyDegenne feat: risk of an estimator, DeGroot statistical information, total variation distance WIP t-measure-probability large-import labelled WIP
29315 kbuzzard chore: raise priority of `IsTopologicalSemiring.toIsModuleTopology` awaiting-author t-topology failing CI
31730 thorimur feat(Meta): declaration manipulation meta API: allow logging on type signature of theorems t-meta failing CI
31242 plp127 feat: express filter as supremum of principal filter and free filter awaiting-author merge-conflict t-order merge conflict
32474 mattrobball perf(Module.LinearMap.Defs): deprioritize projections to parents for SemilinearMapClass t-algebra failing CI
31898 ntapiam feat(LinearAlgebra/TensorAlgebra): implement HopfAlgebra for TensorAlgebra awaiting-author new-contributor t-ring-theory failing CI
31597 grunweg chore(AtLocation): allow throwing a warning when no progress is being made awaiting-author merge-conflict t-meta merge conflict
30525 515801431 feat(Mathlib/Combinatorics/Enumerative/Polya): Add Polya Counting awaiting-author merge-conflict t-combinatorics new-contributor merge conflict
31113 515801431 feat(Mathlib/Combinatorics/Enumerative/Polya.lean): Add additional theorem in `Polya.lean` blocked-by-other-PR merge-conflict t-combinatorics new-contributor blocked on another PR
24441 MrSumato feat(Data/List): add Lyndon-Schutzenberger theorem on list commutativity awaiting-author merge-conflict new-contributor t-data opened from a branch in the main mathlib repo (not a fork)
28057 plp127 feat(SuccOrder): simp lemma to refold `Order.succ` and `Order.pred` awaiting-author merge-conflict t-order merge conflict
31901 callesonne feat(Bicategory/Subbicategory): add full subbicategories using `ObjectProperty` awaiting-author t-category-theory awaiting author
32473 mattrobball chore(Kaehler.JacobiZariski): remove egregious local instance hack awaiting-author t-ring-theory opened from a branch in the main mathlib repo (not a fork)
18551 joelriou feat(AlgebraicGeometry): the algebraic De Rham complex WIP blocked-by-other-PR merge-conflict t-algebraic-geometry t-algebra opened from a branch in the main mathlib repo (not a fork)
29744 espottesmith feat(Combinatorics): define directed hypergraphs t-combinatorics new-contributor failing CI
31147 daefigueroa feat(Dynamics): point transitive monoid actions and transitive points awaiting-author t-dynamics new-contributor awaiting author
30119 Ruben-VandeVelde feat: WithTop/Bot.mapD awaiting-author merge-conflict t-order merge conflict
28613 espottesmith feat(Combinatorics): define undirected hypergraphs merge-conflict t-combinatorics new-contributor failing CI
23040 grunweg feat: define immersions and smooth embeddings in infinite dimensions WIP blocked-by-other-PR merge-conflict t-differential-geometry opened from a branch in the main mathlib repo (not a fork)
30668 astrainfinita feat: `QuotType` RFC awaiting-zulip t-data awaiting a zulip discussion
30847 joelriou feat(CategoryTheory/Presentable): the representation theorem WIP blocked-by-other-PR merge-conflict t-category-theory blocked on another PR
30817 joelriou feat(CategoryTheory): `κ`-continuous presheaves WIP blocked-by-other-PR t-category-theory blocked on another PR
6633 adomani feat(..Polynomial..): `MvPolynomial`s have no zero divisors awaiting-author merge-conflict t-algebra opened from a branch in the main mathlib repo (not a fork)
28865 grunweg feat: a map is smooth iff its post-composition with an immersion is WIP blocked-by-other-PR merge-conflict t-differential-geometry blocked on another PR
31987 saodimao20 feat: add monotonicity and relation lemmas for mgf and cgf awaiting-author t-measure-probability new-contributor awaiting author
32211 ADedecker feat: inclusion from `ContDiffMapSupportedIn` to `TestFunction` is a topological embedding blocked-by-other-PR merge-conflict t-analysis blocked on another PR
32602 adamtopaz feat: Refactor graph WIP ⚠️ labelled WIP
26912 pechersky chore(Algebra/Ring/Subring): simp tag `Subring.smul_def` merge-conflict t-algebra merge conflict
32737 j-loreaux refactor: rename `MulAction` to `MonoidAction` merge-conflict failing CI
30240 luigi-massacci feat(Analysis/Distribution/ContDiffMapSupportedIn): Add a wrapper for fderiv on D_K^n blocked-by-other-PR t-analysis blocked on another PR
29274 Jlh18 feat(CategoryTheory): HasLimits instance on Grpd blocked-by-other-PR merge-conflict t-category-theory file-removed blocked on another PR
29283 Jlh18 feat(CategoryTheory): define forgetful-core adjunction between Cat and Grpd awaiting-author merge-conflict t-category-theory file-removed merge conflict
21447 erdOne feat(AlgebraicGeometry): the split algebraic torus awaiting-author merge-conflict t-algebraic-geometry opened from a branch in the main mathlib repo (not a fork)
25963 artie2000 refactor(Algebra): uniform API for substructures WIP merge-conflict t-algebra labelled WIP
32938 0xTerencePrime feat(Order/LocallyFinite): prove DenselyOrdered and LocallyFiniteOrder are incompatible awaiting-author t-order new-contributor 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 merge-conflict easy t-ring-theory merge conflict
21495 alreadydone experiment: reducible HasQuotient.quotient' WIP merge-conflict bench-after-CI opened from a branch in the main mathlib repo (not a fork)
32698 farruhx feat(List): add aesop / simp annotations to selected lemmas for improved automation awaiting-author new-contributor t-data awaiting author
27817 zhuyizheng feat: add IMO2025P1 awaiting-author merge-conflict new-contributor IMO merge conflict
26923 oliver-butterley feat(Dynamics/BirkhoffSum): add the pointwise ergodic theorem (Birkhoff's) awaiting-author t-dynamics new-contributor failing CI
33218 Blackfeather007 feat(Algebra): Define the associated graded ring to filtered ring blocked-by-other-PR new-contributor t-ring-theory blocked on another PR
33219 Blackfeather007 feat(Algebra): Define associated graded algebra blocked-by-other-PR new-contributor t-ring-theory blocked on another PR
33220 Blackfeather007 feat(Algebra): Define associated graded module blocked-by-other-PR new-contributor t-ring-theory blocked on another PR
33227 Blackfeather007 feat(Algebra): exact of associated graded exact blocked-by-other-PR new-contributor t-ring-theory blocked on another PR
33226 Blackfeather007 feat(Algebra): associated graded exact of exact and strict blocked-by-other-PR new-contributor t-ring-theory blocked on another PR
33225 Blackfeather007 feat(Algebra): filtered module hom blocked-by-other-PR new-contributor t-ring-theory blocked on another PR
33224 Blackfeather007 feat(Algebra): define filtered alghom blocked-by-other-PR new-contributor t-ring-theory blocked on another PR
33223 unknown unknown title ??? missing CI information
33222 Blackfeather007 feat(Algebra): define filtered add group hom blocked-by-other-PR new-contributor t-ring-theory blocked on another PR
33134 faenuccio feat(Normed/Module/WeakDual): add Goldstine lemma WIP t-analysis labelled WIP
33178 gw90 feat(Analysis/CStarAlgebra/Spectrum): Adding lemmas that the CStarAlgebra norm equals the square root of the spectral radius of star a * a awaiting-author t-analysis new-contributor awaiting author
33138 gasparattila chore(MeasureTheory/Measure/Stieltjes): remove `backward.privateInPublic` awaiting-author t-measure-probability tech debt awaiting author
33307 grunweg Orientable manifolds updated WIP t-differential-geometry labelled WIP
33313 SnirBroshi feat(Combinatorics/SimpleGraph/EdgeColoring): create a basic edge-coloring API blocked-by-other-PR t-combinatorics large-import blocked on another PR
5934 eric-wieser feat: port Data.Rat.MetaDefs help-wanted mathlib-port merge-conflict t-meta opened from a branch in the main mathlib repo (not a fork)
4960 eric-wieser chore: use `open scoped` merge-conflict awaiting-CI opened from a branch in the main mathlib repo (not a fork)
6042 MohanadAhmed feat(LinearAlgebra/Matrix/SVD): Singular Value Decomposition of R or C Matrices WIP please-adopt merge-conflict t-algebra opened from a branch in the main mathlib repo (not a fork)
4127 kmill refactor: create HasAdj class, define Digraph, and generalize some SimpleGraph API awaiting-author merge-conflict t-combinatorics opened from a branch in the main mathlib repo (not a fork)
27752 plp127 feat(Order): `NoBotOrder α` implies `NoMinOrder α` under `IsDirected α (· ≥ ·)` awaiting-author merge-conflict t-order failing CI
32921 faenuccio refactor Submodule.map WIP awaiting-author merge-conflict t-algebra labelled WIP
32889 artie2000 feat(Algebra): forgetful lemmas for `map` and `comap` on substructures blocked-by-other-PR awaiting-author merge-conflict t-algebra blocked on another PR
32960 dleijnse feat(FieldTheory): adjoin pth roots awaiting-author t-algebra new-contributor awaiting author
33163 Aaron1011 feat: prove subgroup of (M -> Z) is finitely generated awaiting-author new-contributor t-ring-theory awaiting author
25481 kbuzzard chore: refactor Algebra.TensorProduct.rightAlgebra t-algebra opened from a branch in the main mathlib repo (not a fork)
28972 themathqueen feat(LinearAlgebra/Matrix): star-algebra automorphisms on matrices are unitarily inner awaiting-author t-analysis t-algebra awaiting author
14444 digama0 fix(GeneralizeProofs): unreachable! bug awaiting-author merge-conflict t-meta opened from a branch in the main mathlib repo (not a fork)
25138 chrisflav chore(RingTheory/Ideal): make `RingHom.ker` take a `RingHom` instead of `RingHomClass` awaiting-author merge-conflict t-algebra opened from a branch in the main mathlib repo (not a fork)
31018 joelriou feat(CategoryTheory): the κ-accessible category of κ-directed posets WIP t-category-theory labelled WIP
33386 joelriou feat(AlgebraicTopology/SimplicialSet): decidable instances WIP RFC t-algebraic-topology labelled WIP
24665 Komyyy feat(Mathlib/Topology/Metrizable/Uniformity): every uniform space is generated by a family of pseudometrics WIP merge-conflict t-topology opened from a branch in the main mathlib repo (not a fork)
33381 urkud feat: add a version of the Schwarz lemma blocked-by-other-PR merge-conflict t-analysis blocked on another PR
33448 astrainfinita refactor: deprecate `ContinuousLinearMapClass` awaiting-author t-topology t-algebra awaiting author
33462 eric-wieser feat: teach `fun_prop` about `ContinousMultilinearMap.compContinuousLinearMap` t-analysis opened from a branch in the main mathlib repo (not a fork)
32725 joelriou feat(CategoryTheory): presheaves of types which preserve a limit awaiting-author t-category-theory awaiting author
32840 joelriou chore(CategoryTheory): remove the old Ext API WIP merge-conflict t-category-theory large-import file-removed labelled WIP
33133 0xTerencePrime feat(Algebra/Group/Center): add Decidable (IsMulCentral a) instance awaiting-author t-algebra new-contributor awaiting author
33191 sinhp feat(CategoryTheory): Locally cartesian closed structure on presheaf categories WIP blocked-by-other-PR merge-conflict t-category-theory blocked on another PR
28153 kckennylau feat(Simproc): Simproc for explicit diagonal matrices awaiting-author merge-conflict t-meta merge conflict
25500 eric-wieser feat: delaborators for metadata awaiting-author delegated merge-conflict t-meta large-import opened from a branch in the main mathlib repo (not a fork)
28191 kckennylau feat(Logic): tag Injective, Surjective, and Bijective with fun_prop awaiting-author merge-conflict t-meta merge conflict
30432 kckennylau feat(AlgebraicGeometry): define the non-vanishing locus of a set in Proj awaiting-author t-algebraic-geometry awaiting author
27262 Timeroot feat(Tactic/Bound): bound? for proof scripts awaiting-author t-meta failing CI
32389 LLaurance feat(Analysis): Trigonometric identities awaiting-author t-analysis awaiting author
33502 MrQubo fix(Tactic/ProxyType): Pass params explicitly in proxy_equiv% implementation WIP t-meta new-contributor labelled WIP
22657 Xmask19 feat: a graph is maximally acyclic iff it is a tree merge-conflict t-combinatorics new-contributor opened from a branch in the main mathlib repo (not a fork)
26368 Whysoserioushah feat(RingTheory/TwoSidedIdeal/SpanAsSum): span of set as finsum awaiting-author merge-conflict t-ring-theory merge conflict
28013 astrainfinita feat: Lindemann-Weierstrass Theorem awaiting-author merge-conflict t-analysis t-algebra failing CI
21344 kbuzzard chore: attempt to avoid diamond in OreLocalization please-adopt t-algebra opened from a branch in the main mathlib repo (not a fork)
33112 alreadydone feat(GroupAction): `(M →[M] M) ≃* Mᵐᵒᵖ` awaiting-author t-algebra t-group-theory awaiting author
31187 loefflerd feat(NumberTheory/LSeries): Define the L-series of a modular form WIP t-number-theory labelled WIP
30375 sinhp feat(CategoryTheory): Basics of Locally Cartesian Closed Categories WIP blocked-by-other-PR t-category-theory blocked on another PR
32991 artie2000 chore(Algebra/Algebra): remove `Algebra.cast` coercion merge-conflict t-algebra failing CI
27972 smmercuri refactor: make `Valuation.Completion` a `def` and refactor more of `AdicValuation.lean` WIP merge-conflict t-number-theory t-algebra labelled WIP
17176 arulandu feat: integrals and integrability with .re awaiting-author please-adopt merge-conflict t-measure-probability new-contributor opened from a branch in the main mathlib repo (not a fork)
33010 xgenereux feat: localizations of primes in Dedekind domains are valuation subrings WIP blocked-by-other-PR awaiting-author large-import t-ring-theory blocked on another PR
33454 astrainfinita feat: lemmas about `IsometryClass` awaiting-author t-topology t-analysis awaiting author
13740 YaelDillies feat: more robust ae notation awaiting-author t-meta t-measure-probability opened from a branch in the main mathlib repo (not a fork)
32165 yuanyi-350 feat(Real/Trigonometric): Add `sum_cos_arith_progression` and prepare for Dirichlet kernel awaiting-author merge-conflict t-analysis merge conflict
33368 urkud feat: define `Complex.UnitDisc.shift` merge-conflict t-analysis awaiting-zulip awaiting a zulip discussion
33450 astrainfinita refactor: deprecate `LinearIsometryClass` blocked-by-other-PR merge-conflict t-topology t-analysis t-algebra blocked on another PR
33702 JovanGerb doc(Algebra/Quotient): update `HasQuotient.Quotient` doc-string delegated t-algebra delegated
33434 astrainfinita chore: redefine `Finsupp.indicator` using `Finsupp.onFinset` t-data failing CI
33554 themathqueen chore(Analysis/Normed/Module/Normalize): allow for `RCLike` instead of just the reals awaiting-author merge-conflict t-analysis merge conflict
33561 kbuzzard chore: cont -> continuous_toFun merge-conflict merge conflict
27507 grunweg wip(commandStart): check the indentation of declaration keywords also WIP merge-conflict t-linter labelled WIP
26088 grunweg chore(Linter/DirectoryDependency): move forbidden directories into a JSON file please-adopt merge-conflict t-linter looking for help
33330 michael-novak-math feat: add arc-length reparametrization of parametrized curves merge-conflict t-analysis new-contributor merge conflict
24010 grunweg feat(Counterexamples): a non-negative function, not a.e. zero, with vanishing lowe… WIP blocked-by-other-PR please-adopt merge-conflict t-measure-probability opened from a branch in the main mathlib repo (not a fork)
28700 Timeroot feat(ModelTheory): Set.Definable is transitive merge-conflict t-logic large-import merge conflict
30608 grunweg feat: another lemma about derivatives of parametric integrals awaiting-author merge-conflict t-analysis merge conflict
30610 grunweg feat: yet another lemma about differentiability of parametric integrals blocked-by-other-PR merge-conflict t-analysis blocked on another PR
33299 kingiler feat: Add decidable membership for Interval awaiting-author t-order new-contributor awaiting author
32190 vihdzp chore(Algebra/Order/Ring/Archimedean): generalize theorems to `OrderHomClass` + `RingHomClass` t-algebra failing CI
30142 shalliso feat(Topology/Baire): define IsNonMeagre merge-conflict t-topology new-contributor failing CI
32210 ADedecker feat: iteratedFDeriv as a linear map on test functions awaiting-author merge-conflict t-analysis merge conflict
32401 ADedecker feat: monotonicity of D^n(U) in n and in U as CLMs delegated merge-conflict t-analysis merge conflict
32410 callesonne feat(Bicategory/FunctorCategory/Pseudo): Add evaluation pseudofunctor WIP blocked-by-other-PR merge-conflict t-category-theory blocked on another PR
30562 dwrensha fix(Data/Fintype/Perm): make the main logic of Equiv.instFintype irreducible awaiting-author t-data failing CI
33669 eric-wieser chore(Data/Nat/Digits): refactor to use List.rightpad merge-conflict large-import opened from a branch in the main mathlib repo (not a fork)
25905 mans0954 feat(RingTheory/Polynomial/SmallDegreeVieta): polynomial versions of results in Algebra.QuadraticDiscriminant please-adopt merge-conflict t-ring-theory looking for help
25907 mans0954 feat: low order roots of unity please-adopt t-algebra looking for help
26339 mans0954 feat(Analysis/Normed/Module/WeakDual): Banach Dieudonné Lemma WIP please-adopt merge-conflict t-analysis large-import looking for help
26340 mans0954 feat(Algebra/Module/NestAlgebra): Nest algebras please-adopt merge-conflict t-algebra looking for help
26341 mans0954 feat(LinearAlgebra/QuadraticForm/Basis): Free Tensor product of Quadratic Maps WIP please-adopt merge-conflict t-algebra large-import looking for help
33808 seewoo5 feat(Manifold/MFDeriv): add fun_prop to `MDifferentiable` awaiting-author t-differential-geometry awaiting author
26344 mans0954 feat(Analysis/NormedSpace/MStructure): The component projections on WithLp 1 (α × β) are L-projections WIP please-adopt merge-conflict t-analysis file-removed looking for help
26347 mans0954 feat(Data/Finset/RangeDistance): abs_sub_lt_of_mem_finset_range please-adopt merge-conflict t-data looking for help
26349 mans0954 feat(Analysis/SpecialFunctions/Trigonometric/Basic): sin and cos of multiples of π / 3 help-wanted please-adopt t-analysis looking for help
26348 mans0954 feat(Analysis/LocallyConvex/Prime): the prime map WIP please-adopt merge-conflict t-analysis looking for help
26983 mans0954 feat(Order/LatticeElements): distributive, standard and neutral elements of a lattice WIP please-adopt merge-conflict t-order looking for help
29980 mans0954 refactor(RingTheory/Polynomial/Resultant/Quadratic): Re-implement QuadraticDiscriminant for R[X] please-adopt merge-conflict looking for help
29387 mans0954 feat(Analysis/LocallyConvex/WeakSpace): toWeakSpace_closedAbsConvexHull_eq blocked-by-other-PR please-adopt merge-conflict t-analysis blocked on another PR
29378 mans0954 feat(Analysis/LocallyConvex/AbsConvex): Balanced and AbsConvex sets under linear maps please-adopt merge-conflict t-analysis looking for help
29856 mans0954 feat(Analysis/Normed/Ring/Basic): Add NonUnitalNonAssocSeminormedRing and NonUnitalNonAssocNormedRing please-adopt t-analysis looking for help
12934 grunweg chore: replace more uses of > or ≥ by < or ≤ help-wanted awaiting-author merge-conflict ??? opened from a branch in the main mathlib repo (not a fork)
28070 grunweg style: improve indentation of multi-linear enumerations in doc-strings merge-conflict failing CI
29077 grunweg feat(Manifold/Instances/Icc): golf smoothness proof using immersions blocked-by-other-PR merge-conflict t-differential-geometry blocked on another PR
32880 0xTerencePrime feat(Analysis/Asymptotics): define subpolynomial growth awaiting-author t-analysis new-contributor failing CI
33435 astrainfinita feat: algebra automorphisms of monoid algebras merge-conflict t-algebra merge conflict
33814 seewoo5 feat(Manifold/MFDeriv): add `MDifferentiable.pow` with FunProp blocked-by-other-PR merge-conflict t-differential-geometry blocked on another PR
33948 anivegesana feat(Analysis/Normed/Algebra): matrix exponential of nilpotent matrix t-analysis new-contributor failing CI
33270 vihdzp chore(Order/Disjoint): use `to_dual` awaiting-author t-order failing CI
26291 RemyDegenne feat(Probability): Cameron-Martin theorem WIP blocked-by-other-PR merge-conflict t-measure-probability blocked on another PR*
30030 JonBannon feat(MeasureTheory): add `MemLp.Const` class and instances to unify `p = ∞` and `μ.IsFiniteMeasure` cases awaiting-author merge-conflict t-measure-probability failing CI
33807 adamtopaz feat: TypeCat refactor WIP merge-conflict t-category-theory labelled WIP
29610 llllvvuu feat(LinearAlgebra): define LinearMap.Eigenbasis awaiting-author merge-conflict t-algebra merge conflict
31610 rudynicolop feat(Computability/NFA): Kleene star closure for Regular Languages via NFA awaiting-author awaiting-CI new-contributor t-computability does not pass CI
27493 themathqueen feat(RingTheory/Coalgebra): define Frobenius algebra blocked-by-other-PR awaiting-author t-ring-theory blocked on another PR
33992 tb65536 feat(NumberTheory/NumberField/ExistsRamified): Galois group is generated by inertia subgroups blocked-by-other-PR t-number-theory t-algebra blocked on another PR
33542 yuanyi-350 feat(integral): Error Estimation for the Rectangle Rule in Numerical Integration awaiting-author merge-conflict t-analysis failing CI
30582 RemyDegenne feat: extension of a function to the closure of a submodule WIP merge-conflict t-topology labelled WIP
33535 erdOne feat(Algebra/Category): `Under.pushout` preserves finite limits for flat homomorphisms awaiting-author t-algebra awaiting author
28631 faenuccio feat(Data\Nat\ModEq.lean): add grind attribute to ModEq WIP merge-conflict t-data labelled WIP
30391 rudynicolop feat(Data/List): list splitting definitions and lemmas awaiting-author new-contributor t-data awaiting author
27704 vihdzp feat: link `Minimal` and `IsLeast` together awaiting-author merge-conflict t-order failing CI
33126 CoolRmal feat: function composition preserves boundedness merge-conflict t-order merge conflict
20719 gio256 feat(AlgebraicTopology): delaborators for truncated simplicial notations merge-conflict t-meta infinity-cosmos t-algebraic-topology opened from a branch in the main mathlib repo (not a fork)
31348 PatrickMassot chore: fix a docstring typo documentation awaiting-author t-analysis opened from a branch in the main mathlib repo (not a fork)
10991 thorimur feat: `tfae` block tactic WIP modifies-tactic-syntax merge-conflict t-meta opened from a branch in the main mathlib repo (not a fork)
34005 MSpill feat: inverse function theorem for manifolds (concrete version) awaiting-author t-differential-geometry new-contributor failing CI
29282 Jlh18 feat(CategoryTheory): HasColimits instance on Grpd blocked-by-other-PR merge-conflict t-category-theory new-contributor blocked on another PR
29587 uniwuni feat(GroupTheory/Finiteness): define finitely generated semigroups merge-conflict t-group-theory merge conflict
29774 Raph-DG feat(AlgebraicGeometry): Order of vanishing of elements of the function field of locally noetherian, integral schemes blocked-by-other-PR merge-conflict t-algebraic-geometry file-removed blocked on another PR
28796 grunweg feat: immersions are smooth awaiting-author merge-conflict t-differential-geometry merge conflict
28905 grunweg feat: immersions are locally embeddings blocked-by-other-PR merge-conflict t-differential-geometry blocked on another PR
30504 grunweg feat: add custom elaborators for immersions blocked-by-other-PR merge-conflict t-meta t-differential-geometry blocked on another PR
32039 HugLycan feat(Tactic/Positivity): handle non-zeroness in non-orders WIP merge-conflict t-meta new-contributor labelled WIP
32745 LTolDe feat(Topology/Algebra): add MulActionConst.lean awaiting-author t-topology new-contributor awaiting author
34131 Ruben-VandeVelde fix: update create_deprecated_modules.lean WIP please-adopt CI opened from a branch in the main mathlib repo (not a fork)
34134 Paul-Lez feat(Mathlib/Analysis/PDE/Quasilinear/Characteristics): the method of characteristics for first order quasilinear PDEs WIP t-analysis labelled WIP
33478 anishrajeev feat(ModelTheory): define a subset of the topology over complete types blocked-by-other-PR merge-conflict t-logic new-contributor blocked on another PR
32546 anishrajeev feat(ModelTheory): Prove compactness of the type space merge-conflict t-logic new-contributor merge conflict
30853 JovanGerb feat(LinearAlgebra/AffineSpace/Simplex): `CoeFun` instance for `Simplex` awaiting-author merge-conflict t-euclidean-geometry merge conflict
34195 eric-wieser feat: continuous bundled actions t-topology t-algebra large-import opened from a branch in the main mathlib repo (not a fork)
33495 vihdzp chore(RingTheory/HahnSeries/Basic): redefine `order` using `unbotD` blocked-by-other-PR merge-conflict t-ring-theory blocked on another PR
31180 CoolRmal feat(Analysis): a closed convex set is the intersection of countably many half-spaces in a separable Banach space awaiting-author merge-conflict t-analysis new-contributor failing CI
33504 ldct feat: Add lemmas for DihedralGroup.fintypeHelper awaiting-author t-group-theory awaiting author
34238 Ruben-VandeVelde feat: some lemmas about AlgHom 1 and * awaiting-author t-algebra awaiting author
31092 FlAmmmmING feat(Algebra/Group/ForwardDiff.lean): Add theorem `sum_shift_eq_fwdDiff_iter`. delegated t-algebra new-contributor delegated
32828 Hagb feat(Algebra/Order/Group/Defs): add `IsOrderedAddMonoid.toIsOrderedCancelAddMonoid'` t-algebra awaiting-zulip awaiting a zulip discussion
34141 gululu996-ui feat(Combinatorics/SimpleGraph/Acyclic): finite trees have at least two degree-one vertices awaiting-author t-combinatorics new-contributor awaiting author
29014 ShreckYe feat(Data/List/Scan): some theorems that relate `scanl` with `foldl` merge-conflict t-data merge conflict
33689 BoltonBailey feat(Probability): PMF point mass function WIP blocked-by-other-PR t-measure-probability blocked on another PR
33680 BoltonBailey feat(Probability/ProbabilityMassFunction): add Total Variation distance blocked-by-other-PR t-measure-probability blocked on another PR
21476 grunweg feat(lint-style): enable running on downstream projects awaiting-author merge-conflict t-linter opened from a branch in the main mathlib repo (not a fork)
34129 idontgetoutmuch feat: define Ehresmann connections awaiting-author t-differential-geometry new-contributor awaiting author
33749 plp127 feat: `NNRat` is countable awaiting-author t-data large-import awaiting author
34371 grunweg feat: module instance on ContMDiffMap WIP t-differential-geometry labelled WIP
34396 dupuisf feat: notation for `Ring.inverse` t-algebra awaiting-zulip awaiting a zulip discussion
34219 or4nge19 feat(MeasureTheory/BorelSpace): measurability of annuli on (pseudo)(e)metric space blocked-by-other-PR t-measure-probability carleson blocked on another PR
33052 JovanGerb feat: replace `rw??` tactic with `#infoview_search` command delegated merge-conflict t-meta large-import file-removed failing CI
33209 JovanGerb feat(infoview_search): move to new frontend blocked-by-other-PR merge-conflict t-meta large-import file-removed blocked on another PR
33132 BoltonBailey feat(Computability): Single-tape TM complexity WIP t-computability labelled WIP
34155 zcyemi feat(Geometry/Euclidean/Triangle): add altitudeFoot lies strictly between endpoints for an obtuse angle awaiting-author t-euclidean-geometry failing CI
34186 faenuccio feat(GroupTheory/SpecificGroups/Cyclic): a quotient of a cyclic group is cyclic awaiting-author t-group-theory awaiting author
31836 hanwenzhu chore(MeasureTheory/IntervalIntegral): generalize fundamental theorem of calculus to `HasDerivWithinAt` instead of `HasDerivAt` awaiting-author merge-conflict t-analysis t-measure-probability merge conflict
12879 grunweg feat: port ge_or_gt linter from mathlib3 blocked-by-other-PR merge-conflict t-linter tech debt ??? opened from a branch in the main mathlib repo (not a fork)
34262 grunweg feat: add mfderiv_const_smul awaiting-author t-differential-geometry awaiting author
33110 dagurtomas feat(CategoryTheory): adjoint functor theorems for presentable categories WIP t-category-theory labelled WIP
34361 grunweg chore: rename comp' to fun_comp a few more times; use to_fun to autog… blocked-by-other-PR t-analysis blocked on another PR
8608 eric-wieser feat: multiplicativize `AddTorsor` WIP please-adopt merge-conflict t-algebra opened from a branch in the main mathlib repo (not a fork)
34506 kbuzzard perf(RingTheory/Extension/Generators): universe switch WIP t-ring-theory labelled WIP
33963 gasparattila feat(Topology/UniformSpace/Closeds): completeness of `(Nonempty)Compacts` t-topology awaiting review
34268 gasparattila feat(Topology/Sets): continuity of operations on `(Nonempty)Compacts` t-topology awaiting review
34270 gasparattila feat(Topology/UniformSpace/Closeds): `(Nonempty)Compacts.toCloseds` is a closed embedding t-topology awaiting review
34276 gasparattila feat(Topology/Sets): discreteness of `(Nonempty)Compacts` blocked-by-other-PR t-topology blocked on another PR
34273 gasparattila feat(Topology/Sets): finite sets are dense in `(Nonempty)Compacts` blocked-by-other-PR t-topology blocked on another PR
34278 gasparattila feat(Topology/Sets): connectedness of `NonemptyCompacts` blocked-by-other-PR t-topology blocked on another PR
34280 gasparattila feat(Topology/Sets): local connectedness of `(Nonempty)Compacts` blocked-by-other-PR t-topology blocked on another PR
34275 gasparattila feat(Topology/Sets): topological properties of `(Nonempty)Compacts.map` blocked-by-other-PR t-topology blocked on another PR
31377 CoolRmal feat: a series of smooth functions that converges (locally) uniformly is smooth awaiting-author merge-conflict t-topology new-contributor failing CI
34123 staroperator feat(Data/Set/Finite): finite distributivity for complete distributive lattices t-order awaiting review
26158 upobir feat(NumberTheory/Divisors): add int divisors awaiting-author t-number-theory awaiting author
33031 chiyunhsu feat(Combinatorics/Enumerative/Partition): add combinatorial proof of Euler's partition theorem t-combinatorics new-contributor awaiting-zulip awaiting a zulip discussion
27835 edegeltje feat(Tactic): ring modulo a given characteristic WIP awaiting-author merge-conflict t-meta large-import migrated-from-branch labelled WIP
33954 or4nge19 feat(CategoryTheory/Abelian): add Filtration API awaiting-author t-category-theory awaiting author
34092 staroperator feat(SetTheory/ZFC): properties of `ZFSet.omega` t-set-theory awaiting review
34279 grunweg chore: use `to_fun` more blocked-by-other-PR merge-conflict blocked on another PR
33817 FlAmmmmING fix(Combinatorics/Enumerative/Schroder.lean): Fix the definition and theorem of smallSchroder. t-combinatorics new-contributor large-import awaiting review
34227 stepan2698-cpu feat: If sum of densities is at least one, the sumset covers the naturals t-combinatorics new-contributor awaiting review
34130 FlAmmmmING feat(Combinatorics/SimpleGraph/Acyclic): Add new theorem `isTree_iff_uniqueShortest_path` awaiting-author t-combinatorics new-contributor awaiting author
34501 eric-wieser chore(Data/Fintype/Induction): add a workaround for a bug in `induction` awaiting-author t-meta opened from a branch in the main mathlib repo (not a fork)
32872 JovanGerb feat(Data/Real/Basic): don't expose the definition of `Real` merge-conflict t-data failing CI
33295 AntoineChambert-Loir feat(Algebra/Central/End): center of the group of automorphisms of a free module WIP merge-conflict t-algebra labelled WIP
26087 grunweg feat: a `SliceModel` typeclass for models with corners for embedded submanifolds t-differential-geometry failing CI
34028 floor-licker feat(SimpleGraph): add max-flow/min-cut weak duality t-combinatorics new-contributor awaiting review
16074 Rida-Hamadani feat: combinatorial maps and planar graphs merge-conflict t-combinatorics opened from a branch in the main mathlib repo (not a fork)
25841 mitchell-horner feat(Combinatorics/SimpleGraph): prove the Kővári–Sós–Turán theorem blocked-by-other-PR t-combinatorics blocked on another PR
34257 grunweg feat(Tactic/ToFun): allow configuring the name of the generated declaration awaiting-author merge-conflict t-meta merge conflict
32609 PrParadoxy feat(LinearAlgebra/PiTensorProduct): Relation between nested tensor products and tensor products indexed by dependent sums blocked-by-other-PR merge-conflict t-algebra new-contributor blocked on another PR
29000 JovanGerb feat(Tactic/Push): add basic tags and tests blocked-by-other-PR merge-conflict t-meta blocked on another PR
27053 tb65536 feat: Galois group of `x^n - x - 1` WIP t-algebra large-import labelled WIP
29792 robertmaxton42 feat(RelCWComplex): a (relative, concrete) CW complex is the colimit of its skeleta blocked-by-other-PR merge-conflict t-topology large-import blocked on another PR
24100 eric-wieser feat: restore some explicit binders from Lean 3 awaiting-author merge-conflict t-topology t-algebra tech debt opened from a branch in the main mathlib repo (not a fork)
33520 NoneMore feat(ModelTheory/ElementarySubstructures): add a variant of Tarski-Vaught test taking sets as input t-logic new-contributor awaiting review
34633 mitchell-horner feat(Combinatorics/SimpleGraph): define the Zarankiewicz function blocked-by-other-PR t-combinatorics blocked on another PR
34656 vihdzp refactor: review `exists_irreducible_of_degree_pos` theorems t-algebra awaiting-zulip t-ring-theory awaiting a zulip discussion
34675 YaelDillies feat: comultiplication as a bialgebra hom blocked-by-other-PR toric t-ring-theory blocked on another PR
30327 luigi-massacci feat(Analysis/Distribution/TestFunction): add characterizations of continuity for linear maps on test functions blocked-by-other-PR merge-conflict t-analysis blocked on another PR
30329 luigi-massacci feat(Analysis/Distribution/TestFunction): integrating against a measure as a continuous linear map on test functions blocked-by-other-PR merge-conflict t-analysis blocked on another PR*
29411 llllvvuu feat(LinearAlgebra/Matrix/Rank): rank factorization awaiting-author merge-conflict t-algebra merge conflict
30260 imbrem feat(CategoryTheory/Monoidal): added CocartesianMonoidalCategory blocked-by-other-PR merge-conflict t-category-theory new-contributor large-import blocked on another PR
30258 imbrem feat(CategoryTheory/Monoidal): to_additive for proofs using `monoidal` blocked-by-other-PR merge-conflict t-category-theory new-contributor large-import blocked on another PR
30927 callesonne feat(Bicategory/Yoneda): add the yoneda pseudofunctor t-category-theory failing CI
32608 PrParadoxy feat(LinearAlgebra/PiTensorProduct): API for PiTensorProducts indexed by sets t-algebra new-contributor awaiting-zulip awaiting a zulip discussion
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 t-topology large-import blocked on another PR
32983 JovanGerb feat: use `LE.le` for subset relation in `Set`, `Finset`, `PSet`, `ZFSet` merge-conflict t-data failing CI
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 t-analysis blocked on another PR
30255 luigi-massacci feat(Analysis/Distribution/ContDiffMapSupportedIn): specialize singleton seminorm family for D_K^n when n finite blocked-by-other-PR merge-conflict t-analysis blocked on another PR
32829 Hagb feat(Data/Finsupp/MonomialOrder): weaken `IsOrderedCancelAddMonoid` to `IsOrderedAddMonoid` blocked-by-other-PR t-order blocked on another PR
32742 LTolDe feat(MeasureTheory/Constructions/Polish/Basic): add class SuslinSpace t-measure-probability new-contributor awaiting-zulip awaiting a zulip discussion
33470 erdOne feat: generalize `Polynomial.freeMonic` awaiting-author t-algebra awaiting author
33109 felixpernegger feat(Data/Nat/Choose): Binomial inversion awaiting-author new-contributor t-data awaiting author
24000 YaelDillies feat: correspondence between affine group schemes and Hopf algebras blocked-by-other-PR t-algebraic-geometry FLT toric opened from a branch in the main mathlib repo (not a fork)
30920 callesonne feat(Category/Grpd): define the bicategory of groupoids merge-conflict t-category-theory large-import failing CI
30121 idontgetoutmuch feat(Mathlib/Geometry/Manifold): principal fiber bundle core awaiting-author t-differential-geometry new-contributor awaiting author
27918 kim-em chore: refactor WithBot/WithTop as structures WIP merge-conflict file-removed labelled WIP
29605 alreadydone experiment(Algebra): unbundle npow/zpow from Monoid/InvDivMonoid WIP merge-conflict awaiting-CI t-algebra labelled WIP
25474 adomani test for .lean/.md check WIP merge-conflict t-linter file-removed opened from a branch in the main mathlib repo (not a fork)
33991 grunweg test: pretty-printing of class abbrev WIP merge-conflict large-import file-removed opened from a branch in the main mathlib repo (not a fork)
34484 grunweg test: debugging mfderiv_smul erws WIP blocked-by-other-PR t-differential-geometry blocked on another PR
31110 bryangingechen ci: don't delete merged branches awaiting-author merge-conflict CI opened from a branch in the main mathlib repo (not a fork)
33707 jcommelin ci: add commit verification for transient and automated commits merge-conflict CI failing CI
31102 JOSHCLUNE feat: require LeanHammer merge-conflict t-meta new-contributor failing CI
33431 gululu996-ui feat(Combinatorics/SimpleGraph/Bipartite): characterize bipartite simple graphs by even cycles awaiting-author t-combinatorics new-contributor awaiting author
34007 martinwintermath feat(Algebra/Module/Submodule/Dual): dual operator for submodules awaiting-author t-algebra new-contributor awaiting author
33928 jsm28 feat(Combinatorics/Tiling/TileSet): indexed families of tiles t-combinatorics awaiting review
34473 JovanGerb feat: remove `Membership` instance for `SetLike` merge-conflict t-set-theory failing CI
34271 gasparattila feat(Topology/Sets): second-countability of `(Nonempty)Compacts` blocked-by-other-PR t-topology blocked on another PR
34171 SnirBroshi feat(Combinatorics/SimpleGraph/Hasse): Define the Eulerian path of a path graph t-combinatorics awaiting review
34716 CoolRmal feat: a right continuous strongly adapted process is progressively measurable WIP t-measure-probability brownian labelled WIP
31008 RemyDegenne refactor: generalize the index of the process in the Doob decomposition WIP t-measure-probability labelled WIP
34454 vihdzp refactor: `logMahlerMeasure_eq_log_MahlerMeasure` → `log_mahlerMeasure` awaiting-author t-analysis awaiting author
30185 alreadydone feat(MathlibTest): kernel reduction of nsmul on elliptic curve over ZMod awaiting-author t-number-theory t-algebraic-geometry t-algebra awaiting author
33044 bryangingechen ci: also get cache for parent commit awaiting-author merge-conflict CI failing CI
31809 ADedecker feat: differentiation of test function as a CLM blocked-by-other-PR merge-conflict t-analysis blocked on another PR
34375 jvanwinden feat(MeasureTheory/Function/AEEqOfLIntegral): introduce lemmas for rewriting a.e. inequalities t-measure-probability new-contributor awaiting review
30620 plp127 feat: copy LE and LT on preorder and partial order awaiting-author t-order awaiting author
34000 grunweg chore: golf using fun_prop [foo] syntax WIP merge-conflict labelled WIP
34188 vihdzp feat: abbrev for `Std.Total (· ≤ ·)` merge-conflict t-order merge conflict
34202 or4nge19 feat(Topology/MetricSpace): annuli in (pseudo)(e)metric spaces awaiting-author t-topology carleson awaiting author
32570 ksenono feat(Combinatorics/SimpleGraph): bipartite subgraphs and vertex-disjoint graphs for Konig's theorem t-combinatorics new-contributor awaiting review
32555 ksenono feat(Combinatorics/SimpleGraph/Matching): maximum and maximal matchings for Konig's theorem t-combinatorics new-contributor awaiting review
34636 CoolRmal feat(MeasureTheory/Analysis): the Fourier coefficients of a function can be computed by integrating over a box t-measure-probability awaiting review
34053 christian-oudard feat: Add error function (erf) and complementary error function (erfc) awaiting-author t-analysis new-contributor awaiting author
33599 nielstron feat(Computability/ContextFreeGrammar): closure under union blocked-by-other-PR new-contributor t-computability blocked on another PR
33601 nielstron feat(Computability/ContextFreeGrammar): Concatenation of CFGs is CFG blocked-by-other-PR new-contributor t-computability blocked on another PR
33592 nielstron feat(Computability/ContextFreeGrammar): mapping between two types of nonterminal symbols awaiting-author new-contributor t-computability failing CI
33108 alreadydone feat(Topology): `π₁(E⧸G)⧸π₁(E) ≃* G` for `E` path connected WIP merge-conflict t-topology t-algebraic-topology labelled WIP
19860 YaelDillies refactor: review the `simps` projections of `OneHom`, `MulHom`, `MonoidHom` WIP t-algebra opened from a branch in the main mathlib repo (not a fork)
21031 YaelDillies chore: get rid of generic hom coercions WIP opened from a branch in the main mathlib repo (not a fork)
34191 IlPreteRosso feat(Topology/Algebra/InfiniteSum): Discrete Convolution API 1st PR t-topology new-contributor awaiting review
31508 FLDutchmann feat(Tactic): `algebra` tactic. blocked-by-other-PR awaiting-author merge-conflict t-meta blocked on another PR
33619 vihdzp refactor: flip `Ixx_def` theorems merge-conflict awaiting-CI t-order does not pass CI
33080 sinhp feat(Category Theory): Cartesian Natural Transformation awaiting-author t-category-theory awaiting author
34397 Parcly-Taxel feat: integral representation of the AGM awaiting-author t-analysis awaiting author
34018 CoolRmal feat: series representation of cosecant awaiting-author t-analysis awaiting author
33832 alreadydone feat(Algebra): localization preserves unique factorization awaiting-author t-algebra maintainer-merge awaiting author
34709 dennj feat(Analysis/ODE): add discrete Grönwall inequality t-analysis new-contributor awaiting review
34729 vihdzp chore: `no_expose` various `Ordinal` definitions t-set-theory awaiting review
29788 robertmaxton42 feat(Topology): adds bundled continuous maps for sum, sigma, subtype, mapsto, inclusion awaiting-author t-topology large-import awaiting author
34908 CoolRmal feat(GroupTheory): a characteristic subgroup of a characteristic subgroup is characteristic WIP t-algebra t-group-theory labelled WIP
31361 alreadydone feat(Algebra/Order): convex subgroups awaiting-author t-algebra t-order awaiting author
34394 Citronhat feat(Algebra/Order/Ring): add constructors for linear ordered rings awaiting-author t-algebra new-contributor awaiting author
34895 eric-wieser chore: backquote tactic names in error messages delegated t-meta opened from a branch in the main mathlib repo (not a fork)
34182 IlPreteRosso feat(Data/Finsupp/Single, Data/Finsupp/Indicator): Add set_indicator_singleton, indicator_singleton; golfed single_eq_set_indicator, single_eq_indicator new-contributor t-data large-import awaiting review
34151 gasparattila feat(Topology/Sets): product of `Closeds` t-topology awaiting review
31925 alreadydone feat(Topology): étalé space associated to a predicate on sections blocked-by-other-PR merge-conflict t-topology blocked on another PR
34099 mcdoll feat(Analysis/Distribution): Fourier multiplier t-analysis awaiting review
33634 xgenereux feat(ValuationSubring): eq_self_or_eq_top_of_le blocked-by-other-PR t-algebra large-import blocked on another PR
34088 kbuzzard perf(RingTheory/Kaehler/Polynomial): change universe name for speed-up WIP t-ring-theory labelled WIP
34956 kbuzzard test: add a file with universe tests t-ring-theory failing CI
33493 michelsol feat(RingTheory/Polynomial): An explicit formula for the Chebyshev polynomials of the first kind awaiting-author new-contributor t-ring-theory awaiting author
28468 alreadydone feat(Algebra): ring API for `AddLocalization` awaiting-author t-algebra large-import t-ring-theory awaiting author
34815 Deep0Thinking feat(Analysis/SpecialFunctions/ImproperIntegrals): Frullani integral blocked-by-other-PR awaiting-author t-analysis new-contributor large-import blocked on another PR
34573 Kha chore(Analysis/Normed/Lp/SmoothApprox): shake public imports failing CI
34093 YellPika feat(Order/OmegaCompletePartialOrder): add `OmegaCompletePartialOrder` instance for `Option` with basic `ωScottContinuous` lemmas t-order new-contributor awaiting review
34266 gasparattila feat(Topology/Sets): basis of `(Nonempty)Compacts` t-topology awaiting review
9820 jjaassoonn feat(RingTheory/GradedAlgebra/HomogeneousIdeal): generalize to homogeneous submodule merge-conflict t-ring-theory opened from a branch in the main mathlib repo (not a fork)
29030 b-mehta feat(Combinatorics): prove the Rado selection lemma t-combinatorics opened from a branch in the main mathlib repo (not a fork)
27664 pechersky feat(Topology,Analysis): discrete topology metric space and normed groups awaiting-author merge-conflict t-topology failing CI
34475 artie2000 fix: remove some nolints WIP merge-conflict t-ring-theory labelled WIP
34646 vihdzp feat: predicate for algebraically closed subfields blocked-by-other-PR merge-conflict t-algebra blocked on another PR
34652 vihdzp feat: more theorems on `Polynomial.toSubring` blocked-by-other-PR merge-conflict t-ring-theory blocked on another PR
34720 Paul-Lez feat(RingTheory/PowerSeries/Composition): define composition of power series awaiting-zulip t-ring-theory failing CI
34756 Hagb feat(Algebra/Order/Monoid/Unbundled/WithTop): `AddEquiv` between `WithBot` t-algebra awaiting review
34808 YaelDillies feat(Combinatorics/SimpleGraph): isolated vertices RFC t-combinatorics awaiting review
26985 agjftucker feat(Analysis/Calculus/ImplicitFunction): define implicitFunctionOfProdDomain t-analysis new-contributor awaiting review
32744 NoneMore feat(ModelTheory/Definablity): add `DefinableFun` definition and lemmas t-logic new-contributor awaiting review
30431 kckennylau feat(RingTheory): a homogeneous submodule is the span of its homogeneous elements t-ring-theory failing CI
14501 jjaassoonn feat: module structure of filtered colimit of abelian groups over filtered colimit of rings awaiting-author merge-conflict t-category-theory t-algebra workshop-AIM-AG-2024 ??? opened from a branch in the main mathlib repo (not a fork)
26986 WangYiran01 feat(Partition): add bijection for partitions with max part ≤ r awaiting-author merge-conflict t-combinatorics new-contributor failing CI
25035 ScottCarnahan feat(Algebra/Module/Equiv/Defs): linear equivalence between linear hom and semilinear hom WIP merge-conflict t-algebra opened from a branch in the main mathlib repo (not a fork)
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 merge-conflict t-measure-probability new-contributor blocked on another PR
33463 khwilson feat(Mathlib/Analysis/Polynomial/MahlerMeasure): Mahler Measure for other rings awaiting-author t-analysis new-contributor awaiting author
33631 xgenereux feat(ValuationSubring): simp lemmas for idealOfLE/ofPrime in relation to top/bot t-algebra awaiting review
34481 DAE123456 feat: Ore's Theorem t-combinatorics new-contributor awaiting review
34722 GrigorenkoPV feat(Data/Finset/RangeDistance): add new-contributor t-data awaiting review
34809 YaelDillies feat: induced subgraphs of complete multipartite graphs are complete multipartite t-combinatorics awaiting review
33611 urkud feat(ImplicitFunction): add a parametric version awaiting-author t-analysis awaiting author
27702 FLDutchmann feat(NumberTheory/SelbergSieve): define Lambda-squared sieves and prove important properties delegated merge-conflict t-number-theory failing CI
28499 yoh-tanimoto feat(MeasureTheory/VectorMeasure): add integral of a vector-valued function against a vector measure blocked-by-other-PR merge-conflict t-measure-probability blocked on another PR
28693 faenuccio feat(Analysis.Normed.Module.Milman-Pettis): add Milman-Pettis theorem WIP merge-conflict t-analysis labelled WIP
31141 peabrainiac feat(Analysis/Calculus): parametric integrals over smooth functions are smooth awaiting-author t-analysis maintainer-merge awaiting author
35122 Marygold-Dusk feat: define C^n submersions t-differential-geometry new-contributor awaiting review
32845 jonasvanderschaaf feat(CategoryTheory): `GrothendieckTopology.yoneda` preserves certain (co)limits awaiting-author t-category-theory new-contributor t-condensed large-import awaiting author
33969 goliath-klein refactor(PiTensorProduct/{InjectiveNorm, ProjectiveNorm}): Currently, injectiveSeminorm = projectiveSeminorm WIP merge-conflict t-analysis new-contributor large-import labelled WIP
34248 erdOne chore: get rid of `LocalizedModule.mk` awaiting-author merge-conflict t-algebra merge conflict
27307 xyzw12345 feat(RingTheory/GradedAlgebra): homogeneous relation awaiting-author t-ring-theory awaiting author
34939 erdOne chore(AlgebraicGeometry): use relative gluing in `IdealSheaf` merge-conflict t-algebraic-geometry failing CI
33821 JohnnyTeutonic feat(LinearAlgebra/Matrix/Hermitian): add IsSkewHermitian predicate awaiting-author t-algebra awaiting author
34990 bwangpj feat: `ContinuousSMul (∀ i, N i) (∀ i, γ i)` t-topology awaiting review
34994 bwangpj feat: Countable.of_module_finite t-algebra FLT large-import awaiting review
34650 vihdzp feat: redefine `Polynomial.toSubring` with better def-eqs t-ring-theory failing CI
34846 fpvandoorn fix: module system and translate interaction blocked-by-other-PR awaiting-author merge-conflict t-meta blocked on another PR
34931 eric-wieser perf: make TensorProduct.lift irreducible with a unification hint merge-conflict t-algebra opened from a branch in the main mathlib repo (not a fork)
34164 Scarlett-le feat(Geometry/Euclidean/Sphere): define arcs on spheres awaiting-author t-euclidean-geometry awaiting author
34969 kim-em feat(RingTheory/HopfAlgebra): prove antipode is antihomomorphism t-ring-theory awaiting review
33032 ksenono feat(Combinatorics/SimpleGraph): Konig’s theorem on bipartite graphs blocked-by-other-PR merge-conflict t-combinatorics new-contributor blocked on another PR
31662 edwin1729 feat(Topology/Order): topological basis of scott topology on Complete… awaiting-author merge-conflict t-topology new-contributor merge conflict
27198 robin-carlier feat(CategoryTheory/Monoidal/DayConvolution): the Yoneda embedding is monoidal (for Day convolution) blocked-by-other-PR merge-conflict t-category-theory file-removed blocked on another PR
34159 wangying11123 feat(Geometry/Euclidean/Similarity): Add Triangle similarity on oangle awaiting-author t-euclidean-geometry new-contributor awaiting author
32807 WilliamCoram feat: Define the Gauss norm for MvPowerSeries new-contributor t-ring-theory awaiting review
35255 vlad902 feat(SimpleGraph): `cycleGraph.IsContained` in every graph with a cycle blocked-by-other-PR t-combinatorics blocked on another PR
34799 vlad902 feat(SimpleGraph): the cycle graph and complete graph are Hamiltonian blocked-by-other-PR merge-conflict t-combinatorics large-import blocked on another PR
31366 FaffyWaffles feat(Analysis/SpecialFunctions/StirlingRobbins): Robbins' sharp stepwise bound for stirlingSeq awaiting-author t-analysis new-contributor awaiting author
34571 xroblot feat(CyclotomicField/Galois): the bijection between subfields and subgroups of Dirichlet characters blocked-by-other-PR merge-conflict t-algebra large-import blocked on another PR
31560 AntoineChambert-Loir feat(Topology/Sion): the minimax theorem of von Neumann - Sion t-topology awaiting review
33944 artie2000 feat(Algebra/Ring): formally real rings t-algebra awaiting review
34069 artie2000 feat(Algebra/Order/Algebra): algebra is ordered iff inclusion map is monotone t-algebra t-order awaiting review
34702 pfaffelh feat(Data/FinsetPowerset): The set `{v : List.Vector Bool n | v.val.count = k}` has cardinality `n.choose k` t-data large-import awaiting review
34820 staroperator feat(Order/Ideal): more results on order ideals t-order large-import awaiting review
35144 daniel-carranza feat(CategoryTheory/Enriched): tensor product of enriched categories awaiting-author t-category-theory new-contributor infinity-cosmos awaiting author
33050 mkaratarakis feat: lemmas for the analytic part of the proof of the Gelfond–Schneider theorem WIP t-number-theory new-contributor labelled WIP
30900 vihdzp feat: run-length encoding t-data awaiting review
33217 Blackfeather007 feat(Algebra): define associated graded structure for abelian group awaiting-author new-contributor t-ring-theory awaiting author
34948 joneugster feat(scripts/autolabel): add option to configure number of applied labels CI awaiting review
33020 FormulaRabbit81 chore(Topology): Deprecate file merge-conflict t-topology large-import merge conflict
34677 joneugster feat(scripts/autolabel): add missing folders CI awaiting review
23042 joneugster feat(CategoryTheory/Enriched/Limits): add HasConicalLimitsOfSize.shrink WIP please-adopt t-category-theory infinity-cosmos opened from a branch in the main mathlib repo (not a fork)
23142 joneugster feat(CategoryTheory/Enriched/Limits): add API for HasConicalLimit awaiting-author please-adopt t-category-theory infinity-cosmos opened from a branch in the main mathlib repo (not a fork)
23145 joneugster feat(CategoryTheory/Enriched/Limits): add IsConicalLimits blocked-by-other-PR please-adopt merge-conflict t-category-theory infinity-cosmos opened from a branch in the main mathlib repo (not a fork)
20401 RemyDegenne feat: add sigmaFinite_iUnion awaiting-author merge-conflict t-measure-probability opened from a branch in the main mathlib repo (not a fork)
33281 michelsol feat(Analysis/SpecialFunctions/Integrals): integral of 1/sqrt(1-x^2) and its integrability. merge-conflict t-analysis new-contributor merge conflict
35339 grunweg feat: "confusing variables" linter please-adopt merge-conflict awaiting-CI t-linter ❌? looking for help
35342 grunweg feat: add Diffeomorph.sumSumSumComm WIP t-differential-geometry labelled WIP
27897 grunweg feat: check indentation of doc-strings merge-conflict awaiting-CI t-linter does not pass CI
11500 mcdoll refactor(Topology/Algebra/Module/WeakDual): Clean up awaiting-author merge-conflict t-topology ??? opened from a branch in the main mathlib repo (not a fork)
20428 madvorak feat(Data/Sign): lemmas about `∈ Set.range SignType.cast` WIP merge-conflict t-data opened from a branch in the main mathlib repo (not a fork)
29281 plp127 doc: `Fin.natAdd_castLEEmb` merge-conflict t-data merge conflict
34797 vlad902 feat(SimpleGraph): `cycleGraph_EulerianCircuit` is a cycle awaiting-author t-combinatorics awaiting author
34165 zcyemi feat(Archive/Imo/Imo2012Q5): IMO 2012 Q5 blocked-by-other-PR merge-conflict IMO large-import blocked on another PR
27936 alreadydone feat(Algebra): additivize Dvd and Prime awaiting-author merge-conflict t-algebra merge conflict
34156 zcyemi feat(Analysis/Convex/Between): add lemmas on convex combination of mem simplex interior merge-conflict t-analysis merge conflict
34503 alreadydone chore(RingTheory/Localization): generalize FractionRing to semirings WIP merge-conflict awaiting-CI t-algebra t-ring-theory labelled WIP
34973 chrisflav chore: replace `Punit` by `PUnit` merge-conflict failing CI
35134 fpvandoorn feat(translate): print constant names with hover info awaiting-author merge-conflict t-meta merge conflict
29777 yuanyi-350 feat(Functional Analysis): closed Range Theorem WIP blocked-by-other-PR awaiting-author merge-conflict t-analysis new-contributor blocked on another PR
29151 yuanyi-350 feat: Corollary of Hahn–Banach theorem awaiting-author merge-conflict t-analysis new-contributor large-import merge conflict
35341 grunweg feat: lint against the tactic.skipAssignedInstances option in mathlib please-adopt t-linter looking for help
35344 grunweg feat: lint upon uses of the mono tactic please-adopt RFC t-linter looking for help
29965 RemyDegenne feat(probability): define subtraction of kernels WIP t-measure-probability large-import labelled WIP
34442 JohnnyTeutonic feat(Algebra/Lie/Classical): add basis for sl(n) relative to chosen diagonal index t-algebra awaiting review
35152 j-loreaux feat: add missing API for `lp E p` t-analysis awaiting review
32534 erdOne feat(AlgebraicGeometry): Zariski's main theorem WIP t-ring-theory labelled WIP
35398 vlad902 feat(SimpleGraph): `bypass` lemmas t-combinatorics awaiting review
35414 joneugster feat(Cache): Allow arguments of the form `Mathlib.Data.+` which correspond to a folder but not a file t-meta CI awaiting review
35413 joneugster fix(Util/CountHeartbeats): move elaboration in #count_heartbeats inside a namespace t-meta awaiting review
16215 adomasbaliuka feat(Tactic/Linter): lint unwanted unicode merge-conflict t-linter opened from a branch in the main mathlib repo (not a fork)
32918 michelsol feat: define `supEdist` and `supDist` merge-conflict t-topology new-contributor merge conflict
34909 SnirBroshi feat(Data/Sym/Sym2): `fromRel` equivalence with `Sigma` over a `Quotient` t-data awaiting review
33275 YuvalFilmus feat(Trigonometric/Chebyshev/Extremal): Chebyshev polynomials maximize iterated derivatives t-analysis awaiting review
33850 YuvalFilmus feat(Chebyshev/ChebyshevGauss): Chebyshev–Gauss formula t-analysis awaiting review
29145 JovanGerb chore: use `to_additive` in more places merge-conflict t-meta awaiting-CI does not pass CI
33288 vihdzp chore(Combinatorics/SimpleGraph/Paths): review API merge-conflict t-combinatorics merge conflict
34024 adomani feat: the global syntax linter blocked-by-other-PR merge-conflict t-linter large-import blocked on another PR
34601 themathqueen feat(Combinatorics/SimpleGraph/AdjMatrix): adjacency matrix API t-combinatorics large-import awaiting review
35017 robo7179 feat(Combinatorics/SimpleGraph/Acyclic): add every nontrivial tree has atleast two leaves t-combinatorics new-contributor awaiting review
30001 vihdzp feat: concept generated by set of objects/attributes blocked-by-other-PR t-order blocked on another PR
16553 grunweg WIP: tinkering with orientable manifolds WIP blocked-by-other-PR merge-conflict t-differential-geometry opened from a branch in the main mathlib repo (not a fork)
34578 dennj feat: define Boolean circuits over abstract gate families new-contributor t-computability awaiting review
31607 grunweg chore: rename `continuous{,On,At,Within}_const` to `ContinuousFoo.const` delegated merge-conflict awaiting-CI does not pass CI
27500 Komyyy feat: the Riemann zeta function is meromorphic WIP t-analysis large-import labelled WIP
35418 vlad902 feat(SimpleGraph): `IsAcyclic` iff not 2-edge-reachable t-combinatorics awaiting review
26345 mans0954 feat(Analysis/LocallyConvex/Polar): Bipolar theorem awaiting-author please-adopt merge-conflict t-analysis large-import looking for help
26413 michaellee94 feat: existence of maximal solutions for ODEs meeting Picard-Lindelöf conditions blocked-by-other-PR merge-conflict t-analysis new-contributor blocked on another PR
33387 AntoineChambert-Loir chore(LinearAlgebra/Transvection/Basic): mv Transvection.lean file to Transvection.Basic.lean blocked-by-other-PR merge-conflict t-algebra file-removed blocked on another PR
33392 AntoineChambert-Loir feat(LinearAlgebra/Transvection/Generation): non-exceptional case in Dieudonné's theorem blocked-by-other-PR merge-conflict t-algebra file-removed blocked on another PR
33402 AntoineChambert-Loir feat(LinearAlgebra/Transvection/Generation): prove exceptional case in Dieudonné's theorem blocked-by-other-PR t-algebra file-removed blocked on another PR
33485 AntoineChambert-Loir feat(LinearAlgebra/Transvection/Generation): prove the third part of Dieudonné's theorem blocked-by-other-PR merge-conflict t-algebra file-removed blocked on another PR
33560 AntoineChambert-Loir feat(LinearAlgebra/Transvection/Generation): a linear equivalence is the product of dilatransvections blocked-by-other-PR merge-conflict t-algebra file-removed blocked on another PR
33692 AntoineChambert-Loir feat(LinearAlgebra/Transvection/SpecialLinearGroup): generation of the special linear group by transvections blocked-by-other-PR merge-conflict t-algebra file-removed blocked on another PR
33715 AntoineChambert-Loir feat(LinearAlgebra/Projectivization/Action): prove that the action is 2-transitive and primitive blocked-by-other-PR merge-conflict t-algebra large-import file-removed blocked on another PR
33882 AntoineChambert-Loir feat(LinearAlgebra/Transvection/SpecialLinearGroup): commutators in the special linear group blocked-by-other-PR merge-conflict t-algebra file-removed blocked on another PR
33916 AntoineChambert-Loir feat(LinearAlgebra/SpecialLinearGroup/Simple): simplicity of the projective special linear group. blocked-by-other-PR merge-conflict t-algebra large-import file-removed blocked on another PR
33736 fbarroero feat(RingTheory/Polynomial/GaussNorm): The `gaussNorm` is an absolute value if `v` is a nonarchimedean absolute value t-ring-theory awaiting review
31425 robertmaxton42 feat(Topology): implement delaborators for non-standard topology notation t-topology awaiting review
31613 xyzw12345 feat(RepresentationTheory/GroupCohomology): Non-abelian Group Cohomology awaiting-author t-algebra large-import awaiting author
33712 wangying11123 feat(Geometry/Euclidean/Angle/Unoriented/Projection): Add sameray_orthogonalProjection_vsub_of_angle_lt awaiting-author t-euclidean-geometry new-contributor awaiting author
33786 hdmkindom feat(Analysis/Matrix): add Jacobian matrix for matrix-valued functions awaiting-author t-analysis new-contributor awaiting author
30667 FrederickPu feat(‎Mathlib/Algebra/Group/Subgroup/Pointwise): subgroup mul t-algebra new-contributor failing CI
34025 lua-vr feat(Integral.Bochner.Set): add `tendsto_setIntegral_of_monotone₀` delegated t-measure-probability delegated
35448 mathlib-splicebot chore(Mathlib/Tactic/Linter/GlobalSyntax.lean): automated extraction new-contributor t-linter opened from a branch in the main mathlib repo (not a fork)
33664 ooovi feat(Geometry/Convex/Cone/Pointed): face lattice of pointed cones blocked-by-other-PR awaiting-author merge-conflict file-removed t-convex-geometry ❌? blocked on another PR
33793 LTolDe feat(MeasureTheory/Constructions/Polish/Basic): add lemma AnalyticSet.inter_nonempty_of_nowhereMeagre awaiting-author t-measure-probability new-contributor awaiting author
35400 vlad902 feat(SimpleGraph): `IsEdgeReachable` lemmas t-combinatorics awaiting review
34851 dennj feat(Data/Matrix/Mul): add diagonal and transpose lemmas for vector operations new-contributor t-data awaiting review
24965 erdOne refactor: Make `IsLocalHom` take unbundled map delegated merge-conflict t-algebra opened from a branch in the main mathlib repo (not a fork)
25622 eric-wieser refactor: overhaul instances on LocalizedModule merge-conflict t-algebra opened from a branch in the main mathlib repo (not a fork)
25980 Multramate refactor(Algebra/Group/Submonoid/Operations): rename restrict to domRestrict and add restrict merge-conflict t-group-theory merge conflict
25981 Multramate feat(GroupTheory/GroupAction/Basic): define homomorphisms of fixed subgroups induced by homomorphisms of groups merge-conflict large-import t-group-theory merge conflict
28546 Sfgangloff feat(SymbolicDynamics): basic setup of Zd, full shift, cylinders, pat… t-dynamics new-contributor awaiting review
35313 LexinonCraft feat: IMO 2025 Q4 awaiting-author new-contributor IMO awaiting author
28462 joelriou feat(AlgebraicTopology/SimplicialSet): the relative cell complex attached to a rank function for a pairing WIP blocked-by-other-PR merge-conflict t-algebraic-topology blocked on another PR
29764 ScottCarnahan feat(Algebra/Vertex): API up to residue products (WIP) blocked-by-other-PR merge-conflict t-algebra large-import blocked on another PR
35316 mkaratarakis feat: lemmas for the analytic part of the proof of the Gelfond–Schneider theorem (Part 4/5) blocked-by-other-PR t-number-theory new-contributor blocked on another PR
31603 alreadydone chore(Algebra): make `RatFunc` an abbrev awaiting-author merge-conflict RFC t-algebra merge conflict
33276 NicolaBernini feat: Rename List.reverse_perm to List.reverse_perm_self and List.reverse_perm' to List.reverse_perm_iff awaiting-author merge-conflict new-contributor t-data merge conflict
33303 sinhp feat(CategoryTheory): The monads and comonads of locally cartesian closed categories WIP merge-conflict t-category-theory labelled WIP
33441 dupuisf feat: add `LawfulInv` class for types with an inverse that behaves like `Ring.inverse` merge-conflict t-algebra awaiting-zulip awaiting a zulip discussion
33795 alreadydone feat(Topology/Sheaves): LocalPredicate prerequisite for étalé spaces merge-conflict t-topology merge conflict
33810 dupuisf feat: add instances of `LawfulInv` WIP blocked-by-other-PR merge-conflict ⚠️ blocked on another PR
34075 eric-wieser feat: add a typeclass for the continuum hypothesis awaiting-author merge-conflict t-set-theory opened from a branch in the main mathlib repo (not a fork)
34179 alreadydone refactor(Algebra): weaken NormalizationMonoid awaiting-author merge-conflict t-algebra t-ring-theory merge conflict
35197 j-loreaux feat: Hölder framework for `lp` spaces blocked-by-other-PR merge-conflict t-analysis blocked on another PR
34245 staroperator feat(Data/Set): add `Set.Uncountable` awaiting-zulip t-data failing CI
31449 kim-em feat(SemilocallySimplyConnected): definition and alternative formulation awaiting-author t-topology awaiting author
34557 kim-em feat(Topology/Homotopy): add Path.subpathOn for restricting paths to subintervals awaiting-author t-topology awaiting author
34077 kbuzzard perf: increase priority of instSMulOfMul t-algebra awaiting-zulip awaiting a zulip discussion
26299 adomani perf: the `whitespace` linter only acts on modified files awaiting-author t-linter awaiting-zulip awaiting a zulip discussion
35345 grunweg feat(Linter.openClassical): also lint for Classical declarations as t-linter failing CI
34674 Citronhat feat(Algebra/Order/Ring): replace ENNReal lemmas with WithTop versions merge-conflict t-algebra new-contributor merge conflict
31892 jsm28 feat(Geometry/Euclidean/Sphere/PolePolar): poles and polars blocked-by-other-PR t-euclidean-geometry blocked on another PR
31893 jsm28 feat(Geometry/Euclidean/Sphere/Tangent): characterize `tangentsFrom` blocked-by-other-PR t-euclidean-geometry blocked on another PR
31981 jsm28 feat(Geometry/Euclidean/Incenter): `tangentSet` and `tangentsFrom` lemmas blocked-by-other-PR t-euclidean-geometry blocked on another PR
35360 vlad902 chore: rename `cycleGraph_EulerianCircuit` to `cycleGraph.cycle` t-combinatorics awaiting review
26966 vihdzp feat: the Dedekind–MacNeille completion blocked-by-other-PR t-order blocked on another PR
35472 rao107 feat(Probability): add `CharacteristicFunction` section to binomial distribution blocked-by-other-PR t-measure-probability new-contributor blocked on another PR
33252 SnirBroshi chore(Combinatorics/SimpleGraph/Coloring): use `IsIndepSet` instead of `IsAntichain` to spell "a color class is an independent set" t-combinatorics awaiting review
35417 joneugster refactor(Cache): use module name for file hash instead of non-resolved file path blocked-by-other-PR merge-conflict t-meta CI blocked on another PR
34193 bwangpj feat(Topology/Algebra/Ring): ContinuousAddEquiv.mulLeft, mulRight t-topology maintainer-merge FLT awaiting review
35521 grunweg feat: the unusedSetOptionIn linter (rebased) WIP t-linter large-import labelled WIP
32891 felixpernegger feat(Topology/EMetricSpace): Introduction of ```Weak(Pseudo)EMetricSpace``` awaiting-author merge-conflict t-topology new-contributor failing CI
35277 marcelolynch ci: remove outdated logic in workflows awaiting-author CI file-removed awaiting author
35216 kim-em doc(Tactic/Translate/ToDual): add deployment guide for @[to_dual] documentation enhancement awaiting-author awaiting author
30666 erdOne feat(NumberTheory): every number field has a ramified prime awaiting-author t-number-theory t-algebra failing CI
34954 brianrabern feat(Combinatorics/SimpleGraph/Acyclic): add colorable and chromaticN… t-combinatorics new-contributor awaiting review
33416 vihdzp chore(Order/GameAdd): add `elab_as_elim` attributes merge-conflict t-order merge conflict
34637 mcdoll feat(Analysis/Distribution): support t-analysis awaiting review
34240 mcdoll feat(Analysis/Distribution): additional properties of the support WIP blocked-by-other-PR merge-conflict t-analysis blocked on another PR
35558 mcdoll feat(Analysis/Distribution): algebraic properties of the support blocked-by-other-PR t-analysis blocked on another PR
34298 CoolRmal feat(MeasureTheory): Integral over Ioi tends to zero t-measure-probability awaiting review
35352 themathqueen feat(Analysis/CStarAlgebra): the norm of a positive linear functional `f` on a unital C*-algebra is `f 1` awaiting-author t-analysis awaiting author
25989 Multramate feat(NumberTheory/EllipticDivisibilitySequence): add elliptic nets awaiting-author t-number-theory large-import awaiting author
35411 daniel-carranza feat(CategoryTheory/Enriched/Limits): define cotensors in an enriched category WIP blocked-by-other-PR t-category-theory infinity-cosmos blocked on another PR
35545 joelriou feat(Algebra/Category/ModuleCat): the internal hom for presheaves of modules WIP t-algebra labelled WIP
28246 Sebi-Kumar feat(AlgebraicTopology/FundamentalGroupoid): the n-sphere is simply connected for n > 1 awaiting-author new-contributor t-algebraic-topology awaiting author
29533 Thmoas-Guan feat(Algebra): maximal Cohen Macaulay module blocked-by-other-PR merge-conflict large-import ⚠️ blocked on another PR*
29557 Thmoas-Guan feat(Algebra): finite projective dimension of regular blocked-by-other-PR t-algebra large-import blocked on another PR
31611 thorimur feat(Meta): `withPlural` wrapper for more readable messages in source awaiting-author merge-conflict t-meta merge conflict
35568 goliath-klein refactor(PiTensorProduct/{InjectiveNorm, ProjectiveNorm}): switch NormedSpace instance to `projectiveSeminorm` blocked-by-other-PR new-contributor blocked on another PR
31697 Thmoas-Guan feat(Homology): bijection between `Ext` blocked-by-other-PR t-category-theory t-algebra blocked on another PR
31768 Thmoas-Guan feat(Homology): `Ext` commute with ulift functor blocked-by-other-PR t-category-theory t-algebra blocked on another PR
31851 Thmoas-Guan feat(Algebra/Homology): Injective dimension in linear equiv blocked-by-other-PR t-algebra blocked on another PR
35524 grunweg feat: text-based linter against \t followed by tactic mode t-linter awaiting-zulip failing CI
31219 Thmoas-Guan feat(Algebra): lemma about `IsBaseChange` under exact sequence awaiting-author t-ring-theory awaiting author
31222 Thmoas-Guan feat(Algebra): `Hom` commute with flat base change blocked-by-other-PR t-algebra large-import blocked on another PR
33369 Thmoas-Guan feat(Homology): `Ext` commute with flat base change blocked-by-other-PR large-import ⚠️ blocked on another PR
35547 Ruben-VandeVelde chore: tidy various files awaiting-author opened from a branch in the main mathlib repo (not a fork)
34249 xyzw12345 feat(GroupTheory/GroupAction/Hom): connect existing definitions `MulDistribMulActionHom` and `DistribMulActionHom` using `to_additive` delegated t-algebra delegated
34119 themathqueen feat(LinearAlgebra/Matrix/WithConv): `Matrix.toLin'` as a star-algebra equivalence between their convolutive rings blocked-by-other-PR t-algebra large-import blocked on another PR
35421 farmanb feat(CategoryTheory): preradicals in abelian categories awaiting-author t-category-theory new-contributor awaiting author
35578 Shreyas4991 fix: writer monad should use an additive logging type awaiting-zulip t-data awaiting a zulip discussion
35510 chrisflav feat(RingTheory): weakly étale algebras WIP blocked-by-other-PR t-ring-theory blocked on another PR
30077 agjftucker feat(Analysis/Calculus/ImplicitFunction): define implicitFunctionOfBivariate t-analysis awaiting review
35441 harahu chore(NumberTheory): fix indentation in markdown lists t-number-theory awaiting review
35447 themathqueen feat(LinearAlgebra/UnitaryGroup): the transpose and conjugate of a unitary matrix as a unitary matrix t-algebra awaiting review
35451 samueloettl feat(MeasureTheory.Function): compMeasurePreserving_iterate t-measure-probability new-contributor awaiting review
35458 harahu chore(Algebra): fix indentation in markdown lists t-algebra awaiting review
33121 SnirBroshi feat(Combinatorics/SimpleGraph/Hasse): paths in a graph are isomorphic to path graphs t-combinatorics awaiting review
34054 YellPika feat(Order/OmegaCompletePartialOrder): OmegaCompletePartialOrder instance for `Sigma` with basic `ωScottContinuous` lemmas awaiting-author t-order new-contributor please-merge-master awaiting author
34859 wwylele feat(MeasureTheory): WithLp 2 (U × V) → U × V is measure preserving t-measure-probability awaiting review
33292 SnirBroshi feat(Combinatorics/SimpleGraph/LineGraph): lift copies/isomorphisms to line-graph t-combinatorics large-import awaiting review
31884 Thmoas-Guan feat(RingTheory): definition of Gorenstein local ring 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
33377 Thmoas-Guan feat(RingTheory): polynomial over Gorenstein ring is Gorenstein blocked-by-other-PR large-import t-ring-theory blocked on another PR
33379 Thmoas-Guan feat(RingTheory): Gorenstein local ring is Cohen Macaulay blocked-by-other-PR large-import t-ring-theory blocked on another PR
33380 Thmoas-Guan feat(RingTheory): Gorenstein local ring is Cohen--Macaulay local ring of type one blocked-by-other-PR large-import t-ring-theory blocked on another PR
35588 eric-wieser chore(Util/Qq): remove `meta` t-meta awaiting-CI opened from a branch in the main mathlib repo (not a fork)
35285 SnirBroshi feat(Algebra/LinearRecurrence): define a standard basis for the solution space of a linear recurrence t-algebra awaiting review
34315 LessnessRandomness feat(Combinatorics/SimpleGraph/Bipartite): Prove upper bound of edge set cardinality of bipartite graph t-combinatorics awaiting review
29203 Hagb feat(RingTheory/MvPolynomial/Groebner): add Gröbner basis awaiting-author large-import t-ring-theory awaiting author
34873 Hagb feat(RingTheory/MvPolynomial/Groebner/Remainder): polynomial remainder used with Gröbner basis WIP blocked-by-other-PR merge-conflict large-import t-ring-theory blocked on another PR
34966 Deep0Thinking feat(MeasureTheory): add `continuousWithinAt_Ici/Iic_primitive_Ioi/Iio` and `continuousOn_Ici/Iic_primitive_Ioi/Iio/Ici/Iic` t-measure-probability new-contributor awaiting review
34144 IvanRenison feat(Data/ENat): add lemma `ENat.iInf_eq_coe_iff` t-data awaiting review
35615 SnirBroshi feat(Combinatorics/SimpleGraph/Maps): lemmas about support t-combinatorics awaiting review
35616 SnirBroshi feat(Combinatorics/SimpleGraph/Copy): `IsContained` and `IsIndContained` are preorders t-combinatorics awaiting review
35613 SnirBroshi feat(Combinatorics/SimpleGraph/Clique): use `IsContained` instead of an explicit embedding from top t-combinatorics awaiting review
35619 SnirBroshi feat(Combinatorics/SimpleGraph/Clique): intersection and union of cliques t-combinatorics awaiting review
30526 SnirBroshi chore(Logic/Relation): use `≤` to spell subrelation t-logic awaiting review
35554 vihdzp refactor: deprecate `Trunc` in favor of `Squash` awaiting-CI t-data does not pass CI
12933 grunweg chore: replace some use of > or ≥ by < or ≤ awaiting-author merge-conflict opened from a branch in the main mathlib repo (not a fork)
35620 inaciovasquez2020 feat(Fintype): choose element from nonempty finite type new-contributor t-data failing CI
35043 winstonyin refactor(Analysis/ODE): restate existence and uniqueness using integral curve API blocked-by-other-PR blocked on another PR
35638 vihdzp chore(Topology/Order/OrderClosed): use `to_dual` blocked-by-other-PR blocked on another PR
35622 SnirBroshi feat(Logic/Function/Basic): `onFun` and `swap` preserve relation properties t-logic awaiting review
34941 urkud feat(FDeriv/Prod): generalize to TVS blocked-by-other-PR t-analysis blocked on another PR
34937 tannerduve feat(Computability): semilattice instance on Turing degrees new-contributor t-computability large-import awaiting review
35295 Rida-Hamadani feat(SimpleGraph): `dropLast` of a cycle is a path t-combinatorics awaiting review
35655 Rida-Hamadani feat(SimpleGraph): strongly regular graphs have diameter 2 blocked-by-other-PR t-combinatorics blocked on another PR
32941 kim-em feat(GroupTheory/Artin): add braid groups as Artin groups of type A blocked-by-other-PR t-group-theory blocked on another PR
22366 kim-em feat: `check_equalities` tactic for diagnosing defeq problems delegated t-meta opened from a branch in the main mathlib repo (not a fork)
35504 JoaBjo feat(Probability/Distributions/Exponential): add MGF, moments, and memoryless property t-measure-probability new-contributor awaiting review
33746 ster-oc feat(Algebra/Module/ZLattice): align `ZSpan.floor` to `Int.floor` API merge-conflict t-algebra new-contributor merge conflict
35011 whocares-abt feat(Combinatorics/SimpleGraph/Copy): add degree of copy less than original t-combinatorics new-contributor awaiting review
35635 vihdzp chore(Order/Interval/Set/LinearOrder): use `to_dual` awaiting-CI t-order does not pass CI
35178 grunweg chore: split `T%` elaborator into its own file and move to `Topology` WIP merge-conflict labelled WIP
31580 grunweg feat: towards `ContMDiff` support in fun_prop WIP merge-conflict t-meta t-differential-geometry labelled WIP
28291 vasnesterov feat(Tactic): tactic for computing asymptotics of real functions WIP blocked-by-other-PR t-meta t-analysis large-import blocked on another PR
35671 CoolRmal feat: APIs for semifinite measures WIP t-measure-probability labelled WIP
35666 urkud chore(Calculus/FDeriv/Pi): migrate to TVS blocked-by-other-PR blocked on another PR
33972 YuvalFilmus feat(Analysis/Polynomial/Order): polynomial has fixed sign beyond largest root t-analysis awaiting-zulip awaiting a zulip discussion
35136 joelriou feat(AlgebraicGeometry): points of the small étale site WIP blocked-by-other-PR merge-conflict t-algebraic-geometry large-import blocked on another PR
34830 parabamoghv feat(CategoryTheory/Monoidal): add definition of categorical groups WIP t-category-theory new-contributor labelled WIP
33688 Citronhat feat(PMF): add expectation lemmas for Poisson PMF awaiting-author t-measure-probability new-contributor awaiting author
31766 SuccessMoses feat(Topology/EMetricSpace): continuity of arc length awaiting-author merge-conflict t-topology new-contributor merge conflict
35682 chenson2018 chore(Computability/Partrec): remove `linter.flexible` exceptions t-computability maintainer-merge awaiting review
33143 wwylele feat(PowerSeries): pentagonal number theorem t-algebra awaiting review
35697 gasparattila chore: call `dsimp` in the default tactics of `Homeomorph` fields blocked-by-other-PR blocked on another PR
33257 NickAdfor feat(Combinatorics/SimpleGraph/Bipartite): Odd Cycle Theorem (A Solution to TODO) t-combinatorics new-contributor awaiting review
34599 cameronfreer feat(Logic/Equiv/Fintype): generalize toCompl and exists_extending_pair to finite source new-contributor t-group-theory awaiting review
35440 harahu chore(Order): fix indentation in markdown lists t-order awaiting review
35549 JovanGerb fix(Translate): don't look in arguments of free variables in `shouldTranslate` t-meta awaiting review
30982 jsm28 feat(Geometry/Euclidean/Angle/Incenter): angle bisection and the incenter t-euclidean-geometry awaiting review
32294 jsm28 feat(Geometry/Euclidean/Angle/Incenter): distance from second intersection with circumcircle blocked-by-other-PR t-euclidean-geometry blocked on another PR
34717 CoolRmal feat: add more APIs for the first derivative test WIP ⚠️ labelled WIP
33691 kim-em feat(scripts): add find-ci-errors.sh to diagnose widespread CI failures delegated merge-conflict CI merge conflict
35642 SnirBroshi feat(SimpleGraph/Walks/Operations): `p.dropLast.length` lemmas t-combinatorics awaiting review
35555 JovanGerb perf: add `AddMonoid` shortcut instance for linear maps merge-conflict merge conflict
35680 joelriou feat(CategoryTheory/Sites): alternative constructor for points WIP t-category-theory labelled WIP
31046 Thmoas-Guan feat(Homology) : compatibility of map between `Ext` t-category-theory awaiting review
31644 Thmoas-Guan feat(Algebra): projective dimension of quotient regular sequence blocked-by-other-PR awaiting-author t-ring-theory blocked on another PR
35150 JovanGerb chore(Order/OrderDual): move material on `OrderDual` t-order large-import awaiting review
29776 yuanyi-350 chore: refactor `ContinuousLinearMap.isOpenMap` by separating it into sublemmas WIP t-analysis labelled WIP
35631 SnirBroshi feat(SimpleGraph/Walks/Operations): `p.dropLast.support` lemmas t-combinatorics awaiting review
33864 Timeroot feat(Computability/Primrec): Proving several Nat arithmetic functions are primrec t-computability large-import failing CI
35494 Timeroot feat(Topology/Perfect): simp frontier_singleton awaiting-author t-topology awaiting author
35493 xroblot feat(RamificationInertia): add `ramificationIdx_algebra_tower'` t-number-theory awaiting review
34848 bjornsolheim feat(Analysis/Convex/Cone): min and max tensor products are equal when one factor is simplicial and generating awaiting-author t-analysis awaiting author
34867 urkud feat(FDeriv/Comp): migrate to TVS awaiting-author t-analysis awaiting author
34419 ster-oc feat(RCLike): add `Continuous.re` and similar awaiting-author t-analysis new-contributor awaiting author
35664 Rida-Hamadani feat(SimpleGraph): the adjacency matrix of empty and complete graphs t-combinatorics awaiting review
26479 thefundamentaltheor3m feat(Analysis/Complex/CauchyIntegral): Cauchy–Goursat for Unbounded Rectangles awaiting-author t-analysis new-contributor sphere-packing awaiting author
35582 nielsvoss feat(Analysis/InnerProductSpace): add theorems about the adjoint, kernel, range, and orthogonal complement awaiting-author t-analysis new-contributor awaiting author
33501 SnirBroshi feat(Combinatorics/SimpleGraph/Finite): degrees for infinite graphs awaiting-author t-combinatorics large-import awaiting author
34734 FLDutchmann refactor(Tactic): change `ring` to allow for coefficients in a variable type delegated merge-conflict t-meta failing CI
34759 Hagb feat(RingTheory/MvPolynomial/MonomialOrder): add degree with `⊥` as degree of `0` blocked-by-other-PR merge-conflict t-ring-theory blocked on another PR
34805 DavidLedvinka feat(Tactic): generalize ofScientific NormNum extension to `DivisionSemiring` awaiting-author merge-conflict t-meta merge conflict
34854 GrigorenkoPV chore(Combinatorics/Enumerative/Catalan): split into `Basic` & `Tree` merge-conflict new-contributor merge conflict
35292 Rida-Hamadani feat(SimpleGraph): taking twice from a walk equals taking the minimum t-combinatorics awaiting review
35696 GrigorenkoPV fix(Data/Rel): change what `image_eq_cod_of_dom_subset` states new-contributor t-data awaiting review
28248 YaelDillies feat: binomial random variables t-measure-probability awaiting review
33985 YellPika feat(Order/OmegaCompletePartialOrder): `OmegaCompletePartialOrder` instance for `Sum` with basic `ωScottContinuous` lemmas t-order new-contributor large-import awaiting review
34697 wwylele feat(Geometry/Euclidean): the Euclidean volume measure t-euclidean-geometry t-measure-probability awaiting review
35042 JovanGerb chore: remove `meta` form `import Mathlib.Tactic...` large-import awaiting review
35273 grunweg chore: replace `continuity` -> `fun_prop` in remaining auto-parameters t-topology awaiting review
35481 FrankieeW chore(NumberTheory/Zsqrtd): inline duplicated order lemmas into instances t-number-theory new-contributor awaiting review
35565 felixpernegger feat(Topology): sequentially T2 spaces t-topology awaiting review
35590 chrisflav feat(Algebra): add `AlgHom.ulift` t-algebra awaiting review
35735 mkaratarakis feat(NumberTheory): analytical properties and lower bounds for Gelfond-Schneider auxiliary function blocked-by-other-PR t-number-theory new-contributor blocked on another PR
35744 mkaratarakis feat(NumberTheory): non-vanishing derivative and algebraic lower bound for Gelfond-Schneider blocked-by-other-PR t-number-theory blocked on another PR
35743 mkaratarakis feat(NumberTheory): non-vanishing derivative and norm lower bounds for Gelfond-Schneider blocked-by-other-PR t-number-theory blocked on another PR
35280 khwilson feat(Mathlib/Analysis/Polynomial/MahlerMeasure): Mahler Measure estimate in terms of supNorm t-analysis new-contributor awaiting review
35718 Parcly-Taxel chore: remove some `respectTransparency` options awaiting-author awaiting author
34728 j-loreaux feat: continuous linear equivalence between continuous `ℝ`- and `𝕜`-linear functionals, when equipped with the weak⋆-topology merge-conflict t-analysis failing CI
33364 BoltonBailey feat(Analysis/Convex/SimplicialComplex): add AbstractSimplicialComplex + constructions t-analysis maintainer-merge t-algebraic-topology awaiting review
34558 kim-em feat(Topology): add StrictMono finite partition lemmas and path partitioning awaiting-author t-topology awaiting author
29458 LiamSchilling feat(MvPolynomial/WeightedHomogenous): relate `weightedTotalDegree` to `degrees` and `degreeOf` awaiting-author new-contributor t-ring-theory awaiting author
35755 Vilin97 feat(Analysis/ODE): forward Euler method convergence WIP new-contributor ⚠️ labelled WIP
34364 YuvalFilmus feat(Chebyshev/RootsExtrema): bound iterated derivatives of Chebyshev T on [-1, 1] t-analysis awaiting review
35738 GrigorenkoPV perf: remove some `aesop`s and `grind`s awaiting-author new-contributor awaiting author
35296 Rida-Hamadani feat(SimpleGraph): taking or droping from a cycle results in a path blocked-by-other-PR merge-conflict t-combinatorics blocked on another PR
33466 Shreyas4991 refactor(Combinatorics/Digraph): add vertex sets awaiting-author please-adopt t-combinatorics looking for help
25834 Rida-Hamadani feat(SimpleGraph): girth-diameter inequality blocked-by-other-PR t-combinatorics blocked on another PR
21342 YaelDillies refactor(Normed/Group/Quotient): generalise to non-abelian groups t-analysis opened from a branch in the main mathlib repo (not a fork)
34871 zhuyizheng feat(Calculus): Taylor with integral remainder t-analysis large-import awaiting review
33662 Pjotr5 feat(Algebra/Order/BigOperators/Expect): add lemmas and strict variants t-algebra new-contributor awaiting review
30505 mariainesdff feat(NumberTheory/RatFunc/Ostrowski): prove Ostrowski's theorem for K(X) t-number-theory t-algebra awaiting review
35239 JohnnyTeutonic feat(Logic/Function): add Lawvere fixed-point theorem awaiting-author merge-conflict t-logic merge conflict
34154 euprunin chore: golf using `grind` (and add four supporting `grind` annotations) awaiting review
32282 jsm28 feat(Geometry/Euclidean/Angle/Incenter): unoriented angle bisection blocked-by-other-PR t-euclidean-geometry blocked on another PR
32295 jsm28 feat(Archive/Imo/Imo2024Q4): IMO 2024 Q4 blocked-by-other-PR IMO blocked on another PR
35287 arnoudvanderleer feat(AlgebraicTopology/SimplicialSet): define isomorphisms in simplicial sets, and the coherent isomorphism simplicial set awaiting-author new-contributor infinity-cosmos t-algebraic-topology awaiting author
33543 JovanGerb feat: use `to_dual` for `HeytingAlgebra` merge-conflict t-algebra failing CI
35740 LLaurance chore(SimpleGraph/Basic): clean up and shorten t-combinatorics awaiting review
34760 astrainfinita chore: use `RelHomClass` in `IsChain.image` t-order awaiting review
35402 samueloettl feat(Dynamics/BirkhoffSum): birkhoffAverage const t-dynamics new-contributor awaiting review
31595 astrainfinita chore: redefine `Ideal.IsPrime` t-algebra awaiting review
33329 mcdoll feat(Analysis): Fourier-based Sobolev spaces WIP blocked-by-other-PR t-analysis blocked on another PR
33443 sahanwijetunga feat: Define Isometries of Bilinear Spaces awaiting-author t-algebra new-contributor awaiting author
35530 xroblot feat(RingTheory): add the class `HasFiniteQuotients` t-ring-theory awaiting review
20238 maemre feat(Computability/DFA): Closure of regular languages under some set operations awaiting-author merge-conflict new-contributor t-computability awaiting-zulip opened from a branch in the main mathlib repo (not a fork)
22361 rudynicolop feat(Computability/NFA): nfa closure properties awaiting-author merge-conflict new-contributor t-computability awaiting-zulip opened from a branch in the main mathlib repo (not a fork)
26735 Raph-DG feat(AlgebraicGeometry): The codimension of a point of a scheme is equal to the krull dimension of the stalk t-algebraic-geometry awaiting review
33780 ooovi feat(Geometry/Convex/Cone): lineality space of pointed cones t-convex-geometry awaiting review
33479 zcyemi feat(Geometry/Euclidean/Sphere/Power): Add theorem about cospherical points on two intersecting lines delegated t-euclidean-geometry large-import delegated
32825 erdOne perf(RingTheory): `attribute [irreducible] KaehlerDifferential` awaiting-author t-ring-theory awaiting author
26304 Raph-DG feat(AlgebraicGeometry): Definition of algebraic cycles blocked-by-other-PR RFC t-algebraic-geometry blocked on another PR
35365 wwylele feat(LinearAlgebra/Simplex): closedInterior = interior + face.closedInterior t-algebra awaiting review
30872 rudynicolop feat(Computability/NFA): NFA closure under concatenation awaiting-author new-contributor t-computability failing CI
29354 themathqueen refactor(Algebra/Algebra/Equiv): allow for non-unital `AlgEquiv` awaiting-author t-algebra failing CI
33449 yuanyi-350 feat(ProbabilityTheory): Add Poisson limit theorem t-measure-probability maintainer-merge file-removed awaiting review
35821 SnirBroshi feat(Order/ConditionallyCompleteLattice): `sInf s ≤ sSup t` for `(s ∩ t).Nonempty` t-order awaiting review
34911 smmercuri feat: idelic product formula WIP blocked-by-other-PR merge-conflict ⚠️ blocked on another PR
35081 tb65536 feat(Topology/Algebra/Group/Extension): define short exact sequence of topological groups t-topology maintainer-merge awaiting review
35163 CoolRmal feat(Topology): comparison of two Hausdorff topologies awaiting-author t-topology awaiting author
35100 stepan2698-cpu feat: definition of a character of a representation t-algebra new-contributor awaiting review
35436 daniel-carranza feat(CategoryTheory/Monoidal/Closed): Prove the isomorphism of internal hom objects C(x \otimes y, z) and C(y, C(x, z)) delegated t-category-theory new-contributor infinity-cosmos delegated
30122 xroblot Development branch (1) WIP merge-conflict large-import labelled WIP
35041 b-mehta feat(Combinatorics): prove the Rado selection lemma t-combinatorics failing CI
35652 dennj feat(LinearAlgebra/Matrix): add `Matrix.mul_eq_smul_one_symm` t-algebra new-contributor awaiting review
35654 euprunin chore: golf using `grind` awaiting review
35662 FrankieeW feat(NumberTheory/Zsqrtd): add Archimedean instance via le_arch t-number-theory new-contributor awaiting review
35683 gasparattila fix(Tactic/FunProp): detect `Continuous.subtype_mk` as compositional t-meta awaiting review
34932 erdOne feat(AlgebraicGeometry): formally etale morphisms delegated merge-conflict t-algebraic-geometry merge conflict
35573 antisubnoous feat(NumberTheory/Chebyshev): express the Chebyshev theta function in terms of the prime counting function t-number-theory new-contributor awaiting review
34713 dennj feat(Probability/Markov): stationary distributions for stochastic matrices awaiting-author t-algebra new-contributor awaiting author
23929 meithecatte feat(Computability/NFA): improve bound on pumping lemma awaiting-author new-contributor t-computability awaiting-zulip opened from a branch in the main mathlib repo (not a fork)
35128 DAE123456 feat : Define anti_pascal awaiting-author t-algebra new-contributor awaiting author
34507 metakunt feat(NumberTheory/AKSPrimality): Adds the AKS primality test t-number-theory awaiting review
35713 Parcly-Taxel feat: Bird–Wadler duality theorems t-data awaiting review
35656 euprunin chore(ModelTheory): golf proofs t-logic awaiting review
35677 euprunin chore(SetTheory): golf proofs t-set-theory awaiting review
29534 Thmoas-Guan feat(Algebra): global dimension of regular local ring blocked-by-other-PR t-algebra large-import blocked on another PR
29232 vihdzp feat: more theorems on `SuccAddOrder` merge-conflict t-algebra t-order failing CI
29796 Thmoas-Guan feat(RingTheory): regular of finite global dimension blocked-by-other-PR large-import t-ring-theory blocked on another PR
32458 vihdzp feat: order isomorphisms preserve successor/predecessor limits awaiting-author merge-conflict t-order failing CI
35552 vihdzp chore(SetTheory/Ordinal/Basic): remove `backward.privateInPublic` tech debt t-set-theory awaiting review
35609 BoltonBailey chore: deprecate Turing files blocked-by-other-PR merge-conflict t-computability blocked on another PR
30758 Timeroot chore: tag abs_inv and abs_div with grind= t-algebra awaiting review
35446 kbuzzard perf: try lowering prio for A(0) instances, A a graded object delegated t-algebra delegated
35853 vihdzp chore(SetTheory/Ordinal): deprecate more theorems on `succ` t-set-theory awaiting review
35394 HugLycan feat(Tactic/Positivity): make positivity work for types that are not partial orders awaiting-author t-meta new-contributor awaiting author
35084 edegeltje feat(Combinatorics/SimpleGraph): The Cayley graph for structures with `Mul`/`Add` t-combinatorics awaiting review
35865 vihdzp chore: review `Cardinal.ord` API t-set-theory awaiting review
33458 NoneMore feat(ModelTheory): add lifting for embeddings to languages with constants t-logic new-contributor awaiting review
35435 WenrongZou feat(RingTheory/MvPowerSeries): toMvPowerSeries and rename t-ring-theory awaiting review
32672 tb65536 feat: haar measures on short exact sequences blocked-by-other-PR t-topology t-measure-probability FLT blocked on another PR
8102 miguelmarco feat(Tactic): add `unify_denoms` and `collect_signs` tactics good first issue modifies-tactic-syntax please-adopt merge-conflict t-meta new-contributor opened from a branch in the main mathlib repo (not a fork)
35603 2500223210-max feat(GroupTheory/Frattini): add more theorems awaiting-author new-contributor large-import t-group-theory failing CI
35868 Raph-DG feat(Topology): Added in a variant of the sheaf condition which assumes non triviality of the cover WIP t-topology labelled WIP
35415 joneugster feat(Cache): enable partial cache in downstream projects t-meta CI awaiting review
34676 joneugster chore(Algebra/CharP/MixedCharZero): update file to make use of the module system t-algebra failing CI
35193 Brian-Nugent feat(Topology/Closeds): implement category of closed sets in topological spaces awaiting-author t-topology new-contributor awaiting author
35684 spitters feat(CategoryTheory/MarkovCategory): Kleisli PMF is a Markov category awaiting-author t-category-theory new-contributor awaiting author
35465 MixedMatched feat(Data/Multiset/Powerset): show injectivity and monotonicity of powerset new-contributor t-data awaiting review
34583 adomani feat: basic properties of subnormal subgroups large-import t-group-theory awaiting review
35268 tb65536 feat(Topology/Algebra/Module/LinearMap): units in `M →L[R] M` are homeomorphisms t-topology t-algebra awaiting review
34209 mike1729 feat(Analysis/Normed): Schauder basis definition and characterization via projections t-analysis new-contributor awaiting review
35078 grunweg feat: immersed points awaiting-author t-differential-geometry awaiting author
34626 grunweg feat: analytification of schemes (affine case) WIP blocked-by-other-PR merge-conflict t-differential-geometry please-merge-master blocked on another PR
35653 pepamontero feat: add ChartedSpace structure on orbit space t-differential-geometry new-contributor awaiting review
35657 Rida-Hamadani feat(SimpleGraph): distance equal or greater than two in terms of common neighborhood awaiting-author t-combinatorics awaiting author
24434 joelriou feat(CategoryTheory): effectiveness of descent WIP blocked-by-other-PR merge-conflict t-category-theory opened from a branch in the main mathlib repo (not a fork)
35608 BoltonBailey chore(Computability): move TM files to a single folder t-computability file-removed awaiting review
35598 Paul-Lez feat(CategoryTheory/Abelian/Exact): add easy lemmas about short exactness awaiting-author t-category-theory awaiting author
33791 PhoenixIra feat: Generalization of FixedPointApproximants to CompletePartialOrder merge-conflict t-order new-contributor merge conflict
35630 SnirBroshi feat(Data/List/Basic): relate `dropLast` and `concat` t-data awaiting review
35669 SnirBroshi feat(Mathlib/Data/Finset/Mex): `sInf sᶜ ≤ s.encard` blocked-by-other-PR t-order blocked on another PR
35830 AntoineChambert-Loir feat(Data/Nat/Choose/Plurinomial): plurinomial coefficients t-data awaiting review
35857 AlexeyMilovanov feat(Logic.Equiv.BijectiveBase2): add bijective base-2 numeration t-logic new-contributor awaiting review
35776 IvanRenison feat(Combinatorics): define `HasAdj` for capturing the common structure of different kinds of (simple) graphs t-combinatorics awaiting review
35822 SnirBroshi feat(Order/ConditionallyCompleteLattice): `sSup (f '' s) ≤ f (sSup s)` t-order awaiting review
35423 Rob23oba feat: add congruence lemmas for `Function.update` and `Pi.single` t-algebra awaiting review
35217 kim-em feat: auxiliary lemmas for Artin and braid groups awaiting-author t-group-theory awaiting author
35762 xroblot feat(CyclotomicFields/Galois): compute the image of the stabilizer of an unramified prime ideal in `(ℤ/nℤ)ˣ` blocked-by-other-PR t-algebra large-import blocked on another PR
35031 JovanGerb feat(CategoryTheory/Limits/Cones): use `to_dual` blocked-by-other-PR merge-conflict t-category-theory blocked on another PR
35431 CoolRmal feat: Conditional Jensen's Inequality for a general measure blocked-by-other-PR t-measure-probability blocked on another PR
35033 homeowmorphism feat: a group if finitely generated if and only if there exists a surjective homomorphism from a `FreeGroup` on an arbitrary finite type `α` to the group blocked-by-other-PR merge-conflict new-contributor t-group-theory blocked on another PR
35218 kim-em feat(GroupTheory/Coxeter/Perm): type A Coxeter group maps to symmetric group blocked-by-other-PR t-group-theory blocked on another PR
35219 kim-em feat(GroupTheory/Artin): define Artin groups and their universal property blocked-by-other-PR t-group-theory blocked on another PR
35649 JovanGerb feat(Order/GaloisConnection/Defs): use `to_dual` for `GaloisInsertion`/`GaloisCoinsertion` t-order failing CI
35605 j-loreaux feat: transfer instances of `ContinuousFunctionalCalculus` to type synonyms with weaker topologies merge-conflict t-analysis failing CI
35802 xroblot feat(RamificationInertia): splitting in the decomposition field blocked-by-other-PR merge-conflict t-number-theory ❌? blocked on another PR
35250 vlad902 feat(SimpleGraph): redefine `cycleGraph` independent of `circulantGraph` t-combinatorics awaiting review
35540 tb65536 feat(GroupTheory/ResiduallyFinite): define residually finite groups t-algebra t-group-theory awaiting review
35592 SnirBroshi chore(Order/Defs/Unbundled): deprecate `def Transitive` in favor of `class IsTrans` t-order awaiting review
35610 IvanRenison feat(Data/Fin): add several lemmas about subtraction of `Fin.{castLT, castAdd, castSucc, castPred}` t-data awaiting review
35672 dennj feat(RingTheory/Polynomial/Cyclotomic): vanishing sums and fiber equidistribution at primitive roots new-contributor t-ring-theory awaiting review
35720 tb65536 feat(NumberTheory/FunctionField): add instances on `FqtInfty` t-topology t-algebra awaiting review
35721 chrisflav chore: fix delaborators for `[Comm][Semi]RingCat` and some more t-algebra awaiting review
28682 Thmoas-Guan feat(RingTheory): definition of regular local ring blocked-by-other-PR t-ring-theory blocked on another PR
28684 Thmoas-Guan feat(RingTheory): definition of regular ring blocked-by-other-PR t-ring-theory blocked on another PR
29701 Thmoas-Guan feat(Algebra/RingTheory): polynomial over regular ring WIP blocked-by-other-PR t-ring-theory blocked on another PR
28683 Thmoas-Guan feat(RingTheory): regular local ring is domain blocked-by-other-PR t-ring-theory blocked on another PR
35628 SnirBroshi feat(Combinatorics/SimpleGraph/Maps): characterize `neighborSet` and `edgeSet` across an embedding t-combinatorics awaiting review
35878 Parcly-Taxel chore: use `induction` for `Quotient.induction` invocations tech debt awaiting review
35841 astrainfinita chore(Order/Defs/LinearOrder): avoid `grind` in very fundamental lemmas t-order awaiting review
26770 Jun2M feat(Combinatorics/Graph): subgraph relations on `Graph` t-combinatorics awaiting review
35880 astrainfinita feat(Order/Defs/LinearOrder): `min_ind` t-order awaiting review
34423 euprunin chore: golf using `grind` awaiting review
35840 SnirBroshi feat(SetTheory/Ordinal/Arithmetic): `typein (· < ·) = natCast` for `ℕ` and `Fin n` t-set-theory awaiting review
35881 astrainfinita chore: do not use `inf` `sup` in `LinearOrder` lemmas blocked-by-other-PR t-order blocked on another PR
35716 IvanRenison feat(Combinatorics/SimpleGraph/Connectivity): add lemmas about reachable, degree and neighbor set t-combinatorics awaiting review
35829 IvanRenison refactor(Data/Last): move `Mathlib.Tactic.BicategoryLike.pairs` to `List.consecutivePairs` t-data awaiting review
34922 vasnesterov feat(Tactic/ComputeAsymptotics/Multiseries): Multiseries definition and structural lemmas awaiting-author t-meta t-data awaiting author
35073 joelriou feat(CategoryTheory/Sites): more on Cech cohomology WIP merge-conflict t-category-theory labelled WIP
33878 xroblot feat(MulChar): generalize duality results on finite abelian groups to multiplicative characters t-number-theory large-import awaiting review
35405 xroblot feat(RamificationInertia): add `ramificationIdx_le_ramificationIdx` and `inertiaDeg_le_inertiaDeg` t-number-theory awaiting review
34440 grunweg feat: linter for name components in uppercase awaiting-author merge-conflict t-linter large-import merge conflict
34519 grunweg feat: environment linter for definitions containing an underscore awaiting-author merge-conflict CI t-linter large-import failing CI
35072 vasnesterov feat(Tactic/ComputeAsymptotics/Multiseries): non-primitive corecursion for `Seq`: `FriendlyOperation` API awaiting-author t-meta t-data awaiting author
35774 astrainfinita chore: use `IsLUB` `IsGLB` in `ConditionallyCompleteLattice` t-order awaiting review
34050 Julian feat(GraphTheory): Graham-Pollak theorem WIP awaiting-author t-combinatorics labelled WIP
35769 SnirBroshi feat(Order/WellFounded): the cardinality of a set is an upper-bound for the amount of elements before the set's mex t-order awaiting review
35798 xroblot feat(RamificationInertia): compute the degrees of the decomposition field and inertia field blocked-by-other-PR t-number-theory large-import blocked on another PR
35800 xroblot feat(RamificationInertia): decomposition fields and inertia fields are unique (up to isomorphism) blocked-by-other-PR merge-conflict t-number-theory blocked on another PR
34773 semaraugusto feat(InformationTheory): add Shannon entropy for probability mass functions awaiting-author new-contributor ⚠️ awaiting author
34963 Parcly-Taxel feat(Archive): proof of the Robbins conjecture t-algebra awaiting review
35826 quangvdao feat(Probability/ProbabilityMassFunction): total variation distance and MetricSpace instance t-measure-probability failing CI
33363 BoltonBailey feat: add `empty_eq_image` simp lemmas t-data awaiting review
34678 joneugster feat(scripts/autolabel): add dependencies for `t-ring-theory` CI awaiting review
34078 joneugster feat(scripts/autolabel): add label dependencies for better automatic label assignment blocked-by-other-PR CI blocked on another PR
35315 mkaratarakis feat: lemmas for the analytic part of the proof of the Gelfond–Schneider theorem (Part 3/5) t-analysis new-contributor awaiting review
35317 mkaratarakis feat: lemmas for the analytic part of the proof of the Gelfond–Schneider theorem (Part 5/5) t-number-theory t-analysis new-contributor awaiting review
34952 joneugster feat(scripts/autolabel): use `Cli` and integrate `curl` call into `autolabel` merge-conflict CI merge conflict
35439 harahu chore(RingTheory): fix indentation in markdown lists t-ring-theory awaiting review
35272 jvanwinden feat(Topology/Instances/EReal): limsup of multiplication by a constant t-topology new-contributor awaiting review
35892 vlad902 feat(Data): lemmas for `List.bagInter` t-data awaiting review
35376 michaellee94 feat(Geometry/Manifold): orientable manifolds WIP merge-conflict t-differential-geometry new-contributor labelled WIP
33406 dupuisf feat: add basics of majorization WIP awaiting-author t-analysis labelled WIP
33188 BryceT233 feat(RingTheory/MvPowerSeries): introduce rename new-contributor large-import t-ring-theory awaiting review
32374 adamtopaz feat(Tactic/WildcardUniverse): Foo.{*, _, v*, max u v} WIP awaiting-author t-meta labelled WIP
34246 staroperator feat(SetTheory/Cardinal): Δ-system lemma t-set-theory awaiting review
34621 homeowmorphism feat(GroupTheory/FreeGroup/Basic): deprecate `FreeGroup Empty ≃ Unit` using `Equiv.ofUnique`, add `Mul` suggestion using `MulEquiv.ofUnique` and add `FreeGroup α ≃* Multiplicative ℤ` new-contributor t-group-theory awaiting review
35528 euprunin chore: golf using `grind` awaiting review
35567 goliath-klein refactor(PiTensorProduct/{InjectiveNorm, ProjectiveNorm}): Golfs new-contributor maintainer-merge awaiting review
35745 khwilson feat(Mathlib/Analysis/Asymptotics/Defs): congr lemmas for IsBigO* t-analysis new-contributor awaiting review
35771 euprunin chore: golf using `exact` awaiting review
35763 kim-em chore(scripts): make rm_set_option cache opt-in via --resume opened from a branch in the main mathlib repo (not a fork)
33506 Rida-Hamadani feat(SimpleGraph): construct a cycle of two distinct paths with same start and end awaiting-author t-combinatorics awaiting author
35858 vihdzp doc(SetTheory/Ordinal/Arithmetic): improve documentation documentation t-set-theory awaiting review
35905 Jun2M feat(Combinatorics/Graph): Add definitions for small graphs (noEdge, bouquet, banana) t-combinatorics awaiting review
35907 JJYYY-JJY fix(Topology/Defs/Basic): preserve noncanonical topology instances in delaboration t-topology new-contributor awaiting review
35908 vihdzp chore(FieldTheory/AbelRuffini): simpler definition of `solvableByRad` t-algebra awaiting review
35665 BryceT233 feat(RingTheory/AdicCompletion): introduce AdicCompletion.finsuppSum new-contributor t-ring-theory awaiting review
35910 LLaurance chore(Probability): remove deprecated items, shorten proofs t-measure-probability awaiting review
35911 grunweg chore: generalise local extensions to any local frame WIP blocked-by-other-PR t-differential-geometry blocked on another PR
32033 Thmoas-Guan feat(Algebra): injective dimension equal supremum of localized module merge-conflict t-algebra large-import merge conflict
32035 Thmoas-Guan feat(RingTheory): localization of Gorenstein local ring blocked-by-other-PR merge-conflict large-import t-ring-theory blocked on another PR
30658 grunweg feat: extend the `whitespace` linter to proof bodies blocked-by-other-PR merge-conflict t-linter large-import blocked on another PR*
35912 WenrongZou feat(RingTheory/FormalGroup): definition and examples of formal group t-ring-theory awaiting review
35539 xgenereux feat(DedekindDomain/Factorization): add `iInf` version of `finprod_heightOneSpectrum_factorization` t-ring-theory awaiting review
34938 peabrainiac feat(Geometry/Manifold): interior and boundary are preserved by (local) diffeomorphisms t-differential-geometry awaiting review
35705 jdhart81 feat(Data/ENNReal, Probability/Independence): division decomposition and self-independence new-contributor t-data awaiting review
35734 mkaratarakis feat(NumberTheory): matrix bounds and Siegel's lemma application for Gelfond-Schneider blocked-by-other-PR t-number-theory new-contributor blocked on another PR
34477 spanning-tree refactor(Order): make CompletePartialOrder extend OrderBot t-order new-contributor awaiting review
35917 dependabot chore(deps): bump the actions-version-updates group across 1 directory with 7 updates CI dependencies github_actions opened from a branch in the main mathlib repo (not a fork)
33714 idontgetoutmuch feat(Mathlib/Geometry/Manifold): Riemannian metrics exist II t-differential-geometry new-contributor awaiting review
35879 Jun2M feat(Combinatorics/Graph): Add graph deletion operations blocked-by-other-PR t-combinatorics blocked on another PR
34875 banrovegrie feat(LinearAlgebra/Matrix): add Sherman-Morrison formula t-algebra new-contributor failing CI
35916 themathqueen feat(Analysis/CStarAlgebra): `IsIdempotentElem a ↔ spectrum R a ⊆ {0, 1}` t-analysis large-import awaiting review
35700 inaciovasquez2020 MeasureTheory: introduce supportDrift for probability measures t-measure-probability new-contributor failing CI
34649 peabrainiac feat(Analysis/Calculus/ContDiff): add notation `ℕ∞ω` for `WithTop ℕ∞` awaiting-author merge-conflict t-differential-geometry t-analysis awaiting-zulip awaiting a zulip discussion
34079 joneugster feat(scripts/autolabel): add dependencies for alg. geometry and diff. geometry awaiting-author CI awaiting author
29982 hrmacbeth feat: new `isolate` tactic t-meta large-import awaiting review
35834 homeowmorphism feat(Mathlib/GroupTheory/PresentedGroup): every group has a presentation new-contributor large-import t-group-theory awaiting review
35639 vihdzp chore(Order/SuccPred/Limit): use `to_dual` on everything that was missing maintainer-merge awaiting review
35944 euprunin chore: replace uses of `omega` with `lia` awaiting review
35325 SnirBroshi feat(SimpleGraph/Acyclic): `ENat.card V ≤ 2 → G.IsAcyclic` t-combinatorics awaiting review
29251 yoh-tanimoto feat(Analysis/InnerProductSpace/): define standard subspaces of a complex Hilbert space awaiting-author t-analysis awaiting author
35772 euprunin chore: golf using `grind` awaiting review
34554 SnirBroshi feat(Data/Nat/Factorization/Divisors): calculate divisors using prime factorization t-data awaiting review
35058 GrigorenkoPV chore: move tendsto_{floor,ceil}_at{Top,Bot} new-contributor large-import awaiting review
35189 euprunin chore: golf proofs awaiting review
35756 mariainesdff feat(Data/Nat/Choose/Multinomial): add lemmas t-combinatorics t-data opened from a branch in the main mathlib repo (not a fork)
35764 YaelDillies feat(Data/Finsupp): characterise when `Finsupp` is `Nontrivial` t-data awaiting review
35804 mariainesdff feat(RingTheory/DividedPowerAlgebra/Init): add universal divided power algebra t-ring-theory opened from a branch in the main mathlib repo (not a fork)
35807 Raph-DG chore(Topology): Generalised some of the instances for Function.locallyFinsuppWithin t-topology awaiting review
35818 Vierkantor chore(Tactic): rewrite `finiteness` tactic docstring documentation t-meta awaiting review
31891 jsm28 feat(Geometry/Euclidean/Sphere/OrthRadius): lemmas for setting up and using polars t-euclidean-geometry awaiting review
35884 Parcly-Taxel chore: fix induction and recursor names tech debt awaiting review
26013 tsuki8 feat(Data/Finset/Card,Data/Set/Finite/Basic): TODO needs a better title awaiting-author new-contributor t-data awaiting author
35954 mcdoll feat(Analysis/Fourier): the Fourier transform as bounded continuous function t-analysis awaiting review
34632 mitchell-horner feat(Combinatorics/SimpleGraph): add `BipartiteDoubleCover` t-combinatorics awaiting review
35069 A-M-Berns feat(Geometry/Polygon): simple polygons and boundary map t-euclidean-geometry new-contributor awaiting review
29624 mcdoll feat(LinearAlgebra/LinearPMap): add definition of resolvent and first resolvent identity awaiting-author t-analysis t-algebra failing CI
35243 ScottCarnahan chore(Algebra/MonoidAlgebra/PointwiseSMul): switch action from Finsupp to (Add)MonoidAlgebra and multiplicativize t-algebra large-import awaiting review
35851 vihdzp chore(SetTheory/Ordinal/Arithmetic): remove `backward.privateInPublic` tech debt t-set-theory awaiting review
35956 Scarlett-le feat: add orthogonality lemmas for inner product spacesonal t-analysis awaiting review
28685 mitchell-horner feat(Combinatorics/SimpleGraph): prove the minimal-degree version of the Erdős-Stone theorem t-combinatorics awaiting review
32987 kim-em feat: pipeline downloads and decompression in `cache get` t-meta maintainer-merge failing CI
34910 SnirBroshi feat(Combinatorics/SimpleGraph/Acyclic): a graph is a tree iff it's acyclic and has exactly `n - 1` edges blocked-by-other-PR t-combinatorics blocked on another PR
35947 euprunin chore: replace `aesop` with `grind` where the latter is significantly faster failing CI
35632 SnirBroshi feat(Data/List/TakeDrop): `take`/`drop` + `tail`/`dropLast` almost commute t-data awaiting review
35962 euprunin chore: golf using `simp` awaiting review
35960 vihdzp chore(Order/ConditionallyCompleteLattice/Basic): remove `backward.isDefEq.respectTransparency` easy t-order awaiting review
34758 Hagb feat(RingTheory/MvPolynomial/MonomialOrder): misc lemmas t-ring-theory awaiting review
35896 harahu chore(misc): fix typos awaiting review
35928 xgenereux feat(Subalgebra/Lattice): add notation for Algebra.adjoin t-algebra awaiting review
35805 adrianmartir feat(NumberTheory/Divisors): Add `infinite_setOf_divisors_iff` t-number-theory new-contributor awaiting review
35964 b-reinke feat(CategoryTheory/Linear): define category algebra WIP t-category-theory t-algebra labelled WIP
35966 joelriou feat(CategoryTheory/Abelian): the localization w.r.t. a Serre class is abelian t-category-theory large-import awaiting review
35442 dhyan-aranha feat: Affine line with doubled origin counter example awaiting-author t-algebraic-geometry new-contributor awaiting author
34444 joelriou feat(CategoryTheory): exact functors from the localization w.r.t. a Serre class WIP blocked-by-other-PR t-category-theory large-import blocked on another PR
35308 martinwintermath feat(Geometry/Convex/Cone): Add coercion from submodule to cone awaiting-author t-convex-geometry awaiting author
35874 xgenereux feat(Adjoin/Polynomial/Bivariate): IsAlgebraic.adjoin_singleton t-algebra awaiting review
35637 vihdzp chore(Topology/Order/LeftRight): use `to_dual` maintainer-merge awaiting review
34757 Hagb feat(Algebra/MvPolynomial/Rename): some lemmas about `rename` and `killCompl` t-algebra awaiting review
26942 pechersky feat(RingTheory/Valuation/ValueGroupIso): isomorphism of value groups when compatible blocked-by-other-PR merge-conflict t-order t-ring-theory blocked on another PR
34624 homeowmorphism feat(GroupTheory/FreeGroup/Basic): surjection between types induces surjection between free groups on those types new-contributor t-group-theory awaiting review
33958 chrisflav feat(AlgebraicGeometry): the small affine étale site WIP t-algebraic-geometry labelled WIP
33129 Paul-Lez feat(Tactic/Simproc/VecPerm): add simproc for permuting entries of a vector t-meta awaiting review
35808 xroblot feat(RamificationInertia): splitting in the inertia field blocked-by-other-PR t-algebra large-import blocked on another PR
34513 urkud feat(ContinuousAlternatingMap): generalize some definitions blocked-by-other-PR t-analysis blocked on another PR
35984 urkud feat(Topology/VectorBundle): add `simp` lemmas t-topology awaiting review
35597 BryceT233 feat(AdicTopology): add lemmas about adic topology t-topology new-contributor awaiting review
35707 BryceT233 feat(RingTheory/MvPowerSeries): introduce `truncTotal` new-contributor t-ring-theory awaiting review
35647 BryceT233 feat(RingTheory/Ideal/Quotient): add a canonical inclusion map new-contributor t-ring-theory awaiting review
35646 BryceT233 feat(Algebra): add two lemmas about submodule smul t-algebra new-contributor awaiting review
35987 grunweg chore(Tactic/FunProp): document that config options must come before … t-meta awaiting review
33790 eliasjudin feat(CategoryTheory/Preadditive/Mat): add natural transformation and isomorphism extension theorems awaiting-author t-category-theory new-contributor awaiting author
25737 robin-carlier feat(AlgebraicTopology/SimplexCategory/GeneratorsRelations/NormalForms): Normal forms for `P_δ`s delegated t-category-theory t-algebraic-topology failing CI
35594 chrisflav feat(RingTheory): `Extension.CotangentSpace` commutes with base change t-ring-theory awaiting review
25740 robin-carlier feat(AlgebraicTopology/SimplexCategory/GeneratorsRelations): `SimplexCategoryGenRel.toSimplexCategory` is an equivalence blocked-by-other-PR t-algebraic-topology blocked on another PR
35991 xroblot feat(RamificationInertia): various results about decomposition field and inertia field blocked-by-other-PR large-import ⚠️ blocked on another PR
32989 kim-em fix(Tactic/Simps): skip @[defeq] inference for non-exposed definitions awaiting-author merge-conflict t-meta failing CI
35963 Parcly-Taxel refactor: review Kleene algebra axioms t-algebra awaiting review
35974 justus-springer feat(Algebra/Polynomial/Bivariate): more API for swap t-algebra maintainer-merge awaiting review
15355 adomani feat: MiM PR report WIP ⚠️ opened from a branch in the main mathlib repo (not a fork)
34263 grunweg feat: mfderiv_smul blocked-by-other-PR t-differential-geometry blocked on another PR
22464 adomani feat(CI): declarations diff in Lean awaiting-author merge-conflict CI opened from a branch in the main mathlib repo (not a fork)
29909 Vierkantor feat(CI): add build output to CI workflows delegated merge-conflict CI merge conflict
35477 harahu chore(Geometry): fix markdown lists awaiting review
34727 ocfnash feat: the Geck construction yields a Lie algebra with the expected Cartan matrix WIP t-algebra large-import labelled WIP
35977 jessealama feat(Algebra/Homology): add dimension lemmas for homological complex differentials t-algebra 🟤 running CI
29186 winstonyin feat: IsIntegralCurve for solutions to ODEs t-differential-geometry t-analysis t-dynamics awaiting review
35110 bryangingechen ci: refactor maintainer_*.yml workflows to use new helper actions awaiting-author merge-conflict CI merge conflict
35113 bryangingechen ci: refactor commit_verification so it works on PRs from forks awaiting-author merge-conflict CI merge conflict
35349 RemyDegenne feat: data processing inequality for the Kullback-Leibler divergence WIP blocked-by-other-PR merge-conflict t-measure-probability large-import blocked on another PR
35412 joneugster feat(Tactic/Linter): add unicode linter for unicode variant-selectors merge-conflict t-linter failing CI
35602 JovanGerb feat: replace `IsWellFounded` with `WellFounded` merge-conflict t-data failing CI
35790 Brian-Nugent feat(CategoryTheory/Algebra): Flasque Sheaves have vanishing cohomology WIP blocked-by-other-PR merge-conflict new-contributor large-import ⚠️ blocked on another PR
35998 gasparattila feat: affine isomorphisms between spaces of affine maps t-algebra awaiting review
30357 grunweg chore: golf using custom elaborators awaiting-author merge-conflict t-differential-geometry merge conflict
36007 grunweg chore(Geometry/Manifold/Algebra): golf using custom elaborators t-differential-geometry awaiting review
36009 grunweg chore(Geometry/Manifold/MFDeriv/SpecificFunctions): golf using custom… t-differential-geometry awaiting review
36010 grunweg chore(Geometry/Manifold/MFDeriv): golf using custom elaborators t-differential-geometry 🟤 running CI
36011 grunweg chore(Geometry/Manifold/VectorBundle/MDifferentiable): golf using cus… t-differential-geometry awaiting review
35724 matthewjasper feat(RingTheory/DedekindDomain/AdicValuation): v-adic integers of `K` are a localization at v^c new-contributor FLT large-import t-ring-theory awaiting review
35291 mcdoll feat(Fourier): improved version of Riemann-Lebesgue WIP blocked-by-other-PR merge-conflict large-import ⚠️ blocked on another PR
34705 mpenciak feat(AlgebraicGeometry): Grassmannian functor t-ring-theory awaiting review
35513 vihdzp refactor: redefine `Order.cof` for a preorder t-order maintainer-merge t-set-theory awaiting review
36006 gasparattila feat(LinearAlgebra): dimension of `P →ᵃ[R] W` blocked-by-other-PR t-algebra large-import blocked on another PR
36014 euprunin chore: golf proofs awaiting review
35329 BryceT233 feat(Data/Finsupp): add computational lemmas for cons and single new-contributor t-data awaiting review
36015 mcdoll chore(Analysis/SchwartzMap): unify style for `mkCLM` uses t-analysis awaiting review
35953 mcdoll feat(Analysis/SchwartzMap): estimates for `Lp` and `BCF` norms t-analysis ??? missing CI information
33935 mckoen feat(CategoryTheory/Monoidal/Arrow): define monoidal structure on arrow category t-category-theory awaiting review
34491 urkud feat(ContinuousMultilinearMap): generalize some definitions delegated t-analysis delegated
25906 pfaffelh feat(Topology/Compactness/CompactSystem): closed and compact square cylinders form a compact system merge-conflict t-topology merge conflict
35900 matthewjasper chore: Fix non-defeq diamonds on OrderDual merge-conflict t-order new-contributor merge conflict
34906 seewoo5 feat(NumberTheory/Bernoulli): von Staudt-Clausen theorem t-number-theory large-import awaiting review
35328 astrainfinita chore: use `IsLUB` `IsGLB` in `CompleteLattice` t-order awaiting review
35401 joelriou feat(CategoryTheory/Sites): the equivalence between `DescentData'` and `DescentData` t-category-theory awaiting review
35607 gasparattila fix(Tactic): make `eta_expand` idempotent t-meta awaiting review
35661 chrisflav feat(Geometry/Manifold): a smooth map induces a morphism of locally ringed spaces t-differential-geometry t-algebraic-geometry awaiting review
35693 euprunin chore: avoid passing explicit lemmas to `grind` and (terminal) `simp_all` where unnecessary awaiting review
35702 plp127 feat: uniqueness of partial fraction decomposition t-algebra awaiting review
35731 euprunin chore: golf using `exact`/`simpa` awaiting review
35732 TJHeeringa feat: Added reproducing kernels t-analysis new-contributor awaiting review
35760 astrainfinita chore: deprecate `ConditionallyCompleteLinearOrderedField` t-algebra t-order awaiting review
26394 winstonyin feat: existence of local flows on manifolds WIP merge-conflict t-differential-geometry labelled WIP
35775 IvanRenison feat(Data/List): add theorem `length_eq_two'` t-data awaiting review
35786 DavidLedvinka feat(Order): Add simp lemma for `IsRelUpperSet` and `IsRelLowerSet` t-order awaiting review
35820 smmercuri feat: unit lemmas and embedding for `FiniteAdeleRing` t-ring-theory awaiting review
35828 AntoineChambert-Loir feat(RingTheory/GradedAlgebra/Homogeneous/Hom): homogeneous algebra maps and evaluation t-ring-theory awaiting review
35842 WenrongZou feat(MvPowerSeries): subst_C and omit some finiteness of index set t-ring-theory awaiting review
35866 gad-wiseman feat(Topology/Homotopy/Basic): maps homotopic rel S agree on S t-topology new-contributor awaiting review
35584 joelriou feat(CategoryTheory/Sites): the monoidal category structure on sheaves using fiber functors WIP blocked-by-other-PR t-category-theory blocked on another PR
34863 JovanGerb feat(to_dual): support recursively reordering arguments t-meta awaiting review
35939 joelriou feat(Algebra/Homology): a homology exact sequence for triangles of cochain complexes t-category-theory awaiting review
36019 stepan2698-cpu chore: update undergrad.yaml awaiting review
35286 urkud chore: reduce defeq abuse awaiting review
26464 joelriou feat(LinearAlgebra): generators of pi tensor products awaiting-author merge-conflict t-algebra file-removed failing CI
29699 Thmoas-Guan feat(Algebra/RingTheory): global dimension of regular ring blocked-by-other-PR merge-conflict t-algebra large-import blocked on another PR
29703 Thmoas-Guan feat(Algebra/RingTheory): Hilbert's Syzygy theorem (projective version) blocked-by-other-PR merge-conflict large-import t-ring-theory blocked on another PR
29802 Thmoas-Guan feat(Algebra/RingTheory): Auslander–Buchsbaum–Serre criterion and its corollaries blocked-by-other-PR merge-conflict large-import t-ring-theory blocked on another PR
35467 ZRTMRH feat(Combinatorics): add Schreier graphs, Cayley graphs, and Cayley sum graphs t-combinatorics new-contributor awaiting review
35733 mkaratarakis feat: Algebraic setup and matrix coefficients for Gelfond-Schneider theorem t-number-theory new-contributor awaiting review
34588 Ruben-VandeVelde feat: add generalizations of some padicVal{Nat,Int} lemmas awaiting-author merge-conflict t-number-theory merge conflict
35198 j-loreaux feat: generalize Hölder's inequality for sums to `Real.HolderTriple` merge-conflict t-analysis merge conflict
35569 goliath-klein refactor(PiTensorProduct/{InjectiveNorm, ProjectiveNorm}): deprecate `injectiveSeminorm` blocked-by-other-PR new-contributor blocked on another PR
35781 mcdoll feat(Analysis/SchwartzMap): translation of arguments t-analysis awaiting review
35791 kim-em chore: make mk_all always use module format opened from a branch in the main mathlib repo (not a fork)
26395 winstonyin feat: $C^1$ vector fields on compact manifolds define global flows WIP blocked-by-other-PR merge-conflict t-differential-geometry blocked on another PR
34288 winstonyin feat: Integral curve is smooth in initial condition blocked-by-other-PR t-analysis blocked on another PR
33650 vihdzp refactor: deprecate bespoke `Hyperreal` machinery ready-to-merge t-algebra awaiting bors
25822 ScottCarnahan WIP: experiments with vertex algebras WIP merge-conflict large-import labelled WIP
26377 Whysoserioushah feat(RingTheory/SimpleRing/TensorProduct): tensor product of a simple algebra and a central simple algebra is simple merge-conflict large-import t-ring-theory merge conflict
34402 loefflerd feat(Analysis/Complex/UpperHalfPlane): invariant measure t-analysis large-import awaiting review
28286 bwangpj feat(Geometry/Manifold/ContMDiff): basic lemmas for analytic (`C^ω`) functions awaiting-author t-differential-geometry new-contributor awaiting author
35812 khwilson feat(MeasureTheory/Group/GeometryOfNumbers): successive minima and existence of a directional basis t-measure-probability new-contributor awaiting review
33355 0xTerencePrime feat(Combinatorics/SimpleGraph/Connectivity): define vertex connectivity t-combinatorics new-contributor awaiting review
35997 themathqueen feat(Analysis/CStarAlgebra/CFC/Order): conjugating with a star projection in a C*-algebra t-analysis awaiting review
35943 SnirBroshi feat(Analysis/Complex/Trigonometric): `cos(2x) = 1 - 2 * sin(x)^2` t-analysis awaiting review
35961 joelriou feat(CategoryTheory/Sites): fiber functors invert morphisms which become isomorphisms after sheafification t-category-theory awaiting review
35976 Phelixh feat: add add Liu's uncertainty theory foundations (core/distribution/process modules) new-contributor 🟤 ⚠️ running CI
30750 SnirBroshi feat(Data/Quot): `toSet` and `equivClassOf` awaiting-author awaiting-zulip t-data awaiting a zulip discussion
34711 urkud refactor(padicValNat): redefine using `maxPowDvdDiv` merge-conflict merge conflict
33375 kex-y feat(Probability): Local and stable properties blocked-by-other-PR merge-conflict t-measure-probability brownian blocked on another PR
33683 joelriou feat(AlgebraicTopology/SimplicialSet): the simplicial homotopy induced by an homotopy WIP blocked-by-other-PR t-algebraic-topology blocked on another PR
34040 Ruben-VandeVelde feat: generalize HasCompl.compl image/preimage lemmas to Involutive awaiting-author t-data awaiting author
35576 Tehlikeli107 ⚡ [performance] Pre-compile regexes in lake-build-wrapper.py awaiting-author merge-conflict CI new-contributor file-removed failing CI
36012 grunweg chore(Geometry/Manifold/VectorField/Pullback): golf using custom elab… t-differential-geometry awaiting review
36008 grunweg chore(Geometry/Manifold/ContMDiffMFDeriv): golf using custom elaborators t-differential-geometry awaiting review
35986 grunweg feat: tag ContDiff.{continuous,differentiable} as fun_prop t-analysis awaiting review
33372 kex-y feat(Probability): Countable infimum of stopping times is a stopping time t-measure-probability brownian awaiting review
26160 oliver-butterley feat(MeasureTheory.VectorMeasure): add several lemmas which characterize variation t-measure-probability new-contributor awaiting review
34622 vihdzp feat: Nat/Int casts on char two rings t-algebra awaiting review
35979 xgenereux chore(RatFunc/AsPolynomial): use Valuation.IsTrivialOn and simplify proofs awaiting review
35933 urkud chore(WellFounded): drop unneeded `Set.Nonempty` assumptions awaiting review
36001 harahu fix(docs): deduplicate yaml key easy awaiting review
36041 SproutSeeds feat(SimpleGraph/Matching): add maximal and maximum matching defs t-combinatorics new-contributor awaiting review
33668 Citronhat feat(PMF): add lintegral formulas for PMF awaiting-author t-measure-probability new-contributor awaiting author
36042 SproutSeeds feat(SimpleGraph/VertexCover): add minimal/minimum cover defs t-combinatorics new-contributor awaiting review
35709 tb65536 feat(AlgebraicGeometry/EllipticCurve/Reduction): define multiplicative and additive reduction t-number-theory t-algebraic-geometry t-algebra awaiting review
35710 tb65536 feat(AlgebraicGeometry/EllipticCurve/Reduction): define split multiplicative reduction blocked-by-other-PR t-number-theory t-algebraic-geometry t-algebra blocked on another PR
33082 AntoineChambert-Loir feat(GroupTheory/SpecificGroups/Alternating/Simple): the alternating group on at least 5 letters is simple. t-group-theory awaiting review
36040 grunweg feat: better error message in T% elaborator t-meta t-differential-geometry awaiting review
36022 SproutSeeds feat(SimpleGraph): redefine `IsBridge` via `deleteEdges` t-combinatorics new-contributor awaiting review
35370 joelriou feat(CategoryTheory/Triangulated/TStructure): the spectral object WIP blocked-by-other-PR merge-conflict t-category-theory large-import blocked on another PR
35369 joelriou feat(CategoryTheory/Triangulated/TStructure): properties of truncations indexed by `EInt` that use the octahedron axiom WIP blocked-by-other-PR merge-conflict t-category-theory large-import blocked on another PR
36048 kim-em feat(Tactic/DefEqAbuse): disambiguate identical-sides isDefEq failures t-meta opened from a branch in the main mathlib repo (not a fork)
36023 SproutSeeds feat(SimpleGraph): add maximal clique/indep-set defs and use MaximalFor t-combinatorics new-contributor awaiting review
36024 euprunin chore: golf proofs failing CI
34435 huaizhangchu feat(Probability): convolution of Poisson distributions blocked-by-other-PR t-measure-probability new-contributor large-import blocked on another PR
35298 robin-carlier chore: make `SimplicialObject` and `SSet` abbrevs awaiting-author t-algebraic-topology awaiting author
35368 joelriou feat(CategoryTheory/Triangulated/TStructure): extensions of truncations to the extended integers t-category-theory awaiting review
36050 SproutSeeds feat(Combinatorics/SimpleGraph/Connectivity): add edge reachability and connectivity numbers t-combinatorics new-contributor 🟤 running CI
33461 loefflerd feat(NumberTheory/Modular): stabilizers for action on upper halfplane WIP large-import ⚠️ labelled WIP
35643 chrisflav chore(Algebra): make `TensorProduct.equivOfCompatibleSMul` more linear t-algebra awaiting review
36051 euprunin chore: golf using `grind` awaiting review
32583 MJ141592 refactor(SimpleGraph): change bridges not to require the edge to be present awaiting-author t-combinatorics new-contributor failing CI
25848 joelriou feat/refactor: redefinition of homology + derived categories WIP merge-conflict t-category-theory t-topology large-import labelled WIP
27229 WilliamCoram feat(GroupTheory/DoubleCoset): multiple lemmas new-contributor FLT t-group-theory awaiting review
36053 SproutSeeds feat(SimpleGraph/Matching): add graph-level IsMatching predicate t-combinatorics new-contributor awaiting review
36056 SproutSeeds chore: rename ordered-cancel add monoid counterexample file new-contributor file-removed awaiting review
36062 huaizhangchu feat(Probability/PMF): add PMF.integrable_of_summable_norm t-measure-probability new-contributor awaiting review
35175 joelriou feat(CategoryTheory/Sites): characterization of conservative families of points t-category-theory awaiting review
35048 b-mehta feat(Analysis/Normed/Operator): prove the Fredholm alternative merge-conflict t-analysis merge conflict
35201 joelriou feat(CategoryTheory/Sites): points of presheaf toposes WIP blocked-by-other-PR t-category-theory blocked on another PR
35757 joelriou feat(Topology/Sheaves): points of the site of a topological space and specializations WIP blocked-by-other-PR merge-conflict t-category-theory blocked on another PR
24383 YaelDillies feat: distributive Haar characters of `ℝ` and `ℂ` WIP awaiting-CI t-measure-probability FLT file-removed opened from a branch in the main mathlib repo (not a fork)
24373 YaelDillies refactor: golf `modularCharacter` merge-conflict awaiting-CI t-measure-probability opened from a branch in the main mathlib repo (not a fork)
34015 erdOne feat(AlgebraicGeometry): category of schemes affine over a base awaiting-author t-algebraic-geometry awaiting author
29550 Raph-DG feat(RingTheory): Order of vanishing in a discrete valuation ring file-removed t-ring-theory awaiting review
25273 YaelDillies refactor: make `MonoidAlgebra` into a one-field structure WIP t-algebra large-import opened from a branch in the main mathlib repo (not a fork)
35585 farmanb feat(CategoryTheory/Abelian/Preradical): add Stenström's colon construction for preradicals awaiting-author t-category-theory new-contributor awaiting author
26231 chrisflav feat(CategoryTheory/Sites): sheaf condition and coproducts t-category-theory awaiting review
36067 smmercuri feat(NumberTheory/NumberField/FinitePlaces): `Module.Finite (v.adicCompletion K) (w.adicCompletion L)` ⚠️ awaiting review
35089 RemyDegenne feat: Radon-Nikodym derivative of a map is a conditional expectation awaiting-author t-measure-probability awaiting author
36063 SproutSeeds feat(SimpleGraph/Connectivity): add vertex reachability and connectivity numbers t-combinatorics new-contributor awaiting review
35813 joelriou feat(Algebra/Homology): a factorization lemma WIP blocked-by-other-PR t-category-theory blocked on another PR
35374 joelriou feat(Algebra/Homology/SpectralObject): `HasSpectralSequence` t-category-theory awaiting review
31135 kckennylau feat(RingTheory): is localization iff is localization on saturation merge-conflict t-ring-theory merge conflict
30399 kckennylau feat(RingTheory): make HomogeneousLocalization.map take a graded ring hom merge-conflict t-ring-theory failing CI
30379 kckennylau feat(RingTheory): isomorphism of graded rings blocked-by-other-PR merge-conflict t-ring-theory blocked on another PR
30365 kckennylau feat(RingTheory): define R-linear graded algebra homomorphism merge-conflict t-ring-theory merge conflict
30334 kckennylau feat(RingTheory): define maps of homogeneous ideals merge-conflict t-ring-theory merge conflict
26061 kckennylau (WIP) feat(AlgebraicGeometry): define Projective Space WIP blocked-by-other-PR merge-conflict t-algebraic-geometry blocked on another PR
35586 farmanb feat(CategoryTheory/Abelian/Preradical): introduce and characterize radicals blocked-by-other-PR t-category-theory new-contributor blocked on another PR
35970 adrianmartir feat(CategoryTheory/Profunctor): Add profunctors and a basic API for them t-category-theory new-contributor awaiting review
36060 edegeltje chore(CategoryTheory/Classifier): namespace Classifier, rename HasClassifier, move file t-category-theory file-removed awaiting review
30367 kckennylau feat(Data): define grading-preserving isomorphisms t-data failing CI
36075 edegeltje chore(CategoryTheory): Deprecate `CategoryTheory/Topos/Classifier.lean` module 🟤 running CI
36072 erdOne feat(AlgebraicGeometry): essential smallness of affine schemes locally of finite type over a base 🟤 ⚠️ opened from a branch in the main mathlib repo (not a fork)
32245 erdOne feat(RingTheory): the `coassoc_simps` simp set t-meta maintainer-merge toric t-ring-theory awaiting review
27274 peabrainiac feat(Geometry/Diffeology): continuous diffeologies & D-topology-lemmas merge-conflict t-differential-geometry merge conflict
35532 mariainesdff feat(Ringtheory/DedekindDomain): add RingEquiv lemmas t-ring-theory opened from a branch in the main mathlib repo (not a fork)
35989 chrisflav feat(RingTheory): define finite split algebras t-ring-theory 🟤 running CI
34784 tb65536 refactor(GroupTheory/Commutator/Basic): to_additivize commutators t-algebra t-group-theory failing CI
36082 chrisflav feat(CategoryTheory/Sites): being subcanonical is reflected by full faithful continuous functors t-category-theory failing CI
35331 SnirBroshi feat(SimpleGraph/Subgraph): small things about `spanningCoe` and a small golf t-combinatorics maintainer-merge awaiting review
33895 jessealama feat(Computability/Primrec): add list_take, list_drop, list_modify, and list_set new-contributor t-computability awaiting review
35778 kebekus feat: improve the mean value property of harmonic functions t-analysis awaiting review
35946 loefflerd feat(NumberTheory/Modular): interior and closure of fundamental domain ⚠️ awaiting review
32305 faenuccio feat: define Sobolev Spaces WIP blocked-by-other-PR merge-conflict t-analysis large-import opened from a branch in the main mathlib repo (not a fork)
33942 artie2000 feat(Algebra/Group/Submonoid): submonoid support awaiting-author t-algebra awaiting author
34031 lua-vr feat(Dynamics/BirkhoffSum): add the maximal ergodic theorem blocked-by-other-PR t-dynamics blocked on another PR
34120 winstonyin feat: `GroupWithZero` versions of `le` lemmas WIP large-import ⚠️ labelled WIP
34917 chrisflav feat(AlgebraicGeometry/Sites): characterization of sheaves for the `P`-qc topology WIP blocked-by-other-PR merge-conflict t-algebraic-geometry blocked on another PR
35375 joelriou feat(Algebra/Homology/SpectralObject): first quadrant spectral objects WIP blocked-by-other-PR merge-conflict t-category-theory blocked on another PR
35538 bilichboris feat(Analysis/VonNeumannAlgebra): double commutant theorem awaiting-author merge-conflict t-analysis new-contributor merge conflict
36030 joelriou feat(Algebra/Homology): more API for `SpectralObject.E` blocked-by-other-PR t-category-theory t-algebra blocked on another PR
36032 joelriou feat(Algebra/Homology/SpectralObject): differentials on pages blocked-by-other-PR merge-conflict t-category-theory t-algebra blocked on another PR
36078 tb65536 feat(LinearAlgebra/Eigenspace/ContinuousLinearMap): eigenspaces of a continuous linear map are closed t-topology t-algebra awaiting review
36088 pevogam feat: add a LE version of previous div_lt_div_iff_mul_lt_mul theorem t-algebra new-contributor 🟤 running CI
35904 chrisflav feat(CategoryTheory/Sites): the maximal `1`-hypercover containing a `0`-hypercover t-category-theory awaiting review
36083 gasparattila feat: decomposition of `ContinuousAffineMap` as an `Equiv` 🟤 ⚠️ running CI
35213 kim-em chore: use @[to_dual] in ConditionallyCompleteLattice blocked-by-other-PR blocked on another PR
35210 kim-em chore: use @[to_dual] in CompleteLattice extras and Set.Lattice blocked-by-other-PR blocked on another PR
35518 kim-em chore: forbid prime (') in filenames, rename LinearCombination' file-removed opened from a branch in the main mathlib repo (not a fork)
36093 tb65536 feat(GroupTheory/Nilpotent): remove `[IsNilpotent]` assumption from some theorems t-algebra t-group-theory awaiting review
35593 chrisflav feat(RingTheory/Extension): naive cotangent complex commutes with flat base change blocked-by-other-PR t-ring-theory blocked on another PR
35209 kim-em chore: use @[to_dual] extensively in CompleteLattice awaiting-author merge-conflict merge conflict
35214 kim-em chore: use @[to_dual] in GaloisConnection and Interval.Set.Disjoint blocked-by-other-PR blocked on another PR
35753 Vilin97 feat(Topology/Algebra/Order): regular grid helpers and piecewise linear interpolation t-topology new-contributor awaiting review
36097 matthewjasper chore: make psuedoparents of algebraic substructures reducible 🟤 running CI
36059 joelriou feat(CategoryTheory/Functor): exactness properties of conservative families of exact functors t-category-theory 🟤 running CI
36095 kim-em chore: remove stray comment about backward.isDefEq.respectTransparency opened from a branch in the main mathlib repo (not a fork)
35950 kim-em feat(Tactic): add inferInstanceAs% to fix type leakage ⚠️ opened from a branch in the main mathlib repo (not a fork)
32942 kim-em feat(CategoryTheory/Monoidal/Rigid): tensor product of exact pairings awaiting-author t-category-theory awaiting author
35323 martinwintermath feat(Geometry/Convex/Cone): Add lemmas for PointedCone.dual t-convex-geometry awaiting review
35429 CoolRmal feat: a convex, lower-semicontinuous, and positively homogeneous function is the supremum of a family of linear functions t-analysis awaiting review
35871 edegeltje feat(CategoryTheory/Limits): `IsPullback.mono_fst_of_mono` and similar t-category-theory awaiting review
35882 Thmoas-Guan feat(Algebra/ModuleCat): API on short complex in ModuleCat t-algebra awaiting review
35906 scp020 feat(Combinatorics/SimpleGraph/Walks): add Walk.IsChord and Walk.IsChordless t-combinatorics new-contributor awaiting review
36091 JJYYY-JJY feat(Analysis.LocallyConvex.Separation): add Eidelheit's separation theorem t-analysis new-contributor awaiting review
35957 Scarlett-le feat: add dist_center_midpoint_lt_radius for spheres t-euclidean-geometry 🟤 running CI
36020 SproutSeeds feat(Combinatorics/Enumerative/DoubleCounting): add weighted bipartite lower bound t-combinatorics new-contributor awaiting review
36099 SnirBroshi feat(Combinatorics/SimpleGraph/Sum): `edgeSet` equivalence blocked-by-other-PR t-combinatorics blocked on another PR
33831 vihdzp refactor(RingTheory/Polynomial/SmallDegreeVieta): convert to {p : R[X]} (hp : p.natDegree = 2) awaiting-author merge-conflict t-ring-theory merge conflict
36064 marcelolynch ci: Push to the cache using OIDC and federated credentials merge-conflict CI merge conflict
36101 wwylele feat(RingTheory): lemmas about power of maximal ideal t-ring-theory awaiting review
35951 parabamoghv feat(CategoryTheory/Monoidal): evaluation coevaluation isomorphisms t-category-theory new-contributor awaiting review
35627 SnirBroshi feat(Combinatorics/SimpleGraph/Finite): min/max degrees of top/bot t-combinatorics awaiting review
26212 Thmoas-Guan feat(Algebra): the Rees theorem for depth large-import t-ring-theory awaiting review
26803 bjoernkjoshanssen feat: second partial derivatives test awaiting-author t-analysis awaiting author
26214 Thmoas-Guan feat(Algebra): definition of depth blocked-by-other-PR t-algebra large-import blocked on another PR
26216 Thmoas-Guan feat(Algebra): depth of QuotSMulTop blocked-by-other-PR t-algebra large-import blocked on another PR
26215 Thmoas-Guan feat(Algebra): Auslander–Buchsbaum theorem blocked-by-other-PR t-algebra large-import blocked on another PR
34026 SnkXyx feat(Algebra/MvPolynomial): add mainVariable t-algebra new-contributor awaiting review
26217 Thmoas-Guan feat(Algebra): Ischebeck theorem blocked-by-other-PR t-algebra large-import blocked on another PR
35559 mike1729 feat(Analysis/Normed): weak-topology embedding into weak-star bidual and compactenss transfer theorem t-analysis new-contributor awaiting review
36103 SnkXyx feat(Algebra/MvPolynomial/CharacteristicSet): add Characteristic Set t-algebra new-contributor failing CI
35785 Brian-Nugent feat(CategoryTheory/Topology): Add Flasque Sheaves merge-conflict t-category-theory new-contributor merge conflict
36104 LarsenClose feat(CategoryTheory/Endofunctor/Algebra): add Adámek's initial algebra theorem t-category-theory new-contributor failing CI
36017 SproutSeeds feat(Algebra/Order/BigOperators/Group/Finset): add sum_mul_le_sum_sum_filter_of_le_card_filter t-algebra new-contributor awaiting review
36055 SproutSeeds chore: rename rpow monotonicity lemmas t-analysis new-contributor 🟤 running CI
33348 AntoineChambert-Loir feat(LinearAlgebra/Transvection): characterization of transvections among dilatransvections t-algebra awaiting review
36106 nielsvoss chore(Analysis/InnerProductSpace): remove a hypothesis from LinearMap.IsSymmetric.card_filter_eigenvalues_eq t-analysis awaiting review
35215 kim-em chore: use @[to_dual] in FixedPoints awaiting review
36105 LLaurance chore(Algebra): shorten, style t-algebra awaiting review
35945 euprunin chore: replace uses of `aesop` with `simp` awaiting review
35533 mariainesdff feat(RingTheory/DedekindDomain/Ideal/Lemmas): add nontrivial_heightOneSpectrum t-ring-theory opened from a branch in the main mathlib repo (not a fork)
35886 euprunin chore: exhaustively replace `measurability`/`continuity` → `fun_prop`, `simp_all` → `simp` where possible awaiting review
34742 Brian-Nugent feat(SheafCohomology): add API for Sheaf Cohomology t-category-theory new-contributor large-import awaiting review
36031 sgouezel feat: linter to make sure defs are `implicit_reducible` if they output classes ⚠️ failing CI
32334 EtienneC30 feat: independence of Gaussian processes t-measure-probability brownian awaiting review
34841 RemyDegenne feat(InformationTheory): chain rule for the Kullback-Leibler divergence WIP merge-conflict t-measure-probability large-import labelled WIP
36100 plp127 feat(FieldTheory/KrullTopology): generalize theorems t-algebra awaiting review
36111 smmercuri fix: non-defeq projections in `WithAbs` t-analysis 🟤 running CI
28582 Thmoas-Guan feat(Data): some lemmas about WithBot ENat awaiting-author t-data awaiting author
26218 Thmoas-Guan feat(Algebra): definition of cohen macaulay blocked-by-other-PR t-algebra large-import blocked on another PR
28599 Thmoas-Guan feat(RingTheory): polynomial over CM ring is CM blocked-by-other-PR large-import t-ring-theory blocked on another PR
34881 CBirkbeck feat(ModularForm/NumberTheory/Delta): Define the delta function t-number-theory maintainer-merge 🟤 running CI
36112 tb65536 feat(CategoryTheory/Monoidal/Cartesian/Grp_): conjugation as a morphism t-category-theory t-algebraic-geometry t-algebra t-group-theory awaiting review
26245 Thmoas-Guan feat(Algebra): cohen macaulay local ring is catenary blocked-by-other-PR t-algebra large-import blocked on another PR
35867 edegeltje feat(CategoryTheory/Topos): Define subobject classifier for sheaf of types t-category-theory awaiting review
36107 sgouezel chore: mark definitions outputting classes as `implicit_reducible` 🟤 running CI
26957 Thmoas-Guan feat(Algebra): unmixed thm of Cohen-Macaulay ring blocked-by-other-PR t-algebra large-import blocked on another PR
36113 tb65536 feat(CategoryTheory/Monoidal/Grp_): add constructor for `Grp.mk A ⟶ Grp.mk B` awaiting-CI t-category-theory t-algebraic-geometry 🟤 does not pass CI
36114 euprunin chore: golf proofs 🟤 running CI
29934 smmercuri feat(Field/WithAbs): the lift of a ring homomorphism from `WithAbs v` to `WithAbs w` to their completions WIP merge-conflict FLT ⚠️ labelled WIP
30322 kckennylau feat(RingTheory): base change of graded algebra t-ring-theory failing CI
36115 urkud chore(CategoryTheory): reduce `Set α = α → Prop` defeq abuse 🟤 running CI
28072 kckennylau feat(RingTheory/Valuation): make tactic rw_val_equiv awaiting-author t-ring-theory failing CI
26743 grunweg feat: product rule for Lie bracket on manifolds t-differential-geometry awaiting review
35847 euprunin chore: golf proofs ready-to-merge awaiting bors
35157 Multramate feat(RingTheory/AdjoinRoot): add IsFractionRing for AdjoinRoot awaiting-author t-algebra t-ring-theory awaiting author
29425 pechersky feat(NumberTheory/Padics/Torsion): `HasEnoughRootsOfUnity ℤ_[p] (p - 1)` blocked-by-other-PR awaiting-author merge-conflict t-ring-theory blocked on another PR
36086 Multramate feat(Algebra): add liftEquiv for groups, rings, algebras, and adjoin roots t-algebra 🟤 running CI
27980 smmercuri feat: dimensions of completions at infinite place extensions blocked-by-other-PR merge-conflict t-number-theory FLT large-import blocked on another PR
32058 Thmoas-Guan feat(Algebra): category version Baer criterion blocked-by-other-PR t-category-theory t-algebra blocked on another PR
36116 xgenereux feat(Module/Torsion): P-primary component t-algebra 🟤 running CI
29558 Thmoas-Guan feat(Algebra): definition of global dimension blocked-by-other-PR merge-conflict t-ring-theory blocked on another PR
31999 Thmoas-Guan feat(RingTheory): global dimension equals the supremum over localizations blocked-by-other-PR awaiting-author t-ring-theory blocked on another PR
36087 matthewjasper chore: fix diamonds for Real/Complex Algebra instances awaiting review
31879 Thmoas-Guan feat(Algebra/Homology): Projective dimension in linear equiv awaiting-author t-algebra awaiting author
36092 tb65536 feat(CategoryTheory/Monoidal/Cartesian/Grp_): `Grp` has kernels t-category-theory large-import awaiting review
35846 BryceT233 feat(RingTheory/MvPowerSeries): add completeness for `MvPowerSeries` blocked-by-other-PR new-contributor t-ring-theory blocked on another PR
35433 morrison-daniel feat(LinearAlgebra/ExteriorAlgebra/Basic): adds multiplication lemmas for `ExteriorAlgebra` delegated t-algebra failing CI
35337 Thmoas-Guan feat(RingTheory): some lemma about span rank awaiting-author t-ring-theory 🟤 running CI
35850 vihdzp refactor: nicer definition for ordinal logarithm maintainer-merge t-set-theory failing CI
36117 vihdzp chore(RingTheory/IntegralDomain): review file t-ring-theory 🟤 running CI
34138 pfaffelh feat(MeasureTheory): Introduce `MassFunction α` giving rise to a `Measure α ⊤` t-measure-probability new-contributor awaiting review*
35651 sun123zxy feat(Mathlib/RingTheory/Ideal/Cotangent): `Submodule.map` definition of cotangent spaces awaiting-author new-contributor t-ring-theory awaiting author
32881 foderm feat(AlgebraicTopology/SimplicialObject): define simplicial homotopy awaiting-author new-contributor t-algebraic-topology awaiting author
35378 joelriou feat(Algebra/Homology/SpectralObject): construction of the objects on the pages of the spectral sequence t-category-theory t-algebra awaiting review
35767 kebekus feat: asymptotics of the `logCounting` function of Value Distribution Theory t-analysis awaiting review
36124 chrisflav feat(AlgebraicGeometry): `fromTildeΓ` is an isomorphism given a global presentation t-algebraic-geometry maintainer-merge 🟤 running CI
35535 mariainesdff feat(RingTheory/ClassGroup): prove mulEquiv awaiting-author t-ring-theory opened from a branch in the main mathlib repo (not a fork)
25978 Bergschaf feat(Order/Sublocale): Open Sublocales t-order 🟤 running CI
34777 sqrt-of-2 feat(Combinatorics/SetFamily/Intersecting): L-intersecting families ready-to-merge t-combinatorics new-contributor awaiting bors
35675 Thmoas-Guan feat(RingTheory/Smooth): some lemma about formally smooth t-ring-theory awaiting review
35948 chrisflav feat(AlgebraicGeometry): the pro-étale site of a scheme WIP t-algebraic-geometry labelled WIP
36069 Equilibris feat(Data/PFunctor): Universe generic W new-contributor t-data awaiting review
36128 grunweg Levicivita minimal WIP t-differential-geometry 🟤 labelled WIP
35958 bryangingechen ci: add conditionals on {lean,batteries}-pr-testing steps CI opened from a branch in the main mathlib repo (not a fork)
33842 joelriou feat(Algebra/Homology): spectral sequences WIP blocked-by-other-PR merge-conflict t-category-theory large-import blocked on another PR
36029 joelriou feat(Algebra/Homology): exact sequences for `SpectralObject.E` blocked-by-other-PR merge-conflict t-category-theory t-algebra blocked on another PR
35673 Parcly-Taxel feat: radical lemmas for natural numbers and integers awaiting-author file-removed t-ring-theory awaiting author
35890 grunweg chore: delete deprecated module Topology/PartialHomeomorph easy t-topology awaiting review
36119 Ruizsolveall feat(Topology/Covering): fundamental group of the circle is ℤ t-topology new-contributor awaiting review
36066 EtienneC30 feat: independence of processes with almost everywhere equal marginals ready-to-merge t-measure-probability awaiting bors
36131 ADedecker doc: fix reference to Bourbaki in Analysis.Convex.Approximation documentation easy t-analysis 🟤 running CI
26293 RemyDegenne feat: tightness from convergence of characteristic functions blocked-by-other-PR t-measure-probability blocked on another PR
27953 CoolRmal feat(ProbabilityTheory): Conditional Jensen's Inequality t-measure-probability new-contributor failing CI
35993 xgenereux chore: fix typo easy t-algebra awaiting review
35893 b-mehta feat(Data/Nat/Choose/Lucas): add choose_mul_mul and choose_pow_mul_pow_mul modular congruence lemmas t-data awaiting review
35895 edegeltje feat(CategoryTheory/Topos/Classifier): subobject classifiers, isos and equivalences t-category-theory awaiting review
35921 grunweg chore: remove some superfluous parens t-algebra awaiting review
34521 huaizhangchu feat(MeasureTheory): add measurableEmbedding_natCast awaiting-author t-measure-probability new-contributor awaiting author
36109 justus-springer feat(FieldTheory/RatFunc): Lüroth's theorem blocked-by-other-PR 🟤 ⚠️ blocked on another PR
32692 WilliamCoram feat: define multivariate restricted power series awaiting-author t-number-theory new-contributor t-ring-theory failing CI
29996 vihdzp chore(Order/Concept): `IsIntent` and `IsExtent` t-order maintainer-merge awaiting review
36110 mariainesdff feat(RingTheory/Valuation): add API delegated t-ring-theory 🟤 opened from a branch in the main mathlib repo (not a fork)
30551 smmercuri feat: dimension formulae for infinite places above WIP blocked-by-other-PR merge-conflict ⚠️ blocked on another PR
35408 MichaelStollBayreuth feat(NumberTheory/Height/Basic): add {mul|log}Height_comp_le, {mul|log}Height_fun_mul_eq t-number-theory t-algebra awaiting review
36013 pfaffelh feat(Topology/Compactness/CompactSystem): introduce compact Systems ⚠️ awaiting review
35233 kim-em chore: lake shake --add-public --keep-implied --keep-prefix --fix awaiting-author maintainer-merge large-import awaiting author
36130 vbeffara feat(Combionatorics/SimpleGraphs): generalize SimpleGraph.map to any function easy t-combinatorics new-contributor failing CI
34427 CoolRmal feat(MeasureTheory): Strong measurability is preserved under division in a group with zero t-measure-probability awaiting review
36132 smmercuri feat(NumberField/InfinitePlace/Ramification): add `placesOver` FLT ⚠️ failing CI
30339 grunweg feat: extend a tangent vector for a locally smooth vector field t-differential-geometry awaiting review
34940 michaellee94 feat: the graph of a continuous function on a $C^n$ manifold is a $C^n$ manifold awaiting-author t-differential-geometry new-contributor failing CI
36120 jjdishere feat(NumberTheory/Padics): Algebraically closedness of `C_p` WIP blocked-by-other-PR t-analysis t-algebra blocked on another PR
36122 kim-em chore: bump toolchain to v4.29.0-rc4 ready-to-merge dependency-bump 🟤 opened from a branch in the main mathlib repo (not a fork)
35008 b-mehta feat(Algebra/Order/BigOperators): order properties of subsets in groups with zero merge-conflict t-algebra large-import failing CI
35923 MichaelStollBayreuth feat(NumberTheory/Height/Basic): height bounds for products blocked-by-other-PR t-number-theory t-algebra large-import 🟤 blocked on another PR
35925 MichaelStollBayreuth feat(NumberTheory/Height/MvPolynomial): new file blocked-by-other-PR t-number-theory t-algebra 🟤 blocked on another PR
35927 MichaelStollBayreuth feat(NumberTheory/Height/MvPolynomial): upper bound for polynomial maps blocked-by-other-PR merge-conflict t-number-theory t-algebra large-import blocked on another PR
35940 MichaelStollBayreuth feat(NumberTheory/Height/MvPolynomial): lower height bounds for images under polynomial maps blocked-by-other-PR t-number-theory t-algebra large-import blocked on another PR
35941 MichaelStollBayreuth feat(NumberTheory/Height/MvPolynomial): add height bounds for `![x*y, x+y, 1]` blocked-by-other-PR t-number-theory t-algebra 🟤 blocked on another PR
36135 mathlib-splicebot chore(Mathlib/Algebra/Category/ModuleCat/Sheaf/Quasicoherent.lean): automated extraction ready-to-merge t-algebra new-contributor opened from a branch in the main mathlib repo (not a fork)
26390 jjdishere feat(Topology/Algebra): Krasner's lemma WIP t-number-theory t-topology t-algebra labelled WIP
36136 mathlib-splicebot chore(Mathlib/LinearAlgebra/Matrix/Kronecker.lean): automated extraction ready-to-merge t-algebra new-contributor opened from a branch in the main mathlib repo (not a fork)
36068 justus-springer feat(RingTheory/Polynomial/GaussLemma): `mem_lifts` lemma for primitive polynomials maintainer-merge t-ring-theory 🟤 running CI
26975 Whysoserioushah feat: a norm_num extension for complex numbers t-meta failing CI
35899 themathqueen feat(Analysis): `extremePoints 𝕜 (closedBall 0 1) ⊆ sphere 0 1` t-analysis awaiting review
35922 MichaelStollBayreuth feat(NumberTheory/Height/Basic): {mul|log}Height_{eq_one_of_subsingleton|sumElim_zero_eq} blocked-by-other-PR t-number-theory t-algebra large-import blocked on another PR
35572 joelriou feat(CategoryTheory/Sites/Point): fiber functors are monoidal WIP blocked-by-other-PR t-category-theory blocked on another PR
34551 IlPreteRosso refactor(Data.Finset.*Antidiagonal): rename defs to `set*Antidiagonal` and deprecate old names in namespace Finset awaiting-author t-algebra new-contributor awaiting author
35773 joelriou refactor(Algebra/Category/ModuleCat): another approach to the module structure on stalks WIP blocked-by-other-PR merge-conflict t-category-theory t-algebra blocked on another PR
35312 Komyyy feat(Order/Filter/Pointwise): `((∀ᶠ|∃ᶠ) x in op f, p x) ↔ ((∀ᶠ|∃ᶠ) x in f, p (op x))` t-order awaiting review
36140 RemyDegenne feat: `FiniteUnion` 🟤 ⚠️ running CI
35659 BryceT233 chore(Data/Finsupp): update pointwise module structure new-contributor t-data awaiting review
35670 BryceT233 feat(RingTheory/AdicCompletion): completeness of `AdicCompletion` blocked-by-other-PR new-contributor t-ring-theory blocked on another PR
34788 justus-springer feat(Algebra/Polynomial/AlgebraMap): add Polynomial.aeval_eq_aeval_map delegated t-algebra delegated
34045 smmercuri feat: `algebraMap K L` is uniform continuous with respect to adic topologies, when the ideal `w` of `L` lies above `v` t-algebra FLT awaiting review
36125 chrisflav feat(CategoryTheory/Abelian): five lemma variant for zero objects on the left resp. on the right t-category-theory 🟤 running CI
36129 kbuzzard chore: make sheaves into a full subcategory of presheaves WIP merge-conflict labelled WIP
36123 justus-springer feat(FieldTheory/IntermediateField/Basic): Add missing `coe_div` and attributes easy t-algebra maintainer-merge awaiting review
36108 justus-springer feat(Algebra/Polynomial/Eval/Subring): not_mem_map_range awaiting-author t-algebra awaiting author
36089 pfaffelh feat(Topology/Compactness/CompactSystem): set system of finite unions of sets in a compact system is again a compact system ⚠️ failing CI
30112 gaetanserre feat(Probability.Kernel): add representation of kernel as a map of a uniform measure t-measure-probability awaiting review
36138 tb65536 chore(Topology/Algebra/InfiniteSum/Group): generalize the Cauchy criterion to `CommMonoid` awaiting-CI t-topology t-analysis t-algebra t-group-theory 🟤 does not pass CI
26872 faenuccio chore(RingTheory/Valuation/RankOne): modify the definition of Valuation.RankOne using its range rather than its codomain blocked-by-other-PR awaiting-author merge-conflict t-algebra blocked on another PR
35327 SnirBroshi feat(SimpleGraph/Acyclic): the union of two trees that share exactly one vertex is a tree t-combinatorics awaiting review
35819 CBirkbeck feat(NumberTheory/ModularForm/EisensteinSeries/E2): Prove E2 is MDifferentiable t-number-theory awaiting review
36141 robin-carlier feat(CI): add paragraph about use of AI in new contributors comment CI awaiting review
36133 justus-springer feat(FieldTheory/RatFunc/Luroth): algEquivAdjoin WIP blocked-by-other-PR t-algebra blocked on another PR
36137 smmercuri feat: define pullbacks of `HeightOneSpectrum` t-ring-theory 🟤 running CI
36081 joelriou refactor(CategoryTheory/Sites): redefine the category of sheaves using `ObjectProperty.FullSubcategory` WIP merge-conflict t-category-theory large-import ❌? labelled WIP
34528 Maldooor feat: Reproducing Kernel Hilbert Spaces and Moore's theorem t-analysis maintainer-merge awaiting review
30579 smmercuri feat : `v.adicCompletionIntegers K` is compact when `K` is a number field WIP blocked-by-other-PR large-import ⚠️ blocked on another PR
35797 xroblot feat(IsGaloisGroup): if `B/A` and `B/A'` are Galois with the same Galois group, then `A ≃+* A'` t-algebra awaiting review
36036 grunweg Hm covder bundled WIP t-differential-geometry 🟤 labelled WIP
35098 b-mehta feat(Analysis/Normed): relate compactness of operators to locally compact spaces delegated t-analysis failing CI
36118 jjdishere fix(NumberTheory/Padics): remove diamond normed instance on C_p awaiting review
36043 robin-carlier feat: add `dsimp%` elaborator t-meta 🟤 running CI
36126 chrisflav feat(CategoryTheory/MorphismProperty): API for sites on `P.Over ⊤ X` t-category-theory awaiting review
36142 erdOne feat(Topology): sheaves of modules in `Over U` merge-conflict t-topology large-import 🟤 running CI