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: 158 new lemmas discovered by a weightless verifier-mediated learner Autolabel PRs #27698: Pull request #41508 opened by jeremiahrthompson
1m 26s
1m 26s
chore(Data): rename setOf to Set.ofPred Autolabel PRs #27697: Pull request #41507 opened by YaelDillies
1m 28s
1m 28s
refactor(Data): make Set a one-field structure Autolabel PRs #27696: Pull request #41506 opened by YaelDillies
1m 21s
1m 21s
feat(GroupTheory): define left-orderable groups Autolabel PRs #27695: Pull request #41505 opened by homeowmorphism
1m 21s
1m 21s
feat: add formula for the j-invariant of an elliptic curve Autolabel PRs #27694: Pull request #41504 opened by Paul-Lez
1m 31s
1m 31s
feat(GRewrite): support strict rewriting in >/≥ Autolabel PRs #27693: Pull request #41503 opened by JovanGerb
1m 31s
1m 31s
[Merged by Bors] - feat(Topology/Algebra/InfiniteSum/NatInt): hasProd versions of ℕ+/ℕ transfer lemmas Autolabel PRs #27692: Pull request #41502 opened by pepamontero
1m 33s
1m 33s
feat(Analysis/Calculus/LipschitzSmooth): baillon-haddad theorem Autolabel PRs #27691: Pull request #41501 opened by FordUniver
1m 21s
1m 21s
[Merged by Bors] - chore(Geometry/Manifold/Submersion): reword 'project intentions' phrase Autolabel PRs #27690: Pull request #41500 opened by grunweg
1m 23s
1m 23s
feat(NumberTheory): add bernoulli'_five, bernoulli'_six and riemannZeta_six Autolabel PRs #27689: Pull request #41499 opened by qdiazblanco
1m 20s
1m 20s
feat(Analysis/SpecificLimits/Normed): ∑ n ^ 2 * r ^ n = r * (1 + r) / (1 - r) ^ 3 Autolabel PRs #27688: Pull request #41498 opened by pepamontero
1m 25s
1m 25s
[Merged by Bors] - chore: remove some redundant classical Autolabel PRs #27687: Pull request #41497 opened by felixpernegger
1m 45s
1m 45s
feat: companion lemmas to MeromorphicOn.exists_ecanonicalDecomp, API for the extended canonical decomposition Autolabel PRs #27686: Pull request #41496 opened by kebekus
1m 28s
1m 28s
feat(Analysis/Calculus/LipschitzSmooth): add descent lemma Autolabel PRs #27685: Pull request #41495 opened by FordUniver
1m 24s
1m 24s
feat(Analysis/Convex): first-order convexity inequalities Autolabel PRs #27684: Pull request #41494 opened by FordUniver
1m 40s
1m 40s
[Merged by Bors] - chore: simplify show _ from by _ to show _ by _ Autolabel PRs #27683: Pull request #41493 opened by kbuzzard
1m 20s
1m 20s
[Merged by Bors] - perf: make valuation unexposed Autolabel PRs #27682: Pull request #41492 opened by smmercuri
1m 25s
1m 25s
feat(NumberTheory/Bernoulli): add bernoulli'_five and bernoulli'_six Autolabel PRs #27681: Pull request #41491 opened by qdiazblanco
1m 19s
1m 19s
refactor: make adicCompletionIntegers a type Autolabel PRs #27680: Pull request #41490 opened by smmercuri
1m 18s
1m 18s
feat(RepresentationTheory/Character): add integral result for character and conjugacy classes Autolabel PRs #27679: Pull request #41489 opened by Yu-Misaka
1m 23s
1m 23s
feat(LinearAlgebra/Dimension/Free): division version of tower law Autolabel PRs #27678: Pull request #41488 opened by artie2000
1m 25s
1m 25s
feat: implement pi-base cross-reference attribute Autolabel PRs #27677: Pull request #41487 opened by Deicyde
1m 17s
1m 17s
feat(Analysis/Convex/Intrinsic): add open segment intrinsic interior results Autolabel PRs #27676: Pull request #41486 opened by TTony2019
1m 17s
1m 17s
feat: multiplication by a regular function in D^n as a CLM (bilin version) Autolabel PRs #27675: Pull request #41485 opened by luigi-massacci
1m 26s
1m 26s
feat(CategoryTheory): kan extensions from isos Autolabel PRs #27674: Pull request #41484 opened by FernandoChu
1m 18s
1m 18s