Skip to content

Pull requests: leanprover-community/mathlib4

New pull request New
1,980 Open 31,253 Closed
1,980 Open 31,253 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(MeasureTheory.VectorMeasure): add a definition of total variation for VectorMeasure t-measure-probability Measure theory / Probability theory
#33811 opened Jan 10, 2026 by yoh-tanimoto • Draft
1
feat: add instances of LawfulInv blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) WIP Work in progress
#33810 opened Jan 9, 2026 by dupuisf Loading…
1 task
2
feat(Manifold/MFDeriv): add fun_prop to MDifferentiable t-differential-geometry Manifolds etc
#33808 opened Jan 9, 2026 by seewoo5 Loading…
1
feat: TypeCat refactor t-category-theory Category theory WIP Work in progress
#33807 opened Jan 9, 2026 by adamtopaz Loading…
1
feat(RingTheory/Localization/Ideal): generalize comap_map_of_isPrime_disjoint to primary ideals t-algebra Algebra (groups, rings, fields, etc) t-ring-theory Ring theory
#33806 opened Jan 9, 2026 by tb65536 Loading…
1
feat(AlgebraicGeometry): relative normalization in coproduct t-algebraic-geometry Algebraic geometry
#33805 opened Jan 9, 2026 by erdOne Loading…
1
feat(RingTheory/Localization/Ideal): map distributes over inf t-algebra Algebra (groups, rings, fields, etc) t-ring-theory Ring theory
#33804 opened Jan 9, 2026 by tb65536 Loading…
1
feat(RingTheory): integral closure commutes with standard etale basechange large-import Automatically added label for PRs with a significant increase in transitive imports t-ring-theory Ring theory
#33803 opened Jan 9, 2026 by erdOne Loading…
1
feat: Schur's lemma for monoid representations 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)
#33802 opened Jan 9, 2026 by stepan2698-cpu Loading…
2
chore: add missing mem lemmas
#33801 opened Jan 9, 2026 by artie2000 Loading…
2
ci(lint_and_suggest.yml): rename job CI Modifies the continuous integration setup or other automation easy < 20s of review time. See the lifecycle page for guidelines.
#33800 opened Jan 9, 2026 by bryangingechen Loading…
1
feat(Combinatorics/SimpleGraph/Basic): decidability instance for fromRel.Adj awaiting-CI This PR doesn't pass CI yet. This label is automatically removed once it does. maintainer-merge A reviewer has approved the changed; awaiting maintainer approval. t-combinatorics Combinatorics
#33798 opened Jan 9, 2026 by Paul-Lez Loading…
4
chore(Order/Defs/Unbundled): deprecate IsTotal in favor of core's Std.Total
#33797 opened Jan 9, 2026 by SnirBroshi Loading…
1
feat(LinearAlgebra/Matrix/Trace): trace map surjectivity easy < 20s of review time. See the lifecycle page for guidelines. t-algebra Algebra (groups, rings, fields, etc)
#33796 opened Jan 9, 2026 by JohnnyTeutonic Loading…
4
feat(Topology/Sheaves): LocalPredicate prerequisite for étalé spaces t-topology Topological spaces, uniform spaces, metric spaces, filters
#33795 opened Jan 9, 2026 by alreadydone Loading…
1
perf(RingTheory/Polynomial/DegreeLT): optimize proof for kernel checking t-algebra Algebra (groups, rings, fields, etc)
#33794 opened Jan 9, 2026 by Kha Loading…
3
feat(MeasureTheory/Constructions/Polish/Basic): add lemma AnalyticSet.inter_nonempty_of_nowhereMeagre new-contributor This PR was made by a contributor with at most 5 merged PRs. Welcome to the community!
#33793 opened Jan 9, 2026 by LTolDe Loading…
1
feat(GroupTheory/FiniteAbelian): construct bijection between subgroups and subgroups of the dual blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) t-group-theory Group theory
#33792 opened Jan 9, 2026 by xroblot Loading…
1 task
2
feat: Generalization of FixedPointApproximants to CompletePartialOrder new-contributor This PR was made by a contributor with at most 5 merged PRs. Welcome to the community!
#33791 opened Jan 9, 2026 by PhoenixIra Loading…
2
feat(CategoryTheory/Preadditive/Mat): add natural transformation and isomorphism extension theorems awaiting-author A reviewer has asked the author a question or requested changes. new-contributor This PR was made by a contributor with at most 5 merged PRs. Welcome to the community! t-category-theory Category theory
#33790 opened Jan 9, 2026 by eliasjudin Loading…
9
chore(Algebra): move LinearMap.ker_restrictScalars t-algebra Algebra (groups, rings, fields, etc)
#33788 opened Jan 9, 2026 by harahu Loading…
1
doc(Topology/Baire/BaireMeasurable): add naming convention for notation residualEq easy < 20s of review time. See the lifecycle page for guidelines. 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
#33787 opened Jan 9, 2026 by LTolDe Loading…
2
feat(Analysis/Matrix): add Jacobian matrix for matrix-valued functions new-contributor This PR was made by a contributor with at most 5 merged PRs. Welcome to the community! t-analysis Analysis (normed *, calculus)
#33786 opened Jan 9, 2026 by hdmkindom Loading…
1
feat: small lemmas on ArchimedeanClass t-algebra Algebra (groups, rings, fields, etc)
#33785 opened Jan 9, 2026 by vihdzp Loading…
3
refactor(Topology/Irreducible): weaken assumptions of preimage_mem_irreducibleComponents_of_isPreirreducible_fiber t-topology Topological spaces, uniform spaces, metric spaces, filters
#33784 opened Jan 9, 2026 by tb65536 Loading…
1
ProTip! What’s not been updated in a month: updated:<2025-12-09.