Skip to content

Pull requests: leanprover-community/mathlib4

New pull request New
1,994 Open 29,570 Closed
1,994 Open 29,570 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/Normed/Operator): definition of singular values for linear maps new-contributor This PR was made by a contributor with at most 5 merged PRs. Welcome to the community! t-analysis Analysis (normed *, calculus) WIP Work in progress
#32126 opened Nov 26, 2025 by nielsvoss • Draft
2
feat(SimpleGraph/Walks/Subwalks): p₁.IsSubwalk p₂ ↔ p₁.darts <:+: p₂.darts and similar theorems t-combinatorics Combinatorics
#32125 opened Nov 26, 2025 by SnirBroshi Loading…
1
feat(SimpleGraph/Walks/Operations): expand basic drop/take/reverse API t-combinatorics Combinatorics
#32124 opened Nov 26, 2025 by SnirBroshi Loading…
1
feat(LinearAlgebra): rank of commutative semiring over itself t-algebra Algebra (groups, rings, fields, etc)
#32123 opened Nov 26, 2025 by alreadydone Loading…
1
refactor(Topology): relax Eventually to Frequently for TendstoUniformly.continuous delegated This pull request has been delegated to the PR author (or occasionally another non-maintainer).
#32122 opened Nov 26, 2025 by wwylele Loading…
4
feat(Analysis): tendsto_zpow_nhdsNE_zero_cobounded delegated This pull request has been delegated to the PR author (or occasionally another non-maintainer). t-analysis Analysis (normed *, calculus)
#32120 opened Nov 26, 2025 by erdOne Loading…
9
doc: balance parentheses and brackets
#32119 opened Nov 25, 2025 by harahu Loading…
1
feat(Algebra): prerequisites for #31919 t-algebra Algebra (groups, rings, fields, etc) t-ring-theory Ring theory
#32118 opened Nov 25, 2025 by alreadydone Loading…
3
feat(MeasureTheory\Group\Action): add μ(c • s ∩ t) = μ(s ∩ c⁻¹ • t) and similar 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
#32117 opened Nov 25, 2025 by ster99 Loading…
1
feat(Geometry/Euclidean/Angle/Unoriented/TriangleInequality): Add criterion for equality case blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) t-euclidean-geometry Affine and axiomatic geometry
#32116 opened Nov 25, 2025 by LessnessRandomness Loading…
1 task
10
chore(Data/Set): golf Injective.compl_image_eq using grind t-data Data (lists, quotients, numbers, etc)
#32115 opened Nov 25, 2025 by euprunin Loading…
1
chore(Data/Vector): golf ofFn_get t-data Data (lists, quotients, numbers, etc)
#32113 opened Nov 25, 2025 by euprunin Loading…
1
chore(MeasureTheory/MeasurableSpace): golf generateFrom_pi_eq using grind t-measure-probability Measure theory / Probability theory
#32112 opened Nov 25, 2025 by euprunin Loading…
1
feat(RingTheory/AdjoinRoot): map t-ring-theory Ring theory toric Part of the ongoing formalisation of toric varieties
#32111 opened Nov 25, 2025 by YaelDillies Loading…
6
chore(Logic/Equiv): golf Function.Injective.map_swap using grind t-logic Logic (model theory, etc)
#32110 opened Nov 25, 2025 by euprunin Loading…
1
feat(LinearAlgebra/Span): improve R ∙ x notation precedence and printing
#32108 opened Nov 25, 2025 by JovanGerb Loading…
2
chore(Data/Int/Fib): add fib_neg t-data Data (lists, quotients, numbers, etc)
#32107 opened Nov 25, 2025 by themathqueen Loading…
6
feat(SimpleGraph/Walks/Operations): golf ext_support using darts_injective and map_{fst,snd}_darts
#32106 opened Nov 25, 2025 by SnirBroshi Loading…
1
feat(CategoryTheory): constructor for Ext-groups using an 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
#32105 opened Nov 25, 2025 by joelriou Loading…
6 tasks
2
refactor(Algebra/Polynomial/Splits): continue deprecation merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) t-algebra Algebra (groups, rings, fields, etc)
#32103 opened Nov 25, 2025 by tb65536 Loading…
2
feat(Combinatorics/SimpleGraph): add simp lemma getVert_map for Walk.map new-contributor This PR was made by a contributor with at most 5 merged PRs. Welcome to the community! t-combinatorics Combinatorics
#32102 opened Nov 25, 2025 by maix00 Loading…
5
feat(Algebra): add subsingleton of IsZero for AddCommGrpCat awaiting-author A reviewer has asked the author a question or requested changes. t-algebra Algebra (groups, rings, fields, etc)
#32101 opened Nov 25, 2025 by Thmoas-Guan Loading…
6
feat(Geometry/Euclidean/../TriangleInequality): one equality case of the vector triangle inequality t-euclidean-geometry Affine and axiomatic geometry
#32100 opened Nov 25, 2025 by JovanGerb Loading…
1
feat(RingTheory): universal coprime factorization ring t-ring-theory Ring theory
#32099 opened Nov 25, 2025 by erdOne Loading…
1
feat(RingTheory): injective dimension of quotSMulTop blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot)
#32098 opened Nov 25, 2025 by Thmoas-Guan Loading…
3 tasks
2
ProTip! Mix and match filters to narrow down what you’re looking for.