Skip to content

Pull requests: leanprover-community/mathlib4

New pull request New
1,907 Open 30,902 Closed
1,907 Open 30,902 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

Sg param i
#33384 opened Dec 29, 2025 by sgouezel • Draft
2
Add Theorem about Sbtw.angle_eq and Wbtw.angle_eq new-contributor This PR was made by a contributor with at most 5 merged PRs. Welcome to the community! t-euclidean-geometry Affine and axiomatic geometry
#33383 opened Dec 29, 2025 by dsfxcimk Loading…
2
feat(Combinatorics/SimpleGraph/Acyclic): characterize trees via bridges new-contributor This PR was made by a contributor with at most 5 merged PRs. Welcome to the community! t-combinatorics Combinatorics
#33382 opened Dec 29, 2025 by WangYiran01 Loading…
1
feat: add a version of the Schwarz lemma blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) t-analysis Analysis (normed *, calculus)
#33381 opened Dec 29, 2025 by urkud Loading…
2 tasks
2
feat(RingTheory): Gorenstein local ring is Cohen--Macaulay local ring of type one 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
#33380 opened Dec 29, 2025 by Thmoas-Guan Loading…
2 tasks
2
feat(RingTheory): Gorenstein local ring is Cohen Macaulay 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
#33379 opened Dec 29, 2025 by Thmoas-Guan Loading…
5 tasks
2
feat(RingTheory): polynomial over Gorenstein ring is Gorenstein 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
#33377 opened Dec 29, 2025 by Thmoas-Guan Loading…
3 tasks
2
chore(Analysis/InnerProductSpace/Rayleigh): clean up and fix a non-terminal simp maintainer-merge A reviewer has approved the changed; awaiting maintainer approval. t-analysis Analysis (normed *, calculus)
#33376 opened Dec 29, 2025 by yuanyi-350 Loading…
@grunweg
6
feat(Probability): Local and stable properties blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) brownian Part of the ongoing formalization of the Brownian motion and stochastic integrals t-measure-probability Measure theory / Probability theory
#33375 opened Dec 29, 2025 by kex-y Loading…
3 tasks
3
feat: Simple lemmas about convergence in WithTop brownian Part of the ongoing formalization of the Brownian motion and stochastic integrals t-topology Topological spaces, uniform spaces, metric spaces, filters
#33374 opened Dec 29, 2025 by kex-y Loading…
1
feat(Analysis/Deriv): Add iteratedDeriv_comp_sub_const t-analysis Analysis (normed *, calculus)
#33373 opened Dec 29, 2025 by yuanyi-350 Loading…
1
feat(Probability): Countable infimum of stopping times is a stopping time blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) brownian Part of the ongoing formalization of the Brownian motion and stochastic integrals t-measure-probability Measure theory / Probability theory
#33372 opened Dec 29, 2025 by kex-y Loading…
1 task
2
feat(Probability): Right continuous filtrations brownian Part of the ongoing formalization of the Brownian motion and stochastic integrals t-measure-probability Measure theory / Probability theory
#33371 opened Dec 29, 2025 by kex-y Loading…
1
feat: all root system bases arise via IsAddIndecomposable.baseOf 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-algebra Algebra (groups, rings, fields, etc)
#33370 opened Dec 29, 2025 by ocfnash Loading…
1 task
2
feat(Homology): Ext commute with flat base change 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
#33369 opened Dec 29, 2025 by Thmoas-Guan Loading…
3 tasks
2
feat: define Complex.UnitDisc.shift t-analysis Analysis (normed *, calculus)
#33368 opened Dec 29, 2025 by urkud Loading…
1
feat(Geometry/Euclidean/Angle/Oriented/Affine): Add oangle sign lemmas for two intersecting lines t-euclidean-geometry Affine and axiomatic geometry
#33365 opened Dec 29, 2025 by zcyemi Loading…
5
feat(Analysis/Convex/SimplicialComplex): add constructions when union is affinely independent t-analysis Analysis (normed *, calculus)
#33364 opened Dec 29, 2025 by BoltonBailey Loading…
1
feat: add empty_eq_image simp lemmas t-data Data (lists, quotients, numbers, etc)
#33363 opened Dec 28, 2025 by BoltonBailey Loading…
1
feat: weaken assumptions in Schwarz lemma t-analysis Analysis (normed *, calculus)
#33362 opened Dec 28, 2025 by urkud Loading…
4
feat(RingTheory/Nakayama): refine Nakayama's lemma 00DV (8) new-contributor This PR was made by a contributor with at most 5 merged PRs. Welcome to the community! t-ring-theory Ring theory
#33361 opened Dec 28, 2025 by sun123zxy Loading…
1
feat(Algebra/Homology): functoriality of extMk with respect to the injective resolution blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) t-category-theory Category theory WIP Work in progress
#33360 opened Dec 28, 2025 by joelriou Loading…
2 tasks
2
feat(Algebra/Module/SpanRank): add comparing lemmas for span rank 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)
#33359 opened Dec 28, 2025 by sun123zxy Loading…
2
feat(Algebra/Homology): functoriality of ProjectiveResolution.extMk blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) t-category-theory Category theory WIP Work in progress
#33358 opened Dec 28, 2025 by joelriou Loading…
1 task
2
feat: hasDetPlusMinusOne_iff_abs_det
#33356 opened Dec 28, 2025 by Ruben-VandeVelde Loading…
1
ProTip! Type g p on any issue or pull request to go back to the pull request listing page.