Skip to content

Pull requests: leanprover-community/mathlib4

New pull request New
1,605 Open 24,214 Closed
1,605 Open 24,214 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: beta distribution new-contributor This PR was made by a contributor with at most 5 merged PRs. Welcome to the community! t-measure-probability Measure theory / Probability theory
#26325 opened Jun 23, 2025 by TOMILO87 Loading…
2
refactor: move the definition of IsRegular earlier maintainer-merge t-algebra Algebra (groups, rings, fields, etc)
#26321 opened Jun 23, 2025 by eric-wieser Loading…
4
chore: weaken hypotheses for a Gaussian measure to be a probability measure t-measure-probability Measure theory / Probability theory
#26320 opened Jun 23, 2025 by EtienneC30 Loading…
1
ci: specify leanprover-community/mathlib4 when checking out master CI Modifies the continuous integration / deployment setup
#26319 opened Jun 23, 2025 by Vierkantor Loading…
1
feat: add BooleanσAlgebra awaiting-author A reviewer has asked the author a question or requested changes. new-contributor This PR was made by a contributor with at most 5 merged PRs. Welcome to the community! t-order Order theory
#26318 opened Jun 23, 2025 by PierreQuinton Loading…
3
feat: norm_num plugin for Nat.clog t-meta Tactics, attributes or user commands
#26317 opened Jun 23, 2025 by plp127 Loading…
1
feat(RingTheory): degree of rational function field extension t-algebra Algebra (groups, rings, fields, etc)
#26316 opened Jun 23, 2025 by alreadydone Loading…
@riccardobrasca
2
feat: continuous bilinear forms blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) t-analysis Analysis (normed *, calculus)
#26315 opened Jun 23, 2025 by EtienneC30 Loading…
1 task
2
feat: Finsupp.supportedEquivFinsupp_symm_single t-algebra Algebra (groups, rings, fields, etc)
#26314 opened Jun 23, 2025 by kckennylau Loading…
7
feat: 4 lemmas about Finsupp.mapDomain.linearEquiv t-algebra Algebra (groups, rings, fields, etc)
#26313 opened Jun 23, 2025 by kckennylau Loading…
5
feat: Finsupp.degree_eq_sum t-data Data (lists, quotients, numbers, etc)
#26312 opened Jun 23, 2025 by kckennylau Loading…
1
(WIP) Binary form t-algebra Algebra (groups, rings, fields, etc)
#26310 opened Jun 23, 2025 by kckennylau Loading…
3 tasks
5
chore(Data/Finsupp/Basic): split file t-data Data (lists, quotients, numbers, etc) tech debt Tracking cross-cutting technical debt, see e.g. the "Technical debt counters" stream on zulip
#26309 opened Jun 23, 2025 by BoltonBailey Loading…
4
feat(Analysis.NormedSpace): add normalized vectors new-contributor This PR was made by a contributor with at most 5 merged PRs. Welcome to the community! t-analysis Analysis (normed *, calculus)
#26308 opened Jun 23, 2025 by LessnessRandomness Loading…
1
refactor: make IsIdempotentElem a one-field structure large-import Automatically added label for PRs with a significant increase in transitive imports t-algebra Algebra (groups, rings, fields, etc)
#26307 opened Jun 23, 2025 by j-loreaux • Draft
1
refactor: make IsSelfAdjoint a one-field structure.
#26306 opened Jun 23, 2025 by j-loreaux • Draft
1
feat(AlgebraicGeometry): Definition of algebraic cycles blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) RFC Request for comment
#26304 opened Jun 23, 2025 by Raph-DG Loading…
2 tasks
2
feat(AlgebraicTopology): the fundamental lemma of homotopical algebra 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-category-theory Category theory WIP Work in progress
#26303 opened Jun 23, 2025 by joelriou Loading…
2 tasks
2
feat: introduce the Laplace operator t-analysis Analysis (normed *, calculus)
#26302 opened Jun 23, 2025 by kebekus Loading…
3
feat(LinearAlgebra/Matrix/Determinant/TotallyUnimodular): 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)
#26301 opened Jun 23, 2025 by Ivan-Sergeyev Loading…
1
feat(Analysis/Calculus/FDeriv): continuous differentiability from continuous partial derivatives on an open domain in a product space new-contributor This PR was made by a contributor with at most 5 merged PRs. Welcome to the community! t-analysis Analysis (normed *, calculus)
#26300 opened Jun 23, 2025 by igorkhavkine Loading…
2 tasks done
2
perf: the commandStart linter only acts on modified files t-linter Linter
#26299 opened Jun 23, 2025 by adomani Loading…
4
test: the commandStart linter only acts on modified files. awaiting-author A reviewer has asked the author a question or requested changes. WIP Work in progress
#26298 opened Jun 23, 2025 by adomani • Draft
16
feat(RingTheory): lemmas about TensorProduct and IsBaseChange t-algebra Algebra (groups, rings, fields, etc)
#26297 opened Jun 23, 2025 by mbkybky Loading…
1
feat: closure of rationals in real intervals t-topology Topological spaces, uniform spaces, metric spaces, filters
#26296 opened Jun 23, 2025 by alreadydone Loading…
1
ProTip! Exclude everything labeled bug with -label:bug.