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
11,549 workflow runs
11,549 workflow runs

Filter by Event

Filter by Status

Filter by Branch

Filter by Actor

experiment: how many inferInstanceAs can be replaced with inferInstanceAs% (#36420 version) Add "closed-pr" emoji in Zulip #11570: Pull request #36515 closed by kim-em
17s
17s
experiment: rm_set_option.py after greedily deploying #35950's inferInstanceAs% Add "closed-pr" emoji in Zulip #11569: Pull request #36573 closed by kim-em
16s
16s
[Merged by Bors] - refactor: deduplicate PartialOrder (Order.Ideal P) instances Add "closed-pr" emoji in Zulip #11568: Pull request #37467 closed by mathlib-bors bot
7s
7s
[Merged by Bors] - feat(Topology/Algebra/Ring): ContinuousAddEquiv.mulLeft, mulRight Add "closed-pr" emoji in Zulip #11567: Pull request #34193 closed by mathlib-bors bot
8s
8s
[Merged by Bors] - doc(Tactic): fix typos Add "closed-pr" emoji in Zulip #11566: Pull request #37517 closed by mathlib-bors bot
6s
6s
[Merged by Bors] - doc(Order): fix typos Add "closed-pr" emoji in Zulip #11565: Pull request #37519 closed by mathlib-bors bot
8s
8s
[Merged by Bors] - chore: also try dsimp for proving continuity in the Homeomorph fields Add "closed-pr" emoji in Zulip #11564: Pull request #35697 closed by mathlib-bors bot
8s
8s
[Merged by Bors] - feat(AlgebraicGeometry/EllipticCurve/Reduction): define split multiplicative reduction Add "closed-pr" emoji in Zulip #11563: Pull request #35710 closed by mathlib-bors bot
6s
6s
[Merged by Bors] - feat(Algebra/Module/Submodule/Invariant): lemmas for invtSubmodule (f + g) and invtSubmodule (c • f) Add "closed-pr" emoji in Zulip #11562: Pull request #36847 closed by mathlib-bors bot
6s
6s
[Merged by Bors] - chore(Algebra/Order): generalise ordered algebra lemmas Add "closed-pr" emoji in Zulip #11561: Pull request #37040 closed by mathlib-bors bot
5s
5s
[Merged by Bors] - feat(Combinatorics/SimpleGraph): hamiltonian graphs don't contain bridges Add "closed-pr" emoji in Zulip #11560: Pull request #36802 closed by mathlib-bors bot
6s
6s
[Merged by Bors] - chore(RefinedDiscrTree/Lookup): remove reference counting workaround Add "closed-pr" emoji in Zulip #11559: Pull request #36994 closed by mathlib-bors bot
8s
8s
[Merged by Bors] - chore: remove double instance on CommRing (SeparationQuotient α) Add "closed-pr" emoji in Zulip #11558: Pull request #37481 closed by mathlib-bors bot
5s
5s
[Merged by Bors] - feat(Geometry/Manifold): a smooth map induces a morphism of locally ringed spaces Add "closed-pr" emoji in Zulip #11557: Pull request #35661 closed by mathlib-bors bot
5s
5s
[Merged by Bors] - feat(CStarAlgebra): Ring.inverse is convex and antitone on strictly positive operators Add "closed-pr" emoji in Zulip #11556: Pull request #37009 closed by mathlib-bors bot
6s
6s
[Merged by Bors] - chore(Geometry/Convex/Cone): deprecate Convex.toCone Add "closed-pr" emoji in Zulip #11555: Pull request #37392 closed by mathlib-bors bot
8s
8s
[Merged by Bors] - feat(Valuation/Discrete/RankOne): generalize results to Ring Add "closed-pr" emoji in Zulip #11554: Pull request #37497 closed by mathlib-bors bot
7s
7s
refactor: make Ideal.Fiber a one-field structure Add "closed-pr" emoji in Zulip #11553: Pull request #37491 closed by tb65536
15s
15s
chore(RingTheory/LocalRing/ResidueField/Fiber): split file Add "closed-pr" emoji in Zulip #11552: Pull request #37498 closed by tb65536
16s
16s
[Merged by Bors] - chore: remove an instance diamond in homotopy groups Add "closed-pr" emoji in Zulip #11551: Pull request #37485 closed by mathlib-bors bot
7s
7s
[Merged by Bors] - refactor(Topology): redefine Topology.IsQuotientMap with Topology.IsCoinducing Add "closed-pr" emoji in Zulip #11550: Pull request #36957 closed by mathlib-bors bot
9s
9s
[Merged by Bors] - feat(Combinatorics/SimpleGraph/Walk/Operations): clean up append/concat Add "closed-pr" emoji in Zulip #11549: Pull request #36705 closed by mathlib-bors bot
9s
9s
[Merged by Bors] - ci(pre-commit): add hook mixed-line-endings --fix=lf Add "closed-pr" emoji in Zulip #11548: Pull request #37496 closed by mathlib-bors bot
5s
5s
[Merged by Bors] - feat(Combinatorics/SimpleGraph/Maps): every homomorphism f : H →g G factors through id : H →g G.comap f Add "closed-pr" emoji in Zulip #11547: Pull request #37017 closed by mathlib-bors bot
6s
6s
[Merged by Bors] - feat(Topology/Sets): continuity of operations on (Nonempty)Compacts Add "closed-pr" emoji in Zulip #11546: Pull request #34268 closed by mathlib-bors bot
8s
8s