Skip to content

Actions: leanprover-community/mathlib4

Actions

Autolabel PRs

Actions

Loading...
Loading

Show workflow options

Create status badge

Loading
add_label_from_diff.yaml
2,500+ workflow runs
2,500+ workflow runs

Filter by Event

⌥ + click/return to exclude

Filter by Status

⌥ + click/return to exclude

Filter by Branch

⌥ + click/return to exclude

Filter by Actor

⌥ + click/return to exclude
feat(Algebra): use Is*Apply for LinearMap Autolabel PRs #25720: Pull request #39638 opened by mcdoll
1m 11s
1m 11s
[Merged by Bors] - feat(Topology/Algebra): use Is*Apply for ContinuousLinearMap Autolabel PRs #25719: Pull request #39637 opened by mcdoll
1m 19s
1m 19s
feat(RingTheory/HopfAlgebra): ascending Pochhammer is of binomial type Autolabel PRs #25718: Pull request #39636 opened by RaggedR
1m 19s
1m 19s
feat: club sets (#37677) Autolabel PRs #25717: Commit c724781 pushed by mathlib-bors Bot
1m 11s staging-squash-merge.tmp
staging-squash-merge.tmp
1m 11s
feat(LinearAlgebra/Eigenspace/Matrix): a scalar is in the spectrum iff it's an eigenvalue Autolabel PRs #25716: Pull request #39635 opened by SnirBroshi
1m 21s
1m 21s
chore: fix naming of coeff_C_ne_zero (#39632) Autolabel PRs #25715: Commit ae5f1c0 pushed by mathlib-bors Bot
1m 17s staging-squash-merge.tmp
staging-squash-merge.tmp
1m 17s
[Merged by Bors] - feat(LinearAlgebra/Matrix/Nondegenerate): more API and generalize to non-domains Autolabel PRs #25714: Pull request #39634 opened by SnirBroshi
1m 13s
1m 13s
[Merged by Bors] - doc: module docstrings for files split off from Topology.Algebra.Module.LinearMap Autolabel PRs #25713: Pull request #39633 opened by ADedecker
1m 14s
1m 14s
[Merged by Bors] - chore: fix naming of coeff_C_ne_zero Autolabel PRs #25712: Pull request #39632 opened by justus-springer
1m 15s
1m 15s
chore: make Injective and Surjective fun_propable Autolabel PRs #25711: Pull request #39631 opened by MichaelStollBayreuth
1m 19s
1m 19s
[Merged by Bors] - feat(Sheaves/EtaleSpace): new file Autolabel PRs #25710: Pull request #39630 opened by urkud
1m 14s
1m 14s
[Merged by Bors] - feat(RingTheory/Coalgebra/Convolution): Algebra instance on convolution semiring Autolabel PRs #25709: Pull request #39629 opened by hawkrobe
1m 15s
1m 15s
feat(Geometry/Convex): modules are convex spaces (#39531) Autolabel PRs #25708: Commit bb1f406 pushed by mathlib-bors Bot
1m 34s staging-squash-merge.tmp
staging-squash-merge.tmp
1m 34s
[Merged by Bors] - feat: add ofScientific lemmas for Complex/RCLike/Quaternion Autolabel PRs #25707: Pull request #39628 opened by eric-wieser
2m 45s
2m 45s
feat(Geometry/Convex): modules are convex spaces (#39531) Autolabel PRs #25706: Commit bb1f406 pushed by mathlib-bors Bot
2m 11s staging-squash-merge.tmp
staging-squash-merge.tmp
2m 11s
feat(Combinatorics/SimpleGraph/LapMatrix): 0 is always an eigenvalue Autolabel PRs #25705: Pull request #39627 opened by SnirBroshi
1m 33s
1m 33s
[Merged by Bors] - feat(RingTheory/MvPowerSeries): partial derivatives of MvPowerSeries Autolabel PRs #25704: Pull request #39626 opened by justus-springer
1m 51s
1m 51s
[Merged by Bors] - feat(RingTheory/MvPowerSeries/Trunc): generalize truncation lemmas Autolabel PRs #25703: Pull request #39625 opened by justus-springer
2m 17s
2m 17s
[Merged by Bors] - feat(Algebra/MvPolynomial/PDeriv): a coefficient formula for pderiv Autolabel PRs #25702: Pull request #39624 opened by justus-springer
1m 17s
1m 17s
[Merged by Bors] - feat(Algebra/MvPolynomial/Basic): coeff_C_of_ne_zero and coeff_add_single_C Autolabel PRs #25701: Pull request #39623 opened by justus-springer
1m 59s
1m 59s
feat(CategoryTheory): add a grind propagator that normalizes morphism composition Autolabel PRs #25700: Pull request #39622 opened by kim-em
1m 36s
1m 36s
[Merged by Bors] - refactor(Topology): use WithTopology to define WithConstructibleTopology Autolabel PRs #25699: Pull request #39621 opened by chrisflav
1m 18s
1m 18s
[Merged by Bors] - feat: missing nnratCast lemmas for RCLike Autolabel PRs #25698: Pull request #39620 opened by eric-wieser
1m 16s
1m 16s
feat(CategoryTheory): the bicategory of profunctors Autolabel PRs #25697: Pull request #39619 opened by dagurtomas
1m 24s
1m 24s
feat(CategoryTheory/Subobject): Heyting algebra structure on Subobject in elementary topoi Autolabel PRs #25696: Pull request #39618 opened by node0000
1m 22s
1m 22s
ProTip! You can narrow down the results and go further in time using created:<2026-05-20 or the other filters available.