Skip to content

Pull requests: leanprover-community/mathlib4

New pull request New
2,291 Open 34,589 Closed
2,291 Open 34,589 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: remove an instance diamond in homotopy groups
#37485 opened Apr 1, 2026 by sgouezel Loading…
1
feat(RingTheory/Finiteness): Improve fg_induction t-ring-theory Ring theory
#37484 opened Apr 1, 2026 by martinwintermath Loading…
1
chore(RepresentationTheory): regeneralise Rep.subrepresentation to Monoid CFT Part of the ongoing formalisation of class field theory easy < 20s of review time. See the lifecycle page for guidelines. t-algebra Algebra (groups, rings, fields, etc)
#37483 opened Apr 1, 2026 by YaelDillies Loading…
1
chore: test two consecutive simps in the flexible linter easy < 20s of review time. See the lifecycle page for guidelines.
#37482 opened Apr 1, 2026 by grunweg Loading…
1
chore: remove double instance on CommRing (SeparationQuotient α) t-topology Topological spaces, uniform spaces, metric spaces, filters
#37481 opened Apr 1, 2026 by sgouezel Loading…
2
feat(AlgebraicTopology): homology of contractible spaces t-algebraic-topology Algebraic topology
#37480 opened Apr 1, 2026 by erdOne Loading…
1
feat(Distribution): make parameters implicit in favor of type ascription t-analysis Analysis (normed *, calculus)
#37479 opened Apr 1, 2026 by ADedecker Loading…
1
chore(Order): make CompleteDistribLattice.MinimalAxioms.of semireducible t-order Order theory
#37478 opened Apr 1, 2026 by YaelDillies Loading…
1
feat: canonical decomposition of complex-meromorphic functions on disks t-analysis Analysis (normed *, calculus)
#37477 opened Apr 1, 2026 by kebekus Loading…
1
chore(Topology/Compactness): style cleanup for some instances 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
#37476 opened Apr 1, 2026 by felixpernegger Loading…
@grunweg
2
chore: golf proofs awaiting-author A reviewer has asked the author a question or requested changes.
#37475 opened Apr 1, 2026 by euprunin Loading…
4
perf: no expose SplittingField t-algebra Algebra (groups, rings, fields, etc) tech debt Tracking cross-cutting technical debt, see e.g. the "Technical debt counters" stream on zulip WIP Work in progress
#37474 opened Apr 1, 2026 by Komyyy Loading…
1
chore: deprecate module Topology.Algebra.Module.StrongTopology easy < 20s of review time. See the lifecycle page for guidelines. t-topology Topological spaces, uniform spaces, metric spaces, filters
#37473 opened Apr 1, 2026 by ADedecker Loading…
1
feat(RingTheory/MvPolynomial/MonomialOrder): add leadingTerm_mul lemma new-contributor This PR was made by a contributor with at most 5 merged PRs. Welcome to the community! t-ring-theory Ring theory
#37471 opened Apr 1, 2026 by NoahW314 Loading…
6
feat(SetTheory/Ordinal): add add_iSup, mul_iSup and friends new-contributor This PR was made by a contributor with at most 5 merged PRs. Welcome to the community! t-set-theory Set theory
#37470 opened Apr 1, 2026 by SabrinaJewson Loading…
@vihdzp
13
refactor: deduplicate PartialOrder (Order.Ideal P) instances t-order Order theory
#37467 opened Apr 1, 2026 by Komyyy Loading…
3
feat(Torsion/PrimaryComponent): direct sum of primaryComponent on primes is the whole module large-import Automatically added label for PRs with a significant increase in transitive imports t-algebra Algebra (groups, rings, fields, etc)
#37466 opened Apr 1, 2026 by xgenereux Loading…
1
feat(Geometry/Convex/Cone): Minor additions to pointed cones awaiting-author A reviewer has asked the author a question or requested changes. t-convex-geometry Affine geometry, cones, simplices
#37464 opened Mar 31, 2026 by martinwintermath Loading…
4
style(RingTheory/Ideal/KrullsHeightTheorem): capitalization convention for minimalPrimes new-contributor This PR was made by a contributor with at most 5 merged PRs. Welcome to the community! t-ring-theory Ring theory
#37463 opened Mar 31, 2026 by hommmmm Loading…
3
chore: golf using gcongr
#37462 opened Mar 31, 2026 by grunweg Loading…
1
chore: golf using the field tactic
#37461 opened Mar 31, 2026 by grunweg Loading…
5
feat(LinearAlgebra/AffineSpace): add Desargues's theorem 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)
#37456 opened Mar 31, 2026 by Robertboy18 Loading…
8
doc: König → Kőnig documentation Improvements or additions to documentation t-set-theory Set theory
#37455 opened Mar 31, 2026 by vihdzp Loading…
@grunweg
2
chore(Mathlib/Topology/Category/LightProfinite/Limits.lean): automated extraction t-topology Topological spaces, uniform spaces, metric spaces, filters
#37454 opened Mar 31, 2026 by mathlib-splicebot bot Loading…
@PatrickMassot
1
chore(Mathlib/Condensed/Light/Module.lean): automated extraction t-condensed Condensed mathematics
#37453 opened Mar 31, 2026 by mathlib-splicebot bot Loading…
1
ProTip! Adding no:label will show everything without a label.