Skip to content

Pull requests: leanprover-community/mathlib4

New pull request New
3,108 Open 40,028 Closed
3,108 Open 40,028 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(Geometry/Euclidean): relate perpBisector and reflection large-import Automatically added label for PRs with a significant increase in transitive imports t-euclidean-geometry Affine and axiomatic geometry
#43788 opened Sep 14, 2026 by wwylele Collaborator Loading…
2
chore: remove unnecessary set_option lines auto-merge-after-CI Please do not add manually. Requests for a bot to merge automatically once CI is done. ready-to-merge This PR has been sent to bors. tech debt Tracking cross-cutting technical debt, see e.g. the "Technical debt counters" stream on zulip
#43787 opened Sep 14, 2026 by mathlib-nolints Bot Loading…
2
fix: use the PR number in the deprecation reminder message CI Modifies the continuous integration setup or other automation maintainer-merge A reviewer has approved the changed; awaiting maintainer approval.
#43786 opened Sep 13, 2026 by kim-em Contributor Loading…
3
chore: point Order/Atoms deprecations at the right replacements t-order Order theory
#43785 opened Sep 13, 2026 by kim-em Contributor Loading…
1
fix(Tactic/Inclusion): record the module registering an inclusion family t-meta Tactics, attributes or user commands
#43784 opened Sep 13, 2026 by kim-em Contributor Loading…
1
feat(Data/List/SignVariations): add List.signVariations 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)
#43783 opened Sep 13, 2026 by tomaz1502 Collaborator Loading…
20
chore: lake shake --add-public --keep-implied --keep-prefix --fix
#43782 opened Sep 13, 2026 by mathlib-nolints Bot Loading…
1
chore(AffineSpace/Independent): remove two backward.isDefEq.respectTransparency t-algebra Algebra (groups, rings, fields, etc) tech debt Tracking cross-cutting technical debt, see e.g. the "Technical debt counters" stream on zulip
#43781 opened Sep 13, 2026 by vlad902 Collaborator Loading…
1
feat: q-analogs new-contributor This PR was made by a contributor with at most 5 merged PRs. Welcome to the community! t-combinatorics Combinatorics
#43780 opened Sep 13, 2026 by SashaIr Contributor Loading…
2
feat: shuffles, permuted lists and other prerequisites for combinatorics new-contributor This PR was made by a contributor with at most 5 merged PRs. Welcome to the community!
#43779 opened Sep 13, 2026 by SashaIr Contributor Loading…
6
feat(Linter): linter for redundant <| syntax t-linter Linter
#43777 opened Sep 13, 2026 by JovanGerb Contributor Loading…
3
feat(LinearAlgebra/Matrix/SchurComplement): rank-one determinant formula det(1 - φ•c) = 1 - φ c large-import Automatically added label for PRs with a significant increase in transitive imports new-contributor This PR was made by a contributor with at most 5 merged PRs. Welcome to the community!
#43776 opened Sep 13, 2026 by tobias-weiss-ai-xr Loading…
3
feat: make simp? and to_dual?/to_additive? more concise maintainer-merge A reviewer has approved the changed; awaiting maintainer approval. t-meta Tactics, attributes or user commands
#43775 opened Sep 13, 2026 by JovanGerb Contributor Loading…
3
refactor(*): use IsSelfInv and IsSelfNeg blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot)
#43774 opened Sep 13, 2026 by justus-springer Collaborator Loading…
1 task
3
feat(Algebra/Group/Pointwise/Set/SelfInv): a few more lemmas about self-inverse sets t-algebra Algebra (groups, rings, fields, etc)
#43773 opened Sep 13, 2026 by justus-springer Collaborator Loading…
3
chore: update Mathlib dependencies 2026-09-13 bors-staging This PR is currently being built by bors on the staging branch. dependency-bump This PR bumps the version of an upstream dependency (but not toolchain). ready-to-merge This PR has been sent to bors.
#43772 opened Sep 13, 2026 by mathlib-update-dependencies Bot Loading…
2
feat(Analysis/Asymptotics): add IsTheta.comp_tendsto easy < 20s of review time. See the lifecycle page for guidelines. t-analysis Analysis (normed *, calculus)
#43771 opened Sep 13, 2026 by loefflerd Contributor Loading…
1
feat(AffineSpace/FiniteDimensional): generalize typeclasses t-algebra Algebra (groups, rings, fields, etc)
#43770 opened Sep 13, 2026 by vlad902 Collaborator Loading…
6
feat(Combinatorics/HypergraphLike): add graph-like class blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) t-combinatorics Combinatorics
#43768 opened Sep 13, 2026 by Jun2M Collaborator Loading…
1 task
1
feat(LinearAlgebra/SymmetricAlgebra): symmetric algebra is graded t-algebra Algebra (groups, rings, fields, etc)
#43767 opened Sep 13, 2026 by hawkrobe Contributor Loading…
1
feat(LinearAlgebra/SymmetricAlgebra): functoriality t-algebra Algebra (groups, rings, fields, etc)
#43766 opened Sep 13, 2026 by hawkrobe Contributor Loading…
1
chore(Algebra/MonoidHom): moving coe from .ofClass to .toMonoidHom blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot)
#43765 opened Sep 13, 2026 by jjdishere Collaborator Loading…
2 tasks
2
feat(Basic/IsEmpty/Defs): add Fin.isEmpty_iff easy < 20s of review time. See the lifecycle page for guidelines. maintainer-merge A reviewer has approved the changed; awaiting maintainer approval. t-data Data (lists, quotients, numbers, etc)
#43763 opened Sep 13, 2026 by b-mehta Contributor Loading…
3
feat(Algebra/Ring/Pi): add Pi.addCommGroupWithOne instance t-algebra Algebra (groups, rings, fields, etc)
#43761 opened Sep 12, 2026 by b-mehta Contributor Loading…
1
feat: add Filter.HasBasis.iInf_of_finite delegated This pull request has been delegated to the PR author (or occasionally another non-maintainer). easy < 20s of review time. See the lifecycle page for guidelines. t-order Order theory
#43760 opened Sep 12, 2026 by j-loreaux Contributor Loading…
4
ProTip! Find all pull requests that aren't related to any open issues with -linked:issue.