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
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
chore: specify doc-strings of auto-generated additive declarations di… Autolabel PRs #27755: Pull request #41565 opened by grunweg
1m 22s
1m 22s
chore: unexpose public sections with no defs Autolabel PRs #27754: Pull request #41564 opened by felixpernegger
1m 21s
1m 21s
[Merged by Bors] - chore: update Mathlib dependencies 2026-07-10 Autolabel PRs #27753: Pull request #41563 opened by mathlib-update-dependencies Bot
1m 21s
1m 21s
feat: add the haveILetI linter, flagging haveI/letI in tactic proofs … Autolabel PRs #27752: Pull request #41562 opened by kbuzzard
1m 27s
1m 27s
feat(NumberTheory): use IsApply for ModularForm etc Autolabel PRs #27751: Pull request #41561 opened by mcdoll
1m 18s
1m 18s
feat(Analysis): use IsApply for GroupSeminorm Autolabel PRs #27750: Pull request #41560 opened by mcdoll
1m 29s
1m 29s
chore(Data/List/MinMax): use to_dual Autolabel PRs #27749: Pull request #41559 opened by JovanGerb
1m 25s
1m 25s
chore(order/ConditionallyCompleteLattice): use to_dual more Autolabel PRs #27748: Pull request #41558 opened by JovanGerb
1m 24s
1m 24s
feat(Analysis/Convolution): add convolution_symm, convolution, (3 more lemmas) Autolabel PRs #27747: Pull request #41557 opened by lakesare
1m 27s
1m 27s
feat(RingTheory): add lemmas about reesAlgebra Autolabel PRs #27746: Pull request #41556 opened by Thmoas-Guan
1m 22s
1m 22s
feat(Algebra/Order/Antidiagonal): connect Finset.HasAntidiagonal with Filter.TendstoCofinite Autolabel PRs #27745: Pull request #41555 opened by BryceT233
1m 20s
1m 20s
chore: remove noncomputable section when only theorems in file Autolabel PRs #27744: Pull request #41554 opened by felixpernegger
1m 20s
1m 20s
[Merged by Bors] - chore(CategoryTheory/Sites/Descent/Precoverage): deprecate duplicate theorem Autolabel PRs #27743: Pull request #41553 opened by tb65536
1m 30s
1m 30s
feat(Analysis/Calculus): monotonicity from nonnegative lower right Dini derivative outside a countable set Autolabel PRs #27742: Pull request #41552 opened by benjub
1m 19s
1m 19s