Skip to content

Pull requests: leanprover-community/mathlib4

New pull request New
2,022 Open 31,475 Closed
2,022 Open 31,475 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

refactor(GroupTheory/CommutingProbability): clean up using grind t-algebra Algebra (groups, rings, fields, etc) t-group-theory Group theory
#34076 opened Jan 17, 2026 by tb65536 Loading…
3
feat: add a typeclass for the continuum hypothesis t-set-theory Set theory
#34075 opened Jan 17, 2026 by eric-wieser Loading…
2
feat(Asymptotics/TVS): prove that IsBigOTVS is equivalent to IsBigO t-analysis Analysis (normed *, calculus)
#34074 opened Jan 17, 2026 by urkud Loading…
1
feat(LinearAlgebra/FiniteDimensional): add finrank_ker_of_surjective t-algebra Algebra (groups, rings, fields, etc)
#34073 opened Jan 17, 2026 by JohnnyTeutonic Loading…
1
feat(Chebyshev polynomials): Prove that the roots of the Chebyshev polynomials (except 0) are irrational. large-import Automatically added label for PRs with a significant increase in transitive imports t-analysis Analysis (normed *, calculus)
#34072 opened Jan 17, 2026 by yuanyi-350 Loading…
2
feat: ContinuousMonoidHom.toMonoidHom_injective maintainer-merge A reviewer has approved the changed; awaiting maintainer approval. t-topology Topological spaces, uniform spaces, metric spaces, filters
#34071 opened Jan 17, 2026 by bwangpj Loading…
3
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). merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) 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…
4
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
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 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
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
ProTip! Adding no:label will show everything without a label.