Skip to content

Pull requests: leanprover-community/mathlib4

New pull request New
2,584 Open 37,029 Closed
2,584 Open 37,029 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

chore: update Mathlib dependencies 2026-06-04 auto-merge-after-CI Please do not add manually. Requests for a bot to merge automatically once CI is done. dependency-bump This PR bumps the version of an upstream dependency (but not toolchain).
#40240 opened Jun 4, 2026 by mathlib-update-dependencies Bot Loading…
1
feat: add NumberField.Units.finrank_eq t-number-theory Number theory (also use t-algebra or t-analysis to specialize)
#40239 opened Jun 4, 2026 by riccardobrasca Member Loading…
1
feat: add norm_zpow t-ring-theory Ring theory
#40238 opened Jun 4, 2026 by riccardobrasca Member Loading…
1
fix(scripts): add_deprecations.sh generates additive aliases for @[to_additive] decls awaiting-author A reviewer has asked the author a question or requested changes. CI Modifies the continuous integration setup or other automation LLM-generated PRs with substantial input from LLMs - review accordingly new-contributor This PR was made by a contributor with at most 5 merged PRs. Welcome to the community!
#40237 opened Jun 4, 2026 by syedjafri06193 Loading…
1
4
feat(AlgebraicTopology/SimplicialSet): any simplicial set is the colimit of its monogenous subcomplexes t-algebraic-topology Algebraic topology
#40236 opened Jun 4, 2026 by joelriou Contributor Loading…
1
refactor(Analysis/Convex): use the new convexity concepts t-convex-geometry Affine geometry, cones, simplices WIP Work in progress
#40235 opened Jun 4, 2026 by YaelDillies Contributor Loading…
1 task done
2
fix: label parsing in the check_title workflow CI Modifies the continuous integration setup or other automation
#40234 opened Jun 4, 2026 by grunweg Contributor Loading…
1
ci: split build job so post-build chain overlaps test+lint CI Modifies the continuous integration setup or other automation LLM-generated PRs with substantial input from LLMs - review accordingly
#40233 opened Jun 4, 2026 by bryangingechen Contributor • Draft
2
feat: add zeta_sub_one_dvd_intCast_iff and related declarations
#40232 opened Jun 4, 2026 by riccardobrasca Member Loading…
1
feat(Algebra/Category): pushforward of quasi-coherent sheafs t-category-theory Category theory
#40231 opened Jun 4, 2026 by chrisflav Member Loading…
1
chore: clean up backward.privateInPublic around d₂₃ t-algebra Algebra (groups, rings, fields, etc) tech debt Tracking cross-cutting technical debt, see e.g. the "Technical debt counters" stream on zulip
#40228 opened Jun 4, 2026 by thorimur Contributor Loading…
11
chore: replace _aux with Aux in defs with no other underscores awaiting-author A reviewer has asked the author a question or requested changes. awaiting-CI This PR does not pass CI yet. This label is automatically removed once it does.
#40227 opened Jun 4, 2026 by thorimur Contributor Loading…
11
feat(Analysis/CStarAlgebra/ApproximateUnit): pure 1 is an increasing approx unit easy < 20s of review time. See the lifecycle page for guidelines. t-analysis Analysis (normed *, calculus)
#40226 opened Jun 4, 2026 by themathqueen Collaborator Loading…
1
feat(RingTheory/LaurentSeries): leibniz product rule for derivative awaiting-author A reviewer has asked the author a question or requested changes. LLM-generated PRs with substantial input from LLMs - review accordingly new-contributor This PR was made by a contributor with at most 5 merged PRs. Welcome to the community! t-ring-theory Ring theory
#40225 opened Jun 4, 2026 by localparty Loading…
5
feat(Tactic/Group): strengthen the group tactic and add tests new-contributor This PR was made by a contributor with at most 5 merged PRs. Welcome to the community! t-meta Tactics, attributes or user commands WIP Work in progress
#40224 opened Jun 4, 2026 by AlexBrodbelt Collaborator Loading…
4
chore: replace (by exact occurences awaiting-CI This PR does not pass CI yet. This label is automatically removed once it does.
#40223 opened Jun 4, 2026 by felixpernegger Contributor • Draft
3
chore: reduce imports
#40222 opened Jun 4, 2026 by JovanGerb Contributor • Draft
8
feat: add Monoid.End.equiv t-algebra Algebra (groups, rings, fields, etc)
#40221 opened Jun 4, 2026 by riccardobrasca Member Loading…
2
feat: add prime_units_mul and variants t-algebra Algebra (groups, rings, fields, etc)
#40220 opened Jun 4, 2026 by riccardobrasca Member Loading…
1
feat: add LinearIndependent.update t-algebra Algebra (groups, rings, fields, etc)
#40219 opened Jun 4, 2026 by riccardobrasca Member Loading…
1
doc(RingTheory/DedekindDomain/LinearDisjoint): fix typos in the module docstring documentation Improvements or additions to documentation t-ring-theory Ring theory
#40218 opened Jun 4, 2026 by mbkybky Collaborator Loading…
2
chore(Data/{FunLike/SetLike}): unprime coe_injective' awaiting-CI This PR does not pass CI yet. This label is automatically removed once it does. t-data Data (lists, quotients, numbers, etc)
#40215 opened Jun 4, 2026 by YaelDillies Contributor Loading…
@Vierkantor
1
chore: omega to lia replacements that require unfolding min/max
#40214 opened Jun 4, 2026 by chenson2018 Contributor • Draft
1
feat(Topology/MetricSpace): the L^1 direct sum of metric spaces t-topology Topological spaces, uniform spaces, metric spaces, filters
#40212 opened Jun 4, 2026 by YaelDillies Contributor Loading…
1 task done
6
chore(Data/Finsupp/Order): add Finsupp.support_add_eq' for canonically ordered Finsupps new-contributor This PR was made by a contributor with at most 5 merged PRs. Welcome to the community! t-data Data (lists, quotients, numbers, etc)
#40210 opened Jun 4, 2026 by Yu-Misaka Collaborator Loading…
@faenuccio
12
ProTip! no:milestone will show everything without a milestone.