Skip to content

Pull requests: leanprover-community/mathlib4

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
Assignee
Filter by who’s assigned
Assigned to nobody Loading
Sort

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…
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…
chore: replace by exact occurences
#40223 opened Jun 4, 2026 by felixpernegger Contributor Draft
chore: reduce imports
#40222 opened Jun 4, 2026 by JovanGerb Contributor Draft
feat: add Monoid.End.equiv t-algebra Algebra (groups, rings, fields, etc)
#40221 opened Jun 4, 2026 by riccardobrasca Member Loading…
feat: add prime_units_mul and variants t-algebra Algebra (groups, rings, fields, etc)
#40220 opened Jun 4, 2026 by riccardobrasca Member Loading…
feat: add LinearIndependent.update t-algebra Algebra (groups, rings, fields, etc)
#40219 opened Jun 4, 2026 by riccardobrasca Member Loading…
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…
chore: adaptations for Aesop import reduction
#40217 opened Jun 4, 2026 by JovanGerb Contributor Loading…
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…
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
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…
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…
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…
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…
feat(Combinatorics): incidence-based HypergraphLike class
#40204 opened Jun 4, 2026 by Jun2M Collaborator Loading…
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…
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…
find_model attribute from Meta Café t-differential-geometry Manifolds etc
#40199 opened Jun 3, 2026 by scholzhannah Collaborator Draft
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…
feat: valuation of an algebraic element t-ring-theory Ring theory
#40197 opened Jun 3, 2026 by plp127 Contributor Loading…
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…
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…
ProTip! Type g i on any issue or pull request to go back to the issue listing page.