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 to_dual for DedekindCut Autolabel PRs #27738: Pull request #41548 opened by JovanGerb
1m 22s
1m 22s
[Merged by Bors] - ci: run lake cache shadow pipeline with patched lake version with latest features Autolabel PRs #27737: Pull request #41547 opened by marcelolynch
1m 29s
1m 29s
feat: the product of vector measures Autolabel PRs #27736: Pull request #41546 opened by sgouezel
1m 21s
1m 21s
feat(RepresentationTheory/Homological/ContCohomology): add inflation maps in continuous cohomology Autolabel PRs #27735: Pull request #41545 opened by rmhi
1m 35s
1m 35s
refactor(Algebra/Polynomial): make coeff return a Finsupp Autolabel PRs #27734: Pull request #41544 opened by YaelDillies
1m 35s
1m 35s
[Merged by Bors] - refactor(NumberTheory): make InfinitePlace.Completion a one-field structure Autolabel PRs #27733: Pull request #41543 opened by smmercuri
1m 21s
1m 21s
refactor(AlgebraicGeometry/Sites/Small): golf and remove defeqs Autolabel PRs #27732: Pull request #41542 opened by tb65536
1m 19s
1m 19s
chore: prefer classical over open scoped Classical in proofs Autolabel PRs #27731: Pull request #41541 opened by felixpernegger
1m 21s
1m 21s
chore: rename arguments of Nat.strong_induction_on Autolabel PRs #27730: Pull request #41540 opened by plp127
1m 18s
1m 18s
chore(RepresentationTheory/Homological/ContCohomology): refactor functoriality Autolabel PRs #27729: Pull request #41539 opened by rmhi
1m 34s
1m 34s
feat(Algebra/Quaternion): quaternion are central simple Autolabel PRs #27728: Pull request #41538 opened by Mathias-Stout
1m 31s
1m 31s
feat(RingTheory/TwoSidedIdeal/Lattice): add lemmas on two-sided ideals Autolabel PRs #27727: Pull request #41537 opened by Mathias-Stout
1m 20s
1m 20s
chore(Algebra): make quaternion directory Autolabel PRs #27726: Pull request #41536 opened by Mathias-Stout
1m 31s
1m 31s
[Merged by Bors] - chore: move dualDistribEquiv Autolabel PRs #27725: Pull request #41535 opened by YaelDillies
1m 25s
1m 25s
feat(Geometry/Manifold): add ContMDiffConstSMul typeclass Autolabel PRs #27724: Pull request #41534 opened by qdiazblanco
20m 13s
20m 13s
refactor: notation for EventuallyEq on Set Autolabel PRs #27723: Pull request #41533 opened by YaelDillies
1m 28s
1m 28s
chore: remove all unneeded classical Autolabel PRs #27722: Pull request #41532 opened by felixpernegger
1m 29s
1m 29s
feat: scalar multiplication as a CLM on D^n Autolabel PRs #27721: Pull request #41531 opened by luigi-massacci
1m 29s
1m 29s
feat(CategoryTheory): pasting for kan extensions Autolabel PRs #27720: Pull request #41530 opened by FernandoChu
1m 30s
1m 30s
feat: Émile Borel's classic "Growth Lemma" Autolabel PRs #27719: Pull request #41529 opened by kebekus
1m 36s
1m 36s
[Merged by Bors] - feat(RingTheory/PicardGroup): invertible modules over semirings are locally free Autolabel PRs #27718: Pull request #41528 opened by alreadydone
1m 19s
1m 19s
[Merged by Bors] - feat(Topology/Algebra/ValuativeTopology): checking IsValuativeTopology using any compatible valuation Autolabel PRs #27717: Pull request #41527 opened by mathlib-splicebot Bot
1m 39s
1m 39s
[Merged by Bors] - refactor(NumberTheory): make adicCompletion a one-field structure Autolabel PRs #27716: Pull request #41526 opened by smmercuri
1m 29s
1m 29s
feat(RepresentationTheory): add Smooth.Basic for smooth representations Autolabel PRs #27715: Pull request #41525 opened by JX-Mo
1m 18s
1m 18s
feat(SimpleGraph/Trails): in a preconnected Eulerian graph there exists an Eulerian circuit from any vertex Autolabel PRs #27714: Pull request #41524 opened by SnirBroshi
1m 14s
1m 14s