Skip to content

Pull requests: leanprover-community/mathlib4

New pull request New
2,855 Open 38,175 Closed
2,855 Open 38,175 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(Combinatorics/SimpleGraph/Decomp): dropUntil API to match existing takeUntil API t-combinatorics Combinatorics
#41668 opened Jul 13, 2026 by SnirBroshi Collaborator Loading…
1
feat(GCDMonoid): DistribLattice Associates blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) large-import Automatically added label for PRs with a significant increase in transitive imports t-algebra Algebra (groups, rings, fields, etc)
#41667 opened Jul 13, 2026 by alreadydone Contributor Loading…
1 task
3
feat(Order): constructors for DistribLattice and IsModularLattice large-import Automatically added label for PRs with a significant increase in transitive imports t-order Order theory
#41666 opened Jul 13, 2026 by alreadydone Contributor Loading…
2
feat(Topology/Connected): transport path-connectedness along homeomorphisms 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-topology Topological spaces, uniform spaces, metric spaces, filters
#41665 opened Jul 12, 2026 by korbonits Contributor Loading…
3
perf(FieldTheory/PurelyInseparable): golf proof t-algebra Algebra (groups, rings, fields, etc)
#41664 opened Jul 12, 2026 by kbuzzard Member Loading…
4
feat(Topology/Connected): products of locally (path-)connected spaces are locally (path-)connected 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-topology Topological spaces, uniform spaces, metric spaces, filters
#41663 opened Jul 12, 2026 by korbonits Contributor Loading…
3
fix(scripts/runSkimmer): only lake update skimmer CI Modifies the continuous integration setup or other automation easy < 20s of review time. See the lifecycle page for guidelines.
#41662 opened Jul 12, 2026 by thorimur Contributor Loading…
2
feat(Topology/Connected): connected and path components of products and pi types 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-topology Topological spaces, uniform spaces, metric spaces, filters
#41661 opened Jul 12, 2026 by korbonits Contributor Loading…
3
chore(CategoryTheory/Presentable/Basic): remove bad instance t-category-theory Category theory
#41660 opened Jul 12, 2026 by JovanGerb Contributor Loading…
1
feat(Algebra/Order/GroupWithZero): generalize from MonoidWithZero to MulZeroClass t-algebra Algebra (groups, rings, fields, etc)
#41659 opened Jul 12, 2026 by NoahW314 Contributor Loading…
1
chore: Fix documentation for nnqsmul and nnqsmul_def t-algebra Algebra (groups, rings, fields, etc)
#41658 opened Jul 12, 2026 by ldct Collaborator Loading…
2
feat: haveI/letI tactic linter t-linter Linter
#41657 opened Jul 12, 2026 by JovanGerb Contributor Loading…
1
feat(AlgebraicTopology): order relation between simplices of the nerve of a partial order t-algebraic-topology Algebraic topology
#41656 opened Jul 12, 2026 by joelriou Contributor Loading…
1
feat(AlgebraicTopology): filtration of Δ[p] ⊗ Δ[1] blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) t-algebraic-topology Algebraic topology WIP Work in progress
#41655 opened Jul 12, 2026 by joelriou Contributor Loading…
2 tasks
2
chore: rename QuotientAddGroup.mk_out_eq_mul to mk_out_eq_add LLM-generated PRs with substantial input from LLMs - review accordingly t-group-theory Group theory
#41654 opened Jul 12, 2026 by adomani Contributor Loading…
1
fix(Data/Finsupp/MonomialOrder): add the missing namespace for deprecated names easy < 20s of review time. See the lifecycle page for guidelines. t-data Data (lists, quotients, numbers, etc)
#41653 opened Jul 12, 2026 by Hagb Collaborator Loading…
1
feat(GroupTheory/PGroup): maximal subgroups of abelian p-groups have index p blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) t-group-theory Group theory
#41652 opened Jul 12, 2026 by xroblot Collaborator Loading…
1 task
3
feat(GroupTheory): coatoms of the subgroup lattice and the Set.Ici correspondence t-group-theory Group theory WIP Work in progress
#41651 opened Jul 12, 2026 by xroblot Collaborator Loading…
1
feat(FieldTheory/IntermediateField): adjoining a shifted or scaled generator t-algebra Algebra (groups, rings, fields, etc)
#41649 opened Jul 12, 2026 by xroblot Collaborator Loading…
1
chore(Combinatorics/SimpleGraph): fix naming of colorable_iff_forall_connectedComponents easy < 20s of review time. See the lifecycle page for guidelines. t-combinatorics Combinatorics
#41648 opened Jul 12, 2026 by Rida-Hamadani Collaborator Loading…
1
chore: add missing to_additive docstrings (Normed, TransferInstance) LLM-generated PRs with substantial input from LLMs - review accordingly t-topology Topological spaces, uniform spaces, metric spaces, filters
#41647 opened Jul 12, 2026 by adomani Contributor Loading…
1
chore: convenience constructor for IsImmersionAtOfComplement blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) t-differential-geometry Manifolds etc
#41646 opened Jul 12, 2026 by grunweg Contributor Loading…
1 task
1
chore: add missing to_additive docstrings in Combinatorics and Dynamics LLM-generated PRs with substantial input from LLMs - review accordingly
#41645 opened Jul 12, 2026 by adomani Contributor • Draft
1
chore: add missing to_additive docstrings in Algebra (BigOperators, Order, ...) LLM-generated PRs with substantial input from LLMs - review accordingly
#41644 opened Jul 12, 2026 by adomani Contributor • Draft
1
chore: add missing to_additive docstrings in category theory files LLM-generated PRs with substantial input from LLMs - review accordingly
#41643 opened Jul 12, 2026 by adomani Contributor Loading…
1
ProTip! Adding no:label will show everything without a label.