Why is my PR not on the queue?

This page was last updated on: February 24, 2026 at 23:02 UTC

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

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

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

Number Author Title Labels CI status? not blocked? no merge conflict? ready? awaiting review? On the review queue? Missing topic label? PR's overall status
13847 alreadydone feat(EllipticCurve): the universal elliptic curve merge-conflict awaiting-author t-algebra t-algebraic-geometry ??? opened from a branch in the main mathlib repo (not a fork)
14167 alreadydone feat: Group scheme structure on Weierstrass curve merge-conflict WIP 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 merge-conflict awaiting-author 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 merge-conflict awaiting-author t-algebra t-meta ??? opened from a branch in the main mathlib repo (not a fork)
12679 MichaelStollBayreuth perf(NumberTheory/RamificationInertia): speed up slow file merge-conflict WIP ??? opened from a branch in the main mathlib repo (not a fork)
13057 alreadydone feat(NumberTheory): characterize elliptic divisibility sequences merge-conflict t-algebra t-number-theory blocked-by-other-PR ??? opened from a branch in the main mathlib repo (not a fork)
12192 Ruben-VandeVelde feat: generalize isLittleO_const_id_atTop/atBot merge-conflict awaiting-author 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 t-topology awaiting-CI ??? opened from a branch in the main mathlib repo (not a fork)
10521 eric-wieser chore: generalize `IsBoundedLinearMap` to modules merge-conflict awaiting-author 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 merge-conflict WIP 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 merge-conflict WIP blocked-by-other-PR ??? opened from a branch in the main mathlib repo (not a fork)
11100 eric-wieser feat(CategoryTheory/Limits): add `Functor.mapBinaryBiconeInv` merge-conflict t-category-theory awaiting-CI ??? opened from a branch in the main mathlib repo (not a fork)
8503 thorimur feat: meta utils for `refine?` merge-conflict awaiting-author t-meta ??? opened from a branch in the main mathlib repo (not a fork)
8519 eric-wieser refactor(LinearAlgebra/TensorProduct): golf using `liftAddHom` merge-conflict awaiting-author 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 t-algebra awaiting-CI ??? opened from a branch in the main mathlib repo (not a fork)
8658 eric-wieser feat: support right actions for `Con` merge-conflict awaiting-author 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 merge-conflict awaiting-author t-algebra ??? opened from a branch in the main mathlib repo (not a fork)
8961 eric-wieser refactor: use the coinduced topology on ULift please-adopt merge-conflict awaiting-author awaiting-CI ??? opened from a branch in the main mathlib repo (not a fork)
9146 laughinggas feat(Data/ZMod/Defs): Topological structure on `ZMod` merge-conflict t-algebra awaiting-author t-topology ??? opened from a branch in the main mathlib repo (not a fork)
9229 eric-wieser refactor(Algebra/GradedMonoid): Use `HMul` to define `GMul` merge-conflict WIP 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 merge-conflict awaiting-author t-analysis ??? opened from a branch in the main mathlib repo (not a fork)
9356 alexjbest feat: assumption? merge-conflict awaiting-author 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 t-algebra t-measure-probability merge-conflict t-analysis ??? 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 t-algebra t-analysis awaiting-CI ??? opened from a branch in the main mathlib repo (not a fork)
9570 eric-wieser feat(Algebra/Star): Non-commutative generalization of `StarModule` merge-conflict WIP t-algebra awaiting-CI ??? 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 WIP merge-conflict awaiting-author help-wanted t-analysis ??? opened from a branch in the main mathlib repo (not a fork)
6580 adomani chore: `move_add`-driven replacements merge-conflict awaiting-author ??? opened from a branch in the main mathlib repo (not a fork)
6630 MohanadAhmed feat: Reduced Spectral Theorem merge-conflict WIP 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 merge-conflict awaiting-author help-wanted 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 merge-conflict WIP t-meta ??? opened from a branch in the main mathlib repo (not a fork)
6931 urkud refactor(Analysis/Normed*): use `RingHomIsometric` for `*.norm_cast` merge-conflict help-wanted t-analysis ??? opened from a branch in the main mathlib repo (not a fork)
7227 kmill feat: flexible binders and integration into notation3 merge-conflict WIP 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` merge-conflict awaiting-author t-order ??? opened from a branch in the main mathlib repo (not a fork)
7467 ADedecker feat: spectrum of X →ᵇ ℂ is StoneCech X merge-conflict WIP 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` merge-conflict t-topology blocked-by-other-PR ??? opened from a branch in the main mathlib repo (not a fork)
7601 digama0 feat: ring hom support in `ring` merge-conflict awaiting-author t-algebra t-meta ??? 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 t-algebra easy awaiting-CI ??? opened from a branch in the main mathlib repo (not a fork)
7713 RemyDegenne feat: add_left/right_inj for measures merge-conflict awaiting-author 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 merge-conflict awaiting-author 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 slow-typeclass-synthesis t-algebra ??? 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 merge-conflict WIP t-topology t-meta ??? opened from a branch in the main mathlib repo (not a fork)
7932 eric-wieser refactor(Algebra/TrivSqZeroExt): replace with a structure merge-conflict t-algebra awaiting-CI ??? opened from a branch in the main mathlib repo (not a fork)
7962 eric-wieser feat: `DualNumber (Quaternion R)` as a `CliffordAlgebra` merge-conflict WIP t-algebra ??? opened from a branch in the main mathlib repo (not a fork)
8364 thorimur feat: `refine?` merge-conflict blocked-by-other-PR 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 t-algebra awaiting-CI ??? opened from a branch in the main mathlib repo (not a fork)
5133 kmill feat: IntermediateField adjoin syntax for sets of elements merge-conflict WIP 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 merge-conflict WIP 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` merge-conflict awaiting-author 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 t-algebra awaiting-CI ??? opened from a branch in the main mathlib repo (not a fork)
6210 MohanadAhmed feat(Data/IsROrC/Basic): add a `StarOrderedRing` instance merge-conflict WIP t-algebra t-analysis ??? opened from a branch in the main mathlib repo (not a fork)
6328 astrainfinita chore: make some instance about `Sub...Class` lower priority merge-conflict WIP t-algebra awaiting-CI ??? 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...` merge-conflict WIP 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 t-algebra t-order merge-conflict slow-typeclass-synthesis awaiting-author ??? 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 merge-conflict WIP 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` merge-conflict WIP t-meta ??? opened from a branch in the main mathlib repo (not a fork)
12353 thorimur feat: `conv%` merge-conflict WIP t-meta ??? opened from a branch in the main mathlib repo (not a fork)
7903 urkud feat: define `UnboundedSpace` merge-conflict help-wanted t-topology ??? opened from a branch in the main mathlib repo (not a fork)
15679 adomani test: refactor in CI merge-conflict WIP ??? opened from a branch in the main mathlib repo (not a fork)
7565 shuxuezhuyi feat(Topology/Algebra/Order): extend homeomorphism of `Ioo` to `Icc` merge-conflict t-topology blocked-by-other-PR 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 merge-conflict WIP 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` merge-conflict t-linter awaiting-author ??? 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 merge-conflict WIP t-topology ??? opened from a branch in the main mathlib repo (not a fork)
11393 mcdoll feat(Analysis/Distribution/SchwartzSpace): The Heine-Borel property merge-conflict WIP t-analysis ??? opened from a branch in the main mathlib repo (not a fork)
9444 erdOne feat: Various instances regarding `𝓞 K`. merge-conflict help-wanted 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 merge-conflict t-computability awaiting-author ??? opened from a branch in the main mathlib repo (not a fork)
10387 adomani feat(Tactic/ComputeDegree): add `polynomial` tactic WIP RFC t-meta ??? opened from a branch in the main mathlib repo (not a fork)
9154 astrainfinita feat: `npow` / `nsmul` / `Nat.cast`/ `zpow` / `zsmul` implemented using `Nat.binaryRec` merge-conflict awaiting-author t-algebra blocked-by-other-PR ??? opened from a branch in the main mathlib repo (not a fork)
6603 tydeu feat: automatically try `cache get` before build merge-conflict WIP CI ??? opened from a branch in the main mathlib repo (not a fork)
6058 apurvnakade feat: duality theory for cone programs merge-conflict WIP t-analysis ??? opened from a branch in the main mathlib repo (not a fork)
6449 ADedecker feat: functions with finite fibers merge-conflict awaiting-author 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-algebraic-geometry t-category-theory ??? 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 astrainfinita chore(FieldTheory/KummerExtension): move some lemmas earlier merge-conflict awaiting-author t-algebra ??? opened from a branch in the main mathlib repo (not a fork)
12429 adomani feat: toND -- auto-generating natDegree t-algebra RFC merge-conflict awaiting-author t-meta ??? 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 t-data new-contributor ??? opened from a branch in the main mathlib repo (not a fork)
15448 urkud chore(*): deprecate `Option.elim'` merge-conflict awaiting-author 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 merge-conflict awaiting-author t-algebra ??? opened from a branch in the main mathlib repo (not a fork)
6517 MohanadAhmed feat: discrete Fourier transform of a finite sequence merge-conflict awaiting-author 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 merge-conflict t-algebra awaiting-author t-number-theory ??? opened from a branch in the main mathlib repo (not a fork)
15600 adomani feat: lint also `let` vs `have` merge-conflict WIP 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 t-computability WIP ??? opened from a branch in the main mathlib repo (not a fork)
14038 adomani test/decl diff in lean dev merge-conflict WIP ??? opened from a branch in the main mathlib repo (not a fork)
7861 shuxuezhuyi feat(Geometry/Hyperbolic/UpperHalfPlane): instance IsometricSMul PSL(2, ℝ) ℍ merge-conflict blocked-by-other-PR 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 t-topology awaiting-author 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 merge-conflict awaiting-author t-logic ??? opened from a branch in the main mathlib repo (not a fork)
14078 Ruben-VandeVelde feat(CI): continue after mk_all fails merge-conflict awaiting-author CI ??? opened from a branch in the main mathlib repo (not a fork)
11283 hmonroe feat(ModelTheory/Satisfiability): define theory with independent sentence merge-conflict WIP t-logic ??? opened from a branch in the main mathlib repo (not a fork)
16914 siddhartha-gadgil Loogle syntax with non-reserved merge-conflict WIP ??? opened from a branch in the main mathlib repo (not a fork)
13782 alreadydone feat(EllipticCurve): ZSMul formula in terms of division polynomials t-algebra t-number-theory blocked-by-other-PR merge-conflict t-algebraic-geometry ??? opened from a branch in the main mathlib repo (not a fork)
8118 iwilare feat(CategoryTheory): add dinatural transformations merge-conflict awaiting-author t-category-theory ??? opened from a branch in the main mathlib repo (not a fork)
14242 js2357 feat: Prove equivalence of `isDedekindDomain` and `isDedekindDomainDvr` merge-conflict t-algebra blocked-by-other-PR new-contributor ??? opened from a branch in the main mathlib repo (not a fork)
7516 ADedecker perf: use `abbrev` to prevent unifying useless data merge-conflict WIP ??? opened from a branch in the main mathlib repo (not a fork)
17127 astrainfinita 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 merge-conflict blocked-by-other-PR new-contributor t-logic ??? opened from a branch in the main mathlib repo (not a fork)
16888 metinersin feat(ModelTheory/Complexity): Define conjunctive and disjunctive normal forms merge-conflict blocked-by-other-PR new-contributor t-logic ??? opened from a branch in the main mathlib repo (not a fork)
16889 metinersin feat(ModelTheory/Complexity): Normal forms merge-conflict blocked-by-other-PR new-contributor t-logic ??? opened from a branch in the main mathlib repo (not a fork)
14712 astrainfinita perf: change instance priority and order about `OfNat` merge-conflict slow-typeclass-synthesis t-algebra delegated ??? opened from a branch in the main mathlib repo (not a fork)
5995 astrainfinita feat: add APIs about `Quotient.choice` merge-conflict awaiting-author 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` merge-conflict awaiting-author 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 merge-conflict blocked-by-other-PR 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 t-data new-contributor merge-conflict awaiting-author ??? 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 merge-conflict WIP 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 please-adopt t-data new-contributor merge-conflict awaiting-author ??? opened from a branch in the main mathlib repo (not a fork)
13514 madvorak feat(Computability/ContextFreeGrammar): closure under union merge-conflict t-computability blocked-by-other-PR ??? opened from a branch in the main mathlib repo (not a fork)
9654 urkud feat: add `@[mk_eq]` version of `@[mk_iff]` merge-conflict awaiting-author t-meta ??? opened from a branch in the main mathlib repo (not a fork)
16704 AntoineChambert-Loir feat(Mathlib.Data.Ordering.Dickson): Dickson orders merge-conflict WIP t-order ??? opened from a branch in the main mathlib repo (not a fork)
16355 Ruben-VandeVelde feat: odd_{add,sub}_one merge-conflict t-algebra awaiting-author t-number-theory ??? opened from a branch in the main mathlib repo (not a fork)
8479 alexjbest feat: use leaff in CI merge-conflict WIP awaiting-author ??? ⚠️ 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 merge-conflict awaiting-author new-contributor t-logic ??? opened from a branch in the main mathlib repo (not a fork)
18716 jjaassoonn feat(Algebra/Module/GradedModule): quotient and subgrading WIP t-algebra blocked-by-other-PR awaiting-CI merge-conflict opened from a branch in the main mathlib repo (not a fork)
9341 winstonyin feat: Naturality of integral curves merge-conflict awaiting-author t-differential-geometry ??? opened from a branch in the main mathlib repo (not a fork)
13248 hcWang942 feat: basic concepts of auction theory merge-conflict awaiting-author new-contributor t-logic ??? opened from a branch in the main mathlib repo (not a fork)
9344 erdOne feat: Add `AddGroup.FG` -> `Module.Finite ℤ` as instances merge-conflict awaiting-author t-algebra ??? opened from a branch in the main mathlib repo (not a fork)
12133 ADedecker feat: generalize instIsLowerProd to arbitrary products merge-conflict awaiting-author t-topology t-order ??? opened from a branch in the main mathlib repo (not a fork)
16637 astrainfinita perf: reorder `extends` of `(Add)Monoid` merge-conflict WIP t-algebra opened from a branch in the main mathlib repo (not a fork)
8661 joelriou feat(CategoryTheory/Sites): descent of sheaves merge-conflict WIP t-category-theory ??? opened from a branch in the main mathlib repo (not a fork)
10476 shuxuezhuyi feat(Topology/UniformSpace): define uniform preordered space merge-conflict awaiting-author t-topology ??? opened from a branch in the main mathlib repo (not a fork)
17593 astrainfinita chore(Algebra/Order/GroupWithZero/Unbundled): deprecate useless lemmas, use `ZeroLEOneClass` merge-conflict t-algebra blocked-by-other-PR t-order ??? opened from a branch in the main mathlib repo (not a fork)
17623 astrainfinita feat(Algebra/Order/GroupWithZero/Unbundled): add some lemmas merge-conflict t-algebra awaiting-zulip t-order ??? opened from a branch in the main mathlib repo (not a fork)
17624 astrainfinita feat(Algebra/Order/GroupWithZero/Unbundled): generalize lemmas merge-conflict t-algebra blocked-by-other-PR t-order ??? opened from a branch in the main mathlib repo (not a fork)
17513 astrainfinita perf: do not search algebraic hierarchies when using `map_*` lemmas merge-conflict WIP t-algebra awaiting-bench ??? opened from a branch in the main mathlib repo (not a fork)
17515 astrainfinita perf: do not need `simp low` now merge-conflict t-algebra blocked-by-other-PR 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 merge-conflict WIP 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 merge-conflict WIP ??? 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 merge-conflict awaiting-author t-logic ??? opened from a branch in the main mathlib repo (not a fork)
11210 hmonroe Test commit merge-conflict WIP ??? opened from a branch in the main mathlib repo (not a fork)
19621 Command-Master feat: Multiplicity and prime-adic valuation of derivations merge-conflict t-algebra blocked-by-other-PR 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 t-algebra blocked-by-other-PR t-category-theory merge-conflict opened from a branch in the main mathlib repo (not a fork)
15269 kkytola feat: Add ENNReal.floor t-algebra blocked-by-other-PR t-order merge-conflict awaiting-author ??? opened from a branch in the main mathlib repo (not a fork)
15773 kkytola feat: Add type class for ENat-valued floor functions merge-conflict awaiting-author t-order ??? opened from a branch in the main mathlib repo (not a fork)
3251 kmill feat: deriving `LinearOrder` for simple enough inductive types merge-conflict WIP awaiting-author t-meta ??? opened from a branch in the main mathlib repo (not a fork)
3610 TimothyGu feat: derive Infinite automatically for inductive types merge-conflict awaiting-author t-meta ??? missing CI information
16120 awainverse feat(ModelTheory/Algebra/Ring/Basic): Ring homomorphisms are a `StrongHomClass` for the language of rings merge-conflict t-algebra RFC t-logic ??? 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 merge-conflict awaiting-author t-topology new-contributor ??? opened from a branch in the main mathlib repo (not a fork)
18474 astrainfinita perf: lower the priority of `*WithOne.to*` instances merge-conflict slow-typeclass-synthesis t-algebra 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 merge-conflict awaiting-author 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 merge-conflict blocked-by-other-PR 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 merge-conflict t-computability awaiting-author new-contributor ??? opened from a branch in the main mathlib repo (not a fork)
8362 urkud feat(Asymptotics): define `ReflectsGrowth` merge-conflict awaiting-author t-analysis ??? opened from a branch in the main mathlib repo (not a fork)
6692 prakol16 feat: disjoint indexed union of local homeomorphisms merge-conflict awaiting-author 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 merge-conflict awaiting-author 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 merge-conflict WIP ??? 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 merge-conflict awaiting-author t-meta ??? opened from a branch in the main mathlib repo (not a fork)
11837 trivial1711 feat: completion of a uniform multiplicative group WIP t-algebra merge-conflict help-wanted t-topology opened from a branch in the main mathlib repo (not a fork)
12670 trivial1711 feat: completion of a nonarchimedean multiplicative group merge-conflict t-algebra t-topology blocked-by-other-PR 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 merge-conflict t-computability awaiting-author ??? opened from a branch in the main mathlib repo (not a fork)
19697 quangvdao feat(BigOperators/Fin): Sum/product over `Fin` intervals merge-conflict awaiting-author 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` merge-conflict WIP ??? 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 large-import new-contributor merge-conflict awaiting-author t-topology ??? 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 merge-conflict awaiting-author t-topology ??? opened from a branch in the main mathlib repo (not a fork)
18785 erdOne feat(CategoryTheory): command that generates instances for `MorphismProperty` merge-conflict awaiting-author t-category-theory t-meta ??? opened from a branch in the main mathlib repo (not a fork)
16311 madvorak feat(Computability): regular languages are context-free merge-conflict WIP 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 merge-conflict t-computability awaiting-author new-contributor ??? opened from a branch in the main mathlib repo (not a fork)
17005 YnirPaz feat(SetTheory/Cardinal/Regular): define singular cardinals merge-conflict WIP 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 merge-conflict awaiting-author 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 merge-conflict modifies-tactic-syntax awaiting-author 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 merge-conflict awaiting-author carleson t-measure-probability ??? 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 merge-conflict awaiting-author 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-algebra t-category-theory 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 merge-conflict awaiting-author t-data ??? opened from a branch in the main mathlib repo (not a fork)
13648 urkud feat(Topology/Module): generalize `ContinuousLinearMap.compSL` t-algebra merge-conflict awaiting-author t-topology t-analysis 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 merge-conflict blocked-by-other-PR new-contributor t-logic ??? 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 t-combinatorics t-analysis blocked-by-other-PR ??? 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 t-category-theory large-import merge-conflict ??? 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 astrainfinita perf: lower the priority of `Normed*.to*` instances merge-conflict slow-typeclass-synthesis t-algebra t-analysis ??? opened from a branch in the main mathlib repo (not a fork)
16944 YnirPaz feat(SetTheory/Cardinal/Cofinality): lemmas about limit ordinals and cofinality merge-conflict WIP 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` merge-conflict awaiting-author 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 merge-conflict t-linter awaiting-author ??? opened from a branch in the main mathlib repo (not a fork)
19013 quangvdao feat(Algebra/BigOperators/Fin): Add `finSigmaFinEquiv` merge-conflict awaiting-author 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 merge-conflict awaiting-author 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 merge-conflict awaiting-author CI ??? opened from a branch in the main mathlib repo (not a fork)
15774 kkytola feat: Topology on `ENat` merge-conflict WIP t-topology t-order ??? opened from a branch in the main mathlib repo (not a fork)
20222 eric-wieser feat: generalize lemmas about derivatives merge-conflict blocked-by-other-PR 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 t-data enhancement new-contributor merge-conflict awaiting-author 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 merge-conflict WIP t-topology t-analysis ??? opened from a branch in the main mathlib repo (not a fork)
13124 astrainfinita chore: remove `CovariantClass` and `ContravariantClass` merge-conflict WIP opened from a branch in the main mathlib repo (not a fork)
19275 eric-wieser fix: if nolint files change, do a full rebuild merge-conflict delegated opened from a branch in the main mathlib repo (not a fork)
15212 victorliu5296 feat: Add fundamental theorem of calculus-2 for Banach spaces t-measure-probability new-contributor merge-conflict awaiting-author t-analysis ??? 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 merge-conflict t-topology documentation awaiting-author ??? 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) merge-conflict blocked-by-other-PR 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) merge-conflict blocked-by-other-PR t-category-theory large-import ??? opened from a branch in the main mathlib repo (not a fork)
19425 hrmacbeth perf: gcongr forward-reasoning adjustment merge-conflict awaiting-author ??? opened from a branch in the main mathlib repo (not a fork)
20873 vbeffara feat(Topology/Covering): path lifting and homotopy lifting merge-conflict awaiting-author t-topology new-contributor opened from a branch in the main mathlib repo (not a fork)
22817 peabrainiac feat(CategoryTheory/Sites): local sites merge-conflict WIP t-category-theory ??? opened from a branch in the main mathlib repo (not a fork)
16314 astrainfinita 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 merge-conflict awaiting-author ??? 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 t-category-theory awaiting-CI ??? 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 slow-typeclass-synthesis t-algebra awaiting-CI ??? opened from a branch in the main mathlib repo (not a fork)
13038 adomani feat: Mathlib weekly reports awaiting-author CI t-meta ??? opened from a branch in the main mathlib repo (not a fork)
5952 eric-wieser feat: add Qq wrappers for ToExpr merge-conflict awaiting-CI t-meta ??? opened from a branch in the main mathlib repo (not a fork)
15483 astrainfinita chore(GroupTheory/Coset): reduce defeq abuse merge-conflict t-algebra ??? opened from a branch in the main mathlib repo (not a fork)
16594 astrainfinita perf: reorder `extends` and remove some instances in algebra hierarchy merge-conflict slow-typeclass-synthesis t-algebra ??? opened from a branch in the main mathlib repo (not a fork)
19467 quangvdao feat(MvPolynomial/Equiv): Add `MvPolynomial.finSuccEquivNth` merge-conflict t-algebra blocked-by-other-PR ??? 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 merge-conflict awaiting-author t-algebra new-contributor opened from a branch in the main mathlib repo (not a fork)
19117 eric-wieser feat: derivatives of matrix operations merge-conflict WIP t-analysis opened from a branch in the main mathlib repo (not a fork)
12605 astrainfinita chore: attribute [induction_eliminator] merge-conflict awaiting-author ??? 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 merge-conflict awaiting-author t-algebra opened from a branch in the main mathlib repo (not a fork)
23593 erdOne feat(AlgebraicGeometry): the tilde construction is functorial merge-conflict awaiting-author 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 merge-conflict WIP 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 merge-conflict WIP carleson t-measure-probability opened from a branch in the main mathlib repo (not a fork)
14731 adomani feat: the repeated typeclass assumption linter merge-conflict WIP t-linter large-import opened from a branch in the main mathlib repo (not a fork)
13649 astrainfinita 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 merge-conflict WIP t-differential-geometry blocked-by-other-PR opened from a branch in the main mathlib repo (not a fork)
22809 b-reinke feat: Category algebras and path algebras WIP t-algebra t-category-theory new-contributor opened from a branch in the main mathlib repo (not a fork)
14675 adomani dev: the repeated variable linter merge-conflict WIP t-linter ??? opened from a branch in the main mathlib repo (not a fork)
14330 Ruben-VandeVelde chore: split Mathlib.Algebra.Star.Basic merge-conflict awaiting-author ??? 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 merge-conflict awaiting-author 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 merge-conflict WIP t-data ??? opened from a branch in the main mathlib repo (not a fork)
11524 mcdoll refactor: Introduce type-class for SchwartzMap merge-conflict WIP t-analysis ??? opened from a branch in the main mathlib repo (not a fork)
11003 thorimur chore: migrate to `tfae` block tactic merge-conflict WIP blocked-by-other-PR 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 new-contributor t-computability merge-conflict 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 merge-conflict awaiting-author 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 RFC t-data t-meta ??? 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] t-computability awaiting-author new-contributor ??? opened from a branch in the main mathlib repo (not a fork)
24642 grunweg WIP-feat: add layercake formula for ENNReal-valued functions merge-conflict WIP carleson t-analysis opened from a branch in the main mathlib repo (not a fork)
21712 grunweg chore: generalise more lemmas to `ContinuousENorm` merge-conflict carleson awaiting-CI t-measure-probability opened from a branch in the main mathlib repo (not a fork)
21375 grunweg WIP: generalise lemmas to ENorm WIP awaiting-CI t-measure-probability carleson merge-conflict 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 t-order merge-conflict help-wanted awaiting-author t-topology ??? 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 large-import new-contributor ??? opened from a branch in the main mathlib repo (not a fork)
12438 jjaassoonn feat: some APIs for flat modules merge-conflict WIP t-category-theory ??? opened from a branch in the main mathlib repo (not a fork)
8740 digama0 fix: improve `recall` impl / error reporting merge-conflict awaiting-author awaiting-CI t-meta 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 CI delegated ??? 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 merge-conflict WIP awaiting-author CI ??? opened from a branch in the main mathlib repo (not a fork)
12799 jstoobysmith feat(LinearAlgebra/UnitaryGroup): Add properties of Special Unitary Group please-adopt t-algebra new-contributor merge-conflict awaiting-author ??? 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)
23929 meithecatte feat(Computability/NFA): improve bound on pumping lemma t-computability awaiting-zulip new-contributor opened from a branch in the main mathlib repo (not a fork)
21734 adomani fix(PR summary): checkout GITHUB_SHA merge-conflict WIP awaiting-author CI ??? opened from a branch in the main mathlib repo (not a fork)
13483 adomani feat: automatically replace deprecations merge-conflict awaiting-author delegated 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 merge-conflict awaiting-author new-contributor t-meta ??? opened from a branch in the main mathlib repo (not a fork)
25912 BoltonBailey feat: add simp lemmas for trig functions on `π * 2⁻¹` awaiting-author blocked-by-other-PR t-analysis blocked on another PR
23953 b-reinke feat(Data/Matroid/Tutte): define the Tutte polynomial of a matroid merge-conflict WIP t-data opened from a branch in the main mathlib repo (not a fork)
25921 BoltonBailey feat: scripts to analyze overlap between namespaces WIP migrated-from-branch t-meta labelled WIP
18771 joelriou feat(LinearAlgebra/ExteriorPower): exterior powers of free modules are free merge-conflict WIP t-algebra blocked-by-other-PR 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 merge-conflict WIP t-algebra blocked-by-other-PR ??? opened from a branch in the main mathlib repo (not a fork)
18735 joelriou feat(Algebra/Module): presentation of the exterior power merge-conflict WIP t-algebra blocked-by-other-PR 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 merge-conflict awaiting-author 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 merge-conflict t-differential-geometry delegated ??? 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 awaiting-zulip new-contributor ??? opened from a branch in the main mathlib repo (not a fork)
25561 callesonne feat(Category/Grpd): define the bicategory of groupoids merge-conflict awaiting-author 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
26395 winstonyin feat: $C^1$ vector fields on compact manifolds define global flows merge-conflict WIP t-differential-geometry blocked-by-other-PR blocked on another PR
26465 joelriou feat(Algebra/Module): presentation of the `PiTensorProduct` merge-conflict file-removed t-algebra blocked-by-other-PR blocked on another PR
26467 joelriou feat(LinearAlgebra): the tensor product of a finite family of free modules is free WIP t-algebra blocked-by-other-PR merge-conflict file-removed blocked on another PR
20784 eric-wieser fix: prevent `exact?` recursing forever on `n = 55` t-set-theory 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 merge-conflict WIP 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 xgenereux feat(Algebra/SkewMonoidAlgebra/Basic): add SkewMonoidAlgebra merge-conflict WIP 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 t-topology easy awaiting author
26911 JovanGerb chore: fix naming of `mono` and `monotone` merge-conflict delegated 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 merge-conflict awaiting-author 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 merge-conflict WIP t-category-theory opened from a branch in the main mathlib repo (not a fork)
26987 joelriou chore: deprecating module LinearAlgebra.PiTensorProduct merge-conflict WIP t-algebra blocked-by-other-PR blocked on another PR
27435 callesonne feat(Normed/Algebra/Logarithm): add FormalMultilinearSeries of logarithm around `1` WIP t-analysis labelled WIP
24668 robertmaxton42 feat(LinearAlgebra): add inductive principle for the free product of algebras merge-conflict t-algebra blocked-by-other-PR ??? opened from a branch in the main mathlib repo (not a fork)
13973 digama0 feat: lake exe refactor, initial framework merge-conflict awaiting-author t-meta ??? opened from a branch in the main mathlib repo (not a fork)
10190 jstoobysmith feat(AlgebraicTopology): add Augmented Simplex Category t-algebraic-topology WIP t-category-theory new-contributor merge-conflict ??? opened from a branch in the main mathlib repo (not a fork)
25914 eric-wieser feat: add an ext lemma for the opposite category merge-conflict awaiting-author t-category-theory awaiting-CI 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 merge-conflict WIP t-algebra opened from a branch in the main mathlib repo (not a fork)
24260 plp127 feat(Topology): add API for Hereditarily Lindelof spaces merge-conflict awaiting-author t-topology ??? opened from a branch in the main mathlib repo (not a fork)
27813 javra feat: IMO 2025 Q1 IMO WIP labelled WIP
27608 RemyDegenne feat(MeasureTheory): typeclasses for measures with finite moments merge-conflict WIP t-measure-probability labelled WIP
27826 xgenereux feat(Subsemiring): mk_eq_zero WIP t-algebra labelled WIP
27050 BoltonBailey doc(Control/Monad/Cont): add docstrings awaiting-author t-data failing CI
27225 eric-wieser refactor(Tactic/Lift): deprecate the third with argument awaiting-author t-meta 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 merge-conflict t-set-theory blocked-by-other-PR new-contributor 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 t-set-theory new-contributor opened from a branch in the main mathlib repo (not a fork)
25484 VTrelat feat(SetTheory/ZFC/Booleans): define Boolean algebra in ZFC merge-conflict t-set-theory blocked-by-other-PR new-contributor 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 merge-conflict WIP t-ring-theory labelled WIP
22909 AntoineChambert-Loir feat(RingTheory/Pure): pure submodules merge-conflict t-ring-theory blocked-by-other-PR 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 merge-conflict t-ring-theory blocked-by-other-PR ??? 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 merge-conflict WIP t-ring-theory ??? opened from a branch in the main mathlib repo (not a fork)
20431 erdOne feat(RingTheory/AdicCompletion): monotonicity of adic-completeness merge-conflict awaiting-author 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 merge-conflict awaiting-author t-ring-theory large-import ??? opened from a branch in the main mathlib repo (not a fork)
18646 jxjwan feat(RingTheory): isotypic components merge-conflict t-ring-theory new-contributor opened from a branch in the main mathlib repo (not a fork)
17246 pechersky feat(RingTheory/PrimaryDecomposition): PIR of Noetherian under jacobson condition merge-conflict awaiting-author 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 t-ring-theory large-import opened from a branch in the main mathlib repo (not a fork)
11212 shuxuezhuyi feat(GroupTheory/GroupAction): instance `MulAction (β ⧸ H) α` merge-conflict awaiting-author t-group-theory large-import ??? opened from a branch in the main mathlib repo (not a fork)
27886 alreadydone feat(Algebra): (Mv)Polynomial.X is irreducible assuming NoZeroDivisors merge-conflict awaiting-author t-algebra merge conflict
26200 adomani fix: add label when landrun fails merge-conflict CI merge conflict
17469 joelriou feat(Algebra/ModuleCat/Differentials/Presheaf): the presheaf of relative differentials WIP t-category-theory large-import merge-conflict t-algebraic-geometry opened from a branch in the main mathlib repo (not a fork)
27709 kckennylau chore: fix links merge-conflict WIP labelled WIP
28075 tristan-f-r chore(Finsupp/Indicator): make non-classical awaiting-author t-data easy awaiting author
20671 thefundamentaltheor3m feat(Analysis/Asymptotics/SpecificAsymptotics): Proving that 𝛔ₖ(n) = O(nᵏ⁺¹) t-number-theory new-contributor large-import merge-conflict awaiting-author ??? opened from a branch in the main mathlib repo (not a fork)
20267 joelriou feat(CategoryTheory): comma categories are accessible merge-conflict WIP awaiting-author 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 t-ring-theory large-import merge conflict
27444 grunweg feat: generalise more lemmas to enorms carleson WIP ⚠️ labelled WIP
24862 grunweg feat(LocallyIntegrable): generalise more to enorms merge-conflict WIP carleson t-measure-probability 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 WIP new-contributor will-close-soon awaiting-author help-wanted t-analysis 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 t-data new-contributor ??? 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)
26394 winstonyin feat: existence of local flows on manifolds merge-conflict WIP t-differential-geometry labelled WIP
27759 plp127 chore(FreeAbelianGroup): deprecate multiplication merge-conflict t-algebra large-import failing CI
8102 miguelmarco feat(Tactic): add `unify_denoms` and `collect_signs` tactics please-adopt new-contributor merge-conflict modifies-tactic-syntax good first issue t-meta ??? opened from a branch in the main mathlib repo (not a fork)
7873 astrainfinita perf: reorder `extends` and change instance priority in algebra hierarchy merge-conflict slow-typeclass-synthesis t-algebra blocked-by-other-PR ??? opened from a branch in the main mathlib repo (not a fork)
27446 grunweg chore: more enorm lemmas merge-conflict WIP carleson labelled WIP
14583 lecopivo fix: make concrete cycle notation local merge-conflict awaiting-author ??? 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 new-contributor merge-conflict awaiting-author t-logic blocked on another PR
28622 alreadydone chore(Mathlib): replace `=>` by `↦` merge-conflict merge conflict
24793 tristan-f-r feat: trace of unitarily similar matrices merge-conflict awaiting-author t-algebra ??? 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` merge-conflict t-algebra blocked-by-other-PR new-contributor opened from a branch in the main mathlib repo (not a fork)
7300 ah1112 feat: synthetic geometry merge-conflict awaiting-author help-wanted 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 t-data new-contributor merge conflict
25488 VTrelat feat(SetTheory/ZFC/Rationals): define rationals in ZFC merge-conflict t-set-theory blocked-by-other-PR new-contributor 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 t-data new-contributor failing CI
28787 alreadydone feat(Counterexamples): a domain whose ring of differences is not a domain merge-conflict t-algebra blocked-by-other-PR large-import blocked on another PR
24719 madvorak feat(LinearAlgebra/Matrix/NonsingularInverse): inverting `Matrix` inverts its `LinearEquiv` awaiting-author t-algebra ??? 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 merge-conflict WIP t-ring-theory labelled WIP
28148 kckennylau feat(Matrix): Simproc and Rw-proc for Matrix Transpose merge-conflict t-meta merge conflict
24373 YaelDillies refactor: golf `modularCharacter` awaiting-CI t-measure-probability opened from a branch in the main mathlib repo (not a fork)
28686 mitchell-horner feat(Combinatorics/SimpleGraph): prove the Erdős-Stone theorem merge-conflict WIP blocked-by-other-PR t-combinatorics blocked on another PR
28687 mitchell-horner feat(Combinatorics/SimpleGraph): prove the Erdős-Stone-Simonovits theorem merge-conflict WIP blocked-by-other-PR t-combinatorics blocked on another PR
28689 mitchell-horner feat(Combinatorics/SimpleGraph): prove well-known corollaries of the Erdős-Stone-Simonovits theorem merge-conflict WIP blocked-by-other-PR t-combinatorics blocked on another PR
26952 robin-carlier feat(CategoryTheory/DayConvolution): monoid objects internal to day convolutions merge-conflict blocked-by-other-PR t-category-theory blocked on another PR
27133 robin-carlier feat(CategoryTheory/Monoidal/DayConvolution): `C ⊛⥤ V` is monoidal closed when `V` is merge-conflict blocked-by-other-PR t-category-theory blocked on another PR
27151 robin-carlier feat(CategoryTheory/Monoidal/DayConvolution): `C ⊛⥤ V` is braided/symmetric when `C` and `V` are braided/symmetric merge-conflict blocked-by-other-PR t-category-theory blocked on another PR
27175 robin-carlier feat(CategoryTheory/Monoidal/DayConvolution): `LawfulDayConvolutionMonoidalCategoryStruct.ι C V D` is monoidal when the target is `C ⊛⥤ V` merge-conflict blocked-by-other-PR t-category-theory blocked on another PR
25741 robin-carlier feat(AlgebraicTopology/SimplexCategory/SimplicialObject): definitions of simplicial objects by generators and relation t-algebraic-topology blocked-by-other-PR t-category-theory large-import merge-conflict blocked on another PR
26931 javra feat(CategoryTheory/Enriched): `V`-enriched isomorphisms merge-conflict awaiting-author t-category-theory infinity-cosmos merge conflict
27707 FLDutchmann feat(NumberTheory/SelbergSieve): define Selberg's weights and prove basic results. merge-conflict t-number-theory blocked-by-other-PR t-analysis blocked on another PR
25208 erdOne feat(LinearAlgebra): `tensor_induction` macro merge-conflict WIP t-algebra RFC ??? opened from a branch in the main mathlib repo (not a fork)
28803 astrainfinita refactor: unbundle algebra from `ENormed*` t-algebra merge-conflict slow-typeclass-synthesis awaiting-zulip t-analysis ❌? infrastructure-related CI failing
29232 vihdzp feat: more theorems on `SuccAddOrder` t-algebra t-order failing CI
26935 Paul-Lez feat(Analysis/SpecialFunction/NthRoot): definition and basic API of Real.nthRoot t-analysis failing CI
27995 kckennylau feat(RingTheory/Valuation): alternate constructors for Valuation t-ring-theory awaiting-CI does not pass CI
26159 upobir feat(Algebra/QuadraticDiscriminant): Adding inequalities on quadratic from inequalities on discriminant awaiting-author t-algebra awaiting author
28151 iehality feat(Computability): r.e. sets are closed under inter/union/projection/composition merge-conflict t-computability awaiting-author merge conflict
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 merge-conflict blocked-by-other-PR t-meta blocked on another PR
13036 joelriou feat(CategoryTheory/Sites): under certain conditions, cover preserving functors preserve 1-hypercovers merge-conflict WIP t-category-theory ??? 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 merge-conflict WIP 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 ℂ` t-analysis easy 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 large-import awaiting-CI t-meta does not pass CI
25069 erdOne feat(EllipticCurve): rational points of singular nodal cubics merge-conflict awaiting-author t-algebraic-geometry ??? opened from a branch in the main mathlib repo (not a fork)
25070 erdOne feat(EllipticCurve): rational points on singular cuspidal cubics merge-conflict awaiting-author t-algebraic-geometry ??? opened from a branch in the main mathlib repo (not a fork)
26670 yu-yama feat(GroupExtension/Abelian): define `conjClassesEquivH1` merge-conflict awaiting-author t-algebra merge conflict
26154 ADedecker refactor: add refactored APIs for algebraic filter bases merge-conflict t-topology merge conflict
27024 grunweg feat: Gram-Schmidt orthonormalisation for sections of a vector bundle merge-conflict awaiting-author t-differential-geometry merge conflict
28580 kmill refactor: simplify implementation of `filter_upwards` merge-conflict t-order t-meta 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 merge-conflict WIP t-category-theory awaiting-CI ??? 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 merge-conflict WIP t-algebra blocked-by-other-PR blocked on another PR
28067 grunweg Docstring enumerations merge-conflict blocked-by-other-PR blocked on another PR
28908 joelriou feat(CategoryTheory): Pullback functors on `Over` categories in `Type` have right adjoints merge-conflict awaiting-author t-category-theory failing CI
25480 ocfnash feat: define a concrete model of the `𝔤₂` root system merge-conflict WIP t-algebra large-import 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` merge-conflict WIP ⚠️ 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 merge-conflict awaiting-author t-category-theory new-contributor merge conflict
27214 robin-carlier feat(CategoryTheory/Limits/Shapes/Pullback/Categorical): Categorical pullback squares merge-conflict t-category-theory merge conflict
27391 robin-carlier feat(CategoryTheory/Limits/Shapes/Pullback/Categorical): pseudofunctoriality structure of categorical pullback squares merge-conflict blocked-by-other-PR t-category-theory blocked on another PR
27432 robin-carlier feat(CategoryTheory/Limits/Shapes/Pullback/Categorical): pseudofunctoriality of categorical pulback squares merge-conflict blocked-by-other-PR t-category-theory blocked on another PR
27481 robin-carlier feat(CategoryTheory/Limits/Shapes/Pullback/Categorical): adjunctions and equivalences of categorical pullback squares merge-conflict blocked-by-other-PR t-category-theory large-import blocked on another PR
27686 robin-carlier feat(CategoryTheory/Limits/Shapes/Pullback/Categorical/Square): more API for `CatPullbackSquare` merge-conflict blocked-by-other-PR t-category-theory large-import blocked on another PR
27687 robin-carlier feat(CategoryTheory/Limits/Shapes/Pullback/Categorical): squares equivalent to a `CatPullbackSquare` merge-conflict blocked-by-other-PR t-category-theory large-import blocked on another PR
27688 robin-carlier feat(CategoryTheory/Limits/Shapes/Pullback/Categorical): coherence statement for `CatPullbackSquare.inverse` merge-conflict blocked-by-other-PR t-category-theory large-import blocked on another PR
27689 robin-carlier feat(CategoryTheory/Limits/Shapes/Pullback/Categorical): horizontal pasting calculus for `CatPullbackSquare` merge-conflict blocked-by-other-PR t-category-theory large-import blocked on another PR
27690 robin-carlier feat(CategoryTheory/Limits/Shapes/Pullback/Categorical): vertical pasting calculus for `CatPullbackSquare` merge-conflict blocked-by-other-PR t-category-theory large-import blocked on another PR
27740 robin-carlier feat(CategoryTheory/Limits/Shapes/Pullback/Categorical): pasting calculus for `CategoricalPullback` merge-conflict blocked-by-other-PR t-category-theory large-import blocked on another PR
26330 Timeroot feat: "Junk value" test file awaiting-author t-data awaiting author
28452 plp127 feat: Define `ZMod.fintype` without cases awaiting-author t-data awaiting author
26466 robin-carlier feat(AlgebraicTopology/SimplexCategory/Augmented): the canonical monoid object in the augmented simplex category merge-conflict t-algebraic-topology t-category-theory merge conflict
28074 grunweg Isbilinearmap merge-conflict WIP labelled WIP
26579 robin-carlier feat(CategoryTheory/Limits/Pullbacks/Categorical/CatCospanTransform): equivalences of categorical cospans merge-conflict blocked-by-other-PR t-category-theory large-import blocked on another PR
26578 robin-carlier feat(CategoryTheory/Limits/Pullbacks/Categorical/CatCospanTransform): adjunctions of categorical cospans merge-conflict t-category-theory large-import merge conflict
27634 agjftucker fix(Analysis/Calculus/Implicit): consistently rename {`map`, `fun`, `function`} to `fun` merge-conflict blocked-by-other-PR t-analysis blocked on another PR
28245 robin-carlier feat(CategoryTheory/Bicategory/NaturalTransformation/Icon): strict associativity and unitality of icon composition WIP blocked-by-other-PR t-category-theory awaiting-CI large-import merge-conflict blocked on another PR
30079 dagurtomas feat(CategoryTheory): IsSheafFor as a multiequalizer condition WIP t-category-theory labelled WIP
29012 grunweg chore: reduce `Topology` imports in `Data` merge-conflict file-removed failing CI
26601 yuma-mizuno feat(CategoryTheory): make `Functor.comp` irreducible merge-conflict WIP t-category-theory labelled WIP
25740 robin-carlier feat(AlgebraicTopology/SimplexCategory/GeneratorsRelations): `SimplexCategoryGenRel.toSimplexCategory` is an equivalence merge-conflict t-algebraic-topology blocked-by-other-PR large-import blocked on another PR
23621 astrainfinita chore: deprecate `LinearOrderedComm{Monoid, Group}WithZero` merge-conflict t-algebra t-order ??? opened from a branch in the main mathlib repo (not a fork)
28630 Antidite feat(Archive/Imo): right isosceles configuration in the complex plane IMO awaiting-author new-contributor awaiting author
30192 erdOne feat(RingTheory): valuative topology = adic topology for discrete rank 1 valuations merge-conflict WIP t-ring-theory t-topology labelled WIP
26886 pechersky feat(NumberTheory/Padics/ValuativeRel): ValuativeRel ℚ_[p] WIP t-number-theory blocked-by-other-PR t-algebra merge-conflict t-analysis blocked on another PR
27314 pechersky feat(TopologyValued): `Valued` based on a range topology merge-conflict t-topology blocked-by-other-PR blocked on another PR
30135 erdOne feat(RingTheory): `ValuativeRel` on subrings awaiting-author t-ring-theory awaiting author
28328 pechersky chore(Topology/Valued): golf using local finite order of WithZeroTopology t-number-theory blocked-by-other-PR t-algebra large-import merge-conflict t-topology blocked on another PR
16773 arulandu feat(Probability/Distributions): formalize Beta distribution merge-conflict awaiting-author new-contributor t-measure-probability ??? 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 merge-conflict awaiting-author t-category-theory merge conflict
21853 smmercuri feat: the adele ring of a number field is locally compact merge-conflict WIP 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 t-number-theory t-algebra awaiting-CI merge-conflict labelled WIP
27302 tristan-f-r feat(Fintype/Quotient): finLiftOn₂ awaiting-author t-data awaiting author
28925 grunweg chore: remove `linear_combination'` tactic merge-conflict file-removed awaiting-zulip awaiting a zulip discussion
29432 lecopivo feat: `data_synth` tactic to prove `HasFDerivAt 𝕜 f ?f' x` and similar WIP t-meta labelled WIP
29855 eric-wieser chore(Data/Finset/Sort): lemmas about `0 : Fin _` and `Fin.last _` t-data t-order delegated easy 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 merge-conflict t-algebra awaiting-author t-number-theory ??? 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 merge-conflict WIP t-category-theory awaiting-CI labelled WIP
30460 janithamalith feat(Nat): add lemma nat_card_orbit_mul_card_stabilizer_eq_card_group awaiting-author t-group-theory new-contributor awaiting author
25737 robin-carlier feat(AlgebraicTopology/SimplexCategory/GeneratorsRelations/NormalForms): Normal forms for `P_δ`s t-algebraic-topology delegated t-category-theory failing CI
30209 Ruben-VandeVelde feat: some TwoSidedIdeal.span lemmas awaiting-author t-ring-theory FLT awaiting author
25225 xcloudyunx feat(Combinatorics/SimpleGraph): Eulerian walk in connected graph contains all vertices awaiting-author t-combinatorics new-contributor ??? 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` t-data new-contributor failing CI
25978 Bergschaf feat(Order/Sublocale): Open Sublocales merge-conflict t-order merge conflict
29355 girving feat(Trigonometric): Taylor series bounds for sin and cos merge-conflict t-analysis failing CI
28298 thorimur chore: dedent `to_additive` docstrings merge-conflict documentation awaiting-author merge conflict
28737 astrainfinita refactor: deprecate `MulEquivClass` merge-conflict awaiting-author t-algebra merge conflict
28676 sun123zxy feat(NumberTheory/ArithmeticFunction): wrap `Nat.totient` as an `ArithmeticFunction` t-number-theory new-contributor large-import merge-conflict awaiting-author merge conflict
30299 franv314 feat(Topology/Instances): Cantor set new-contributor merge-conflict file-removed awaiting-author t-topology merge conflict
30303 franv314 chore(Topology/Instances): add deprecated module merge-conflict blocked-by-other-PR new-contributor blocked on another PR
27976 smmercuri feat: `ramificationIdx` for `NumberField.InfinitePlace` merge-conflict WIP t-number-theory labelled WIP
30975 mariainesdff feat(Data/Finsupp/Defs): add Finsupp.restrict awaiting-author t-data awaiting author
26357 javra feat(CategoryTheory): linear categories as `ModuleCat R`-enriched categories merge-conflict awaiting-author t-category-theory large-import merge conflict
26085 grunweg feat: disjoint unions distribute with products of manifolds please-adopt WIP t-differential-geometry merge-conflict looking for help
27180 ADedecker feat: quotient of a monoid with zero by a multiplicative congruence merge-conflict t-algebra delegated 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` merge-conflict awaiting-author 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 merge-conflict WIP t-category-theory labelled WIP
22361 rudynicolop feat(Computability/NFA): nfa closure properties new-contributor t-computability merge-conflict awaiting-author awaiting-zulip ??? opened from a branch in the main mathlib repo (not a fork)
30158 nicolaviolette feat: combinatorics simplegraph basic awaiting-author t-combinatorics new-contributor awaiting author
27708 vihdzp feat: unions and intersections of ordinals are ordinals merge-conflict awaiting-author t-set-theory merge conflict
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 merge-conflict blocked-by-other-PR large-import t-measure-probability blocked on another PR
29992 vlad902 feat(Order): finite (Max)Chains always contains a top/max element merge-conflict WIP t-order large-import labelled WIP
26901 5hv5hvnk feat: a simproc version of `compute_degree` awaiting-CI new-contributor merge-conflict awaiting-author t-meta does not pass CI
31020 grunweg feat: mfderiv of Sum.inl and Sum.inr merge-conflict WIP ⚠️ labelled WIP
28685 mitchell-horner feat(Combinatorics/SimpleGraph): prove the minimal-degree version of the Erdős-Stone theorem merge-conflict WIP blocked-by-other-PR t-combinatorics blocked on another PR
25775 emilyriehl feat(AlgebraicTopology/SimplicialSet/NerveAdjunction): to Strict Segal 2 t-algebraic-topology t-category-theory merge-conflict awaiting-author infinity-cosmos failing CI
14752 AntoineChambert-Loir fix(Topology/Algebra/Valued): repair definition of Valued merge-conflict WIP t-topology t-algebra ??? 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-algebra t-number-theory t-analysis merge conflict
29458 LiamSchilling feat(MvPolynomial/WeightedHomogenous): relate `weightedTotalDegree` to `degrees` and `degreeOf` awaiting-author t-ring-theory new-contributor awaiting author
30150 imbrem feat(CategoryTheory/Monoidal): to_additive for MonoidalCategory t-category-theory large-import new-contributor merge-conflict awaiting-zulip t-meta awaiting a zulip discussion
25765 JovanGerb feat(gcongr): lemma for rewriting inside divisibility delegated t-data delegated
30824 grunweg wip: another smoothness lemma for local frames merge-conflict WIP t-differential-geometry labelled WIP
30322 kckennylau feat(RingTheory): base change of graded algebra merge-conflict awaiting-author t-ring-theory merge conflict
31593 Ruben-VandeVelde feat: some lemmas about MonoidAlgebra merge-conflict awaiting-author t-algebra merge conflict
31596 grunweg chore: remove extraneous uses of push_neg merge-conflict WIP labelled WIP
26885 pechersky feat(Topology/ValuativeRel): ValuativeTopology 𝒪[K] t-algebra t-number-theory t-topology failing CI
15651 TpmKranz feat(Computability/NFA): operations for Thompson's construction new-contributor t-computability merge-conflict awaiting-author 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 merge-conflict WIP t-algebra RFC ??? opened from a branch in the main mathlib repo (not a fork)
22464 adomani feat(CI): declarations diff in Lean awaiting-author CI ??? opened from a branch in the main mathlib repo (not a fork)
27392 Paul-Lez feat(Tactic/SimpUtils): add simproc finding commands large-import merge-conflict file-removed awaiting-author t-meta failing CI
15649 TpmKranz feat(Computability): introduce Generalised NFA as bridge to Regular Expression new-contributor t-computability merge-conflict awaiting-author awaiting-zulip ??? opened from a branch in the main mathlib repo (not a fork)
20238 maemre feat(Computability/DFA): Closure of regular languages under some set operations new-contributor t-computability merge-conflict awaiting-author 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 merge-conflict awaiting-author t-meta ??? opened from a branch in the main mathlib repo (not a fork)
5863 eric-wieser feat: add elaborators for concrete matrices merge-conflict help-wanted blocked-by-other-PR t-meta opened from a branch in the main mathlib repo (not a fork)
5919 MithicSpirit feat: implement orthogonality for AffineSubspace WIP new-contributor merge-conflict help-wanted t-analysis ??? opened from a branch in the main mathlib repo (not a fork)
7386 madvorak feat: Define linear programs merge-conflict WIP t-algebra RFC ??? opened from a branch in the main mathlib repo (not a fork)
9352 chenyili0818 feat: arithmetic lemmas for `gradient` merge-conflict awaiting-author 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 merge-conflict awaiting-author 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 merge-conflict WIP awaiting-author t-algebra opened from a branch in the main mathlib repo (not a fork)
10977 grunweg feat: germs of smooth functions t-differential-geometry merge-conflict awaiting-author 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) merge-conflict awaiting-author t-logic ??? opened from a branch in the main mathlib repo (not a fork)
11890 adomani feat: the terminal refine linter merge-conflict t-linter awaiting-author ??? opened from a branch in the main mathlib repo (not a fork)
12006 adomani feat: the `suffa` tactic merge-conflict awaiting-author t-meta ??? opened from a branch in the main mathlib repo (not a fork)
13442 dignissimus feat: mabel tactic for multiplicative abelian groups new-contributor merge-conflict modifies-tactic-syntax awaiting-author help-wanted t-meta 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 merge-conflict awaiting-author 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 merge-conflict awaiting-author 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 merge-conflict awaiting-author 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 merge-conflict awaiting-author 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 merge-conflict awaiting-author 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 merge-conflict awaiting-author 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 merge-conflict awaiting-author 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 t-algebra t-category-theory awaiting-CI merge-conflict awaiting-author 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 merge-conflict awaiting-author 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 merge-conflict blocked-by-other-PR t-logic ??? opened from a branch in the main mathlib repo (not a fork)
19323 madvorak feat: Function to Sum decomposition merge-conflict WIP t-data ??? opened from a branch in the main mathlib repo (not a fork)
19378 adamtopaz feat: Explanation widgets merge-conflict awaiting-author 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 t-order t-data merge-conflict t-algebraic-geometry opened from a branch in the main mathlib repo (not a fork)
20051 Timeroot feat: `Clone` and some instances merge-conflict awaiting-author t-algebra blocked-by-other-PR 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 merge-conflict awaiting-author t-data ??? opened from a branch in the main mathlib repo (not a fork)
20648 anthonyde feat: formalize regular expression -> εNFA merge-conflict t-computability awaiting-zulip new-contributor ??? 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 large-import merge-conflict t-combinatorics t-logic opened from a branch in the main mathlib repo (not a fork)
20652 jjaassoonn feat: categorical description of center of a ring merge-conflict awaiting-author t-algebra t-category-theory 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 merge-conflict t-computability blocked-by-other-PR opened from a branch in the main mathlib repo (not a fork)
21270 GabinKolly feat(ModelTheory/Bundled): first-order embeddings and equivalences from equalities merge-conflict awaiting-author large-import t-logic ??? 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 merge-conflict blocked-by-other-PR t-logic ??? opened from a branch in the main mathlib repo (not a fork)
21616 peabrainiac feat(Topology): concatenating countably many paths merge-conflict awaiting-author 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 merge-conflict awaiting-author 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 merge-conflict awaiting-author 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 t-algebra new-contributor awaiting-CI large-import merge-conflict opened from a branch in the main mathlib repo (not a fork)
22159 shetzl feat: add definition of pushdown automata merge-conflict t-computability awaiting-author new-contributor ??? opened from a branch in the main mathlib repo (not a fork)
22231 pechersky feat(Algebra/Valued): `AdicExpansion` initial defns merge-conflict t-algebra awaiting-author t-topology ??? opened from a branch in the main mathlib repo (not a fork)
22232 pechersky feat(Algebra/Valued): `AdicExpansion.apprUpto` merge-conflict t-topology blocked-by-other-PR opened from a branch in the main mathlib repo (not a fork)
22233 pechersky feat(Algebra/Valued): `AdicExpansion.evalAt` merge-conflict t-topology blocked-by-other-PR ??? opened from a branch in the main mathlib repo (not a fork)
22302 658060 feat: add `CategoryTheory.Topos.Power` merge-conflict awaiting-author 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 merge-conflict t-computability awaiting-author new-contributor ??? 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` merge-conflict awaiting-author 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 merge-conflict awaiting-author 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 merge-conflict awaiting-author 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 t-algebra t-category-theory large-import merge-conflict opened from a branch in the main mathlib repo (not a fork)
23460 Timeroot feat: Definition of `Clone` merge-conflict t-algebra blocked-by-other-PR ??? opened from a branch in the main mathlib repo (not a fork)
23503 apnelson1 feat(Topology/Instances/ENat): ENat and tsum merge-conflict WIP t-topology large-import ??? opened from a branch in the main mathlib repo (not a fork)
23585 plp127 feat: `Filter.atMax` and `Filter.atMin` merge-conflict WIP t-order ??? opened from a branch in the main mathlib repo (not a fork)
23758 erdOne feat(Topology/Algebra): linearly topologized iff non-archimedean t-algebra large-import merge-conflict awaiting-author t-topology ??? 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 merge-conflict awaiting-author 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 merge-conflict awaiting-author 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 merge-conflict awaiting-author 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 merge-conflict awaiting-author 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 merge-conflict t-linter awaiting-author 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 merge-conflict awaiting-author t-number-theory new-contributor merge conflict
25974 scholzhannah feat(Topology/Compactness/CompactlyCoherentSpace): compact coherentification (k-ification) merge-conflict t-topology large-import merge conflict
26051 Komyyy feat(Mathlib/GroupTheory/SpecificGroups/Alternating): A_n is simple iff n = 3 or 5 ≤ n merge-conflict WIP t-group-theory large-import labelled WIP
26165 oliver-butterley feat(MeasureTheory.VectorMeasure): add lemma which shows that variation of a `ℝ≥0∞` VectorMeasure is equal to itself merge-conflict blocked-by-other-PR new-contributor t-measure-probability blocked on another PR
26300 igorkhavkine feat(Analysis/Calculus/FDeriv): continuous differentiability from continuous partial derivatives on an open domain in a product space WIP new-contributor merge-conflict awaiting-author t-analysis labelled WIP
26329 Timeroot feat: Definition of `Clone` notations and typeclasses merge-conflict awaiting-author t-algebra awaiting-CI does not pass CI
26398 ChrisHughes24 feat(ModelTheory): definable functions please-adopt merge-conflict t-logic looking for help
26399 ChrisHughes24 refactor(ModelTheory): tidy up proof of Ax-Grothendieck with definable functions merge-conflict blocked-by-other-PR t-logic blocked on another PR
26432 AntoineChambert-Loir feat(Data.Nat.LogFueled): fueled version of `clog` merge-conflict t-data failing CI
26594 metakunt feat(Algebra/Polynomial/ZMod): Add Polynomial.equiv_of_nat_of_polynomial_zmod merge-conflict awaiting-author t-algebra new-contributor merge conflict
26644 kckennylau feat(SetTheory/ZFC): Define the language of sets and state the ZFC axioms merge-conflict awaiting-author t-set-theory merge conflict
26648 eric-wieser chore(TensorProduct): remove more `suppress_compilation`s merge-conflict blocked-by-core-PR t-algebra opened from a branch in the main mathlib repo (not a fork)
26757 fweth feat(CategoryTheory/Topos): define elementary topos merge-conflict awaiting-author 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 merge-conflict WIP t-category-theory t-meta labelled WIP
26942 pechersky feat(RingTheory/Valuation/ValueGroupIso): isomorphism of value groups when compatible merge-conflict t-ring-theory blocked-by-other-PR t-order blocked on another PR
26990 joelriou feat(CategoryTheory/Abelian): Noetherian objects form a Serre class merge-conflict WIP t-category-theory labelled WIP
27098 Paul-Lez feat(Algebra/Category/ModuleCat/Sheaf/VectorBundle): define vector bundles merge-conflict awaiting-author t-algebra merge conflict
27155 Pjotr5 feat: Shearer's bound on the independence number of triangle free graphs merge-conflict awaiting-author t-combinatorics new-contributor failing CI
27163 pechersky feat(Topology/ValuativeRel): of and to basis of compatible valuations t-number-theory t-algebra merge-conflict awaiting-author t-topology merge conflict
27187 Komyyy feat: `NONote` represents ordinals < ε₀ merge-conflict WIP t-set-theory labelled WIP
27215 kckennylau feat(AlgebraicGeometry): Define the Zariski site on `CommRingCatᵒᵖ` merge-conflict awaiting-author t-algebraic-geometry merge conflict
27309 kckennylau feat(CategoryTheory): a presheaf on `CostructuredArrow F d` can be extended to a presheaf on `C` merge-conflict WIP t-category-theory labelled WIP
27321 kckennylau feat(CategoryTheory): Colimit can be computed fiberwise merge-conflict t-category-theory awaiting-CI does not pass CI
27417 PierreQuinton feat: add `SigmaCompleteLattice` merge-conflict awaiting-author t-order merge conflict
27534 PierreQuinton feat: a typeclass for `sSup`/`sInf` to be lawful merge-conflict t-order merge conflict
27753 YunkaiZhang233 feat(CategoryTheory): implemented proofs for factorisation categories being equivalent to iterated comma categories in two ways merge-conflict awaiting-author t-category-theory new-contributor merge conflict
27824 ChrisHughes24 feat(Calculus): exists_gt_of_deriv_pos and variants merge-conflict awaiting-author t-analysis merge conflict
27850 fyqing feat: 0-dimensional manifolds are discrete and countable merge-conflict awaiting-author t-differential-geometry new-contributor merge conflict
27973 smmercuri feat: the ring of integers of a `ℤₘ₀`-valued field is compact whenever it is a DVR and the residue field is finite merge-conflict awaiting-author t-algebra large-import merge conflict
28072 kckennylau feat(RingTheory/Valuation): make tactic rw_val_equiv merge-conflict awaiting-author t-ring-theory merge conflict
28124 kckennylau feat(Tactic): Call an arbitrary Simproc merge-conflict t-meta failing CI
28125 nonisomorphiclinearmap feat(Combinatorics): basic definition of simplicial complexes merge-conflict t-combinatorics new-contributor merge conflict
28316 eric-wieser feat(Tactic/NormNum): better trace nodes merge-conflict t-meta 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 merge-conflict awaiting-author t-meta merge conflict
28530 nonisomorphiclinearmap feat(Combinatorics/SimplicialComplex/Topology): add standard simplices and geometric realisation (colimit + functoriality) merge-conflict blocked-by-other-PR t-combinatorics new-contributor blocked on another PR
28868 yury-harmonic feat(Positive): add `OfNat` instance merge-conflict t-algebra large-import failing CI
28871 JaafarTanoukhi feat(Combinatorics/Digraph): Tournaments merge-conflict t-combinatorics new-contributor merge conflict
29055 vihdzp feat: `Ordinal.toENat` merge-conflict awaiting-author t-set-theory merge conflict
29108 JonBannon feat(MeasureTheory): add `LInfty.lean` with `Mul` and `const` related results. merge-conflict awaiting-author t-measure-probability merge conflict
29425 pechersky feat(NumberTheory/Padics/Torsion): `HasEnoughRootsOfUnity ℤ_[p] (p - 1)` merge-conflict awaiting-author t-ring-theory blocked-by-other-PR blocked on another PR
29500 vihdzp feat: `WellFoundedLT (LowerSet α)` merge-conflict awaiting-author t-order merge conflict
29526 llllvvuu feat: `Multiset.map f` identifies `f` up to permutation merge-conflict t-data merge conflict
29675 yury-harmonic feat(Wolstenholme): new file merge-conflict awaiting-author help-wanted t-data looking for help
29720 javra feat(CategoryTheory): `TransportEnrichment` and `ForgetEnrichment` as 2-functors merge-conflict WIP t-category-theory labelled WIP
29827 js2357 feat: define two (trivial) ContinuousMulEquivs merge-conflict t-topology FLT large-import failing CI
29947 JaafarTanoukhi feat(Combinatorics/Digraph): Maps merge-conflict t-combinatorics new-contributor merge conflict
30004 luigi-massacci feat(MeasureTheory/Integral/TestAgainst): integrating BCFs against a finite measure or an L1Loc map as CLMs merge-conflict awaiting-author t-analysis t-measure-probability merge conflict
30042 JovanGerb feat(push): `@[push]` attributes for `∈` in `Set`, `Finset` and `Multiset` merge-conflict awaiting-author t-meta merge conflict
30312 kckennylau feat(RingTheory): define graded ring homomorphisms merge-conflict t-ring-theory blocked-by-other-PR blocked on another PR
30334 kckennylau feat(RingTheory): define maps of homogeneous ideals merge-conflict t-ring-theory blocked-by-other-PR blocked on another PR
30355 kckennylau feat(Logic): graded functions merge-conflict t-data merge conflict
30367 kckennylau feat(Data): define grading-preserving isomorphisms merge-conflict blocked-by-other-PR t-data blocked on another PR
30451 kckennylau feat(HomogeneousIdeal): generalize to homogeneous submodule merge-conflict t-ring-theory failing CI
30933 joelriou feat(CategoryTheory): the linearization of a category merge-conflict awaiting-author t-category-theory merge conflict
31194 grunweg feat: add `#check'` command and tactic, which only show explicit arguments merge-conflict awaiting-author t-meta merge conflict
31351 grunweg feat: manifolds with smooth boundary merge-conflict WIP t-differential-geometry labelled WIP
31356 adomani feat: add inspect-like functions merge-conflict t-meta merge conflict
31604 maksym-radziwill feat: analyticity of dslope merge-conflict awaiting-author t-analysis merge conflict
31738 robertmaxton42 feat: quivers can be represented as functors from the walking quiver merge-conflict awaiting-author t-category-theory failing CI
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 t-algebra blocked-by-other-PR 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 merge-conflict WIP 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 merge-conflict WIP ??? opened from a branch in the main mathlib repo (not a fork)
6859 MohanadAhmed feat: TryLean4Bundle: Windows Bundle Creator WIP help-wanted 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 merge-conflict WIP ??? ⚠️ 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 merge-conflict WIP 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 merge-conflict WIP t-algebra RFC ??? 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 merge-conflict WIP t-algebra RFC ??? 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 merge-conflict WIP t-algebraic-topology new-contributor ??? 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 please-adopt merge-conflict t-topology blocked-by-other-PR ??? opened from a branch in the main mathlib repo (not a fork)
12251 ScottCarnahan refactor(RingTheory/HahnSeries): several generalizations merge-conflict WIP 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 please-adopt merge-conflict awaiting-author t-measure-probability opened from a branch in the main mathlib repo (not a fork)
12452 JADekker feat(Cocardinal): add some more api t-topology awaiting-CI ??? opened from a branch in the main mathlib repo (not a fork)
14426 adomani feat: `#min_imps` command (development branch) merge-conflict WIP ??? ⚠️ opened from a branch in the main mathlib repo (not a fork)
14686 smorel394 feat(AlgebraicGeometry/Grassmannian): define the Grassmannian scheme please-adopt WIP workshop-AIM-AG-2024 merge-conflict t-algebraic-geometry ??? opened from a branch in the main mathlib repo (not a fork)
17071 ScottCarnahan feat(LinearAlgebra/RootSystem): separation, base, cartanMatrix merge-conflict WIP 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 t-category-theory large-import merge-conflict t-algebraic-geometry opened from a branch in the main mathlib repo (not a fork)
18626 hannahfechtner feat: define Artin braid groups merge-conflict awaiting-author t-algebra new-contributor ??? opened from a branch in the main mathlib repo (not a fork)
18784 erdOne feat(AlgebraicGeometry): use `addMorphismPropertyInstances` merge-conflict t-algebraic-geometry blocked-by-other-PR 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 merge-conflict WIP blocked-by-other-PR ⚠️ 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 merge-conflict WIP new-contributor t-meta ??? 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 t-category-theory new-contributor merge-conflict awaiting-author ??? opened from a branch in the main mathlib repo (not a fork)
22805 ScottCarnahan feat(FieldTheory/Finite): fixed points of Frobenius automorphism merge-conflict WIP 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 merge-conflict awaiting-author 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 merge-conflict WIP 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 merge-conflict WIP 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 merge-conflict WIP t-ring-theory labelled WIP
25906 pfaffelh feat(Topology/Compactness/CompactSystem): closed and compact square cylinders form a compact system merge-conflict t-topology blocked-by-other-PR blocked on another PR
25900 pfaffelh feat(Topology/Compactness/CompactSystem): set system of finite unions of sets in a compact system is again a compact system merge-conflict t-topology blocked-by-other-PR blocked on another PR
26455 ScottCarnahan feat(LinearAlgebra/RootSystem): API for CartanMatrix merge-conflict WIP t-algebra labelled WIP
26804 kckennylau feat(SetTheory): ZFSet is a model of ZFC merge-conflict WIP t-set-theory labelled WIP
26881 emo916math feat(Analysis/Calculus/Deriv/Star): a formula for `deriv (conj ∘ f ∘ conj)` awaiting-author t-analysis new-contributor awaiting author
26890 robin-carlier feat(CategoryTheory/Monoidal/DayConvolution): more API for `DayFunctor` merge-conflict t-category-theory merge conflict
26310 kckennylau feat: binary forms merge-conflict awaiting-author t-algebra merge conflict
26283 kckennylau feat: resultant of polynomials merge-conflict WIP t-algebra labelled WIP
27991 sinianluoye feat(Rat): add Rat.den_eq_of_add_den_eq_one and its dependent lemmas awaiting-author t-data new-contributor failing CI
28215 5hv5hvnk feat: strong and Weak connectivity for Digraphs WIP new-contributor merge-conflict awaiting-author t-combinatorics labelled WIP
28970 Whysoserioushah feat(Algebra/Algebra/ReducedNorm): defines reduced norm and trace merge-conflict awaiting-author t-algebra merge conflict
29212 Whysoserioushah feat(Algebra/CrossProductAlgebra/Defs): define Cross Product Algebra merge-conflict awaiting-author t-algebra merge conflict
29514 grunweg feat(CI): use more strict mode merge-conflict WIP CI labelled WIP
29574 JarodAlper feat: regular local rings are domains merge-conflict t-ring-theory new-contributor failing CI
28718 imbrem feat: class for chosen finite coproducts blocked-by-other-PR t-category-theory new-contributor merge-conflict awaiting-author blocked on another PR
30352 kckennylau feat(RingTheory): Homogeneous localization of tensor product merge-conflict WIP blocked-by-other-PR ⚠️ blocked on another PR
30366 sinhp feat(CategoryTheory): The Preliminaries for Locally Cartesian Closed Categories merge-conflict awaiting-author t-category-theory merge conflict
26765 KiringYJ feat(MeasureTheory/PiSystem): add π-λ theorem and SetLike instance awaiting-author t-measure-probability new-contributor awaiting author
29409 Julian feat(Mathlib/Analysis): deriv_eq_self and deriv_exp_iff awaiting-author t-analysis awaiting author
31513 FLDutchmann feat(Tactic): `polynomial` tactic merge-conflict blocked-by-other-PR t-meta blocked on another PR
27306 xyzw12345 feat: `lie_ring` tactic and `LieReduce` command t-meta failing CI
29434 ntapiam feat(NonAssoc/LieAdmissible): prove every ring/algebra is LieAdmissible t-algebra new-contributor failing CI
27694 grunweg feat: Gram-Schmidt orthonormalisation preserves continuity of sections merge-conflict t-differential-geometry blocked-by-other-PR blocked on another PR
27025 grunweg feat: Gram-Schmidt procedure on smooth vector bundles yields smooth sections merge-conflict t-differential-geometry blocked-by-other-PR blocked on another PR
30637 strihanje01 feat(Combinatorics/SetFamily/Lindstrom): Lindstrom's theorem for subfamilies with equal unions t-combinatorics new-contributor failing CI
31949 ADedecker chore: prefer `Pi.single i 1 j` over `fun j => if i = j then 1 else 0` t-algebra awaiting-author awaiting author
25902 pfaffelh feat: The finite product of semi-rings (in terms of measure theory) is a semi-ring. t-measure-probability brownian large-import merge-conflict awaiting-author merge conflict
31571 erdOne feat(RingTheory): existence of local algebra with given residue field awaiting-author t-ring-theory awaiting author
29517 pechersky feat(RingTheory/Torsion): torsion = union of roots of unity merge-conflict awaiting-author t-algebra failing CI
31176 mcdoll feat(Analysis): Taylor's theorem with the integral remainder t-analysis awaiting-author awaiting author
28933 artie2000 chore(Data): correct definition for `single_apply` merge-conflict WIP labelled WIP
24627 pechersky feat(Topology/Algebra/Valued): `IsLinearTopology 𝒪[K] K` and `𝒪[K] 𝒪[K]` merge-conflict awaiting-author t-topology opened from a branch in the main mathlib repo (not a fork)
27756 grunweg feat: `Weak(Pseudo)EMetricSpace`, generalises `(Pseudo)EMetricSpace` merge-conflict WIP t-topology carleson labelled WIP
31817 kckennylau chore: remove extra monic hypotheses from divByMonic and modByMonic lemmas t-algebra t-ring-theory awaiting-author failing CI
24016 plp127 feat: fine uniformity merge-conflict t-topology ??? opened from a branch in the main mathlib repo (not a fork)
30995 kckennylau feat(RingTheory): replace ofLinearEquiv with limit t-ring-theory awaiting-author awaiting author
32094 grunweg feat(runLinter): allow only running certain linters t-linter CI failing CI
32095 grunweg chore: fix some explicitVarOfIff linter errors please-adopt WIP merge-conflict looking for help
29982 hrmacbeth feat: new `isolate` tactic merge-conflict awaiting-author large-import t-meta failing CI
31796 dobronx1325 feat(Data/Real/EReal): add mul_lt_mul_of_pos_left theorem t-data new-contributor failing CI
27258 JovanGerb feat: Imo2020 q6 IMO awaiting-author awaiting author
26138 xroblot Development branch (2) WIP merge-conflict labelled WIP
31729 thorimur chore: log on theorem type signature in unused instances in type linters merge-conflict blocked-by-other-PR large-import blocked on another PR
32157 peabrainiac feat(Analysis/Calculus): Hadamard's lemma t-analysis blocked-by-other-PR blocked on another PR
26436 AntoineChambert-Loir feat(Mathlib/Data/Nat/Prime/Defs): fuel Nat.minFac merge-conflict t-data awaiting-author failing CI
24514 b-mehta chore(Int/GCD): use fuel in xgcd awaiting-author t-data merge-conflict ??? opened from a branch in the main mathlib repo (not a fork)
32169 saodimao20 feat: add convolution_comp_add_right t-analysis new-contributor awaiting-author awaiting author
31132 kckennylau feat(Algebra): saturation of a submonoid t-algebra failing CI
28244 robin-carlier feat(CategoryTheory/Bicategory/NaturalTransformation): Icons WIP blocked-by-other-PR t-category-theory awaiting-CI large-import merge-conflict blocked on another PR
29933 smmercuri chore: fix `def` naming isses in `Normed/Field/WithAbs.lean` WIP merge-conflict labelled WIP
27980 smmercuri feat: dimensions of completions at infinite place extensions t-number-theory blocked-by-other-PR large-import merge-conflict FLT blocked on another PR
31350 grunweg feat: (unoriented) bordism groups merge-conflict WIP t-differential-geometry blocked-by-other-PR blocked on another PR
26389 jjdishere feat(RingTheory): Perfectoid Field t-algebra WIP t-topology t-analysis labelled WIP
26390 jjdishere feat(Topology/Algebra): Krasner's lemma WIP t-number-theory t-algebra t-topology labelled WIP
32285 awainverse chore(ModelTheory/Bundled): Replace CategoryTheory.Bundled t-logic awaiting-author awaiting author
31663 xroblot feat(Algebra): more instances about `min`, `max`, `iSup` and `iInf` of sub-algebras t-algebra WIP labelled WIP
31950 callesonne feat(CategoryTheory/Product/Basic): make `Hom` into a 1-field structure WIP t-category-theory merge-conflict labelled WIP
27579 RemyDegenne feat: risk of an estimator, DeGroot statistical information, total variation distance WIP large-import t-measure-probability labelled WIP
29315 kbuzzard chore: raise priority of `IsTopologicalSemiring.toIsModuleTopology` awaiting-author t-topology failing CI
30551 smmercuri feat: dimension formulae for infinite places above WIP blocked-by-other-PR merge-conflict ⚠️ blocked on another PR
31730 thorimur feat(Meta): declaration manipulation meta API: allow logging on type signature of theorems t-meta failing CI
31242 plp127 feat: express filter as supremum of principal filter and free filter t-order awaiting-author merge-conflict merge conflict
32474 mattrobball perf(Module.LinearMap.Defs): deprioritize projections to parents for SemilinearMapClass t-algebra failing CI
31898 ntapiam feat(LinearAlgebra/TensorAlgebra): implement HopfAlgebra for TensorAlgebra new-contributor t-ring-theory awaiting-author failing CI
31597 grunweg chore(AtLocation): allow throwing a warning when no progress is being made awaiting-author t-meta merge-conflict merge conflict
30525 515801431 feat(Mathlib/Combinatorics/Enumerative/Polya): Add Polya Counting t-combinatorics new-contributor awaiting-author merge-conflict merge conflict
31113 515801431 feat(Mathlib/Combinatorics/Enumerative/Polya.lean): Add additional theorem in `Polya.lean` t-combinatorics new-contributor blocked-by-other-PR merge-conflict blocked on another PR
24441 MrSumato feat(Data/List): add Lyndon-Schutzenberger theorem on list commutativity merge-conflict awaiting-author t-data new-contributor ??? 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 t-order merge-conflict merge conflict
31901 callesonne feat(Bicategory/Subbicategory): add full subbicategories using `ObjectProperty` t-category-theory awaiting-author awaiting author
32473 mattrobball chore(Kaehler.JacobiZariski): remove egregious local instance hack t-ring-theory awaiting-author opened from a branch in the main mathlib repo (not a fork)
18551 joelriou feat(AlgebraicGeometry): the algebraic De Rham complex WIP t-algebra blocked-by-other-PR merge-conflict t-algebraic-geometry 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 t-dynamics new-contributor awaiting-author awaiting author
30119 Ruben-VandeVelde feat: WithTop/Bot.mapD awaiting-author t-order merge-conflict merge conflict
28613 espottesmith feat(Combinatorics): define undirected hypergraphs t-combinatorics new-contributor merge-conflict failing CI
23040 grunweg feat: define immersions and smooth embeddings in infinite dimensions merge-conflict WIP t-differential-geometry blocked-by-other-PR opened from a branch in the main mathlib repo (not a fork)
26231 chrisflav feat(CategoryTheory/Sites): sheaf condition and coproducts awaiting-author t-category-theory WIP labelled WIP
30668 astrainfinita feat: `QuotType` RFC t-data awaiting-zulip awaiting a zulip discussion
30847 joelriou feat(CategoryTheory/Presentable): the representation theorem WIP blocked-by-other-PR t-category-theory merge-conflict blocked on another PR
30817 joelriou feat(CategoryTheory): `κ`-continuous presheaves WIP t-category-theory blocked-by-other-PR blocked on another PR
6633 adomani feat(..Polynomial..): `MvPolynomial`s have no zero divisors merge-conflict awaiting-author 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 merge-conflict WIP t-differential-geometry blocked-by-other-PR blocked on another PR
31987 saodimao20 feat: add monotonicity and relation lemmas for mgf and cgf t-measure-probability new-contributor awaiting-author awaiting author
32211 ADedecker feat: inclusion from `ContDiffMapSupportedIn` to `TestFunction` is a topological embedding t-analysis blocked-by-other-PR merge-conflict blocked on another PR
32602 adamtopaz feat: Refactor graph WIP ⚠️ labelled WIP
26912 pechersky chore(Algebra/Ring/Subring): simp tag `Subring.smul_def` merge-conflict t-algebra merge conflict
32737 j-loreaux refactor: rename `MulAction` to `MonoidAction` merge-conflict failing CI
30240 luigi-massacci feat(Analysis/Distribution/ContDiffMapSupportedIn): Add a wrapper for fderiv on D_K^n t-analysis awaiting-author awaiting author
29274 Jlh18 feat(CategoryTheory): HasLimits instance on Grpd file-removed blocked-by-other-PR t-category-theory merge-conflict blocked on another PR
29283 Jlh18 feat(CategoryTheory): define forgetful-core adjunction between Cat and Grpd file-removed t-category-theory awaiting-author merge-conflict merge conflict
21447 erdOne feat(AlgebraicGeometry): the split algebraic torus merge-conflict awaiting-author t-algebraic-geometry ??? opened from a branch in the main mathlib repo (not a fork)
25963 artie2000 refactor(Algebra): uniform API for substructures merge-conflict WIP t-algebra labelled WIP
32938 0xTerencePrime feat(Order/LocallyFinite): prove DenselyOrdered and LocallyFiniteOrder are incompatible t-order new-contributor awaiting-author awaiting author
33077 YaelDillies feat(Data/Rel): balls WIP t-data labelled WIP
31226 erdOne chore(RingTheory): add `@[ext]` to `Ideal.Quotient.algHom_ext` awaiting-author t-ring-theory easy merge-conflict merge conflict
21495 alreadydone experiment: reducible HasQuotient.quotient' WIP bench-after-CI merge-conflict 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 t-data new-contributor awaiting-author awaiting author
27817 zhuyizheng feat: add IMO2025P1 IMO awaiting-author new-contributor merge-conflict merge conflict
26923 oliver-butterley feat(Dynamics/BirkhoffSum): add the pointwise ergodic theorem (Birkhoff's) t-dynamics new-contributor awaiting-author failing CI
33218 Blackfeather007 feat(Algebra): Define the associated graded ring to filtered ring t-ring-theory new-contributor blocked-by-other-PR blocked on another PR
33219 Blackfeather007 feat(Algebra): Define associated graded algebra t-ring-theory new-contributor blocked-by-other-PR blocked on another PR
33220 Blackfeather007 feat(Algebra): Define associated graded module t-ring-theory new-contributor blocked-by-other-PR blocked on another PR
33227 Blackfeather007 feat(Algebra): exact of associated graded exact t-ring-theory new-contributor blocked-by-other-PR blocked on another PR
33226 Blackfeather007 feat(Algebra): associated graded exact of exact and strict t-ring-theory new-contributor blocked-by-other-PR blocked on another PR
33225 Blackfeather007 feat(Algebra): filtered module hom t-ring-theory new-contributor blocked-by-other-PR blocked on another PR
33224 Blackfeather007 feat(Algebra): define filtered alghom t-ring-theory new-contributor blocked-by-other-PR blocked on another PR
33223 Blackfeather007 feat(Algebra): define filtered ring homomorphism t-ring-theory new-contributor blocked-by-other-PR blocked on another PR
33222 Blackfeather007 feat(Algebra): define filtered add group hom new-contributor t-ring-theory blocked-by-other-PR blocked on another PR
33134 faenuccio feat(Normed/Module/WeakDual): add Goldstine lemma WIP t-analysis labelled WIP
33178 gw90 feat(Analysis/CStarAlgebra/Spectrum): Adding lemmas that the CStarAlgebra norm equals the square root of the spectral radius of star a * a new-contributor t-analysis awaiting-author awaiting author
33138 gasparattila chore(MeasureTheory/Measure/Stieltjes): remove `backward.privateInPublic` t-measure-probability tech debt awaiting-author 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 large-import t-combinatorics blocked-by-other-PR blocked on another PR
5934 eric-wieser feat: port Data.Rat.MetaDefs merge-conflict help-wanted mathlib-port t-meta ??? 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 please-adopt WIP t-algebra merge-conflict ??? 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 merge-conflict awaiting-author 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 t-order merge-conflict failing CI
32921 faenuccio refactor Submodule.map WIP awaiting-author t-algebra merge-conflict labelled WIP
32889 artie2000 feat(Algebra): forgetful lemmas for `map` and `comap` on substructures t-algebra awaiting-author blocked-by-other-PR merge-conflict blocked on another PR
32960 dleijnse feat(FieldTheory): adjoin pth roots t-algebra new-contributor awaiting-author awaiting author
33163 Aaron1011 feat: prove subgroup of (M -> Z) is finitely generated t-ring-theory new-contributor awaiting-author awaiting author
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 t-algebra t-analysis awaiting-author awaiting author
14444 digama0 fix(GeneralizeProofs): unreachable! bug merge-conflict awaiting-author 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` t-algebra awaiting-author merge-conflict 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 t-algebraic-topology WIP RFC labelled WIP
24665 Komyyy feat(Mathlib/Topology/Metrizable/Uniformity): every uniform space is generated by a family of pseudometrics WIP t-topology merge-conflict ??? opened from a branch in the main mathlib repo (not a fork)
33381 urkud feat: add a version of the Schwarz lemma t-analysis blocked-by-other-PR merge-conflict blocked on another PR
33448 astrainfinita refactor: deprecate `ContinuousLinearMapClass` t-topology t-algebra awaiting-author 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 t-category-theory awaiting-author awaiting author
32840 joelriou chore(CategoryTheory): remove the old Ext API file-removed t-category-theory large-import merge-conflict WIP labelled WIP
33133 0xTerencePrime feat(Algebra/Group/Center): add Decidable (IsMulCentral a) instance t-algebra new-contributor awaiting-author awaiting author
33191 sinhp feat(CategoryTheory): Locally cartesian closed structure on presheaf categories WIP t-category-theory blocked-by-other-PR merge-conflict ??? blocked on another PR
28153 kckennylau feat(Simproc): Simproc for explicit diagonal matrices merge-conflict awaiting-author t-meta merge conflict
25500 eric-wieser feat: delaborators for metadata large-import merge-conflict awaiting-author delegated t-meta opened from a branch in the main mathlib repo (not a fork)
28191 kckennylau feat(Logic): tag Injective, Surjective, and Bijective with fun_prop merge-conflict awaiting-author t-meta merge conflict
30432 kckennylau feat(AlgebraicGeometry): define the non-vanishing locus of a set in Proj awaiting-author t-algebraic-geometry awaiting author
27262 Timeroot feat(Tactic/Bound): bound? for proof scripts awaiting-author t-meta failing CI
32389 LLaurance feat(Analysis): Trigonometric identities t-analysis awaiting-author awaiting author
33502 MrQubo fix(Tactic/ProxyType): Pass params explicitly in proxy_equiv% implementation new-contributor t-meta WIP labelled WIP
22657 Xmask19 feat: a graph is maximally acyclic iff it is a tree merge-conflict t-combinatorics new-contributor opened from a branch in the main mathlib repo (not a fork)
26368 Whysoserioushah feat(RingTheory/TwoSidedIdeal/SpanAsSum): span of set as finsum merge-conflict awaiting-author t-ring-theory merge conflict
28013 astrainfinita feat: Lindemann-Weierstrass Theorem t-algebra t-analysis awaiting-author merge-conflict 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ᵐᵒᵖ` t-algebra t-group-theory awaiting-author 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 t-category-theory merge-conflict merge conflict
32991 artie2000 chore(Algebra/Algebra): remove `Algebra.cast` coercion t-algebra merge-conflict failing CI
27972 smmercuri refactor: make `Valuation.Completion` a `def` and refactor more of `AdicValuation.lean` WIP t-number-theory t-algebra merge-conflict labelled WIP
17176 arulandu feat: integrals and integrability with .re merge-conflict awaiting-author new-contributor t-measure-probability please-adopt ??? opened from a branch in the main mathlib repo (not a fork)
33010 xgenereux feat: localizations of primes in Dedekind domains are valuation subrings t-ring-theory large-import awaiting-author WIP blocked-by-other-PR blocked on another PR
33454 astrainfinita feat: lemmas about `IsometryClass` t-topology t-analysis awaiting-author awaiting author
13740 YaelDillies feat: more robust ae notation t-meta t-measure-probability awaiting-author 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 t-analysis awaiting-author merge-conflict merge conflict
33368 urkud feat: define `Complex.UnitDisc.shift` t-analysis awaiting-zulip merge-conflict awaiting a zulip discussion
33450 astrainfinita refactor: deprecate `LinearIsometryClass` t-algebra t-analysis blocked-by-other-PR t-topology merge-conflict blocked on another PR
33702 JovanGerb doc(Algebra/Quotient): update `HasQuotient.Quotient` doc-string t-algebra delegated 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 t-analysis awaiting-author merge-conflict merge conflict
33561 kbuzzard chore: cont -> continuous_toFun merge-conflict merge conflict
27507 grunweg wip(commandStart): check the indentation of declaration keywords also WIP t-linter merge-conflict labelled WIP
26088 grunweg chore(Linter/DirectoryDependency): move forbidden directories into a JSON file please-adopt t-linter merge-conflict looking for help
33330 michael-novak-math feat: add arc-length reparametrization of parametrized curves t-analysis new-contributor merge-conflict merge conflict
24010 grunweg feat(Counterexamples): a non-negative function, not a.e. zero, with vanishing lowe… merge-conflict please-adopt WIP blocked-by-other-PR t-measure-probability opened from a branch in the main mathlib repo (not a fork)
28700 Timeroot feat(ModelTheory): Set.Definable is transitive merge-conflict large-import t-logic merge conflict
30608 grunweg feat: another lemma about derivatives of parametric integrals merge-conflict awaiting-author t-analysis merge conflict
30610 grunweg feat: yet another lemma about differentiability of parametric integrals merge-conflict blocked-by-other-PR t-analysis blocked on another PR
33299 kingiler feat: Add decidable membership for Interval awaiting-author new-contributor t-order 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 t-topology new-contributor merge-conflict failing CI
32210 ADedecker feat: iteratedFDeriv as a linear map on test functions merge-conflict t-analysis awaiting-author merge conflict
32401 ADedecker feat: monotonicity of D^n(U) in n and in U as CLMs merge-conflict t-analysis delegated merge conflict
32410 callesonne feat(Bicategory/FunctorCategory/Pseudo): Add evaluation pseudofunctor merge-conflict WIP t-category-theory blocked-by-other-PR blocked on another PR
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 large-import merge-conflict 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 merge-conflict t-ring-theory please-adopt looking for help
25907 mans0954 feat: low order roots of unity t-algebra please-adopt looking for help
26339 mans0954 feat(Analysis/Normed/Module/WeakDual): Banach Dieudonné Lemma merge-conflict WIP t-analysis large-import please-adopt looking for help
26340 mans0954 feat(Algebra/Module/NestAlgebra): Nest algebras merge-conflict t-algebra please-adopt looking for help
26341 mans0954 feat(LinearAlgebra/QuadraticForm/Basis): Free Tensor product of Quadratic Maps merge-conflict WIP t-algebra large-import please-adopt looking for help
33808 seewoo5 feat(Manifold/MFDeriv): add fun_prop to `MDifferentiable` awaiting-author t-differential-geometry awaiting author
26344 mans0954 feat(Analysis/NormedSpace/MStructure): The component projections on WithLp 1 (α × β) are L-projections merge-conflict WIP t-analysis file-removed please-adopt looking for help
26347 mans0954 feat(Data/Finset/RangeDistance): abs_sub_lt_of_mem_finset_range merge-conflict t-data please-adopt looking for help
26349 mans0954 feat(Analysis/SpecialFunctions/Trigonometric/Basic): sin and cos of multiples of π / 3 help-wanted t-analysis please-adopt looking for help
26348 mans0954 feat(Analysis/LocallyConvex/Prime): the prime map merge-conflict WIP t-analysis please-adopt looking for help
26983 mans0954 feat(Order/LatticeElements): distributive, standard and neutral elements of a lattice merge-conflict WIP t-order please-adopt looking for help
29980 mans0954 refactor(RingTheory/Polynomial/Resultant/Quadratic): Re-implement QuadraticDiscriminant for R[X] merge-conflict please-adopt looking for help
29387 mans0954 feat(Analysis/LocallyConvex/WeakSpace): toWeakSpace_closedAbsConvexHull_eq merge-conflict blocked-by-other-PR t-analysis please-adopt blocked on another PR
29378 mans0954 feat(Analysis/LocallyConvex/AbsConvex): Balanced and AbsConvex sets under linear maps merge-conflict t-analysis please-adopt looking for help
29856 mans0954 feat(Analysis/Normed/Ring/Basic): Add NonUnitalNonAssocSeminormedRing and NonUnitalNonAssocNormedRing t-analysis please-adopt looking for help
12934 grunweg chore: replace more uses of > or ≥ by < or ≤ merge-conflict awaiting-author help-wanted ??? 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
31595 astrainfinita chore: redefine `Ideal.IsPrime` t-algebra merge-conflict merge conflict
29077 grunweg feat(Manifold/Instances/Icc): golf smoothness proof using immersions merge-conflict blocked-by-other-PR 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 t-differential-geometry blocked-by-other-PR merge-conflict blocked on another PR
33948 anivegesana feat(Analysis/Normed/Algebra): matrix exponential of nilpotent matrix new-contributor t-analysis failing CI
33270 vihdzp chore(Order/Disjoint): use `to_dual` t-order awaiting-author failing CI
26291 RemyDegenne feat(Probability): Cameron-Martin theorem WIP blocked-by-other-PR t-measure-probability merge-conflict blocked on another PR
30112 gaetanserre feat(Probability.Kernel): add representation of kernel as a map of a uniform measure t-measure-probability awaiting review
30030 JonBannon feat(MeasureTheory): add `MemLp.Const` class and instances to unify `p = ∞` and `μ.IsFiniteMeasure` cases awaiting-author t-measure-probability merge-conflict failing CI
33807 adamtopaz feat: TypeCat refactor WIP t-category-theory merge-conflict labelled WIP
29610 llllvvuu feat(LinearAlgebra): define LinearMap.Eigenbasis merge-conflict t-algebra awaiting-author merge conflict
31610 rudynicolop feat(Computability/NFA): Kleene star closure for Regular Languages via NFA t-computability new-contributor awaiting-author awaiting-CI does not pass CI
27493 themathqueen feat(RingTheory/Coalgebra): define Frobenius algebra t-ring-theory awaiting-author blocked-by-other-PR blocked on another PR
33992 tb65536 feat(NumberTheory/NumberField/ExistsRamified): Galois group is generated by inertia subgroups t-number-theory t-algebra blocked-by-other-PR 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 t-topology WIP merge-conflict 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 t-data merge-conflict labelled WIP
32825 erdOne perf(RingTheory): `attribute [irreducible] KaehlerDifferential` maintainer-merge awaiting-author t-ring-theory awaiting author
30391 rudynicolop feat(Data/List): list splitting definitions and lemmas t-data new-contributor awaiting-author awaiting author
27704 vihdzp feat: link `Minimal` and `IsLeast` together awaiting-author t-order merge-conflict failing CI
33126 CoolRmal feat: function composition preserves boundedness t-order merge-conflict merge conflict
20719 gio256 feat(AlgebraicTopology): delaborators for truncated simplicial notations merge-conflict t-algebraic-topology infinity-cosmos t-meta ??? 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 merge-conflict WIP modifies-tactic-syntax t-meta ??? opened from a branch in the main mathlib repo (not a fork)
34031 lua-vr feat(Dynamics/BirkhoffSum): add the maximal ergodic theorem blocked-by-other-PR t-dynamics blocked on another PR
25899 pfaffelh feat(Topology/Compactness/CompactSystem): introduce compact Systems merge-conflict awaiting-author t-topology brownian failing CI
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 merge-conflict blocked-by-other-PR new-contributor t-category-theory 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 merge-conflict file-removed blocked-by-other-PR t-algebraic-geometry blocked on another PR
28796 grunweg feat: immersions are smooth t-differential-geometry merge-conflict awaiting-author 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 t-meta t-differential-geometry merge-conflict blocked on another PR
15355 adomani feat: MiM PR report WIP ⚠️ opened from a branch in the main mathlib repo (not a fork)
32039 HugLycan feat(Tactic/Positivity): handle non-zeroness in non-orders WIP new-contributor t-meta merge-conflict labelled WIP
33831 vihdzp refactor(RingTheory/Polynomial/SmallDegreeVieta): convert to {p : R[X]} (hp : p.natDegree = 2) t-ring-theory awaiting-author awaiting author
32745 LTolDe feat(Topology/Algebra): add MulActionConst.lean awaiting-author new-contributor t-topology awaiting author
34131 Ruben-VandeVelde fix: update create_deprecated_modules.lean please-adopt WIP 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 t-logic blocked-by-other-PR merge-conflict 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 t-euclidean-geometry merge-conflict 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` awaiting-CI t-ring-theory does not pass CI
26975 Whysoserioushah feat: a norm_num extension for complex numbers t-meta failing CI
31180 CoolRmal feat(Analysis): a closed convex set is the intersection of countably many half-spaces in a separable Banach space t-analysis new-contributor merge-conflict awaiting-author 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`. t-algebra new-contributor delegated delegated
32828 Hagb feat(Algebra/Order/Group/Defs): add `IsOrderedAddMonoid.toIsOrderedCancelAddMonoid'` awaiting-zulip t-algebra awaiting a zulip discussion
34141 gululu996-ui feat(Combinatorics/SimpleGraph/Acyclic): finite trees have at least two degree-one vertices awaiting-author new-contributor t-combinatorics awaiting author
29014 ShreckYe feat(Data/List/Scan): some theorems that relate `scanl` with `foldl` merge-conflict t-data merge conflict
30758 Timeroot chore: tag abs_inv and abs_div with grind= t-algebra delegated failing CI
34263 grunweg feat: mfderiv_smul t-differential-geometry blocked-by-other-PR blocked on another PR
33689 BoltonBailey feat(Probability): PMF point mass function t-measure-probability WIP blocked-by-other-PR blocked on another PR
33680 BoltonBailey feat(Probability/ProbabilityMassFunction): add Total Variation distance t-measure-probability blocked-by-other-PR blocked on another PR
21476 grunweg feat(lint-style): enable running on downstream projects merge-conflict t-linter awaiting-author ??? 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
32458 vihdzp feat: order isomorphisms preserve successor/predecessor limits t-order awaiting-author failing CI
33749 plp127 feat: `NNRat` is countable t-data large-import awaiting-author awaiting author
33355 0xTerencePrime feat(Combinatorics/SimpleGraph/Connectivity): define vertex connectivity awaiting-author new-contributor t-combinatorics 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 carleson blocked-by-other-PR t-measure-probability blocked on another PR
33052 JovanGerb feat: replace `rw??` tactic with `#infoview_search` command large-import delegated t-meta file-removed merge-conflict failing CI
33209 JovanGerb feat(infoview_search): move to new frontend large-import file-removed t-meta blocked-by-other-PR merge-conflict blocked on another PR
33132 BoltonBailey feat(Computability): Single-tape TM complexity t-computability WIP labelled WIP
34155 zcyemi feat(Geometry/Euclidean/Triangle): add altitudeFoot lies strictly between endpoints for an obtuse angle t-euclidean-geometry awaiting-author ❌? infrastructure-related CI failing
34050 Julian feat(GraphTheory): Graham-Pollak theorem WIP awaiting-author t-combinatorics labelled WIP
34186 faenuccio feat(GroupTheory/SpecificGroups/Cyclic): a quotient of a cyclic group is cyclic t-group-theory awaiting-author awaiting author
31836 hanwenzhu chore(MeasureTheory/IntervalIntegral): generalize fundamental theorem of calculus to `HasDerivWithinAt` instead of `HasDerivAt` t-analysis t-measure-probability awaiting-author merge-conflict merge conflict
12879 grunweg feat: port ge_or_gt linter from mathlib3 merge-conflict t-linter tech debt blocked-by-other-PR ??? 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
32583 MJ141592 refactor(SimpleGraph): change bridges not to require the edge to be present t-combinatorics new-contributor awaiting-author failing CI
34361 grunweg chore: rename comp' to fun_comp a few more times; use to_fun to autog… t-analysis blocked-by-other-PR blocked on another PR
8608 eric-wieser feat: multiplicativize `AddTorsor` merge-conflict WIP t-algebra please-adopt ??? 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
33458 NoneMore feat(ModelTheory): add lifting for embeddings to languages with constants t-logic new-contributor awaiting review
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` t-topology blocked-by-other-PR blocked on another PR
34273 gasparattila feat(Topology/Sets): finite sets are dense in `(Nonempty)Compacts` t-topology blocked-by-other-PR blocked on another PR
34278 gasparattila feat(Topology/Sets): connectedness of `NonemptyCompacts` t-topology blocked-by-other-PR blocked on another PR
34280 gasparattila feat(Topology/Sets): local connectedness of `(Nonempty)Compacts` t-topology blocked-by-other-PR blocked on another PR
34275 gasparattila feat(Topology/Sets): topological properties of `(Nonempty)Compacts.map` t-topology blocked-by-other-PR blocked on another PR
31377 CoolRmal feat: a series of smooth functions that converges (locally) uniformly is smooth t-topology new-contributor awaiting-author merge-conflict failing CI
34192 bwangpj feat(MeasureTheory): mulEquivHaarChar_eq_one_of_compactSpace t-measure-probability awaiting review
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
29934 smmercuri feat(Field/WithAbs): the lift of a ring homomorphism from `WithAbs v` to `WithAbs w` to their completions merge-conflict WIP FLT ⚠️ labelled WIP
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 merge-conflict large-import migrated-from-branch t-meta awaiting-author WIP labelled WIP
33954 or4nge19 feat(CategoryTheory/Abelian): add Filtration API t-category-theory awaiting-author awaiting author
34092 staroperator feat(SetTheory/ZFC): properties of `ZFSet.omega` t-set-theory awaiting review
34138 pfaffelh feat(MeasureTheory): Introduce `MassFunction α` giving rise to a `Measure α ⊤` t-measure-probability new-contributor 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. new-contributor t-combinatorics 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
34029 lua-vr feat(Order/PartialSups): add exists_partialSups_eq t-order awaiting review
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` t-data merge-conflict failing CI
33295 AntoineChambert-Loir feat(Algebra/Central/End): center of the group of automorphisms of a free module t-algebra WIP merge-conflict 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 t-combinatorics blocked-by-other-PR blocked on another PR
34257 grunweg feat(Tactic/ToFun): allow configuring the name of the generated declaration t-meta awaiting-author merge-conflict merge conflict
34554 SnirBroshi feat(Data/Nat/Factorization/Divisors): calculate divisors using prime factorization t-data delegated delegated
34519 grunweg feat: environment linter for definitions containing an underscore t-linter CI large-import awaiting-author failing CI
32609 PrParadoxy feat(LinearAlgebra/PiTensorProduct): Relation between nested tensor products and tensor products indexed by dependent sums new-contributor blocked-by-other-PR merge-conflict t-algebra blocked on another PR
34364 YuvalFilmus feat(Chebyshev/RootsExtrema): bound iterated derivatives of Chebyshev T on [-1, 1] t-analysis awaiting review
29000 JovanGerb feat(Tactic/Push): add basic tags and tests merge-conflict blocked-by-other-PR t-meta blocked on another PR
27053 tb65536 feat: Galois group of `x^n - x - 1` WIP t-algebra large-import labelled WIP
30379 kckennylau feat(RingTheory): isomorphism of graded rings merge-conflict blocked-by-other-PR t-ring-theory blocked on another PR
29792 robertmaxton42 feat(RelCWComplex): a (relative, concrete) CW complex is the colimit of its skeleta merge-conflict blocked-by-other-PR large-import t-topology blocked on another PR
31135 kckennylau feat(RingTheory): is localization iff is localization on saturation merge-conflict blocked-by-other-PR t-ring-theory blocked on another PR
24100 eric-wieser feat: restore some explicit binders from Lean 3 merge-conflict awaiting-author tech debt t-topology t-algebra 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
34521 huaizhangchu feat(MeasureTheory): add measurableEmbedding_natCast t-measure-probability new-contributor awaiting review
34633 mitchell-horner feat(Combinatorics/SimpleGraph): define the Zarankiewicz function t-combinatorics blocked-by-other-PR blocked on another PR
34656 vihdzp refactor: review `exists_irreducible_of_degree_pos` theorems t-ring-theory t-algebra awaiting-zulip awaiting a zulip discussion
34675 YaelDillies feat: comultiplication as a bialgebra hom t-ring-theory blocked-by-other-PR toric blocked on another PR
30327 luigi-massacci feat(Analysis/Distribution/TestFunction): add characterizations of continuity for linear maps on test functions merge-conflict blocked-by-other-PR 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 merge-conflict blocked-by-other-PR t-analysis blocked on another PR
30989 kckennylau feat(RingTheory): Teichmuller map awaiting-author merge-conflict t-ring-theory merge conflict
31007 kckennylau feat(RingTheory): generalise perfection to monoids merge-conflict t-ring-theory failing CI
30365 kckennylau feat(RingTheory): define R-linear graded algebra homomorphism merge-conflict blocked-by-other-PR t-ring-theory blocked on another PR
29411 llllvvuu feat(LinearAlgebra/Matrix/Rank): rank factorization merge-conflict awaiting-author t-algebra merge conflict
30399 kckennylau feat(RingTheory): make HomogeneousLocalization.map take a graded ring hom merge-conflict blocked-by-other-PR t-ring-theory blocked on another PR
30260 imbrem feat(CategoryTheory/Monoidal): added CocartesianMonoidalCategory merge-conflict blocked-by-other-PR large-import new-contributor t-category-theory blocked on another PR
30258 imbrem feat(CategoryTheory/Monoidal): to_additive for proofs using `monoidal` merge-conflict blocked-by-other-PR large-import new-contributor t-category-theory 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 new-contributor awaiting-zulip t-algebra 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 large-import t-topology 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 merge-conflict blocked-by-other-PR 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
33791 PhoenixIra feat: Generalization of FixedPointApproximants to CompletePartialOrder new-contributor t-order awaiting review
32742 LTolDe feat(MeasureTheory/Constructions/Polish/Basic): add class SuslinSpace new-contributor awaiting-zulip t-measure-probability awaiting a zulip discussion
34310 kaantahti feat(Combinatorics): add Sperner's Lemma new-contributor awaiting-author awaiting-CI t-combinatorics does not pass CI
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 t-algebraic-geometry toric FLT blocked-by-other-PR opened from a branch in the main mathlib repo (not a fork)
30920 callesonne feat(Category/Grpd): define the bicategory of groupoids t-category-theory large-import merge-conflict failing CI
30121 idontgetoutmuch feat(Mathlib/Geometry/Manifold): principal fiber bundle core awaiting-author t-differential-geometry new-contributor awaiting author
31339 grunweg chore: move lemma merge-conflict blocked-by-other-PR blocked on another PR
27918 kim-em chore: refactor WithBot/WithTop as structures file-removed merge-conflict WIP labelled WIP
29605 alreadydone experiment(Algebra): unbundle npow/zpow from Monoid/InvDivMonoid merge-conflict t-algebra awaiting-CI WIP labelled WIP
25474 adomani test for .lean/.md check merge-conflict t-linter file-removed WIP ??? opened from a branch in the main mathlib repo (not a fork)
33991 grunweg test: pretty-printing of class abbrev merge-conflict file-removed large-import WIP opened from a branch in the main mathlib repo (not a fork)
34484 grunweg test: debugging mfderiv_smul erws t-differential-geometry blocked-by-other-PR WIP blocked on another PR
31110 bryangingechen ci: don't delete merged branches awaiting-author CI merge-conflict opened from a branch in the main mathlib repo (not a fork)
33707 jcommelin ci: add commit verification for transient and automated commits CI merge-conflict failing CI
31102 JOSHCLUNE feat: require LeanHammer merge-conflict new-contributor t-meta failing CI
33431 gululu996-ui feat(Combinatorics/SimpleGraph/Bipartite): characterize bipartite simple graphs by even cycles new-contributor t-combinatorics awaiting-author awaiting author
34007 martinwintermath feat(Algebra/Module/Submodule/Dual): dual operator for submodules t-algebra new-contributor awaiting-author awaiting author
33928 jsm28 feat(Combinatorics/Tiling/TileSet): indexed families of tiles t-combinatorics awaiting review
34473 JovanGerb feat: remove `Membership` instance for `SetLike` t-set-theory merge-conflict failing CI
34271 gasparattila feat(Topology/Sets): second-countability of `(Nonempty)Compacts` t-topology blocked-by-other-PR 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 brownian t-measure-probability 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` t-analysis awaiting-author awaiting author
34728 j-loreaux feat: continuous linear equivalence between continuous `ℝ`- and `𝕜`-linear functionals, when equipped with the weak⋆-topology t-analysis blocked-by-other-PR ❌? blocked on another PR
30185 alreadydone feat(MathlibTest): kernel reduction of nsmul on elliptic curve over ZMod t-algebra t-number-theory t-algebraic-geometry awaiting-author awaiting author
33044 bryangingechen ci: also get cache for parent commit awaiting-author CI merge-conflict failing CI
31809 ADedecker feat: differentiation of test function as a CLM blocked-by-other-PR t-analysis merge-conflict blocked on another PR
34375 jvanwinden feat(MeasureTheory/Function/AEEqOfLIntegral): introduce lemmas for rewriting a.e. inequalities new-contributor t-measure-probability awaiting review
34779 tb65536 refactor(Computability/TMComputable): generalize from `FinEncoding` t-computability awaiting review
30620 plp127 feat: copy LE and LT on preorder and partial order t-order awaiting-author awaiting author
34000 grunweg chore: golf using fun_prop [foo] syntax WIP merge-conflict labelled WIP
34188 vihdzp feat: abbrev for `Std.Total (· ≤ ·)` t-order merge-conflict merge conflict
34202 or4nge19 feat(Topology/MetricSpace): annuli in (pseudo)(e)metric spaces carleson t-topology awaiting-author 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) t-analysis new-contributor awaiting-author awaiting author
33599 nielstron feat(Computability/ContextFreeGrammar): closure under union blocked-by-other-PR t-computability new-contributor blocked on another PR
33601 nielstron feat(Computability/ContextFreeGrammar): Concatenation of CFGs is CFG t-computability new-contributor blocked-by-other-PR blocked on another PR
33592 nielstron feat(Computability/ContextFreeGrammar): mapping between two types of nonterminal symbols awaiting-author t-computability new-contributor failing CI
33108 alreadydone feat(Topology): `π₁(E⧸G)⧸π₁(E) ≃* G` for `E` path connected t-algebraic-topology WIP t-topology merge-conflict 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
34629 plp127 feat: cyclic group with explicit generator is equivalent to `ZMod n` t-group-theory merge-conflict merge conflict
31508 FLDutchmann feat(Tactic): `algebra` tactic. t-meta awaiting-author blocked-by-other-PR merge-conflict blocked on another PR
33619 vihdzp refactor: flip `Ixx_def` theorems t-order awaiting-CI merge-conflict does not pass CI
33080 sinhp feat(Category Theory): Cartesian Natural Transformation t-category-theory awaiting-author awaiting author
34427 CoolRmal feat(MeasureTheory): Strong measurability is preserved under division in a group with zero t-measure-probability awaiting review
34397 Parcly-Taxel feat: integral representation of the AGM t-analysis awaiting-author awaiting author
32334 EtienneC30 feat: independence of Gaussian processes brownian t-measure-probability awaiting-author awaiting author
34018 CoolRmal feat: series representation of cosecant t-analysis awaiting-author awaiting author
33832 alreadydone feat(Algebra): localization preserves unique factorization t-algebra maintainer-merge awaiting-author awaiting author
34611 adomani feat: perfect subgroups t-group-theory awaiting-author 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 large-import t-topology awaiting-author 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 t-algebra t-order awaiting-author awaiting author
34394 Citronhat feat(Algebra/Order/Ring): add constructors for linear ordered rings new-contributor t-algebra awaiting-author awaiting author
34895 eric-wieser chore: backquote tactic names in error messages t-meta delegated 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 large-import t-data new-contributor 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 t-topology blocked-by-other-PR merge-conflict blocked on another PR
34099 mcdoll feat(Analysis/Distribution): Fourier multiplier t-analysis awaiting review
34788 justus-springer feat(Algebra/Polynomial/AlgebraMap): add Polynomial.aeval_eq_aeval_map t-algebra ❌? infrastructure-related CI failing
34938 peabrainiac feat(Geometry/Manifold): interior and boundary are preserved by (local) diffeomorphisms t-differential-geometry blocked-by-other-PR blocked on another PR
34556 Parcly-Taxel feat: IMO 2002 Q3 IMO failing CI
33634 xgenereux feat(ValuationSubring): eq_self_or_eq_top_of_le blocked-by-other-PR large-import t-algebra blocked on another PR
34622 vihdzp feat: Nat/Int casts on char two rings t-algebra awaiting review
34088 kbuzzard perf(RingTheory/Kaehler/Polynomial): change universe name for speed-up t-ring-theory WIP 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 t-ring-theory new-contributor awaiting-author awaiting author
33668 Citronhat feat(PMF): add lintegral formulas for PMF t-measure-probability new-contributor awaiting review
28468 alreadydone feat(Algebra): ring API for `AddLocalization` t-algebra large-import t-ring-theory awaiting-author awaiting author
34815 Deep0Thinking feat(Analysis/SpecialFunctions/ImproperIntegrals): Frullani integral new-contributor large-import t-analysis awaiting-author blocked-by-other-PR 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
34435 huaizhangchu feat(Probability): convolution of Poisson distributions t-measure-probability large-import new-contributor awaiting review
26293 RemyDegenne feat: tightness from convergence of characteristic functions t-measure-probability blocked-by-other-PR blocked on another PR
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)
30579 smmercuri feat : `v.adicCompletionIntegers K` is compact when `K` is a number field WIP blocked-by-other-PR large-import merge-conflict ⚠️ blocked on another PR
34045 smmercuri feat: `algebraMap K L` is uniform continuous with respect to adic topologies, when the ideal `w` of `L` lies above `v` blocked-by-other-PR FLT t-algebra merge-conflict blocked on another PR
33662 Pjotr5 feat(Algebra/Order/BigOperators/Expect): add lemmas and strict variants new-contributor t-algebra awaiting review
26061 kckennylau (WIP) feat(AlgebraicGeometry): define Projective Space merge-conflict WIP t-algebraic-geometry blocked-by-other-PR blocked on another PR
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 t-topology merge-conflict failing CI
35041 b-mehta feat(Combinatorics): prove the Rado selection lemma t-combinatorics ❌? infrastructure-related CI failing
34475 artie2000 fix: remove some nolints t-ring-theory WIP merge-conflict labelled WIP
34646 vihdzp feat: predicate for algebraically closed subfields t-algebra blocked-by-other-PR merge-conflict blocked on another PR
34652 vihdzp feat: more theorems on `Polynomial.toSubring` blocked-by-other-PR t-ring-theory merge-conflict blocked on another PR
34720 Paul-Lez feat(RingTheory/PowerSeries/Composition): define composition of power series t-ring-theory awaiting-zulip failing CI
34026 SnkXyx feat(Algebra/MvPolynomial): add mainVariable t-algebra new-contributor awaiting review
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 new-contributor t-logic 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 t-algebra workshop-AIM-AG-2024 t-category-theory merge-conflict awaiting-author ??? opened from a branch in the main mathlib repo (not a fork)
32374 adamtopaz feat(Tactic/WildcardUniverse): Foo.{*, _, v*, max u v} t-meta maintainer-merge awaiting-author awaiting author
26986 WangYiran01 feat(Partition): add bijection for partitions with max part ≤ r awaiting-author t-combinatorics new-contributor merge-conflict failing CI
32672 tb65536 feat: haar measures on short exact sequences t-measure-probability t-topology FLT awaiting-author blocked-by-other-PR blocked on another PR
25035 ScottCarnahan feat(Algebra/Module/Equiv/Defs): linear equivalence between linear hom and semilinear hom WIP t-algebra merge-conflict ??? 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 new-contributor t-measure-probability merge-conflict blocked on another PR
33463 khwilson feat(Mathlib/Analysis/Polynomial/MahlerMeasure): Mahler Measure for other rings new-contributor t-analysis awaiting-author 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
34875 banrovegrie feat(LinearAlgebra/Matrix): add Sherman-Morrison formula t-algebra new-contributor ❌? infrastructure-related CI failing
33363 BoltonBailey feat: add `empty_eq_image` simp lemmas t-data awaiting-author awaiting author
33611 urkud feat(ImplicitFunction): add a parametric version t-analysis awaiting-author awaiting author
27702 FLDutchmann feat(NumberTheory/SelbergSieve): define Lambda-squared sieves and prove important properties t-number-theory delegated merge-conflict failing CI
28499 yoh-tanimoto feat(MeasureTheory/VectorMeasure): add integral of a vector-valued function against a vector measure blocked-by-other-PR t-measure-probability merge-conflict blocked on another PR
28693 faenuccio feat(Analysis.Normed.Module.Milman-Pettis): add Milman-Pettis theorem WIP t-analysis merge-conflict labelled WIP
31141 peabrainiac feat(Analysis/Calculus): parametric integrals over smooth functions are smooth t-analysis maintainer-merge awaiting-author 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 new-contributor t-category-theory t-condensed large-import awaiting-author awaiting author
33969 goliath-klein refactor(PiTensorProduct/{InjectiveNorm, ProjectiveNorm}): Currently, injectiveSeminorm = projectiveSeminorm WIP t-analysis new-contributor large-import merge-conflict labelled WIP
34248 erdOne chore: get rid of `LocalizedModule.mk` awaiting-author t-algebra merge-conflict 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` t-algebraic-geometry merge-conflict failing CI
34626 grunweg feat: analytification of schemes (affine case) merge-conflict WIP t-differential-geometry blocked-by-other-PR please-merge-master blocked on another PR
33821 JohnnyTeutonic feat(LinearAlgebra/Matrix/Hermitian): add IsSkewHermitian predicate t-algebra awaiting-author awaiting author
34963 Parcly-Taxel feat(Archive): proof of the Robbins conjecture ⚠️ awaiting review
34990 bwangpj feat: `ContinuousSMul (∀ i, N i) (∀ i, γ i)` t-topology awaiting review
34994 bwangpj feat: Countable.of_module_finite t-algebra large-import FLT awaiting review
34650 vihdzp feat: redefine `Polynomial.toSubring` with better def-eqs t-ring-theory failing CI
35128 DAE123456 feat : Define anti_pascal t-algebra new-contributor awaiting-author awaiting author
34318 adomani feat: a nilpotent simple group is cyclic t-group-theory awaiting-author awaiting author
26588 faenuccio feat(Algebra/GroupWithZero/WithZero): add the multiplicative embedding with zero from the range t-algebra t-order awaiting review
34846 fpvandoorn fix: module system and translate interaction t-meta awaiting-author blocked-by-other-PR merge-conflict blocked on another PR
34931 eric-wieser perf: make TensorProduct.lift irreducible with a unification hint t-algebra merge-conflict opened from a branch in the main mathlib repo (not a fork)
35031 JovanGerb feat(CategoryTheory/Limits/Cones): use `to_dual` blocked-by-other-PR merge-conflict ⚠️ blocked on another PR
34759 Hagb feat(RingTheory/MvPolynomial/MonomialOrder): add degree with `⊥` as degree of `0` blocked-by-other-PR t-ring-theory blocked on another PR
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
35013 CoolRmal feat(Topology/Bornology): a locally bounded function maps a compact set to a bounded set t-topology awaiting review
35014 RemyDegenne feat: Radon-Nikodym derivative of a composition-product t-measure-probability awaiting review
35015 RemyDegenne feat: `rnDeriv` as ratio of densities wrt a dominating measure t-measure-probability awaiting review
33032 ksenono feat(Combinatorics/SimpleGraph): Konig’s theorem on bipartite graphs t-combinatorics new-contributor blocked-by-other-PR merge-conflict blocked on another PR
31662 edwin1729 feat(Topology/Order): topological basis of scott topology on Complete… t-topology new-contributor awaiting-author merge-conflict merge conflict
33506 Rida-Hamadani feat(SimpleGraph): construct a cycle of two distinct paths with same start and end blocked-by-other-PR t-combinatorics blocked on another PR
27198 robin-carlier feat(CategoryTheory/Monoidal/DayConvolution): the Yoneda embedding is monoidal (for Day convolution) merge-conflict file-removed blocked-by-other-PR t-category-theory blocked on another PR
34159 wangying11123 feat(Geometry/Euclidean/Similarity): Add Triangle similarity on oangle t-euclidean-geometry new-contributor awaiting-author awaiting author
34760 astrainfinita chore: use `RelHomClass` in `IsChain.image` t-order awaiting-author awaiting author
32692 WilliamCoram feat: define multivariate restricted power series t-ring-theory t-number-theory new-contributor awaiting-author failing CI
32807 WilliamCoram feat: Define the Gauss norm for MvPowerSeries t-ring-theory new-contributor awaiting review
35255 vlad902 feat(SimpleGraph): `cycleGraph.IsContained` in every graph with a cycle t-combinatorics blocked-by-other-PR blocked on another PR
34799 vlad902 feat(SimpleGraph): the cycle graph and complete graph are Hamiltonian t-combinatorics large-import blocked-by-other-PR merge-conflict blocked on another PR
34423 euprunin chore: golf using `grind` awaiting review
34583 adomani feat: basic properties of subnormal subgroups large-import t-group-theory awaiting-author awaiting author
31366 FaffyWaffles feat(Analysis/SpecialFunctions/StirlingRobbins): Robbins' sharp stepwise bound for stirlingSeq t-analysis new-contributor awaiting-author awaiting author
33878 xroblot feat(MulChar): generalize duality results on finite abelian groups to multiplicative characters large-import t-number-theory blocked-by-other-PR merge-conflict blocked on another PR
34571 xroblot feat(CyclotomicField/Galois): the bijection between subfields and subgroups of Dirichlet characters large-import blocked-by-other-PR t-algebra merge-conflict blocked on another PR
33443 sahanwijetunga feat: Define Isometries of Bilinear Spaces t-algebra new-contributor awaiting-author awaiting author
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
25992 Multramate feat(RingTheory/Ideal/Span): add pair lemmas t-ring-theory awaiting review
34702 pfaffelh feat(Data/FinsetPowerset): The set `{v : List.Vector Bool n | v.val.count = k}` has cardinality `n.choose k` large-import t-data awaiting review
34820 staroperator feat(Order/Ideal): more results on order ideals t-order large-import awaiting review
35081 tb65536 feat(Topology/Algebra/Group/Extension): define short exact sequence of topological groups t-topology awaiting review
35089 RemyDegenne feat: Radon-Nikodym derivative of a map is a conditional expectation t-measure-probability ??? missing CI information
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
34757 Hagb feat(Algebra/MvPolynomial/Rename): some lemmas about `rename` and `killCompl` t-algebra awaiting review
34758 Hagb feat(RingTheory/MvPolynomial/MonomialOrder): misc lemmas t-ring-theory awaiting review
35250 vlad902 feat(SimpleGraph): redefine `cycleGraph` independent of `circulantGraph` t-combinatorics awaiting review
33329 mcdoll feat(Analysis): Fourier-based Sobolev spaces WIP t-analysis blocked-by-other-PR blocked on another PR
25834 Rida-Hamadani feat(SimpleGraph): girth-diameter inequality blocked-by-other-PR t-combinatorics blocked on another PR
35292 Rida-Hamadani feat(SimpleGraph): taking twice from a walk equals taking the minimum t-combinatorics awaiting review
35144 daniel-carranza feat(CategoryTheory/Enriched): tensor product of enriched categories new-contributor t-category-theory infinity-cosmos awaiting-author awaiting author
33249 Rida-Hamadani feat(SimpleGraph): `take` is path if original walk is path t-combinatorics awaiting review
35308 martinwintermath feat(Geometry/Convex/Cone): Add coercion from submodule to cone t-convex-geometry awaiting review
35296 Rida-Hamadani feat(SimpleGraph): taking or droping from a cycle results in a path blocked-by-other-PR t-combinatorics blocked on another PR
33050 mkaratarakis feat: lemmas for the analytic part of the proof of the Gelfond–Schneider theorem t-number-theory new-contributor WIP labelled WIP
34649 peabrainiac feat(Analysis/Calculus/ContDiff): add notation `ℕ∞ω` for `WithTop ℕ∞` t-differential-geometry t-analysis awaiting-author awaiting-zulip awaiting a zulip discussion
34914 jvanwinden feat(Analysis/Normed/Module/FiniteDimension): add lemmas on IsTheta and summability t-analysis new-contributor awaiting review
30900 vihdzp feat: run-length encoding t-data awaiting review
35058 GrigorenkoPV chore: move tendsto_{floor,ceil}_at{Top,Bot} new-contributor large-import awaiting review
35106 tb65536 feat(AlgebraicGeometry/IdealSheaf/IrreducibleComponent): subscheme structure on an irreducible component t-algebraic-geometry awaiting review
33217 Blackfeather007 feat(Algebra): define associated graded structure for abelian group new-contributor t-ring-theory awaiting-author awaiting author
34948 joneugster feat(scripts/autolabel): add option to configure number of applied labels CI ??? missing CI information
33020 FormulaRabbit81 chore(Topology): Deprecate file t-topology large-import merge-conflict merge conflict
34952 joneugster feat(scripts/autolabel): use `Cli` and integrate `curl` call into `autolabel` CI ??? missing CI information
35331 SnirBroshi feat(SimpleGraph/Subgraph): small things about `spanningCoe` and a small golf t-combinatorics awaiting review
34066 joneugster feat(scripts/autolabel): introduce topic label dependencies CI ??? missing CI information
34677 joneugster feat(scripts/autolabel): add missing folders CI ??? missing CI information
34678 joneugster feat(scripts/autolabel): add dependencies for `t-ring-theory` CI blocked-by-other-PR ??? blocked on another PR
34079 joneugster feat(scripts/autolabel): add dependencies for alg. geometry and diff. geometry blocked-by-other-PR CI ??? blocked on another PR
34078 joneugster feat(scripts/autolabel): add label dependencies for better automatic label assignment blocked-by-other-PR CI ??? blocked on another PR
23042 joneugster feat(CategoryTheory/Enriched/Limits): add HasConicalLimitsOfSize.shrink WIP t-category-theory infinity-cosmos please-adopt ??? opened from a branch in the main mathlib repo (not a fork)
23142 joneugster feat(CategoryTheory/Enriched/Limits): add API for HasConicalLimit awaiting-author t-category-theory infinity-cosmos please-adopt ??? opened from a branch in the main mathlib repo (not a fork)
23145 joneugster feat(CategoryTheory/Enriched/Limits): add IsConicalLimits merge-conflict blocked-by-other-PR t-category-theory infinity-cosmos please-adopt opened from a branch in the main mathlib repo (not a fork)
20401 RemyDegenne feat: add sigmaFinite_iUnion merge-conflict awaiting-author 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. new-contributor merge-conflict t-analysis 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 t-linter awaiting-CI does not pass CI
11500 mcdoll refactor(Topology/Algebra/Module/WeakDual): Clean up merge-conflict awaiting-author 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` merge-conflict WIP t-data opened from a branch in the main mathlib repo (not a fork)
35323 martinwintermath feat(Geometry/Convex/Cone): Add lemmas for PointedCone.dual t-convex-geometry awaiting review
29281 plp127 doc: `Fin.natAdd_castLEEmb` merge-conflict t-data merge conflict
34797 vlad902 feat(SimpleGraph): `cycleGraph_EulerianCircuit` is a cycle t-combinatorics awaiting-author awaiting author
34165 zcyemi feat(Archive/Imo/Imo2012Q5): IMO 2012 Q5 blocked-by-other-PR large-import IMO merge-conflict blocked on another PR
27936 alreadydone feat(Algebra): additivize Dvd and Prime t-algebra awaiting-author merge-conflict merge conflict
35363 joelriou feat(CategoryTheory/Triangulated/TStructure): properties of `truncLT` and `truncGE` which use the octahedron axiom WIP t-category-theory large-import blocked-by-other-PR ❌? blocked on another PR
34156 zcyemi feat(Analysis/Convex/Between): add lemmas on convex combination of mem simplex interior t-analysis merge-conflict merge conflict
34503 alreadydone chore(RingTheory/Localization): generalize FractionRing to semirings t-ring-theory t-algebra awaiting-CI WIP merge-conflict labelled WIP
34973 chrisflav chore: replace `Punit` by `PUnit` merge-conflict ❌? infrastructure-related CI failing
35134 fpvandoorn feat(translate): print constant names with hover info t-meta awaiting-author merge-conflict merge conflict
35356 joelriou feat(Algebra/Homology): definition of the category of spectral sequences WIP t-algebra t-category-theory blocked-by-other-PR blocked on another PR
35372 joelriou feat(Algebra/Homology/SpectralObject): `SpectralSequenceMkData` WIP t-algebra t-category-theory blocked-by-other-PR blocked on another PR
35359 joelriou feat(Algebra/Homology/SpectralObject): kernel and cokernel of differentials WIP t-algebra t-category-theory blocked-by-other-PR blocked on another PR
35361 joelriou feat(Algebra/Homology/SpectralObject): cycles as cokernels and opcycles as kernels WIP t-algebra t-category-theory blocked-by-other-PR blocked on another PR
29777 yuanyi-350 feat(Functional Analysis): closed Range Theorem WIP blocked-by-other-PR new-contributor awaiting-author t-analysis merge-conflict blocked on another PR
35378 joelriou feat(Algebra/Homology/SpectralObject): construction of the objects on the pages of the spectral sequence WIP t-algebra t-category-theory blocked-by-other-PR blocked on another PR
35349 RemyDegenne feat: data processing inequality for the Kullback-Leibler divergence WIP t-measure-probability large-import blocked-by-other-PR blocked on another PR
34841 RemyDegenne feat(InformationTheory): chain rule for the Kullback-Leibler divergence WIP t-measure-probability large-import blocked-by-other-PR blocked on another PR
29151 yuanyi-350 feat: Corollary of Hahn–Banach theorem awaiting-author new-contributor large-import t-analysis merge-conflict 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 t-linter RFC looking for help
29965 RemyDegenne feat(probability): define subtraction of kernels WIP t-measure-probability large-import labelled WIP
34189 bwangpj feat(MeasureTheory/Measure): haarScalarFactor_map t-measure-probability FLT awaiting review
35387 joelriou feat(CategoryTheory/Triangulated): abelian subcategories WIP t-category-theory blocked-by-other-PR blocked on another PR
25984 Multramate feat(AlgebraicGeometry/EllipticCurve/Affine/Point): add equivalences between points and explicit WithZero types t-algebraic-geometry awaiting review
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
35157 Multramate feat(RingTheory/AdjoinRoot): add IsFractionRing for AdjoinRoot t-ring-theory t-algebra awaiting review
35163 CoolRmal feat(Topology): comparison of two Hausdorff topologies t-topology awaiting review
35172 Parcly-Taxel feat(Archive): minimal axioms for Boolean algebra ⚠️ awaiting review
35193 Brian-Nugent feat(Topology/Closeds): implement category of closed sets in topologi… t-topology new-contributor awaiting review
35205 j-loreaux feat: `Subobject.topologicalClosure_mono` t-topology awaiting review
35239 JohnnyTeutonic feat(Logic/Function): add Lawvere fixed-point theorem t-logic awaiting-author awaiting author
25848 joelriou feat/refactor: redefinition of homology + derived categories WIP t-category-theory large-import t-topology merge-conflict labelled WIP
33189 peabrainiac feat(Geometry/Manifold): the interior of a manifold is open t-differential-geometry awaiting-author blocked-by-other-PR blocked on another PR
32534 erdOne feat(AlgebraicGeometry): Zariski's main theorem WIP t-ring-theory labelled WIP
35398 vlad902 feat(SimpleGraph): `bypass` lemmas t-combinatorics awaiting review
28248 YaelDillies feat: binomial random variables t-measure-probability awaiting review
35300 Ljon4ik4 feat: Semi-direct sum of Lie algebras t-algebra new-contributor awaiting review
35412 joneugster feat(Tactic/Linter): add unicode linter for unicode variant-selectors t-linter awaiting review
35414 joneugster feat(Cache): Allow arguments of the form `Mathlib.Data.+` which correspond to a folder but not a file CI t-meta awaiting review
35413 joneugster fix(Util/CountHeartbeats): move elaboration in #count_heartbeats inside a namespace t-meta awaiting review
34676 joneugster chore(Algebra/CharP/MixedCharZero): update file to make use of the module system t-algebra 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` t-topology new-contributor merge-conflict 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 awaiting-CI t-meta merge-conflict does not pass CI
33288 vihdzp chore(Combinatorics/SimpleGraph/Paths): review API t-combinatorics merge-conflict merge conflict
34024 adomani feat: the global syntax linter large-import blocked-by-other-PR t-linter merge-conflict blocked on another PR
34477 spanning-tree refactor(Order): make CompletePartialOrder extend OrderBot t-order new-contributor merge-conflict merge conflict
35005 b-mehta chore(Algebra/Order/BigOperators): move lemmas which don't use addition out of Ring t-algebra large-import merge-conflict merge conflict
35008 b-mehta feat(Algebra/Order/BigOperators): order properties of subsets in groups with zero t-algebra blocked-by-other-PR large-import merge-conflict 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 merge-conflict WIP t-differential-geometry blocked-by-other-PR ??? opened from a branch in the main mathlib repo (not a fork)
35327 SnirBroshi feat(SimpleGraph/Acyclic): the union of two trees that share exactly one vertex is a tree t-combinatorics awaiting review
34015 erdOne feat(AlgebraicGeometry): category of schemes affine over a base t-algebraic-geometry awaiting review
35206 j-loreaux feat: `Cauchy.map` for functions uniformly continuous on a set t-topology awaiting review
35268 tb65536 feat(Topology/Algebra/Module/LinearMap): units in `M →L[R] M` are homeomorphisms t-topology t-algebra awaiting review
35269 tb65536 refactor(Topology/Algebra/Module/LinearMap): adjust statement of `coe_mul` and `coe_pow` t-topology t-algebra awaiting review
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 awaiting-CI merge-conflict does not pass CI
27500 Komyyy feat: the Riemann zeta function is meromorphic WIP t-analysis large-import labelled WIP
35210 kim-em chore: use @[to_dual] in CompleteLattice extras and Set.Lattice blocked-by-other-PR blocked on another PR
35418 vlad902 feat(SimpleGraph): `IsAcyclic` iff not 2-edge-reachable t-combinatorics awaiting review
26345 mans0954 feat(Analysis/LocallyConvex/Polar): Bipolar theorem merge-conflict awaiting-author t-analysis large-import please-adopt looking for help
34588 Ruben-VandeVelde feat: add generalizations of some padicVal{Nat,Int} lemmas t-number-theory awaiting-author awaiting author
27229 WilliamCoram feat(GroupTheory/DoubleCoset): multiple lemmas FLT t-group-theory new-contributor awaiting-author awaiting author
26413 michaellee94 feat: existence of maximal solutions for ODEs meeting Picard-Lindelöf conditions blocked-by-other-PR new-contributor t-analysis merge-conflict blocked on another PR
35146 harahu doc(CategoryTheory/Bicategory/Kan): clarify Kan adjunction docstrings t-category-theory awaiting review
33387 AntoineChambert-Loir chore(LinearAlgebra/Transvection/Basic): mv Transvection.lean file to Transvection.Basic.lean file-removed t-algebra blocked-by-other-PR merge-conflict blocked on another PR
33392 AntoineChambert-Loir feat(LinearAlgebra/Transvection/Generation): non-exceptional case in Dieudonné's theorem t-algebra blocked-by-other-PR file-removed merge-conflict blocked on another PR
33402 AntoineChambert-Loir feat(LinearAlgebra/Transvection/Generation): prove exceptional case in Dieudonné's theorem file-removed t-algebra blocked-by-other-PR merge-conflict blocked on another PR
33485 AntoineChambert-Loir feat(LinearAlgebra/Transvection/Generation): prove the third part of Dieudonné's theorem file-removed t-algebra blocked-by-other-PR merge-conflict blocked on another PR
33560 AntoineChambert-Loir feat(LinearAlgebra/Transvection/Generation): a linear equivalence is the product of dilatransvections file-removed t-algebra blocked-by-other-PR merge-conflict blocked on another PR
33692 AntoineChambert-Loir feat(LinearAlgebra/Transvection/SpecialLinearGroup): generation of the special linear group by transvections t-algebra file-removed blocked-by-other-PR merge-conflict blocked on another PR
33715 AntoineChambert-Loir feat(LinearAlgebra/Projectivization/Action): prove that the action is 2-transitive and primitive file-removed blocked-by-other-PR t-algebra large-import merge-conflict blocked on another PR
33882 AntoineChambert-Loir feat(LinearAlgebra/Transvection/SpecialLinearGroup): commutators in the special linear group blocked-by-other-PR file-removed t-algebra merge-conflict blocked on another PR
33916 AntoineChambert-Loir feat(LinearAlgebra/SpecialLinearGroup/Simple): simplicity of the projective special linear group. file-removed large-import blocked-by-other-PR t-algebra merge-conflict blocked on another PR
34894 felixpernegger feat(Topology/Separation): add weakly first countable spaces t-topology awaiting-author awaiting author
35426 kim-em ci: add daily master tags CI delegated opened from a branch in the main mathlib repo (not a fork)
33736 fbarroero feat(RingTheory/Polynomial/GaussNorm): The `gaussNorm` is an absolute value if `v` is a nonarchimedean absolute value t-ring-theory awaiting review
34594 kim-em feat(LinearAlgebra/ConvexSpace): show AffineSpace is a ConvexSpace t-algebra awaiting-author awaiting author
31425 robertmaxton42 feat(Topology): implement delaborators for non-standard topology notation t-topology awaiting review
31613 xyzw12345 feat(RepresentationTheory/GroupCohomology): Non-abelian Group Cohomology t-algebra large-import awaiting-author awaiting author
33712 wangying11123 feat(Geometry/Euclidean/Angle/Unoriented/Projection): Add sameray_orthogonalProjection_vsub_of_angle_lt new-contributor t-euclidean-geometry awaiting-author awaiting author
32260 jsm28 feat(Geometry/Euclidean/Angle/Oriented/Affine): oriented angle bisection and halving unoriented angles t-euclidean-geometry maintainer-merge awaiting review
33786 hdmkindom feat(Analysis/Matrix): add Jacobian matrix for matrix-valued functions t-analysis new-contributor awaiting-author 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₀` t-measure-probability delegated delegated
35431 CoolRmal feat: Conditional Jensen's Inequality for a general measure blocked-by-other-PR ⚠️ blocked on another PR
35448 mathlib-splicebot chore(Mathlib/Tactic/Linter/GlobalSyntax.lean): automated extraction t-linter new-contributor opened from a branch in the main mathlib repo (not a fork)
33664 ooovi feat(Geometry/Convex/Cone/Pointed): face lattice of pointed cones file-removed awaiting-author t-convex-geometry merge-conflict blocked-by-other-PR ❌? blocked on another PR
33793 LTolDe feat(MeasureTheory/Constructions/Polish/Basic): add lemma AnalyticSet.inter_nonempty_of_nowhereMeagre t-measure-probability new-contributor awaiting-author awaiting author
32881 foderm feat(AlgebraicTopology/SimplicialObject): define simplicial homotopy new-contributor t-algebraic-topology awaiting-author awaiting author
34068 leomayer1 feat: give functor categories an instance of `HasBinaryBiproducts` t-category-theory new-contributor maintainer-merge awaiting review
26803 bjoernkjoshanssen feat: second partial derivatives test t-analysis awaiting-author awaiting author
35400 vlad902 feat(SimpleGraph): `IsEdgeReachable` lemmas t-combinatorics awaiting review
35069 A-M-Berns feat(Geometry/Polygon): simple polygons and boundary map new-contributor blocked-by-other-PR ⚠️ blocked on another PR
34851 dennj feat(Data/Matrix/Mul): add diagonal and transpose lemmas for vector operations t-data new-contributor awaiting review
24965 erdOne refactor: Make `IsLocalHom` take unbundled map t-algebra delegated merge-conflict opened from a branch in the main mathlib repo (not a fork)
25622 eric-wieser refactor: overhaul instances on LocalizedModule t-algebra merge-conflict opened from a branch in the main mathlib repo (not a fork)
25822 ScottCarnahan WIP: experiments with vertex algebras WIP large-import merge-conflict labelled WIP
25980 Multramate refactor(Algebra/Group/Submonoid/Operations): rename restrict to domRestrict and add restrict t-group-theory merge-conflict merge conflict
25981 Multramate feat(GroupTheory/GroupAction/Basic): define homomorphisms of fixed subgroups induced by homomorphisms of groups t-group-theory large-import merge-conflict merge conflict
26013 tsuki8 feat(Data/Finset/Card,Data/Set/Finite/Basic): TODO needs a better title awaiting-author t-data new-contributor merge-conflict merge conflict
26377 Whysoserioushah feat(RingTheory/SimpleRing/TensorProduct): tensor product of a simple algebra and a central simple algebra is simple t-ring-theory large-import merge-conflict merge conflict
28546 Sfgangloff feat(SymbolicDynamics): basic setup of Zd, full shift, cylinders, pat… t-dynamics new-contributor awaiting review
35086 kebekus feat: add congruence lemmas for integrability t-measure-probability maintainer-merge awaiting review
35279 BoltonBailey chore(Data/Nat/Choose): add grind annotations t-data awaiting review
35301 RemyDegenne feat: `klDiv` and scalar multiplication t-measure-probability awaiting review
35309 Ruben-VandeVelde chore: rename nat_abs_sum_le t-algebra awaiting review
35313 LexinonCraft feat: IMO 2025 Q4 IMO new-contributor awaiting-author awaiting author
26464 joelriou feat(LinearAlgebra): generators of pi tensor products file-removed awaiting-author t-algebra merge-conflict failing CI
28286 bwangpj feat(Geometry/Manifold/ContMDiff): basic lemmas for analytic (`C^ω`) functions awaiting-author t-differential-geometry new-contributor merge-conflict merge conflict
28462 joelriou feat(AlgebraicTopology/SimplicialSet): the relative cell complex attached to a rank function for a pairing t-algebraic-topology WIP merge-conflict labelled WIP
29624 mcdoll feat(LinearAlgebra/LinearPMap): add definition of resolvent and first resolvent identity t-algebra t-analysis awaiting-author merge-conflict failing CI
29764 ScottCarnahan feat(Algebra/Vertex): API up to residue products (WIP) t-algebra blocked-by-other-PR large-import merge-conflict blocked on another PR
29942 smmercuri feat(InfinitePlace/Completion): embeddings of `w.Completion` factor through embeddings of `v.Completion` when `w` extends `v` FLT blocked-by-other-PR t-number-theory large-import merge-conflict blocked on another PR
30750 SnirBroshi feat(Data/Quot): `toSet` and `equivClassOf` t-data awaiting-author awaiting-zulip merge-conflict awaiting a zulip discussion
35316 mkaratarakis feat: lemmas for the analytic part of the proof of the Gelfond–Schneider theorem (Part 4/5) t-number-theory new-contributor blocked-by-other-PR blocked on another PR
31603 alreadydone chore(Algebra): make `RatFunc` an abbrev awaiting-author t-algebra RFC merge-conflict merge conflict
33276 NicolaBernini feat: Rename List.reverse_perm to List.reverse_perm_self and List.reverse_perm' to List.reverse_perm_iff new-contributor awaiting-author t-data merge-conflict merge conflict
33303 sinhp feat(CategoryTheory): The monads and comonads of locally cartesian closed categories WIP t-category-theory merge-conflict labelled WIP
33375 kex-y feat(Probability): Local and stable properties brownian t-measure-probability blocked-by-other-PR merge-conflict blocked on another PR
33441 dupuisf feat: add `LawfulInv` class for types with an inverse that behaves like `Ring.inverse` awaiting-zulip t-algebra merge-conflict awaiting a zulip discussion
33683 joelriou feat(AlgebraicTopology/SimplicialSet): the simplicial homotopy induced by an homotopy blocked-by-other-PR t-algebraic-topology WIP merge-conflict blocked on another PR
33790 eliasjudin feat(CategoryTheory/Preadditive/Mat): add natural transformation and isomorphism extension theorems t-category-theory new-contributor awaiting-author merge-conflict merge conflict
33795 alreadydone feat(Topology/Sheaves): LocalPredicate prerequisite for étalé spaces t-topology merge-conflict merge conflict
33810 dupuisf feat: add instances of `LawfulInv` WIP blocked-by-other-PR merge-conflict ⚠️ blocked on another PR
35469 kim-em chore(GroupAction/DomAct): mark DomMulAct as instance_reducible awaiting-author awaiting author
34040 Ruben-VandeVelde feat: generalize HasCompl.compl image/preimage lemmas to Involutive t-data awaiting-author merge-conflict merge conflict
34075 eric-wieser feat: add a typeclass for the continuum hypothesis t-set-theory awaiting-author merge-conflict opened from a branch in the main mathlib repo (not a fork)
34179 alreadydone refactor(Algebra): weaken NormalizationMonoid t-ring-theory t-algebra awaiting-author merge-conflict merge conflict
34230 smmercuri refactor: use 1-field structure to define the `WithAbs` type synonym large-import merge-conflict merge conflict
35048 b-mehta feat(Analysis/Normed/Operator): prove the Fredholm alternative t-analysis merge-conflict merge conflict
35073 joelriou feat(CategoryTheory/Sites): more on Cech cohomology WIP t-category-theory blocked-by-other-PR merge-conflict blocked on another PR
35197 j-loreaux feat: Hölder framework for `lp` spaces blocked-by-other-PR t-analysis merge-conflict blocked on another PR
35243 ScottCarnahan chore(Algebra/MonoidAlgebra/PointwiseSMul): switch action from Finsupp to (Add)MonoidAlgebra and multiplicativize large-import t-algebra merge-conflict merge conflict
35291 mcdoll feat(Fourier): improved version of Riemann-Lebesgue WIP large-import merge-conflict ⚠️ labelled WIP
34245 staroperator feat(Data/Set): add `Set.Uncountable` t-data awaiting-zulip ❌? infrastructure-related CI failing
31449 kim-em feat(SemilocallySimplyConnected): definition and alternative formulation t-topology awaiting-author awaiting author
34557 kim-em feat(Topology/Homotopy): add Path.subpathOn for restricting paths to subintervals t-topology awaiting-author awaiting author
34551 IlPreteRosso refactor(Data.Finset.*Antidiagonal): rename defs to `set*Antidiagonal` and deprecate old names in namespace Finset t-algebra new-contributor awaiting-author awaiting author
34077 kbuzzard perf: increase priority of instSMulOfMul t-algebra awaiting-zulip awaiting a zulip discussion
34558 kim-em feat(Topology): add StrictMono finite partition lemmas and path partitioning t-topology awaiting review
26299 adomani perf: the `whitespace` linter only acts on modified files t-linter awaiting-zulip awaiting-author awaiting a zulip discussion
33348 AntoineChambert-Loir feat(LinearAlgebra/Transvection): characterization of transvections among dilatransvections t-algebra awaiting review
34440 grunweg feat: linter for name components in uppercase t-linter large-import maintainer-merge awaiting-author awaiting author
35345 grunweg feat(Linter.openClassical): also lint for Classical declarations as t-linter failing CI
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)
35143 SnirBroshi fix: restore `#min_imports` and other commands large-import file-removed t-meta maintainer-merge awaiting review
35409 JovanGerb chore(Translate): use `Term.applyAttributes` t-meta maintainer-merge awaiting review
34674 Citronhat feat(Algebra/Order/Ring): replace ENNReal lemmas with WithTop versions new-contributor t-algebra merge-conflict merge conflict
34793 MichaelStollBayreuth feat(Algebra/Group/FiniteSupport): new file t-algebra WIP labelled WIP
34658 MichaelStollBayreuth feat(Algebra/Group/FiniteSupport): add HasFinite(Mul)Support and API WIP t-algebra labelled WIP
28582 Thmoas-Guan feat(Data): some lemmas about WithBot ENat t-data awaiting-author awaiting author
31891 jsm28 feat(Geometry/Euclidean/Sphere/OrthRadius): lemmas for setting up and using polars t-euclidean-geometry awaiting review
31892 jsm28 feat(Geometry/Euclidean/Sphere/PolePolar): poles and polars blocked-by-other-PR t-euclidean-geometry blocked on another PR
31893 jsm28 feat(Geometry/Euclidean/Sphere/Tangent): characterize `tangentsFrom` blocked-by-other-PR t-euclidean-geometry blocked on another PR
31981 jsm28 feat(Geometry/Euclidean/Incenter): `tangentSet` and `tangentsFrom` lemmas t-euclidean-geometry blocked-by-other-PR blocked on another PR
34784 tb65536 refactor(GroupTheory/Commutator/Basic): to_additivize commutators t-algebra t-group-theory awaiting review
26214 Thmoas-Guan feat(Algebra): definition of depth t-algebra blocked-by-other-PR large-import blocked on another PR
26215 Thmoas-Guan feat(Algebra): Auslander–Buchsbaum theorem t-algebra blocked-by-other-PR large-import blocked on another PR
26216 Thmoas-Guan feat(Algebra): depth of QuotSMulTop t-algebra blocked-by-other-PR large-import blocked on another PR
26217 Thmoas-Guan feat(Algebra): Ischebeck theorem t-algebra blocked-by-other-PR large-import blocked on another PR
26218 Thmoas-Guan feat(Algebra): definition of cohen macaulay t-algebra blocked-by-other-PR large-import blocked on another PR
26245 Thmoas-Guan feat(Algebra): cohen macaulay local ring is catenary WIP t-algebra blocked-by-other-PR large-import blocked on another PR
34734 FLDutchmann refactor(Tactic): change `ring` to allow for coefficients in a variable type t-meta delegated failing CI
26957 Thmoas-Guan feat(Algebra): unmixed thm of Cohen-Macaulay ring t-algebra blocked-by-other-PR large-import blocked on another PR
33372 kex-y feat(Probability): Countable infimum of stopping times is a stopping time t-measure-probability brownian awaiting review
35360 vlad902 chore: rename `cycleGraph_EulerianCircuit` to `cycleGraph.cycle` t-combinatorics awaiting review
35478 JovanGerb chore: refactor `Lean.MVarId.gcongr` to use a monad t-meta maintainer-merge awaiting review
35113 bryangingechen ci: refactor commit_verification so it works on PRs from forks CI awaiting-author ??? missing CI information
26966 vihdzp feat: the Dedekind–MacNeille completion blocked-by-other-PR t-order blocked on another PR
33650 vihdzp refactor: deprecate bespoke `Hyperreal` machinery t-algebra awaiting review
34598 A-M-Berns feat(Geometry/Polygon): nondegeneracy conditions and interconversion with Affine.Triangle new-contributor t-euclidean-geometry maintainer-merge awaiting review
35472 rao107 feat(Probability): add `CharacteristicFunction` section to binomial distribution new-contributor t-measure-probability blocked-by-other-PR blocked on another PR
35376 michaellee94 feat(Geometry/Manifold): orientable manifolds new-contributor WIP t-differential-geometry blocked-by-other-PR 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 new-contributor blocked-by-other-PR merge-conflict ⚠️ blocked on another PR
35110 bryangingechen ci: refactor maintainer_*.yml workflows to use new helper actions CI awaiting-author ??? missing CI information
35442 dhyan-aranha feat: Affine line with doubled origin counter example new-contributor awaiting-author t-algebraic-geometry awaiting author
26160 oliver-butterley feat(MeasureTheory.VectorMeasure): add several lemmas which characterize variation new-contributor t-measure-probability awaiting review
33252 SnirBroshi chore(Combinatorics/SimpleGraph/Coloring): use `IsIndepSet` instead of `IsAntichain` to spell "a color class is an independent set" t-combinatorics awaiting review
35189 euprunin chore: golf proofs awaiting review
35286 urkud chore: reduce defeq abuse awaiting review
35320 harahu doc(AlgebraicGeometry/Morphisms/Basic): tidy docstrings awaiting review
35329 BryceT233 feat(Data/Finsupp): add computational lemmas for cons and single t-data new-contributor awaiting review
35351 urkud refactor(Algebra/*): generalize `of_ringEquiv` lemmas awaiting review
35365 wwylele feat(LinearAlgebra/Simplex): closedInterior = interior + face.closedInterior t-algebra awaiting review
35381 joelriou feat(CategoryTheory): constructor for abelian categories t-category-theory awaiting review
29558 Thmoas-Guan feat(Algebra): definition of global dimension t-ring-theory blocked-by-other-PR blocked on another PR
32000 Thmoas-Guan feat(Algebra): projective dimension equal supremum of localized module awaiting-author t-algebra failing CI
31879 Thmoas-Guan feat(Algebra/Homology): Projective dimension in linear equiv t-algebra awaiting-author awaiting author
31999 Thmoas-Guan feat(RingTheory): global dimension equals the supremum over localizations awaiting-author blocked-by-other-PR t-ring-theory blocked on another PR
35021 SnirBroshi chore(Data/Bool/Count): golf using grind t-data maintainer-merge awaiting review
28599 Thmoas-Guan feat(RingTheory): polynomial over CM ring is CM t-ring-theory large-import blocked-by-other-PR blocked on another PR
35415 joneugster feat(Cache): enable partial cache in downstream projects CI t-meta merge-conflict merge conflict
35417 joneugster refactor(Cache): use module name for file hash instead of non-resolved file path CI t-meta blocked-by-other-PR merge-conflict blocked on another PR
34193 bwangpj feat(Topology/Algebra/Ring): ContinuousAddEquiv.mulLeft, mulRight t-topology FLT maintainer-merge awaiting review
35201 joelriou feat(CategoryTheory/Sites): points of presheaf toposes WIP t-category-theory blocked-by-other-PR merge-conflict blocked on another PR
35521 grunweg feat: the unusedSetOptionIn linter (rebased) WIP t-linter large-import labelled WIP
34911 smmercuri feat: idelic product formula WIP ⚠️ labelled WIP
26961 mariainesdff feat(RingTheory/PowerSeries/Substitution): add API t-ring-theory awaiting review
32891 felixpernegger feat(Topology/EMetricSpace): Introduction of ```Weak(Pseudo)EMetricSpace``` awaiting-author new-contributor t-topology merge-conflict failing CI
30505 mariainesdff feat(NumberTheory/RatFunc/Ostrowski): prove Ostrowski's theorem for K(X) t-algebra awaiting-author t-number-theory WIP labelled WIP
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
35277 marcelolynch ci: remove outdated logic in workflows file-removed CI awaiting-author ??? missing CI information
34154 euprunin chore: golf using `grind` (and add four supporting `grind` annotations) awaiting review
32245 erdOne feat(RingTheory): the `coassoc_simps` simp set t-ring-theory toric t-meta awaiting review
24383 YaelDillies feat: distributive Haar characters of `ℝ` and `ℂ` WIP awaiting-CI t-measure-probability file-removed FLT opened from a branch in the main mathlib repo (not a fork)
34742 Brian-Nugent feat(SheafCohomology): add API for Sheaf Cohomology new-contributor large-import t-category-theory awaiting review
35303 xroblot feat(RamicationInertia): define decomposition and inertia fields t-number-theory awaiting review
35216 kim-em doc(Tactic/Translate/ToDual): add deployment guide for @[to_dual] documentation awaiting-author enhancement awaiting author
35540 tb65536 feat(GroupTheory/ResiduallyFinite): define residually finite groups t-algebra t-group-theory awaiting review
33842 joelriou feat(Algebra/Homology): spectral sequences WIP t-category-theory large-import blocked-by-other-PR merge-conflict blocked on another PR
35374 joelriou feat(Algebra/Homology/SpectralObject): `HasSpectralSequence` WIP t-category-theory blocked-by-other-PR merge-conflict blocked on another PR
35375 joelriou feat(Algebra/Homology/SpectralObject): first quadrant spectral objects WIP t-category-theory blocked-by-other-PR merge-conflict blocked on another PR
35544 chrisflav feat(RingTheory): `I / I ^ 2` commutes with flat base change t-ring-theory awaiting review
30666 erdOne feat(NumberTheory): every number field has a ramified prime t-number-theory awaiting-author t-algebra failing CI
35552 vihdzp chore(SetTheory/Ordinal/Basic): remove `backward.privateInPublic` t-set-theory awaiting review
34954 brianrabern feat(Combinatorics/SimpleGraph/Acyclic): add colorable and chromaticN… t-combinatorics new-contributor awaiting review
35371 xroblot feat(MulAction): add a SMulDistribClass instance for subgroups t-algebra awaiting review
35386 Brian-Nugent feat: CategoryTheory.toSheafify induces an isomorphism on stalks t-algebraic-geometry t-topology t-category-theory new-contributor awaiting review
34267 Brian-Nugent feat(Topology/Algebra): Add API for Sheaves of abelian groups t-topology new-contributor awaiting review
33416 vihdzp chore(Order/GameAdd): add `elab_as_elim` attributes t-order merge-conflict merge conflict
34637 mcdoll feat(Analysis/Distribution): support t-analysis awaiting review
34240 mcdoll feat(Analysis/Distribution): additional properties of the support WIP t-analysis merge-conflict blocked-by-other-PR 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
35198 j-loreaux feat: generalize Hölder's inequality for sums to `Real.HolderTriple` t-analysis awaiting review
26212 Thmoas-Guan feat(Algebra): the Rees theorem for depth large-import t-ring-theory awaiting review
34491 urkud feat(ContinuousMultilinearMap): generalize some definitions t-analysis awaiting review
34513 urkud feat(ContinuousAlternatingMap): generalize some definitions blocked-by-other-PR t-analysis blocked on another PR
34624 homeowmorphism feat(GroupTheory/FreeGroup/Basic): surjection between types induces surjection between free groups t-group-theory new-contributor awaiting review
34380 Rogerhu12 feat(GroupTheory/Focal): add focal subgroup theorem t-group-theory new-contributor maintainer-merge awaiting review
35352 themathqueen feat(Analysis/CStarAlgebra): the norm of a positive linear functional `f` on a unital C*-algebra is `f 1` t-analysis awaiting-author awaiting author
28682 Thmoas-Guan feat(RingTheory): definition of regular local ring t-ring-theory blocked-by-other-PR blocked on another PR
28684 Thmoas-Guan feat(RingTheory): definition of regular ring t-ring-theory blocked-by-other-PR blocked on another PR
29701 Thmoas-Guan feat(Algebra/RingTheory): polynomial over regular ring t-ring-theory blocked-by-other-PR blocked on another PR
34112 euprunin chore: golf using `grind` (and add one supporting `grind` annotation) maintainer-merge awaiting review
35019 JovanGerb feat(Algebra/Homology/ComplexShape): use `to_dual` maintainer-merge ⚠️ awaiting review
25989 Multramate feat(NumberTheory/EllipticDivisibilitySequence): add elliptic nets t-number-theory large-import awaiting-author awaiting author
34863 JovanGerb feat(to_dual): support recursively reordering arguments ⚠️ awaiting review
35411 daniel-carranza feat(CategoryTheory/Enriched/Limits): define cotensors in an enriched category WIP t-category-theory infinity-cosmos blocked-by-other-PR blocked on another PR
35545 joelriou feat(Algebra/Category/ModuleCat): the internal hom for presheaves of modules t-algebra WIP labelled WIP
28246 Sebi-Kumar feat(AlgebraicTopology/FundamentalGroupoid): the n-sphere is simply connected for n > 1 t-algebraic-topology new-contributor awaiting-author awaiting author
35565 felixpernegger feat(Topology): sequentially T2 spaces t-topology awaiting review
28683 Thmoas-Guan feat(RingTheory): regular local ring is domain t-ring-theory blocked-by-other-PR blocked on another PR
29533 Thmoas-Guan feat(Algebra): maximal Cohen Macaulay module blocked-by-other-PR large-import t-algebra blocked on another PR
29557 Thmoas-Guan feat(Algebra): finite projective dimension of regular blocked-by-other-PR large-import t-algebra blocked on another PR
29534 Thmoas-Guan feat(Algebra): global dimension of regular local ring blocked-by-other-PR large-import t-algebra blocked on another PR
29699 Thmoas-Guan feat(Algebra/RingTheory): global dimension of regular ring blocked-by-other-PR large-import t-algebra blocked on another PR
29796 Thmoas-Guan feat(RingTheory): regular of finite global dimension blocked-by-other-PR 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 large-import t-ring-theory blocked on another PR
29703 Thmoas-Guan feat(Algebra/RingTheory): Hilbert's Syzygy theorem (projective version) blocked-by-other-PR large-import t-ring-theory blocked on another PR
31611 thorimur feat(Meta): `withPlural` wrapper for more readable messages in source t-meta awaiting-author merge-conflict merge conflict
35568 goliath-klein refactor(PiTensorProduct/{InjectiveNorm, ProjectiveNorm}): switch NormedSpace instance to `projectiveSeminorm` blocked-by-other-PR new-contributor blocked on another PR
35569 goliath-klein refactor(PiTensorProduct/{InjectiveNorm, ProjectiveNorm}): deprecate `injectiveSeminorm` blocked-by-other-PR new-contributor blocked on another PR
31697 Thmoas-Guan feat(Homology): bijection between `Ext` t-algebra blocked-by-other-PR t-category-theory blocked on another PR
33792 xroblot feat(GroupTheory/FiniteAbelian): construct bijection between subgroups and subgroups of the dual t-group-theory awaiting review
29909 Vierkantor feat(CI): add build output to CI workflows CI awaiting review
34940 michaellee94 feat: the graph of a continuous function on a $C^n$ manifold is a $C^n$ manifold t-differential-geometry new-contributor awaiting-author awaiting author
31768 Thmoas-Guan feat(Homology): `Ext` commute with ulift functor t-algebra blocked-by-other-PR t-category-theory blocked on another PR
31851 Thmoas-Guan feat(Algebra/Homology): Injective dimension in linear equiv t-algebra blocked-by-other-PR blocked on another PR
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 t-ring-theory awaiting-author awaiting author
31222 Thmoas-Guan feat(Algebra): `Hom` commute with flat base change blocked-by-other-PR large-import t-algebra blocked on another PR
33369 Thmoas-Guan feat(Homology): `Ext` commute with flat base change large-import blocked-by-other-PR t-topology 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)
32942 kim-em feat(CategoryTheory/Monoidal/Rigid): tensor product of exact pairings t-category-theory awaiting-author awaiting author
34249 xyzw12345 feat(GroupTheory/GroupAction/Hom): connect existing definitions `MulDistribMulActionHom` and `DistribMulActionHom` using `to_additive` t-algebra delegated delegated
35497 justus-springer feat(CategoryTheory/Triangulated): add extension_product t-category-theory blocked-by-other-PR merge-conflict blocked on another PR
34705 mpenciak feat(AlgebraicGeometry): Grassmannian functor t-ring-theory awaiting review
29996 vihdzp chore(Order/Concept): `IsIntent` and `IsExtent` t-order maintainer-merge awaiting review
35559 mike1729 feat(Analysis/Normed): weak-topology embedding into weak-star bidual and compactenss transfer theorem t-analysis new-contributor awaiting review
34119 themathqueen feat(LinearAlgebra/Matrix/WithConv): `Matrix.toLin'` as a star-algebra equivalence between their convolutive rings t-algebra blocked-by-other-PR large-import blocked on another PR
29186 winstonyin feat: IsIntegralCurve for solutions to ODEs t-dynamics t-differential-geometry t-analysis awaiting review
35421 farmanb feat(CategoryTheory): preradicals in abelian categories t-category-theory new-contributor awaiting-author awaiting author
35578 Shreyas4991 fix: writer monad should use an additive logging type t-data awaiting-zulip awaiting a zulip discussion
35586 farmanb feat(CategoryTheory/Abelian/Preradical): introduce and characterize radicals blocked-by-other-PR t-category-theory new-contributor blocked on another PR
35585 farmanb feat(CategoryTheory/Abelian/Preradical): add Stenström's colon construction for preradicals blocked-by-other-PR t-category-theory new-contributor blocked on another PR
35317 mkaratarakis feat: lemmas for the analytic part of the proof of the Gelfond–Schneider theorem (Part 5/5) t-number-theory new-contributor t-analysis awaiting review
35510 chrisflav feat(RingTheory): weakly étale algebras WIP t-ring-theory blocked-by-other-PR blocked on another PR
30077 agjftucker feat(Analysis/Calculus/ImplicitFunction): define implicitFunctionOfBivariate t-analysis awaiting review
35266 j-loreaux refactor: make `OrderIso.ofHomInv` take actual `OrderHom`s instead of using classes t-order awaiting review
35423 Rob23oba feat: add congruence lemmas for `Function.update` and `Pi.single` ⚠️ awaiting review
35429 CoolRmal feat: a convex, lower-semicontinuous, and positively homogeneous function is the supremum of a family of linear functions ⚠️ awaiting review
35435 WenrongZou feat(RingTheory/MvPowerSeries): toMvPowerSeries and rename t-ring-theory awaiting review
35438 harahu chore(Tactic): fix indentation in markdown lists 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 new-contributor t-measure-probability awaiting review
35458 harahu chore(Algebra): fix indentation in markdown lists t-algebra awaiting review
33479 zcyemi feat(Geometry/Euclidean/Sphere/Power): Add theorem about cospherical points on two intersecting lines large-import t-euclidean-geometry maintainer-merge awaiting review
35325 SnirBroshi feat(SimpleGraph/Acyclic): `ENat.card V ≤ 2 → G.IsAcyclic` t-combinatorics 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 new-contributor t-order please-merge-master awaiting-author 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 large-import t-combinatorics awaiting review
31884 Thmoas-Guan feat(RingTheory): definition of Gorenstein local ring blocked-by-other-PR t-ring-theory blocked on another PR
31995 Thmoas-Guan feat(RingTheory): Module being injective is local property t-ring-theory large-import awaiting-author awaiting author
32033 Thmoas-Guan feat(Algebra): injective dimension equal supremum of localized module blocked-by-other-PR large-import t-algebra blocked on another PR
32035 Thmoas-Guan feat(RingTheory): localization of Gorenstein local ring blocked-by-other-PR t-ring-theory large-import blocked on another PR
32098 Thmoas-Guan feat(RingTheory): injective dimension of quotSMulTop blocked-by-other-PR t-ring-theory blocked on another PR
33377 Thmoas-Guan feat(RingTheory): polynomial over Gorenstein ring is Gorenstein large-import blocked-by-other-PR t-ring-theory blocked on another PR
35465 MixedMatched feat(Data/Multiset/Powerset): show injectivity and monotonicity of powerset t-data new-contributor awaiting review
33379 Thmoas-Guan feat(RingTheory): Gorenstein local ring is Cohen Macaulay large-import blocked-by-other-PR t-ring-theory blocked on another PR
33380 Thmoas-Guan feat(RingTheory): Gorenstein local ring is Cohen--Macaulay local ring of type one large-import blocked-by-other-PR t-ring-theory blocked on another PR
35528 euprunin chore: golf using `grind` awaiting review
34632 mitchell-horner feat(Combinatorics/SimpleGraph): add `BipartiteDoubleCover` t-combinatorics awaiting review
27599 mitchell-horner feat(Combinatorics/SimpleGraph): define `CompleteEquipartiteSubgraph` t-combinatorics awaiting review
34711 urkud refactor(padicValNat): redefine using `maxPowDvdDiv` awaiting review
35588 eric-wieser chore(Util/Qq): remove `meta` t-meta awaiting-CI opened from a branch in the main mathlib repo (not a fork)
34871 zhuyizheng feat(Calculus): Taylor with integral remainder large-import t-analysis awaiting review
35576 Tehlikeli107 ⚡ [performance] Pre-compile regexes in lake-build-wrapper.py file-removed awaiting-author CI new-contributor ❌? infrastructure-related CI failing
33895 jessealama feat(Computability/Primrec): add list_take, list_drop, list_modify, and list_set new-contributor t-computability awaiting review
34854 GrigorenkoPV chore(Combinatorics/Enumerative/Catalan): split into `Basic` & `Tree` new-contributor awaiting review
35217 kim-em feat: auxiliary lemmas for Artin and braid groups awaiting-author ⚠️ awaiting author
35218 kim-em feat(GroupTheory/Coxeter/Perm): type A Coxeter group maps to symmetric group blocked-by-other-PR ⚠️ blocked on another PR
35219 kim-em feat(GroupTheory/Artin): define Artin groups and their universal property 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)
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
35571 Tehlikeli107 feat(Probability.Process): formalize Brownian motion, Ito calculus, a… t-measure-probability new-contributor failing CI
35209 kim-em chore: use @[to_dual] extensively in CompleteLattice awaiting-author awaiting author
24434 joelriou feat(CategoryTheory): effectiveness of descent merge-conflict WIP t-category-theory blocked-by-other-PR opened from a branch in the main mathlib repo (not a fork)
33543 JovanGerb feat: use `to_dual` for `HeytingAlgebra` t-algebra failing CI
33985 YellPika feat(Order/OmegaCompletePartialOrder): `OmegaCompletePartialOrder` instance for `Sum` with basic `ωScottContinuous` lemmas new-contributor large-import t-order awaiting review
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 t-ring-theory large-import blocked-by-other-PR WIP merge-conflict blocked on another PR
35583 grunweg feat(label_new_contributor): link to the 'why is my PR not on the queue' dashboard CI ??? missing CI information
34873 Hagb feat(RingTheory/MvPolynomial/Groebner/Remainder): polynomial remainder used with Gröbner basis large-import blocked-by-other-PR t-ring-theory WIP merge-conflict blocked on another PR
35364 joelriou feat(CategoryTheory/Triangulated/TStructure): `truncLE` and `truncGT` WIP t-category-theory large-import blocked-by-other-PR merge-conflict blocked on another PR
35367 joelriou feat(CategoryTheory/Triangulated/TStucture): induced t-structures WIP t-category-theory large-import blocked-by-other-PR merge-conflict blocked on another PR
35368 joelriou feat(CategoryTheory/Triangulated/TStructure): extensions of truncations to the extended integers WIP t-category-theory large-import blocked-by-other-PR merge-conflict 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 t-category-theory large-import merge-conflict blocked on another PR
35370 joelriou feat(CategoryTheory/Triangulated/TStructure): the spectral object WIP t-category-theory large-import blocked-by-other-PR merge-conflict blocked on another PR
35589 j-loreaux feat: `SeparatelyContinuousMul` class for multiplication which is continuous in each variable t-topology awaiting review
34966 Deep0Thinking feat(MeasureTheory): add `continuousWithinAt_Ici/Iic_primitive_Ioi/Iio` and `continuousOn_Ici/Iic_primitive_Ioi/Iio/Ici/Iic` new-contributor t-measure-probability awaiting review
35396 joelriou feat(CategoryTheory/Sites): descent data when we have pullbacks t-category-theory awaiting review
35401 joelriou feat(CategoryTheory/Sites): the equivalence between `DescentData'` and `DescentData` WIP t-category-theory blocked-by-other-PR blocked on another PR
35603 2500223210-max feat(GroupTheory/Frattini): add more theorems new-contributor t-group-theory large-import failing CI
35567 goliath-klein refactor(PiTensorProduct/{InjectiveNorm, ProjectiveNorm}): Golfs maintainer-merge new-contributor awaiting review
35326 jano-wol feat: root space decomposition of ideals of Lie algebras t-algebra awaiting review
33082 AntoineChambert-Loir feat(GroupTheory/SpecificGroups/Alternating/Simple): the alternating group on at least 5 letters is simple. t-group-theory awaiting review
35574 bwangpj feat: PrimeSpectrum.irreducibleSpace_iff_nilradical_isPrime t-ring-theory awaiting review
35608 BoltonBailey chore(Computability): move TM files to a single folder t-computability file-removed awaiting review
34144 IvanRenison feat(Data/ENat): add lemma `ENat.iInf_eq_coe_iff` t-data awaiting review
35590 chrisflav feat(Algebra): add `AlgHom.ulift` t-algebra awaiting review
35592 SnirBroshi chore(Order/Defs/Unbundled): deprecate `def Transitive` in favor of `class IsTrans` t-order awaiting review
35609 BoltonBailey chore: deprecate Turing files t-computability blocked-by-other-PR blocked on another PR
34697 wwylele feat(Geometry/Euclidean): the Euclidean volume measure t-euclidean-geometry t-measure-probability awaiting review
35581 mpenciak feat(RingTheory/MvPolynomial): MvPolynomial is isomorphic to the direct sum of its homogeneous submodules t-ring-theory awaiting review
35607 gasparattila fix(Tactic): make `eta_expand` idempotent t-meta awaiting review
35612 joelriou feat(CategoryTheory/Abelian): the localization w.r.t. a Serre class t-category-theory awaiting review
34444 joelriou feat(CategoryTheory): the localization w.r.t. a Serre class is an abelian category WIP t-category-theory blocked-by-other-PR blocked on another PR
35481 FrankieeW chore(NumberTheory/Zsqrtd): inline duplicated order lemmas into instances new-contributor t-number-theory 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
34906 seewoo5 feat(NumberTheory/Bernoulli): von Staudt-Clausen theorem t-number-theory large-import 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
26743 grunweg feat: product rule for Lie bracket on manifolds t-differential-geometry awaiting review
35260 MichaelStollBayreuth feat(Data/Fintype/Order): add API for ciSup with finite indexing type t-order awaiting review
35261 j-loreaux feat: `push` lemmas for `Filter.NeBot` t-order awaiting review
35304 euprunin chore: golf proofs awaiting review
35312 Komyyy feat(Order/Filter/Pointwise): `((∀ᶠ|∃ᶠ) x in op f, p x) ↔ ((∀ᶠ|∃ᶠ) x in f, p (op x))` t-order awaiting review
35355 joelriou feat(Algebra/Homology/SpectralSequence): complex shapes for pages of spectral sequences t-algebra t-category-theory awaiting review
35357 joelriou feat(Algebra/Homology): definition of spectral objects in abelian categories t-algebra t-category-theory awaiting review
35358 wwylele feat(Geometry/Euclidean): Simplex.closedInterior is closed t-euclidean-geometry maintainer-merge awaiting review
35362 joelriou feat(CategoryTheory/Triangulated/TStructure): more on `truncLT` and `truncGE` t-category-theory awaiting review
35391 peabrainiac feat(Geometry/Manifold): API for extended coordinate changes t-differential-geometry awaiting review
35405 xroblot feat(RamificationInertia): add `ramificationIdx_le_ramificationIdx` and `inertiaDeg_le_inertiaDeg` t-number-theory awaiting review
35416 joneugster feat(Data/Set/Basic): add some missing lemmas t-data awaiting review
35486 Vierkantor chore(Tactic): improve `continuity` tactic and attribute docstrings documentation t-meta maintainer-merge awaiting review
35487 xgenereux feat(Submodule/Lattice): Add `Submodule.disjoint_iff_add_eq_zero` t-algebra awaiting review
35495 Vierkantor chore(Tactic): improve `econstructor` and `fconstructor` tactic docstrings documentation t-meta maintainer-merge awaiting review
35502 Vierkantor chore(Tactic): document `existsi`, `use` and `use_discharger` tactics documentation t-meta maintainer-merge awaiting review
35508 chrisflav feat(AlgebraicGeometry): Zariski sheaves preserve products t-algebraic-geometry large-import awaiting review
35554 vihdzp refactor: deprecate `Trunc` in favor of `Squash` t-data awaiting-CI does not pass CI
35628 SnirBroshi feat(Combinatorics/SimpleGraph/Maps): characterize `neighborSet` and `edgeSet` across an embedding t-combinatorics awaiting review
12933 grunweg chore: replace some use of > or ≥ by < or ≤ merge-conflict awaiting-author ??? opened from a branch in the main mathlib repo (not a fork)
35630 SnirBroshi feat(Data/List/Basic): relate `dropLast` and `concat` t-data awaiting review
27274 peabrainiac feat(Geometry/Diffeology): continuous diffeologies & D-topology-lemmas merge-conflict t-differential-geometry merge conflict
35632 SnirBroshi feat(Data/List/TakeDrop): `take`/`drop` + `tail`/`dropLast` almost commute t-data awaiting review
35620 inaciovasquez2020 feat(Fintype): choose element from nonempty finite type t-data new-contributor 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
33449 yuanyi-350 feat(ProbabilityTheory): Add Poisson limit theorem t-measure-probability awaiting review
35622 SnirBroshi feat(Logic/Function/Basic): `onFun` and `swap` preserve relation properties t-logic awaiting review
35610 IvanRenison feat(Data/Fin): add several lemmas about subtraction of `Fin.{castLT, castAdd, castSucc, castPred}` t-data awaiting review
35470 kim-em chore(Algebra/Quaternion): make `Quaternion` instance_reducible tech debt t-analysis awaiting review
33214 JJYYY-JJY chore(Data/List/Rotate): add simp attributes t-data new-contributor awaiting-author awaiting author
35643 chrisflav chore(Algebra): make `TensorProduct.equivOfCompatibleSMul` more linear t-algebra awaiting review
35647 BryceT233 feat(RingTheory/Ideal/Quotient): add a canonical inclusion map t-ring-theory new-contributor awaiting review
35530 xroblot feat(RingTheory): add the class `HasFiniteQuotients` t-ring-theory awaiting review
35651 sun123zxy feat(Mathlib/RingTheory/Ideal/Cotangent): `Submodule.map` definition of cotangent spaces t-ring-theory new-contributor awaiting review
33714 idontgetoutmuch feat(Mathlib/Geometry/Manifold): Riemannian metrics exist II t-differential-geometry new-contributor awaiting-author awaiting author
35072 vasnesterov feat(Tactic/ComputeAsymptotics/Multiseries): non-primitive corecursion for `Seq`: `FriendlyOperation` API t-data t-meta awaiting review
34941 urkud feat(FDeriv/Prod): generalize to TVS blocked-by-other-PR t-analysis blocked on another PR
34246 staroperator feat(SetTheory/Cardinal): Δ-system lemma t-set-theory awaiting review
34881 CBirkbeck feat(ModularForm/NumberTheory/Delta): Define the delta function ⚠️ awaiting review
35653 pepamontero feat: add ChartedSpace structure on orbit space new-contributor ⚠️ awaiting review
33764 IvanRenison feat(Combinatorics/SimpleGraph/Diam): drop `Finite α` from `ediam_le_two_mul_radius` t-combinatorics awaiting review
34937 tannerduve feat(Computability): semilattice instance on Turing degrees t-computability new-contributor large-import awaiting review
34727 ocfnash feat: the Geck construction yields a Lie algebra with the expected Cartan matrix WIP t-algebra please-merge-master labelled WIP
35482 xgenereux feat: generalize `prod_eq_mul_prod_diff_singleton` ⚠️ awaiting review
35295 Rida-Hamadani feat(SimpleGraph): `dropLast` of a cycle is a path t-combinatorics awaiting review
35402 samueloettl feat(Dynamics/BirkhoffSum): birkhoffAverage const t-dynamics new-contributor awaiting review
35659 BryceT233 chore(Data/Finsupp): update pointwise module structure t-data new-contributor awaiting review
35655 Rida-Hamadani feat(SimpleGraph): strongly regular graphs have diameter 2 blocked-by-other-PR t-combinatorics blocked on another PR
35660 BryceT233 feat(LinearAlgebra/Finsupp): add lemmas about `lsum` and submodule t-algebra new-contributor large-import awaiting review
35661 chrisflav feat(Geometry/Manifold): a smooth map induces a morphism of locally ringed spaces t-algebraic-geometry t-differential-geometry awaiting review
32941 kim-em feat(GroupTheory/Artin): add braid groups as Artin groups of type A t-group-theory blocked-by-other-PR blocked on another PR
32987 kim-em feat: pipeline downloads and decompression in `cache get` t-meta awaiting review
35233 kim-em chore: run `lake shake --add-public --keep-implied --keep-prefix --fix` large-import failing CI
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)
35657 Rida-Hamadani feat(SimpleGraph): distance equal or greater than two in terms of common neighborhood t-combinatorics awaiting review
35321 harahu doc: capitalize the proper name Kan easy awaiting review
35504 JoaBjo feat(Probability/Distributions/Exponential): add MGF, moments, and memoryless property new-contributor t-measure-probability awaiting review
35514 farmanb feat(CategoryTheory/Abelian/Preradical): introduce basic definition of preradicals t-category-theory new-contributor awaiting review
35515 WenrongZou feat(Topology/HomotopyGroup): Homeomorphism between GenLoop t-topology awaiting review
35516 chrisflav feat(RingTheory): pure ideals t-ring-theory awaiting review
35531 mariainesdff feat(FieldTheory/Finite/Valuation): add IsTrivialOn t-algebra opened from a branch in the main mathlib repo (not a fork)
35534 xgenereux feat(Torsion/Basic): Add a few convenient lemmas for torsion submodules t-algebra awaiting review
27953 CoolRmal feat(ProbabilityTheory): Conditional Jensen's Inequality new-contributor t-measure-probability failing CI
35446 kbuzzard perf: try lowering prio for A(0) instances, A a graded object t-algebra awaiting review
35602 JovanGerb feat: replace `IsWellFounded` with `WellFounded` ⚠️ failing CI
35649 JovanGerb feat(Order/GaloisConnection/Defs): use `to_dual` for `GaloisInsertion`/`GaloisCoinsertion` ⚠️ failing CI
35672 dennj feat(RingTheory/Polynomial/Cyclotomic): vanishing sums and fiber equidistribution at primitive roots t-ring-theory new-contributor awaiting review
33746 ster-oc feat(Algebra/Module/ZLattice): align `ZSpan.floor` to `Int.floor` API t-algebra new-contributor merge-conflict merge conflict
35213 kim-em chore: use @[to_dual] in ConditionallyCompleteLattice blocked-by-other-PR merge-conflict blocked on another PR
35214 kim-em chore: use @[to_dual] in GaloisConnection and Interval.Set.Disjoint blocked-by-other-PR merge-conflict blocked on another PR
35215 kim-em chore: use @[to_dual] in FixedPoints awaiting-author merge-conflict merge conflict
35328 astrainfinita chore: use `IsLUB` `IsGLB` in `CompleteLattice` `ConditionallyCompleteLattice` t-order awaiting review
35652 dennj feat(LinearAlgebra/Matrix): add `Matrix.mul_eq_smul_one_symm` t-algebra new-contributor awaiting review
35675 Thmoas-Guan feat(RingTheory/Smooth): some lemma about formally smooth t-ring-theory awaiting review
33840 vihdzp feat(SetTheory/Ordinal/CantorNormalForm): Evaluate a Finsupp as a CNF t-set-theory awaiting review
35011 whocares-abt feat(Combinatorics/SimpleGraph/Copy): add degree of copy less than original t-combinatorics new-contributor awaiting review
35637 vihdzp chore(Topology/Order/LeftRight): use `to_dual` awaiting review
35654 euprunin chore: golf using `grind` awaiting review
35673 Parcly-Taxel feat: radical lemmas for natural numbers and integers file-removed t-ring-theory awaiting review
35635 vihdzp chore(Order/Interval/Set/LinearOrder): use `to_dual` t-order awaiting-CI 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 t-differential-geometry merge-conflict t-meta labelled WIP
30421 grunweg feat: support products in the differential geometry elaborators t-differential-geometry merge-conflict WIP labelled WIP
35532 mariainesdff feat(Ringtheory/DedekindDomain): add RingEquiv lemmas t-ring-theory opened from a branch in the main mathlib repo (not a fork)
35394 HugLycan feat(Tactic/Positivity): make positivity work for types that are not partial orders new-contributor t-meta awaiting-author awaiting author
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)
35625 vihdzp chore: make `liftFun_antisymmRel` public t-order maintainer-merge awaiting review
26292 RemyDegenne feat(MeasureTheory): tightness of the range of a sequence t-measure-probability awaiting-author awaiting author
34215 justus-springer feat(FieldTheory/RatFunc): Degree of field extension K(X)/K(f) t-algebra new-contributor awaiting review
28291 vasnesterov feat(Tactic): tactic for computing asymptotics of real functions WIP t-analysis t-meta large-import blocked-by-other-PR blocked on another PR
34877 justus-springer refactor(RingTheory/Localization/Integral): Simplify `integerNormalization` t-ring-theory awaiting review
29550 Raph-DG feat(RingTheory): Order of vanishing in a discrete valuation ring file-removed t-ring-theory awaiting-author failing CI
35477 harahu chore(Geometry): fix markdown lists 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 ℤ` t-group-theory new-contributor awaiting review
35535 mariainesdff feat(RingTheory/ClassGroup): prove mulEquiv t-ring-theory awaiting-CI opened from a branch in the main mathlib repo (not a fork)
35671 CoolRmal feat: APIs for semifinite measures WIP t-measure-probability labelled WIP
29449 mitchell-horner feat(Combinatorics/SimpleGraph): more API for Turán density t-combinatorics large-import awaiting-author awaiting author
34773 semaraugusto feat(InformationTheory): add Shannon entropy for probability mass functions new-contributor awaiting-author ⚠️ awaiting author
35666 urkud chore(Calculus/FDeriv/Pi): migrate to TVS blocked-by-other-PR blocked on another PR
30872 rudynicolop feat(Computability/NFA): NFA closure under concatenation t-computability new-contributor maintainer-merge awaiting-author failing CI
35681 harahu chore(CategoryTheory): fix indentation in markdown lists t-category-theory awaiting review
33461 loefflerd feat(NumberTheory/Modular): stabilizers for action on upper halfplane WIP large-import ⚠️ labelled WIP
35639 vihdzp chore(Order/SuccPred/Limit): use `to_dual` on everything that was missing awaiting review
33972 YuvalFilmus feat(Analysis/Polynomial/Order): polynomial has fixed sign beyond largest root t-analysis awaiting-zulip awaiting a zulip discussion
35662 FrankieeW feat(NumberTheory/Zsqrtd): add Archimedean instance via le_arch t-number-theory new-contributor awaiting review
35677 euprunin chore(SetTheory): golf proofs t-set-theory awaiting review
32989 kim-em fix(Tactic/Simps): skip @[defeq] inference for non-exposed definitions t-meta maintainer-merge awaiting-author failing CI
35491 mariainesdff feat(RingTheory/Noetherian/Basic): prove IsNoetherianRing.of_ringEquiv t-ring-theory awaiting-author opened from a branch in the main mathlib repo (not a fork)
35136 joelriou feat(AlgebraicGeometry): points of the small étale site WIP t-algebraic-geometry blocked-by-other-PR large-import merge-conflict blocked on another PR
34830 parabamoghv feat(CategoryTheory/Monoidal): add definition of categorical groups t-category-theory new-contributor WIP labelled WIP
35180 grunweg fix(Geometry/Manifold/Notation): better error message if the expected type contains metavariables t-differential-geometry easy t-meta awaiting review
35669 SnirBroshi feat(Mathlib/Data/Finset/Mex): `sInf sᶜ ≤ s.encard` t-order awaiting review
35690 AntoineChambert-Loir feat(Algebra/TrivSqZeroExt): the canonical ideal has square zero t-algebra large-import awaiting review
33688 Citronhat feat(PMF): add expectation lemmas for Poisson PMF new-contributor t-measure-probability awaiting-author awaiting author
34055 sgouezel feat: vector measures associated to functions of bounded variation t-measure-probability awaiting review
35693 euprunin chore: avoid passing explicit lemmas to `grind` and (terminal) `simp_all` where unnecessary awaiting review
35683 gasparattila fix(Tactic/FunProp): detect `Continuous.subtype_mk` as compositional t-meta awaiting review
35593 chrisflav feat(RingTheory/Extension): naive cotangent complex commutes with flat base change t-ring-theory blocked-by-other-PR blocked on another PR
35694 AntoineChambert-Loir feat(Data/Finset/Sym): prove two lemmas t-data awaiting review
30658 grunweg feat: extend the `whitespace` linter to proof bodies blocked-by-other-PR large-import t-linter merge-conflict blocked on another PR
31766 SuccessMoses feat(Topology/EMetricSpace): continuity of arc length new-contributor t-topology awaiting-author merge-conflict merge conflict
35696 GrigorenkoPV fix(Data/Rel): change what `image_eq_cod_of_dom_subset` states t-data new-contributor ??? missing CI information
35695 euprunin chore: replace `aesop` with `lia` where possible awaiting review
35682 chenson2018 chore(Computability/Partrec): remove `linter.flexible` exceptions t-computability maintainer-merge awaiting review
35699 chrisflav chore(RingTheory/Etale/Kaehler): mention `FormallyEtale` in the names t-ring-theory awaiting review
35656 euprunin chore(ModelTheory): golf proofs t-logic awaiting review
33143 wwylele feat(PowerSeries): pentagonal number theorem t-algebra awaiting review
35594 chrisflav feat(RingTheory): `Extension.CotangentSpace` commutes with base change t-ring-theory blocked-by-other-PR blocked on another PR
34917 chrisflav feat(AlgebraicGeometry/Sites): characterization of sheaves for the `P`-qc topology WIP t-algebraic-geometry large-import blocked-by-other-PR blocked on another PR
35697 gasparattila chore: call `dsimp` in the default tactics of `Homeomorph` fields blocked-by-other-PR blocked on another PR
33935 mckoen feat(CategoryTheory/Monoidal/Arrow): define monoidal structure on arrow category t-category-theory awaiting review
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 t-group-theory new-contributor awaiting review
34922 vasnesterov feat(Tactic/ComputeAsymptotics/Multiseries): Multiseries definition and structural lemmas t-data t-meta awaiting review
35035 joelriou feat(CategoryTheory/Limits/FormalCoproducts): an extradegeneracy for the Cech object t-category-theory awaiting review
35403 tb65536 feat(Topology/Algebra/Ring/Ideal): the connected component of zero is an ideal t-algebra t-ring-theory t-topology awaiting review
35408 MichaelStollBayreuth feat(NumberTheory/Height/Basic): add {mul|log}Height_comp_le, {mul|log}Height_fun_mul_eq t-number-theory awaiting review
35439 harahu chore(RingTheory): fix indentation in markdown lists t-ring-theory awaiting review
35440 harahu chore(Order): fix indentation in markdown lists t-order awaiting review
35539 xgenereux feat(DedekindDomain/Factorization): add `iInf` version of `finprod_heightOneSpectrum_factorization` t-ring-theory awaiting review
35549 JovanGerb fix(Translate): don't look in arguments of free variables in `shouldTranslate` t-meta awaiting review
35573 antisubnoous feat(NumberTheory/Chebyshev): express the Chebyshev theta function in terms of the prime counting function t-number-theory new-contributor awaiting review
30982 jsm28 feat(Geometry/Euclidean/Angle/Incenter): angle bisection and the incenter t-euclidean-geometry awaiting review
32282 jsm28 feat(Geometry/Euclidean/Angle/Incenter): unoriented angle bisection t-euclidean-geometry blocked-by-other-PR blocked on another PR
32294 jsm28 feat(Geometry/Euclidean/Angle/Incenter): distance from second intersection with circumcircle t-euclidean-geometry blocked-by-other-PR blocked on another PR
32295 jsm28 feat(Archive/Imo/Imo2024Q4): IMO 2024 Q4 IMO blocked-by-other-PR blocked on another PR
34288 winstonyin feat: Integral curve is smooth in initial condition t-analysis awaiting review
29870 mckoen feat(CategoryTheory/Adhesive): subobjects in adhesive categories have binary coproducts t-category-theory awaiting-author awaiting author
34717 CoolRmal feat: add more APIs for the first derivative test WIP ⚠️ labelled WIP
34543 j-loreaux refactor: improve API connecting `ℝ`- and `𝕜`-linear functionals t-analysis awaiting-author awaiting author
35597 BryceT233 feat(AdicTopology): add lemmas about adic topology t-topology new-contributor awaiting review
35703 plp127 chore(Data/Fin/Tuple/Basic): rename recursor arguments awaiting review
35000 plp127 feat(Algebra/Polynomial/PartialFractions): generalize to powers t-algebra delegated delegated
24065 kim-em chore: script to give topological sort of modules awaiting-author merge-conflict opened from a branch in the main mathlib repo (not a fork)
33691 kim-em feat(scripts): add find-ci-errors.sh to diagnose widespread CI failures CI delegated merge-conflict merge conflict
35078 grunweg feat: immersed points WIP blocked-by-other-PR merge-conflict ⚠️ blocked on another PR
35175 joelriou feat(CategoryTheory/Sites): characterization of conservative families of points WIP t-category-theory blocked-by-other-PR merge-conflict blocked on another PR
35605 j-loreaux feat: transfer instances of `ContinuousFunctionalCalculus` to type synonyms with weaker topologies merge-conflict ⚠️ failing CI
35707 BryceT233 feat(RingTheory/MvPowerSeries): introduce `truncTotal` new-contributor ⚠️ awaiting review
35709 tb65536 feat(AlgebraicGeometry/EllipticCurve/Reduction): define multiplicative and additive reduction t-algebra t-algebraic-geometry t-number-theory ??? missing CI information
33780 ooovi feat(Geometry/Convex/Cone): lineality space of pointed cones t-convex-geometry awaiting review
33942 artie2000 feat(Algebra/Group/Submonoid): submonoid support t-algebra awaiting-author awaiting author
35710 tb65536 feat(AlgebraicGeometry/EllipticCurve/Reduction): define split multiplicative reduction t-algebra t-algebraic-geometry t-number-theory blocked-by-other-PR blocked on another PR
35572 joelriou feat(CategoryTheory/Sites/Point): fiber functors are monoidal t-category-theory 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
33958 chrisflav feat(AlgebraicGeometry): the small affine étale site WIP t-algebraic-geometry blocked-by-other-PR blocked on another PR
35287 arnoudvanderleer feat(AlgebraicTopology/SimplicialSet): define isomorphisms in simplicial sets, and the coherent isomorphism simplicial set t-algebraic-topology new-contributor infinity-cosmos awaiting-author awaiting author
35646 BryceT233 feat(Algebra): add two lemmas about submodule smul new-contributor ⚠️ awaiting review
35642 SnirBroshi feat(SimpleGraph/Walks/Operations): `p.dropLast.length` lemmas t-combinatorics awaiting review
32704 euprunin chore: remove use of `erw` awaiting-author t-topology t-category-theory t-measure-probability awaiting author
35555 JovanGerb perf: add `AddMonoid` shortcut instance for linear maps merge-conflict merge conflict
35714 harahu chore(misc): fix indentation in markdown lists IMO awaiting review
35680 joelriou feat(CategoryTheory/Sites): alternative constructor for points WIP t-category-theory labelled WIP
33757 fpvandoorn feat: classical "decidability" instances on sets and ideals t-ring-theory t-data failing CI
35670 BryceT233 feat(RingTheory/AdicCompletion): completeness of `AdicCompletion` blocked-by-other-PR new-contributor ⚠️ blocked on another PR
35665 BryceT233 feat(RingTheory/AdicCompletion): introduce AdicCompletion.finsuppSum new-contributor ⚠️ awaiting review
35684 spitters feat(CategoryTheory/MarkovCategory): Kleisli PMF is a Markov category t-category-theory new-contributor awaiting review
35713 Parcly-Taxel feat: Bird–Wadler duality theorems ⚠️ awaiting review
34120 winstonyin feat: `GroupWithZero` versions of `le` lemmas WIP ⚠️ labelled WIP
26872 faenuccio chore(RingTheory/Valuation/RankOne): modify the definition of Valuation.RankOne using its range rather than its codomain t-algebra blocked-by-other-PR merge-conflict blocked on another PR
35715 joelriou feat(Alebra/Category/ModuleCat/Sheaf): the category of sheaves of modules is a localization of the category of presheaves of modules t-algebra t-category-theory awaiting review
35698 chrisflav feat(CategoryTheory/Sites): `Presieve.IsSheafFor` is local on the target t-category-theory awaiting review
34713 dennj feat(Probability/Markov): stationary distributions for stochastic matrices t-algebra new-contributor awaiting review
35705 jdhart81 feat(Data/ENNReal, Probability/Independence): division decomposition and self-independence new-contributor ⚠️ failing CI
35084 edegeltje feat(Combinatorics/SimpleGraph): The Cayley graph for structures with `Mul`/`Add` t-combinatorics awaiting review
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 awaiting-author t-ring-theory blocked-by-other-PR blocked on another PR
30204 yonggyuchoimath feat(Algebra/Category/Ring/EqualizerPushout): add effectiveEpi_of_faithfullyFlat in CommRingCatᵒᵖ blocked-by-other-PR t-category-theory ??? blocked on another PR
32058 Thmoas-Guan feat(Algebra): category version Baer criterion t-algebra t-category-theory awaiting-author awaiting author
34944 jessealama feat(Algebra/Ring/NegOnePow): add negOnePow ↔ natAbs bridge lemmas t-algebra awaiting review
35150 JovanGerb chore(Order/OrderDual): move material on `OrderDual` large-import t-order awaiting review
29776 yuanyi-350 chore: refactor `ContinuousLinearMap.isOpenMap` by separating it into sublemmas WIP t-analysis labelled WIP
29354 themathqueen refactor(Algebra/Algebra/Equiv): allow for non-unital `AlgEquiv` t-algebra awaiting-author failing CI
35513 vihdzp refactor: redefine `Order.cof` for a preorder t-set-theory t-order awaiting review
30640 SnirBroshi feat(Combinatorics/SimpleGraph/Acyclic): acyclic and bridge theorems + golfing t-combinatorics maintainer-merge awaiting review
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 large-import t-computability failing CI
35627 SnirBroshi feat(Combinatorics/SimpleGraph/Finite): min/max degrees of top/bot t-combinatorics awaiting review
35283 Multramate feat(Algebra/Polynomial): add Polynomial.algHomEquiv and its bivariate version t-algebra easy awaiting-author awaiting author
35437 harahu chore(Topology): fix indentation in markdown lists t-topology awaiting review
35494 Timeroot feat(Topology/Perfect): simp frontier_singleton t-topology awaiting-author awaiting author
35706 vihdzp chore(Algebra/Group/Finsupp): fix argument names t-algebra awaiting-author awaiting author
35718 Parcly-Taxel chore: remove some `respectTransparency` options failing CI
33364 BoltonBailey feat(Analysis/Convex/SimplicialComplex): add AbstractSimplicialComplex + constructions t-analysis t-algebraic-topology maintainer-merge awaiting review
35272 jvanwinden feat(Topology/Instances/EReal): limsup of multiplication by a constant t-topology new-contributor merge-conflict awaiting-author merge conflict
35721 chrisflav chore: fix delaborators for `[Comm][Semi]RingCat` and some more t-algebra awaiting review
33501 SnirBroshi feat(Combinatorics/SimpleGraph/Finite): degrees for infinite graphs large-import t-combinatorics awaiting-author merge-conflict merge conflict
26770 Jun2M feat(Combinatorics/Graph): subgraph relations on `Graph` t-combinatorics awaiting review
35719 joelriou feat(CategoryTheory/Sites): skyscraper sheaves t-category-theory ??? missing CI information
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)) new-contributor t-category-theory infinity-cosmos awaiting-author awaiting author
26303 joelriou feat(AlgebraicTopology): the fundamental lemma of homotopical algebra t-algebraic-topology t-category-theory awaiting review
35098 b-mehta feat(Analysis/Normed): relate compactness of operators to locally compact spaces t-analysis awaiting-author merge-conflict merge conflict
34777 sqrt-of-2 WIP: feat(Combinatorics/SetFamily/Intersecting): L-intersecting families t-combinatorics new-contributor WIP labelled WIP
35493 xroblot feat(RamificationInertia): add `ramificationIdx_algebra_tower'` t-number-theory awaiting review
35711 joelriou chore(CategoryTheory/Sites): fix IsSheaf.isSheafFor t-category-theory maintainer-merge awaiting review
30122 xroblot Development branch (1) WIP large-import labelled WIP
21342 YaelDillies refactor(Normed/Group/Quotient): generalise to non-abelian groups t-analysis merge-conflict opened from a branch in the main mathlib repo (not a fork)
35722 joelriou feat(CategoryTheory/Sites): the fiber functor associated to `Point.comap` WIP t-category-theory blocked-by-other-PR blocked on another PR
34848 bjornsolheim feat(Analysis/Convex/Cone): min and max tensor products are equal when one factor is simplicial and generating t-analysis awaiting-author awaiting author
34867 urkud feat(FDeriv/Comp): migrate to TVS t-analysis awaiting-author awaiting author
35280 khwilson feat(Mathlib/Analysis/Polynomial/MahlerMeasure): Mahler Measure estimate in terms of supNorm t-analysis new-contributor awaiting-author merge-conflict ❌? infrastructure-related CI failing
35720 tb65536 feat(NumberTheory/FunctionField): add instances on `FqtInfty` t-topology t-algebra awaiting review
35496 justus-springer feat(CategoryTheory/Triangulated): Rotated octahedron axiom t-category-theory awaiting review
34419 ster-oc feat(RCLike): add `Continuous.re` and similar t-analysis new-contributor awaiting-author awaiting author
35598 Paul-Lez feat(CategoryTheory/Abelian/Exact): add easy lemmas about short exactness WIP t-category-theory labelled WIP
35724 matthewjasper feat(RingTheory/DedekindDomain/AdicValuation): v-adic integers of `K` are a localization at v^c t-ring-theory new-contributor large-import FLT awaiting review
33129 Paul-Lez feat(Tactic/Simproc/VecPerm): add simproc for permuting entries of a vector t-meta failing CI
30357 grunweg chore: golf using custom elaborators t-differential-geometry awaiting-author awaiting author
35599 tb65536 feat(RingTheory/Lasker): second uniqueness theorem for primary decomposition t-ring-theory t-algebra awaiting review
35039 wwylele feat(LinearAlgebra/AffineSpace): small lemmas about lineMap and homothety t-algebra awaiting review
35664 Rida-Hamadani feat(SimpleGraph): the adjacency matrix of empty and complete graphs t-combinatorics awaiting review
34091 staroperator feat(SetTheory/Cardinal): generalize infinite pigeonhole principle t-set-theory delegated delegated
32305 faenuccio feat: define Sobolev Spaces merge-conflict WIP t-analysis large-import blocked-by-other-PR opened from a branch in the main mathlib repo (not a fork)
30811 yonggyuchoimath feat(AlgebraicGeometry.EffectiveEpi): effective epimorphisms in schemes blocked-by-other-PR t-algebraic-geometry blocked on another PR
31338 grunweg chore: move Pretrivialization, Trivialization to the Bundle namespace merge-conflict t-differential-geometry merge conflict
33406 dupuisf feat: add basics of majorization t-analysis awaiting-author awaiting author
35731 euprunin chore: golf using `exact`/`simpa` awaiting review
35726 euprunin chore: golf using `simp` awaiting review
35315 mkaratarakis feat: lemmas for the analytic part of the proof of the Gelfond–Schneider theorem (Part 3/5) t-analysis new-contributor awaiting-author failing CI
29960 yonggyuchoimath feat(Algebra/Category/Ring): equalizers of pushout maps of tensor product inclusions new-contributor t-ring-theory awaiting-author awaiting author
34209 mike1729 feat(Analysis/Normed): Schauder basis definition and characterization via projections t-analysis new-contributor awaiting-author awaiting author
35733 mkaratarakis feat: Algebraic setup and matrix coefficients for Gelfond-Schneider theorem t-number-theory new-contributor ❌? infrastructure-related CI failing
35467 ZRTMRH feat(Combinatorics): add Schreier graphs, Cayley graphs, and Cayley sum graphs t-combinatorics new-contributor awaiting review
35734 mkaratarakis feat(NumberTheory): matrix bounds and Siegel's lemma application for Gelfond-Schneider new-contributor t-number-theory blocked-by-other-PR blocked on another PR
26304 Raph-DG feat(AlgebraicGeometry): Definition of algebraic cycles t-algebraic-geometry RFC awaiting-author awaiting author
33466 Shreyas4991 refactor(Combinatorics/Digraph): add vertex sets t-combinatorics awaiting-author please-adopt looking for help
35538 bilichboris feat(Analysis/VonNeumannAlgebra): double commutant theorem t-analysis new-contributor awaiting-author awaiting author
34932 erdOne feat(AlgebraicGeometry): formally etale morphisms t-algebraic-geometry maintainer-merge awaiting review
35529 joelriou feat(CategoryTheory/Sites): characterization of covering sieves using locally surjective morphisms t-category-theory awaiting-author awaiting author
34919 kebekus feat: singleton indicators as functions with locally finite support t-topology delegated delegated
35735 mkaratarakis feat(NumberTheory): analytical properties and lower bounds for Gelfond-Schneider auxiliary function t-number-theory new-contributor blocked-by-other-PR blocked on another PR
35650 grunweg covariant derivatives sandbox WIP t-differential-geometry awaiting-CI merge-conflict labelled WIP
34805 DavidLedvinka feat(Tactic): generalize ofScientific NormNum extension to `DivisionSemiring` t-meta awaiting-author awaiting author
35716 IvanRenison feat(Combinatorics/SimpleGraph/Connectivity): add lemmas about reachable, degree and neighbor set t-combinatorics awaiting review
35097 pevogam feat: add a LE version of previous lt_one_iff_num_lt_denom theorem t-algebra new-contributor easy awaiting-author awaiting author
35737 kim-em chore: remove no-longer-needed backwards compatibility options awaiting review
35736 mathlib-splicebot chore(Mathlib/Topology/Algebra/Module/LinearMap.lean): automated extraction new-contributor t-topology opened from a branch in the main mathlib repo (not a fork)
34204 loefflerd feat(LinearAlgebra/QuadraticForm): Sylvester's law of inertia t-algebra awaiting review
29251 yoh-tanimoto feat(Analysis/InnerProductSpace/): define standard subspaces of a complex Hilbert space t-analysis awaiting-author awaiting author
35337 Thmoas-Guan feat(RingTheory): some lemma about span rank t-ring-theory awaiting-author awaiting author
35080 rwst doc(RingTheory/PowerSeries/Derivative): main def/stmts, docstrings t-ring-theory awaiting-author awaiting author
35564 kebekus feat: introduce `HarmonicContOnCl` t-analysis awaiting-author awaiting author
35732 TJHeeringa feat: Added reproducing kernels new-contributor ⚠️ failing CI
35717 chrisflav feat(AlgebraicGeometry): weakly étale morphisms t-algebraic-geometry awaiting review
26479 thefundamentaltheor3m feat(Analysis/Complex/CauchyIntegral): Cauchy–Goursat for Unbounded Rectangles new-contributor t-analysis sphere-packing awaiting-author awaiting author
35464 tb65536 feat(Analysis/InnerProductSpace/Rayleigh): the norm of a symmetric operator is the supremum of the Rayleigh quotients t-analysis ready-to-merge ❌? contradictory labels
35689 kebekus chore: add theorem attributes, trivial theorems on orders of meromorphic functions t-analysis delegated delegated
35727 euprunin chore(Analysis/Complex): simplify proof of `Complex.orderClosedTopology` t-analysis awaiting review
34402 loefflerd feat(Analysis/Complex/UpperHalfPlane): invariant measure large-import t-analysis awaiting-author awaiting author
35738 GrigorenkoPV perf: remove some `aesop`s and `grind`s new-contributor ??? missing CI information
35582 nielsvoss feat(Analysis/InnerProductSpace): add theorems about the adjoint, kernel, range, and orthogonal complement t-analysis new-contributor awaiting-author awaiting author
35445 themathqueen feat(Analysis): `{LinearMap, Matrix}.trace` as a positive linear map t-analysis large-import delegated delegated
35057 grunweg feat: equivalent characterisation of split continuous linear maps t-analysis ready-to-merge awaiting bors
30339 grunweg feat: extend a tangent vector for a locally smooth vector field t-differential-geometry awaiting-CI does not pass CI
35100 stepan2698-cpu feat: definition of a character of a representation t-algebra new-contributor awaiting review
35739 chrisflav chore(Algebra): fix diamond with `Algebra.compHom` at reducible transparency t-algebra ??? missing CI information
35174 nielsvoss feat(Analysis/InnerProductSpace): a linear map composed with its adjoint is symmetric t-analysis new-contributor ready-to-merge awaiting bors
35183 tb65536 feat(Analysis/InnerProductSpace/Rayleigh): basic API for Rayleigh quotients t-analysis ready-to-merge awaiting bors
34049 smmercuri refactor: use 1-field structure to define the `WithVal` type synonym t-topology awaiting-author awaiting author
35626 vihdzp chore(Order/InitialSeg): remove backward.privateInPublic t-order easy awaiting-author awaiting author
34920 Parcly-Taxel feat: asymptotic lemmas on the `cobounded` filter t-analysis awaiting-author awaiting author
35640 kebekus feat: Liouville Theorem for harmonic functions t-analysis awaiting-author awaiting author
35503 mariainesdff feat(RingTheory/Valuation): add IsTrivialOn_lemmas t-ring-theory delegated opened from a branch in the main mathlib repo (not a fork)
33188 BryceT233 feat(RingTheory/MvPowerSeries): introduce rename new-contributor t-ring-theory large-import ??? missing CI information
34838 mkaratarakis feat: lemmas for the analytic part of the proof of the Gelfond–Schneider theorem (Part 2/4) t-analysis new-contributor ready-to-merge awaiting bors