Skip to content

Pull requests: leanprover-community/mathlib4

New pull request New
2,745 Open 38,010 Closed
2,745 Open 38,010 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

chore: reduce import all
#41389 opened Jul 5, 2026 by felixpernegger Contributor Loading…
1
feat(Data/Set): add mono of right inv t-data Data (lists, quotients, numbers, etc)
#41388 opened Jul 5, 2026 by emlis42 Contributor Loading…
1
chore: remove redundant open Classical in
#41387 opened Jul 5, 2026 by felixpernegger Contributor Loading…
2
feat: lemma enorm_toReal easy < 20s of review time. See the lifecycle page for guidelines. t-analysis Analysis (normed *, calculus)
#41386 opened Jul 5, 2026 by sgouezel Contributor Loading…
1
chore(Topology/Order/OrderClosed): add label to hypothesis [NeBot _] easy < 20s of review time. See the lifecycle page for guidelines. t-topology Topological spaces, uniform spaces, metric spaces, filters
#41385 opened Jul 5, 2026 by themathqueen Collaborator Loading…
1
feat(Algebra/Category/ModuleCat): the category of sheaves of modules is Grothendieck abelian t-category-theory Category theory
#41383 opened Jul 5, 2026 by joelriou Contributor Loading…
1
chore: remove (all) redundant backward.privateInPublic.warn exceptions tech debt Tracking cross-cutting technical debt, see e.g. the "Technical debt counters" stream on zulip
#41382 opened Jul 5, 2026 by felixpernegger Contributor Loading…
1
feat(Combinatorics/SimpleGraph/Girth): egirth and (cycleGraph n).Free blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) t-combinatorics Combinatorics
#41381 opened Jul 5, 2026 by SnirBroshi Collaborator Loading…
4 tasks
2
feat(Combinatorics/SimpleGraph/Girth): relate girth and egirth t-combinatorics Combinatorics
#41380 opened Jul 5, 2026 by SnirBroshi Collaborator Loading…
1
chore(RingTheory/*): remove domain assumptions by generalizing from torsion free to faithful smul t-algebra Algebra (groups, rings, fields, etc) t-ring-theory Ring theory
#41379 opened Jul 5, 2026 by tb65536 Contributor Loading…
3
chore(RingTheory/QuasiFinite/Basic): extract instance from ramification proof t-algebra Algebra (groups, rings, fields, etc) t-ring-theory Ring theory
#41378 opened Jul 5, 2026 by tb65536 Contributor Loading…
1
refactor(RingTheory/RamificationInertia/Ramification): generalize ramificationIdx_pos blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) t-algebra Algebra (groups, rings, fields, etc) t-ring-theory Ring theory
#41377 opened Jul 5, 2026 by tb65536 Contributor Loading…
2 tasks
2
feat(Topology/Algebra/Group/Basic,Algebra/Group/Pointwise/Set/Basic): add Filter.map_{sub,div}{Left,Right}_nhds{,LT,GT,NE}
#41376 opened Jul 5, 2026 by teorth Contributor Loading…
2
feat(Analysis/SpecialFunctions/Pow/Asymptotics): add Real.tendsto_rpow_atTop_of_base_gt_one t-analysis Analysis (normed *, calculus)
#41375 opened Jul 4, 2026 by teorth Contributor Loading…
1
chore(SimpleGraph/Girth): namespace egirth_le_length under IsCycle t-combinatorics Combinatorics
#41374 opened Jul 4, 2026 by SnirBroshi Collaborator Loading…
1
feat(SimpleGraph): some CliqueFree/Free lemmas t-combinatorics Combinatorics
#41373 opened Jul 4, 2026 by SnirBroshi Collaborator Loading…
1
feat(Data/ENat/Basic): coe versions of m + 1 ≤ n ↔ m < n t-data Data (lists, quotients, numbers, etc)
#41372 opened Jul 4, 2026 by SnirBroshi Collaborator Loading…
1
feat(Order/SuccPred): succ a ≤ b ↔ a < b when b is not maximal t-order Order theory
#41371 opened Jul 4, 2026 by SnirBroshi Collaborator Loading…
1
fix(Tactic/FunProp): resolve names to be unfolded maintainer-merge A reviewer has approved the changed; awaiting maintainer approval. t-meta Tactics, attributes or user commands
#41370 opened Jul 4, 2026 by gasparattila Contributor Loading…
@joneugster
3
feat(RingTheory/Localization/Ideal): generalize IsLocalization.isMaximal_of_isMaximal_disjoint t-algebra Algebra (groups, rings, fields, etc) t-ring-theory Ring theory
#41369 opened Jul 4, 2026 by tb65536 Contributor Loading…
1
chore(RingTheory/Localization/AtPrime/Extension): switch over to new definition of inertiaDeg awaiting-CI This PR does not pass CI yet. This label is automatically removed once it does. blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) t-algebra Algebra (groups, rings, fields, etc) t-ring-theory Ring theory
#41368 opened Jul 4, 2026 by tb65536 Contributor Loading…
1 task
2
feat(CategoryTheory/Functor): stability of Leibniz pushouts under cobase change merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) WIP Work in progress
#41367 opened Jul 4, 2026 by mckoen Collaborator Loading…
chore(Algebra/SkewPolynomial): rename the conversion functions to coeff/ofCoeff t-algebra Algebra (groups, rings, fields, etc)
#41365 opened Jul 4, 2026 by YaelDillies Contributor Loading…
1
chore(SimpleGraph/Clique): tidy CliqueFree iff lemmas t-combinatorics Combinatorics
#41364 opened Jul 4, 2026 by SnirBroshi Collaborator Loading…
1
perf(Algebra/MonoidAlgebra): no_expose the Add instance
#41362 opened Jul 4, 2026 by JovanGerb Contributor • Draft
5
ProTip! Adding no:label will show everything without a label.