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,899 workflow runs
4,899 workflow runs

Filter by Event

Filter by Status

Filter by Branch

Filter by Actor

[Merged by Bors] - chore: use positivity [h, h'] once more Add "closed-pr" emoji in Zulip #4908: Pull request #30656 closed by mathlib-bors bot
5s
5s
[Merged by Bors] - feat: Field, FiniteDimensional and Algebra.IsSeparable instances for WithAbs Add "closed-pr" emoji in Zulip #4907: Pull request #27974 closed by mathlib-bors bot
5s
5s
[Merged by Bors] - feat(Analysis): PathConnectedSpace ℂˣ Add "closed-pr" emoji in Zulip #4906: Pull request #30418 closed by mathlib-bors bot
9s
9s
[Merged by Bors] - chore: use the positivity [h, h'] syntax when useful Add "closed-pr" emoji in Zulip #4905: Pull request #30654 closed by mathlib-bors bot
6s
6s
[Merged by Bors] - feat(Analysis/InnerProductSpace/Positive): U.starProjection ≤ V.starProjection iff U ≤ V Add "closed-pr" emoji in Zulip #4904: Pull request #27162 closed by mathlib-bors bot
6s
6s
[Merged by Bors] - chore: move isProperMap_iff_isClosedMap_filter next to the ultrafilter version Add "closed-pr" emoji in Zulip #4903: Pull request #30409 closed by mathlib-bors bot
7s
7s
[Merged by Bors] - feat: the action underlying a topological additive torsor is proper Add "closed-pr" emoji in Zulip #4902: Pull request #30411 closed by mathlib-bors bot
7s
7s
[Merged by Bors] - refactor(AlgebraicGeometry) : an argument is incorrectly explicit Add "closed-pr" emoji in Zulip #4901: Pull request #30629 closed by mathlib-bors bot
7s
7s
[Merged by Bors] - feat(LinearAlgebra/Matrix/PosDef): kronecker of positive (semi-)definite matrices is positive (semi-)definite Add "closed-pr" emoji in Zulip #4900: Pull request #28097 closed by mathlib-bors bot
6s
6s
[Merged by Bors] - chore(AlgebraicTopology): clean up FundamentalGroupoid Add "closed-pr" emoji in Zulip #4899: Pull request #28234 closed by mathlib-bors bot
4s
4s
[Merged by Bors] - feat(FieldTheory): abelian extensions Add "closed-pr" emoji in Zulip #4898: Pull request #23669 closed by mathlib-bors bot
7s
7s
[Merged by Bors] - chore: remove @[gcongr] from opow_le_opow_right Add "closed-pr" emoji in Zulip #4897: Pull request #30651 closed by mathlib-bors bot
4s
4s
[Merged by Bors] - feat(Algebra/Order/Module): add missing instances Add "closed-pr" emoji in Zulip #4896: Pull request #30544 closed by mathlib-bors bot
8s
8s
[Merged by Bors] - feat(Analysis): semilinearize ContinuousLinearMapWOT Add "closed-pr" emoji in Zulip #4895: Pull request #30597 closed by mathlib-bors bot
4s
4s
[Merged by Bors] - feat: a topological group acts on itself properly Add "closed-pr" emoji in Zulip #4894: Pull request #30387 closed by mathlib-bors bot
7s
7s
x feat(Algebra): generalize Picard group to semirings Add "closed-pr" emoji in Zulip #4893: Pull request #30624 closed by alreadydone
24s
24s
x feat(Algebra): generalize ModuleCat to Semiring Add "closed-pr" emoji in Zulip #4892: Pull request #30636 closed by alreadydone
15s
15s
[Merged by Bors] - chore(Analysis/Matrix/Order): IsStrictlyPositive x iff x.PosDef Add "closed-pr" emoji in Zulip #4891: Pull request #30050 closed by mathlib-bors bot
6s
6s
[Merged by Bors] - refactor(Analysis/InnerProductSpace/Positive): generalize positivity to use IsSymmetric instead of IsSelfAdjoint and CompleteSpace Add "closed-pr" emoji in Zulip #4890: Pull request #30000 closed by mathlib-bors bot
8s
8s
[Merged by Bors] - feat(Topology/Connected): locally (path-)connected compact spaces have finitely many (path-)connected components Add "closed-pr" emoji in Zulip #4889: Pull request #30316 closed by mathlib-bors bot
9s
9s
[Merged by Bors] - chore(Analysis/SpecialFunctions/CFC/Rpow/Basic): extra TFAE conditions for nonnegativity Add "closed-pr" emoji in Zulip #4888: Pull request #30340 closed by mathlib-bors bot
7s
7s
[Merged by Bors] - feat: Finsupp.comapDomain_surjective Add "closed-pr" emoji in Zulip #4887: Pull request #29756 closed by mathlib-bors bot
11s
11s
[Merged by Bors] - feat: add module instance to ContDiffMapSupportedIn Add "closed-pr" emoji in Zulip #4886: Pull request #30198 closed by mathlib-bors bot
5s
5s
[Merged by Bors] - chore(Algebra/Group/EvenFunction): don't import torsion-free modules Add "closed-pr" emoji in Zulip #4885: Pull request #30628 closed by mathlib-bors bot
5s
5s
[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