Skip to content

Pull requests: leanprover-community/mathlib4

New pull request New
2,362 Open 35,223 Closed
2,362 Open 35,223 Closed
Author
Filter by author
Loading
Label
Filter by label
Loading
Use alt + click/return to exclude labels
or ⇧ + click/return for logical OR
Projects
Filter by project
Loading
Milestones
Filter by milestone
Loading
Reviews
Filter by reviews
No reviews Review required Approved review Changes requested
Assignee
Filter by who’s assigned
Assigned to nobody Loading
Sort
Sort by
Newest Oldest Most commented Least commented Recently updated Least recently updated Best match
Most reactions
👍 👎 😄 🎉 😕 ❤️ 🚀 👀

Pull requests list

feat(Order/ConditionallyCompleteLattice): ConditionallyCompleteSemiLatticeInf help-wanted The author needs attention to resolve issues t-order Order theory
#38192 opened Apr 18, 2026 by Jun2M Collaborator • Draft
2
refactor: deprecate Mathlib.LinearAlgebra.FreeModule.StrongRankCondition awaiting-bench This PR needs to be benchmarked before merging t-ring-theory Ring theory
#38191 opened Apr 17, 2026 by artie2000 Collaborator Loading…
5
refactor(Topology/Sion): use a dense and continuous completion to generalize the statements blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot)
#38190 opened Apr 17, 2026 by AntoineChambert-Loir Collaborator Loading…
1 task
3
feat: simplify proof of IsAdjoinRootMonic.mkOfAdjoinEqTop' t-ring-theory Ring theory
#38189 opened Apr 17, 2026 by artie2000 Collaborator Loading…
1
feat(RingTheory/Ideal/Over): image of primeCompl under a surjective algebraMap t-algebra Algebra (groups, rings, fields, etc) t-ring-theory Ring theory
#38188 opened Apr 17, 2026 by tb65536 Contributor Loading…
1
perf(RingTheory/Ideal/Quotient/Defs): clean up Ring instances again t-ring-theory Ring theory
#38187 opened Apr 17, 2026 by JovanGerb Contributor Loading…
5
feat(RingTheory/QuasiFinite/Basic): Localizations of the fiber are finite over the residue field t-algebra Algebra (groups, rings, fields, etc) t-ring-theory Ring theory
#38186 opened Apr 17, 2026 by tb65536 Contributor Loading…
1
feat(Order/Partition): operations over Frame t-order Order theory
#38185 opened Apr 17, 2026 by Jun2M Collaborator Loading…
1
chore(Algebra/Algebra/Tower): make IsScalarTower.ofAlgHom an alias of Algebra.algHom t-algebra Algebra (groups, rings, fields, etc) t-ring-theory Ring theory
#38184 opened Apr 17, 2026 by tb65536 Contributor Loading…
1
feat(NumberTheory/Height/NumberField): results on heights over the rational numbers t-number-theory Number theory (also use t-algebra or t-analysis to specialize)
#38183 opened Apr 17, 2026 by MichaelStollBayreuth Contributor Loading…
@tb65536
1
feat(RingTheory/Spectrum/Prime/Noetherian): rank of an Artinian ring over a field t-algebra Algebra (groups, rings, fields, etc) t-ring-theory Ring theory
#38182 opened Apr 17, 2026 by tb65536 Contributor Loading…
2
feat(CategoryTheory/Sites): Over.post F preserves one-hypercovers if F does t-category-theory Category theory
#38181 opened Apr 17, 2026 by chrisflav Member Loading…
1
chore(CategoryTheory/Limits): limit properties of MorphismProperty.Under t-category-theory Category theory
#38180 opened Apr 17, 2026 by chrisflav Member Loading…
1
feat(Combinatorics): Pentagonal numbers maintainer-merge A reviewer has approved the changed; awaiting maintainer approval. t-combinatorics Combinatorics
#38179 opened Apr 17, 2026 by wwylele Collaborator Loading…
29
chore(Topology): redefine TopologicalSpace.Opens.mapMapIso using OrderIso.equivalence t-topology Topological spaces, uniform spaces, metric spaces, filters
#38178 opened Apr 17, 2026 by Brian-Nugent Collaborator Loading…
1
chore(RingTheory/Localization): mirror tensor product compatibilities and golf t-ring-theory Ring theory
#38177 opened Apr 17, 2026 by chrisflav Member Loading…
@riccardobrasca
1
feat(RingTheory): local isomorphisms blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) t-ring-theory Ring theory
#38176 opened Apr 17, 2026 by chrisflav Member Loading…
1 task
2
feat: add UniqueFactorizationMonoid.pow_dvd_pow_iff_dvd t-ring-theory Ring theory
#38175 opened Apr 17, 2026 by riccardobrasca Member Loading…
@jcommelin
1
chore(CategoryTheory/EpiMono): use to_dual
#38173 opened Apr 17, 2026 by JovanGerb Contributor Loading…
1
feat(AlgebraicTopology/SimplicialSet): Mulstruct.mulOne and oneMul t-algebraic-topology Algebraic topology
#38172 opened Apr 17, 2026 by joelriou Contributor Loading…
@robin-carlier
1
feat(Analysis/Calculus/Deriv): add deriv_const_mul_id' new-contributor This PR was made by a contributor with at most 5 merged PRs. Welcome to the community! t-analysis Analysis (normed *, calculus)
#38171 opened Apr 17, 2026 by emlis42 Loading…
4
feat(Algebra/Module/FinitePresentation) : Finitely Presented Module Lemma new-contributor This PR was made by a contributor with at most 5 merged PRs. Welcome to the community! t-algebra Algebra (groups, rings, fields, etc)
#38170 opened Apr 17, 2026 by maddycrim Collaborator Loading…
10
chore(GroupTheory/Finiteness): make Subgroup.FG a class t-algebra Algebra (groups, rings, fields, etc) t-group-theory Group theory
#38169 opened Apr 17, 2026 by tb65536 Contributor Loading…
@riccardobrasca
1
feat: if E is finite dimensional, E →L[𝕜] F has the product topology blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot)
#38168 opened Apr 17, 2026 by ADedecker Member Loading…
1 task
2
chore: bump toolchain to v4.30.0-rc2 dependency-bump This PR bumps the version of an upstream dependency (but not toolchain).
#38167 opened Apr 17, 2026 by Garmelon Contributor Loading…
2
ProTip! Exclude everything labeled bug with -label:bug.