-
Notifications
You must be signed in to change notification settings - Fork 667
Pull requests: leanprover-community/mathlib4
Author
Label
Projects
Milestones
Reviews
Assignee
Sort
Pull requests list
chore(IntegrableOn): generalise one more section to enorms
carleson
part of the ongoing formalization of Carleson's theorem
t-measure-probability
Measure theory / Probability theory
#27419
opened Jul 24, 2025 by
grunweg
Loading…
wip(Intervalintegral): generalise more lemmas to enorms
t-measure-probability
Measure theory / Probability theory
#27418
opened Jul 24, 2025 by
grunweg
Loading…
feat: add Order theory
SigmaCompleteLattice
t-order
#27417
opened Jul 24, 2025 by
PierreQuinton
Loading…
feat(Algebra/Homology): Ext modules
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-category-theory
Category theory
WIP
Work in progress
#27416
opened Jul 24, 2025 by
joelriou
Loading…
1 task
feat(ModelTheory): Semilinear sets in This PR depends on another PR (this label is automatically managed by a bot)
t-logic
Logic (model theory, etc)
ℕ
are closed under intersection and complement
blocked-by-other-PR
#27414
opened Jul 24, 2025 by
staroperator
Loading…
3 of 6 tasks
feat(Valued/LocallyCompact): do not require RankOne to show IsDVR
blocked-by-other-PR
This PR depends on another PR (this label is automatically managed by a bot)
#27412
opened Jul 24, 2025 by
pechersky
Loading…
1 task
feat(GroupTheory/ArchimedeanDensely): locally finite linearly ordered groups are mul archimedean
awaiting-author
A reviewer has asked the author a question or requested changes.
t-algebra
Algebra (groups, rings, fields, etc)
t-order
Order theory
#27410
opened Jul 24, 2025 by
pechersky
Loading…
chore: generalize typeclass assumptions on DFinsupp SMul
maintainer-merge
t-data
Data (lists, quotients, numbers, etc)
#27409
opened Jul 23, 2025 by
eric-wieser
Loading…
feat:
@[grind]
annotate Finset.{mem_{Icc,Ico,Ioc,Ioo},{prod,sum}_congr}
#27408
opened Jul 23, 2025 by
euprunin
Loading…
feat(Topology/ClusterPt): Swapped version of Topological spaces, uniform spaces, metric spaces, filters
ClusterPt.frequently
t-topology
#27407
opened Jul 23, 2025 by
tb65536
Loading…
feat(MeasureTheory/Measure/AddContent): Add lemma Measure theory / Probability theory
addContent_biUnion_eq
t-measure-probability
#27406
opened Jul 23, 2025 by
tb65536
Loading…
fix(to_additive): expand kernel projections to use Tactics, attributes or user commands
reorder
t-meta
#27405
opened Jul 23, 2025 by
JovanGerb
Loading…
feat:
@[grind]
annotate Finset.mem_{filter,insert,sdiff,singleton}
#27404
opened Jul 23, 2025 by
euprunin
Loading…
feat: replace probably erroneous usage of ⬝ (with old \cdot) by · (with \centerdot)
new-contributor
This PR was made by a contributor with at most 5 merged PRs. Welcome to the community!
#27403
opened Jul 23, 2025 by
MoritzBeroRoos
Loading…
fix: delete a duplicate instance
easy
< 20s of review time. See the lifecycle page for guidelines.
ready-to-merge
This PR has been sent to bors.
t-algebra
Algebra (groups, rings, fields, etc)
#27402
opened Jul 23, 2025 by
eric-wieser
Loading…
fix: make This PR was made by a contributor with at most 5 merged PRs. Welcome to the community!
t-meta
Tactics, attributes or user commands
compile_inductive%
work correctly with new compiler
new-contributor
#27401
opened Jul 23, 2025 by
zwarich
Loading…
feat: define geometrically reduced algebras
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)
#27400
opened Jul 23, 2025 by
dleijnse
Loading…
feat: replace every usage of ⬝ᵥ (with old \cdot) by ·ᵥ (with \centerdot)
new-contributor
This PR was made by a contributor with at most 5 merged PRs. Welcome to the community!
#27399
opened Jul 23, 2025 by
MoritzBeroRoos
Loading…
chore(*): fix some scattered adaptation notes
ready-to-merge
This PR has been sent to bors.
tech debt
Tracking cross-cutting technical debt, see e.g. the "Technical debt counters" stream on zulip
#27396
opened Jul 23, 2025 by
Vierkantor
Loading…
feat(Algebra/Homology): the canonical t-structure on the derived category
t-category-theory
Category theory
WIP
Work in progress
#27395
opened Jul 23, 2025 by
joelriou
Loading…
feat(Tactic/SimpUtils): add simproc finding commands
t-meta
Tactics, attributes or user commands
#27392
opened Jul 23, 2025 by
Paul-Lez
Loading…
feat(CategoryTheory/Limits/Shapes/Pullback/Categorical): pseudofunctoriality structure of categorical pullback squares
blocked-by-other-PR
This PR depends on another PR (this label is automatically managed by a bot)
t-category-theory
Category theory
#27391
opened Jul 23, 2025 by
robin-carlier
Loading…
1 task
feat(FieldTheory/Galois): normal basis theorem
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)
WIP
Work in progress
#27390
opened Jul 23, 2025 by
alreadydone
Loading…
2 tasks
chore(Analysis): remove a few unneccessary assignments in instance declarations
ready-to-merge
This PR has been sent to bors.
t-analysis
Analysis (normed *, calculus)
tech debt
Tracking cross-cutting technical debt, see e.g. the "Technical debt counters" stream on zulip
#27389
opened Jul 23, 2025 by
Vierkantor
Loading…
Previous Next
ProTip!
Adding no:label will show everything without a label.