Skip to content

Pull requests: leanprover-community/mathlib4

New pull request New
2,586 Open 37,012 Closed
2,586 Open 37,012 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(RingTheory/LaurentSeries): leibniz product rule for derivative new-contributor This PR was made by a contributor with at most 5 merged PRs. Welcome to the community! t-ring-theory Ring theory
#40225 opened Jun 4, 2026 by localparty Loading…
3
feat(Tactic/Group): strengthen the group tactic and add tests new-contributor This PR was made by a contributor with at most 5 merged PRs. Welcome to the community! t-meta Tactics, attributes or user commands WIP Work in progress
#40224 opened Jun 4, 2026 by AlexBrodbelt Collaborator Loading…
3
chore: replace by exact occurences
#40223 opened Jun 4, 2026 by felixpernegger Contributor • Draft
2
chore: reduce imports
#40222 opened Jun 4, 2026 by JovanGerb Contributor • Draft
3
feat: add Monoid.End.equiv t-algebra Algebra (groups, rings, fields, etc)
#40221 opened Jun 4, 2026 by riccardobrasca Member Loading…
1
feat: add prime_units_mul and variants t-algebra Algebra (groups, rings, fields, etc)
#40220 opened Jun 4, 2026 by riccardobrasca Member Loading…
1
feat: add LinearIndependent.update t-algebra Algebra (groups, rings, fields, etc)
#40219 opened Jun 4, 2026 by riccardobrasca Member Loading…
1
doc(RingTheory/DedekindDomain/LinearDisjoint): fix typos in the module docstring documentation Improvements or additions to documentation t-ring-theory Ring theory
#40218 opened Jun 4, 2026 by mbkybky Collaborator Loading…
2
chore: adaptations for Aesop import reduction
#40217 opened Jun 4, 2026 by JovanGerb Contributor Loading…
3
chore(Data/{FunLike/SetLike}): unprime coe_injective' awaiting-CI This PR does not pass CI yet. This label is automatically removed once it does. t-data Data (lists, quotients, numbers, etc)
#40215 opened Jun 4, 2026 by YaelDillies Contributor Loading…
@Vierkantor
1
chore: omega to lia replacements that require unfolding min/max
#40214 opened Jun 4, 2026 by chenson2018 Contributor • Draft
1
feat(Topology/MetricSpace): the L^1 direct sum of metric spaces t-topology Topological spaces, uniform spaces, metric spaces, filters
#40212 opened Jun 4, 2026 by YaelDillies Contributor Loading…
1 task done
6
chore(Data/Finsupp/Order): add Finsupp.support_add_eq' for canonically ordered Finsupps 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)
#40210 opened Jun 4, 2026 by Yu-Misaka Collaborator Loading…
@faenuccio
12
feat: measurability of positive and negative parts delegated This pull request has been delegated to the PR author (or occasionally another non-maintainer). ready-to-merge This PR has been sent to bors. t-measure-probability Measure theory / Probability theory
#40209 opened Jun 4, 2026 by kebekus Collaborator Loading…
4
chore: expire delegations if later pushes touch sensitive files CI Modifies the continuous integration setup or other automation maintainer-merge A reviewer has approved the changed; awaiting maintainer approval.
#40207 opened Jun 4, 2026 by bryangingechen Contributor Loading…
3
feat(RingTheory/MvPowerSeries): multivariable power series ring is a noetherian ring when the index is finite large-import Automatically added label for PRs with a significant increase in transitive imports t-ring-theory Ring theory
#40205 opened Jun 4, 2026 by BryceT233 Contributor Loading…
1
feat(Combinatorics): incidence-based HypergraphLike class
#40204 opened Jun 4, 2026 by Jun2M Collaborator Loading…
2
feat(Geometry/Manifold/Diffeomorph): A diffeomorphism induces a manifold
#40202 opened Jun 3, 2026 by Bergschaf Collaborator Loading…
3
feat: lemmas about Matrix is symmetric iff bilinear form is symmetric 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)
#40201 opened Jun 3, 2026 by gw90 Contributor Loading…
@themathqueen
23
feat(FinitelyPresentedGroup): add definitional equivalence with generating set given by S : Set G large-import Automatically added label for PRs with a significant increase in transitive imports new-contributor This PR was made by a contributor with at most 5 merged PRs. Welcome to the community! t-group-theory Group theory
#40200 opened Jun 3, 2026 by AlecsFerra Loading…
@tb65536
5
find_model attribute from Meta Café t-differential-geometry Manifolds etc
#40199 opened Jun 3, 2026 by scholzhannah Collaborator • Draft
1
feat: more API for integrals wrt vector measures awaiting-author A reviewer has asked the author a question or requested changes. t-measure-probability Measure theory / Probability theory
#40198 opened Jun 3, 2026 by sgouezel Contributor Loading…
@EtienneC30
10
feat: valuation of an algebraic element t-ring-theory Ring theory
#40197 opened Jun 3, 2026 by plp127 Contributor Loading…
1
feat(Algebra/Module/LocalizedModule): generalize smul'_mk easy < 20s of review time. See the lifecycle page for guidelines. t-algebra Algebra (groups, rings, fields, etc)
#40196 opened Jun 3, 2026 by eric-wieser Member Loading…
1
feat(LinearAlgebra/Dual): identify the range of a dual map 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)
#40195 opened Jun 3, 2026 by mathnerdwhouseschatgpt Loading…
3
ProTip! Type g i on any issue or pull request to go back to the issue listing page.