Skip to content

Pull requests: leanprover-community/mathlib4

New pull request New
3,144 Open 38,963 Closed
3,144 Open 38,963 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(GroupTheory/SpecificGroups/Cyclic): comparison and index of subgroups generated by powers t-group-theory Group theory
#42754 opened Aug 14, 2026 by xroblot Collaborator Loading…
1
refactor: redefine spectralRadius in terms of quasispectrum merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot)
#42753 opened Aug 13, 2026 by j-loreaux Contributor Loading…
fix(Cache): give each cache process its own temporary file names CI Modifies the continuous integration setup or other automation
#42752 opened Aug 13, 2026 by kim-em Contributor Loading…
1
chore(Algebra/QuadraticAlgebra): rename map/mapEquiv to changeGenerator t-algebra Algebra (groups, rings, fields, etc)
#42751 opened Aug 13, 2026 by xroblot Collaborator Loading…
1
feat(Topology): generalise IsometricSmul to WeakPseudoEMetricSpace and friends blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot)
#42750 opened Aug 13, 2026 by felixpernegger Contributor Loading…
1 task
4
feat(RingTheory/Bialgebra): expose (Add)MonoidAlgebra.liftMulEquiv t-ring-theory Ring theory
#42749 opened Aug 13, 2026 by kim-em Contributor Loading…
1
chore(LinearAlgebra): tidy markdown headers t-algebra Algebra (groups, rings, fields, etc)
#42748 opened Aug 13, 2026 by harahu Contributor Loading…
1
feat(Topology): generalise Dilation to WeakPseudoEMetricSpace and friends blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) LLM-generated PRs with substantial input from LLMs - review accordingly
#42747 opened Aug 13, 2026 by felixpernegger Contributor Loading…
1 task
4
chore: remove outdated adaptation notes after #42161 t-category-theory Category theory tech debt Tracking cross-cutting technical debt, see e.g. the "Technical debt counters" stream on zulip
#42745 opened Aug 13, 2026 by JovanGerb Contributor Loading…
1
feat(Analysis/InnerProductSpace): complexification of Hilbert spaces t-analysis Analysis (normed *, calculus) tech debt Tracking cross-cutting technical debt, see e.g. the "Technical debt counters" stream on zulip
#42744 opened Aug 13, 2026 by themathqueen Collaborator • Draft
1
chore(Tactic): mark two runtime-only imports as shake: keep LLM-generated PRs with substantial input from LLMs - review accordingly maintainer-merge A reviewer has approved the changed; awaiting maintainer approval. t-meta Tactics, attributes or user commands
#42743 opened Aug 13, 2026 by bryangingechen Contributor Loading…
5
feat: the set of Fredholm operators between two Banach spaces is open blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) t-topology Topological spaces, uniform spaces, metric spaces, filters
#42742 opened Aug 13, 2026 by ADedecker Member Loading…
1 task
2
feat(Topology): generalise Isometry to WeakPseudoEMetricSpace and friends LLM-generated PRs with substantial input from LLMs - review accordingly t-topology Topological spaces, uniform spaces, metric spaces, filters
#42741 opened Aug 13, 2026 by felixpernegger Contributor Loading…
1 task
3
chore: mark AlgebraicGeometry.PrimeSpectrum.Top as implicit_reducible t-algebraic-geometry Algebraic geometry tech debt Tracking cross-cutting technical debt, see e.g. the "Technical debt counters" stream on zulip
#42740 opened Aug 13, 2026 by JovanGerb Contributor Loading…
1
chore(Order/Interval): define Unique (Iic 0) directly, drop a defeq option in Traj tech debt Tracking cross-cutting technical debt, see e.g. the "Technical debt counters" stream on zulip
#42739 opened Aug 13, 2026 by FrankieNC Collaborator Loading…
1
chore(Data/Finset): mark Equiv.restrictPreimageFinset implicit_reducible t-measure-probability Measure theory / Probability theory tech debt Tracking cross-cutting technical debt, see e.g. the "Technical debt counters" stream on zulip
#42738 opened Aug 13, 2026 by FrankieNC Collaborator Loading…
1
feat(Algebra/Order/Kleene): add Kleene algebra instances for MulOppos… 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)
#42737 opened Aug 13, 2026 by Jack1320 Loading…
2
chore: mark Triangle.mk as implicit_reducible t-category-theory Category theory tech debt Tracking cross-cutting technical debt, see e.g. the "Technical debt counters" stream on zulip
#42736 opened Aug 13, 2026 by JovanGerb Contributor Loading…
2
chore(Probability/ProbabilityMassFunction): remove defeq option in Monad t-measure-probability Measure theory / Probability theory tech debt Tracking cross-cutting technical debt, see e.g. the "Technical debt counters" stream on zulip
#42735 opened Aug 13, 2026 by FrankieNC Collaborator Loading…
1
chore(Probability/Martingale): remove defeq options in OptionalStopping t-measure-probability Measure theory / Probability theory tech debt Tracking cross-cutting technical debt, see e.g. the "Technical debt counters" stream on zulip
#42734 opened Aug 13, 2026 by FrankieNC Collaborator Loading…
1
chore(Probability): remove 15/24 backward.isDefEq.respectTransparency options t-measure-probability Measure theory / Probability theory tech debt Tracking cross-cutting technical debt, see e.g. the "Technical debt counters" stream on zulip
#42733 opened Aug 13, 2026 by FrankieNC Collaborator Loading…
3
feat(TacticAnalysis): suggest rwa for rw followed by assumption t-meta Tactics, attributes or user commands
#42732 opened Aug 13, 2026 by CoolRmal Contributor Loading…
5
feat(LinearAlgebra/Dimension): add corank t-algebra Algebra (groups, rings, fields, etc)
#42731 opened Aug 13, 2026 by martinwintermath Contributor Loading…
1
chore: mark Cat.of as implicit_reducible t-category-theory Category theory tech debt Tracking cross-cutting technical debt, see e.g. the "Technical debt counters" stream on zulip
#42730 opened Aug 13, 2026 by JovanGerb Contributor Loading…
1
feat(Order/GaloisConnection): add variant of l_sSup and l_sInf delegated This pull request has been delegated to the PR author (or occasionally another non-maintainer). t-order Order theory
#42729 opened Aug 13, 2026 by martinwintermath Contributor Loading…
8
ProTip! Type g i on any issue or pull request to go back to the issue listing page.