Pull requests: leanprover-community/mathlib
Author
Label
Projects
Milestones
Reviews
Assignee
Sort
Pull requests list
chore(*): add mathlib4 synchronization comments
awaiting-review
The author would like community review of the PR
easy
< 20s of review time. See the lifecycle page for guidelines.
mathlib4-synchronization
This PR *only* adds a message to the module doc about synchronization with mathlib4
#19240
opened Aug 20, 2023 by
github-actions
bot
Loading…
refactor: change notation for interval integrals
awaiting-review
The author would like community review of the PR
modifies-synchronized-file
This PR touches a files that has already been ported to mathlib4, and may need a synchronization PR.
RFC
Request for comment
too-late
This PR was ready too late for inclusion in mathlib3
#19225
opened Jun 30, 2023 by
urkud
Loading…
feat(topology/algebra/infinite_sum) : define infinite products
awaiting-review
The author would like community review of the PR
modifies-synchronized-file
This PR touches a files that has already been ported to mathlib4, and may need a synchronization PR.
too-late
This PR was ready too late for inclusion in mathlib3
#19219
opened Jun 29, 2023 by
AntoineChambert-Loir
Loading…
Test leanprover-community/lean#812
too-late
This PR was ready too late for inclusion in mathlib3
WIP
Work in progress
#19192
opened Jun 15, 2023 by
eric-wieser
Loading…
feat(measure_theory/measure): show that bounded continuous functions separate measures
too-late
This PR was ready too late for inclusion in mathlib3
feat(topology/algebra/infinite_sum): Extract A reviewer has asked the author a question or requested changes
modifies-synchronized-file
This PR touches a files that has already been ported to mathlib4, and may need a synchronization PR.
too-late
This PR was ready too late for inclusion in mathlib3
none from a sum over option types
awaiting-author
#19150
opened Jun 4, 2023 by
dtumad
Loading…
feat(analysis/calculus/fderiv/exp): derivative of The author needs attention to resolve issues
too-late
This PR was ready too late for inclusion in mathlib3
WIP
Work in progress
exp ℝ (A x) in non-commutative rings
help-wanted
#19056
opened May 21, 2023 by
eric-wieser
Loading…
1 task done
refactor(measure_theory/measure/lebesgue): use The author would like to see what CI has to say before doing more work.
modifies-synchronized-file
This PR touches a files that has already been ported to mathlib4, and may need a synchronization PR.
too-late
This PR was ready too late for inclusion in mathlib3
WIP
Work in progress
‖a‖₊ • instead of ennreal.of_real (|a|) *
awaiting-CI
#19018
opened May 15, 2023 by
eric-wieser
Loading…
feat(measure_theory/measure/haar_lebesgue): the volume measures on This PR touches a files that has already been ported to mathlib4, and may need a synchronization PR.
t-measure-probability
Measure theory / Probability theory
too-late
This PR was ready too late for inclusion in mathlib3
WIP
Work in progress
euclidean_space ℝ ι and ι → ℝ agree
modifies-synchronized-file
#19013
opened May 14, 2023 by
eric-wieser
Loading…
3 tasks done
feat(library): max-flow min-cut
help-wanted
The author needs attention to resolve issues
too-late
This PR was ready too late for inclusion in mathlib3
WIP
Work in progress
#18998
opened May 12, 2023 by
amilchew
Loading…
feat(library): weak duality of max-flow min-cut theorem
awaiting-review
The author would like community review of the PR
too-late
This PR was ready too late for inclusion in mathlib3
#18996
opened May 12, 2023 by
amilchew
Loading…
refactor(linear_algebra/*): Rename The author would like to see what CI has to say before doing more work.
modifies-synchronized-file
This PR touches a files that has already been ported to mathlib4, and may need a synchronization PR.
too-late
This PR was ready too late for inclusion in mathlib3
WIP
Work in progress
linear_equiv.range to linear_equiv.range_eq_top
awaiting-CI
#18969
opened May 8, 2023 by
tb65536
Loading…
feat(order/filter,topology/instances/nnreal): upgrade some lemmas to A reviewer has asked the author a question or requested changes
modifies-synchronized-file
This PR touches a files that has already been ported to mathlib4, and may need a synchronization PR.
t-order
Order hierarchy
t-topology
Topological spaces, uniform spaces, metric spaces, filters
too-late
This PR was ready too late for inclusion in mathlib3
iff
awaiting-author
#18964
opened May 7, 2023 by
urkud
Loading…
feat(zmod/basic)
modifies-synchronized-file
This PR touches a files that has already been ported to mathlib4, and may need a synchronization PR.
too-late
This PR was ready too late for inclusion in mathlib3
#18953
opened May 6, 2023 by
laughinggas
Loading…
feat(ring_theory/derivation): support non-commutative rings (via bimodules)
too-late
This PR was ready too late for inclusion in mathlib3
WIP
Work in progress
#18936
opened May 3, 2023 by
eric-wieser
Loading…
1 task done
refactor(number_theory/modular_forms/slash_actions): slash actions are families of Request for comment
t-number-theory
Number theory (also use t-algebra or t-analysis to specialize)
too-late
This PR was ready too late for inclusion in mathlib3
distrib_mul_actions
RFC
#18932
opened May 3, 2023 by
eric-wieser
Loading…
feat(algebra/*): morphisms from closures are equal if they agree on generators
awaiting-CI
The author would like to see what CI has to say before doing more work.
awaiting-review
The author would like community review of the PR
modifies-synchronized-file
This PR touches a files that has already been ported to mathlib4, and may need a synchronization PR.
t-algebra
Algebra (groups, rings, fields etc)
too-late
This PR was ready too late for inclusion in mathlib3
#18836
opened Apr 19, 2023 by
eric-wieser
Loading…
feat(inner_product_space/positive): matrix.pos_semidef iff x.to_euclidean_lin.is_positive
awaiting-review
The author would like community review of the PR
blocked-by-other-PR
This PR depends on another PR which is still in the queue. A bot manages this label via PR comment.
not-too-late
This PR was ready at the point mathlib3 was frozen: we will try to merge it and port it to mathlib4
#18786
opened Apr 10, 2023 by
themathqueen
Loading…
1 task
feat(inner_product_space/positive): defines square root of a linear map
blocked-by-other-PR
This PR depends on another PR which is still in the queue. A bot manages this label via PR comment.
not-ready-to-merge
t-analysis
Analysis (normed *, calculus)
#18779
opened Apr 9, 2023 by
themathqueen
Loading…
1 task
feat(topology/noetherian_space): use The author would like community review of the PR
too-late
This PR was ready too late for inclusion in mathlib3
well_founded_(lt/gt)
awaiting-review
chore(*): bundle typeclasses
awaiting-CI
The author would like to see what CI has to say before doing more work.
awaiting-review
The author would like community review of the PR
t-order
Order hierarchy
too-late
This PR was ready too late for inclusion in mathlib3
#18775
opened Apr 9, 2023 by
vihdzp
Loading…
chore(data/fintype/card): instance The author would like to see what CI has to say before doing more work.
awaiting-review
The author would like community review of the PR
modifies-synchronized-file
This PR touches a files that has already been ported to mathlib4, and may need a synchronization PR.
too-late
This PR was ready too late for inclusion in mathlib3
well_founded_of_trans_of_irrefl
awaiting-CI
chore(logic/hydra): instance A reviewer has asked the author a question or requested changes
modifies-synchronized-file
This PR touches a files that has already been ported to mathlib4, and may need a synchronization PR.
too-late
This PR was ready too late for inclusion in mathlib3
well_founded.cut_expand
awaiting-author
#18757
opened Apr 7, 2023 by
vihdzp
Loading…
feat(order/well_founded): The author would like community review of the PR
blocked-by-other-PR
This PR depends on another PR which is still in the queue. A bot manages this label via PR comment.
too-late
This PR was ready too late for inclusion in mathlib3
well_founded_lt.has_min, etc.
awaiting-review
feat(order/rel_classes): housekeeping
awaiting-review
The author would like community review of the PR
blocked-by-other-PR
This PR depends on another PR which is still in the queue. A bot manages this label via PR comment.
modifies-synchronized-file
This PR touches a files that has already been ported to mathlib4, and may need a synchronization PR.
not-too-late
This PR was ready at the point mathlib3 was frozen: we will try to merge it and port it to mathlib4
t-order
Order hierarchy
#18750
opened Apr 6, 2023 by
vihdzp
Loading…
1 task
Previous Next
ProTip!
no:milestone will show everything without a milestone.