Why is my PR not on the queue?

This page was last updated on: November 14, 2025 at 06:51 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
14345 digama0 feat: the Dialectica category is monoidal closed t-category-theory awaiting-author awaiting author
12452 JADekker feat(Cocardinal) : add some more api t-topology awaiting-CI does not pass CI
10099 mcdoll feat: Integration by parts for higher dimensional spaces t-measure-probability t-analysis WIP labelled WIP
10998 hmonroe feat(Logic): Arithmetization of partial recursive functions (toward Gödel's first incompleteness theorem) t-logic awaiting-author awaiting author
9510 eric-wieser feat(Analysis/Calculus/DualNumber): Extending differentiable functions to dual numbers t-algebra t-analysis awaiting-CI WIP labelled WIP
9352 chenyili0818 feat: arithmetic lemmas for `gradient` t-analysis awaiting-author awaiting author
9469 dupuisf feat: maximum modulus principle for functions vanishing at infinity t-analysis awaiting-author awaiting author
6859 MohanadAhmed TryLean4Bundle: Windows Bundle Creator CI WIP help-wanted looking for help
5745 alexjbest feat: a tactic to consume type annotations, and make constructor nicer t-meta awaiting-author awaiting author
15224 AnthonyBordg feat(CategoryTheory/Sites): covering families and their associated Grothendieck topology new-contributor t-category-theory awaiting-author awaiting author
14563 awueth feat: if-then-else of exclusive or statement new-contributor t-algebra awaiting-author awaiting author
10387 adomani feat(Tactic/ComputeDegree): add `polynomial` tactic RFC t-meta WIP labelled WIP
9693 madvorak feat: Linear programming in the standard form t-algebra RFC WIP labelled WIP
7386 madvorak feat: Define linear programs t-algebra RFC WIP labelled WIP
7219 Ruben-VandeVelde feat: Equivs for AddMonoidAlgebras t-algebra awaiting-author failing CI
13163 erdOne feat(.vscode/module-docstring.code-snippet): Prevent auto-complete from firing on `do` t-meta awaiting-author awaiting author
10026 madvorak Linear programming according to Antoine Chambert-Loir's book t-algebra RFC WIP labelled WIP
10159 madvorak Linear programming according to Antoine Chambert-Loir's book — affine version t-algebra RFC WIP labelled WIP
11890 adomani feat: the terminal refine linter t-linter awaiting-author awaiting author
11090 pangelinos feat: define spectral spaces and prove that a quasi-compact open of a spectral space is spectral new-contributor t-topology please-adopt good first issue looking for help
9795 sinhp feat: the type `Fib` of fibre of a function at a point t-category-theory awaiting-author awaiting author
15055 sinhp feat: the category of pointed objects of a concrete category t-category-theory awaiting-author awaiting author
16253 Shreyas4991 feat: Basics of Discrete Fair Division in Mathlib awaiting-author WIP ⚠️ labelled WIP
15121 Eloitor feat: iff theorems for IsSplitEpi and IsSplitMono in opposite category new-contributor t-category-theory awaiting-author failing CI
15895 madvorak feat(Computability/ContextFreeGrammar): mapping between two types of nonterminal symbols t-computability WIP labelled WIP
16570 yuma-mizuno chore(Tactic/CategoryTheory): change `TermElabM` to `MetaM` t-meta WIP labelled WIP
10591 adri326 feat(Topology/Algebra/ConstMulAction): properties of continuous actions in Hausdorff spaces t-algebra t-topology awaiting-author awaiting author
10796 mcdoll feat(Tactic/Positivity): non-negativity of functions t-meta WIP labelled WIP
14603 awueth feat: degree is invariant under graph isomorphism new-contributor t-combinatorics WIP labelled WIP
19329 adomani perf(CI): automatically benchmark PRs when they are opened CI WIP labelled WIP
20459 Ruben-VandeVelde chore: fix names of roots_C_mul_X_{add,sub}_C_of_IsUnit t-algebra awaiting-author awaiting author
10977 grunweg feat: germs of smooth functions t-analysis t-topology t-differential-geometry awaiting-author failing CI
19378 adamtopaz feat: Explanation widgets t-meta awaiting-author awaiting author
19323 madvorak feat: Function to Sum decomposition t-data WIP labelled WIP
18461 hannahfechtner feat: left and right common multiples mixins new-contributor t-algebra awaiting-author awaiting author
20797 vbeffara feat(Topology/Covering): CM version of eq_of_comp_eq new-contributor t-topology easy awaiting-author awaiting author
20466 MohanadAhmed feat: Sherman Morrison formula for rank 1 update of the matrix inverse t-data awaiting-author awaiting author
18749 GabinKolly feat(ModelTheory): preparatory work for the existence of Fraïsse limits t-logic awaiting-author awaiting author
20649 GabinKolly feat(ModelTheory/Graph): prove characterization of the fraisse limit of finite simple graphs large-import t-logic t-combinatorics WIP labelled WIP
10660 eric-wieser feat(LinearAlgebra/CliffordAlgebra): construction from a basis t-algebra awaiting-author WIP labelled WIP
15355 adomani feat: MiM PR report WIP ⚠️ labelled WIP
21495 alreadydone experiment: reducible HasQuotient.quotient' bench-after-CI WIP labelled WIP
21447 erdOne feat(AlgebraicGeometry): the split algebraic torus t-algebraic-geometry awaiting-author awaiting author
13442 dignissimus feat: mabel tactic for multiplicative abelian groups new-contributor t-meta modifies-tactic-syntax awaiting-author help-wanted looking for help
21501 sksgurdldi feat(List): add sum_zipWith_eq_finset_sum new-contributor t-algebra awaiting-author awaiting author
19062 hannahfechtner feat(Algebra/PresentedMonoid/Basic) : facts about rel t-algebra awaiting-author awaiting author
22302 658060 feat: add `CategoryTheory.Topos.Power` new-contributor t-category-theory awaiting-author awaiting author
20636 eric-wieser feat: multiplication of intervals in rings t-algebra awaiting-author awaiting author
22784 grunweg feat: add Diffeomorph.sumSumSumComm t-differential-geometry WIP labelled WIP
22159 shetzl feat: add definition of pushdown automata t-computability new-contributor awaiting-author awaiting author
23042 joneugster feat(CategoryTheory/Enriched/Limits): add HasConicalLimitsOfSize.shrink infinity-cosmos t-category-theory WIP labelled WIP
23142 joneugster feat(CategoryTheory/Enriched/Limits): add API for HasConicalLimit infinity-cosmos t-category-theory awaiting-author awaiting author
23285 AntoineChambert-Loir refactor: directed systems in terms of functors large-import t-algebra t-category-theory WIP labelled WIP
21829 Whysoserioushah feat(LinearAlgebra/TensorProduct/HomTensor): Add TensorProduct of Hom-modules t-algebra awaiting-author awaiting author
22861 eric-wieser feat: add the trace of a bilinear form t-algebra awaiting-author awaiting author
22888 plp127 perf: replace `Lean.Expr.swapBVars` with a better? implementation t-meta awaiting-author awaiting author
23772 SEU-Prime Create Amice.lean t-number-theory WIP ??? labelled WIP
21903 yhtq feat: add from/toList between `FreeSemigroup` and `List` with relative theorems large-import new-contributor t-algebra awaiting-CI does not pass CI
24000 YaelDillies feat: correspondence between Hopf algebras and affine group schemes toric FLT t-algebraic-geometry WIP labelled WIP
21270 GabinKolly feat(ModelTheory/Bundled): first-order embeddings and equivalences from equalities large-import t-logic awaiting-author awaiting author
13038 adomani feat: Mathlib weekly reports CI t-meta awaiting-author awaiting author
19613 madvorak refactor(Combinatorics/Optimization/ValuedCSP): make only valid `FractionalOperation` possible t-combinatorics failing CI
24219 Paul-Lez feat: linear independence of the tensor product of two linearly independent families toric t-algebra WIP labelled WIP
20652 jjaassoonn feat: categorical description of center of a ring t-algebra t-category-theory awaiting-author failing CI
21616 peabrainiac feat(Topology): concatenating countably many paths t-topology awaiting-author awaiting author
23585 plp127 feat: `Filter.atMax` and `Filter.atMin` t-order WIP labelled WIP
18861 YaelDillies refactor: make `Set.mem_graphOn` defeq t-data awaiting-author failing CI
23503 apnelson1 feat(Topology/Instances/ENat): ENat and tsum large-import t-topology WIP labelled WIP
22809 b-reinke feat: Category algebras and path algebras new-contributor t-algebra t-category-theory WIP labelled WIP
22488 smmercuri fix: lower priority for `UniformSpace.Completion.instSMul` FLT t-topology awaiting-author awaiting author
15649 TpmKranz feat(Computability): introduce Generalised NFA as bridge to Regular Expression awaiting-zulip t-computability new-contributor awaiting-author awaiting a zulip discussion
20648 anthonyde feat: formalize regular expression -> εNFA awaiting-zulip t-computability new-contributor awaiting a zulip discussion
23220 mattrobball refactor(Module.LinearMap.Defs): make `SemilinearMapClass` extend `AddMonoidHomClass` t-algebra awaiting-author awaiting author
24665 Komyyy feat(Mathlib/Topology/Metrizable/Uniformity): every uniform space is generated by a family of pseudometrics t-topology WIP labelled WIP
23213 mattrobball chore(RingTheory.Derivation): add a `LinearMapClass` instance t-algebra delegated delegated
23214 mattrobball perf(Module.LinearMap.Defs): deprioritize projections to parents for `SemilinearMapClass` t-algebra delegated delegated
24155 eric-wieser feat: add a "rw_proc" for fin vectors t-data RFC t-meta awaiting-author awaiting author
22314 shetzl feat: add leftmost derivations for context-free grammars t-computability new-contributor awaiting-author awaiting author
21276 GabinKolly feat(ModelTheory/Substructures): define equivalences between equal substructures t-logic awaiting-author awaiting author
24008 meithecatte chore(EpsilonNFA): replace manual lemmas with @[simps] t-computability new-contributor awaiting-author awaiting author
24618 b-mehta feat(Analysis): add Schur inequality and variants t-analysis WIP labelled WIP
24957 eric-wieser feat: use ` binderNameHint` in sum_congr t-algebra failing CI
5919 MithicSpirit feat: implement orthogonality for AffineSubspace new-contributor t-analysis WIP help-wanted looking for help
21624 sinhp feat(CategoryTheory): The (closed) monoidal structure on the product category of families of (closed) monoidal categories t-category-theory awaiting-author failing CI
11155 smorel394 feat(LinearAlgebra/Multilinear/DirectSum, LinearAlgebra/DirectSum/{PiTensorProduct,Finsupp}): interaction between `MultilinearMap` and `DirectSum`, and between `PiTensorProduct` and `DirectSum` t-algebra please-adopt looking for help
19456 AntoineChambert-Loir feat(Data/Finsupp/MonomialOrder/DegRevLex): homogeneous reverse lexicographic order t-data t-order t-algebraic-geometry WIP labelled WIP
24690 ScottCarnahan feat (Data.Prod): Reverse lexicographic order t-order WIP labelled WIP
24065 kim-em chore: script to give topological sort of modules awaiting-author awaiting author
20238 maemre feat(Computability/DFA): Closure of regular languages under some set operations awaiting-zulip t-computability new-contributor awaiting-author awaiting a zulip discussion
25473 adomani feat(CI): check that Mathlib files have lean or md extension CI delegated delegated
24441 MrSumato feat(Data/List): add Lyndon-Schutzenberger theorem on list commutativity t-data new-contributor awaiting-author awaiting author
23929 meithecatte feat(Computability/NFA): improve bound on pumping lemma awaiting-zulip t-computability new-contributor awaiting a zulip discussion
25035 ScottCarnahan feat (Algebra/Module/Equiv/Defs): Linear equivalence between linear hom and semilinear hom. t-algebra WIP labelled WIP
25034 ScottCarnahan feat (Algebra/Module/Equiv/Basic): Restriction of scalars from a semilinear equivalence to a linear equivalence. t-algebra WIP labelled WIP
24540 robertmaxton42 feat(Quiv): add the empty, vertex, point, interval, and walking quivers t-category-theory awaiting-author failing CI
22790 mhk119 feat: Extend `taylor_mean_remainder_lagrange` to `x < x_0` new-contributor t-analysis awaiting-author awaiting author
21344 kbuzzard chore: attempt to avoid diamond in OreLocalization t-algebra please-adopt looking for help
25585 Paul-Lez feat(Tactic/Linters/DeprecatedSimpLemma): lint for deprecated simp lemmas t-linter awaiting-author failing CI
25802 dagurtomas feat(AlgebraicTopology): anodyne morphisms of simplicial sets t-topology WIP labelled WIP
25835 erdOne WIP: Weierstrass elliptic functions t-analysis WIP labelled WIP
25765 JovanGerb feat(gcongr): lemma for rewriting inside divisibility t-data delegated delegated
25921 BoltonBailey feat: scripts to analyze overlap between namespaces migrated-from-branch t-meta WIP labelled WIP
26239 BoltonBailey feat: add sample pre-commit git hook file WIP ⚠️ labelled WIP
26293 RemyDegenne feat: tightness from convergence of characteristic functions t-measure-probability WIP labelled WIP
20924 tomaz1502 feat(Computability/QueryComplexity): Oracle-based computation t-computability failing CI
26087 grunweg feat: a `SliceModel` typeclass for models with corners for embedded submanifolds t-differential-geometry failing CI
26389 jjdishere feat(RingTheory): Perfectoid Field t-algebra t-analysis t-topology WIP labelled WIP
26432 AntoineChambert-Loir feat(Data.Nat.LogFueled): fueled version of `clog` t-data failing CI
25739 literandltx feat(NumberTheory/LegendreSymbol): Add sqrt‐of‐residue theorems for p=4k+3 and p=8k+5 new-contributor t-number-theory awaiting-author awaiting author
25993 Multramate feat(Algebra/Group/Units/Hom): add map lemmas t-algebra awaiting-author awaiting author
26013 tsuki8 feat(Data/Finset/Card,Data/Set/Finite/Basic) t-data new-contributor awaiting-author awaiting author
26283 kckennylau (WIP) Resultant t-algebra WIP labelled WIP
26743 grunweg WIP: product rule for Lie bracket on manifolds t-differential-geometry WIP labelled WIP
16303 grunweg feat(CI): check for badly formatted titles or missing/contradictory labels CI awaiting-author failing CI
20784 eric-wieser fix: prevent `exact?` recursing forever on `n = 55` t-set-theory failing CI
26990 joelriou feat(CategoryTheory/Abelian): Noetherian objects form a Serre class t-category-theory WIP labelled WIP
26994 Paul-Lez feat(Topology/MetricSpace/Pseudo/Defs): add easy lemma about opens in topological spaces t-topology easy awaiting-author awaiting author
27069 FrankieNC feat(Analysis/MetricSpace/HausdorffDimension): prove dimH of intervals and segments is 1 new-contributor t-topology awaiting-author awaiting author
18230 digama0 feat(Tactic/ScopedNS): extend `scoped[NS]` to more commands t-meta awaiting-author awaiting author
27187 Komyyy feat: `NONote` represents ordinals < ε₀ t-set-theory WIP labelled WIP
12006 adomani feat: the `suffa` tactic t-meta awaiting-author ??? missing CI information
27435 callesonne feat(Normed/Algebra/Logarithm): add FormalMultilinearSeries of logarithm around `1` t-analysis WIP labelled WIP
21915 YaelDillies feat: simproc for `Int.divisorsAntidiag` t-meta WIP labelled WIP
27507 grunweg wip(commandStart): check the indentation of declaration keywords also t-linter WIP labelled WIP
26594 metakunt feat(Algebra/Polynomial/ZMod): Add Polynomial.equiv_of_nat_of_polynomial_zmod new-contributor t-algebra awaiting-author awaiting author
22464 adomani feat(CI): declarations diff in Lean CI awaiting-author awaiting author
27297 hugh-fox feat: add an equality between sums and products of cartesian products new-contributor t-algebra awaiting-author awaiting author
27704 vihdzp feat: link `Minimal` and `IsLeast` together t-order awaiting-author failing CI
14237 js2357 feat: Define the localization of a fractional ideal at a prime ideal new-contributor t-algebra awaiting-author failing CI
27756 grunweg feat: `Weak(Pseudo)EMetricSpace`, generalises `(Pseudo)EMetricSpace` carleson t-topology WIP labelled WIP
25989 Multramate feat(NumberTheory/EllipticDivisibilitySequence): add elliptic nets t-number-theory awaiting-author awaiting author
27813 javra feat: IMO 2025 Q1 IMO WIP labelled WIP
27753 YunkaiZhang233 feat(CategoryTheory): implemented proofs for factorisation categories being equivalent to iterated comma categories in two ways new-contributor t-category-theory awaiting-author awaiting author
27826 xgenereux feat(Subsemiring): mk_eq_zero t-algebra WIP labelled WIP
27050 BoltonBailey doc(Control/Monad/Cont): add docstrings t-data awaiting-author failing CI
25916 BoltonBailey feat: add `simp` lemma `coeff_eq_zero_of_not_mem_support` t-algebra awaiting-author failing CI
27225 eric-wieser refactor(Tactic/Lift): deprecate the third with argument t-meta awaiting-author awaiting author
26341 mans0954 feat(LinearAlgebra/QuadraticForm/Basis): Free Tensor product of Quadratic Maps large-import t-algebra WIP labelled WIP
26340 mans0954 feat(Algebra/Module/NestAlgebra): Nest algebras t-algebra failing CI
26158 upobir feat(NumberTheory/Divisors): add int divisors t-number-theory awaiting-author awaiting author
26483 metakunt feat (RingTheory/RootsOfUnity/PrimitiveRoots) : Add equiv_primitiveRoots_of_coprimePow t-ring-theory new-contributor awaiting-author awaiting author
26368 Whysoserioushah feat(RingTheory/TwoSidedIdeal/SpanAsSum): span of set as finsum t-ring-theory awaiting-author awaiting author
14733 jjaassoonn feat(RingTheory/Flat/CategoryTheory): a module is flat iff tensoring preserves finite limits t-ring-theory awaiting-author awaiting author
14727 jjaassoonn feat(RingTheory/Flat/CategoryTheory): a flat module has vanishing higher Tor groups t-ring-theory awaiting-author awaiting author
27309 kckennylau feat(CategoryTheory): a presheaf on `CostructuredArrow F d` can be extended to a presheaf on `C` t-category-theory WIP labelled WIP
27417 PierreQuinton feat: add `SigmaCompleteLattice` t-order awaiting-author awaiting author
26765 KiringYJ feat(MeasureTheory/PiSystem): add π-λ theorem and SetLike instance new-contributor t-measure-probability awaiting review
27534 PierreQuinton feat: a typeclass for `sSup`/`sInf` to be lawful t-order awaiting review
28075 tristan-f-r chore(Finsupp/Indicator): make non-classical t-data easy awaiting-author awaiting author
23758 erdOne feat(Topology/Algebra): linearly topologized iff non-archimedean large-import t-algebra t-topology awaiting-author awaiting author
27850 fyqing feat: 0-dimensional manifolds are discrete and countable new-contributor t-differential-geometry awaiting-author awaiting author
27444 grunweg feat: generalise more lemmas to enorms carleson WIP ⚠️ labelled WIP
24850 pechersky feat(Topology/UniformSpace/Ultra): uniform spaces induced by pseudometrics are ultra if system is ultra t-topology awaiting review
27226 xcloudyunx feat(Combinatorics/SimpleGraph): Add Subgraph.inclusion_edge_apply_coe and inclusion_edgeSet_apply_coe new-contributor t-combinatorics awaiting-author awaiting author
22925 ggranberry feat(Mathlib/PlaceHolder/ToeplitzHausdorff): Toeplitz-Hausdorff will-close-soon new-contributor t-analysis awaiting-author WIP help-wanted looking for help
26125 faenuccio first commit dependency-bump WIP labelled WIP
26349 mans0954 feat(Analysis/SpecialFunctions/Trigonometric/Basic): sin and cos of multiples of π / 3 t-analysis help-wanted looking for help
5897 eric-wieser feat: add a `MonadError` instance for `ContT` t-meta awaiting-author awaiting author
23881 YaelDillies feat: `ℝ≥0`-valued Lᵖ norm t-measure-probability awaiting-author awaiting author
28072 kckennylau feat(RingTheory/Valuation): make tactic rw_val_equiv t-ring-theory awaiting review
28631 faenuccio feat(Data\Nat\ModEq.lean): add grind attribute to ModEq t-data WIP labelled WIP
26329 Timeroot feat: Definition of `Clone` notations and typeclasses t-algebra awaiting-CI awaiting-author does not pass CI
27752 plp127 feat(Order): `NoBotOrder α` implies `NoMinOrder α` under `IsDirected α (· ≥ ·)` t-order awaiting-author failing CI
28125 nonisomorphiclinearmap feat(Combinatorics): basic definition of simplicial complexes new-contributor t-combinatorics awaiting review
28186 Sebi-Kumar feat(Topology/Homotopy/Path): Add IsEquiv instance for Path.Homotopic new-contributor t-topology awaiting review
24514 b-mehta chore(Int/GCD): use fuel in xgcd t-data awaiting-author awaiting author
26645 erdOne feat(RingTheory/PowerSeries): Construction of `Q` such that `P(Q(X)) = X` t-ring-theory awaiting-author awaiting author
28680 vihdzp feat: set has cardinality one iff singleton t-set-theory easy awaiting-author awaiting author
26078 kckennylau feat(AlgebraicGeometry): add x, y, px, py for points on elliptic curves t-algebraic-geometry awaiting-author awaiting author
27479 iu-isgood feat: Abel's Binomial Theorem t-data new-contributor awaiting-author failing CI
25700 grunweg feat: lint upon uses of the `mono` tactic t-linter RFC please-adopt looking for help
28325 pechersky feat(WithZeroTopology): `locallyCompactSpace_iff_locallyFiniteOrder_units` large-import t-order t-topology awaiting review
24333 xcloudyunx feat(Combinatorics/SimpleGraph): cycle graph implementation for generic vertex types new-contributor t-combinatorics awaiting-author awaiting author
27155 Pjotr5 feat: Shearer's bound on the independence number of triangle free graphs new-contributor t-combinatorics awaiting-author failing CI
24719 madvorak feat(LinearAlgebra/Matrix/NonsingularInverse): inverting `Matrix` inverts its `LinearEquiv` t-algebra awaiting-author awaiting author
27242 hugh-fox feat: add Gauss-like formula for sums of digit sums large-import t-data new-contributor awaiting-author awaiting author
27261 Sebi-Kumar feat(Topology): add definition for subpaths new-contributor t-topology awaiting-author awaiting author
26644 kckennylau feat(SetTheory/ZFC): Define the language of sets and state the ZFC axioms t-set-theory awaiting-author awaiting author
26914 quangvdao feat(Data/PFunctor/Univariate): more definitions for univariate `PFunctor` t-data awaiting review
26648 eric-wieser chore(TensorProduct): remove more `suppress_compilation`s t-algebra blocked-by-core-PR blocked on another PR
23238 YaelDillies feat: extended floor and ceil t-algebra awaiting review
28056 grunweg wip: existence of Riemannian metrics t-differential-geometry WIP labelled WIP
24373 YaelDillies refactor: golf `modularCharacter` t-measure-probability awaiting-CI does not pass CI
24383 YaelDillies feat: distributive Haar characters of `ℝ` and `ℂ` file-removed FLT t-measure-probability awaiting-CI WIP labelled WIP
25500 eric-wieser feat: delaborators for metadata large-import t-meta delegated awaiting-author awaiting author
28316 eric-wieser feat(Tactic/NormNum): better trace nodes t-meta failing CI
26240 grunweg perf(CommandLinterLinter): use Substring more t-linter RFC awaiting review
26299 adomani perf: the `commandStart` linter only acts on modified files t-linter awaiting-author awaiting author
26455 ScottCarnahan WIP - feat (LinearAlgebra/RootSystem): API for CartanMatrix t-algebra WIP labelled WIP
26156 oliver-butterley feat(MeasureTheory.VectorMeasure) : add a definition of total variation for VectorMeasure new-contributor t-measure-probability awaiting-author failing CI
25920 BoltonBailey feat(Data/Finsupp/Basic): `Finsupp.optionElim'` migrated-from-branch t-data awaiting review
22231 pechersky feat(Algebra/Valued): `AdicExpansion` initial defns t-algebra t-topology awaiting-author awaiting author
29232 vihdzp feat: more theorems on `SuccAddOrder` t-order t-algebra failing CI
26935 Paul-Lez feat(Analysis/SpecialFunction/NthRoot): definition and basic API of Real.nthRoot t-analysis failing CI
26310 kckennylau Binary form t-algebra awaiting-author awaiting author
27321 kckennylau feat(CategoryTheory): Colimit can be computed fiberwise t-category-theory awaiting-CI does not pass CI
29108 JonBannon feat(MeasureTheory): add `LInfty.lean` with `Mul` and `const` related results. t-measure-probability awaiting-author awaiting author
22954 eric-wieser feat(RingTheory/Congruence/Hom): copy from GroupTheory t-ring-theory failing CI
27995 kckennylau feat(RingTheory/Valuation): alternate constructors for Valuation t-ring-theory awaiting-CI does not pass CI
28613 espottesmith feat(Combinatorics): define undirected hypergraphs new-contributor t-combinatorics awaiting review
26159 upobir feat(Algebra/QuadraticDiscriminant): Adding inequalities on quadratic from inequalities on discriminant t-algebra awaiting-author awaiting author
29212 Whysoserioushah feat(Algebra/CrossProductAlgebra/Defs) : Define Cross Product Algebra t-algebra awaiting-author awaiting author
28511 YaelDillies feat(Finsupp): `congr!`-compatible version of `prod_congr` t-algebra awaiting review
27701 vihdzp feat: `a < b + c ↔ a < b ∨ ∃ d < c, a = b + d` t-algebra awaiting-author awaiting author
26881 emo916math feat(Analysis/Calculus/Deriv/Star) A formula for `deriv (conj ∘ f ∘ conj)` new-contributor t-analysis awaiting-author awaiting author
24533 robertmaxton42 feat (ULift): conjugation by ULift.up/down, misc cast/heq lemmas t-data awaiting-author awaiting author
26462 PSchwahn feat(LinearAlgebra/Projection): add results about inverse of `Submodule.prodEquivOfIsCompl` new-contributor t-algebra awaiting-author awaiting author
29434 ntapiam feat(NonAssoc/LieAdmissible): prove every ring/algebra is LieAdmissible new-contributor t-algebra failing CI
28286 bwangpj feat(Geometry/Manifold/ContMDiff): basic lemmas for analytic (`C^ω`) functions new-contributor t-differential-geometry awaiting-author awaiting author
26614 Rida-Hamadani feat(SimpleGraph): add more API for `take`/`drop` t-combinatorics awaiting-author failing CI
28124 kckennylau feat(Tactic): Call an arbitrary Simproc t-meta failing CI
29527 kim-em feat: script for checking Github URLs CI WIP labelled WIP
27098 Paul-Lez feat(Algebra/Category/ModuleCat/Sheaf/VectorBundle): define vector bundles t-algebra awaiting-author awaiting author
25778 thefundamentaltheor3m feat: Monotonicity of `setIntegral` for nonnegative functions new-contributor t-measure-probability awaiting-author awaiting author
26920 yuma-mizuno feat(Tactic.CategoryTheory): add associator inserting tactic t-category-theory t-meta WIP labelled WIP
29615 eric-wieser chore: add a computable shortcut for `AddCommMonoid ℂ` bench-after-CI t-analysis easy failing CI
24184 YaelDillies feat: `[G : H]` notation for the index of `H : Subgroup G` t-algebra RFC awaiting review
22043 YaelDillies chore: shortcut instance for `Neg ℤˣ` file-removed t-algebra awaiting review
26110 YaelDillies feat: sharp monoids toric t-algebra awaiting review
29675 yury-harmonic feat(Wolstenholme): new file t-data awaiting-author help-wanted looking for help
29720 javra feat(CategoryTheory): `TransportEnrichment` and `ForgetEnrichment` as 2-functors t-category-theory WIP labelled WIP
29010 grunweg chore: more tests for field_simp features and edge cases failing CI
27937 madvorak feat(Logic/Basic): `congr_heq₂` t-logic awaiting-author awaiting author
27702 FLDutchmann feat(NumberTheory/SelbergSieve): define Lambda-squared sieves and prove important properties t-number-theory awaiting-author awaiting author
29530 ShreckYe feat(Dynamics/PeriodicPts): some theorems for `Pi.map` in `Dynamics/PeriodicPts` analogous to those for `Prod.map` large-import ⚠️ awaiting review
25899 pfaffelh feat(Topology/Compactness/CompactSystem): introduce compact Systems t-topology awaiting-author awaiting author
25902 pfaffelh feat: The finite product of semi-rings (in terms of measure theory) is a semi-ring. large-import t-measure-probability awaiting-author awaiting author
26051 Komyyy feat(Mathlib/GroupTheory/SpecificGroups/Alternating): A_n is simple iff n = 3 or 5 ≤ n t-group-theory large-import WIP labelled WIP
27500 Komyyy feat: the Riemann zeta function is meromorphic large-import t-analysis WIP labelled WIP
28057 plp127 feat(SuccOrder): simp lemma to refold `Order.succ` and `Order.pred` t-order awaiting-author awaiting author
29400 ShreckYe feat(`Algebra/BigOperators`): products of the results of insertion and removal on tuples and lists, and some needed lemmas large-import ⚠️ awaiting review
29235 yoh-tanimoto feat(Topology/Algebra/Module/ClosedSubmodule): add `mapEquiv`, a variation of `ClosedSubmodule.map` for CLE t-topology awaiting review
29500 vihdzp feat: `WellFoundedLT (LowerSet α)` t-order awaiting-author awaiting author
29870 mckoen feat(CategoryTheory/Adhesive): subobjects in adhesive categories have binary coproducts t-category-theory WIP labelled WIP
29688 tb65536 feat(FieldTheory/IsGaloisGroup): prove the Galois correspondence for `IsGaloisGroup` t-algebra awaiting review
27215 kckennylau feat(AlgebraicGeometry): Define the Zariski site on `CommRingCatᵒᵖ` t-algebraic-geometry awaiting-author awaiting author
28175 dsfxcimk feat: exterior angle theorem new-contributor t-euclidean-geometry awaiting-author awaiting author
29624 mcdoll feat(LinearAlgebra/LinearPMap): add definition of resolvent and first resolvent identity t-algebra awaiting review
29588 Periecle feat(Analysis/Complex/Residue): Implement residue theory for complex functions at isolated singularities new-contributor t-analysis awaiting-author failing CI
28871 JaafarTanoukhi feat(Combinatorics/Digraph): Tournaments new-contributor t-combinatorics awaiting review
25905 mans0954 feat(RingTheory/Polynomial/SmallDegreeVieta): polynomial versions of results in Algebra.QuadraticDiscriminant t-ring-theory awaiting-author awaiting author
29596 alreadydone chore(Algebra): extract `Submonoid.IsLocalizationMap` t-algebra awaiting review
29965 RemyDegenne feat(probability): define subtraction of kernels t-measure-probability WIP labelled WIP
29933 smmercuri chore: fix `def` naming isses in `Normed/Field/WithAbs.lean` WIP labelled WIP
29622 uniwuni feat(RepresentationTheory/Commutative): simple representations of commutative monoids are 1-dimensional t-algebra awaiting-author awaiting author
24050 Paul-Lez feat(Data/Finsupp/Pointwise): generalise pointwise scalar multiplication of finsupps t-data awaiting-author awaiting author
25324 eric-wieser feat: more functorial results about DFinsupp t-data t-algebra awaiting-author awaiting author
26330 Timeroot feat: "Junk value" test file t-data awaiting-author awaiting author
28452 plp127 feat: Define `ZMod.fintype` without cases t-data awaiting-author awaiting author
25974 scholzhannah feat(Topology/Compactness/CompactlyCoherentSpace): compact coherentification (k-ification) large-import t-topology awaiting review
24789 Ruben-VandeVelde chore: move Algebra.Group.Hom.End to Algebra.Ring file-removed t-algebra awaiting-author awaiting author
26287 mbkybky feat(Data/ENat/Lattice): coercion to `WithBot ℕ∞` commutes with `biSup` t-data awaiting review
26923 oliver-butterley feat(Dynamics/BirkhoffSum): add the pointwise ergodic theorem (Birkhoff's) new-contributor t-dynamics awaiting review
30142 shalliso feat(Topology/Baire): define IsNonMeagre new-contributor t-topology failing CI
30079 dagurtomas feat(CategoryTheory): IsSheafFor as a multiequalizer condition t-category-theory WIP labelled WIP
27262 Timeroot feat(Tactic/Bound): bound? for proof scripts t-meta awaiting-author awaiting author
29734 bwangpj feat(Probability/Kernel): \phi-irreducibility of kernels t-measure-probability awaiting review
29376 vlad902 feat(SimpleGraph): helper lemmas for `Walk.IsSubwalk` t-combinatorics awaiting review
19860 YaelDillies refactor: review the `simps` projections of `OneHom`, `MulHom`, `MonoidHom` t-algebra WIP labelled WIP
25814 vlad902 feat(SimpleGraph): weaker condition for paths in acyclic graphs t-combinatorics awaiting review
28630 Antidite feat(Archive/Imo): right isosceles configuration in the complex plane IMO new-contributor awaiting-author awaiting author
25760 robin-carlier feat(CategoryTheory/Bicategory): (2,1)-categories and `Pith` t-category-theory awaiting-author failing CI
26347 mans0954 feat(Data/Finset/RangeDistance): abs_sub_lt_of_mem_finset_range t-data awaiting review
26885 pechersky feat(Topology/ValuativeRel): ValuativeTopology 𝒪[K] t-algebra t-topology t-number-theory awaiting review
27073 pechersky feat(Archive/Examples/Local): files showcasing properties of local fields t-number-theory awaiting-author awaiting author
30135 erdOne feat(RingTheory): `ValuativeRel` on subrings t-ring-theory awaiting-author awaiting author
26985 agjftucker feat(Analysis/Calculus/Implicit): define implicitFunOfProdDomain new-contributor t-analysis awaiting review
28191 kckennylau feat(Logic): tag Injective, Surjective, and Bijective with fun_prop t-meta awaiting-author awaiting author
29827 js2357 feat: define two (trivial) ContinuousMulEquivs large-import FLT t-topology failing CI
29361 FlAmmmmING feat: Catalan generating function as a formal power series t-ring-theory new-contributor awaiting review
26292 RemyDegenne feat(MeasureTheory): tightness of the range of a sequence t-measure-probability awaiting-author failing CI
30107 grunweg chore: track occurrences of 'nonrec' as technical debt tech debt CI awaiting review
30116 FormulaRabbit81 feat(Measure): proof that a relatively compact set of measures is tight large-import t-measure-probability awaiting review
26983 mans0954 feat(Order/LatticeElements): distributive, standard and neutral elements of a lattice t-order WIP labelled WIP
30355 kckennylau feat(Logic): graded functions t-data awaiting review
29744 espottesmith feat(Combinatorics): define directed hypergraphs new-contributor t-combinatorics awaiting review
29347 themathqueen refactor(Algebra/Star/StarAlgHom): let `StarAlgEquiv` extend `StarRingEquiv` instead of `RingEquiv` t-algebra awaiting review
29947 JaafarTanoukhi feat(Combinatorics/Digraph): Maps new-contributor t-combinatorics awaiting review
26284 plp127 feat: faster implementation of `Nat.primeFactorsList` + `@[csimp]` lemma t-data awaiting-author awaiting author
29798 Cyantain feat(FieldTheory/IsIntegrallyClosed): lemma to judge whether an element is integral new-contributor t-algebra delegated awaiting-author awaiting author
27254 yuanyi-350 2025 imo problem3 IMO awaiting review
26961 mariainesdff feat(RingTheory/PowerSeries/Substitution): add API t-ring-theory awaiting review
28970 Whysoserioushah feat(Algebra/Algebra/ReducedNorm) : Defines reduced norm and trace t-algebra awaiting-author awaiting author
30333 paulorauber feat(Probability): definition of trajMeasure new-contributor t-measure-probability awaiting-author awaiting author
27422 vihdzp feat: relate images to pointwise negation/inverses t-data t-algebra awaiting-author awaiting author
30233 Komyyy refactor(Topology/Sequences): generalize seq-compactness lemmas to metrizable space large-import t-topology awaiting review
27302 tristan-f-r feat(Fintype/Quotient): finLiftOn₂ t-data awaiting-author awaiting author
30119 Ruben-VandeVelde feat: WithTop/Bot.mapD t-order awaiting-author awaiting author
29432 lecopivo feat: `data_synth` tactic to prove `HasFDerivAt 𝕜 f ?f' x` and similar t-meta WIP labelled WIP
29855 eric-wieser chore(Data/Finset/Sort): lemmas about `0 : Fin _` and `Fin.last _` t-data t-order easy delegated failing CI
30003 vlad902 feat(Order): helper lemmas for `IsChain`/`IsAntichain` t-order awaiting review
28604 alreadydone chore(Algebra/Ring/Defs): add two classes (minimally invasive version) t-algebra awaiting review
29634 YaelDillies feat: missing instance `NonUnitalCommSemiring R → NonUnitalNonAssocCommSemiring R` t-algebra awaiting-CI help-wanted looking for help
30037 linesthatinterlace feat: Fin.find update ⚠️ awaiting review
28141 YaelDillies chore: deprecate `BialgHom.coe_toLinearMap` t-ring-theory toric awaiting review
29980 mans0954 refactor(RingTheory/Polynomial/Resultant/Quadratic): Re-implement QuadraticDiscriminant for R[X] awaiting review
22771 alreadydone feat(Homotopy/Lifting): monodromy of covering maps and lifting criterion t-algebraic-topology blocked on another PR
29315 kbuzzard chore: raise priority of `IsTopologicalSemiring.toIsModuleTopology` t-topology awaiting-author failing CI
29409 Julian feat(Mathlib/Analysis): deriv_eq_self and deriv_exp_iff t-analysis awaiting-author awaiting author
30432 kckennylau feat(AlgebraicGeometry): define the non-vanishing locus of a set in Proj t-algebraic-geometry awaiting review
29706 kim-em feat: add piCongrSigmaFiber and piCongrFiberwise equivalences FLT t-logic awaiting review
29969 smmercuri refactor: use isometry extensions for completions at infinite places of number fields awaiting review
30460 janithamalith feat(Nat): add lemma nat_card_orbit_mul_card_stabilizer_eq_card_group t-group-theory new-contributor awaiting-author awaiting author
29362 stepanholub feat:(Data/List) add the notion of period of List and prove the Periodicity Lemma t-data new-contributor awaiting review
30344 Deep0Thinking feat(MeasureTheory/Integral): add versions of `exists_eq_interval_average` and first mean value theorem for integrals new-contributor t-measure-probability awaiting review
27703 vihdzp feat: `le_of_forall_ne` et. al t-order awaiting-author awaiting author
25737 robin-carlier feat(AlgebraicTopology/SimplexCategory/GeneratorsRelations/NormalForms): Normal forms for `P_δ`s t-algebraic-topology t-category-theory delegated failing CI
26757 fweth feat(CategoryTheory/Topos): define elementary topos new-contributor t-category-theory awaiting-author failing CI
30209 Ruben-VandeVelde feat: some TwoSidedIdeal.span lemmas t-ring-theory FLT awaiting-author awaiting author
25225 xcloudyunx feat(Combinatorics/SimpleGraph): Eulerian walk in connected graph contains all vertices new-contributor t-combinatorics awaiting-author awaiting author
27307 xyzw12345 feat(RingTheory/GradedAlgebra): homogeneous relation t-ring-theory awaiting review
30750 SnirBroshi feat(Data/Quot): `toSet` and `equivClassOf` t-data awaiting review
30746 jeremypparker feat(Data/EReal): toReal_pos t-data new-contributor easy failing CI
27817 zhuyizheng feat: add IMO2025P1 IMO new-contributor awaiting-author awaiting author
27206 grhkm21 feat(CategoryTheory/Adjunction): partial adjoints are adjoints t-category-theory awaiting-author failing CI
27196 YaelDillies refactor(Polynomial/Bivariate): swap `X` and `Y` for improved notation toric t-algebra WIP labelled WIP
30526 SnirBroshi chore(Logic/Relation): use `Subrelation` to state theorems awaiting-zulip awaiting a zulip discussion
30259 erdOne feat(Valuation): uniformizer of discrete valuation t-ring-theory awaiting review
30336 kckennylau feat(RingTheory): some lemmas about the irrelevant ideal t-ring-theory awaiting review
30582 RemyDegenne feat: extension of a function to the closure of a submodule t-topology awaiting review
23835 chrisflav feat(Topology): cardinality of connected components is bounded by cardinality of fiber t-topology awaiting-author failing CI
30547 mariainesdff feat(Algebra/Polynomial/AlgebraMap): add Polynomial.mapAlgHom lemmas t-algebra awaiting author
26332 Timeroot feat(ModelTheory/Definability): TermDefinable functions t-logic awaiting review
21031 YaelDillies chore: get rid of generic hom coercions WIP labelled WIP
26088 grunweg chore(Linter/DirectoryDependency): move forbidden directories into a JSON file t-linter please-adopt looking for help
26129 LessnessRandomness feat(Geometry/Euclidean/Angle/Unoriented): triangle inequality for angles new-contributor t-euclidean-geometry awaiting review
29995 vihdzp feat: more lemmas on `Concept` t-order awaiting-author failing CI
30821 chriseth fix(Computability/Tape): introduce write-simplification theorem that uses `ListBlank.mk` t-computability new-contributor awaiting review
30824 grunweg wip: another smoothness lemma for local frames t-differential-geometry WIP labelled WIP
30828 DeVilhena-Paulo feat: implementation of `Finmap.merge` t-data new-contributor failing CI
29422 jsm28 fix(Data/Finset/Max): Use `DecidableEq` for `insert` lemmas t-data awaiting review
29437 SnirBroshi feat(Data/Seq): add Seq.subsequence and prove basic theorems about it large-import t-data new-contributor awaiting review
29411 llllvvuu feat(LinearAlgebra/Matrix/Rank): rank factorization awaiting-author ⚠️ awaiting author
29526 llllvvuu feat: `Multiset.map f` identifies `f` up to permutation t-data awaiting review
29982 hrmacbeth feat: new `isolate` tactic large-import t-meta awaiting review
30668 astrainfinita feat: `QuotLike` t-data awaiting-zulip RFC awaiting-author awaiting a zulip discussion
29921 mans0954 refactor(RingTheory/Polynomial/SmallDegreeVieta) : Convert to {p : R[X]} (hp : p.natDegree = 2) t-ring-theory awaiting-author awaiting author
30902 adomani chore: longLine warnings happen starting at the 101st character awaiting-zulip t-linter awaiting a zulip discussion
30882 themathqueen feat(Data/Nat/Fib): the Cassini and Catalan identities t-data t-algebra awaiting review
30436 wwylele feat(Topology/InfiniteSum): tprod_one_{add/sub}_ordered t-topology awaiting review
30831 chrisflav feat(AlgebraicGeometry): the fpqc topology t-algebraic-geometry WIP labelled WIP
26986 WangYiran01 feat(Partition): add bijection for partitions with max part ≤ r new-contributor t-combinatorics awaiting-author awaiting author
25603 callesonne feat(Bicategory/InducedBicategory): add induced bicategories t-category-theory awaiting-author awaiting author
30914 eric-wieser feat(Data/Set/NAry): lemmas for `diff` t-data t-order delegated delegated
26464 joelriou feat(LinearAlgebra): generators of pi tensor products file-removed t-algebra awaiting-author awaiting author
28868 yury-harmonic feat(Positive): add `OfNat` instance large-import t-algebra failing CI
29735 vihdzp feat: order instances on quotients t-order failing CI
30121 idontgetoutmuch Principal fiber bundle core new-contributor t-differential-geometry awaiting-author awaiting author
27946 plp127 refactor: have `MetrizableSpace` not depend on `MetricSpace` t-topology awaiting review
30293 vlad902 feat(SimpleGraph): there exists a maximal path/trail in a graph with finite edges t-combinatorics awaiting review
29960 yonggyuchoimath feat(Algebra/Category/Ring): equalizers of pushout maps of tensor product inclusions new-contributor ⚠️ awaiting review
29539 YaelDillies feat: monoid algebras are invariant under base change t-ring-theory toric large-import awaiting review
30892 vihdzp feat: head/last element of flattened list large-import t-data awaiting-author awaiting author
29186 winstonyin feat: IsIntegralCurve for solutions to ODEs t-dynamics t-analysis t-differential-geometry awaiting review
25856 MichaelStollBayreuth perf(Data.Real.Sqrt): make Real.sqrt irreducible migrated-from-branch t-data awaiting review
30378 mans0954 refactor(Order/Hom/Lattice): Use default `initialize_simps_projections` configuration for `LatticeHom`. t-order awaiting-author awaiting author
31008 RemyDegenne refactor: generalize the index of the process in the Doob decomposition t-measure-probability WIP labelled WIP
30667 FrederickPu Subgroup mul new-contributor t-algebra awaiting-author awaiting author
27579 RemyDegenne feat: risk of an estimator, DeGroot statistical information, total variation distance large-import t-measure-probability WIP labelled WIP
30562 dwrensha fix(Data/Fintype/Perm): make the main logic of Equiv.instFintype irreducible t-data awaiting-author awaiting author
31013 vihdzp chore: deprecate `AsLinearOrder` t-order awaiting-author awaiting author
25945 adomani feat: the empty line in commands linter large-import t-linter awaiting review
18236 joelriou feat(Algebra/Category/ModuleCat/Presheaf): the endofunctor of presheaves of modules induced by an oplax natural transformation t-algebra t-category-theory awaiting-CI awaiting-author WIP labelled WIP
30620 plp127 feat: copy LE and LT on preorder and partial order t-order awaiting review
30933 joelriou feat(CategoryTheory): the linearization of a category t-category-theory awaiting-author awaiting author
30069 IvanRenison feat(Combinatorics/SimpleGraph): add lemma `IsTree.dist_ne_of_adj` and necessary lemmas t-combinatorics awaiting review
30004 luigi-massacci feat(MeasureTheory/Integral/TestAgainst): integrating BCFs against a finite measure or an L1Loc map as CLMs t-measure-probability t-analysis awaiting-author awaiting author
25803 erdOne feat: taylor expansion of `1 / z ^ r` t-analysis awaiting-author awaiting author
26398 ChrisHughes24 feat(ModelTheory): definable functions t-logic please-adopt looking for help
30975 mariainesdff feat(Data/Finsupp/Defs): add Finsupp.restrict t-data awaiting-author awaiting author
29946 smmercuri feat(InfinitePlace/Ramification): embeddings of unramified/ramified infinite places satisfy `IsUnmixed/IsMixed` FLT t-number-theory awaiting review
30800 dagurtomas feat(Condensed): cartesian monoidal functor LightProfinite -> LightCondSet large-import ⚠️ awaiting review
30131 fpvandoorn feat: alias_in attribute t-meta awaiting review
26857 Thmoas-Guan feat(Algebra): define associated graded structure for abelian group t-algebra awaiting-author awaiting author
21342 YaelDillies refactor(Normed/Group/Quotient): generalise to non-abelian groups t-analysis WIP labelled WIP
31102 JOSHCLUNE Require LeanHammer new-contributor failing CI
30936 themathqueen feat(Data/Int): define `Int.fib`, the Fibonacci numbers on the integers t-data awaiting review
30758 Timeroot chore: tag abs_inv and abs_div with grind= t-algebra awaiting review
28399 Ruben-VandeVelde feat: ring-theoretic fractions in Rat t-ring-theory awaiting-author awaiting author
26011 linesthatinterlace feat: add elementary lifts for `OneHom`, `MulHom`, `MonoidHom` and `RingHom`. migrated-from-branch t-algebra failing CI
27664 pechersky feat(Topology,Analysis): discrete topology metric space and normed groups t-topology awaiting review
31110 bryangingechen ci: don't delete merged branches CI awaiting-author awaiting author
26588 faenuccio feat(Algebra/GroupWithZero/WithZero): add the multiplicative embedding with zero from the range t-order t-algebra awaiting review
30408 kckennylau feat(RingTheory): more algebra instances for HomogeneousLocalization and linear constructors t-ring-theory failing CI
30525 515801431 Polya_counting new-contributor t-combinatorics awaiting review
30768 tb65536 chore(GroupTheory/Subgroup/Centralizer): replace `centralizer (zpowers s)` with `centralizer {s}` t-group-theory t-algebra awaiting review
30855 Ruben-VandeVelde fix: deprecate IsTotal in favour of Std.Total RFC awaiting review
30867 erdOne feat(RingTheory/Etale): standard etale maps t-ring-theory awaiting review
31119 LLaurance feat(Combinatorics/SimpleGraph/Walk): a vertex of a walk is in its tail starting from the second vertex onwards t-combinatorics awaiting review
30322 kckennylau feat(RingTheory): base change of graded algebra ⚠️ awaiting review
31120 LLaurance feat(Combinatorics/SimpleGraph/Connectivity/Subgraph): toSubgraph and Subgraph.map preserve connectivity t-combinatorics awaiting review
31148 kex-y feat(Probability): Local and stable properties t-measure-probability WIP labelled WIP
30880 themathqueen feat(Analysis/InnerProductSpace): finite-dimensional inner product space with coalgebra implies an algebra structure t-analysis awaiting review
30345 vlad902 feat(Order): replace the implementation of `Set.chainHeight` large-import t-order awaiting review
31178 morrison-daniel feat(LinearAlgebra/Multilinear): basis for multilinear maps large-import new-contributor t-algebra awaiting review
28215 5hv5hvnk Draft PR, for Strong and Weak connectivity for Digraphs new-contributor t-combinatorics awaiting-author failing CI
28198 Sebi-Kumar feat(Analysis/InnerProductSpace/PiL2): Add instances for EuclideanSpace rank and EuclideanSpace being infinite new-contributor t-analysis awaiting-author awaiting author
30363 smmercuri feat: `PadicInt` is isomorphic to the integers of the uniform space completion `(Rat.padicValuation p).Completion` ⚠️ awaiting review
25831 ScottCarnahan feat (RingTheory/HahnSeries): Powers of a binomial t-ring-theory WIP labelled WIP
29871 zach1502 feat(Matrix/Transvection): Gauss pivot determinant identity and pivot preservation new-contributor t-algebra awaiting-author awaiting author
30609 FlAmmmmING feat(Combinatorics/Enumerative/Catalan): large and small Schröder numbers new-contributor t-combinatorics awaiting-author awaiting author
30881 FlAmmmmING feat(RingTheory/PowerSeries/Schroder.lean) : Define the generating function for large and small Schroder number new-contributor ⚠️ awaiting review
31176 mcdoll feat(Analysis): Taylor's theorem with the integral remainder t-analysis WIP labelled WIP
30109 scholzhannah feat: the subcomplexes of a (relative classical) CW complex form a completely distributive lattice t-topology awaiting-author awaiting author
26300 igorkhavkine feat(Analysis/Calculus/FDeriv): continuous differentiability from continuous partial derivatives on an open domain in a product space new-contributor t-analysis awaiting-author WIP labelled WIP
30439 plp127 feat: `norm_num` extension for `IsSquare` on `Nat`, `Int`, `Rat` t-meta awaiting review
31107 rudynicolop feat(Data/Multiset): add Multiset filter and bind lemmas t-data new-contributor awaiting review
30391 rudynicolop feat(Data/List): list splitting definitions and lemmas t-data new-contributor awaiting review
30158 nicolaviolette feat: combinatorics simplegraph basic new-contributor t-combinatorics awaiting-author awaiting author
26544 vihdzp feat(SetTheory/ZFC/Ordinal): Lean ordinals to ZFC ordinals large-import t-set-theory delegated delegated
31168 Rob23oba fix: reduce the amount of coercion instances that are always tried failing CI
27308 xyzw12345 feat(LinearAlgebra/SymmetricAlgebra): IsSymmetricAlgebra t-algebra awaiting review
30431 kckennylau feat(RingTheory): a homogeneous submodule is the span of its homogeneous elements t-ring-theory failing CI
27245 rirarika feat: multivariate polynomial ring properties about irreducibility new-contributor t-algebra awaiting-author awaiting author
27229 WilliamCoram feat(GroupTheory/DoubleCoset): multiple lemmas t-group-theory FLT new-contributor failing CI
25907 mans0954 feat: low order roots of unity t-algebra awaiting review
27516 gaetanserre feat: add rational approximation lemma for suprema in `unitInterval` t-topology awaiting-author awaiting author
30608 grunweg feat: another lemma about derivatives of parametric integrals t-analysis awaiting-author awaiting author
31103 YaelDillies feat: removing leaves from a connected graph keeps it connected t-combinatorics awaiting review
30639 SnirBroshi feat(Combinatorics/SimpleGraph/Connectivity/Connected): `IsBridge` is antitone t-combinatorics awaiting review
30612 grunweg feat: add ContDiff.lipschitzOnWith t-analysis awaiting-author awaiting author
30894 dupuisf feat(CStarAlgebra): the log is operator monotone t-analysis awaiting-author awaiting author
29758 SnirBroshi feat(RingTheory/RootsOfUnity): exp(pi * i * q) is a root of unity for rational q t-ring-theory new-contributor awaiting review
30246 dwrensha make Nat.digits use well-founded recursion once again t-data awaiting review
31243 FlAmmmmING feat(Mathlib/Combinatorics/SimpleGraph/Planar.lean): Define the planar graph in mathlib new-contributor t-combinatorics awaiting review
30648 loefflerd feat(NumberTheory/ModularForms): define the strict width of a subgroup t-number-theory awaiting review
30181 alreadydone feat(Data/Nat): reducible strong recursion t-data awaiting review
30477 jsm28 feat(Geometry/Euclidean/Angle/Bisector): oriented angle bisection and equal distance large-import t-euclidean-geometry awaiting review
30637 strihanje01 feat(Combinatorics/SetFamily/Lindstrom): Lindstrom's theorem for subfamilies with equal unions new-contributor t-combinatorics awaiting review
30733 harahu doc(Combinatorics): spell cliquefree as clique-free t-combinatorics awaiting review
30885 erdOne chore(RingTheory): better defeqs for `PrimeSpectrum.preimageOrderIsoTensorResidueField` t-ring-theory awaiting review
30973 vihdzp feat: generalize `Finsupp.lex_lt_iff_of_unique` t-order awaiting review
30984 erdOne feat(RingTheory): lemmas about scaleRoots t-ring-theory large-import awaiting review
30994 kim-em feat: `fix_deprecations.py` script CI awaiting review
31011 YuvalFilmus feat: properties of Chebyshev polynomials over the reals new-contributor ⚠️ awaiting review
26039 tsuki8 feat(RingTheory/MvPolynomial/{MonomialOrder,Ideal}): leadingTerm t-ring-theory large-import new-contributor awaiting review
29788 robertmaxton42 feat (Topology): adds bundled continuous maps for sum, sigma, subtype, mapsto, inclusion large-import ⚠️ failing CI
26777 YaelDillies chore(Data/Set/Image): move `BooleanAlgebra` material to `Order` large-import t-data WIP labelled WIP
26071 linesthatinterlace feat: Add `id` and `comp` classes for `FunLike` and `refl`, `trans` and `symm` classes for `EquivLike` t-data RFC WIP labelled WIP
28944 linesthatinterlace refactor(Order/Hom/Basic): reorder definitions t-order awaiting-author awaiting author
27973 smmercuri feat: the ring of integers of a `ℤₘ₀`-valued field is compact whenever it is a DVR and the residue field is finite large-import t-algebra awaiting-author awaiting author
30560 dwrensha fix(LinearAlgebra/Alternating/Basic): avoid deep recursion in MultilinearMap.alternatization t-algebra awaiting-author awaiting author
30974 mariainesdff feat(Algebra/Algebra/Basic): add RingHom.commSemiringToCommRing t-algebra awaiting-author 🟤 running CI
29354 themathqueen refactor(Algebra/Algebra/Equiv): allow for non-unital `AlgEquiv` t-algebra awaiting review
30423 erdOne feat(RingTheory): API for valuative rel t-ring-theory awaiting review
30214 SnirBroshi feat(Data/List/Basic): add `Fin` variants of `*mem_iff_getElem` t-data new-contributor awaiting review
19046 j-loreaux feat: define class `SemigroupAction` t-algebra awaiting review
31038 rudynicolop feat(Computability/NFA): NFA acceptsFrom definitions and lemmas t-computability new-contributor awaiting review
30318 joelriou feat(Algebra/ModuleCat/Presheaf): composition of pushforwards and pullbacks and compatibilites t-algebra t-algebraic-geometry t-category-theory awaiting review
30696 joelriou feat(Order/Category): `PardOrdEmb` has filtered colimits large-import t-order awaiting review
30757 SnirBroshi feat(Combinatorics/SimpleGraph/Acyclic): `singletonGraph` and `subgraphOfAdj` are trees t-combinatorics awaiting review
30771 dagurtomas chore(CategoryTheory): move `Closed` directory into `Monoidal` file-removed awaiting review
30826 SnirBroshi feat(Combinatorics/SimpleGraph/Connectivity/Subgraph): map a walk to its own subgraph t-combinatorics awaiting review
30827 dagurtomas feat(Condensed): constructions for light condensed objects can be done in an equivalent small category large-import t-condensed awaiting review
30877 YaelDillies feat(Algebra/MonoidAlgebra): extend the `R[M]` notation to `MonoidAlgebra R M` t-algebra awaiting review
31054 jsm28 feat(LinearAlgebra/AffineSpace/Simplex/Basic): faces and `reindex` t-algebra awaiting review
30595 winstonyin feat: $C^n$ implicit function theorem t-analysis awaiting review
30678 YaelDillies refactor(Algebra/Quaternion): intermediate `Module` instance t-algebra awaiting review
30120 FernandoChu feat(CategoryTheory): Pullback of equalizer is an equalizer large-import t-category-theory awaiting review
30030 JonBannon feat(MeasureTheory): add `MemLp.Const` class and instances to unify `p = ∞` and `μ.IsFiniteMeasure` cases t-measure-probability awaiting-author failing CI
30416 SnirBroshi feat(Logic/Relation): lemmas relating `Relation.Map` and `Function.onFun` new-contributor t-logic awaiting review
30041 josephmckinsey feat(Algebra/Order/Floor): generalize mul_floor_div theorems to rings and semirings new-contributor t-algebra awaiting review
28100 themathqueen feat(LinearAlgebra/GeneralLinearGroup): algebra automorphisms in endomorphisms are inner t-algebra awaiting review
26580 vasnesterov feat(Tactic/Order): translate linear orders to `Int` large-import t-meta awaiting review
31226 erdOne chore(RingTheory): add `@[ext]` to `Ideal.Quotient.algHom_ext` t-ring-theory easy awaiting-author awaiting author
31287 YaelDillies refactor(SetTheory/ZFC): deduplicate coercion to sets t-set-theory awaiting review
31263 LiranShaul feat: arbitrary product of injective modules is injective large-import new-contributor t-algebra awaiting-author awaiting author
30962 WangYiran01 feat(Combinatorics/Enumerative): add lattice path lemmas and counts new-contributor t-combinatorics awaiting review
31072 euprunin golf(Combinatorics/Quiver/Path): golf `exists_eq_comp_and_notMem_tail_of_mem_vertices` using `grind` t-combinatorics awaiting review
31077 peabrainiac feat(Topology): `nhdsSetWithin` filter t-topology awaiting review
31086 kckennylau feat(Util): open unscoped t-meta awaiting review
31087 joelriou feat(CategoryTheory/Sites): categories of sheaves on Over categories, as a pseudofunctor t-category-theory awaiting review
31092 FlAmmmmING feat(Algebra/Group/ForwardDiff.lean): Add theorem `sum_shift_eq_fwdDiff_iter`. new-contributor t-algebra awaiting review
27971 smmercuri feat: weak approximation theorems for infinite places of a number field FLT t-algebra t-number-theory awaiting review
30940 jessealama feat(Data/Set/Image): add Option.range lemmas for elim function t-data awaiting review
31348 PatrickMassot chore: fix a docstring typo t-analysis easy awaiting-author documentation awaiting author
30976 mariainesdff feat(Data/Nat/Choose/Multinomial): add multinomial_eq_of_support_subset t-data awaiting-author awaiting author
29270 euprunin chore: remove redundant `refine` invocations awaiting review
29055 vihdzp feat: `Ordinal.toENat` t-set-theory awaiting-author awaiting author
30754 Jlh18 feat (CategoryTheory/Comma/Over/Pushforward): define pushforwards t-category-theory RFC awaiting review
30647 JovanGerb chore(Tactic/Ring): use Qq more honestly t-meta awaiting review
30669 harahu doc(Algebra): fix typos t-algebra awaiting review
29151 yuanyi-350 feat: Corollary of Hahn–Banach theorem large-import new-contributor awaiting-author ⚠️ awaiting author
29776 yuanyi-350 chore(Functional Analysis) : refactor `ContinuousLinearMap.isOpenMap` by separating it into sublemmas t-analysis awaiting-author WIP labelled WIP
30144 alreadydone feat(Data/Nat): kernel reducible binaryRec t-data t-algebra awaiting review
30242 YaelDillies chore: rename `mul_le_mul_right'` to `mul_le_mul_left` t-order t-algebra awaiting review
30657 alreadydone feat(Algebra): generalize Picard group to Semiring t-algebra awaiting review
31113 515801431 feat(Mathlib/Combinatorics/Enumerative/Polya.lean): Add additional theorem in `Polya.lean` new-contributor t-combinatorics awaiting review
31132 kckennylau Feat(Algebra): saturation of a submonoid t-algebra awaiting review
28719 mitchell-horner refactor: redefine `IsTuranMaximal` t-combinatorics awaiting review
27991 sinianluoye feat (Rat): add Rat.den_eq_of_add_den_eq_one and its dependent lemmas t-data new-contributor awaiting-author failing CI
30047 ooovi feat(Combinatorics/SimpleGraph): edge labellings maintainer-merge t-combinatorics awaiting-author awaiting author
22919 plp127 feat(Data/Fintype/Pi): Make `Fintype` instance for `RelHom`s computable t-data awaiting-author awaiting author
31101 emilyriehl feat(Algebraic Topology): the strict bicategory of quasicategories t-algebraic-topology infinity-cosmos t-category-theory awaiting-author awaiting author
31201 euprunin chore(RingTheory): golf `isPrimary_decomposition_pairwise_ne_radical` using `grind` t-ring-theory maintainer-merge awaiting review
30727 joelriou feat(CategoryTheory/Presentable): presentable objects in `Type` t-category-theory awaiting review
30795 joelriou feat(CategoryTheory): final functors from a `κ`-filtered category large-import t-category-theory WIP labelled WIP
27258 JovanGerb Imo2020 q6 IMO awaiting review
29147 ocfnash feat: miscellaneous root system lemmas t-algebra awaiting review
31118 LLaurance feat(Combinatorics/SimpleGraph/Connectivity/Subgraph): the path of a walk is a subgraph of the walk itself t-combinatorics awaiting review
30559 SnirBroshi feat(Data/Sym/Sym2): add `Sym2.diagSet` t-data awaiting review
28557 ShreckYe feat(Data/Nat/Factorization): some results on equality of powers of naturals proved from factorization t-data awaiting review
27824 ChrisHughes24 feat(Calculus): exists_gt_of_deriv_pos and variants t-analysis awaiting-author awaiting author
29449 mitchell-horner feat(Combinatorics/SimpleGraph): add Turán density related theorems t-combinatorics awaiting review
31416 SnirBroshi feat(Combinatorics/SimpleGraph/Walk): lemmas about the first and last darts/edges t-combinatorics awaiting review
30232 SnirBroshi feat(Combinatorics/SimpleGraph/Connectivity/Subgraph): add `ConnectedComponent.toSubgraph` new-contributor t-combinatorics awaiting review
31418 mitchell-horner feat(Combinatorics/SimpleGraph): impl `Iso.degree_eq` and `Iso.minDegree_eq` and `Iso.maxDegree_eq` t-combinatorics awaiting review
27602 mitchell-horner feat(Combinatorics/SimpleGraph): define `CompleteBipartiteSubgraph` t-combinatorics awaiting review
31423 harahu doc(Combinatorics): ensure only a single H1 header per file t-combinatorics awaiting review
27599 mitchell-horner feat(Combinatorics/SimpleGraph): define `CompleteEquipartiteSubgraph` t-combinatorics awaiting review
27493 themathqueen feat(RingTheory/Coalgebra): define Frobenius algebra t-ring-theory awaiting review
30987 AntoineChambert-Loir feat(LinearAlgebra/SpecialLinearGroup): special linear group of a module t-algebra awaiting review
26710 metakunt feat (Data/Nat/Digits/Lemmas): Add digits_getD t-data new-contributor awaiting review
30853 JovanGerb feat(LinearAlgebra/AffineSpace/Simplex): `CoeFun` instance for `Simplex` ⚠️ awaiting review
31055 jsm28 feat(Geometry/Euclidean/Projection): `orthogonalProjectionSpan_congr` maintainer-merge t-euclidean-geometry awaiting review
30618 wwylele feat(Combinatorics): Glaisher's theorem t-combinatorics awaiting review
28346 joelriou feat(AlgebraicTopology/SimplicialSet): rank functions for pairings t-algebraic-topology awaiting review
30860 FormulaRabbit81 feat(Measure): prove the space of probability measures on a compact space is compact large-import WIP ⚠️ labelled WIP
31097 joelriou feat(AlgebraicTopology): the model category structure on Over categories t-algebraic-topology awaiting review
31140 b-mehta chore(Data/Int/GCD): review API t-data failing CI
31313 plp127 feat(HasSumUniformlyOn): generalize theorem t-topology awaiting-author awaiting author
31431 harahu doc(Data): misc. improvements t-data awaiting review
29610 llllvvuu feat(LinearAlgebra): define LinearMap.Eigenbasis t-algebra awaiting review
22782 alreadydone feat(Topology): étalé space associated to a predicate on sections t-topology merge conflict
22662 plp127 feat: Localization.Away.lift (computably) t-algebra awaiting review
31144 YaelDillies feat: transfer `FaithfulSMul`/`NoZeroSMulDivisors` along equivs t-algebra awaiting review
31194 grunweg feat: add `#check'` command and tactic, which only show explicit arguments t-meta awaiting review
31199 YaelDillies feat: recursion principle for `Mᵐ⁰` CFT t-algebra awaiting review
31204 jsm28 feat(LinearAlgebra/AffineSpace/Combination): `affineCombination_mem_affineSpan_image` t-algebra awaiting review
31206 jsm28 feat(Geometry/Euclidean/Incenter): bound coordinates of the incenter t-euclidean-geometry awaiting review
30548 fbarroero feat(Analysis/Polynomial/MahlerMeasure): the Mahler measure of a linear polynomial and applications large-import t-analysis t-number-theory awaiting-author awaiting author
31462 ScottCarnahan feat (Algebra/Lie/Extension): 2-cocycle from a Lie algebra extension with abelian kernel and a linear splitting t-algebra awaiting review
28248 YaelDillies feat: expectation and (conditional) variance of a Bernoulli random variable t-measure-probability awaiting-author awaiting author
30988 erdOne feat(AlgebraicGeometry): descending affine cover of an inverse limit large-import t-algebraic-geometry awaiting review
30348 RemyDegenne feat: convergence in probability implies convergence in distribution maintainer-merge t-measure-probability awaiting review
30140 chrisflav feat(AlgebraicGeometry): locally directed colimits in `P.Over ⊤ S` t-algebraic-geometry awaiting review
27306 xyzw12345 feat: `lie_ring` tactic and `LieReduce` command t-meta awaiting review
30171 smmercuri feat(DedekindDomain/AdicValuation): `le_one` lemmas for `HeightOneSpectrum.valuation` and specialisations to `Rat` t-ring-theory awaiting review
31036 chrisflav chore(RingTheory): prerequisites for #31034 t-ring-theory awaiting review
31467 maix00 feat(Combinatorics/SimpleGraph): add simp lemma `getVert_map` for `Walk.map` new-contributor t-combinatorics awaiting review
30797 adamtopaz feat(Mathlib/Tactic/CategoryStar): Category* t-meta awaiting review
26231 chrisflav feat(CategoryTheory/Sites): sheaf condition and coproducts t-category-theory awaiting-author failing CI
31001 gasparattila fix(Tactic/FunProp): fix "loose bvar in expression" error t-meta awaiting review
31308 alreadydone feat(RingTheory): `Module.Invertible.tmul_comm` t-ring-theory t-algebra awaiting review
31444 harahu doc(Probability/Martingale/BorelCantelli): polish docstrings t-measure-probability delegated delegated
27244 xroblot feat(RingTheory/DedekindDomain): lifting an ideal in an extension is injective t-ring-theory large-import awaiting review
15443 YaelDillies feat: Marcinkiewicz-Zygmund inequality t-analysis WIP labelled WIP
31429 llllvvuu feat(Topology): generalize `IsModuleTopology` lemmas to semilinear maps t-topology awaiting review
25799 dagurtomas feat(CategoryTheory): the universal property of localized monoidal categories t-category-theory awaiting review
31473 YaelDillies feat(RingTheory): compute `counitAlgHom`/`comulAlgHom` on specific bialgebras t-ring-theory toric awaiting review
31366 FaffyWaffles feat(Analysis/SpecialFunctions/StirlingRobbins): Robbins' sharp stepwise bound for stirlingSeq new-contributor t-analysis awaiting-author awaiting author
27053 tb65536 (WIP) Galois group of `x^n - x - 1` large-import t-algebra WIP labelled WIP
31362 BeibeiX0 feat(partitions): generalized pentagonal numbers. new-contributor t-combinatorics awaiting review
31489 alreadydone feat(FieldTheory): fg extension over perfect field is separably generated large-import t-algebra failing CI
30998 erdOne feat(FieldTheory): fg extension over perfect field is separably generated t-algebra awaiting-author awaiting author
31351 grunweg feat: manifolds with smooth boundary t-differential-geometry WIP labelled WIP
26831 AntoineChambert-Loir feat(GroupTheory/SpecificGroups/Alternating/MaximalSubgroups): maximal subgroups of the alternating group t-group-theory awaiting review
24965 erdOne refactor: Make `IsLocalHom` take unbundled map t-algebra awaiting review
30133 smmercuri feat: `WithVal v` and `WithVal w` are isomorphic as uniform spaces when `v` and `w` are equivalent valuations ⚠️ awaiting review
31145 FernandoChu chore(CategoryTheory): `IsRegularEpi` and its `MorphismProperty` large-import t-category-theory awaiting review
31210 jsm28 feat(Geometry/Euclidean/MongePoint): `reindex` lemmas t-euclidean-geometry awaiting review
31215 ScottCarnahan feat (RingTheory/HahnSeries): introduce binomialFamily and generalized powers. t-ring-theory awaiting review
31224 YaelDillies feat(Algebra/Homology): pushforward of connected complexes CFT t-algebra awaiting review
31425 robertmaxton42 feat (Topology) : implement delaborators for non-standard topology notation t-topology awaiting-author awaiting author
29425 pechersky feat(NumberTheory/Padics/Torsion): `HasEnoughRootsOfUnity ℤ_[p] (p - 1)` t-ring-theory awaiting review
24627 pechersky feat(Topology/Algebra/Valued): `IsLinearTopology 𝒪[K] K` and `𝒪[K] 𝒪[K]` t-topology awaiting review
31494 jsm28 feat(Geometry/Euclidean/Sphere/SecondInter): `eq_or_eq_secondInter_of_mem_affineSpan_pair_iff_mem` t-euclidean-geometry awaiting review
31240 AntoineChambert-Loir feat: base change properties, direct sums, bases, modules of linear maps t-algebra awaiting review
29517 pechersky feat(RingTheory/Torsion): torsion = union of roots of unity t-algebra failing CI
31133 thorimur feat(Linter): combinators for linter option boilerplate t-linter t-meta awaiting review
31498 zcyemi feat(LinearAlgebra/AffineSpace/Independent): add affine independence permutation lemmas for three points t-algebra awaiting review
31499 zcyemi feat(LinearAlgebra/AffineSpace/FiniteDimensional): add lemma preserving affine independence under collinear point replacement t-algebra awaiting review
25779 robin-carlier feat(CategoryTheory/Bicategory/NaturalTransformations): strong and lax natural transformations of lax functors t-category-theory awaiting review
29145 JovanGerb chore: use `to_additive` in more places awaiting-CI t-meta does not pass CI
31395 peakpoint feat(Analysis/Normed/Affine/Isometry): interpret `AffineIsometry{Map,Equiv}` as `ContinuousAffine{Map,Equiv}` new-contributor t-analysis awaiting-author awaiting author
31298 jjdishere feat(RingTheory/AdicCompletion): `IsAdicComplete.lift` APIs for `RingHoms` t-ring-theory awaiting review
31503 Scarlett-le feat(Geometry/Euclidean/PerpBisector): add distance inequalities for Sbtw with perpendicularity new-contributor t-euclidean-geometry awaiting review
31496 Scarlett-le feat(Geometry/Euclidean/Sphere/Power): power equals squared tangent length and characterization of tangency large-import new-contributor t-euclidean-geometry awaiting review
30349 loefflerd feat(Topology/Constructions): `IsDiscrete` predicate on sets t-topology awaiting-author awaiting author
31414 SnirBroshi feat(Data/Nat/Bitwise): formula for the xor of {0,...,n} t-data awaiting review
31506 FLDutchmann feat: Qq version of getLevel maintainer-merge t-meta awaiting review
31353 EtienneC30 feat: ofLp and toLp of a sum t-algebra t-analysis awaiting-author awaiting author
31173 jsm28 feat(Mathlib/Geometry/Euclidean/Incenter): excenters do not lie in faces t-euclidean-geometry awaiting review
26390 jjdishere feat(Topology/Algebra): Krasner's lemma t-algebra t-topology t-number-theory WIP labelled WIP
26277 AntoineChambert-Loir feat(RingTheory/Congruence/Hom): prove basic isomorphisms theorems for ring congruences t-ring-theory awaiting review
31227 YaelDillies feat(Algebra/Homology): sandwich a comm group between two finite comm groups CFT maintainer-merge t-algebra awaiting review
31464 Ljon4ik4 improved R-linearity to A-linearity in the PushForward of Derivations t-ring-theory new-contributor awaiting review
31231 Jlh18 refactor: MorphismProperty.HasPullbacksAlong t-category-theory awaiting review
30895 callesonne feat(Bicategory/Modification/Pseudo): define modifications between strong natural transformations of pseudofunctors t-category-theory awaiting review
30132 callesonne feat(Bicategory/Functor/Strict): add `StrictPseudofunctor` t-category-theory awaiting review
31388 b-mehta feat(Topology/Order): add unordered versions of topological Rolle's theorem tech debt t-analysis awaiting-author awaiting author
31512 gasparattila feat(MeasureTheory): typeclass for measurability of equality t-measure-probability awaiting review
31504 joelriou refactor(CategoryTheory/Shift): export Functor.CommShift.commShiftIso t-category-theory awaiting review
31407 SnirBroshi feat(Analysis/SpecialFunctions/Gamma/BohrMollerup): Gamma is strictly decreasing on (0, 1] t-analysis awaiting review
31180 CoolRmal feat(Analysis): a closed convex set is the intersection of countably many half-spaces in a separable Banach space new-contributor t-analysis awaiting-author awaiting author
29856 mans0954 feat(Analysis/Normed/Ring/Basic): Add NonUnitalNonAssocSeminormedRing and NonUnitalNonAssocNormedRing awaiting-bench t-analysis awaiting review
29512 grunweg feat: check for PR titles which do not start with "feat" etc. CI failing CI
31520 harahu doc(Geometry): ensure only a single H1 header per file t-differential-geometry awaiting review
31519 harahu doc(FieldTheory): ensure only a single H1 header per file t-algebra awaiting review
31521 harahu doc(GroupTheory): ensure only a single H1 header per file t-group-theory awaiting review
31522 harahu doc(LinearAlgebra): ensure only a single H1 header per file t-algebra awaiting review
31179 SnirBroshi feat(Algebra/QuadraticAlgebra/NormDeterminant): norm = det of left-mul endomorphism t-algebra awaiting review
26912 pechersky chore(Algebra/Ring/Subring): simp tag `Subring.smul_def` t-algebra awaiting review
31524 harahu doc(Logic/Equiv/Fintype): fix typos t-logic awaiting review
28766 yury-harmonic feat(Nat/Factorial): use binary splitting for `ascFactorial`/`descFactorial` t-data new-contributor awaiting-author awaiting author
30879 grunweg feat: beta reduce in the `T%` elaborator t-differential-geometry t-meta awaiting review
28793 grunweg feat: smooth immersions t-differential-geometry awaiting review
26149 vasnesterov feat(Topology): continuous surjection from Cantor set to Hilbert cube t-topology awaiting review
30168 joelriou feat(CategoryTheory): closure under bounded colimits large-import t-category-theory awaiting review
30570 SnirBroshi feat(Combinatorics/SimpleGraph/Connectivity/Connected): `reachabilitySet` ⚠️ awaiting review
30798 joelriou feat(Algebra/Category/ModuleCat): a functorial projective resolution t-category-theory awaiting review
30812 joelriou feat(CategoryTheory/Abelian): construction of reduced left resolutions t-category-theory awaiting review
30897 euprunin chore(Order/Defs): golf multiple lemmas in `LinearOrder` using `grind` t-order awaiting review
31051 joelriou chore(CategoryTheory): adding grind annotations for `op_comp` and `Quiver.Hom.comp_toLoc` t-category-theory awaiting review
31147 daefigueroa feat(Dynamics): point transitive monoid actions and transitive points new-contributor t-dynamics awaiting review
31221 themathqueen chore(Algebra/Star/LinearMap): moving stuff around large-import t-algebra awaiting review
31239 Paul-Lez feat(NumberTheory/NumberField/InfinitePlace): A few easy lemmas about totally real fields t-number-theory awaiting review
31242 plp127 feat: express filter as supremum of principal filter and free filter t-order awaiting review
31250 joelriou feat(AlgebraicTopology): inductive construction of StrictSegal structures t-algebraic-topology maintainer-merge awaiting review
31256 jsm28 feat(Geometry/Euclidean/SignedDist): `signedInfDist_reindex` t-euclidean-geometry awaiting review
31257 jsm28 feat(LinearAlgebra/AffineSpace/Simplex/Basic): more `reindex` lemmas t-algebra awaiting review
31258 joelriou chore(CategoryTheory/Limits/Types): split Shapes.lean large-import t-category-theory awaiting review
31259 YaelDillies refactor(Dynamics): use `SetRel` notions of separation and cover t-dynamics awaiting review
31294 erdOne feat(Analysis): Weierstrass ℘ functions t-analysis awaiting review
31309 gasparattila feat(Probability/Independence): reindexing lemmas for `iIndep*` t-measure-probability awaiting review
31315 Parcly-Taxel feat: IMO 2010 Q5 IMO awaiting review
31356 adomani feat: add inspect-like functions t-meta awaiting review
31358 erdOne feat(RingTheory): universal factorization map of polynomials ⚠️ awaiting review
31371 euprunin chore(RingTheory): golf `RingTheory/` using `order` awaiting review
31387 gasparattila feat(Topology/Separation): condition for regularity given a subbasis t-topology awaiting review
31389 YaelDillies chore: golf proofs involving permutations awaiting review
31400 joelriou feat(CategoryTheory): deriving functors using a right derivability structure t-category-theory awaiting review
31401 SnirBroshi feat(NumberTheory/Real/GoldenRatio): add two more fib identities t-number-theory awaiting review
31526 Aaron1011 feat: Add multiplicative version of structure theorem for finitely generated abelian groups t-group-theory new-contributor awaiting review
28266 euprunin chore(RingTheory): golf entire `single_one_eq_pow` using `simp`. deprecate `single_inv`. t-ring-theory awaiting review
12032 mcdoll feat: delta distribution as a limit t-analysis WIP labelled WIP
31528 bwangpj feat: MulAction.fixedPoints and MulAction.fixedBy under MulActionHom t-group-theory large-import failing CI
31502 urkud feat: add a version of Bernoulli's inequality large-import t-algebra awaiting review
24019 urkud feat(Analysis): Poincaré lemma for 1-forms t-analysis failing CI
30331 urkud feat(Calculus): derivative of `ContinuousAlternatingMap.compContinuousLinearMap` t-analysis awaiting review
30950 jessealama feat: add AffineEquiv.ofLinearEquiv t-algebra delegated delegated
31376 euprunin chore: use `order` instead of `linarith` to make the intent clearer awaiting review
31530 euprunin chore(Data/List): golf entire `drop_length_sub_one` using `ext; grind` t-data awaiting review
30389 euprunin fix: correctly apply `hint` priority (was always set to default 1000 due to a bug) t-meta bug awaiting review
31539 joelriou feat(CategoryTheory/Triangulated): basic lemmas for t-structures t-category-theory awaiting review
28349 kckennylau feat(Meta): add notation for naming stacked polynomials t-meta awaiting-author awaiting author
26212 Thmoas-Guan feat(Algebra): the Rees theorem for depth large-import t-algebra awaiting review
26210 Thmoas-Guan feat(RingTheory): associated primes of localized module t-ring-theory large-import awaiting-author awaiting author
24730 YaelDillies feat(RingTheory): group-like elements t-ring-theory toric awaiting review
31536 joelriou feat(CategoryTheory/Triangulated): the category of triangles is preadditive large-import t-category-theory awaiting review
31537 RemyDegenne feat: totally bounded sets have finite covers maintainer-merge t-topology awaiting review
28599 Thmoas-Guan feat(RingTheory) : polynomial over CM ring is CM t-ring-theory large-import WIP labelled WIP
28582 Thmoas-Guan feat(Data): some lemmas about WithBot ENat t-data awaiting-author awaiting author
28682 Thmoas-Guan feat(RingTheory): definition of regular local ring t-ring-theory awaiting-author awaiting author
29558 Thmoas-Guan feat(Algebra): definition of global dimension t-ring-theory awaiting-author awaiting author
26975 Whysoserioushah feat: a norm_num extension for complex numbers t-meta failing CI
31219 Thmoas-Guan feat(Algebra): lemma about `IsBaseChange` under exact sequence ⚠️ awaiting review
31543 grunweg chore: rename FiniteDimensional.of_fintype_basis t-algebra awaiting review
31540 themathqueen chore: move `LinearAlgebra/Matrix/HermitianFunctionalCalculus` to `Analysis/Matrix` file-removed maintainer-merge t-analysis awaiting review
30083 grunweg feat: local frames in a vector bundle t-differential-geometry awaiting review
31550 RemyDegenne feat: properties of sub-Gaussian random variables t-measure-probability awaiting review
31511 bwangpj feat: fixed points of normal subgroup is stable under the group action t-group-theory awaiting review
31027 YaelDillies chore: shortcut instance for `Nat` to be mul-torsion-free CFT t-algebra awaiting review
31430 gasparattila feat(Topology/Sets): `Unique`, `Nontrivial`, etc. instances for `(Nonempty)Compacts` t-topology awaiting review
31487 b-mehta feat(SpecialFunctions/Log): tight bounds on artanh(x) t-analysis awaiting-author awaiting author
31549 ADedecker feat: more API on tsupport and operations on functions t-topology awaiting review
31555 EtienneC30 feat: bounded distance implies bounded space t-topology awaiting review
25822 ScottCarnahan WIP: experiments with vertex algebras large-import WIP labelled WIP
30928 themathqueen chore(LinearAlgebra/Matrix/PosDef): rename `Matrix.InnerProductSpace.ofMatrix` t-algebra awaiting review
31514 staroperator feat(Order): reprove Dickson's lemma t-order awaiting review
27107 AntoineChambert-Loir feat(GroupTheory/GroupAction/SubMulAction/Combination) : combinations and group actions t-group-theory awaiting review
31548 AntoineChambert-Loir feat(Analysis/Convex/Quasiconvex): properties of quasiconcave functions large-import ⚠️ awaiting review
31547 AntoineChambert-Loir feat(Analysis/Convex/SaddlePoint): define saddle points of a map large-import ⚠️ awaiting review
31326 sgouezel chore: deprecate `smooth` variants of `contMDiff` results t-differential-geometry awaiting review
31403 JovanGerb feat(push_neg): tag `not_frequently` and `not_eventually` t-meta delegated delegated
31166 gasparattila feat(Topology/Sets): add `NonemptyCompacts.map` t-topology awaiting review
30201 luigi-massacci feat: add differentiation for ContDiffMapSupportedIn maintainer-merge t-analysis awaiting review
31046 Thmoas-Guan feat(Homology) : map between `Ext` induced by exact functor ⚠️ awaiting review
31554 bwangpj feat: define Subrepresentation FLT t-algebra awaiting review
31541 RemyDegenne feat: Monotonicity of hitting times t-measure-probability awaiting-author awaiting author
28884 kim-em chore: deprecate ShiftLeft Int instance t-data awaiting review
31559 joelriou feat(Algebra/Homology): a factorization of morphisms of cochain complexes t-category-theory awaiting review
30870 tb65536 refactor(FieldTheory/*): partially switch over from `Polynomial.Splits` to `Polynomial.Factors` t-algebra awaiting review
31497 staroperator feat(Algebra/Group): semigroup ideals maintainer-merge t-algebra awaiting review
31273 euprunin chore(MeasureTheory/MeasurableSpace): golf `measurableSet_generateFrom_singleton_iff` using `grind` maintainer-merge t-measure-probability awaiting review
31398 YaelDillies feat(MeasureTheory/Measure): `comap_apply` version for measurable equivs maintainer-merge t-measure-probability awaiting review
31558 AntoineChambert-Loir feat(Topology/Sublevel): sublevels and overlevels, relation with semicontinuity t-topology awaiting review
31551 RemyDegenne feat: `gaussianReal_const_sub` t-measure-probability awaiting-author awaiting author
30989 kckennylau feat(RingTheory): Teichmuller map ⚠️ failing CI
30995 kckennylau feat(RingTheory): adic limit t-ring-theory awaiting-author awaiting author
30833 kckennylau feat(Data): IsScalarTower for ZMod t-data awaiting-author failing CI
30451 kckennylau feat(HomogeneousIdeal): generalize to homogeneous submodule t-ring-theory failing CI
31007 kckennylau feat(RingTheory): generalise perfection to monoids ⚠️ failing CI
28013 astrainfinita feat: Lindemann-Weierstrass Theorem t-algebra t-analysis awaiting review
31121 jessealama feat: add ComplexShape.EulerCharSigns for generalized Euler characteristic t-algebra t-category-theory awaiting-author awaiting author
31562 MichaelStollBayreuth chore: clean up imports awaiting review
31278 ADedecker feat: approximate continuous functions by smooth functions maintainer-merge t-analysis t-differential-geometry failing CI
31571 erdOne feat(RingTheory): existence of local algebra with given residue field t-ring-theory awaiting review
31570 tb65536 feat(GroupTheory/Perm/ClosureSwap): add slight generalization t-group-theory awaiting review
31573 SnirBroshi feat(Combinatorics/SimpleGraph): split `Walk.lean` into 4 files t-combinatorics awaiting review
31572 tb65536 feat(Algebra/Group/Subgroup/Basic): API lemma relating `inertia` and `subgroupOf` t-group-theory t-algebra awaiting review
30650 JovanGerb perf(reassoc, to_app, elementwise): don't pass the same proof to the kernel again maintainer-merge t-meta awaiting review
13740 YaelDillies feat: more robust ae notation t-measure-probability t-meta awaiting review
30213 SnirBroshi feat(Data/List/GetD): golf and add lemmas for `get` and `getElem?` t-data new-contributor awaiting review
30706 astrainfinita refactor(Analysis/NormedSpace/Exponential): remove the `𝕂` argument from `exp` t-analysis blocked on another PR
30684 YaelDillies chore: deprecate `monoidalOfHasFiniteProducts` large-import t-category-theory awaiting review
30814 yuanyi-350 feat(LinearAlgebra/Dimension/RankDecomposition): Rank decomposition and bases adapted to a linear map t-algebra awaiting review
30851 FormulaRabbit81 feat(Topology): prove there exists an embedding of separable metric spaces in the hilbert cube file-removed ⚠️ awaiting review
30857 erdOne feat(RingTheory): miscellaneous lemmas about etale t-ring-theory awaiting review
30983 erdOne feat(RingTheory): results on resultant t-ring-theory awaiting review
31264 plp127 feat(Filter): replace coframe instance with better defeqs t-order awaiting review
31265 joelriou feat(AlgebraicTopology): Edge and CompStruct for simplicial sets t-algebraic-topology awaiting review
31293 erdOne feat(Algebra/InfiniteSum): `HasProdUniformly` and friends t-algebra t-topology RFC awaiting review
31305 kim-em feat: grind golfing in Topology/Path ⚠️ awaiting review
31324 YaelDillies chore(Finsupp): move `mapRange.equiv` earlier t-algebra awaiting review
31337 chrisflav feat(CategoryTheory): add predicate `IsRepresentedBy` t-category-theory awaiting review
31342 kim-em feat: `extract_goal` preserves explicit foralls t-meta awaiting review
31360 erdOne feat(RingTheory): coeffs of a poly is integral if it divides an integral poly t-ring-theory awaiting review
31374 euprunin chore: use `order` instead of `aesop` to make the intent clearer awaiting review
31377 CoolRmal feat: a series of smooth functions that converges (locally) uniformly is smooth new-contributor t-topology awaiting review
31385 harahu doc(MathlibTest): demote repeated H1 headers to H2 awaiting review
31421 joelriou feat(CategoryTheory): HasCardinalLT for MorphismProperty and ObjectProperty t-category-theory awaiting review
31428 harahu doc(AlgebraicTopology/SingularSet): fix typos t-algebraic-topology awaiting review
31424 joelriou feat(CategoryTheory): description of the type WalkingMultispan t-category-theory awaiting review
31441 harahu doc(Dynamics): polish docstrings t-dynamics awaiting review
31446 harahu doc(MeasureTheory/Measure/Regular): polish docstrings t-measure-probability awaiting review
31449 kim-em feat(SemilocallySimplyConnected): definition and alternative formulation ⚠️ awaiting review
31535 ADedecker feat: small tweaks to `PointwiseConvergenceCLM` maintainer-merge t-topology awaiting review
29562 ShreckYe feat(Analysis/SpecialFunctions/Trigonometric): tangent half-angle substitution t-analysis awaiting review
31575 kim-em chore: reverse the directions of Path.symm_cast and trans_cast t-topology awaiting review
29458 LiamSchilling feat(MvPolynomial/WeightedHomogenous): relate `weightedTotalDegree` to `degrees` and `degreeOf` t-ring-theory new-contributor awaiting-author awaiting author
31114 mcdoll feat(Analysis): use new notation for Fourier transform on Schwartz functions and simplify presentation t-analysis awaiting review
31525 kim-em feat: convex combinations in `Set.Icc` t-topology awaiting review
31577 mcdoll feat(Analysis): the topology of pointwise convergence is locally convex t-analysis awaiting review
26803 bjoernkjoshanssen feat: second partial derivatives test t-analysis awaiting-author failing CI
31557 kex-y feat: lemmas on the stopped process and stopped value t-measure-probability awaiting review
31408 peakpoint feat(Analysis/Calculus/LHopital): L'Hopital's rule from within a convex set new-contributor t-analysis awaiting review
31564 EtienneC30 feat: injectivity of the map forgetting the continuity of bilinear maps t-topology awaiting review
31566 EtienneC30 feat: when a measure is equal to a `gaussianReal` t-measure-probability awaiting review
30129 vlad902 feat(SimpleGraph): define and prove basic theory of vertex covers t-combinatorics awaiting review
28693 faenuccio feat(Analysis.Normed.Module.Milman-Pettis): add Milman-Pettis theorem t-analysis WIP labelled WIP
29997 xroblot feat(CyclotomicFields): general formula for the discriminant large-import t-number-theory awaiting review
31581 kebekus feat: behavior of the counting function under addition t-analysis awaiting review
31556 kebekus feat: behavior of the proximity function under addition t-analysis awaiting review
31584 joelriou chore: move CategoryTheory.ComposableArrows file-removed t-category-theory awaiting review
23940 YaelDillies feat: polytopes toric t-analysis awaiting-author failing CI
31546 RemyDegenne feat: MeasurableSet.iff maintainer-merge t-measure-probability awaiting review
31545 RemyDegenne feat: products of identically distributed random variables t-measure-probability awaiting-author awaiting author
31583 kebekus feat: describe the logarithmic counting function in terms of circle averages large-import t-analysis awaiting review
31574 kim-em feat: lemmas for paths-up-to-homotopy t-algebraic-topology t-topology awaiting review
31434 stepanholub feat: simple divisibility lemma t-data new-contributor awaiting review
31544 RemyDegenne feat: add `MeasureTheory.Measure.integrable_comp_iff` maintainer-merge t-measure-probability awaiting review
31451 jsm28 feat(Analysis/Convex/Combination): `centerMass_const`, `centerMass_congr` t-convex-geometry maintainer-merge t-analysis awaiting review
31493 jsm28 feat(Geometry/Euclidean/Incenter): `incenter_mem_interior` maintainer-merge t-euclidean-geometry awaiting review
31579 xroblot feat(Data/Nat/Digits): prove the bijection induced by `Nat.ofDigits` and use it to compute the sum of the sum of digits t-data awaiting review
31062 zcyemi feat(Geometry/Euclidean/Similarity): add triangle similarity t-euclidean-geometry awaiting review
31590 SuccessMoses Add `simp` attr to `commutatorElement_def` new-contributor t-algebra failing CI
31591 gasparattila chore(Topology/Sets): use prefix naming for `toCompacts` in `simps` t-topology awaiting review
31592 gasparattila chore(Tactic/Measurability): `fun_prop` lemmas for solving `MeasurableSet {x | ...}` goals t-measure-probability awaiting review
31341 dagurtomas feat(CategoryTheory): constructors for monoidal functors after pre/post composing with monoidal equivalences t-category-theory awaiting-author awaiting author
30039 JovanGerb feat(push): `push` annotations for `Real.log` t-meta awaiting-author awaiting author
31593 Ruben-VandeVelde feat: some lemmas about MonoidAlgebra t-algebra awaiting review
30042 JovanGerb feat(push): `@[push]` attributes for `∈` in `Set`, `Finset` and `Multiset` t-meta awaiting-author awaiting author
31518 YaelDillies chore(LinearAlgebra/Matrix): import less analysis file-removed t-analysis awaiting review
31336 chrisflav feat(CategoryTheory/Sites): cover of pullback from cover of left or right component t-category-theory awaiting-author awaiting author
31217 YaelDillies feat: turn a closed walk into a cycle t-combinatorics awaiting review
31569 sgouezel feat: drop a finiteness assumptions in covariance results t-measure-probability awaiting review
31595 astrainfinita chore: redefine `Ideal.IsPrime` t-algebra awaiting review
30071 Jlh18 feat: dualize Pseudofunctor.CoGrothendieck results to Pseudofunctor.Grothendieck t-category-theory awaiting review
31415 SnirBroshi feat(NumberTheory/Niven): `exp(q π i)` is integral for rational `q` t-number-theory awaiting-author awaiting author
27606 CBirkbeck Eisenstein q exp identity large-import awaiting-author awaiting author
30594 j-loreaux feat: generalize continuity results for the continuous functional calculus t-analysis awaiting review
30842 kim-em feat: add Aristotle task for command palette CI awaiting review
31031 gasparattila feat(Topology/UniformSpace): define the Hausdorff uniformity t-topology awaiting review
31433 sinhp feat (CategoryTheory): Computable cartesian monoidal structure on slices induced by chosen pullbacks t-category-theory awaiting review
27163 pechersky feat(Topology/ValuativeRel): of and to basis of compatible valuations t-algebra t-topology t-number-theory awaiting review
30505 mariainesdff feat(NumberTheory/RatFunc/Ostrowski): prove Ostrowski's theorem for K(X) t-algebra t-number-theory awaiting-author awaiting author
31399 CoolRmal feat: Conditional expectation commutes with continuous linear functionals and affine functions. new-contributor t-measure-probability awaiting review
31161 AntoineChambert-Loir feat(RingTheory/MvPolynomial/IrrQuadratic): irreducibility of sum X_i Y_i ⚠️ awaiting review
31605 euprunin chore(Combinatorics/SimpleGraph): golf `circulantGraph_eq_symm` using `grind` t-combinatorics awaiting review
31534 euprunin chore(Probability/ProbabilityMassFunction): golf entire `support_bindOnSupport` using `ext; simp` t-measure-probability awaiting review
31598 euprunin chore(Data/List): golf `ofFn_eq_pmap` using `ext; grind` t-data awaiting review
31597 grunweg chore(AtLocation): allow throwing a warning when no progress is being made t-meta awaiting review
31599 euprunin chore(Data/List): golf `insertIdx_pmap` using `ext; grind` t-data awaiting review
31602 euprunin chore(Data/Set): golf `image_sUnion` using `grind` t-data awaiting review
30913 eric-wieser feat(Computability/Language): add subtraction notation maintainer-merge t-computability failing CI
31563 EtienneC30 feat: small lemma about InnerProductSpace.toDual t-analysis awaiting review
31603 alreadydone chore(Algebra): make `RatFunc` an abbrev t-algebra RFC awaiting review
31607 grunweg chore: rename `continuous{,On,At,Within}_const to `ContinuousXXX.const` awaiting-CI does not pass CI
31600 grunweg chore: replace by_cases! with by_cases when the push_neg step does no… WIP labelled WIP
31596 grunweg chore: remove extraneous uses of push_neg WIP labelled WIP
31510 JovanGerb feat(contrapose): cancel negations, and support `↔` maintainer-merge t-meta awaiting review
31609 JovanGerb fix(rw??): `whnf` on equality hypotheses t-meta awaiting review
31608 JovanGerb fix(unfold?): improved implementation of `isUserFriendly` t-meta failing CI
31247 rudynicolop feat(Computability/DFA): add DFA complement, union, and intersection t-computability new-contributor awaiting review
31523 kim-em chore: fix version comparison in lake update hook awaiting review
31611 thorimur feat(Meta): `withPlural` wrapper for more readable messages in source t-meta awaiting review
31244 kim-em chore: use generic `map_X` lemmas where possible awaiting review
30793 LessnessRandomness feat(Analysis/InnerProductSpace/Basic): add a simp lemma t-analysis awaiting-author awaiting author
31612 JovanGerb chore(Tactic/Translate): rename the `ToAdditive` folder file-removed t-meta awaiting review
27508 chrisflav feat(RingTheory): height under ring homomorphism t-ring-theory large-import awaiting review
27821 BGuillemet feat(CategoryTheory/Sites/Sheaf): functorial version of Sheaf.homEquiv new-contributor t-category-theory awaiting review
29565 joelriou feat(CategoryTheory): dense functors t-category-theory awaiting review
31149 riccardobrasca feat: power series over a noetherian ring is noetherian t-ring-theory maintainer-merge awaiting review
31198 YaelDillies feat(Algebra): characterise when a quotient is nontrivial CFT large-import t-algebra awaiting review
31235 CoolRmal feat (Topology): IsCompletelyPseudoMetrizable t-topology awaiting review
31237 euprunin chore(Logic/Equiv): golf entire `Perm.subtypeCongr.symm` using `rfl` t-logic awaiting review
31286 bryangingechen ci: make new contributor labeling work for users with a private profile CI awaiting review
31363 euprunin chore(LinearAlgebra/AffineSpace): golf entire `attach_affineCombination_of_injective` using `simp` t-algebra awaiting review
31438 b-mehta chore(Order/UnorderedInterval): add basic uIoo lemmas t-order awaiting review
31453 kim-em feat: locally contractible spaces t-topology awaiting review
31465 bryangingechen ci: Notify Zulip on update dependencies workflow failure CI awaiting review
31458 bwangpj feat: Subgroup.mem_sup for arbitrary groups when one of the subgroups is normal t-algebra awaiting review
31470 ADedecker feat: define test functions in the sense of distribution theory t-analysis awaiting review
31471 Scarlett-le feat(LinearAlgebra/AffineSpace): add commutativity lemmas for line parallelism new-contributor t-algebra awaiting review
31475 YaelDillies feat: a pullback of schemes is canonically over the second component t-algebraic-geometry awaiting review
31490 themathqueen chore(Algebra): move `QuadraticAlgebra` to `QuadraticAlgebra/Defs` file-removed t-algebra awaiting review
31384 harahu doc(Archive): ensure only a single H1 header per file IMO maintainer-merge awaiting review
31604 maksym-radziwill feat: analyticity of dslope t-analysis awaiting-author awaiting author
26770 Jun2M feat(Combinatorics/Graph) : subgraph relations on `Graph` t-combinatorics awaiting review
31159 gasparattila feat(Topology/Sets): add `Compacts.toCloseds` t-topology awaiting review
30524 mcdoll feat: Basics of Montel spaces t-analysis awaiting review
29283 Jlh18 feat(CategoryTheory): define forgetful-core adjunction between Cat and Grpd new-contributor t-category-theory awaiting review
29279 Jlh18 feat: free groupoid on a category, free-forgetful adjunction large-import new-contributor t-category-theory awaiting-author failing CI
31613 xyzw12345 feat(RepresentationTheory/GroupCohomology): Non-abelian Group Cohomology large-import t-algebra WIP labelled WIP
31392 YaelDillies feat: compute the PMF of a product measure t-measure-probability awaiting-author awaiting author
28026 kim-em feat: grind annotations for `Disjoint` awaiting-author ⚠️ failing CI
31074 mcdoll feat(Analysis/Normed): extend densely defined LinearMaps to CLM t-analysis 🟤 running CI
31614 qawbecrdtey chore(Control/Fix): remove redundant import t-data easy 🟤 running CI
31606 euprunin chore(Data/PNat): deprecate `gcd_eq_left` t-data awaiting review
31615 euprunin chore(Data/DFinsupp): golf `Data.DFinsupp.Defs` using `grind` and `simp` t-data 🟤 running CI
31307 euprunin chore: golf using the combination `ext` and `grind` awaiting-author awaiting author
14426 adomani dev: `#min_imps` command merge-conflict WIP labelled WIP
14167 alreadydone feat: Group scheme structure on Weierstrass curve workshop-AIM-AG-2024 t-algebraic-geometry merge-conflict WIP labelled WIP
13847 alreadydone feat(EllipticCurve): the universal elliptic curve t-algebra t-algebraic-geometry merge-conflict awaiting-author merge conflict
13297 urkud feat(Semicontinuous): add `comp` lemma t-order t-topology merge-conflict awaiting-author merge conflict
12679 MichaelStollBayreuth perf(NumberTheory/RamificationInertia): speed up slow file merge-conflict WIP labelled WIP
12934 grunweg chore: replace more uses of > or ≥ by < or ≤ merge-conflict awaiting-author help-wanted looking for help
12608 eric-wieser feat: allow `nsmul` / `zsmul` to be omitted again, with a warning t-algebra t-meta merge-conflict awaiting-author merge conflict
12936 mattrobball chore(Quiver.Opposite): make `Quiver.Hom.op/unop` `abbrev`'s merge-conflict merge conflict
12933 grunweg chore: replace some use of > or ≥ by < or ≤ merge-conflict awaiting-author failing CI
11617 urkud refactor(Finset): redefine Finset.diag, review API t-logic merge-conflict awaiting-author merge conflict
12192 Ruben-VandeVelde feat: generalize isLittleO_const_id_atTop/atBot t-analysis merge-conflict awaiting-author merge conflict
10024 ADedecker feat: rename `connectedComponentOfOne` to `identityComponent`, prove that it is normal and open t-topology awaiting-CI merge-conflict does not pass CI
11100 eric-wieser feat(CategoryTheory/Limits): add `Functor.mapBinaryBiconeInv` t-category-theory awaiting-CI merge-conflict does not pass CI
10521 eric-wieser chore: generalize `IsBoundedLinearMap` to modules t-analysis merge-conflict awaiting-author merge conflict
10594 lecopivo feat: `fun_trans` function transformation tactic e.g. for computing derivatives t-meta merge-conflict WIP labelled WIP
10721 urkud feat(Order/FunLike): define `PointwiseLE` t-logic t-order merge-conflict ??? missing CI information
8503 thorimur feat: meta utils for `refine?` t-meta merge-conflict awaiting-author merge conflict
9354 chenyili0818 feat: monotonicity of gradient on convex real-valued functions t-analysis merge-conflict awaiting-author merge conflict
8961 eric-wieser refactor: use the coinduced topology on ULift awaiting-CI merge-conflict please-adopt awaiting-author looking for help
9487 eric-wieser feat: the exponential of dual numbers over non-commutative rings t-measure-probability t-algebra t-analysis merge-conflict WIP labelled WIP
8788 FMLJohn feat(Algebra/Module/GradeZeroModule): if `A` is a graded semiring and `M` is a graded `A`-module, then each grade of `M` is a module over the 0-th grade of `A`. t-algebra merge-conflict merge conflict
8906 jjaassoonn feat: add some missing lemmas about linear algebra t-algebra merge-conflict awaiting-author failing CI
9146 laughinggas feat(Data/ZMod/Defs): Topological structure on `ZMod` t-algebra t-topology merge-conflict awaiting-author merge conflict
8658 eric-wieser feat: support right actions for `Con` t-algebra merge-conflict awaiting-author merge conflict
8616 eric-wieser feat(Algebra/FreeAlgebra): add right action and `IsCentralScalar` t-algebra awaiting-CI merge-conflict does not pass CI
9356 alexjbest feat: assumption? t-meta merge-conflict awaiting-author merge conflict
8519 eric-wieser refactor(LinearAlgebra/TensorProduct): golf using `liftAddHom` t-algebra merge-conflict awaiting-author merge conflict
9229 eric-wieser refactor(Algebra/GradedMonoid): Use `HMul` to define `GMul` t-algebra merge-conflict WIP labelled WIP
9570 eric-wieser feat(Algebra/Star): Non-commutative generalization of `StarModule` t-algebra awaiting-CI merge-conflict WIP labelled WIP
9564 AntoineChambert-Loir weaken commutativity assumptions for AdjoinRoot.lift and AdjoinRoot.liftHom t-algebra merge-conflict WIP labelled WIP
9642 eric-wieser refactor(Analysis/Normed/{Group/Field}/Basic): Let `extends` generate the repeated fields t-analysis merge-conflict awaiting-author WIP help-wanted looking for help
7427 MohanadAhmed Mohanad ahmed/sort eigenvalues abs merge-conflict WIP labelled WIP
7227 kmill feat: flexible binders and integration into notation3 t-meta merge-conflict WIP labelled WIP
7835 shuxuezhuyi feat(LinearAlgebra/Matrix): `lift` for projective special linear group t-algebra merge-conflict awaiting-author ??? missing CI information
6630 MohanadAhmed feat: Reduced Spectral Theorem t-algebra merge-conflict WIP labelled WIP
6580 adomani chore: `move_add`-driven replacements merge-conflict awaiting-author merge conflict
6931 urkud refactor(Analysis/Normed*): use `RingHomIsometric` for `*.norm_cast` t-analysis merge-conflict help-wanted ??? looking for help
7713 RemyDegenne feat: add_left/right_inj for measures t-measure-probability merge-conflict awaiting-author merge conflict
7909 mcdoll fix(Tactic/Continuity): remove npowRec and add new tag for Continuous.pow t-topology t-meta merge-conflict WIP labelled WIP
7962 eric-wieser feat: `DualNumber (Quaternion R)` as a `CliffordAlgebra` t-algebra merge-conflict WIP labelled WIP
6791 eric-wieser refactor: Use flat structures for morphisms awaiting-CI merge-conflict awaiting-author help-wanted looking for help
7875 astrainfinita chore: make `SMulCommClass A A B` and `SMulCommClass A B B` higher priority slow-typeclass-synthesis t-algebra merge-conflict ??? missing CI information
6777 adomani chore(Co*variantClass): replace eta-expanded (· * ·), (· + ·), (· ≤ ·), (· < ·) merge-conflict merge conflict
7932 eric-wieser refactor(Algebra/TrivSqZeroExt): replace with a structure t-algebra awaiting-CI merge-conflict does not pass CI
7601 digama0 feat: ring hom support in `ring` t-algebra t-meta merge-conflict awaiting-author merge conflict
7467 ADedecker feat: spectrum of X →ᵇ ℂ is StoneCech X t-analysis merge-conflict WIP labelled WIP
7615 eric-wieser chore(LinearAlgebra/Basic): generalize compatibleMaps to semilinear maps t-algebra awaiting-CI easy merge-conflict does not pass CI
6930 kmill feat: `resynth_instances` tactic for resynthesizing instances in the goal or local context t-meta merge-conflict WIP labelled WIP
7351 shuxuezhuyi feat(Topology/Algebra/Order): extend function on `Ioo` to `Icc` t-order merge-conflict awaiting-author merge conflict
6210 MohanadAhmed feat(Data/IsROrC/Basic): add a `StarOrderedRing` instance t-algebra t-analysis merge-conflict WIP labelled WIP
6268 eric-wieser Fixups to #3838 merge-conflict WIP labelled WIP
4127 kmill refactor: create HasAdj class, define Digraph, and generalize some SimpleGraph API t-combinatorics merge-conflict awaiting-author merge conflict
5133 kmill feat: IntermediateField adjoin syntax for sets of elements t-algebra merge-conflict WIP labelled WIP
6328 astrainfinita chore: make some instance about `Sub...Class` lower priority t-algebra awaiting-CI merge-conflict WIP labelled WIP
6491 eric-wieser chore(Mathlib/Algebra/Hom/GroupAction): add `SMulHomClass.comp_smul` t-algebra merge-conflict merge conflict
6633 adomani feat(..Polynomial..): `MvPolynomial`s have no zero divisors t-algebra merge-conflict awaiting-author merge conflict
7076 grunweg feat: define measure zero subsets of a manifold t-measure-probability t-differential-geometry merge-conflict WIP labelled WIP
6993 jjaassoonn feat : lemmas about `AddMonoidAlgebra.{divOf, modOf}` t-algebra merge-conflict merge conflict
6403 astrainfinita chore: change instance priorities of `Ordered*` hierarchy slow-typeclass-synthesis t-order t-algebra merge-conflict awaiting-author merge conflict
6330 astrainfinita chore: make some instance about `Sub...Class` higher priority than `Sub...` slow-typeclass-synthesis t-algebra merge-conflict WIP labelled WIP
3808 kim-em feat: #formalize, backed by a choice of LLMs t-meta merge-conflict awaiting-author merge conflict
4871 j-loreaux feat: define the additive submonoid of positive elements in a star ordered ring t-algebra awaiting-CI merge-conflict ??? does not pass CI
6002 slerpyyy feat(Analysis.SpecialFunctions.Gaussian): add `integrable_fun_mul_exp_neg_mul_sq` t-analysis merge-conflict awaiting-author merge conflict
6195 eric-wieser chore(RingTheory/TensorProduct): golf the `mul` definition t-algebra awaiting-CI merge-conflict does not pass CI
5912 ADedecker feat(Analysis.Distribution.ContDiffMapSupportedIn): space of smooth maps with support in a fixed compact t-analysis merge-conflict WIP labelled WIP
5934 eric-wieser feat: port Data.Rat.MetaDefs t-meta merge-conflict mathlib-port help-wanted looking for help
6079 eric-wieser fix: deduplicate variables awaiting-CI merge-conflict does not pass CI
4960 eric-wieser chore: use `open scoped` awaiting-CI merge-conflict does not pass CI
3757 thorimur feat: config options for `fail_if_no_progress` t-meta merge-conflict WIP labelled WIP
12353 thorimur feat: `conv%` t-meta merge-conflict WIP labelled WIP
7903 urkud feat: define `UnboundedSpace` t-topology merge-conflict help-wanted looking for help
15400 grunweg feat: "confusing variables" linter t-linter merge-conflict WIP labelled WIP
14654 grunweg feat(runLinter): allow only running certain linters t-linter RFC merge-conflict failing CI
15679 adomani test: refactor in CI merge-conflict WIP labelled WIP
10629 madvorak feat: List.cons_sublist_append_iff_right t-data merge-conflict merge conflict
9973 Ruben-VandeVelde feat: polynomials formed by lists t-data merge-conflict please-adopt looking for help
12926 joelriou feat(CategoryTheory): the monoidal category structure induced by a monoidal functor t-category-theory merge-conflict WIP labelled WIP
12869 adomani feat: linter and script for `theorem` vs `lemma` t-linter merge-conflict awaiting-author merge conflict
12093 ADedecker feat: tweak the definition of semicontinuity to behave better in nonlinear orders t-topology merge-conflict WIP labelled WIP
11393 mcdoll feat(Analysis/Distribution/SchwartzSpace): The Heine-Borel property t-analysis merge-conflict WIP labelled WIP
9444 erdOne feat: Various instances regarding `𝓞 K`. t-number-theory merge-conflict help-wanted looking for help
8931 hmonroe feat(Computable): define P, NP, and NP-complete t-computability merge-conflict awaiting-author failing CI
8608 eric-wieser feat: multiplicativize `AddTorsor` t-algebra merge-conflict WIP labelled WIP
6603 tydeu feat: automatically try `cache get` before build CI merge-conflict WIP labelled WIP
6058 apurvnakade feat: duality theory for cone programs t-analysis merge-conflict WIP labelled WIP
6449 ADedecker feat: functions with finite fibers t-topology merge-conflict awaiting-author failing CI
13791 digama0 refactor: Primrec and Partrec tech debt t-computability merge-conflict merge conflict
11964 adamtopaz feat: The functor of points of a scheme t-algebraic-geometry t-category-theory merge-conflict merge conflict
12418 rosborn style: replace preimage_val with ↓∩ notation merge-conflict merge conflict
9978 astrainfinita chore(FieldTheory/KummerExtension): move some lemmas earlier t-algebra merge-conflict awaiting-author merge conflict
12429 adomani feat: toND -- auto-generating natDegree t-algebra RFC t-meta merge-conflict awaiting-author merge conflict
12751 Command-Master feat: add lemmas for Nat/Bits, Nat/Bitwise and Nat/Size t-data new-contributor merge-conflict merge conflict
15448 urkud chore(*): deprecate `Option.elim'` tech debt merge-conflict awaiting-author ??? missing CI information
10349 Shamrock-Frost refactor(CategoryTheory/MorphismProperty) t-category-theory merge-conflict failing CI
10350 Shamrock-Frost feat(Data/Setoid): add the operations of taking the equivalence class of an element and of saturating a set wrt an equivalence relation t-data merge-conflict ??? missing CI information
13573 Shamrock-Frost feat: add multivariate polynomial modules t-algebra merge-conflict awaiting-author merge conflict
6517 MohanadAhmed feat: discrete Fourier transform of a finite sequence t-algebra merge-conflict awaiting-author merge conflict
13155 alreadydone feat(NumberTheory/EllipticDivisibilitySequence): show elliptic relations follow from even-odd recursion t-algebra t-number-theory merge-conflict awaiting-author merge conflict
15600 adomani feat: lint also `let` vs `have` t-linter merge-conflict WIP labelled WIP
14038 adomani test/decl diff in lean dev merge-conflict WIP labelled WIP
7545 shuxuezhuyi feat: APIs of `Function.extend f g e'` when `f` is injective t-logic merge-conflict awaiting-author merge conflict
14078 Ruben-VandeVelde feat(CI): continue after mk_all fails CI merge-conflict awaiting-author failing CI
11800 JADekker feat : Define KappaLindelöf spaces awaiting-zulip t-topology merge-conflict please-adopt looking for help
11283 hmonroe feat(ModelTheory/Satisfiability): define theory with independent sentence t-logic merge-conflict WIP labelled WIP
16914 siddhartha-gadgil Loogle syntax with non-reserved merge-conflict WIP labelled WIP
10991 thorimur feat: `tfae` block tactic t-meta merge-conflict modifies-tactic-syntax WIP labelled WIP
16464 Parcly-Taxel chore: deprecate `Nat.(case_)strong_induction_on` tech debt merge-conflict merge conflict
8118 iwilare feat(CategoryTheory): add dinatural transformations t-category-theory merge-conflict awaiting-author merge conflict
7516 ADedecker perf: use `abbrev` to prevent unifying useless data merge-conflict WIP labelled WIP
17127 astrainfinita chore: remove global `Quotient.mk` `⟦·⟧` notation t-data merge-conflict merge conflict
14712 astrainfinita perf: change instance priority and order about `OfNat` slow-typeclass-synthesis t-algebra merge-conflict delegated merge conflict
11500 mcdoll refactor(Topology/Algebra/Module/WeakDual): Clean up t-topology merge-conflict awaiting-author merge conflict
5995 astrainfinita feat: add APIs about `Quotient.choice` t-data RFC merge-conflict awaiting-author merge conflict
8029 alreadydone refactor: Homotopy between Functions not ContinuousMaps t-topology RFC merge-conflict merge conflict
13156 erdOne refactor(Algebra/Module/LocalizedModule): Redefine `LocalizedModule` in terms of `OreLocalization`. t-algebra merge-conflict failing CI
16348 urkud refactor(Topology): require `LinearOrder` with `OrderTopology` t-order t-topology merge-conflict awaiting-author merge conflict
16925 YnirPaz feat(SetTheory/Cardinal/Cofinality): aleph index of singular cardinal has infinite cofinality t-set-theory merge-conflict WIP labelled WIP
9605 davikrehalt feat(Data/Finset & List): Add Lemmas for Sorting and Filtering t-data new-contributor merge-conflict please-adopt awaiting-author looking for help
9654 urkud feat: add `@[mk_eq]` version of `@[mk_iff]` t-meta merge-conflict awaiting-author merge conflict
16704 AntoineChambert-Loir feat(Mathlib.Data.Ordering.Dickson): Dickson orders t-order merge-conflict WIP labelled WIP
16355 Ruben-VandeVelde feat: odd_{add,sub}_one t-algebra t-number-theory merge-conflict awaiting-author merge conflict
8479 alexjbest feat: use leaff in CI merge-conflict awaiting-author WIP ⚠️ labelled WIP
14598 Command-Master chore: add typeclasses to unify various `add_top`, `add_eq_top`, etc. new-contributor t-order t-algebra merge-conflict merge conflict
12778 MichaelStollBayreuth perf: decouple algebraic and order hierarchies in type class search slow-typeclass-synthesis t-order t-algebra merge-conflict merge conflict
16885 metinersin feat(ModelTheory/Complexity): define literals new-contributor t-logic merge-conflict awaiting-author merge conflict
9341 winstonyin feat: Naturality of integral curves t-differential-geometry merge-conflict awaiting-author merge conflict
13248 hcWang942 feat: basic concepts of auction theory new-contributor t-logic merge-conflict awaiting-author merge conflict
9344 erdOne feat: Add `AddGroup.FG` -> `Module.Finite ℤ` as instances t-algebra merge-conflict awaiting-author merge conflict
12133 ADedecker feat: generalize instIsLowerProd to arbitrary products t-order t-topology merge-conflict awaiting-author merge conflict
16637 astrainfinita perf: reorder `extends` of `(Add)Monoid` t-algebra merge-conflict WIP labelled WIP
14739 urkud feat(Measure): add `gcongr` lemmas t-measure-probability merge-conflict awaiting-author WIP help-wanted looking for help
8661 joelriou feat(CategoryTheory/Sites): descent of sheaves t-category-theory merge-conflict WIP labelled WIP
10476 shuxuezhuyi feat(Topology/UniformSpace): define uniform preordered space t-topology merge-conflict awaiting-author merge conflict
17623 astrainfinita feat(Algebra/Order/GroupWithZero/Unbundled): add some lemmas awaiting-zulip t-order t-algebra merge-conflict awaiting a zulip discussion
17513 astrainfinita perf: do not search algebraic hierarchies when using `map_*` lemmas awaiting-bench t-algebra merge-conflict WIP labelled WIP
19212 Julian feat(LinearAlgebra): add a variable_alias for VectorSpace t-algebra merge-conflict merge conflict
19337 zeramorphic feat(Data/Finsupp): generalise `Finsupp` to any "zero" value t-data merge-conflict merge conflict
10332 adri326 feat(Topology/Sets): define regular open sets and their boolean algebra t-topology merge-conflict WIP labelled WIP
14501 jjaassoonn feat: module structure of filtered colimit of abelian groups over filtered colimit of rings workshop-AIM-AG-2024 t-algebra t-category-theory merge-conflict awaiting-author merge conflict
18756 astrainfinita refactor: deprecate `DistribMulActionSemiHomClass` `MulSemiringActionSemiHomClass` t-algebra merge-conflict merge conflict
17071 ScottCarnahan feat : (LinearAlgebra/RootSystem) : Separation, base, cartanMatrix t-algebra merge-conflict WIP labelled WIP
19125 yhtq feat: add theorems to transfer `IsGalois` between pairs of fraction rings new-contributor t-algebra merge-conflict failing CI
18841 hrmacbeth chore: change some `linarith`s to `linear_combination`s merge-conflict WIP labelled WIP
18748 astrainfinita refactor: deprecate `ContinuousLinearMapClass` t-algebra t-topology merge-conflict merge conflict
11142 hmonroe feat(ProofTheory): Define logical symbols abstractly; opens new top-level section, drawing from lean4-logic t-logic merge-conflict awaiting-author merge conflict
11210 hmonroe Test commit merge-conflict WIP labelled WIP
15773 kkytola feat: Add type class for ENat-valued floor functions t-order merge-conflict awaiting-author merge conflict
3251 kmill feat: deriving `LinearOrder` for simple enough inductive types t-meta merge-conflict awaiting-author WIP labelled WIP
3610 TimothyGu feat: derive Infinite automatically for inductive types t-meta merge-conflict awaiting-author merge conflict
16120 awainverse feat(ModelTheory/Algebra/Ring/Basic): Ring homomorphisms are a `StrongHomClass` for the language of rings t-logic t-algebra RFC merge-conflict failing CI
20527 trivial1711 refactor(Topology/UniformSpace/Completion): more descriptive names for `α → Completion α` t-topology merge-conflict merge conflict
17739 Aaron1011 feat(Topology/Order/DenselyOrdered): prove Not (IsOpen) for intervals new-contributor t-topology merge-conflict awaiting-author merge conflict
18474 astrainfinita perf: lower the priority of `*WithOne.to*` instances t-data slow-typeclass-synthesis t-algebra merge-conflict merge conflict
20656 Komyyy feat(Mathlib/Geometry/Manifold/VectorBundle/Sphere): convert orthogonal smooth `M → 𝕊ⁿ` & `M → ℝⁿ⁺¹` to smooth `M → T𝕊ⁿ` t-differential-geometry merge-conflict please-adopt looking for help
15711 znssong feat(Combinatorics/SimpleGraph): Some lemmas about walk, cycle and Hamiltonian cycle new-contributor t-combinatorics merge-conflict awaiting-author merge conflict
18629 tomaz1502 feat(Computability.Timed): Formalization of runtime complexity of List.merge t-computability new-contributor merge-conflict awaiting-author merge conflict
8362 urkud feat(Asymptotics): define `ReflectsGrowth` t-analysis merge-conflict awaiting-author failing CI
6692 prakol16 feat: disjoint indexed union of local homeomorphisms t-topology merge-conflict awaiting-author failing CI
19291 PieterCuijpers feat(Algebra/Order/Hom): add quantale homomorphism new-contributor t-algebra merge-conflict awaiting-author failing CI
19352 hrmacbeth chore: change some `nlinarith`s to `linear_combination`s merge-conflict WIP labelled WIP
20372 jvlmdr feat(MeasureTheory/Function): Add ContinuousLinearMap.bilinearCompLp(L) new-contributor t-measure-probability merge-conflict merge conflict
17176 arulandu feat: integrals and integrability with .re new-contributor t-measure-probability merge-conflict awaiting-author merge conflict
20872 grunweg feat: lint against the tactic.skipAssignedInstances option in mathlib tech debt t-linter merge-conflict awaiting-author merge conflict
2605 eric-wieser chore: better error message in linarith t-meta merge-conflict awaiting-author merge conflict
11837 trivial1711 feat: completion of a uniform multiplicative group t-algebra t-topology merge-conflict WIP help-wanted looking for help
14686 smorel394 feat (AlgebraicGeometry/Grassmannian): define the Grassmannian scheme workshop-AIM-AG-2024 t-algebraic-geometry merge-conflict please-adopt WIP looking for help
9449 hmonroe feat: Add Turing machine with the quintet definition (TMQ) and a chainable step function for each TM type t-computability merge-conflict awaiting-author failing CI
20663 EtienneC30 feat: `PFunLike` typeclass for partial homomorphisms and `LinearPMapClass` t-data t-algebra merge-conflict WIP labelled WIP
19697 quangvdao feat(BigOperators/Fin): Sum/product over `Fin` intervals t-data merge-conflict awaiting-author failing CI
19353 hrmacbeth chore: golf some term/rw proofs using `linear_combination` merge-conflict WIP labelled WIP
10678 adri326 feat(Topology/UniformSpace): prove that a uniform space is completely regular t-topology merge-conflict awaiting-author merge conflict
18785 erdOne feat(CategoryTheory): command that generates instances for `MorphismProperty` t-category-theory t-meta merge-conflict awaiting-author merge conflict
15942 grunweg chore: move style linters into their own file; document all current linters t-linter merge-conflict awaiting-author merge conflict
16311 madvorak feat(Computability): regular languages are context-free t-computability merge-conflict WIP labelled WIP
19943 AlexLoitzl feat(Computability): Add Chomsky Normal Form Grammar and translation t-computability new-contributor merge-conflict awaiting-author merge conflict
17005 YnirPaz feat(SetTheory/Cardinal/Regular): define singular cardinals t-set-theory merge-conflict WIP labelled WIP
12054 adomani feat: auto-bugs t-meta merge-conflict awaiting-author merge conflict
5062 adomani feat(Tactic/Prune + test/Prune): add `prune` tactic, for removing unnecessary hypotheses t-meta merge-conflict modifies-tactic-syntax awaiting-author merge conflict
21433 grunweg chore: change more lemmas to be about enorm instead of nnnorm carleson t-measure-probability merge-conflict awaiting-author merge conflict
21099 chrisflav chore(RingTheory/Generators): use unification hints for variables and relations t-algebra merge-conflict merge conflict
21269 658060 (WIP) feat (CategoryTheory/Topos): Add topos theory content new-contributor t-category-theory merge-conflict awaiting-author WIP labelled WIP
12394 JADekker feat : define pre-tight and tight measures t-measure-probability merge-conflict please-adopt awaiting-author looking for help
20454 urkud chore(TangentCone): review names t-analysis merge-conflict failing CI
16550 awainverse feat(ModelTheory): A typeclass for languages expanding other languages t-logic merge-conflict awaiting-author merge conflict
13686 fpvandoorn feat: some finset lemmas t-data merge-conflict awaiting-author merge conflict
14313 grhkm21 feat(RepresentationTheory/FdRep): FdRep is a full subcategory of Rep new-contributor t-algebra t-category-theory merge-conflict failing CI
18626 hannahfechtner feat : define Artin braid groups new-contributor t-algebra merge-conflict awaiting-author merge conflict
10823 alexkeizer feat: convert curried type functions into uncurried type functions t-data merge-conflict awaiting-author merge conflict
13648 urkud feat(Topology/Module): generalize `ContinuousLinearMap.compSL` t-algebra t-analysis t-topology merge-conflict awaiting-author failing CI
21959 BGuillemet feat(Topology/ContinuousMap): Stone-Weierstrass theorem for MvPolynomial new-contributor t-topology merge-conflict merge conflict
20750 adomani feat: the envLinter syntax linter large-import t-linter merge-conflict failing CI
18470 astrainfinita perf: lower the priority of `Normed*.to*` instances slow-typeclass-synthesis t-algebra t-analysis merge-conflict ❌? infrastructure-related CI failing
16944 YnirPaz feat(SetTheory/Cardinal/Cofinality): lemmas about limit ordinals and cofinality t-set-theory merge-conflict WIP labelled WIP
17368 Felix-Weilacher feat(Topology/Baire/BaireMeasurable): add the Kuratowski-Ulam theorem t-topology merge-conflict failing CI
8767 eric-wieser refactor(Cache): tidy lake-manifest parsing in Cache t-meta merge-conflict failing CI
15578 znssong feat(Function): Fixed points of function `f` with `f(x) >= x` new-contributor t-analysis merge-conflict awaiting-author merge conflict
22805 ScottCarnahan feat (FieldTheory/Finite): fixed points of frobenius t-algebra merge-conflict WIP labelled WIP
22660 Ruben-VandeVelde chore: follow naming convention around Group.IsNilpotent t-algebra merge-conflict merge conflict
13999 adomani feat: a linter to flag potential confusing conventions t-linter merge-conflict awaiting-author merge conflict
19013 quangvdao feat(Algebra/BigOperators/Fin): Add `finSigmaFinEquiv` t-algebra merge-conflict awaiting-author merge conflict
19189 YnirPaz feat(SetTheory/Ordinal/Arithmetic): order isomorphism between omega and the natural numbers t-set-theory merge-conflict awaiting-author merge conflict
19227 adomani fix(CI): unwrap `lake test` in problem matcher CI merge-conflict awaiting-author merge conflict
20874 grunweg chore(nolint.yml): use shallow clones CI merge-conflict awaiting-author merge conflict
15774 kkytola feat: Topology on `ENat` t-order t-topology merge-conflict WIP labelled WIP
18284 chrisflav feat(AlgebraicGeometry): relative gluing of schemes t-algebraic-geometry merge-conflict WIP labelled WIP
20613 grunweg chore: golf using `List.toArrayMap` large-import merge-conflict failing CI
22682 grunweg chore(Topology/Homeomorph): split out various constructions tech debt t-topology RFC merge-conflict failing CI
21018 markimunro feat(Data/Matrix): add file with key definitions and theorems about elementary row operations t-data new-contributor merge-conflict awaiting-author enhancement failing CI
23514 eric-wieser refactor: smooth over Lattice/LinearOrder inheritance merge-conflict failing CI
22810 pechersky feat(Counterexamples): metric space not induced by norm t-analysis t-topology merge-conflict WIP labelled WIP
13124 astrainfinita chore: remove `CovariantClass` and `ContravariantClass` merge-conflict WIP labelled WIP
20401 RemyDegenne feat: add sigmaFinite_iUnion t-measure-probability merge-conflict awaiting-author merge conflict
19275 eric-wieser fix: if nolint files change, do a full rebuild merge-conflict delegated failing CI
12251 ScottCarnahan refactor(RingTheory/HahnSeries) : several generalizations t-order t-algebra merge-conflict WIP labelled WIP
22727 grunweg feat: rewrite the isolated by and colon linters in Lean t-linter merge-conflict awaiting-author merge conflict
15212 victorliu5296 feat: Add fundamental theorem of calculus-2 for Banach spaces new-contributor t-measure-probability t-analysis merge-conflict awaiting-author merge conflict
22701 ctchou feat(Combinatorics): the Katona circle method new-contributor t-combinatorics merge-conflict merge conflict
23786 grunweg Mr librarynote def 2b large-import merge-conflict WIP labelled WIP
23411 PatrickMassot chore: remove finiteness from Order.Filter.Lift longest-pole t-topology merge-conflict merge conflict
22579 kvanvels doc(Topology/Defs/Induced): fix comments on three functions related to RestrictGenTopology t-topology merge-conflict awaiting-author documentation merge conflict
21488 imbrem feat(CategoryTheory/Monoidal): premonoidal categories new-contributor t-category-theory merge-conflict merge conflict
21525 sinhp feat(CategoryTheory): Locally Cartesian Closed Categories (Prelim) large-import t-category-theory merge-conflict merge conflict
19425 hrmacbeth perf: gcongr forward-reasoning adjustment merge-conflict awaiting-author merge conflict
20873 vbeffara feat(Topology/Covering): path lifting and homotopy lifting new-contributor t-topology merge-conflict awaiting-author failing CI
22817 peabrainiac feat(CategoryTheory/Sites): local sites t-category-theory merge-conflict WIP labelled WIP
6252 michaellee94 feat(Geometry/Manifolds/Instances/Homeomorph): Homeomorphism maps `C^k` manifolds to `C^k` manifolds t-differential-geometry merge-conflict WIP labelled WIP
16314 astrainfinita chore(Data/Quot): deprecate `ind*'` APIs t-data merge-conflict merge conflict
23509 eric-wieser refactor: Make ENNReal an abbrev t-data merge-conflict failing CI
11455 adomani fix: unsqueeze simp, re Yaël's comments on #11259 merge-conflict awaiting-author merge conflict
7325 eric-wieser chore: use preimageIso instead of defeq abuse for InducedCategory t-category-theory awaiting-CI merge-conflict does not pass CI
7874 astrainfinita chore: make `IsScalarTower A A B` and `IsScalarTower A B B` higher priority slow-typeclass-synthesis t-algebra awaiting-CI merge-conflict ??? does not pass CI
5952 eric-wieser feat: add Qq wrappers for ToExpr awaiting-CI t-meta merge-conflict does not pass CI
15483 astrainfinita chore(GroupTheory/Coset): reduce defeq abuse t-algebra merge-conflict merge conflict
16594 astrainfinita perf: reorder `extends` and remove some instances in algebra hierarchy slow-typeclass-synthesis t-algebra merge-conflict failing CI
20567 grunweg feat(Cache): two small features t-meta merge-conflict merge conflict
20313 thefundamentaltheor3m feat(Data/Complex/Exponential): prove some useful results about the complex exponential. new-contributor t-analysis merge-conflict failing CI
22698 Kiolt feat: notation for whisker(Left/Right)Iso toric t-category-theory merge-conflict failing CI
20730 kuotsanhsu feat(LinearAlgebra/Matrix/SchurTriangulation): prove Schur decomposition/triangulation new-contributor t-algebra merge-conflict awaiting-author failing CI
19117 eric-wieser feat: derivatives of matrix operations t-analysis merge-conflict WIP labelled WIP
12605 astrainfinita chore: attribute [induction_eliminator] merge-conflict awaiting-author merge conflict
15099 joelriou feat(CategoryTheory/Sites): the Mayer-Vietoris long exact sequence in sheaf cohomology t-category-theory merge-conflict WIP labelled WIP
23859 urkud feat(Topology/../Order/Field): generalize to `Semifield` t-topology merge-conflict merge conflict
23810 b-reinke chore(Order/Interval): generalize succ/pred lemmas to partial orders t-order merge-conflict merge conflict
24285 madvorak chore(Algebra/*-{Category,Homology}): remove unnecessary universe variables t-algebra merge-conflict merge conflict
8370 eric-wieser refactor(Analysis/NormedSpace/Exponential): remove the `𝕂` argument from `exp` awaiting-zulip t-analysis merge-conflict failing CI
22583 imathwy feat: affinespace homeomorphism t-algebra merge-conflict awaiting-author failing CI
24322 mattrobball chore: merge repeated `Type*` binders merge-conflict awaiting-author failing CI
23593 erdOne feat(AlgebraicGeometry): the tilde construction is functorial t-algebraic-geometry merge-conflict awaiting-author merge conflict
21065 eric-wieser feat: generalize `tangentConeAt.lim_zero` to TVS t-analysis merge-conflict WIP labelled WIP
22721 grunweg chore(MeasureTheory/Function/LpSeminorm/Basic): generalise more results to enorm classes carleson t-measure-probability merge-conflict WIP labelled WIP
24354 grunweg chore(HasFiniteIntegral): rename three lemmas t-measure-probability merge-conflict merge conflict
14731 adomani feat: the repeated typeclass assumption linter large-import t-linter merge-conflict WIP labelled WIP
13649 astrainfinita chore: redefine `Nat.div2` `Nat.bodd` merge-conflict merge conflict
19520 erdOne refactor(Algebra/Module): Redefine `LocalizedModule` in terms of `OreLocalization` t-algebra merge-conflict failing CI
14675 adomani dev: the repeated variable linter t-linter merge-conflict WIP labelled WIP
14330 Ruben-VandeVelde chore: split Mathlib.Algebra.Star.Basic merge-conflict awaiting-author merge conflict
14023 mattrobball perf(RingTheory.OreLocalization): make data irreducible merge-conflict ??? missing CI information
8511 eric-wieser refactor(MeasureTheory/Measure/Haar/Basic): partially generalize to the affine case t-measure-probability merge-conflict awaiting-author merge conflict
7994 ericrbg chore: generalize `LieSubalgebra.mem_map_submodule` t-algebra merge-conflict please-adopt looking for help
6317 eric-wieser refactor(Data/Finsupp/Defs): make Finsupp.single defeq to Pi.single t-data merge-conflict WIP labelled WIP
4979 mhk119 doc(Data/Nat/Bitblast): initial commit t-data merge-conflict merge conflict
11524 mcdoll refactor: Introduce type-class for SchwartzMap t-analysis merge-conflict WIP labelled WIP
22269 Thmoas-Guan chore(Algebra): replace Submodule.quotient.mk with Submodule.mkQ t-algebra merge-conflict awaiting-author merge conflict
23546 JovanGerb feat(LinearAlgebra/AffineSpace/AffineSubspace): rename `AffineSubspace.mk'` to `Submodule.shift` t-euclidean-geometry merge-conflict merge conflict
19315 quangvdao feat(Data/Finsupp/Fin): Add `Finsupp` operations on `Fin` tuple t-data merge-conflict awaiting-author merge conflict
7907 urkud feat: introduce `NthRoot` notation class t-algebra t-analysis awaiting-CI merge-conflict does not pass CI
24642 grunweg WIP-feat: add layercake formula for ENNReal-valued functions carleson t-analysis merge-conflict WIP labelled WIP
21712 grunweg chore: generalise more lemmas to `ContinuousENorm` carleson t-measure-probability awaiting-CI merge-conflict does not pass CI
21375 grunweg WIP: generalise lemmas to ENorm carleson t-measure-probability awaiting-CI merge-conflict WIP labelled WIP
15115 kkytola feat: Generalize assumptions in liminf and limsup results in ENNReals t-order t-topology merge-conflict awaiting-author help-wanted looking for help
17129 joneugster feat(Tactic/Linter): add unicode linter for unicode variant-selectors large-import t-linter merge-conflict delegated awaiting-author failing CI
17131 joneugster feat(Tactic/Linter): add unicode linter for unwanted characters large-import t-linter merge-conflict awaiting-author merge conflict
22837 joneugster feat(Data/Set/Basic): add subset_iff and not_mem_subset_iff t-set-theory t-data merge-conflict merge conflict
24100 eric-wieser feat: restore some explicit binders from Lean 3 tech debt merge-conflict awaiting-author ⚠️ failing CI
21476 grunweg feat(lint-style): enable running on downstream projects t-linter merge-conflict merge conflict
23349 BGuillemet feat: add LocallyLipschitzOn.lipschitzOnWith_of_isCompact and two small lemmas about Lipschitz functions large-import new-contributor t-topology merge-conflict merge conflict
12438 jjaassoonn feat: some APIs for flat modules t-category-theory merge-conflict WIP labelled WIP
8740 digama0 fix: improve `recall` impl / error reporting awaiting-CI t-meta merge-conflict awaiting-author does not pass CI
21182 joneugster fix(Util/CountHeartbeats): move elaboration in #count_heartbeats inside a namespace t-meta merge-conflict merge conflict
23371 grunweg chore: mark `Disjoint.{eq_bot, inter_eq}` simp t-order merge-conflict awaiting-author merge conflict
16062 adomani Test/ci olean size CI merge-conflict awaiting-author WIP labelled WIP
16020 adomani feat: compare PR `olean`s size with `master` CI merge-conflict failing CI
12799 jstoobysmith feat(LinearAlgebra/UnitaryGroup): Add properties of Special Unitary Group new-contributor t-algebra merge-conflict please-adopt awaiting-author looking for help
23709 plp127 feat: `Nat.findFrom` t-data merge-conflict failing CI
25340 dupuisf chore(Analysis/Convex): move files pertaining to convex/concave functions to their own folder t-convex-geometry merge-conflict merge conflict
13994 grunweg chore(Topology): replace continuity -> fun_prop t-topology merge-conflict failing CI
21734 adomani fix(PR summary): checkout GITHUB_SHA CI merge-conflict awaiting-author WIP labelled WIP
13483 adomani feat: automatically replace deprecations t-meta merge-conflict delegated awaiting-author failing CI
20334 miguelmarco feat: allow polyrith to use a local Singular/Sage install new-contributor t-meta merge-conflict awaiting-author merge conflict
23953 b-reinke feat(Data/Matroid/Tutte): define the Tutte polynomial of a matroid t-data merge-conflict WIP labelled WIP
18441 ADedecker refactor(AdicTopology): use new API for algebraic filter bases, and factor some code t-algebra t-topology merge-conflict merge conflict
18439 ADedecker refactor: use new algebraic filter bases API in `FiniteAdeleRing` t-algebra t-topology merge-conflict merge conflict
18438 ADedecker refactor: adapt `KrullTopology` to the new algebraic filter bases API t-algebra t-topology merge-conflict merge conflict
13964 pechersky feat(Data/DigitExpansion): begin defining variant of reals without rationals t-data merge-conflict merge conflict
16074 Rida-Hamadani feat: combinatorial maps and planar graphs t-combinatorics merge-conflict merge conflict
16801 awainverse feat(ModelTheory/Equivalence): The quotient type of formulas modulo a theory t-logic merge-conflict awaiting-author merge conflict
17458 urkud refactor(Algebra/Group): make `IsUnit` a typeclass awaiting-zulip t-algebra merge-conflict failing CI
17627 hrmacbeth feat: universal properties of vector bundle constructions t-differential-geometry merge-conflict delegated merge conflict
19444 joelriou feat(CategoryTheory/Sites): Equivalence of categories of sheaves with a dense subsite that is 1-hypercover dense t-category-theory merge-conflict WIP labelled WIP
22928 javra feat(CategoryTheory): infrastructure for inclusion morphisms into products in categories with 0-morphisms t-category-theory merge-conflict failing CI
23763 grunweg feat(Linter.openClassical): also lint for Classical declarations as … t-linter merge-conflict failing CI
24710 chrisflav chore(Data/Set): `tsum` version of `Set.encard_iUnion_of_finite` for non-finite types t-data merge-conflict failing CI
24823 eric-wieser refactor: add `hom` lemmas for the `MonoidalCategory` structure on `ModuleCat` t-algebra merge-conflict merge conflict
25071 erdOne feat(EllipticCurve): basic API for singular cubics t-algebraic-geometry merge-conflict merge conflict
25218 kckennylau feat(AlgebraicGeometry): Tate normal form of elliptic curves awaiting-zulip new-contributor t-algebraic-geometry merge-conflict awaiting a zulip discussion
25283 Brian-Nugent feat: regular local rings new-contributor t-algebra merge-conflict merge conflict
25561 callesonne feat(Category/Grpd): define the bicategory of groupoids t-category-theory merge-conflict awaiting-author merge conflict
25573 JovanGerb feat: define `∃ x > y, ...` notation to mean `∃ x, y < x ∧ ...` t-meta merge-conflict merge conflict
25622 eric-wieser refactor: overhaul instances on LocalizedModule t-algebra merge-conflict failing CI
25816 sgouezel chore: kill coercion from EquivLike to Equiv t-logic merge-conflict WIP labelled WIP
25988 Multramate refactor(AlgebraicGeometry/EllipticCurve/*): replace Fin 3 with products t-algebraic-geometry merge-conflict merge conflict
26012 linesthatinterlace feat: Low-level derivatives of lifts on `OneHom`, `MulHom` and `MonoidHom` migrated-from-branch t-algebra merge-conflict merge conflict
26090 grunweg chore: make `finiteness` a default tactic merge-conflict failing CI
26776 sgouezel refactor: make `I` an outparam, and use forgetful inheritance in products RFC merge-conflict WIP labelled WIP
7596 alreadydone feat: covering maps from properly discontinuous actions and discrete subgroups file-removed t-topology merge-conflict merge conflict
24405 mcdoll refactor(Topology/Algebra/Module/WeakDual): Clean up large-import t-topology merge-conflict merge conflict
26647 b-mehta feat(Data/Sym/Sym2): lift commutative operations to sym2 t-data merge-conflict WIP labelled WIP
26067 mapehe feat(Topology/StoneCech): exists_continuous_surjection_from_StoneCech_to_dense_range t-topology merge-conflict merge conflict
23990 robertmaxton42 feat (Types.Colimits): Quot is functorial and colimitEquivQuot is natural new-contributor t-category-theory merge-conflict awaiting-author merge conflict
10541 xgenereux feat(Algebra/SkewMonoidAlgebra/Basic): add SkewMonoidAlgebra new-contributor t-algebra merge-conflict WIP labelled WIP
25999 bjoernkjoshanssen feat(Topology/Compactification): projective line over ℝ is homeomorphic to the one-point compactification of ℝ t-topology merge-conflict failing CI
24096 plp127 feat(Topology): Completely Regular Space iff Uniformizable t-topology merge-conflict merge conflict
25710 Paul-Lez feat(Mathlib/Analysis/PDE/Quasilinear/Characteristics): the method of characteristics for first order quasilinear PDEs t-analysis merge-conflict WIP labelled WIP
26911 JovanGerb chore: fix naming of `mono` and `monotone` merge-conflict delegated merge conflict
21838 joneugster feat(Cache): Allow arguments of the form `Mathlib.Data` which correspond to a folder but not a file CI t-meta merge-conflict awaiting-author merge conflict
25611 erdOne chore(RingTheory): add `Algebra (FractionRing R) (FractionRing S)` t-algebra merge-conflict failing CI
25284 alreadydone feat(LinearAlgebra/Contraction): bijectivity of `dualTensorHom` + generalize to CommSemiring t-algebra merge-conflict awaiting-author merge conflict
22749 joelriou feat(CategoryTheory/Abelian): the Gabriel-Popescu theorem as a localization with respect to a Serre class t-category-theory merge-conflict WIP labelled WIP
26804 kckennylau (WIP) feat(SetTheory): ZFSet is a model of ZFC t-set-theory merge-conflict WIP labelled WIP
20428 madvorak feat(Data/Sign): lemmas about `∈ Set.range SignType.cast` t-data merge-conflict WIP labelled WIP
26608 vihdzp feat(SetTheory/Cardinal/Aleph): `o.card ≤ ℵ_ o` and variants t-set-theory merge-conflict merge conflict
20029 FrederickPu Allow for Config attributes to be set directly new-contributor t-meta merge-conflict WIP labelled WIP
13973 digama0 feat: lake exe refactor, initial framework t-meta merge-conflict awaiting-author merge conflict
11021 jstoobysmith feat(AlgebraicTopology) : add join of augmented SSets t-algebraic-topology new-contributor merge-conflict WIP labelled WIP
10190 jstoobysmith feat(AlgebraicTopology): add Augmented Simplex Category t-algebraic-topology new-contributor t-category-theory merge-conflict WIP labelled WIP
26303 joelriou feat(AlgebraicTopology): the fundamental lemma of homotopical algebra t-algebraic-topology large-import t-category-theory merge-conflict WIP labelled WIP
20719 gio256 feat(AlgebraicTopology): delaborators for truncated simplicial notations t-algebraic-topology infinity-cosmos t-meta merge-conflict merge conflict
9935 jstoobysmith feat(AlgebraicTopology): add constructors for horns t-algebraic-topology new-contributor merge-conflict awaiting-author merge conflict
25914 eric-wieser feat: add an ext lemma for the opposite category t-category-theory awaiting-CI merge-conflict awaiting-author does not pass CI
20208 js2357 feat: Define the localization of a fractional ideal at a prime ideal t-algebra merge-conflict WIP labelled WIP
24260 plp127 feat(Topology): add API for Hereditarily Lindelof spaces t-topology merge-conflict awaiting-author merge conflict
27608 RemyDegenne feat(MeasureTheory): typeclasses for measures with finite moments t-measure-probability merge-conflict WIP labelled WIP
26306 j-loreaux refactor: make `IsSelfAdjoint` and `IsIdempotentElem` one-field structures. large-import merge-conflict failing CI
25726 tb65536 (WIP) Galois group of `x ^ n - x - 1` large-import t-algebra merge-conflict WIP labelled WIP
25991 Multramate feat(AlgebraicGeometry/EllipticCurve): generalise nonsingular condition t-algebraic-geometry merge-conflict failing CI
25985 Multramate feat(AlgebraicGeometry/EllipticCurve/Jacobian): add equivalences between points and explicit WithZero types t-algebraic-geometry merge-conflict failing CI
25984 Multramate feat(AlgebraicGeometry/EllipticCurve/Affine): add equivalences between points and explicit WithZero types t-algebraic-geometry merge-conflict failing CI
25982 Multramate feat(AlgebraicGeometry/EllipticCurve/Group): compute range of baseChange t-algebraic-geometry merge-conflict failing CI
25981 Multramate feat(GroupTheory/GroupAction/Basic): define homomorphisms of fixed subgroups induced by homomorphisms of groups t-group-theory merge-conflict failing CI
25980 Multramate feat(GroupTheory/Submonoid/Operations): define homomorphisms of subgroups induced by homomorphisms of groups t-group-theory merge-conflict failing CI
25485 VTrelat feat(SetTheory/ZFC/Naturals): define natural numbers in ZFC t-set-theory new-contributor merge-conflict failing CI
25474 adomani test for .lean/.md check file-removed t-linter merge-conflict failing CI
25238 Hagb feat(Tactic/ComputeDegree): add support for scalar multiplication with different types new-contributor t-meta merge-conflict merge conflict
11632 mattrobball chore(Group/RingTheory.Congruence): make `Quotient`'s reducible t-group-theory merge-conflict merge conflict
26385 jjdishere feat(RingTheory/Perfectoid): define integral perfectoid rings t-ring-theory merge-conflict WIP labelled WIP
22898 AntoineChambert-Loir feat(RingTheory/TensorProduct/DirectLimit/FG): direct limit of finitely generated submodules and tensor product t-ring-theory merge-conflict WIP labelled WIP
20431 erdOne feat(RingTheory/AdicCompletion): monotonicity of adic-completeness t-ring-theory merge-conflict awaiting-author merge conflict
19596 Command-Master feat(RingTheory/Valuation/PrimeMultiplicity): define `WithTop ℤ`-valued prime multiplicity on a fraction field t-ring-theory large-import merge-conflict awaiting-author merge conflict
18646 jxjwan feat(RingTheory): isotypic components t-ring-theory new-contributor merge-conflict failing CI
17246 pechersky feat(RingTheory/PrimaryDecomposition): PIR of Noetherian under jacobson condition t-ring-theory merge-conflict awaiting-author failing CI
21474 erdOne feat(RingTheory): replace `Ring.DimensionLEOne` with `Ring.KrullDimLE` t-ring-theory large-import merge-conflict failing CI
11575 ScottCarnahan feat (RingTheory/HahnSeries/Addition): Lemmas on leading terms t-ring-theory merge-conflict WIP labelled WIP
9820 jjaassoonn feat(RingTheory/GradedAlgebra/HomogeneousIdeal): generalize to homogeneous submodule t-ring-theory merge-conflict merge conflict
9339 FMLJohn feat (RingTheory/GradedAlgebra/HomogeneousIdeal): given a finitely generated homogeneous ideal of a graded semiring, construct a finite spanning set for the ideal which only contains homogeneous elements t-ring-theory merge-conflict merge conflict
11212 shuxuezhuyi feat(GroupTheory/GroupAction): instance `MulAction (β ⧸ H) α` t-group-theory large-import merge-conflict awaiting-author merge conflict
27886 alreadydone feat(Algebra): (Mv)Polynomial.X is irreducible assuming NoZeroDivisors t-algebra merge-conflict awaiting-author merge conflict
26200 adomani fix: add label when landrun fails CI merge-conflict merge conflict
17469 joelriou feat(Algebra/ModuleCat/Differentials/Presheaf): the presheaf of relative differentials large-import t-algebraic-geometry t-category-theory merge-conflict WIP labelled WIP
18254 callesonne feat(Bicategory/Modification/Pseudo): define modifications between strong natural transformations of pseudofunctors t-category-theory merge-conflict awaiting-author merge conflict
27709 kckennylau chore: fix links merge-conflict WIP labelled WIP
20671 thefundamentaltheor3m feat(Analysis/Asymptotics/SpecificAsymptotics): Proving that 𝛔ₖ(n) = O(nᵏ⁺¹) large-import new-contributor t-number-theory merge-conflict awaiting-author merge conflict
20267 joelriou feat(CategoryTheory): comma categories are accessible t-category-theory merge-conflict awaiting-author WIP labelled WIP
27451 kckennylau feat(RingTheory/Valuation): define ball, closed ball, and sphere t-ring-theory merge-conflict merge conflict
27987 kckennylau feat(RingTheory/Valuation): define ball, closed ball, and sphere t-ring-theory large-import merge-conflict merge conflict
24862 grunweg feat(LocallyIntegrable): generalise more to enorms carleson t-measure-probability merge-conflict WIP labelled WIP
27003 eric-wieser chore: use `Simp.ResultQ` more often t-meta merge-conflict merge conflict
25483 VTrelat chore(Data/Set/Prod, SetTheory/ZFC/Basic): add theorem prod_subset_of_prod and extend ZFC model t-data new-contributor merge-conflict merge conflict
25401 digama0 feat(Util): SuppressSorry option t-meta merge-conflict merge conflict
26394 winstonyin feat: existence of local flows on manifolds t-differential-geometry merge-conflict WIP labelled WIP
27759 plp127 chore(FreeAbelianGroup): deprecate multiplication large-import t-algebra merge-conflict failing CI
8102 miguelmarco feat(Tactic): add `unify_denoms` and `collect_signs` tactics new-contributor t-meta merge-conflict please-adopt modifies-tactic-syntax good first issue looking for help
14203 dagurtomas feat(Algebra/ModuleCat): descent data workshop-AIM-AG-2024 t-algebra t-algebraic-geometry t-category-theory merge-conflict WIP labelled WIP
27446 grunweg chore: more enorm lemmas carleson merge-conflict WIP labelled WIP
14583 lecopivo fix: make concrete cycle notation local merge-conflict awaiting-author merge conflict
19097 Vierkantor chore(Algebra.Polynomial): split `Polynomial/Basic.lean` into smaller files t-algebra merge-conflict merge conflict
28622 alreadydone chore(Mathlib): replace `=>` by `↦` merge-conflict merge conflict
24793 tristan-f-r feat: trace of unitarily similar matrices t-algebra merge-conflict awaiting-author merge conflict
28532 alreadydone chore(Algebra/Ring/Defs): add two classes and extend more t-algebra merge-conflict merge conflict
27872 JovanGerb chore(gcongr): clean up imports large-import merge-conflict delegated failing CI
28626 alreadydone chore(Archive, Counterexamples): replace => by ↦ merge-conflict merge conflict
7300 ah1112 feat: synthetic geometry t-euclidean-geometry merge-conflict awaiting-author help-wanted looking for help
13795 astrainfinita perf(Algebra/{Group, GroupWithZero, Ring}/InjSurj): reduce everything t-algebra merge-conflict merge conflict
28150 Equilibris chore: clean up proofs typevec proofs t-data new-contributor merge-conflict merge conflict
27868 grunweg linter indentation playground t-linter merge-conflict WIP labelled WIP
27403 MoritzBeroRoos fix: replace probably erroneous usage of ⬝ (with old \cdot) by · (with \centerdot) new-contributor merge-conflict merge conflict
28042 kckennylau feat(Topology/ValuativeRel): a topological basis indexed by pairs of elements t-ring-theory merge-conflict merge conflict
26015 linesthatinterlace feat: Add high-level generalizations from `MonoidHom` lifts migrated-from-branch t-algebra merge-conflict failing CI
27399 MoritzBeroRoos chore: replace every usage of ⬝ᵥ (with old \cdot) by ·ᵥ (with \centerdot) new-contributor merge-conflict merge conflict
27835 edegeltje feat(Tactic): ring modulo a given characteristic migrated-from-branch large-import t-meta merge-conflict ❌? infrastructure-related CI failing
25889 plp127 fix(Tactic/Widget/Conv): fix various issues t-meta merge-conflict merge conflict
28933 artie2000 WIP chore(Data): correct definition for `single_apply` merge-conflict failing CI
27437 kckennylau feat(RingTheory/Valuation): some lemmas about comparing with 1 and 0 and with each other t-ring-theory merge-conflict WIP labelled WIP
28708 sjh227 feat (Data) : edit DoublyStochastic, add Stochastic to matrix t-data new-contributor merge-conflict merge conflict
6042 MohanadAhmed feat(LinearAlgebra/Matrix/SVD): Singular Value Decomposition of R or C Matrices t-algebra merge-conflict please-adopt WIP looking for help
27785 staroperator chore(Algebra/Group/Submonoid): golf `Nat.addSubmonoidClosure_one` using `simp` large-import t-algebra merge-conflict merge conflict
28148 kckennylau feat(Matrix): Simproc and Rw-proc for Matrix Transpose t-meta merge-conflict merge conflict
26931 javra feat(CategoryTheory/Enriched): `V`-enriched isomorphisms infinity-cosmos t-category-theory merge-conflict awaiting-author merge conflict
25208 erdOne feat(LinearAlgebra): `tensor_induction` macro t-algebra RFC merge-conflict WIP labelled WIP
28803 astrainfinita refactor: unbundle algebra from `ENormed*` awaiting-zulip slow-typeclass-synthesis t-algebra t-analysis merge-conflict awaiting a zulip discussion
26603 vihdzp refactor(SetTheory/Ordinal/FixedPoint): redefine `Ordinal.deriv` t-set-theory merge-conflict failing CI
25662 erdOne chore: redefine `LocalizedModule` t-algebra merge-conflict failing CI
27566 wwylele feat(Data/Real): Archimedean.embedReal is a ring hom when M is an ordered ring large-import t-data merge-conflict merge conflict
28151 iehality feat(Computability): r.e. sets are closed under inter/union/projection/composition t-computability merge-conflict awaiting-author merge conflict
12143 adomani feat: generic linter, absorbing `cdot` linter and `attribute [instance] in` linter t-linter merge-conflict ??? missing CI information
26908 robin-carlier feat(CategoryTheory/Monoidal/DayConvolution): alternative ext principle for unitors t-category-theory merge-conflict merge conflict
27150 robin-carlier feat(CategoryTheory/Monoidal/DayConvolution): constructors for braided and symmetric structure on day convolutions monoidal categories t-category-theory merge-conflict merge conflict
27119 robin-carlier feat(CategoryTheory/Monoidal/DayConvolution): constructors for closed monoidal day convolution monoidal structures t-category-theory merge-conflict merge conflict
28411 zcyemi feat(LinearAlgebra/AffineSpace/Simplex/Centroid): define centroid and medians large-import t-algebra merge-conflict failing CI
28623 gilesgshaw feat(Logic/Basic): minor additions and simplification of proofs new-contributor t-logic merge-conflict merge conflict
24692 ScottCarnahan feat (RingTheory/HahnSeries/Basic): isomorphism of Hahn series induced by order isomorphism t-order merge-conflict WIP labelled WIP
13036 joelriou feat(CategoryTheory/Sites): under certain conditions, cover preserving functors preserve 1-hypercovers t-category-theory merge-conflict WIP labelled WIP
27335 eric-wieser chore(Data/List): use simp-normal-form for boolean equalities t-data merge-conflict failing CI
22517 j-loreaux feat: `ℕ+` powers in semigroups large-import merge-conflict WIP ⚠️ labelled WIP
27933 grunweg chore(OrdNode): format code example in code blocks t-data merge-conflict merge conflict
28802 grunweg feat: a tactic linter for continuity/measurability which can be `fun_prop` large-import awaiting-CI t-meta merge-conflict does not pass CI
25069 erdOne feat(EllipticCurve): rational points of singular nodal cubics t-algebraic-geometry merge-conflict awaiting-author merge conflict
25070 erdOne feat(EllipticCurve): rational points on singular cuspidal cubics t-algebraic-geometry merge-conflict awaiting-author merge conflict
29574 JarodAlper Regular local rings are domains t-ring-theory new-contributor merge-conflict failing CI
26670 yu-yama feat(GroupExtension/Abelian): define `conjClassesEquivH1` t-algebra merge-conflict awaiting-author merge conflict
26154 ADedecker refactor: add refactored APIs for algebraic filter bases t-topology merge-conflict merge conflict
27024 grunweg feat: Gram-Schmidt orthonormalisation for sections of a vector bundle t-differential-geometry merge-conflict awaiting-author merge conflict
28580 kmill refactor: simplify implementation of `filter_upwards` t-order t-meta merge-conflict failing CI
29605 alreadydone experiment(Algebra): unbundle npow/zpow from Monoid/InvDivMonoid t-algebra awaiting-CI merge-conflict does not pass CI
26890 robin-carlier feat(CategoryTheory/Monoidal/DayConvolution) : more API for `DayFunctor` t-category-theory merge-conflict merge conflict
7125 eric-wieser feat: additive monoid structure via biproducts t-category-theory awaiting-CI merge-conflict WIP labelled WIP
25138 chrisflav chore(RingTheory/Ideal): make `RingHom.ker` take a `RingHom` instead of `RingHomClass` t-algebra merge-conflict failing CI
29281 plp127 docs: `Fin.natAdd_castLEEmb` t-data merge-conflict merge conflict
27972 smmercuri refactor: make `Valuation.Completion` a `def` and refactor more of `AdicValuation.lean` t-algebra t-number-theory merge-conflict WIP labelled WIP
28908 joelriou feat(CategoryTheory): Pullback functors on `Over` categories in `Type` have right adjoints t-category-theory merge-conflict awaiting-author failing CI
25480 ocfnash feat: define a concrete model of the `𝔤₂` root system large-import t-algebra merge-conflict WIP labelled WIP
29330 plp127 chore: define `Fin.cycleIcc` with conditions t-group-theory merge-conflict merge conflict
29118 edegeltje chore(CategoryTheory): align `refl` and `rfl` declarations in CategoryTheory will-close-soon t-category-theory merge-conflict awaiting-author merge conflict
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]` t-number-theory merge-conflict merge conflict
27668 IvanRenison feat(Analysis/InnerProductSpace): define outer product of linear maps t-analysis merge-conflict failing CI
12278 Rida-Hamadani feat(Combinatorics/SimpleGraph): Provide iff statements for distance equal and greater than 2 t-combinatorics merge-conflict awaiting-author failing CI
29092 zhuyizheng feat(MeasureTheory): add absolutely continuous functions, FTC and integration by parts new-contributor t-measure-probability merge-conflict awaiting-author merge conflict
26178 ppls-nd-prs feat(CategoryTheory/Limits): Fubini for products new-contributor t-category-theory merge-conflict awaiting-author merge conflict
27214 robin-carlier feat(CategoryTheory/Limits/Shapes/Pullback/Categorical): Categorical pullback squares t-category-theory merge-conflict merge conflict
26466 robin-carlier feat(AlgebraicTopology/SimplexCategory/Augmented): the canonical monoid object in the augmented simplex category t-algebraic-topology t-category-theory merge-conflict merge conflict
28074 grunweg Isbilinearmap merge-conflict WIP labelled WIP
26578 robin-carlier feat(CategoryTheory/Limits/Pullbacks/Categorical/CatCospanTransform): adjunctions of categorical cospans large-import t-category-theory merge-conflict merge conflict
27970 smmercuri feat: collections of distinct infinite places contain values that diverge around 1 FLT t-algebra t-number-theory merge-conflict WIP labelled WIP
25042 alreadydone feat(Topology): restriction/extension of Trivialization and composition with Homeomorph t-topology merge-conflict merge conflict
29012 grunweg chore: reduce `Topology` imports in `Data` file-removed merge-conflict failing CI
26601 yuma-mizuno feat(CategoryTheory): make `Functor.comp` irreducible t-category-theory merge-conflict WIP labelled WIP
23621 astrainfinita chore: deprecate `LinearOrderedComm{Monoid, Group}WithZero` t-order t-algebra merge-conflict merge conflict
30192 erdOne feat(RingTheory): valuative topology = adic topology for discrete rank 1 valuations t-ring-theory t-topology merge-conflict WIP labelled WIP
26344 mans0954 feat(Analysis/NormedSpace/MStructure): The component projections on WithLp 1 (α × β) are L-projections file-removed t-analysis merge-conflict WIP labelled WIP
25992 Multramate feat(RingTheory/Ideal/Span): add pair lemmas t-ring-theory merge-conflict awaiting-author merge conflict
29587 uniwuni feat(GroupTheory/Finiteness): define finitely generated semigroups merge-conflict ⚠️ merge conflict
29241 yoh-tanimoto feat(Analysis/InnerProductSpace/Orthogonal): add duplicates for `ClosedSubmodule` merge-conflict awaiting-author ⚠️ merge conflict
16239 Rida-Hamadani feat(Geometry/Manifold): orientable manifolds t-differential-geometry merge-conflict awaiting-author failing CI
16773 arulandu feat(Probability/Distributions): formalize Beta distribution new-contributor t-measure-probability merge-conflict awaiting-author failing CI
22657 Xmask19 feat: a graph is maximally acyclic iff it is a tree new-contributor t-combinatorics merge-conflict failing CI
27445 erdOne chore(RingTheory/LocalRing): fix problematic instance t-algebra merge-conflict failing CI
27990 kckennylau feat(Counterexamples): a nontrivial valuation with discrete topology t-ring-theory merge-conflict merge conflict
24434 joelriou feat(CategoryTheory): effectiveness of descent t-category-theory merge-conflict WIP labelled WIP
28243 robin-carlier chore(CategoryTheory/Bicategory): move some `eqToHom` lemmas t-category-theory merge-conflict awaiting-author merge conflict
9273 grunweg feat: extended charts are local diffeomorphisms on their source t-differential-geometry merge-conflict awaiting-author merge conflict
29120 eric-wieser feat: add a typeclass for the indiscrete topology t-topology merge-conflict failing CI
15045 Command-Master fix(LinearAlgebra/Alternating/Basic): fix `MultilinearMap.alternatization` t-algebra merge-conflict awaiting-author ??? missing CI information
26339 mans0954 feat(Analysis/Normed/Module/WeakDual): Banach Dieudonné Lemma large-import t-analysis merge-conflict WIP labelled WIP
29378 mans0954 feat(Analysis/LocallyConvex/AbsConvex): Balanced and AbsConvex sets under linear maps t-analysis merge-conflict merge conflict
21853 smmercuri feat: the adele ring of a number field is locally compact large-import t-number-theory merge-conflict WIP labelled WIP
26913 Paul-Lez feat(NumberTheory/{*}): add a few lemmas about number field and cyclotomic extensions t-algebra t-number-theory awaiting-CI merge-conflict WIP labelled WIP
28925 grunweg chore: remove `linear_combination'` tactic file-removed awaiting-zulip merge-conflict awaiting a zulip discussion
30248 dwrensha chore: remove obsolete NormDigits namespace t-data merge-conflict merge conflict
19616 adamtopaz fix: fix the definition of the absolute Galois group of a field t-algebra t-number-theory merge-conflict awaiting-author merge conflict
28826 alreadydone feat(CategoryTheory): Additive and Linear when Hom types are only monoids t-category-theory awaiting-CI merge-conflict WIP labelled WIP
28126 Sebi-Kumar feat(AlgebraicTopology/FundamentalGroupoid): relate equality in fundamental groupoid to homotopy t-algebraic-topology new-contributor merge-conflict awaiting-author merge conflict
30271 artie2000 chore: "weaken" typeclasses for totally ordered fields bench-after-CI t-meta merge-conflict failing CI
24532 robertmaxton42 feat(LinearAlgebra/FreeProduct): fill out the `FreeProduct.asPowers` namespace t-algebra merge-conflict failing CI
22366 kim-em feat: `check_equalities` tactic for diagnosing defeq problems t-meta merge-conflict delegated failing CI
26436 AntoineChambert-Loir feat(Mathlib/Data/Nat/Prime/Defs): fuel Nat.minFac t-data merge-conflict failing CI
27683 dupuisf feat: grind tags for set operations t-data merge-conflict failing CI
25978 Bergschaf feat(Order/Sublocale): Open Sublocales t-order merge-conflict merge conflict
29355 girving feat(Trigonometric): Taylor series bounds for sin and cos t-analysis merge-conflict failing CI
29514 grunweg More strict mode CI merge-conflict WIP labelled WIP
28298 thorimur chore: dedent `to_additive` docstrings merge-conflict awaiting-author documentation merge conflict
23600 mattrobball perf(Quiver.Basic): make `IsThin` a `class` merge-conflict delegated merge conflict
28737 astrainfinita refactor: deprecate `MulEquivClass` t-algebra merge-conflict awaiting-author merge conflict
28676 sun123zxy feat(NumberTheory/ArithmeticFunction): wrap `Nat.totient` as an `ArithmeticFunction` large-import new-contributor t-number-theory merge-conflict awaiting-author merge conflict
30421 grunweg WIP: support products in the differential geometry elaborators merge-conflict failing CI
30299 franv314 feat(Topology/Instances): Cantor set file-removed new-contributor t-topology merge-conflict awaiting-author merge conflict
30690 grunweg style(Order): fix whitespace t-order merge-conflict merge conflict
27364 101damnations feat(RepresentationTheory/Homological/GroupCohomology): cohomology of finite cyclic groups t-algebra merge-conflict awaiting-author merge conflict
26138 xroblot Development branch (2) merge-conflict WIP labelled WIP
28962 grunweg chore: enable the flexible linter in mathlib merge-conflict failing CI
27976 smmercuri feat: `ramificationIdx` for `NumberField.InfinitePlace` t-number-theory merge-conflict WIP labelled WIP
26357 javra feat(CategoryTheory): linear categories as `ModuleCat R`-enriched categories large-import t-category-theory merge-conflict awaiting-author merge conflict
26085 grunweg feat: disjoint unions distribute with products of manifolds t-differential-geometry merge-conflict please-adopt WIP looking for help
27180 ADedecker feat: quotient of a monoid with zero by a multiplicative congruence t-algebra merge-conflict delegated merge conflict
30790 urkud chore: partially migrate from `ContinuousMap.continuous` merge-conflict failing CI
29435 sgouezel WIP: typeclass experiment t-algebra merge-conflict WIP labelled WIP
26259 Raph-DG feat(Topology): Connecting different notions of locally finite t-topology merge-conflict awaiting-author merge conflict
25692 Whysoserioushah feat(RingTheory/MatrixAlgebra): add a more general version of `matrixEquivTensor` t-ring-theory merge-conflict awaiting-author merge conflict
25012 urkud refactor(*): migrate from `Matrix.toLin'` to `Matrix.mulVecLin` merge-conflict failing CI
27918 kim-em wip: refactor WithBot/WithTop as structures file-removed merge-conflict failing CI
29638 yuma-mizuno feat(CategoryTheory): define descent data by presieves t-category-theory merge-conflict WIP labelled WIP
31182 fgdorais chore: adaptations for batteries#1486 blocked-by-batt-PR merge-conflict blocked on another PR
22361 rudynicolop feat(Computability/NFA): nfa closure properties awaiting-zulip t-computability new-contributor merge-conflict awaiting-author awaiting a zulip discussion
27392 Paul-Lez feat(Tactic/SimpUtils): add simproc finding commands file-removed large-import t-meta merge-conflict awaiting-author failing CI*
29909 Vierkantor feat(CI): add build output to CI workflows CI merge-conflict merge conflict
31220 fgdorais chore: adaptations for batteries#1489 large-import blocked-by-batt-PR merge-conflict blocked on another PR
27708 vihdzp feat: unions and intersections of ordinals are ordinals t-set-theory merge-conflict awaiting-author merge conflict
26446 joelriou refactor(CategoryTheory): make morphisms in full subcategories a 1-field structure large-import t-category-theory merge-conflict WIP labelled WIP
29550 Raph-DG feat(RingTheory): Order of vanishing in a discrete valuation ring t-ring-theory file-removed merge-conflict awaiting-author failing CI
28132 dupuisf feat: preliminary `grind` tags for `IsUnit` t-algebra merge-conflict merge conflict
29020 grunweg chore: squeeze a few non-terminal simps merge-conflict awaiting-author merge conflict
29076 yury-harmonic feat(BigOperators/ModEq): new file merge-conflict ⚠️ failing CI
26735 Raph-DG feat(AlgebraicGeometry): The codimension of a point of a scheme is equal to the krull dimension of the stalk large-import t-algebraic-geometry merge-conflict awaiting-author failing CI
30686 grunweg tracking: #30658 split into pieces large-import merge-conflict failing CI
30484 vihdzp refactor: override `≤` and `<` in `Function.Injective.semilatticeSup`, etc. t-order merge-conflict merge conflict
29877 Komyyy feat: inner product of the gradient t-analysis merge-conflict merge conflict
31270 fgdorais chore: adaptations for batteries#1490 blocked-by-batt-PR merge-conflict blocked on another PR
29992 vlad902 feat(Order): finite (Max)Chains always contains a top/max element large-import t-order merge-conflict WIP labelled WIP
26901 5hv5hvnk feat: a simproc version of `compute_degree` new-contributor awaiting-CI t-meta merge-conflict awaiting-author does not pass CI
28153 kckennylau feat(Simproc): Simproc for explicit diagonal matrices t-meta merge-conflict awaiting-author merge conflict
26348 mans0954 WIP: feature(Analysis/LocallyConvex/Prime): The prime map t-analysis merge-conflict WIP labelled WIP
27443 yuanyi-350 doc: Stacks tags t-algebra t-analysis merge-conflict awaiting-author merge conflict
31020 grunweg feat: mfderiv of Sum.inl and Sum.inr merge-conflict WIP ⚠️ labelled WIP
26345 mans0954 feat(Analysis/LocallyConvex/Polar): Bipolar theorem large-import t-analysis merge-conflict awaiting-author merge conflict
29369 vlad902 feat(SimpleGraph): `IsSubwalk` of common Walk decompositions t-combinatorics merge-conflict merge conflict
25775 emilyriehl feat(AlgebraicTopology/SimplicialSet/NerveAdjunction): to Strict Segal 2 t-algebraic-topology infinity-cosmos t-category-theory merge-conflict awaiting-author ❌? infrastructure-related CI failing
10235 urkud feat: add `Decidable`, `Fintype`, `Encodable` linters awaiting-bench large-import t-linter t-meta merge-conflict awaiting-author failing CI
14444 digama0 fix(GeneralizeProofs): unreachable! bug t-meta merge-conflict awaiting-author merge conflict
30666 erdOne feat(NumberTheory): every number field has a ramified prime t-algebra t-number-theory merge-conflict awaiting-author failing CI
25481 kbuzzard chore: refactor Algebra.TensorProduct.rightAlgebra t-algebra merge-conflict delegated merge conflict
29937 Thmoas-Guan feat(RingTheory): `ringKrullDim` of quotient via supportDim t-ring-theory merge-conflict merge conflict
14752 AntoineChambert-Loir fix(Topology/Algebra/Valued): repair definition of Valued t-algebra t-topology merge-conflict WIP labelled WIP
25848 joelriou feat/refactor: redefinition of homology + derived categories large-import t-topology t-category-theory merge-conflict WIP labelled WIP
31505 dsfxcimk Yulia new-contributor t-euclidean-geometry merge-conflict awaiting-author failing CI
30366 sinhp feat (CategoryTheory): The Preliminaries for Locally Cartesian Closed Categories t-category-theory merge-conflict awaiting-author merge conflict
30373 sinhp feat (CategoryTheory) : LCCC sections (constructing right adjoint to `Over.ChosenPullback.pullback`) t-category-theory merge-conflict awaiting-author merge conflict
31332 sinhp feat(CategoryTheory): Exponentiable morphisms t-category-theory merge-conflict WIP labelled WIP
30441 linesthatinterlace fix(Data/List/Sort): Deprecate and replace `List.Sorted` merge-conflict merge conflict
26827 pechersky feat(Analysis/Normed/ValuativeRel): helper instance for NormedField t-algebra t-analysis t-number-theory merge-conflict merge conflict
30281 j-loreaux chore(Analysis/{NormedSpace,Normed/Module}): migrate all remaining files file-removed t-analysis merge-conflict merge conflict
30122 xroblot Development branch (1) large-import merge-conflict WIP labelled WIP
29014 ShreckYe feat(Data/List/Scan): some theorems that relate `scanl` with `foldl` t-data merge-conflict merge conflict
27936 alreadydone feat(Algebra): additivize Dvd and Prime t-algebra merge-conflict merge conflict
28546 Sfgangloff feat(SymbolicDynamics): basic setup of Zd, full shift, cylinders, pat… new-contributor t-dynamics merge-conflict merge conflict
30150 imbrem feat(CategoryTheory/Monoidal): to_additive for MonoidalCategory large-import awaiting-zulip new-contributor t-category-theory t-meta merge-conflict awaiting a zulip discussion
27706 xroblot feat(RingTheory/Localization/AtPrime): inertia degree and ramification index are preserved by localization t-ring-theory merge-conflict failing CI
26484 peabrainiac feat(Geometry/Diffeology): basics of diffeological spaces t-differential-geometry merge-conflict merge conflict
28291 vasnesterov feat(Tactic): tactic for computing asymptotics of real functions t-analysis t-meta merge-conflict WIP labelled WIP
28070 grunweg style: improve indentation of multi-linear enumerations in doc-strings merge-conflict failing CI
31587 JovanGerb Lean pr testing 11156 merge-conflict failing CI*
31345 dagurtomas feat(CategoryTheory): some API for transporting monoidal morphism properties large-import t-category-theory merge-conflict delegated merge conflict
15651 TpmKranz feat(Computability/NFA): operations for Thompson's construction awaiting-zulip t-computability new-contributor merge-conflict awaiting-author awaiting a zulip discussion
24614 JovanGerb chore: rename field `inf` to `min` in `Lattice` awaiting-zulip t-order merge-conflict awaiting a zulip discussion
12879 grunweg feat: port ge_or_gt linter from mathlib3 tech debt t-linter merge-conflict blocked-by-other-PR blocked on another PR
13057 alreadydone feat(NumberTheory): characterize elliptic divisibility sequences t-algebra t-number-theory merge-conflict blocked-by-other-PR blocked on another PR
10842 mcdoll chore: simplify proofs using new positivity extensions and tests merge-conflict blocked-by-other-PR WIP blocked on another PR
7564 shuxuezhuyi feat(Topology/Algebra/Order): extend strictly monotone function on `Ioo` to homeomorphism on `Icc` t-topology merge-conflict blocked-by-other-PR blocked on another PR
8364 thorimur feat: `refine?` t-meta merge-conflict blocked-by-other-PR blocked on another PR
7565 shuxuezhuyi feat(Topology/Algebra/Order): extend homeomorphism of `Ioo` to `Icc` t-order t-topology merge-conflict blocked-by-other-PR blocked on another PR
9154 astrainfinita feat: `npow` / `nsmul` / `Nat.cast`/ `zpow` / `zsmul` implemented using `Nat.binaryRec` t-algebra merge-conflict awaiting-author blocked-by-other-PR blocked on another PR
7861 shuxuezhuyi feat(Geometry/Hyperbolic/UpperHalfPlane): instance IsometricSMul PSL(2, ℝ) ℍ t-euclidean-geometry merge-conflict blocked-by-other-PR blocked on another PR
12087 JADekker feat : complete API for K-Lindelöf spaces t-topology merge-conflict please-adopt blocked-by-other-PR blocked on another PR
13782 alreadydone feat(EllipticCurve): ZSMul formula in terms of division polynomials t-algebra t-algebraic-geometry t-number-theory merge-conflict blocked-by-other-PR blocked on another PR
14242 js2357 feat: Prove equivalence of `isDedekindDomain` and `isDedekindDomainDvr` new-contributor t-algebra merge-conflict blocked-by-other-PR blocked on another PR
16215 adomasbaliuka feat(Tactic/Linter): lint unwanted unicode t-linter merge-conflict blocked-by-other-PR blocked on another PR
16888 metinersin feat(ModelTheory/Complexity): Define conjunctive and disjunctive normal forms new-contributor t-logic merge-conflict blocked-by-other-PR blocked on another PR
16887 metinersin feat(ModelTheory/Complexity): define conjunctive and disjunctive formulas new-contributor t-logic merge-conflict blocked-by-other-PR blocked on another PR
16889 metinersin feat(ModelTheory/Complexity): Normal forms new-contributor t-logic merge-conflict blocked-by-other-PR blocked on another PR
13965 pechersky feat(Data/DigitExpansion): reals via digit expansion are complete t-data merge-conflict blocked-by-other-PR blocked on another PR
17519 grunweg feat: the `metrisableSpace` linter t-linter merge-conflict blocked-by-other-PR blocked on another PR*
12750 Command-Master feat: define Gray code t-data new-contributor merge-conflict awaiting-author blocked-by-other-PR blocked on another PR
13514 madvorak feat(Computability/ContextFreeGrammar): closure under union t-computability merge-conflict blocked-by-other-PR blocked on another PR
17518 grunweg feat: lint on declarations mentioning `Invertible` or `Unique` awaiting-zulip t-linter merge-conflict blocked-by-other-PR blocked on another PR*
18716 jjaassoonn feat(Algebra/Module/GradedModule): quotient and subgrading t-algebra awaiting-CI merge-conflict blocked-by-other-PR WIP blocked on another PR
18784 erdOne feat(AlgebraicGeometry) use `addMorphismPropertyInstances` t-algebraic-geometry merge-conflict blocked-by-other-PR blocked on another PR
17593 astrainfinita chore(Algebra/Order/GroupWithZero/Unbundled): deprecate useless lemmas, use `ZeroLEOneClass` t-order t-algebra merge-conflict blocked-by-other-PR blocked on another PR
17624 astrainfinita feat(Algebra/Order/GroupWithZero/Unbundled): generalize lemmas t-order t-algebra merge-conflict blocked-by-other-PR blocked on another PR
17515 astrainfinita perf: do not need `simp low` now t-algebra merge-conflict blocked-by-other-PR blocked on another PR
18876 GabinKolly feat(ModelTheory/Fraisse): add proof that Fraïssé limits exist t-logic blocked-by-other-PR blocked on another PR
19281 Vierkantor chore(Algebra/{MonoidAlgebra,Polynomial}): algebra structure in `Basic.lean` t-algebra merge-conflict blocked-by-other-PR blocked on another PR
19621 Command-Master feat: Multiplicity and prime-adic valuation of derivations large-import t-algebra merge-conflict blocked-by-other-PR blocked on another PR
18262 joelriou feat(Algebra/Category/ModuleCat/Presheaf): exterior powers of presheaves of modules t-algebra t-category-theory merge-conflict blocked-by-other-PR WIP blocked on another PR
15269 kkytola feat: Add ENNReal.floor t-order t-algebra merge-conflict awaiting-author blocked-by-other-PR blocked on another PR
17471 joelriou feat(Algebra/ModuleCat/Differentials/Sheaf): the sheaf of relative differentials large-import t-algebraic-geometry t-category-theory merge-conflict blocked-by-other-PR WIP blocked on another PR
19462 joelriou feat(AlgebraicGeometry): étale sheafification t-algebraic-geometry merge-conflict blocked-by-other-PR WIP blocked on another PR
15720 znssong feat(SimpleGraph): The Bondy-Chvátal theorem new-contributor t-combinatorics merge-conflict blocked-by-other-PR blocked on another PR
12670 trivial1711 feat: completion of a nonarchimedean multiplicative group t-algebra t-topology merge-conflict blocked-by-other-PR blocked on another PR
21277 GabinKolly feat(ModelTheory/PartialEquiv): Define the mapping of a self-partialEquiv through an embedding t-logic blocked-by-other-PR blocked on another PR
20248 peabrainiac feat(Topology/Compactness): first-countable locally path-connected spaces are delta-generated large-import new-contributor t-topology merge-conflict awaiting-author blocked-by-other-PR blocked on another PR
20956 tomaz1502 feat(Computability/QueryComplexity/Sort.lean): Formalization of upper bound of queries for merge sort t-computability blocked-by-other-PR blocked on another PR
22233 pechersky feat(Algebra/Valued): `AdicExpansion.evalAt` t-topology blocked-by-other-PR blocked on another PR
22232 pechersky feat(Algebra/Valued): `AdicExpansion.apprUpto` t-topology blocked-by-other-PR blocked on another PR
14060 YnirPaz feat(SetTheory/Ordinal/Clubs): define club sets and prove basic properties new-contributor t-logic merge-conflict blocked-by-other-PR blocked on another PR
16000 YaelDillies feat: Croot-Sisask Almost Periodicity t-analysis t-combinatorics blocked-by-other-PR blocked on another PR
22340 sinhp feat(CategoryTheory): Locally Cartesian Closed Categories (Beck-Chevalley Conditions) large-import t-category-theory merge-conflict blocked-by-other-PR WIP blocked on another PR
23145 joneugster feat(CategoryTheory/Enriched/Limits): add IsConicalLimits infinity-cosmos t-category-theory merge-conflict blocked-by-other-PR blocked on another PR
20222 eric-wieser feat: generalize lemmas about derivatives t-analysis merge-conflict blocked-by-other-PR blocked on another PR
22321 sinhp feat(CategoryTheory): Locally Cartesian Closed Categories (Definition) large-import t-category-theory merge-conflict blocked-by-other-PR blocked on another PR
22319 sinhp feat(CategoryTheory): Locally Cartesian Closed Categories (Sections Right Adjoint) large-import t-category-theory merge-conflict blocked-by-other-PR blocked on another PR
24010 grunweg feat(Counterexamples): a non-negative function, not a.e. zero, with vanishing lowe… t-measure-probability please-adopt blocked-by-other-PR WIP blocked on another PR
24016 plp127 feat: fine uniformity t-topology blocked-by-other-PR blocked on another PR
21238 joneugster feat(Cache): enable partial cache in downstream projects CI t-meta merge-conflict blocked-by-other-PR blocked on another PR
21842 joneugster refactor(Cache): use module name for file hash instead of non-resolved file path CI t-meta merge-conflict blocked-by-other-PR blocked on another PR*
19467 quangvdao feat(MvPolynomial/Equiv): Add `MvPolynomial.finSuccEquivNth` t-algebra merge-conflict blocked-by-other-PR blocked on another PR
24549 grunweg feat: define embedded submanifolds, attempt 1 t-differential-geometry merge-conflict blocked-by-other-PR WIP blocked on another PR
11003 thorimur chore: migrate to `tfae` block tactic t-meta merge-conflict blocked-by-other-PR WIP blocked on another PR
16186 joneugster chore: use emoji-variant-selector `\uFE0F` for emojis ✅️,❌️,💥️,🟡️ t-linter merge-conflict awaiting-author blocked-by-other-PR blocked on another PR
15654 TpmKranz feat(Computability): language-preserving maps between NFA and RE awaiting-zulip t-computability new-contributor merge-conflict blocked-by-other-PR blocked on another PR
24550 grunweg feat: define `SliceModel` typeclass for models with corners for embedded submanifolds t-differential-geometry merge-conflict blocked-by-other-PR WIP blocked on another PR
18755 astrainfinita refactor: deprecate `LinearIsometryClass` t-algebra t-analysis merge-conflict blocked-by-other-PR blocked on another PR
5863 eric-wieser feat: add elaborators for concrete matrices t-meta blocked-by-other-PR help-wanted blocked on another PR
25912 BoltonBailey feat: add simp lemmas for trig functions on `π * 2⁻¹` t-analysis awaiting-author blocked-by-other-PR blocked on another PR
18771 joelriou feat(LinearAlgebra/ExteriorPower): exterior powers of free modules are free t-algebra merge-conflict blocked-by-other-PR WIP blocked on another PR
25926 BoltonBailey feat: add lemma about `degreeOf_eq_degree` t-algebra blocked-by-other-PR blocked on another PR
20051 Timeroot feat: `Clone` and some instances t-algebra awaiting-author blocked-by-other-PR blocked on another PR
18662 joelriou feat(LinearAlgebra/ExteriorPower): generators of the exterior powers t-algebra merge-conflict blocked-by-other-PR WIP blocked on another PR
18735 joelriou feat(Algebra/Module): presentation of the exterior power t-algebra merge-conflict blocked-by-other-PR WIP blocked on another PR
18551 joelriou feat(AlgebraicGeometry): the algebraic De Rham complex t-algebra t-algebraic-geometry merge-conflict blocked-by-other-PR WIP blocked on another PR
26185 vasnesterov feat(Counterexamples): Peano curve large-import t-topology merge-conflict blocked-by-other-PR blocked on another PR
26395 winstonyin feat: $C^1$ vector fields on compact manifolds define global flows t-differential-geometry merge-conflict blocked-by-other-PR WIP blocked on another PR
26465 joelriou feat(Algebra/Module): presentation of the `PiTensorProduct` file-removed t-algebra merge-conflict blocked-by-other-PR blocked on another PR
26467 joelriou feat(LinearAlgebra): the tensor product of a finite family of free modules is free file-removed t-algebra merge-conflict blocked-by-other-PR WIP blocked on another PR
26165 oliver-butterley feat(MeasureTheory.VectorMeasure): add lemma which shows that variation of a `ℝ≥0∞` VectorMeasure is equal to itself new-contributor t-measure-probability blocked-by-other-PR blocked on another PR
26168 oliver-butterley feat(MeasureTheory.VectorMeasure) : variation defined as a supremum is equal to variation defined using the Hahn-Jordan decomposition. new-contributor t-measure-probability blocked-by-other-PR blocked on another PR
26160 oliver-butterley feat(MeasureTheory.VectorMeasure): add several lemmas which characterize variation new-contributor t-measure-probability blocked-by-other-PR blocked on another PR
24912 YaelDillies feat: affine monoids toric t-algebra blocked-by-other-PR blocked on another PR
10654 smorel394 feat(LinearAlgebra/{ExteriorPower,LinearIndependent,TensorPower}): define the exterior powers of a module and prove some of their basic properties large-import t-algebra merge-conflict please-adopt blocked-by-other-PR blocked on another PR
27070 vasnesterov golf: use `order` large-import merge-conflict blocked-by-other-PR WIP blocked on another PR
19607 madvorak Block matrix totally unimodular merge-conflict blocked-by-other-PR WIP blocked on another PR
26987 joelriou chore: deprecating module LinearAlgebra.PiTensorProduct t-algebra merge-conflict blocked-by-other-PR WIP blocked on another PR
24668 robertmaxton42 feat(LinearAlgebra): add inductive principle for the free product of algebras t-algebra merge-conflict blocked-by-other-PR blocked on another PR
10006 jstoobysmith feat(AlgebraicTopology): homotopy in quasicategories t-algebraic-topology new-contributor merge-conflict awaiting-author blocked-by-other-PR blocked on another PR
26399 ChrisHughes24 refactor(ModelTheory): tidy up proof of Ax-Grothendieck with definable functions t-logic blocked-by-other-PR blocked on another PR
25486 VTrelat feat(SetTheory/ZFC/Integers): define integers in ZFC t-set-theory new-contributor merge-conflict blocked-by-other-PR blocked on another PR
25484 VTrelat feat(SetTheory/ZFC/Booleans): define Boolean algebra in ZFC t-set-theory new-contributor merge-conflict blocked-by-other-PR blocked on another PR
22909 AntoineChambert-Loir feat(RingTheory/Pure): pure submodules t-ring-theory merge-conflict blocked-by-other-PR blocked on another PR
22908 AntoineChambert-Loir feat(RingTheory/Finiteness/Small): tensor product of the system of small submodules t-ring-theory merge-conflict blocked-by-other-PR blocked on another PR
14089 callesonne feat(Bicategory/Functorbicategory): define bicategory of pseudofunctors t-category-theory merge-conflict blocked-by-other-PR blocked on another PR
28208 Sebi-Kumar feat(Topology): add the definition `foldTrans` to concatenate finite sequences of paths new-contributor t-topology blocked-by-other-PR blocked on another PR
27897 grunweg feat: check indentation of doc-strings t-linter awaiting-CI merge-conflict blocked-by-other-PR blocked on another PR
27996 grunweg feat: check indentation in doc-strings, medium version merge-conflict blocked-by-other-PR WIP ⚠️ blocked on another PR
7873 astrainfinita perf: reorder `extends` and change instance priority in algebra hierarchy slow-typeclass-synthesis t-algebra merge-conflict blocked-by-other-PR blocked on another PR
28530 nonisomorphiclinearmap feat(Combinatorics/SimplicialComplex/Topology): add standard simplices and geometric realisation (colimit + functoriality) new-contributor t-combinatorics blocked-by-other-PR blocked on another PR
27557 chrisflav feat(RingTheory/KrullDimension): dimension of `R / (x)` for a nonzerodivisor t-ring-theory large-import merge-conflict blocked-by-other-PR blocked on another PR
27542 chrisflav feat(RingTheory/KrullDimension): dimension of polynomial ring t-ring-theory large-import merge-conflict blocked-by-other-PR blocked on another PR
28502 gilesgshaw feat(Logic/Basic): avoid unnecessary uses of choice new-contributor t-logic merge-conflict awaiting-author blocked-by-other-PR blocked on another PR
27198 robin-carlier feat(CategoryTheory/Monoidal/DayConvolution): the Yoneda embedding is monoidal (for Day convolution) file-removed t-category-theory merge-conflict blocked-by-other-PR blocked on another PR
26719 AntoineChambert-Loir feat(RingTheory/PolynomialLaw/Basic): extends polynomial laws to arbitrary universes t-ring-theory large-import blocked-by-other-PR blocked on another PR
28499 yoh-tanimoto feat(MeasureTheory/VectorMeasure): add integral of a vector-valued function against a vector measure t-measure-probability blocked-by-other-PR blocked on another PR
19582 yu-yama feat(GroupExtension/Abelian): define `OfMulDistribMulAction.equivH2` new-contributor t-algebra merge-conflict blocked-by-other-PR blocked on another PR
25488 VTrelat feat(SetTheory/ZFC/Rationals): define rationals in ZFC t-set-theory new-contributor merge-conflict blocked-by-other-PR blocked on another PR
28787 alreadydone feat(Counterexamples): a domain whose ring of differences is not a domain large-import t-algebra merge-conflict blocked-by-other-PR blocked on another PR
28686 mitchell-horner feat(Combinatorics/SimpleGraph): prove the Erdős-Stone theorem t-combinatorics merge-conflict blocked-by-other-PR WIP blocked on another PR
28687 mitchell-horner feat(Combinatorics/SimpleGraph): prove the Erdős-Stone-Simonovits theorem t-combinatorics merge-conflict blocked-by-other-PR WIP blocked on another PR
28689 mitchell-horner feat(Combinatorics/SimpleGraph): prove well-known corollaries of the Erdős-Stone-Simonovits theorem t-combinatorics merge-conflict blocked-by-other-PR WIP blocked on another PR
26952 robin-carlier feat(CategoryTheory/DayConvolution): monoid objects internal to day convolutions t-category-theory merge-conflict blocked-by-other-PR blocked on another PR
27133 robin-carlier feat(CategoryTheory/Monoidal/DayConvolution): `C ⊛⥤ V` is monoidal closed when `V` is t-category-theory merge-conflict blocked-by-other-PR blocked on another PR
27151 robin-carlier feat(CategoryTheory/Monoidal/DayConvolution): `C ⊛⥤ V` is braided/symmetric when `C` and `V` are braided/symmetric t-category-theory merge-conflict blocked-by-other-PR blocked on another PR
27175 robin-carlier feat(CategoryTheory/Monoidal/DayConvolution): `LawfulDayConvolutionMonoidalCategoryStruct.ι C V D` is monoidal when the target is `C ⊛⥤ V` t-category-theory merge-conflict blocked-by-other-PR blocked on another PR
26413 michaellee94 feat(Analysis/ODE/MaximalSolution): Existence of maximal solutions for ODE meeting Picard-Lindelöf conditions new-contributor t-analysis merge-conflict awaiting-author blocked-by-other-PR blocked on another PR
25741 robin-carlier feat(AlgebraicTopology/SimplexCategory/SimplicialObject): definitions of simplicial objects by generators and relation t-algebraic-topology large-import t-category-theory merge-conflict blocked-by-other-PR blocked on another PR
27707 FLDutchmann feat(NumberTheory/SelbergSieve): define Selberg's weights and prove basic results. t-analysis t-number-theory merge-conflict blocked-by-other-PR blocked on another PR
27898 grunweg feat: check indentation of doc-strings, basic version t-linter merge-conflict blocked-by-other-PR blocked on another PR
28865 grunweg feat: a map is smooth iff its post-composition with an immersion is t-differential-geometry merge-conflict blocked-by-other-PR WIP blocked on another PR
28905 grunweg feat: immersions are locally embeddings merge-conflict blocked-by-other-PR ⚠️ blocked on another PR
29077 grunweg feat(Manifold/Instances/Icc): golf smoothness proof using immersions merge-conflict blocked-by-other-PR ⚠️ blocked on another PR
28804 grunweg feat: a few more tactic linters t-meta merge-conflict blocked-by-other-PR blocked on another PR
29204 ShreckYe feat(GroupTheory/OrderOfElement): `Pi.orderOf_eq` and its related and depended-upon theorems related to `Pi`, `minimalPeriod`, and `IsPeriodicPt` t-group-theory large-import t-dynamics merge-conflict blocked-by-other-PR blocked on another PR
29243 yoh-tanimoto feat(Analysis/InnerProductSpace/Projection/Submodule): add `sup_orthogonal` for `ClosedSubmodules` merge-conflict blocked-by-other-PR ⚠️ blocked on another PR
29251 yoh-tanimoto feat(Analysis/InnerProductSpace/): define standard subspaces of a complex Hilbert space merge-conflict blocked-by-other-PR ⚠️ blocked on another PR
27950 alreadydone feat(MonoidAlgebra): criteria for `single` to be a unit, irreducible or prime t-algebra merge-conflict blocked-by-other-PR WIP labelled WIP
29764 ScottCarnahan feat (Algebra/Vertex): API up to residue products (WIP) large-import t-algebra blocked-by-other-PR blocked on another PR
29790 robertmaxton42 feat (IsCoherentWith) : families of maps from a coherent collection of subspaces lift uniquely to maps from the total space large-import blocked-by-other-PR ⚠️ blocked on another PR
28067 grunweg Docstring enumerations merge-conflict blocked-by-other-PR blocked on another PR
25900 pfaffelh feat (Topology/Compactness/CompactSystem): Set system of finite unions of sets in a compact system is again a compact system t-topology merge-conflict blocked-by-other-PR blocked on another PR
25906 pfaffelh feat (Topology/Compactness/CompactSystem): Closed and compact square cylinders form a compact system. t-topology merge-conflict blocked-by-other-PR blocked on another PR
26304 Raph-DG feat(AlgebraicGeometry): Definition of algebraic cycles t-algebraic-geometry RFC merge-conflict blocked-by-other-PR blocked on another PR
29934 smmercuri feat(Field/WithAbs): the lift of a ring homomorphism from `WithAbs v` to `WithAbs w` to their completions FLT blocked-by-other-PR WIP ⚠️ blocked on another PR
30001 vihdzp feat: concept generated by set of objects/attributes t-order blocked-by-other-PR blocked on another PR
28786 mitchell-horner feat(Combinatorics/SimpleGraph): restate Turán's theorem in terms of `extremalNumber` t-combinatorics blocked-by-other-PR blocked on another PR
29274 Jlh18 feat(CategoryTheory): HasLimits instance on Grpd new-contributor blocked-by-other-PR ⚠️ blocked on another PR
27391 robin-carlier feat(CategoryTheory/Limits/Shapes/Pullback/Categorical): pseudofunctoriality structure of categorical pullback squares t-category-theory merge-conflict blocked-by-other-PR blocked on another PR
27432 robin-carlier feat(CategoryTheory/Limits/Shapes/Pullback/Categorical): pseudofunctoriality of categorical pulback squares t-category-theory merge-conflict blocked-by-other-PR blocked on another PR
27481 robin-carlier feat(CategoryTheory/Limits/Shapes/Pullback/Categorical): adjunctions and equivalences of categorical pullback squares large-import t-category-theory merge-conflict blocked-by-other-PR blocked on another PR
27686 robin-carlier feat(CategoryTheory/Limits/Shapes/Pullback/Categorical/Square): more API for `CatPullbackSquare` large-import t-category-theory merge-conflict blocked-by-other-PR blocked on another PR
27687 robin-carlier feat(CategoryTheory/Limits/Shapes/Pullback/Categorical): squares equivalent to a `CatPullbackSquare` large-import t-category-theory merge-conflict blocked-by-other-PR blocked on another PR
27688 robin-carlier feat(CategoryTheory/Limits/Shapes/Pullback/Categorical): coherence statement for `CatPullbackSquare.inverse` large-import t-category-theory merge-conflict blocked-by-other-PR blocked on another PR
27689 robin-carlier feat(CategoryTheory/Limits/Shapes/Pullback/Categorical): horizontal pasting calculus for `CatPullbackSquare` large-import t-category-theory merge-conflict blocked-by-other-PR blocked on another PR
27690 robin-carlier feat(CategoryTheory/Limits/Shapes/Pullback/Categorical): vertical pasting calculus for `CatPullbackSquare` large-import t-category-theory merge-conflict blocked-by-other-PR blocked on another PR
27740 robin-carlier feat(CategoryTheory/Limits/Shapes/Pullback/Categorical): pasting calculus for `CategoricalPullback` large-import t-category-theory merge-conflict blocked-by-other-PR blocked on another PR
30077 agjftucker feat(Analysis/Calculus/ImplicitFunOfBivariate): define implicitFunOfBivariate t-analysis blocked-by-other-PR blocked on another PR
26942 pechersky feat(RingTheory/Valuation/ValueGroupIso): isomorphism of value groups when compatible t-ring-theory t-order blocked-by-other-PR blocked on another PR
29792 robertmaxton42 feat (RelCWComplex): a (relative, concrete) CW complex is the colimit of its skeleta large-import blocked-by-other-PR ⚠️ blocked on another PR
26579 robin-carlier feat(CategoryTheory/Limits/Pullbacks/Categorical/CatCospanTransform): equivalences of categorical cospans large-import t-category-theory merge-conflict blocked-by-other-PR blocked on another PR
23040 grunweg feat: define immersions and smooth embeddings in infinite dimensions t-differential-geometry merge-conflict blocked-by-other-PR WIP blocked on another PR
27634 agjftucker fix(Analysis/Calculus/Implicit): consistently rename {`map`, `fun`, `function`} to `fun` t-analysis merge-conflict blocked-by-other-PR blocked on another PR
27366 101damnations feat(RepresentationTheory/Homological/GroupCohomology/Hilbert90): add Hilbert 90 for cyclic groups large-import t-algebra merge-conflict blocked-by-other-PR blocked on another PR
28244 robin-carlier feat(CategoryTheory/Bicategory/NaturalTransformation): Icons large-import t-category-theory awaiting-CI merge-conflict blocked-by-other-PR WIP blocked on another PR
28245 robin-carlier feat(CategoryTheory/Bicategory/NaturalTransformation/Icon): strict associativity and unitality of icon composition large-import t-category-theory awaiting-CI merge-conflict blocked-by-other-PR WIP blocked on another PR
28718 imbrem Added chosen finite coproducts new-contributor t-category-theory awaiting-author blocked-by-other-PR blocked on another PR
23177 faenuccio feat: more lemmas about ordered groups with zero large-import t-order awaiting-CI blocked-by-other-PR WIP blocked on another PR
25740 robin-carlier feat(AlgebraicTopology/SimplexCategory/GeneratorsRelations): `SimplexCategoryGenRel.toSimplexCategory` is an equivalence t-algebraic-topology large-import merge-conflict blocked-by-other-PR blocked on another PR
30185 alreadydone feat(MathlibTest): kernel reduction of nsmul on elliptic curve over ZMod t-algebra t-algebraic-geometry t-number-theory blocked-by-other-PR blocked on another PR
26886 pechersky feat(NumberTheory/Padics/ValuativeRel): ValuativeRel ℚ_[p] t-algebra t-analysis t-number-theory merge-conflict blocked-by-other-PR WIP blocked on another PR
27314 pechersky feat(TopologyValued): `Valued` based on a range topology t-topology merge-conflict blocked-by-other-PR blocked on another PR
25143 chrisflav feat(RingTheory): smooth algebras have smooth Noetherian models t-ring-theory merge-conflict blocked-by-other-PR blocked on another PR
30112 gaetanserre feat(Probability.Kernel): add representation of kernel as a map of a uniform measure t-measure-probability blocked-by-other-PR blocked on another PR
27694 grunweg feat: Gram-Schmidt orthonormalisation preserves continuity of sections t-differential-geometry blocked-by-other-PR blocked on another PR
27025 grunweg feat: Gram-Schmidt procedure on smooth vector bundles yields smooth sections t-differential-geometry blocked-by-other-PR blocked on another PR
16553 grunweg WIP: tinkering with orientable manifolds t-differential-geometry merge-conflict blocked-by-other-PR WIP blocked on another PR
30334 kckennylau feat(RingTheory): define maps of homogeneous ideals t-ring-theory blocked-by-other-PR blocked on another PR
30312 kckennylau feat(RingTheory): define graded ring homomorphisms t-ring-theory blocked-by-other-PR blocked on another PR
30365 kckennylau feat(RingTheory): define R-linear graded algebra homomorphism blocked-by-other-PR ⚠️ blocked on another PR
30367 kckennylau feat(Data): define grading-preserving isomorphisms t-data blocked-by-other-PR blocked on another PR
30010 xroblot feat(CyclotomicFields): generalize `IsPrimitiveRoot.integralPowerBasis` to all (nonzero) integers large-import t-number-theory merge-conflict blocked-by-other-PR blocked on another PR
30379 kckennylau feat(RingTheory): isomorphism of graded rings blocked-by-other-PR ⚠️ blocked on another PR
28328 pechersky chore(Topology/Valued): golf using local finite order of WithZeroTopology large-import t-algebra t-topology t-number-theory merge-conflict blocked-by-other-PR blocked on another PR
29282 Jlh18 feat(CategoryTheory): HasColimits instance on Grpd new-contributor merge-conflict blocked-by-other-PR ⚠️ blocked on another PR
30356 grunweg feat: follow-up to #28793 t-differential-geometry blocked-by-other-PR blocked on another PR
28796 grunweg feat: immersions are smooth t-differential-geometry blocked-by-other-PR WIP blocked on another PR
26966 vihdzp feat: the Dedekind–MacNeille completion t-order awaiting-author blocked-by-other-PR blocked on another PR
28853 grunweg feat: product of immersions is an immersion t-differential-geometry blocked-by-other-PR blocked on another PR
29387 mans0954 feat(Analysis/LocallyConvex/WeakSpace): toWeakSpace_closedAbsConvexHull_eq t-analysis merge-conflict blocked-by-other-PR blocked on another PR
30504 grunweg feat: add custom elaborators for immersions t-differential-geometry merge-conflict blocked-by-other-PR blocked on another PR
30610 grunweg feat: yet another lemma about differentiability of parametric integrals t-analysis blocked-by-other-PR blocked on another PR
28152 Sebi-Kumar feat(AlgebraicTopology): characterize simply connectedness in terms of loops t-algebraic-topology new-contributor merge-conflict blocked-by-other-PR blocked on another PR
28246 Sebi-Kumar feat(AlgebraicTopology/FundamentalGroupoid): the n-sphere is simply connected for n > 1 t-algebraic-topology new-contributor merge-conflict blocked-by-other-PR blocked on another PR
29000 JovanGerb feat(Tactic/Push): add basic tags and tests merge-conflict blocked-by-other-PR ⚠️ blocked on another PR
30658 grunweg chore: rebase and continuation of #26926 (more spacing fixes) large-import merge-conflict blocked-by-other-PR blocked on another PR
28700 Timeroot feat(ModelTheory): Set.Definable is transitive large-import t-logic merge-conflict blocked-by-other-PR blocked on another PR
27100 staroperator feat(ModelTheory): Presburger definability and semilinear sets t-logic merge-conflict blocked-by-other-PR blocked on another PR
30925 callesonne feat(Bicategory/InducedBicategory): add induced bicategories t-category-theory blocked-by-other-PR blocked on another PR
27510 chrisflav feat(RingTheory/Height): height of ideal is height of preimage plus height in quotient t-ring-theory large-import merge-conflict blocked-by-other-PR blocked on another PR
30898 vihdzp feat: characterization of `List.splitBy` large-import t-data merge-conflict blocked-by-other-PR blocked on another PR
26872 faenuccio chore(RingTheory/Valuation/RankOne): modify the definition of Valuation.RankOne using its range rather than its codomain t-algebra awaiting-author blocked-by-other-PR blocked on another PR
30985 erdOne feat(AlgbraicGeometry), `Hom(-, X)` commutes with inverse limits for schemes of finite presentation large-import t-algebraic-geometry 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 ⚠️ blocked on another PR
30462 grunweg Everything I wanted about immersions merge-conflict blocked-by-other-PR blocked on another PR
30981 jsm28 feat(Geometry/Euclidean/Angle/Bisector): oriented angle bisection mod π large-import t-euclidean-geometry blocked-by-other-PR blocked on another PR
30982 jsm28 feat(Geometry/Euclidean/Angle/Incenter): angle bisection and the incenter large-import t-euclidean-geometry blocked-by-other-PR blocked on another PR
30303 franv314 chore(Topology/Instances): add deprecated module new-contributor merge-conflict blocked-by-other-PR blocked on another PR
30357 grunweg chore: golf using custom elaborators awaiting-bench t-differential-geometry merge-conflict blocked-by-other-PR blocked on another PR
30900 vihdzp feat: run-length encoding large-import t-data merge-conflict blocked-by-other-PR blocked on another PR
26061 kckennylau (WIP) feat(AlgebraicGeometry): define Projective Space t-algebraic-geometry blocked-by-other-PR WIP blocked on another PR
26860 Thmoas-Guan feat(Algebra): Define associated graded module t-algebra blocked-by-other-PR blocked on another PR
30399 kckennylau feat(RingTheory): make HomogeneousLocalization.map take a graded ring hom merge-conflict blocked-by-other-PR ⚠️ blocked on another PR
31019 vihdzp feat: colex order on finsupps blocked-by-other-PR ⚠️ blocked on another PR
30649 loefflerd feat(NumberTheory/ModularForms): adjoin -1 to a subgroup t-number-theory blocked-by-other-PR blocked on another PR
26858 Thmoas-Guan feat(Algebra): Define the associated graded ring to filtered ring t-algebra blocked-by-other-PR blocked on another PR
26859 Thmoas-Guan feat(Algebra): Define associated graded algebra t-algebra blocked-by-other-PR blocked on another PR
26861 Thmoas-Guan feat(Algebra): define filtered add group hom t-algebra blocked-by-other-PR blocked on another PR
26862 Thmoas-Guan feat(Algebra): define filtered ring homomorphism t-algebra blocked-by-other-PR blocked on another PR
26863 Thmoas-Guan feat(Algebra): define filtered alghom t-algebra blocked-by-other-PR blocked on another PR
26867 Thmoas-Guan feat(Algebra): filtered module hom t-algebra blocked-by-other-PR blocked on another PR
26868 Thmoas-Guan feat(Algebra): associated graded exact of exact and strict t-algebra blocked-by-other-PR blocked on another PR
26869 Thmoas-Guan feat(Algebra): exact of associated graded exact t-algebra blocked-by-other-PR blocked on another PR
30579 smmercuri feat : `v.adicCompletionIntegers K` is compact when `K` is a number field merge-conflict blocked-by-other-PR WIP ⚠️ blocked on another PR
30766 dagurtomas feat(CategoryTheory): transport closed monoidal structure along equivalence file-removed blocked-by-other-PR ⚠️ blocked on another PR
30329 luigi-massacci feat(Analysis/Distribution/TestFunction): integrating against a measure as a continuous linear map on test functions merge-conflict blocked-by-other-PR ⚠️ blocked on another PR*
30328 luigi-massacci feat(Analysis/Distribution/TestFunction): the inclusion of test functions into bounded continuous functions as a continuous linear map merge-conflict blocked-by-other-PR ⚠️ blocked on another PR
30327 luigi-massacci feat(Analysis/Distribution/TestFunction): add characterizations of continuity for linear maps on test functions merge-conflict blocked-by-other-PR ⚠️ blocked on another PR
30325 luigi-massacci feat(Analysis/Distribution/TestFunction): Endow test functions with the canonical LF topology merge-conflict blocked-by-other-PR ⚠️ blocked on another PR
30278 luigi-massacci feat: compactly supported C^n bundled maps ("test functions") t-analysis merge-conflict blocked-by-other-PR blocked on another PR
30255 luigi-massacci feat(Analysis/Distribution/ContDiffMapSupportedIn): specialize singleton seminorm family for D_K^n when n finite merge-conflict blocked-by-other-PR ⚠️ blocked on another PR
30253 luigi-massacci feat(Analysis/Distribution/ContDiffMapSupportedIn): Add a wrapper for iteratedFDeriv on the type of bundled smooth compactly supported maps merge-conflict blocked-by-other-PR ⚠️ blocked on another PR
30240 luigi-massacci feat(Analysis/Distribution/ContDiffMapSupportedIn): Add a wrapper for fderiv on D_K^n merge-conflict blocked-by-other-PR ⚠️ blocked on another PR
30239 luigi-massacci feat(Analysis/Distribution/ContDiffMapSupportedIn): Add characterization of continuity for maps into D_K^n, continuity of inclusion into C_b merge-conflict blocked-by-other-PR ⚠️ blocked on another PR
27980 smmercuri feat: dimensions of completions at infinite place extensions large-import FLT t-number-theory merge-conflict blocked-by-other-PR blocked on another PR
31056 jsm28 feat(Geometry/Euclidean/Altitude): `reindex` lemmas t-euclidean-geometry blocked-by-other-PR blocked on another PR
31057 jsm28 feat(Geometry/Euclidean/Incenter): `reindex` lemmas t-euclidean-geometry blocked-by-other-PR blocked on another PR
30342 joelriou feat(Algebra/Category/ModuleCat/Sheaf): compatibilities of pushforward and pullbacks on sheaves of modules t-category-theory blocked-by-other-PR WIP blocked on another PR
30482 vihdzp feat: colex order on (dependent) finsupps t-order blocked-by-other-PR blocked on another PR
29996 vihdzp chore(Order/Concept): `IsIntent` and `IsExtent` t-order blocked-by-other-PR blocked on another PR
29942 smmercuri feat(InfinitePlace/Completion): embeddings of `w.Completion` factor through embeddings of `v.Completion` when `w` extends `v` FLT merge-conflict blocked-by-other-PR ⚠️ blocked on another PR
30551 smmercuri feat: dimension formulae for infinite places above blocked-by-other-PR WIP ⚠️ blocked on another PR
30350 joelriou feat(AlgebraicGeometry): the pseudofunctor which sends a scheme to its category of sheaves of modules large-import t-algebraic-geometry blocked-by-other-PR blocked on another PR
31076 mcdoll feat(Analysis/InnerProductSpace): extension to linear isometry equivalence t-analysis blocked-by-other-PR blocked on another PR
29948 mcdoll feat(Analysis/Fourier): the Fourier transform on L^2 merge-conflict blocked-by-other-PR ⚠️ blocked on another PR
30352 kckennylau (WIP) feat(RingTheory): Homogeneous localization of tensor product merge-conflict blocked-by-other-PR WIP blocked on another PR
31078 AntoineChambert-Loir feat:(LinearAlgebra/SpecialLinearGroup) : center of the special linear group of a module t-algebra blocked-by-other-PR blocked on another PR
19475 YaelDillies feat: group markings t-algebra blocked-by-other-PR WIP blocked on another PR
31108 grunweg Immersions nochoice t-differential-geometry blocked-by-other-PR WIP blocked on another PR
30811 yonggyuchoimath feat(AlgebraicGeometry.EffectiveEpi): effective epimorphisms in schemes merge-conflict blocked-by-other-PR ⚠️ blocked on another PR
31135 kckennylau feat(RingTheory): is localization iff is localization on saturation blocked-by-other-PR ⚠️ blocked on another PR
31141 peabrainiac feat(Analysis/Calculus): parametric integrals over smooth functions are smooth t-analysis blocked-by-other-PR blocked on another PR
29309 LLaurance feat(Combinatorics): any connected graph contains a vertex that leaves the graph preconnected if removed large-import new-contributor t-combinatorics awaiting-author blocked-by-other-PR blocked on another PR
31152 FernandoChu feat(CategoryTheory): regular categories have strong-epi-mono factorisations large-import t-category-theory blocked-by-other-PR blocked on another PR
26377 Whysoserioushah feat(RingTheory/SimpleRing/TensorProduct): tensor product of a simple algebra and a central simple algebra is simple t-ring-theory merge-conflict blocked-by-other-PR blocked on another PR
31205 jsm28 feat(Analysis/Convex/Side): affine combinations and sides of faces of a simplex t-convex-geometry blocked-by-other-PR blocked on another PR
30871 urkud feat(DifferentialForm): pullback commutes with exterior derivative t-analysis merge-conflict blocked-by-other-PR blocked on another PR
29774 Raph-DG feat(AlgebraicGeometry): Order of vanishing of elements of the function field of locally noetherian, integral schemes file-removed merge-conflict blocked-by-other-PR ⚠️ blocked on another PR
25834 Rida-Hamadani feat(SimpleGraph): girth-diameter inequality t-combinatorics merge-conflict blocked-by-other-PR WIP blocked on another PR
25273 YaelDillies refactor: make `MonoidAlgebra` into a one-field structure toric large-import t-algebra blocked-by-other-PR WIP blocked on another PR
30927 callesonne feat(Bicategory/Yoneda): add the yoneda pseudofunctor merge-conflict blocked-by-other-PR ⚠️ blocked on another PR
31169 callesonne feat(Bicategory/Product): add products of bicategories t-category-theory merge-conflict blocked-by-other-PR blocked on another PR
30736 alreadydone feat(RingTheory): Picard group of a domain is isomorphic to ClassGroup large-import t-algebra blocked-by-other-PR blocked on another PR
25903 pfaffelh feat(MeasureTheory): finite unions of sets in a semi-ring (in terms of measure theory) form a ring large-import t-measure-probability merge-conflict blocked-by-other-PR blocked on another PR
29365 staroperator feat(SetTheory/ZFC): add `ZFSet.card` t-set-theory blocked-by-other-PR blocked on another PR
31162 AntoineChambert-Loir feat(LinearAlgebra/Dual/BaseChange): base change of a linear form (on the Module.Dual) blocked-by-other-PR ⚠️ blocked on another PR
23460 Timeroot feat: Definition of `Clone` t-algebra blocked-by-other-PR blocked on another PR
30190 joelriou feat(CategoryTheory/Sites): functoriality of descent data t-category-theory blocked-by-other-PR WIP blocked on another PR
30926 callesonne feat(Bicategory/Functorbicategory): define bicategory of pseudofunctors t-category-theory merge-conflict blocked-by-other-PR blocked on another PR
31079 mcdoll feat(Analysis/ContDiff): smooth compactly supported functions are dense in Lp t-analysis blocked-by-other-PR blocked on another PR
30339 grunweg feat: extend a tangent vector for a locally smooth vector field t-differential-geometry blocked-by-other-PR blocked on another PR
31339 grunweg Movelemma blocked-by-other-PR blocked on another PR
31338 grunweg chore: move Pretrivialization, Trivialization to the Bundle namespace t-differential-geometry blocked-by-other-PR blocked on another PR
30640 SnirBroshi feat(Combinatorics/SimpleGraph/Acyclic): a maximally acyclic graph is a tree blocked-by-other-PR ⚠️ blocked on another PR
30189 joelriou feat(CategoryTheory/Sites): descent data t-category-theory blocked-by-other-PR WIP blocked on another PR
28685 mitchell-horner feat(Combinatorics/SimpleGraph): prove the minimal-degree version of the Erdős-Stone theorem t-combinatorics merge-conflict blocked-by-other-PR WIP blocked on another PR
25841 mitchell-horner feat(Combinatorics/SimpleGraph): prove the Kővári–Sós–Turán theorem t-combinatorics merge-conflict blocked-by-other-PR WIP blocked on another PR
26184 vasnesterov feat(Topology): every compact metric space is image of Cantor set large-import t-topology merge-conflict blocked-by-other-PR blocked on another PR
31018 joelriou feat(CategoryTheory): the κ-accessible category of κ-directed posets large-import t-category-theory merge-conflict blocked-by-other-PR WIP blocked on another PR
30089 loefflerd feat(NumberTheory/ModularForms): Bounds on modular forms and q-expansion coeffs large-import t-number-theory blocked-by-other-PR WIP blocked on another PR
27433 YaelDillies refactor: make `⇑e⁻¹ = ⇑e.symm` simp CFT blocked-by-other-PR blocked on another PR
30817 joelriou feat(CategoryTheory): `κ`-continuous presheaves large-import t-category-theory blocked-by-other-PR WIP blocked on another PR
30464 joelriou feat(CategoryTheory): κ-presentable objects in a κ-accessible category is an essentially small category large-import t-category-theory blocked-by-other-PR WIP blocked on another PR
30755 joelriou feat(CategoryTheory): presentable objects form a dense subcategory large-import t-category-theory blocked-by-other-PR WIP blocked on another PR
31137 joelriou feat(CategoryTheory): an accessible category is essentially large large-import t-category-theory blocked-by-other-PR WIP blocked on another PR
30533 joelriou feat(CategoryTheory): presentable objects and adjunctions large-import t-category-theory blocked-by-other-PR WIP blocked on another PR
30731 joelriou feat(CategoryTheory/Presentable): transport via an equivalence large-import t-category-theory blocked-by-other-PR WIP blocked on another PR
30507 joelriou feat(CategoryTheory): MorphismProperty.isLocal is closed under `κ`-filtered colimits large-import t-category-theory blocked-by-other-PR WIP blocked on another PR
30459 joelriou refactor(CategoryTheory/Presentable): cleaning up HasCardinalFilteredGenerator(s) t-category-theory blocked-by-other-PR WIP blocked on another PR
30241 joelriou feat(CategoryTheory): locally presentable categories and strong generators large-import t-category-theory blocked-by-other-PR WIP blocked on another PR
30513 joelriou feat(CategoryTheory): orthogonal-reflection construction: existence of the left adjoint large-import t-category-theory blocked-by-other-PR WIP blocked on another PR
30554 joelriou feat(CategoryTheory): localization of locally presentable categories large-import t-category-theory blocked-by-other-PR WIP blocked on another PR
30847 joelriou feat(CategoryTheory/Presentable): the representation theorem large-import t-category-theory blocked-by-other-PR WIP blocked on another PR
30247 joelriou feat(CategoryTheory): categories of presheaves are locally presentable large-import t-category-theory blocked-by-other-PR WIP blocked on another PR
31083 joelriou feat(CategoryTheory): properties of objects for pseudofunctors to Cat t-category-theory blocked-by-other-PR WIP blocked on another PR
27378 peakpoint refactor(Geometry/Euclidean/Projection): redefine projection and reflection for affine subspaces new-contributor t-euclidean-geometry blocked-by-other-PR blocked on another PR
29777 yuanyi-350 feat(Functional Analysis) : Closed Range Theorem large-import new-contributor t-analysis awaiting-author blocked-by-other-PR WIP blocked on another PR
27953 CoolRmal feat(ProbabilityTheory): Conditional Jensen's Inequality new-contributor t-measure-probability blocked-by-other-PR blocked on another PR
31187 loefflerd feat(NumberTheory/LSeries): Define the L-series of a modular form large-import t-number-theory blocked-by-other-PR WIP blocked on another PR
31411 CoolRmal feat : a convex lower-semicontinuous function is the supremum of a sequence of affine functions in a separable space new-contributor t-analysis blocked-by-other-PR blocked on another PR
31274 joelriou feat(AlgebraicTopology): edges and "triangles" in the nerve of a category t-algebraic-topology blocked-by-other-PR WIP blocked on another PR
31174 joelriou refactor(AlgebraicTopology): refactor the homotopy category and the nerve adjunction t-algebraic-topology blocked-by-other-PR WIP blocked on another PR
31325 joelriou feat(AlgebraicTopology): a computable monoidal functor instance for `hoFunctor` t-algebraic-topology blocked-by-other-PR blocked on another PR
31426 joelriou feat(CategoryTheory): DiagramWithUniqueTerminal t-category-theory blocked-by-other-PR WIP blocked on another PR
30605 joelriou feat(CategoryTheory): for any filtered category, there exists a final functor from a directed poset t-category-theory blocked-by-other-PR WIP blocked on another PR
29203 Hagb feat(RingTheory/MvPolynomial/Groebner) : add Gröbner basis t-ring-theory large-import blocked-by-other-PR blocked on another PR
28462 joelriou feat(AlgebraicTopology/SimplicialSet): the relative cell complex attached to a rank function for a pairing t-algebraic-topology merge-conflict blocked-by-other-PR WIP blocked on another PR
25825 yuma-mizuno feat(CategoryTheory/Bicategory): define lax transformations between oplax functors large-import t-category-theory blocked-by-other-PR blocked on another PR
30567 wwylele feat(Combinatorics): generating function for partitions file-removed t-combinatorics blocked-by-other-PR blocked on another PR
28351 joelriou feat(AlgebraicTopology/SimplicialSet): the rank function with values in natural numbers of a regular pairing t-algebraic-topology blocked-by-other-PR WIP blocked on another PR
30576 smmercuri feat: `adicCompletion` for `Rat` is uniform isomorphic to `Padic` blocked-by-other-PR WIP ⚠️ blocked on another PR
31034 chrisflav feat(RingTheory/Extension/Cotangent): basis of free cotangent space can be realized as a presentation t-ring-theory merge-conflict blocked-by-other-PR blocked on another PR
31081 chrisflav feat(RingTheory/StandardSmooth): presentation independent characterization t-ring-theory merge-conflict blocked-by-other-PR blocked on another PR
31165 AntoineChambert-Loir feat(LinearAlgebra/Transvection): base change of transvections large-import t-algebra blocked-by-other-PR blocked on another PR
31500 zcyemi feat(Analysis/Convex/Between): add lemmas on affine independence under strict betweenness blocked-by-other-PR ⚠️ blocked on another PR
27414 staroperator feat(ModelTheory): Semilinear sets are closed under intersection, difference and complement t-logic blocked-by-other-PR blocked on another PR
26388 jjdishere feat(RingTheory/Perfectoid): Fontaine's theta map and the de Rham period rings t-ring-theory t-algebra t-number-theory blocked-by-other-PR blocked on another PR
26384 jjdishere feat(RingTheory/Perfectoid): Fontaine's theta map is surjective t-algebra t-number-theory blocked-by-other-PR labelled WIP
30375 sinhp feat(CategoryTheory): Basics of Locally Cartesian Closed Categories t-category-theory merge-conflict blocked-by-other-PR WIP blocked on another PR
30202 luigi-massacci feat(Analysis/Distribution/ContDiffMapSupportedIn): Add TopologicalSpace and LocallyConvexSpace instances. t-analysis blocked-by-other-PR blocked on another PR
28972 themathqueen feat(LinearAlgebra/Matrix): star-algebra automorphisms on matrices are unitarily inner t-algebra merge-conflict blocked-by-other-PR blocked on another PR
31409 SnirBroshi feat(Analysis/SpecialFunctions/Gamma/BohrMollerup): the Gamma function has a minimum in (1, 2) t-analysis blocked-by-other-PR blocked on another PR
30236 luigi-massacci feat(Analysis/Distribution/ContDiffMapSupportedIn): Add withSeminorms instance. t-analysis blocked-by-other-PR blocked on another PR
31138 AntoineChambert-Loir feat(LinearAlgebra/Transvection): the determinant of transvection in a module is equal to 1 large-import t-algebra blocked-by-other-PR blocked on another PR
31452 jsm28 feat(Analysis/Convex/StrictCombination): convex combinations in strictly convex sets and spaces t-convex-geometry blocked-by-other-PR blocked on another PR
31495 jsm28 feat(Geometry/Euclidean/Sphere/SecondInter): `secondInter` and sides of faces of a simplex t-euclidean-geometry blocked-by-other-PR blocked on another PR
26213 Thmoas-Guan feat(Algebra): Ext iso quotient regular sequence large-import t-algebra blocked-by-other-PR blocked on another PR
26214 Thmoas-Guan feat(Algebra): definition of depth large-import t-algebra blocked-by-other-PR blocked on another PR
26215 Thmoas-Guan feat(Algebra): Auslander–Buchsbaum theorem large-import t-algebra blocked-by-other-PR blocked on another PR
26351 RemyDegenne feat: covering and packing numbers of sets in a metric space t-topology awaiting-author blocked-by-other-PR blocked on another PR
26216 Thmoas-Guan feat(Algebra): depth of QuotSMulTop large-import t-algebra blocked-by-other-PR blocked on another PR
26217 Thmoas-Guan feat(Algebra): Ischebeck theorem large-import t-algebra blocked-by-other-PR blocked on another PR
26218 Thmoas-Guan feat(Algebra): definition of cohen macaulay large-import t-algebra blocked-by-other-PR blocked on another PR
26245 Thmoas-Guan feat(Algebra): cohen macaulay local ring is catenary large-import t-algebra blocked-by-other-PR WIP blocked on another PR
26957 Thmoas-Guan feat(Algebra): unmixed thm of Cohen-Macaulay ring large-import t-algebra blocked-by-other-PR blocked on another PR
28684 Thmoas-Guan feat(RingTheory) : definition of regular ring t-ring-theory blocked-by-other-PR WIP blocked on another PR
28683 Thmoas-Guan feat(RingTheory) : regular local ring is domain t-ring-theory blocked-by-other-PR WIP blocked on another PR
29533 Thmoas-Guan feat(Algebra): maximal Cohen Macaulay module large-import blocked-by-other-PR ⚠️ blocked on another PR*
29557 Thmoas-Guan feat(Algebra): finite projective dimension of regular large-import blocked-by-other-PR ⚠️ blocked on another PR
29670 Thmoas-Guan feat(Algebra): projective dimension equal supremum of localized module t-ring-theory blocked-by-other-PR blocked on another PR
29534 Thmoas-Guan feat(Algebra): global dimension of regular local ring large-import blocked-by-other-PR ⚠️ blocked on another PR
29699 Thmoas-Guan feat(Algebra/RingTheory) : Global dimension of regular ring large-import 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
29703 Thmoas-Guan feat(Algebra/RingTheory): Hilbert's Syzygy theorem (projective version) large-import blocked-by-other-PR ⚠️ blocked on another PR
29796 Thmoas-Guan feat(RingTheory) : regular of finite global dimension large-import blocked-by-other-PR ⚠️ blocked on another PR
29802 Thmoas-Guan feat(Algebra/RingTheory) : Auslander–Buchsbaum–Serre criterion and its corollaries large-import blocked-by-other-PR ⚠️ blocked on another PR
30309 luigi-massacci feat(Analysis/Distribution/TestFunction): Add module instance to TestFunction merge-conflict blocked-by-other-PR ⚠️ blocked on another PR
30799 YaelDillies refactor: unify the two versions of `pow_eq_one_iff` large-import t-algebra awaiting-CI blocked-by-other-PR blocked on another PR
26291 RemyDegenne feat(Probability): Cameron-Martin theorem t-measure-probability merge-conflict blocked-by-other-PR WIP blocked on another PR*
31513 FLDutchmann feat(Tactic): `polynomial` tactic t-meta blocked-by-other-PR blocked on another PR
30563 YaelDillies chore(Algebra): replace `NoZeroSMulDivisors` with `Module.IsTorsionFree` large-import t-algebra blocked-by-other-PR WIP blocked on another PR
31350 grunweg feat: (unoriented) bordism groups t-differential-geometry blocked-by-other-PR WIP blocked on another PR
31561 EtienneC30 feat: monotonicity of Holderianity t-topology blocked-by-other-PR blocked on another PR
30920 callesonne feat(Category/Grpd): define the bicategory of groupoids t-category-theory blocked-by-other-PR blocked on another PR
31567 EtienneC30 feat: characteristic function of a Gaussian measure blocked-by-other-PR ⚠️ blocked on another PR
30921 EtienneC30 feat: characterizing Gaussian measures through the shape of the characteristic function t-measure-probability blocked-by-other-PR blocked on another PR
30744 grunweg feat: more extensions for differential geometry elaborators t-differential-geometry t-meta blocked-by-other-PR blocked on another PR
30463 grunweg feat: support products and disjoint unions in the differential geometry elaborators t-differential-geometry t-meta blocked-by-other-PR blocked on another PR
30872 rudynicolop feat(Computability/NFA): NFA closure under concatenation t-computability new-contributor blocked-by-other-PR blocked on another PR
31492 fcoUnda Nthroot improvement new-contributor t-analysis awaiting-author blocked-by-other-PR blocked on another PR
30258 imbrem feat(CategoryTheory/Monoidal): to_additive for proofs using `monoidal` large-import new-contributor merge-conflict blocked-by-other-PR ⚠️ blocked on another PR
30260 imbrem feat(CategoryTheory/Monoidal): added CocartesianMonoidalCategory large-import new-contributor merge-conflict blocked-by-other-PR ⚠️ blocked on another PR
29819 mcdoll feat(Analysis/Distribution): tempered distributions t-analysis merge-conflict blocked-by-other-PR WIP blocked on another PR
31568 joelriou feat(CategoryTheory/Triangulated): truncation functors for t-structures large-import t-category-theory blocked-by-other-PR WIP blocked on another PR
31565 EtienneC30 feat: characteristic function equals dual characteristic function blocked-by-other-PR ⚠️ blocked on another PR
26973 peabrainiac feat(Geometry/Diffeology): diffeologies generated from sets of plots t-differential-geometry merge-conflict blocked-by-other-PR blocked on another PR
27274 peabrainiac feat(Geometry/Diffeology): continuous diffeologies & D-topology-lemmas t-differential-geometry merge-conflict blocked-by-other-PR blocked on another PR
31588 joelriou feat(CategoryTheory/ComposableArrows): compositions of 1 or 2 morphisms t-category-theory blocked-by-other-PR WIP blocked on another PR
31586 joelriou feat(CategoryTheory/Triangulated): spectral objects t-category-theory blocked-by-other-PR WIP blocked on another PR
31455 kim-em feat: products of locally contractible spaces t-topology blocked-by-other-PR blocked on another PR
31508 FLDutchmann feat(Tactic): `algebra` tactic. t-meta blocked-by-other-PR blocked on another PR
30931 Thmoas-Guan feat(RingTheory): Gorenstein local ring large-import merge-conflict blocked-by-other-PR ⚠️ blocked on another PR
31560 AntoineChambert-Loir feat(Topology/Sion): the minimax theorem of von Neumann - Sion large-import blocked-by-other-PR ⚠️ blocked on another PR
25797 dagurtomas feat(Condensed): closed symmetric monoidal structure on light condensed modules large-import t-condensed merge-conflict blocked-by-other-PR blocked on another PR
30532 Thmoas-Guan feat(Homology) : `Ext` commute with flat base change large-import merge-conflict awaiting-author blocked-by-other-PR WIP ⚠️ blocked on another PR
31222 Thmoas-Guan feat(Algebra): `Hom` commute with flat base change large-import merge-conflict blocked-by-other-PR ⚠️ blocked on another PR
31368 dagurtomas feat(Condensed): characterize internal projectivity large-import merge-conflict blocked-by-other-PR ⚠️ blocked on another PR
31580 grunweg feat: towards `ContMDiff` support in fun_prop t-differential-geometry t-meta blocked-by-other-PR WIP blocked on another PR
31406 JovanGerb feat(push_neg): `push_neg +distrib` syntax t-meta blocked-by-other-PR blocked on another PR
31478 BGuillemet feat(CategoryTheory/Sites): `uliftYoneda` for sheaves over a subcanonical topology t-category-theory merge-conflict blocked-by-other-PR blocked on another PR
31059 gasparattila feat(Topology/Sets): define the Vietoris topology on `(Nonempty)Compacts` blocked-by-other-PR ⚠️ blocked on another PR
28468 alreadydone feat(Algebra): ring API for `AddLocalization` t-algebra merge-conflict blocked-by-other-PR blocked on another PR
31364 YaelDillies feat: binomial random graphs t-measure-probability t-combinatorics blocked-by-other-PR blocked on another PR
31610 rudynicolop feat(Computability/NFA): Kleene star closure for Regular Languages via NFA t-computability new-contributor blocked-by-other-PR blocked on another PR