Skip to content

Pull requests: leanprover-community/mathlib4

New pull request New
2,698 Open 37,541 Closed
2,698 Open 37,541 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: fix duplicated lemma t-measure-probability Measure theory / Probability theory
#40870 opened Jun 21, 2026 by sgouezel Contributor Loading…
1
refactor(Topology): add deprecation module for LocPathConnected blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) t-topology Topological spaces, uniform spaces, metric spaces, filters
#40869 opened Jun 21, 2026 by felixpernegger Contributor Loading…
1 task
4
refactor(Topology): rename LocPathConnected file-removed A Lean module was (re)moved without a `deprecated_module` annotation t-topology Topological spaces, uniform spaces, metric spaces, filters
#40868 opened Jun 21, 2026 by felixpernegger Contributor Loading…
4
chore: remove stray Subtype.eq_iff declaration maintainer-merge A reviewer has approved the changed; awaiting maintainer approval. t-topology Topological spaces, uniform spaces, metric spaces, filters
#40867 opened Jun 21, 2026 by wwylele Collaborator Loading…
3
feat(FieldTheory/Galois/IsGaloisGroup): add IsGaloisGroup.of_isScalarTower' for towers of domains blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) t-ring-theory Ring theory
#40866 opened Jun 21, 2026 by xroblot Collaborator Loading…
2 tasks
2
refactor(Algebra/Module/Equiv): update name and refactor API ofLinearEquiv t-algebra Algebra (groups, rings, fields, etc)
#40865 opened Jun 21, 2026 by TJHeeringa Contributor • Draft
2
feat(RingTheory/Localization/FractionRing): add IsFractionRing.fixingSubgroup_range_algebraMap t-ring-theory Ring theory
#40864 opened Jun 21, 2026 by xroblot Collaborator Loading…
1
feat(Algebra/Homology): the injective derivability structure t-category-theory Category theory WIP Work in progress
#40863 opened Jun 21, 2026 by joelriou Contributor Loading…
1
chore(CategoryTheory/Comma/Arrow): use to_dual t-category-theory Category theory
#40862 opened Jun 21, 2026 by JovanGerb Contributor Loading…
1
doc: add wikidata attributes documentation Improvements or additions to documentation LLM-generated PRs with substantial input from LLMs - review accordingly
#40861 opened Jun 21, 2026 by Deicyde Contributor Loading…
39
feat(Algebra/Group/GreensRelations): add equivalence classes and posets for Green's relations blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) 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)
#40860 opened Jun 21, 2026 by ReemMelamed Loading…
1 task
3
perf(RingTheory/Kaehler/JacobiZariski): remove useless instances t-ring-theory Ring theory
#40858 opened Jun 21, 2026 by faenuccio Contributor Loading…
6
feat(RingTheory/Radical): radical of principal ideals in a UFD large-import Automatically added label for PRs with a significant increase in transitive imports t-ring-theory Ring theory
#40857 opened Jun 21, 2026 by BryceT233 Contributor Loading…
1
feat(Data/ENNReal): add sum_div t-data Data (lists, quotients, numbers, etc)
#40855 opened Jun 20, 2026 by NoahW314 Contributor Loading…
2
chore(NumberTheory/PrimeCounting): minor golf new-contributor This PR was made by a contributor with at most 5 merged PRs. Welcome to the community! t-number-theory Number theory (also use t-algebra or t-analysis to specialize)
#40854 opened Jun 20, 2026 by teorth Contributor Loading…
@MichaelStollBayreuth
2
chore: fix bad indentation t-algebra Algebra (groups, rings, fields, etc)
#40853 opened Jun 20, 2026 by grunweg Contributor Loading…
1
feat: OddIndent linter t-linter Linter
#40852 opened Jun 20, 2026 by thorimur Contributor • Draft
1
feat(MeasureTheory/Integral/MeanInequalities): strict Hölder's inequality for Lebesgue integrals t-measure-probability Measure theory / Probability theory
#40851 opened Jun 20, 2026 by SnirBroshi Collaborator Loading…
1
chore: update Mathlib dependencies 2026-06-21 auto-merge-after-CI Please do not add manually. Requests for a bot to merge automatically once CI is done. dependency-bump This PR bumps the version of an upstream dependency (but not toolchain).
#40849 opened Jun 20, 2026 by mathlib-update-dependencies Bot Loading…
2
WIP large-import Automatically added label for PRs with a significant increase in transitive imports t-ring-theory Ring theory
#40848 opened Jun 20, 2026 by fbarroero Collaborator Loading…
2
feat(Analysis/SpecialFunctions/Log/InvLog): add simp lemma form of deriv_inv_log new-contributor This PR was made by a contributor with at most 5 merged PRs. Welcome to the community!
#40847 opened Jun 20, 2026 by teorth Contributor Loading…
2
feat(Analysis/InnerProductSpace/TensorProduct): add TensorProduct.congrL 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
#40846 opened Jun 20, 2026 by TJHeeringa Contributor Loading…
2 tasks
2
feat(FinitelyPresentedGroup): quotient of a finitely group by a subgroup which is finitely generated under normal closure is finitely presented new-contributor This PR was made by a contributor with at most 5 merged PRs. Welcome to the community! t-group-theory Group theory
#40845 opened Jun 20, 2026 by laredo02 Loading…
2
feat(Algebra/Divisibility/Basic): introduce right division (RightDvd) 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)
#40843 opened Jun 20, 2026 by ReemMelamed Loading…
2
feat(Topology/Algebra): add ContinuousLinearEquiv.ofContinuousLinearMap awaiting-author A reviewer has asked the author a question or requested changes. t-topology Topological spaces, uniform spaces, metric spaces, filters
#40841 opened Jun 20, 2026 by TJHeeringa Contributor Loading…
23
ProTip! Mix and match filters to narrow down what you’re looking for.