Skip to content

Pull requests: leanprover-community/mathlib4

New pull request New
2,149 Open 32,548 Closed
2,149 Open 32,548 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(Algebra/LinearRecurrence): define a standard basis for the solution space of a linear recurrence t-algebra Algebra (groups, rings, fields, etc)
#35285 opened Feb 14, 2026 by SnirBroshi Loading…
1
feat: add (m)differentiableAt_of_(m)fderiv_injective easy < 20s of review time. See the lifecycle page for guidelines. t-analysis Analysis (normed *, calculus) t-differential-geometry Manifolds etc
#35284 opened Feb 14, 2026 by grunweg Loading…
1
feat(Algebra/Polynomial): add Polynomial.algHomEquiv and its bivariate version easy < 20s of review time. See the lifecycle page for guidelines. t-algebra Algebra (groups, rings, fields, etc)
#35283 opened Feb 13, 2026 by Multramate Loading…
3
chore(Analysis): fix markdown list indentation awaiting-author A reviewer has asked the author a question or requested changes. t-analysis Analysis (normed *, calculus)
#35282 opened Feb 13, 2026 by harahu Loading…
@grunweg
2
chore: fix markdown list indentation
#35281 opened Feb 13, 2026 by harahu • Draft
1
feat(Mathlib/Analysis/Polynomial/MahlerMeasure): Mahler Measure estimate in terms of supNorm new-contributor This PR was made by a contributor with at most 5 merged PRs. Welcome to the community! t-analysis Analysis (normed *, calculus)
#35280 opened Feb 13, 2026 by khwilson Loading…
2
chore(Data/Nat/Choose): add grind annotations t-data Data (lists, quotients, numbers, etc)
#35279 opened Feb 13, 2026 by BoltonBailey Loading…
4
chore: replace continuity by fun_prop in a few proofs t-topology Topological spaces, uniform spaces, metric spaces, filters
#35278 opened Feb 13, 2026 by grunweg Loading…
3
ci: remove outdated logic in workflows CI Modifies the continuous integration setup or other automation file-removed A Lean module was (re)moved without a `deprecated_module` annotation
#35277 opened Feb 13, 2026 by marcelolynch Loading…
1
chore: explicit field names for Concept.copy easy < 20s of review time. See the lifecycle page for guidelines. t-order Order theory
#35276 opened Feb 13, 2026 by vihdzp Loading…
1
feat: extent/intent theorems for indexed suprema/infima t-order Order theory
#35275 opened Feb 13, 2026 by vihdzp Loading…
1
doc(CategoryTheory/Bicategory/NaturalTransformation): tidy docstrings t-category-theory Category theory
#35274 opened Feb 13, 2026 by harahu Loading…
1
chore: replace continuity -> fun_prop in remaining auto-parameters awaiting-CI This PR does not pass CI yet. This label is automatically removed once it does. 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 WIP Work in progress
#35273 opened Feb 13, 2026 by grunweg Loading…
1 task
2
feat(Topology/Instances/EReal): limsup of multiplication by a constant 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
#35272 opened Feb 13, 2026 by jvanwinden Loading…
3
refactor(Topology/Algebra/Module/LinearMap): adjust statement of coe_mul and coe_pow t-algebra Algebra (groups, rings, fields, etc) t-topology Topological spaces, uniform spaces, metric spaces, filters
#35269 opened Feb 13, 2026 by tb65536 Loading…
1
feat(Topology/Algebra/Module/LinearMap): units in M →L[R] M are homeomorphisms t-algebra Algebra (groups, rings, fields, etc) t-topology Topological spaces, uniform spaces, metric spaces, filters
#35268 opened Feb 13, 2026 by tb65536 Loading…
1
feat: deprecate Expr.isConstantApplication awaiting-author A reviewer has asked the author a question or requested changes. maintainer-merge A reviewer has approved the changed; awaiting maintainer approval. t-meta Tactics, attributes or user commands
#35267 opened Feb 13, 2026 by JovanGerb Loading…
7
refactor: make OrderIso.ofHomInv take actual OrderHoms instead of using classes t-order Order theory
#35266 opened Feb 13, 2026 by j-loreaux Loading…
1
ci: Change actionlint fail level from error to any CI Modifies the continuous integration setup or other automation maintainer-merge A reviewer has approved the changed; awaiting maintainer approval.
#35265 opened Feb 13, 2026 by bryangingechen Loading…
@joneugster
3
refactor: use OrderSupInfSet large-import Automatically added label for PRs with a significant increase in transitive imports t-order Order theory
#35263 opened Feb 13, 2026 by astrainfinita • Draft
1
feat: push lemmas for Filter.NeBot t-order Order theory
#35261 opened Feb 13, 2026 by j-loreaux Loading…
1
feat(Data/Fintype/Order): add API for ciSup with finite indexing type t-order Order theory
#35260 opened Feb 13, 2026 by MichaelStollBayreuth Loading…
1
feat: add a definition and API lemmas for Polynomial.homogenize and MvPolynomial t-algebra Algebra (groups, rings, fields, etc)
#35259 opened Feb 13, 2026 by MichaelStollBayreuth Loading…
1
feat(Data/Finsupp/Order): add lemma Finsupp.single_le_sum t-data Data (lists, quotients, numbers, etc)
#35258 opened Feb 13, 2026 by MichaelStollBayreuth Loading…
1
feat(CategoryTheory): equality of morphisms can be checked on a cover t-category-theory Category theory
#35257 opened Feb 13, 2026 by chrisflav Loading…
2
ProTip! Mix and match filters to narrow down what you’re looking for.