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
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
[Merged by Bors] - chore(CategoryTheory/Limits): generalise universes in instances for representable functors Autolabel PRs #25841: Pull request #39760 opened by chrisflav
1m 11s
1m 11s
doc(Order/Cofinal): update module docstring (#39756) Autolabel PRs #25840: Commit a6d7083 pushed by mathlib-bors Bot
1m 17s staging-squash-merge.tmp
staging-squash-merge.tmp
1m 17s
[Merged by Bors] - chore(FieldTheory/KrullTopology): move lemmas to earlier file Autolabel PRs #25839: Pull request #39759 opened by plp127
1m 13s
1m 13s
[Merged by Bors] - chore: use skip instead of -failIfUnchanged in the default tactic of Homeomorph Autolabel PRs #25838: Pull request #39758 opened by gasparattila
1m 17s
1m 17s
[Merged by Bors] - chore(Algebra/Star): clean up simp lemmas about bundled star equivalences Autolabel PRs #25837: Pull request #39757 opened by gasparattila
1m 20s
1m 20s
[Merged by Bors] - doc(Order/Cofinal): update module docstring Autolabel PRs #25836: Pull request #39756 opened by vihdzp
1m 16s
1m 16s
chore(GroupTheory): remove a defeq abuse Autolabel PRs #25835: Pull request #39755 opened by wwylele
1m 13s
1m 13s
[Merged by Bors] - feat: the natural filtration of a process is the filtration generated by the process Autolabel PRs #25834: Pull request #39754 opened by EtienneC30
1m 20s
1m 20s
[Merged by Bors] - feat: the sigma-algebra generated by the constant indicator of a set is smaller than the one generated by the set Autolabel PRs #25833: Pull request #39753 opened by mathlib-splicebot Bot
1m 25s
1m 25s
feat(Nat/Digits/Lemma): add a lemma to unfold Nat.digitsAppend Autolabel PRs #25832: Pull request #39752 opened by xroblot
1m 18s
1m 18s
[Merged by Bors] - feat: if a sigma-algebra is independent from itself then all sets in it have measure 0 or 1 Autolabel PRs #25831: Pull request #39750 opened by mathlib-splicebot Bot
1m 17s
1m 17s
[Merged by Bors] - feat: when the indicator is independent from a random variable Autolabel PRs #25830: Pull request #39749 opened by EtienneC30
1m 12s
1m 12s
ProTip! You can narrow down the results and go further in time using created:<2026-05-23 or the other filters available.