Skip to content

Pull requests: leanprover-community/mathlib4

New pull request New
2,044 Open 31,961 Closed
2,044 Open 31,961 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(Analysis/Normed/Module/{HahnBanach, Dual}): Weaken [NormedAddCommGroup] to seminormed new-contributor This PR was made by a contributor with at most 5 merged PRs. Welcome to the community!
#34585 opened Jan 29, 2026 by goliath-klein Loading…
feat: definition of a semisimple representation new-contributor This PR was made by a contributor with at most 5 merged PRs. Welcome to the community!
#34584 opened Jan 29, 2026 by stepan2698-cpu Loading…
1
feat: basic properties of subnormal subgroups large-import Automatically added label for PRs with a significant increase in transitive imports
#34583 opened Jan 29, 2026 by adomani Loading…
1
style: fix whitespace
#34582 opened Jan 29, 2026 by grunweg Loading…
6
feat(Algebra/Group/Subgroup/Ker): kernel of a homomorphism composed with an isomorphism 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)
#34580 opened Jan 29, 2026 by homeowmorphism Loading…
5
feat: ¬ x <ᵥ 0 easy < 20s of review time. See the lifecycle page for guidelines. t-algebra Algebra (groups, rings, fields, etc)
#34579 opened Jan 29, 2026 by vihdzp Loading…
1
feat: define Boolean circuits over abstract gate families new-contributor This PR was made by a contributor with at most 5 merged PRs. Welcome to the community!
#34578 opened Jan 29, 2026 by dennj Loading…
1
feat: use more fun_prop/measurability auto-parameters t-measure-probability Measure theory / Probability theory
#34577 opened Jan 29, 2026 by grunweg Loading…
1
feat(Analysis/Calculus/Deriv/Inverse): add deriv_zero_of_frequently_mem_discrete t-analysis Analysis (normed *, calculus) t-topology Topological spaces, uniform spaces, metric spaces, filters
#34576 opened Jan 29, 2026 by tb65536 Loading…
1
feat(Integral/Pi): add more convenience API t-measure-probability Measure theory / Probability theory
#34575 opened Jan 29, 2026 by urkud • Draft
1
chore(Analysis/Normed/Lp/SmoothApprox): shake public imports
#34573 opened Jan 29, 2026 by Kha Loading…
11
feat(RingTheory/UniqueFactorizationDomain/Basic): associated elements have the same number of factors delegated This pull request has been delegated to the PR author (or occasionally another non-maintainer). t-algebra Algebra (groups, rings, fields, etc)
#34572 opened Jan 29, 2026 by tb65536 Loading…
6
feat(CyclotomicField/Galois): the bijection between subfields and subgroups of Dirichlet characters 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
#34571 opened Jan 29, 2026 by xroblot Loading…
1 task
2
feat(DirichletCharacter): any element of the conductorSet is divisible by the conductor delegated This pull request has been delegated to the PR author (or occasionally another non-maintainer). t-number-theory Number theory (also use t-algebra or t-analysis to specialize)
#34569 opened Jan 29, 2026 by xroblot Loading…
5
chore(Geometry/Euclidean): golf a proof delegated This pull request has been delegated to the PR author (or occasionally another non-maintainer). t-euclidean-geometry Affine and axiomatic geometry
#34567 opened Jan 29, 2026 by jcommelin Loading…
5
chore: add a test for differential geometry elaborator errors in the … t-differential-geometry Manifolds etc t-meta Tactics, attributes or user commands
#34564 opened Jan 29, 2026 by grunweg Loading…
1
feat(CategoryTheory): Frobenius reciprocity for regular categories 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-category-theory Category theory
#34563 opened Jan 29, 2026 by FernandoChu Loading…
11
chore: fix and re-enable differential geometry elaborators test easy < 20s of review time. See the lifecycle page for guidelines. t-meta Tactics, attributes or user commands
#34562 opened Jan 29, 2026 by grunweg Loading…
1
feat: bounded variation functions have left and right limits, and limits at infinity t-topology Topological spaces, uniform spaces, metric spaces, filters
#34559 opened Jan 29, 2026 by sgouezel Loading…
1
feat(Topology): add StrictMono finite partition lemmas and path partitioning t-topology Topological spaces, uniform spaces, metric spaces, filters
#34558 opened Jan 29, 2026 by kim-em Loading…
1
feat(Topology/Homotopy): add Path.subpathOn for restricting paths to subintervals awaiting-author A reviewer has asked the author a question or requested changes. t-topology Topological spaces, uniform spaces, metric spaces, filters
#34557 opened Jan 29, 2026 by kim-em Loading…
2
feat: IMO 2002 Q3 IMO Math olympiad problems
#34556 opened Jan 29, 2026 by Parcly-Taxel Loading…
1
feat(Data/Nat/Factorization/Divisors): calculate divisors using prime factorization delegated This pull request has been delegated to the PR author (or occasionally another non-maintainer). t-data Data (lists, quotients, numbers, etc)
#34554 opened Jan 29, 2026 by SnirBroshi Loading…
16
feat(Tactic): Add NormNum extension for NNReal.rpow t-analysis Analysis (normed *, calculus) t-meta Tactics, attributes or user commands
#34553 opened Jan 28, 2026 by DavidLedvinka Loading…
1
chore(Analysis/SchwartzSpace): make some definitions private t-analysis Analysis (normed *, calculus)
#34552 opened Jan 28, 2026 by mcdoll Loading…
4
ProTip! Add no:assignee to see everything that’s not assigned.