Skip to content

Actions: leanprover-community/mathlib4

Actions

.github/workflows/zulip_emoji_awaiting_author.yaml

Actions

Loading...
Loading

Show workflow options

Create status badge

Loading
zulip_emoji_awaiting_author.yaml
3,070 workflow runs
3,070 workflow runs

Filter by Event

Filter by Status

Filter by Branch

Filter by Actor

refactor(Topology/UniformSpace/Completion): more descriptive names for α → Completion α .github/workflows/zulip_emoji_awaiting_author.yaml #2974: Pull request #20527 unlabeled by trivial1711
January 6, 2025 20:28 3s trivial1711-coeAddHom
trivial1711-coeAddHom
January 6, 2025 20:28 3s
[Merged by Bors] - fix: silence the #-command linter on noisy commands .github/workflows/zulip_emoji_awaiting_author.yaml #2973: Pull request #20525 labeled by leanprover-community-mathlib4-bot
January 6, 2025 20:16 1s adomani/silence_hash_command_linter_when_messages_are_present
adomani/silence_hash_command_linter_when_messages_are_present
January 6, 2025 20:16 1s
[Merged by Bors] - perf: improves the performance of the Repr (Equiv.Perm α) instance (1/4) .github/workflows/zulip_emoji_awaiting_author.yaml #2972: Pull request #20519 labeled by leanprover-community-mathlib4-bot
January 6, 2025 19:56 2s Komyyy/Equiv.Perm.instRepr3
Komyyy/Equiv.Perm.instRepr3
January 6, 2025 19:56 2s
[Merged by Bors] - chore: to_additive various results on groups, group actions .github/workflows/zulip_emoji_awaiting_author.yaml #2971: Pull request #20498 labeled by leanprover-community-mathlib4-bot
January 6, 2025 19:55 2s ACL/Primitive-1
ACL/Primitive-1
January 6, 2025 19:55 2s
[Merged by Bors] - fix: silence the #-command linter on noisy commands .github/workflows/zulip_emoji_awaiting_author.yaml #2970: Pull request #20525 labeled by leanprover-community-mathlib4-bot
January 6, 2025 19:44 2s adomani/silence_hash_command_linter_when_messages_are_present
adomani/silence_hash_command_linter_when_messages_are_present
January 6, 2025 19:44 2s
feat(Combinatorics/SimpleGraph/Walk): add penultimate and dropLast .github/workflows/zulip_emoji_awaiting_author.yaml #2969: Pull request #16382 labeled by YaelDillies
January 6, 2025 19:24 13s CM_wsnd
CM_wsnd
January 6, 2025 19:24 13s
feat(Algebra/Ring): generalise and extend material about sums of squares and semireal rings .github/workflows/zulip_emoji_awaiting_author.yaml #2968: Pull request #16094 labeled by YaelDillies
January 6, 2025 18:37 21s real_closed_field_dev
real_closed_field_dev
January 6, 2025 18:37 21s
feat(Algebra/Category/Grp/LargeColimits): large colimits in the category of commutative additive groups .github/workflows/zulip_emoji_awaiting_author.yaml #2967: Pull request #20522 labeled by mathlib4-dependent-issues-bot
January 6, 2025 17:46 1s SM.bigColimit
SM.bigColimit
January 6, 2025 17:46 1s
feat(Data/Finset/Card): of cardinality between .github/workflows/zulip_emoji_awaiting_author.yaml #2966: Pull request #20433 labeled by madvorak
January 6, 2025 17:45 2s finset-of-card-between
finset-of-card-between
January 6, 2025 17:45 2s
feat(Data/Finset/Card): of cardinality between .github/workflows/zulip_emoji_awaiting_author.yaml #2965: Pull request #20433 unlabeled by madvorak
January 6, 2025 17:44 16s finset-of-card-between
finset-of-card-between
January 6, 2025 17:44 16s
feat(Algebra/Category/Grp/LargeColimits): large colimits in the category of commutative additive groups .github/workflows/zulip_emoji_awaiting_author.yaml #2964: Pull request #20522 labeled by smorel394
January 6, 2025 17:41 2s SM.bigColimit
SM.bigColimit
January 6, 2025 17:41 2s
[Merged by Bors] - chore(*): replace no_index (ofNat n) with ofNat(n) everywhere .github/workflows/zulip_emoji_awaiting_author.yaml #2963: Pull request #20521 labeled by leanprover-community-mathlib4-bot
January 6, 2025 17:27 1s add-ofNat-macro
add-ofNat-macro
January 6, 2025 17:27 1s
feat(Algebra/Ring): generalise and extend material about sums of squares and semireal rings .github/workflows/zulip_emoji_awaiting_author.yaml #2962: Pull request #16094 unlabeled by mathlib4-dependent-issues-bot
January 6, 2025 17:22 3s real_closed_field_dev
real_closed_field_dev
January 6, 2025 17:22 3s
feat(Combinatorics/SimpleGraph/Walk): add penultimate and dropLast .github/workflows/zulip_emoji_awaiting_author.yaml #2961: Pull request #16382 unlabeled by leanprover-community-bot-assistant
January 6, 2025 16:54 2s CM_wsnd
CM_wsnd
January 6, 2025 16:54 2s
[Merged by Bors] - feat(RingTheory/Ideal): 37 cast to an ideal is just the whole ring. .github/workflows/zulip_emoji_awaiting_author.yaml #2960: Pull request #20244 labeled by leanprover-community-mathlib4-bot
January 6, 2025 16:52 3s nat-ideal-eq-top
nat-ideal-eq-top
January 6, 2025 16:52 3s
[Merged by Bors] - chore(*): replace no_index (ofNat n) with ofNat(n) everywhere .github/workflows/zulip_emoji_awaiting_author.yaml #2959: Pull request #20521 labeled by Vierkantor
January 6, 2025 16:20 3s add-ofNat-macro
add-ofNat-macro
January 6, 2025 16:20 3s
chore(Algebra/Algebra/Defs): add an algebraMap field to Algebra instead of extending RingHom .github/workflows/zulip_emoji_awaiting_author.yaml #2958: Pull request #20518 unlabeled by edegeltje
January 6, 2025 16:20 2s blizzard_inc/fieldify_algebraMap
blizzard_inc/fieldify_algebraMap
January 6, 2025 16:20 2s
[Merged by Bors] - feat(RingTheory): being unramified is a local property .github/workflows/zulip_emoji_awaiting_author.yaml #2957: Pull request #20323 unlabeled by erdOne
January 6, 2025 16:18 17s erd1/localUnramified
erd1/localUnramified
January 6, 2025 16:18 17s
perf: improves the performance of the Repr (Equiv.Perm α) instance (3/4) .github/workflows/zulip_emoji_awaiting_author.yaml #2956: Pull request #12610 labeled by Komyyy
January 6, 2025 16:14 2s Komyyy/Equiv.Perm.instRepr
Komyyy/Equiv.Perm.instRepr
January 6, 2025 16:14 2s
[Merged by Bors] - chore: don't import algebra in Data.Multiset.Basic .github/workflows/zulip_emoji_awaiting_author.yaml #2955: Pull request #19775 unlabeled by leanprover-community-bot-assistant
January 6, 2025 16:09 2s multiset_no_algebra
multiset_no_algebra
January 6, 2025 16:09 2s
chore(Algebra/Algebra/Defs): add an algebraMap field to Algebra instead of extending RingHom .github/workflows/zulip_emoji_awaiting_author.yaml #2954: Pull request #20518 labeled by edegeltje
January 6, 2025 16:02 2s blizzard_inc/fieldify_algebraMap
blizzard_inc/fieldify_algebraMap
January 6, 2025 16:02 2s
chore(Algebra/Algebra/Defs): add an algebraMap field to Algebra instead of extending RingHom .github/workflows/zulip_emoji_awaiting_author.yaml #2953: Pull request #20518 labeled by edegeltje
January 6, 2025 16:02 2s blizzard_inc/fieldify_algebraMap
blizzard_inc/fieldify_algebraMap
January 6, 2025 16:02 2s
[Merged by Bors] - perf: improves the performance of the Repr (Equiv.Perm α) instance (1/4) .github/workflows/zulip_emoji_awaiting_author.yaml #2952: Pull request #20519 labeled by Komyyy
January 6, 2025 16:02 3s Komyyy/Equiv.Perm.instRepr3
Komyyy/Equiv.Perm.instRepr3
January 6, 2025 16:02 3s
[Merged by Bors] - perf: improves the performance of the Repr (Equiv.Perm α) instance (1/4) .github/workflows/zulip_emoji_awaiting_author.yaml #2951: Pull request #20519 labeled by Komyyy
January 6, 2025 16:02 2s Komyyy/Equiv.Perm.instRepr3
Komyyy/Equiv.Perm.instRepr3
January 6, 2025 16:02 2s
[Merged by Bors] - feat: A disjoint union is finite iff all sets are finite, and all but finitely many are empty .github/workflows/zulip_emoji_awaiting_author.yaml #2950: Pull request #20457 labeled by leanprover-community-mathlib4-bot
January 6, 2025 15:56 1s SG_carleson3
SG_carleson3
January 6, 2025 15:56 1s