Skip to content

Pull requests: leanprover-community/mathlib4

New pull request New
2,356 Open 35,222 Closed
2,356 Open 35,222 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/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 awaiting-CI This PR does not pass CI yet. This label is automatically removed once it does. 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…
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 t-combinatorics Combinatorics
#38179 opened Apr 17, 2026 by wwylele Collaborator Loading…
17
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…
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…
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…
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…
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
feat: add coercion lemmas for PartialEquiv.transEquiv and Equiv.transPartialEquiv t-logic Logic (model theory, etc)
#38166 opened Apr 17, 2026 by scholzhannah Collaborator Loading…
1
perf: no_expose for |x| awaiting-CI This PR does not pass CI yet. This label is automatically removed once it does. large-import Automatically added label for PRs with a significant increase in transitive imports
#38165 opened Apr 17, 2026 by JovanGerb Contributor Loading…
5
feat: add IsCompact.isVonNBounded t-topology Topological spaces, uniform spaces, metric spaces, filters
#38164 opened Apr 17, 2026 by ADedecker Member Loading…
1
feat(AlgebraicTopology): strong anodyne extensions respects isomorphisms blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) t-algebraic-topology Algebraic topology
#38163 opened Apr 17, 2026 by joelriou Contributor Loading…
1 task
2
fix: wrong set-builder syntax in the definition of CompactConvergenceCLM t-topology Topological spaces, uniform spaces, metric spaces, filters
#38161 opened Apr 17, 2026 by ADedecker Member Loading…
1
chore: remove some backward.proofsInPublic
#38159 opened Apr 17, 2026 by jcommelin Member Loading…
1
Illustration of a weird behaviour t-topology Topological spaces, uniform spaces, metric spaces, filters
#38158 opened Apr 17, 2026 by ADedecker Member • Draft
1
ProTip! Filter pull requests by the default branch with base:master.