Skip to content

Pull requests: leanprover-community/mathlib4

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
Assignee
Filter by who’s assigned
Assigned to nobody Loading
Sort

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…
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…
feat: add norm_zpow t-ring-theory Ring theory
#40238 opened Jun 4, 2026 by riccardobrasca Member Loading…
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…
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
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…
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
feat(Algebra/Category): pushforward of quasi-coherent sheafs t-category-theory Category theory
#40231 opened Jun 4, 2026 by chrisflav Member Loading…
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…
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…
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…
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…
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…
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
chore: reduce imports
#40222 opened Jun 4, 2026 by JovanGerb Contributor Draft
feat: add Monoid.End.equiv t-algebra Algebra (groups, rings, fields, etc)
#40221 opened Jun 4, 2026 by riccardobrasca Member Loading…
feat: add prime_units_mul and variants t-algebra Algebra (groups, rings, fields, etc)
#40220 opened Jun 4, 2026 by riccardobrasca Member Loading…
feat: add LinearIndependent.update t-algebra Algebra (groups, rings, fields, etc)
#40219 opened Jun 4, 2026 by riccardobrasca Member Loading…
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…
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…
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
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…
ProTip! no:milestone will show everything without a milestone.