Skip to content

Pull requests: leanprover-community/mathlib4

New pull request New
2,666 Open 37,399 Closed
2,666 Open 37,399 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: Cartan's formula of Value Distribution Theory t-analysis Analysis (normed *, calculus)
#40696 opened Jun 17, 2026 by kebekus Collaborator • Draft
1
feat(Topology/Semicontinuity/Hemicontinuity): intersections with compact absolutely convex sets large-import Automatically added label for PRs with a significant increase in transitive imports t-topology Topological spaces, uniform spaces, metric spaces, filters
#40695 opened Jun 17, 2026 by khwilson Contributor Loading…
1 task
2
feat(Algebra/Group/Hom): upgrade a MulHom to a MonoidHom when codomain is left-cancellative t-algebra Algebra (groups, rings, fields, etc)
#40694 opened Jun 17, 2026 by pechersky Contributor Loading…
1
feat(GroupTheory): generalize GrothendieckGroup to take a CommSemigroup blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) t-group-theory Group theory
#40693 opened Jun 17, 2026 by pechersky Contributor Loading…
5 tasks
2
feat(GroupTheory/Finite): torsion free and FG WithOne M is when M is t-group-theory Group theory
#40692 opened Jun 17, 2026 by pechersky Contributor Loading…
1 task
2
feat(Algebra/Group/WithOne): lift_symm_injective easy < 20s of review time. See the lifecycle page for guidelines. t-algebra Algebra (groups, rings, fields, etc)
#40691 opened Jun 17, 2026 by pechersky Contributor Loading…
1
feat(Algebra/Group): characterize Monoid npow as semigroup iterated mul t-algebra Algebra (groups, rings, fields, etc)
#40690 opened Jun 17, 2026 by pechersky Contributor Loading…
1
feat(Algebra/Group/WithOne): isFooCancel when source is t-algebra Algebra (groups, rings, fields, etc)
#40689 opened Jun 17, 2026 by pechersky Contributor Loading…
1
feat(Algebra/Group/WithOne): Subsingleton when IsEmpty source
#40688 opened Jun 17, 2026 by pechersky Contributor Loading…
2
feat(Analysis/ODE): uniqueness of integral curves on intervals and intersections new-contributor This PR was made by a contributor with at most 5 merged PRs. Welcome to the community! t-analysis Analysis (normed *, calculus)
#40687 opened Jun 17, 2026 by michaellee94 Collaborator Loading…
@mcdoll
2
feat(Analysis/Matrix): prove Hadamard's determinant inequality
#40683 opened Jun 16, 2026 by dennj Contributor Loading…
2
doc: add wikidata attributes LLM-generated PRs with substantial input from LLMs - review accordingly WIP Work in progress
#40682 opened Jun 16, 2026 by Deicyde Contributor Loading…
39
feat(wip): code action testing infrastructure t-meta Tactics, attributes or user commands
#40681 opened Jun 16, 2026 by thorimur Contributor • Draft
3
chore: remove redudant nolint simpNF
#40680 opened Jun 16, 2026 by felixpernegger Contributor Loading…
4
feat(Tactic): setm tactic t-meta Tactics, attributes or user commands
#40679 opened Jun 16, 2026 by lua-vr Contributor • Draft
3
ci(cache): consolidate cache fetching into one action, warmed from master CI Modifies the continuous integration setup or other automation
#40678 opened Jun 16, 2026 by marcelolynch Contributor Loading…
1
chore: update Data.PFunctor.Univariate.M docstring with example usage 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)
#40677 opened Jun 16, 2026 by nrs-status Contributor Loading…
11
chore: add deprecations for Data/Set/{Accumulate,Dissipate}
#40676 opened Jun 16, 2026 by grunweg Contributor Loading…
1 task done
4
feat(Topology): iff version of many .prodMap lemmas 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-topology Topological spaces, uniform spaces, metric spaces, filters
#40673 opened Jun 16, 2026 by ADedecker Member Loading…
1 task
2
perf(Algebra/Group/Action/Defs): don't exposeMul.toSMulMulOpposite awaiting-CI This PR does not pass CI yet. This label is automatically removed once it does. t-algebra Algebra (groups, rings, fields, etc)
#40672 opened Jun 16, 2026 by JovanGerb Contributor Loading…
3
chore(Algebra/Ring/Periodic): automated extraction from #38483 maintainer-merge A reviewer has approved the changed; awaiting maintainer approval. t-algebra Algebra (groups, rings, fields, etc)
#40669 opened Jun 16, 2026 by mathlib-splicebot Bot Loading…
3
chore(Tactic/Linarith/Parsing): remove local abbrev for TreeMap maintainer-merge A reviewer has approved the changed; awaiting maintainer approval. t-meta Tactics, attributes or user commands
#40668 opened Jun 16, 2026 by JovanGerb Contributor Loading…
3
feat(Combinatorics/SimpleGraph/Paths): p.IsPath → p.dropLast.IsPath easy < 20s of review time. See the lifecycle page for guidelines. t-combinatorics Combinatorics
#40667 opened Jun 16, 2026 by SnirBroshi Collaborator Loading…
2
chore(Matrix/GeneralLinearGroup/Projective): sort out namespace and golf the proof large-import Automatically added label for PRs with a significant increase in transitive imports t-group-theory Group theory
#40666 opened Jun 16, 2026 by Whysoserioushah Collaborator Loading…
1
feat(RepresentationTheory): the character values of a finite group are algebraic integers LLM-generated PRs with substantial input from LLMs - review accordingly t-algebra Algebra (groups, rings, fields, etc)
#40665 opened Jun 16, 2026 by Yu-Misaka Collaborator Loading…
5
ProTip! Follow long discussions with comments:>50.