Skip to content

Pull requests: leanprover-community/mathlib4

New pull request New
2,265 Open 33,493 Closed
2,265 Open 33,493 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: integrability with respect to a countable sum of measures t-measure-probability Measure theory / Probability theory
#36355 opened Mar 8, 2026 by EtienneC30 • Draft
1
chore(Order/Hom/Bounded): use to_dual t-order Order theory
#36354 opened Mar 8, 2026 by gasparattila Loading…
1
feat(NumberField/InfinitePlace/Ramification): add cardinality results for (un)ramified places over t-number-theory Number theory (also use t-algebra or t-analysis to specialize)
#36353 opened Mar 8, 2026 by smmercuri Loading…
1
chore(Mathlib/CategoryTheory/Limits/Shapes/Pullback/IsPullback/Basic.lean): automated extraction 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-category-theory Category theory
#36352 opened Mar 8, 2026 by mathlib-splicebot bot Loading…
4
doc(Analysis): fix typos easy < 20s of review time. See the lifecycle page for guidelines. t-analysis Analysis (normed *, calculus)
#36351 opened Mar 8, 2026 by harahu Loading…
2
feat(Algebra/Star/SelfAdjoint): IsSelfAdjoint of Invertible t-algebra Algebra (groups, rings, fields, etc)
#36350 opened Mar 8, 2026 by SnirBroshi Loading…
1
feat(LinearAlgebra/Matrix): expand IsSymm/IsHermitian API t-algebra Algebra (groups, rings, fields, etc)
#36349 opened Mar 8, 2026 by SnirBroshi Loading…
1
feat(Algebra/Star/Basic): StarAddMonoid.toStarModule{Nat,Int} doesn't need commutativity easy < 20s of review time. See the lifecycle page for guidelines. t-algebra Algebra (groups, rings, fields, etc)
#36348 opened Mar 8, 2026 by SnirBroshi Loading…
1
feat(NumberTheory/QuadraticField): define quadratic number fields over ℚ new-contributor This PR was made by a contributor with at most 5 merged PRs. Welcome to the community! t-number-theory Number theory (also use t-algebra or t-analysis to specialize) WIP Work in progress
#36347 opened Mar 8, 2026 by FrankieeW Loading…
3
chore: add simp lemma to unfold Algebra.algHom
#36346 opened Mar 8, 2026 by kckennylau Loading…
1
feat(AlgebraicGeometry): Vanishing for Affine Schemes 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!
#36345 opened Mar 8, 2026 by Brian-Nugent • Draft
2
chore(Data/Matrix/Mul): fix references in docstrings easy < 20s of review time. See the lifecycle page for guidelines. t-data Data (lists, quotients, numbers, etc)
#36343 opened Mar 8, 2026 by SnirBroshi Loading…
1
chore(Data/Matrix/Composition): fix docstring easy < 20s of review time. See the lifecycle page for guidelines. t-data Data (lists, quotients, numbers, etc)
#36342 opened Mar 8, 2026 by SnirBroshi Loading…
1
feat(RepresentationTheory/Action): Create representation from Action, second step of refactor Rep t-algebra Algebra (groups, rings, fields, etc)
#36341 opened Mar 8, 2026 by Whysoserioushah Loading…
1
feat: Int.mul_{pos,nonpos,neg}_iff easy < 20s of review time. See the lifecycle page for guidelines. t-data Data (lists, quotients, numbers, etc)
#36340 opened Mar 8, 2026 by Parcly-Taxel Loading…
3
feat(CategoryTheory/Over): Over X is equivalent to PUnit if X is strict initial awaiting-author A reviewer has asked the author a question or requested changes. t-category-theory Category theory
#36339 opened Mar 7, 2026 by chrisflav Loading…
2
doc(Algebra): fix typos easy < 20s of review time. See the lifecycle page for guidelines. t-algebra Algebra (groups, rings, fields, etc)
#36338 opened Mar 7, 2026 by harahu Loading…
2
feat: add indiscrete topology lemmas 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
#36336 opened Mar 7, 2026 by NoahW314 Loading…
7
feat(Combinatorics/SimpleGraph/AdjMatrix): adjacency matrices are Hermitian large-import Automatically added label for PRs with a significant increase in transitive imports t-combinatorics Combinatorics
#36335 opened Mar 7, 2026 by SnirBroshi Loading…
2
feat(AlgebraicGeometry/EllipticCurve): add notation and pretty printer for points t-algebraic-geometry Algebraic geometry
#36334 opened Mar 7, 2026 by Multramate Loading…
2
test: checkTypeEvenMore large-import Automatically added label for PRs with a significant increase in transitive imports t-linter Linter
#36333 opened Mar 7, 2026 by thorimur • Draft
1
feat(Analysis/Normed/Module/WeakDual): register bornology and boundedness API new-contributor This PR was made by a contributor with at most 5 merged PRs. Welcome to the community! t-analysis Analysis (normed *, calculus)
#36332 opened Mar 7, 2026 by mike1729 Loading…
3 tasks
2
feat(UpperHalfPlane): define PGL action on the upper half-plane
#36330 opened Mar 7, 2026 by urkud Loading…
1
feat(PowerSeries): add barebones Log.lean t-ring-theory Ring theory
#36329 opened Mar 7, 2026 by rwst Loading…
1
feat(AlgebraicGeometry/EllipticCurve): improve API for maps and base changes t-algebraic-geometry Algebraic geometry
#36328 opened Mar 7, 2026 by Multramate Loading…
1
ProTip! no:milestone will show everything without a milestone.