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(LinearAlgebra): characterize triangularizable semisimple endomorphisms Autolabel PRs #27780: Pull request #41590 opened by yuanyi-350
1m 21s
1m 21s
chore(Order/ConditionallyCompletePartialOrder/Indexed): use to_dual more to kill TODO Autolabel PRs #27779: Pull request #41589 opened by yuanyi-350
1m 28s
1m 28s
[Merged by Bors] - chore: use Sort* in the definition of Equiv Autolabel PRs #27778: Pull request #41588 opened by plp127
1m 28s
1m 28s
[Merged by Bors] - chore: refactor bench suite Autolabel PRs #27777: Pull request #41587 opened by Garmelon
1m 19s
1m 19s
[Merged by Bors] - chore: update Mathlib dependencies 2026-07-10 Autolabel PRs #27776: Pull request #41586 opened by mathlib-update-dependencies Bot
1m 25s
1m 25s
chore(Analysis/RCLike/Basic): state norm_I with positive polarity Autolabel PRs #27775: Pull request #41585 opened by kim-em
1m 38s
1m 38s
chore: complete generalization of oneLePart lemmas to DivInvMonoid Autolabel PRs #27774: Pull request #41584 opened by kim-em
1m 36s
1m 36s
chore: move simple_obj into Functor namespace, golf proofs, tidy docstring Autolabel PRs #27773: Pull request #41583 opened by kim-em
1m 38s
1m 38s
chore(Geometry/Euclidean/Sphere): drop unneeded distinctness hypothesis Autolabel PRs #27772: Pull request #41582 opened by kim-em
1m 49s
1m 49s
chore(AlgebraicTopology/Reedy): cosmetic cleanups Autolabel PRs #27771: Pull request #41581 opened by kim-em
1m 32s
1m 32s
chore: golf FormalMultilinearSeries.fderiv_sum Autolabel PRs #27770: Pull request #41580 opened by kim-em
1m 27s
1m 27s
doc: fix docstrings still using the deprecated name CardinalFilteredPoset Autolabel PRs #27769: Pull request #41579 opened by kim-em
1m 33s
1m 33s
chore: weaken hypotheses of Algebra.IsUnramifiedIn.ramificationIdx_eq_one Autolabel PRs #27768: Pull request #41578 opened by kim-em
1m 24s
1m 24s
chore: add gcongr attribute to Nat.ascFactorial_le and Nat.descFactorial_le Autolabel PRs #27767: Pull request #41577 opened by kim-em
1m 12s
1m 12s
chore: use uniqueDiffOn_uIcc at existing call sites Autolabel PRs #27766: Pull request #41576 opened by kim-em
1m 21s
1m 21s
chore(Analysis/RCLike): move I_smul_of_mem_skewAdjoint out of IsSelfAdjoint namespace Autolabel PRs #27765: Pull request #41575 opened by kim-em
1m 8s
1m 8s
doc: remove dangling reference to deleted lemma in asymptotics docstring Autolabel PRs #27764: Pull request #41574 opened by kim-em
1m 20s
1m 20s
doc: fix composition order in Presieve.pullback docstring Autolabel PRs #27763: Pull request #41573 opened by kim-em
1m 10s
1m 10s
feat: IsMulApplyEqComp instances for RelHom/RelEmbedding/RelIso and MulAction (α →o α) α Autolabel PRs #27762: Pull request #41572 opened by kim-em
1m 11s
1m 11s
doc: fix typos in SimplicialSet docstrings Autolabel PRs #27761: Pull request #41571 opened by kim-em
1m 14s
1m 14s
doc: fix and add docstrings in RingTheory/Invariant/Galois Autolabel PRs #27760: Pull request #41570 opened by kim-em
1m 20s
1m 20s
[Merged by Bors] - chore(Topology/DiscreteSubset): fix typo eventualy -> eventually in lemma name Autolabel PRs #27759: Pull request #41569 opened by kim-em
1m 10s
1m 10s
[Merged by Bors] - doc: fix docstring of orthogonalProjectionOnto Autolabel PRs #27758: Pull request #41568 opened by kim-em
1m 21s
1m 21s
doc: fix TFAE list rendering in Rees theorem module docstring Autolabel PRs #27757: Pull request #41567 opened by kim-em
1m 50s
1m 50s
chore: fix malformed deprecation date in Rep/Res Autolabel PRs #27756: Pull request #41566 opened by kim-em
1m 21s
1m 21s