Skip to content

Pull requests: leanprover-community/mathlib4

New pull request New
2,725 Open 38,006 Closed
2,725 Open 38,006 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(SimpleGraph/Clique): tidy CliqueFree iff lemmas t-combinatorics Combinatorics
#41364 opened Jul 4, 2026 by SnirBroshi Collaborator Loading…
1
feat(SimpleGraph/Acyclic): a graph is acyclic iff it is free of cycle graphs delegated This pull request has been delegated to the PR author (or occasionally another non-maintainer). t-combinatorics Combinatorics
#41363 opened Jul 4, 2026 by SnirBroshi Collaborator Loading…
5
perf(Algebra/MonoidAlgebra): no_expose the Add instance
#41362 opened Jul 4, 2026 by JovanGerb Contributor • Draft
2
feat(Data/Finset/Lattice/Fold): add sup_eq_iSup' carleson part of the ongoing formalization of Carleson's theorem 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)
#41361 opened Jul 4, 2026 by lakesare Contributor Loading…
4
feat(Topology/Order/IntermediateValue): add fixed point theorem easy < 20s of review time. See the lifecycle page for guidelines. 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
#41360 opened Jul 4, 2026 by franv314 Loading…
4
feat(Analysis/RCLike/Basic): add norm_I carleson part of the ongoing formalization of Carleson's theorem easy < 20s of review time. See the lifecycle page for guidelines. new-contributor This PR was made by a contributor with at most 5 merged PRs. Welcome to the community! t-analysis Analysis (normed *, calculus)
#41359 opened Jul 4, 2026 by lakesare Contributor Loading…
4
doc(ModelTheory): fix partial equivalence theorem reference new-contributor This PR was made by a contributor with at most 5 merged PRs. Welcome to the community! t-logic Logic (model theory, etc)
#41358 opened Jul 4, 2026 by erdkocak Loading…
2
feat(Tactic/ComputablePolynomial): mv_mem, axiom-free ideal membership for MvPolynomial blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) t-meta Tactics, attributes or user commands
#41356 opened Jul 4, 2026 by mkaratarakis Contributor Loading…
1 task
2
feat(Tactic/ComputablePolynomial): mv_decide, axiom-free reflection for MvPolynomial blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) t-meta Tactics, attributes or user commands
#41355 opened Jul 4, 2026 by mkaratarakis Contributor Loading…
1 task
2
feat(Tactic/ComputablePolynomial): add CommRing and Algebra instances for MvSparsePoly blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) t-meta Tactics, attributes or user commands
#41354 opened Jul 4, 2026 by mkaratarakis Contributor Loading…
1 task
3
feat(Tactic/ComputablePolynomial): the Finsupp bridge and injectivity of MvSparsePoly.toPoly blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) t-meta Tactics, attributes or user commands
#41353 opened Jul 4, 2026 by mkaratarakis Contributor Loading…
1 task
2
feat(Tactic/ComputablePolynomial): multiplication and negation for MvSparsePoly blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) t-meta Tactics, attributes or user commands
#41352 opened Jul 4, 2026 by mkaratarakis Contributor Loading…
1 task
2
feat(Tactic/ComputablePolynomial): add MvSparsePoly.ofList, X and monomial multiplication blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) t-meta Tactics, attributes or user commands
#41351 opened Jul 4, 2026 by mkaratarakis Contributor Loading…
1 task
3
feat(Tactic/ComputablePolynomial): define MvSparsePoly, a computable multivariate polynomial blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) t-meta Tactics, attributes or user commands
#41350 opened Jul 4, 2026 by mkaratarakis Contributor Loading…
1 task
3
feat(Tactic/ComputablePolynomial): the lexicographic monomial order on MvDegrees blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) t-meta Tactics, attributes or user commands
#41349 opened Jul 4, 2026 by mkaratarakis Contributor Loading…
1 task
2
feat(Tactic/ComputablePolynomial): define MvDegrees, exponent vectors for multivariate polynomials t-meta Tactics, attributes or user commands
#41348 opened Jul 4, 2026 by mkaratarakis Contributor Loading…
2
feat(Tactic/ComputablePolynomial): poly_dvd_cert, certificate-based polynomial divisibility t-meta Tactics, attributes or user commands
#41347 opened Jul 4, 2026 by mkaratarakis Contributor Loading…
1
feat(Tactic/ComputablePolynomial): poly_eval and poly_dvd tactics blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) t-meta Tactics, attributes or user commands
#41346 opened Jul 4, 2026 by mkaratarakis Contributor Loading…
1 task
2
feat(Tactic/ComputablePolynomial): poly_decide, axiom-free reflection for Polynomial blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) t-meta Tactics, attributes or user commands
#41345 opened Jul 4, 2026 by mkaratarakis Contributor Loading…
1 task
2
feat(Tactic/ComputablePolynomial): division with remainder and SparsePoly ≃ₐ Polynomial blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) t-meta Tactics, attributes or user commands
#41344 opened Jul 4, 2026 by mkaratarakis Contributor Loading…
1 task
2
feat(Tactic/ComputablePolynomial): gcd, content and primitive part for SparsePoly blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) t-meta Tactics, attributes or user commands
#41343 opened Jul 4, 2026 by mkaratarakis Contributor Loading…
1 task
2
feat(Tactic/ComputablePolynomial): degree and pseudo-division bounds for SparsePoly blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) t-meta Tactics, attributes or user commands
#41342 opened Jul 4, 2026 by mkaratarakis Contributor Loading…
1 task
2
feat(Tactic/ComputablePolynomial): add CommRing and Algebra instances for SparsePoly blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) t-meta Tactics, attributes or user commands
#41341 opened Jul 4, 2026 by mkaratarakis Contributor Loading…
1 task
3
feat(Tactic/ComputablePolynomial): add SparsePoly.ofList and injectivity of toPoly blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) t-meta Tactics, attributes or user commands
#41340 opened Jul 4, 2026 by mkaratarakis Contributor Loading…
1 task
3
feat(Tactic/ComputablePolynomial): define SparsePoly, a computable univariate polynomial t-meta Tactics, attributes or user commands
#41339 opened Jul 4, 2026 by mkaratarakis Contributor Loading…
2
ProTip! Mix and match filters to narrow down what you’re looking for.