Skip to content

Pull requests: leanprover-community/mathlib4

New pull request New
2,022 Open 31,469 Closed
2,022 Open 31,469 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: use push _ ∈ _
#34070 opened Jan 16, 2026 by JovanGerb Loading…
1
feat(Algebra/Order/Algebra): algebra is ordered iff inclusion map is monotone t-algebra Algebra (groups, rings, fields, etc)
#34069 opened Jan 16, 2026 by artie2000 Loading…
1
feat: give functor categories an instance of HasBinaryBiproducts new-contributor This PR was made by a contributor with at most 5 merged PRs. Welcome to the community! t-category-theory Category theory
#34068 opened Jan 16, 2026 by leomayer1 Loading…
1
ci: Revert "Retry logic for linting step (#34059)" CI Modifies the continuous integration setup or other automation delegated This pull request has been delegated to the PR author (or occasionally another non-maintainer). new-contributor This PR was made by a contributor with at most 5 merged PRs. Welcome to the community!
#34067 opened Jan 16, 2026 by marcelolynch Loading…
3
feat(scripts/autolabel): allow multiple labels, avoid labels of dependent topic areas CI Modifies the continuous integration setup or other automation
#34066 opened Jan 16, 2026 by joneugster Loading…
1
feat: Orzech property implies stable finiteness easy < 20s of review time. See the lifecycle page for guidelines. maintainer-merge A reviewer has approved the changed; awaiting maintainer approval. t-algebra Algebra (groups, rings, fields, etc) t-ring-theory Ring theory
#34064 opened Jan 16, 2026 by alreadydone Loading…
3
chore(Topology/Order): fix name of nhdsLT lemma t-topology Topological spaces, uniform spaces, metric spaces, filters
#34063 opened Jan 16, 2026 by b-mehta Loading…
1
feat: more instances of PolynormableSpace t-analysis Analysis (normed *, calculus) t-topology Topological spaces, uniform spaces, metric spaces, filters
#34062 opened Jan 16, 2026 by ADedecker Loading…
1
feat(RingTheory/IsPrimary): generalize isPrimary_inf to submodules awaiting-CI This PR doesn't 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-algebra Algebra (groups, rings, fields, etc) t-ring-theory Ring theory
#34061 opened Jan 16, 2026 by tb65536 Loading…
1 task
2
feat(RingTheory/Ideal/Colon): add a few API lemmas t-algebra Algebra (groups, rings, fields, etc) t-ring-theory Ring theory
#34060 opened Jan 16, 2026 by tb65536 Loading…
1
chore: move tsum lemmas in ENNReal.Lemmas to InfiniteSum.ENNReal t-topology Topological spaces, uniform spaces, metric spaces, filters
#34058 opened Jan 16, 2026 by sgouezel Loading…
1
chore(LinearAlgebra/Matrix/BilinearForm): sort out namespaces
#34057 opened Jan 16, 2026 by loefflerd Loading…
1
perf(Algebra): higher priority for Algebra.to_smulCommClass maintainer-merge A reviewer has approved the changed; awaiting maintainer approval. t-algebra Algebra (groups, rings, fields, etc)
#34056 opened Jan 16, 2026 by alreadydone Loading…
9
feat: vector measures associated to functions of bounded variation
#34055 opened Jan 16, 2026 by sgouezel • Draft
1
feat(Order/OmegaCompletePartialOrder): OmegaCompletePartialOrder instance for Sigma with basic ωScottContinuous lemmas 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 new-contributor This PR was made by a contributor with at most 5 merged PRs. Welcome to the community!
#34054 opened Jan 16, 2026 by YellPika Loading…
2 tasks
2
feat: Add error function (erf) and complementary error function (erfc) new-contributor This PR was made by a contributor with at most 5 merged PRs. Welcome to the community! t-analysis Analysis (normed *, calculus)
#34053 opened Jan 16, 2026 by christian-oudard Loading…
3 tasks done
5
feat(LinearAlgebra/Alternating): add map_eq_zero_of_card_lt t-algebra Algebra (groups, rings, fields, etc)
#34052 opened Jan 16, 2026 by JohnnyTeutonic Loading…
1
feat(GraphTheory): Graham-Pollak theorem awaiting-author A reviewer has asked the author a question or requested changes. t-combinatorics Combinatorics WIP Work in progress
#34050 opened Jan 16, 2026 by Julian Loading…
2
fix: defeq abuse in WithVal
#34049 opened Jan 16, 2026 by smmercuri Loading…
1
feat(Algebra/Polynomial/Splits): generalize Splits.of_splits_map to injective ring homomorphisms t-algebra Algebra (groups, rings, fields, etc) t-ring-theory Ring theory
#34048 opened Jan 16, 2026 by tb65536 Loading…
1
feat(Algebra/Polynomial/Splits): add Splits.image_rootSet_of_monic t-algebra Algebra (groups, rings, fields, etc) t-ring-theory Ring theory
#34046 opened Jan 16, 2026 by tb65536 Loading…
1
feat: algebraMap K L is uniform continuous with respect to adic topologies, when the ideal w of L lies above v blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) FLT part of the ongoing formalization of Fermat's Last Theorem
#34045 opened Jan 16, 2026 by smmercuri Loading…
1 task
2
feat(Chebyshev/RootsExtrema): Irrationality of roots of Chebyshev T (other than zero) large-import Automatically added label for PRs with a significant increase in transitive imports merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot)
#34044 opened Jan 16, 2026 by YuvalFilmus Loading…
3
chore: deprecate Data/Tree/RBMap easy < 20s of review time. See the lifecycle page for guidelines. large-import Automatically added label for PRs with a significant increase in transitive imports t-data Data (lists, quotients, numbers, etc) tech debt Tracking cross-cutting technical debt, see e.g. the "Technical debt counters" stream on zulip
#34043 opened Jan 16, 2026 by grunweg Loading…
1
feat(to_dual): use the new to_dual_cast framework 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)
#34042 opened Jan 16, 2026 by JovanGerb Loading…
1 task
1
ProTip! Type g i on any issue or pull request to go back to the issue listing page.