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: finrank is preserved by IsFractionRing Autolabel PRs #27884: Pull request #41694 opened by tb65536
1m 25s
1m 25s
feat: generalize MonoidHom.isStrictMap_prodMap to arbitrary products Autolabel PRs #27883: Pull request #41693 opened by ADedecker
1m 19s
1m 19s
[Merged by Bors] - chore: tweak bench suite Autolabel PRs #27882: Pull request #41692 opened by Garmelon
1m 18s
1m 18s
[Merged by Bors] - feat(SetTheory/Cardinal/ToNat): Cardinal.toNat version of eq_of_forall_le_iff Autolabel PRs #27881: Pull request #41691 opened by tb65536
1m 29s
1m 29s
[Merged by Bors] - chore: bump toolchain to v4.32.0 Autolabel PRs #27880: Pull request #41690 opened by Garmelon
1m 26s
1m 26s
feat: add Homeomorph.Set.univPi Autolabel PRs #27879: Pull request #41689 opened by ADedecker
1m 17s
1m 17s
[Merged by Bors] - feat(RingTheory/Localization/Integer): cardinality of finsetIntegerMultiple Autolabel PRs #27878: Pull request #41688 opened by tb65536
1m 17s
1m 17s
[Merged by Bors] - chore: update Mathlib dependencies 2026-07-13 Autolabel PRs #27877: Pull request #41687 opened by mathlib-update-dependencies Bot
1m 18s
1m 18s
feat: relate Hom.piMap and Subobject.pi Autolabel PRs #27876: Pull request #41686 opened by ADedecker
1m 28s
1m 28s
feat: free modular lattice on three generators Autolabel PRs #27875: Pull request #41685 opened by plp127
2m 26s
2m 26s
feat: API for logarithmic derivatives of meromorphic functions Autolabel PRs #27874: Pull request #41684 opened by kebekus
1m 25s
1m 25s
[Merged by Bors] - feat(Data/Finset/Image): Finset.image as an Equiv Autolabel PRs #27873: Pull request #41683 opened by tb65536
1m 30s
1m 30s
feat(LinearAlgebra/LinearIndependent/Basic): linear independence along faithful algebra maps Autolabel PRs #27872: Pull request #41682 opened by tb65536
1m 18s
1m 18s
[Merged by Bors] - chore: ignore more revisions in .git-blame-ignore-revs Autolabel PRs #27871: Pull request #41681 opened by grunweg
1m 16s
1m 16s
chore: remove redudant haveI/letI in defs Autolabel PRs #27870: Pull request #41680 opened by felixpernegger
1m 26s
1m 26s
[Merged by Bors] - feat(Order/OrderIsoNat+Data/Finset/Sort): add finiteness and identity theorems for linear orders Autolabel PRs #27869: Pull request #41679 opened by paulcadman
1m 16s
1m 16s
refactor(RepresentationTheory): record the concrete binary biproduct Autolabel PRs #27868: Pull request #41678 opened by JX-Mo
1m 17s
1m 17s
feat(MeasureTheory): characterize strong measurability for inner regular measures Autolabel PRs #27867: Pull request #41677 opened by CoolRmal
1m 25s
1m 25s
feat(Topology): prove the Bing-Nagata-Smirnov metrization theorem Autolabel PRs #27866: Pull request #41676 opened by CoolRmal
1m 16s
1m 16s
feat(AlgebraicTopology): pushout diagrams in the filtration of Δ[p] ⊗ Δ[1] Autolabel PRs #27865: Pull request #41675 opened by joelriou
1m 13s
1m 13s
feat(RingTheory/DedekindDomain): add divisor group Autolabel PRs #27864: Pull request #41674 opened by vaca22
1m 25s
1m 25s
[Merged by Bors] - refactor(LinearAlgebra.Matrix.Determinant.Bird): move Bird determinant definitions into a submodule Autolabel PRs #27863: Pull request #41673 opened by paulcadman
1m 17s
1m 17s
[Merged by Bors] - chore(Data/{W}Seq): cleanup flexible linter exceptions Autolabel PRs #27862: Pull request #41672 opened by vlad902
1m 27s
1m 27s
Topology: pseudometrizable spaces are paracompact Autolabel PRs #27861: Pull request #41671 opened by CoolRmal
1m 18s
1m 18s
feat(Topology): add discrete and sigma-discrete families Autolabel PRs #27860: Pull request #41670 opened by CoolRmal
1m 18s
1m 18s
ProTip! You can narrow down the results and go further in time using created:<2026-07-13 or the other filters available.