Skip to content

Pull requests: leanprover-community/mathlib4

New pull request New
2,351 Open 34,985 Closed
2,351 Open 34,985 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(CategoryTheory): deprecate Adjunction.leftAdjointsCoyonedaEquiv t-category-theory Category theory
#37943 opened Apr 12, 2026 by dagurtomas Contributor Loading…
1
feat(MeasureTheory/Integral/IntervalIntegral/Fubini): Fubini swap for two iterated interval integrals new-contributor This PR was made by a contributor with at most 5 merged PRs. Welcome to the community! t-measure-probability Measure theory / Probability theory
#37942 opened Apr 12, 2026 by yanghangAI Loading…
4
feat(RingTheory/MvPolynomial/Homogeneous): add homogeneousComponent lemma t-ring-theory Ring theory
#37941 opened Apr 12, 2026 by NoahW314 Contributor Loading…
1
feat(Algebra/Category): introduce the category of local algebras with a fixed residue field blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot)
#37940 opened Apr 12, 2026 by BryceT233 Contributor Loading…
1 task
2
feat(Order/Completion): embed a partial order into a dense and complete order t-order Order theory WIP Work in progress
#37939 opened Apr 11, 2026 by AntoineChambert-Loir Collaborator Loading…
@vihdzp
13
feat(Probability/Posterior): Posterior PMFs and Various Lemmas new-contributor This PR was made by a contributor with at most 5 merged PRs. Welcome to the community! t-measure-probability Measure theory / Probability theory
#37938 opened Apr 11, 2026 by SamuelSchlesinger Loading…
2
chore: avoid superfluous use of push_neg with contrapose, by_contra o…
#37937 opened Apr 11, 2026 by grunweg Contributor Loading…
5
feat(Topology/Order): DenselyOrdered of PreconnectedSpace awaiting-author A reviewer has asked the author a question or requested changes. t-topology Topological spaces, uniform spaces, metric spaces, filters
#37935 opened Apr 11, 2026 by NoahW314 Contributor Loading…
2
feat(FieldTheory): definition of transcendental separable field extension t-algebra Algebra (groups, rings, fields, etc)
#37934 opened Apr 11, 2026 by Thmoas-Guan Collaborator Loading…
1
feat(LinearAlgebra/Matrix/Hermitian): A block-diagonal matrix is Hermitian iff each block is Hermitian easy < 20s of review time. See the lifecycle page for guidelines. maintainer-merge A reviewer has approved the changed; awaiting maintainer approval. 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)
#37933 opened Apr 11, 2026 by danieldia-dev Loading…
26
feat: Exponential map of Lie group is smooth merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) new-contributor This PR was made by a contributor with at most 5 merged PRs. Welcome to the community!
#37932 opened Apr 11, 2026 by idontgetoutmuch Collaborator Loading…
3
chore(Tactic): make the (deprecated) replace syntax a @[tactic_alt] documentation Improvements or additions to documentation t-meta Tactics, attributes or user commands
#37931 opened Apr 11, 2026 by Vierkantor Contributor Loading…
1
chore(SimpleGraph): move cycleGraph to its own file t-combinatorics Combinatorics
#37930 opened Apr 11, 2026 by vlad902 Collaborator Loading…
1
chore(Tactic): rewrite reduce_mod_char tactic docstring documentation Improvements or additions to documentation t-meta Tactics, attributes or user commands
#37929 opened Apr 11, 2026 by Vierkantor Contributor Loading…
1
refactor(Computability.Encoding): unbundle Γ and remove FinEncoding new-contributor This PR was made by a contributor with at most 5 merged PRs. Welcome to the community!
#37928 opened Apr 11, 2026 by AlexeyMilovanov Contributor Loading…
6
chore(Tactic): rewrite order tactic docstring documentation Improvements or additions to documentation t-meta Tactics, attributes or user commands
#37927 opened Apr 11, 2026 by Vierkantor Contributor Loading…
1
feat(Analysis/Analytic): add AnalyticAt properties for iterated dslope new-contributor This PR was made by a contributor with at most 5 merged PRs. Welcome to the community! t-analysis Analysis (normed *, calculus)
#37926 opened Apr 11, 2026 by e-271828 Contributor Loading…
5
chore: try to use fast_instance in basic definitions
#37925 opened Apr 11, 2026 by sgouezel Contributor • Draft
7
perf(Tactic/FastInstance): use whnf on data fields t-meta Tactics, attributes or user commands
#37924 opened Apr 11, 2026 by JovanGerb Contributor Loading…
4
feat(Analysis/Calculus/DSlope): add eq_smul_dslope_of_zero and iterated version new-contributor This PR was made by a contributor with at most 5 merged PRs. Welcome to the community! t-analysis Analysis (normed *, calculus)
#37923 opened Apr 11, 2026 by e-271828 Contributor Loading…
@j-loreaux
4
chore: cleanup of adaptation notes delegated This pull request has been delegated to the PR author (or occasionally another non-maintainer). tech debt Tracking cross-cutting technical debt, see e.g. the "Technical debt counters" stream on zulip
#37922 opened Apr 11, 2026 by kim-em Contributor Loading…
7
feat(Mathlib/LinearAlgebra): embeddings of free modules t-algebra Algebra (groups, rings, fields, etc)
#37919 opened Apr 11, 2026 by artie2000 Collaborator Loading…
1
feat(Analysis/InnerProductSpace): Gram matrix det ≠ 0 iff input vectors are independent large-import Automatically added label for PRs with a significant increase in transitive imports t-analysis Analysis (normed *, calculus)
#37918 opened Apr 11, 2026 by wwylele Collaborator Loading…
@j-loreaux
5
refactor: elimate string manipulation in TacticAnalysis.verifyTryThisSuggestions t-meta Tactics, attributes or user commands
#37917 opened Apr 11, 2026 by chenson2018 Contributor Loading…
@JovanGerb
1
feat(Topology/CWComplex): 1-skeleton Graph of CWComplex t-topology Topological spaces, uniform spaces, metric spaces, filters
#37915 opened Apr 10, 2026 by Jun2M Collaborator Loading…
1
ProTip! Add no:assignee to see everything that’s not assigned.