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

Actions: leanprover-community/mathlib3

Actions

Cross off linked issues

Actions

Loading...
Loading

Show workflow options

Create status badge

Loading
sync_closed_tasks.yaml
47 workflow runs
47 workflow runs

Filter by Event

Filter by Status

Filter by Branch

Filter by Actor

The Shapley-Folkman lemma Cross off linked issues #12490: Issue #18135 closed by YaelDillies
July 4, 2024 21:18 12s
July 4, 2024 21:18 12s
old WIP trying to replace fractional_ideal by submodule in class_group: to be ported Cross off linked issues #12489: Pull request #19245 closed by alreadydone
June 28, 2024 02:36 9s alreadydone:class_group_without_fractional
alreadydone:class_group_without_fractional
June 28, 2024 02:36 9s
old WIP trying to replace fractional_ideal by submodule in class_group: to be ported Cross off linked issues #12488: Pull request #19245 reopened by alreadydone
June 28, 2024 02:36 9s alreadydone:class_group_without_fractional
alreadydone:class_group_without_fractional
June 28, 2024 02:36 9s
old WIP trying to replace fractional_ideal by submodule in class_group: to be ported Cross off linked issues #12487: Pull request #19245 closed by alreadydone
June 28, 2024 00:09 14s alreadydone:class_group_without_fractional
alreadydone:class_group_without_fractional
June 28, 2024 00:09 14s
refactor: change notation for interval integrals Cross off linked issues #12486: Pull request #19225 closed by urkud
June 20, 2024 04:06 9s YK-interval-integral
YK-interval-integral
June 20, 2024 04:06 9s
add file containing the Weierstrass M-test Cross off linked issues #12485: Pull request #8981 closed by CBirkbeck
May 28, 2024 18:21 11s Weierstrass_M_TEST
Weierstrass_M_TEST
May 28, 2024 18:21 11s
refactor(group_theory/perm/basic): Redefine pow in terms of iterate Cross off linked issues #12484: Pull request #18077 closed by YaelDillies
April 20, 2024 13:13 17s perm_pow_iterate
perm_pow_iterate
April 20, 2024 13:13 17s
chore(algebra/order/ring/lemmas): remove useless lemmas, use namespace without_zero_le_one Cross off linked issues #12483: Pull request #16525 closed by eric-wieser
March 23, 2024 23:17 12s FR_order_refactor18
FR_order_refactor18
March 23, 2024 23:17 12s
chore(algebra/order/ring/lemmas): use suffix ₚ, create aliases Cross off linked issues #12482: Pull request #16523 closed by eric-wieser
March 23, 2024 23:16 12s FR_order_refactor16
FR_order_refactor16
March 23, 2024 23:16 12s
feat(topology/algebra/infinite_sum): Multiplicativise Cross off linked issues #12481: Pull request #18405 closed by YaelDillies
March 23, 2024 21:41 8s tprod
tprod
March 23, 2024 21:41 8s
refactor(algebra/group/defs): Use nsmul in zsmul_rec Cross off linked issues #12480: Pull request #17826 closed by YaelDillies
March 23, 2024 15:34 14s zsmul_nsmul_rec
zsmul_nsmul_rec
March 23, 2024 15:34 14s
feat(tactic/polyrith): solve more problems by testing for membership in the radical Cross off linked issues #12479: Pull request #15425 closed by eric-wieser
March 23, 2024 12:12 13s polyrith-radical
polyrith-radical
March 23, 2024 12:12 13s
fix(tactic/polyrith): fix crash when hypotheses are constant polynomials Cross off linked issues #12478: Pull request #17142 closed by eric-wieser
March 23, 2024 12:11 12s eric-wieser/fix-polyrith
eric-wieser/fix-polyrith
March 23, 2024 12:11 12s
feat(category_theory/bicategory/adjunction): add adjunction in bicategories Cross off linked issues #12477: Pull request #13418 closed by yuma-mizuno
February 24, 2024 07:28 15s bicategory-adjunction
bicategory-adjunction
February 24, 2024 07:28 15s
chore(data/rat/*): Rearrange imports Cross off linked issues #12476: Pull request #18609 closed by YaelDillies
February 9, 2024 22:23 12s shuffle_nnrat
shuffle_nnrat
February 9, 2024 22:23 12s
Jordan-Chevalley decomposition Cross off linked issues #12475: Issue #4973 closed by ocfnash
February 7, 2024 15:49 15s
February 7, 2024 15:49 15s
feat(analysic/convex): add lemmas and defs about low-dimensional simplices Cross off linked issues #12474: Pull request #19101 closed by urkud
February 7, 2024 06:41 11s YK-std-simpl
YK-std-simpl
February 7, 2024 06:41 11s
feat(order/minimal): Image of maximals under a rel_embedding Cross off linked issues #12473: Pull request #17017 closed by erdOne
December 31, 2023 05:30 11s image_maximals
image_maximals
December 31, 2023 05:30 11s
@[mk_iff] causes a type error Cross off linked issues #12472: Issue #10696 closed by YaelDillies
December 17, 2023 14:21 11s
December 17, 2023 14:21 11s
feat(combinatorics/simple_graph): Triangle counting Cross off linked issues #12471: Pull request #19206 closed by YaelDillies
December 8, 2023 11:19 12s triangle_counting
triangle_counting
December 8, 2023 11:19 12s
feat(geometry/manifold): Integral curve of vector fields Cross off linked issues #12470: Pull request #17140 closed by winstonyin
November 29, 2023 00:31 11s integral_curve
integral_curve
November 29, 2023 00:31 11s
feat(order/monotone/monovary): Monovarying functions are jointly monotone Cross off linked issues #12469: Pull request #17932 closed by YaelDillies
November 18, 2023 11:41 10s monovary_exists_monotone
monovary_exists_monotone
November 18, 2023 11:41 10s
feat(group_theory/marking): Group markings Cross off linked issues #12468: Pull request #18256 closed by YaelDillies
November 18, 2023 11:36 12s group_marking
group_marking
November 18, 2023 11:36 12s
feat(measure_theory/function/intersectivity): Bergelson Intersectivity Lemma Cross off linked issues #12467: Pull request #18732 closed by YaelDillies
November 18, 2023 11:24 10s bergelson_intersectivity
bergelson_intersectivity
November 18, 2023 11:24 10s
feat(analysis/cauchy_equation): Add Cauchy's Functional Equation Cross off linked issues #12466: Pull request #12933 closed by YaelDillies
November 18, 2023 11:19 10s Cauchy's-Functional-Equation
Cauchy's-Functional-Equation
November 18, 2023 11:19 10s