Skip to content

Pull requests: leanprover-community/mathlib4

New pull request New
2,324 Open 34,696 Closed
2,324 Open 34,696 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(Algebra/Algebra/Operations): add Submodule.mul_eq_bot 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)
#37626 opened Apr 4, 2026 by NoahW314 Loading…
2
feat(LinearAlgebra/Matrix/Charpoly): general coefficient formula as sum of principal minors 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)
#37625 opened Apr 3, 2026 by slavanaprienko Loading…
4
feat(Combinatorics/SimpleGraph/Maps): add theorems about composition t-combinatorics Combinatorics
#37624 opened Apr 3, 2026 by IvanRenison Loading…
1
feat(Order/RelIso): add theorems about RelHom.comp and RelEmbedding.trans t-order Order theory
#37623 opened Apr 3, 2026 by IvanRenison Loading…
4
feat: trace-nilpotency criterion t-algebra Algebra (groups, rings, fields, etc)
#37622 opened Apr 3, 2026 by jano-wol Loading…
1
feat(Analysis/Asymptotics): if u is eventually positive and u ~ v then v is eventually positive t-analysis Analysis (normed *, calculus)
#37621 opened Apr 3, 2026 by vasnesterov Loading…
2
feat(Combinatorics/Graph): Add Graph intersection operations t-combinatorics Combinatorics
#37620 opened Apr 3, 2026 by Jun2M Loading…
5
feat(topology): Small inductive dimension t-topology Topological spaces, uniform spaces, metric spaces, filters
#37619 opened Apr 3, 2026 by FernandoChu Loading…
3
feat(PowerSeries): rename a power series as multivariate power series 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-ring-theory Ring theory
#37618 opened Apr 3, 2026 by WenrongZou Loading…
1 task done
2
doc(FieldTheory): avoid lazy continuation lines t-algebra Algebra (groups, rings, fields, etc)
#37617 opened Apr 3, 2026 by harahu Loading…
1
fix(GroupTheory): avoid unintentional list item continuation lines t-group-theory Group theory
#37615 opened Apr 3, 2026 by harahu Loading…
@tb65536
1
feat: notation for UniformConvergenceCLM t-topology Topological spaces, uniform spaces, metric spaces, filters
#37614 opened Apr 3, 2026 by ADedecker Loading…
1
chore: move files to new Topology.Algebra.Module.Spaces subfolder file-removed A Lean module was (re)moved without a `deprecated_module` annotation merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) t-topology Topological spaces, uniform spaces, metric spaces, filters
#37613 opened Apr 3, 2026 by ADedecker Loading…
2
feat(ContinuousFunctionalCalculus): add integral representation for x ↦ x ^ p for p ∈ (1, 2) t-analysis Analysis (normed *, calculus)
#37612 opened Apr 3, 2026 by dupuisf Loading…
@j-loreaux
2
feat(Combinatorics/Graph): add OrderBot instance for Graph t-combinatorics Combinatorics
#37610 opened Apr 3, 2026 by Jun2M Loading…
1
feat: use a constructor for NNReal t-data Data (lists, quotients, numbers, etc)
#37609 opened Apr 3, 2026 by sgouezel Loading…
1
chore: don't expose the definition of nnnorm t-analysis Analysis (normed *, calculus)
#37608 opened Apr 3, 2026 by sgouezel Loading…
1
feat(AlgebraicTopology/SimplicialSet): connected components of simplicial sets blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) t-algebraic-topology Algebraic topology
#37607 opened Apr 3, 2026 by joelriou Loading…
1 task
2
feat: Add Function.prod and Function.diag
#37606 opened Apr 3, 2026 by linesthatinterlace Loading…
5
feat: pushing Lattice and predecessors through Equiv
#37605 opened Apr 3, 2026 by Parcly-Taxel Loading…
3
feat: fun_prop lemmas for GL n R and SL n R t-topology Topological spaces, uniform spaces, metric spaces, filters
#37604 opened Apr 3, 2026 by j-loreaux Loading…
13
refactor: SetSemiring as a 1-field structure 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
#37603 opened Apr 3, 2026 by Parcly-Taxel Loading…
2 tasks
7
feat(NumberTheory/ModularForms): arithmetic subgroups act properly discontinuously 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
#37602 opened Apr 3, 2026 by loefflerd Loading…
1 task
2
feat(Topology/Algebra/Group/Matrix): refactor; continuity of maps on GL(n) and SL(n) t-topology Topological spaces, uniform spaces, metric spaces, filters
#37601 opened Apr 3, 2026 by loefflerd Loading…
1
chore: use inferInstanceAs to define the distance on padic integers t-number-theory Number theory (also use t-algebra or t-analysis to specialize)
#37599 opened Apr 3, 2026 by sgouezel Loading…
@MichaelStollBayreuth
1
ProTip! Add no:assignee to see everything that’s not assigned.