Skip to content

Pull requests: leanprover-community/mathlib4

New pull request New
2,601 Open 36,539 Closed
2,601 Open 36,539 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(Module/Projective): direct sum of projective modules is projective t-algebra Algebra (groups, rings, fields, etc)
#39764 opened May 24, 2026 by vlad902 Collaborator Loading…
6
feat(Algebra/GroupWithZero/Divisibility): add mul_dvd_left_iff_isUnit t-algebra Algebra (groups, rings, fields, etc)
#39763 opened May 24, 2026 by NoahW314 Contributor Loading…
1
chore(Topology/UniformSpace): rename uniformContinuous_iff to uniformContinuous_iff_le_comap t-topology Topological spaces, uniform spaces, metric spaces, filters
#39762 opened May 24, 2026 by plp127 Contributor Loading…
2
chore(CategoryTheory/Limits): generalise universes in instances for representable functors t-category-theory Category theory
#39760 opened May 23, 2026 by chrisflav Member Loading…
1
chore(FieldTheory/KrullTopology): move lemmas to earlier file t-algebra Algebra (groups, rings, fields, etc)
#39759 opened May 23, 2026 by plp127 Contributor Loading…
2
chore: use skip instead of -failIfUnchanged in the default tactic of Homeomorph t-topology Topological spaces, uniform spaces, metric spaces, filters
#39758 opened May 23, 2026 by gasparattila Contributor Loading…
@grunweg
3
chore(Algebra/Star): clean up simp lemmas about bundled star equivalences
#39757 opened May 23, 2026 by gasparattila Contributor Loading…
2
chore(GroupTheory): remove a defeq abuse t-group-theory Group theory tech debt Tracking cross-cutting technical debt, see e.g. the "Technical debt counters" stream on zulip
#39755 opened May 23, 2026 by wwylele Collaborator Loading…
1
feat: the natural filtration of a process is the filtration generated by the process blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) brownian Part of the ongoing formalization of the Brownian motion and stochastic integrals t-measure-probability Measure theory / Probability theory
#39754 opened May 23, 2026 by EtienneC30 Member Loading…
1 task
2
feat: the sigma-algebra generated by the constant indicator of a set is smaller than the one generated by the set t-measure-probability Measure theory / Probability theory
#39753 opened May 23, 2026 by mathlib-splicebot Bot Loading…
2
feat(Nat/Digits/Lemma): add a lemma to unfold Nat.digitsAppend easy < 20s of review time. See the lifecycle page for guidelines. t-data Data (lists, quotients, numbers, etc)
#39752 opened May 23, 2026 by xroblot Collaborator Loading…
2
feat: if a sigma-algebra is independent from itself then all sets in it have measure 0 or 1 blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) brownian Part of the ongoing formalization of the Brownian motion and stochastic integrals t-measure-probability Measure theory / Probability theory
#39750 opened May 23, 2026 by mathlib-splicebot Bot Loading…
1 task
4
feat: when the indicator is independent from a random variable brownian Part of the ongoing formalization of the Brownian motion and stochastic integrals t-measure-probability Measure theory / Probability theory
#39749 opened May 23, 2026 by EtienneC30 Member Loading…
1
feat: another independence monotonicity lemma brownian Part of the ongoing formalization of the Brownian motion and stochastic integrals t-measure-probability Measure theory / Probability theory
#39748 opened May 23, 2026 by EtienneC30 Member Loading…
1
feat: intervals Ici/Ioi are cofinal/closed under suprema t-order Order theory
#39747 opened May 23, 2026 by vihdzp Collaborator Loading…
8
feat: Dieudonné measure on a well-order blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) t-measure-probability Measure theory / Probability theory t-set-theory Set theory
#39746 opened May 23, 2026 by vihdzp Collaborator Loading…
2 tasks
2
feat: install gh inside the devcontainer CI Modifies the continuous integration setup or other automation
#39745 opened May 23, 2026 by joneugster Contributor Loading…
@bryangingechen
1
feat(NumberTheory/Height/NumberField): Northcott property blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) t-number-theory Number theory (also use t-algebra or t-analysis to specialize)
#39744 opened May 23, 2026 by MichaelStollBayreuth Contributor Loading…
1 task
2
feat(FieldTheory): the field of adjoining all pth roots t-algebra Algebra (groups, rings, fields, etc)
#39740 opened May 23, 2026 by Thmoas-Guan Collaborator Loading…
@chrisflav
11
chore: generalize IsZeroOneMeasure.exists_eq_dirac t-measure-probability Measure theory / Probability theory WIP Work in progress
#39739 opened May 23, 2026 by RemyDegenne Contributor Loading…
1
feat(Algebra/Algebra/Bilinear): generalize to NonUnitalNonAssocCommSemiring t-algebra Algebra (groups, rings, fields, etc)
#39738 opened May 23, 2026 by NoahW314 Contributor Loading…
1
feat(RingTheory/MvPolynomial/MonomialOrder): add leadingTerm lemmas t-ring-theory Ring theory
#39736 opened May 23, 2026 by NoahW314 Contributor Loading…
1
feat(LinearAlgebra/Matrix): regularized inverse limit and trace continuity LLM-generated PRs with substantial input from LLMs - review accordingly 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)
#39735 opened May 23, 2026 by allenhaozhu • Draft
2
feat(Analysis/CStarAlgebra/CStarMatrix): operator-monotone rpow/log/sqrt specializations LLM-generated PRs with substantial input from LLMs - review accordingly new-contributor This PR was made by a contributor with at most 5 merged PRs. Welcome to the community! t-analysis Analysis (normed *, calculus)
#39734 opened May 23, 2026 by allenhaozhu • Draft
2
feat(LinearAlgebra/Matrix): nonsingular inverse commutes with any monoid hom of matrix rings LLM-generated PRs with substantial input from LLMs - review accordingly 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)
#39733 opened May 23, 2026 by allenhaozhu • Draft
2
ProTip! Updated in the last three days: updated:>2026-05-21.