Skip to content

Pull requests: leanprover-community/mathlib4

New pull request New
2,654 Open 37,325 Closed
2,654 Open 37,325 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

feat(Analysis): use IsApply for TestFunction t-analysis Analysis (normed *, calculus)
#40608 opened Jun 15, 2026 by mcdoll Member Loading…
1
feat(Analysis): use IsApply for ContDiffMapSupportedIn t-analysis Analysis (normed *, calculus)
#40607 opened Jun 15, 2026 by mcdoll Member Loading…
1
feat(Logic/Relation): some EqvGen API t-logic Logic (model theory, etc)
#40606 opened Jun 14, 2026 by mathlib-splicebot Bot Loading…
2
feat(LinearAlgebra/Matrix/GeneralLinear/Projective): add iso between psl and pgl when algebraically closed large-import Automatically added label for PRs with a significant increase in transitive imports t-algebra Algebra (groups, rings, fields, etc)
#40605 opened Jun 14, 2026 by Whysoserioushah Collaborator Loading…
1
feat(Algebra.GroupWithZero): generalize SMulZeroClass to MonoidWithZero and lift MulDistribMulAction to nonZeroDivisors t-algebra Algebra (groups, rings, fields, etc) WIP Work in progress
#40604 opened Jun 14, 2026 by xroblot Collaborator Loading…
2
chore: refactor the vector measure integral by changing the reference measure t-measure-probability Measure theory / Probability theory
#40603 opened Jun 14, 2026 by sgouezel Contributor Loading…
2
chore: move strong measurability proof to setToFun t-measure-probability Measure theory / Probability theory
#40602 opened Jun 14, 2026 by sgouezel Contributor Loading…
1
ci: add tech debt label CI Modifies the continuous integration setup or other automation LLM-generated PRs with substantial input from LLMs - review accordingly
#40601 opened Jun 14, 2026 by BoltonBailey Collaborator Loading…
5
feat(LinearAlgebra): rank-nullity theorems for Submodule map/comap 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)
#40599 opened Jun 14, 2026 by ChiCubed Contributor Loading…
3
[WIP] feat: add Mathlib.Biology.Longevity.PhenoAge formal contract (K-Lean Phase B) new-contributor This PR was made by a contributor with at most 5 merged PRs. Welcome to the community!
#40598 opened Jun 14, 2026 by Heime-Jorgen • Draft
2
feat(GroupTheory/SpecificGroups/Cyclic): add IsCyclic.subgroup_le/eq_subgroup_iff t-group-theory Group theory WIP Work in progress
#40597 opened Jun 14, 2026 by xroblot Collaborator Loading…
1
chore: remove TODO on characteristic functions t-measure-probability Measure theory / Probability theory
#40595 opened Jun 14, 2026 by LLaurance Collaborator Loading…
1
chore(MathlibTest): fix defLemma warnings tech debt Tracking cross-cutting technical debt, see e.g. the "Technical debt counters" stream on zulip
#40593 opened Jun 14, 2026 by grunweg Contributor Loading…
1
chore(Counterexamples/DirectSumIsInternal): fix defLemma error easy < 20s of review time. See the lifecycle page for guidelines. tech debt Tracking cross-cutting technical debt, see e.g. the "Technical debt counters" stream on zulip
#40592 opened Jun 14, 2026 by grunweg Contributor Loading…
1
feat(Topology/Algebra): inv and div for infinite products over groups with zero t-topology Topological spaces, uniform spaces, metric spaces, filters
#40591 opened Jun 14, 2026 by ajirving Contributor Loading…
5
feat(RingTheory/AdjoinRoot): more on `AdjoinRoot' of monic polynomials t-ring-theory Ring theory
#40590 opened Jun 14, 2026 by BryceT233 Contributor Loading…
1
feat(Analysis): integral test for infinite sums t-analysis Analysis (normed *, calculus)
#40588 opened Jun 14, 2026 by ajirving Contributor Loading…
1
feat(MeasureTheory): weaken hypotheses on the continuity-multiplication and xˢ·exp(-xᵖ) integrability 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
#40587 opened Jun 14, 2026 by dennj Contributor Loading…
5
ci: self-heal nightly-testing-green after a history rewrite CI Modifies the continuous integration setup or other automation
#40586 opened Jun 14, 2026 by kim-em Contributor Loading…
1
feat: holder continuity of suprema and infima t-topology Topological spaces, uniform spaces, metric spaces, filters
#40585 opened Jun 14, 2026 by CoolRmal Contributor • Draft
1 task
3
chore(Order): add to_dual tags in Mathlib/Order/ConditionallyCompleteLattice/Indexed t-order Order theory
#40584 opened Jun 14, 2026 by CoolRmal Contributor Loading…
1
feat(Analysis/Fourier/Convolution): drop continuity hypotheses from the convolution theorems new-contributor This PR was made by a contributor with at most 5 merged PRs. Welcome to the community! t-analysis Analysis (normed *, calculus)
#40583 opened Jun 14, 2026 by dennj Contributor Loading…
2
feat(Analysis): the one-sided Laplace transform 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
#40582 opened Jun 13, 2026 by dennj Contributor Loading…
@kex-y
3
feat(Analysis/InnerProductSpace): Gram completeness — equal Gram matrices give a unitary new-contributor This PR was made by a contributor with at most 5 merged PRs. Welcome to the community!
#40580 opened Jun 13, 2026 by ibarrajo • Draft
3
feat(Algebra/Category/Ring): preserve limits to CommMonCat 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)
#40579 opened Jun 13, 2026 by jcreinhold Contributor Loading…
6
ProTip! Exclude everything labeled bug with -label:bug.