Skip to content

Pull requests: leanprover-community/mathlib4

New pull request New
1,913 Open 30,932 Closed
1,913 Open 30,932 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: OrderTypes new-contributor This PR was made by a contributor with at most 5 merged PRs. Welcome to the community! t-order Order theory
#33420 opened Dec 31, 2025 by YanYablonovskiy • Draft
2
feat: Have equality form for #t - #s in addition to the inequality new-contributor This PR was made by a contributor with at most 5 merged PRs. Welcome to the community! t-data Data (lists, quotients, numbers, etc)
#33419 opened Dec 31, 2025 by R-Peleg Loading…
2
refactor(RingTheory/Ideal/Basic): clean up proofs t-algebra Algebra (groups, rings, fields, etc) t-ring-theory Ring theory
#33418 opened Dec 31, 2025 by tb65536 Loading…
1
feat: {Continuous}Linear{Isometry}Equiv.conj{Continuous, Star}AlgEquiv are "almost" injective 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)
#33417 opened Dec 31, 2025 by themathqueen Loading…
1 task
2
chore(Order/GameAdd): add elab_as_elim attributes t-order Order theory
#33416 opened Dec 31, 2025 by vihdzp Loading…
1
chore(Analysis/SchwartzSpace): explicit variables for derivCLM and fderivCLM t-analysis Analysis (normed *, calculus)
#33415 opened Dec 30, 2025 by mcdoll Loading…
1
feat(Topology/Separation/NotNormal): generalize to non-separable spaces t-topology Topological spaces, uniform spaces, metric spaces, filters
#33414 opened Dec 30, 2025 by peakpoint Loading…
1
chore(Order/WithBot): rename some theorems t-order Order theory
#33413 opened Dec 30, 2025 by vihdzp Loading…
1
chore(CategoryTheory/Pi/Monoidal): monoidal Functor.pi and Functor.pi' t-category-theory Category theory
#33412 opened Dec 30, 2025 by robin-carlier Loading…
1
feat(Analysis/DiscreteConvolution): Discrete convolution API basics new-contributor This PR was made by a contributor with at most 5 merged PRs. Welcome to the community! t-analysis Analysis (normed *, calculus)
#33411 opened Dec 30, 2025 by IlPreteRosso Loading…
2
feat(LinearAlgebra/AffineSpace/Ceva): Ceva's theorem t-algebra Algebra (groups, rings, fields, etc)
#33409 opened Dec 30, 2025 by jsm28 Loading…
1
feat: add basics of majorization blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot)
#33406 opened Dec 30, 2025 by dupuisf Loading…
1 task
2
chore(Algebra): move LinearMap.mul{Left, Right, LeftRight} to earlier file t-algebra Algebra (groups, rings, fields, etc)
#33405 opened Dec 30, 2025 by themathqueen Loading…
3
feat(Analysis/SchwartzSpace): scalar multiplication with linear factors t-analysis Analysis (normed *, calculus)
#33404 opened Dec 30, 2025 by mcdoll Loading…
1 task done
3
feat(GroupTheory/FiniteAbelian): prove that the restriction map is surjective
#33403 opened Dec 30, 2025 by xroblot Loading…
1
feat(LinearAlgebra/Transvection/Generation): prove exceptional case in Dieudonné's theorem blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) file-removed A Lean module was (re)moved without a `deprecated_module` annotation t-algebra Algebra (groups, rings, fields, etc)
#33402 opened Dec 30, 2025 by AntoineChambert-Loir Loading…
5 tasks
2
feat: IsStrictOrderedRing (Lex R⟦Γ⟧) large-import Automatically added label for PRs with a significant increase in transitive imports t-ring-theory Ring theory
#33398 opened Dec 30, 2025 by vihdzp Loading…
1
feat(Algebra/Star/LinearMap): intrinsic star for continuous linear maps large-import Automatically added label for PRs with a significant increase in transitive imports t-algebra Algebra (groups, rings, fields, etc)
#33397 opened Dec 30, 2025 by themathqueen Loading…
1
feat: add lemmas about doubly stochastic matrices t-analysis Analysis (normed *, calculus)
#33394 opened Dec 30, 2025 by dupuisf Loading…
1
experiment: more commandStart linter exceptions awaiting-CI This PR doesn't pass CI yet. This label is automatically removed once it does. 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
#33393 opened Dec 29, 2025 by grunweg Loading…
1 task
3
feat(LinearAlgebra/Transvection/Generation): non-exceptional case in Dieudonné's theorem blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) file-removed A Lean module was (re)moved without a `deprecated_module` annotation t-algebra Algebra (groups, rings, fields, etc)
#33392 opened Dec 29, 2025 by AntoineChambert-Loir Loading…
4 tasks
2
feat(RingTheory/Ideal): generalize Submodule.colon to sets new-contributor This PR was made by a contributor with at most 5 merged PRs. Welcome to the community! t-ring-theory Ring theory WIP Work in progress
#33390 opened Dec 29, 2025 by farmanb Loading…
2
feat(Mathlib/Analysis/SpecialFunctions/Log/Base): More log asymptotics new-contributor This PR was made by a contributor with at most 5 merged PRs. Welcome to the community! t-analysis Analysis (normed *, calculus)
#33389 opened Dec 29, 2025 by khwilson Loading…
2
doc(docs/100.yaml): add recently-proven theorems awaiting-author A reviewer has asked the author a question or requested changes. easy < 20s of review time. See the lifecycle page for guidelines. new-contributor This PR was made by a contributor with at most 5 merged PRs. Welcome to the community!
#33388 opened Dec 29, 2025 by plby Loading…
10
chore(LinearAlgebra/Transvection/Basic): mv Transvection.lean file to Transvection.Basic.lean blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) file-removed A Lean module was (re)moved without a `deprecated_module` annotation t-algebra Algebra (groups, rings, fields, etc)
#33387 opened Dec 29, 2025 by AntoineChambert-Loir Loading…
2 tasks
2
ProTip! Adding no:label will show everything without a label.