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
[Merged by Bors] - refactor(RingTheory/HopfAlgebra): ofConvInverse constructor Autolabel PRs #25866: Pull request #39785 opened by hawkrobe
1m 11s
1m 11s
[Merged by Bors] - chore(Analysis/InnerProductSpace/JointEigenspace): Remove duplicated namespace in name of LinearMap.IsSymmetric.directSum_isInternal_of_pairwise_commute Autolabel PRs #25865: Pull request #39784 opened by JonBannon
1m 11s
1m 11s
feat(Order/Interval/Finset): Set.ncard lemmas for LocallyFiniteOrder Autolabel PRs #25864: Pull request #39783 opened by SnirBroshi
1m 14s
1m 14s
feat(Tactic): nonempty attribute Autolabel PRs #25863: Pull request #39782 opened by robin-carlier
1m 13s
1m 13s
feat(Order/WellFoundedSet): partial-ordered codomain of a monotone surjective from α × β is well-founded give well-ordered α and β Autolabel PRs #25862: Pull request #39781 opened by Hagb
1m 13s
1m 13s
chore: test fast_instance% everywhere Autolabel PRs #25861: Pull request #39780 opened by riccardobrasca
1m 18s
1m 18s
feat(Order/WellFoundedSet): a set is finite if both a linear order and its opposite order are well founded on it Autolabel PRs #25860: Pull request #39779 opened by Hagb
1m 11s
1m 11s
[Merged by Bors] - feat(Projectivization/Independence): add lemma about independence Autolabel PRs #25859: Pull request #39778 opened by Whysoserioushah
1m 20s
1m 20s
[Merged by Bors] - feat(Order/WellFoundedSet): minimal element of a nonempty set exists if < is well founded on the set Autolabel PRs #25858: Pull request #39777 opened by Hagb
1m 14s
1m 14s
[Merged by Bors] - feat(Logic/Function/Basic) : lemmas about composition of and in onFun Autolabel PRs #25857: Pull request #39776 opened by Hagb
1m 11s
1m 11s
[Merged by Bors] - feat(Order/WellFounded): wellFounded_{lt,gt}.min is {Minimal,Maximal} Autolabel PRs #25856: Pull request #39775 opened by Hagb
1m 20s
1m 20s
feat(Order/WellFounded): WellFounded on subtype iff the relation restricted on the subtype is WellFounded Autolabel PRs #25855: Pull request #39774 opened by Hagb
1m 18s
1m 18s
perf: add some fast_instance% Autolabel PRs #25854: Pull request #39773 opened by kbuzzard
1m 20s
1m 20s
perf(Algebra/Ring/Defs): unfold the new Semiring instances Autolabel PRs #25853: Pull request #39772 opened by JovanGerb
1m 20s
1m 20s
feat(GroupTheory/PCore): define the p-core of a subgroup Autolabel PRs #25852: Pull request #39771 opened by kim-em
1m 12s
1m 12s
[Merged by Bors] - feat: atoms of a countably generated measurable space Autolabel PRs #25851: Pull request #39770 opened by mathlib-splicebot Bot
1m 11s
1m 11s
chore(Topology): refactor proofs where grind? fails Autolabel PRs #25850: Pull request #39769 opened by chenson2018
1m 9s
1m 9s
[Merged by Bors] - feat: another version of dominated convergence for AEMeasurable functions Autolabel PRs #25849: Pull request #39768 opened by mathlib-splicebot Bot
1m 9s
1m 9s
[Merged by Bors] - feat: add an alias for the forward direction of indepFun_iff_map_prod_eq_prod_map_map Autolabel PRs #25848: Pull request #39767 opened by EtienneC30
1m 18s
1m 18s
[Merged by Bors] - feat(Topology/Algebra/Module): call eta_expand in the default tactic of ContinuousLinearEquiv Autolabel PRs #25847: Pull request #39766 opened by gasparattila
1m 18s
1m 18s
[Merged by Bors] - doc(RingTheory): fix local ring doc comment Autolabel PRs #25846: Pull request #39765 opened by vlad902
1m 23s
1m 23s
[Merged by Bors] - feat(Module/Projective): direct sum of projective modules is projective Autolabel PRs #25845: Pull request #39764 opened by vlad902
1m 21s
1m 21s
feat(Algebra/GroupWithZero/Divisibility): add mul_dvd_left_iff_isUnit Autolabel PRs #25844: Pull request #39763 opened by NoahW314
1m 9s
1m 9s
[Merged by Bors] - chore(Topology/UniformSpace): rename uniformContinuous_iff to uniformContinuous_iff_le_comap Autolabel PRs #25843: Pull request #39762 opened by plp127
1m 11s
1m 11s
[Merged by Bors] - chore(scripts): update nolints.json Autolabel PRs #25842: Pull request #39761 opened by mathlib-nolints Bot
1m 13s
1m 13s
ProTip! You can narrow down the results and go further in time using created:<2026-05-24 or the other filters available.