Skip to content

Actions: leanprover-community/mathlib4

Actions

lint and suggest

Actions

Loading...
Loading

Show workflow options

Create status badge

Loading
lint_and_suggest_pr.yml
73,733 workflow runs
73,733 workflow runs

Filter by Event

Filter by Status

Filter by Branch

Filter by Actor

feat(RingTheory/Powerseries): Weierstrass preparation for complete local ring lint and suggest #83512: Pull request #21944 synchronize by Thmoas-Guan
February 16, 2025 07:12 55s Weierstrass-preparation-aux
Weierstrass-preparation-aux
February 16, 2025 07:12 55s
feat(RingTheory/Powerseries): Weierstrass preparation for complete local ring lint and suggest #83511: Pull request #21944 synchronize by Thmoas-Guan
February 16, 2025 07:09 1m 26s Weierstrass-preparation-aux
Weierstrass-preparation-aux
February 16, 2025 07:09 1m 26s
feat: extensible push_neg tactic lint and suggest #83510: Pull request #21769 synchronize by JovanGerb
February 16, 2025 06:38 1m 27s push_neg-Finite
push_neg-Finite
February 16, 2025 06:38 1m 27s
feat(RingTheory/Powerseries): Weierstrass preparation for complete local ring lint and suggest #83509: Pull request #21944 opened by Thmoas-Guan
February 16, 2025 05:56 1m 21s Weierstrass-preparation-aux
Weierstrass-preparation-aux
February 16, 2025 05:56 1m 21s
chore(*): fix some Fintype/DecidableEq linter errors lint and suggest #83508: Pull request #21943 opened by urkud
February 16, 2025 05:41 1m 34s YK-fintype-dec
YK-fintype-dec
February 16, 2025 05:41 1m 34s
feat: add from/toList between FreeSemigroup and List with relative theorems lint and suggest #83507: Pull request #21903 synchronize by yhtq
February 16, 2025 05:40 1m 22s GuoZiXun/staffs
GuoZiXun/staffs
February 16, 2025 05:40 1m 22s
feat: extensible push_neg tactic lint and suggest #83506: Pull request #21769 synchronize by JovanGerb
February 16, 2025 05:40 2m 34s push_neg-Finite
push_neg-Finite
February 16, 2025 05:40 2m 34s
feat: add from/toList between FreeSemigroup and List with relative theorems lint and suggest #83505: Pull request #21903 synchronize by yhtq
February 16, 2025 05:30 1m 27s GuoZiXun/staffs
GuoZiXun/staffs
February 16, 2025 05:30 1m 27s
chore(LocallyConvex/Basic): generalize TC assumptions lint and suggest #83504: Pull request #21942 opened by urkud
February 16, 2025 05:29 1m 21s YK-balanced-divring
YK-balanced-divring
February 16, 2025 05:29 1m 21s
feat: extensible push_neg tactic lint and suggest #83503: Pull request #21769 synchronize by JovanGerb
February 16, 2025 05:06 1m 24s push_neg-Finite
push_neg-Finite
February 16, 2025 05:06 1m 24s
feat(EGauge): add egauge_univ lint and suggest #83502: Pull request #21941 opened by urkud
February 16, 2025 03:32 1m 42s YK-egauge-univ
YK-egauge-univ
February 16, 2025 03:32 1m 42s
feat: extensible push_neg tactic lint and suggest #83501: Pull request #21769 synchronize by JovanGerb
February 16, 2025 03:32 1m 48s push_neg-Finite
push_neg-Finite
February 16, 2025 03:32 1m 48s
feat(GroupAction/Pointwise): add MapsTo.smul_set lint and suggest #83500: Pull request #21940 opened by urkud
February 16, 2025 03:31 1m 23s YK-mapsTo-smul-set
YK-mapsTo-smul-set
February 16, 2025 03:31 1m 23s
chore: automatically deprime common uses of cases' lint and suggest #83499: Pull request #21939 opened by Parcly-Taxel
February 16, 2025 03:26 1m 33s deprime-cases-automated
deprime-cases-automated
February 16, 2025 03:26 1m 33s
feat: extensible push_neg tactic lint and suggest #83498: Pull request #21769 synchronize by JovanGerb
February 16, 2025 03:21 1m 27s push_neg-Finite
push_neg-Finite
February 16, 2025 03:21 1m 27s
feat: extensible push_neg tactic lint and suggest #83497: Pull request #21769 synchronize by JovanGerb
February 16, 2025 02:55 1m 45s push_neg-Finite
push_neg-Finite
February 16, 2025 02:55 1m 45s
feat(Geometry/Euclidean/Sphere/Basic): diameters lint and suggest #83496: Pull request #21622 synchronize by jsm28
February 16, 2025 02:51 1m 30s jsm28/diameter
jsm28/diameter
February 16, 2025 02:51 1m 30s
feat(Data/List/Triwise): List.Triwise lint and suggest #83495: Pull request #21936 synchronize by jsm28
February 16, 2025 02:47 1m 32s jsm28/triwise
jsm28/triwise
February 16, 2025 02:47 1m 32s
feat(Set/Function): add Semiconj.mapsTo_image_right lint and suggest #83494: Pull request #21938 opened by urkud
February 16, 2025 02:44 1m 40s YK-semiconj-mapsto
YK-semiconj-mapsto
February 16, 2025 02:44 1m 40s
[Merged by Bors] - chore(RingTheory): golf IsPrimitiveRoot.exists_pos lint and suggest #83493: Pull request #21937 opened by erdOne
February 16, 2025 02:41 1m 24s erd1/golfIsPrimitiveRoot
erd1/golfIsPrimitiveRoot
February 16, 2025 02:41 1m 24s
feat(Data/List/Triwise): List.Triwise lint and suggest #83492: Pull request #21936 opened by jsm28
February 16, 2025 02:37 1m 22s jsm28/triwise
jsm28/triwise
February 16, 2025 02:37 1m 22s
feat: extensible push_neg tactic lint and suggest #83491: Pull request #21769 synchronize by JovanGerb
February 16, 2025 02:30 1m 24s push_neg-Finite
push_neg-Finite
February 16, 2025 02:30 1m 24s
feat(NumberTheory): p-adic cyclotomic character lint and suggest #83490: Pull request #21934 synchronize by erdOne
February 16, 2025 02:28 1m 43s erd1/cyclcotomicChar
erd1/cyclcotomicChar
February 16, 2025 02:28 1m 43s
feat(Geometry/Euclidean/Sphere/Basic): diameters lint and suggest #83489: Pull request #21622 synchronize by jsm28
February 16, 2025 02:27 1m 34s jsm28/diameter
jsm28/diameter
February 16, 2025 02:27 1m 34s
feat(Geometry/Euclidean/Sphere/Basic): diameters lint and suggest #83488: Pull request #21622 synchronize by jsm28
February 16, 2025 02:17 1m 41s jsm28/diameter
jsm28/diameter
February 16, 2025 02:17 1m 41s