Skip to content

Pull requests: leanprover-community/mathlib4

New pull request New
2,300 Open 34,554 Closed
2,300 Open 34,554 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

chore: golf using simp
#37458 opened Mar 31, 2026 by euprunin Loading…
1
chore(LinearIndependent): use preferred form Finsupp.sum in lemma easy < 20s of review time. See the lifecycle page for guidelines. t-algebra Algebra (groups, rings, fields, etc)
#37457 opened Mar 31, 2026 by xgenereux Loading…
1
feat(LinearAlgebra/AffineSpace): add Desargues's theorem 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)
#37456 opened Mar 31, 2026 by Robertboy18 Loading…
5
doc: König → Kőnig documentation Improvements or additions to documentation t-set-theory Set theory
#37455 opened Mar 31, 2026 by vihdzp Loading…
1
chore(Mathlib/Topology/Category/LightProfinite/Limits.lean): automated extraction t-topology Topological spaces, uniform spaces, metric spaces, filters
#37454 opened Mar 31, 2026 by mathlib-splicebot bot Loading…
1
chore(Mathlib/Condensed/Light/Module.lean): automated extraction t-condensed Condensed mathematics
#37453 opened Mar 31, 2026 by mathlib-splicebot bot Loading…
1
chore(Mathlib/Condensed/Light/Epi.lean): automated extraction t-condensed Condensed mathematics
#37452 opened Mar 31, 2026 by mathlib-splicebot bot Loading…
1
chore(Mathlib/CategoryTheory/EffectiveEpi/Preserves.lean): automated extraction t-category-theory Category theory
#37451 opened Mar 31, 2026 by mathlib-splicebot bot Loading…
1
chore: update Mathlib dependencies 2026-03-31 dependency-bump This PR bumps the version of an upstream dependency (but not toolchain).
#37450 opened Mar 31, 2026 by mathlib-update-dependencies bot Loading…
1
feat(Condensed): the free light condensed module on ℕ∪∞ is internally projective blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot)
#37449 opened Mar 31, 2026 by dagurtomas Loading…
4 tasks
10
chore(Algebra): use IsMulCommutative to spell Std.Commutative (· * ·) t-group-theory Group theory
#37448 opened Mar 31, 2026 by SnirBroshi Loading…
5
feat(FunctionField): a function field is finite over Fq(y) for transcendental y
#37447 opened Mar 31, 2026 by xgenereux Loading…
1
refactor(Algebra): uniform API for substructures t-data Data (lists, quotients, numbers, etc)
#37446 opened Mar 31, 2026 by artie2000 Loading…
1 task
1
feat(Topology/Order): set of compact elements, generating basic opens contained in a Locale.PT, is directed blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) 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
#37445 opened Mar 31, 2026 by edwin1729 Loading…
1 task
3
feat: typeclass for zero-dimensional spaces 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 t-topology Topological spaces, uniform spaces, metric spaces, filters
#37444 opened Mar 31, 2026 by vihdzp Loading…
1 task
2
feat(Combinatorics/SimpleGraph/Walks/Operations): permutations of support t-combinatorics Combinatorics
#37443 opened Mar 31, 2026 by SnirBroshi Loading…
1
feat(CategoryTheory/ObjectProperty): add ObjectProperty.Nonempty awaiting-author A reviewer has asked the author a question or requested changes. t-category-theory Category theory
#37442 opened Mar 31, 2026 by justus-springer Loading…
2
fix(FunProp): be less strict about the shape of morphism theorems t-meta Tactics, attributes or user commands
#37441 opened Mar 31, 2026 by lecopivo Loading…
1
chore: split Topology.Algebra.Module.StrongTopology delegated This pull request has been delegated to the PR author (or occasionally another non-maintainer). file-removed A Lean module was (re)moved without a `deprecated_module` annotation t-topology Topological spaces, uniform spaces, metric spaces, filters
#37440 opened Mar 31, 2026 by ADedecker Loading…
8
feat: UniformConvergenceCLM version of ContinuousLinearEquiv.arrowCongr t-topology Topological spaces, uniform spaces, metric spaces, filters
#37439 opened Mar 31, 2026 by ADedecker Loading…
1
feat(Algebra/SkewPolynomial/Basic): add more API t-algebra Algebra (groups, rings, fields, etc)
#37438 opened Mar 31, 2026 by mariainesdff Loading…
1
feat(Algebra/SkewPolynomial/Basic): add API t-algebra Algebra (groups, rings, fields, etc)
#37437 opened Mar 31, 2026 by mariainesdff Loading…
1
feat: UniformIntegrable lemmas brownian Part of the ongoing formalization of the Brownian motion and stochastic integrals t-measure-probability Measure theory / Probability theory WIP Work in progress
#37436 opened Mar 31, 2026 by RemyDegenne Loading…
1
feat: ContinuousLinearMap.pi as a continuous linear equivalence t-topology Topological spaces, uniform spaces, metric spaces, filters
#37435 opened Mar 31, 2026 by ADedecker Loading…
1
feat(Algebra/Group/Submonoid/Basic): add lemma t-algebra Algebra (groups, rings, fields, etc)
#37434 opened Mar 31, 2026 by mariainesdff Loading…
1
ProTip! Filter pull requests by the default branch with base:master.