Skip to content

Pull requests: leanprover-community/mathlib4

New pull request New
1,535 Open 23,552 Closed
1,535 Open 23,552 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

refactor(Geometry/Euclidean/Projection): redefine projection and reflection for affine subspaces new-contributor This PR was made by a contributor with at most 5 merged PRs. Welcome to the community! t-euclidean-geometry Affine and axiomatic geometry
#25578 opened Jun 8, 2025 by peakpoint Loading…
1
perf: replace measurability by fun_prop bench-after-CI Once the PR passes CI, comment `!bench` on the PR t-measure-probability Measure theory / Probability theory
#25577 opened Jun 8, 2025 by plp127 Loading…
2
feat(SetTheory/Cardinal): relate nonemptiness of a set to its cardinality easy < 20s of review time. See the lifecycle page for guidelines. t-set-theory Set theory
#25576 opened Jun 7, 2025 by b-mehta Loading…
1
feat(SimpleGraph): ext for walks based on getVert and support t-combinatorics Combinatorics
#25575 opened Jun 7, 2025 by Rida-Hamadani Loading…
6
feat(Cardinal/Finite): ENat powers and cardinality t-data Data (lists, quotients, numbers, etc) t-set-theory Set theory
#25574 opened Jun 7, 2025 by D-Thomine Loading…
1
feat: define ∃ x > y, ... notation to mean ∃ x, y < x ∧ ... t-meta Tactics, attributes or user commands
#25573 opened Jun 7, 2025 by JovanGerb • Draft
1
docs(LinearAlgebra/Matrix/ToLin): fix docstring documentation Improvements or additions to documentation easy < 20s of review time. See the lifecycle page for guidelines. t-algebra Algebra (groups, rings, fields, etc)
#25571 opened Jun 7, 2025 by plp127 Loading…
1
feat(Bicategory/Functor/LocallyDiscrete): add Functor.toPseudofunctor t-category-theory Category theory
#25569 opened Jun 7, 2025 by callesonne Loading…
1
feat(CategoryTheory/Bicategory/NaturalTransformations): strong and lax natural transformations of lax functors t-category-theory Category theory
#25565 opened Jun 7, 2025 by robin-carlier Loading…
13
feat(Topology/Algebra/Module): interaction between ContinuousLinearMap.coprod and ContinuousLinearEquiv.prodComm awaiting-author A reviewer has asked the author a question or requested changes. t-analysis Analysis (normed *, calculus)
#25564 opened Jun 7, 2025 by igorkhavkine Loading…
4
style: move Topology.StoneCech into Topology.Compactification t-topology Topological spaces, uniform spaces, metric spaces, filters
#25563 opened Jun 7, 2025 by Komyyy Loading…
1
feat(Analysis/Normed/Operator): continuity of forming ContinuousLinearMap coproducts pointwise awaiting-author A reviewer has asked the author a question or requested changes. t-analysis Analysis (normed *, calculus)
#25562 opened Jun 7, 2025 by igorkhavkine Loading…
2
feat(Category/Grpd): define the bicategory of groupoids t-category-theory Category theory
#25561 opened Jun 7, 2025 by callesonne Loading…
3
chore: split Mathlib/Topology/Algebra/RestrictedProduct file-removed A Lean module was (re)moved without a `deprecated_module` annotation t-topology Topological spaces, uniform spaces, metric spaces, filters
#25558 opened Jun 7, 2025 by kbuzzard Loading…
3
feat(Data.Nat.LogFueled): fueled version of clog t-data Data (lists, quotients, numbers, etc) WIP Work in progress
#25557 opened Jun 7, 2025 by AntoineChambert-Loir Loading…
1
chore: remove >6 month old material in Deprecated file-removed A Lean module was (re)moved without a `deprecated_module` annotation tech debt Tracking cross-cutting technical debt, see e.g. the "Technical debt counters" stream on zulip
#25556 opened Jun 7, 2025 by Parcly-Taxel Loading…
1
feat(Finset/SymmDiff): add additional api lemmas easy < 20s of review time. See the lifecycle page for guidelines. t-data Data (lists, quotients, numbers, etc)
#25553 opened Jun 7, 2025 by b-mehta Loading…
4
doc: explain the fields of MonadWriter documentation Improvements or additions to documentation t-data Data (lists, quotients, numbers, etc)
#25550 opened Jun 6, 2025 by eric-wieser Loading…
1
refactor(CategoryTheory/Monoidal): define Mon_.Hom using type class IsMon_Hom t-category-theory Category theory
#25549 opened Jun 6, 2025 by yuma-mizuno Loading…
4
chore(CategoryTheory/Limits/Shape/End): define coends t-category-theory Category theory
#25548 opened Jun 6, 2025 by robin-carlier Loading…
1
refactor(CategoryTheory/Monoidal/Mod_): refactor Mod_ using MonoidalLeftAction blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) t-category-theory Category theory
#25545 opened Jun 6, 2025 by robin-carlier Loading…
1 task
2
fix(PR summary): use hash instead of branch name CI Modifies the continuous integration / deployment setup delegated
#25544 opened Jun 6, 2025 by adomani Loading…
7
feat(MeasureTheory/Measure): bound Hausdorff measure under orthogonal projection 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
#25543 opened Jun 6, 2025 by FrankieNC Loading…
11
test: changes for PR summary large-import Automatically added label for PRs with a significant increase in transitive imports
#25540 opened Jun 6, 2025 by adomani Loading…
feat(number_theory/legendre_symbol): Add sqrt‐of‐residue theorems for p=4k+3 and p=8k+5 new-contributor This PR was made by a contributor with at most 5 merged PRs. Welcome to the community!
#25537 opened Jun 6, 2025 by literandltx Loading…
ProTip! no:milestone will show everything without a milestone.