Why is my PR not on the queue?

This page was last updated on: December 05, 2025 at 08:15 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
9469 dupuisf feat: maximum modulus principle for functions vanishing at infinity t-analysis 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
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
13163 erdOne feat(.vscode/module-docstring.code-snippet): Prevent auto-complete from firing on `do` t-meta 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
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
20459 Ruben-VandeVelde chore: fix names of roots_C_mul_X_{add,sub}_C_of_IsUnit t-algebra awaiting-author awaiting author
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
15355 adomani feat: MiM PR report WIP ⚠️ labelled WIP
21495 alreadydone experiment: reducible HasQuotient.quotient' bench-after-CI WIP labelled WIP
21501 sksgurdldi feat(List): add sum_zipWith_eq_finset_sum new-contributor t-algebra 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
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
22888 plp127 perf: replace `Lean.Expr.swapBVars` with a better? implementation t-meta awaiting-author awaiting author
24000 YaelDillies feat: correspondence between Hopf algebras and affine group schemes toric FLT t-algebraic-geometry WIP labelled WIP
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
18861 YaelDillies refactor: make `Set.mem_graphOn` defeq t-data awaiting-author failing CI
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
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
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
24065 kim-em chore: script to give topological sort of modules awaiting-author awaiting author
25473 adomani feat(CI): check that Mathlib files have lean or md extension CI delegated delegated
23929 meithecatte feat(Computability/NFA): improve bound on pumping lemma awaiting-zulip t-computability new-contributor awaiting a zulip discussion
21344 kbuzzard chore: attempt to avoid diamond in OreLocalization t-algebra please-adopt looking for help
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
25993 Multramate feat(Algebra/Group/Units/Hom): add map lemmas t-algebra awaiting-author awaiting author
20784 eric-wieser fix: prevent `exact?` recursing forever on `n = 55` t-set-theory failing CI
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
27435 callesonne feat(Normed/Algebra/Logarithm): add FormalMultilinearSeries of logarithm around `1` t-analysis WIP labelled WIP
27507 grunweg wip(commandStart): check the indentation of declaration keywords also t-linter WIP labelled WIP
27704 vihdzp feat: link `Minimal` and `IsLeast` together t-order awaiting-author failing CI
27813 javra feat: IMO 2025 Q1 IMO WIP labelled WIP
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
28075 tristan-f-r chore(Finsupp/Indicator): make non-classical t-data easy awaiting-author awaiting author
27444 grunweg feat: generalise more lemmas to enorms carleson WIP ⚠️ labelled WIP
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
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
28631 faenuccio feat(Data\Nat\ModEq.lean): add grind attribute to ModEq t-data WIP labelled WIP
27752 plp127 feat(Order): `NoBotOrder α` implies `NoMinOrder α` under `IsDirected α (· ≥ ·)` t-order awaiting-author failing CI
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
24719 madvorak feat(LinearAlgebra/Matrix/NonsingularInverse): inverting `Matrix` inverts its `LinearEquiv` t-algebra awaiting-author awaiting author
24373 YaelDillies refactor: golf `modularCharacter` t-measure-probability awaiting-CI does not pass CI
26299 adomani perf: the `commandStart` linter only acts on modified files t-linter 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
27995 kckennylau feat(RingTheory/Valuation): alternate constructors for Valuation t-ring-theory awaiting-CI does not pass CI
26159 upobir feat(Algebra/QuadraticDiscriminant): Adding inequalities on quadratic from inequalities on discriminant t-algebra awaiting-author awaiting author
27701 vihdzp feat: `a < b + c ↔ a < b ∨ ∃ d < c, a = b + d` t-algebra awaiting-author awaiting author
26462 PSchwahn feat(LinearAlgebra/Projection): add results about inverse of `Submodule.prodEquivOfIsCompl` new-contributor t-algebra awaiting-author awaiting author
28286 bwangpj feat(Geometry/Manifold/ContMDiff): basic lemmas for analytic (`C^ω`) functions new-contributor t-differential-geometry awaiting-author awaiting author
29527 kim-em feat: script for checking Github URLs CI WIP labelled WIP
25778 thefundamentaltheor3m feat: Monotonicity of `setIntegral` for nonnegative functions new-contributor t-measure-probability awaiting-author awaiting author
29615 eric-wieser chore: add a computable shortcut for `AddCommMonoid ℂ` bench-after-CI t-analysis easy failing CI
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
28057 plp127 feat(SuccOrder): simp lemma to refold `Order.succ` and `Order.pred` t-order awaiting-author awaiting author
29870 mckoen feat(CategoryTheory/Adhesive): subobjects in adhesive categories have binary coproducts t-category-theory WIP labelled WIP
28175 dsfxcimk feat: exterior angle theorem new-contributor t-euclidean-geometry awaiting-author awaiting author
29588 Periecle feat(Analysis/Complex/Residue): Implement residue theory for complex functions at isolated singularities new-contributor t-analysis awaiting-author failing CI
24050 Paul-Lez feat(Data/Finsupp/Pointwise): generalise pointwise scalar multiplication of finsupps t-data 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
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
19860 YaelDillies refactor: review the `simps` projections of `OneHom`, `MulHom`, `MonoidHom` t-algebra WIP labelled WIP
28630 Antidite feat(Archive/Imo): right isosceles configuration in the complex plane IMO new-contributor awaiting-author awaiting author
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
26284 plp127 feat: faster implementation of `Nat.primeFactorsList` + `@[csimp]` lemma t-data awaiting-author awaiting author
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
29634 YaelDillies feat: missing instance `NonUnitalCommSemiring R → NonUnitalNonAssocCommSemiring R` t-algebra awaiting-CI help-wanted looking for help
30460 janithamalith feat(Nat): add lemma nat_card_orbit_mul_card_stabilizer_eq_card_group t-group-theory new-contributor 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
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
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
26088 grunweg chore(Linter/DirectoryDependency): move forbidden directories into a JSON file t-linter please-adopt looking for help
30828 DeVilhena-Paulo feat: implementation of `Finmap.merge` t-data new-contributor failing CI
30902 adomani chore: longLine warnings happen starting at the 101st character awaiting-zulip t-linter awaiting a zulip discussion
30914 eric-wieser feat(Data/Set/NAry): lemmas for `diff` t-data t-order delegated delegated
30378 mans0954 refactor(Order/Hom/Lattice): Use default `initialize_simps_projections` configuration for `LatticeHom`. t-order awaiting-author awaiting author
30667 FrederickPu Subgroup mul new-contributor t-algebra awaiting-author awaiting author
31013 vihdzp chore: deprecate `AsLinearOrder` t-order awaiting-author awaiting author
30975 mariainesdff feat(Data/Finsupp/Defs): add Finsupp.restrict t-data awaiting-author awaiting author
30408 kckennylau feat(RingTheory): more algebra instances for HomogeneousLocalization and linear constructors t-ring-theory 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
29871 zach1502 feat(Matrix/Transvection): Gauss pivot determinant identity and pivot preservation new-contributor t-algebra awaiting-author awaiting author
30109 scholzhannah feat: the subcomplexes of a (relative classical) CW complex form a completely distributive lattice t-topology awaiting-author awaiting author
30158 nicolaviolette feat: combinatorics simplegraph basic new-contributor t-combinatorics awaiting-author awaiting author
30431 kckennylau feat(RingTheory): a homogeneous submodule is the span of its homogeneous elements t-ring-theory failing CI
27229 WilliamCoram feat(GroupTheory/DoubleCoset): multiple lemmas t-group-theory FLT new-contributor failing CI
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
30612 grunweg feat: add ContDiff.lipschitzOnWith t-analysis awaiting-author awaiting author
30560 dwrensha fix(LinearAlgebra/Alternating/Basic): avoid deep recursion in MultilinearMap.alternatization t-algebra awaiting-author awaiting author
31226 erdOne chore(RingTheory): add `@[ext]` to `Ideal.Quotient.algHom_ext` t-ring-theory easy awaiting-author awaiting author
31348 PatrickMassot chore: fix a docstring typo t-analysis easy awaiting-author documentation awaiting author
26231 chrisflav feat(CategoryTheory/Sites): sheaf condition and coproducts t-category-theory awaiting-author failing CI
29145 JovanGerb chore: use `to_additive` in more places awaiting-CI t-meta does not pass CI
29458 LiamSchilling feat(MvPolynomial/WeightedHomogenous): relate `weightedTotalDegree` to `degrees` and `degreeOf` t-ring-theory new-contributor awaiting-author awaiting author
28693 faenuccio feat(Analysis.Normed.Module.Milman-Pettis): add Milman-Pettis theorem t-analysis WIP labelled WIP
30039 JovanGerb feat(push): `push` annotations for `Real.log` t-meta awaiting-author awaiting author
25765 JovanGerb feat(gcongr): lemma for rewriting inside divisibility t-data delegated delegated
31607 grunweg chore: rename `continuous{,On,At,Within}_const to `ContinuousFoo.const` awaiting-CI delegated does not pass CI
30526 SnirBroshi chore(Logic/Relation): use `Subrelation` to state theorems awaiting-zulip awaiting a zulip discussion
31637 Whysoserioushah feat(Data/Matrix/Basis): add some lemmas t-data awaiting-author awaiting author
30562 dwrensha fix(Data/Fintype/Perm): make the main logic of Equiv.instFintype irreducible t-data awaiting-author awaiting author
26885 pechersky feat(Topology/ValuativeRel): ValuativeTopology 𝒪[K] t-algebra t-topology t-number-theory failing CI
31326 sgouezel chore: deprecate `smooth` variants of `contMDiff` results t-differential-geometry awaiting-author failing CI
12032 mcdoll feat: delta distribution as a limit t-analysis WIP labelled WIP
24965 erdOne refactor: Make `IsLocalHom` take unbundled map t-algebra delegated delegated
22464 adomani feat(CI): declarations diff in Lean CI awaiting-author awaiting author
30842 kim-em feat: add Aristotle task for command palette CI awaiting review
30988 erdOne feat(AlgebraicGeometry): descending affine cover of an inverse limit t-algebraic-geometry awaiting review
26777 YaelDillies chore(Data/Set/Image): move `BooleanAlgebra` material to `Order` t-data WIP labelled WIP
24383 YaelDillies feat: distributive Haar characters of `ℝ` and `ℂ` file-removed FLT t-measure-probability awaiting-CI WIP labelled WIP
23881 YaelDillies feat: `ℝ≥0`-valued Lᵖ norm t-measure-probability awaiting-author awaiting author
21915 YaelDillies feat: simproc for `Int.divisorsAntidiag` t-meta WIP labelled WIP
21342 YaelDillies refactor(Normed/Group/Quotient): generalise to non-abelian groups t-analysis WIP labelled WIP
15443 YaelDillies feat: Marcinkiewicz-Zygmund inequality t-analysis WIP labelled WIP
31263 LiranShaul feat: arbitrary product of injective modules is injective new-contributor t-algebra awaiting-author awaiting author
27602 mitchell-horner feat(Combinatorics/SimpleGraph): define `CompleteBipartiteSubgraph` t-combinatorics awaiting-author awaiting author
31590 SuccessMoses chore: tag `commutatorElement_def` with `simp` new-contributor t-algebra awaiting-author failing CI
28613 espottesmith feat(Combinatorics): define undirected hypergraphs new-contributor t-combinatorics failing CI
25802 dagurtomas feat(AlgebraicTopology): anodyne morphisms of simplicial sets t-topology WIP labelled WIP
29744 espottesmith feat(Combinatorics): define directed hypergraphs new-contributor t-combinatorics failing CI
6859 MohanadAhmed feat: TryLean4Bundle: Windows Bundle Creator CI WIP help-wanted looking for help
12452 JADekker feat(Cocardinal): add some more api t-topology awaiting-CI ??? does not pass CI
19062 hannahfechtner feat(Algebra/PresentedMonoid/Basic): facts about rel t-algebra awaiting-author awaiting author
23772 SEU-Prime feat: Amice equivalence t-number-theory WIP ??? labelled WIP
24533 robertmaxton42 feat(ULift): conjugation by ULift.up/down, misc cast/heq lemmas t-data awaiting-author awaiting author
25034 ScottCarnahan feat(Algebra/Module/Equiv/Basic): Restriction of scalars from a semilinear equivalence to a linear equivalence t-algebra WIP labelled WIP
25035 ScottCarnahan feat(Algebra/Module/Equiv/Defs): linear equivalence between linear hom and semilinear hom t-algebra WIP labelled WIP
26013 tsuki8 feat(Data/Finset/Card,Data/Set/Finite/Basic): TODO needs a better title t-data new-contributor 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
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
29921 mans0954 refactor(RingTheory/Polynomial/SmallDegreeVieta): convert to {p : R[X]} (hp : p.natDegree = 2) t-ring-theory awaiting-author awaiting author
29361 FlAmmmmING feat: Catalan generating function as a formal power series t-ring-theory new-contributor awaiting-author awaiting author
30609 FlAmmmmING feat(Combinatorics/Enumerative/Catalan): large and small Schröder numbers new-contributor t-combinatorics awaiting-author awaiting author
25907 mans0954 feat: low order roots of unity t-algebra awaiting-author awaiting author
26765 KiringYJ feat(MeasureTheory/PiSystem): add π-λ theorem and SetLike instance new-contributor t-measure-probability awaiting-author awaiting author
31719 maksym-radziwill feat: Borel-Caratheodory (2nd revision) t-analysis awaiting-author failing CI
30190 joelriou feat(CategoryTheory/Sites): functoriality of descent data t-category-theory WIP labelled WIP
29409 Julian feat(Mathlib/Analysis): deriv_eq_self and deriv_exp_iff t-analysis awaiting-author awaiting author
22366 kim-em feat: `check_equalities` tactic for diagnosing defeq problems t-meta delegated failing CI
31611 thorimur feat(Meta): `withPlural` wrapper for more readable messages in source maintainer-merge t-meta awaiting review
31854 erdOne chore(AlgebraicGeometry): API for `𝒪ₓ`-modules t-algebraic-geometry awaiting-author awaiting author
27306 xyzw12345 feat: `lie_ring` tactic and `LieReduce` command t-meta failing CI
27664 pechersky feat(Topology,Analysis): discrete topology metric space and normed groups t-topology awaiting-author failing CI
29422 jsm28 fix(Data/Finset/Max): Use `DecidableEq` for `insert` lemmas t-data awaiting review
31597 grunweg chore(AtLocation): allow throwing a warning when no progress is being made t-meta awaiting-author awaiting author
30678 YaelDillies refactor(Algebra/Quaternion): intermediate `Module` instance t-algebra awaiting review
29434 ntapiam feat(NonAssoc/LieAdmissible): prove every ring/algebra is LieAdmissible new-contributor t-algebra failing CI
30436 wwylele feat(Topology/InfiniteSum): tprod_one_{add/sub}_ordered t-topology awaiting-author failing CI
29151 yuanyi-350 feat: Corollary of Hahn–Banach theorem new-contributor awaiting-author ⚠️ awaiting author
29856 mans0954 feat(Analysis/Normed/Ring/Basic): Add NonUnitalNonAssocSeminormedRing and NonUnitalNonAssocNormedRing t-analysis awaiting-author awaiting author
27254 yuanyi-350 feat: 2025 imo problem3 IMO failing CI
28141 YaelDillies chore: deprecate `BialgHom.coe_toLinearMap` t-ring-theory toric awaiting-zulip awaiting a zulip discussion
30637 strihanje01 feat(Combinatorics/SetFamily/Lindstrom): Lindstrom's theorem for subfamilies with equal unions new-contributor t-combinatorics failing CI
31259 YaelDillies refactor(Dynamics): use `SetRel` notions of separation and cover t-dynamics awaiting review
31949 ADedecker chore: prefer `Pi.single i 1 j` over `fun j => if i = j then 1 else 0` t-algebra awaiting-author awaiting author
31965 bwangpj feat: fiber of RingHom.specComap t-ring-theory awaiting-author awaiting author
30981 jsm28 feat(Geometry/Euclidean/Angle/Bisector): oriented angle bisection mod π t-euclidean-geometry awaiting review
31525 kim-em feat: convex combinations in `Set.Icc` t-topology delegated delegated
30877 YaelDillies feat(Algebra/MonoidAlgebra): extend the `R[M]` notation to `MonoidAlgebra R M` t-algebra awaiting-author awaiting author
31571 erdOne feat(RingTheory): existence of local algebra with given residue field t-ring-theory awaiting-author awaiting author
31176 mcdoll feat(Analysis): Taylor's theorem with the integral remainder t-analysis awaiting-author awaiting author
30350 joelriou feat(AlgebraicGeometry): the pseudofunctor which sends a scheme to its category of sheaves of modules t-algebraic-geometry awaiting-author awaiting author
30432 kckennylau feat(AlgebraicGeometry): define the non-vanishing locus of a set in Proj t-algebraic-geometry awaiting-author awaiting author
31984 kim-em feat: proposed definition of `ConvexSpace` t-algebra awaiting review
31989 Thmoas-Guan feat(RingTheory): add ideal fg of Noetherian lemma t-ring-theory easy awaiting-author awaiting author
25835 erdOne WIP: Weierstrass elliptic functions t-analysis WIP labelled WIP
26975 Whysoserioushah feat: a norm_num extension for complex numbers t-meta failing CI
31817 kckennylau chore: remove extra monic hypotheses from divByMonic and modByMonic lemmas t-ring-theory t-algebra awaiting-author failing CI
30995 kckennylau feat(RingTheory): replace ofLinearEquiv with limit t-ring-theory awaiting-author awaiting author
30620 plp127 feat: copy LE and LT on preorder and partial order t-order awaiting-author awaiting author
25803 erdOne feat: taylor expansion of `1 / z ^ r` t-analysis awaiting-author awaiting author
32094 grunweg feat(runLinter): allow only running certain linters t-linter CI failing CI
31366 FaffyWaffles feat(Analysis/SpecialFunctions/StirlingRobbins): Robbins' sharp stepwise bound for stirlingSeq new-contributor t-analysis awaiting-author awaiting author
31960 urkud feat: a lower bound for the volume of a cone on the unit sphere t-measure-probability awaiting review
31796 dobronx1325 feat(Data/Real/EReal): add mul_lt_mul_of_pos_left theorem t-data new-contributor failing CI
26743 grunweg feat: product rule for Lie bracket on manifolds t-differential-geometry WIP labelled WIP
31210 jsm28 feat(Geometry/Euclidean/MongePoint): `reindex` lemmas t-euclidean-geometry awaiting review
27258 JovanGerb feat: Imo2020 q6 IMO awaiting-author awaiting author
31362 BeibeiX0 feat(partitions): generalized pentagonal numbers new-contributor t-combinatorics awaiting-author awaiting author
31755 kaantahti feat(Combinatorics): Add Sperner's Lemma formalization new-contributor t-combinatorics WIP labelled WIP
30030 JonBannon feat(MeasureTheory): add `MemLp.Const` class and instances to unify `p = ∞` and `μ.IsFiniteMeasure` cases t-measure-probability awaiting-author failing CI
31315 Parcly-Taxel feat: IMO 2010 Q5 IMO awaiting-author awaiting author
27599 mitchell-horner feat(Combinatorics/SimpleGraph): define `CompleteEquipartiteSubgraph` t-combinatorics awaiting-author awaiting author
31592 gasparattila chore(Tactic/Measurability): `fun_prop` lemmas for solving `MeasurableSet {x | ...}` goals t-measure-probability awaiting review
30744 grunweg feat: more extensions for differential geometry elaborators t-differential-geometry t-meta failing CI
29508 zhuyizheng feat(MeasureTheory): FTC and integration by parts for absolutely continuous functions new-contributor t-measure-probability awaiting-author awaiting author
30293 vlad902 feat(SimpleGraph): there exists a maximal path/trail in a graph with finite edges t-combinatorics awaiting review
30886 urkud feat(DifferentialForm): exterior derivative applied to vector fields t-analysis awaiting review
30525 515801431 feat(Mathlib/Combinatorics/Enumerative/Polya): Add Polya Counting new-contributor t-combinatorics awaiting-author awaiting author
30750 SnirBroshi feat(Data/Quot): `toSet` and `equivClassOf` t-data awaiting-zulip awaiting-author awaiting a zulip discussion
26588 faenuccio feat(Algebra/GroupWithZero/WithZero): add the multiplicative embedding with zero from the range t-order t-algebra failing CI
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
32039 HugLycan Feat/positivity-zeroness new-contributor t-meta WIP labelled WIP
29354 themathqueen refactor(Algebra/Algebra/Equiv): allow for non-unital `AlgEquiv` t-algebra awaiting-author awaiting author
28604 alreadydone chore(Algebra/Ring/Defs): add two classes (minimally invasive version) t-algebra awaiting-author awaiting author
27053 tb65536 feat: Galois group of `x^n - x - 1` large-import t-algebra WIP labelled WIP
31500 zcyemi feat(Analysis/Convex/Between): add lemmas on affine independence under strict betweenness t-convex-geometry awaiting-author awaiting author
26831 AntoineChambert-Loir feat(GroupTheory/SpecificGroups/Alternating/MaximalSubgroups): maximal subgroups of the alternating group t-group-theory awaiting review
31062 zcyemi feat(Geometry/Euclidean/Similarity): add triangle similarity t-euclidean-geometry awaiting-author awaiting author
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
31979 jsm28 feat(LinearAlgebra/AffineSpace/Independent): injectivity of spans of images t-algebra awaiting review
32041 thomaskwaring feat(Combinatorics/SimpleGraph/Acyclic): every acyclic subgraph can be extended to a maximal one new-contributor t-combinatorics awaiting review
32042 chrisflav feat(AlgebraicGeometry): quasi compact covers t-algebraic-geometry awaiting review
31995 Thmoas-Guan feat(RingTheory) : Module being injective is local property t-ring-theory awaiting-author awaiting author
29558 Thmoas-Guan feat(Algebra): definition of global dimension t-ring-theory awaiting-author awaiting author
31929 kim-em feat: replace `Finsupp.embDomain_apply` with more general lemma delegated ⚠️ delegated
32169 saodimao20 feat: add convolution_comp_add_right new-contributor t-analysis awaiting-author awaiting author
31455 kim-em feat: products of locally contractible spaces t-topology delegated delegated
31059 gasparattila feat(Topology/Sets): define the Vietoris topology on `(Nonempty)Compacts` t-topology awaiting review
31219 Thmoas-Guan feat(Algebra): lemma about `IsBaseChange` under exact sequence t-ring-theory awaiting-author awaiting author
28944 linesthatinterlace refactor(Order/Hom/Basic): reorder definitions t-order awaiting review
30133 smmercuri feat: `WithVal v` and `WithVal w` are isomorphic as uniform spaces when `v` and `w` are equivalent valuations t-algebra t-topology awaiting review
31132 kckennylau feat(Algebra): saturation of a submonoid t-algebra failing CI
31662 edwin1729 feat(Topology/Order): topological basis of scott topology on Complete… new-contributor t-topology awaiting-author awaiting author
28546 Sfgangloff feat(SymbolicDynamics): basic setup of Zd, full shift, cylinders, pat… new-contributor t-dynamics awaiting-author awaiting author
30892 vihdzp feat: head/last element of flattened list large-import t-data awaiting-author awaiting author
31836 hanwenzhu chore(MeasureTheory/IntervalIntegral): generalize fundamental theorem of calculus to `HasDerivWithinAt` instead of `HasDerivAt` t-measure-probability t-analysis awaiting-author awaiting author
30998 erdOne feat(FieldTheory): fg extension over perfect field is separably generated t-algebra awaiting review
31754 dagurtomas feat: light profinite sets are injective objects t-condensed t-topology t-category-theory WIP labelled WIP
31987 saodimao20 feat: add monotonicity and relation lemmas for mgf and cgf new-contributor t-measure-probability awaiting review
31838 qawbecrdtey chore(Data/Finset/Basic): use more dot notation in `Data.Finset.Basic` t-data awaiting review
32004 jsm28 feat(Geometry/Euclidean/Angle/Sphere): unoriented law of sines with circumradius t-euclidean-geometry awaiting review
32019 jsm28 feat(Geometry/Euclidean/Projection): `map` and subtype lemmas t-euclidean-geometry awaiting review
30757 SnirBroshi feat(Combinatorics/SimpleGraph/Acyclic): `singletonGraph` and `subgraphOfAdj` are trees t-combinatorics awaiting review
26389 jjdishere feat(RingTheory): Perfectoid Field t-algebra t-analysis t-topology WIP labelled WIP
26390 jjdishere feat(Topology/Algebra): Krasner's lemma t-algebra t-topology t-number-theory WIP labelled WIP
30736 alreadydone feat(RingTheory): Picard group of a domain is isomorphic to ClassGroup large-import t-algebra awaiting review
32232 grunweg chore: tidy flexible linter exceptions failing CI
31733 jsm28 feat(Geometry/Euclidean/Incenter): `orthRadius` lemmas t-euclidean-geometry awaiting review
31780 euprunin feat: add `grind` annotations for `SimpleGraph.Walk.length_{support,darts,edges}` t-combinatorics awaiting review
31092 FlAmmmmING feat(Algebra/Group/ForwardDiff.lean): Add theorem `sum_shift_eq_fwdDiff_iter`. new-contributor t-algebra awaiting-author awaiting author
31921 DavidLedvinka feat: FiniteExhaustion brownian t-data awaiting review
31706 Thmoas-Guan feat(Algebra/ModuleCat): `ModuleCat.uliftFunctor` t-algebra awaiting-author awaiting author
30666 erdOne feat(NumberTheory): every number field has a ramified prime t-algebra t-number-theory awaiting-author failing CI
32118 alreadydone feat(Algebra): prerequisites for #31919 t-ring-theory t-algebra awaiting-author awaiting author
28786 mitchell-horner feat(Combinatorics/SimpleGraph): restate Turán's theorem in terms of `extremalNumber` t-combinatorics awaiting review
30484 vihdzp refactor: override `≤` and `<` in `Function.Injective.semilatticeSup`, etc. t-order awaiting review
30921 EtienneC30 feat: characterizing Gaussian measures through the shape of the characteristic function brownian t-measure-probability awaiting review
31141 peabrainiac feat(Analysis/Calculus): parametric integrals over smooth functions are smooth 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 failing CI
32267 vlad902 feat(SimpleGraph): add `SimpleGraph.HomClass` t-combinatorics awaiting review
21031 YaelDillies chore: get rid of generic hom coercions WIP labelled WIP
32134 mitchell-horner feat(Topology/Real): theorems linking `IsGLB` with `BddBelow`, `Antitone`, `Tendsto _ atTop` large-import t-topology awaiting-author awaiting author
31444 harahu doc(Probability/Martingale/BorelCantelli): polish docstrings t-measure-probability delegated delegated
13740 YaelDillies feat: more robust ae notation t-measure-probability t-meta awaiting review
28351 joelriou feat(AlgebraicTopology/SimplicialSet): the rank function with values in natural numbers of a regular pairing t-algebraic-topology awaiting review
26719 AntoineChambert-Loir feat(RingTheory/PolynomialLaw/Basic): extends polynomial laws to arbitrary universes t-ring-theory large-import blocked on another PR
30851 FormulaRabbit81 feat(Topology): prove there exists an embedding of separable metric spaces in the hilbert cube t-topology awaiting review
28853 grunweg feat: product of immersions is an immersion t-differential-geometry awaiting-author failing CI
31988 winstonyin feat: Uniqueness of implicit function t-analysis awaiting review
32159 zhuyizheng feat(Order): gaps of disjoint intervals new-contributor ⚠️ failing CI
32165 yuanyi-350 feat(Real/Trigonometric): Add `sum_cos_arith_progression` and prepare for Dirichlet kernel t-analysis awaiting-author awaiting author
32152 Lingyin00 feat(GroupTheory/SpecificGroups/Cyclic): generalize the proof of prime_card by not assuming Finite t-group-theory new-contributor awaiting-author awaiting author
32300 bjornsolheim feat(Geometry/Convex/Cone): define and characterize generating convex cone t-convex-geometry new-contributor awaiting review
26986 WangYiran01 feat(Partition): add bijection for partitions with max part ≤ r new-contributor t-combinatorics awaiting-author failing CI
31891 jsm28 feat(Geometry/Euclidean/Sphere/OrthRadius): lemmas for setting up and using polars t-euclidean-geometry awaiting review
26961 mariainesdff feat(RingTheory/PowerSeries/Substitution): add API t-ring-theory awaiting-author awaiting review
30505 mariainesdff feat(NumberTheory/RatFunc/Ostrowski): prove Ostrowski's theorem for K(X) t-algebra t-number-theory awaiting-author failing CI
32285 awainverse chore(ModelTheory/Bundled): Replace CategoryTheory.Bundled t-logic awaiting-author awaiting author
31449 kim-em feat(SemilocallySimplyConnected): definition and alternative formulation awaiting-author ⚠️ awaiting author
29283 Jlh18 feat(CategoryTheory): define forgetful-core adjunction between Cat and Grpd file-removed t-category-theory awaiting-author awaiting author
31663 xroblot feat(Algebra): more instances about `min`, `max`, `iSup` and `iInf` of sub-algebras t-algebra WIP labelled WIP
31879 Thmoas-Guan feat(Algebra/Homology): Projective dimension in linear equiv t-algebra awaiting-author awaiting author
31746 Maldooor refactor(LinearAlgebra/Matrix): generalize positive semidefinite matrices to infinite dimensions large-import new-contributor t-algebra WIP labelled WIP
32146 foderm feat(ModelTheory): add characterizations of complete theories new-contributor t-logic awaiting review
31707 Thmoas-Guan feat(Homology): map between `Ext` induced by exact functor t-algebra t-category-theory awaiting-author awaiting author
32058 Thmoas-Guan feat(Algebra): category version Baer criterion t-algebra t-category-theory awaiting-author awaiting author
30920 callesonne feat(Category/Grpd): define the bicategory of groupoids large-import t-category-theory failing CI
31121 jessealama feat: add ComplexShape.EulerCharSigns for generalized Euler characteristic t-algebra t-category-theory awaiting-author awaiting author
32318 urkud feat: `toSpanSingleton` as a continuous linear equivalence awaiting-zulip t-topology awaiting a zulip discussion
31610 rudynicolop feat(Computability/NFA): Kleene star closure for Regular Languages via NFA t-computability new-contributor awaiting review
29624 mcdoll feat(LinearAlgebra/LinearPMap): add definition of resolvent and first resolvent identity t-algebra t-analysis awaiting-author failing CI
32195 JovanGerb feat(Data/Finset/Empty): add `@[push]` tags for pushing negation ⚠️ awaiting review
30826 SnirBroshi feat(Combinatorics/SimpleGraph/Connectivity/Subgraph): map a walk to its own subgraph t-combinatorics awaiting review
27100 staroperator feat(ModelTheory): Presburger definability and semilinear sets t-logic awaiting review
30239 luigi-massacci feat(Analysis/Distribution/ContDiffMapSupportedIn): Add postcomposition by a CLM as a CLM on D_K^n t-analysis awaiting review
30926 callesonne feat(Bicategory/Functorbicategory): define bicategory of pseudofunctors t-category-theory blocked on another PR
31057 jsm28 feat(Geometry/Euclidean/Incenter): `reindex` lemmas t-euclidean-geometry awaiting review
32043 thomaskwaring feat(Combinatorics/SimpleGraph/Acyclic): characterise maximal acyclic subgraphs new-contributor t-combinatorics awaiting review
32124 SnirBroshi feat(SimpleGraph/Walks/Operations): expand basic drop/take/reverse API t-combinatorics awaiting review
32201 joelriou feat(AlgebraicTopology): dimension of simplicial sets t-algebraic-topology awaiting review
32337 plp127 feat: generalize urysohns lemma t-topology awaiting review
30618 wwylele feat(Combinatorics): Glaisher's theorem t-combinatorics awaiting review
30144 alreadydone feat(Data/Nat): kernel reducible binaryRec t-data t-algebra failing CI
29960 yonggyuchoimath feat(Algebra/Category/Ring): equalizers of pushout maps of tensor product inclusions new-contributor ⚠️ awaiting review
29369 vlad902 feat(SimpleGraph): `IsSubwalk` of common Walk decompositions large-import t-combinatorics awaiting review
30872 rudynicolop feat(Computability/NFA): NFA closure under concatenation t-computability new-contributor awaiting-author awaiting author
31019 vihdzp feat: colex order on finsupps ⚠️ awaiting review
31205 jsm28 feat(Analysis/Convex/Side): affine combinations and sides of faces of a simplex t-convex-geometry awaiting review
32345 joelriou feat(AlgebraicTopology): relative morphisms of simplicial sets t-algebraic-topology awaiting review
32279 joelriou feat(CategoryTheory): effective epi in the category of functors to types t-category-theory WIP labelled WIP
31673 vasnesterov chore(Tactic/Order): use `AtomM` t-meta awaiting review
31812 xroblot feat(CMField): add `IsCyclotomicExtension.Rat.isCMField` ⚠️ awaiting review
32045 xroblot chore(Trace/Quotient): move isomorphism to `Localization.AtPrime.Basic` t-ring-theory awaiting review
27702 FLDutchmann feat(NumberTheory/SelbergSieve): define Lambda-squared sieves and prove important properties t-number-theory awaiting review
30885 erdOne chore(RingTheory): better defeqs for `PrimeSpectrum.preimageOrderIsoTensorResidueField` t-ring-theory large-import awaiting review
32355 bjornsolheim feat(Geometry/Convex/Cone): define and characterize finitely generated and simplicial pointed cones t-convex-geometry new-contributor awaiting review
32359 YuvalFilmus feat(LinearAlgebra/Lagrange): Formula for leading coefficient of a polynomial new-contributor t-algebra failing CI
31845 smmercuri feat: `UniformSpace.Completion.mapRingEquiv` t-topology awaiting-author awaiting author
31492 fcoUnda Nthroot improvement awaiting-zulip new-contributor t-analysis awaiting a zulip discussion
29942 smmercuri feat(InfinitePlace/Completion): embeddings of `w.Completion` factor through embeddings of `v.Completion` when `w` extends `v` FLT ⚠️ awaiting review
32357 YuvalFilmus feat(Polynomial/Roots): add a theorem for computing roots new-contributor t-algebra awaiting review
32089 erdOne feat(Analysis): derivative of Weierstrass ℘ maintainer-merge t-analysis awaiting review
32360 YuvalFilmus feat(Chebyshev): degree, leadingCoeff, eval_neg t-ring-theory new-contributor awaiting review
32365 yury-harmonic feat: `norm_num` extension for `IsSquare` t-meta awaiting review
26483 metakunt feat(RingTheory/RootsOfUnity/PrimitiveRoots): add equiv_primitiveRoots_of_coprimePow t-ring-theory new-contributor awaiting-author failing CI
32327 EtienneC30 chore(Probability): split `Independence.Kernel` tech debt t-measure-probability awaiting-author awaiting author
31925 alreadydone feat(Topology): étalé space associated to a predicate on sections t-topology awaiting-author awaiting author
32369 metakunt feat(RingTheory/Coprime/Lemmas): Add Int.isCoprime_gcdA t-ring-theory new-contributor awaiting review
32188 euprunin feat: add `grind` annotation for `ENNReal.inv_eq_zero` t-data awaiting review
32085 dagurtomas feat(CategoryTheory): sheaf categories are regular epi categories t-category-theory WIP labelled WIP
30391 rudynicolop feat(Data/List): list splitting definitions and lemmas t-data new-contributor awaiting review
32375 erdOne feat(RingTheory): More API for `Ideal.ResidueField` t-ring-theory awaiting review
32116 LessnessRandomness feat(Geometry/Euclidean/Angle/Unoriented/TriangleInequality): Add criterion for equality case t-euclidean-geometry awaiting review
29393 staroperator feat(SetTheory/ZFC): `card (V_ o) = preBeth o` large-import t-set-theory awaiting review
31876 mcdoll feat(Analysis/Distribution): integration by parts for Schwartz functions t-analysis awaiting review
31967 bwangpj feat: IrreducibleSpace.of_openCover t-topology awaiting review
32160 SnirBroshi feat(Combinatorics/SimpleGraph/Walks): helper theorems about `darts` and `support` t-combinatorics awaiting review
32238 YaelDillies feat(Combinatorics/SimpleGraph): distributivity of box product over sum large-import t-combinatorics awaiting review
32259 jsm28 feat(Analysis/SpecialFunctions/Trigonometric/Angle): `toReal` addition lemmas t-analysis awaiting review
32372 bwangpj feat: InfiniteGalois.normalAutEquivQuotient ⚠️ awaiting review
32371 KaiErikNiermann fix: minor error in comment of example for natural transformation new-contributor easy ❌? infrastructure-related CI failing
32323 LLaurance feat(Combinatorics/SimpleGraph/Connectivity): exists vertex adjacent to any vertex of a nontrivial connected graph t-combinatorics awaiting review
31766 SuccessMoses feat(Topology/EMetricSpace): continuity of arc length new-contributor awaiting-author ⚠️ awaiting author
31908 YaelDillies feat: Bernoulli random variables t-measure-probability awaiting review
31880 gululu996-ui feat(Combinatorics/SimpleGraph/Hamiltonian): Add theorem 'IsNotHamiltonian_if_IsBridge' new-contributor t-combinatorics awaiting-author failing CI
31901 callesonne feat(Bicategory/Subbicategory): add full subbicategories using `ObjectProperty` t-category-theory awaiting review
32385 kebekus feat: derivatives of meromorphic functions are meromorphic t-analysis awaiting review
30582 RemyDegenne feat: extension of a function to the closure of a submodule t-topology WIP labelled WIP
26351 RemyDegenne feat: covering and packing numbers of sets in a metric space brownian t-topology awaiting-author awaiting author
32367 BoltonBailey feat(Computability): add finEncodings for List Bool and pairs of types ⚠️ awaiting review
31551 RemyDegenne feat: `gaussianReal_const_sub` t-measure-probability awaiting review
32064 chrisflav feat(RingTheory/Smooth): smooth algebra over Noetherian base is flat t-ring-theory awaiting review
31898 ntapiam feat(LinearAlgebra/TensorAlgebra): implement HopfAlgebra for TensorAlgebra t-ring-theory new-contributor awaiting-author failing CI
32389 LLaurance feat(Analysis): Trigonometric identities ❌? ⚠️ infrastructure-related CI failing
27579 RemyDegenne feat: risk of an estimator, DeGroot statistical information, total variation distance large-import t-measure-probability WIP labelled WIP
32382 YaelDillies chore(Algebra/Order/AddGroupWithTop): golf t-algebra failing CI
31165 AntoineChambert-Loir feat(LinearAlgebra/Transvection): base change of transvections large-import t-algebra delegated delegated
32194 alreadydone feat(LinearAlgebra): more on StrongRankCondition t-algebra awaiting-author awaiting author
32339 alreadydone chore(LinearAlgebra/Dimension): generalize and golf t-algebra awaiting review
32373 erdOne feat(Analysis): `HasFPowerSeriesOnBall (fun x ↦ 1 / (1 - x))` and friends t-analysis awaiting review
32395 ADedecker feat: specialize `[pre, post]comp_uniformConvergenceCLM` to `CompactConvergenceCLM` t-topology 🟤 running CI
30880 themathqueen feat(Analysis/InnerProductSpace): finite-dimensional inner product space with an algebra implies a coalgebra maintainer-merge t-analysis awaiting-author awaiting author
32381 YaelDillies chore: deprecate `ENat.not_lt_zero` in favor of `not_neg` t-data maintainer-merge awaiting review
32131 Vierkantor feat(scripts): count the number of tactics without a docstring large-import CI t-meta awaiting review
30570 SnirBroshi feat(Combinatorics/SimpleGraph/Connectivity/Connected): `reachabilitySet` t-combinatorics awaiting review
32383 joelriou feat(Algebra/Homology): extensions of bifunctors to complexes preserve homotopies t-algebra t-category-theory awaiting review
30605 joelriou feat(CategoryTheory): for any filtered category, there exists a final functor from a directed poset t-category-theory awaiting-author awaiting author
32406 JovanGerb feat(tauto): better error message on failure t-meta awaiting review
31711 joelriou feat(CategoryTheory/Sites): the category structure on the points of a site t-category-theory awaiting review
31998 Thmoas-Guan feat(Algebra): localized module in `ModuleCat` t-algebra awaiting-author awaiting author
32386 riccardobrasca feat: add classical version of Hilbert 90 large-import t-number-theory WIP labelled WIP
31528 bwangpj feat: MulAction.fixedPoints and MulAction.fixedBy under MulActionHom t-group-theory large-import awaiting review
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
31653 ster99 feat(MeasureTheory): Foelner filters new-contributor awaiting-author ⚠️ awaiting author
30116 FormulaRabbit81 feat(Measure): proof that a relatively compact set of measures is tight t-measure-probability awaiting-author awaiting author
32128 grunweg dev: investigate the private module linter not firing failing CI
31807 edegeltje feat(CategoryTheory/Cat/Basic): Turning 1- and 2-morphisms in Cat into a 1-field structure t-category-theory awaiting-author awaiting author
32264 jjtowery feat(Bicategory): add lax slice bicategory new-contributor t-category-theory awaiting-author awaiting author
32370 apnelson1 feat(Combinatorics/Matroid): refactor matroid supportedness tactic WIP ⚠️ labelled WIP
29948 mcdoll feat(Analysis/Fourier): the Fourier transform on L^2 large-import t-analysis awaiting review
32405 Shaddaaa feat(CategoryTheory/Sites): (Co)continuity of `Over.iteratedSliceEquiv` large-import new-contributor t-category-theory awaiting-author awaiting author
31433 sinhp feat(CategoryTheory): Computable cartesian monoidal structure on slices induced by chosen pullbacks t-category-theory awaiting-author awaiting author
31505 dsfxcimk feat: Add some oangle theorems new-contributor t-euclidean-geometry awaiting-author awaiting author
32411 mcdoll feat(Analysis/Distribution): the bilinear pairing of Schwartz functions t-analysis awaiting review
31395 peakpoint feat(Analysis/Normed/Affine/Isometry): interpret `AffineIsometry{Map,Equiv}` as `ContinuousAffine{Map,Equiv}` new-contributor t-analysis awaiting review
31425 robertmaxton42 feat(Topology) : implement delaborators for non-standard topology notation t-topology awaiting review
32163 zhuyizheng feat(MeasureTheory): interval integral is absolutely continuous new-contributor t-measure-probability awaiting review
32190 vihdzp chore(Algebra/Order/Ring/Archimedean): generalize theorems to `OrderHomClass` + `RingHomClass` t-algebra awaiting review
31732 fbarroero feat(NumberTheory/MahlerMeasure.lean): Northcott's Theorem t-number-theory awaiting review
31247 rudynicolop feat(Computability/DFA): add DFA complement, union, and intersection t-computability new-contributor awaiting-author awaiting author
32254 YaelDillies feat(Algebra/MonoidAlgebra): congruence isomorphisms t-algebra awaiting review
32398 YaelDillies chore(Algebra/MonoidAlgebra): use `to_additive` more t-algebra awaiting review
32423 joelriou feat(CategoryTheory): more preservation properties of functors t-category-theory awaiting review
32356 YuvalFilmus feat(Arsinh): add arcosh new-contributor t-analysis awaiting-author awaiting author
31503 Scarlett-le feat(Geometry/Euclidean/PerpBisector): add distance inequalities for Sbtw with perpendicularity new-contributor t-euclidean-geometry awaiting-author awaiting author
32218 mkaratarakis feat: lemmas about the `House` of an algebraic number new-contributor t-number-theory awaiting-author awaiting author
32215 jonasvanderschaaf feat(ModelTheory/Types): Construct a topology on CompleteType and prove the space is compact new-contributor ⚠️ awaiting review
32422 kim-em fix(Linter): deprecated module linter now fires for public/meta imports t-linter awaiting-author failing CI
32353 ADedecker feat: define the space of distributions maintainer-merge t-analysis awaiting-author failing CI
29315 kbuzzard chore: raise priority of `IsTopologicalSemiring.toIsModuleTopology` t-topology awaiting-author failing CI
31478 BGuillemet feat(CategoryTheory/Sites): `uliftYoneda` for sheaves over a subcanonical topology t-category-theory awaiting review
31862 erdOne chore: unify `LocalizedModule` and `OreLocalization` t-algebra awaiting review
30089 loefflerd feat(NumberTheory/ModularForms): Bounds on modular forms and q-expansion coeffs t-number-theory WIP blocked on another PR
32077 artie2000 feat(Algebra/Order/Ring/Ordering): ring ordering constructions large-import t-algebra awaiting-author awaiting author
32424 joelriou feat(CategoryTheory): the Yoneda embedding for a locally small category t-category-theory awaiting review
30333 paulorauber feat(Probability): definition of trajMeasure new-contributor t-measure-probability awaiting-author awaiting author
30213 SnirBroshi feat(Data/List/GetD): golf and add lemmas for `get` and `getElem?` t-data new-contributor awaiting review
29530 ShreckYe feat(Dynamics/PeriodicPts): some theorems for `Pi.map` in `Dynamics/PeriodicPts` analogous to those for `Prod.map` large-import t-dynamics awaiting-author awaiting author
25143 chrisflav feat(RingTheory): smooth algebras have smooth Noetherian models t-ring-theory awaiting author
31161 AntoineChambert-Loir feat(RingTheory/MvPolynomial/IrrQuadratic): irreducibility of sum X_i Y_i t-ring-theory awaiting-author awaiting author
26212 Thmoas-Guan feat(Algebra): the Rees theorem for depth large-import t-algebra awaiting review
28582 Thmoas-Guan feat(Data): some lemmas about WithBot ENat t-data awaiting-author awaiting author
32429 erdOne feat(RingTheory): `IsIntegrallyClosed R[X]` t-ring-theory awaiting review
28682 Thmoas-Guan feat(RingTheory): definition of regular local ring t-ring-theory awaiting-author awaiting author
29937 Thmoas-Guan feat(RingTheory): `ringKrullDim` of quotient via supportDim t-ring-theory awaiting-author merge conflict
29186 winstonyin feat: IsIntegralCurve for solutions to ODEs t-dynamics t-analysis t-differential-geometry awaiting-author awaiting author
32430 YaelDillies chore: delete `Units.mulDistribMulAction'` bench-after-CI t-algebra awaiting review
31508 FLDutchmann feat(Tactic): `algebra` tactic. t-meta awaiting-author awaiting author
30758 Timeroot chore: tag abs_inv and abs_div with grind= t-algebra awaiting-author awaiting review
28100 themathqueen feat(LinearAlgebra/GeneralLinearGroup): algebra automorphisms in endomorphisms are inner t-algebra awaiting review
32364 Ruben-VandeVelde feat: lemmas about bernoulli t-analysis t-number-theory awaiting-author awaiting author
27946 plp127 refactor: have `MetrizableSpace` not depend on `MetricSpace` t-topology awaiting-author awaiting author
32432 YaelDillies feat: `MulDistribMulAction M Nˣ` instance CFT t-algebra awaiting review
32433 YaelDillies feat: an irreducible element of a submonoid isn't zero CFT t-algebra awaiting review
32428 sven-manthe feat(Algebra): add Subsemigroup.op t-algebra awaiting review
32434 YaelDillies feat(Algebra/Homology): miscellaneous lemmas CFT t-algebra awaiting review
31717 thorimur chore: refactor `Type*` and `Sort*` to use `mkFreshLevelParam` large-import t-meta awaiting review
29362 stepanholub feat(Data/List): periods of lists; prove the Periodicity Lemma t-data new-contributor awaiting review
32435 YaelDillies chore(Algebra/Module): make select `Module` assumptions CFT t-algebra awaiting review
32427 YaelDillies refactor(Algebra/Algebra): genericise algebra instances for subsemirings CFT t-algebra failing CI
31986 SnirBroshi feat(Data/List/Cycle): `{next,prev}_getElem` without `Nodup` + infix theorems t-data awaiting-author awaiting author
31689 barni120400 feat(Combinatorics/Additive): subset-sum definition and basic properties new-contributor t-combinatorics awaiting review
32437 WenrongZou feat(Algebra/Category/ModuleCat/Sheaf/Quasicoherent): construction of `Presentation` new-contributor t-algebra awaiting review
32281 ajirving feat(NumberTheory.Chebyshev): prove connection between prime counting and theta large-import new-contributor t-number-theory WIP labelled WIP
31133 thorimur feat(Linter): combinators for linter option boilerplate t-linter t-meta awaiting review
32439 joelriou feat(Algebra/Homology): morphisms in the derived category between single complexes t-algebra t-category-theory awaiting review
32363 euprunin chore: golf using `simpa` awaiting review
32320 euprunin experiment(Algebra): measure the impact of removing redundant tactic invocations (WIP) t-algebra WIP labelled WIP
31147 daefigueroa feat(Dynamics): point transitive monoid actions and transitive points new-contributor t-dynamics merge conflict
32441 euprunin chore(Algebra/DirectSum): remove use of `erw` in `mul_eq_dfinsuppSum` t-algebra awaiting review
32442 joelriou feat(CategoryTheory/Localization): inverse in `SmallShiftedHom` t-category-theory awaiting review
27542 chrisflav feat(RingTheory/KrullDimension): dimension of polynomial ring t-ring-theory large-import failing CI
31034 chrisflav feat(RingTheory/Extension/Cotangent): basis of free cotangent space can be realized as a presentation t-ring-theory awaiting review
32005 metakunt feat(Algebra/Polynomial/Basic): Add ofMultiset new-contributor t-algebra awaiting review
32379 marwahaha feat(Analysis/SpecialFunctions): prove expNegInvGlue is not analytic at zero new-contributor t-analysis awaiting review
31406 JovanGerb feat(push_neg): `push_neg +distrib` syntax t-meta awaiting-author awaiting author
30853 JovanGerb feat(LinearAlgebra/AffineSpace/Simplex): `CoeFun` instance for `Simplex` ⚠️ awaiting review
32414 SnirBroshi feat(NumberTheory/ArithmeticFunction/Carmichael): Carmichael totient function 🟤 ⚠️ running CI
32176 JovanGerb feat(translate): refactor `applyReplacementFun` and more t-meta awaiting review
31803 grunweg chore(Tactic/Linters): remove `public section` t-linter awaiting review
32403 FLDutchmann fix(FieldSimp): `declaration has free variables` kernel errors t-meta awaiting review
32340 SnirBroshi doc(1000.yaml): add `ZMod` version of Chinese remainder theorem failing CI
32416 kim-em feat(TacticAnalysis): add generic env var-based tryAtEachStep linter large-import 🟤 ⚠️ running CI
32445 vihdzp chore: avoid non-terminal simp t-order easy 🟤 running CI
31886 CoolRmal feat: the family of limits in probability of sequences of uniformly integrable random variables is uniformly integrable brownian t-measure-probability awaiting review
30241 joelriou feat(CategoryTheory): locally presentable categories and strong generators t-category-theory blocked on another PR
31174 joelriou refactor(AlgebraicTopology): refactor the homotopy category and the nerve adjunction t-algebraic-topology awaiting review
31452 jsm28 feat(Analysis/Convex/StrictCombination): convex combinations in strictly convex sets and spaces t-convex-geometry awaiting review
31757 mcdoll feat(Analysis/Distribution): definition of tempered distributions t-analysis awaiting review
32079 wwylele feat(Topology): UniformContinuous version of uniform limit theorem t-topology awaiting review
32080 plp127 feat(Topology): Completely Regular Space iff Uniformizable t-topology awaiting review
32144 EtienneC30 feat: add a predicate HasGaussianLaw brownian t-measure-probability awaiting review
32231 grunweg chore: use the to_fun attribute awaiting review
32297 mcdoll feat(Analysis/Distribution): composition of temperate growth functions t-analysis awaiting review
32303 joelriou feat(CategoryTheory): commutation of bifunctors to shifts in two variables t-category-theory awaiting review
32306 plp127 fix(depRewrite): make `rw!` cleanup casts correctly t-meta awaiting review
32326 chrisflav feat(Algebra/ModuleCat): extension of scalars is comonadic for a faithfully flat algebra t-ring-theory awaiting review
32444 vihdzp feat: `SignType` is a complete linear order large-import t-data t-order easy awaiting review
29437 SnirBroshi feat(Data/Seq): add Seq.subsequence and prove basic theorems about it t-data new-contributor awaiting review
29596 alreadydone chore(Algebra): extract `Submonoid.IsLocalizationMap` t-algebra awaiting author
32377 JovanGerb chore(Order/BoundedOrder/Basic): use `to_dual` 🟤 running CI
32448 vihdzp chore(Order/SuccPred/Basic): use `where` notation t-order easy 🟤 running CI
32262 alreadydone feat(Algebra): Dedekind-finite and stably finite rings t-ring-theory t-algebra awaiting review
32443 vihdzp feat: `SuccOrder` and `PredOrder` instances for `SignType` t-data 🟤 running CI
32408 mirefek feat(SetTheory/Ordinal): Improve API for Ordinal.toType t-set-theory new-contributor awaiting review
31930 SnirBroshi feat(Data/List/Basic): `idxOf` lemmas t-data awaiting review
32333 euprunin chore: golf using `grind` awaiting review
32451 vihdzp chore(Topology/Order/Basic): golf `instIsCountablyGenerated_atTop` t-topology awaiting review
32452 vihdzp chore: add `variable [OrderTopology α]` t-topology easy 🟤 running CI
31471 Scarlett-le feat(LinearAlgebra/AffineSpace): add commutativity lemmas for line parallelism new-contributor t-algebra awaiting-author awaiting author
32453 Hagb feat(Tactic/WLOG): add `wlog!` a variant of `wlog` that calls `push_neg` t-meta 🟤 running CI
29687 vihdzp feat: standard part in non-Archimedean field t-algebra awaiting review
31730 thorimur feat(Meta): declaration manipulation meta API: allow logging on type signature of theorems t-meta failing CI
32450 morrison-daniel feat(LinearAlgebra/Multilinear): constructing `MultilinearMap` over `DirectSum` new-contributor t-algebra 🟤 running CI
32374 adamtopaz feat(Tactic/WildcardUniverse): Foo.{*, _, v*, max u v} t-meta awaiting review
32455 vihdzp feat: order topologies of successor orders t-order t-topology 🟤 running CI
32030 newell feat(Analysis/AperiodicOrder/Delone): Delone Sets t-analysis awaiting review
31416 SnirBroshi feat(Combinatorics/SimpleGraph/Walk): lemmas about the first and last darts/edges t-combinatorics failing CI
32412 Brian-Nugent feat: add Artinian schemes new-contributor t-algebraic-geometry awaiting-author 🟤 running CI
30622 kim-em feat: replace some tauto with grind awaiting-author ⚠️ awaiting author
29776 yuanyi-350 chore: refactor `ContinuousLinearMap.isOpenMap` by separating it into sublemmas t-analysis WIP labelled WIP
32458 vihdzp feat: order isomorphisms preserve successor/predecessor limits t-order 🟤 running CI
32460 loefflerd feat(ModularForms): norm and trace maps t-number-theory 🟤 running CI
31802 joelriou feat(AlgebraicTopology): horns in `Δ[2]` as pushouts t-algebraic-topology awaiting review
32461 joelriou feat(Algebra/Homology): more API for the HomComplex from a single cochain complex large-import t-algebra t-category-theory 🟤 running CI
26384 jjdishere feat(RingTheory/Perfectoid): Fontaine's theta map is surjective t-algebra t-number-theory labelled WIP
32316 Thmoas-Guan feat(Homology/ModuleCat): Dimension Shifting tools in ModuleCat t-algebra t-category-theory awaiting-author awaiting author
32252 ajirving feat(NumberTheory.Chebyshev): prove relationship between psi and theta large-import new-contributor t-number-theory 🟤 running CI
32447 vihdzp chore(Order/SuccPred/Basic): use `to_dual` t-order 🟤 running CI
32457 vihdzp chore: mark `Set.not_finite` as `simp` t-data awaiting review
32462 vihdzp refactor: make `abbrev`s for `IsDirected α (· ≤ ·)` and `IsDirected α (· ≥ ·)` t-order awaiting-CI 🟤 does not pass CI
28599 Thmoas-Guan feat(RingTheory): polynomial over CM ring is CM t-ring-theory large-import WIP labelled WIP
32449 vihdzp refactor: `Ordinal.toType` → `Ordinal.ToType` t-set-theory awaiting-CI 🟤 does not pass CI
31558 AntoineChambert-Loir feat(Topology/Sublevel): sublevels in relation with semicontinuity and compactness t-topology awaiting author
32407 harahu doc: fix typos found by codespell awaiting review
13847 alreadydone feat(EllipticCurve): the universal elliptic curve t-algebra t-algebraic-geometry merge-conflict awaiting-author merge conflict
14167 alreadydone feat: Group scheme structure on Weierstrass curve workshop-AIM-AG-2024 t-algebraic-geometry merge-conflict WIP labelled WIP
13297 urkud feat(Semicontinuous): add `comp` lemma t-order t-topology merge-conflict awaiting-author merge conflict
12936 mattrobball chore(Quiver.Opposite): make `Quiver.Hom.op/unop` `abbrev`'s merge-conflict merge conflict
12934 grunweg chore: replace more uses of > or ≥ by < or ≤ merge-conflict awaiting-author help-wanted looking for help
12933 grunweg chore: replace some use of > or ≥ by < or ≤ merge-conflict awaiting-author failing CI
12608 eric-wieser feat: allow `nsmul` / `zsmul` to be omitted again, with a warning t-algebra t-meta merge-conflict awaiting-author merge conflict
12679 MichaelStollBayreuth perf(NumberTheory/RamificationInertia): speed up slow file merge-conflict WIP labelled WIP
12192 Ruben-VandeVelde feat: generalize isLittleO_const_id_atTop/atBot t-analysis merge-conflict awaiting-author merge conflict
11617 urkud refactor(Finset): redefine Finset.diag, review API t-logic 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
10594 lecopivo feat: `fun_trans` function transformation tactic e.g. for computing derivatives t-meta merge-conflict WIP labelled WIP
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
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
8519 eric-wieser refactor(LinearAlgebra/TensorProduct): golf using `liftAddHom` t-algebra merge-conflict awaiting-author merge conflict
8658 eric-wieser feat: support right actions for `Con` t-algebra merge-conflict awaiting-author merge conflict
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
9356 alexjbest feat: assumption? t-meta 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
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
8961 eric-wieser refactor: use the coinduced topology on ULift awaiting-CI merge-conflict please-adopt awaiting-author looking for help
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
9354 chenyili0818 feat: monotonicity of gradient on convex real-valued functions t-analysis merge-conflict awaiting-author merge conflict
9570 eric-wieser feat(Algebra/Star): Non-commutative generalization of `StarModule` t-algebra awaiting-CI merge-conflict WIP labelled WIP
9229 eric-wieser refactor(Algebra/GradedMonoid): Use `HMul` to define `GMul` t-algebra merge-conflict WIP labelled WIP
6630 MohanadAhmed feat: Reduced Spectral Theorem t-algebra 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
7351 shuxuezhuyi feat(Topology/Algebra/Order): extend function on `Ioo` to `Icc` t-order merge-conflict awaiting-author merge conflict
7227 kmill feat: flexible binders and integration into notation3 t-meta merge-conflict WIP labelled WIP
6931 urkud refactor(Analysis/Normed*): use `RingHomIsometric` for `*.norm_cast` t-analysis merge-conflict help-wanted ??? looking for help
7615 eric-wieser chore(LinearAlgebra/Basic): generalize compatibleMaps to semilinear maps t-algebra awaiting-CI easy merge-conflict does not pass CI
7909 mcdoll fix(Tactic/Continuity): remove npowRec and add new tag for Continuous.pow t-topology t-meta merge-conflict WIP labelled WIP
7932 eric-wieser refactor(Algebra/TrivSqZeroExt): replace with a structure t-algebra awaiting-CI merge-conflict does not pass CI
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
6580 adomani chore: `move_add`-driven replacements merge-conflict awaiting-author merge conflict
6930 kmill feat: `resynth_instances` tactic for resynthesizing instances in the goal or local context t-meta merge-conflict WIP labelled WIP
7467 ADedecker feat: spectrum of X →ᵇ ℂ is StoneCech X t-analysis merge-conflict WIP labelled WIP
7713 RemyDegenne feat: add_left/right_inj for measures t-measure-probability merge-conflict awaiting-author merge conflict
6791 eric-wieser refactor: Use flat structures for morphisms awaiting-CI merge-conflict awaiting-author help-wanted looking for help
7601 digama0 feat: ring hom support in `ring` t-algebra t-meta merge-conflict awaiting-author merge conflict
7962 eric-wieser feat: `DualNumber (Quaternion R)` as a `CliffordAlgebra` t-algebra merge-conflict WIP labelled WIP
6777 adomani chore(Co*variantClass): replace eta-expanded (· * ·), (· + ·), (· ≤ ·), (· < ·) merge-conflict merge conflict
7076 grunweg feat: define measure zero subsets of a manifold t-measure-probability t-differential-geometry merge-conflict WIP labelled WIP
6403 astrainfinita chore: change instance priorities of `Ordered*` hierarchy slow-typeclass-synthesis t-order t-algebra 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
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
4127 kmill refactor: create HasAdj class, define Digraph, and generalize some SimpleGraph API t-combinatorics merge-conflict awaiting-author merge conflict
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
6328 astrainfinita chore: make some instance about `Sub...Class` lower priority t-algebra awaiting-CI merge-conflict WIP labelled WIP
6210 MohanadAhmed feat(Data/IsROrC/Basic): add a `StarOrderedRing` instance t-algebra t-analysis 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
6330 astrainfinita chore: make some instance about `Sub...Class` higher priority than `Sub...` slow-typeclass-synthesis t-algebra merge-conflict WIP labelled WIP
4960 eric-wieser chore: use `open scoped` awaiting-CI merge-conflict does not pass CI
6079 eric-wieser fix: deduplicate variables awaiting-CI merge-conflict does not pass CI
5133 kmill feat: IntermediateField adjoin syntax for sets of elements t-algebra merge-conflict WIP labelled WIP
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
13124 astrainfinita chore: remove `CovariantClass` and `ContravariantClass` merge-conflict WIP labelled WIP
19275 eric-wieser fix: if nolint files change, do a full rebuild merge-conflict delegated failing CI
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
19425 hrmacbeth perf: gcongr forward-reasoning adjustment merge-conflict awaiting-author merge conflict
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
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
20313 thefundamentaltheor3m feat(Data/Complex/Exponential): prove some useful results about the complex exponential. new-contributor t-analysis merge-conflict 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
8370 eric-wieser refactor(Analysis/NormedSpace/Exponential): remove the `𝕂` argument from `exp` awaiting-zulip t-analysis merge-conflict failing CI
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
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
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
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
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
13994 grunweg chore(Topology): replace continuity -> fun_prop t-topology merge-conflict failing CI
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
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
7596 alreadydone feat: covering maps from properly discontinuous actions and discrete subgroups file-removed t-topology merge-conflict merge conflict
10541 xgenereux feat(Algebra/SkewMonoidAlgebra/Basic): add SkewMonoidAlgebra new-contributor t-algebra merge-conflict WIP labelled WIP
13973 digama0 feat: lake exe refactor, initial framework t-meta merge-conflict awaiting-author merge conflict
10190 jstoobysmith feat(AlgebraicTopology): add Augmented Simplex Category t-algebraic-topology new-contributor t-category-theory merge-conflict WIP labelled WIP
20208 js2357 feat: Define the localization of a fractional ideal at a prime ideal t-algebra merge-conflict WIP labelled WIP
11632 mattrobball chore(Group/RingTheory.Congruence): make `Quotient`'s reducible t-group-theory merge-conflict 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
9820 jjaassoonn feat(RingTheory/GradedAlgebra/HomogeneousIdeal): generalize to homogeneous submodule 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
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
20267 joelriou feat(CategoryTheory): comma categories are accessible t-category-theory merge-conflict awaiting-author WIP labelled WIP
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
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
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
6042 MohanadAhmed feat(LinearAlgebra/Matrix/SVD): Singular Value Decomposition of R or C Matrices t-algebra merge-conflict please-adopt WIP looking for help
13036 joelriou feat(CategoryTheory/Sites): under certain conditions, cover preserving functors preserve 1-hypercovers t-category-theory merge-conflict WIP labelled WIP
7125 eric-wieser feat: additive monoid structure via biproducts t-category-theory awaiting-CI merge-conflict WIP labelled WIP
12278 Rida-Hamadani feat(Combinatorics/SimpleGraph): Provide iff statements for distance equal and greater than 2 t-combinatorics merge-conflict awaiting-author failing CI
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
9273 grunweg feat: extended charts are local diffeomorphisms on their source t-differential-geometry merge-conflict awaiting-author merge conflict
15045 Command-Master fix(LinearAlgebra/Alternating/Basic): fix `MultilinearMap.alternatization` t-algebra merge-conflict awaiting-author ??? missing CI information
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
14444 digama0 fix(GeneralizeProofs): unreachable! bug t-meta merge-conflict awaiting-author merge conflict
14752 AntoineChambert-Loir fix(Topology/Algebra/Valued): repair definition of Valued t-algebra t-topology merge-conflict WIP labelled WIP
10235 urkud feat: add `Decidable`, `Fintype`, `Encodable` linters awaiting-bench large-import t-linter t-meta merge-conflict awaiting-author failing CI
15651 TpmKranz feat(Computability/NFA): operations for Thompson's construction awaiting-zulip t-computability new-contributor merge-conflict awaiting-author awaiting a zulip discussion
9693 madvorak feat: Linear programming in the standard form t-algebra RFC merge-conflict WIP labelled WIP
15649 TpmKranz feat(Computability): introduce Generalised NFA as bridge to Regular Expression awaiting-zulip t-computability new-contributor merge-conflict awaiting-author awaiting a zulip discussion
20238 maemre feat(Computability/DFA): Closure of regular languages under some set operations awaiting-zulip t-computability new-contributor merge-conflict awaiting-author awaiting a zulip discussion
5745 alexjbest feat: a tactic to consume type annotations, and make constructor nicer t-meta merge-conflict awaiting-author merge conflict
5919 MithicSpirit feat: implement orthogonality for AffineSubspace new-contributor t-analysis merge-conflict WIP help-wanted looking for help
7219 Ruben-VandeVelde feat: Equivs for AddMonoidAlgebras t-algebra merge-conflict awaiting-author merge conflict
7386 madvorak feat: Define linear programs t-algebra RFC merge-conflict WIP labelled WIP
9352 chenyili0818 feat: arithmetic lemmas for `gradient` t-analysis merge-conflict awaiting-author merge conflict
9795 sinhp feat: the type `Fib` of fibre of a function at a point t-category-theory merge-conflict awaiting-author merge conflict
10660 eric-wieser feat(LinearAlgebra/CliffordAlgebra): construction from a basis t-algebra merge-conflict awaiting-author WIP labelled WIP
10977 grunweg feat: germs of smooth functions t-analysis t-topology t-differential-geometry merge-conflict awaiting-author failing CI
10998 hmonroe feat(Logic): Arithmetization of partial recursive functions (toward Gödel's first incompleteness theorem) t-logic merge-conflict awaiting-author merge conflict
11155 smorel394 feat(LinearAlgebra/Multilinear/DirectSum, LinearAlgebra/DirectSum/{PiTensorProduct,Finsupp}): interaction between `MultilinearMap` and `DirectSum`, and between `PiTensorProduct` and `DirectSum` t-algebra merge-conflict please-adopt looking for help
11890 adomani feat: the terminal refine linter t-linter merge-conflict awaiting-author merge conflict
12006 adomani feat: the `suffa` tactic t-meta merge-conflict awaiting-author merge conflict
13442 dignissimus feat: mabel tactic for multiplicative abelian groups new-contributor t-meta merge-conflict modifies-tactic-syntax awaiting-author help-wanted looking for help
14237 js2357 feat: Define the localization of a fractional ideal at a prime ideal new-contributor t-algebra merge-conflict awaiting-author failing CI
14345 digama0 feat: the Dialectica category is monoidal closed t-category-theory merge-conflict awaiting-author merge conflict
14727 jjaassoonn feat(RingTheory/Flat/CategoryTheory): a flat module has vanishing higher Tor groups t-ring-theory merge-conflict awaiting-author merge conflict
14733 jjaassoonn feat(RingTheory/Flat/CategoryTheory): a module is flat iff tensoring preserves finite limits t-ring-theory merge-conflict awaiting-author merge conflict
15055 sinhp feat: the category of pointed objects of a concrete category t-category-theory merge-conflict awaiting-author merge conflict
15224 AnthonyBordg feat(CategoryTheory/Sites): covering families and their associated Grothendieck topology new-contributor t-category-theory merge-conflict awaiting-author merge conflict
16303 grunweg feat(CI): check for badly formatted titles or missing/contradictory labels CI merge-conflict awaiting-author failing CI
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 merge-conflict awaiting-author WIP labelled WIP
18749 GabinKolly feat(ModelTheory): preparatory work for the existence of Fraïsse limits t-logic merge-conflict awaiting-author merge conflict
19323 madvorak feat: Function to Sum decomposition t-data merge-conflict WIP labelled WIP
19378 adamtopaz feat: Explanation widgets t-meta merge-conflict awaiting-author merge conflict
19456 AntoineChambert-Loir feat(Data/Finsupp/MonomialOrder/DegRevLex): homogeneous reverse lexicographic order t-data t-order t-algebraic-geometry merge-conflict WIP labelled WIP
6268 eric-wieser fix: fixups to #3838 merge-conflict WIP labelled WIP
6993 jjaassoonn feat: lemmas about `AddMonoidAlgebra.{divOf, modOf}` t-algebra merge-conflict merge conflict
7427 MohanadAhmed feat: eigenvalues sorted in ascending/descending order merge-conflict WIP ⚠️ labelled WIP
9339 FMLJohn feat(RingTheory/GradedAlgebra/HomogeneousIdeal): given a finitely generated homogeneous ideal of a graded semiring, construct a finite spanning set for the ideal which only contains homogeneous elements t-ring-theory merge-conflict merge conflict
9564 AntoineChambert-Loir chore: weaken commutativity assumptions for AdjoinRoot.lift and AdjoinRoot.liftHom t-algebra merge-conflict WIP ??? labelled WIP
10026 madvorak feat: linear programming according to Antoine Chambert-Loir's book t-algebra RFC merge-conflict WIP labelled WIP
10159 madvorak feat: linear programming according to Antoine Chambert-Loir's book — affine version t-algebra RFC merge-conflict WIP labelled WIP
10349 Shamrock-Frost refactor(CategoryTheory/MorphismProperty): some clean-ups t-category-theory merge-conflict ??? missing CI information
11021 jstoobysmith feat(AlgebraicTopology): add join of augmented SSets t-algebraic-topology new-contributor merge-conflict WIP labelled WIP
11800 JADekker feat: KappaLindelöf spaces awaiting-zulip t-topology merge-conflict please-adopt ??? looking for help
11575 ScottCarnahan feat(RingTheory/HahnSeries/Addition): lemmas on leading terms t-ring-theory merge-conflict WIP labelled WIP
12251 ScottCarnahan refactor(RingTheory/HahnSeries): several generalizations t-order t-algebra merge-conflict WIP labelled WIP
12394 JADekker feat: define pre-tight and tight measures t-measure-probability merge-conflict please-adopt awaiting-author looking for help
14426 adomani feat: `#min_imps` command (development branch) merge-conflict WIP ??? ⚠️ labelled WIP
14686 smorel394 feat(AlgebraicGeometry/Grassmannian): define the Grassmannian scheme workshop-AIM-AG-2024 t-algebraic-geometry merge-conflict please-adopt WIP ??? looking for help
17071 ScottCarnahan feat(LinearAlgebra/RootSystem): separation, base, cartanMatrix t-algebra merge-conflict WIP ??? labelled WIP
18626 hannahfechtner feat: define Artin braid groups new-contributor t-algebra merge-conflict awaiting-author merge conflict
20029 FrederickPu feat(Tactic/simps): allow for Config attributes to be set directly new-contributor t-meta merge-conflict WIP labelled WIP
14089 callesonne feat(Bicategory/Functorbicategory): define bicategory of pseudofunctors t-category-theory merge-conflict merge conflict
20527 trivial1711 refactor(Topology/UniformSpace/Completion): more descriptive names for `α → Completion α` t-topology 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
20872 grunweg feat: lint against the tactic.skipAssignedInstances option in mathlib tech debt t-linter merge-conflict 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
20454 urkud chore(TangentCone): review names t-analysis merge-conflict failing CI
21959 BGuillemet feat(Topology/ContinuousMap): Stone-Weierstrass theorem for MvPolynomial new-contributor t-topology merge-conflict merge conflict
22660 Ruben-VandeVelde chore: follow naming convention around Group.IsNilpotent t-algebra merge-conflict merge conflict
20874 grunweg chore(nolint.yml): use shallow clones CI merge-conflict awaiting-author merge conflict
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
20401 RemyDegenne feat: add sigmaFinite_iUnion t-measure-probability merge-conflict awaiting-author merge conflict
22727 grunweg feat: rewrite the isolated by and colon linters in Lean t-linter merge-conflict awaiting-author merge conflict
22701 ctchou feat(Combinatorics): the Katona circle method new-contributor t-combinatorics merge-conflict merge conflict
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
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
23509 eric-wieser refactor: Make ENNReal an abbrev t-data merge-conflict failing CI
20567 grunweg feat(Cache): two small features t-meta merge-conflict merge conflict
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
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
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
23546 JovanGerb feat(LinearAlgebra/AffineSpace/AffineSubspace): rename `AffineSubspace.mk'` to `Submodule.shift` t-euclidean-geometry merge-conflict merge conflict
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
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
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
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
21734 adomani fix(PR summary): checkout GITHUB_SHA CI merge-conflict awaiting-author WIP labelled WIP
23953 b-reinke feat(Data/Matroid/Tutte): define the Tutte polynomial of a matroid t-data 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
25988 Multramate refactor(AlgebraicGeometry/EllipticCurve/*): replace Fin 3 with products t-algebraic-geometry merge-conflict merge conflict
26090 grunweg chore: make `finiteness` a default tactic merge-conflict failing CI
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
25999 bjoernkjoshanssen feat(Topology/Compactification): projective line over ℝ is homeomorphic to the one-point compactification of ℝ t-topology merge-conflict failing CI
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
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
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
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
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
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
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
21474 erdOne feat(RingTheory): replace `Ring.DimensionLEOne` with `Ring.KrullDimLE` t-ring-theory large-import merge-conflict failing CI
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
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
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
27446 grunweg chore: more enorm lemmas carleson merge-conflict WIP labelled WIP
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
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
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
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
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
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
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
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
25138 chrisflav chore(RingTheory/Ideal): make `RingHom.ker` take a `RingHom` instead of `RingHomClass` t-algebra merge-conflict failing CI
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
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
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
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
22657 Xmask19 feat: a graph is maximally acyclic iff it is a tree new-contributor t-combinatorics 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
29120 eric-wieser feat: add a typeclass for the indiscrete topology t-topology merge-conflict failing CI
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
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
24532 robertmaxton42 feat(LinearAlgebra/FreeProduct): fill out the `FreeProduct.asPowers` namespace t-algebra 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
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
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
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
29638 yuma-mizuno feat(CategoryTheory): define descent data by presieves t-category-theory merge-conflict WIP labelled WIP
22361 rudynicolop feat(Computability/NFA): nfa closure properties awaiting-zulip t-computability new-contributor merge-conflict awaiting-author awaiting a zulip discussion
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
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
29877 Komyyy feat: inner product of the gradient t-analysis merge-conflict merge conflict
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
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
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
25481 kbuzzard chore: refactor Algebra.TensorProduct.rightAlgebra t-algebra merge-conflict delegated merge conflict
26827 pechersky feat(Analysis/Normed/ValuativeRel): helper instance for NormedField t-algebra t-analysis t-number-theory merge-conflict merge conflict
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
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
26484 peabrainiac feat(Geometry/Diffeology): basics of diffeological spaces t-differential-geometry merge-conflict merge conflict
31388 b-mehta feat(Topology/Order): add unordered versions of topological Rolle's theorem tech debt t-analysis merge-conflict awaiting-author merge conflict
30706 astrainfinita refactor(Analysis/NormedSpace/Exponential): remove the `𝕂` argument from `exp` t-analysis merge-conflict awaiting-author blocked on another PR
30824 grunweg wip: another smoothness lemma for local frames t-differential-geometry merge-conflict WIP labelled WIP
30962 WangYiran01 feat(Combinatorics/Enumerative): add lattice path lemmas and counts new-contributor t-combinatorics merge-conflict merge conflict
30322 kckennylau feat(RingTheory): base change of graded algebra t-ring-theory merge-conflict awaiting-author merge conflict
28013 astrainfinita feat: Lindemann-Weierstrass Theorem t-algebra t-analysis merge-conflict merge conflict
31593 Ruben-VandeVelde feat: some lemmas about MonoidAlgebra t-algebra merge-conflict awaiting-author merge conflict
31596 grunweg chore: remove extraneous uses of push_neg merge-conflict WIP labelled WIP
31600 grunweg chore: replace by_cases! with by_cases when the push_neg step does no… merge-conflict WIP labelled WIP
26087 grunweg feat: a `SliceModel` typeclass for models with corners for embedded submanifolds t-differential-geometry merge-conflict failing CI
26240 grunweg perf(CommandLinterLinter): use Substring more t-linter RFC merge-conflict merge conflict
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
28070 grunweg style: improve indentation of multi-linear enumerations in doc-strings merge-conflict failing CI
20466 MohanadAhmed feat: Sherman Morrison formula for rank 1 update of the matrix inverse t-data merge-conflict awaiting-author merge conflict
20648 anthonyde feat: formalize regular expression -> εNFA awaiting-zulip t-computability new-contributor merge-conflict awaiting a zulip discussion
20649 GabinKolly feat(ModelTheory/Graph): prove characterization of the fraisse limit of finite simple graphs large-import t-logic t-combinatorics merge-conflict WIP labelled WIP
20652 jjaassoonn feat: categorical description of center of a ring t-algebra t-category-theory merge-conflict awaiting-author failing CI
20924 tomaz1502 feat(Computability/QueryComplexity): Oracle-based computation t-computability merge-conflict failing CI
21270 GabinKolly feat(ModelTheory/Bundled): first-order embeddings and equivalences from equalities large-import t-logic merge-conflict awaiting-author merge conflict
21447 erdOne feat(AlgebraicGeometry): the split algebraic torus t-algebraic-geometry merge-conflict awaiting-author merge conflict
21616 peabrainiac feat(Topology): concatenating countably many paths t-topology merge-conflict awaiting-author merge conflict
21624 sinhp feat(CategoryTheory): The (closed) monoidal structure on the product category of families of (closed) monoidal categories t-category-theory merge-conflict awaiting-author failing CI
21829 Whysoserioushah feat(LinearAlgebra/TensorProduct/HomTensor): Add TensorProduct of Hom-modules t-algebra merge-conflict awaiting-author merge conflict
21903 yhtq feat: add from/toList between `FreeSemigroup` and `List` with relative theorems large-import new-contributor t-algebra awaiting-CI merge-conflict does not pass CI
22159 shetzl feat: add definition of pushdown automata t-computability new-contributor merge-conflict awaiting-author merge conflict
22231 pechersky feat(Algebra/Valued): `AdicExpansion` initial defns t-algebra t-topology merge-conflict awaiting-author merge conflict
22302 658060 feat: add `CategoryTheory.Topos.Power` new-contributor t-category-theory merge-conflict awaiting-author merge conflict
22314 shetzl feat: add leftmost derivations for context-free grammars t-computability new-contributor merge-conflict awaiting-author merge conflict
22662 plp127 feat: Localization.Away.lift (computably) t-algebra merge-conflict merge conflict
22790 mhk119 feat: Extend `taylor_mean_remainder_lagrange` to `x < x_0` new-contributor t-analysis merge-conflict awaiting-author merge conflict
22861 eric-wieser feat: add the trace of a bilinear form t-algebra merge-conflict awaiting-author merge conflict
22919 plp127 feat(Data/Fintype/Pi): Make `Fintype` instance for `RelHom`s computable t-data merge-conflict awaiting-author merge conflict
22954 eric-wieser feat(RingTheory/Congruence/Hom): copy from GroupTheory t-ring-theory merge-conflict failing CI
23285 AntoineChambert-Loir refactor: directed systems in terms of functors large-import t-algebra t-category-theory merge-conflict WIP labelled WIP
23503 apnelson1 feat(Topology/Instances/ENat): ENat and tsum large-import t-topology merge-conflict WIP labelled WIP
23585 plp127 feat: `Filter.atMax` and `Filter.atMin` t-order merge-conflict WIP labelled WIP
23758 erdOne feat(Topology/Algebra): linearly topologized iff non-archimedean large-import t-algebra t-topology merge-conflict awaiting-author merge conflict
23835 chrisflav feat(Topology): cardinality of connected components is bounded by cardinality of fiber t-topology merge-conflict awaiting-author failing CI
24333 xcloudyunx feat(Combinatorics/SimpleGraph): cycle graph implementation for generic vertex types new-contributor t-combinatorics merge-conflict awaiting-author merge conflict
24441 MrSumato feat(Data/List): add Lyndon-Schutzenberger theorem on list commutativity t-data new-contributor merge-conflict awaiting-author merge conflict
24540 robertmaxton42 feat(Quiv): add the empty, vertex, point, interval, and walking quivers t-category-theory merge-conflict awaiting-author failing CI
24789 Ruben-VandeVelde chore: move Algebra.Group.Hom.End to Algebra.Ring file-removed t-algebra merge-conflict awaiting-author merge conflict
24850 pechersky feat(Topology/UniformSpace/Ultra): uniform spaces induced by pseudometrics are ultra if system is ultra t-topology merge-conflict merge conflict
25324 eric-wieser feat: more functorial results about DFinsupp t-data t-algebra merge-conflict awaiting-author merge conflict
25500 eric-wieser feat: delaborators for metadata large-import t-meta merge-conflict delegated awaiting-author merge conflict
25585 Paul-Lez feat(Tactic/Linters/DeprecatedSimpLemma): lint for deprecated simp lemmas t-linter merge-conflict awaiting-author 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 merge-conflict awaiting-author merge conflict
25760 robin-carlier feat(CategoryTheory/Bicategory): (2,1)-categories and `Pith` t-category-theory merge-conflict awaiting-author failing CI
25905 mans0954 feat(RingTheory/Polynomial/SmallDegreeVieta): polynomial versions of results in Algebra.QuadraticDiscriminant t-ring-theory merge-conflict awaiting-author merge conflict
25974 scholzhannah feat(Topology/Compactness/CompactlyCoherentSpace): compact coherentification (k-ification) large-import t-topology merge-conflict merge conflict
25989 Multramate feat(NumberTheory/EllipticDivisibilitySequence): add elliptic nets t-number-theory merge-conflict awaiting-author merge conflict
26051 Komyyy feat(Mathlib/GroupTheory/SpecificGroups/Alternating): A_n is simple iff n = 3 or 5 ≤ n t-group-theory large-import merge-conflict WIP labelled WIP
26158 upobir feat(NumberTheory/Divisors): add int divisors t-number-theory merge-conflict awaiting-author merge conflict
26292 RemyDegenne feat(MeasureTheory): tightness of the range of a sequence t-measure-probability merge-conflict awaiting-author failing CI
26293 RemyDegenne feat: tightness from convergence of characteristic functions t-measure-probability merge-conflict WIP labelled WIP
26300 igorkhavkine feat(Analysis/Calculus/FDeriv): continuous differentiability from continuous partial derivatives on an open domain in a product space new-contributor t-analysis merge-conflict awaiting-author WIP labelled WIP
26329 Timeroot feat: Definition of `Clone` notations and typeclasses t-algebra awaiting-CI merge-conflict awaiting-author does not pass CI
26332 Timeroot feat(ModelTheory/Definability): TermDefinable functions t-logic merge-conflict merge conflict
26340 mans0954 feat(Algebra/Module/NestAlgebra): Nest algebras t-algebra merge-conflict failing CI
26341 mans0954 feat(LinearAlgebra/QuadraticForm/Basis): Free Tensor product of Quadratic Maps large-import t-algebra merge-conflict WIP labelled WIP
26347 mans0954 feat(Data/Finset/RangeDistance): abs_sub_lt_of_mem_finset_range t-data merge-conflict merge conflict
26368 Whysoserioushah feat(RingTheory/TwoSidedIdeal/SpanAsSum): span of set as finsum t-ring-theory merge-conflict awaiting-author merge conflict
26398 ChrisHughes24 feat(ModelTheory): definable functions t-logic merge-conflict please-adopt looking for help
26432 AntoineChambert-Loir feat(Data.Nat.LogFueled): fueled version of `clog` t-data merge-conflict failing CI
26594 metakunt feat(Algebra/Polynomial/ZMod): Add Polynomial.equiv_of_nat_of_polynomial_zmod new-contributor t-algebra merge-conflict awaiting-author merge conflict
26644 kckennylau feat(SetTheory/ZFC): Define the language of sets and state the ZFC axioms t-set-theory merge-conflict awaiting-author merge conflict
26648 eric-wieser chore(TensorProduct): remove more `suppress_compilation`s t-algebra merge-conflict blocked-by-core-PR blocked on another PR
26757 fweth feat(CategoryTheory/Topos): define elementary topos new-contributor t-category-theory merge-conflict awaiting-author failing CI
26803 bjoernkjoshanssen feat: second partial derivatives test t-analysis merge-conflict awaiting-author failing CI
26857 Thmoas-Guan feat(Algebra): define associated graded structure for abelian group t-algebra merge-conflict awaiting-author merge conflict
26914 quangvdao feat(Data/PFunctor/Univariate): more definitions for univariate `PFunctor` t-data merge-conflict merge conflict
26920 yuma-mizuno feat(Tactic.CategoryTheory): add associator inserting tactic t-category-theory t-meta merge-conflict WIP labelled WIP
26923 oliver-butterley feat(Dynamics/BirkhoffSum): add the pointwise ergodic theorem (Birkhoff's) new-contributor t-dynamics merge-conflict merge conflict
26983 mans0954 feat(Order/LatticeElements): distributive, standard and neutral elements of a lattice t-order merge-conflict WIP labelled WIP
26990 joelriou feat(CategoryTheory/Abelian): Noetherian objects form a Serre class t-category-theory merge-conflict WIP labelled WIP
27098 Paul-Lez feat(Algebra/Category/ModuleCat/Sheaf/VectorBundle): define vector bundles t-algebra merge-conflict awaiting-author merge conflict
27155 Pjotr5 feat: Shearer's bound on the independence number of triangle free graphs new-contributor t-combinatorics merge-conflict awaiting-author failing CI
27163 pechersky feat(Topology/ValuativeRel): of and to basis of compatible valuations t-algebra t-topology t-number-theory merge-conflict awaiting-author merge conflict
27187 Komyyy feat: `NONote` represents ordinals < ε₀ t-set-theory merge-conflict WIP labelled WIP
27215 kckennylau feat(AlgebraicGeometry): Define the Zariski site on `CommRingCatᵒᵖ` t-algebraic-geometry merge-conflict awaiting-author merge conflict
27245 NickAdfor feat: multivariate polynomial ring properties about irreducibility new-contributor t-algebra merge-conflict awaiting-author merge conflict
27261 Sebi-Kumar feat(Topology): add definition for subpaths new-contributor t-topology merge-conflict awaiting-author merge conflict
27262 Timeroot feat(Tactic/Bound): bound? for proof scripts t-meta merge-conflict awaiting-author merge conflict
27307 xyzw12345 feat(RingTheory/GradedAlgebra): homogeneous relation t-ring-theory merge-conflict awaiting-author merge conflict
27309 kckennylau feat(CategoryTheory): a presheaf on `CostructuredArrow F d` can be extended to a presheaf on `C` t-category-theory merge-conflict WIP labelled WIP
27321 kckennylau feat(CategoryTheory): Colimit can be computed fiberwise t-category-theory awaiting-CI merge-conflict does not pass CI
27417 PierreQuinton feat: add `SigmaCompleteLattice` t-order merge-conflict awaiting-author merge conflict
27500 Komyyy feat: the Riemann zeta function is meromorphic large-import t-analysis merge-conflict WIP labelled WIP
27534 PierreQuinton feat: a typeclass for `sSup`/`sInf` to be lawful t-order merge-conflict merge conflict
27753 YunkaiZhang233 feat(CategoryTheory): implemented proofs for factorisation categories being equivalent to iterated comma categories in two ways new-contributor t-category-theory merge-conflict awaiting-author merge conflict
27824 ChrisHughes24 feat(Calculus): exists_gt_of_deriv_pos and variants t-analysis merge-conflict awaiting-author merge conflict
27850 fyqing feat: 0-dimensional manifolds are discrete and countable new-contributor t-differential-geometry merge-conflict awaiting-author merge conflict
27973 smmercuri feat: the ring of integers of a `ℤₘ₀`-valued field is compact whenever it is a DVR and the residue field is finite large-import t-algebra merge-conflict awaiting-author merge conflict
28056 grunweg wip: existence of Riemannian metrics t-differential-geometry merge-conflict WIP labelled WIP
28072 kckennylau feat(RingTheory/Valuation): make tactic rw_val_equiv t-ring-theory merge-conflict awaiting-author merge conflict
28124 kckennylau feat(Tactic): Call an arbitrary Simproc t-meta merge-conflict failing CI
28125 nonisomorphiclinearmap feat(Combinatorics): basic definition of simplicial complexes new-contributor t-combinatorics merge-conflict merge conflict
28191 kckennylau feat(Logic): tag Injective, Surjective, and Bijective with fun_prop t-meta merge-conflict awaiting-author merge conflict
28316 eric-wieser feat(Tactic/NormNum): better trace nodes t-meta merge-conflict failing CI
28325 pechersky feat(WithZeroTopology): `locallyCompactSpace_iff_locallyFiniteOrder_units` large-import t-order t-topology merge-conflict failing CI
28349 kckennylau feat(Meta): add notation for naming stacked polynomials t-meta merge-conflict awaiting-author merge conflict
28868 yury-harmonic feat(Positive): add `OfNat` instance large-import t-algebra merge-conflict failing CI
28871 JaafarTanoukhi feat(Combinatorics/Digraph): Tournaments new-contributor t-combinatorics merge-conflict merge conflict
29055 vihdzp feat: `Ordinal.toENat` t-set-theory merge-conflict awaiting-author merge conflict
29108 JonBannon feat(MeasureTheory): add `LInfty.lean` with `Mul` and `const` related results. t-measure-probability merge-conflict awaiting-author merge conflict
29235 yoh-tanimoto feat(Topology/Algebra/Module/ClosedSubmodule): add `mapEquiv`, a variation of `ClosedSubmodule.map` for CLE t-topology merge-conflict merge conflict
29411 llllvvuu feat(LinearAlgebra/Matrix/Rank): rank factorization merge-conflict awaiting-author ⚠️ merge conflict
29500 vihdzp feat: `WellFoundedLT (LowerSet α)` t-order merge-conflict awaiting-author merge conflict
29526 llllvvuu feat: `Multiset.map f` identifies `f` up to permutation t-data merge-conflict merge conflict
29610 llllvvuu feat(LinearAlgebra): define LinearMap.Eigenbasis t-algebra merge-conflict merge conflict
29675 yury-harmonic feat(Wolstenholme): new file t-data merge-conflict awaiting-author help-wanted looking for help
29720 javra feat(CategoryTheory): `TransportEnrichment` and `ForgetEnrichment` as 2-functors t-category-theory merge-conflict WIP labelled WIP
29827 js2357 feat: define two (trivial) ContinuousMulEquivs large-import FLT t-topology merge-conflict failing CI
29947 JaafarTanoukhi feat(Combinatorics/Digraph): Maps new-contributor t-combinatorics merge-conflict merge conflict
29965 RemyDegenne feat(probability): define subtraction of kernels t-measure-probability merge-conflict WIP labelled WIP
29980 mans0954 refactor(RingTheory/Polynomial/Resultant/Quadratic): Re-implement QuadraticDiscriminant for R[X] merge-conflict merge conflict
30004 luigi-massacci feat(MeasureTheory/Integral/TestAgainst): integrating BCFs against a finite measure or an L1Loc map as CLMs t-measure-probability t-analysis merge-conflict awaiting-author merge conflict
30042 JovanGerb feat(push): `@[push]` attributes for `∈` in `Set`, `Finset` and `Multiset` t-meta merge-conflict awaiting-author merge conflict
30121 idontgetoutmuch Principal fiber bundle core new-contributor t-differential-geometry merge-conflict awaiting-author merge conflict
30131 fpvandoorn feat: alias_in attribute t-meta merge-conflict merge conflict
30233 Komyyy refactor(Topology/Sequences): generalize seq-compactness lemmas to metrizable space large-import t-topology merge-conflict merge conflict
30355 kckennylau feat(Logic): graded functions t-data merge-conflict merge conflict
30451 kckennylau feat(HomogeneousIdeal): generalize to homogeneous submodule t-ring-theory merge-conflict failing CI
30668 astrainfinita feat: `QuotLike` t-data awaiting-zulip RFC merge-conflict awaiting-author awaiting a zulip discussion
30933 joelriou feat(CategoryTheory): the linearization of a category t-category-theory merge-conflict awaiting-author merge conflict
31008 RemyDegenne refactor: generalize the index of the process in the Doob decomposition t-measure-probability merge-conflict WIP labelled WIP
31102 JOSHCLUNE Require LeanHammer new-contributor merge-conflict failing CI
31194 grunweg feat: add `#check'` command and tactic, which only show explicit arguments t-meta merge-conflict awaiting-author merge conflict
31351 grunweg feat: manifolds with smooth boundary t-differential-geometry merge-conflict WIP labelled WIP
31356 adomani feat: add inspect-like functions t-meta merge-conflict merge conflict
31604 maksym-radziwill feat: analyticity of dslope t-analysis merge-conflict awaiting-author merge conflict
31613 xyzw12345 feat(RepresentationTheory/GroupCohomology): Non-abelian Group Cohomology large-import t-algebra merge-conflict WIP labelled WIP
31738 robertmaxton42 feat: quivers can be represented as functors from the walking quiver t-category-theory merge-conflict awaiting-author failing CI
30083 grunweg feat: local frames in a vector bundle t-differential-geometry merge-conflict awaiting-author failing CI
31587 JovanGerb Lean pr testing 11156 merge-conflict WIP labelled WIP*
21269 658060 feat(CategoryTheory/Topos): basic definitions and results in topos theory new-contributor t-category-theory merge-conflict awaiting-author WIP labelled WIP
22805 ScottCarnahan feat(FieldTheory/Finite): fixed points of Frobenius automorphism t-algebra merge-conflict WIP labelled WIP
23990 robertmaxton42 feat(Types.Colimits): Quot is functorial and colimitEquivQuot is natural new-contributor t-category-theory merge-conflict awaiting-author merge conflict
24690 ScottCarnahan feat(Data.Prod): reverse lexicographic order t-order merge-conflict WIP labelled WIP
24692 ScottCarnahan feat(RingTheory/HahnSeries/Basic): isomorphism of Hahn series induced by order isomorphism t-order merge-conflict WIP labelled WIP
25726 tb65536 feat: Galois group of `x ^ n - x - 1` large-import t-algebra merge-conflict WIP labelled WIP
25831 ScottCarnahan feat(RingTheory/HahnSeries): Powers of a binomial t-ring-theory merge-conflict WIP labelled WIP
26156 oliver-butterley feat(MeasureTheory.VectorMeasure): add a definition of total variation for VectorMeasure new-contributor t-measure-probability merge-conflict awaiting-author failing CI
26455 ScottCarnahan feat(LinearAlgebra/RootSystem): API for CartanMatrix t-algebra merge-conflict WIP labelled WIP
26770 Jun2M feat(Combinatorics/Graph): subgraph relations on `Graph` t-combinatorics merge-conflict merge conflict
26804 kckennylau feat(SetTheory): ZFSet is a model of ZFC t-set-theory merge-conflict WIP labelled WIP
26890 robin-carlier feat(CategoryTheory/Monoidal/DayConvolution): more API for `DayFunctor` t-category-theory merge-conflict merge conflict
26348 mans0954 feat(Analysis/LocallyConvex/Prime): the prime map t-analysis merge-conflict WIP labelled WIP
26310 kckennylau feat: binary forms t-algebra merge-conflict awaiting-author merge conflict
26283 kckennylau feat: resultant of polynomials t-algebra merge-conflict WIP labelled WIP
28215 5hv5hvnk feat: strong and Weak connectivity for Digraphs new-contributor t-combinatorics merge-conflict awaiting-author WIP labelled WIP
28708 sjh227 feat (Data): edit DoublyStochastic, add Stochastic to matrix t-data new-contributor merge-conflict merge conflict
28970 Whysoserioushah feat(Algebra/Algebra/ReducedNorm): defines reduced norm and trace t-algebra merge-conflict awaiting-author merge conflict
29212 Whysoserioushah feat(Algebra/CrossProductAlgebra/Defs): define Cross Product Algebra t-algebra merge-conflict awaiting-author merge conflict
29281 plp127 doc: `Fin.natAdd_castLEEmb` t-data merge-conflict merge conflict
29514 grunweg feat(CI): use more strict mode CI merge-conflict WIP labelled WIP
29574 JarodAlper feat: regular local rings are domains t-ring-theory new-contributor merge-conflict failing CI
29788 robertmaxton42 feat(Topology): adds bundled continuous maps for sum, sigma, subtype, mapsto, inclusion large-import merge-conflict ⚠️ failing CI
30366 sinhp feat(CategoryTheory): The Preliminaries for Locally Cartesian Closed Categories t-category-theory merge-conflict awaiting-author merge conflict
30855 Ruben-VandeVelde fix: deprecate IsTotal in favour of Std.Total RFC merge-conflict merge conflict
24614 JovanGerb chore: rename field `inf` to `min` in `Lattice` awaiting-zulip t-order merge-conflict failing CI
31148 kex-y feat(Probability): Local and stable properties brownian t-measure-probability merge-conflict WIP labelled WIP
25899 pfaffelh feat(Topology/Compactness/CompactSystem): introduce compact Systems brownian t-topology merge-conflict awaiting-author merge conflict
25902 pfaffelh feat: The finite product of semi-rings (in terms of measure theory) is a semi-ring. brownian large-import t-measure-probability merge-conflict awaiting-author merge conflict
29517 pechersky feat(RingTheory/Torsion): torsion = union of roots of unity t-algebra merge-conflict awaiting-author failing CI
27918 kim-em wip: refactor WithBot/WithTop as structures file-removed merge-conflict failing CI
25822 ScottCarnahan WIP: experiments with vertex algebras merge-conflict WIP labelled WIP
28933 artie2000 chore(Data): correct definition for `single_apply` merge-conflict WIP labelled WIP
24627 pechersky feat(Topology/Algebra/Valued): `IsLinearTopology 𝒪[K] K` and `𝒪[K] 𝒪[K]` t-topology merge-conflict awaiting-author merge conflict
26912 pechersky chore(Algebra/Ring/Subring): simp tag `Subring.smul_def` t-algebra merge-conflict merge conflict
27756 grunweg feat: `Weak(Pseudo)EMetricSpace`, generalises `(Pseudo)EMetricSpace` carleson t-topology merge-conflict WIP labelled WIP
31595 astrainfinita chore: redefine `Ideal.IsPrime` t-algebra merge-conflict awaiting-author merge conflict
24016 plp127 feat: fine uniformity t-topology merge-conflict merge conflict
26614 Rida-Hamadani feat(SimpleGraph): add more API for `take`/`drop` t-combinatorics merge-conflict awaiting-author failing CI
32095 grunweg chore: fix some explicitVarOfIff linter errors merge-conflict please-adopt WIP looking for help
29982 hrmacbeth feat: new `isolate` tactic large-import t-meta merge-conflict awaiting-author failing CI
31007 kckennylau feat(RingTheory): generalise perfection to monoids merge-conflict ⚠️ failing CI
30047 ooovi feat(Combinatorics/SimpleGraph): edge labellings maintainer-merge t-combinatorics merge-conflict awaiting-author merge conflict
26138 xroblot Development branch (2) merge-conflict WIP labelled WIP
26436 AntoineChambert-Loir feat(Mathlib/Data/Nat/Prime/Defs): fuel Nat.minFac t-data merge-conflict awaiting-author failing CI
24514 b-mehta chore(Int/GCD): use fuel in xgcd t-data merge-conflict awaiting-author merge conflict
31152 FernandoChu feat(CategoryTheory): regular categories have strong-epi-mono factorisations t-category-theory merge-conflict awaiting-author merge conflict
31361 alreadydone feat(Algebra/Order): convex subgroups t-order t-algebra merge-conflict awaiting-author merge conflict
29934 smmercuri feat(Field/WithAbs): the lift of a ring homomorphism from `WithAbs v` to `WithAbs w` to their completions FLT merge-conflict WIP ⚠️ labelled WIP
29933 smmercuri chore: fix `def` naming isses in `Normed/Field/WithAbs.lean` merge-conflict WIP labelled WIP
31377 CoolRmal feat: a series of smooth functions that converges (locally) uniformly is smooth new-contributor t-topology merge-conflict awaiting-author merge conflict
30860 FormulaRabbit81 feat(Measure): prove the space of probability measures on a compact space is compact merge-conflict WIP ⚠️ labelled WIP
30504 grunweg feat: add custom elaborators for immersions t-differential-geometry merge-conflict failing CI
27557 chrisflav feat(RingTheory/KrullDimension): dimension of `R / (x)` for a nonzerodivisor t-ring-theory large-import merge-conflict failing CI
25848 joelriou feat/refactor: redefinition of homology + derived categories large-import t-topology t-category-theory merge-conflict WIP labelled WIP
30989 kckennylau feat(RingTheory): Teichmuller map merge-conflict awaiting-author ⚠️ merge conflict
32242 vihdzp feat: missing instances for `OrderDual`/`Lex`/`Colex` t-order merge-conflict merge conflict
27703 vihdzp feat: `le_of_forall_ne` et. al t-order merge-conflict awaiting-author merge conflict
31950 callesonne feat(CategoryTheory/Product/Basic): make `Hom` into a 1-field structure t-category-theory merge-conflict WIP labelled WIP
26464 joelriou feat(LinearAlgebra): generators of pi tensor products file-removed t-algebra merge-conflict awaiting-author merge conflict
31671 vasnesterov feat: `norm_num` extension for `IsSquare` via `Irrational` t-meta merge-conflict WIP labelled WIP
31110 bryangingechen ci: don't delete merged branches CI merge-conflict awaiting-author merge conflict
27364 101damnations feat(RepresentationTheory/Homological/GroupCohomology): cohomology of finite cyclic groups t-algebra merge-conflict awaiting-author merge conflict
30122 xroblot Development branch (1) merge-conflict WIP labelled WIP
28291 vasnesterov feat(Tactic): tactic for computing asymptotics of real functions t-analysis t-meta merge-conflict WIP labelled WIP
32210 ADedecker feat: iteratedFDeriv as a linear map on test functions t-analysis merge-conflict awaiting review
32401 ADedecker feat: monotonicity of D^n(U) in n and in U as CLMs t-analysis merge-conflict merge conflict
30439 plp127 feat: `norm_num` extension for `IsSquare` on `Nat`, `Int`, `Rat` t-meta merge-conflict awaiting-author merge conflict
32419 kim-em fix(scripts/lint-style): improve Mathlib.Init import error messages t-linter merge-conflict awaiting-author merge conflict
30441 linesthatinterlace refactor(`Data/List/Sort`): deprecate and replace `List.Sorted` t-data merge-conflict merge conflict
32127 CoolRmal feat: use IndexedPartition.piecewise to create simple/measurable/strongly measurable functions brownian large-import t-measure-probability merge-conflict merge conflict
29203 Hagb feat(RingTheory/MvPolynomial/Groebner): add Gröbner basis t-ring-theory merge-conflict awaiting-author WIP blocked on another PR
31603 alreadydone chore(Algebra): make `RatFunc` an abbrev t-algebra RFC merge-conflict awaiting-author merge conflict
32425 kim-em feat(Linter/FlexibleLinter): generate Try this: simp only suggestions t-linter merge-conflict ❌? infrastructure-related CI failing
31242 plp127 feat: express filter as supremum of principal filter and free filter t-order merge-conflict awaiting-author merge conflict
13057 alreadydone feat(NumberTheory): characterize elliptic divisibility sequences t-algebra t-number-theory merge-conflict blocked-by-other-PR blocked on another PR
12879 grunweg feat: port ge_or_gt linter from mathlib3 tech debt t-linter 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
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
16887 metinersin feat(ModelTheory/Complexity): define conjunctive and disjunctive formulas new-contributor t-logic 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
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
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
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
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
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
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
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
22321 sinhp feat(CategoryTheory): Locally Cartesian Closed Categories (Definition) 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
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
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
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
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
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
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
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
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
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
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
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
28067 grunweg Docstring enumerations 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
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
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
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
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
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
16553 grunweg WIP: tinkering with orientable manifolds t-differential-geometry merge-conflict blocked-by-other-PR WIP 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
29387 mans0954 feat(Analysis/LocallyConvex/WeakSpace): toWeakSpace_closedAbsConvexHull_eq t-analysis 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
30898 vihdzp feat: characterization of `List.splitBy` large-import t-data merge-conflict 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
30303 franv314 chore(Topology/Instances): add deprecated module new-contributor 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
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
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
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
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
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
31081 chrisflav feat(RingTheory/StandardSmooth): presentation independent characterization t-ring-theory merge-conflict 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
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
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
28468 alreadydone feat(Algebra): ring API for `AddLocalization` t-algebra merge-conflict blocked-by-other-PR blocked on another PR
27953 CoolRmal feat(ProbabilityTheory): Conditional Jensen's Inequality new-contributor t-measure-probability merge-conflict 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
30399 kckennylau feat(RingTheory): make HomogeneousLocalization.map take a graded ring hom 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
5863 eric-wieser feat: add elaborators for concrete matrices t-meta merge-conflict blocked-by-other-PR help-wanted blocked on another PR
18876 GabinKolly feat(ModelTheory/Fraisse): add proof that Fraïssé limits exist t-logic merge-conflict blocked-by-other-PR blocked on another PR
20051 Timeroot feat: `Clone` and some instances t-algebra 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 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 merge-conflict blocked-by-other-PR blocked on another PR
22232 pechersky feat(Algebra/Valued): `AdicExpansion.apprUpto` t-topology merge-conflict blocked-by-other-PR blocked on another PR
22233 pechersky feat(Algebra/Valued): `AdicExpansion.evalAt` t-topology merge-conflict blocked-by-other-PR blocked on another PR
23460 Timeroot feat: Definition of `Clone` t-algebra merge-conflict blocked-by-other-PR blocked on another PR
26061 kckennylau (WIP) feat(AlgebraicGeometry): define Projective Space t-algebraic-geometry merge-conflict blocked-by-other-PR WIP blocked on another PR
26160 oliver-butterley feat(MeasureTheory.VectorMeasure): add several lemmas which characterize variation new-contributor t-measure-probability merge-conflict blocked-by-other-PR 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 merge-conflict blocked-by-other-PR blocked on another PR
26399 ChrisHughes24 refactor(ModelTheory): tidy up proof of Ax-Grothendieck with definable functions t-logic merge-conflict blocked-by-other-PR blocked on another PR
26858 Thmoas-Guan feat(Algebra): Define the associated graded ring to filtered ring t-algebra merge-conflict blocked-by-other-PR blocked on another PR
26859 Thmoas-Guan feat(Algebra): Define associated graded algebra t-algebra merge-conflict blocked-by-other-PR blocked on another PR
26860 Thmoas-Guan feat(Algebra): Define associated graded module t-algebra merge-conflict blocked-by-other-PR blocked on another PR
26861 Thmoas-Guan feat(Algebra): define filtered add group hom t-algebra merge-conflict blocked-by-other-PR blocked on another PR
26862 Thmoas-Guan feat(Algebra): define filtered ring homomorphism t-algebra merge-conflict blocked-by-other-PR blocked on another PR
26863 Thmoas-Guan feat(Algebra): define filtered alghom t-algebra merge-conflict blocked-by-other-PR blocked on another PR
26867 Thmoas-Guan feat(Algebra): filtered module hom t-algebra merge-conflict blocked-by-other-PR blocked on another PR
26868 Thmoas-Guan feat(Algebra): associated graded exact of exact and strict t-algebra merge-conflict blocked-by-other-PR blocked on another PR
26869 Thmoas-Guan feat(Algebra): exact of associated graded exact t-algebra 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 merge-conflict awaiting-author 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 merge-conflict blocked-by-other-PR blocked on another PR
27378 peakpoint refactor(Geometry/Euclidean/Projection): redefine projection and reflection for affine subspaces new-contributor t-euclidean-geometry 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 merge-conflict 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 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 merge-conflict blocked-by-other-PR blocked on another PR
29425 pechersky feat(NumberTheory/Padics/Torsion): `HasEnoughRootsOfUnity ℤ_[p] (p - 1)` t-ring-theory merge-conflict awaiting-author blocked-by-other-PR blocked on another PR
30001 vihdzp feat: concept generated by set of objects/attributes t-order merge-conflict blocked-by-other-PR blocked on another PR
30077 agjftucker feat(Analysis/Calculus/ImplicitFunOfBivariate): define implicitFunOfBivariate t-analysis 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 merge-conflict blocked-by-other-PR blocked on another PR
30312 kckennylau feat(RingTheory): define graded ring homomorphisms t-ring-theory merge-conflict blocked-by-other-PR blocked on another PR
30334 kckennylau feat(RingTheory): define maps of homogeneous ideals t-ring-theory merge-conflict blocked-by-other-PR blocked on another PR
30365 kckennylau feat(RingTheory): define R-linear graded algebra homomorphism merge-conflict blocked-by-other-PR ⚠️ blocked on another PR
30367 kckennylau feat(Data): define grading-preserving isomorphisms t-data merge-conflict blocked-by-other-PR blocked on another PR
30379 kckennylau feat(RingTheory): isomorphism of graded rings merge-conflict 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 merge-conflict blocked-by-other-PR blocked on another PR
31083 joelriou feat(CategoryTheory): properties of objects for pseudofunctors to Cat t-category-theory merge-conflict blocked-by-other-PR WIP blocked on another PR
31580 grunweg feat: towards `ContMDiff` support in fun_prop t-differential-geometry t-meta merge-conflict blocked-by-other-PR WIP blocked on another PR
19475 YaelDillies feat: group markings t-algebra blocked-by-other-PR WIP blocked on another PR
30339 grunweg feat: extend a tangent vector for a locally smooth vector field t-differential-geometry merge-conflict blocked-by-other-PR blocked on another PR
31338 grunweg chore: move Pretrivialization, Trivialization to the Bundle namespace t-differential-geometry merge-conflict blocked-by-other-PR blocked on another PR
31339 grunweg Movelemma 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
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
18784 erdOne feat(AlgebraicGeometry): use `addMorphismPropertyInstances` t-algebraic-geometry merge-conflict blocked-by-other-PR blocked on another PR
19607 madvorak feat: block matrices are totally unimodular merge-conflict blocked-by-other-PR WIP ⚠️ 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
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
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 merge-conflict 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 merge-conflict 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 merge-conflict blocked-by-other-PR ⚠️ blocked on another PR
28718 imbrem feat: class for chosen finite coproducts new-contributor t-category-theory merge-conflict awaiting-author blocked-by-other-PR blocked on another PR
30352 kckennylau feat(RingTheory): Homogeneous localization of tensor product merge-conflict 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 merge-conflict blocked-by-other-PR blocked on another PR
31513 FLDutchmann feat(Tactic): `polynomial` tactic t-meta merge-conflict blocked-by-other-PR blocked on another PR
27694 grunweg feat: Gram-Schmidt orthonormalisation preserves continuity of sections t-differential-geometry merge-conflict blocked-by-other-PR blocked on another PR
27025 grunweg feat: Gram-Schmidt procedure on smooth vector bundles yields smooth sections t-differential-geometry merge-conflict blocked-by-other-PR blocked on another PR
29777 yuanyi-350 feat(Functional Analysis): closed Range Theorem new-contributor t-analysis awaiting-author blocked-by-other-PR WIP blocked on another PR
30982 jsm28 feat(Geometry/Euclidean/Angle/Incenter): angle bisection and the incenter t-euclidean-geometry blocked-by-other-PR blocked on another PR
30831 chrisflav feat(AlgebraicGeometry): the fpqc topology t-algebraic-geometry blocked-by-other-PR blocked on another PR
29764 ScottCarnahan feat(Algebra/Vertex): API up to residue products (WIP) t-algebra merge-conflict blocked-by-other-PR blocked on another PR
28248 YaelDillies feat: binomial random variables t-measure-probability blocked-by-other-PR blocked on another PR
31873 wwylele refactor: re-prove Euler's partition theorem from Glaisher's theorem file-removed merge-conflict 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 merge-conflict blocked-by-other-PR blocked on another PR
29449 mitchell-horner feat(Combinatorics/SimpleGraph): add Turán density related theorems t-combinatorics blocked-by-other-PR blocked on another PR
31113 515801431 feat(Mathlib/Combinatorics/Enumerative/Polya.lean): Add additional theorem in `Polya.lean` new-contributor t-combinatorics blocked-by-other-PR blocked on another PR
30881 FlAmmmmING feat(RingTheory/PowerSeries/Schroder.lean): Define the generating function for large and small Schroder number new-contributor blocked-by-other-PR ⚠️ blocked on another PR
31332 sinhp feat(CategoryTheory): Exponentiable morphisms t-category-theory blocked-by-other-PR blocked on another PR
31729 thorimur chore: log on theorem type signature in unused instances in type linters large-import merge-conflict blocked-by-other-PR blocked on another PR
32157 peabrainiac feat(Analysis/Calculus): Hadamard's lemma t-analysis blocked-by-other-PR blocked on another PR
26966 vihdzp feat: the Dedekind–MacNeille completion t-order merge-conflict awaiting-author blocked-by-other-PR blocked on another PR
23177 faenuccio feat: more lemmas about ordered groups with zero t-order awaiting-CI blocked-by-other-PR WIP blocked on another PR
31018 joelriou feat(CategoryTheory): the κ-accessible category of κ-directed posets t-category-theory merge-conflict blocked-by-other-PR WIP blocked on another PR
31805 joelriou feat(AlgebraicTopology): horns in Δ[n] as multicoequalizers t-algebraic-topology blocked-by-other-PR WIP 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
29996 vihdzp chore(Order/Concept): `IsIntent` and `IsExtent` t-order 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
30375 sinhp feat(CategoryTheory): Basics of Locally Cartesian Closed Categories t-category-theory blocked-by-other-PR WIP blocked on another PR
32000 Thmoas-Guan feat(Algebra): projective dimension equal supremum of localized module blocked-by-other-PR ⚠️ blocked on another PR
32033 Thmoas-Guan feat(Algebra): injective dimension equal supremum of localized module blocked-by-other-PR ⚠️ blocked on another PR
31999 Thmoas-Guan feat(RingTheory): global dimension equals the supremum over localizations awaiting-author blocked-by-other-PR ⚠️ blocked on another PR
29701 Thmoas-Guan feat(Algebra/RingTheory): polynomial over regular ring t-ring-theory blocked-by-other-PR blocked on another PR
31046 Thmoas-Guan feat(Homology) : compatibility of map between `Ext` t-category-theory blocked-by-other-PR blocked on another PR
31697 Thmoas-Guan feat(Homology): bijection between `Ext` t-algebra t-category-theory blocked-by-other-PR blocked on another PR
31325 joelriou feat(AlgebraicTopology): a computable monoidal functor instance for `hoFunctor` t-algebraic-topology merge-conflict blocked-by-other-PR blocked on another PR
31222 Thmoas-Guan feat(Algebra): `Hom` commute with flat base change large-import blocked-by-other-PR ⚠️ blocked on another PR
30373 sinhp feat(CategoryTheory) : LCCC sections (constructing right adjoint to `Over.ChosenPullback.pullback`) t-category-theory blocked-by-other-PR blocked on another PR
30576 smmercuri feat: `adicCompletion` for `Rat` is uniform isomorphic to `Padic` blocked-by-other-PR WIP ⚠️ blocked on another PR
32021 jsm28 feat(Geometry/Euclidean/Altitude): `map` and `restrict` lemmas t-euclidean-geometry 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
31919 alreadydone feat(RingTheory): integrally closed subring of a field is intersection of valuation subrings t-ring-theory blocked-by-other-PR blocked on another PR
31135 kckennylau feat(RingTheory): is localization iff is localization on saturation merge-conflict blocked-by-other-PR ⚠️ blocked on another PR
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
31350 grunweg feat: (unoriented) bordism groups 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
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
30240 luigi-massacci feat(Analysis/Distribution/ContDiffMapSupportedIn): Add a wrapper for fderiv on D_K^n t-analysis blocked-by-other-PR blocked on another PR
29274 Jlh18 feat(CategoryTheory): HasLimits instance on Grpd file-removed t-category-theory blocked-by-other-PR blocked on another PR
32125 SnirBroshi feat(SimpleGraph/Walks/Subwalks): `p₁.IsSubwalk p₂ ↔ p₁.darts <:+: p₂.darts` and similar theorems t-combinatorics blocked-by-other-PR blocked on another PR
31560 AntoineChambert-Loir feat(Topology/Sion): the minimax theorem of von Neumann - Sion blocked-by-other-PR ⚠️ blocked on another PR
27493 themathqueen feat(RingTheory/Coalgebra): define Frobenius algebra t-ring-theory awaiting-author blocked-by-other-PR blocked on another PR
32260 jsm28 feat(Geometry/Euclidean/Angle/Oriented/Affine): oriented angle bisection and halving unoriented angles t-euclidean-geometry blocked-by-other-PR blocked on another PR
28796 grunweg feat: immersions are smooth t-differential-geometry merge-conflict blocked-by-other-PR WIP blocked on another PR
32202 joelriou feat(AlgebraicTopology): finite simplicial sets t-algebraic-topology blocked-by-other-PR WIP blocked on another PR
32237 joelriou feat(AlgebraicTopology): binary products of standard simplices t-algebraic-topology blocked-by-other-PR WIP blocked on another PR
32251 joelriou feat(AlgebraicTopology): binary products of finite simplicial sets are finite t-algebraic-topology blocked-by-other-PR WIP blocked on another PR
32265 joelriou feat(AlgebraicTopology): finite colimits of finite simplicial sets are finite t-algebraic-topology blocked-by-other-PR WIP blocked on another PR
30129 vlad902 feat(SimpleGraph): define and prove basic theory of vertex covers t-combinatorics blocked-by-other-PR blocked on another PR
32270 jsm28 feat(Geometry/Euclidean/Incenter): `map` and `restrict` lemmas t-euclidean-geometry blocked-by-other-PR blocked on another PR
32273 jsm28 feat(Analysis/Convex/Side): affine combinations on same / opposite side of face of a simplex as a vertex t-convex-geometry t-analysis blocked-by-other-PR blocked on another PR
32278 jsm28 feat(Geometry/Euclidean/Incenter): excenters on sides of faces t-euclidean-geometry blocked-by-other-PR blocked on another PR
32266 joelriou feat(AlgebraicTopology): finite simplicial sets are `ℵ₀`-presentable, t-algebraic-geometry blocked-by-other-PR WIP blocked on another PR
32282 jsm28 feat(Geometry/Euclidean/Angle/Incenter): unoriented angle bisection t-euclidean-geometry blocked-by-other-PR blocked on another PR
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
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
31892 jsm28 feat(Geometry/Euclidean/Sphere/PolePolar): poles and polars t-euclidean-geometry blocked-by-other-PR blocked on another PR
31893 jsm28 feat(Geometry/Euclidean/Sphere/Tangent): characterize `tangentsFrom` t-euclidean-geometry blocked-by-other-PR blocked on another PR
31981 jsm28 feat(Geometry/Euclidean/Incenter): `tangentSet` and `tangentsFrom` lemmas t-euclidean-geometry blocked-by-other-PR blocked on another PR
32307 mcdoll feat(Analysis/Distribution): `(1 + |x|^2)^r` has temperate growth t-analysis blocked-by-other-PR WIP blocked on another PR
32308 joelriou feat(Algebra/Homology): the bifunctor `F.map₂CochainComplex` commutes with shifts t-category-theory blocked-by-other-PR WIP blocked on another PR
32317 joelriou feat(CategoryTheory): natural transformations between bifunctors which commute to shifts in two variables t-category-theory blocked-by-other-PR WIP blocked on another PR
32319 urkud feat: add `ContDiffAt.continuousAt_fderiv` etc t-analysis blocked-by-other-PR blocked on another PR
30532 Thmoas-Guan feat(Homology) : `Ext` commute with flat base change large-import t-category-theory merge-conflict blocked-by-other-PR blocked on another PR
32171 Thmoas-Guan feat(RingTheory): polynomial over Gorenstein ring is Gorenstein t-ring-theory large-import merge-conflict 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
28462 joelriou feat(AlgebraicTopology/SimplicialSet): the relative cell complex attached to a rank function for a pairing t-algebraic-topology blocked-by-other-PR WIP blocked on another PR
32347 joelriou feat(AlgebraicTopology/SimplicialSet): structures to study homotopy groups of Kan complexes t-algebraic-topology blocked-by-other-PR blocked on another PR
27706 xroblot feat(RingTheory/Localization/AtPrime): inertia degree and ramification index are preserved by localization t-ring-theory blocked-by-other-PR blocked on another PR
30927 callesonne feat(Bicategory/Yoneda): add the yoneda pseudofunctor 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
30811 yonggyuchoimath feat(AlgebraicGeometry.EffectiveEpi): effective epimorphisms in schemes 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
32027 alreadydone feat(Counterexamples): invertible module not isomorphic to any ideal t-ring-theory merge-conflict blocked-by-other-PR ❌? blocked on another PR
30931 Thmoas-Guan feat(RingTheory): Gorenstein local ring is Cohen Macaulay large-import merge-conflict blocked-by-other-PR ❌? ⚠️ blocked on another PR
26291 RemyDegenne feat(Probability): Cameron-Martin theorem t-measure-probability blocked-by-other-PR WIP blocked on another PR*
31749 YaelDillies refactor: make `LinearOrderedCommMonoidWithZero`s cancellative file-removed large-import t-algebra blocked-by-other-PR 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
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*
32147 EtienneC30 feat: independence of Gaussian random variables brownian t-measure-probability blocked-by-other-PR blocked on another PR
32330 ADedecker feat: postcomposition by a CLM as a CLM on test functions t-analysis blocked-by-other-PR blocked on another PR
31809 ADedecker feat: differentiation of test function as a CLM t-analysis blocked-by-other-PR blocked on another PR
32211 ADedecker feat: inclusion from `ContDiffMapSupportedIn` to `TestFunction` is a topological embedding t-analysis merge-conflict blocked-by-other-PR blocked on another PR
32269 EtienneC30 feat: introduce Gaussian processes brownian t-measure-probability blocked-by-other-PR blocked on another PR
32334 EtienneC30 feat: independence of Gaussian processes brownian t-measure-probability blocked-by-other-PR blocked on another PR
32410 callesonne feat(Bicategory/FunctorCategory/Pseudo): Add evaluation pseudofunctor t-category-theory blocked-by-other-PR WIP blocked on another PR
29819 mcdoll feat(Analysis/Distribution): tempered distributions t-analysis merge-conflict blocked-by-other-PR WIP 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
32418 Thmoas-Guan feat(RingTheory): Gorenstein local ring is Cohen--Macaulay local ring of type 1 merge-conflict blocked-by-other-PR ❌? ⚠️ blocked on another PR
32294 jsm28 feat(Geometry/Euclidean/Angle/Incenter): distance from second intersection with circumcircle t-euclidean-geometry blocked-by-other-PR blocked on another PR
32295 jsm28 feat(Archive/Imo/Imo2024Q4): IMO 2024 Q4 IMO blocked-by-other-PR blocked on another PR
30817 joelriou feat(CategoryTheory): `κ`-continuous presheaves t-category-theory blocked-by-other-PR WIP labelled WIP
30847 joelriou feat(CategoryTheory/Presentable): the representation theorem t-category-theory merge-conflict blocked-by-other-PR WIP blocked on another PR
30247 joelriou feat(CategoryTheory): categories of presheaves are locally presentable t-category-theory blocked-by-other-PR WIP blocked on another PR
31187 loefflerd feat(NumberTheory/LSeries): Define the L-series of a modular form t-number-theory blocked-by-other-PR WIP blocked on another PR
30799 YaelDillies refactor: unify the two versions of `pow_eq_one_iff` file-removed 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 blocked on another PR
29534 Thmoas-Guan feat(Algebra): global dimension of regular local ring large-import merge-conflict blocked-by-other-PR ⚠️ blocked on another PR
29699 Thmoas-Guan feat(Algebra/RingTheory): global dimension of regular ring large-import merge-conflict blocked-by-other-PR ⚠️ blocked on another PR
29703 Thmoas-Guan feat(Algebra/RingTheory): Hilbert's Syzygy theorem (projective version) large-import merge-conflict blocked-by-other-PR ⚠️ blocked on another PR
29796 Thmoas-Guan feat(RingTheory): regular of finite global dimension large-import merge-conflict blocked-by-other-PR ⚠️ blocked on another PR
29802 Thmoas-Guan feat(Algebra/RingTheory): Auslander–Buchsbaum–Serre criterion and its corollaries large-import merge-conflict blocked-by-other-PR ⚠️ blocked on another PR
31644 Thmoas-Guan feat(Algebra): projective dimension of quotient regular sequence t-ring-theory merge-conflict awaiting-author blocked-by-other-PR blocked on another PR
31768 Thmoas-Guan feat(Homology): `Ext` commute with ulift functor t-algebra t-category-theory merge-conflict blocked-by-other-PR blocked on another PR
31851 Thmoas-Guan feat(Algebra/Homology): Injective dimension in linear equiv t-algebra merge-conflict blocked-by-other-PR blocked on another PR
31884 Thmoas-Guan feat(RingTheory): definition of Gorenstein local ring merge-conflict blocked-by-other-PR ⚠️ blocked on another PR
32035 Thmoas-Guan feat(RingTheory): localization of Gorenstein local ring merge-conflict blocked-by-other-PR ⚠️ blocked on another PR
32098 Thmoas-Guan feat(RingTheory): injective dimension of quotSMulTop merge-conflict 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
26216 Thmoas-Guan feat(Algebra): depth of QuotSMulTop large-import t-algebra blocked-by-other-PR blocked on another PR
28683 Thmoas-Guan feat(RingTheory): regular local ring is domain t-ring-theory blocked-by-other-PR WIP blocked on another PR
32305 faenuccio feat: define Weak Derivatives large-import t-analysis merge-conflict blocked-by-other-PR WIP blocked on another PR
30551 smmercuri feat: dimension formulae for infinite places above merge-conflict blocked-by-other-PR WIP ⚠️ blocked on another PR
31885 CoolRmal feat: Integrable if UI + convergence in measure brownian t-measure-probability blocked-by-other-PR 🟤 blocked on another PR
32454 Hagb chore: simplify some proofs with `wlog!` blocked-by-other-PR blocked on another PR
32105 joelriou feat(CategoryTheory): computing Ext-groups using an injective resolution large-import t-category-theory blocked-by-other-PR WIP labelled WIP
26215 Thmoas-Guan feat(Algebra): Auslander–Buchsbaum theorem large-import t-algebra blocked-by-other-PR blocked on another PR
32081 Thmoas-Guan feat(RingTheory/Homology): `Ext` over Noetherian ring finitely generated t-algebra t-category-theory 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
26217 Thmoas-Guan feat(Algebra): Ischebeck theorem large-import t-algebra blocked-by-other-PR 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
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