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/Group/Units/Basic): deduplicate lemmas by generalizing to IsDedekindFiniteMonoid Autolabel PRs #27648: Pull request #41457 opened by NoahW314
1m 19s
1m 19s
chore: fix some ENat-related instances of backward.isDefEq.respectTransparency Autolabel PRs #27647: Pull request #41456 opened by vlad902
1m 28s
1m 28s
[Merged by Bors] - doc(Algebra/GroupWithZero): replace Nonzero M with Nontrivial M Autolabel PRs #27646: Pull request #41455 opened by NoahW314
1m 24s
1m 24s
feat(Topology/ContinuousMap): domMulAct action on bounded continuous maps Autolabel PRs #27645: Pull request #41454 opened by EzequielS2
1m 46s
1m 46s
feat(Algebra/GroupWithZero): prove that Is{Left,Right}CancelMulZero is Dedekind-finite Autolabel PRs #27644: Pull request #41453 opened by NoahW314
1m 27s
1m 27s
feat(Topology/ContinuousMap): domMulAct action on bounded continuous maps Autolabel PRs #27643: Pull request #41452 opened by EzequielS2
1m 22s
1m 22s
feat(Topology/ContinuousMap): domMulAct action on bounded continuous maps Autolabel PRs #27642: Pull request #41451 opened by EzequielS2
1m 30s
1m 30s
chore: remove uses of Subrelation Autolabel PRs #27641: Pull request #41450 opened by chenson2018
1m 24s
1m 24s
feat(Topology/ContinuousMap): domMulAct action on C(X, Y) Autolabel PRs #27640: Pull request #41449 opened by EzequielS2
2m 3s
2m 3s
[Merged by Bors] - doc(LinearAlgebra/Matrix/ToLin): fix typos Autolabel PRs #27639: Pull request #41448 opened by mathlib-splicebot Bot
1m 17s
1m 17s
chore(Combinatorics/SimpleGraph/Trails): golf and cleanup Autolabel PRs #27638: Pull request #41447 opened by SnirBroshi
1m 32s
1m 32s
chore: add missing noncomputable Autolabel PRs #27637: Pull request #41446 opened by YaelDillies
1m 18s
1m 18s
refactor(Order/JordanHolder): remove Iso from JordanHolderLattice Autolabel PRs #27636: Pull request #41445 opened by tb65536
1m 21s
1m 21s
Prove the universal property of SymmetricPower (lift) Autolabel PRs #27635: Pull request #41444 opened by gmcninch-prof
1m 20s
1m 20s
feat(RingTheory/AdjoinRoot): add AdjoinRoot.isFractionRing Autolabel PRs #27634: Pull request #41443 opened by alreadydone
1m 20s
1m 20s
chore(CategoryTheory/Comma/Over/OverClass): refactor OverClass Autolabel PRs #27633: Pull request #41442 opened by tb65536
1m 17s
1m 17s
[Merged by Bors] - chore(GroupTheory/FreeGroup/Basic): automated extraction from #38114 Autolabel PRs #27632: Pull request #41441 opened by mathlib-splicebot Bot
1m 26s
1m 26s
chore(GroupTheory/Schreier): automated extraction from #38114 Autolabel PRs #27631: Pull request #41440 opened by mathlib-splicebot Bot
1m 27s
1m 27s
feat(GroupTheory/Descent): add versions showing finiteness of torsion Autolabel PRs #27630: Pull request #41439 opened by MichaelStollBayreuth
1m 18s
1m 18s
doc(Matrix): mention bundled forms in docstrings Autolabel PRs #27629: Pull request #41438 opened by SnirBroshi
1m 18s
1m 18s
doc: improve calc? tactic docstring Autolabel PRs #27628: Pull request #41437 opened by xixifusi1213-gif
1m 19s
1m 19s
feat(Topology/MetricSpace): add separatesPoints_lipschitzWith_one Autolabel PRs #27627: Pull request #41436 opened by b-mehta
1m 20s
1m 20s
feat(Combinatorics/SimpleGraph/Hamiltonian): a graph with a Hamiltonian path is connected Autolabel PRs #27626: Pull request #41435 opened by SnirBroshi
1m 19s
1m 19s
feat(Logic/Function): add Set.separatesPoints_mono Autolabel PRs #27625: Pull request #41434 opened by b-mehta
1m 23s
1m 23s
feat(Combinatorics/SimpleGraph/Paths): more path/circuit/cycle lemmas Autolabel PRs #27624: Pull request #41433 opened by SnirBroshi
1m 22s
1m 22s