8000 Pull requests · leanprover-community/mathlib4 · GitHub
[go: up one dir, main page]
Skip to content

Pull requests: leanprover-community/mathlib4

New pull request New
2,066 Open 31,907 Closed
2,066 Open 31,907 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 8000
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(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…
3
feat(Algebra/Order/Antidiag): add HasMulAntidiagonal and apply @[to_additive] 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)
#34551 opened Jan 28, 2026 by IlPreteRosso Loading…
4
chore: fix bench suite typos CI Modifies the continuous integration setup or other automation ready-to-merge This PR has been sent to bors.
#34550 opened Jan 28, 2026 by Garmelon Loading…
2
feat(Finpartition): remove unnecessary DistribLattice assumptions t-order Order theory
#34545 opened Jan 28, 2026 by gasparattila Loading…
1
feat(CategoryTheory): constant functors are accessible, accessibility is preserved by composition t-category-theory Category theory
#34544 opened Jan 28, 2026 by dagurtomas Loading…
2
refactor: improve API connecting ℝ- and 𝕜-linear functionals blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) t-analysis Analysis (normed *, calculus)
#34543 opened Jan 28, 2026 by j-loreaux Loading…
1 task
2
feat(Probability/Independence): add iIndep_of_iIndep_of_le lemmas maintainer-merge A reviewer has approved the changed; awaiting maintainer approval. new-contributor This PR was made by a contributor with at most 5 merged PRs. Welcome to the community! t-measure-probability Measure theory / Probability theory
#34542 opened Jan 28, 2026 by jvanwinden Loading…
11
chore(CategoryTheory/Adjunction): slightly generalize universes in adjoint functor theorem t-category-theory Category theory
#34541 opened Jan 28, 2026 by dagurtomas Loading…
1
feat(Cache): continue trying to download if the first repository had some errors awaiting-author A reviewer has asked the author a question or requested changes. CI Modifies the continuous integration setup or other automation
#34539 opened Jan 28, 2026 by grunweg Loading…
2
chore(Tactic/CasesM): improve casesm, cases_type and constructorm tactic docstrings documentation Improvements or additions to documentation t-meta Tactics, attributes or user commands
#34538 opened Jan 28, 2026 by Vierkantor Loading…
1
chore(Tactic/Cases): improve cases' and induction' docstrings documentation Improvements or additions to documentation t-meta Tactics, attributes or user commands
#34537 opened Jan 28, 2026 by Vierkantor Loading…
1
chore(Algebra/Group/Subgroup/Basic): tag instIsMulTorsionFree with to_additive easy < 20s of review time. See the lifecycle page for guidelines. t-algebra Algebra (groups, rings, fields, etc)
#34536 opened Jan 28, 2026 by tb65536 Loading…
1
feat(Topology/Algebra/ContinuousMonoidHom): add missing API for monoid structure t-topology Topological spaces, uniform spaces, metric spaces, filters
#34535 opened Jan 28, 2026 by tb65536 Loading…
1
feat(NumberTheory/Height/Basic): positivity extensions t-meta Tactics, attributes or user commands t-number-theory Number theory (also use t-algebra or t-analysis to specialize)
#34534 opened Jan 28, 2026 by MichaelStollBayreuth Loading…
3
feat: add API lemmas for Multiset.prod_map and finprod large-import Automatically added label for PRs with a significant increase in transitive imports t-algebra Algebra (groups, rings, fields, etc)
#34533 opened Jan 28, 2026 by MichaelStollBayreuth Loading…
3
feat(GroupTheory/GroupAction/SubMulAction/Combination): primitivity of the action large-import Automatically added label for PRs with a significant increase in transitive imports t-group-theory Group theory
#34531 opened Jan 28, 2026 by AntoineChambert-Loir Loading…
2
fix: remove defeq abuse in the Hahn-Banach theorem maintainer-merge A reviewer has approved the changed; awaiting maintainer approval. t-analysis Analysis (normed *, calculus) tech debt Tracking cross-cutting technical debt, see e.g. the "Technical debt counters" stream on zulip
#34530 opened Jan 28, 2026 by j-loreaux Loading…
3
feat(Topology/UniformSpace): compactness of Closeds t-topology Topological spaces, uniform spaces, metric spaces, filters
#34529 opened Jan 28, 2026 by gasparattila Loading…
1
feat: Reproducing Kernel Hilbert Spaces and Moore's theorem t-analysis Analysis (normed *, calculus)
#34528 opened Jan 28, 2026 by Maldooor • Draft
1
chore: avoid redundant error message in differential geometry elaborators t-differential-geometry Manifolds etc t-meta Tactics, attributes or user commands
#34527 opened Jan 28, 2026 by grunweg Loading…
1 task done
5
chore(*): use apply +allowSynthFailures syntax 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 tech debt Tracking cross-cutting technical debt, see e.g. the "Technical debt counters" stream on zulip
#34525 opened Jan 28, 2026 by Vierkantor Loading…
1 task
@grunweg
2
feat(Tactic/ApplyWith): use a config_elab for apply (config := cfg) maintainer-merge A reviewer has approved the changed; awaiting maintainer approval. t-meta Tactics, attributes or user commands
#34524 opened Jan 28, 2026 by Vierkantor Loading…
11
chore(*): shake further large-import Automatically added label for PRs with a significant increase in transitive imports
#34523 opened Jan 28, 2026 by Kha Loading…
4
chore(Analysis/Distribution): simplify some proofs t-analysis Analysis (normed *, calculus)
#34522 opened Jan 28, 2026 by LLaurance Loading…
1
ProTip! What’s not been updated in a month: updated:<2025-12-28.
0