Skip to content

Pull requests: leanprover-community/mathlib4

New pull request New
2,685 Open 37,599 Closed
2,685 Open 37,599 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 (all) instances of simp; infer_instance
#40915 opened Jun 23, 2026 by felixpernegger Contributor Loading…
2
chore(Algebra/Algebra/Basic): delete redundant Algebra.ofSubring instance t-algebra Algebra (groups, rings, fields, etc) t-ring-theory Ring theory
#40914 opened Jun 23, 2026 by tb65536 Contributor Loading…
1
chore(Algebra/Algebra/Tower): upgrade extendScalarsOfSurjective to an equiv awaiting-CI This PR does not pass CI yet. This label is automatically removed once it does. t-algebra Algebra (groups, rings, fields, etc) t-ring-theory Ring theory
#40913 opened Jun 22, 2026 by tb65536 Contributor Loading…
1
chore(FieldTheory/Galois/IsGaloisGroup): remove FaithfulSMul assumptions where possible 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
#40912 opened Jun 22, 2026 by tb65536 Contributor Loading…
2 tasks
2
feat(RingTheory/Ideal): add Algebra.HasGoingUp new-contributor This PR was made by a contributor with at most 5 merged PRs. Welcome to the community! t-ring-theory Ring theory
#40911 opened Jun 22, 2026 by rshlyakh Loading…
2
feat: add comap_map_eq_of_unramified and related declarations t-ring-theory Ring theory
#40910 opened Jun 22, 2026 by riccardobrasca Member Loading…
1
feat(Algebra/Notation/Indicator): pointwise evaluation of a function-valued indicator brownian Part of the ongoing formalization of the Brownian motion and stochastic integrals t-algebra Algebra (groups, rings, fields, etc)
#40909 opened Jun 22, 2026 by FrankieNC Collaborator Loading…
1
feat(MeasureTheory): add semicontinuous Portmanteau criteria
#40908 opened Jun 22, 2026 by CoolRmal Contributor • Draft
1
feat: add isCoprime_of_not_zeta_sub_one_dvd and related lemmas t-number-theory Number theory (also use t-algebra or t-analysis to specialize)
#40906 opened Jun 22, 2026 by riccardobrasca Member Loading…
1
feat(FieldTheory): the compositum of two abelian extensions is abelian t-algebra Algebra (groups, rings, fields, etc) WIP Work in progress
#40905 opened Jun 22, 2026 by xroblot Collaborator Loading…
1
chore(Algebra/Group/WithOne): remove stale TODO 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)
#40904 opened Jun 22, 2026 by jiangf13 Loading…
2
feat(Topology): generalise Trivialization.symm awaiting-author A reviewer has asked the author a question or requested changes. t-topology Topological spaces, uniform spaces, metric spaces, filters
#40903 opened Jun 22, 2026 by peabrainiac Collaborator Loading…
@grunweg
4
feat: zero-dimensional spaces 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
#40901 opened Jun 22, 2026 by vihdzp Collaborator Loading…
2 tasks
2
feat(Analysis/Matrix): spectral theorem for normal matrices awaiting-author A reviewer has asked the author a question or requested changes. LLM-generated PRs with substantial input from LLMs - review accordingly new-contributor This PR was made by a contributor with at most 5 merged PRs. Welcome to the community! t-analysis Analysis (normed *, calculus)
#40900 opened Jun 22, 2026 by judsonpereirademoura-netizen Loading…
5
feat(Data/FunLike): add abbrevs for pointwise multiplication large-import Automatically added label for PRs with a significant increase in transitive imports t-algebra Algebra (groups, rings, fields, etc)
#40899 opened Jun 22, 2026 by mcdoll Member • Draft
2
feat: add delaborators for mfderivWithin, HasMFDerivWithinAt and HasMFDerivAt t-differential-geometry Manifolds etc
#40898 opened Jun 22, 2026 by scholzhannah Collaborator Loading…
@grunweg
1
feat: HasSmallInductiveDimensionLT is monotonic t-topology Topological spaces, uniform spaces, metric spaces, filters
#40897 opened Jun 22, 2026 by vihdzp Collaborator Loading…
1
feat(Algebra/Homology): more on the functoriality of categories of homological complexes t-algebra Algebra (groups, rings, fields, etc) t-category-theory Category theory
#40895 opened Jun 22, 2026 by joelriou Contributor Loading…
4
From assumption t-differential-geometry Manifolds etc WIP Work in progress
#40894 opened Jun 22, 2026 by grunweg Contributor Loading…
1
feat: search for an IsManifold hypothesis first t-differential-geometry Manifolds etc WIP Work in progress
#40893 opened Jun 22, 2026 by grunweg Contributor Loading…
1
feat(Algebra/Homology): homological complexes in full subcategories t-algebra Algebra (groups, rings, fields, etc) t-category-theory Category theory
#40892 opened Jun 22, 2026 by joelriou Contributor Loading…
3
feat(Algebra/Homology): existence of injective resolutions for cochain complexes t-algebra Algebra (groups, rings, fields, etc) t-category-theory Category theory
#40887 opened Jun 22, 2026 by joelriou Contributor Loading…
1 task done
6
feat(CategoryTheory/Localization): small additions maintainer-merge A reviewer has approved the changed; awaiting maintainer approval. t-category-theory Category theory
#40884 opened Jun 22, 2026 by joelriou Contributor Loading…
6
feat(Analysis): use Is*Apply for Seminorm t-analysis Analysis (normed *, calculus)
#40880 opened Jun 22, 2026 by mcdoll Member Loading…
1
feat: lemmas about the smallInductiveDimension 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
#40879 opened Jun 22, 2026 by vihdzp Collaborator Loading…
1 of 2 tasks
3
ProTip! Filter pull requests by the default branch with base:master.