Skip to content

Pull requests: leanprover-community/mathlib4

New pull request New
1,258 Open 20,571 Closed
1,258 Open 20,571 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
Sort
Sort by
Newest Oldest Most commented Least commented Recently updated Least recently updated Best match
Most reactions
👍 👎 😄 🎉 😕 ❤️ 🚀 👀

Pull requests list

doc: fix docstring of liminf_const_add documentation Improvements or additions to documentation easy < 20s of review time. See the lifecycle page for guidelines. ready-to-merge This PR has been sent to bors. t-topology Topological spaces, uniform spaces, metric spaces, filters
#22280 opened Feb 25, 2025 by kbuzzard Loading…
4
feat(RingTheory/GradedAlgebra): homogeneous relation 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)
#22279 opened Feb 25, 2025 by xyzw12345 Loading…
2
feat(CategoryTheory/Sums/Basic): functors out of Sum large-import Automatically added label for PRs with a significant increase in transitive imports t-category-theory Category theory
#22278 opened Feb 25, 2025 by robin-carlier Loading…
1
feat: generalize rank_reindex to rectangular matrices easy < 20s of review time. See the lifecycle page for guidelines. t-data Data (lists, quotients, numbers, etc)
#22277 opened Feb 25, 2025 by eric-wieser Loading…
1
feat(CategoryTheory/Products/Associator): compatibility of associator t-category-theory Category theory
#22276 opened Feb 25, 2025 by robin-carlier Loading…
1
refactor(CategoryTheory/ConcreteCategory): concreteify NatTrans.naturality_apply t-category-theory Category theory tech debt Tracking cross-cutting technical debt, see e.g. the "Technical debt counters" stream on zulip
#22275 opened Feb 25, 2025 by Vierkantor Loading…
1
feat(CategoryTheory/MorphismProperty): If P is stable under retracts, then P respects isomorphisms. t-category-theory Category theory
#22274 opened Feb 25, 2025 by joelriou Loading…
1
feat(Simproc): simproc for ∃ a', ... ∧ a' = a ∧ ... large-import Automatically added label for PRs with a significant increase in transitive imports t-meta Tactics, attributes or user commands WIP Work in progress
#22273 opened Feb 25, 2025 by vasnesterov Loading…
1
chore(AlgebraicGeometry): clean up erw and porting notes t-algebraic-geometry Algebraic geometry tech debt Tracking cross-cutting technical debt, see e.g. the "Technical debt counters" stream on zulip
#22272 opened Feb 25, 2025 by Vierkantor Loading…
1
feat(MeasureTheory): define an additive content from a projective family of measures t-measure-probability Measure theory / Probability theory
#22271 opened Feb 25, 2025 by RemyDegenne Loading…
@EtienneC30
1
chore(Algebra):replace Submodule.quotient.mk with Submodule.mkQ
#22269 opened Feb 25, 2025 by Thmoas-Guan Loading…
2
feat: a = b → AntisymmRel r a b easy < 20s of review time. See the lifecycle page for guidelines. ready-to-merge This PR has been sent to bors. t-order Order theory
#22268 opened Feb 25, 2025 by vihdzp Loading…
8
feat(Data/Part): Add missing to_additive in Part.lean 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! t-data Data (lists, quotients, numbers, etc)
#22267 opened Feb 25, 2025 by staroperator Loading…
1
feat(Geometry/Euclidean/Angle/Unoriented): triangle inequality large-import Automatically added label for PRs with a significant increase in transitive imports t-euclidean-geometry Affine and axiomatic geometry
#22265 opened Feb 25, 2025 by Timeroot Loading…
1
feature(Analysis/Seminorm): Add closedBall equivalents of open ball results t-analysis Analysis (normed *, calculus)
#22264 opened Feb 25, 2025 by mans0954 Loading…
1
feat: Prove r_zpow 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)
#22263 opened Feb 25, 2025 by ldct Loading…
1
chore: remove automated porting warnings in Data/Set/Lattice t-data Data (lists, quotients, numbers, etc)
#22262 opened Feb 25, 2025 by kim-em Loading…
1
chore: split Algebra/BigOperators/Group/Finset/Basic
#22261 opened Feb 25, 2025 by kim-em Loading…
1
feat: Add SampleableExt PNat new-contributor This PR was made by a contributor with at most 5 merged PRs. Welcome to the community!
#22260 opened Feb 25, 2025 by ldct Loading…
1
feat(Data/Fin): add @[simp] lemmas
#22259 opened Feb 25, 2025 by urkud Loading…
3
chore(GCongr/CoreAttrs): add some List.Perm attrs easy < 20s of review time. See the lifecycle page for guidelines. t-data Data (lists, quotients, numbers, etc)
#22257 opened Feb 25, 2025 by urkud Loading…
1
feat: Metric Spaces are T6 new-contributor This PR was made by a contributor with at most 5 merged PRs. Welcome to the community!
#22256 opened Feb 25, 2025 by plp127 • Draft
7
feat: register trivial for hint t-meta Tactics, attributes or user commands
#22255 opened Feb 24, 2025 by euprunin Loading…
1
feat: $C^1$ vector fields on compact manifolds define global flows blocked-by-other-PR This PR depends on another PR to Mathlib (this label is automatically managed by a bot) t-differential-geometry Manifolds etc WIP Work in progress
#22254 opened Feb 24, 2025 by winstonyin Loading…
1 task
2
feat(Set): lemmas about set difference t-data Data (lists, quotients, numbers, etc)
#22253 opened Feb 24, 2025 by apnelson1 Loading…
2
ProTip! Updated in the last three days: updated:>2025-02-22.