Skip to content

Actions: leanprover-community/mathlib4

Actions

Add "closed-pr" emoji in Zulip

Actions

Loading...
Loading

Show workflow options

Create status badge

Loading
zulip_emoji_closed_pr.yaml
4,900 workflow runs
4,900 workflow runs

Filter by Event

Filter by Status

Filter by Branch

Filter by Actor

[Merged by Bors] - chore: missing fun_prop attribute Add "closed-pr" emoji in Zulip #4884: Pull request #30635 closed by mathlib-bors bot
8s
8s
[Merged by Bors] - feat(CategoryTheory/Monoidal): mapMon of a lax-braided functor is lax-braided Add "closed-pr" emoji in Zulip #4883: Pull request #29136 closed by mathlib-bors bot
12s
12s
[Merged by Bors] - chore(Algebra/ModEq): don't import modules Add "closed-pr" emoji in Zulip #4882: Pull request #30614 closed by mathlib-bors bot
8s
8s
[Merged by Bors] - chore: use grw, gcongr more Add "closed-pr" emoji in Zulip #4881: Pull request #30508 closed by mathlib-bors bot
10s
10s
[Merged by Bors] - chore: mark one lemma as simp Add "closed-pr" emoji in Zulip #4880: Pull request #30529 closed by mathlib-bors bot
12s
12s
[Merged by Bors] - feat: add Finset lemmas Add "closed-pr" emoji in Zulip #4879: Pull request #30539 closed by mathlib-bors bot
8s
8s
[Merged by Bors] - chore: generalize Egorov file to measurable edist assumption Add "closed-pr" emoji in Zulip #4878: Pull request #30604 closed by mathlib-bors bot
11s
11s
feat(RingTheory/TensorProduct/Pi): add piScalarRight_symm_apply_algebraMap Add "closed-pr" emoji in Zulip #4877: Pull request #30611 closed by smmercuri
22s
22s
[Merged by Bors] - fix: Improve definition of SimplexCategoryGenRel.IsAdmissible Add "closed-pr" emoji in Zulip #4876: Pull request #30586 closed by mathlib-bors bot
13s
13s
[Merged by Bors] - feat(CategoryTheory): Exists gives images Add "closed-pr" emoji in Zulip #4875: Pull request #30088 closed by mathlib-bors bot
12s
12s
[Merged by Bors] - doc(Combinatorics): fix typos Add "closed-pr" emoji in Zulip #4874: Pull request #30621 closed by mathlib-bors bot
8s
8s
[Merged by Bors] - feat(Analysis/InnerProductSpace/TensorProduct): LinearIsometry.lTensor and .rTensor Add "closed-pr" emoji in Zulip #4873: Pull request #30613 closed by mathlib-bors bot
12s
12s
[Merged by Bors] - chore(NumberTheory/ArithmeticFunction): remove notation scope Add "closed-pr" emoji in Zulip #4872: Pull request #30465 closed by mathlib-bors bot
10s
10s
[Merged by Bors] - chore(IsPrimitiveRoot): cleanup statement of IsPrimitiveRoot.prime_dvd_of_dvd_norm_sub_one Add "closed-pr" emoji in Zulip #4871: Pull request #30581 closed by mathlib-bors bot
11s
11s
[Merged by Bors] - chore: golf proof for choose_le_two_pow Add "closed-pr" emoji in Zulip #4870: Pull request #30617 closed by mathlib-bors bot
23s
23s
[Merged by Bors] - doc: fixes for Turing machine docs Add "closed-pr" emoji in Zulip #4869: Pull request #30500 closed by mathlib-bors bot
11s
11s
[Merged by Bors] - doc(AlgebraicTopology): fix typos Add "closed-pr" emoji in Zulip #4868: Pull request #30616 closed by mathlib-bors bot
14s
14s
[Merged by Bors] - feat(Positivity): add support for positivity [h₁, h₂] syntax Add "closed-pr" emoji in Zulip #4867: Pull request #30388 closed by mathlib-bors bot
13s
13s
[Merged by Bors] - feat(Data/Nat): define Nat.nthRoot Add "closed-pr" emoji in Zulip #4866: Pull request #28768 closed by mathlib-bors bot
7s
7s
[Merged by Bors] - refactor: define ≤/< on WithBot/WithTop by induction Add "closed-pr" emoji in Zulip #4865: Pull request #19668 closed by mathlib-bors bot
11s
11s
[Merged by Bors] - feat(Analysis/InnerProductSpace): define the inner product on tensor products Add "closed-pr" emoji in Zulip #4864: Pull request #27228 closed by mathlib-bors bot
6s
6s
feat: add ContDiff.lipschitzOnWith Add "closed-pr" emoji in Zulip #4863: Pull request #12673 closed by grunweg
14s
14s
[Merged by Bors] - feat: asymptotic cone of a set Add "closed-pr" emoji in Zulip #4862: Pull request #27292 closed by mathlib-bors bot
6s
6s
[Merged by Bors] - fix: update the continuity lemma library note Add "closed-pr" emoji in Zulip #4861: Pull request #30606 closed by mathlib-bors bot
5s
5s
[Merged by Bors] - chore: rename fields in ImplicitFunctionData Add "closed-pr" emoji in Zulip #4860: Pull request #30607 closed by mathlib-bors bot
8s
8s