Skip to content
This repository has been archived by the owner on Jul 24, 2024. It is now read-only.

Pull requests: leanprover-community/mathlib3

283 Open 18,590 Closed
283 Open 18,590 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
Sort
Sort by
Newest Oldest Most commented Least commented Recently updated Least recently updated Best match
Most reactions
👍 👎 😄 🎉 😕 ❤️ 🚀 👀

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…
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…
1
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…
1
feat(measure_theory/measure): show that bounded continuous functions separate measures too-late This PR was ready too late for inclusion in mathlib3
#19189 opened Jun 14, 2023 by pfaffelh • Draft
feat(topology/algebra/infinite_sum): Extract none from a sum over option types awaiting-author 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
#19150 opened Jun 4, 2023 by dtumad Loading…
10
feat(analysis/calculus/fderiv/exp): derivative of exp ℝ (A x) in non-commutative rings 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
#19056 opened May 21, 2023 by eric-wieser Loading…
1 task done
10
refactor(measure_theory/measure/lebesgue): use ‖a‖₊ • instead of ennreal.of_real (|a|) * awaiting-CI 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
#19018 opened May 15, 2023 by eric-wieser Loading…
feat(measure_theory/measure/haar_lebesgue): the volume measures on euclidean_space ℝ ι and ι → ℝ agree modifies-synchronized-file 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
#19013 opened May 14, 2023 by eric-wieser Loading…
3 tasks done
1
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…
6
refactor(linear_algebra/*): Rename linear_equiv.range to linear_equiv.range_eq_top awaiting-CI 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
#18969 opened May 8, 2023 by tb65536 Loading…
feat(order/filter,topology/instances/nnreal): upgrade some lemmas to iff awaiting-author 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
#18964 opened May 7, 2023 by urkud Loading…
10
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…
28
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
1
refactor(number_theory/modular_forms/slash_actions): slash actions are families of distrib_mul_actions RFC 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
#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…
2
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
1
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
2
feat(topology/noetherian_space): use well_founded_(lt/gt) awaiting-review The author would like community review of the PR too-late This PR was ready too late for inclusion in mathlib3
#18776 opened Apr 9, 2023 by vihdzp • Draft
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…
1
chore(data/fintype/card): instance well_founded_of_trans_of_irrefl 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. too-late This PR was ready too late for inclusion in mathlib3
#18774 opened Apr 9, 2023 by vihdzp • Draft
chore(logic/hydra): instance well_founded.cut_expand awaiting-author 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
#18757 opened Apr 7, 2023 by vihdzp Loading…
4
feat(order/well_founded): well_founded_lt.has_min, etc. 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. too-late This PR was ready too late for inclusion in mathlib3
#18751 opened Apr 6, 2023 by vihdzp • Draft
1 task
1
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
1
feat(logic/relation): auxiliary forall_exists_rel relation awaiting-author 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
#18713 opened Apr 2, 2023 by vihdzp Loading…
3
ProTip! Follow long discussions with comments:>50.