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,066 workflow runs
3,066 workflow runs

Filter by Event

Filter by Status

Filter by Branch

Filter by Actor

[Merged by Bors] - chore(Ideal/Basic): dependent generalization of Ideal.pi .github/workflows/zulip_emoji_awaiting_author.yaml #2995: Pull request #20535 labeled by leanprover-community-mathlib4-bot
January 7, 2025 01:48 2s dependent_Ideal.pi
dependent_Ideal.pi
January 7, 2025 01:48 2s
[Merged by Bors] - fix: do not keep only the first line of hints .github/workflows/zulip_emoji_awaiting_author.yaml #2994: Pull request #19756 labeled by leanprover-community-mathlib4-bot
January 7, 2025 01:14 2s eric-wieser/hint-fix
eric-wieser/hint-fix
January 7, 2025 01:14 2s
[Merged by Bors] - chore(Ideal/Basic): dependent generalization of Ideal.pi .github/workflows/zulip_emoji_awaiting_author.yaml #2993: Pull request #20535 labeled by alreadydone
January 7, 2025 01:11 3s dependent_Ideal.pi
dependent_Ideal.pi
January 7, 2025 01:11 3s
chore(Noetherian/Artinian): generalize to Semiring .github/workflows/zulip_emoji_awaiting_author.yaml #2992: Pull request #20534 labeled by alreadydone
January 7, 2025 01:04 2s Semiring_Noetherian_Artinian
Semiring_Noetherian_Artinian
January 7, 2025 01:04 2s
[Merged by Bors] - chore: don't import algebra in Data.Multiset.Basic .github/workflows/zulip_emoji_awaiting_author.yaml #2991: Pull request #19775 labeled by leanprover-community-mathlib4-bot
January 6, 2025 23:37 2s multiset_no_algebra
multiset_no_algebra
January 6, 2025 23:37 2s
[Merged by Bors] - feat(CategoryTheory/Triangulated/Adjunction): the right adjoint of a triangulated functor is triangulated .github/workflows/zulip_emoji_awaiting_author.yaml #2990: Pull request #20255 labeled by joelriou
January 6, 2025 22:52 15s SM.adjointTriangulated
SM.adjointTriangulated
January 6, 2025 22:52 15s
[Merged by Bors] - feat(Analysis): asymptotics of inversion at atBot and 𝓝[<] 0 .github/workflows/zulip_emoji_awaiting_author.yaml #2989: Pull request #19817 labeled by leanprover-community-mathlib4-bot
January 6, 2025 22:27 2s vasnesterov/inv_atBot
vasnesterov/inv_atBot
January 6, 2025 22:27 2s
[Merged by Bors] - feat(Analysis/Analytic): lemmas about smul for power series .github/workflows/zulip_emoji_awaiting_author.yaml #2988: Pull request #19816 labeled by leanprover-community-mathlib4-bot
January 6, 2025 22:23 2s vasnesterov/HasFPowerSeriesOnBall_lemmas
vasnesterov/HasFPowerSeriesOnBall_lemmas
January 6, 2025 22:23 2s
[Merged by Bors] - perf: remove @[simp] on Fintype.card_of{IsEmpty,Subsingleton} .github/workflows/zulip_emoji_awaiting_author.yaml #2987: Pull request #20524 labeled by j-loreaux
January 6, 2025 22:11 3s j-loreaux/remove-simp-Fintype.of
j-loreaux/remove-simp-Fintype.of
January 6, 2025 22:11 3s
[Merged by Bors] - feat: add @[simp] lemma Prod.norm_mk .github/workflows/zulip_emoji_awaiting_author.yaml #2986: Pull request #20411 labeled by leanprover-community-mathlib4-bot
January 6, 2025 22:10 2s YK-prod-norm-mk
YK-prod-norm-mk
January 6, 2025 22:10 2s
[Merged by Bors] - chore: cleanup many erw .github/workflows/zulip_emoji_awaiting_author.yaml #2985: Pull request #20484 labeled by leanprover-community-mathlib4-bot
January 6, 2025 22:04 1s use_simp
use_simp
January 6, 2025 22:04 1s
feat(Analysis/Normed/Group/SeparationQuotient): add normed lifts and mk .github/workflows/zulip_emoji_awaiting_author.yaml #2984: Pull request #18178 labeled by j-loreaux
January 6, 2025 22:02 15s yoh-tanimoto-separationquotient-lift
yoh-tanimoto-separationquotient-lift
January 6, 2025 22:02 15s
feat(RingTheory/Idempotents): generalize to Semiring, add Corner and direct product decomposition .github/workflows/zulip_emoji_awaiting_author.yaml #2983: Pull request #20531 labeled by alreadydone
January 6, 2025 21:59 3s Idempotent_DirectProduct
Idempotent_DirectProduct
January 6, 2025 21:59 3s
feat(Algebra/Ring): generalise and extend material about sums of squares and semireal rings .github/workflows/zulip_emoji_awaiting_author.yaml #2982: Pull request #16094 unlabeled by artie2000
January 6, 2025 21:36 16s real_closed_field_dev
real_closed_field_dev
January 6, 2025 21:36 16s
chore: protect Filter.nhds_{iInf,inf} .github/workflows/zulip_emoji_awaiting_author.yaml #2981: Pull request #20530 labeled by j-loreaux
January 6, 2025 21:24 1s j-loreaux/protect-Filter.nhds_iInf
j-loreaux/protect-Filter.nhds_iInf
January 6, 2025 21:24 1s
chore: protect Filter.nhds_{iInf,inf} .github/workflows/zulip_emoji_awaiting_author.yaml #2980: Pull request #20530 labeled by j-loreaux
January 6, 2025 21:24 2s j-loreaux/protect-Filter.nhds_iInf
j-loreaux/protect-Filter.nhds_iInf
January 6, 2025 21:24 2s
feat(Aesop): Make some SetLike rules unsafe, add new SetLike rules .github/workflows/zulip_emoji_awaiting_author.yaml #2979: Pull request #20477 labeled by artie2000
January 6, 2025 21:23 1s artie2000-aesop-changes
artie2000-aesop-changes
January 6, 2025 21:23 1s
feat(Analysis): summable multipliable .github/workflows/zulip_emoji_awaiting_author.yaml #2978: Pull request #16546 labeled by j-loreaux
January 6, 2025 21:15 14s summable_multipliable
summable_multipliable
January 6, 2025 21:15 14s
[Merged by Bors] - doc: change "module homomorphism" to "linear map" .github/workflows/zulip_emoji_awaiting_author.yaml #2977: Pull request #20481 labeled by leanprover-community-mathlib4-bot
January 6, 2025 20:53 1s trivial1711-linear-map
trivial1711-linear-map
January 6, 2025 20:53 1s
feat(Combinatorics/SimpleGraph/Walk): add penultimate and dropLast .github/workflows/zulip_emoji_awaiting_author.yaml #2976: Pull request #16382 unlabeled by Command-Master
January 6, 2025 20:34 16s CM_wsnd
CM_wsnd
January 6, 2025 20:34 16s
feat(Algebra/Ring): generalise and extend material about sums of squares and semireal rings .github/workflows/zulip_emoji_awaiting_author.yaml #2975: Pull request #16094 labeled by mathlib4-dependent-issues-bot
January 6, 2025 20:34 2s real_closed_field_dev
real_closed_field_dev
January 6, 2025 20:34 2s
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