Why is my PR not on the queue?

This page was last updated on: December 13, 2025 at 11:56 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 awaiting-author t-analysis awaiting author
9510 eric-wieser feat(Analysis/Calculus/DualNumber): Extending differentiable functions to dual numbers WIP awaiting-CI t-analysis t-algebra labelled WIP
14563 awueth feat: if-then-else of exclusive or statement awaiting-author t-algebra new-contributor awaiting author
10387 adomani feat(Tactic/ComputeDegree): add `polynomial` tactic WIP t-meta RFC labelled WIP
13163 erdOne feat(.vscode/module-docstring.code-snippet): Prevent auto-complete from firing on `do` awaiting-author t-meta awaiting author
16253 Shreyas4991 feat: Basics of Discrete Fair Division in Mathlib WIP awaiting-author ⚠️ labelled WIP
15121 Eloitor feat: iff theorems for IsSplitEpi and IsSplitMono in opposite category awaiting-author t-category-theory new-contributor failing CI
15895 madvorak feat(Computability/ContextFreeGrammar): mapping between two types of nonterminal symbols WIP t-computability labelled WIP
16570 yuma-mizuno chore(Tactic/CategoryTheory): change `TermElabM` to `MetaM` WIP t-meta labelled WIP
10591 adri326 feat(Topology/Algebra/ConstMulAction): properties of continuous actions in Hausdorff spaces awaiting-author t-topology t-algebra awaiting author
10796 mcdoll feat(Tactic/Positivity): non-negativity of functions WIP t-meta labelled WIP
14603 awueth feat: degree is invariant under graph isomorphism WIP t-combinatorics new-contributor labelled WIP
20459 Ruben-VandeVelde chore: fix names of roots_C_mul_X_{add,sub}_C_of_IsUnit awaiting-author t-algebra awaiting author
18461 hannahfechtner feat: left and right common multiples mixins awaiting-author t-algebra new-contributor awaiting author
15355 adomani feat: MiM PR report WIP ⚠️ labelled WIP
21495 alreadydone experiment: reducible HasQuotient.quotient' WIP bench-after-CI labelled WIP
21501 sksgurdldi feat(List): add sum_zipWith_eq_finset_sum awaiting-author t-algebra new-contributor awaiting author
20636 eric-wieser feat: multiplication of intervals in rings awaiting-author t-algebra awaiting author
22784 grunweg feat: add Diffeomorph.sumSumSumComm WIP t-differential-geometry labelled WIP
23042 joneugster feat(CategoryTheory/Enriched/Limits): add HasConicalLimitsOfSize.shrink WIP t-category-theory infinity-cosmos labelled WIP
23142 joneugster feat(CategoryTheory/Enriched/Limits): add API for HasConicalLimit awaiting-author t-category-theory infinity-cosmos awaiting author
22888 plp127 perf: replace `Lean.Expr.swapBVars` with a better? implementation awaiting-author t-meta awaiting author
13038 adomani feat: Mathlib weekly reports awaiting-author t-meta CI 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 WIP t-algebra toric labelled WIP
18861 YaelDillies refactor: make `Set.mem_graphOn` defeq awaiting-author t-data failing CI
22809 b-reinke feat: Category algebras and path algebras WIP t-category-theory t-algebra new-contributor labelled WIP
22488 smmercuri fix: lower priority for `UniformSpace.Completion.instSMul` awaiting-author t-topology FLT awaiting author
24665 Komyyy feat(Mathlib/Topology/Metrizable/Uniformity): every uniform space is generated by a family of pseudometrics WIP t-topology labelled WIP
24155 eric-wieser feat: add a "rw_proc" for fin vectors awaiting-author t-meta RFC t-data awaiting author
21276 GabinKolly feat(ModelTheory/Substructures): define equivalences between equal substructures awaiting-author t-logic awaiting author
24008 meithecatte chore(EpsilonNFA): replace manual lemmas with @[simps] awaiting-author new-contributor t-computability awaiting author
24618 b-mehta feat(Analysis): add Schur inequality and variants WIP t-analysis 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 delegated CI delegated
23929 meithecatte feat(Computability/NFA): improve bound on pumping lemma new-contributor t-computability awaiting-zulip awaiting a zulip discussion
21344 kbuzzard chore: attempt to avoid diamond in OreLocalization please-adopt t-algebra looking for help
25921 BoltonBailey feat: scripts to analyze overlap between namespaces WIP t-meta migrated-from-branch 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 awaiting-author t-algebra 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 awaiting-author easy t-topology awaiting author
27069 FrankieNC feat(Analysis/MetricSpace/HausdorffDimension): prove dimH of intervals and segments is 1 awaiting-author t-topology new-contributor awaiting author
18230 digama0 feat(Tactic/ScopedNS): extend `scoped[NS]` to more commands awaiting-author t-meta awaiting author
27435 callesonne feat(Normed/Algebra/Logarithm): add FormalMultilinearSeries of logarithm around `1` WIP t-analysis labelled WIP
27507 grunweg wip(commandStart): check the indentation of declaration keywords also WIP t-linter labelled WIP
27704 vihdzp feat: link `Minimal` and `IsLeast` together awaiting-author t-order failing CI
27813 javra feat: IMO 2025 Q1 WIP IMO labelled WIP
27826 Louddy feat(Subsemiring): mk_eq_zero WIP t-algebra labelled WIP
27050 BoltonBailey doc(Control/Monad/Cont): add docstrings awaiting-author t-data failing CI
25916 BoltonBailey feat: add `simp` lemma `coeff_eq_zero_of_not_mem_support` awaiting-author t-algebra failing CI
27225 eric-wieser refactor(Tactic/Lift): deprecate the third with argument awaiting-author t-meta awaiting author
28075 tristan-f-r chore(Finsupp/Indicator): make non-classical awaiting-author easy t-data awaiting author
27444 grunweg feat: generalise more lemmas to enorms WIP carleson ⚠️ labelled WIP
27226 xcloudyunx feat(Combinatorics/SimpleGraph): Add Subgraph.inclusion_edge_apply_coe and inclusion_edgeSet_apply_coe awaiting-author t-combinatorics new-contributor awaiting author
22925 ggranberry feat(Mathlib/PlaceHolder/ToeplitzHausdorff): Toeplitz-Hausdorff help-wanted WIP awaiting-author t-analysis new-contributor will-close-soon looking for help
26349 mans0954 feat(Analysis/SpecialFunctions/Trigonometric/Basic): sin and cos of multiples of π / 3 help-wanted t-analysis looking for help
5897 eric-wieser feat: add a `MonadError` instance for `ContT` awaiting-author t-meta awaiting author
28631 faenuccio feat(Data\Nat\ModEq.lean): add grind attribute to ModEq WIP t-data labelled WIP
27752 plp127 feat(Order): `NoBotOrder α` implies `NoMinOrder α` under `IsDirected α (· ≥ ·)` awaiting-author t-order failing CI
26645 erdOne feat(RingTheory/PowerSeries): Construction of `Q` such that `P(Q(X)) = X` awaiting-author t-ring-theory awaiting author
28680 vihdzp feat: set has cardinality one iff singleton awaiting-author easy t-set-theory awaiting author
26078 kckennylau feat(AlgebraicGeometry): add x, y, px, py for points on elliptic curves awaiting-author t-algebraic-geometry awaiting author
27479 iu-isgood feat: Abel's Binomial Theorem awaiting-author new-contributor t-data failing CI
25700 grunweg feat: lint upon uses of the `mono` tactic please-adopt RFC t-linter looking for help
24719 madvorak feat(LinearAlgebra/Matrix/NonsingularInverse): inverting `Matrix` inverts its `LinearEquiv` awaiting-author t-algebra awaiting author
24373 YaelDillies refactor: golf `modularCharacter` awaiting-CI t-measure-probability does not pass CI
26299 adomani perf: the `commandStart` linter only acts on modified files awaiting-author t-linter awaiting author
29232 vihdzp feat: more theorems on `SuccAddOrder` t-algebra t-order failing CI
26935 Paul-Lez feat(Analysis/SpecialFunction/NthRoot): definition and basic API of Real.nthRoot t-analysis failing CI
27995 kckennylau feat(RingTheory/Valuation): alternate constructors for Valuation awaiting-CI t-ring-theory does not pass CI
26159 upobir feat(Algebra/QuadraticDiscriminant): Adding inequalities on quadratic from inequalities on discriminant awaiting-author t-algebra awaiting author
27701 vihdzp feat: `a < b + c ↔ a < b ∨ ∃ d < c, a = b + d` awaiting-author t-algebra awaiting author
26462 PSchwahn feat(LinearAlgebra/Projection): add results about inverse of `Submodule.prodEquivOfIsCompl` awaiting-author t-algebra new-contributor awaiting author
28286 bwangpj feat(Geometry/Manifold/ContMDiff): basic lemmas for analytic (`C^ω`) functions awaiting-author t-differential-geometry new-contributor awaiting author
29527 kim-em feat: script for checking Github URLs WIP CI labelled WIP
25778 thefundamentaltheor3m feat: Monotonicity of `setIntegral` for nonnegative functions awaiting-author t-measure-probability new-contributor awaiting author
29615 eric-wieser chore: add a computable shortcut for `AddCommMonoid ℂ` easy t-analysis bench-after-CI failing CI
29010 grunweg chore: more tests for field_simp features and edge cases failing CI
27937 madvorak feat(Logic/Basic): `congr_heq₂` awaiting-author t-logic awaiting author
29870 mckoen feat(CategoryTheory/Adhesive): subobjects in adhesive categories have binary coproducts WIP t-category-theory labelled WIP
29588 Periecle feat(Analysis/Complex/Residue): Implement residue theory for complex functions at isolated singularities awaiting-author t-analysis new-contributor failing CI
24050 Paul-Lez feat(Data/Finsupp/Pointwise): generalise pointwise scalar multiplication of finsupps awaiting-author t-data awaiting author
26330 Timeroot feat: "Junk value" test file awaiting-author t-data awaiting author
28452 plp127 feat: Define `ZMod.fintype` without cases awaiting-author t-data awaiting author
30142 shalliso feat(Topology/Baire): define IsNonMeagre t-topology new-contributor failing CI
30079 dagurtomas feat(CategoryTheory): IsSheafFor as a multiequalizer condition WIP t-category-theory labelled WIP
19860 YaelDillies refactor: review the `simps` projections of `OneHom`, `MulHom`, `MonoidHom` WIP t-algebra labelled WIP
28630 Antidite feat(Archive/Imo): right isosceles configuration in the complex plane awaiting-author new-contributor IMO awaiting author
27073 pechersky feat(Archive/Examples/Local): files showcasing properties of local fields awaiting-author t-number-theory awaiting author
30135 erdOne feat(RingTheory): `ValuativeRel` on subrings awaiting-author t-ring-theory awaiting author
26284 plp127 feat: faster implementation of `Nat.primeFactorsList` + `@[csimp]` lemma awaiting-author t-data awaiting author
27302 tristan-f-r feat(Fintype/Quotient): finLiftOn₂ awaiting-author t-data awaiting author
29432 lecopivo feat: `data_synth` tactic to prove `HasFDerivAt 𝕜 f ?f' x` and similar WIP t-meta labelled WIP
29855 eric-wieser chore(Data/Finset/Sort): lemmas about `0 : Fin _` and `Fin.last _` delegated easy t-order t-data failing CI
29634 YaelDillies feat: missing instance `NonUnitalCommSemiring R → NonUnitalNonAssocCommSemiring R` help-wanted awaiting-CI t-algebra looking for help
30460 janithamalith feat(Nat): add lemma nat_card_orbit_mul_card_stabilizer_eq_card_group awaiting-author new-contributor t-group-theory awaiting author
25737 robin-carlier feat(AlgebraicTopology/SimplexCategory/GeneratorsRelations/NormalForms): Normal forms for `P_δ`s delegated t-category-theory t-algebraic-topology failing CI
30209 Ruben-VandeVelde feat: some TwoSidedIdeal.span lemmas awaiting-author FLT t-ring-theory awaiting author
25225 xcloudyunx feat(Combinatorics/SimpleGraph): Eulerian walk in connected graph contains all vertices awaiting-author t-combinatorics new-contributor awaiting author
27817 zhuyizheng feat: add IMO2025P1 awaiting-author new-contributor IMO awaiting author
27206 grhkm21 feat(CategoryTheory/Adjunction): partial adjoints are adjoints awaiting-author t-category-theory failing CI
27196 YaelDillies refactor(Polynomial/Bivariate): swap `X` and `Y` for improved notation WIP t-algebra toric labelled WIP
26088 grunweg chore(Linter/DirectoryDependency): move forbidden directories into a JSON file please-adopt t-linter looking for help
30828 DeVilhena-Paulo feat: implementation of `Finmap.merge` new-contributor t-data failing CI
30902 adomani chore: longLine warnings happen starting at the 101st character t-linter awaiting-zulip awaiting a zulip discussion
30378 mans0954 refactor(Order/Hom/Lattice): Use default `initialize_simps_projections` configuration for `LatticeHom`. awaiting-author t-order awaiting author
30667 FrederickPu Subgroup mul awaiting-author t-algebra new-contributor awaiting author
30975 mariainesdff feat(Data/Finsupp/Defs): add Finsupp.restrict awaiting-author t-data 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 awaiting-author t-analysis new-contributor awaiting author
29871 zach1502 feat(Matrix/Transvection): Gauss pivot determinant identity and pivot preservation awaiting-author t-algebra new-contributor awaiting author
30109 scholzhannah feat: the subcomplexes of a (relative classical) CW complex form a completely distributive lattice awaiting-author t-topology awaiting author
30158 nicolaviolette feat: combinatorics simplegraph basic awaiting-author t-combinatorics new-contributor 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 new-contributor FLT t-group-theory failing CI
27516 gaetanserre feat: add rational approximation lemma for suprema in `unitInterval` awaiting-author t-topology awaiting author
30608 grunweg feat: another lemma about derivatives of parametric integrals awaiting-author t-analysis awaiting author
30612 grunweg feat: add ContDiff.lipschitzOnWith awaiting-author t-analysis awaiting author
30560 dwrensha fix(LinearAlgebra/Alternating/Basic): avoid deep recursion in MultilinearMap.alternatization awaiting-author t-algebra awaiting author
31226 erdOne chore(RingTheory): add `@[ext]` to `Ideal.Quotient.algHom_ext` awaiting-author easy t-ring-theory awaiting author
31348 PatrickMassot chore: fix a docstring typo documentation awaiting-author easy t-analysis awaiting author
29145 JovanGerb chore: use `to_additive` in more places t-meta awaiting-CI does not pass CI
29458 LiamSchilling feat(MvPolynomial/WeightedHomogenous): relate `weightedTotalDegree` to `degrees` and `degreeOf` awaiting-author new-contributor t-ring-theory awaiting author
25765 JovanGerb feat(gcongr): lemma for rewriting inside divisibility delegated t-data delegated
31607 grunweg chore: rename `continuous{,On,At,Within}_const to `ContinuousFoo.const` delegated awaiting-CI does not pass CI
31637 Whysoserioushah feat(Data/Matrix/Basis): add some lemmas awaiting-author t-data awaiting author
30562 dwrensha fix(Data/Fintype/Perm): make the main logic of Equiv.instFintype irreducible awaiting-author t-data awaiting author
26885 pechersky feat(Topology/ValuativeRel): ValuativeTopology 𝒪[K] t-number-theory t-topology t-algebra failing CI
31326 sgouezel chore: deprecate `smooth` variants of `contMDiff` results awaiting-author t-differential-geometry failing CI
12032 mcdoll feat: delta distribution as a limit WIP t-analysis labelled WIP
24965 erdOne refactor: Make `IsLocalHom` take unbundled map delegated t-algebra delegated
22464 adomani feat(CI): declarations diff in Lean awaiting-author CI awaiting author
26777 YaelDillies chore(Data/Set/Image): move `BooleanAlgebra` material to `Order` WIP t-data labelled WIP
24383 YaelDillies feat: distributive Haar characters of `ℝ` and `ℂ` WIP awaiting-CI t-measure-probability FLT file-removed labelled WIP
23881 YaelDillies feat: `ℝ≥0`-valued Lᵖ norm awaiting-author t-measure-probability awaiting author
21915 YaelDillies feat: simproc for `Int.divisorsAntidiag` WIP t-meta labelled WIP
21342 YaelDillies refactor(Normed/Group/Quotient): generalise to non-abelian groups WIP t-analysis labelled WIP
15443 YaelDillies feat: Marcinkiewicz-Zygmund inequality WIP t-analysis labelled WIP
31263 LiranShaul feat: arbitrary product of injective modules is injective awaiting-author t-algebra new-contributor awaiting author
31590 SuccessMoses chore: tag `commutatorElement_def` with `simp` awaiting-author t-algebra new-contributor failing CI
25802 dagurtomas feat(AlgebraicTopology): anodyne morphisms of simplicial sets WIP t-topology labelled WIP
6859 MohanadAhmed feat: TryLean4Bundle: Windows Bundle Creator help-wanted WIP CI looking for help
12452 JADekker feat(Cocardinal): add some more api awaiting-CI t-topology ??? does not pass CI
19062 hannahfechtner feat(Algebra/PresentedMonoid/Basic): facts about rel awaiting-author t-algebra awaiting author
23772 SEU-Prime feat: Amice equivalence WIP t-number-theory ??? labelled WIP
24533 robertmaxton42 feat(ULift): conjugation by ULift.up/down, misc cast/heq lemmas awaiting-author t-data awaiting author
25034 ScottCarnahan feat(Algebra/Module/Equiv/Basic): Restriction of scalars from a semilinear equivalence to a linear equivalence WIP t-algebra labelled WIP
25035 ScottCarnahan feat(Algebra/Module/Equiv/Defs): linear equivalence between linear hom and semilinear hom WIP t-algebra labelled WIP
26013 tsuki8 feat(Data/Finset/Card,Data/Set/Finite/Basic): TODO needs a better title awaiting-author new-contributor t-data awaiting author
26881 emo916math feat(Analysis/Calculus/Deriv/Star): a formula for `deriv (conj ∘ f ∘ conj)` awaiting-author t-analysis new-contributor awaiting author
27991 sinianluoye feat(Rat): add Rat.den_eq_of_add_den_eq_one and its dependent lemmas awaiting-author new-contributor t-data failing CI
29921 mans0954 refactor(RingTheory/Polynomial/SmallDegreeVieta): convert to {p : R[X]} (hp : p.natDegree = 2) awaiting-author t-ring-theory awaiting author
25907 mans0954 feat: low order roots of unity awaiting-author t-algebra awaiting author
26765 KiringYJ feat(MeasureTheory/PiSystem): add π-λ theorem and SetLike instance awaiting-author t-measure-probability new-contributor awaiting author
31719 maksym-radziwill feat: Borel-Caratheodory (2nd revision) awaiting-author t-analysis failing CI
29409 Julian feat(Mathlib/Analysis): deriv_eq_self and deriv_exp_iff awaiting-author t-analysis awaiting author
22366 kim-em feat: `check_equalities` tactic for diagnosing defeq problems delegated t-meta failing CI
31854 erdOne chore(AlgebraicGeometry): API for `𝒪ₓ`-modules awaiting-author t-algebraic-geometry 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 awaiting-author t-topology failing CI
29434 ntapiam feat(NonAssoc/LieAdmissible): prove every ring/algebra is LieAdmissible t-algebra new-contributor failing CI
29151 yuanyi-350 feat: Corollary of Hahn–Banach theorem awaiting-author new-contributor ⚠️ awaiting author
29856 mans0954 feat(Analysis/Normed/Ring/Basic): Add NonUnitalNonAssocSeminormedRing and NonUnitalNonAssocNormedRing awaiting-author t-analysis awaiting author
28141 YaelDillies chore: deprecate `BialgHom.coe_toLinearMap` awaiting-zulip toric t-ring-theory awaiting a zulip discussion
30637 strihanje01 feat(Combinatorics/SetFamily/Lindstrom): Lindstrom's theorem for subfamilies with equal unions t-combinatorics new-contributor 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` awaiting-author t-algebra awaiting author
31965 bwangpj feat: fiber of RingHom.specComap awaiting-author t-ring-theory awaiting author
31571 erdOne feat(RingTheory): existence of local algebra with given residue field awaiting-author t-ring-theory awaiting author
31176 mcdoll feat(Analysis): Taylor's theorem with the integral remainder awaiting-author t-analysis awaiting author
30350 joelriou feat(AlgebraicGeometry): the pseudofunctor which sends a scheme to its category of sheaves of modules awaiting-author t-algebraic-geometry awaiting author
30432 kckennylau feat(AlgebraicGeometry): define the non-vanishing locus of a set in Proj awaiting-author t-algebraic-geometry awaiting author
31989 Thmoas-Guan feat(RingTheory): add ideal fg of Noetherian lemma awaiting-author easy t-ring-theory awaiting author
25835 erdOne WIP: Weierstrass elliptic functions WIP t-analysis 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 awaiting-author t-algebra t-ring-theory failing CI
30995 kckennylau feat(RingTheory): replace ofLinearEquiv with limit awaiting-author t-ring-theory awaiting author
32094 grunweg feat(runLinter): allow only running certain linters CI t-linter failing CI
31366 FaffyWaffles feat(Analysis/SpecialFunctions/StirlingRobbins): Robbins' sharp stepwise bound for stirlingSeq awaiting-author t-analysis new-contributor awaiting author
31796 dobronx1325 feat(Data/Real/EReal): add mul_lt_mul_of_pos_left theorem new-contributor t-data failing CI
27258 JovanGerb feat: Imo2020 q6 awaiting-author IMO awaiting author
31755 kaantahti feat(Combinatorics): Add Sperner's Lemma formalization WIP t-combinatorics new-contributor labelled WIP
30030 JonBannon feat(MeasureTheory): add `MemLp.Const` class and instances to unify `p = ∞` and `μ.IsFiniteMeasure` cases awaiting-author t-measure-probability failing CI
31315 Parcly-Taxel feat: IMO 2010 Q5 awaiting-author IMO awaiting author
30744 grunweg feat: more extensions for differential geometry elaborators t-meta t-differential-geometry failing CI
30886 urkud feat(DifferentialForm): exterior derivative applied to vector fields t-analysis awaiting review
30750 SnirBroshi feat(Data/Quot): `toSet` and `equivClassOf` awaiting-author awaiting-zulip t-data awaiting a zulip discussion
26588 faenuccio feat(Algebra/GroupWithZero/WithZero): add the multiplicative embedding with zero from the range t-algebra t-order failing CI
32039 HugLycan Feat/positivity-zeroness WIP t-meta new-contributor labelled WIP
31500 zcyemi feat(Analysis/Convex/Between): add lemmas on affine independence under strict betweenness awaiting-author t-convex-geometry awaiting author
32042 chrisflav feat(AlgebraicGeometry): quasi compact covers t-algebraic-geometry awaiting review
32169 saodimao20 feat: add convolution_comp_add_right awaiting-author t-analysis new-contributor awaiting author
28944 linesthatinterlace refactor(Order/Hom/Basic): reorder definitions t-order 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… awaiting-author t-topology new-contributor awaiting author
31836 hanwenzhu chore(MeasureTheory/IntervalIntegral): generalize fundamental theorem of calculus to `HasDerivWithinAt` instead of `HasDerivAt` awaiting-author t-analysis t-measure-probability awaiting author
31987 saodimao20 feat: add monotonicity and relation lemmas for mgf and cgf t-measure-probability new-contributor awaiting review
26389 jjdishere feat(RingTheory): Perfectoid Field WIP t-topology t-analysis t-algebra labelled WIP
26390 jjdishere feat(Topology/Algebra): Krasner's lemma WIP t-number-theory t-topology t-algebra labelled WIP
28786 mitchell-horner feat(Combinatorics/SimpleGraph): restate Turán's theorem in terms of `extremalNumber` t-combinatorics awaiting review
30921 EtienneC30 feat: characterizing Gaussian measures through the shape of the characteristic function t-measure-probability brownian awaiting review
31180 CoolRmal feat(Analysis): a closed convex set is the intersection of countably many half-spaces in a separable Banach space awaiting-author t-analysis new-contributor failing CI
21031 YaelDillies chore: get rid of generic hom coercions WIP labelled WIP
31988 winstonyin feat: Uniqueness of implicit function t-analysis awaiting review
32165 yuanyi-350 feat(Real/Trigonometric): Add `sum_cos_arith_progression` and prepare for Dirichlet kernel awaiting-author t-analysis awaiting author
32152 Lingyin00 feat(GroupTheory/SpecificGroups/Cyclic): generalize the proof of prime_card by not assuming Finite awaiting-author new-contributor t-group-theory awaiting author
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 review
30505 mariainesdff feat(NumberTheory/RatFunc/Ostrowski): prove Ostrowski's theorem for K(X) awaiting-author t-number-theory t-algebra failing CI
32285 awainverse chore(ModelTheory/Bundled): Replace CategoryTheory.Bundled awaiting-author t-logic awaiting author
31663 xroblot feat(Algebra): more instances about `min`, `max`, `iSup` and `iInf` of sub-algebras WIP t-algebra labelled WIP
30920 callesonne feat(Category/Grpd): define the bicategory of groupoids t-category-theory large-import failing CI
29624 mcdoll feat(LinearAlgebra/LinearPMap): add definition of resolvent and first resolvent identity awaiting-author t-analysis t-algebra failing CI
27100 staroperator feat(ModelTheory): Presburger definability and semilinear sets t-logic awaiting review
31057 jsm28 feat(Geometry/Euclidean/Incenter): `reindex` lemmas t-euclidean-geometry awaiting review
32124 SnirBroshi feat(SimpleGraph/Walks/Operations): expand basic drop/take/reverse API t-combinatorics awaiting review
32279 joelriou feat(CategoryTheory): effective epi in the category of functors to types WIP t-category-theory labelled WIP
29942 smmercuri feat(InfinitePlace/Completion): embeddings of `w.Completion` factor through embeddings of `v.Completion` when `w` extends `v` FLT ⚠️ awaiting review
31925 alreadydone feat(Topology): étalé space associated to a predicate on sections awaiting-author t-topology awaiting author
32188 euprunin feat: add `grind` annotation for `ENNReal.inv_eq_zero` t-data awaiting review
30391 rudynicolop feat(Data/List): list splitting definitions and lemmas new-contributor t-data awaiting review
29393 staroperator feat(SetTheory/ZFC): `card (V_ o) = preBeth o` t-set-theory large-import awaiting review
31967 bwangpj feat: IrreducibleSpace.of_openCover t-topology awaiting review
32238 YaelDillies feat(Combinatorics/SimpleGraph): distributivity of box product over sum t-combinatorics large-import awaiting review
30582 RemyDegenne feat: extension of a function to the closure of a submodule WIP t-topology labelled WIP
26351 RemyDegenne feat: covering and packing numbers of sets in a metric space awaiting-author t-topology brownian awaiting author
31551 RemyDegenne feat: `gaussianReal_const_sub` t-measure-probability awaiting review
32389 LLaurance feat(Analysis): Trigonometric identities ❌? ⚠️ infrastructure-related CI failing
27579 RemyDegenne feat: risk of an estimator, DeGroot statistical information, total variation distance WIP t-measure-probability large-import labelled WIP
32131 Vierkantor feat(scripts): count the number of tactics without a docstring t-meta CI large-import awaiting review
30605 joelriou feat(CategoryTheory): for any filtered category, there exists a final functor from a directed poset awaiting-author t-category-theory awaiting author
32386 riccardobrasca feat: add classical version of Hilbert 90 WIP t-number-theory large-import labelled WIP
31653 ster99 feat(MeasureTheory): Foelner filters awaiting-author new-contributor ⚠️ awaiting author
32370 apnelson1 feat(Combinatorics/Matroid): refactor matroid supportedness tactic WIP ⚠️ labelled WIP
31433 sinhp feat(CategoryTheory): Computable cartesian monoidal structure on slices induced by chosen pullbacks awaiting-author t-category-theory awaiting author
31425 robertmaxton42 feat(Topology) : implement delaborators for non-standard topology notation t-topology awaiting review
32163 zhuyizheng feat(MeasureTheory): interval integral is absolutely continuous t-measure-probability new-contributor awaiting review
32218 mkaratarakis feat: lemmas about the `House` of an algebraic number awaiting-author t-number-theory new-contributor awaiting author
29315 kbuzzard chore: raise priority of `IsTopologicalSemiring.toIsModuleTopology` awaiting-author t-topology failing CI
31862 erdOne chore: unify `LocalizedModule` and `OreLocalization` t-algebra awaiting review
28682 Thmoas-Guan feat(RingTheory): definition of regular local ring awaiting-author t-ring-theory awaiting author
30758 Timeroot chore: tag abs_inv and abs_div with grind= t-algebra awaiting review
31886 CoolRmal feat: the family of limits in probability of sequences of uniformly integrable random variables is uniformly integrable t-measure-probability brownian awaiting review
31730 thorimur feat(Meta): declaration manipulation meta API: allow logging on type signature of theorems t-meta failing 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 WIP t-analysis labelled WIP
32316 Thmoas-Guan feat(Homology/ModuleCat): Dimension Shifting tools in ModuleCat awaiting-author t-category-theory t-algebra awaiting author
32194 alreadydone feat(LinearAlgebra): more on StrongRankCondition t-algebra awaiting review
32159 zhuyizheng feat(Order): gaps of disjoint intervals t-order new-contributor failing CI
30333 paulorauber feat(Probability): definition of trajMeasure t-measure-probability new-contributor maintainer-merge awaiting review
30293 vlad902 feat(SimpleGraph): there exists a maximal path/trail in a graph with finite edges awaiting-author t-combinatorics awaiting author
32474 mattrobball perf(Module.LinearMap.Defs): deprioritize projections to parents for SemilinearMapClass t-algebra failing CI
31219 Thmoas-Guan feat(Algebra): lemma about `IsBaseChange` under exact sequence awaiting-author t-ring-theory awaiting author
31898 ntapiam feat(LinearAlgebra/TensorAlgebra): implement HopfAlgebra for TensorAlgebra awaiting-author new-contributor t-ring-theory failing CI
30736 alreadydone feat(RingTheory): Picard group of a domain is isomorphic to ClassGroup t-algebra large-import awaiting review
31960 urkud feat: a lower bound for the volume of a cone on the unit sphere t-measure-probability awaiting review
30484 vihdzp refactor: override `≤` and `<` in `Function.Injective.semilatticeSup`, etc. t-order awaiting review
31611 thorimur feat(Meta): `withPlural` wrapper for more readable messages in source awaiting-author t-meta awaiting author
13740 YaelDillies feat: more robust ae notation t-meta t-measure-probability awaiting review
32127 CoolRmal feat: use IndexedPartition.piecewise to create simple/measurable/strongly measurable functions t-measure-probability large-import brownian awaiting review
32267 vlad902 feat(SimpleGraph): add `SimpleGraph.HomClass` t-combinatorics awaiting review
32323 LLaurance feat(Combinatorics/SimpleGraph/Connectivity): exists vertex adjacent to any vertex of a nontrivial connected graph t-combinatorics awaiting review
28468 alreadydone feat(Algebra): ring API for `AddLocalization` awaiting-author t-algebra large-import awaiting author
31998 Thmoas-Guan feat(Algebra): localized module in `ModuleCat` awaiting-author t-algebra awaiting author
31995 Thmoas-Guan feat(RingTheory) : Module being injective is local property awaiting-author t-ring-theory awaiting author
32134 mitchell-horner feat(Topology/Real): theorems linking `IsGLB` with `BddBelow`, `Antitone`, `Tendsto _ atTop` t-topology large-import awaiting review
31901 callesonne feat(Bicategory/Subbicategory): add full subbicategories using `ObjectProperty` awaiting-author t-category-theory awaiting author
31879 Thmoas-Guan feat(Algebra/Homology): Projective dimension in linear equiv awaiting-author t-algebra failing CI
32326 chrisflav feat(Algebra/ModuleCat): extension of scalars is comonadic for a faithfully flat algebra awaiting-author t-ring-theory awaiting author
29960 yonggyuchoimath feat(Algebra/Category/Ring): equalizers of pushout maps of tensor product inclusions awaiting-author new-contributor t-ring-theory awaiting author
32473 mattrobball chore(Kaehler.JacobiZariski): remove egregious local instance hack awaiting-author t-ring-theory awaiting author
26719 AntoineChambert-Loir feat(RingTheory/PolynomialLaw/Basic): extends polynomial laws to arbitrary universes blocked-by-other-PR large-import t-ring-theory blocked on another PR
27599 mitchell-horner feat(Combinatorics/SimpleGraph): define `CompleteEquipartiteSubgraph` t-combinatorics awaiting review
30436 wwylele feat(Topology/InfiniteSum): tprod_one_{add/sub}_ordered t-topology awaiting review
32367 BoltonBailey feat(Computability): add finEncodings for List Bool and pairs of types t-computability awaiting review
31610 rudynicolop feat(Computability/NFA): Kleene star closure for Regular Languages via NFA new-contributor t-computability awaiting review
32374 adamtopaz feat(Tactic/WildcardUniverse): Foo.{*, _, v*, max u v} t-meta awaiting review
32427 YaelDillies refactor(Algebra/Algebra): genericise algebra instances for subsemirings t-algebra CFT awaiting review
32433 YaelDillies feat: an irreducible element of a submonoid isn't zero t-algebra CFT awaiting review
32045 xroblot chore(Trace/Quotient): move isomorphism to `Localization.AtPrime.Basic` t-ring-theory awaiting review
32128 grunweg dev: investigate the private module linter not firing failing CI
31706 Thmoas-Guan feat(Algebra/ModuleCat): `ModuleCat.uliftFunctor` awaiting-author t-algebra awaiting author
32273 jsm28 feat(Analysis/Convex/Side): affine combinations on same / opposite side of face of a simplex as a vertex t-analysis t-convex-geometry awaiting review
29744 espottesmith feat(Combinatorics): define directed hypergraphs t-combinatorics new-contributor failing CI
31147 daefigueroa feat(Dynamics): point transitive monoid actions and transitive points awaiting-author t-dynamics new-contributor awaiting author
30089 loefflerd feat(NumberTheory/ModularForms): Bounds on modular forms and q-expansion coeffs WIP blocked-by-other-PR t-number-theory large-import blocked on another PR
31121 jessealama feat: add ComplexShape.EulerCharSigns for generalized Euler characteristic awaiting-author t-category-theory t-algebra awaiting author
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
27542 chrisflav feat(RingTheory/KrullDimension): dimension of polynomial ring large-import t-ring-theory awaiting review
32602 adamtopaz feat: Refactor graph WIP ⚠️ labelled WIP
28972 themathqueen feat(LinearAlgebra/Matrix): star-algebra automorphisms on matrices are unitarily inner t-algebra failing CI
32160 SnirBroshi feat(Combinatorics/SimpleGraph/Walks): helper theorems about `darts` and `support` t-combinatorics awaiting review
31013 vihdzp chore: deprecate `AsLinearOrder` t-order awaiting review
31984 kim-em feat: definition of `ConvexSpace` t-algebra awaiting review
32455 vihdzp feat: order topologies of successor orders t-topology t-order awaiting review
31449 kim-em feat(SemilocallySimplyConnected): definition and alternative formulation ⚠️ awaiting review
28599 Thmoas-Guan feat(RingTheory): polynomial over CM ring is CM WIP large-import t-ring-theory labelled WIP
28604 alreadydone chore(Algebra/Ring/Defs): add two classes (minimally invasive version) t-algebra awaiting review
30116 FormulaRabbit81 feat(MeasureTheory): a relatively compact set of measures is tight t-measure-probability large-import awaiting review
32425 kim-em feat(Linter/FlexibleLinter): generate Try this: simp only suggestions delegated t-linter delegated
32583 MJ141592 refactor(SimpleGraph): change bridges not to require the edge to be present awaiting-author t-combinatorics new-contributor failing CI
32645 vihdzp feat(SetTheory/Cardinal): formulas for `sum (fun n : ℕ ↦ x ^ n)` t-set-theory awaiting review
31595 astrainfinita chore: redefine `Ideal.IsPrime` t-algebra awaiting review
28582 Thmoas-Guan feat(Data): some lemmas about WithBot ENat awaiting-author t-data awaiting author
26986 WangYiran01 feat(Partition): add bijection for partitions with max part ≤ r awaiting-author t-combinatorics new-contributor awaiting author
31492 fcoUnda chore(Analysis/SpecialFunctions): nthRoot improvement awaiting-author t-analysis new-contributor awaiting author
28546 Sfgangloff feat(SymbolicDynamics): basic setup of Zd, full shift, cylinders, pat… awaiting-author t-dynamics new-contributor awaiting author
32644 chriseth feat(Data/Set/Card): Add simplification theorem about cardinalities of "big" cartesian products. awaiting-author new-contributor t-data awaiting author
32654 YaelDillies feat(Combinatorics): a clique has size at most the chromatic number t-combinatorics awaiting review
30880 themathqueen feat(Analysis/InnerProductSpace): finite-dimensional inner product space with an algebra implies a coalgebra delegated t-analysis delegated
31133 thorimur feat(Linter): combinators for linter option boilerplate t-meta t-linter awaiting review
31444 harahu doc(Probability/Martingale/BorelCantelli): fix presumed LaTeX typo delegated t-measure-probability delegated
30988 erdOne feat(AlgebraicGeometry): descending affine cover of an inverse limit t-algebraic-geometry large-import awaiting review
29948 mcdoll feat(Analysis/Fourier): the Fourier transform on `L^2` t-analysis awaiting review
31495 jsm28 feat(Geometry/Euclidean/Sphere/SecondInter): `secondInter` and sides of faces of a simplex t-euclidean-geometry awaiting review
32242 vihdzp feat: missing instances for `OrderDual`/`Lex`/`Colex` t-order awaiting review
32493 euprunin feat(Algebra/Group/Action): add `grind` annotation for `smul_eq_mul` ⚠️ awaiting review
32626 vihdzp chore(Order/WithBot): add to_dual attributes (part 2) awaiting-CI t-order does not pass CI
32668 kim-em feat(TacticAnalysis): copy args when replacing linarith with grind t-meta awaiting review
32458 vihdzp feat: order isomorphisms preserve successor/predecessor limits awaiting-author t-order awaiting author
32673 CoolRmal feat: an open subset of a Baire space is Baire t-topology large-import awaiting review
29186 winstonyin feat: IsIntegralCurve for solutions to ODEs t-differential-geometry t-analysis t-dynamics awaiting review
32676 Scarlett-le doc(Sphere.Power): add theorem to 1000.yaml and author credit t-euclidean-geometry new-contributor failing CI
24000 YaelDillies feat: correspondence between affine group schemes and Hopf algebras WIP t-algebraic-geometry FLT toric labelled WIP
26608 vihdzp feat(SetTheory/Cardinal/Aleph): `o.card ≤ ℵ_ o` and variants t-set-theory awaiting review
32678 harahu doc(MeasureTheory): fix typos t-measure-probability awaiting review
30898 vihdzp feat: characterization of `List.splitBy` t-data awaiting review
32480 ADedecker feat: define `PolynormableSpace` t-analysis maintainer-merge awaiting review
32688 grunweg chore: update complex analysis library overview t-analysis failing CI
32444 vihdzp feat: `SignType` is a complete linear order t-order t-data awaiting review
31478 BGuillemet feat(CategoryTheory/Sites): `uliftYoneda` for sheaves over a subcanonical topology awaiting-author t-category-theory awaiting author
26231 chrisflav feat(CategoryTheory/Sites): sheaf condition and coproducts WIP awaiting-author t-category-theory labelled WIP
32675 kebekus feat: meromorphic functions are measurable t-analysis large-import awaiting review
26303 joelriou feat(AlgebraicTopology): the fundamental lemma of homotopical algebra WIP t-category-theory t-algebraic-topology labelled WIP
28175 dsfxcimk feat: exterior angle theorem t-euclidean-geometry new-contributor awaiting review
32699 mirefek doc: update `use` doc-string to distinguish `exists` / `use` / `use!` t-meta new-contributor failing CI
30668 astrainfinita feat: `QuotType` RFC awaiting-zulip t-data awaiting a zulip discussion
32080 plp127 feat(Topology): Completely Regular Space iff Uniformizable t-topology awaiting review
32702 SnirBroshi chore(Combinatorics/SimpleGraph/Connectivity): move `Finite ConnectedComponent` instance from `WalkCounting.lean` to `Connected.lean` t-combinatorics awaiting review
32556 vihdzp doc: fix URL in docs documentation awaiting-author awaiting author
30190 joelriou feat(CategoryTheory/Sites): functoriality of descent data awaiting-author t-category-theory large-import awaiting author
31766 SuccessMoses feat(Topology/EMetricSpace): continuity of arc length awaiting-author t-topology new-contributor awaiting author
26483 metakunt feat(RingTheory/RootsOfUnity/PrimitiveRoots): add equivPrimitiveRootsOfCoprimePow new-contributor t-ring-theory awaiting review
31954 wwylele feat(Counterexamples): Weierstrass function is continuous and nowhere differentiable t-analysis awaiting review
32435 YaelDillies chore(Algebra/Module): make select `Module` assumptions t-algebra CFT awaiting review
32479 WenrongZou feat(RingTheory/PowerSeries/Substitution): add `le_order_subst` new-contributor t-ring-theory awaiting review
32482 sgouezel feat: extend Stieltjes measures to more general index types t-measure-probability awaiting review
32532 SnirBroshi feat(Combinatorics/SimpleGraph/Connectivity): connected components are maximally connected subsets/subgraphs t-combinatorics awaiting review
32555 ksenono feat(Combinatorics/SimpleGraph/Matching): maximum and maximal matchings for Konig's theorem t-combinatorics new-contributor awaiting review
32559 WenrongZou feat(RingTheory/PowerSeries): toSubring and ofSubring for MvPowerSeries new-contributor t-ring-theory awaiting review
32639 euprunin chore: golf using `grind`. add `grind` annotations. awaiting review
32422 kim-em fix(Linter): deprecated module linter now fires for public/meta imports delegated t-linter delegated
31092 FlAmmmmING feat(Algebra/Group/ForwardDiff.lean): Add theorem `sum_shift_eq_fwdDiff_iter`. t-algebra new-contributor awaiting review
32712 erdOne feat(Logic/Equiv): `Option α × β ≃ β ⊕ α × β` t-logic awaiting review
32710 erdOne feat(Topology/MetricSpace): proper iff `dist _` is proper map t-topology awaiting review
32307 mcdoll feat(Analysis/Distribution): `(1 + |x|^2)^r` has temperate growth WIP blocked-by-other-PR t-analysis blocked on another PR
27702 FLDutchmann feat(NumberTheory/SelbergSieve): define Lambda-squared sieves and prove important properties delegated t-number-theory delegated
32672 tb65536 feat: haar measures on short exact sequences t-measure-probability awaiting review
26212 Thmoas-Guan feat(Algebra): the Rees theorem for depth awaiting-author t-algebra large-import awaiting author
32719 EtienneC30 feat: another version of mapping Gaussian measures t-measure-probability brownian awaiting review
26743 grunweg feat: product rule for Lie bracket on manifolds WIP t-differential-geometry labelled WIP
29283 Jlh18 feat(CategoryTheory): define forgetful-core adjunction between Cat and Grpd awaiting-author t-category-theory file-removed awaiting author
32734 Vierkantor chore(Tactic): document remaining undocumented tactics documentation t-meta failing CI
32735 Jlh18 refactor: move `CategoryTheory.Category.Grpd` to `CategoryTheory.Groupoid.Grpd.Basic` file-removed failing CI
32526 PrParadoxy chore(LinearAlgebra/Multilinear/Basic.lean): remove `erw`s in `restr` awaiting-author t-algebra new-contributor awaiting author
28693 faenuccio feat(Analysis.Normed.Module.Milman-Pettis): add Milman-Pettis theorem WIP t-analysis labelled WIP
32215 jonasvanderschaaf feat(ModelTheory/Types): Construct a topology on CompleteType and prove the space is compact awaiting-author new-contributor ⚠️ awaiting author
32742 LTolDe feet: add class SuslinSpace new-contributor failing CI
32745 LTolDe feat(Topology/Algebra): add MulActionConst.lean t-topology new-contributor failing CI
32748 LorenzoLuccioli chore(Topology/ContinuousOn): Add `fun_prop` tag to `ContinuousAt.comp_continuousWithinAt` t-topology failing CI
32019 jsm28 feat(Geometry/Euclidean/Projection): `map` and subtype lemmas t-euclidean-geometry awaiting review
30981 jsm28 feat(Geometry/Euclidean/Angle/Bisector): oriented angle bisection mod π t-euclidean-geometry awaiting review
32146 foderm feat(ModelTheory): add characterizations of complete theories t-logic new-contributor awaiting review
32671 themathqueen chore(LinearAlgebra/GeneralLinearGroup/AlgEquiv): slightly generalize t-algebra awaiting review
32755 alreadydone chore(Topology/Compactness): golf t-topology awaiting review
31508 FLDutchmann feat(Tactic): `algebra` tactic. awaiting-author t-meta awaiting author
32405 Shaddaaa feat(CategoryTheory/Sites): (Co)continuity of `Over.iteratedSliceEquiv` awaiting-author t-category-theory new-contributor maintainer-merge large-import awaiting author
31059 gasparattila feat(Topology/Sets): define the Vietoris topology on `(Nonempty)Compacts` t-topology awaiting review
32740 LTolDe feat: add IsNowhereDense helpers new-contributor large-import ⚠️ awaiting review
32590 sgouezel feat: use `IsCompletelyPseudometrizable` class in measure regularity statements ⚠️ awaiting review
32758 chrisflav feat(RingTheory/FinitePresentation): a finite product of finitely presented algebras is finitely presented t-ring-theory failing CI
32738 euprunin chore: golf using `grind`. add `grind` annotations. failing CI
32703 chrisflav chore(RingTheory): rename `RingHom.specComap` to `PrimeSpectrum.comap` t-ring-theory awaiting review
32589 grunweg feat: smooth embeddings t-differential-geometry awaiting review
32704 euprunin chore: remove use of `erw` awaiting review
30851 FormulaRabbit81 feat(Topology): prove there exists an embedding of separable metric spaces in the hilbert cube t-topology awaiting review
32118 alreadydone feat(Algebra): prerequisites for #31919 t-algebra t-ring-theory awaiting review
32382 YaelDillies chore(Algebra/Order/AddGroupWithTop): golf t-algebra awaiting review
32541 YaelDillies chore: import Tactic.Attr.Register privately large-import awaiting review
32567 vihdzp feat: `CompleteLinearOrder (Πₗ i, α i)` t-order awaiting review
32570 ksenono feat(Combinatorics/SimpleGraph): bipartite subgraphs and vertex-disjoint graphs for Konig's theorem t-combinatorics new-contributor awaiting review
32603 themathqueen chore: add deprecated file and clean up imports in another t-algebra awaiting review
32611 tb65536 feat(FieldTheory/Galois/IsGaloisGroup): add `IsGaloisGroup.finite` t-algebra awaiting review
32764 plp127 feat(Topology/Separation): completely normal iff hereditarily normal t-topology awaiting review
32608 PrParadoxy feat(LinearAlgebra/PiTensorProduct): API for PiTensorProducts indexed by sets new-contributor ⚠️ awaiting review
27254 yuanyi-350 feat: 2025 imo problem3 IMO awaiting review
32766 mcdoll feat(Analysis/TemperedDistribution): embedding of temperate growth functions t-analysis awaiting review
32767 mcdoll feat(Analysis/TemperedDistribution): embedding of `Lp`-functions t-analysis awaiting review
32768 mcdoll feat(Analysis/TemperedDistribution): embedding of Schwartz functions t-analysis awaiting review
32769 mcdoll feat(Analysis/TemperedDistribution): multiplication with temperate growth functions t-analysis awaiting review
32770 mcdoll feat(Analysis/TemperedDistribution): derivatives t-analysis 🟤 running CI
27053 tb65536 feat: Galois group of `x^n - x - 1` WIP t-algebra large-import labelled WIP
32771 tb65536 feat(Algebra/Order/BigOperators/Group): criterion for `m.card ≤ m.toFinset.card + 1` t-algebra t-order t-data awaiting review
32772 tb65536 feat(Data/Set/Card): criterion for `s.ncard ≤ (f '' s).ncard + 1` t-data awaiting review
32640 vihdzp feat: cardinality of Hahn series t-algebra t-ring-theory awaiting review
32773 Hagb feat(Algebra/GroupWithZero/NonZeroDivisors): add some lemmas about multiplication t-algebra awaiting review
32775 urkud feat(VitaliFamily): prove `filterAt_enlarge` t-measure-probability awaiting review
32774 Hagb feat(Algebra/GroupWithZero/NonZeroDivisors): add a lemma about product t-algebra large-import awaiting review
25042 alreadydone feat(Topology): restriction/extension of Trivialization and composition with Homeomorph merge-conflict t-topology merge conflict
31560 AntoineChambert-Loir feat(Topology/Sion): the minimax theorem of von Neumann - Sion blocked-by-other-PR ⚠️ blocked on another PR
32513 euprunin feat(Algebra/Polynomial): add `grind` annotations for `C_mul_monomial` and `monomial_mul_C` t-algebra awaiting review
32043 thomaskwaring feat(Combinatorics/SimpleGraph/Acyclic): characterise maximal acyclic subgraphs t-combinatorics new-contributor awaiting review
32733 dleijnse feat(FieldTheory): X^n - t separable iff n nonzero t-algebra new-contributor awaiting review
32779 sgouezel feat: more consequences of Riesz-Markov-Kakutani t-measure-probability awaiting review
32652 BGuillemet feat(CategoryTheory/Sites): add the Grothendieck topology generated by a precoverage awaiting-author t-category-theory maintainer-merge failing CI
32756 chrisflav chore(CategoryTheory/Limits): more API for wide pullbacks delegated t-category-theory delegated
32739 Rida-Hamadani chore(SimpleGraph): golf and improve style of `Subwalks.lean` t-combinatorics awaiting review
32782 xroblot feat(Cyclotomic): compute the torsion order of a cyclotomic field ⚠️ awaiting review
32784 sgouezel feat: more API for FiniteMeasure and ProbabilityMeasure t-measure-probability awaiting review
32786 sgouezel feat: construct a bounded continuous map from a continuous compactly supported map t-topology awaiting review
32777 madvorak doc: Contributing moved to Contributing failing CI
32787 Hagb feat(RingTheory/MvPolynomial/MonomialOrder): add several lemmas about `leadingTerm` and inequality on degree t-ring-theory awaiting review
32788 Hagb feat(RingTheory/MvPolynomial/MonomialOrder): add some variants of `sPolynomial_mul_monomial` t-ring-theory awaiting review
32725 joelriou feat(CategoryTheory): presheaves of types which preserves a limit awaiting-author t-category-theory awaiting author
28462 joelriou feat(AlgebraicTopology/SimplicialSet): the relative cell complex attached to a rank function for a pairing WIP blocked-by-other-PR merge-conflict t-algebraic-topology blocked on another PR
32724 grunweg feat: lint against unscoped uses of the linter.flexible option t-linter awaiting review
32789 harahu doc(RingTheory): fix typos t-ring-theory awaiting review
32793 harahu doc(NumberTheory): fix typos t-number-theory awaiting review
26446 joelriou refactor(CategoryTheory): make morphisms in full subcategories a 1-field structure WIP t-category-theory large-import labelled WIP
26923 oliver-butterley feat(Dynamics/BirkhoffSum): add the pointwise ergodic theorem (Birkhoff's) merge-conflict t-dynamics new-contributor merge conflict
32365 yury-harmonic feat: `norm_num` extension for `IsSquare` delegated t-meta failing CI
32262 alreadydone feat(Algebra): stably finite rings t-algebra t-ring-theory awaiting review
31707 Thmoas-Guan feat(Homology): map between `Ext` induced by exact functor awaiting-author t-category-theory t-algebra awaiting author
31361 alreadydone feat(Algebra/Order): convex subgroups awaiting-author t-algebra t-order failing CI
32698 farruhx feat(List): add aesop / simp annotations to selected lemmas for improved automation new-contributor t-data awaiting review
32330 ADedecker feat: postcomposition by a CLM as a CLM on test functions t-analysis awaiting review
32360 YuvalFilmus feat(Chebyshev): degree, leadingCoeff, eval_neg new-contributor t-ring-theory awaiting review
32116 LessnessRandomness feat(Geometry/Euclidean/Angle/Unoriented/TriangleInequality): Add criterion for equality case awaiting-author t-euclidean-geometry awaiting author
32797 riccardobrasca start WIP RFC t-algebra labelled WIP
25138 chrisflav chore(RingTheory/Ideal): make `RingHom.ker` take a `RingHom` instead of `RingHomClass` awaiting-author t-algebra failing CI
32437 WenrongZou feat(Algebra/Category/ModuleCat/Sheaf/Quasicoherent): construction of `Presentation` t-algebra new-contributor awaiting review
30112 gaetanserre feat(Probability.Kernel): add representation of kernel as a map of a uniform measure t-measure-probability awaiting review
32552 ksenono feat(SetTheory/Cardinal): helpers for Konig's theorem new-contributor t-set-theory awaiting review
32746 dagurtomas chore(CategoryTheory): generalize subpresheaf to subfunctor awaiting-author t-category-theory file-removed failing CI
32801 Hagb feat(RingTheory/MvPolynomial/Ideal): `sPolynomial` preserves ideal membership t-ring-theory awaiting review
32265 joelriou feat(AlgebraicTopology): finite colimits of finite simplicial sets are finite maintainer-merge t-algebraic-topology awaiting review
32803 erdOne feat(RIngTheory): more-linear version of `tensorKaehlerEquiv` t-ring-theory awaiting review
32692 WilliamCoram feat: define multivariate restricted power series t-number-theory new-contributor t-ring-theory awaiting review
32805 gasparattila feat(Topology/UniformSpace/Closeds): continuity of closure t-topology awaiting review
32806 erdOne feat(RingTheory): base change of ideal with flat quotients t-ring-theory awaiting review
32802 erdOne feat(RingTheory): more ergonomic version of jacobi criterion for smoothness t-ring-theory awaiting review
32562 YaelDillies chore(Data/Finsupp): rename the `toFun` projection to `apply` in `simps` maintainer-merge t-data awaiting review
30047 ooovi feat(Combinatorics/SimpleGraph): edge labellings delegated t-combinatorics delegated
32808 gasparattila feat(Topology/Maps): add `IsClosedEmbedding.of_comp` t-topology awaiting review
32737 j-loreaux refactor: rename `MulAction` to `MonoidAction` awaiting review
32807 WilliamCoram feat: Define the Gauss norm for MvPowerSeries new-contributor t-ring-theory failing CI
32300 bjornsolheim feat(Geometry/Convex/Cone): define and characterize generating convex cone new-contributor t-convex-geometry awaiting review
31138 AntoineChambert-Loir feat(LinearAlgebra/Transvection): auxiliary lemmas to compute the determinant of transvection in a module t-algebra large-import awaiting review
25925 BoltonBailey feat: file for lemmas about MvPolynomials over NoZeroDivisors awaiting-author t-algebra awaiting author
32792 plp127 feat(Topology): uniformity has linearly ordered basis implies completely normal t-topology awaiting review
32429 erdOne feat(RingTheory): `IsIntegrallyClosed R[X]` t-ring-theory awaiting review
31161 AntoineChambert-Loir feat(RingTheory/MvPolynomial/IrrQuadratic): irreducibility of sum X_i Y_i t-ring-theory awaiting review
32696 YuvalFilmus feat(SpecialFunctions/Artanh): basic definition and partial equivalence t-analysis new-contributor awaiting review
32747 j-loreaux feat: integer inequalities from multiples in a strict ordered ring t-algebra maintainer-merge awaiting review
28411 zcyemi feat(LinearAlgebra/AffineSpace/Simplex/Centroid): define centroid and medians t-algebra large-import awaiting review
32403 FLDutchmann fix(FieldSimp): `declaration has free variables` kernel errors t-meta awaiting review
32190 vihdzp chore(Algebra/Order/Ring/Archimedean): generalize theorems to `OrderHomClass` + `RingHomClass` t-algebra failing CI
32813 erdOne feat(AlgebraicGeometry): relative normalization of schemes t-algebraic-geometry awaiting review
30131 fpvandoorn feat: alias_in attribute t-meta awaiting review
32809 erdOne feat(RingTheory): residue field of `I[X]` t-ring-theory awaiting review
32237 joelriou feat(AlgebraicTopology): binary products of standard simplices maintainer-merge t-algebraic-topology awaiting review
31717 thorimur chore: refactor `Type*` and `Sort*` to use `mkFreshLevelParam` t-meta large-import awaiting review
30872 rudynicolop feat(Computability/NFA): NFA closure under concatenation new-contributor t-computability maintainer-merge awaiting review
32814 joelriou feat(Algebra/Homology): equivOfIsKInjective t-category-theory large-import awaiting review
32492 bjornsolheim feat(LinearAlgebra/TensorProduct): explicit tensor product decomposition in a finite basis t-algebra new-contributor awaiting review
32715 chiyunhsu feat(Data/Nat/Factorization): add theorems about ordCompl new-contributor t-data awaiting review
32820 gasparattila feat(Topology/Sets): range of `(Nonempty)Compacts.map` t-topology awaiting review
32815 tb65536 refactor: rename `Splits.splits_of_dvd` to `Splits.of_dvd` t-algebra awaiting review
32259 jsm28 feat(Analysis/SpecialFunctions/Trigonometric/Angle): `toReal` addition lemmas awaiting-author t-analysis awaiting author
32749 thorimur fix: respect visibility in `notation3` t-meta awaiting review
32560 AntoineChambert-Loir feat(LinearAlgebra/Dimension/Constructions): construct a basis from one of submodule and quotient t-algebra failing CI
32371 KaiErikNiermann fix: minor error in comment of example for natural transformation easy new-contributor awaiting review
32818 tb65536 refactor(Algebra/Polynomial/Splits): continue deprecation t-algebra awaiting review
32763 JohnnyTeutonic feat(Algebra/Lie/CartanMatrix): add Cartan matrices for classical typ… awaiting-author t-algebra new-contributor file-removed awaiting author
30240 luigi-massacci feat(Analysis/Distribution/ContDiffMapSupportedIn): Add a wrapper for fderiv on D_K^n blocked-by-other-PR t-analysis blocked on another PR
30576 smmercuri feat: `adicCompletion` for `Rat` is uniform isomorphic to `Padic` ⚠️ awaiting review
32210 ADedecker feat: iteratedFDeriv as a linear map on test functions t-analysis awaiting review
32521 j-loreaux refactor: generalize semicontinuity t-topology file-removed awaiting review
32591 YaelDillies chore(Algebra/MonoidAlgebra): scope `Algebra R[M] A[M]` instance t-algebra awaiting review
32600 PrParadoxy feat(LinearAlgebra/Multilinear): composition of multilinear maps new-contributor ⚠️ awaiting review
32617 erdOne feat(RingTheory): field extension over perfect fields are smooth t-ring-theory awaiting review
32657 mattrobball chore: clean up imports from #31746 t-data awaiting review
32660 dagurtomas feat(Topology): sandwich lemmas for profinite sets t-topology awaiting review
32664 harahu doc: fix articles a/an awaiting review
32665 erdOne feat(RingTheory): quasi-finite algebras t-ring-theory awaiting review
32254 YaelDillies feat(Algebra/MonoidAlgebra): complete the map API t-algebra awaiting review
32823 erdOne feat(RingTheory): construct etale neighborhood that isolates point in fiber t-ring-theory awaiting review
32811 erdOne feat(RingTheory): predicate on satisfying Zariski's main theorem t-ring-theory awaiting review
32412 Brian-Nugent feat: add Artinian schemes awaiting-author t-algebraic-geometry new-contributor awaiting author
32744 NoneMore feat(ModelTheory/Definablity): add `DefinableFun` definition and lemmas t-logic new-contributor awaiting review
32826 felixpernegger feat(Data/Tuple/Sort): Sort of perm is its inverse new-contributor t-data awaiting review
31505 dsfxcimk feat: Add some oangle theorems t-euclidean-geometry new-contributor awaiting review
30640 SnirBroshi feat(Combinatorics/SimpleGraph/Acyclic): define `reachabilitySet` + a maximally acyclic graph is a tree t-combinatorics awaiting review
32754 felixpernegger feat(Data/Set/Card): ncard of complement of set is Nat.card - ncard of set easy new-contributor maintainer-merge t-data awaiting review
32761 harahu doc(FieldTheory): fix typos t-algebra maintainer-merge awaiting review
32781 harahu doc(GroupTheory): fix typos maintainer-merge t-group-theory awaiting review
25822 ScottCarnahan WIP: experiments with vertex algebras WIP large-import labelled WIP
32819 harahu doc(Geometry): fix typos 🟤 running CI
30526 SnirBroshi chore(Logic/Relation): use `Subrelation` to state theorems awaiting-zulip awaiting a zulip discussion
32828 Hagb feat(Algebra/Order/Group/Defs): add `IsOrderedAddMonoid.toIsOrderedCancelAddMonoid'` t-algebra awaiting review
32794 YuvalFilmus feat(Arcosh): continuity, differentiability, bijectivity t-analysis awaiting review
32791 luisacicolini chore: `grind` tags for `Logic/Relation` ready-to-merge t-logic new-contributor 🟤 contradictory labels
32824 Vilin97 Prove that the diameter of a Euclidean ball is twice its radius. t-analysis new-contributor awaiting review
32832 0xTerencePrime fix(Order/Interval): simplify Ioo lemmas under DenselyOrdered + LocallyFinite t-order new-contributor 🟤 running CI
32231 grunweg chore: use the to_fun attribute awaiting review
32830 loefflerd refactor: use "@[to_fun]" to generate some lemmas WIP labelled WIP
32760 grunweg feat: inclusion of an open submanifold is an immersion t-differential-geometry awaiting review
32822 artie2000 chore(Algebra/Ring/Subsemiring/Order): relate `Subsemiring.nonneg` with `AddSubmonoid.nonneg` t-algebra awaiting review
32440 thorimur feat: make the `unusedDecidableInType` linter fire when `Decidable*` instances are used only inside of proofs in the type t-linter awaiting review
32281 ajirving feat(NumberTheory.Chebyshev): prove connection between prime counting and theta t-number-theory new-contributor large-import awaiting review
32836 YaelDillies feat(Algebra): characterise when a submodule constructor is equal to `⊥` t-algebra 🟤 running CI
32837 erdOne feat(RingTheory): noetherian model for etale algebras large-import t-ring-theory awaiting review
32838 YaelDillies feat(Algebra): localising a torsion-free module at regular elements t-algebra 🟤 running CI
30344 Deep0Thinking feat(MeasureTheory/Integral): add versions of `exists_eq_interval_average` and first mean value theorem for integrals t-measure-probability new-contributor awaiting review
7596 alreadydone feat: covering maps from properly discontinuous actions and discrete subgroups t-topology 🟤 running CI
32834 YaelDillies chore(Algebra): move `CharZero.of_module` earlier maintainer-merge 🟤 running CI
31807 edegeltje feat(CategoryTheory/Cat/Basic): Turning 1- and 2-morphisms in Cat into a 1-field structure awaiting-author t-category-theory awaiting author
28796 grunweg feat: immersions are smooth awaiting-author t-differential-geometry failing CI
32835 vasnesterov fix(Tactic/Order): equal but not syntactically equal types bug WIP t-meta 🟤 labelled WIP
32679 YaelDillies chore(Data/Sym2): improve defeq of `diagSet` t-data failing CI
31908 YaelDillies feat: Bernoulli random variables t-measure-probability awaiting review
29687 vihdzp feat: standard part in non-Archimedean field t-algebra awaiting review
32839 YaelDillies chore(RingTheory/HahnSeries): fix delaborator easy t-ring-theory awaiting review
31141 peabrainiac feat(Analysis/Calculus): parametric integrals over smooth functions are smooth awaiting-author t-analysis awaiting author
32584 CBirkbeck feat(NumberTheory/EisensteinSeries/E2): Define the Eisenstein series E2 awaiting-author t-number-theory maintainer-merge large-import awaiting author
32684 Parcly-Taxel feat: a simple unit-distance embedding of the Heawood graph t-combinatorics 🟤 running CI
32804 vihdzp feat: more lemmas on `LinearOrderedAddCommGroupWithTop` t-algebra awaiting review
32841 0xTerencePrime feat(Analysis/Normed/Group/Seminorm): define SupSet instances t-analysis new-contributor 🟤 running CI
32582 metakunt chore(Data/Finset): Rename filter_neg to filter_not ready-to-merge new-contributor t-data awaiting bors
26831 AntoineChambert-Loir feat(GroupTheory/SpecificGroups/Alternating/MaximalSubgroups): maximal subgroups of the alternating group t-group-theory awaiting review
32306 plp127 fix(depRewrite): make `rw!` cleanup casts correctly t-meta awaiting review
13847 alreadydone feat(EllipticCurve): the universal elliptic curve awaiting-author merge-conflict t-algebraic-geometry t-algebra merge conflict
14167 alreadydone feat: Group scheme structure on Weierstrass curve WIP merge-conflict t-algebraic-geometry workshop-AIM-AG-2024 labelled WIP
13297 urkud feat(Semicontinuous): add `comp` lemma awaiting-author merge-conflict t-topology t-order merge conflict
12608 eric-wieser feat: allow `nsmul` / `zsmul` to be omitted again, with a warning awaiting-author merge-conflict t-meta t-algebra merge conflict
12679 MichaelStollBayreuth perf(NumberTheory/RamificationInertia): speed up slow file WIP merge-conflict labelled WIP
12934 grunweg chore: replace more uses of > or ≥ by < or ≤ help-wanted awaiting-author merge-conflict looking for help
12933 grunweg chore: replace some use of > or ≥ by < or ≤ awaiting-author merge-conflict failing CI
12192 Ruben-VandeVelde feat: generalize isLittleO_const_id_atTop/atBot awaiting-author merge-conflict t-analysis merge conflict
11617 urkud refactor(Finset): redefine Finset.diag, review API awaiting-author merge-conflict t-logic merge conflict
11100 eric-wieser feat(CategoryTheory/Limits): add `Functor.mapBinaryBiconeInv` merge-conflict awaiting-CI t-category-theory does not pass CI
10721 urkud feat(Order/FunLike): define `PointwiseLE` merge-conflict t-order t-logic ??? missing CI information
10024 ADedecker feat: rename `connectedComponentOfOne` to `identityComponent`, prove that it is normal and open merge-conflict awaiting-CI t-topology does not pass CI
10521 eric-wieser chore: generalize `IsBoundedLinearMap` to modules awaiting-author merge-conflict t-analysis merge conflict
10594 lecopivo feat: `fun_trans` function transformation tactic e.g. for computing derivatives WIP merge-conflict t-meta labelled WIP
8519 eric-wieser refactor(LinearAlgebra/TensorProduct): golf using `liftAddHom` awaiting-author merge-conflict t-algebra merge conflict
8503 thorimur feat: meta utils for `refine?` awaiting-author merge-conflict t-meta merge conflict
8616 eric-wieser feat(Algebra/FreeAlgebra): add right action and `IsCentralScalar` merge-conflict awaiting-CI t-algebra does not pass CI
8906 jjaassoonn feat: add some missing lemmas about linear algebra awaiting-author merge-conflict t-algebra failing CI
9487 eric-wieser feat: the exponential of dual numbers over non-commutative rings WIP merge-conflict t-analysis t-algebra t-measure-probability labelled WIP
9229 eric-wieser refactor(Algebra/GradedMonoid): Use `HMul` to define `GMul` WIP merge-conflict t-algebra labelled WIP
9354 chenyili0818 feat: monotonicity of gradient on convex real-valued functions awaiting-author merge-conflict t-analysis merge conflict
9642 eric-wieser refactor(Analysis/Normed/{Group/Field}/Basic): Let `extends` generate the repeated fields help-wanted WIP awaiting-author merge-conflict t-analysis looking for help
8961 eric-wieser refactor: use the coinduced topology on ULift awaiting-author please-adopt merge-conflict awaiting-CI looking for help
8658 eric-wieser feat: support right actions for `Con` awaiting-author merge-conflict t-algebra merge conflict
8788 FMLJohn feat(Algebra/Module/GradeZeroModule): if `A` is a graded semiring and `M` is a graded `A`-module, then each grade of `M` is a module over the 0-th grade of `A`. merge-conflict t-algebra merge conflict
9146 laughinggas feat(Data/ZMod/Defs): Topological structure on `ZMod` awaiting-author merge-conflict t-topology t-algebra merge conflict
9356 alexjbest feat: assumption? awaiting-author merge-conflict t-meta merge conflict
9570 eric-wieser feat(Algebra/Star): Non-commutative generalization of `StarModule` WIP merge-conflict awaiting-CI t-algebra labelled WIP
7875 astrainfinita chore: make `SMulCommClass A A B` and `SMulCommClass A B B` higher priority merge-conflict t-algebra slow-typeclass-synthesis ??? missing CI information
6630 MohanadAhmed feat: Reduced Spectral Theorem WIP merge-conflict t-algebra labelled WIP
6930 kmill feat: `resynth_instances` tactic for resynthesizing instances in the goal or local context WIP merge-conflict t-meta labelled WIP
6931 urkud refactor(Analysis/Normed*): use `RingHomIsometric` for `*.norm_cast` help-wanted merge-conflict t-analysis ??? looking for help
7713 RemyDegenne feat: add_left/right_inj for measures awaiting-author merge-conflict t-measure-probability merge conflict
7615 eric-wieser chore(LinearAlgebra/Basic): generalize compatibleMaps to semilinear maps merge-conflict easy awaiting-CI t-algebra does not pass CI
7932 eric-wieser refactor(Algebra/TrivSqZeroExt): replace with a structure merge-conflict awaiting-CI t-algebra does not pass CI
7962 eric-wieser feat: `DualNumber (Quaternion R)` as a `CliffordAlgebra` WIP merge-conflict t-algebra labelled WIP
6791 eric-wieser refactor: Use flat structures for morphisms help-wanted awaiting-author merge-conflict awaiting-CI looking for help
6777 adomani chore(Co*variantClass): replace eta-expanded (· * ·), (· + ·), (· ≤ ·), (· < ·) merge-conflict merge conflict
6580 adomani chore: `move_add`-driven replacements awaiting-author merge-conflict merge conflict
7467 ADedecker feat: spectrum of X →ᵇ ℂ is StoneCech X WIP merge-conflict t-analysis labelled WIP
7835 shuxuezhuyi feat(LinearAlgebra/Matrix): `lift` for projective special linear group awaiting-author merge-conflict t-algebra ??? missing CI information
7351 shuxuezhuyi feat(Topology/Algebra/Order): extend function on `Ioo` to `Icc` awaiting-author merge-conflict t-order merge conflict
7227 kmill feat: flexible binders and integration into notation3 WIP merge-conflict t-meta labelled WIP
7601 digama0 feat: ring hom support in `ring` awaiting-author merge-conflict t-meta t-algebra merge conflict
7909 mcdoll fix(Tactic/Continuity): remove npowRec and add new tag for Continuous.pow WIP merge-conflict t-meta t-topology labelled WIP
6079 eric-wieser fix: deduplicate variables merge-conflict awaiting-CI does not pass CI
6002 slerpyyy feat(Analysis.SpecialFunctions.Gaussian): add `integrable_fun_mul_exp_neg_mul_sq` awaiting-author merge-conflict t-analysis merge conflict
6195 eric-wieser chore(RingTheory/TensorProduct): golf the `mul` definition merge-conflict awaiting-CI t-algebra does not pass CI
6491 eric-wieser chore(Mathlib/Algebra/Hom/GroupAction): add `SMulHomClass.comp_smul` merge-conflict t-algebra merge conflict
6210 MohanadAhmed feat(Data/IsROrC/Basic): add a `StarOrderedRing` instance WIP merge-conflict t-analysis t-algebra labelled WIP
6330 astrainfinita chore: make some instance about `Sub...Class` higher priority than `Sub...` WIP merge-conflict t-algebra slow-typeclass-synthesis labelled WIP
7076 grunweg feat: define measure zero subsets of a manifold WIP merge-conflict t-differential-geometry t-measure-probability labelled WIP
4960 eric-wieser chore: use `open scoped` merge-conflict awaiting-CI does not pass CI
5133 kmill feat: IntermediateField adjoin syntax for sets of elements WIP merge-conflict t-algebra labelled WIP
4127 kmill refactor: create HasAdj class, define Digraph, and generalize some SimpleGraph API awaiting-author merge-conflict t-combinatorics merge conflict
4871 j-loreaux feat: define the additive submonoid of positive elements in a star ordered ring merge-conflict awaiting-CI t-algebra ??? does not pass CI
5912 ADedecker feat(Analysis.Distribution.ContDiffMapSupportedIn): space of smooth maps with support in a fixed compact WIP merge-conflict t-analysis labelled WIP
5934 eric-wieser feat: port Data.Rat.MetaDefs help-wanted mathlib-port merge-conflict t-meta looking for help
6328 FR-vdash-bot chore: make some instance about `Sub...Class` lower priority WIP merge-conflict awaiting-CI t-algebra labelled WIP
6403 astrainfinita chore: change instance priorities of `Ordered*` hierarchy awaiting-author merge-conflict t-algebra t-order slow-typeclass-synthesis merge conflict
3757 thorimur feat: config options for `fail_if_no_progress` WIP merge-conflict t-meta labelled WIP
12353 thorimur feat: `conv%` WIP merge-conflict t-meta labelled WIP
7903 urkud feat: define `UnboundedSpace` help-wanted merge-conflict t-topology looking for help
15400 grunweg feat: "confusing variables" linter WIP merge-conflict t-linter labelled WIP
15679 adomani test: refactor in CI WIP merge-conflict labelled WIP
10629 madvorak feat: List.cons_sublist_append_iff_right merge-conflict t-data merge conflict
9973 Ruben-VandeVelde feat: polynomials formed by lists please-adopt merge-conflict t-data looking for help
12926 joelriou feat(CategoryTheory): the monoidal category structure induced by a monoidal functor WIP merge-conflict t-category-theory labelled WIP
12869 adomani feat: linter and script for `theorem` vs `lemma` awaiting-author merge-conflict t-linter merge conflict
12093 ADedecker feat: tweak the definition of semicontinuity to behave better in nonlinear orders WIP merge-conflict t-topology labelled WIP
11393 mcdoll feat(Analysis/Distribution/SchwartzSpace): The Heine-Borel property WIP merge-conflict t-analysis labelled WIP
9444 erdOne feat: Various instances regarding `𝓞 K`. help-wanted merge-conflict t-number-theory looking for help
8931 hmonroe feat(Computable): define P, NP, and NP-complete awaiting-author merge-conflict t-computability failing CI
8608 eric-wieser feat: multiplicativize `AddTorsor` WIP merge-conflict t-algebra labelled WIP
6603 tydeu feat: automatically try `cache get` before build WIP merge-conflict CI labelled WIP
6058 apurvnakade feat: duality theory for cone programs WIP merge-conflict t-analysis labelled WIP
6449 ADedecker feat: functions with finite fibers awaiting-author merge-conflict t-topology failing CI
13791 digama0 refactor: Primrec and Partrec merge-conflict t-computability tech debt merge conflict
11964 adamtopaz feat: The functor of points of a scheme merge-conflict t-category-theory t-algebraic-geometry merge conflict
12418 rosborn style: replace preimage_val with ↓∩ notation merge-conflict merge conflict
9978 FR-vdash-bot chore(FieldTheory/KummerExtension): move some lemmas earlier awaiting-author merge-conflict t-algebra merge conflict
12429 adomani feat: toND -- auto-generating natDegree awaiting-author merge-conflict t-meta RFC t-algebra merge conflict
12751 Command-Master feat: add lemmas for Nat/Bits, Nat/Bitwise and Nat/Size merge-conflict new-contributor t-data merge conflict
15448 urkud chore(*): deprecate `Option.elim'` awaiting-author merge-conflict tech debt ??? missing CI information
10350 Shamrock-Frost feat(Data/Setoid): add the operations of taking the equivalence class of an element and of saturating a set wrt an equivalence relation merge-conflict t-data ??? missing CI information
13573 Shamrock-Frost feat: add multivariate polynomial modules awaiting-author merge-conflict t-algebra merge conflict
6517 MohanadAhmed feat: discrete Fourier transform of a finite sequence awaiting-author merge-conflict t-algebra merge conflict
13155 alreadydone feat(NumberTheory/EllipticDivisibilitySequence): show elliptic relations follow from even-odd recursion awaiting-author merge-conflict t-number-theory t-algebra merge conflict
15600 adomani feat: lint also `let` vs `have` WIP merge-conflict t-linter labelled WIP
14038 adomani test/decl diff in lean dev WIP merge-conflict labelled WIP
7545 shuxuezhuyi feat: APIs of `Function.extend f g e'` when `f` is injective awaiting-author merge-conflict t-logic merge conflict
14078 Ruben-VandeVelde feat(CI): continue after mk_all fails awaiting-author merge-conflict CI failing CI
11283 hmonroe feat(ModelTheory/Satisfiability): define theory with independent sentence WIP merge-conflict t-logic labelled WIP
16914 siddhartha-gadgil Loogle syntax with non-reserved WIP merge-conflict labelled WIP
8118 iwilare feat(CategoryTheory): add dinatural transformations awaiting-author merge-conflict t-category-theory merge conflict
7516 ADedecker perf: use `abbrev` to prevent unifying useless data WIP merge-conflict labelled WIP
17127 FR-vdash-bot chore: remove global `Quotient.mk` `⟦·⟧` notation merge-conflict t-data merge conflict
14712 FR-vdash-bot perf: change instance priority and order about `OfNat` delegated merge-conflict t-algebra slow-typeclass-synthesis merge conflict
11500 mcdoll refactor(Topology/Algebra/Module/WeakDual): Clean up awaiting-author merge-conflict t-topology merge conflict
5995 FR-vdash-bot feat: add APIs about `Quotient.choice` awaiting-author merge-conflict RFC t-data merge conflict
8029 alreadydone refactor: Homotopy between Functions not ContinuousMaps merge-conflict RFC t-topology merge conflict
13156 erdOne refactor(Algebra/Module/LocalizedModule): Redefine `LocalizedModule` in terms of `OreLocalization`. merge-conflict t-algebra failing CI
16348 urkud refactor(Topology): require `LinearOrder` with `OrderTopology` awaiting-author merge-conflict t-topology t-order merge conflict
16925 YnirPaz feat(SetTheory/Cardinal/Cofinality): aleph index of singular cardinal has infinite cofinality WIP merge-conflict t-set-theory labelled WIP
9605 davikrehalt feat(Data/Finset & List): Add Lemmas for Sorting and Filtering awaiting-author please-adopt merge-conflict new-contributor t-data looking for help
9654 urkud feat: add `@[mk_eq]` version of `@[mk_iff]` awaiting-author merge-conflict t-meta merge conflict
16704 AntoineChambert-Loir feat(Mathlib.Data.Ordering.Dickson): Dickson orders WIP merge-conflict t-order labelled WIP
16355 Ruben-VandeVelde feat: odd_{add,sub}_one awaiting-author merge-conflict t-number-theory t-algebra merge conflict
8479 alexjbest feat: use leaff in CI WIP awaiting-author merge-conflict ⚠️ labelled WIP
14598 Command-Master chore: add typeclasses to unify various `add_top`, `add_eq_top`, etc. merge-conflict t-algebra t-order new-contributor merge conflict
12778 MichaelStollBayreuth perf: decouple algebraic and order hierarchies in type class search merge-conflict t-algebra t-order slow-typeclass-synthesis merge conflict
16885 metinersin feat(ModelTheory/Complexity): define literals awaiting-author merge-conflict t-logic new-contributor merge conflict
9341 winstonyin feat: Naturality of integral curves awaiting-author merge-conflict t-differential-geometry merge conflict
13248 hcWang942 feat: basic concepts of auction theory awaiting-author merge-conflict t-logic new-contributor merge conflict
9344 erdOne feat: Add `AddGroup.FG` -> `Module.Finite ℤ` as instances awaiting-author merge-conflict t-algebra merge conflict
12133 ADedecker feat: generalize instIsLowerProd to arbitrary products awaiting-author merge-conflict t-topology t-order merge conflict
16637 FR-vdash-bot perf: reorder `extends` of `(Add)Monoid` WIP merge-conflict t-algebra labelled WIP
14739 urkud feat(Measure): add `gcongr` lemmas help-wanted WIP awaiting-author merge-conflict t-measure-probability looking for help
8661 joelriou feat(CategoryTheory/Sites): descent of sheaves WIP merge-conflict t-category-theory labelled WIP
10476 shuxuezhuyi feat(Topology/UniformSpace): define uniform preordered space awaiting-author merge-conflict t-topology merge conflict
17623 FR-vdash-bot feat(Algebra/Order/GroupWithZero/Unbundled): add some lemmas merge-conflict t-algebra t-order awaiting-zulip awaiting a zulip discussion
17513 FR-vdash-bot perf: do not search algebraic hierarchies when using `map_*` lemmas WIP merge-conflict t-algebra awaiting-bench labelled WIP
19212 Julian feat(LinearAlgebra): add a variable_alias for VectorSpace merge-conflict t-algebra merge conflict
19337 zeramorphic feat(Data/Finsupp): generalise `Finsupp` to any "zero" value merge-conflict t-data merge conflict
10332 adri326 feat(Topology/Sets): define regular open sets and their boolean algebra WIP merge-conflict t-topology labelled WIP
14501 jjaassoonn feat: module structure of filtered colimit of abelian groups over filtered colimit of rings awaiting-author merge-conflict t-category-theory t-algebra workshop-AIM-AG-2024 merge conflict
18756 astrainfinita refactor: deprecate `DistribMulActionSemiHomClass` `MulSemiringActionSemiHomClass` merge-conflict t-algebra merge conflict
19125 yhtq feat: add theorems to transfer `IsGalois` between pairs of fraction rings merge-conflict t-algebra new-contributor failing CI
18841 hrmacbeth chore: change some `linarith`s to `linear_combination`s WIP merge-conflict labelled WIP
18748 FR-vdash-bot refactor: deprecate `ContinuousLinearMapClass` merge-conflict t-topology t-algebra merge conflict
11142 hmonroe feat(ProofTheory): Define logical symbols abstractly; opens new top-level section, drawing from lean4-logic awaiting-author merge-conflict t-logic merge conflict
11210 hmonroe Test commit WIP merge-conflict labelled WIP
15773 kkytola feat: Add type class for ENat-valued floor functions awaiting-author merge-conflict t-order merge conflict
3251 kmill feat: deriving `LinearOrder` for simple enough inductive types WIP awaiting-author merge-conflict t-meta labelled WIP
3610 TimothyGu feat: derive Infinite automatically for inductive types awaiting-author merge-conflict t-meta merge conflict
16120 awainverse feat(ModelTheory/Algebra/Ring/Basic): Ring homomorphisms are a `StrongHomClass` for the language of rings merge-conflict RFC t-algebra t-logic failing CI
17739 Aaron1011 feat(Topology/Order/DenselyOrdered): prove Not (IsOpen) for intervals awaiting-author merge-conflict t-topology new-contributor merge conflict
18474 FR-vdash-bot perf: lower the priority of `*WithOne.to*` instances merge-conflict t-algebra slow-typeclass-synthesis t-data merge conflict
15711 znssong feat(Combinatorics/SimpleGraph): Some lemmas about walk, cycle and Hamiltonian cycle awaiting-author merge-conflict t-combinatorics new-contributor merge conflict
18629 tomaz1502 feat(Computability.Timed): Formalization of runtime complexity of List.merge awaiting-author merge-conflict new-contributor t-computability merge conflict
8362 urkud feat(Asymptotics): define `ReflectsGrowth` awaiting-author merge-conflict t-analysis failing CI
6692 prakol16 feat: disjoint indexed union of local homeomorphisms awaiting-author merge-conflict t-topology failing CI
19291 PieterCuijpers feat(Algebra/Order/Hom): add quantale homomorphism awaiting-author merge-conflict t-algebra new-contributor failing CI
19352 hrmacbeth chore: change some `nlinarith`s to `linear_combination`s WIP merge-conflict labelled WIP
20372 jvlmdr feat(MeasureTheory/Function): Add ContinuousLinearMap.bilinearCompLp(L) merge-conflict t-measure-probability new-contributor merge conflict
17176 arulandu feat: integrals and integrability with .re awaiting-author merge-conflict t-measure-probability new-contributor merge conflict
2605 eric-wieser chore: better error message in linarith awaiting-author merge-conflict t-meta merge conflict
11837 trivial1711 feat: completion of a uniform multiplicative group help-wanted WIP merge-conflict t-topology t-algebra looking for help
9449 hmonroe feat: Add Turing machine with the quintet definition (TMQ) and a chainable step function for each TM type awaiting-author merge-conflict t-computability failing CI
19697 quangvdao feat(BigOperators/Fin): Sum/product over `Fin` intervals awaiting-author merge-conflict t-data failing CI
19353 hrmacbeth chore: golf some term/rw proofs using `linear_combination` WIP merge-conflict labelled WIP
10678 adri326 feat(Topology/UniformSpace): prove that a uniform space is completely regular awaiting-author merge-conflict t-topology merge conflict
18785 erdOne feat(CategoryTheory): command that generates instances for `MorphismProperty` awaiting-author merge-conflict t-meta t-category-theory merge conflict
15942 grunweg chore: move style linters into their own file; document all current linters awaiting-author merge-conflict t-linter merge conflict
16311 madvorak feat(Computability): regular languages are context-free WIP merge-conflict t-computability labelled WIP
19943 AlexLoitzl feat(Computability): Add Chomsky Normal Form Grammar and translation awaiting-author merge-conflict new-contributor t-computability merge conflict
17005 YnirPaz feat(SetTheory/Cardinal/Regular): define singular cardinals WIP merge-conflict t-set-theory labelled WIP
12054 adomani feat: auto-bugs awaiting-author merge-conflict t-meta merge conflict
5062 adomani feat(Tactic/Prune + test/Prune): add `prune` tactic, for removing unnecessary hypotheses awaiting-author modifies-tactic-syntax merge-conflict t-meta merge conflict
16550 awainverse feat(ModelTheory): A typeclass for languages expanding other languages awaiting-author merge-conflict t-logic merge conflict
13686 fpvandoorn feat: some finset lemmas awaiting-author merge-conflict t-data merge conflict
14313 grhkm21 feat(RepresentationTheory/FdRep): FdRep is a full subcategory of Rep merge-conflict t-category-theory t-algebra new-contributor failing CI
10823 alexkeizer feat: convert curried type functions into uncurried type functions awaiting-author merge-conflict t-data merge conflict
13648 urkud feat(Topology/Module): generalize `ContinuousLinearMap.compSL` awaiting-author merge-conflict t-topology t-analysis t-algebra failing CI
18470 FR-vdash-bot perf: lower the priority of `Normed*.to*` instances merge-conflict t-analysis t-algebra slow-typeclass-synthesis ❌? infrastructure-related CI failing
16944 YnirPaz feat(SetTheory/Cardinal/Cofinality): lemmas about limit ordinals and cofinality WIP merge-conflict t-set-theory labelled WIP
17368 Felix-Weilacher feat(Topology/Baire/BaireMeasurable): add the Kuratowski-Ulam theorem merge-conflict t-topology failing CI
8767 eric-wieser refactor(Cache): tidy lake-manifest parsing in Cache merge-conflict t-meta failing CI
15578 znssong feat(Function): Fixed points of function `f` with `f(x) >= x` awaiting-author merge-conflict t-analysis new-contributor merge conflict
13999 adomani feat: a linter to flag potential confusing conventions awaiting-author merge-conflict t-linter merge conflict
19013 quangvdao feat(Algebra/BigOperators/Fin): Add `finSigmaFinEquiv` awaiting-author merge-conflict t-algebra merge conflict
19189 YnirPaz feat(SetTheory/Ordinal/Arithmetic): order isomorphism between omega and the natural numbers awaiting-author merge-conflict t-set-theory merge conflict
19227 adomani fix(CI): unwrap `lake test` in problem matcher awaiting-author merge-conflict CI merge conflict
15774 kkytola feat: Topology on `ENat` WIP merge-conflict t-topology t-order labelled WIP
18284 chrisflav feat(AlgebraicGeometry): relative gluing of schemes WIP merge-conflict t-algebraic-geometry labelled WIP
13124 FR-vdash-bot chore: remove `CovariantClass` and `ContravariantClass` WIP merge-conflict labelled WIP
19275 eric-wieser fix: if nolint files change, do a full rebuild delegated merge-conflict failing CI
15212 victorliu5296 feat: Add fundamental theorem of calculus-2 for Banach spaces awaiting-author merge-conflict t-analysis t-measure-probability new-contributor merge conflict
19425 hrmacbeth perf: gcongr forward-reasoning adjustment awaiting-author merge-conflict merge conflict
6252 michaellee94 feat(Geometry/Manifolds/Instances/Homeomorph): Homeomorphism maps `C^k` manifolds to `C^k` manifolds WIP merge-conflict t-differential-geometry labelled WIP
16314 FR-vdash-bot chore(Data/Quot): deprecate `ind*'` APIs merge-conflict t-data merge conflict
11455 adomani fix: unsqueeze simp, re Yaël's comments on #11259 awaiting-author merge-conflict merge conflict
7325 eric-wieser chore: use preimageIso instead of defeq abuse for InducedCategory merge-conflict awaiting-CI t-category-theory does not pass CI
7874 astrainfinita chore: make `IsScalarTower A A B` and `IsScalarTower A B B` higher priority merge-conflict awaiting-CI t-algebra slow-typeclass-synthesis ??? does not pass CI
5952 eric-wieser feat: add Qq wrappers for ToExpr merge-conflict t-meta awaiting-CI does not pass CI
15483 FR-vdash-bot chore(GroupTheory/Coset): reduce defeq abuse merge-conflict t-algebra merge conflict
16594 FR-vdash-bot perf: reorder `extends` and remove some instances in algebra hierarchy merge-conflict t-algebra slow-typeclass-synthesis failing CI
20313 thefundamentaltheor3m feat(Data/Complex/Exponential): prove some useful results about the complex exponential. merge-conflict t-analysis new-contributor failing CI
19117 eric-wieser feat: derivatives of matrix operations WIP merge-conflict t-analysis labelled WIP
12605 FR-vdash-bot chore: attribute [induction_eliminator] awaiting-author merge-conflict merge conflict
15099 joelriou feat(CategoryTheory/Sites): the Mayer-Vietoris long exact sequence in sheaf cohomology WIP merge-conflict t-category-theory labelled WIP
8370 eric-wieser refactor(Analysis/NormedSpace/Exponential): remove the `𝕂` argument from `exp` merge-conflict t-analysis awaiting-zulip failing CI
14731 adomani feat: the repeated typeclass assumption linter WIP merge-conflict t-linter large-import labelled WIP
13649 FR-vdash-bot chore: redefine `Nat.div2` `Nat.bodd` merge-conflict merge conflict
19520 erdOne refactor(Algebra/Module): Redefine `LocalizedModule` in terms of `OreLocalization` merge-conflict t-algebra failing CI
14675 adomani dev: the repeated variable linter WIP merge-conflict t-linter labelled WIP
14330 Ruben-VandeVelde chore: split Mathlib.Algebra.Star.Basic awaiting-author merge-conflict merge conflict
8511 eric-wieser refactor(MeasureTheory/Measure/Haar/Basic): partially generalize to the affine case awaiting-author merge-conflict t-measure-probability merge conflict
7994 ericrbg chore: generalize `LieSubalgebra.mem_map_submodule` please-adopt merge-conflict t-algebra looking for help
6317 eric-wieser refactor(Data/Finsupp/Defs): make Finsupp.single defeq to Pi.single WIP merge-conflict t-data labelled WIP
4979 mhk119 doc(Data/Nat/Bitblast): initial commit merge-conflict t-data merge conflict
11524 mcdoll refactor: Introduce type-class for SchwartzMap WIP merge-conflict t-analysis labelled WIP
19315 quangvdao feat(Data/Finsupp/Fin): Add `Finsupp` operations on `Fin` tuple awaiting-author merge-conflict t-data merge conflict
7907 urkud feat: introduce `NthRoot` notation class merge-conflict awaiting-CI t-analysis t-algebra does not pass CI
15115 kkytola feat: Generalize assumptions in liminf and limsup results in ENNReals help-wanted awaiting-author merge-conflict t-topology t-order looking for help
17129 joneugster feat(Tactic/Linter): add unicode linter for unicode variant-selectors awaiting-author delegated merge-conflict t-linter large-import failing CI
17131 joneugster feat(Tactic/Linter): add unicode linter for unwanted characters awaiting-author merge-conflict t-linter large-import merge conflict
12438 jjaassoonn feat: some APIs for flat modules WIP merge-conflict t-category-theory labelled WIP
8740 digama0 fix: improve `recall` impl / error reporting awaiting-author merge-conflict t-meta awaiting-CI does not pass CI
16062 adomani Test/ci olean size WIP awaiting-author merge-conflict CI labelled WIP
16020 adomani feat: compare PR `olean`s size with `master` merge-conflict CI failing CI
12799 jstoobysmith feat(LinearAlgebra/UnitaryGroup): Add properties of Special Unitary Group awaiting-author please-adopt merge-conflict t-algebra new-contributor looking for help
13994 grunweg chore(Topology): replace continuity -> fun_prop merge-conflict t-topology failing CI
13483 adomani feat: automatically replace deprecations awaiting-author delegated merge-conflict t-meta failing CI
20334 miguelmarco feat: allow polyrith to use a local Singular/Sage install awaiting-author merge-conflict t-meta new-contributor merge conflict
18441 ADedecker refactor(AdicTopology): use new API for algebraic filter bases, and factor some code merge-conflict t-topology t-algebra merge conflict
18439 ADedecker refactor: use new algebraic filter bases API in `FiniteAdeleRing` merge-conflict t-topology t-algebra merge conflict
18438 ADedecker refactor: adapt `KrullTopology` to the new algebraic filter bases API merge-conflict t-topology t-algebra merge conflict
13964 pechersky feat(Data/DigitExpansion): begin defining variant of reals without rationals merge-conflict t-data merge conflict
16074 Rida-Hamadani feat: combinatorial maps and planar graphs merge-conflict t-combinatorics merge conflict
16801 awainverse feat(ModelTheory/Equivalence): The quotient type of formulas modulo a theory awaiting-author merge-conflict t-logic merge conflict
17458 urkud refactor(Algebra/Group): make `IsUnit` a typeclass merge-conflict t-algebra awaiting-zulip failing CI
17627 hrmacbeth feat: universal properties of vector bundle constructions delegated merge-conflict t-differential-geometry merge conflict
19444 joelriou feat(CategoryTheory/Sites): Equivalence of categories of sheaves with a dense subsite that is 1-hypercover dense WIP merge-conflict t-category-theory labelled WIP
10541 Louddy feat(Algebra/SkewMonoidAlgebra/Basic): add SkewMonoidAlgebra WIP merge-conflict t-algebra new-contributor labelled WIP
13973 digama0 feat: lake exe refactor, initial framework awaiting-author merge-conflict t-meta merge conflict
10190 jstoobysmith feat(AlgebraicTopology): add Augmented Simplex Category WIP merge-conflict t-category-theory new-contributor t-algebraic-topology labelled WIP
20208 js2357 feat: Define the localization of a fractional ideal at a prime ideal WIP merge-conflict t-algebra labelled WIP
19596 Command-Master feat(RingTheory/Valuation/PrimeMultiplicity): define `WithTop ℤ`-valued prime multiplicity on a fraction field awaiting-author merge-conflict large-import t-ring-theory merge conflict
18646 jxjwan feat(RingTheory): isotypic components merge-conflict new-contributor t-ring-theory failing CI
17246 pechersky feat(RingTheory/PrimaryDecomposition): PIR of Noetherian under jacobson condition awaiting-author merge-conflict t-ring-theory failing CI
9820 jjaassoonn feat(RingTheory/GradedAlgebra/HomogeneousIdeal): generalize to homogeneous submodule merge-conflict t-ring-theory merge conflict
11212 shuxuezhuyi feat(GroupTheory/GroupAction): instance `MulAction (β ⧸ H) α` awaiting-author merge-conflict large-import t-group-theory merge conflict
17469 joelriou feat(Algebra/ModuleCat/Differentials/Presheaf): the presheaf of relative differentials WIP merge-conflict t-category-theory t-algebraic-geometry large-import labelled WIP
20267 joelriou feat(CategoryTheory): comma categories are accessible WIP awaiting-author merge-conflict t-category-theory labelled WIP
8102 miguelmarco feat(Tactic): add `unify_denoms` and `collect_signs` tactics good first issue modifies-tactic-syntax please-adopt merge-conflict t-meta new-contributor looking for help
14583 lecopivo fix: make concrete cycle notation local awaiting-author merge-conflict merge conflict
19097 Vierkantor chore(Algebra.Polynomial): split `Polynomial/Basic.lean` into smaller files merge-conflict t-algebra merge conflict
7300 ah1112 feat: synthetic geometry help-wanted awaiting-author merge-conflict t-euclidean-geometry looking for help
13795 astrainfinita perf(Algebra/{Group, GroupWithZero, Ring}/InjSurj): reduce everything merge-conflict t-algebra merge conflict
6042 MohanadAhmed feat(LinearAlgebra/Matrix/SVD): Singular Value Decomposition of R or C Matrices WIP please-adopt merge-conflict t-algebra looking for help
13036 joelriou feat(CategoryTheory/Sites): under certain conditions, cover preserving functors preserve 1-hypercovers WIP merge-conflict t-category-theory labelled WIP
7125 eric-wieser feat: additive monoid structure via biproducts WIP merge-conflict awaiting-CI t-category-theory labelled WIP
12278 Rida-Hamadani feat(Combinatorics/SimpleGraph): Provide iff statements for distance equal and greater than 2 awaiting-author merge-conflict t-combinatorics failing CI
16239 Rida-Hamadani feat(Geometry/Manifold): orientable manifolds awaiting-author merge-conflict t-differential-geometry failing CI
16773 arulandu feat(Probability/Distributions): formalize Beta distribution awaiting-author merge-conflict t-measure-probability new-contributor failing CI
9273 grunweg feat: extended charts are local diffeomorphisms on their source awaiting-author merge-conflict t-differential-geometry merge conflict
15045 Command-Master fix(LinearAlgebra/Alternating/Basic): fix `MultilinearMap.alternatization` awaiting-author merge-conflict t-algebra ??? missing CI information
19616 adamtopaz fix: fix the definition of the absolute Galois group of a field awaiting-author merge-conflict t-number-theory t-algebra merge conflict
14444 digama0 fix(GeneralizeProofs): unreachable! bug awaiting-author merge-conflict t-meta merge conflict
14752 AntoineChambert-Loir fix(Topology/Algebra/Valued): repair definition of Valued WIP merge-conflict t-topology t-algebra labelled WIP
10235 urkud feat: add `Decidable`, `Fintype`, `Encodable` linters awaiting-author merge-conflict t-meta t-linter large-import awaiting-bench failing CI
15651 TpmKranz feat(Computability/NFA): operations for Thompson's construction awaiting-author merge-conflict new-contributor t-computability awaiting-zulip awaiting a zulip discussion
9693 madvorak feat: Linear programming in the standard form WIP merge-conflict RFC t-algebra labelled WIP
15649 TpmKranz feat(Computability): introduce Generalised NFA as bridge to Regular Expression awaiting-author merge-conflict new-contributor t-computability awaiting-zulip awaiting a zulip discussion
20238 maemre feat(Computability/DFA): Closure of regular languages under some set operations awaiting-author merge-conflict new-contributor t-computability awaiting-zulip awaiting a zulip discussion
5745 alexjbest feat: a tactic to consume type annotations, and make constructor nicer awaiting-author merge-conflict t-meta merge conflict
5919 MithicSpirit feat: implement orthogonality for AffineSubspace help-wanted WIP merge-conflict t-analysis new-contributor looking for help
7219 Ruben-VandeVelde feat: Equivs for AddMonoidAlgebras awaiting-author merge-conflict t-algebra merge conflict
7386 madvorak feat: Define linear programs WIP merge-conflict RFC t-algebra labelled WIP
9352 chenyili0818 feat: arithmetic lemmas for `gradient` awaiting-author merge-conflict t-analysis merge conflict
9795 sinhp feat: the type `Fib` of fibre of a function at a point awaiting-author merge-conflict t-category-theory merge conflict
10660 eric-wieser feat(LinearAlgebra/CliffordAlgebra): construction from a basis WIP awaiting-author merge-conflict t-algebra labelled WIP
10977 grunweg feat: germs of smooth functions awaiting-author merge-conflict t-differential-geometry t-topology t-analysis failing CI
10998 hmonroe feat(Logic): Arithmetization of partial recursive functions (toward Gödel's first incompleteness theorem) awaiting-author merge-conflict t-logic merge conflict
11155 smorel394 feat(LinearAlgebra/Multilinear/DirectSum, LinearAlgebra/DirectSum/{PiTensorProduct,Finsupp}): interaction between `MultilinearMap` and `DirectSum`, and between `PiTensorProduct` and `DirectSum` please-adopt merge-conflict t-algebra looking for help
11890 adomani feat: the terminal refine linter awaiting-author merge-conflict t-linter merge conflict
12006 adomani feat: the `suffa` tactic awaiting-author merge-conflict t-meta merge conflict
13442 dignissimus feat: mabel tactic for multiplicative abelian groups help-wanted awaiting-author modifies-tactic-syntax merge-conflict t-meta new-contributor looking for help
14237 js2357 feat: Define the localization of a fractional ideal at a prime ideal awaiting-author merge-conflict t-algebra new-contributor failing CI
14345 digama0 feat: the Dialectica category is monoidal closed awaiting-author merge-conflict t-category-theory merge conflict
14727 jjaassoonn feat(RingTheory/Flat/CategoryTheory): a flat module has vanishing higher Tor groups awaiting-author merge-conflict t-ring-theory merge conflict
14733 jjaassoonn feat(RingTheory/Flat/CategoryTheory): a module is flat iff tensoring preserves finite limits awaiting-author merge-conflict t-ring-theory merge conflict
15055 sinhp feat: the category of pointed objects of a concrete category awaiting-author merge-conflict t-category-theory merge conflict
15224 AnthonyBordg feat(CategoryTheory/Sites): covering families and their associated Grothendieck topology awaiting-author merge-conflict t-category-theory new-contributor merge conflict
16303 grunweg feat(CI): check for badly formatted titles or missing/contradictory labels awaiting-author merge-conflict CI failing CI
18236 joelriou feat(Algebra/Category/ModuleCat/Presheaf): the endofunctor of presheaves of modules induced by an oplax natural transformation WIP awaiting-author merge-conflict awaiting-CI t-category-theory t-algebra labelled WIP
18749 GabinKolly feat(ModelTheory): preparatory work for the existence of Fraïsse limits awaiting-author merge-conflict t-logic merge conflict
19323 madvorak feat: Function to Sum decomposition WIP merge-conflict t-data labelled WIP
19378 adamtopaz feat: Explanation widgets awaiting-author merge-conflict t-meta merge conflict
19456 AntoineChambert-Loir feat(Data/Finsupp/MonomialOrder/DegRevLex): homogeneous reverse lexicographic order WIP merge-conflict t-algebraic-geometry t-order t-data labelled WIP
6268 eric-wieser fix: fixups to #3838 WIP merge-conflict labelled WIP
6993 jjaassoonn feat: lemmas about `AddMonoidAlgebra.{divOf, modOf}` merge-conflict t-algebra merge conflict
7427 MohanadAhmed feat: eigenvalues sorted in ascending/descending order WIP merge-conflict ⚠️ labelled WIP
9339 FMLJohn feat(RingTheory/GradedAlgebra/HomogeneousIdeal): given a finitely generated homogeneous ideal of a graded semiring, construct a finite spanning set for the ideal which only contains homogeneous elements merge-conflict t-ring-theory merge conflict
9564 AntoineChambert-Loir chore: weaken commutativity assumptions for AdjoinRoot.lift and AdjoinRoot.liftHom WIP merge-conflict t-algebra ??? labelled WIP
10026 madvorak feat: linear programming according to Antoine Chambert-Loir's book WIP merge-conflict RFC t-algebra labelled WIP
10159 madvorak feat: linear programming according to Antoine Chambert-Loir's book — affine version WIP merge-conflict RFC t-algebra labelled WIP
10349 Shamrock-Frost refactor(CategoryTheory/MorphismProperty): some clean-ups merge-conflict t-category-theory ??? missing CI information
11021 jstoobysmith feat(AlgebraicTopology): add join of augmented SSets WIP merge-conflict new-contributor t-algebraic-topology labelled WIP
11800 JADekker feat: KappaLindelöf spaces please-adopt merge-conflict t-topology awaiting-zulip ??? looking for help
11575 ScottCarnahan feat(RingTheory/HahnSeries/Addition): lemmas on leading terms WIP merge-conflict t-ring-theory labelled WIP
12251 ScottCarnahan refactor(RingTheory/HahnSeries): several generalizations WIP merge-conflict t-algebra t-order labelled WIP
12394 JADekker feat: define pre-tight and tight measures awaiting-author please-adopt merge-conflict t-measure-probability looking for help
14426 adomani feat: `#min_imps` command (development branch) WIP merge-conflict ??? ⚠️ labelled WIP
14686 smorel394 feat(AlgebraicGeometry/Grassmannian): define the Grassmannian scheme WIP please-adopt merge-conflict t-algebraic-geometry workshop-AIM-AG-2024 ??? looking for help
17071 ScottCarnahan feat(LinearAlgebra/RootSystem): separation, base, cartanMatrix WIP merge-conflict t-algebra ??? labelled WIP
18626 hannahfechtner feat: define Artin braid groups awaiting-author merge-conflict t-algebra new-contributor merge conflict
20029 FrederickPu feat(Tactic/simps): allow for Config attributes to be set directly WIP merge-conflict t-meta new-contributor labelled WIP
10991 thorimur feat: `tfae` block tactic WIP modifies-tactic-syntax merge-conflict t-meta labelled WIP
6633 adomani feat(..Polynomial..): `MvPolynomial`s have no zero divisors awaiting-author merge-conflict t-algebra merge conflict
20527 trivial1711 refactor(Topology/UniformSpace/Completion): more descriptive names for `α → Completion α` merge-conflict t-topology merge conflict
20656 Komyyy feat(Mathlib/Geometry/Manifold/VectorBundle/Sphere): convert orthogonal smooth `M → 𝕊ⁿ` & `M → ℝⁿ⁺¹` to smooth `M → T𝕊ⁿ` please-adopt merge-conflict t-differential-geometry looking for help
20872 grunweg feat: lint against the tactic.skipAssignedInstances option in mathlib awaiting-author merge-conflict t-linter tech debt merge conflict
21433 grunweg chore: change more lemmas to be about enorm instead of nnnorm awaiting-author merge-conflict t-measure-probability carleson merge conflict
20454 urkud chore(TangentCone): review names merge-conflict t-analysis failing CI
21959 BGuillemet feat(Topology/ContinuousMap): Stone-Weierstrass theorem for MvPolynomial merge-conflict t-topology new-contributor merge conflict
22660 Ruben-VandeVelde chore: follow naming convention around Group.IsNilpotent merge-conflict t-algebra merge conflict
20874 grunweg chore(nolint.yml): use shallow clones awaiting-author merge-conflict CI merge conflict
20613 grunweg chore: golf using `List.toArrayMap` merge-conflict large-import failing CI
22682 grunweg chore(Topology/Homeomorph): split out various constructions merge-conflict RFC t-topology tech debt failing CI
21018 markimunro feat(Data/Matrix): add file with key definitions and theorems about elementary row operations enhancement awaiting-author merge-conflict new-contributor t-data 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 WIP merge-conflict t-topology t-analysis labelled WIP
20401 RemyDegenne feat: add sigmaFinite_iUnion awaiting-author merge-conflict t-measure-probability merge conflict
22727 grunweg feat: rewrite the isolated by and colon linters in Lean awaiting-author merge-conflict t-linter merge conflict
22579 kvanvels doc(Topology/Defs/Induced): fix comments on three functions related to RestrictGenTopology documentation awaiting-author merge-conflict t-topology merge conflict
21488 imbrem feat(CategoryTheory/Monoidal): premonoidal categories merge-conflict t-category-theory new-contributor merge conflict
21525 sinhp feat(CategoryTheory): Locally Cartesian Closed Categories (Prelim) merge-conflict t-category-theory large-import merge conflict
20873 vbeffara feat(Topology/Covering): path lifting and homotopy lifting awaiting-author merge-conflict t-topology new-contributor failing CI
22817 peabrainiac feat(CategoryTheory/Sites): local sites WIP merge-conflict t-category-theory labelled WIP
23509 eric-wieser refactor: Make ENNReal an abbrev merge-conflict t-data failing CI
20567 grunweg feat(Cache): two small features merge-conflict t-meta merge conflict
22698 Kiolt feat: notation for whisker(Left/Right)Iso merge-conflict t-category-theory toric failing CI
20730 kuotsanhsu feat(LinearAlgebra/Matrix/SchurTriangulation): prove Schur decomposition/triangulation awaiting-author merge-conflict t-algebra new-contributor failing CI
23859 urkud feat(Topology/../Order/Field): generalize to `Semifield` merge-conflict t-topology merge conflict
23810 b-reinke chore(Order/Interval): generalize succ/pred lemmas to partial orders merge-conflict t-order merge conflict
24285 madvorak chore(Algebra/*-{Category,Homology}): remove unnecessary universe variables merge-conflict t-algebra merge conflict
22583 imathwy feat: affinespace homeomorphism awaiting-author merge-conflict t-algebra failing CI
23593 erdOne feat(AlgebraicGeometry): the tilde construction is functorial awaiting-author merge-conflict t-algebraic-geometry merge conflict
21065 eric-wieser feat: generalize `tangentConeAt.lim_zero` to TVS WIP merge-conflict t-analysis labelled WIP
22721 grunweg chore(MeasureTheory/Function/LpSeminorm/Basic): generalise more results to enorm classes WIP merge-conflict t-measure-probability carleson labelled WIP
24354 grunweg chore(HasFiniteIntegral): rename three lemmas merge-conflict t-measure-probability merge conflict
23546 JovanGerb feat(LinearAlgebra/AffineSpace/AffineSubspace): rename `AffineSubspace.mk'` to `Submodule.shift` merge-conflict t-euclidean-geometry merge conflict
24642 grunweg WIP-feat: add layercake formula for ENNReal-valued functions WIP merge-conflict t-analysis carleson labelled WIP
21712 grunweg chore: generalise more lemmas to `ContinuousENorm` merge-conflict awaiting-CI t-measure-probability carleson does not pass CI
21375 grunweg WIP: generalise lemmas to ENorm WIP merge-conflict awaiting-CI t-measure-probability carleson labelled WIP
22837 joneugster feat(Data/Set/Basic): add subset_iff and not_mem_subset_iff merge-conflict t-data t-set-theory merge conflict
24100 eric-wieser feat: restore some explicit binders from Lean 3 awaiting-author merge-conflict tech debt ⚠️ failing CI
21476 grunweg feat(lint-style): enable running on downstream projects merge-conflict t-linter merge conflict
23349 BGuillemet feat: add LocallyLipschitzOn.lipschitzOnWith_of_isCompact and two small lemmas about Lipschitz functions merge-conflict t-topology new-contributor large-import merge conflict
21182 joneugster fix(Util/CountHeartbeats): move elaboration in #count_heartbeats inside a namespace merge-conflict t-meta merge conflict
23371 grunweg chore: mark `Disjoint.{eq_bot, inter_eq}` simp awaiting-author merge-conflict t-order merge conflict
23709 plp127 feat: `Nat.findFrom` merge-conflict t-data failing CI
25340 dupuisf chore(Analysis/Convex): move files pertaining to convex/concave functions to their own folder merge-conflict t-convex-geometry merge conflict
21734 adomani fix(PR summary): checkout GITHUB_SHA WIP awaiting-author merge-conflict CI labelled WIP
23953 b-reinke feat(Data/Matroid/Tutte): define the Tutte polynomial of a matroid WIP merge-conflict t-data labelled WIP
22928 javra feat(CategoryTheory): infrastructure for inclusion morphisms into products in categories with 0-morphisms merge-conflict t-category-theory failing CI
23763 grunweg feat(Linter.openClassical): also lint for Classical declarations as … merge-conflict t-linter failing CI
24710 chrisflav chore(Data/Set): `tsum` version of `Set.encard_iUnion_of_finite` for non-finite types merge-conflict t-data failing CI
24823 eric-wieser refactor: add `hom` lemmas for the `MonoidalCategory` structure on `ModuleCat` merge-conflict t-algebra merge conflict
25071 erdOne feat(EllipticCurve): basic API for singular cubics merge-conflict t-algebraic-geometry merge conflict
25218 kckennylau feat(AlgebraicGeometry): Tate normal form of elliptic curves merge-conflict t-algebraic-geometry new-contributor awaiting-zulip awaiting a zulip discussion
25283 Brian-Nugent feat: regular local rings merge-conflict t-algebra new-contributor merge conflict
25561 callesonne feat(Category/Grpd): define the bicategory of groupoids awaiting-author merge-conflict t-category-theory merge conflict
25573 JovanGerb feat: define `∃ x > y, ...` notation to mean `∃ x, y < x ∧ ...` merge-conflict t-meta merge conflict
25622 eric-wieser refactor: overhaul instances on LocalizedModule merge-conflict t-algebra failing CI
25988 Multramate refactor(AlgebraicGeometry/EllipticCurve/*): replace Fin 3 with products merge-conflict t-algebraic-geometry merge conflict
26090 grunweg chore: make `finiteness` a default tactic merge-conflict failing CI
24405 mcdoll refactor(Topology/Algebra/Module/WeakDual): Clean up merge-conflict t-topology large-import merge conflict
26647 b-mehta feat(Data/Sym/Sym2): lift commutative operations to sym2 WIP merge-conflict t-data labelled WIP
26067 mapehe feat(Topology/StoneCech): exists_continuous_surjection_from_StoneCech_to_dense_range merge-conflict t-topology merge conflict
25999 bjoernkjoshanssen feat(Topology/Compactification): projective line over ℝ is homeomorphic to the one-point compactification of ℝ merge-conflict t-topology failing CI
25710 Paul-Lez feat(Mathlib/Analysis/PDE/Quasilinear/Characteristics): the method of characteristics for first order quasilinear PDEs WIP merge-conflict t-analysis labelled WIP
26911 JovanGerb chore: fix naming of `mono` and `monotone` delegated merge-conflict merge conflict
21838 joneugster feat(Cache): Allow arguments of the form `Mathlib.Data` which correspond to a folder but not a file awaiting-author merge-conflict t-meta CI merge conflict
25611 erdOne chore(RingTheory): add `Algebra (FractionRing R) (FractionRing S)` merge-conflict t-algebra failing CI
25284 alreadydone feat(LinearAlgebra/Contraction): bijectivity of `dualTensorHom` + generalize to CommSemiring awaiting-author merge-conflict t-algebra merge conflict
22749 joelriou feat(CategoryTheory/Abelian): the Gabriel-Popescu theorem as a localization with respect to a Serre class WIP merge-conflict t-category-theory labelled WIP
20428 madvorak feat(Data/Sign): lemmas about `∈ Set.range SignType.cast` WIP merge-conflict t-data labelled WIP
20719 gio256 feat(AlgebraicTopology): delaborators for truncated simplicial notations merge-conflict t-meta infinity-cosmos t-algebraic-topology merge conflict
25914 eric-wieser feat: add an ext lemma for the opposite category awaiting-author merge-conflict awaiting-CI t-category-theory does not pass CI
24260 plp127 feat(Topology): add API for Hereditarily Lindelof spaces awaiting-author merge-conflict t-topology merge conflict
27608 RemyDegenne feat(MeasureTheory): typeclasses for measures with finite moments WIP merge-conflict t-measure-probability labelled WIP
25991 Multramate feat(AlgebraicGeometry/EllipticCurve): generalise nonsingular condition merge-conflict t-algebraic-geometry failing CI
25985 Multramate feat(AlgebraicGeometry/EllipticCurve/Jacobian): add equivalences between points and explicit WithZero types merge-conflict t-algebraic-geometry failing CI
25984 Multramate feat(AlgebraicGeometry/EllipticCurve/Affine): add equivalences between points and explicit WithZero types merge-conflict t-algebraic-geometry failing CI
25982 Multramate feat(AlgebraicGeometry/EllipticCurve/Group): compute range of baseChange merge-conflict t-algebraic-geometry failing CI
25981 Multramate feat(GroupTheory/GroupAction/Basic): define homomorphisms of fixed subgroups induced by homomorphisms of groups merge-conflict t-group-theory failing CI
25980 Multramate feat(GroupTheory/Submonoid/Operations): define homomorphisms of subgroups induced by homomorphisms of groups merge-conflict t-group-theory failing CI
25485 VTrelat feat(SetTheory/ZFC/Naturals): define natural numbers in ZFC merge-conflict new-contributor t-set-theory failing CI
25474 adomani test for .lean/.md check merge-conflict t-linter file-removed failing CI
25238 Hagb feat(Tactic/ComputeDegree): add support for scalar multiplication with different types merge-conflict t-meta new-contributor merge conflict
26385 jjdishere feat(RingTheory/Perfectoid): define integral perfectoid rings WIP merge-conflict t-ring-theory labelled WIP
22898 AntoineChambert-Loir feat(RingTheory/TensorProduct/DirectLimit/FG): direct limit of finitely generated submodules and tensor product WIP merge-conflict t-ring-theory labelled WIP
20431 erdOne feat(RingTheory/AdicCompletion): monotonicity of adic-completeness awaiting-author merge-conflict t-ring-theory merge conflict
21474 erdOne feat(RingTheory): replace `Ring.DimensionLEOne` with `Ring.KrullDimLE` merge-conflict large-import t-ring-theory failing CI
27886 alreadydone feat(Algebra): (Mv)Polynomial.X is irreducible assuming NoZeroDivisors awaiting-author merge-conflict t-algebra merge conflict
26200 adomani fix: add label when landrun fails merge-conflict CI merge conflict
27709 kckennylau chore: fix links WIP merge-conflict labelled WIP
20671 thefundamentaltheor3m feat(Analysis/Asymptotics/SpecificAsymptotics): Proving that 𝛔ₖ(n) = O(nᵏ⁺¹) awaiting-author merge-conflict t-number-theory new-contributor large-import merge conflict
27451 kckennylau feat(RingTheory/Valuation): define ball, closed ball, and sphere merge-conflict t-ring-theory merge conflict
27987 kckennylau feat(RingTheory/Valuation): define ball, closed ball, and sphere merge-conflict large-import t-ring-theory merge conflict
24862 grunweg feat(LocallyIntegrable): generalise more to enorms WIP merge-conflict t-measure-probability carleson labelled WIP
27003 eric-wieser chore: use `Simp.ResultQ` more often merge-conflict t-meta merge conflict
25483 VTrelat chore(Data/Set/Prod, SetTheory/ZFC/Basic): add theorem prod_subset_of_prod and extend ZFC model merge-conflict new-contributor t-data merge conflict
25401 digama0 feat(Util): SuppressSorry option merge-conflict t-meta merge conflict
26394 winstonyin feat: existence of local flows on manifolds WIP merge-conflict t-differential-geometry labelled WIP
27759 plp127 chore(FreeAbelianGroup): deprecate multiplication merge-conflict t-algebra large-import failing CI
27446 grunweg chore: more enorm lemmas WIP merge-conflict carleson labelled WIP
28622 alreadydone chore(Mathlib): replace `=>` by `↦` merge-conflict merge conflict
24793 tristan-f-r feat: trace of unitarily similar matrices awaiting-author merge-conflict t-algebra merge conflict
27872 JovanGerb chore(gcongr): clean up imports delegated merge-conflict large-import failing CI
28626 alreadydone chore(Archive, Counterexamples): replace => by ↦ merge-conflict merge conflict
28150 Equilibris chore: clean up proofs typevec proofs merge-conflict new-contributor t-data merge conflict
27868 grunweg linter indentation playground WIP merge-conflict t-linter labelled WIP
27403 MoritzBeroRoos fix: replace probably erroneous usage of ⬝ (with old \cdot) by · (with \centerdot) merge-conflict new-contributor merge conflict
28042 kckennylau feat(Topology/ValuativeRel): a topological basis indexed by pairs of elements merge-conflict t-ring-theory merge conflict
27399 MoritzBeroRoos chore: replace every usage of ⬝ᵥ (with old \cdot) by ·ᵥ (with \centerdot) merge-conflict new-contributor merge conflict
27835 edegeltje feat(Tactic): ring modulo a given characteristic merge-conflict t-meta large-import migrated-from-branch ❌? infrastructure-related CI failing
25889 plp127 fix(Tactic/Widget/Conv): fix various issues merge-conflict t-meta merge conflict
27437 kckennylau feat(RingTheory/Valuation): some lemmas about comparing with 1 and 0 and with each other WIP merge-conflict t-ring-theory labelled WIP
27785 staroperator chore(Algebra/Group/Submonoid): golf `Nat.addSubmonoidClosure_one` using `simp` merge-conflict t-algebra large-import merge conflict
28148 kckennylau feat(Matrix): Simproc and Rw-proc for Matrix Transpose merge-conflict t-meta merge conflict
26931 javra feat(CategoryTheory/Enriched): `V`-enriched isomorphisms awaiting-author merge-conflict t-category-theory infinity-cosmos merge conflict
25208 erdOne feat(LinearAlgebra): `tensor_induction` macro WIP merge-conflict RFC t-algebra labelled WIP
28803 astrainfinita refactor: unbundle algebra from `ENormed*` merge-conflict t-analysis t-algebra slow-typeclass-synthesis awaiting-zulip awaiting a zulip discussion
26603 vihdzp refactor(SetTheory/Ordinal/FixedPoint): redefine `Ordinal.deriv` merge-conflict t-set-theory failing CI
25662 erdOne chore: redefine `LocalizedModule` merge-conflict t-algebra failing CI
27566 wwylele feat(Data/Real): Archimedean.embedReal is a ring hom when M is an ordered ring merge-conflict t-data large-import merge conflict
28151 iehality feat(Computability): r.e. sets are closed under inter/union/projection/composition awaiting-author merge-conflict t-computability merge conflict
26908 robin-carlier feat(CategoryTheory/Monoidal/DayConvolution): alternative ext principle for unitors merge-conflict t-category-theory merge conflict
27150 robin-carlier feat(CategoryTheory/Monoidal/DayConvolution): constructors for braided and symmetric structure on day convolutions monoidal categories merge-conflict t-category-theory merge conflict
27119 robin-carlier feat(CategoryTheory/Monoidal/DayConvolution): constructors for closed monoidal day convolution monoidal structures merge-conflict t-category-theory merge conflict
28623 gilesgshaw feat(Logic/Basic): minor additions and simplification of proofs merge-conflict t-logic new-contributor merge conflict
27335 eric-wieser chore(Data/List): use simp-normal-form for boolean equalities merge-conflict t-data failing CI
22517 j-loreaux feat: `ℕ+` powers in semigroups WIP merge-conflict large-import ⚠️ labelled WIP
27933 grunweg chore(OrdNode): format code example in code blocks merge-conflict t-data merge conflict
28802 grunweg feat: a tactic linter for continuity/measurability which can be `fun_prop` merge-conflict t-meta awaiting-CI large-import does not pass CI
25069 erdOne feat(EllipticCurve): rational points of singular nodal cubics awaiting-author merge-conflict t-algebraic-geometry merge conflict
25070 erdOne feat(EllipticCurve): rational points on singular cuspidal cubics awaiting-author merge-conflict t-algebraic-geometry merge conflict
26670 yu-yama feat(GroupExtension/Abelian): define `conjClassesEquivH1` awaiting-author merge-conflict t-algebra merge conflict
26154 ADedecker refactor: add refactored APIs for algebraic filter bases merge-conflict t-topology merge conflict
27024 grunweg feat: Gram-Schmidt orthonormalisation for sections of a vector bundle awaiting-author merge-conflict t-differential-geometry merge conflict
28580 kmill refactor: simplify implementation of `filter_upwards` merge-conflict t-meta t-order failing CI
29605 alreadydone experiment(Algebra): unbundle npow/zpow from Monoid/InvDivMonoid merge-conflict awaiting-CI t-algebra does not pass CI
27972 smmercuri refactor: make `Valuation.Completion` a `def` and refactor more of `AdicValuation.lean` WIP merge-conflict t-number-theory t-algebra labelled WIP
28908 joelriou feat(CategoryTheory): Pullback functors on `Over` categories in `Type` have right adjoints awaiting-author merge-conflict t-category-theory failing CI
25480 ocfnash feat: define a concrete model of the `𝔤₂` root system WIP merge-conflict t-algebra large-import labelled WIP
29330 plp127 chore: define `Fin.cycleIcc` with conditions merge-conflict t-group-theory merge conflict
27829 dupuisf feat: modify `cfc_tac` to use `grind` WIP merge-conflict ⚠️ labelled WIP
21950 erdOne feat(NumberTheory/Padics): the completion of `ℚ` at a finite place is `ℚ_[p]` merge-conflict t-number-theory merge conflict
27668 IvanRenison feat(Analysis/InnerProductSpace): define outer product of linear maps merge-conflict t-analysis failing CI
29092 zhuyizheng feat(MeasureTheory): add absolutely continuous functions, FTC and integration by parts awaiting-author merge-conflict t-measure-probability new-contributor merge conflict
26178 ppls-nd-prs feat(CategoryTheory/Limits): Fubini for products awaiting-author merge-conflict t-category-theory new-contributor merge conflict
27214 robin-carlier feat(CategoryTheory/Limits/Shapes/Pullback/Categorical): Categorical pullback squares merge-conflict t-category-theory merge conflict
26466 robin-carlier feat(AlgebraicTopology/SimplexCategory/Augmented): the canonical monoid object in the augmented simplex category merge-conflict t-category-theory t-algebraic-topology merge conflict
28074 grunweg Isbilinearmap WIP merge-conflict labelled WIP
26578 robin-carlier feat(CategoryTheory/Limits/Pullbacks/Categorical/CatCospanTransform): adjunctions of categorical cospans merge-conflict t-category-theory large-import merge conflict
29012 grunweg chore: reduce `Topology` imports in `Data` merge-conflict file-removed failing CI
26601 yuma-mizuno feat(CategoryTheory): make `Functor.comp` irreducible WIP merge-conflict t-category-theory labelled WIP
23621 astrainfinita chore: deprecate `LinearOrderedComm{Monoid, Group}WithZero` merge-conflict t-algebra t-order merge conflict
30192 erdOne feat(RingTheory): valuative topology = adic topology for discrete rank 1 valuations WIP merge-conflict t-topology t-ring-theory labelled WIP
26344 mans0954 feat(Analysis/NormedSpace/MStructure): The component projections on WithLp 1 (α × β) are L-projections WIP merge-conflict t-analysis file-removed labelled WIP
25992 Multramate feat(RingTheory/Ideal/Span): add pair lemmas awaiting-author merge-conflict t-ring-theory 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` awaiting-author merge-conflict ⚠️ merge conflict
22657 Xmask19 feat: a graph is maximally acyclic iff it is a tree merge-conflict t-combinatorics new-contributor failing CI
27990 kckennylau feat(Counterexamples): a nontrivial valuation with discrete topology merge-conflict t-ring-theory merge conflict
28243 robin-carlier chore(CategoryTheory/Bicategory): move some `eqToHom` lemmas awaiting-author merge-conflict t-category-theory merge conflict
29120 eric-wieser feat: add a typeclass for the indiscrete topology merge-conflict t-topology failing CI
26339 mans0954 feat(Analysis/Normed/Module/WeakDual): Banach Dieudonné Lemma WIP merge-conflict t-analysis large-import labelled WIP
29378 mans0954 feat(Analysis/LocallyConvex/AbsConvex): Balanced and AbsConvex sets under linear maps merge-conflict t-analysis merge conflict
21853 smmercuri feat: the adele ring of a number field is locally compact WIP merge-conflict t-number-theory large-import labelled WIP
26913 Paul-Lez feat(NumberTheory/{*}): add a few lemmas about number field and cyclotomic extensions WIP merge-conflict awaiting-CI t-number-theory t-algebra labelled WIP
28925 grunweg chore: remove `linear_combination'` tactic merge-conflict awaiting-zulip file-removed awaiting a zulip discussion
28826 alreadydone feat(CategoryTheory): Additive and Linear when Hom types are only monoids WIP merge-conflict awaiting-CI t-category-theory labelled WIP
28126 Sebi-Kumar feat(AlgebraicTopology/FundamentalGroupoid): relate equality in fundamental groupoid to homotopy awaiting-author merge-conflict new-contributor t-algebraic-topology merge conflict
24532 robertmaxton42 feat(LinearAlgebra/FreeProduct): fill out the `FreeProduct.asPowers` namespace merge-conflict t-algebra failing CI
27683 dupuisf feat: grind tags for set operations merge-conflict t-data failing CI
25978 Bergschaf feat(Order/Sublocale): Open Sublocales merge-conflict t-order merge conflict
29355 girving feat(Trigonometric): Taylor series bounds for sin and cos merge-conflict t-analysis failing CI
28298 thorimur chore: dedent `to_additive` docstrings documentation awaiting-author merge-conflict merge conflict
28737 astrainfinita refactor: deprecate `MulEquivClass` awaiting-author merge-conflict t-algebra merge conflict
28676 sun123zxy feat(NumberTheory/ArithmeticFunction): wrap `Nat.totient` as an `ArithmeticFunction` awaiting-author merge-conflict t-number-theory new-contributor large-import merge conflict
30421 grunweg WIP: support products in the differential geometry elaborators merge-conflict failing CI
30299 franv314 feat(Topology/Instances): Cantor set awaiting-author merge-conflict t-topology new-contributor file-removed merge conflict
30690 grunweg style(Order): fix whitespace merge-conflict t-order merge conflict
27976 smmercuri feat: `ramificationIdx` for `NumberField.InfinitePlace` WIP merge-conflict t-number-theory labelled WIP
26357 javra feat(CategoryTheory): linear categories as `ModuleCat R`-enriched categories awaiting-author merge-conflict t-category-theory large-import merge conflict
26085 grunweg feat: disjoint unions distribute with products of manifolds WIP please-adopt merge-conflict t-differential-geometry looking for help
27180 ADedecker feat: quotient of a monoid with zero by a multiplicative congruence delegated merge-conflict t-algebra merge conflict
30790 urkud chore: partially migrate from `ContinuousMap.continuous` merge-conflict failing CI
26259 Raph-DG feat(Topology): Connecting different notions of locally finite awaiting-author merge-conflict t-topology merge conflict
25692 Whysoserioushah feat(RingTheory/MatrixAlgebra): add a more general version of `matrixEquivTensor` awaiting-author merge-conflict t-ring-theory 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 WIP merge-conflict t-category-theory labelled WIP
22361 rudynicolop feat(Computability/NFA): nfa closure properties awaiting-author merge-conflict new-contributor t-computability awaiting-zulip awaiting a zulip discussion
31220 fgdorais chore: adaptations for batteries#1489 merge-conflict blocked-by-batt-PR large-import blocked on another PR
27708 vihdzp feat: unions and intersections of ordinals are ordinals awaiting-author merge-conflict t-set-theory merge conflict
29550 Raph-DG feat(RingTheory): Order of vanishing in a discrete valuation ring awaiting-author merge-conflict file-removed t-ring-theory failing CI
28132 dupuisf feat: preliminary `grind` tags for `IsUnit` merge-conflict t-algebra merge conflict
26735 Raph-DG feat(AlgebraicGeometry): The codimension of a point of a scheme is equal to the krull dimension of the stalk awaiting-author merge-conflict t-algebraic-geometry large-import failing CI
30686 grunweg tracking: #30658 split into pieces merge-conflict large-import failing CI
29877 Komyyy feat: inner product of the gradient merge-conflict t-analysis merge conflict
29992 vlad902 feat(Order): finite (Max)Chains always contains a top/max element WIP merge-conflict t-order large-import labelled WIP
26901 5hv5hvnk feat: a simproc version of `compute_degree` awaiting-author merge-conflict t-meta awaiting-CI new-contributor does not pass CI
28153 kckennylau feat(Simproc): Simproc for explicit diagonal matrices awaiting-author merge-conflict t-meta merge conflict
31020 grunweg feat: mfderiv of Sum.inl and Sum.inr WIP merge-conflict ⚠️ labelled WIP
26345 mans0954 feat(Analysis/LocallyConvex/Polar): Bipolar theorem awaiting-author merge-conflict t-analysis large-import merge conflict
25775 emilyriehl feat(AlgebraicTopology/SimplicialSet/NerveAdjunction): to Strict Segal 2 awaiting-author merge-conflict t-category-theory infinity-cosmos t-algebraic-topology ❌? infrastructure-related CI failing
25481 kbuzzard chore: refactor Algebra.TensorProduct.rightAlgebra delegated merge-conflict t-algebra merge conflict
26827 pechersky feat(Analysis/Normed/ValuativeRel): helper instance for NormedField merge-conflict t-number-theory t-analysis t-algebra merge conflict
29014 ShreckYe feat(Data/List/Scan): some theorems that relate `scanl` with `foldl` merge-conflict t-data merge conflict
27936 alreadydone feat(Algebra): additivize Dvd and Prime merge-conflict t-algebra merge conflict
30150 imbrem feat(CategoryTheory/Monoidal): to_additive for MonoidalCategory merge-conflict t-meta t-category-theory new-contributor awaiting-zulip large-import awaiting a zulip discussion
26484 peabrainiac feat(Geometry/Diffeology): basics of diffeological spaces merge-conflict t-differential-geometry merge conflict
31388 b-mehta feat(Topology/Order): add unordered versions of topological Rolle's theorem awaiting-author merge-conflict t-analysis tech debt merge conflict
30706 astrainfinita refactor(Analysis/NormedSpace/Exponential): remove the `𝕂` argument from `exp` blocked-by-other-PR t-analysis blocked on another PR
30824 grunweg wip: another smoothness lemma for local frames WIP merge-conflict t-differential-geometry labelled WIP
30322 kckennylau feat(RingTheory): base change of graded algebra awaiting-author merge-conflict t-ring-theory merge conflict
28013 astrainfinita feat: Lindemann-Weierstrass Theorem merge-conflict t-analysis t-algebra merge conflict
31593 Ruben-VandeVelde feat: some lemmas about MonoidAlgebra awaiting-author merge-conflict t-algebra merge conflict
31596 grunweg chore: remove extraneous uses of push_neg WIP merge-conflict labelled WIP
31600 grunweg chore: replace by_cases! with by_cases when the push_neg step does no… WIP merge-conflict labelled WIP
26087 grunweg feat: a `SliceModel` typeclass for models with corners for embedded submanifolds merge-conflict t-differential-geometry failing CI
26240 grunweg perf(CommandLinterLinter): use Substring more merge-conflict RFC t-linter merge conflict
27392 Paul-Lez feat(Tactic/SimpUtils): add simproc finding commands awaiting-author merge-conflict t-meta large-import file-removed failing CI*
29909 Vierkantor feat(CI): add build output to CI workflows merge-conflict CI 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 awaiting-author merge-conflict t-data merge conflict
20648 anthonyde feat: formalize regular expression -> εNFA merge-conflict new-contributor t-computability awaiting-zulip awaiting a zulip discussion
20649 GabinKolly feat(ModelTheory/Graph): prove characterization of the fraisse limit of finite simple graphs WIP merge-conflict t-combinatorics t-logic large-import labelled WIP
20652 jjaassoonn feat: categorical description of center of a ring awaiting-author merge-conflict t-category-theory t-algebra failing CI
20924 tomaz1502 feat(Computability/QueryComplexity): Oracle-based computation merge-conflict t-computability failing CI
21270 GabinKolly feat(ModelTheory/Bundled): first-order embeddings and equivalences from equalities awaiting-author merge-conflict t-logic large-import merge conflict
21447 erdOne feat(AlgebraicGeometry): the split algebraic torus awaiting-author merge-conflict t-algebraic-geometry merge conflict
21616 peabrainiac feat(Topology): concatenating countably many paths awaiting-author merge-conflict t-topology merge conflict
21624 sinhp feat(CategoryTheory): The (closed) monoidal structure on the product category of families of (closed) monoidal categories awaiting-author merge-conflict t-category-theory failing CI
21829 Whysoserioushah feat(LinearAlgebra/TensorProduct/HomTensor): Add TensorProduct of Hom-modules awaiting-author merge-conflict t-algebra merge conflict
21903 yhtq feat: add from/toList between `FreeSemigroup` and `List` with relative theorems merge-conflict awaiting-CI t-algebra new-contributor large-import does not pass CI
22159 shetzl feat: add definition of pushdown automata awaiting-author merge-conflict new-contributor t-computability merge conflict
22231 pechersky feat(Algebra/Valued): `AdicExpansion` initial defns awaiting-author merge-conflict t-topology t-algebra merge conflict
22302 658060 feat: add `CategoryTheory.Topos.Power` awaiting-author merge-conflict t-category-theory new-contributor merge conflict
22314 shetzl feat: add leftmost derivations for context-free grammars awaiting-author merge-conflict new-contributor t-computability merge conflict
22662 plp127 feat: Localization.Away.lift (computably) merge-conflict t-algebra merge conflict
22790 mhk119 feat: Extend `taylor_mean_remainder_lagrange` to `x < x_0` awaiting-author merge-conflict t-analysis new-contributor merge conflict
22861 eric-wieser feat: add the trace of a bilinear form awaiting-author merge-conflict t-algebra merge conflict
22919 plp127 feat(Data/Fintype/Pi): Make `Fintype` instance for `RelHom`s computable awaiting-author merge-conflict t-data merge conflict
22954 eric-wieser feat(RingTheory/Congruence/Hom): copy from GroupTheory merge-conflict t-ring-theory failing CI
23285 AntoineChambert-Loir refactor: directed systems in terms of functors WIP merge-conflict t-category-theory t-algebra large-import labelled WIP
23503 apnelson1 feat(Topology/Instances/ENat): ENat and tsum WIP merge-conflict t-topology large-import labelled WIP
23585 plp127 feat: `Filter.atMax` and `Filter.atMin` WIP merge-conflict t-order labelled WIP
23758 erdOne feat(Topology/Algebra): linearly topologized iff non-archimedean awaiting-author merge-conflict t-topology t-algebra large-import merge conflict
23835 chrisflav feat(Topology): cardinality of connected components is bounded by cardinality of fiber awaiting-author merge-conflict t-topology failing CI
24333 xcloudyunx feat(Combinatorics/SimpleGraph): cycle graph implementation for generic vertex types awaiting-author merge-conflict t-combinatorics new-contributor merge conflict
24540 robertmaxton42 feat(Quiv): add the empty, vertex, point, interval, and walking quivers awaiting-author merge-conflict t-category-theory failing CI
24789 Ruben-VandeVelde chore: move Algebra.Group.Hom.End to Algebra.Ring awaiting-author merge-conflict t-algebra file-removed merge conflict
24850 pechersky feat(Topology/UniformSpace/Ultra): uniform spaces induced by pseudometrics are ultra if system is ultra merge-conflict t-topology merge conflict
25324 eric-wieser feat: more functorial results about DFinsupp awaiting-author merge-conflict t-algebra t-data merge conflict
25500 eric-wieser feat: delaborators for metadata awaiting-author delegated merge-conflict t-meta large-import merge conflict
25585 Paul-Lez feat(Tactic/Linters/DeprecatedSimpLemma): lint for deprecated simp lemmas awaiting-author merge-conflict t-linter failing CI
25739 literandltx feat(NumberTheory/LegendreSymbol): Add sqrt‐of‐residue theorems for p=4k+3 and p=8k+5 awaiting-author merge-conflict t-number-theory new-contributor merge conflict
25760 robin-carlier feat(CategoryTheory/Bicategory): (2,1)-categories and `Pith` awaiting-author merge-conflict t-category-theory failing CI
25905 mans0954 feat(RingTheory/Polynomial/SmallDegreeVieta): polynomial versions of results in Algebra.QuadraticDiscriminant awaiting-author merge-conflict t-ring-theory merge conflict
25974 scholzhannah feat(Topology/Compactness/CompactlyCoherentSpace): compact coherentification (k-ification) merge-conflict t-topology large-import merge conflict
25989 Multramate feat(NumberTheory/EllipticDivisibilitySequence): add elliptic nets awaiting-author merge-conflict t-number-theory merge conflict
26051 Komyyy feat(Mathlib/GroupTheory/SpecificGroups/Alternating): A_n is simple iff n = 3 or 5 ≤ n WIP merge-conflict large-import t-group-theory labelled WIP
26158 upobir feat(NumberTheory/Divisors): add int divisors awaiting-author merge-conflict t-number-theory merge conflict
26292 RemyDegenne feat(MeasureTheory): tightness of the range of a sequence awaiting-author merge-conflict t-measure-probability failing CI
26293 RemyDegenne feat: tightness from convergence of characteristic functions WIP merge-conflict t-measure-probability labelled WIP
26300 igorkhavkine feat(Analysis/Calculus/FDeriv): continuous differentiability from continuous partial derivatives on an open domain in a product space WIP awaiting-author merge-conflict t-analysis new-contributor labelled WIP
26329 Timeroot feat: Definition of `Clone` notations and typeclasses awaiting-author merge-conflict awaiting-CI t-algebra does not pass CI
26340 mans0954 feat(Algebra/Module/NestAlgebra): Nest algebras merge-conflict t-algebra failing CI
26341 mans0954 feat(LinearAlgebra/QuadraticForm/Basis): Free Tensor product of Quadratic Maps WIP merge-conflict t-algebra large-import labelled WIP
26347 mans0954 feat(Data/Finset/RangeDistance): abs_sub_lt_of_mem_finset_range merge-conflict t-data merge conflict
26368 Whysoserioushah feat(RingTheory/TwoSidedIdeal/SpanAsSum): span of set as finsum awaiting-author merge-conflict t-ring-theory merge conflict
26398 ChrisHughes24 feat(ModelTheory): definable functions please-adopt merge-conflict t-logic looking for help
26432 AntoineChambert-Loir feat(Data.Nat.LogFueled): fueled version of `clog` merge-conflict t-data failing CI
26594 metakunt feat(Algebra/Polynomial/ZMod): Add Polynomial.equiv_of_nat_of_polynomial_zmod awaiting-author merge-conflict t-algebra new-contributor merge conflict
26644 kckennylau feat(SetTheory/ZFC): Define the language of sets and state the ZFC axioms awaiting-author merge-conflict t-set-theory merge conflict
26648 eric-wieser chore(TensorProduct): remove more `suppress_compilation`s blocked-by-core-PR merge-conflict t-algebra blocked on another PR
26757 fweth feat(CategoryTheory/Topos): define elementary topos awaiting-author merge-conflict t-category-theory new-contributor failing CI
26803 bjoernkjoshanssen feat: second partial derivatives test awaiting-author merge-conflict t-analysis failing CI
26857 Thmoas-Guan feat(Algebra): define associated graded structure for abelian group awaiting-author merge-conflict t-algebra merge conflict
26914 quangvdao feat(Data/PFunctor/Univariate): more definitions for univariate `PFunctor` merge-conflict t-data merge conflict
26920 yuma-mizuno feat(Tactic.CategoryTheory): add associator inserting tactic WIP merge-conflict t-meta t-category-theory labelled WIP
26983 mans0954 feat(Order/LatticeElements): distributive, standard and neutral elements of a lattice WIP merge-conflict t-order labelled WIP
26990 joelriou feat(CategoryTheory/Abelian): Noetherian objects form a Serre class WIP merge-conflict t-category-theory labelled WIP
27098 Paul-Lez feat(Algebra/Category/ModuleCat/Sheaf/VectorBundle): define vector bundles awaiting-author merge-conflict t-algebra merge conflict
27155 Pjotr5 feat: Shearer's bound on the independence number of triangle free graphs awaiting-author merge-conflict t-combinatorics new-contributor failing CI
27163 pechersky feat(Topology/ValuativeRel): of and to basis of compatible valuations awaiting-author merge-conflict t-number-theory t-topology t-algebra merge conflict
27187 Komyyy feat: `NONote` represents ordinals < ε₀ WIP merge-conflict t-set-theory labelled WIP
27215 kckennylau feat(AlgebraicGeometry): Define the Zariski site on `CommRingCatᵒᵖ` awaiting-author merge-conflict t-algebraic-geometry merge conflict
27245 rirarika feat: multivariate polynomial ring properties about irreducibility awaiting-author merge-conflict t-algebra new-contributor merge conflict
27261 Sebi-Kumar feat(Topology): add definition for subpaths awaiting-author merge-conflict t-topology new-contributor merge conflict
27262 Timeroot feat(Tactic/Bound): bound? for proof scripts awaiting-author merge-conflict t-meta merge conflict
27307 xyzw12345 feat(RingTheory/GradedAlgebra): homogeneous relation awaiting-author merge-conflict t-ring-theory merge conflict
27309 kckennylau feat(CategoryTheory): a presheaf on `CostructuredArrow F d` can be extended to a presheaf on `C` WIP merge-conflict t-category-theory labelled WIP
27321 kckennylau feat(CategoryTheory): Colimit can be computed fiberwise merge-conflict awaiting-CI t-category-theory does not pass CI
27417 PierreQuinton feat: add `SigmaCompleteLattice` awaiting-author merge-conflict t-order merge conflict
27500 Komyyy feat: the Riemann zeta function is meromorphic WIP merge-conflict t-analysis large-import labelled WIP
27534 PierreQuinton feat: a typeclass for `sSup`/`sInf` to be lawful merge-conflict t-order merge conflict
27753 YunkaiZhang233 feat(CategoryTheory): implemented proofs for factorisation categories being equivalent to iterated comma categories in two ways awaiting-author merge-conflict t-category-theory new-contributor merge conflict
27824 ChrisHughes24 feat(Calculus): exists_gt_of_deriv_pos and variants awaiting-author merge-conflict t-analysis merge conflict
27850 fyqing feat: 0-dimensional manifolds are discrete and countable awaiting-author merge-conflict t-differential-geometry new-contributor merge conflict
27973 smmercuri feat: the ring of integers of a `ℤₘ₀`-valued field is compact whenever it is a DVR and the residue field is finite awaiting-author merge-conflict t-algebra large-import merge conflict
28056 grunweg wip: existence of Riemannian metrics WIP merge-conflict t-differential-geometry labelled WIP
28072 kckennylau feat(RingTheory/Valuation): make tactic rw_val_equiv awaiting-author merge-conflict t-ring-theory merge conflict
28124 kckennylau feat(Tactic): Call an arbitrary Simproc merge-conflict t-meta failing CI
28125 nonisomorphiclinearmap feat(Combinatorics): basic definition of simplicial complexes merge-conflict t-combinatorics new-contributor merge conflict
28191 kckennylau feat(Logic): tag Injective, Surjective, and Bijective with fun_prop awaiting-author merge-conflict t-meta merge conflict
28316 eric-wieser feat(Tactic/NormNum): better trace nodes merge-conflict t-meta failing CI
28325 pechersky feat(WithZeroTopology): `locallyCompactSpace_iff_locallyFiniteOrder_units` merge-conflict t-topology t-order large-import failing CI
28349 kckennylau feat(Meta): add notation for naming stacked polynomials awaiting-author merge-conflict t-meta merge conflict
28868 yury-harmonic feat(Positive): add `OfNat` instance merge-conflict t-algebra large-import failing CI
28871 JaafarTanoukhi feat(Combinatorics/Digraph): Tournaments merge-conflict t-combinatorics new-contributor merge conflict
29055 vihdzp feat: `Ordinal.toENat` awaiting-author merge-conflict t-set-theory merge conflict
29108 JonBannon feat(MeasureTheory): add `LInfty.lean` with `Mul` and `const` related results. awaiting-author merge-conflict t-measure-probability merge conflict
29235 yoh-tanimoto feat(Topology/Algebra/Module/ClosedSubmodule): add `mapEquiv`, a variation of `ClosedSubmodule.map` for CLE merge-conflict t-topology merge conflict
29411 llllvvuu feat(LinearAlgebra/Matrix/Rank): rank factorization awaiting-author merge-conflict ⚠️ merge conflict
29500 vihdzp feat: `WellFoundedLT (LowerSet α)` awaiting-author merge-conflict t-order merge conflict
29526 llllvvuu feat: `Multiset.map f` identifies `f` up to permutation merge-conflict t-data merge conflict
29610 llllvvuu feat(LinearAlgebra): define LinearMap.Eigenbasis merge-conflict t-algebra merge conflict
29675 yury-harmonic feat(Wolstenholme): new file help-wanted awaiting-author merge-conflict t-data looking for help
29720 javra feat(CategoryTheory): `TransportEnrichment` and `ForgetEnrichment` as 2-functors WIP merge-conflict t-category-theory labelled WIP
29827 js2357 feat: define two (trivial) ContinuousMulEquivs merge-conflict t-topology FLT large-import failing CI
29947 JaafarTanoukhi feat(Combinatorics/Digraph): Maps merge-conflict t-combinatorics new-contributor merge conflict
29965 RemyDegenne feat(probability): define subtraction of kernels WIP merge-conflict t-measure-probability 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 awaiting-author merge-conflict t-analysis t-measure-probability merge conflict
30042 JovanGerb feat(push): `@[push]` attributes for `∈` in `Set`, `Finset` and `Multiset` awaiting-author merge-conflict t-meta merge conflict
30121 idontgetoutmuch Principal fiber bundle core awaiting-author merge-conflict t-differential-geometry new-contributor merge conflict
30233 Komyyy refactor(Topology/Sequences): generalize seq-compactness lemmas to metrizable space merge-conflict t-topology large-import merge conflict
30355 kckennylau feat(Logic): graded functions merge-conflict t-data merge conflict
30451 kckennylau feat(HomogeneousIdeal): generalize to homogeneous submodule merge-conflict t-ring-theory failing CI
30933 joelriou feat(CategoryTheory): the linearization of a category awaiting-author merge-conflict t-category-theory merge conflict
31008 RemyDegenne refactor: generalize the index of the process in the Doob decomposition WIP merge-conflict t-measure-probability labelled WIP
31102 JOSHCLUNE Require LeanHammer merge-conflict new-contributor failing CI
31194 grunweg feat: add `#check'` command and tactic, which only show explicit arguments awaiting-author merge-conflict t-meta merge conflict
31351 grunweg feat: manifolds with smooth boundary WIP merge-conflict t-differential-geometry labelled WIP
31356 adomani feat: add inspect-like functions merge-conflict t-meta merge conflict
31604 maksym-radziwill feat: analyticity of dslope awaiting-author merge-conflict t-analysis merge conflict
31613 xyzw12345 feat(RepresentationTheory/GroupCohomology): Non-abelian Group Cohomology WIP merge-conflict t-algebra large-import labelled WIP
31738 robertmaxton42 feat: quivers can be represented as functors from the walking quiver awaiting-author merge-conflict t-category-theory failing CI
30083 grunweg feat: local frames in a vector bundle awaiting-author merge-conflict t-differential-geometry failing CI
31587 JovanGerb Lean pr testing 11156 WIP merge-conflict labelled WIP*
21269 658060 feat(CategoryTheory/Topos): basic definitions and results in topos theory WIP awaiting-author merge-conflict t-category-theory new-contributor labelled WIP
22805 ScottCarnahan feat(FieldTheory/Finite): fixed points of Frobenius automorphism WIP merge-conflict t-algebra labelled WIP
23990 robertmaxton42 feat(Types.Colimits): Quot is functorial and colimitEquivQuot is natural awaiting-author merge-conflict t-category-theory new-contributor merge conflict
24690 ScottCarnahan feat(Data.Prod): reverse lexicographic order WIP merge-conflict t-order labelled WIP
24692 ScottCarnahan feat(RingTheory/HahnSeries/Basic): isomorphism of Hahn series induced by order isomorphism WIP merge-conflict t-order labelled WIP
25831 ScottCarnahan feat(RingTheory/HahnSeries): Powers of a binomial WIP merge-conflict t-ring-theory labelled WIP
26156 oliver-butterley feat(MeasureTheory.VectorMeasure): add a definition of total variation for VectorMeasure awaiting-author merge-conflict t-measure-probability new-contributor failing CI
26455 ScottCarnahan feat(LinearAlgebra/RootSystem): API for CartanMatrix WIP merge-conflict t-algebra labelled WIP
26770 Jun2M feat(Combinatorics/Graph): subgraph relations on `Graph` merge-conflict t-combinatorics merge conflict
26804 kckennylau feat(SetTheory): ZFSet is a model of ZFC WIP merge-conflict t-set-theory labelled WIP
26890 robin-carlier feat(CategoryTheory/Monoidal/DayConvolution): more API for `DayFunctor` merge-conflict t-category-theory merge conflict
26348 mans0954 feat(Analysis/LocallyConvex/Prime): the prime map WIP merge-conflict t-analysis labelled WIP
26310 kckennylau feat: binary forms awaiting-author merge-conflict t-algebra merge conflict
26283 kckennylau feat: resultant of polynomials WIP merge-conflict t-algebra labelled WIP
28215 5hv5hvnk feat: strong and Weak connectivity for Digraphs WIP awaiting-author merge-conflict t-combinatorics new-contributor labelled WIP
28970 Whysoserioushah feat(Algebra/Algebra/ReducedNorm): defines reduced norm and trace awaiting-author merge-conflict t-algebra merge conflict
29212 Whysoserioushah feat(Algebra/CrossProductAlgebra/Defs): define Cross Product Algebra awaiting-author merge-conflict t-algebra merge conflict
29281 plp127 doc: `Fin.natAdd_castLEEmb` merge-conflict t-data merge conflict
29514 grunweg feat(CI): use more strict mode WIP merge-conflict CI labelled WIP
29574 JarodAlper feat: regular local rings are domains merge-conflict new-contributor t-ring-theory failing CI
29788 robertmaxton42 feat(Topology): adds bundled continuous maps for sum, sigma, subtype, mapsto, inclusion merge-conflict large-import ⚠️ failing CI
30366 sinhp feat(CategoryTheory): The Preliminaries for Locally Cartesian Closed Categories awaiting-author merge-conflict t-category-theory merge conflict
30855 Ruben-VandeVelde fix: deprecate IsTotal in favour of Std.Total merge-conflict RFC merge conflict
24614 JovanGerb chore: rename field `inf` to `min` in `Lattice` merge-conflict t-order awaiting-zulip failing CI
31148 kex-y feat(Probability): Local and stable properties WIP merge-conflict t-measure-probability brownian labelled WIP
25899 pfaffelh feat(Topology/Compactness/CompactSystem): introduce compact Systems awaiting-author merge-conflict t-topology brownian merge conflict
25902 pfaffelh feat: The finite product of semi-rings (in terms of measure theory) is a semi-ring. awaiting-author merge-conflict t-measure-probability large-import brownian merge conflict
29517 pechersky feat(RingTheory/Torsion): torsion = union of roots of unity awaiting-author merge-conflict t-algebra failing CI
28933 artie2000 chore(Data): correct definition for `single_apply` WIP merge-conflict labelled WIP
24627 pechersky feat(Topology/Algebra/Valued): `IsLinearTopology 𝒪[K] K` and `𝒪[K] 𝒪[K]` awaiting-author merge-conflict t-topology merge conflict
26912 pechersky chore(Algebra/Ring/Subring): simp tag `Subring.smul_def` merge-conflict t-algebra merge conflict
27756 grunweg feat: `Weak(Pseudo)EMetricSpace`, generalises `(Pseudo)EMetricSpace` WIP merge-conflict t-topology carleson labelled WIP
24016 plp127 feat: fine uniformity merge-conflict t-topology merge conflict
26614 Rida-Hamadani feat(SimpleGraph): add more API for `take`/`drop` awaiting-author merge-conflict t-combinatorics failing CI
32095 grunweg chore: fix some explicitVarOfIff linter errors WIP please-adopt merge-conflict looking for help
29982 hrmacbeth feat: new `isolate` tactic awaiting-author merge-conflict t-meta large-import failing CI
31007 kckennylau feat(RingTheory): generalise perfection to monoids merge-conflict ⚠️ failing CI
26138 xroblot Development branch (2) WIP merge-conflict labelled WIP
26436 AntoineChambert-Loir feat(Mathlib/Data/Nat/Prime/Defs): fuel Nat.minFac awaiting-author merge-conflict t-data failing CI
24514 b-mehta chore(Int/GCD): use fuel in xgcd awaiting-author merge-conflict t-data merge conflict
31152 FernandoChu feat(CategoryTheory): regular categories have strong-epi-mono factorisations awaiting-author merge-conflict t-category-theory merge conflict
29934 smmercuri feat(Field/WithAbs): the lift of a ring homomorphism from `WithAbs v` to `WithAbs w` to their completions WIP merge-conflict FLT ⚠️ labelled WIP
29933 smmercuri chore: fix `def` naming isses in `Normed/Field/WithAbs.lean` WIP merge-conflict labelled WIP
31377 CoolRmal feat: a series of smooth functions that converges (locally) uniformly is smooth awaiting-author merge-conflict t-topology new-contributor merge conflict
30860 FormulaRabbit81 feat(Measure): prove the space of probability measures on a compact space is compact WIP merge-conflict ⚠️ labelled WIP
30504 grunweg feat: add custom elaborators for immersions merge-conflict t-differential-geometry failing CI
27557 chrisflav feat(RingTheory/KrullDimension): dimension of `R / (x)` for a nonzerodivisor merge-conflict large-import t-ring-theory failing CI
25848 joelriou feat/refactor: redefinition of homology + derived categories WIP merge-conflict t-category-theory t-topology large-import labelled WIP
30989 kckennylau feat(RingTheory): Teichmuller map awaiting-author merge-conflict ⚠️ merge conflict
31950 callesonne feat(CategoryTheory/Product/Basic): make `Hom` into a 1-field structure WIP merge-conflict t-category-theory labelled WIP
26464 joelriou feat(LinearAlgebra): generators of pi tensor products awaiting-author merge-conflict t-algebra file-removed merge conflict
31110 bryangingechen ci: don't delete merged branches awaiting-author merge-conflict CI merge conflict
27364 101damnations feat(RepresentationTheory/Homological/GroupCohomology): cohomology of finite cyclic groups awaiting-author merge-conflict t-algebra merge conflict
28291 vasnesterov feat(Tactic): tactic for computing asymptotics of real functions WIP merge-conflict t-meta t-analysis labelled WIP
31603 alreadydone chore(Algebra): make `RatFunc` an abbrev awaiting-author merge-conflict RFC t-algebra merge conflict
31242 plp127 feat: express filter as supremum of principal filter and free filter awaiting-author merge-conflict t-order merge conflict
30927 callesonne feat(Bicategory/Yoneda): add the yoneda pseudofunctor merge-conflict ⚠️ failing CI
31597 grunweg chore(AtLocation): allow throwing a warning when no progress is being made awaiting-author merge-conflict t-meta merge conflict
30439 plp127 feat: `norm_num` extension for `IsSquare` on `Nat`, `Int`, `Rat` awaiting-author merge-conflict t-meta merge conflict
30525 515801431 feat(Mathlib/Combinatorics/Enumerative/Polya): Add Polya Counting awaiting-author merge-conflict t-combinatorics new-contributor merge conflict
24441 MrSumato feat(Data/List): add Lyndon-Schutzenberger theorem on list commutativity awaiting-author merge-conflict new-contributor t-data merge conflict
28057 plp127 feat(SuccOrder): simp lemma to refold `Order.succ` and `Order.pred` awaiting-author merge-conflict t-order merge conflict
31362 BeibeiX0 feat(partitions): generalized pentagonal numbers awaiting-author merge-conflict t-combinatorics new-contributor merge conflict
24434 joelriou feat(CategoryTheory): effectiveness of descent WIP merge-conflict t-category-theory labelled WIP
25841 mitchell-horner feat(Combinatorics/SimpleGraph): prove the Kővári–Sós–Turán theorem WIP merge-conflict t-combinatorics labelled WIP
26332 Timeroot feat(ModelTheory/Definability): TermDefinable functions merge-conflict t-logic merge conflict
30881 FlAmmmmING feat(RingTheory/PowerSeries/Schroder.lean): Define the generating function for large and small Schroder number merge-conflict new-contributor ⚠️ merge conflict
30962 WangYiran01 feat(Combinatorics/Enumerative): add lattice path lemmas and counts merge-conflict t-combinatorics new-contributor failing CI
29354 themathqueen refactor(Algebra/Algebra/Equiv): allow for non-unital `AlgEquiv` awaiting-author merge-conflict t-algebra merge conflict
27918 kim-em wip: refactor WithBot/WithTop as structures merge-conflict file-removed failing CI
30119 Ruben-VandeVelde feat: WithTop/Bot.mapD awaiting-author merge-conflict t-order merge conflict
28708 sjh227 feat(Data): edit DoublyStochastic, add Stochastic to matrix awaiting-author merge-conflict new-contributor t-data merge conflict
28613 espottesmith feat(Combinatorics): define undirected hypergraphs merge-conflict t-combinatorics new-contributor failing CI
25803 erdOne feat: taylor expansion of `1 / z ^ r` awaiting-author merge-conflict t-analysis merge conflict
30620 plp127 feat: copy LE and LT on preorder and partial order awaiting-author merge-conflict t-order merge conflict
30853 JovanGerb feat(LinearAlgebra/AffineSpace/Simplex): `CoeFun` instance for `Simplex` awaiting-author merge-conflict t-euclidean-geometry merge conflict
30144 alreadydone feat(Data/Nat): kernel reducible binaryRec merge-conflict t-algebra t-data failing CI
30122 xroblot Development branch (1) WIP merge-conflict labelled WIP
29508 zhuyizheng feat(MeasureTheory): FTC and integration by parts for absolutely continuous functions awaiting-author merge-conflict t-measure-probability new-contributor merge conflict
29558 Thmoas-Guan feat(Algebra): definition of global dimension awaiting-author merge-conflict t-ring-theory merge conflict
30666 erdOne feat(NumberTheory): every number field has a ramified prime awaiting-author t-number-theory t-algebra failing CI
31325 joelriou feat(AlgebraicTopology): a computable monoidal functor instance for `hoFunctor` WIP merge-conflict t-algebraic-topology labelled WIP
32401 ADedecker feat: monotonicity of D^n(U) in n and in U as CLMs merge-conflict t-analysis merge conflict
13057 alreadydone feat(NumberTheory): characterize elliptic divisibility sequences blocked-by-other-PR merge-conflict t-number-theory t-algebra blocked on another PR
12879 grunweg feat: port ge_or_gt linter from mathlib3 blocked-by-other-PR merge-conflict t-linter tech debt blocked on another PR
10842 mcdoll chore: simplify proofs using new positivity extensions and tests WIP blocked-by-other-PR merge-conflict blocked on another PR
7564 shuxuezhuyi feat(Topology/Algebra/Order): extend strictly monotone function on `Ioo` to homeomorphism on `Icc` blocked-by-other-PR merge-conflict t-topology blocked on another PR
8364 thorimur feat: `refine?` blocked-by-other-PR merge-conflict t-meta blocked on another PR
7565 shuxuezhuyi feat(Topology/Algebra/Order): extend homeomorphism of `Ioo` to `Icc` blocked-by-other-PR merge-conflict t-topology t-order blocked on another PR
9154 FR-vdash-bot feat: `npow` / `nsmul` / `Nat.cast`/ `zpow` / `zsmul` implemented using `Nat.binaryRec` blocked-by-other-PR awaiting-author merge-conflict t-algebra blocked on another PR
7861 shuxuezhuyi feat(Geometry/Hyperbolic/UpperHalfPlane): instance IsometricSMul PSL(2, ℝ) ℍ blocked-by-other-PR merge-conflict t-euclidean-geometry blocked on another PR
13782 alreadydone feat(EllipticCurve): ZSMul formula in terms of division polynomials blocked-by-other-PR merge-conflict t-number-theory t-algebraic-geometry t-algebra blocked on another PR
14242 js2357 feat: Prove equivalence of `isDedekindDomain` and `isDedekindDomainDvr` blocked-by-other-PR merge-conflict t-algebra new-contributor blocked on another PR
16215 adomasbaliuka feat(Tactic/Linter): lint unwanted unicode blocked-by-other-PR merge-conflict t-linter blocked on another PR
16887 metinersin feat(ModelTheory/Complexity): define conjunctive and disjunctive formulas blocked-by-other-PR merge-conflict t-logic new-contributor blocked on another PR
16888 metinersin feat(ModelTheory/Complexity): Define conjunctive and disjunctive normal forms blocked-by-other-PR merge-conflict t-logic new-contributor blocked on another PR
16889 metinersin feat(ModelTheory/Complexity): Normal forms blocked-by-other-PR merge-conflict t-logic new-contributor blocked on another PR
13965 pechersky feat(Data/DigitExpansion): reals via digit expansion are complete blocked-by-other-PR merge-conflict t-data blocked on another PR
17519 grunweg feat: the `metrisableSpace` linter blocked-by-other-PR merge-conflict t-linter blocked on another PR*
12750 Command-Master feat: define Gray code blocked-by-other-PR awaiting-author merge-conflict new-contributor t-data blocked on another PR
13514 madvorak feat(Computability/ContextFreeGrammar): closure under union blocked-by-other-PR merge-conflict t-computability blocked on another PR
17518 grunweg feat: lint on declarations mentioning `Invertible` or `Unique` blocked-by-other-PR merge-conflict t-linter awaiting-zulip blocked on another PR*
18716 jjaassoonn feat(Algebra/Module/GradedModule): quotient and subgrading WIP blocked-by-other-PR merge-conflict awaiting-CI t-algebra blocked on another PR
17593 FR-vdash-bot chore(Algebra/Order/GroupWithZero/Unbundled): deprecate useless lemmas, use `ZeroLEOneClass` blocked-by-other-PR merge-conflict t-algebra t-order blocked on another PR
17624 FR-vdash-bot feat(Algebra/Order/GroupWithZero/Unbundled): generalize lemmas blocked-by-other-PR merge-conflict t-algebra t-order blocked on another PR
17515 FR-vdash-bot perf: do not need `simp low` now blocked-by-other-PR merge-conflict t-algebra blocked on another PR
19281 Vierkantor chore(Algebra/{MonoidAlgebra,Polynomial}): algebra structure in `Basic.lean` blocked-by-other-PR merge-conflict t-algebra blocked on another PR
19621 Command-Master feat: Multiplicity and prime-adic valuation of derivations blocked-by-other-PR merge-conflict t-algebra large-import blocked on another PR
18262 joelriou feat(Algebra/Category/ModuleCat/Presheaf): exterior powers of presheaves of modules WIP blocked-by-other-PR merge-conflict t-category-theory t-algebra blocked on another PR
15269 kkytola feat: Add ENNReal.floor blocked-by-other-PR awaiting-author merge-conflict t-algebra t-order blocked on another PR
19462 joelriou feat(AlgebraicGeometry): étale sheafification WIP blocked-by-other-PR merge-conflict t-algebraic-geometry blocked on another PR
15720 znssong feat(SimpleGraph): The Bondy-Chvátal theorem blocked-by-other-PR merge-conflict t-combinatorics new-contributor blocked on another PR
12670 trivial1711 feat: completion of a nonarchimedean multiplicative group blocked-by-other-PR merge-conflict t-topology t-algebra blocked on another PR
20248 peabrainiac feat(Topology/Compactness): first-countable locally path-connected spaces are delta-generated blocked-by-other-PR awaiting-author merge-conflict t-topology new-contributor large-import blocked on another PR
14060 YnirPaz feat(SetTheory/Ordinal/Clubs): define club sets and prove basic properties blocked-by-other-PR merge-conflict t-logic new-contributor blocked on another PR
16000 YaelDillies feat: Croot-Sisask Almost Periodicity blocked-by-other-PR t-combinatorics t-analysis blocked on another PR
22340 sinhp feat(CategoryTheory): Locally Cartesian Closed Categories (Beck-Chevalley Conditions) WIP blocked-by-other-PR merge-conflict t-category-theory large-import blocked on another PR
23145 joneugster feat(CategoryTheory/Enriched/Limits): add IsConicalLimits blocked-by-other-PR merge-conflict t-category-theory infinity-cosmos blocked on another PR
20222 eric-wieser feat: generalize lemmas about derivatives blocked-by-other-PR merge-conflict t-analysis blocked on another PR
22321 sinhp feat(CategoryTheory): Locally Cartesian Closed Categories (Definition) blocked-by-other-PR merge-conflict t-category-theory large-import blocked on another PR
22319 sinhp feat(CategoryTheory): Locally Cartesian Closed Categories (Sections Right Adjoint) blocked-by-other-PR merge-conflict t-category-theory large-import blocked on another PR
24010 grunweg feat(Counterexamples): a non-negative function, not a.e. zero, with vanishing lowe… WIP blocked-by-other-PR please-adopt t-measure-probability blocked on another PR
21238 joneugster feat(Cache): enable partial cache in downstream projects blocked-by-other-PR merge-conflict t-meta CI blocked on another PR
21842 joneugster refactor(Cache): use module name for file hash instead of non-resolved file path blocked-by-other-PR merge-conflict t-meta CI blocked on another PR*
19467 quangvdao feat(MvPolynomial/Equiv): Add `MvPolynomial.finSuccEquivNth` blocked-by-other-PR merge-conflict t-algebra blocked on another PR
24549 grunweg feat: define embedded submanifolds, attempt 1 WIP blocked-by-other-PR merge-conflict t-differential-geometry blocked on another PR
11003 thorimur chore: migrate to `tfae` block tactic WIP blocked-by-other-PR merge-conflict t-meta blocked on another PR
16186 joneugster chore: use emoji-variant-selector `\uFE0F` for emojis ✅️,❌️,💥️,🟡️ blocked-by-other-PR awaiting-author merge-conflict t-linter blocked on another PR
15654 TpmKranz feat(Computability): language-preserving maps between NFA and RE blocked-by-other-PR merge-conflict new-contributor t-computability awaiting-zulip blocked on another PR
24550 grunweg feat: define `SliceModel` typeclass for models with corners for embedded submanifolds WIP blocked-by-other-PR merge-conflict t-differential-geometry blocked on another PR
18755 FR-vdash-bot refactor: deprecate `LinearIsometryClass` blocked-by-other-PR merge-conflict t-analysis t-algebra blocked on another PR
25912 BoltonBailey feat: add simp lemmas for trig functions on `π * 2⁻¹` blocked-by-other-PR awaiting-author t-analysis blocked on another PR
18771 joelriou feat(LinearAlgebra/ExteriorPower): exterior powers of free modules are free WIP blocked-by-other-PR merge-conflict t-algebra blocked on another PR
18662 joelriou feat(LinearAlgebra/ExteriorPower): generators of the exterior powers WIP blocked-by-other-PR merge-conflict t-algebra blocked on another PR
18735 joelriou feat(Algebra/Module): presentation of the exterior power WIP blocked-by-other-PR merge-conflict t-algebra blocked on another PR
26395 winstonyin feat: $C^1$ vector fields on compact manifolds define global flows WIP blocked-by-other-PR merge-conflict t-differential-geometry blocked on another PR
26465 joelriou feat(Algebra/Module): presentation of the `PiTensorProduct` blocked-by-other-PR merge-conflict t-algebra file-removed blocked on another PR
26467 joelriou feat(LinearAlgebra): the tensor product of a finite family of free modules is free WIP blocked-by-other-PR merge-conflict t-algebra file-removed blocked on another PR
10654 smorel394 feat(LinearAlgebra/{ExteriorPower,LinearIndependent,TensorPower}): define the exterior powers of a module and prove some of their basic properties blocked-by-other-PR please-adopt merge-conflict t-algebra large-import blocked on another PR
26987 joelriou chore: deprecating module LinearAlgebra.PiTensorProduct WIP blocked-by-other-PR merge-conflict t-algebra blocked on another PR
24668 robertmaxton42 feat(LinearAlgebra): add inductive principle for the free product of algebras blocked-by-other-PR merge-conflict t-algebra blocked on another PR
25486 VTrelat feat(SetTheory/ZFC/Integers): define integers in ZFC blocked-by-other-PR merge-conflict new-contributor t-set-theory blocked on another PR
25484 VTrelat feat(SetTheory/ZFC/Booleans): define Boolean algebra in ZFC blocked-by-other-PR merge-conflict new-contributor t-set-theory blocked on another PR
22909 AntoineChambert-Loir feat(RingTheory/Pure): pure submodules blocked-by-other-PR merge-conflict t-ring-theory blocked on another PR
22908 AntoineChambert-Loir feat(RingTheory/Finiteness/Small): tensor product of the system of small submodules blocked-by-other-PR merge-conflict t-ring-theory blocked on another PR
27897 grunweg feat: check indentation of doc-strings blocked-by-other-PR merge-conflict awaiting-CI t-linter blocked on another PR
27996 grunweg feat: check indentation in doc-strings, medium version WIP blocked-by-other-PR merge-conflict ⚠️ blocked on another PR
7873 astrainfinita perf: reorder `extends` and change instance priority in algebra hierarchy blocked-by-other-PR merge-conflict t-algebra slow-typeclass-synthesis blocked on another PR
28502 gilesgshaw feat(Logic/Basic): avoid unnecessary uses of choice blocked-by-other-PR awaiting-author merge-conflict t-logic new-contributor blocked on another PR
27198 robin-carlier feat(CategoryTheory/Monoidal/DayConvolution): the Yoneda embedding is monoidal (for Day convolution) blocked-by-other-PR merge-conflict t-category-theory file-removed blocked on another PR
19582 yu-yama feat(GroupExtension/Abelian): define `OfMulDistribMulAction.equivH2` blocked-by-other-PR merge-conflict t-algebra new-contributor blocked on another PR
25488 VTrelat feat(SetTheory/ZFC/Rationals): define rationals in ZFC blocked-by-other-PR merge-conflict new-contributor t-set-theory blocked on another PR
28787 alreadydone feat(Counterexamples): a domain whose ring of differences is not a domain blocked-by-other-PR merge-conflict t-algebra large-import blocked on another PR
28686 mitchell-horner feat(Combinatorics/SimpleGraph): prove the Erdős-Stone theorem WIP blocked-by-other-PR merge-conflict t-combinatorics blocked on another PR
28687 mitchell-horner feat(Combinatorics/SimpleGraph): prove the Erdős-Stone-Simonovits theorem WIP blocked-by-other-PR merge-conflict t-combinatorics blocked on another PR
28689 mitchell-horner feat(Combinatorics/SimpleGraph): prove well-known corollaries of the Erdős-Stone-Simonovits theorem WIP blocked-by-other-PR merge-conflict t-combinatorics blocked on another PR
26952 robin-carlier feat(CategoryTheory/DayConvolution): monoid objects internal to day convolutions blocked-by-other-PR merge-conflict t-category-theory blocked on another PR
27133 robin-carlier feat(CategoryTheory/Monoidal/DayConvolution): `C ⊛⥤ V` is monoidal closed when `V` is blocked-by-other-PR merge-conflict t-category-theory blocked on another PR
27151 robin-carlier feat(CategoryTheory/Monoidal/DayConvolution): `C ⊛⥤ V` is braided/symmetric when `C` and `V` are braided/symmetric blocked-by-other-PR merge-conflict t-category-theory blocked on another PR
27175 robin-carlier feat(CategoryTheory/Monoidal/DayConvolution): `LawfulDayConvolutionMonoidalCategoryStruct.ι C V D` is monoidal when the target is `C ⊛⥤ V` blocked-by-other-PR merge-conflict t-category-theory blocked on another PR
26413 michaellee94 feat(Analysis/ODE/MaximalSolution): Existence of maximal solutions for ODE meeting Picard-Lindelöf conditions blocked-by-other-PR awaiting-author merge-conflict t-analysis new-contributor blocked on another PR
25741 robin-carlier feat(AlgebraicTopology/SimplexCategory/SimplicialObject): definitions of simplicial objects by generators and relation blocked-by-other-PR merge-conflict t-category-theory large-import t-algebraic-topology blocked on another PR
27707 FLDutchmann feat(NumberTheory/SelbergSieve): define Selberg's weights and prove basic results. blocked-by-other-PR merge-conflict t-number-theory t-analysis blocked on another PR
27898 grunweg feat: check indentation of doc-strings, basic version blocked-by-other-PR merge-conflict t-linter blocked on another PR
29077 grunweg feat(Manifold/Instances/Icc): golf smoothness proof using immersions blocked-by-other-PR merge-conflict ⚠️ blocked on another PR
28804 grunweg feat: a few more tactic linters blocked-by-other-PR merge-conflict t-meta blocked on another PR
29243 yoh-tanimoto feat(Analysis/InnerProductSpace/Projection/Submodule): add `sup_orthogonal` for `ClosedSubmodules` blocked-by-other-PR merge-conflict ⚠️ blocked on another PR
29251 yoh-tanimoto feat(Analysis/InnerProductSpace/): define standard subspaces of a complex Hilbert space blocked-by-other-PR merge-conflict ⚠️ blocked on another PR
27950 alreadydone feat(MonoidAlgebra): criteria for `single` to be a unit, irreducible or prime WIP merge-conflict t-algebra labelled WIP
28067 grunweg Docstring enumerations blocked-by-other-PR merge-conflict blocked on another PR
26304 Raph-DG feat(AlgebraicGeometry): Definition of algebraic cycles blocked-by-other-PR merge-conflict RFC t-algebraic-geometry blocked on another PR
27391 robin-carlier feat(CategoryTheory/Limits/Shapes/Pullback/Categorical): pseudofunctoriality structure of categorical pullback squares blocked-by-other-PR merge-conflict t-category-theory blocked on another PR
27432 robin-carlier feat(CategoryTheory/Limits/Shapes/Pullback/Categorical): pseudofunctoriality of categorical pulback squares blocked-by-other-PR merge-conflict t-category-theory blocked on another PR
27481 robin-carlier feat(CategoryTheory/Limits/Shapes/Pullback/Categorical): adjunctions and equivalences of categorical pullback squares blocked-by-other-PR merge-conflict t-category-theory large-import blocked on another PR
27686 robin-carlier feat(CategoryTheory/Limits/Shapes/Pullback/Categorical/Square): more API for `CatPullbackSquare` blocked-by-other-PR merge-conflict t-category-theory large-import blocked on another PR
27687 robin-carlier feat(CategoryTheory/Limits/Shapes/Pullback/Categorical): squares equivalent to a `CatPullbackSquare` blocked-by-other-PR merge-conflict t-category-theory large-import blocked on another PR
27688 robin-carlier feat(CategoryTheory/Limits/Shapes/Pullback/Categorical): coherence statement for `CatPullbackSquare.inverse` blocked-by-other-PR merge-conflict t-category-theory large-import blocked on another PR
27689 robin-carlier feat(CategoryTheory/Limits/Shapes/Pullback/Categorical): horizontal pasting calculus for `CatPullbackSquare` blocked-by-other-PR merge-conflict t-category-theory large-import blocked on another PR
27690 robin-carlier feat(CategoryTheory/Limits/Shapes/Pullback/Categorical): vertical pasting calculus for `CatPullbackSquare` blocked-by-other-PR merge-conflict t-category-theory large-import blocked on another PR
27740 robin-carlier feat(CategoryTheory/Limits/Shapes/Pullback/Categorical): pasting calculus for `CategoricalPullback` blocked-by-other-PR merge-conflict t-category-theory large-import blocked on another PR
26579 robin-carlier feat(CategoryTheory/Limits/Pullbacks/Categorical/CatCospanTransform): equivalences of categorical cospans blocked-by-other-PR merge-conflict t-category-theory large-import blocked on another PR
27634 agjftucker fix(Analysis/Calculus/Implicit): consistently rename {`map`, `fun`, `function`} to `fun` blocked-by-other-PR merge-conflict t-analysis blocked on another PR
27366 101damnations feat(RepresentationTheory/Homological/GroupCohomology/Hilbert90): add Hilbert 90 for cyclic groups blocked-by-other-PR merge-conflict t-algebra large-import blocked on another PR
28245 robin-carlier feat(CategoryTheory/Bicategory/NaturalTransformation/Icon): strict associativity and unitality of icon composition WIP blocked-by-other-PR merge-conflict awaiting-CI t-category-theory large-import blocked on another PR
25740 robin-carlier feat(AlgebraicTopology/SimplexCategory/GeneratorsRelations): `SimplexCategoryGenRel.toSimplexCategory` is an equivalence blocked-by-other-PR merge-conflict large-import t-algebraic-topology blocked on another PR
26886 pechersky feat(NumberTheory/Padics/ValuativeRel): ValuativeRel ℚ_[p] WIP blocked-by-other-PR merge-conflict t-number-theory t-analysis t-algebra blocked on another PR
27314 pechersky feat(TopologyValued): `Valued` based on a range topology blocked-by-other-PR merge-conflict t-topology blocked on another PR
16553 grunweg WIP: tinkering with orientable manifolds WIP blocked-by-other-PR merge-conflict t-differential-geometry blocked on another PR
28328 pechersky chore(Topology/Valued): golf using local finite order of WithZeroTopology blocked-by-other-PR merge-conflict t-number-theory t-topology t-algebra large-import blocked on another PR
29282 Jlh18 feat(CategoryTheory): HasColimits instance on Grpd blocked-by-other-PR merge-conflict new-contributor ⚠️ blocked on another PR
29387 mans0954 feat(Analysis/LocallyConvex/WeakSpace): toWeakSpace_closedAbsConvexHull_eq blocked-by-other-PR merge-conflict t-analysis blocked on another PR
30610 grunweg feat: yet another lemma about differentiability of parametric integrals blocked-by-other-PR t-analysis blocked on another PR
28152 Sebi-Kumar feat(AlgebraicTopology): characterize simply connectedness in terms of loops blocked-by-other-PR merge-conflict new-contributor t-algebraic-topology blocked on another PR
28246 Sebi-Kumar feat(AlgebraicTopology/FundamentalGroupoid): the n-sphere is simply connected for n > 1 blocked-by-other-PR merge-conflict new-contributor t-algebraic-topology blocked on another PR
28700 Timeroot feat(ModelTheory): Set.Definable is transitive blocked-by-other-PR merge-conflict t-logic large-import blocked on another PR
30462 grunweg Everything I wanted about immersions blocked-by-other-PR merge-conflict blocked on another PR
30303 franv314 chore(Topology/Instances): add deprecated module blocked-by-other-PR merge-conflict new-contributor blocked on another PR
30900 vihdzp feat: run-length encoding blocked-by-other-PR merge-conflict t-data large-import blocked on another PR
30579 smmercuri feat : `v.adicCompletionIntegers K` is compact when `K` is a number field WIP blocked-by-other-PR merge-conflict ⚠️ blocked on another PR
29774 Raph-DG feat(AlgebraicGeometry): Order of vanishing of elements of the function field of locally noetherian, integral schemes blocked-by-other-PR merge-conflict file-removed ⚠️ blocked on another PR
25834 Rida-Hamadani feat(SimpleGraph): girth-diameter inequality WIP blocked-by-other-PR merge-conflict t-combinatorics blocked on another PR
25903 pfaffelh feat(MeasureTheory): finite unions of sets in a semi-ring (in terms of measure theory) form a ring blocked-by-other-PR merge-conflict t-measure-probability large-import blocked on another PR
28685 mitchell-horner feat(Combinatorics/SimpleGraph): prove the minimal-degree version of the Erdős-Stone theorem WIP blocked-by-other-PR merge-conflict t-combinatorics blocked on another PR
30258 imbrem feat(CategoryTheory/Monoidal): to_additive for proofs using `monoidal` blocked-by-other-PR merge-conflict new-contributor large-import ⚠️ blocked on another PR
30260 imbrem feat(CategoryTheory/Monoidal): added CocartesianMonoidalCategory blocked-by-other-PR merge-conflict new-contributor large-import ⚠️ blocked on another PR
26973 peabrainiac feat(Geometry/Diffeology): diffeologies generated from sets of plots blocked-by-other-PR merge-conflict t-differential-geometry blocked on another PR
27274 peabrainiac feat(Geometry/Diffeology): continuous diffeologies & D-topology-lemmas blocked-by-other-PR merge-conflict t-differential-geometry blocked on another PR
27953 CoolRmal feat(ProbabilityTheory): Conditional Jensen's Inequality blocked-by-other-PR merge-conflict t-measure-probability new-contributor blocked on another PR
30399 kckennylau feat(RingTheory): make HomogeneousLocalization.map take a graded ring hom blocked-by-other-PR merge-conflict ⚠️ blocked on another PR
30357 grunweg chore: golf using custom elaborators blocked-by-other-PR merge-conflict t-differential-geometry awaiting-bench blocked on another PR
5863 eric-wieser feat: add elaborators for concrete matrices help-wanted blocked-by-other-PR merge-conflict t-meta blocked on another PR
18876 GabinKolly feat(ModelTheory/Fraisse): add proof that Fraïssé limits exist blocked-by-other-PR merge-conflict t-logic blocked on another PR
20051 Timeroot feat: `Clone` and some instances blocked-by-other-PR awaiting-author merge-conflict t-algebra blocked on another PR
20956 tomaz1502 feat(Computability/QueryComplexity/Sort.lean): Formalization of upper bound of queries for merge sort blocked-by-other-PR merge-conflict t-computability blocked on another PR
21277 GabinKolly feat(ModelTheory/PartialEquiv): Define the mapping of a self-partialEquiv through an embedding blocked-by-other-PR merge-conflict t-logic blocked on another PR
22232 pechersky feat(Algebra/Valued): `AdicExpansion.apprUpto` blocked-by-other-PR merge-conflict t-topology blocked on another PR
22233 pechersky feat(Algebra/Valued): `AdicExpansion.evalAt` blocked-by-other-PR merge-conflict t-topology blocked on another PR
23460 Timeroot feat: Definition of `Clone` blocked-by-other-PR merge-conflict t-algebra blocked on another PR
26061 kckennylau (WIP) feat(AlgebraicGeometry): define Projective Space WIP blocked-by-other-PR merge-conflict t-algebraic-geometry blocked on another PR
26160 oliver-butterley feat(MeasureTheory.VectorMeasure): add several lemmas which characterize variation blocked-by-other-PR merge-conflict t-measure-probability new-contributor blocked on another PR
26165 oliver-butterley feat(MeasureTheory.VectorMeasure): add lemma which shows that variation of a `ℝ≥0∞` VectorMeasure is equal to itself blocked-by-other-PR merge-conflict t-measure-probability new-contributor blocked on another PR
26399 ChrisHughes24 refactor(ModelTheory): tidy up proof of Ax-Grothendieck with definable functions blocked-by-other-PR merge-conflict t-logic blocked on another PR
26858 Thmoas-Guan feat(Algebra): Define the associated graded ring to filtered ring blocked-by-other-PR merge-conflict t-algebra blocked on another PR
26859 Thmoas-Guan feat(Algebra): Define associated graded algebra blocked-by-other-PR merge-conflict t-algebra blocked on another PR
26860 Thmoas-Guan feat(Algebra): Define associated graded module blocked-by-other-PR merge-conflict t-algebra blocked on another PR
26861 Thmoas-Guan feat(Algebra): define filtered add group hom blocked-by-other-PR merge-conflict t-algebra blocked on another PR
26862 Thmoas-Guan feat(Algebra): define filtered ring homomorphism blocked-by-other-PR merge-conflict t-algebra blocked on another PR
26863 Thmoas-Guan feat(Algebra): define filtered alghom blocked-by-other-PR merge-conflict t-algebra blocked on another PR
26867 Thmoas-Guan feat(Algebra): filtered module hom blocked-by-other-PR merge-conflict t-algebra blocked on another PR
26868 Thmoas-Guan feat(Algebra): associated graded exact of exact and strict blocked-by-other-PR merge-conflict t-algebra blocked on another PR
26869 Thmoas-Guan feat(Algebra): exact of associated graded exact blocked-by-other-PR merge-conflict t-algebra blocked on another PR
26872 faenuccio chore(RingTheory/Valuation/RankOne): modify the definition of Valuation.RankOne using its range rather than its codomain blocked-by-other-PR awaiting-author merge-conflict t-algebra blocked on another PR
26942 pechersky feat(RingTheory/Valuation/ValueGroupIso): isomorphism of value groups when compatible blocked-by-other-PR merge-conflict t-order t-ring-theory blocked on another PR
28208 Sebi-Kumar feat(Topology): add the definition `foldTrans` to concatenate finite sequences of paths blocked-by-other-PR merge-conflict t-topology new-contributor blocked on another PR
28499 yoh-tanimoto feat(MeasureTheory/VectorMeasure): add integral of a vector-valued function against a vector measure blocked-by-other-PR merge-conflict t-measure-probability blocked on another PR
28530 nonisomorphiclinearmap feat(Combinatorics/SimplicialComplex/Topology): add standard simplices and geometric realisation (colimit + functoriality) blocked-by-other-PR merge-conflict t-combinatorics new-contributor blocked on another PR
29425 pechersky feat(NumberTheory/Padics/Torsion): `HasEnoughRootsOfUnity ℤ_[p] (p - 1)` blocked-by-other-PR awaiting-author merge-conflict t-ring-theory blocked on another PR
30001 vihdzp feat: concept generated by set of objects/attributes blocked-by-other-PR merge-conflict t-order blocked on another PR
30077 agjftucker feat(Analysis/Calculus/ImplicitFunOfBivariate): define implicitFunOfBivariate blocked-by-other-PR merge-conflict t-analysis blocked on another PR
30312 kckennylau feat(RingTheory): define graded ring homomorphisms blocked-by-other-PR merge-conflict t-ring-theory blocked on another PR
30334 kckennylau feat(RingTheory): define maps of homogeneous ideals blocked-by-other-PR merge-conflict t-ring-theory blocked on another PR
30365 kckennylau feat(RingTheory): define R-linear graded algebra homomorphism blocked-by-other-PR merge-conflict ⚠️ blocked on another PR
30367 kckennylau feat(Data): define grading-preserving isomorphisms blocked-by-other-PR merge-conflict t-data blocked on another PR
30379 kckennylau feat(RingTheory): isomorphism of graded rings blocked-by-other-PR merge-conflict ⚠️ blocked on another PR
30985 erdOne feat(AlgbraicGeometry), `Hom(-, X)` commutes with inverse limits for schemes of finite presentation blocked-by-other-PR merge-conflict t-algebraic-geometry large-import blocked on another PR
31083 joelriou feat(CategoryTheory): properties of objects for pseudofunctors to Cat WIP blocked-by-other-PR merge-conflict t-category-theory blocked on another PR
31580 grunweg feat: towards `ContMDiff` support in fun_prop WIP blocked-by-other-PR merge-conflict t-meta t-differential-geometry blocked on another PR
19475 YaelDillies feat: group markings WIP blocked-by-other-PR t-algebra blocked on another PR
30339 grunweg feat: extend a tangent vector for a locally smooth vector field blocked-by-other-PR merge-conflict t-differential-geometry blocked on another PR
31338 grunweg chore: move Pretrivialization, Trivialization to the Bundle namespace blocked-by-other-PR merge-conflict t-differential-geometry blocked on another PR
31339 grunweg Movelemma blocked-by-other-PR merge-conflict blocked on another PR
12087 JADekker feat: complete API for K-Lindelöf spaces blocked-by-other-PR please-adopt merge-conflict t-topology ??? blocked on another PR
17471 joelriou feat(Algebra/ModuleCat/Differentials/Sheaf): the sheaf of relative differentials WIP blocked-by-other-PR merge-conflict t-category-theory t-algebraic-geometry large-import blocked on another PR
18784 erdOne feat(AlgebraicGeometry): use `addMorphismPropertyInstances` blocked-by-other-PR merge-conflict t-algebraic-geometry blocked on another PR
19607 madvorak feat: block matrices are totally unimodular WIP blocked-by-other-PR merge-conflict ⚠️ blocked on another PR
25906 pfaffelh feat(Topology/Compactness/CompactSystem): closed and compact square cylinders form a compact system blocked-by-other-PR merge-conflict t-topology 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 blocked-by-other-PR merge-conflict t-topology blocked on another PR
26168 oliver-butterley feat(MeasureTheory.VectorMeasure): variation defined as a supremum is equal to variation defined using the Hahn-Jordan decomposition blocked-by-other-PR merge-conflict t-measure-probability new-contributor blocked on another PR
29792 robertmaxton42 feat(RelCWComplex): a (relative, concrete) CW complex is the colimit of its skeleta blocked-by-other-PR merge-conflict large-import ⚠️ 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 blocked-by-other-PR merge-conflict large-import ⚠️ blocked on another PR
28718 imbrem feat: class for chosen finite coproducts blocked-by-other-PR awaiting-author merge-conflict t-category-theory new-contributor blocked on another PR
30352 kckennylau feat(RingTheory): Homogeneous localization of tensor product WIP blocked-by-other-PR merge-conflict ⚠️ blocked on another PR
31411 CoolRmal feat: a convex lower-semicontinuous function is the supremum of a sequence of affine functions in a separable space blocked-by-other-PR merge-conflict t-analysis new-contributor blocked on another PR
31513 FLDutchmann feat(Tactic): `polynomial` tactic blocked-by-other-PR merge-conflict t-meta blocked on another PR
27694 grunweg feat: Gram-Schmidt orthonormalisation preserves continuity of sections blocked-by-other-PR merge-conflict t-differential-geometry blocked on another PR
27025 grunweg feat: Gram-Schmidt procedure on smooth vector bundles yields smooth sections blocked-by-other-PR merge-conflict t-differential-geometry blocked on another PR
29777 yuanyi-350 feat(Functional Analysis): closed Range Theorem WIP blocked-by-other-PR awaiting-author t-analysis new-contributor blocked on another PR
30831 chrisflav feat(AlgebraicGeometry): the fpqc topology blocked-by-other-PR t-algebraic-geometry blocked on another PR
28248 YaelDillies feat: binomial random variables blocked-by-other-PR t-measure-probability blocked on another PR
30463 grunweg feat: support products and disjoint unions in the differential geometry elaborators blocked-by-other-PR merge-conflict t-meta t-differential-geometry blocked on another PR
29449 mitchell-horner feat(Combinatorics/SimpleGraph): add Turán density related theorems blocked-by-other-PR t-combinatorics blocked on another PR
31332 sinhp feat(CategoryTheory): Exponentiable morphisms blocked-by-other-PR t-category-theory blocked on another PR
31729 thorimur chore: log on theorem type signature in unused instances in type linters blocked-by-other-PR merge-conflict large-import blocked on another PR
32157 peabrainiac feat(Analysis/Calculus): Hadamard's lemma blocked-by-other-PR t-analysis blocked on another PR
26966 vihdzp feat: the Dedekind–MacNeille completion blocked-by-other-PR awaiting-author merge-conflict t-order blocked on another PR
23177 faenuccio feat: more lemmas about ordered groups with zero WIP blocked-by-other-PR awaiting-CI t-order blocked on another PR
31018 joelriou feat(CategoryTheory): the κ-accessible category of κ-directed posets WIP blocked-by-other-PR merge-conflict t-category-theory blocked on another PR
29996 vihdzp chore(Order/Concept): `IsIntent` and `IsExtent` blocked-by-other-PR t-order blocked on another PR
30375 sinhp feat(CategoryTheory): Basics of Locally Cartesian Closed Categories WIP blocked-by-other-PR t-category-theory blocked on another PR
30373 sinhp feat(CategoryTheory) : LCCC sections (constructing right adjoint to `Over.ChosenPullback.pullback`) blocked-by-other-PR t-category-theory blocked on another PR
28244 robin-carlier feat(CategoryTheory/Bicategory/NaturalTransformation): Icons WIP blocked-by-other-PR merge-conflict awaiting-CI t-category-theory large-import blocked on another PR
31919 alreadydone feat(RingTheory): integrally closed subring of a field is intersection of valuation subrings blocked-by-other-PR t-ring-theory blocked on another PR
31135 kckennylau feat(RingTheory): is localization iff is localization on saturation blocked-by-other-PR merge-conflict ⚠️ blocked on another PR
27980 smmercuri feat: dimensions of completions at infinite place extensions blocked-by-other-PR merge-conflict t-number-theory FLT large-import blocked on another PR
31350 grunweg feat: (unoriented) bordism groups WIP blocked-by-other-PR merge-conflict t-differential-geometry blocked on another PR
29274 Jlh18 feat(CategoryTheory): HasLimits instance on Grpd blocked-by-other-PR t-category-theory file-removed blocked on another PR
27493 themathqueen feat(RingTheory/Coalgebra): define Frobenius algebra blocked-by-other-PR awaiting-author t-ring-theory blocked on another PR
30129 vlad902 feat(SimpleGraph): define and prove basic theory of vertex covers blocked-by-other-PR t-combinatorics blocked on another PR
31892 jsm28 feat(Geometry/Euclidean/Sphere/PolePolar): poles and polars blocked-by-other-PR t-euclidean-geometry blocked on another PR
31893 jsm28 feat(Geometry/Euclidean/Sphere/Tangent): characterize `tangentsFrom` blocked-by-other-PR t-euclidean-geometry blocked on another PR
30204 yonggyuchoimath feat(Algebra/Category/Ring/EqualizerPushout): add effectiveEpi_of_faithfullyFlat in CommRingCatᵒᵖ blocked-by-other-PR ⚠️ blocked on another PR
27706 xroblot feat(RingTheory/Localization/AtPrime): inertia degree and ramification index are preserved by localization blocked-by-other-PR t-ring-theory blocked on another PR
31364 YaelDillies feat: binomial random graphs blocked-by-other-PR t-combinatorics t-measure-probability blocked on another PR
32027 alreadydone feat(Counterexamples): invertible module not isomorphic to any ideal blocked-by-other-PR merge-conflict t-ring-theory ❌? blocked on another PR
26291 RemyDegenne feat(Probability): Cameron-Martin theorem WIP blocked-by-other-PR merge-conflict t-measure-probability blocked on another PR*
32147 EtienneC30 feat: independence of Gaussian random variables blocked-by-other-PR t-measure-probability brownian blocked on another PR
32269 EtienneC30 feat: introduce Gaussian processes blocked-by-other-PR t-measure-probability brownian blocked on another PR
31187 loefflerd feat(NumberTheory/LSeries): Define the L-series of a modular form WIP blocked-by-other-PR t-number-theory blocked on another PR
28683 Thmoas-Guan feat(RingTheory): regular local ring is domain WIP blocked-by-other-PR t-ring-theory blocked on another PR
30551 smmercuri feat: dimension formulae for infinite places above WIP blocked-by-other-PR merge-conflict ⚠️ blocked on another PR
31885 CoolRmal feat: Integrable if UI + convergence in measure blocked-by-other-PR t-measure-probability brownian blocked on another PR
32081 Thmoas-Guan feat(RingTheory/Homology): `Ext` over Noetherian ring finitely generated blocked-by-other-PR t-category-theory t-algebra blocked on another PR
29533 Thmoas-Guan feat(Algebra): maximal Cohen Macaulay module blocked-by-other-PR merge-conflict large-import ⚠️ blocked on another PR*
29557 Thmoas-Guan feat(Algebra): finite projective dimension of regular blocked-by-other-PR large-import ⚠️ blocked on another PR
32058 Thmoas-Guan feat(Algebra): category version Baer criterion blocked-by-other-PR awaiting-author t-category-theory t-algebra blocked on another PR
28684 Thmoas-Guan feat(RingTheory): definition of regular ring blocked-by-other-PR t-ring-theory blocked on another PR
29701 Thmoas-Guan feat(Algebra/RingTheory): polynomial over regular ring blocked-by-other-PR t-ring-theory blocked on another PR
31222 Thmoas-Guan feat(Algebra): `Hom` commute with flat base change blocked-by-other-PR large-import ⚠️ blocked on another PR
31768 Thmoas-Guan feat(Homology): `Ext` commute with ulift functor blocked-by-other-PR merge-conflict t-category-theory t-algebra ❌? blocked on another PR
30532 Thmoas-Guan feat(Homology) : `Ext` commute with flat base change blocked-by-other-PR merge-conflict t-category-theory large-import blocked on another PR
32410 callesonne feat(Bicategory/FunctorCategory/Pseudo): Add evaluation pseudofunctor WIP blocked-by-other-PR t-category-theory blocked on another PR
31046 Thmoas-Guan feat(Homology) : compatibility of map between `Ext` blocked-by-other-PR merge-conflict t-category-theory blocked on another PR
31697 Thmoas-Guan feat(Homology): bijection between `Ext` blocked-by-other-PR merge-conflict t-category-theory t-algebra blocked on another PR
32481 ADedecker feat: add `PolynormableSpace.banach_steinhaus` blocked-by-other-PR t-analysis blocked on another PR
31113 515801431 feat(Mathlib/Combinatorics/Enumerative/Polya.lean): Add additional theorem in `Polya.lean` blocked-by-other-PR merge-conflict t-combinatorics new-contributor blocked on another PR
29000 JovanGerb feat(Tactic/Push): add basic tags and tests blocked-by-other-PR merge-conflict ⚠️ blocked on another PR
32125 SnirBroshi feat(SimpleGraph/Walks/Subwalks): `p₁.IsSubwalk p₂ ↔ p₁.darts <:+: p₂.darts` and similar theorems blocked-by-other-PR t-combinatorics blocked on another PR
31851 Thmoas-Guan feat(Algebra/Homology): Injective dimension in linear equiv blocked-by-other-PR merge-conflict t-algebra ❌? blocked on another PR
31884 Thmoas-Guan feat(RingTheory): definition of Gorenstein local ring blocked-by-other-PR merge-conflict ❌? ⚠️ 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
32035 Thmoas-Guan feat(RingTheory): localization of Gorenstein local ring blocked-by-other-PR merge-conflict ❌? ⚠️ blocked on another PR
32098 Thmoas-Guan feat(RingTheory): injective dimension of quotSMulTop blocked-by-other-PR merge-conflict ❌? ⚠️ blocked on another PR
32171 Thmoas-Guan feat(RingTheory): polynomial over Gorenstein ring is Gorenstein blocked-by-other-PR merge-conflict large-import t-ring-theory ❌? blocked on another PR
31644 Thmoas-Guan feat(Algebra): projective dimension of quotient regular sequence blocked-by-other-PR awaiting-author t-ring-theory blocked on another PR
30931 Thmoas-Guan feat(RingTheory): Gorenstein local ring is Cohen Macaulay blocked-by-other-PR merge-conflict large-import ❌? ⚠️ blocked on another PR
32418 Thmoas-Guan feat(RingTheory): Gorenstein local ring is Cohen--Macaulay local ring of type 1 blocked-by-other-PR merge-conflict ❌? ⚠️ blocked on another PR
26377 Whysoserioushah feat(RingTheory/SimpleRing/TensorProduct): tensor product of a simple algebra and a central simple algebra is simple blocked-by-other-PR t-ring-theory blocked on another PR
18551 joelriou feat(AlgebraicGeometry): the algebraic De Rham complex WIP blocked-by-other-PR merge-conflict t-algebraic-geometry t-algebra blocked on another PR
26214 Thmoas-Guan feat(Algebra): definition of depth blocked-by-other-PR t-algebra large-import blocked on another PR
26215 Thmoas-Guan feat(Algebra): Auslander–Buchsbaum theorem blocked-by-other-PR t-algebra large-import blocked on another PR
26216 Thmoas-Guan feat(Algebra): depth of QuotSMulTop blocked-by-other-PR t-algebra large-import blocked on another PR
26217 Thmoas-Guan feat(Algebra): Ischebeck theorem blocked-by-other-PR t-algebra large-import blocked on another PR
26218 Thmoas-Guan feat(Algebra): definition of cohen macaulay blocked-by-other-PR t-algebra large-import blocked on another PR
26245 Thmoas-Guan feat(Algebra): cohen macaulay local ring is catenary WIP blocked-by-other-PR t-algebra large-import blocked on another PR
26957 Thmoas-Guan feat(Algebra): unmixed thm of Cohen-Macaulay ring blocked-by-other-PR t-algebra large-import blocked on another PR
31754 dagurtomas feat(Topology/Category): light profinite sets are injective objects blocked-by-other-PR t-category-theory t-topology blocked on another PR
28905 grunweg feat: immersions are locally embeddings blocked-by-other-PR merge-conflict ⚠️ blocked on another PR
32674 CoolRmal feat: a Gdelta subset of a Baire space is Baire. blocked-by-other-PR t-topology large-import blocked on another PR
32334 EtienneC30 feat: independence of Gaussian processes blocked-by-other-PR t-measure-probability brownian blocked on another PR
23040 grunweg feat: define immersions and smooth embeddings in infinite dimensions WIP blocked-by-other-PR merge-conflict t-differential-geometry blocked on another PR
32677 grunweg chore: generalise `contMDiffOn_writtenInExtend_iff` WIP blocked-by-other-PR t-differential-geometry blocked on another PR
31981 jsm28 feat(Geometry/Euclidean/Incenter): `tangentSet` and `tangentsFrom` lemmas blocked-by-other-PR t-euclidean-geometry blocked on another PR
32278 jsm28 feat(Geometry/Euclidean/Incenter): excenters on sides of faces blocked-by-other-PR t-euclidean-geometry blocked on another PR
30847 joelriou feat(CategoryTheory/Presentable): the representation theorem WIP blocked-by-other-PR merge-conflict t-category-theory blocked on another PR
32643 vihdzp feat: cardinality of Hahn series inverse blocked-by-other-PR merge-conflict t-ring-theory blocked on another PR
32648 vihdzp feat: subfield of Hahn series bounded by a cardinal blocked-by-other-PR merge-conflict ⚠️ blocked on another PR
32144 EtienneC30 feat: add a predicate HasGaussianLaw blocked-by-other-PR t-measure-probability brownian blocked on another PR
30817 joelriou feat(CategoryTheory): `κ`-continuous presheaves WIP blocked-by-other-PR t-category-theory blocked on another PR
31749 YaelDillies refactor: make `LinearOrderedCommMonoidWithZero`s cancellative blocked-by-other-PR t-algebra large-import file-removed blocked on another PR
30185 alreadydone feat(MathlibTest): kernel reduction of nsmul on elliptic curve over ZMod blocked-by-other-PR merge-conflict t-number-theory t-algebraic-geometry t-algebra blocked on another PR
30799 YaelDillies refactor: unify the two versions of `pow_eq_one_iff` blocked-by-other-PR t-algebra large-import file-removed blocked on another PR
32546 anishrajeev feat(ModelTheory): Define and characterize the type space blocked-by-other-PR t-logic new-contributor large-import blocked on another PR
32751 dagurtomas chore(CategoryTheory): module depreactions for #32746 blocked-by-other-PR blocked on another PR
32619 dagurtomas feat(CategoryTheory): the category of type-valued functors has images blocked-by-other-PR t-category-theory blocked on another PR
32021 jsm28 feat(Geometry/Euclidean/Altitude): `map` and `restrict` lemmas blocked-by-other-PR t-euclidean-geometry blocked on another PR
32270 jsm28 feat(Geometry/Euclidean/Incenter): `map` and `restrict` lemmas blocked-by-other-PR t-euclidean-geometry blocked on another PR
32085 dagurtomas feat(CategoryTheory): sheaf categories are regular epi categories blocked-by-other-PR merge-conflict t-category-theory blocked on another PR
30982 jsm28 feat(Geometry/Euclidean/Angle/Incenter): angle bisection and the incenter blocked-by-other-PR t-euclidean-geometry blocked on another PR
32294 jsm28 feat(Geometry/Euclidean/Angle/Incenter): distance from second intersection with circumcircle blocked-by-other-PR t-euclidean-geometry blocked on another PR
32627 dagurtomas feat(Condensed): the functor from light profinite sets preserves effective epimorphisms blocked-by-other-PR merge-conflict ⚠️ blocked on another PR
32757 AntoineChambert-Loir feat(LinearAlgebra/Transvection): the determinant of a transvection is equal to 1. blocked-by-other-PR large-import ⚠️ blocked on another PR
28865 grunweg feat: a map is smooth iff its post-composition with an immersion is WIP blocked-by-other-PR merge-conflict t-differential-geometry blocked on another PR
32609 PrParadoxy feat(LinearAlgebra/PiTensorProduct): Relation between nested tensor products and tensor products indexed by dependent sums blocked-by-other-PR new-contributor ⚠️ blocked on another PR
29819 mcdoll feat(Analysis/Distribution): tempered distributions WIP blocked-by-other-PR merge-conflict t-analysis blocked on another PR
29534 Thmoas-Guan feat(Algebra): global dimension of regular local ring blocked-by-other-PR merge-conflict large-import ⚠️ blocked on another PR
29699 Thmoas-Guan feat(Algebra/RingTheory): global dimension of regular ring blocked-by-other-PR merge-conflict large-import ⚠️ blocked on another PR
29703 Thmoas-Guan feat(Algebra/RingTheory): Hilbert's Syzygy theorem (projective version) blocked-by-other-PR merge-conflict large-import ⚠️ blocked on another PR
29796 Thmoas-Guan feat(RingTheory): regular of finite global dimension blocked-by-other-PR merge-conflict large-import ⚠️ blocked on another PR
29802 Thmoas-Guan feat(Algebra/RingTheory): Auslander–Buchsbaum–Serre criterion and its corollaries blocked-by-other-PR merge-conflict large-import ⚠️ blocked on another PR
30811 yonggyuchoimath feat(AlgebraicGeometry.EffectiveEpi): effective epimorphisms in schemes blocked-by-other-PR ⚠️ blocked on another PR
31999 Thmoas-Guan feat(RingTheory): global dimension equals the supremum over localizations blocked-by-other-PR awaiting-author merge-conflict ⚠️ blocked on another PR
32305 faenuccio feat: define Sobolev Spaces WIP blocked-by-other-PR merge-conflict t-analysis large-import blocked on another PR
32780 Hagb feat(RingTheory/MvPolynomial/MonomialOrder): generalize some `IsRegular` hypotheses to `∈ nonZeroDivisors` blocked-by-other-PR large-import ⚠️ blocked on another PR
32211 ADedecker feat: inclusion from `ContDiffMapSupportedIn` to `TestFunction` is a topological embedding blocked-by-other-PR t-analysis blocked on another PR
32266 joelriou feat(AlgebraicTopology): finite simplicial sets are `ℵ₀`-presentable, WIP blocked-by-other-PR merge-conflict t-algebraic-geometry blocked on another PR
32251 joelriou feat(AlgebraicTopology): binary products of finite simplicial sets are finite WIP blocked-by-other-PR merge-conflict t-algebraic-topology blocked on another PR
30329 luigi-massacci feat(Analysis/Distribution/TestFunction): integrating against a measure as a continuous linear map on test functions blocked-by-other-PR merge-conflict ⚠️ blocked on another PR*
30327 luigi-massacci feat(Analysis/Distribution/TestFunction): add characterizations of continuity for linear maps on test functions blocked-by-other-PR merge-conflict ⚠️ blocked on another PR
30255 luigi-massacci feat(Analysis/Distribution/ContDiffMapSupportedIn): specialize singleton seminorm family for D_K^n when n finite blocked-by-other-PR merge-conflict ⚠️ blocked on another PR
30253 luigi-massacci feat(Analysis/Distribution/ContDiffMapSupportedIn): Add a wrapper for iteratedFDeriv on the type of bundled smooth compactly supported maps blocked-by-other-PR ⚠️ blocked on another PR
31809 ADedecker feat: differentiation of test function as a CLM blocked-by-other-PR t-analysis blocked on another PR
25273 YaelDillies refactor: make `MonoidAlgebra` into a one-field structure WIP blocked-by-other-PR t-algebra large-import blocked on another PR
32260 jsm28 feat(Geometry/Euclidean/Angle/Oriented/Affine): oriented angle bisection and halving unoriented angles blocked-by-other-PR t-euclidean-geometry blocked on another PR
32282 jsm28 feat(Geometry/Euclidean/Angle/Incenter): unoriented angle bisection blocked-by-other-PR t-euclidean-geometry blocked on another PR
32295 jsm28 feat(Archive/Imo/Imo2024Q4): IMO 2024 Q4 blocked-by-other-PR IMO blocked on another PR
32105 joelriou feat(CategoryTheory): computing Ext-groups using an injective resolution WIP blocked-by-other-PR t-category-theory large-import blocked on another PR
32816 joelriou feat(CategoryTheory): computing Ext-groups using a projective resolution WIP blocked-by-other-PR t-category-theory large-import blocked on another PR
29203 Hagb feat(RingTheory/MvPolynomial/Groebner): add Gröbner basis WIP awaiting-author merge-conflict t-ring-theory labelled WIP
29764 ScottCarnahan feat(Algebra/Vertex): API up to residue products (WIP) blocked-by-other-PR merge-conflict t-algebra ❌? blocked on another PR
32701 sgouezel feat: Prokhorov theorem blocked-by-other-PR merge-conflict t-measure-probability blocked on another PR
30658 grunweg chore: rebase and continuation of #26926 (more spacing fixes) blocked-by-other-PR merge-conflict large-import blocked on another PR
32534 erdOne feat(AlgebraicGeometry): affine Zariski's main theorem WIP blocked-by-other-PR t-ring-theory blocked on another PR
30563 YaelDillies chore(Algebra): replace `NoZeroSMulDivisors` with `Module.IsTorsionFree` WIP merge-conflict t-algebra large-import labelled WIP
32840 joelriou chore(CategoryTheory): remove the old Ext API blocked-by-other-PR t-category-theory large-import file-removed blocked on another PR
32829 Hagb feat(Data/Finsupp/MonomialOrder): weaken `IsOrderedCancelAddMonoid` to `IsOrderedAddMonoid` blocked-by-other-PR ⚠️ blocked on another PR