Skip to content

Pull requests: leanprover-community/mathlib4

New pull request New
2,119 Open 32,292 Closed
2,119 Open 32,292 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(LinearAlgebra/BilinearForm): remove BilinForm.IsRefl hypothesis in some theorems t-algebra Algebra (groups, rings, fields, etc)
#34998 opened Feb 8, 2026 by bwangpj Loading…
1
feat(LinearAlgebra/Matrix/Hadamard): convolutive ring on matrices 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)
#34997 opened Feb 8, 2026 by themathqueen Loading…
1 task
2
feat(GroupTheory/FreeGroup/Basic): injection between types induces injection between free groups new-contributor This PR was made by a contributor with at most 5 merged PRs. Welcome to the community!
#34996 opened Feb 8, 2026 by homeowmorphism • Draft
3
chore(AlgebraicGeometry/Sites): use Precoverage.toGrothendieck instead of Pretopology.toGrothendieck t-algebraic-geometry Algebraic geometry
#34995 opened Feb 8, 2026 by chrisflav Loading…
1
feat: Countable.of_module_finite FLT part of the ongoing formalization of Fermat's Last Theorem large-import Automatically added label for PRs with a significant increase in transitive imports t-algebra Algebra (groups, rings, fields, etc)
#34994 opened Feb 8, 2026 by bwangpj Loading…
2
feat(Topology/Category): TopCat.uliftFunctor preserves all limits and colimits large-import Automatically added label for PRs with a significant increase in transitive imports t-category-theory Category theory t-topology Topological spaces, uniform spaces, metric spaces, filters
#34993 opened Feb 8, 2026 by chrisflav Loading…
1
chore(Order): generalize some hypotheses from pos to nonneg t-algebra Algebra (groups, rings, fields, etc)
#34992 opened Feb 8, 2026 by DavidLedvinka Loading…
1
feat: continuous linear maps with a continuous left/right inverseContinuousinverse t-analysis Analysis (normed *, calculus)
#34991 opened Feb 8, 2026 by grunweg Loading…
7
feat: ContinuousSMul (∀ i, N i) (∀ i, γ i) t-topology Topological spaces, uniform spaces, metric spaces, filters
#34990 opened Feb 8, 2026 by bwangpj Loading…
4
feat: to_additive for IsHaarMeasure.comap t-measure-probability Measure theory / Probability theory
#34988 opened Feb 8, 2026 by bwangpj Loading…
1
feat: define Matrix.ProjGenLinGroup 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)
#34987 opened Feb 8, 2026 by urkud Loading…
1 task
2
feat(GeneralLinearGroup): define GeneralLinearGroup.scalar t-algebra Algebra (groups, rings, fields, etc)
#34986 opened Feb 8, 2026 by urkud Loading…
1
feat(Analysis/PSeries): add version of Cauchy condensation with weaker assumptions new-contributor This PR was made by a contributor with at most 5 merged PRs. Welcome to the community! t-analysis Analysis (normed *, calculus)
#34985 opened Feb 8, 2026 by jvanwinden Loading…
2
chore(Polynomial/Div): deprecate noncomputable Decidable non-instance t-algebra Algebra (groups, rings, fields, etc)
#34983 opened Feb 8, 2026 by plp127 Loading…
1
chore(MeasureTheory/Probability): Generalize some lemmas from Measurable to AEMeasurable t-measure-probability Measure theory / Probability theory
#34982 opened Feb 8, 2026 by DavidLedvinka Loading…
1
1
ci: set "author" explicitly in create-pull-request action CI Modifies the continuous integration setup or other automation
#34981 opened Feb 8, 2026 by bryangingechen Loading…
2
feat(Topology/Category): the standard Grothendieck topology on TopCat t-category-theory Category theory
#34979 opened Feb 8, 2026 by chrisflav Loading…
9
docs(CategoryTheory/Bicategory/Functor): clean up docstrings t-category-theory Category theory
#34978 opened Feb 8, 2026 by harahu Loading…
4
feat(CategoryTheory/Sites): a pullback-preserving functor is continuous if it preserves coverings t-category-theory Category theory
#34977 opened Feb 8, 2026 by chrisflav Loading…
2
feat(CategoryTheory/Sites): Equivalence of categories of sheaves with a dense subsite that is 1-hypercover dense t-category-theory Category theory WIP Work in progress
#34976 opened Feb 8, 2026 by joelriou Loading…
1
fix(CategoryTheory/Bicategory): correct instance target t-category-theory Category theory
#34975 opened Feb 8, 2026 by harahu Loading…
1
chore: replace Punit by PUnit
#34973 opened Feb 8, 2026 by chrisflav Loading…
2
chore: rename "Punit" to "PUnit" in definitions awaiting-CI This PR does not pass CI yet. This label is automatically removed once it does.
#34972 opened Feb 8, 2026 by grunweg Loading…
1
chore: rename "Pempty" to "PEmpty" in two definitions easy < 20s of review time. See the lifecycle page for guidelines. t-ring-theory Ring theory
#34971 opened Feb 8, 2026 by grunweg Loading…
1
perf: modulize tests (1/N) CI Modifies the continuous integration setup or other automation
#34970 opened Feb 8, 2026 by Komyyy Loading…
1
ProTip! What’s not been updated in a month: updated:<2026-01-08.